algebraic identities of plus and times discharge symbolically

1 files changed, 16 insertions, 0 deletions

diff --git a/test/test_vm.ml b/test/test_vm.ml
index 16ca63c..4729841 100644
--- a/test/test_vm.ml
+++ b/test/test_vm.ml
@@ -292,6 +292,20 @@ let test_symbolic_interval_entailment () =
     (holds
        {| Query expression: [ForAll variable: X quantifier: ([Natural value: X] :and [GreaterEqual left: X right: 10]) body: [GreaterThan left: X right: 5]] |})
 
+let test_symbolic_algebraic_identity () =
+  (* The specification's flagship symbolic example, in the flat
+     membership form of decision 14. *)
+  Alcotest.(check bool) "adding zero is the identity, over all integers" true
+    (holds
+       {| Query expression: [ForAll variable: X quantifier: [Integer value: X] body: [Plus left: X right: 0 result: X]] |});
+  Alcotest.(check bool) "multiplying by one is the identity, over all rationals"
+    true
+    (holds
+       {| Query expression: [ForAll variable: X quantifier: [Rational value: X] body: [Times left: 1 right: X result: X]] |});
+  Alcotest.(check bool) "strings do not add" false
+    (holds
+       {| Query expression: [ForAll variable: X quantifier: [String value: X] body: [Plus left: X right: 0 result: X]] |})
+
 let test_forall_outside_fragment_still_rejected () =
   match
     load
@@ -489,6 +503,8 @@ let () =
           Alcotest.test_case "inclusion" `Quick test_symbolic_inclusion;
           Alcotest.test_case "interval entailment" `Quick
             test_symbolic_interval_entailment;
+          Alcotest.test_case "algebraic identity" `Quick
+            test_symbolic_algebraic_identity;
           Alcotest.test_case "outside fragment still rejected" `Quick
             test_forall_outside_fragment_still_rejected;
         ] );