symbolic discharge: universals over infinite domains decided by intervals

2 files changed, 53 insertions, 6 deletions

diff --git a/test/test_embedding.ml b/test/test_embedding.ml
index ea55e4f..a2eab95 100644
--- a/test/test_embedding.ml
+++ b/test/test_embedding.ml
@@ -66,9 +66,12 @@ let test_kernel_scan () =
   | Error error -> Alcotest.failf "solve error: %a" Sol.Vm.pp_error error
 
 let test_kernel_totality () =
+  (* A universal over an infinite domain whose body the symbolic
+     fragment cannot read: neither enumerable nor provable, so it
+     must be rejected, embedding or not. *)
   match
     solve
-      {| [ForAll variable: X quantifier: [Integer value: X] body: [True]] |}
+      {| [ForAll variable: X quantifier: [Integer value: X] body: [Sensor id: X]] |}
   with
   | Error (Sol.Vm.Non_total_plan _) -> ()
   | Ok _ -> Alcotest.fail "the embedded engine must keep the totality guard"
diff --git a/test/test_vm.ml b/test/test_vm.ml
index f3d8484..16ca63c 100644
--- a/test/test_vm.ml
+++ b/test/test_vm.ml
@@ -263,13 +263,47 @@ let test_forall_fails () =
   | [ _ :: _ ] -> Alcotest.fail "the universal must fail: Ana is 12"
   | _ -> Alcotest.fail "expected one query"
 
-let test_forall_over_infinite_rejected () =
-  match load {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [True]] |} with
+let holds source = count_solutions source = 1
+
+(* Symbolic discharge: the specification's own two examples, decided
+   without enumerating anything. *)
+
+let test_symbolic_naturals_nonnegative () =
+  Alcotest.(check bool) "every natural is at least zero" true
+    (holds
+       {| Query expression: [ForAll variable: X quantifier: [Natural value: X] body: [GreaterEqual left: X right: 0]] |})
+
+let test_symbolic_integers_not_nonnegative () =
+  Alcotest.(check bool) "not every integer is at least zero" false
+    (holds
+       {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [GreaterEqual left: X right: 0]] |})
+
+let test_symbolic_inclusion () =
+  (* Decision 12: subtype inclusion, decided symbolically. *)
+  Alcotest.(check bool) "every integer is a rational" true
+    (holds
+       {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [Rational value: X]] |});
+  Alcotest.(check bool) "not every rational is an integer" false
+    (holds
+       {| Query expression: [ForAll variable: X quantifier: [Rational value: X] body: [Integer value: X]] |})
+
+let test_symbolic_interval_entailment () =
+  Alcotest.(check bool) "naturals from ten upward exceed five" true
+    (holds
+       {| Query expression: [ForAll variable: X quantifier: ([Natural value: X] :and [GreaterEqual left: X right: 10]) body: [GreaterThan left: X right: 5]] |})
+
+let test_forall_outside_fragment_still_rejected () =
+  match
+    load
+      {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [Equal left: X right: 5]] |}
+  with
   | Error error -> Alcotest.failf "load error: %a" Sol.Program.pp_error error
   | Ok (world, [ query ]) -> (
       match Sol.Vm.Standalone.solve world query with
       | Error (Sol.Vm.Non_total_plan _) -> ()
-      | Ok _ -> Alcotest.fail "a universal over an infinite domain must be rejected")
+      | Ok _ ->
+          Alcotest.fail
+            "a universal the symbolic fragment cannot read must still be rejected")
   | Ok _ -> Alcotest.fail "expected one query"
 
 let test_exists () =
@@ -444,10 +478,20 @@ let () =
         [
           Alcotest.test_case "forall holds" `Quick test_forall_holds;
           Alcotest.test_case "forall fails" `Quick test_forall_fails;
-          Alcotest.test_case "forall over infinite rejected" `Quick
-            test_forall_over_infinite_rejected;
           Alcotest.test_case "exists" `Quick test_exists;
         ] );
+      ( "symbolic",
+        [
+          Alcotest.test_case "naturals nonnegative" `Quick
+            test_symbolic_naturals_nonnegative;
+          Alcotest.test_case "integers not nonnegative" `Quick
+            test_symbolic_integers_not_nonnegative;
+          Alcotest.test_case "inclusion" `Quick test_symbolic_inclusion;
+          Alcotest.test_case "interval entailment" `Quick
+            test_symbolic_interval_entailment;
+          Alcotest.test_case "outside fragment still rejected" `Quick
+            test_forall_outside_fragment_still_rejected;
+        ] );
       ( "criteria",
         [
           Alcotest.test_case "criterion admits" `Quick test_criterion_admits;