diff options
Diffstat (limited to 'test/test_vm.ml')
| -rw-r--r-- | test/test_vm.ml | 32 |
1 files changed, 32 insertions, 0 deletions
diff --git a/test/test_vm.ml b/test/test_vm.ml index ad58720..f3d8484 100644 --- a/test/test_vm.ml +++ b/test/test_vm.ml @@ -278,6 +278,27 @@ let test_exists () = ^ {| Query expression: [Exists variable: P quantifier: [Person name: P age: B] body: [GreaterThan left: B right: 60]] |}) "B=70" +(* Constraint propagation over residue. *) + +let test_contradictory_residue_fails () = + check_answers "an empty interval is no, not a conditioned answer" + {| Query expression: [GreaterThan left: X right: 5] :and [LessThan left: X right: 3] |} + "" + +let test_kind_conflict_fails () = + check_answers "no value is both an integer and a string" + {| Query expression: [Integer value: X] :and [String value: X] |} "" + +let test_finite_narrowing_enumerates () = + check_answers "a pinned natural enumerates like Between" + {| Query expression: [Natural value: X] :and [LessThan left: X right: 4] |} + "X=0; X=1; X=2; X=3" + +let test_rational_bounds_narrow_integers () = + check_answers "strict rational bounds squeeze to integers" + {| Query expression: [Integer value: X] :and [GreaterThan left: X right: 1/2] :and [LessThanEqual left: X right: 5/2] |} + "X=1; X=2" + (* Integrity control at loading: facts must satisfy their schema. *) let test_fact_domain_violation () = @@ -400,6 +421,17 @@ let () = Alcotest.test_case "fact domain violation" `Quick test_fact_domain_violation; ] ); + ( "propagation", + [ + Alcotest.test_case "contradictory residue fails" `Quick + test_contradictory_residue_fails; + Alcotest.test_case "kind conflict fails" `Quick + test_kind_conflict_fails; + Alcotest.test_case "finite narrowing enumerates" `Quick + test_finite_narrowing_enumerates; + Alcotest.test_case "rational bounds narrow integers" `Quick + test_rational_bounds_narrow_integers; + ] ); ( "negation", [ Alcotest.test_case "not adults" `Quick test_negation; |