Add testcases for KD

src/testsuite/Testsuite.ml

@@ -52,10 +52,8 @@ let runSatCheckVerbose (sc:satCheck) =
     let res = runSatCheck sc in
     if (res = expectation)
     then PF.printf "%s\n" (cs "1;32" "Yes")
-    else PF.printf "%s\n  -> %s: Expected %s but got %s!\n"
+    else PF.printf "%s, it is %s\n"
                     (cs "1;31" "No")
-                    (cs "1;31" "Failure")
-                    (sotr expectation)
                     (sotr res)
 
 

src/testsuite/cool-testsuite.ml

@@ -17,11 +17,32 @@ let k_testcases: satCheck list =
     ; c Unsat "False"
     ; c ParseError  "{Fsdf"
     (*; c ParseError  "Fsdf}" *)
+    ; c Unsat "<R> True & [R] False"
+    ; c Unsat "C |- <R> ~C"
+    ; c Sat   "C |- [R] ~C"
+    ]
+
+let kd_testcases =
+    let c a b = (a,kd,b) in
+    [ c Sat   "True"
+    ; c Unsat "False"
+    ; c ParseError  "{Fsdf"
+    (*; c ParseError  "Fsdf}" *)
+    ; c Unsat "<R> True & [R] False"
+    ; c Unsat "C |- <R> ~C"
+    ; c Unsat "C |- [R] ~C"
+    ]
+
+let testcases =
+    let c name table = (name,table) in
+    [ c "K"  k_testcases
+    ; c "KD" kd_testcases
     ]
 
 let main =
-    foreach_l k_testcases (fun tc ->
-        runSatCheckVerbose tc
+    foreach_l testcases (fun (name,table) ->
+        Printf.printf "\n==== Testing logic %s ====\n" name;
+        foreach_l table runSatCheckVerbose
     )
 
 let _ = main