diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml
index 5593a28b5f20ecd4c0016332f0a3b525c0833537..a9e0bb05e4e5d45c0bfb09a9a3fa53fd734c2ca9 100644
--- a/src/debugger/debugger.ml
+++ b/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
];
}
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 7b388db94a07504bd6639e7ce1106c180a329ee3..e667e73789be9c65dfad49da3043f0b432a64464 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/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 =
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index a2531f203a9b104dcc26b6607482df2061dc1199..1e53ea105cc850408de8ac3bd1e91fcb8e2d114a 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/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
+
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index cb7912aa26afd4fd0c8c62437101ae2888b13857..023314926482d70fcf6b8a495e675f5cf587bda6 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/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 =
diff --git a/src/lib/CoAlgReasoner.mli b/src/lib/CoAlgReasoner.mli
index c96f0f943fea65da024216eae0f7b5439305e713..8070ccd301bff46ea2abf433f272672e5e12a0a3 100644
--- a/src/lib/CoAlgReasoner.mli
+++ b/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