Refactor Counterexamples

Author: rcosta358

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

@@ -10,6 +10,7 @@
 import liquidjava.rj_language.ast.formatter.VariableFormatter;
 import liquidjava.rj_language.opt.VCSimplificationResult;
 import liquidjava.smt.Counterexample;
+import liquidjava.utils.Pair;
 import spoon.reflect.cu.SourcePosition;
 
 /**
@@ -32,30 +33,42 @@ public RefinementError(SourcePosition position, Predicate expected, VCSimplifica
                 position, translationTable, customMessage);
         this.expected = expected;
         this.found = found;
-        this.counterexample = counterexample;
+        this.counterexample = filterCounterexample(counterexample);
     }
 
     @Override
     public String getDetails() {
-        Counterexample counterexamples = getCounterExamples();
-        if (counterexamples == null)
+        if (counterexample == null)
             return "";
 
-        String counterexampleString = counterexamples.assignments().stream()
+        String counterexampleString = counterexample.assignments().stream()
                 .map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
                 .collect(Collectors.joining(" && "));
         return "Counterexample: " + counterexampleString;
     }
 
+    public Counterexample getCounterexample() {
+        return counterexample;
+    }
+
+    public Predicate getExpected() {
+        return expected;
+    }
+
+    public VCSimplificationResult getFound() {
+        return found;
+    }
+
     // Filters counterexample assignments only in found VC and sorts them in the order of its binders
-    public Counterexample getCounterExamples() {
+    private Counterexample filterCounterexample(Counterexample counterexample) {
         if (counterexample == null || counterexample.assignments().isEmpty())
             return null;
 
         List<String> binderNames = getFound().getBinders();
         Set<String> knownAssignments = getFound().getImplication().toPredicate().getExpression().getConjuncts().stream()
                 .map(Expression::toString).collect(Collectors.toSet());
-        var assignments = counterexample.assignments().stream().filter(a -> binderNames.contains(a.first()))
+        List<Pair<String, String>> assignments = counterexample.assignments().stream()
+                .filter(a -> binderNames.contains(a.first()))
                 .filter(a -> !knownAssignments.contains(a.first() + " == " + a.second()))
                 .sorted((a, b) -> Integer.compare(binderNames.indexOf(a.first()), binderNames.indexOf(b.first())))
                 .toList();
@@ -65,16 +78,4 @@ public Counterexample getCounterExamples() {
 
         return new Counterexample(assignments);
     }
-
-    public Counterexample getCounterexample() {
-        return counterexample;
-    }
-
-    public Predicate getExpected() {
-        return expected;
-    }
-
-    public VCSimplificationResult getFound() {
-        return found;
-    }
 }