Add SimplifiedExpression

rcosta358 · rcosta358 · commit 0e276f3241e8 · 2026-06-08T11:19:11.000+01:00
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
@@ -82,6 +82,9 @@ public boolean isLiteral() {
      * @return true if it is a boolean expression, false otherwise
      */
     public boolean isBooleanExpression() {
+        if (this instanceof SimplifiedExpression node) {
+            return node.getSimplifiedExpression().isBooleanExpression();
+        }
         if (this instanceof LiteralBoolean || this instanceof Ite || this instanceof AliasInvocation
                 || this instanceof FunctionInvocation) {
             return true;
@@ -99,6 +102,8 @@ public boolean isBooleanExpression() {
     }
 
     public List<Expression> getConjuncts() {
+        if (this instanceof SimplifiedExpression node)
+            return node.getSimplifiedExpression().getConjuncts();
         if (this instanceof BinaryExpression binaryExpression && "&&".equals(binaryExpression.getOperator())) {
             List<Expression> conjuncts = new ArrayList<>();
             conjuncts.addAll(binaryExpression.getFirstOperand().getConjuncts());
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java
@@ -0,0 +1,124 @@
+package liquidjava.rj_language.ast;
+
+import java.util.ArrayList;
+import java.util.List;
+import java.util.Objects;
+
+import liquidjava.diagnostics.errors.LJError;
+import liquidjava.rj_language.visitors.ExpressionVisitor;
+import spoon.reflect.reference.CtTypeReference;
+
+public class SimplifiedExpression extends Expression {
+
+    private final Expression origin;
+    private final List<Binder> binders;
+
+    public SimplifiedExpression(Expression simplified, Expression origin) {
+        this(simplified, origin, List.of());
+    }
+
+    public SimplifiedExpression(Expression simplified, Expression origin, List<Binder> binders) {
+        addChild(simplified);
+        this.origin = origin;
+        this.binders = new ArrayList<>(binders);
+    }
+
+    public Expression getSimplifiedExpression() {
+        return children.get(0);
+    }
+
+    public Expression getOrigin() {
+        return origin;
+    }
+
+    public List<Binder> getBinders() {
+        return binders;
+    }
+
+    @Override
+    public <T> T accept(ExpressionVisitor<T> visitor) throws LJError {
+        return visitor.visitSimplifiedNode(this);
+    }
+
+    @Override
+    public void getVariableNames(List<String> toAdd) {
+        getSimplifiedExpression().getVariableNames(toAdd);
+    }
+
+    @Override
+    public void getStateInvocations(List<String> toAdd, List<String> all) {
+        getSimplifiedExpression().getStateInvocations(toAdd, all);
+    }
+
+    @Override
+    public boolean isBooleanTrue() {
+        return getSimplifiedExpression().isBooleanTrue();
+    }
+
+    @Override
+    public Expression clone() {
+        return new SimplifiedExpression(getSimplifiedExpression().clone(), origin.clone(), binders);
+    }
+
+    @Override
+    public String toString() {
+        return getSimplifiedExpression().toString();
+    }
+
+    @Override
+    public int hashCode() {
+        return Objects.hash(getSimplifiedExpression(), origin, binders);
+    }
+
+    @Override
+    public boolean equals(Object obj) {
+        if (this == obj)
+            return true;
+        if (obj == null)
+            return false;
+        if (getClass() != obj.getClass())
+            return false;
+        SimplifiedExpression other = (SimplifiedExpression) obj;
+        return getSimplifiedExpression().equals(other.getSimplifiedExpression()) && origin.equals(other.origin)
+                && binders.equals(other.binders);
+    }
+
+    public static class Binder {
+        private final String name;
+        private final String type;
+
+        public Binder(String name, String type) {
+            this.name = name;
+            this.type = type;
+        }
+
+        public Binder(String name, CtTypeReference<?> type) {
+            this(name, type.getQualifiedName());
+        }
+
+        public String getName() {
+            return name;
+        }
+
+        public String getType() {
+            return type;
+        }
+
+        @Override
+        public int hashCode() {
+            return Objects.hash(name, type);
+        }
+
+        @Override
+        public boolean equals(Object obj) {
+            if (this == obj)
+                return true;
+            if (obj == null)
+                return false;
+            if (getClass() != obj.getClass())
+                return false;
+            Binder other = (Binder) obj;
+            return name.equals(other.name) && type.equals(other.type);
+        }
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java
@@ -17,6 +17,7 @@
 import liquidjava.rj_language.ast.LiteralReal;
 import liquidjava.rj_language.ast.LiteralString;
 import liquidjava.rj_language.ast.Enum;
+import liquidjava.rj_language.ast.SimplifiedExpression;
 import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
 import liquidjava.rj_language.visitors.ExpressionVisitor;
@@ -61,8 +62,12 @@ private String formatArguments(List<Expression> args) {
     }
 
     private Expression unwrapGroup(Expression expression) {
-        while (expression instanceof GroupExpression group)
-            expression = group.getExpression();
+        while (expression instanceof GroupExpression || expression instanceof SimplifiedExpression) {
+            if (expression instanceof GroupExpression group)
+                expression = group.getExpression();
+            else if (expression instanceof SimplifiedExpression node)
+                expression = node.getSimplifiedExpression();
+        }
         return expression;
     }
 
@@ -161,6 +166,11 @@ public String visitLiteralString(LiteralString lit) {
         return lit.toString();
     }
 
+    @Override
+    public String visitSimplifiedNode(SimplifiedExpression node) {
+        return formatExpression(node.getSimplifiedExpression());
+    }
+
     @Override
     public String visitUnaryExpression(UnaryExpression exp) {
         return exp.getOp() + formatOperand(exp, exp.getExpression(), true);
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java
@@ -4,6 +4,7 @@
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.GroupExpression;
 import liquidjava.rj_language.ast.Ite;
+import liquidjava.rj_language.ast.SimplifiedExpression;
 import liquidjava.rj_language.ast.UnaryExpression;
 
 public enum ExpressionPrecedence {
@@ -16,6 +17,8 @@ public boolean isLowerThan(ExpressionPrecedence other) {
     public static ExpressionPrecedence of(Expression expression) {
         if (expression instanceof GroupExpression group)
             return of(group.getExpression());
+        if (expression instanceof SimplifiedExpression node)
+            return of(node.getSimplifiedExpression());
         if (expression instanceof Ite)
             return TERNARY;
         if (expression instanceof UnaryExpression)
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java
@@ -15,6 +15,7 @@
 import liquidjava.rj_language.ast.LiteralLong;
 import liquidjava.rj_language.ast.LiteralReal;
 import liquidjava.rj_language.ast.LiteralString;
+import liquidjava.rj_language.ast.SimplifiedExpression;
 import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
 import liquidjava.utils.Utils;
@@ -57,6 +58,8 @@ else if (e instanceof FunctionInvocation)
             return functionType(ctx, (FunctionInvocation) e);
         else if (e instanceof AliasInvocation)
             return boolType(factory);
+        else if (e instanceof SimplifiedExpression)
+            return getType(ctx, factory, ((SimplifiedExpression) e).getSimplifiedExpression());
 
         return Optional.empty();
     }
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
@@ -13,6 +13,7 @@
 import liquidjava.rj_language.ast.LiteralLong;
 import liquidjava.rj_language.ast.LiteralReal;
 import liquidjava.rj_language.ast.LiteralString;
+import liquidjava.rj_language.ast.SimplifiedExpression;
 import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
 
@@ -39,9 +40,11 @@ public interface ExpressionVisitor<T> {
 
     T visitLiteralString(LiteralString lit) throws LJError;
 
+    T visitSimplifiedNode(SimplifiedExpression node) throws LJError;
+
     T visitUnaryExpression(UnaryExpression exp) throws LJError;
 
     T visitEnum(Enum en) throws LJError;
 
     T visitVar(Var var) throws LJError;
-}
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java
@@ -15,6 +15,7 @@
 import liquidjava.rj_language.ast.LiteralLong;
 import liquidjava.rj_language.ast.LiteralReal;
 import liquidjava.rj_language.ast.LiteralString;
+import liquidjava.rj_language.ast.SimplifiedExpression;
 import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
 import liquidjava.rj_language.visitors.ExpressionVisitor;
@@ -113,6 +114,11 @@ public Expr<?> visitLiteralString(LiteralString lit) {
         return ctx.makeString(lit.toString());
     }
 
+    @Override
+    public Expr<?> visitSimplifiedNode(SimplifiedExpression node) throws LJError {
+        return node.getSimplifiedExpression().accept(this);
+    }
+
     @Override
     public Expr<?> visitUnaryExpression(UnaryExpression exp) throws LJError {
         return switch (exp.getOp()) {
