Implement lscores for debugger

src/debugger/debugger.ml

@@ -58,7 +58,11 @@ let doStep args =
                 | (str::_) -> (int_of_string str)
                 | [] -> 1
     in
-    repeat steps action
+    try repeat steps action
+    with Reasoner.ReasonerError str -> print_endline ("Error: "^str)
+
+let listCores args =
+    CM.graphIterCores (fun core -> print_endline (CM.coreToString core))
 
 let _ =
   if Array.length Sys.argv < 2 then printUsage()
@@ -76,6 +80,7 @@ let _ =
         Repl.bind "step" doStep "Runs another reasoner step" "" ;
         Repl.bind "st" (fun _ -> printStatus ()) "Prints reasoning status" "";
         Repl.bind "status" (fun _ -> printStatus ()) "Prints reasoning status" "";
+        Repl.bind "lscores" listCores "Lists all cores" "";
         Repl.exitBinding
       ];
     }

src/lib/CoAlgMisc.ml

@@ -223,6 +223,12 @@ and 'a lazylist = unit -> 'a lazyliststep
 
 and ruleEnumeration = rule lazyliststep
 
+let nodeStatusToString : nodeStatus -> string = function
+  | Expandable -> "Expandable"
+  | Open -> "Open"
+  | Sat -> "Sat"
+  | Unsat -> "Unsat"
+
 let lazylistFromList a_list =
     let list_state = ref (Some a_list) in
     fun () -> begin match !list_state with
@@ -454,6 +460,8 @@ let cssAdd cset css = BsSet.add cset css
 let cssFold fkt css init = BsSet.fold fkt css init
 let cssSingleton cset = BsSet.singleton cset
 let cssEqual css1 css2 = BsSet.equal css1 css2
+let cssIter (action: cset -> unit) css =
+    BsSet.iter action css
 
 
 (*****************************************************************************)
@@ -648,6 +656,29 @@ let lfGetAt (sort, nom) f =
   FHt.find !arrayAt.(sort).(f) nom
 let lfToInt lf = lf
 let lfFromInt num = num
+let lfGetFormula sort f = !arrayFormula.(sort).(f)
+
+let bsetToString sort bset : string =
+    let toFormula (lf:localFormula) (lst: string list) : string list =
+        let formula: C.formula = lfGetFormula sort lf in
+        (C.string_of_formula formula) :: lst
+    in
+    let formulaList = bsetFold toFormula bset [] in
+    "{ "^(String.concat ", " formulaList)^" }"
+
+let csetToString sort cset = bsetToString sort cset
+
+let coreToString core =
+    let helper cset lst : string list =
+        (csetToString core.sortC cset):: lst
+    in
+    let constraints = cssFold helper core.constraintsC [] in
+    "Core {\n"^
+    "  Status: " ^ (nodeStatusToString core.statusC) ^ "\n"^
+    "  " ^ bsetToString core.sortC core.bsC ^ "\n" ^
+    "  Constraints: { "^(String.concat "\n                 " constraints)^" }\n"^
+    "}"
+    
 
 let atFormulaGetSubformula f = !arrayDest1.(0).(f)
 let atFormulaGetNominal f =

src/lib/CoAlgMisc.mli

@@ -204,7 +204,7 @@ val cssAdd : cset -> csetSet -> csetSet
 val cssFold : (cset -> 'a -> 'a) -> csetSet -> 'a -> 'a
 val cssSingleton : cset -> csetSet
 val cssEqual : csetSet -> csetSet -> bool
-
+val cssIter : (cset -> unit) -> csetSet -> unit
 
 (*****************************************************************************)
 (*      "Module type" and a specific implementation of state nodes           *)
@@ -246,6 +246,7 @@ val coreGetSolver : core -> Minisat.solver
 val coreGetFht : core -> fht
 val coreGetConstraintParents : core -> cset list
 val coreAddConstraintParent : core -> cset -> unit
+val coreToString : core -> string
 
 
 (*****************************************************************************)
@@ -304,6 +305,7 @@ val bsetIter : (localFormula -> unit) -> bset -> unit
 val bsetFilter : bset -> (localFormula -> bool) -> bset
 val bsetAddTBox : sort -> bset -> bset
 val bsetCopy : bset -> bset
+val bsetToString : sort -> bset -> string
 
 val csetMake : unit -> cset
 val csetAdd : cset -> atFormula -> unit
@@ -314,6 +316,7 @@ val csetAddDot : cset -> unit
 val csetRemDot : cset -> unit
 val csetAddTBox : sort -> cset -> bset
 val csetIter : cset -> (atFormula -> unit) -> unit
+val csetToString : sort -> cset -> string
 
 
 (*****************************************************************************)
@@ -332,6 +335,7 @@ val lfGetNeg : sort -> localFormula -> localFormula option
 val lfGetAt : nominal -> localFormula -> atFormula
 val lfToInt : localFormula -> int
 val lfFromInt : int -> localFormula
+val lfGetFormula : sort -> localFormula -> CoAlgFormula.formula
 
 val atFormulaGetSubformula : atFormula -> localFormula
 val atFormulaGetNominal : atFormula -> nominal
@@ -340,3 +344,4 @@ val lfToAt : sort -> localFormula -> atFormula
 
 val ppFormulae : (string -> sort option) -> CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula ->
     CoAlgFormula.sortedFormula list * CoAlgFormula.sortedFormula * bset
+

src/lib/CoAlgReasoner.ml

@@ -17,6 +17,7 @@ type assumptions = CoAlgFormula.sortedFormula list
 
 type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
 
+exception ReasonerError of string
 
 (*****************************************************************************)
 (*                     Propagation of Satisfiability                         *)
@@ -26,7 +27,7 @@ let propSatFindSucc setCnstr cset =
   if csetHasDot cset then false
   else
     match graphFindCnstr cset with
-      | None -> assert false
+      | None -> raise (ReasonerError "?")
       | Some SatC -> true
       | Some (OpenC _) -> setMemCnstr setCnstr cset
       | Some (UnexpandedC _)
@@ -139,7 +140,7 @@ let rec propagateUnsat = function
         | UState (state, idxopt) -> begin
             match stateGetStatus state with
             | Unsat -> tl
-            | Sat -> assert false
+            | Sat -> raise (ReasonerError "Propagation tells node is unsat, but it is already sat")
             | Open
             | Expandable ->
                 let mbs =
@@ -170,7 +171,7 @@ let rec propagateUnsat = function
         | UCore (core, comesFromCnstr) -> begin
             match coreGetStatus core with
             | Unsat -> tl
-            | Sat -> assert false
+            | Sat -> raise (ReasonerError "Propagation tells node is unsat, but it is already sat")
             | Open
             | Expandable ->
                 let mbs =

src/lib/CoAlgReasoner.mli

@@ -11,6 +11,8 @@ type assumptions = CoAlgFormula.sortedFormula list
 
 type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
 
+exception ReasonerError of string
+
 val isSat : ?verbose:bool -> sortTable -> (string -> CoAlgFormula.sort option) ->
   CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool