From bc34cbda2972fb0a6b04b23c7d957c2027efacdb Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 19:05:48 +0000 Subject: [PATCH 1/3] Decide enum comparisons that a fact of Found already decides Found kept ternaries whose tests a top-level fact such as newMode == BORDERLESS already decides. A new display pass, Known Enum Values, replaces each comparison of a variable with an enum constant that another fact decides by its value, so Folding and Logical fold the ternaries. Only constants of the enum types of the chain's binders are used, which the solver translates as distinct values. Logical simplification also factors the conjuncts both disjuncts share out of a disjunction. Co-Authored-By: Claude Opus 5.5 --- .../rj_language/opt/VCKnownEnumValues.java | 115 ++++++++++++++++++ .../opt/VCLogicalSimplification.java | 27 +++- .../rj_language/opt/VCSimplification.java | 12 +- .../opt/VCKnownEnumValuesTest.java | 42 +++++++ .../opt/VCLogicalSimplificationTest.java | 6 + .../java/liquidjava/utils/VCTestUtils.java | 19 ++- 6 files changed, 214 insertions(+), 7 deletions(-) create mode 100644 liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java create mode 100644 liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCKnownEnumValuesTest.java diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java new file mode 100644 index 000000000..1f87fcba7 --- /dev/null +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java @@ -0,0 +1,115 @@ +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 fact {@code variable == constant}, or {@code variable != constant} when not {@code equal} + */ + private record KnownValue(Expression fact, 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 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()); + } + + /** + * Decides the comparisons that the first fact deciding any decides + */ + @Override + public VCImplication apply(VCImplication implication) { + for (VCImplication row = implication; row != null; row = row.getNext()) + for (Expression fact : factsOf(row.getRefinement().getExpression())) { + KnownValue known = knownValue(fact); + if (known == null) + continue; + VCImplication decided = decide(implication, known); + if (!decided.equals(implication)) + return decided; + } + return implication; + } + + private VCImplication decide(VCImplication implication, KnownValue known) { + if (implication == null) + return null; + VCImplication result = copyWithRefinement(implication, + new Predicate(decide(implication.getRefinement().getExpression(), known))); + result.setNext(decide(implication.getNext(), known)); + return result; + } + + // The expression with the comparisons known decides replaced by their value, except for its own fact + private Expression decide(Expression expression, KnownValue known) { + if (expression == known.fact()) + return expression.clone(); + KnownValue compared = knownValue(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 KnownValue knownValue(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 KnownValue(expression, variable.getName(), rightConstant, equal); + if (right instanceof Var variable && rightConstant == null && leftConstant != null) + return new KnownValue(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; + } +} 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 d8fef4719..7d7780bb2 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 @@ -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 leftConjuncts = left.getConjuncts(), rightConjuncts = right.getConjuncts(); + List common = leftConjuncts.stream().filter(rightConjuncts::contains).distinct().toList(); + if (common.isEmpty()) + return null; + List leftRest = leftConjuncts.stream().filter(c -> !common.contains(c)).toList(); + List 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 conjuncts) { + return conjuncts.stream().map(Expression::clone) + .reduce((first, second) -> new BinaryExpression(first, "&&", second)).get(); } /** 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 82705505e..b215a4d15 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 @@ -25,7 +25,7 @@ public static VCSimplificationResult simplifyToFixedPoint(VCImplication implicat if (implication == null) return null; - List passes = passes(needed); + List 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.getImplication(), NeededVariables.NONE)); } private static VCSimplificationResult simplifyOnce(VCSimplificationResult implication, @@ -55,10 +57,10 @@ private static VCSimplificationResult simplifyOnce(VCSimplificationResult implic return implication; } - private static List passes(NeededVariables needed) { + private static List 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()); } /** diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCKnownEnumValuesTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCKnownEnumValuesTest.java new file mode 100644 index 000000000..5b85b8c6a --- /dev/null +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCKnownEnumValuesTest.java @@ -0,0 +1,42 @@ +package liquidjava.rj_language.opt; + +import static liquidjava.utils.VCTestUtils.*; +import static org.junit.jupiter.api.Assertions.assertEquals; + +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 foldsTheTernariesAFactDecides() { + VCImplication simplified = VCSimplification + .simplifyToFixedPoint(vc("∀mode:Mode. true", "mode == Mode.Video && (mode == Mode.Photo ? a : b)")) + .getImplication(); + assertEquals("mode == Mode.Video && b", simplified.toPredicate().getExpression().toDisplayString()); + } +} 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 index 141744d9f..973d7addd 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCLogicalSimplificationTest.java +++ 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")); diff --git a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java b/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java index 2a039e253..afd8e58b7 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/utils/VCTestUtils.java +++ b/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(); } From 09fafd44ee315cd1c53c704d87386069efe48305 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 19:11:39 +0000 Subject: [PATCH 2/3] Keep premises a conclusion row would decide, and enum types across steps Co-Authored-By: Claude Opus 5.5 --- .../rj_language/opt/VCKnownEnumValues.java | 12 ++++++++---- .../rj_language/opt/VCSimplification.java | 2 +- .../rj_language/opt/VCKnownEnumValuesTest.java | 15 ++++++++++----- 3 files changed, 19 insertions(+), 10 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java index 1f87fcba7..339bac9de 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java @@ -52,19 +52,23 @@ public VCImplication apply(VCImplication implication) { KnownValue known = knownValue(fact); if (known == null) continue; - VCImplication decided = decide(implication, known); + // the last row may be the conclusion, which the other rows cannot assume + boolean onlyLastRow = row.getNext() == null && row != implication; + VCImplication decided = decide(implication, known, onlyLastRow); if (!decided.equals(implication)) return decided; } return implication; } - private VCImplication decide(VCImplication implication, KnownValue known) { + private VCImplication decide(VCImplication implication, KnownValue 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(decide(implication.getRefinement().getExpression(), known))); - result.setNext(decide(implication.getNext(), known)); + new Predicate(decides ? decide(expression, known) : expression.clone())); + result.setNext(decide(implication.getNext(), known, onlyLastRow)); return result; } 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 b215a4d15..344bb8de8 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 @@ -44,7 +44,7 @@ public static VCSimplificationResult simplifyToFixedPoint(VCImplication implicat public static VCSimplificationResult simplifyOnce(VCSimplificationResult implication) { if (implication == null) return null; - return simplifyOnce(implication, passes(implication.getImplication(), NeededVariables.NONE)); + return simplifyOnce(implication, passes(implication.getOriginal().getImplication(), NeededVariables.NONE)); } private static VCSimplificationResult simplifyOnce(VCSimplificationResult implication, diff --git a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCKnownEnumValuesTest.java b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCKnownEnumValuesTest.java index 5b85b8c6a..f2c9a78eb 100644 --- a/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCKnownEnumValuesTest.java +++ b/liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VCKnownEnumValuesTest.java @@ -1,7 +1,6 @@ package liquidjava.rj_language.opt; import static liquidjava.utils.VCTestUtils.*; -import static org.junit.jupiter.api.Assertions.assertEquals; import liquidjava.processor.VCImplication; import liquidjava.rj_language.Predicate; @@ -32,11 +31,17 @@ void decidesConstantsReadInCode() { 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() { - VCImplication simplified = VCSimplification - .simplifyToFixedPoint(vc("∀mode:Mode. true", "mode == Mode.Video && (mode == Mode.Photo ? a : b)")) - .getImplication(); - assertEquals("mode == Mode.Video && b", simplified.toPredicate().getExpression().toDisplayString()); + 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")); } } From f50283433f2a80b0db937a3567ef78e06df08131 Mon Sep 17 00:00:00 2001 From: Catarina Gamboa Date: Tue, 10 Nov 2026 19:17:20 +0000 Subject: [PATCH 3/3] Name the comparisons of Known Enum Values for what they are Co-Authored-By: Claude Opus 5.5 --- .../rj_language/opt/VCKnownEnumValues.java | 26 +++++++++---------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java index 339bac9de..bdaadfec6 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCKnownEnumValues.java @@ -26,9 +26,9 @@ public class VCKnownEnumValues implements VCSimplificationPass { /** - * A fact {@code variable == constant}, or {@code variable != constant} when not {@code equal} + * A comparison {@code variable == constant}, or {@code variable != constant} when not {@code equal} */ - private record KnownValue(Expression fact, String variable, String constant, boolean 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 */ @@ -43,40 +43,40 @@ public VCKnownEnumValues(VCImplication implication) { } /** - * Decides the comparisons that the first fact deciding any decides + * 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())) { - KnownValue known = knownValue(fact); + 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 = decide(implication, known, onlyLastRow); + VCImplication decided = decideRows(implication, known, onlyLastRow); if (!decided.equals(implication)) return decided; } return implication; } - private VCImplication decide(VCImplication implication, KnownValue known, boolean onlyLastRow) { + 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(decide(implication.getNext(), known, onlyLastRow)); + 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, KnownValue known) { - if (expression == known.fact()) + private Expression decide(Expression expression, EnumComparison known) { + if (expression == known.expression()) return expression.clone(); - KnownValue compared = knownValue(expression); + 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()); @@ -92,7 +92,7 @@ private Expression decide(Expression expression, KnownValue known) { } // A comparison of a variable with an enum constant, either way round, or null - private KnownValue knownValue(Expression expression) { + private EnumComparison enumComparison(Expression expression) { if (!(expression instanceof BinaryExpression binary)) return null; boolean equal = "==".equals(binary.getOperator()); @@ -101,9 +101,9 @@ private KnownValue knownValue(Expression expression) { 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 KnownValue(expression, variable.getName(), rightConstant, equal); + return new EnumComparison(expression, variable.getName(), rightConstant, equal); if (right instanceof Var variable && rightConstant == null && leftConstant != null) - return new KnownValue(expression, variable.getName(), leftConstant, equal); + return new EnumComparison(expression, variable.getName(), leftConstant, equal); return null; }