Skip to content

Commit c401924

Browse files
Kirill GolubevKirill Golubev
Kirill Golubev
authored and
Kirill Golubev
committed
z3 translate and drafts for cvc5
1 parent 8321552 commit c401924

File tree

6 files changed

+510
-170
lines changed

6 files changed

+510
-170
lines changed

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java‎

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,8 +6,6 @@
66

77
import liquidjava.processor.context.Context;
88
import liquidjava.rj_language.Predicate;
9-
import liquidjava.rj_language.ast.Expression;
10-
import liquidjava.smt.solver_wrapper.ExprWrapper;
119
import liquidjava.smt.solver_wrapper.SMTWrapper;
1210
import liquidjava.smt.solver_wrapper.Status;
1311

@@ -22,11 +20,8 @@ public void verifySubtype(Predicate subRef, Predicate supRef, Context c)
2220
System.out.println("verification query: " + toVerify); // TODO remove
2321

2422
try {
25-
Expression exp = toVerify.getExpression();
26-
SMTWrapper tz3 = SMTWrapper.getZ3(c);
27-
// com.microsoft.z3.Expr
28-
ExprWrapper e = exp.eval(tz3);
29-
Status s = tz3.verifyExpression(e);
23+
SMTWrapper z3 = SMTWrapper.getZ3(c);
24+
Status s = z3.verifyExpression(toVerify.getExpression());
3025
if (s.equals(Status.SATISFIABLE)) {
3126
System.out.println("result of SMT: Not Ok!");
3227
throw new TypeCheckError(subRef + " not a subtype of " + supRef);

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/smt/solver_wrapper/CVC5Wrapper/CVC5Translator.java‎

Lines changed: 4 additions & 138 deletions
Original file line numberDiff line numberDiff line change
@@ -1,146 +1,12 @@
1-
package liquidjava.smt.solver_wrapper;
1+
package liquidjava.smt.solver_wrapper.CVC5Wrapper;
22

3-
import com.microsoft.z3.Expr;
4-
import com.microsoft.z3.FPExpr;
53
import liquidjava.processor.context.Context;
4+
import liquidjava.rj_language.visitors.AbstractExpressionVisitor;
65

7-
public class TranslatorToCVC5 extends SMTWrapper {
6+
public class CVC5Translator extends AbstractExpressionVisitor {
87

9-
TranslatorToCVC5(Context c) {
8+
CVC5Translator(Context c) {
109

1110
}
1211

13-
@Override
14-
public Status verifyExpression(ExprWrapper e) throws Exception {
15-
return null;
16-
}
17-
18-
@Override
19-
public ExprWrapper makeIntegerLiteral(int value) {
20-
return null;
21-
}
22-
23-
@Override
24-
public ExprWrapper makeLongLiteral(long value) {
25-
return null;
26-
}
27-
28-
@Override
29-
public ExprWrapper makeDoubleLiteral(double value) {
30-
return null;
31-
}
32-
33-
@Override
34-
public ExprWrapper makeString(String s) {
35-
return null;
36-
}
37-
38-
@Override
39-
public ExprWrapper makeBooleanLiteral(boolean value) {
40-
return null;
41-
}
42-
43-
@Override
44-
public ExprWrapper makeFunctionInvocation(String name, ExprWrapper[] params) throws Exception {
45-
return null;
46-
}
47-
48-
@Override
49-
public ExprWrapper makeSelect(String name, ExprWrapper[] params) {
50-
return null;
51-
}
52-
53-
@Override
54-
public ExprWrapper makeStore(String name, ExprWrapper[] params) {
55-
return null;
56-
}
57-
58-
@Override
59-
public ExprWrapper makeEquals(ExprWrapper e1, ExprWrapper e2) {
60-
return null;
61-
}
62-
63-
@Override
64-
public ExprWrapper makeLt(ExprWrapper e1, ExprWrapper e2) {
65-
return null;
66-
}
67-
68-
@Override
69-
public ExprWrapper makeLtEq(ExprWrapper e1, ExprWrapper e2) {
70-
return null;
71-
}
72-
73-
@Override
74-
public ExprWrapper makeGt(ExprWrapper e1, ExprWrapper e2) {
75-
return null;
76-
}
77-
78-
@Override
79-
public ExprWrapper makeGtEq(ExprWrapper e1, ExprWrapper e2) {
80-
return null;
81-
}
82-
83-
@Override
84-
public ExprWrapper makeImplies(ExprWrapper e1, ExprWrapper e2) {
85-
return null;
86-
}
87-
88-
@Override
89-
public ExprWrapper makeBiconditional(ExprWrapper eval, ExprWrapper eval2) {
90-
return null;
91-
}
92-
93-
@Override
94-
public ExprWrapper makeAnd(ExprWrapper eval, ExprWrapper eval2) {
95-
return null;
96-
}
97-
98-
@Override
99-
public ExprWrapper mkNot(ExprWrapper e1) {
100-
return null;
101-
}
102-
103-
@Override
104-
public ExprWrapper makeOr(ExprWrapper eval, ExprWrapper eval2) {
105-
return null;
106-
}
107-
108-
@Override
109-
public ExprWrapper makeMinus(ExprWrapper eval) {
110-
return null;
111-
}
112-
113-
@Override
114-
public ExprWrapper makeAdd(ExprWrapper eval, ExprWrapper eval2) {
115-
return null;
116-
}
117-
118-
@Override
119-
public ExprWrapper makeSub(ExprWrapper eval, ExprWrapper eval2) {
120-
return null;
121-
}
122-
123-
@Override
124-
public ExprWrapper makeMul(ExprWrapper eval, ExprWrapper eval2) {
125-
return null;
126-
}
127-
128-
@Override
129-
public ExprWrapper makeDiv(ExprWrapper eval, ExprWrapper eval2) {
130-
return null;
131-
}
132-
133-
@Override
134-
public ExprWrapper makeMod(ExprWrapper eval, ExprWrapper eval2) {
135-
return null;
136-
}
137-
138-
public FPExpr toFP(ExprWrapper e) {
139-
return null;
140-
}
141-
142-
@Override
143-
public ExprWrapper makeIte(ExprWrapper c, ExprWrapper t, ExprWrapper e) {
144-
return null;
145-
}
14612
}

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/smt/solver_wrapper/CVC5Wrapper/CVC5Wrapper.java‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
package liquidjava.smt.solver_wrapper.CVC5Wrapper;
2+
3+
import liquidjava.processor.context.Context;
4+
import liquidjava.rj_language.ast.Expression;
5+
import liquidjava.smt.solver_wrapper.SMTWrapper;
6+
import liquidjava.smt.solver_wrapper.Status;
7+
import liquidjava.smt.solver_wrapper.Z3Wrapper.Z3Translator;
8+
9+
public class CVC5Wrapper implements SMTWrapper {
10+
11+
public CVC5Wrapper(Context c) {
12+
CVC5Translator cvc5tr = new CVC5Translator(c);
13+
}
14+
15+
@Override
16+
public Status verifyExpression(Expression e) throws Exception {
17+
return null;
18+
}
19+
}

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/smt/solver_wrapper/SMTWrapper.java‎

Lines changed: 9 additions & 25 deletions
Original file line numberDiff line numberDiff line change
@@ -1,35 +1,19 @@
11
package liquidjava.smt.solver_wrapper;
22

3-
import com.martiansoftware.jsap.SyntaxException;
4-
import com.microsoft.z3.BoolExpr;
5-
import com.microsoft.z3.Expr;
6-
import com.microsoft.z3.FuncDecl;
7-
import com.microsoft.z3.Solver;
8-
import liquidjava.processor.context.AliasWrapper;
93
import liquidjava.processor.context.Context;
104
import liquidjava.rj_language.ast.Expression;
11-
import liquidjava.rj_language.visitors.ExpressionVisitor;
12-
import liquidjava.smt.NotFoundError;
135

14-
import java.util.HashMap;
15-
import java.util.List;
16-
import java.util.Map;
6+
import liquidjava.smt.solver_wrapper.CVC5Wrapper.CVC5Wrapper;
7+
import liquidjava.smt.solver_wrapper.Z3Wrapper.Z3Wrapper;
178

18-
public abstract class SMTWrapper {
19-
public static Status verifyExpression(Expression e, Context c) throws Exception {
20-
Z3Translator z3tr = new Z3Translator(c);
9+
public interface SMTWrapper {
10+
Status verifyExpression(Expression e) throws Exception;
2111

22-
e.accept(z3tr);
23-
Expr<?> z3Expr = z3tr.getResult();
24-
25-
Solver s = z3tr.getContext().mkSolver();
12+
static SMTWrapper getZ3(Context c) {
13+
return new Z3Wrapper(c);
14+
}
2615

27-
s.add((BoolExpr) z3Expr);
28-
com.microsoft.z3.Status st = s.check();
29-
if (st.equals(com.microsoft.z3.Status.SATISFIABLE)) {
30-
// Example of values
31-
// System.out.println(s.getModel());
32-
}
33-
return Status.fromZ3(st);
16+
static SMTWrapper getCVC5(Context c) {
17+
return new CVC5Wrapper(c);
3418
}
3519
}

0 commit comments

Comments
 (0)