diff options
Diffstat (limited to 'test')
| -rw-r--r-- | test/test_vm.ml | 16 |
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; ] ); |