Add a single satisfiable game node to states without children

src/lib/CoAlgReasoner.ml

@@ -139,7 +139,6 @@ let solveGame () =
     | Unsat -> PG_Map.unsat_node
     | Open -> stateGetIdx state
   in
-
   let coreGetIdxOr node core =
     match coreGetStatus core with
     | Expandable ->
@@ -160,28 +159,22 @@ let solveGame () =
     | Open -> coreGetIdx core
   in
 
+  let emptyToSat = function
+    | [] -> [PG_Map.sat_node]
+    | x -> x
+  in
+
   let nodeSucessors1 node =
-    let res = match PG_Map.find node with
-      | PG_Map.State state -> List.map fst (stateGetRulesWithIndex state)
-      | PG_Map.Core core -> List.map (stateGetIdxOr (Some PG_Map.unsat_node)) (coreGetChildren core)
-      | PG_Map.Rule (_,cores) -> List.map coreGetIdxOr1 cores
-      | PG_Map.Sat -> [PG_Map.sat_node]
-      | PG_Map.Unsat -> [PG_Map.unsat_node]
-    in
-    if res = [] then begin
-        Printf.printf "Empty children: ";
-        match PG_Map.find node with
-        | PG_Map.State _ -> Printf.printf "State\n"
-        | PG_Map.Core core -> Printf.printf "Core: %s\n" (coreToString core)
-        | PG_Map.Rule _ -> Printf.printf "Rule\n"
-        | PG_Map.Sat -> Printf.printf "Sat\n"
-        | PG_Map.Unsat -> Printf.printf "Unsat\n"
-      end;
-    res
+    match PG_Map.find node with
+    | PG_Map.State state -> emptyToSat (List.map fst (stateGetRulesWithIndex state))
+    | PG_Map.Core core -> List.map (stateGetIdxOr (Some PG_Map.unsat_node)) (coreGetChildren core)
+    | PG_Map.Rule (_,cores) -> List.map coreGetIdxOr1 cores
+    | PG_Map.Sat -> [PG_Map.sat_node]
+    | PG_Map.Unsat -> [PG_Map.unsat_node]
   in
   let nodeSucessors2 node =
     match PG_Map.find node with
-    | PG_Map.State state -> List.map fst (stateGetRulesWithIndex state)
+    | PG_Map.State state -> emptyToSat (List.map fst (stateGetRulesWithIndex state))
     | PG_Map.Core core -> List.map (stateGetIdxOr (Some PG_Map.sat_node)) (coreGetChildren core)
     | PG_Map.Rule (_,cores) -> List.map (coreGetIdxOr (Some PG_Map.sat_node)) cores
     | PG_Map.Sat -> [PG_Map.sat_node]