diff --git a/_oasis b/_oasis
index b114ffaa724aa3800bb9f44d0868192324f447ff..044ad498ed1c6fea4a182af54b90b6c0c864d69c 100644
--- a/_oasis
+++ b/_oasis
@@ -150,6 +150,19 @@ Executable replexample
if flag(static)
CCLib: -static
+Executable debugger
+ CompiledObject: native
+ Path: src/debugger/
+ BuildTools: ocamlbuild
+ MainIs: debugger.ml
+ BuildDepends: interfacencurses, libcool
+ NativeOpt: -cc g++
+ ByteOpt: -cc g++
+ CCOpt: -std=c++98 -x c++
+ if flag(static)
+ CCLib: -static
+
+
# some cabal similar syntax, so steal its syntax highlighting
# vim: ft=cabal
diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml
new file mode 100644
index 0000000000000000000000000000000000000000..bc4fd5b54539a3e23dcb05edfab4db6bd741c1e7
--- /dev/null
+++ b/src/debugger/debugger.ml
@@ -0,0 +1,72 @@
+(** Accepts formulae from the standard input and tests them for satisfiability.
+ Each formula has to be on a separate line and empty lines are ignored.
+ The input is terminated by EOF.
+ @author Florian Widmann
+ *)
+
+module CM = CoAlgMisc
+module CF = CoAlgFormula
+
+module FE = FunctorParsing
+module Reasoner = CoAlgReasoner
+
+open CoolUtils
+
+(* A partial function mapping nominals to their sorts. *)
+let nomTable name =
+ assert (CoAlgFormula.isNominal name);
+ Some 0
+
+
+let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increment = 67108864; space_overhead = 120 }
+
+let printUsage () =
+ print_endline "Usage: \"debugger <functor> <formula>\" where";
+ exit 1
+
+let printResult () =
+ let str = match Reasoner.isRootSat () with
+ | None -> "Reasoning not finished yet"
+ | Some sat -> "Reasoning finished: "^(if sat then "Sat" else "Unsat")
+ in
+ print_endline str
+
+let printStatus () =
+ print_endline ("Generated states: " ^ (string_of_int (CM.graphSizeState ())));
+ print_endline ("Generated cores: " ^ (string_of_int (CM.graphSizeCore ())));
+ print_endline ("Generated constraints: " ^ (string_of_int (CM.graphSizeCnstr ())));
+ print_endline "";
+ print_endline "Queue content:";
+ print_endline (CM.queuePrettyStatus ());
+ print_endline "";
+ printResult ()
+
+let doStep args =
+ if Reasoner.reasonerFinished ()
+ then print_endline "Reasoner already finished!"
+ else try
+ Reasoner.runReasonerStep ()
+ with CoAlgMisc.CoAlg_finished _ -> printResult()
+
+
+let _ =
+ if Array.length Sys.argv < 2 then printUsage()
+ else
+ let formula = Sys.argv.(2) in
+ let sorts = (FE.sortTableFromString Sys.argv.(1)) in
+ let (tbox, f) = CoAlgFormula.importQuery formula in
+ Reasoner.initReasoner sorts nomTable tbox f;
+ let session = {
+ Repl.prompt = "> ";
+ Repl.bindings = Repl.addHelpBinding [
+ Repl.bind "s" doStep "Runs another reasoner step" "" ;
+ 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.exitBinding
+ ];
+ }
+ in
+ Repl.start session
+
+
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index de751dd00ef9c9b07878a2a840626f6a5d2f2b9a..7b388db94a07504bd6639e7ce1106c180a329ee3 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -354,6 +354,11 @@ let doSatPropagation () =
doPropagation := false;
res
+let queuePrettyStatus () =
+ (Printf.sprintf "Constraints: %d\n" (List.length !queueCnstrs))
+ ^(Printf.sprintf "States: %d\n" (List.length !queueStates))
+ ^(Printf.sprintf "Cores1: %d\n" (List.length !queueCores1))
+ ^(Printf.sprintf "Cores2: %d\n" (List.length !queueCores2))
(*****************************************************************************)
(* "Module type" and a specific implementation of the graph *)
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 3dec477383172fe2fca4a116b59dce2e6326b7d3..a2531f203a9b104dcc26b6607482df2061dc1199 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -163,6 +163,7 @@ val queueInsertState : state -> unit
val queueInsertCore : core -> unit
val queueInsertCnstr : cset -> unit
val queueGetElement : unit -> queueElement
+val queuePrettyStatus : unit -> string
val doNominalPropagation : unit -> bool
val doSatPropagation : unit -> bool
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index f0c9d1c3893d9922cb9da4ebaa1968e833c3b2c6..d13903137c0ec83377f5eacd82a3211af162b298 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -7,6 +7,8 @@ open CoAlgMisc
module M = Minisat
+module CU = CoolUtils
+
type sortTable = CoAlgMisc.sortTable
type nomTable = string -> CoAlgFormula.sort option
@@ -608,11 +610,39 @@ let rec expandNodesLoop () =
expandNodesLoop ()
| QEmpty -> ()
-let rec buildGraphLoop () =
+let runReasonerStep () =
expandNodesLoop ();
- propagateNominals ();
+ propagateNominals ()
+
+let rec buildGraphLoop () =
+ runReasonerStep ();
if queueIsEmpty () then () else buildGraphLoop ()
+
+let initReasoner sorts nomTable tbox sf =
+ sortTable := Array.copy sorts;
+ let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
+ let sort = fst sf in
+ let bs1 = bsetAddTBox sort bs in
+ graphInit ();
+ queueInit ();
+ let root = insertCore sort bs1 in
+ graphAddRoot root
+
+let isRootSat () =
+ match coreGetStatus (graphGetRoot ()) with
+ | Expandable -> None
+ | Unsat -> Some false
+ | Sat
+ | Open -> if (queueIsEmpty()) then Some true else None
+
+let reasonerFinished () =
+ match coreGetStatus (graphGetRoot ()) with
+ | Expandable -> false
+ | Unsat
+ | Sat -> true
+ | Open -> queueIsEmpty ()
+
(** A graph-tableau-based decision procedure framework for coalgebraic logics.
@param verbose An optional switch which determines
whether the procedure shall print some information on the standard output.
@@ -625,26 +655,20 @@ let rec buildGraphLoop () =
@param sf A sorted formula.
@return True if sf is satisfiable wrt tbox, false otherwise.
*)
+
let isSat ?(verbose = false) sorts nomTable tbox sf =
let start = if verbose then Unix.gettimeofday () else 0. in
- sortTable := Array.copy sorts;
- let (tbox1, sf1, bs) = ppFormulae nomTable tbox sf in
- let sort = fst sf in
- let bs1 = bsetAddTBox sort bs in
- graphInit ();
- queueInit ();
- let root = insertCore sort bs1 in
- graphAddRoot root;
+ initReasoner sorts nomTable tbox sf;
let sat =
try
buildGraphLoop ();
- match coreGetStatus (graphGetRoot ()) with
- | Expandable -> assert false
- | Unsat -> false
- | Sat
- | Open -> true
+ (* get whether the root is satisfiable *)
+ (* we know that the reasoner finished, so the value is there, *)
+ (* i.e. isRootSat() will give a "Some x" and not "None" *)
+ CU.fromSome (isRootSat())
with CoAlg_finished res -> res
in
+ (* print some statistics *)
if verbose then
let stop = Unix.gettimeofday () in
let addup lst = List.fold_left (fun acc sf -> acc + (CoAlgFormula.sizeSortedFormula sf)) 0 lst in
@@ -652,9 +676,11 @@ let isSat ?(verbose = false) sorts nomTable tbox sf =
print_endline ("Query: " ^ (CoAlgFormula.exportQuery tbox sf));
let size = (CoAlgFormula.sizeSortedFormula sf) + (addup tbox) in
print_endline ("Added Size: " ^ (string_of_int size));
+ (*
print_endline ("Negation Normal Form: " ^ (CoAlgFormula.exportQuery tbox1 sf1));
let nsize = (CoAlgFormula.sizeSortedFormula sf1) + (addup tbox1) in
print_endline ("Added Size: " ^ (string_of_int nsize));
+ *)
print_endline ("Result: Query is " ^ (if not sat then "not " else "") ^ "satisfiable.");
print_endline ("Time: " ^ (string_of_float (stop -. start)));
print_endline ("Generated states: " ^ (string_of_int (graphSizeState ())));
@@ -663,3 +689,4 @@ let isSat ?(verbose = false) sorts nomTable tbox sf =
print_newline ()
else ();
sat
+
diff --git a/src/lib/CoAlgReasoner.mli b/src/lib/CoAlgReasoner.mli
index 941f510b1717ab39ee2cf9056ac4dfcb2c6ad544..c96f0f943fea65da024216eae0f7b5439305e713 100644
--- a/src/lib/CoAlgReasoner.mli
+++ b/src/lib/CoAlgReasoner.mli
@@ -13,3 +13,11 @@ type input = sortTable * nomTable * assumptions * CoAlgFormula.sortedFormula
val isSat : ?verbose:bool -> sortTable -> (string -> CoAlgFormula.sort option) ->
CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> bool
+
+
+val initReasoner : sortTable -> (string -> CoAlgFormula.sort option) ->
+ CoAlgFormula.sortedFormula list -> CoAlgFormula.sortedFormula -> unit
+
+val runReasonerStep : unit -> unit
+val reasonerFinished : unit -> bool
+val isRootSat : unit -> bool option
diff --git a/src/lib/CoolUtils.ml b/src/lib/CoolUtils.ml
index 7b3880be8738e32e07c711e312afe03aec1d0bf4..5f06001044edd9162ba34768517b03936469c220 100644
--- a/src/lib/CoolUtils.ml
+++ b/src/lib/CoolUtils.ml
@@ -56,3 +56,8 @@ let foreach_l a f = List.iter f a
let (<<) f g x = f(g(x))
let repeat n fct = for i = 1 to n do fct () done
+exception No_value
+let fromSome optionalvalue =
+ match optionalvalue with
+ | Some x -> x
+ | None -> raise No_value
diff --git a/src/lib/CoolUtils.mli b/src/lib/CoolUtils.mli
index af5653b1bd7ee489ae0fb1fc7298c04f7aec008a..a79acee065fd1aaff76edb29575e84f942bcb84d 100644
--- a/src/lib/CoolUtils.mli
+++ b/src/lib/CoolUtils.mli
@@ -30,3 +30,6 @@ val foreach_l : ('a list) -> ('a -> unit) -> unit
val repeat : int -> (unit -> unit) -> unit
val (<<) : ('b -> 'c) -> ('a -> 'b) -> ('a -> 'c)
+exception No_value
+val fromSome : 'a option -> 'a
+