Reorganize code, start from Sat nodes as well

Not only finishing cycles but also plain sat nodes may cause a node to
be satisfiable

src/lib/CoAlgReasoner.ml

@@ -118,12 +118,15 @@ let propagateSatMu () =
   let setFinishingCores = setEmptyCore () in
   let setStates = setEmptyState () in
   let setCores = setEmptyCore () in
+  let setSatStates = setEmptyState () in
+  let setSatCores = setEmptyCore () in
   let emptySet = bsetMakeRealEmpty () in
 
   let stateCollector state =
     match stateGetStatus state with
-    | Unsat
-    | Sat -> ()
+    | Unsat -> ()
+    | Sat ->
+       setAddState setSatStates state
     | Expandable
     | Open ->
        setAddState setStates state;
@@ -136,8 +139,9 @@ let propagateSatMu () =
   in
   let coreCollector core =
     match coreGetStatus core with
-    | Unsat
-    | Sat -> ()
+    | Unsat -> ()
+    | Sat ->
+       setAddCore setSatCores core
     | Expandable
     | Open ->
        setAddCore setCores core;
@@ -166,27 +170,6 @@ let propagateSatMu () =
   let rec fixpointstep setStates setCores =
     let allowedStates = setEmptyState () in
     let allowedCores = setEmptyCore () in
-    let initialStates = setEmptyState () in
-    let initialCores = setEmptyCore () in
-
-    let checkFinishingState (state : state) =
-      let ruleiter (dependencies, corelist) : bool =
-        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable) corelist
-      in
-      if not (List.exists ruleiter (stateGetRules state)) then begin
-        setAddState allowedStates state;
-        setAddState initialStates state
-      end
-    in
-    let checkFinishingCore (core : core) =
-      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable)
-                (coreGetChildren core)) then begin
-        setAddCore allowedCores core;
-        setAddCore initialCores core
-      end
-    in
-    setIterState checkFinishingState setFinishingStates;
-    setIterCore checkFinishingCore setFinishingCores;
 
     let rec visitParentStates (core : core) : unit =
       if not (setMemCore setCores core) then ()
@@ -222,8 +205,34 @@ let propagateSatMu () =
       end
     in
 
-    setIterState visitParentCores initialStates;
-    setIterCore visitParentStates initialCores;
+    (* All rule applications need to still be potentially Sat for a
+     * finishing State to be a valid startingpoint for this fixpoint.
+     *)
+    let checkFinishingState (state : state) =
+      let ruleiter (dependencies, corelist) : bool =
+        List.for_all (fun (core : core) -> coreGetStatus core == Unsat || coreGetStatus core == Expandable) corelist
+      in
+      if not (List.exists ruleiter (stateGetRules state)) then begin
+        setAddState allowedStates state;
+        visitParentCores state
+      end
+
+    (* There needs to be a State still potentially Sat for this core
+     * to be considered for the fixpoint
+     *)
+    and checkFinishingCore (core : core) =
+      if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || stateGetStatus state == Expandable)
+                           (coreGetChildren core))
+      then begin
+        setAddCore allowedCores core;
+        visitParentStates core
+      end
+    in
+    setIterState checkFinishingState setFinishingStates;
+    setIterCore checkFinishingCore setFinishingCores;
+    setIterState visitParentCores setSatStates;
+    setIterCore visitParentStates setSatCores;
+
 
     if (setLengthState setStates) = (setLengthState allowedStates) &&
          (setLengthCore setCores) = (setLengthCore allowedCores)