From c9bfcb988679f2ff4d024c6b0140d012fa6ec364 Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hans-peter.deifel@fau.de>
Date: Wed, 18 Oct 2017 20:48:06 +0200
Subject: [PATCH] Make propagation rate configurable with command line flag

Adds the parameter --propagationRate
---
 src/coalg/coalg.ml               | 26 +++++++++++++++++++----
 src/coalgcompare/coalgcompare.ml |  2 +-
 src/debugger/debugger.ml         |  2 +-
 src/lib/CoAlgMisc.mli            |  1 -
 src/lib/CoAlgReasoner.ml         | 19 ++++++++++++-----
 src/lib/CoAlgReasoner.mli        | 12 +++++++++--
 src/lib/CoolGraph.ml             | 36 +++++++++++++++++++++++---------
 src/lib/CoolGraph.mli            |  4 ++++
 src/owl/cool-owl.ml              |  2 +-
 src/testsuite/Testsuite.ml       |  2 +-
 10 files changed, 80 insertions(+), 26 deletions(-)

diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index e4c436e..b56e056 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -24,9 +24,10 @@ let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increm
 type options =
   { verbose : bool
   ; fragment : CM.fragment_spec
+  ; prop_rate : Reasoner.propagation_rate
   }
 
-let defaultOpts = { verbose = false; fragment = CM.Auto }
+let defaultOpts = { verbose = false; fragment = CM.Auto; prop_rate = Reasoner.Adaptive }
 
 let options =
   [ { Args.long = "verbose"
@@ -61,6 +62,23 @@ let options =
         Args.Required_arg
           ("FRAGMENT", fun s a -> { a with fragment = parse_fragment s })
     }
+  ; { Args.long = "propagationRate"
+    ; Args.short = None
+    ; Args.description = "Rate of Unsat/Sat propagation.\n"
+                         ^ "Possible values are:\n"
+                         ^ "   \"once\": Propagate only when the tableaux is fully expanded\n"
+                         ^ "   \"adaptive\": Automatic mode based on the number of open states\n"
+                         ^ "   INTEGER: Propagate after this many expansion steps"
+    ; Args.argument =
+        let parse_prop_rate s = match s with
+          | "once" -> Reasoner.Once
+          | "adaptive" -> Reasoner.Adaptive
+          | _ -> try Reasoner.Fixed (int_of_string s) with
+                 | Failure _ -> raise (Args.ParseError ("Invalid integer: " ^ s))
+        in
+        Args.Required_arg
+          ("RATE", fun s a -> { a with prop_rate = parse_prop_rate s })
+    }
   ]
 
 let printUsage name =
@@ -126,7 +144,7 @@ let choiceSat opts =
           incr counter;
           print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
           flush stdout;
-          printRes (Reasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox f)
+          printRes (Reasoner.isSat ~verbose:verb opts.fragment opts.prop_rate sorts nomTable tbox f)
         else ()
       done
     with End_of_file -> ()
@@ -151,7 +169,7 @@ let choiceProvable opts =
           incr counter;
           print_string ("\nFormula " ^ (string_of_int !counter) ^ ": ");
           flush stdout;
-          printRes (Reasoner.isSat ~verbose:verb opts.fragment sorts nomTable tbox fneg)
+          printRes (Reasoner.isSat ~verbose:verb opts.fragment opts.prop_rate sorts nomTable tbox fneg)
         else ()
       done
     with End_of_file -> ()
@@ -204,7 +222,7 @@ let choiceGraph opts =
 
   let input = read_line () in
   let (tbox, f) = CoAlgFormula.importQuery input in
-  ignore(Reasoner.isSat opts.fragment sorts nomTable tbox f);
+  ignore(Reasoner.isSat opts.fragment opts.prop_rate sorts nomTable tbox f);
   print_endline (Reasoner.G.graphToDot ())
 
 let choiceVerify opts =
diff --git a/src/coalgcompare/coalgcompare.ml b/src/coalgcompare/coalgcompare.ml
index 73540b2..f91d108 100644
--- a/src/coalgcompare/coalgcompare.ml
+++ b/src/coalgcompare/coalgcompare.ml
@@ -125,7 +125,7 @@ let exportALCQuery tbox (_, f) =
 
 
 let solvCoalg sortTable args =
-  G.evaluateFkt (fun (tbox, sf) -> Reasoner.isSat CoAlgMisc.Auto sortTable nomTable tbox sf) args
+  G.evaluateFkt (fun (tbox, sf) -> Reasoner.isSat CoAlgMisc.Auto Reasoner.Adaptive sortTable nomTable tbox sf) args
 
 let solvALC (tbox, sf) =
   let args = exportALCQuery tbox sf in
diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml
index 7c0786d..990f317 100644
--- a/src/debugger/debugger.ml
+++ b/src/debugger/debugger.ml
@@ -101,7 +101,7 @@ let _ =
     let formula = Sys.argv.(2) in
     let sorts = (FE.sortTableFromString Sys.argv.(1)) in
     let (tbox, f) = CoAlgFormula.importQuery formula in
-    Reasoner.initReasoner CoAlgMisc.Auto sorts nomTable tbox f;
+    Reasoner.initReasoner CoAlgMisc.Auto Reasoner.Adaptive sorts nomTable tbox f;
     let session = {
       Repl.prompt = "> ";
       Repl.bindings = Repl.addHelpBinding [
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 81b2bff..321e200 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -229,7 +229,6 @@ type fragment_spec = Auto | Fragment of fragment
 (** Return the fragment of the mu-calculus that the original formula uses *)
 val getFragment : unit -> fragment
 
-
 type fixpoint_type = MU | NU
 type bound_vars = (fixpoint_type * string * CoAlgFormula.HcFHt.key) list
 
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 24fe15c..e3a43de 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -21,12 +21,16 @@ exception ReasonerError of string
 
 module type S = sig
 module G : CoolGraph.S
-val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> sortTable
+
+type propagation_rate = G.propagation_rate = Once | Adaptive | Fixed of int
+
+val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> propagation_rate
+            -> sortTable
             -> (string -> CoAlgFormula.sort option) ->
             CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
 
 
-val initReasoner : CoAlgMisc.fragment_spec -> sortTable
+val initReasoner : CoAlgMisc.fragment_spec -> propagation_rate -> sortTable
                    -> (string -> CoAlgFormula.sort option) ->
                    CoAlgFormula.sortedFormula list
                    -> CoAlgFormula.sortedFormula -> unit
@@ -269,6 +273,9 @@ let solveGame () =
       end
   in
 
+  if getPropagationRate () == Adaptive then
+    setPropagationCounter (Hashtbl.length seenOpen)
+  else ();
   HashSet.iter applySolution seenOpen
 
 (* let propagateSatMu () = *)
@@ -1216,7 +1223,7 @@ let rec buildGraphLoop () =
   (* if propagating nominals added some more queue members, do all again.. *)
   if queueIsEmpty () then () else buildGraphLoop ()
 
-let initReasoner fragSpec sorts nomTable tbox sf =
+let initReasoner fragSpec propagation_rate sorts nomTable tbox sf =
   sortTable := Array.copy sorts;
   let (tbox1, sf1, bs) = ppFormulae fragSpec nomTable tbox sf in
   let sort = fst sf in
@@ -1225,6 +1232,7 @@ let initReasoner fragSpec sorts nomTable tbox sf =
   graphInit ();
   queueInit ();
   PG_Map.reset ();
+  setPropagationRate propagation_rate;
   let root = insertCore sort bs1 focus in
   graphAddRoot root
 
@@ -1242,6 +1250,7 @@ let reasonerFinished () =
   | Sat  -> true
   | Open -> queueIsEmpty ()
 
+type propagation_rate = G.propagation_rate = Once | Adaptive | Fixed of int
 
 (** A graph-tableau-based decision procedure framework for coalgebraic logics.
     @param verbose An optional switch which determines
@@ -1256,9 +1265,9 @@ let reasonerFinished () =
     @return True if sf is satisfiable wrt tbox, false otherwise.
  *)
 
-let isSat ?(verbose = false) fragSpec sorts nomTable tbox sf =
+let isSat ?(verbose = false) fragSpec propagation_rate sorts nomTable tbox sf =
   let start = if verbose then Unix.gettimeofday () else 0. in
-  initReasoner fragSpec sorts nomTable tbox sf;
+  initReasoner fragSpec propagation_rate sorts nomTable tbox sf;
   let sat =
     try
       buildGraphLoop ();
diff --git a/src/lib/CoAlgReasoner.mli b/src/lib/CoAlgReasoner.mli
index b408102..712172e 100644
--- a/src/lib/CoAlgReasoner.mli
+++ b/src/lib/CoAlgReasoner.mli
@@ -16,12 +16,20 @@ exception ReasonerError of string
 
 module type S = sig
 module G : CoolGraph.S
-val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> sortTable
+
+(** Specifies when cool propagates sat/unsat information. *)
+type propagation_rate = G.propagation_rate =
+  | Once          (** Propagate only when the tableaux is fully expanded *)
+  | Adaptive       (** Automatic mode based on the number of open states *)
+  | Fixed of int   (** Propagate after this many expansion steps *)
+
+val isSat : ?verbose:bool -> CoAlgMisc.fragment_spec -> propagation_rate
+            -> sortTable
             -> (string -> CoAlgFormula.sort option) ->
             CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
 
 
-val initReasoner : CoAlgMisc.fragment_spec -> sortTable
+val initReasoner : CoAlgMisc.fragment_spec -> propagation_rate -> sortTable
                    -> (string -> CoAlgFormula.sort option) ->
                    CoAlgFormula.sortedFormula list
                    -> CoAlgFormula.sortedFormula -> unit
diff --git a/src/lib/CoolGraph.ml b/src/lib/CoolGraph.ml
index 24382db..c715f03 100644
--- a/src/lib/CoolGraph.ml
+++ b/src/lib/CoolGraph.ml
@@ -53,6 +53,10 @@ module type S = sig
   val queueGetElement : unit -> queueElement
   val queuePrettyStatus : unit -> string
 
+  type propagation_rate = Once | Adaptive | Fixed of int
+  val setPropagationRate : propagation_rate -> unit
+  val getPropagationRate : unit -> propagation_rate
+
   val setPropagationCounter : int -> unit
   val doNominalPropagation : unit -> bool
   val doSatPropagation : unit -> bool
@@ -329,19 +333,31 @@ let queueGetElement () =
 
 let doNominalPropagation () = !doPropagation
 
+type propagation_rate = Once | Adaptive | Fixed of int
+
+let prop_rate = ref Once
+
+let setPropagationRate p = prop_rate := p
+
+let getPropagationRate () = !prop_rate
+
 let setPropagationCounter count =
   doPropagationCounter := count
 
-let doSatPropagation () =
-  if !doPropagationCounter == 0
-  then true
-  else begin
-      doPropagationCounter := !doPropagationCounter - 1;
-      false
-    end
-  (* let res = !doPropagation in *)
-  (* doPropagation := false; *)
-  (* res *)
+let doSatPropagation () = match !prop_rate with
+  | Once -> false
+  | Fixed n ->
+     if !doPropagationCounter == 0 then begin
+         doPropagationCounter := n; true
+       end else begin
+         decr doPropagationCounter; false
+       end
+  | Adaptive ->
+     if !doPropagationCounter == 0 then
+         true                   (* the new value has to be set in the reasoner *)
+       else begin
+         decr doPropagationCounter; false
+       end
 
 (*****************************************************************************)
 (*        "Module type" and a specific implementation of the graph           *)
diff --git a/src/lib/CoolGraph.mli b/src/lib/CoolGraph.mli
index 9f3a2b2..aae81f2 100644
--- a/src/lib/CoolGraph.mli
+++ b/src/lib/CoolGraph.mli
@@ -48,6 +48,10 @@ module type S = sig
   val queueGetElement : unit -> queueElement
   val queuePrettyStatus : unit -> string
 
+  type propagation_rate = Once | Adaptive | Fixed of int
+  val setPropagationRate : propagation_rate -> unit
+  val getPropagationRate : unit -> propagation_rate
+
   val setPropagationCounter : int -> unit
   val doNominalPropagation : unit -> bool
   val doSatPropagation : unit -> bool
diff --git a/src/owl/cool-owl.ml b/src/owl/cool-owl.ml
index 5ea42a0..b69393f 100644
--- a/src/owl/cool-owl.ml
+++ b/src/owl/cool-owl.ml
@@ -45,7 +45,7 @@ let consistency () =
         | (_, []) -> raise (Exception "File needs to contain at least one ontology")
     in
     let (sorts,nomTable,axioms) = OWL.to_coalg ontology in
-    let cons = CR.isSat CoAlgMisc.Auto sorts nomTable axioms (0,CF.TRUE) in
+    let cons = CR.isSat CoAlgMisc.Auto CR.Adaptive sorts nomTable axioms (0,CF.TRUE) in
     let cons = if cons then "yes" else "no" in
     let (ontoname, _) = ontology in
     Printf.printf "%s consistent: %s\n" ontoname cons
diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml
index b0b7987..329b4f9 100644
--- a/src/testsuite/Testsuite.ml
+++ b/src/testsuite/Testsuite.ml
@@ -41,7 +41,7 @@ let runSatCheck (_,logic,input) =
       (* isSat leaks tons of memory. Call it in new process to allow the OS to
          reclaim that memory between calls. *)
       match Unix.fork () with
-      | 0 -> let res = CR.isSat CoAlgMisc.Auto logic nomTable tbox f in
+      | 0 -> let res = CR.isSat CoAlgMisc.Auto CR.Adaptive logic nomTable tbox f in
              if res then exit 0 else exit 1
       | -1 -> raise (CoAlgFormula.CoAlgException "fork() failed")
       | _ -> match Unix.wait () with
-- 
GitLab