Change SimplifiedExpression to SimplifiedPredicate

Author: rcosta358

…j_language/ast/SimplifiedExpression.java …ava/rj_language/SimplifiedPredicate.javaliquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java renamed to liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java renamed to liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java

@@ -1,73 +1,58 @@
-package liquidjava.rj_language.ast;
+package liquidjava.rj_language;
 
 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 {
+public class SimplifiedPredicate extends Predicate {
 
-    private final Expression origin;
+    private final Predicate simplified;
+    private final Predicate origin;
     private final List<Binder> binders;
 
-    public SimplifiedExpression(Expression simplified, Expression origin) {
+    public SimplifiedPredicate(Predicate simplified, Predicate origin) {
         this(simplified, origin, List.of());
     }
 
-    public SimplifiedExpression(Expression simplified, Expression origin, List<Binder> binders) {
-        addChild(simplified);
+    public SimplifiedPredicate(Predicate simplified, Predicate origin, List<Binder> binders) {
+        super(simplified.getExpression());
+        this.simplified = simplified;
         this.origin = origin;
         this.binders = new ArrayList<>(binders);
     }
 
-    public Expression getSimplifiedExpression() {
-        return children.get(0);
+    public Predicate getSimplifiedPredicate() {
+        return simplified;
     }
 
-    public Expression getOrigin() {
+    public Predicate 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();
+        return getSimplifiedPredicate().isBooleanTrue();
     }
 
     @Override
-    public Expression clone() {
-        return new SimplifiedExpression(getSimplifiedExpression().clone(), origin.clone(), binders);
+    public SimplifiedPredicate clone() {
+        return new SimplifiedPredicate(getSimplifiedPredicate().clone(), origin.clone(), binders);
     }
 
     @Override
     public String toString() {
-        return getSimplifiedExpression().toString();
+        return getSimplifiedPredicate().toString();
     }
 
     @Override
     public int hashCode() {
-        return Objects.hash(getSimplifiedExpression(), origin, binders);
+        return Objects.hash(getSimplifiedPredicate(), origin, binders);
     }
 
     @Override
@@ -78,8 +63,8 @@ public boolean equals(Object obj) {
             return false;
         if (getClass() != obj.getClass())
             return false;
-        SimplifiedExpression other = (SimplifiedExpression) obj;
-        return getSimplifiedExpression().equals(other.getSimplifiedExpression()) && origin.equals(other.origin)
+        SimplifiedPredicate other = (SimplifiedPredicate) obj;
+        return getSimplifiedPredicate().equals(other.getSimplifiedPredicate()) && origin.equals(other.origin)
                 && binders.equals(other.binders);
     }
 

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

@@ -82,9 +82,6 @@ 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;
@@ -102,8 +99,6 @@ 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());

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionFormatter.java

@@ -17,7 +17,6 @@
 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;
@@ -62,11 +61,9 @@ private String formatArguments(List<Expression> args) {
     }
 
     private Expression unwrapGroup(Expression expression) {
-        while (expression instanceof GroupExpression || expression instanceof SimplifiedExpression) {
+        while (expression instanceof GroupExpression) {
             if (expression instanceof GroupExpression group)
                 expression = group.getExpression();
-            else if (expression instanceof SimplifiedExpression node)
-                expression = node.getSimplifiedExpression();
         }
         return expression;
     }
@@ -166,11 +163,6 @@ 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);

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/formatter/ExpressionPrecedence.java

@@ -4,7 +4,6 @@
 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 {
@@ -17,8 +16,6 @@ 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)

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/typing/TypeInfer.java

@@ -15,7 +15,6 @@
 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;
@@ -58,9 +57,6 @@ 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();
     }
 

liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java

@@ -13,7 +13,6 @@
 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;
 
@@ -40,8 +39,6 @@ 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;

liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java

@@ -15,7 +15,6 @@
 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;
@@ -114,11 +113,6 @@ 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()) {