onestep decision implemented based on flag

src/exes/coalg/coalg.ml

@@ -16,6 +16,9 @@ module FE = FunctorParsing
 
 open CoolUtils
 
+let a_list_functor_tableau_onestep =
+  ["K", "ot"; "CL", "t"; "GML", "o"; "PML", ""]
+
 (* A partial function mapping nominals to their sorts. *)
 let nomTable name =
   assert (CoAlgFormula.isNominal name);
@@ -177,8 +180,18 @@ let printUsage name =
 
 let counter = ref 0
 
+exception Not_Implemented of string
+let check_implementation logic onestep = 
+  match (List.assoc logic a_list_functor_tableau_onestep) with
+  | "ot" | "to"   -> onestep
+  | "o"           -> let _ = (print_endline "\nOnly onestep implementation available") in true
+  | "t"           -> let _ = (print_endline "\nOnly tableau implementation available") in false
+  | _             -> raise (Not_Implemented  (logic ^ "is not implemented!"))        
+
 let choiceSat opts =
     let verb = opts.verbose in
+    let onestep = check_implementation Sys.argv.(2) opts.onestep
+    in
     let sorts = (FE.sortTableFromString Sys.argv.(2)) in
 
     (* test if GML or PML occurs in sort table *)
@@ -199,7 +212,7 @@ let choiceSat opts =
           incr counter;
           print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
           flush stdout;
-          printRes (Reasoner.isSat ~verbose:verb opts.fragment opts.game_solver opts.prop_rate sorts nomTable tbox f)
+          printRes (Reasoner.isSat ~onestep:onestep ~verbose:verb opts.fragment opts.game_solver opts.prop_rate sorts nomTable tbox f)
         else ()
       done
     with End_of_file -> ()