Improve Counterexamples

Author: rcosta358

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

@@ -6,4 +6,5 @@ public class Colors {
     public static final String GREY = "\u001B[90m";
     public static final String BOLD_RED = "\u001B[1;31m";
     public static final String BOLD_YELLOW = "\u001B[1;33m";
+    public static final String CYAN = "\u001B[36m";
 }

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

@@ -77,7 +77,7 @@ public String toString() {
         // details
         String details = getDetails();
         if (!details.isEmpty()) {
-            sb.append(" --> ").append(String.join("\n     ", details.split("\n"))).append("\n");
+            sb.append(Colors.CYAN).append(" --> ").append(String.join("\n     ", details.split("\n"))).append(Colors.RESET).append("\n");
         }
 
         // location

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

@@ -27,20 +27,22 @@ public RefinementError(SourcePosition position, ValDerivationNode expected, ValD
 
     @Override
     public String getDetails() {
-        return "Counterexample: " + getCounterExampleString();
+        String counterexampleString = getCounterExampleString();
+        if (counterexampleString == null)
+            return "";
+        return "Counterexample: " + counterexampleString;
     }
 
     public String getCounterExampleString() {
         if (counterexample == null || counterexample.assignments().isEmpty())
-            return "";
+            return null;
 
-        // filter fresh variables and join assignements with &&
-        String counterexampleExp = counterexample.assignments().stream().filter(a -> !a.startsWith("#fresh_"))
-                .reduce((a, b) -> a + " && " + b).orElse("");
+        // join assignements with &&
+        String counterexampleExp = String.join(" && ", counterexample.assignments());
 
         // check if counterexample is trivial (same as the found value)
         if (counterexampleExp.equals(found.getValue().toString()))
-            return "";
+            return null;
 
         return counterexampleExp;
     }

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

@@ -18,8 +18,10 @@
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.List;
 import java.util.Map;
+import java.util.Set;
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.errors.LJError;
@@ -40,13 +42,15 @@ public class TranslatorToZ3 implements AutoCloseable {
     private final Map<String, FuncDecl<?>> funcTranslation = new HashMap<>();
     private final Map<String, Expr<?>> funcAppTranslation = new HashMap<>();
     private final Map<Expr<?>, String> exprToNameTranslation = new HashMap<>();
+    private final Set<String> instanceVariableRefinements;
 
-    public TranslatorToZ3(liquidjava.processor.context.Context c) {
-        TranslatorContextToZ3.translateVariables(z3, c.getContext(), varTranslation);
-        TranslatorContextToZ3.storeVariablesSubtypes(z3, c.getAllVariablesWithSupertypes(), varSuperTypes);
-        TranslatorContextToZ3.addAliases(c.getAliases(), aliasTranslation);
-        TranslatorContextToZ3.addGhostFunctions(z3, c.getGhosts(), funcTranslation);
-        TranslatorContextToZ3.addGhostStates(z3, c.getGhostStates(), funcTranslation);
+    public TranslatorToZ3(liquidjava.processor.context.Context context) {
+        TranslatorContextToZ3.translateVariables(z3, context.getContext(), varTranslation);
+        TranslatorContextToZ3.storeVariablesSubtypes(z3, context.getAllVariablesWithSupertypes(), varSuperTypes);
+        TranslatorContextToZ3.addAliases(context.getAliases(), aliasTranslation);
+        TranslatorContextToZ3.addGhostFunctions(z3, context.getGhosts(), funcTranslation);
+        TranslatorContextToZ3.addGhostStates(z3, context.getGhostStates(), funcTranslation);
+        instanceVariableRefinements = context.getCtxInstanceVars().stream().map(v -> v.getRefinement().toString()).collect(Collectors.toSet());
     }
 
     @SuppressWarnings("unchecked")
@@ -66,18 +70,21 @@ public Counterexample getCounterexample(Model model) {
             if (decl.getArity() == 0) {
                 Symbol name = decl.getName();
                 Expr<?> value = model.getConstInterp(decl);
+                String assignment = name + " == " + value;
                 // Skip values of uninterpreted sorts
-                if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT)
-                    assignments.add(name + " == " + value);
+                if (value.getSort().getSortKind() != Z3_sort_kind.Z3_UNINTERPRETED_SORT && !instanceVariableRefinements.contains(assignment))
+                    assignments.add(assignment);
             }
         }
         // Extract function application values
         for (Map.Entry<String, Expr<?>> entry : funcAppTranslation.entrySet()) {
-            String label = entry.getKey();
+            String name = entry.getKey();
             Expr<?> application = entry.getValue();
             Expr<?> value = model.eval(application, true);
-            assignments.add(label + " = " + value);
-        }
+            String assignment = name + " == " + value;
+            if (!instanceVariableRefinements.contains(assignment))
+                assignments.add(assignment);
+        }        
         return new Counterexample(assignments);
     }