Simplification Migration

CONTRIBUTING.md

@@ -37,9 +37,8 @@ To run specific tests, run:
 
 ```bash
 mvn -pl liquidjava-verifier -Dtest=ExpressionFormatterTest test
-mvn -pl liquidjava-verifier -Dtest=ExpressionSimplifierTest test
 mvn -pl liquidjava-verifier -Dtest=RefinementsParserTest test
-mvn -pl liquidjava-verifier -Dtest=VariableResolverTest test
+mvn -pl liquidjava-verifier -Dtest=VCSimplificationTest test
 ```
 
 ## Release

liquidjava-verifier/src/main/java/liquidjava/diagnostics/DebugLog.java

@@ -56,7 +56,7 @@ public static void smtVerifying(SourcePosition position) {
 
     /**
      * Flat-predicate fallback: prints top-level conjuncts in order with no per-variable grouping. Used by SMT entry
-     * points that don't carry the structured per-variable {@link VCImplication} chain (e.g. ExpressionSimplifier).
+     * points that don't carry the structured per-variable {@link VCImplication} chain.
      */
     public static void smtStart(Predicate premises, Predicate conclusion) {
         if (!enabled()) {

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java

@@ -5,9 +5,10 @@
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.TranslationTable;
+import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.Predicate;
 import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
-import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import liquidjava.smt.Counterexample;
 import spoon.reflect.cu.SourcePosition;
 
@@ -18,14 +19,15 @@
  */
 public class RefinementError extends LJError {
 
-    private final ValDerivationNode expected;
-    private final ValDerivationNode found;
+    private final Predicate expected;
+    private final VCImplication found;
     private final Counterexample counterexample;
 
-    public RefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
+    public RefinementError(SourcePosition position, Predicate expected, VCImplication found,
             TranslationTable translationTable, Counterexample counterexample, String customMessage) {
-        super("Refinement Error", String.format("%s is not a subtype of %s", found.getValue().toDisplayString(),
-                expected.getValue().toDisplayString()), position, translationTable, customMessage);
+        super("Refinement Error", String.format("%s is not a subtype of %s",
+                found.toPredicate().getExpression().toDisplayString(), expected.getExpression().toDisplayString()),
+                position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
         this.counterexample = counterexample;
@@ -44,12 +46,14 @@ public String getCounterExampleString() {
             return null;
 
         List<String> foundVarNames = new ArrayList<>();
-        found.getValue().getVariableNames(foundVarNames);
+        Expression foundExpression = found.toPredicate().getExpression();
+        Expression expectedExpression = expected.getExpression();
+        foundExpression.getVariableNames(foundVarNames);
         // also keep resolved static-final constants (e.g. Integer.MAX_VALUE) referenced by either side of the
         // subtyping check, so the counterexample maps the symbolic name back to its compile-time value
-        found.getValue().getResolvedConstantNames(foundVarNames);
-        expected.getValue().getResolvedConstantNames(foundVarNames);
-        List<String> foundAssignments = found.getValue().getConjuncts().stream().map(Expression::toString).toList();
+        foundExpression.getResolvedConstantNames(foundVarNames);
+        expectedExpression.getResolvedConstantNames(foundVarNames);
+        List<String> foundAssignments = foundExpression.getConjuncts().stream().map(Expression::toString).toList();
         String counterexampleString = counterexample.assignments().stream()
                 // only include variables that appear in the found value and are not already fixed there
                 .filter(a -> foundVarNames.contains(a.first())
@@ -69,11 +73,11 @@ public Counterexample getCounterexample() {
         return counterexample;
     }
 
-    public ValDerivationNode getExpected() {
+    public Predicate getExpected() {
         return expected;
     }
 
-    public ValDerivationNode getFound() {
+    public VCImplication getFound() {
         return found;
     }
 }

liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java

@@ -1,7 +1,8 @@
 package liquidjava.diagnostics.errors;
 
 import liquidjava.diagnostics.TranslationTable;
-import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
+import liquidjava.processor.VCImplication;
+import liquidjava.rj_language.Predicate;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -11,23 +12,24 @@
  */
 public class StateRefinementError extends LJError {
 
-    private final ValDerivationNode expected;
-    private final ValDerivationNode found;
+    private final Predicate expected;
+    private final VCImplication found;
 
-    public StateRefinementError(SourcePosition position, ValDerivationNode expected, ValDerivationNode found,
+    public StateRefinementError(SourcePosition position, Predicate expected, VCImplication found,
             TranslationTable translationTable, String customMessage) {
-        super("State Refinement Error", String.format("Expected state %s but found %s",
-                expected.getValue().toDisplayString(), found.getValue().toDisplayString()), position, translationTable,
-                customMessage);
+        super("State Refinement Error",
+                String.format("Expected state %s but found %s", expected.getExpression().toDisplayString(),
+                        found.toPredicate().getExpression().toDisplayString()),
+                position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
     }
 
-    public ValDerivationNode getExpected() {
+    public Predicate getExpected() {
         return expected;
     }
 
-    public ValDerivationNode getFound() {
+    public VCImplication getFound() {
         return found;
     }
 }

liquidjava-verifier/src/main/java/liquidjava/processor/VCImplication.java

@@ -93,6 +93,10 @@ public VCImplication simplify() {
         return VCSimplification.simplifyToFixedPoint(this);
     }
 
+    public Predicate toPredicate() {
+        return hasBinder() || hasNext() ? toConjunctions() : refinement;
+    }
+
     public Predicate toConjunctions() {
         Predicate c = new Predicate();
         if (name == null && type == null && next == null)

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/VCChecker.java

@@ -53,6 +53,7 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         TranslationTable map = new TranslationTable();
         String[] s = { Keys.WILDCARD, Keys.THIS };
         VCImplication impl = joinPredicates(expectedType, mainVars, lrv, map);
+        VCImplication implBeforeChange = impl.clone();
         Predicate premisesBeforeChange = impl.toConjunctions();
         Predicate premises;
         Predicate expected;
@@ -81,8 +82,8 @@ public void processSubtyping(Predicate expectedType, List<GhostState> list, CtEl
         }
         DebugLog.smtResult(result);
         if (result.isError()) {
-            throw new RefinementError(element.getPosition(), expectedType.simplify(context),
-                    premisesBeforeChange.simplify(context), map, result.getCounterexample(), customMessage);
+            throw new RefinementError(element.getPosition(), expectedType, implBeforeChange.simplify(), map,
+                    result.getCounterexample(), customMessage);
         }
     }
 
@@ -405,17 +406,15 @@ private VCImplication buildPremiseChain(TranslationTable map, Predicate... predi
     protected void throwRefinementError(SourcePosition position, Predicate expected, Predicate found,
             Counterexample counterexample, String customMessage) throws RefinementError {
         TranslationTable map = new TranslationTable();
-        Predicate premises = buildPremiseChain(map, expected, found).toConjunctions();
-        throw new RefinementError(position, expected.simplify(context), premises.simplify(context), map, counterexample,
-                customMessage);
+        VCImplication premises = buildPremiseChain(map, expected, found);
+        throw new RefinementError(position, expected, premises.simplify(), map, counterexample, customMessage);
     }
 
     protected void throwStateRefinementError(SourcePosition position, Predicate found, Predicate expected,
             String customMessage) throws StateRefinementError {
         TranslationTable map = new TranslationTable();
         VCImplication foundState = buildPremiseChain(map, expected, found);
-        throw new StateRefinementError(position, expected.simplify(context),
-                foundState.toConjunctions().simplify(context), map, customMessage);
+        throw new StateRefinementError(position, expected, foundState.simplify(), map, customMessage);
     }
 
     protected void throwStateConflictError(SourcePosition position, Predicate expected) throws StateConflictError {

liquidjava-verifier/src/main/java/liquidjava/rj_language/Predicate.java

@@ -9,6 +9,7 @@
 import liquidjava.diagnostics.DebugLog;
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.NotFoundError;
+import liquidjava.processor.VCImplication;
 import liquidjava.processor.context.AliasWrapper;
 import liquidjava.processor.context.Context;
 import liquidjava.processor.context.GhostFunction;
@@ -27,10 +28,8 @@
 import liquidjava.rj_language.ast.LiteralReal;
 import liquidjava.rj_language.ast.UnaryExpression;
 import liquidjava.rj_language.ast.Var;
-import liquidjava.utils.StaticConstants;
-import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
-import liquidjava.rj_language.opt.ExpressionSimplifier;
 import liquidjava.rj_language.parsing.RefinementsParser;
+import liquidjava.utils.StaticConstants;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Keys;
 import liquidjava.utils.constants.Ops;
@@ -260,15 +259,9 @@ public Predicate getOrigin() {
         return this;
     }
 
-    public ValDerivationNode simplify(Context context) {
-        // collect aliases from context
-        Map<String, AliasDTO> aliases = new HashMap<>();
-        for (AliasWrapper aw : context.getAliases()) {
-            aliases.put(aw.getName(), aw.createAliasDTO());
-        }
-        // simplify expression
-        ValDerivationNode result = ExpressionSimplifier.simplify(exp.clone(), aliases);
-        DebugLog.simplification(this.getExpression(), result.getValue());
+    public VCImplication simplify() {
+        VCImplication result = new VCImplication(clone()).simplify();
+        DebugLog.simplification(this.getExpression(), result.getRefinement().getExpression());
         return result;
     }