Implement testcase skipping to avoid PML crashes

src/testsuite/cool-testsuite.ml

@@ -100,9 +100,9 @@ let kOrKd_testcases : satCheck list =
 
 let pml_testcases : testcase_section =
     use_functor "PML"
-    [ sat   "{>= 1/3} C & {< 1/2} D"
-    ; sat   "{>= 1/3} C & {< 1/2} C"
-    ; unsat "{< 1/3} C & {>= 1/2} C"
+    [ sat   "SKIP {>= 1/3} C & {< 1/2} D"
+    ; sat   "SKIP {>= 1/3} C & {< 1/2} C"
+    ; unsat "SKIP {< 1/3} C & {>= 1/2} C"
     ; sat   "{< 1/3} C & {< 1/2} C"
     ]
 
@@ -119,13 +119,15 @@ let testcases =
     ; pml_testcases
     ; use_functor "PML + K"
         [ sat "(P4 + False)"
-        ; sat "(({>= 3/5} p0 & {>= 2/5} p1) + False)"
-        ; sat "({>= 3/5} (False + <R1> True & <R2> True) & {>= 2/5} ({>= 1/10} p0 & {>= 1/10} (~ p0) + False ) + False)"
+        ; sat "SKIP (({>= 3/5} p0 & {>= 2/5} p1) + False)"
+        ; sat "SKIP ({>= 3/5} (False + <R1> True & <R2> True) & {>= 2/5} ({>= 1/10} p0 & {>= 1/10} (~ p0) + False ) + False)"
         ]
     ]
 
 let main =
+    let skipchecker = Str.regexp "SKIP " in (* skip formulas beginning with "SKIP " *)
     let success = ref 0 in
+    let skipped = ref 0 in
     let failed = ref 0 in
     foreach_l testcases (fun (name,table) ->
         Printf.printf "==== Testing %s ====\n" name;
@@ -134,19 +136,26 @@ let main =
         Printf.printf "sortTable = %s\n" (FP.stringFromSortTable sorts);
         *)
         foreach_l table (fun sc ->
-            let (expected,_,_) = sc in
-            let actual = runSatCheckVerbose sc in
-            (* compare the expected and the actual result *)
-            if actual = expected
-            then success := !success + 1
-            else failed := !failed + 1
+            let (expected,sort,formula) = sc in
+            if Str.string_match skipchecker formula 0
+            then begin
+                print_endline ("Skipping formula »"^formula^"«");
+                skipped := !skipped + 1
+            end else begin
+                let actual = runSatCheckVerbose sc in
+                (* compare the expected and the actual result *)
+                if actual = expected
+                then success := !success + 1
+                else failed := !failed + 1
+            end
         );
         print_endline ""
     );
     let s n = if n = 1 then "testcase" else "testcases" in
-    Printf.printf "=> %d %s succeeded, %d %s failed.\n"
+    Printf.printf "=> %d %s succeeded, %d %s failed, %d skipped.\n"
         !success (s !success)
         !failed (s !failed)
+        !skipped
 
 let _ = main