Skip to content

Commit 403afed

Browse files
author
ros
committed
Apron Prototyp und kleines Beispiel
1 parent b6502ed commit 403afed

11 files changed

+996
-0
lines changed

‎src/org/sosy_lab/java_smt/solvers/apron/ApronBooleanFormulaManager.java

+80
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,80 @@
1+
/*
2+
* JavaSMT is an API wrapper for a collection of SMT solvers.
3+
* This file is part of JavaSMT.
4+
*
5+
* Copyright (C) 2007-2016 Dirk Beyer
6+
* All rights reserved.
7+
*
8+
* Licensed under the Apache License, Version 2.0 (the "License");
9+
* you may not use this file except in compliance with the License.
10+
* You may obtain a copy of the License at
11+
*
12+
* http://www.apache.org/licenses/LICENSE-2.0
13+
*
14+
* Unless required by applicable law or agreed to in writing, software
15+
* distributed under the License is distributed on an "AS IS" BASIS,
16+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
17+
* See the License for the specific language governing permissions and
18+
* limitations under the License.
19+
*/
20+
21+
package org.sosy_lab.java_smt.solvers.apron;
22+
23+
import org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager;
24+
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
25+
26+
public class ApronBooleanFormulaManager extends AbstractBooleanFormulaManager {
27+
protected ApronBooleanFormulaManager(FormulaCreator pCreator) {
28+
super(pCreator);
29+
}
30+
31+
@Override
32+
protected Object makeVariableImpl(String pVar) {
33+
return null;
34+
}
35+
36+
@Override
37+
protected Object makeBooleanImpl(boolean value) {
38+
return null;
39+
}
40+
41+
@Override
42+
protected Object not(Object pParam1) {
43+
return null;
44+
}
45+
46+
@Override
47+
protected Object and(Object pParam1, Object pParam2) {
48+
return null;
49+
}
50+
51+
@Override
52+
protected Object or(Object pParam1, Object pParam2) {
53+
return null;
54+
}
55+
56+
@Override
57+
protected Object xor(Object pParam1, Object pParam2) {
58+
return null;
59+
}
60+
61+
@Override
62+
protected Object equivalence(Object bits1, Object bits2) {
63+
return null;
64+
}
65+
66+
@Override
67+
protected boolean isTrue(Object bits) {
68+
return false;
69+
}
70+
71+
@Override
72+
protected boolean isFalse(Object bits) {
73+
return false;
74+
}
75+
76+
@Override
77+
protected Object ifThenElse(Object cond, Object f1, Object f2) {
78+
return null;
79+
}
80+
}

‎src/org/sosy_lab/java_smt/solvers/apron/ApronExamples.java

+75
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,75 @@
1+
/*
2+
* JavaSMT is an API wrapper for a collection of SMT solvers.
3+
* This file is part of JavaSMT.
4+
*
5+
* Copyright (C) 2007-2016 Dirk Beyer
6+
* All rights reserved.
7+
*
8+
* Licensed under the Apache License, Version 2.0 (the "License");
9+
* you may not use this file except in compliance with the License.
10+
* You may obtain a copy of the License at
11+
*
12+
* http://www.apache.org/licenses/LICENSE-2.0
13+
*
14+
* Unless required by applicable law or agreed to in writing, software
15+
* distributed under the License is distributed on an "AS IS" BASIS,
16+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
17+
* See the License for the specific language governing permissions and
18+
* limitations under the License.
19+
*/
20+
21+
package org.sosy_lab.java_smt.solvers.apron;
22+
23+
import java.util.Arrays;
24+
import apron.*;
25+
import org.junit.AssumptionViolatedException;
26+
import org.sosy_lab.common.NativeLibraries;
27+
28+
/**
29+
* Simple examples about the Apron Library. Inspired by
30+
* <a href="https://github.com/antoinemine/apron/blob/master/examples/example1.c">...</a>
31+
*/
32+
public class ApronExamples
33+
{
34+
private static void testBox(Manager pManager) throws ApronException {
35+
String[] intVars = {"x"};
36+
String[] realVars = {};
37+
38+
Environment environment = new Environment(intVars, realVars);
39+
//x <= 2 and x >= -3
40+
41+
//x <= 2 --> -x+2 >= 0
42+
Lincons1 cons1 = new Lincons1(environment);
43+
cons1.setCoeff("x",new MpqScalar(-1));
44+
cons1.setCst(new MpqScalar(+2));
45+
cons1.setKind(Lincons1.SUPEQ);
46+
//x >= 3 --> x-3 >= 0
47+
Lincons1 cons2 = new Lincons1(environment);
48+
cons2.setCoeff("x",new MpqScalar(1));
49+
cons2.setCst(new MpqScalar(-3));
50+
cons2.setKind(Lincons1.SUPEQ);
51+
52+
Lincons1[] constraints = {cons1, cons2};
53+
Abstract1 abstract1 = new Abstract1(pManager, constraints);
54+
//is x = 1 satisfiable?
55+
Lincons1 cons3 = new Lincons1(environment);
56+
cons3.setCoeff("x",new MpqScalar(1));
57+
cons3.setCst(new MpqScalar(-1));
58+
cons3.setKind(Lincons1.EQ);
59+
System.out.println("Constraint is satisfiable: "+abstract1.satisfy(pManager, cons3));
60+
61+
//always unsat example, 1 = 0
62+
Lincons1 cons4 = new Lincons1(environment);
63+
cons4.setCoeff("x", new MpqScalar(0));
64+
cons4.setCst(new MpqScalar(1));
65+
cons4.setKind(Lincons1.EQ);
66+
Abstract1 abstract2 = new Abstract1(pManager, new Lincons1[]{cons4});
67+
System.out.println("Abstract-Obj. is Bottom: "+abstract2.isBottom(pManager));
68+
}
69+
70+
public static void main(String[] args) throws ApronException {
71+
Manager manager = new Box();
72+
testBox(manager);
73+
}
74+
}
75+

‎src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaCreator.java

+86
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,86 @@
1+
/*
2+
* JavaSMT is an API wrapper for a collection of SMT solvers.
3+
* This file is part of JavaSMT.
4+
*
5+
* Copyright (C) 2007-2016 Dirk Beyer
6+
* All rights reserved.
7+
*
8+
* Licensed under the Apache License, Version 2.0 (the "License");
9+
* you may not use this file except in compliance with the License.
10+
* You may obtain a copy of the License at
11+
*
12+
* http://www.apache.org/licenses/LICENSE-2.0
13+
*
14+
* Unless required by applicable law or agreed to in writing, software
15+
* distributed under the License is distributed on an "AS IS" BASIS,
16+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
17+
* See the License for the specific language governing permissions and
18+
* limitations under the License.
19+
*/
20+
21+
package org.sosy_lab.java_smt.solvers.apron;
22+
23+
import java.util.List;
24+
import javax.annotation.Nullable;
25+
import org.sosy_lab.java_smt.api.Formula;
26+
import org.sosy_lab.java_smt.api.FormulaType;
27+
import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
28+
import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
29+
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
30+
31+
public class ApronFormulaCreator extends FormulaCreator {
32+
protected ApronFormulaCreator(
33+
Object pO,
34+
Object boolType,
35+
@Nullable Object pIntegerType,
36+
@Nullable Object pRationalType,
37+
@Nullable Object stringType,
38+
@Nullable Object regexType) {
39+
super(pO, boolType, pIntegerType, pRationalType, stringType, regexType);
40+
}
41+
42+
@Override
43+
public Object getBitvectorType(int bitwidth) {
44+
return null;
45+
}
46+
47+
@Override
48+
public Object getFloatingPointType(FloatingPointType type) {
49+
return null;
50+
}
51+
52+
@Override
53+
public Object getArrayType(Object indexType, Object elementType) {
54+
return null;
55+
}
56+
57+
@Override
58+
public Object makeVariable(Object pO, String varName) {
59+
return null;
60+
}
61+
62+
@Override
63+
public FormulaType<?> getFormulaType(Object formula) {
64+
return null;
65+
}
66+
67+
@Override
68+
public Object callFunctionImpl(Object declaration, List args) {
69+
return null;
70+
}
71+
72+
@Override
73+
public Object declareUFImpl(String pName, Object pReturnType, List pArgTypes) {
74+
return null;
75+
}
76+
77+
@Override
78+
protected Object getBooleanVarDeclarationImpl(Object pO) {
79+
return null;
80+
}
81+
82+
@Override
83+
public Object visit(FormulaVisitor visitor, Formula formula, Object f) {
84+
return null;
85+
}
86+
}

‎src/org/sosy_lab/java_smt/solvers/apron/ApronFormulaManager.java

+92
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,92 @@
1+
/*
2+
* JavaSMT is an API wrapper for a collection of SMT solvers.
3+
* This file is part of JavaSMT.
4+
*
5+
* Copyright (C) 2007-2016 Dirk Beyer
6+
* All rights reserved.
7+
*
8+
* Licensed under the Apache License, Version 2.0 (the "License");
9+
* you may not use this file except in compliance with the License.
10+
* You may obtain a copy of the License at
11+
*
12+
* http://www.apache.org/licenses/LICENSE-2.0
13+
*
14+
* Unless required by applicable law or agreed to in writing, software
15+
* distributed under the License is distributed on an "AS IS" BASIS,
16+
* WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
17+
* See the License for the specific language governing permissions and
18+
* limitations under the License.
19+
*/
20+
21+
package org.sosy_lab.java_smt.solvers.apron;
22+
23+
import java.util.Map;
24+
import org.checkerframework.checker.nullness.qual.Nullable;
25+
import org.sosy_lab.common.Appender;
26+
import org.sosy_lab.java_smt.api.BooleanFormula;
27+
import org.sosy_lab.java_smt.api.Formula;
28+
import org.sosy_lab.java_smt.api.IntegerFormulaManager;
29+
import org.sosy_lab.java_smt.api.RationalFormulaManager;
30+
import org.sosy_lab.java_smt.basicimpl.AbstractArrayFormulaManager;
31+
import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager;
32+
import org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager;
33+
import org.sosy_lab.java_smt.basicimpl.AbstractEnumerationFormulaManager;
34+
import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager;
35+
import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
36+
import org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager;
37+
import org.sosy_lab.java_smt.basicimpl.AbstractSLFormulaManager;
38+
import org.sosy_lab.java_smt.basicimpl.AbstractStringFormulaManager;
39+
import org.sosy_lab.java_smt.basicimpl.AbstractUFManager;
40+
import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
41+
42+
public class ApronFormulaManager extends AbstractFormulaManager <Long, Long, Long, Long>{
43+
/**
44+
* Builds a solver from the given theory implementations.
45+
*
46+
* @param pFormulaCreator
47+
* @param functionManager
48+
* @param booleanManager
49+
* @param pIntegerManager
50+
* @param pRationalManager
51+
* @param bitvectorManager
52+
* @param floatingPointManager
53+
* @param quantifiedManager
54+
* @param arrayManager
55+
* @param slManager
56+
* @param strManager
57+
* @param enumManager
58+
*/
59+
protected ApronFormulaManager(
60+
FormulaCreator pFormulaCreator,
61+
AbstractUFManager functionManager,
62+
AbstractBooleanFormulaManager booleanManager,
63+
@Nullable IntegerFormulaManager pIntegerManager,
64+
@Nullable RationalFormulaManager pRationalManager,
65+
@Nullable AbstractBitvectorFormulaManager bitvectorManager,
66+
@Nullable AbstractFloatingPointFormulaManager floatingPointManager,
67+
@Nullable AbstractQuantifiedFormulaManager quantifiedManager,
68+
@Nullable AbstractArrayFormulaManager arrayManager,
69+
@Nullable AbstractSLFormulaManager slManager,
70+
@Nullable AbstractStringFormulaManager strManager,
71+
@Nullable AbstractEnumerationFormulaManager enumManager) {
72+
super(pFormulaCreator, functionManager, booleanManager, pIntegerManager, pRationalManager,
73+
bitvectorManager, floatingPointManager, quantifiedManager, arrayManager, slManager,
74+
strManager, enumManager);
75+
}
76+
77+
@Override
78+
public BooleanFormula parse(String s) throws IllegalArgumentException {
79+
return null;
80+
}
81+
82+
@Override
83+
public <T extends Formula > T substitute(T f,
84+
Map<? extends Formula, ? extends Formula> fromToMapping) {
85+
return null;
86+
}
87+
88+
@Override
89+
public Appender dumpFormula(Long t) {
90+
return null;
91+
}
92+
}

0 commit comments

Comments
 (0)