diff options
| author | filip <“filip.rabiega@gmail.com”> | 2025-04-22 18:38:38 +0200 |
|---|---|---|
| committer | filip <“filip.rabiega@gmail.com”> | 2025-04-22 18:59:19 +0200 |
| commit | 2e893fd0df7dae8c4ae843d4a23acb098dd97aff (patch) | |
| tree | 1f4a50da28d2e6ef04b2fc2b663790b42352f2ca /test/test_chadprover.ml | |
| parent | af76b11278204c25428c4f95ef51d4aa8f2a1e0e (diff) | |
| download | chadprover-2e893fd0df7dae8c4ae843d4a23acb098dd97aff.tar.gz chadprover-2e893fd0df7dae8c4ae843d4a23acb098dd97aff.tar.bz2 chadprover-2e893fd0df7dae8c4ae843d4a23acb098dd97aff.zip | |
added a functional parser
Diffstat (limited to 'test/test_chadprover.ml')
| -rw-r--r-- | test/test_chadprover.ml | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/test/test_chadprover.ml b/test/test_chadprover.ml index e69de29..9c9575e 100644 --- a/test/test_chadprover.ml +++ b/test/test_chadprover.ml @@ -0,0 +1,24 @@ +open Chadprover.Types +open Chadprover.Lib_utils +open Chadprover.To_string + +let show_example p i = + print_endline ("Proposition p: " ^ (string_of_prop p)); + print_endline ("p in NNF: " ^ (string_of_prop (to_nnf p))); + print_endline ("Interpretation i: " ^ (string_of_interpr i)); + print_endline ("p under i: " ^ (string_of_prop (interpret p i)) ^ "\n");; + +let p1 = Not(Not(Not(And(Lit "a", Lit "b"))));; +let p2 = Iff(Not(Implies(Or(Lit "a", Lit "b"), And(Lit "b", Lit "c"))), True);; +let i1 = [("a", false); ("b", true); ("c", false)];; +let i2 = [("a", false); ("b", false)];; +let i3 = [("c", true)];; + +let () = + show_example p1 i1; + show_example p1 i2; + show_example p1 i3; + + show_example p2 i1; + show_example p2 i2; + show_example p2 i3;; |