Add prov task

coalg.ml

@@ -5,6 +5,7 @@
  *)
 
 module CM = CoAlgMisc
+module CF = CoAlgFormula
 
 (* The type of formulae that are accepted. *)
 (*
@@ -36,7 +37,7 @@ let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increm
 
 let printUsage () =
   print_endline "Usage: \"alc <task> <functor> [<flags>]\" where";
-  print_endline "       <task> in { sat print }";
+  print_endline "       <task> in { sat print prov (is \f -> not (sat (not f))) }";
   print_endline "       <functor> in { MultiModalK MultiModalKD CoalitionLogic GML";
   print_endline "                      (or: K)     (or: KD)     (or: CL)       }";
   print_endline "       <flags> = a list of the following items";
@@ -79,15 +80,39 @@ let choiceSat () =
       while true do
         let input = read_line () in
         if not (GenAndComp.isEmptyString input) then
-          let (f, tbox) = CoAlgFormula.importQuery input in
+          let (tbox, f) = CoAlgFormula.importQuery input in
           incr counter;
           print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
           flush stdout;
-          printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable f tbox)
+          printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox f)
         else ()
       done
     with End_of_file -> ()
 
+let choiceProvable () =
+    let verb = !verbose in
+    let sorted_not ((s,f):CF.sortedFormula) : CF.sortedFormula =
+        (s,CF.NOT f)
+    in
+    let sorts = [| (parseFunctor Sys.argv.(2), [0]) |] in
+    let printRes sat =
+      if not verb then
+        print_endline (if not sat then "provable\n" else "unprovable\n")
+      else ()
+    in
+    try
+      while true do
+        let input = read_line () in
+        if not (GenAndComp.isEmptyString input) then
+          let (tbox,f) = CoAlgFormula.importQuery input in
+          let fneg = sorted_not f in
+          incr counter;
+          print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
+          flush stdout;
+          printRes (CoAlgReasoner.isSat ~verbose:verb sorts nomTable tbox fneg)
+        else ()
+      done
+    with End_of_file -> ()
 let choicePrint () =
     try
       while true do
@@ -130,6 +155,7 @@ let _ =
     parseFlags Sys.argv 3;
     match choice with
     | "sat" -> choiceSat ()
+    | "prov" -> choiceProvable ()
     | "print" -> choicePrint ()
     | _ -> printUsage ()