From 05680e2f38cadb61df8c691229d371ce37ddbcc9 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 8 Jun 2026 11:19:11 +0100 Subject: [PATCH 1/6] Add SimplifiedExpression --- .../rj_language/ast/Expression.java | 5 + .../rj_language/ast/SimplifiedExpression.java | 124 ++++++++++++++++++ .../ast/formatter/ExpressionFormatter.java | 14 +- .../ast/formatter/ExpressionPrecedence.java | 3 + .../rj_language/ast/typing/TypeInfer.java | 3 + .../visitors/ExpressionVisitor.java | 5 +- .../liquidjava/smt/ExpressionToZ3Visitor.java | 6 + 7 files changed, 157 insertions(+), 3 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java 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 index ee638262e..20c9fe84e 100644 --- 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 getConjuncts() { + if (this instanceof SimplifiedExpression node) + return node.getSimplifiedExpression().getConjuncts(); if (this instanceof BinaryExpression binaryExpression && "&&".equals(binaryExpression.getOperator())) { List 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 new file mode 100644 index 000000000..e06bbc2dc --- /dev/null +++ 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 binders; + + public SimplifiedExpression(Expression simplified, Expression origin) { + this(simplified, origin, List.of()); + } + + public SimplifiedExpression(Expression simplified, Expression origin, List 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 getBinders() { + return binders; + } + + @Override + public T accept(ExpressionVisitor visitor) throws LJError { + return visitor.visitSimplifiedNode(this); + } + + @Override + public void getVariableNames(List toAdd) { + getSimplifiedExpression().getVariableNames(toAdd); + } + + @Override + public void getStateInvocations(List toAdd, List 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 index cf6e4fdce..34d71a1d2 100644 --- 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 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 index fbaa95cbe..ce9678c52 100644 --- 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 index 0fa965cde..140c7ed88 100644 --- 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 index 904690a79..cd2e9e384 100644 --- 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 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; -} \ No newline at end of file +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java index 464cd9898..edf4ba9be 100644 --- 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()) { From d845fa3b8f7dff649a53d3d0a2bf326bb69805a2 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Mon, 8 Jun 2026 18:23:48 +0100 Subject: [PATCH 2/6] Change SimplifiedExpression to SimplifiedPredicate --- ...pression.java => SimplifiedPredicate.java} | 51 +++++++------------ .../rj_language/ast/Expression.java | 5 -- .../ast/formatter/ExpressionFormatter.java | 10 +--- .../ast/formatter/ExpressionPrecedence.java | 3 -- .../rj_language/ast/typing/TypeInfer.java | 4 -- .../visitors/ExpressionVisitor.java | 3 -- .../liquidjava/smt/ExpressionToZ3Visitor.java | 6 --- 7 files changed, 19 insertions(+), 63 deletions(-) rename liquidjava-verifier/src/main/java/liquidjava/rj_language/{ast/SimplifiedExpression.java => SimplifiedPredicate.java} (55%) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java similarity index 55% rename from liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java rename to liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java index e06bbc2dc..de2f34b80 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/SimplifiedExpression.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java @@ -1,33 +1,33 @@ -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 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 binders) { - addChild(simplified); + public SimplifiedPredicate(Predicate simplified, Predicate origin, List 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; } @@ -35,39 +35,24 @@ public List getBinders() { return binders; } - @Override - public T accept(ExpressionVisitor visitor) throws LJError { - return visitor.visitSimplifiedNode(this); - } - - @Override - public void getVariableNames(List toAdd) { - getSimplifiedExpression().getVariableNames(toAdd); - } - - @Override - public void getStateInvocations(List toAdd, List 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); } 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 index 20c9fe84e..ee638262e 100644 --- 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,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 getConjuncts() { - if (this instanceof SimplifiedExpression node) - return node.getSimplifiedExpression().getConjuncts(); if (this instanceof BinaryExpression binaryExpression && "&&".equals(binaryExpression.getOperator())) { List conjuncts = new ArrayList<>(); conjuncts.addAll(binaryExpression.getFirstOperand().getConjuncts()); 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 index 34d71a1d2..2135f41d4 100644 --- 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,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 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); 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 index ce9678c52..fbaa95cbe 100644 --- 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,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) 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 index 140c7ed88..59cd6a0f2 100644 --- 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,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(); } 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 index cd2e9e384..24d030fc9 100644 --- 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,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 visitLiteralString(LiteralString lit) throws LJError; - T visitSimplifiedNode(SimplifiedExpression node) throws LJError; - T visitUnaryExpression(UnaryExpression exp) throws LJError; T visitEnum(Enum en) throws LJError; diff --git a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java index edf4ba9be..464cd9898 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/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()) { From 23cb1b0676884cd584c7a5a8290e4b330ae86e81 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 13:48:42 +0100 Subject: [PATCH 3/6] Requested Changes --- .../rj_language/SimplifiedPredicate.java | 20 ++++--------------- .../ast/formatter/ExpressionFormatter.java | 5 ++--- 2 files changed, 6 insertions(+), 19 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java index de2f34b80..ab0120ca7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java @@ -8,7 +8,6 @@ public class SimplifiedPredicate extends Predicate { - private final Predicate simplified; private final Predicate origin; private final List binders; @@ -18,13 +17,12 @@ public SimplifiedPredicate(Predicate simplified, Predicate origin) { public SimplifiedPredicate(Predicate simplified, Predicate origin, List binders) { super(simplified.getExpression()); - this.simplified = simplified; this.origin = origin; this.binders = new ArrayList<>(binders); } public Predicate getSimplifiedPredicate() { - return simplified; + return new Predicate(getExpression()); } public Predicate getOrigin() { @@ -35,24 +33,14 @@ public List getBinders() { return binders; } - @Override - public boolean isBooleanTrue() { - return getSimplifiedPredicate().isBooleanTrue(); - } - @Override public SimplifiedPredicate clone() { - return new SimplifiedPredicate(getSimplifiedPredicate().clone(), origin.clone(), binders); - } - - @Override - public String toString() { - return getSimplifiedPredicate().toString(); + return new SimplifiedPredicate(new Predicate(getExpression().clone()), origin.clone(), binders); } @Override public int hashCode() { - return Objects.hash(getSimplifiedPredicate(), origin, binders); + return Objects.hash(getExpression(), origin, binders); } @Override @@ -64,7 +52,7 @@ public boolean equals(Object obj) { if (getClass() != obj.getClass()) return false; SimplifiedPredicate other = (SimplifiedPredicate) obj; - return getSimplifiedPredicate().equals(other.getSimplifiedPredicate()) && origin.equals(other.origin) + return getExpression().equals(other.getExpression()) && origin.equals(other.origin) && binders.equals(other.binders); } 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 index 2135f41d4..b26026f6c 100644 --- 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 @@ -61,9 +61,8 @@ private String formatArguments(List args) { } private Expression unwrapGroup(Expression expression) { - while (expression instanceof GroupExpression) { - if (expression instanceof GroupExpression group) - expression = group.getExpression(); + while (expression instanceof GroupExpression group) { + expression = group.getExpression(); } return expression; } From 604bcef893374ba5ac0082b117467e2776b81631 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 13:59:57 +0100 Subject: [PATCH 4/6] Add JavaDocs --- .../liquidjava/rj_language/SimplifiedPredicate.java | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java index ab0120ca7..b38859b0e 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java @@ -6,6 +6,13 @@ import spoon.reflect.reference.CtTypeReference; +/** + * Represents a predicate simplified from another predicate. Stores the original predicate and any variables that must + * be reintroduced as binders when relating the simplified predicate back to its origin. + *

+ * For example, simplifying {@code x == 1 && y > x} with binders {@code x: int, y: int} may produce + * {@code y > 1}. The origin {@code x == 1 && y > x} and binder {@code x: int} are kept so we can relate the simplified predicate back to the original. + */ public class SimplifiedPredicate extends Predicate { private final Predicate origin; @@ -56,6 +63,9 @@ public boolean equals(Object obj) { && binders.equals(other.binders); } + /** + * Represents a variable that must be bound when relating the simplified predicate to its origin + */ public static class Binder { private final String name; private final String type; From 1bc748ad60c8d7dc5f6aa225fb42468b112dde89 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 14:08:10 +0100 Subject: [PATCH 5/6] Formatting --- .../java/liquidjava/rj_language/SimplifiedPredicate.java | 5 +++-- .../rj_language/ast/formatter/ExpressionFormatter.java | 3 +-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java index b38859b0e..bf86d4c20 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/SimplifiedPredicate.java @@ -10,8 +10,9 @@ * Represents a predicate simplified from another predicate. Stores the original predicate and any variables that must * be reintroduced as binders when relating the simplified predicate back to its origin. *

- * For example, simplifying {@code x == 1 && y > x} with binders {@code x: int, y: int} may produce - * {@code y > 1}. The origin {@code x == 1 && y > x} and binder {@code x: int} are kept so we can relate the simplified predicate back to the original. + * For example, simplifying {@code x == 1 && y > x} with binders {@code x: int, y: int} may produce {@code y > 1}. The + * origin {@code x == 1 && y > x} and binder {@code x: int} are kept so we can relate the simplified predicate back to + * the original. */ public class SimplifiedPredicate extends Predicate { 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 index b26026f6c..cf6e4fdce 100644 --- 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 @@ -61,9 +61,8 @@ private String formatArguments(List args) { } private Expression unwrapGroup(Expression expression) { - while (expression instanceof GroupExpression group) { + while (expression instanceof GroupExpression group) expression = group.getExpression(); - } return expression; } From dfb80ab2033669eccc6ab52459c56b9c2ab93fd1 Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Tue, 9 Jun 2026 14:44:29 +0100 Subject: [PATCH 6/6] Minor Changes --- .../main/java/liquidjava/rj_language/ast/typing/TypeInfer.java | 1 + .../java/liquidjava/rj_language/visitors/ExpressionVisitor.java | 2 +- 2 files changed, 2 insertions(+), 1 deletion(-) 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 index 59cd6a0f2..0fa965cde 100644 --- 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 @@ -57,6 +57,7 @@ else if (e instanceof FunctionInvocation) return functionType(ctx, (FunctionInvocation) e); else if (e instanceof AliasInvocation) return boolType(factory); + 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 index 24d030fc9..904690a79 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/ExpressionVisitor.java @@ -44,4 +44,4 @@ public interface ExpressionVisitor { T visitEnum(Enum en) throws LJError; T visitVar(Var var) throws LJError; -} +} \ No newline at end of file