Fold ternaries that a fact of Found decides on an enum value

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java

@@ -0,0 +1,119 @@
+package liquidjava.rj_language.opt;
+
+import static liquidjava.rj_language.opt.VCSimplificationUtils.copyWithRefinement;
+import static liquidjava.rj_language.opt.VCSimplificationUtils.factsOf;
+
+import java.util.HashMap;
+import java.util.Map;
+
+import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Enum;
+import liquidjava.rj_language.ast.Expression;
+import liquidjava.rj_language.ast.LiteralBoolean;
+import liquidjava.rj_language.ast.Var;
+import liquidjava.utils.constants.Formats;
+import spoon.reflect.declaration.CtEnum;
+import spoon.reflect.declaration.CtEnumValue;
+
+/**
+ * Decides the comparisons of a variable with an enum constant that a fact about the variable already decides: under
+ * {@code x == A}, {@code x == A} is true and {@code x == B} false, and under {@code x != A}, {@code x == A} is false,
+ * so the ternaries they test can fold. Only the constants of the enum types of the chain's binders are used, which the
+ * solver translates as distinct values, unlike {@code static final} constants that may share a value
+ */
+public class VCKnownEnumValues implements VCSimplificationPass {
+
+    /**
+     * A comparison {@code variable == constant}, or {@code variable != constant} when not {@code equal}
+     */
+    private record EnumComparison(Expression expression, String variable, String constant, boolean equal) {
+    }
+
+    /** The enum type of each enum constant, by the name the solver translates the constant from */
+    private final Map<String, String> enumTypes = new HashMap<>();
+
+    public VCKnownEnumValues(VCImplication implication) {
+        for (VCImplication row = implication; row != null; row = row.getNext())
+            if (row.getType() != null && row.getType().getDeclaration()instanceof CtEnum<?> enumDecl)
+                for (CtEnumValue<?> value : enumDecl.getEnumValues())
+                    enumTypes.put(String.format(Formats.ENUM, enumDecl.getSimpleName(), value.getSimpleName()),
+                            enumDecl.getQualifiedName());
+    }
+
+    /**
+     * Uses the first fact that decides some comparison to replace those comparisons by their value
+     */
+    @Override
+    public VCImplication apply(VCImplication implication) {
+        for (VCImplication row = implication; row != null; row = row.getNext())
+            for (Expression fact : factsOf(row.getRefinement().getExpression())) {
+                EnumComparison known = enumComparison(fact);
+                if (known == null)
+                    continue;
+                // the last row may be the conclusion, which the other rows cannot assume
+                boolean onlyLastRow = row.getNext() == null && row != implication;
+                VCImplication decided = decideRows(implication, known, onlyLastRow);
+                if (!decided.equals(implication))
+                    return decided;
+            }
+        return implication;
+    }
+
+    private VCImplication decideRows(VCImplication implication, EnumComparison known, boolean onlyLastRow) {
+        if (implication == null)
+            return null;
+        Expression expression = implication.getRefinement().getExpression();
+        boolean decides = !onlyLastRow || implication.getNext() == null;
+        VCImplication result = copyWithRefinement(implication,
+                new Predicate(decides ? decide(expression, known) : expression.clone()));
+        result.setNext(decideRows(implication.getNext(), known, onlyLastRow));
+        return result;
+    }
+
+    // The expression with the comparisons known decides replaced by their value, except for its own fact
+    private Expression decide(Expression expression, EnumComparison known) {
+        if (expression == known.expression())
+            return expression.clone();
+        EnumComparison compared = enumComparison(expression);
+        if (compared != null && compared.variable().equals(known.variable())
+                && enumTypes.get(compared.constant()).equals(enumTypes.get(known.constant()))) {
+            boolean sameConstant = compared.constant().equals(known.constant());
+            if (known.equal())
+                return new LiteralBoolean(sameConstant == compared.equal());
+            if (sameConstant)
+                return new LiteralBoolean(!compared.equal());
+        }
+        Expression result = expression.clone();
+        for (int i = 0; i < expression.getChildren().size(); i++)
+            result.setChild(i, decide(expression.getChildren().get(i), known));
+        return result;
+    }
+
+    // A comparison of a variable with an enum constant, either way round, or null
+    private EnumComparison enumComparison(Expression expression) {
+        if (!(expression instanceof BinaryExpression binary))
+            return null;
+        boolean equal = "==".equals(binary.getOperator());
+        if (!equal && !"!=".equals(binary.getOperator()))
+            return null;
+        Expression left = binary.getFirstOperand(), right = binary.getSecondOperand();
+        String leftConstant = enumConstant(left), rightConstant = enumConstant(right);
+        if (left instanceof Var variable && leftConstant == null && rightConstant != null)
+            return new EnumComparison(expression, variable.getName(), rightConstant, equal);
+        if (right instanceof Var variable && rightConstant == null && leftConstant != null)
+            return new EnumComparison(expression, variable.getName(), leftConstant, equal);
+        return null;
+    }
+
+    // The name of the enum constant an expression is, written in code or in a refinement, or null
+    private String enumConstant(Expression expression) {
+        String name = null;
+        if (expression instanceof Var var)
+            name = var.getName();
+        else if (expression instanceof Enum en && en.getResolvedLiteral() == null)
+            name = en.toString();
+        return enumTypes.containsKey(name) ? name : null;
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCLogicalSimplification.java

@@ -3,6 +3,8 @@
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isFalse;
 import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
 
+import java.util.List;
+
 import liquidjava.rj_language.ast.BinaryExpression;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.Ite;
@@ -146,7 +148,30 @@ private Expression simplifyDisjunction(Expression left, Expression right) {
         // p || p -> p
         if (left.equals(right))
             return left.clone();
-        return null;
+        return factorCommonConjuncts(left, right);
+    }
+
+    /**
+     * Factors the conjuncts both disjuncts share out of a disjunction
+     */
+    private Expression factorCommonConjuncts(Expression left, Expression right) {
+        List<Expression> leftConjuncts = left.getConjuncts(), rightConjuncts = right.getConjuncts();
+        List<Expression> common = leftConjuncts.stream().filter(rightConjuncts::contains).distinct().toList();
+        if (common.isEmpty())
+            return null;
+        List<Expression> leftRest = leftConjuncts.stream().filter(c -> !common.contains(c)).toList();
+        List<Expression> rightRest = rightConjuncts.stream().filter(c -> !common.contains(c)).toList();
+        // c || c && p -> c
+        if (leftRest.isEmpty() || rightRest.isEmpty())
+            return conjunction(common);
+        // c && p || c && q -> c && (p || q)
+        return new BinaryExpression(conjunction(common), "&&",
+                new BinaryExpression(conjunction(leftRest), "||", conjunction(rightRest)));
+    }
+
+    private Expression conjunction(List<Expression> conjuncts) {
+        return conjuncts.stream().map(Expression::clone)
+                .reduce((first, second) -> new BinaryExpression(first, "&&", second)).get();
     }
 
     /**

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCSimplification.java

@@ -25,7 +25,7 @@ public static VCSimplificationResult simplifyToFixedPoint(VCImplication implicat
         if (implication == null)
             return null;
 
-        List<VCSimplificationPass> passes = passes(needed);
+        List<VCSimplificationPass> passes = passes(implication, needed);
         DebugLog.simplificationStart(implication);
         VCSimplificationResult current = new VCSimplificationResult(implication);
         while (true) {
@@ -42,7 +42,9 @@ public static VCSimplificationResult simplifyToFixedPoint(VCImplication implicat
      * Applies one simplification step to a VC chain from all available simplification passes
      */
     public static VCSimplificationResult simplifyOnce(VCSimplificationResult implication) {
-        return simplifyOnce(implication, passes(NeededVariables.NONE));
+        if (implication == null)
+            return null;
+        return simplifyOnce(implication, passes(implication.getOriginal().getImplication(), NeededVariables.NONE));
     }
 
     private static VCSimplificationResult simplifyOnce(VCSimplificationResult implication,
@@ -55,10 +57,10 @@ private static VCSimplificationResult simplifyOnce(VCSimplificationResult implic
         return implication;
     }
 
-    private static List<VCSimplificationPass> passes(NeededVariables needed) {
+    private static List<VCSimplificationPass> passes(VCImplication implication, NeededVariables needed) {
         return List.of(new VCSubstitution(), new VCFunctionSubstitution(), new VCBinderSimplification(needed),
-                new VCFolding(), new VCArithmeticSimplification(), new VCLogicalSimplification(),
-                new VCConstraintSimplification());
+                new VCKnownEnumValues(implication), new VCFolding(), new VCArithmeticSimplification(),
+                new VCLogicalSimplification(), new VCConstraintSimplification());
     }
 
     /**

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCKnownEnumValuesTest.java

@@ -0,0 +1,47 @@
+package liquidjava.rj_language.opt;
+
+import static liquidjava.utils.VCTestUtils.*;
+
+import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.Predicate;
+import liquidjava.rj_language.ast.BinaryExpression;
+import liquidjava.rj_language.ast.Ite;
+import liquidjava.rj_language.ast.Var;
+import org.junit.jupiter.api.Test;
+
+class VCKnownEnumValuesTest {
+
+    @Test
+    void decidesOnlyTheExcludedConstant() {
+        VCImplication implication = vc("∀mode:Mode. mode != Mode.Photo",
+                "mode == Mode.Photo ? a : (mode == Mode.Video ? b : c)");
+        assertSimplificationSteps(new VCKnownEnumValues(implication), implication,
+                step("mode != Mode.Photo", "false ? a : (mode == Mode.Video ? b : c)"));
+    }
+
+    @Test
+    void decidesConstantsReadInCode() {
+        // code reads an enum constant as a variable named after it
+        Var mode = new Var("mode"), photo = new Var("Mode.Photo"), video = new Var("Mode.Video");
+        VCImplication implication = vc("∀mode:Mode. true", "true");
+        implication.setRefinement(new Predicate(new BinaryExpression(mode, "==", photo)));
+        implication.getNext().setRefinement(
+                new Predicate(new Ite(new BinaryExpression(video, "==", mode), new Var("a"), new Var("b"))));
+        assertSimplificationSteps(new VCKnownEnumValues(implication), implication,
+                step("mode == Photo", "false ? a : b"));
+    }
+
+    @Test
+    void keepsPremisesTheConclusionWouldDecide() {
+        VCImplication implication = vc("∀mode:Mode. mode == Mode.Video || p", "mode == Mode.Photo");
+        assertSimplificationSteps(new VCKnownEnumValues(implication), implication,
+                step("mode == Mode.Video || p", "mode == Mode.Photo"));
+    }
+
+    @Test
+    void foldsTheTernariesAFactDecides() {
+        assertSimplificationSteps(vc("∀mode:Mode. true", "mode == Mode.Video && (mode == Mode.Photo ? a : b)"),
+                step("mode == Mode.Video && (mode == Mode.Photo ? a : b)"),
+                step("mode == Mode.Video && (false ? a : b)"), step("mode == Mode.Video && b"));
+    }
+}

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java

@@ -23,6 +23,12 @@ void simplifiesDisjunctionWithBooleanLiterals() {
         assertSimplificationSteps(simplification, vc("false || x"), step("x"));
     }
 
+    @Test
+    void factorsConjunctsSharedByDisjuncts() {
+        assertSimplificationSteps(simplification, vc("a && c || b && c"), step("c && (a || b)"));
+        assertSimplificationSteps(simplification, vc("c || c && b"), step("c"));
+    }
+
     @Test
     void simplifiesDoubleNegation() {
         assertSimplificationSteps(simplification, vc("!!x"), step("x"));

liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java

@@ -13,12 +13,17 @@
 import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.rj_language.parsing.RefinementsParser;
 import spoon.Launcher;
+import spoon.reflect.declaration.CtEnum;
+import spoon.reflect.declaration.CtEnumValue;
+import spoon.reflect.factory.Factory;
 import spoon.reflect.factory.TypeFactory;
 import spoon.reflect.reference.CtTypeReference;
 
 public class VCTestUtils {
 
-    private static final TypeFactory TYPE_FACTORY = new Launcher().getFactory().Type();
+    private static final Factory FACTORY = new Launcher().getFactory();
+    private static final TypeFactory TYPE_FACTORY = FACTORY.Type();
+    private static final CtTypeReference<?> MODE = enumType("Mode", "Photo", "Video");
 
     public static VCImplication vc(String... implications) {
         VCImplication first = null;
@@ -103,9 +108,21 @@ private static CtTypeReference<?> type(String name) {
             return TYPE_FACTORY.BOOLEAN_PRIMITIVE;
         if ("Object".equals(name))
             return TYPE_FACTORY.OBJECT;
+        if ("Mode".equals(name))
+            return MODE;
         throw new IllegalArgumentException("Unsupported test type: " + name);
     }
 
+    private static CtTypeReference<?> enumType(String name, String... values) {
+        CtEnum<?> enumDecl = FACTORY.Enum().create(name);
+        for (String value : values) {
+            CtEnumValue<?> enumValue = FACTORY.Core().createEnumValue();
+            enumValue.setSimpleName(value);
+            enumDecl.addEnumValue(enumValue);
+        }
+        return enumDecl.getReference();
+    }
+
     private static String formatRefinement(VCImplication implication) {
         return implication.getRefinement().getExpression().toDisplayString();
     }