Make Counterexample Filtering Order Insensitive (#204)

Author: rcosta358

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

@@ -6,7 +6,7 @@
 
 import liquidjava.api.CommandLineLauncher;
 import liquidjava.diagnostics.TranslationTable;
-import liquidjava.rj_language.ast.Var;
+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;
@@ -46,16 +46,17 @@ public String getCounterExampleString() {
 
         List<String> foundVarNames = new ArrayList<>();
         found.getValue().getVariableNames(foundVarNames);
+        List<String> foundAssignments = found.getValue().getConjuncts().stream().map(Expression::toString).toList();
         String counterexampleString = counterexample.assignments().stream()
-                // only include variables that appear in the found value
-                .filter(a -> CommandLineLauncher.cmdArgs.debugMode || foundVarNames.contains(a.first()))
+                // only include variables that appear in the found value and are not already fixed there
+                .filter(a -> CommandLineLauncher.cmdArgs.debugMode || (foundVarNames.contains(a.first())
+                        && !foundAssignments.contains(a.first() + " == " + a.second())))
                 // format as "var == value"
                 .map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
                 // join with "&&"
                 .collect(Collectors.joining(" && "));
 
-        String foundString = found.getValue().toDisplayString();
-        if (counterexampleString.isEmpty() || counterexampleString.equals(foundString))
+        if (counterexampleString.isEmpty())
             return null;
 
         return counterexampleString;

liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java

@@ -86,6 +86,16 @@ public boolean isBooleanExpression() {
         return false;
     }
 
+    public List<Expression> getConjuncts() {
+        if (this instanceof BinaryExpression binaryExpression && "&&".equals(binaryExpression.getOperator())) {
+            List<Expression> conjuncts = new ArrayList<>();
+            conjuncts.addAll(binaryExpression.getFirstOperand().getConjuncts());
+            conjuncts.addAll(binaryExpression.getSecondOperand().getConjuncts());
+            return conjuncts;
+        }
+        return List.of(this);
+    }
+
     /**
      * Substitutes the expression first given expression by the second
      *