preliminary propafateSat for μ-Calculus

This still produces wrong results: It assumes every node with empty
focus to be sat.

src/lib/CoAlgReasoner.ml

@@ -113,6 +113,102 @@ let propagateSat () =
   setIterCnstr (fun cset -> graphReplaceCnstr cset SatC) setCnstr
 
 
+let propagateSatMu () =
+  let setFinishingStates = setEmptyState () in
+  let setFinishingCores = setEmptyCore () in
+  let setStates = setEmptyState () in
+  let setCores = setEmptyCore () in
+  let emptySet = bsetMakeRealEmpty () in
+
+  let stateCollector state =
+    match stateGetStatus state with
+    | Unsat
+    | Sat -> ()
+    | Expandable
+    | Open ->
+       setAddState setStates state;
+       if bsetCompare (stateGetDeferral state) emptySet == 0
+       then begin
+           print_endline (stateToString state);
+           setAddState setFinishingStates state
+         end
+       else ()
+  in
+  let coreCollector core =
+    match coreGetStatus core with
+    | Unsat
+    | Sat -> ()
+    | Expandable
+    | Open ->
+       setAddCore setCores core;
+       if bsetCompare (coreGetDeferral core) emptySet == 0
+       then begin
+           print_endline (coreToString core);
+           setAddCore setFinishingCores core
+         end
+       else ()
+  in
+  graphIterStates stateCollector;
+  graphIterCores coreCollector;
+
+  (*
+    In a fixpoint the set called setStates / setCores is narrowed down.
+
+    In each step only those states and cores are retained in setStates
+    / setCores which reach one of setFinishing{States,Cores} in
+    finitely many steps. This new set of States / Cores is collected
+    as allowed{States,Cores} during each fixpoint iteration.
+
+    Only those finishing nodes are retained that have allowed or
+    Successfull Children.
+  *)
+
+  let rec fixpointstep setStates setCores =
+    let allowedStates = setFinishingStates in
+    let allowedCores = setFinishingCores in
+
+    let rec visitParentStates (core : core) : unit =
+      if setMemCore allowedCores core then () else begin
+        let children = coreGetChildren core in
+        let acceptable = List.exists (fun (state) -> setMemState allowedStates state) children in
+        if acceptable then begin
+          print_endline ("Considering Core " ^ (string_of_int (coreGetIdx core)) ^ " as allowed");
+          setAddCore allowedCores core;
+          List.iter (fun (state, _) -> visitParentCores state)
+            (coreGetParents core)
+        end
+      end
+
+    and visitParentCores (state : state) : unit =
+      if setMemState allowedStates state then () else begin
+        let rules = stateGetRules state in
+        let ruleiter (dependencies, corelist) =
+          List.exists (fun (core) -> setMemCore allowedCores core) corelist
+        in
+        let acceptable = List.for_all ruleiter rules in
+        if acceptable then begin
+          print_endline ("Considering State " ^ (string_of_int (stateGetIdx state)) ^ " as allowed");
+          setAddState allowedStates state;
+          List.iter (fun core -> visitParentStates core)
+            (stateGetParents state)
+        end
+      end
+    in
+
+    setIterState visitParentCores setFinishingStates;
+    setIterCore visitParentStates setFinishingCores;
+
+    if (setLengthState setStates) = (setLengthState allowedStates) &&
+      (setLengthCore setCores) = (setLengthCore allowedCores)
+    then begin
+      setIterState (fun state -> stateSetStatus state Sat) setStates;
+      setIterCore (fun core -> coreSetStatus core Sat) setCores;
+    end else
+      fixpointstep allowedStates allowedCores
+  in
+  fixpointstep setStates setCores
+
+
 (*****************************************************************************)
 (*                     Propagation of Unsatisfiability                       *)
 (*****************************************************************************)