Print verifier counterexamples as CEL literals

verifier/README.md

@@ -224,8 +224,8 @@ public class PolicyVerifierExample {
         System.out.println(result.message());
         // Output:
         // Equivalence violation detected. Counterexample input:
-        //   country = "a"
         //   role = "editor"
+        //   country = "a"
         //   port = 443
         break;
       case INCONCLUSIVE:

verifier/src/main/java/dev/cel/verifier/BUILD.bazel

@@ -186,6 +186,7 @@ java_library(
         "//common/ast",
         "//common/ast:cel_block",
         "//common/internal:cel_descriptor_pools",
+        "//common/internal:proto_time_utils",
         "//common/internal:well_known_proto",
         "//common/types",
         "//common/types:cel_types",

verifier/src/main/java/dev/cel/verifier/CelAstToZ3Translator.java

@@ -92,6 +92,11 @@ CelZ3TypeSystem getTypeSystem() {
     return typeSystem;
   }
 
+  /** Returns the input variables, in order of first appearance. */
+  Set<Expr<?>> getInputVariables() {
+    return context.inputVariables();
+  }
+
   /**
    * Returns a Z3 boolean expression asserting that the provided CEL value is a boolean and is true.
    */

verifier/src/main/java/dev/cel/verifier/CelVerifierZ3Impl.java

@@ -259,7 +259,7 @@ public CelVerificationResult verifyEquivalence(
               "Equivalence violation detected.",
               getCounterexampleString(
                   ctx,
-                  translator.getTypeSystem(),
+                  translator,
                   result.model,
                   /* isApproximate= */ false,
                   /* isCounterexample= */ true));
@@ -269,7 +269,7 @@ public CelVerificationResult verifyEquivalence(
                   + " theories, or loop bounds.",
               getCounterexampleString(
                   ctx,
-                  translator.getTypeSystem(),
+                  translator,
                   result.model,
                   /* isApproximate= */ true,
                   /* isCounterexample= */ true));
@@ -345,7 +345,7 @@ CelVerificationResult verifyImplication(
               String.format("%s violation detected.", subjectName),
               getCounterexampleString(
                   ctx,
-                  translator.getTypeSystem(),
+                  translator,
                   result.model,
                   /* isApproximate= */ false,
                   /* isCounterexample= */ true));
@@ -355,7 +355,7 @@ CelVerificationResult verifyImplication(
                   + " theories, or loop bounds.",
               getCounterexampleString(
                   ctx,
-                  translator.getTypeSystem(),
+                  translator,
                   result.model,
                   /* isApproximate= */ true,
                   /* isCounterexample= */ true));
@@ -408,15 +408,15 @@ private CelVerificationResult checkSatisfiability(
                   "Condition is not always true.",
                   getCounterexampleString(
                       ctx,
-                      translator.getTypeSystem(),
+                      translator,
                       result.model,
                       /* isApproximate= */ false,
                       /* isCounterexample= */ true))
               : CelVerificationResult.verified(
                   "Condition is satisfiable."
                       + getCounterexampleString(
                           ctx,
-                          translator.getTypeSystem(),
+                          translator,
                           result.model,
                           /* isApproximate= */ false,
                           /* isCounterexample= */ false));
@@ -432,7 +432,7 @@ private CelVerificationResult checkSatisfiability(
               prefix,
               getCounterexampleString(
                   ctx,
-                  translator.getTypeSystem(),
+                  translator,
                   result.model,
                   /* isApproximate= */ true,
                   /* isCounterexample= */ searchForCounterexample));
@@ -540,12 +540,17 @@ private CelAstToZ3Translator newTranslator(Context ctx, boolean parameterizeUnkn
 
   private static String getCounterexampleString(
       Context ctx,
-      CelZ3TypeSystem typeSystem,
+      CelAstToZ3Translator translator,
       Model model,
       boolean isApproximate,
       boolean isCounterexample) {
     return CelZ3CounterexampleGenerator.generate(
-        ctx, typeSystem, model, isApproximate, isCounterexample);
+        ctx,
+        translator.getTypeSystem(),
+        model,
+        translator.getInputVariables(),
+        isApproximate,
+        isCounterexample);
   }
 
   private enum SolverOutcome {