Added missing test file for Cadical interface

jrh13 · Jun 27, 2024 · 27f8d1c · 27f8d1c
1 parent 1681896
commit 27f8d1c
Showing 1 changed file with 14 additions and 0 deletions.
diff --git a/Cadical/test.ml b/Cadical/test.ml
@@ -0,0 +1,14 @@
+(* ========================================================================= *)
+(* Test the Cadical interface on a set of (relatively easy) tautologies.     *)
+(* ========================================================================= *)
+
+needs "Minisat/taut.ml";;
+
+let TEST_TAUT TAUTCHECKER p =
+  let th = time TAUTCHECKER p in
+  if hyp th = [] && concl th = p
+  then true else failwith "Wrong theorem";;
+
+map (fun (p,s) -> print_string("Attempting "^s); print_newline();
+                  s,TEST_TAUT CADICAL_PROVE p)
+        all_taut;;