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 6b48459e..d2dbccbe 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 @@ -243,29 +243,18 @@ private static Expression simplifyModulo(Expression left, Expression right, List } /** - * Records direct non-zero premises from equalities and inequalities + * Records direct non-zero premises shaped as x != 0 or 0 != x */ private static void addNonZeroExpression(Expression expression, List nonZeroExpressions) { - if (!(expression instanceof BinaryExpression binary)) + if (!(expression instanceof BinaryExpression binary) || !"!=".equals(binary.getOperator())) return; Expression left = binary.getFirstOperand(); Expression right = binary.getSecondOperand(); - if ("!=".equals(binary.getOperator())) { - // x != 0 -> x is non-zero - if (isZero(right)) - nonZeroExpressions.add(left.clone()); - // 0 != x -> x is non-zero - if (isZero(left)) - nonZeroExpressions.add(right.clone()); - } else if ("==".equals(binary.getOperator())) { - // x == n && n != 0 -> x is non-zero - if (isNumericLiteral(right) && !isZero(right)) - nonZeroExpressions.add(left.clone()); - // n == x && n != 0 -> x is non-zero - if (isNumericLiteral(left) && !isZero(left)) - nonZeroExpressions.add(right.clone()); - } + if (isZero(left)) + nonZeroExpressions.add(right.clone()); + if (isZero(right)) + nonZeroExpressions.add(left.clone()); } /** @@ -286,13 +275,6 @@ private static boolean isZero(Expression expression) { return false; } - /** - * Checks whether an expression is a numeric literal - */ - private static boolean isNumericLiteral(Expression expression) { - return expression instanceof LiteralInt || expression instanceof LiteralReal; - } - /** * Checks whether an expression is a numeric one literal */ 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 new file mode 100644 index 00000000..743ad9a4 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java @@ -0,0 +1,251 @@ +package liquidjava.rj_language.opt; + +import liquidjava.processor.SimplifiedVCImplication; +import liquidjava.processor.VCImplication; +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.rj_language.ast.Ite; +import liquidjava.rj_language.ast.LiteralBoolean; +import liquidjava.rj_language.ast.UnaryExpression; + +/** + * Simplifies VCImplication chains by applying logical identities inside refinements + */ +public class VCLogicalSimplification { + + /** + * Applies the first logical simplification available in a VC chain + */ + public static VCImplication apply(VCImplication implication) { + if (implication == null) + return null; + + Expression expression = implication.getRefinement().getExpression(); + Expression simplified = simplify(expression); + if (!expression.equals(simplified)) { + VCImplication result = new SimplifiedVCImplication(implication, new Predicate(simplified), implication); + result.setNext(implication.getNext() == null ? null : implication.getNext().clone()); + return result; + } + + VCImplication next = apply(implication.getNext()); + if (implication.getNext() == null || implication.getNext().equals(next)) + return implication; + + VCImplication result = implication.copyWithRefinement(implication.getRefinement().clone()); + result.setNext(next); + return result; + } + + /** + * Simplifies the first logical identity found inside an expression + */ + private static Expression simplify(Expression expression) { + if (expression instanceof BinaryExpression binary) + return simplifyBinary(binary); + if (expression instanceof UnaryExpression unary) + return simplifyUnary(unary); + if (expression instanceof Ite ite) + return simplifyIte(ite); + if (expression instanceof GroupExpression group) + return simplifyGroup(group); + return expression.clone(); + } + + /** + * Simplifies a binary expression by visiting operands before the current node + */ + private static Expression simplifyBinary(BinaryExpression binary) { + Expression left = binary.getFirstOperand(); + Expression simplifiedLeft = simplify(left); + if (!left.equals(simplifiedLeft)) + return new BinaryExpression(simplifiedLeft, binary.getOperator(), binary.getSecondOperand().clone()); + + Expression right = binary.getSecondOperand(); + Expression simplifiedRight = simplify(right); + if (!right.equals(simplifiedRight)) + return new BinaryExpression(left.clone(), binary.getOperator(), simplifiedRight); + + Expression simplifiedBinary = simplifyLocalBinary(left, right, binary.getOperator()); + if (simplifiedBinary != null) + return simplifiedBinary; + + return new BinaryExpression(left.clone(), binary.getOperator(), right.clone()); + } + + /** + * Simplifies a unary expression by visiting its operand before the current node + */ + private static Expression simplifyUnary(UnaryExpression unary) { + Expression operand = unary.getExpression(); + Expression simplifiedOperand = simplify(operand); + if (!operand.equals(simplifiedOperand)) + return new UnaryExpression(unary.getOp(), simplifiedOperand); + + // !!x -> x + if ("!".equals(unary.getOp()) && isNot(operand)) + return negatedExpression(operand).clone(); + + return new UnaryExpression(unary.getOp(), operand.clone()); + } + + /** + * Simplifies a ternary expression by visiting condition, then branch, and else branch + */ + private static Expression simplifyIte(Ite ite) { + Expression condition = ite.getCondition(); + Expression simplifiedCondition = simplify(condition); + if (!condition.equals(simplifiedCondition)) + return new Ite(simplifiedCondition, ite.getThen().clone(), ite.getElse().clone()); + + Expression thenExpression = ite.getThen(); + Expression simplifiedThen = simplify(thenExpression); + if (!thenExpression.equals(simplifiedThen)) + return new Ite(condition.clone(), simplifiedThen, ite.getElse().clone()); + + Expression elseExpression = ite.getElse(); + Expression simplifiedElse = simplify(elseExpression); + if (!elseExpression.equals(simplifiedElse)) + return new Ite(condition.clone(), thenExpression.clone(), simplifiedElse); + + return new Ite(condition.clone(), thenExpression.clone(), elseExpression.clone()); + } + + /** + * Simplifies an expression wrapped in parentheses while preserving the group node + */ + private static 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 + */ + private static Expression simplifyLocalBinary(Expression left, Expression right, String op) { + return switch (op) { + case "&&" -> simplifyConjunction(left, right); + case "||" -> simplifyDisjunction(left, right); + case "==" -> simplifyEquality(left, right); + case "!=" -> simplifyInequality(left, right); + case "-->" -> simplifyImplication(left, right); + default -> null; + }; + } + + /** + * Applies conjunction identities involving boolean literals and same operands + */ + private static Expression simplifyConjunction(Expression left, Expression right) { + // x && true -> x + if (isTrue(right)) + return left.clone(); + // true && x -> x + if (isTrue(left)) + return right.clone(); + // x && false -> false + if (isFalse(right)) + return right.clone(); + // false && x -> false + if (isFalse(left)) + return left.clone(); + // p && p -> p + if (left.equals(right)) + return left.clone(); + return null; + } + + /** + * Applies disjunction identities involving boolean literals and same operands + */ + private static Expression simplifyDisjunction(Expression left, Expression right) { + // x || true -> true + if (isTrue(right)) + return right.clone(); + // true || x -> true + if (isTrue(left)) + return left.clone(); + // x || false -> x + if (isFalse(right)) + return left.clone(); + // false || x -> x + if (isFalse(left)) + return right.clone(); + // p || p -> p + if (left.equals(right)) + return left.clone(); + return null; + } + + /** + * Applies equality identity for same operands + */ + private static Expression simplifyEquality(Expression left, Expression right) { + // x == x -> true + if (left.equals(right)) + return new LiteralBoolean(true); + return null; + } + + /** + * Applies inequality identity for same operands + */ + private static Expression simplifyInequality(Expression left, Expression right) { + // x != x -> false + if (left.equals(right)) + return new LiteralBoolean(false); + return null; + } + + /** + * Applies implication identities involving boolean literals and same operands + */ + private static Expression simplifyImplication(Expression left, Expression right) { + // x --> true -> true + if (isTrue(right)) + return right.clone(); + // false --> x -> true + if (isFalse(left)) + return new LiteralBoolean(true); + // true --> x -> x + if (isTrue(left)) + return right.clone(); + // x --> x -> true + if (left.equals(right)) + return new LiteralBoolean(true); + return null; + } + + /** + * Checks whether an expression is true + */ + private static boolean isTrue(Expression expression) { + return expression instanceof LiteralBoolean literal && literal.isBooleanTrue(); + } + + /** + * Checks whether an expression is false + */ + private static boolean isFalse(Expression expression) { + return expression instanceof LiteralBoolean literal && !literal.isBooleanTrue(); + } + + /** + * Checks whether an expression is unary logical negation + */ + private static boolean isNot(Expression expression) { + return expression instanceof UnaryExpression unary && "!".equals(unary.getOp()); + } + + /** + * Returns the operand of a unary logical negation expression + */ + private static Expression negatedExpression(Expression expression) { + return ((UnaryExpression) expression).getExpression(); + } +} diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java index 6854b547..4c0dbec4 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java @@ -11,7 +11,7 @@ public class VCSimplification { private static final List> PASSES = List.of(VCSubstitution::apply, VCFolding::apply, - VCArithmeticSimplification::apply); + VCArithmeticSimplification::apply, VCLogicalSimplification::apply); /** * Applies all available simplification steps to a VC chain until a fixed point is reached diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java index 69bf921e..88440c49 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCArithmeticSimplificationTest.java @@ -70,16 +70,6 @@ void simplifiesGuardedDivisionAndModuloIdentities() { chain(expect("0 != x", "0 != x"), expect("0 == 0", "x % x == 0"))); } - @Test - void simplifiesGuardedDivisionAndModuloIdentitiesWhenEqualityImpliesNonZero() { - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x == 1", "0 / x == 0"), - chain(expect("x == 1", "x == 1"), expect("0 == 0", "0 / x == 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("1 == x", "x / x == 1"), - chain(expect("1 == x", "1 == x"), expect("1 == 1", "x / x == 1"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("x == 1", "x % x == 0"), - chain(expect("x == 1", "x == 1"), expect("0 == 0", "x % x == 0"))); - } - @Test void leavesUnguardedDivisionAndModuloIdentitiesUnchanged() { assertSimplificationSteps(VCArithmeticSimplification::apply, vc("0 / x == 0"), @@ -96,21 +86,6 @@ void simplifiesOnlyFirstArithmeticIdentity() { chain(expect("x + 1 > 0", "x + 0 + 1 > 0"))); } - @Test - void simplifiesTernaryExpressionsInConditionThenElseOrder() { - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("(flag + 0 > 0 ? x + 0 : y + 0) > 0"), - chain(expect("(flag > 0 ? x + 0 : y + 0) > 0", "(flag + 0 > 0 ? x + 0 : y + 0) > 0")), - chain(expect("(flag > 0 ? x : y + 0) > 0", "(flag > 0 ? x + 0 : y + 0) > 0")), - chain(expect("(flag > 0 ? x : y) > 0", "(flag > 0 ? x : y + 0) > 0"))); - } - - @Test - void simplifiesGroupedExpressionsAndLeavesUnchangedGroupsAlone() { - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("(x + 0) * y > 0"), - chain(expect("x * y > 0", "(x + 0) * y > 0"))); - assertSimplificationSteps(VCArithmeticSimplification::apply, vc("(x) > 0"), chain(expect("x > 0", "x > 0"))); - } - @Test void recordsOriginWhenSimplifyingLaterImplication() { VCImplication implication = vc("x > 0", "y + 0 > x"); diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java index 104a619c..f3e19ff9 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCImplicationGenerator.java @@ -21,7 +21,7 @@ public VCImplicationGenerator() { @Override public VCImplication generate(SourceOfRandomness random, GenerationStatus status) { - return switch (random.nextInt(0, 11)) { + return switch (random.nextInt(0, 12)) { case 0 -> vc(substitution(random, "x"), comparison(random, "x")); case 1 -> vc(reverseSubstitution(random, "x"), comparison(random, "x")); case 2 -> vc(nonSubstitution(random, "x"), substitution(random, "y"), comparison(random, "y")); @@ -33,6 +33,7 @@ public VCImplication generate(SourceOfRandomness random, GenerationStatus status case 8 -> vc(adjacentConstants(random) + " " + comparisonOperator(random) + " " + intLiteral(random)); case 9 -> vc(arithmeticIdentity(random)); case 10 -> guardedArithmeticIdentity(random); + case 11 -> vc(logicalIdentity(random)); default -> vc(substitution(random, "x"), substitution(random, "y"), foldableComparison(random)); }; } @@ -124,6 +125,29 @@ private static VCImplication guardedArithmeticIdentity(SourceOfRandomness random return vc(guard, use); } + private static String logicalIdentity(SourceOfRandomness random) { + String predicate = "(" + comparison(random, FREE_VARS[random.nextInt(0, FREE_VARS.length - 1)]) + ")"; + return switch (random.nextInt(0, 16)) { + case 0 -> predicate + " && true"; + case 1 -> "true && " + predicate; + case 2 -> predicate + " && false"; + case 3 -> "false && " + predicate; + case 4 -> predicate + " || true"; + case 5 -> "true || " + predicate; + case 6 -> predicate + " || false"; + case 7 -> "false || " + predicate; + case 8 -> predicate + " && " + predicate; + case 9 -> predicate + " || " + predicate; + case 10 -> predicate + " --> true"; + case 11 -> "false --> " + predicate; + case 12 -> "true --> " + predicate; + case 13 -> predicate + " --> " + predicate; + case 14 -> predicate + " == " + predicate; + case 15 -> predicate + " != " + predicate; + default -> "!!" + predicate; + }; + } + private static String comparisonOperator(SourceOfRandomness random) { return COMPARISON_OPS[random.nextInt(0, COMPARISON_OPS.length - 1)]; } diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java new file mode 100644 index 00000000..47b51438 --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java @@ -0,0 +1,99 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.utils.VCTestUtils.*; +import static org.junit.jupiter.api.Assertions.assertEquals; +import static org.junit.jupiter.api.Assertions.assertInstanceOf; +import static org.junit.jupiter.api.Assertions.assertNull; + +import liquidjava.processor.SimplifiedVCImplication; +import liquidjava.processor.VCImplication; +import org.junit.jupiter.api.Test; + +class VCLogicalSimplificationTest { + + @Test + void applyReturnsNullForNullImplication() { + assertNull(VCLogicalSimplification.apply(null)); + } + + @Test + void simplifiesConjunctionWithBooleanLiterals() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x && true"), chain(expect("x", "x && true"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("true && x"), chain(expect("x", "true && x"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x && false"), + chain(expect("false", "x && false"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("false && x"), + chain(expect("false", "false && x"))); + } + + @Test + void simplifiesDisjunctionWithBooleanLiterals() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x || true"), chain(expect("true", "x || true"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("true || x"), chain(expect("true", "true || x"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x || false"), chain(expect("x", "x || false"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("false || x"), chain(expect("x", "false || x"))); + } + + @Test + void simplifiesDoubleNegation() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("!!x"), chain(expect("x", "!!x"))); + } + + @Test + void simplifiesDuplicateLogicalOperands() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("p && p"), chain(expect("p", "p && p"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("p || p"), chain(expect("p", "p || p"))); + } + + @Test + void simplifiesSelfEqualityAndInequality() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x == x"), chain(expect("true", "x == x"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x != x"), chain(expect("false", "x != x"))); + } + + @Test + void simplifiesImplicationIdentities() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x --> true"), + chain(expect("true", "x --> true"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("false --> x"), + chain(expect("true", "false --> x"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("true --> x"), chain(expect("x", "true --> x"))); + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x --> x"), chain(expect("true", "x --> x"))); + } + + @Test + void simplifiesOnlyFirstLogicalIdentity() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("x && true && false"), + chain(expect("x && false", "x && true && false"))); + } + + @Test + void simplifiesNestedExpressionsBeforeParent() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("(x && true) || false"), + chain(expect("x || false", "x && true || false"))); + } + + @Test + void simplifiesIteChildren() { + assertSimplificationSteps(VCLogicalSimplification::apply, vc("cond ? x && true : y || false"), + chain(expect("cond ? x : y || false", "cond ? x && true : y || false"))); + } + + @Test + void recordsOriginWhenSimplifyingLaterImplication() { + VCImplication implication = vc("x > 0", "y || false"); + + VCImplication result = assertSimplificationSteps(VCLogicalSimplification::apply, implication, + chain(expect("x > 0", "x > 0"), expect("y", "y || false"))); + + SimplifiedVCImplication simplifiedNext = assertInstanceOf(SimplifiedVCImplication.class, result.getNext()); + assertEquals("y || false", simplifiedNext.getOrigin().getRefinement().getExpression().toDisplayString()); + } + + @Test + void recordsCurrentImplicationAsOriginWhenSimplifyingExistingSimplifiedImplication() { + VCImplication substituted = VCSubstitution.apply(vc("∀x:int. x == y", "x == x")); + + assertSimplificationSteps(VCLogicalSimplification::apply, substituted, chain(expect("true", "y == y"))); + } +} 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 ffe65220..5565e311 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 @@ -59,6 +59,29 @@ void simplifyOnceAppliesArithmeticWhenNoSubstitutionOrFoldingIsAvailable() { assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x > 0", "x + 0 > 0"))); } + @Test + void simplifyOnceAppliesArithmeticBeforeLogicalSimplification() { + VCImplication implication = vc("x + 0 == x"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x == x", "x + 0 == x")), + chain(expect("true", "x == x"))); + } + + @Test + void simplifyOnceAppliesLogicalWhenNoEarlierSimplificationIsAvailable() { + VCImplication implication = vc("x && true"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, chain(expect("x", "x && true"))); + } + + @Test + void simplifyAppliesLogicalStepsUntilFixedPoint() { + VCImplication implication = vc("x && true && true"); + + assertSimplificationSteps(VCSimplification::simplifyOnce, implication, + chain(expect("x && true", "x && true && true")), chain(expect("x", "x && true"))); + } + @Test void simplifyKeepsApplyingStepsUntilFixedPoint() { VCImplication implication = vc("∀x:int. x == 1 + 2", "x + 1 > 3");