Decouple Z3 From Expressions (#60)

rcosta358 · web-flow · commit aed9efd07d62 · 2025-10-29T14:54:53.000Z
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/AliasInvocation.java
@@ -1,10 +1,10 @@
 package liquidjava.rj_language.ast;
 
-import com.microsoft.z3.Expr;
 import java.util.ArrayList;
 import java.util.List;
 import java.util.stream.Collectors;
-import liquidjava.smt.TranslatorToZ3;
+
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 
 public class AliasInvocation extends Expression {
     String name;
@@ -24,12 +24,8 @@ public List<Expression> getArgs() {
     }
 
     @Override
-    public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
-        Expr<?>[] argsExpr = new Expr[getArgs().size()];
-        for (int i = 0; i < argsExpr.length; i++) {
-            argsExpr[i] = getArgs().get(i).eval(ctx);
-        }
-        return ctx.makeFunctionInvocation(name, argsExpr);
+    public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
+        return visitor.visitAliasInvocation(this);
     }
 
     @Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/BinaryExpression.java
@@ -1,8 +1,8 @@
 package liquidjava.rj_language.ast;
 
-import com.microsoft.z3.Expr;
 import java.util.List;
-import liquidjava.smt.TranslatorToZ3;
+
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 
 public class BinaryExpression extends Expression {
 
@@ -40,45 +40,8 @@ public boolean isArithmeticOperation() {
     }
 
     @Override
-    public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
-        Expr<?> ee1 = getFirstOperand().eval(ctx);
-        Expr<?> ee2 = getSecondOperand().eval(ctx);
-        return evalBinaryOp(ctx, ee1, ee2);
-    }
-
-    private Expr<?> evalBinaryOp(TranslatorToZ3 ctx, Expr<?> e1, Expr<?> e2) {
-        switch (op) {
-        case "&&":
-            return ctx.makeAnd(e1, e2);
-        case "||":
-            return ctx.makeOr(e1, e2);
-        case "-->":
-            return ctx.makeImplies(e1, e2);
-        case "==":
-            return ctx.makeEquals(e1, e2);
-        case "!=":
-            return ctx.mkNot(ctx.makeEquals(e1, e2));
-        case ">=":
-            return ctx.makeGtEq(e1, e2);
-        case ">":
-            return ctx.makeGt(e1, e2);
-        case "<=":
-            return ctx.makeLtEq(e1, e2);
-        case "<":
-            return ctx.makeLt(e1, e2);
-        case "+":
-            return ctx.makeAdd(e1, e2);
-        case "-":
-            return ctx.makeSub(e1, e2);
-        case "*":
-            return ctx.makeMul(e1, e2);
-        case "/":
-            return ctx.makeDiv(e1, e2);
-        case "%":
-            return ctx.makeMod(e1, e2);
-        default: // last case %
-            throw new RuntimeException("Operation " + op + "not supported by z3");
-        }
+    public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
+        return visitor.visitBinaryExpression(this);
     }
 
     @Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java
@@ -9,13 +9,13 @@
 import liquidjava.processor.context.Context;
 import liquidjava.processor.facade.AliasDTO;
 import liquidjava.rj_language.ast.typing.TypeInfer;
-import liquidjava.smt.TranslatorToZ3;
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.utils.Utils;
 import spoon.reflect.factory.Factory;
 
 public abstract class Expression {
 
-    public abstract Expr<?> eval(TranslatorToZ3 ctx) throws Exception;
+    public abstract <T> T accept(ExpressionVisitor<T> visitor) throws Exception;
 
     public abstract void getVariableNames(List<String> toAdd);
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/FunctionInvocation.java
@@ -1,10 +1,10 @@
 package liquidjava.rj_language.ast;
 
-import com.microsoft.z3.Expr;
 import java.util.ArrayList;
 import java.util.List;
 import java.util.stream.Collectors;
-import liquidjava.smt.TranslatorToZ3;
+
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 import liquidjava.utils.Utils;
 
 public class FunctionInvocation extends Expression {
@@ -30,12 +30,8 @@ public void setChild(int index, Expression element) {
     }
 
     @Override
-    public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
-        Expr<?>[] argsExpr = new Expr[getArgs().size()];
-        for (int i = 0; i < argsExpr.length; i++) {
-            argsExpr[i] = getArgs().get(i).eval(ctx);
-        }
-        return ctx.makeFunctionInvocation(name, argsExpr);
+    public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
+        return visitor.visitFunctionInvocation(this);
     }
 
     @Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java
@@ -1,8 +1,8 @@
 package liquidjava.rj_language.ast;
 
-import com.microsoft.z3.Expr;
 import java.util.List;
-import liquidjava.smt.TranslatorToZ3;
+
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 
 public class GroupExpression extends Expression {
 
@@ -15,8 +15,8 @@ public Expression getExpression() {
     }
 
     @Override
-    public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
-        return getExpression().eval(ctx);
+    public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
+        return visitor.visitGroupExpression(this);
     }
 
     public String toString() {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Ite.java
@@ -1,8 +1,8 @@
 package liquidjava.rj_language.ast;
 
-import com.microsoft.z3.Expr;
 import java.util.List;
-import liquidjava.smt.TranslatorToZ3;
+
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 
 public class Ite extends Expression {
 
@@ -25,8 +25,8 @@ public Expression getElse() {
     }
 
     @Override
-    public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
-        return ctx.makeIte(getCondition().eval(ctx), getThen().eval(ctx), getElse().eval(ctx));
+    public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
+        return visitor.visitIte(this);
     }
 
     @Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralBoolean.java
@@ -1,8 +1,8 @@
 package liquidjava.rj_language.ast;
 
-import com.microsoft.z3.Expr;
 import java.util.List;
-import liquidjava.smt.TranslatorToZ3;
+
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 
 public class LiteralBoolean extends Expression {
 
@@ -16,8 +16,9 @@ public LiteralBoolean(String value) {
         this.value = Boolean.parseBoolean(value);
     }
 
-    public Expr<?> eval(TranslatorToZ3 ctx) {
-        return ctx.makeBooleanLiteral(value);
+    @Override
+    public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
+        return visitor.visitLiteralBoolean(this);
     }
 
     public String toString() {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralInt.java
@@ -1,8 +1,8 @@
 package liquidjava.rj_language.ast;
 
-import com.microsoft.z3.Expr;
 import java.util.List;
-import liquidjava.smt.TranslatorToZ3;
+
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 
 public class LiteralInt extends Expression {
 
@@ -17,8 +17,8 @@ public LiteralInt(String v) {
     }
 
     @Override
-    public Expr<?> eval(TranslatorToZ3 ctx) {
-        return ctx.makeIntegerLiteral(value);
+    public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
+        return visitor.visitLiteralInt(this);
     }
 
     public String toString() {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralReal.java
@@ -1,8 +1,8 @@
 package liquidjava.rj_language.ast;
 
-import com.microsoft.z3.Expr;
 import java.util.List;
-import liquidjava.smt.TranslatorToZ3;
+
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 
 public class LiteralReal extends Expression {
 
@@ -17,8 +17,8 @@ public LiteralReal(String v) {
     }
 
     @Override
-    public Expr<?> eval(TranslatorToZ3 ctx) {
-        return ctx.makeDoubleLiteral(value);
+    public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
+        return visitor.visitLiteralReal(this);
     }
 
     public String toString() {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/LiteralString.java
@@ -1,8 +1,8 @@
 package liquidjava.rj_language.ast;
 
-import com.microsoft.z3.Expr;
 import java.util.List;
-import liquidjava.smt.TranslatorToZ3;
+
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 
 public class LiteralString extends Expression {
     private String value;
@@ -12,8 +12,8 @@ public LiteralString(String v) {
     }
 
     @Override
-    public Expr<?> eval(TranslatorToZ3 ctx) {
-        return ctx.makeString(value);
+    public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
+        return visitor.visitLiteralString(this);
     }
 
     public String toString() {
@@ -23,13 +23,11 @@ public String toString() {
     @Override
     public void getVariableNames(List<String> toAdd) {
         // end leaf
-
     }
 
     @Override
     public void getStateInvocations(List<String> toAdd, List<String> all) {
         // end leaf
-
     }
 
     @Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/UnaryExpression.java
@@ -1,8 +1,8 @@
 package liquidjava.rj_language.ast;
 
-import com.microsoft.z3.Expr;
 import java.util.List;
-import liquidjava.smt.TranslatorToZ3;
+
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 
 public class UnaryExpression extends Expression {
 
@@ -22,14 +22,8 @@ public String getOp() {
     }
 
     @Override
-    public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
-        switch (op) {
-        case "-":
-            return ctx.makeMinus(getExpression().eval(ctx));
-        case "!":
-            return ctx.mkNot(getExpression().eval(ctx));
-        }
-        return null;
+    public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
+        return visitor.visitUnaryExpression(this);
     }
 
     @Override
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Var.java
@@ -1,8 +1,8 @@
 package liquidjava.rj_language.ast;
 
-import com.microsoft.z3.Expr;
 import java.util.List;
-import liquidjava.smt.TranslatorToZ3;
+
+import liquidjava.rj_language.visitors.ExpressionVisitor;
 
 public class Var extends Expression {
 
@@ -17,8 +17,8 @@ public String getName() {
     }
 
     @Override
-    public Expr<?> eval(TranslatorToZ3 ctx) throws Exception {
-        return ctx.makeVariable(name);
+    public <T> T accept(ExpressionVisitor<T> visitor) throws Exception {
+        return visitor.visitVar(this);
     }
 
     public String toString() {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java
@@ -0,0 +1,37 @@
+package liquidjava.rj_language.visitors;
+
+import liquidjava.rj_language.ast.AliasInvocation;
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.FunctionInvocation;
+import liquidjava.rj_language.ast.GroupExpression;
+import liquidjava.rj_language.ast.Ite;
+import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.LiteralInt;
+import liquidjava.rj_language.ast.LiteralReal;
+import liquidjava.rj_language.ast.LiteralString;
+import liquidjava.rj_language.ast.UnaryExpression;
+import liquidjava.rj_language.ast.Var;
+
+public interface ExpressionVisitor<T> {
+    T visitAliasInvocation(AliasInvocation alias) throws Exception;
+
+    T visitBinaryExpression(BinaryExpression exp) throws Exception;
+
+    T visitFunctionInvocation(FunctionInvocation fun) throws Exception;
+
+    T visitGroupExpression(GroupExpression exp) throws Exception;
+
+    T visitIte(Ite ite) throws Exception;
+
+    T visitLiteralInt(LiteralInt lit) throws Exception;
+
+    T visitLiteralBoolean(LiteralBoolean lit) throws Exception;
+
+    T visitLiteralReal(LiteralReal lit) throws Exception;
+
+    T visitLiteralString(LiteralString lit) throws Exception;
+
+    T visitUnaryExpression(UnaryExpression exp) throws Exception;
+
+    T visitVar(Var var) throws Exception;
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java b/liquidjava-verifier/src/main/java/liquidjava/smt/SMTEvaluator.java
