Skip to content

Commit 8321552

Browse files
Kirill GolubevKirill Golubev
Kirill Golubev
authored and
Kirill Golubev
committed
accept for expersstion visitor
1 parent 314e406 commit 8321552

12 files changed

Lines changed: 24 additions & 149 deletions

File tree

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

Lines changed: 1 addition & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,7 @@
44
import java.util.List;
55
import java.util.stream.Collectors;
66

7-
import com.microsoft.z3.Expr;
8-
97
import liquidjava.rj_language.visitors.ExpressionVisitor;
10-
import liquidjava.smt.solver_wrapper.ExprWrapper;
11-
import liquidjava.smt.solver_wrapper.SMTWrapper;
128

139
public class AliasInvocation extends Expression {
1410
String name;
@@ -28,19 +24,10 @@ public List<Expression> getArgs() {
2824
}
2925

3026
@Override
31-
public void accept(ExpressionVisitor v) {
27+
public void accept(ExpressionVisitor v) throws Exception {
3228
v.visitAliasInvocation(this);
3329
}
3430

35-
@Override
36-
public ExprWrapper eval(SMTWrapper ctx) throws Exception {
37-
ExprWrapper[] argsExpr = new ExprWrapper[getArgs().size()];
38-
for (int i = 0; i < argsExpr.length; i++) {
39-
argsExpr[i] = getArgs().get(i).eval(ctx);
40-
}
41-
return ctx.makeFunctionInvocation(name, argsExpr);
42-
}
43-
4431
@Override
4532
public String toString() {
4633
return name + "(" + getArgs().stream().map(p -> p.toString()).collect(Collectors.joining(", ")) + ")";

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

Lines changed: 1 addition & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,7 @@
44

55
import java.util.List;
66

7-
import com.microsoft.z3.Expr;
8-
97
import liquidjava.rj_language.visitors.ExpressionVisitor;
10-
import liquidjava.smt.solver_wrapper.ExprWrapper;
11-
import liquidjava.smt.solver_wrapper.SMTWrapper;
128

139
public class BinaryExpression extends Expression {
1410

@@ -46,53 +42,10 @@ public boolean isArithmeticOperation() {
4642
}
4743

4844
@Override
49-
public void accept(ExpressionVisitor v) {
45+
public void accept(ExpressionVisitor v) throws Exception {
5046
v.visitBinaryExpression(this);
5147
}
5248

53-
@Override
54-
public ExprWrapper eval(SMTWrapper ctx) throws Exception {
55-
ExprWrapper ee1 = getFirstOperand().eval(ctx);
56-
ExprWrapper ee2 = getSecondOperand().eval(ctx);
57-
return evalBinaryOp(ctx, ee1, ee2);
58-
}
59-
60-
private ExprWrapper evalBinaryOp(SMTWrapper ctx, ExprWrapper e1, ExprWrapper e2) {
61-
switch (op) {
62-
case "&&":
63-
return ctx.makeAnd(e1, e2);
64-
case "||":
65-
return ctx.makeOr(e1, e2);
66-
case "-->":
67-
return ctx.makeImplies(e1, e2);
68-
case "==":
69-
return ctx.makeEquals(e1, e2);
70-
case "!=":
71-
return ctx.mkNot(ctx.makeEquals(e1, e2));
72-
case ">=":
73-
return ctx.makeGtEq(e1, e2);
74-
case ">":
75-
return ctx.makeGt(e1, e2);
76-
case "<=":
77-
return ctx.makeLtEq(e1, e2);
78-
case "<":
79-
return ctx.makeLt(e1, e2);
80-
case "+":
81-
return ctx.makeAdd(e1, e2);
82-
case "-":
83-
return ctx.makeSub(e1, e2);
84-
case "*":
85-
return ctx.makeMul(e1, e2);
86-
case "/":
87-
return ctx.makeDiv(e1, e2);
88-
case "%":
89-
return ctx.makeMod(e1, e2);
90-
default: // last case %
91-
fail("Reached unkown operation " + op);
92-
return null;
93-
}
94-
}
95-
9649
@Override
9750
public String toString() {
9851
return getFirstOperand().toString() + " " + op + " " + getSecondOperand().toString();

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

Lines changed: 1 addition & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -8,15 +8,10 @@
88
import liquidjava.processor.facade.AliasDTO;
99
import liquidjava.rj_language.ast.typing.TypeInfer;
1010
import liquidjava.rj_language.visitors.ExpressionVisitor;
11-
import liquidjava.smt.solver_wrapper.ExprWrapper;
12-
import liquidjava.smt.solver_wrapper.SMTWrapper;
1311
import spoon.reflect.factory.Factory;
1412

1513
public abstract class Expression {
16-
17-
public abstract void accept(ExpressionVisitor v);
18-
19-
public abstract ExprWrapper eval(SMTWrapper ctx) throws Exception;
14+
public abstract void accept(ExpressionVisitor v) throws Exception;
2015

2116
public abstract void getVariableNames(List<String> toAdd);
2217

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

Lines changed: 1 addition & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -4,11 +4,7 @@
44
import java.util.List;
55
import java.util.stream.Collectors;
66

7-
import com.microsoft.z3.Expr;
8-
97
import liquidjava.rj_language.visitors.ExpressionVisitor;
10-
import liquidjava.smt.solver_wrapper.ExprWrapper;
11-
import liquidjava.smt.solver_wrapper.SMTWrapper;
128

139
public class FunctionInvocation extends Expression {
1410
String name;
@@ -33,19 +29,10 @@ public void setChild(int index, Expression element) {
3329
}
3430

3531
@Override
36-
public void accept(ExpressionVisitor v) {
32+
public void accept(ExpressionVisitor v) throws Exception {
3733
v.visitFunctionInvocation(this);
3834
}
3935

40-
@Override
41-
public ExprWrapper eval(SMTWrapper ctx) throws Exception {
42-
ExprWrapper[] argsExpr = new ExprWrapper[getArgs().size()];
43-
for (int i = 0; i < argsExpr.length; i++) {
44-
argsExpr[i] = getArgs().get(i).eval(ctx);
45-
}
46-
return ctx.makeFunctionInvocation(name, argsExpr);
47-
}
48-
4936
@Override
5037
public String toString() {
5138
return name + "(" + getArgs().stream().map(Expression::toString).collect(Collectors.joining(",")) + ")";

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

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,6 @@
33
import java.util.List;
44

55
import liquidjava.rj_language.visitors.ExpressionVisitor;
6-
import liquidjava.smt.solver_wrapper.ExprWrapper;
7-
import liquidjava.smt.solver_wrapper.SMTWrapper;
86

97
public class GroupExpression extends Expression {
108

@@ -17,15 +15,10 @@ public Expression getExpression() {
1715
}
1816

1917
@Override
20-
public void accept(ExpressionVisitor v) {
18+
public void accept(ExpressionVisitor v) throws Exception {
2119
v.visitGroupExpression(this);
2220
}
2321

24-
@Override
25-
public ExprWrapper eval(SMTWrapper ctx) throws Exception {
26-
return getExpression().eval(ctx);
27-
}
28-
2922
public String toString() {
3023
return "(" + getExpression().toString() + ")";
3124
}

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

Lines changed: 1 addition & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,6 @@
33
import java.util.List;
44

55
import liquidjava.rj_language.visitors.ExpressionVisitor;
6-
import liquidjava.smt.solver_wrapper.ExprWrapper;
7-
import liquidjava.smt.solver_wrapper.SMTWrapper;
86

97
public class Ite extends Expression {
108

@@ -27,15 +25,10 @@ public Expression getElse() {
2725
}
2826

2927
@Override
30-
public void accept(ExpressionVisitor v) {
28+
public void accept(ExpressionVisitor v) throws Exception {
3129
v.visitITE(this);
3230
}
3331

34-
@Override
35-
public ExprWrapper eval(SMTWrapper ctx) throws Exception {
36-
return ctx.makeIte(getCondition().eval(ctx), getThen().eval(ctx), getElse().eval(ctx));
37-
}
38-
3932
@Override
4033
public String toString() {
4134
return getCondition().toString() + "?" + getThen().toString() + ":" + getElse().toString();

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

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,13 +3,14 @@
33
import java.util.List;
44

55
import liquidjava.rj_language.visitors.ExpressionVisitor;
6-
import liquidjava.smt.solver_wrapper.ExprWrapper;
7-
import liquidjava.smt.solver_wrapper.SMTWrapper;
86

97
public class LiteralBoolean extends Expression {
10-
118
boolean value;
129

10+
public boolean getValue() {
11+
return value;
12+
}
13+
1314
public LiteralBoolean(boolean value) {
1415
this.value = value;
1516
}
@@ -23,10 +24,6 @@ public void accept(ExpressionVisitor v) {
2324
v.visitLiteralBoolean(this);
2425
}
2526

26-
public ExprWrapper eval(SMTWrapper ctx) {
27-
return ctx.makeBooleanLiteral(value);
28-
}
29-
3027
public String toString() {
3128
return Boolean.toString(value);
3229
}

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

Lines changed: 5 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -3,12 +3,14 @@
33
import java.util.List;
44

55
import liquidjava.rj_language.visitors.ExpressionVisitor;
6-
import liquidjava.smt.solver_wrapper.ExprWrapper;
7-
import liquidjava.smt.solver_wrapper.SMTWrapper;
86

97
public class LiteralInt extends Expression {
108

11-
private int value;
9+
private final int value;
10+
11+
public int getValue() {
12+
return value;
13+
}
1214

1315
public LiteralInt(int v) {
1416
value = v;
@@ -23,11 +25,6 @@ public void accept(ExpressionVisitor v) {
2325
v.visitLiteralInt(this);
2426
}
2527

26-
@Override
27-
public ExprWrapper eval(SMTWrapper ctx) {
28-
return ctx.makeIntegerLiteral(value);
29-
}
30-
3128
public String toString() {
3229
return Integer.toString(value);
3330
}

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

Lines changed: 4 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,6 @@
33
import java.util.List;
44

55
import liquidjava.rj_language.visitors.ExpressionVisitor;
6-
import liquidjava.smt.solver_wrapper.ExprWrapper;
7-
import liquidjava.smt.solver_wrapper.SMTWrapper;
86

97
public class LiteralReal extends Expression {
108

@@ -23,11 +21,6 @@ public void accept(ExpressionVisitor v) {
2321
v.visitLiteralReal(this);
2422
}
2523

26-
@Override
27-
public ExprWrapper eval(SMTWrapper ctx) {
28-
return ctx.makeDoubleLiteral(value);
29-
}
30-
3124
public String toString() {
3225
return Double.toString(value);
3326
}
@@ -77,4 +70,8 @@ public boolean equals(Object obj) {
7770
return false;
7871
return true;
7972
}
73+
74+
public double getValue() {
75+
return value;
76+
}
8077
}

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

Lines changed: 3 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,6 @@
33
import java.util.List;
44

55
import liquidjava.rj_language.visitors.ExpressionVisitor;
6-
import liquidjava.smt.solver_wrapper.ExprWrapper;
7-
import liquidjava.smt.solver_wrapper.SMTWrapper;
86

97
public class LiteralString extends Expression {
108
private String value;
@@ -18,11 +16,6 @@ public void accept(ExpressionVisitor v) {
1816
v.visitLiteralString(this);
1917
}
2018

21-
@Override
22-
public ExprWrapper eval(SMTWrapper ctx) {
23-
return ctx.makeString(value);
24-
}
25-
2619
public String toString() {
2720
return value;
2821
}
@@ -74,4 +67,7 @@ public boolean equals(Object obj) {
7467
return true;
7568
}
7669

70+
public String getValue() {
71+
return value;
72+
}
7773
}

0 commit comments

Comments
 (0)