Filter Assignments by Variable Names & Use Pair in Counterexample

Author: rcosta358

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

@@ -1,6 +1,6 @@
 package liquidjava.diagnostics.errors;
 
-import java.util.Arrays;
+import java.util.ArrayList;
 import java.util.List;
 import java.util.stream.Collectors;
 
@@ -41,22 +41,14 @@ public String getCounterExampleString() {
         if (counterexample == null || counterexample.assignments().isEmpty())
             return null;
 
-        // filter out assignments of variables that do not appear in the found value
-        String foundValue = found.getValue().toString();
-        List<String> foundTokens = Arrays.asList(foundValue.split("[^a-zA-Z0-9_#]+"));
-        List<String> relevantAssignments = counterexample.assignments().stream().filter(a -> {
-            String varName = a.contains(" == ") ? a.substring(0, a.indexOf(" == ")).trim() : a;
-            return foundTokens.contains(varName);
-        }).collect(Collectors.toList());
+        List<String> foundVarNames = new ArrayList<>();
+        found.getValue().getVariableNames(foundVarNames);
+        String counterexampleExp = counterexample.assignments().stream()
+            .filter(a -> foundVarNames.contains(a.first())) // only include variables that appear in the found value
+            .map(a -> a.first() + " == " + a.second()) // format as "var == value"
+            .collect(Collectors.joining(" && ")); // join with "&&"
 
-        if (relevantAssignments.isEmpty())
-            return null;
-
-        // join assignements with &&
-        String counterexampleExp = String.join(" && ", relevantAssignments);
-
-        // check if counterexample is trivial (same as the found value)
-        if (counterexampleExp.equals(foundValue))
+        if (counterexampleExp.isEmpty() || counterexampleExp.equals(found.getValue().toString()))
             return null;
 
         return counterexampleExp;

liquidjava-verifier/src/main/java/liquidjava/smt/Counterexample.java

@@ -2,5 +2,7 @@
 
 import java.util.List;
 
-public record Counterexample(List<String> assignments) {
+import liquidjava.utils.Pair;
+
+public record Counterexample(List<Pair<String, String>> assignments) {
 }

liquidjava-verifier/src/main/java/liquidjava/smt/TranslatorToZ3.java

@@ -24,6 +24,7 @@
 import liquidjava.diagnostics.errors.LJError;
 import liquidjava.diagnostics.errors.NotFoundError;
 import liquidjava.processor.context.AliasWrapper;
+import liquidjava.utils.Pair;
 import liquidjava.utils.Utils;
 import liquidjava.utils.constants.Keys;
 import com.microsoft.z3.enumerations.Z3_sort_kind;
@@ -59,13 +60,13 @@ public Solver makeSolverForExpression(Expr<?> e) {
      * Extracts the counterexample from the Z3 model
      */
     public Counterexample getCounterexample(Model model) {
-        List<String> assignments = new ArrayList<>();
+        List<Pair<String, String>> assignments = new ArrayList<>();
         // Extract constant variable assignments
         for (FuncDecl<?> decl : model.getDecls()) {
             if (decl.getArity() == 0) {
                 Symbol name = decl.getName();
                 Expr<?> value = model.getConstInterp(decl);
-                String assignment = name + " == " + value;
+                Pair<String, String> assignment = new Pair<>(name.toString(), value.toString());
                 // Skip values of uninterpreted sorts
                 if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT)
                     assignments.add(assignment);
@@ -76,7 +77,7 @@ public Counterexample getCounterexample(Model model) {
             String name = entry.getKey();
             Expr<?> application = entry.getValue();
             Expr<?> value = model.eval(application, true);
-            String assignment = name + " == " + value;
+            Pair<String, String> assignment = new Pair<>(name, value.toString());
             assignments.add(assignment);
         }
         return new Counterexample(assignments);