From 2e893fd0df7dae8c4ae843d4a23acb098dd97aff Mon Sep 17 00:00:00 2001
From: filip <“filip.rabiega@gmail.com”>
Date: Tue, 22 Apr 2025 18:38:38 +0200
Subject: added a functional parser

---
 test/test_chadprover.ml | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)

(limited to 'test/test_chadprover.ml')

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;;
-- 
cgit v1.2.3