From fc2b06be6b1045d4e68149fe7ddbdb6051e352bf Mon Sep 17 00:00:00 2001 From: Ricardo Costa Date: Thu, 18 Jun 2026 20:54:13 +0100 Subject: [PATCH] Remove Group Expression --- .../java/liquidjava/diagnostics/DebugLog.java | 5 -- .../general_checkers/OperationsChecker.java | 11 +-- .../liquidjava/rj_language/Predicate.java | 4 -- .../rj_language/ast/Expression.java | 9 +-- .../rj_language/ast/GroupExpression.java | 70 ------------------- .../ast/formatter/ExpressionFormatter.java | 16 +---- .../ast/formatter/ExpressionPrecedence.java | 3 - .../rj_language/ast/typing/TypeInfer.java | 3 - .../opt/VCArithmeticSimplification.java | 14 ---- .../liquidjava/rj_language/opt/VCFolding.java | 4 -- .../opt/VCLogicalSimplification.java | 14 ---- .../visitors/CreateASTVisitor.java | 3 +- .../visitors/ExpressionVisitor.java | 5 +- .../liquidjava/smt/ExpressionToZ3Visitor.java | 6 -- .../rj_language/opt/VCFoldingTest.java | 6 +- .../rj_language/opt/VCSimplificationTest.java | 5 +- .../parsing/RefinementsParserTest.java | 12 ++++ 17 files changed, 25 insertions(+), 165 deletions(-) delete mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java index 02c407939..67ac7de16 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java +++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java @@ -7,7 +7,6 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.GroupExpression; import liquidjava.utils.Utils; import spoon.reflect.cu.SourcePosition; import spoon.reflect.reference.CtTypeReference; @@ -349,10 +348,6 @@ private static String formatConclusion(Predicate p) { } private static void flattenConjunction(Expression e, List out) { - if (e instanceof GroupExpression g) { - flattenConjunction(g.getExpression(), out); - return; - } if (e instanceof BinaryExpression b && "&&".equals(b.getOperator())) { flattenConjunction(b.getFirstOperand(), out); flattenConjunction(b.getSecondOperand(), out); diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java index 22b4c55bf..5e98d65b0 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java +++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java @@ -18,7 +18,6 @@ import liquidjava.rj_language.Predicate; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.GroupExpression; import org.apache.commons.lang3.NotImplementedException; import spoon.reflect.code.BinaryOperatorKind; import spoon.reflect.code.CtAssignment; @@ -344,7 +343,7 @@ private Predicate getConditionRefinement(CtExpression condition) throws } private Optional unwrapWildcardEquality(Predicate refinement) { - Expression expression = unwrapGroupExpression(refinement.getExpression()); + Expression expression = refinement.getExpression(); if (expression instanceof BinaryExpression binaryExpression && Ops.EQ.equals(binaryExpression.getOperator()) && Keys.WILDCARD.equals(binaryExpression.getFirstOperand().toString())) { return Optional.of(new Predicate(binaryExpression.getSecondOperand())); @@ -360,7 +359,7 @@ private Predicate valueFromRefinement(CtExpression element, Predicate refinem if (value.isPresent()) return value.get(); - Expression expression = unwrapGroupExpression(refinement.getExpression()); + Expression expression = refinement.getExpression(); boolean hasWildcard = refinement.getVariableNames().contains(Keys.WILDCARD); if (!hasWildcard && !expression.isBooleanExpression()) return new Predicate(expression); @@ -376,12 +375,6 @@ private Predicate createFreshValue(CtExpression element, Predicate refinement return Predicate.createVar(newName); } - private Expression unwrapGroupExpression(Expression expression) { - while (expression instanceof GroupExpression groupExpression) - expression = groupExpression.getExpression(); - return expression; - } - /** * Retrieves the refinements for the variable write inside unary operation * diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java index 0516b0985..ff69881ca 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java @@ -20,7 +20,6 @@ import liquidjava.rj_language.ast.Enum; import liquidjava.rj_language.ast.Expression; 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.LiteralChar; @@ -75,9 +74,6 @@ public Predicate(String ref, CtElement element) throws LJError { public Predicate(String ref, CtElement element, String prefix) throws LJError { this.prefix = prefix; exp = parse(ref, element); - if (!(exp instanceof GroupExpression)) { - exp = new GroupExpression(exp); - } exp = resolveStaticFinalConstants(exp, element); } 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..d33b4fcec 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 @@ -86,9 +86,6 @@ public boolean isBooleanExpression() { || this instanceof FunctionInvocation) { return true; } - if (this instanceof GroupExpression ge) { - return ge.getExpression().isBooleanExpression(); - } if (this instanceof BinaryExpression be) { return be.isBooleanOperation() || be.isLogicOperation(); } @@ -169,7 +166,7 @@ public Expression substituteState(Map subMap, String[] toCha sub = sub.substitute(new Var(s), v); } // substitute by sub in parent - e = new GroupExpression(sub); + e = sub; } } e.auxSubstituteState(subMap, toChange); @@ -191,7 +188,7 @@ private void auxSubstituteState(Map subMap, String[] toChang sub = sub.substitute(new Var(s), v); } // substitute by sub in parent - setChild(i, (sub instanceof GroupExpression) ? sub : new GroupExpression(sub)); + setChild(i, sub); } } exp.auxSubstituteState(subMap, toChange); @@ -228,7 +225,7 @@ public Expression changeAlias(Map alias, Context ctx, Factory } sub = sub.substitute(varExp, aliasExp); } - e = new GroupExpression(sub); + e = sub; } } e.auxChangeAlias(alias, ctx, f); 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 deleted file mode 100644 index 4597a1572..000000000 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/GroupExpression.java +++ /dev/null @@ -1,70 +0,0 @@ -package liquidjava.rj_language.ast; - -import java.util.List; - -import liquidjava.diagnostics.errors.LJError; -import liquidjava.rj_language.visitors.ExpressionVisitor; - -public class GroupExpression extends Expression { - - public GroupExpression(Expression e) { - addChild(e); - } - - public Expression getExpression() { - return children.get(0); - } - - @Override - public T accept(ExpressionVisitor visitor) throws LJError { - return visitor.visitGroupExpression(this); - } - - public String toString() { - return getExpression().toString(); - } - - @Override - public void getVariableNames(List toAdd) { - getExpression().getVariableNames(toAdd); - } - - @Override - public void getStateInvocations(List toAdd, List all) { - getExpression().getStateInvocations(toAdd, all); - } - - @Override - public Expression clone() { - return new GroupExpression(getExpression().clone()); - } - - @Override - public boolean isBooleanTrue() { - return getExpression().isBooleanTrue(); - } - - @Override - public int hashCode() { - final int prime = 31; - int result = 1; - result = prime * result + ((getExpression() == null) ? 0 : getExpression().hashCode()); - return result; - } - - @Override - public boolean equals(Object obj) { - if (this == obj) - return true; - if (obj == null) - return false; - if (getClass() != obj.getClass()) - return false; - GroupExpression other = (GroupExpression) obj; - if (getExpression() == null) { - return other.getExpression() == null; - } else { - return getExpression().equals(other.getExpression()); - } - } -} 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..88cab1e1a 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 @@ -8,7 +8,6 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; 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.LiteralChar; @@ -41,31 +40,23 @@ private String formatExpression(Expression expression) { } private String formatExpression(Expression expression, boolean shouldWrap) { - expression = unwrapGroup(expression); if (shouldWrap) return "(" + formatExpression(expression) + ")"; return formatExpression(expression); } private String formatOperand(Expression parent, Expression child, boolean rightOperand) { - child = unwrapGroup(child); return formatExpression(child, needsParentheses(parent, child, rightOperand)); } private String formatCondition(Expression child) { - return formatExpression(child, unwrapGroup(child) instanceof Ite); + return formatExpression(child, child instanceof Ite); } private String formatArguments(List args) { return args.stream().map(expression -> formatExpression(expression, false)).collect(Collectors.joining(", ")); } - private Expression unwrapGroup(Expression expression) { - while (expression instanceof GroupExpression group) - expression = group.getExpression(); - return expression; - } - private boolean needsParentheses(Expression parent, Expression child, boolean rightOperand) { ExpressionPrecedence parentPrecedence = ExpressionPrecedence.of(parent); ExpressionPrecedence childPrecedence = ExpressionPrecedence.of(child); @@ -120,11 +111,6 @@ public String visitFunctionInvocation(FunctionInvocation fun) { return Utils.getSimpleName(fun.getName()) + "(" + formatArguments(fun.getArgs()) + ")"; } - @Override - public String visitGroupExpression(GroupExpression exp) { - return formatExpression(exp.getExpression()); - } - @Override public String visitIte(Ite ite) { return formatCondition(ite.getCondition()) + " ? " + formatCondition(ite.getThen()) + " : " 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..c7df6bf58 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 @@ -2,7 +2,6 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.UnaryExpression; @@ -14,8 +13,6 @@ public boolean isLowerThan(ExpressionPrecedence other) { } public static ExpressionPrecedence of(Expression expression) { - if (expression instanceof GroupExpression group) - return of(group.getExpression()); 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 59cd6a0f2..139128ed0 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 @@ -7,7 +7,6 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; 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.LiteralChar; @@ -51,8 +50,6 @@ else if (e instanceof Ite) return boolType(factory); else if (e instanceof BinaryExpression) return binaryType(ctx, factory, (BinaryExpression) e); - else if (e instanceof GroupExpression) - return getType(ctx, factory, ((GroupExpression) e).getExpression()); else if (e instanceof FunctionInvocation) return functionType(ctx, (FunctionInvocation) e); else if (e instanceof AliasInvocation) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java index 959c799d2..5b752c91f 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCArithmeticSimplification.java @@ -6,7 +6,6 @@ import liquidjava.processor.VCImplication; import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.LiteralInt; import liquidjava.rj_language.ast.LiteralReal; @@ -44,8 +43,6 @@ private Expression simplifyExpression(Expression expression, List no return simplifyUnary(unary, nonZeroExpressions); if (expression instanceof Ite ite) return simplifyIte(ite, nonZeroExpressions); - if (expression instanceof GroupExpression group) - return simplifyGroup(group, nonZeroExpressions); return expression.clone(); } @@ -108,17 +105,6 @@ private Expression simplifyIte(Ite ite, List nonZeroExpressions) { return new Ite(condition.clone(), thenExpression.clone(), elseExpression.clone()); } - /** - * Simplifies an expression wrapped in parentheses while preserving the group node - */ - private Expression simplifyGroup(GroupExpression group, List nonZeroExpressions) { - Expression expression = group.getExpression(); - Expression simplified = simplifyExpression(expression, nonZeroExpressions); - if (!expression.equals(simplified)) - return new GroupExpression(simplified); - return group.clone(); - } - /** * Dispatches a local binary arithmetic identity by operator */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java index eaa4760d4..0f7476604 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java @@ -3,7 +3,6 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Enum; import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.LiteralInt; @@ -33,9 +32,6 @@ private Expression fold(Expression expression) { return foldUnary(unary); if (expression instanceof Ite ite) return foldIte(ite); - // (x) -> x - if (expression instanceof GroupExpression group && group.getChildren().size() == 1) - return group.getExpression().clone(); return expression.clone(); } diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java index 2ba262602..d8fef4719 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java @@ -5,7 +5,6 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Expression; -import liquidjava.rj_language.ast.GroupExpression; import liquidjava.rj_language.ast.Ite; import liquidjava.rj_language.ast.LiteralBoolean; import liquidjava.rj_language.ast.UnaryExpression; @@ -30,8 +29,6 @@ private Expression simplify(Expression expression) { return simplifyUnary(unary); if (expression instanceof Ite ite) return simplifyIte(ite); - if (expression instanceof GroupExpression group) - return simplifyGroup(group); return expression.clone(); } @@ -94,17 +91,6 @@ private Expression simplifyIte(Ite ite) { return new Ite(condition.clone(), thenExpression.clone(), elseExpression.clone()); } - /** - * Simplifies an expression wrapped in parentheses while preserving the group node - */ - private Expression simplifyGroup(GroupExpression group) { - Expression expression = group.getExpression(); - Expression simplified = simplify(expression); - if (!expression.equals(simplified)) - return new GroupExpression(simplified); - return group.clone(); - } - /** * Dispatches a local binary logical identity by operator */ diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java index 680c4695d..1e8ba70a3 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/visitors/CreateASTVisitor.java @@ -10,7 +10,6 @@ import liquidjava.rj_language.ast.Enum; import liquidjava.rj_language.ast.Expression; 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; @@ -96,7 +95,7 @@ private Expression startCreate(ParseTree rc) throws LJError { private Expression predCreate(ParseTree rc) throws LJError { if (rc instanceof PredGroupContext) - return new GroupExpression(create(((PredGroupContext) rc).pred())); + return create(((PredGroupContext) rc).pred()); else if (rc instanceof OpLiteralContext) return create(((OpLiteralContext) rc).literalExpression()); else if (rc instanceof OpMinusContext) 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..f7fe1daf3 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 @@ -5,7 +5,6 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Enum; 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.LiteralChar; @@ -23,8 +22,6 @@ public interface ExpressionVisitor { T visitFunctionInvocation(FunctionInvocation fun) throws LJError; - T visitGroupExpression(GroupExpression exp) throws LJError; - T visitIte(Ite ite) throws LJError; T visitLiteralInt(LiteralInt lit) throws LJError; @@ -44,4 +41,4 @@ public interface ExpressionVisitor { 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..f3a2b21b1 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java +++ b/liquidjava-verifier/src/main/java/liquidjava/smt/ExpressionToZ3Visitor.java @@ -7,7 +7,6 @@ import liquidjava.rj_language.ast.BinaryExpression; import liquidjava.rj_language.ast.Enum; 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.LiteralChar; @@ -68,11 +67,6 @@ public Expr visitFunctionInvocation(FunctionInvocation fun) throws LJError { return ctx.makeFunctionInvocation(fun.getName(), argsExpr); } - @Override - public Expr visitGroupExpression(GroupExpression exp) throws LJError { - return exp.getExpression().accept(this); - } - @Override public Expr visitIte(Ite ite) throws LJError { return ctx.makeIte(ite.getCondition().accept(this), ite.getThen().accept(this), ite.getElse().accept(this)); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java index 15cc99bc3..0c23c4f1c 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCFoldingTest.java @@ -38,8 +38,8 @@ void leavesRealDivisionAndModuloByZeroUnchanged() { @Test void foldsIntegerDivisionTowardZeroForNegativeResults() { - assertSimplificationSteps(folding, vc("(2 - 7) / 2 == -2"), step("(2 - 7) / 2 == -2"), step("-5 / 2 == -2"), - step("-2 == -2"), step("-2 == -2"), step("true")); + assertSimplificationSteps(folding, vc("(2 - 7) / 2 == -2"), step("-5 / 2 == -2"), step("-2 == -2"), + step("-2 == -2"), step("true")); } @Test @@ -104,7 +104,7 @@ void foldsEnumEqualityAndInequality() { } @Test - void recordsOriginWhenOnlyGroupIsUnwrapped() { + void leavesParenthesizedExpressionUnchanged() { assertSimplificationSteps(folding, vc("(x > 0)"), step("x > 0")); } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java index 908ea7164..1ec9ebc6a 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCSimplificationTest.java @@ -91,9 +91,8 @@ void simplifyOnceAppliesLogicalWhenNoEarlierSimplificationIsAvailable() { } @Test - void simplifyUsesFoldingToEnableSubstitutionOnNextStep() { - assertSimplificationSteps(vc("∀x:int. (x) == 3", "x > 0"), step("x == 3", "x > 0"), step("3 > 0"), - step("true")); + void parenthesesDoNotDelaySubstitution() { + assertSimplificationSteps(vc("∀x:int. (x) == 3", "x > 0"), step("3 > 0"), step("true")); } @Test diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/parsing/RefinementsParserTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/parsing/RefinementsParserTest.java index d9c0686e3..cd5c80e2f 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/parsing/RefinementsParserTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/parsing/RefinementsParserTest.java @@ -6,6 +6,8 @@ import org.junit.jupiter.api.Test; import liquidjava.diagnostics.errors.SyntaxError; +import liquidjava.rj_language.ast.BinaryExpression; +import liquidjava.rj_language.ast.Expression; class RefinementsParserTest { @@ -33,4 +35,14 @@ void noHintForUnrelatedSyntaxError() { SyntaxError e = assertThrows(SyntaxError.class, () -> RefinementsParser.createAST("a +", "")); assertEquals("", e.getDetails()); } + + @Test + void parenthesesAreRepresentedByExpressionStructure() { + Expression expression = RefinementsParser.createAST("(a + b) * c", ""); + BinaryExpression product = (BinaryExpression) expression; + BinaryExpression sum = (BinaryExpression) product.getFirstOperand(); + + assertEquals("*", product.getOperator()); + assertEquals("+", sum.getOperator()); + } }