diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml index 8961a2360998c11cd2faa4a970a6f6f97b554929..649a26b637f8bf9df7cb574d049309a77e9e9e09 100644 --- a/src/testsuite/cool-testsuite.ml +++ b/src/testsuite/cool-testsuite.ml @@ -22,6 +22,15 @@ let k_testcases: satCheck list = ; c Sat "C |- [R] ~C" ] + +let nominal_testcases = + let c a b = (a,k,b) in + [ c Sat "@ i' <r> p" + ; c Sat "@ i' <r> i'" + ; c Unsat "@ i' <r> i' & @i' [r] ~ i'" + ; c Sat "@ i' [r] (@ i' (~i')) " + ] + let kd_testcases = let c a b = (a,kd,b) in [ c Sat "True" @@ -36,12 +45,13 @@ let kd_testcases = let testcases = let c name table = (name,table) in [ c "K" k_testcases + ; c "Nominals" nominal_testcases ; c "KD" kd_testcases ] let main = foreach_l testcases (fun (name,table) -> - Printf.printf "\n==== Testing logic %s ====\n" name; + Printf.printf "\n==== Testing %s ====\n" name; foreach_l table runSatCheckVerbose )