Skip to content

Commit 6e9b572

Browse files
Kirill GolubevKirill Golubev
Kirill Golubev
authored and
Kirill Golubev
committed
to solver anglostic expresstion
1 parent 20bef8d commit 6e9b572

12 files changed

Lines changed: 42 additions & 50 deletions

File tree

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java‎

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

77
import com.microsoft.z3.Expr;
88

9-
import liquidjava.smt.TranslatorToZ3;
9+
import liquidjava.smt.solver_wrapper.ExprWrapper;
10+
import liquidjava.smt.solver_wrapper.SMTWrapper;
1011

1112
public class AliasInvocation extends Expression {
1213
String name;
@@ -26,8 +27,8 @@ public List<Expression> getArgs() {
2627
}
2728

2829
@Override
29-
public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
30-
Expr<?>[] argsExpr = new Expr[getArgs().size()];
30+
public ExprWrapper eval(SMTWrapper ctx) throws Exception {
31+
ExprWrapper[] argsExpr = new ExprWrapper[getArgs().size()];
3132
for (int i = 0; i < argsExpr.length; i++) {
3233
argsExpr[i] = getArgs().get(i).eval(ctx);
3334
}

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java‎

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

77
import com.microsoft.z3.Expr;
88

9-
import liquidjava.smt.TranslatorToZ3;
9+
import liquidjava.smt.solver_wrapper.ExprWrapper;
10+
import liquidjava.smt.solver_wrapper.SMTWrapper;
1011

1112
public class BinaryExpression extends Expression {
1213

@@ -44,13 +45,13 @@ public boolean isArithmeticOperation() {
4445
}
4546

4647
@Override
47-
public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
48-
Expr<?> ee1 = getFirstOperand().eval(ctx);
49-
Expr<?> ee2 = getSecondOperand().eval(ctx);
48+
public ExprWrapper eval(SMTWrapper ctx) throws Exception {
49+
ExprWrapper ee1 = getFirstOperand().eval(ctx);
50+
ExprWrapper ee2 = getSecondOperand().eval(ctx);
5051
return evalBinaryOp(ctx, ee1, ee2);
5152
}
5253

53-
private Expr<?> evalBinaryOp(TranslatorToZ3 ctx, Expr<?> e1, Expr<?> e2) {
54+
private ExprWrapper evalBinaryOp(SMTWrapper ctx, ExprWrapper e1, ExprWrapper e2) {
5455
switch (op) {
5556
case "&&":
5657
return ctx.makeAnd(e1, e2);

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java‎

Lines changed: 3 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -4,17 +4,16 @@
44
import java.util.List;
55
import java.util.Map;
66

7-
import com.microsoft.z3.Expr;
8-
97
import liquidjava.processor.context.Context;
108
import liquidjava.processor.facade.AliasDTO;
119
import liquidjava.rj_language.ast.typing.TypeInfer;
12-
import liquidjava.smt.TranslatorToZ3;
10+
import liquidjava.smt.solver_wrapper.ExprWrapper;
11+
import liquidjava.smt.solver_wrapper.SMTWrapper;
1312
import spoon.reflect.factory.Factory;
1413

1514
public abstract class Expression {
1615

17-
public abstract Expr<?> eval(TranslatorToZ3 ctx) throws Exception;
16+
public abstract ExprWrapper eval(SMTWrapper ctx) throws Exception;
1817

1918
public abstract void getVariableNames(List<String> toAdd);
2019

@@ -78,8 +77,6 @@ private void auxSubstitute(Expression from, Expression to) {
7877
/**
7978
* Substitutes the function call with the given parameter to the expression e
8079
*
81-
* @param s
82-
* @param e
8380
*/
8481
public void substituteFunction(String functionName, List<Expression> parameters, Expression sub) {
8582
if (hasChildren())

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java‎

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

77
import com.microsoft.z3.Expr;
88

9-
import liquidjava.smt.TranslatorToZ3;
9+
import liquidjava.smt.solver_wrapper.ExprWrapper;
10+
import liquidjava.smt.solver_wrapper.SMTWrapper;
1011

1112
public class FunctionInvocation extends Expression {
1213
String name;
@@ -31,8 +32,8 @@ public void setChild(int index, Expression element) {
3132
}
3233

3334
@Override
34-
public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
35-
Expr<?>[] argsExpr = new Expr[getArgs().size()];
35+
public ExprWrapper eval(SMTWrapper ctx) throws Exception {
36+
ExprWrapper[] argsExpr = new ExprWrapper[getArgs().size()];
3637
for (int i = 0; i < argsExpr.length; i++) {
3738
argsExpr[i] = getArgs().get(i).eval(ctx);
3839
}
@@ -41,7 +42,7 @@ public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
4142

4243
@Override
4344
public String toString() {
44-
return name + "(" + getArgs().stream().map(p -> p.toString()).collect(Collectors.joining(",")) + ")";
45+
return name + "(" + getArgs().stream().map(Expression::toString).collect(Collectors.joining(",")) + ")";
4546
}
4647

4748
@Override

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,8 @@
22

33
import java.util.List;
44

5-
import com.microsoft.z3.Expr;
6-
7-
import liquidjava.smt.TranslatorToZ3;
5+
import liquidjava.smt.solver_wrapper.ExprWrapper;
6+
import liquidjava.smt.solver_wrapper.SMTWrapper;
87

98
public class GroupExpression extends Expression {
109

@@ -17,7 +16,7 @@ public Expression getExpression() {
1716
}
1817

1918
@Override
20-
public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
19+
public ExprWrapper eval(SMTWrapper ctx) throws Exception {
2120
return getExpression().eval(ctx);
2221
}
2322

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,8 @@
22

33
import java.util.List;
44

5-
import com.microsoft.z3.Expr;
6-
7-
import liquidjava.smt.TranslatorToZ3;
5+
import liquidjava.smt.solver_wrapper.ExprWrapper;
6+
import liquidjava.smt.solver_wrapper.SMTWrapper;
87

98
public class Ite extends Expression {
109

@@ -27,7 +26,7 @@ public Expression getElse() {
2726
}
2827

2928
@Override
30-
public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
29+
public ExprWrapper eval(SMTWrapper ctx) throws Exception {
3130
return ctx.makeIte(getCondition().eval(ctx), getThen().eval(ctx), getElse().eval(ctx));
3231
}
3332

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,8 @@
22

33
import java.util.List;
44

5-
import com.microsoft.z3.Expr;
6-
7-
import liquidjava.smt.TranslatorToZ3;
5+
import liquidjava.smt.solver_wrapper.ExprWrapper;
6+
import liquidjava.smt.solver_wrapper.SMTWrapper;
87

98
public class LiteralBoolean extends Expression {
109

@@ -18,7 +17,7 @@ public LiteralBoolean(String value) {
1817
this.value = Boolean.parseBoolean(value);
1918
}
2019

21-
public Expr<?> eval(TranslatorToZ3 ctx) {
20+
public ExprWrapper eval(SMTWrapper ctx) {
2221
return ctx.makeBooleanLiteral(value);
2322
}
2423

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,8 @@
22

33
import java.util.List;
44

5-
import com.microsoft.z3.Expr;
6-
7-
import liquidjava.smt.TranslatorToZ3;
5+
import liquidjava.smt.solver_wrapper.ExprWrapper;
6+
import liquidjava.smt.solver_wrapper.SMTWrapper;
87

98
public class LiteralInt extends Expression {
109

@@ -19,7 +18,7 @@ public LiteralInt(String v) {
1918
}
2019

2120
@Override
22-
public Expr<?> eval(TranslatorToZ3 ctx) {
21+
public ExprWrapper eval(SMTWrapper ctx) {
2322
return ctx.makeIntegerLiteral(value);
2423
}
2524

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,8 @@
22

33
import java.util.List;
44

5-
import com.microsoft.z3.Expr;
6-
7-
import liquidjava.smt.TranslatorToZ3;
5+
import liquidjava.smt.solver_wrapper.ExprWrapper;
6+
import liquidjava.smt.solver_wrapper.SMTWrapper;
87

98
public class LiteralReal extends Expression {
109

@@ -19,7 +18,7 @@ public LiteralReal(String v) {
1918
}
2019

2120
@Override
22-
public Expr<?> eval(TranslatorToZ3 ctx) {
21+
public ExprWrapper eval(SMTWrapper ctx) {
2322
return ctx.makeDoubleLiteral(value);
2423
}
2524

‎liquidjava-umbrella/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java‎

Lines changed: 3 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,9 +2,8 @@
22

33
import java.util.List;
44

5-
import com.microsoft.z3.Expr;
6-
7-
import liquidjava.smt.TranslatorToZ3;
5+
import liquidjava.smt.solver_wrapper.ExprWrapper;
6+
import liquidjava.smt.solver_wrapper.SMTWrapper;
87

98
public class LiteralString extends Expression {
109
private String value;
@@ -14,7 +13,7 @@ public LiteralString(String v) {
1413
}
1514

1615
@Override
17-
public Expr<?> eval(TranslatorToZ3 ctx) {
16+
public ExprWrapper eval(SMTWrapper ctx) {
1817
return ctx.makeString(value);
1918
}
2019

0 commit comments

Comments
 (0)