diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index c2180eedc9b2e5ba7dedb5882bf5876888c1ba8f..76e4123ff4d67676db68368d8b34fa7ccebcafdb 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -187,10 +187,7 @@ let choiceNNF () =
let choiceGraph () =
choiceSat ();
- print_endline "digraph reasonerstate {";
- CM.graphIterCores (fun core -> print_endline (CM.coreToDot core));
- CM.graphIterStates (fun state -> print_endline (CM.stateToDot state));
- print_endline "}"
+ print_endline (CM.graphToDot ())
let choiceVerify () =
try
diff --git a/src/debugger/debugger.ml b/src/debugger/debugger.ml
index b2366bdeb2f791fe76cabc46531e98b509a88af8..a1a1aaab311b4e3e8b45204f2fb933d6f34c291f 100644
--- a/src/debugger/debugger.ml
+++ b/src/debugger/debugger.ml
@@ -72,10 +72,11 @@ let listStates args =
CM.graphIterStates (fun state -> print_endline (CM.stateToString state))
let exportGraph args =
- print_endline "digraph reasonerstate {";
- CM.graphIterCores (fun core -> print_endline (CM.coreToDot core));
- CM.graphIterStates (fun state -> print_endline (CM.stateToDot state));
- print_endline "}"
+ let out = match args with
+ | (filename::_) -> open_out filename
+ | _ -> stdout
+ in
+ Printf.fprintf out "%s" (CM.graphToDot ())
let showNode = function
| (n::_) ->
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 667d3a6be3d99c1a63af65449f1ead212f2423c2..6d20a7ac4da9096ac1e9d3c49ccc5930e2c457eb 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -811,59 +811,58 @@ let stateToString (state:state): string =
" Parents: { "^(String.concat ", " parents)^" }\n"^
"}"
-let stateToDot (state:state): string =
- let color = match state.statusS with
- | Sat -> "green"
- | Unsat -> "red"
- | Open -> "yellow"
+let nodeToDot idx typ sort formulas deferrals status parentIdxs : string =
+ let color = match status with
+ | Sat -> "#8ae234"
+ | Unsat -> "#ef2929"
+ | Open -> "#729fcf"
| Expandable -> "white"
in
let toFormula (lf:localFormula) (lst: string list) : string list =
- let formula: C.formula = lfGetFormula state.sortS lf in
- if (bsetMem state.deferralS lf)
- then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
+ let formula: C.formula = lfGetFormula sort lf in
+ if (bsetMem deferrals lf)
+ then ("<U>"^(escapeHtml (C.string_of_formula formula))^"</U>") :: lst
else (escapeHtml (C.string_of_formula formula)) :: lst
in
- let formulaList = bsetFold toFormula state.bsS [] in
- let ownidx = (string_of_int state.idxS) in
+ let formulaList = bsetFold toFormula formulas [] in
+ let ownidx = (string_of_int idx) in
let parents =
- List.map (fun (co:core) ->
- "Node"^string_of_int co.idxC^" -> Node"^ownidx^";")
- state.parentsS
+ List.map (fun (parentIdx) ->
+ "Node"^string_of_int parentIdx^" -> Node"^ownidx^";")
+ parentIdxs
in
- "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
- ^ ",label=<State " ^ ownidx
- ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
+ let style = if typ = "Core" then "filled,rounded" else "filled" in
+ "Node" ^ ownidx ^ " [shape=box,style=\"" ^ style
+ ^ "\",fillcolor=\"" ^ color ^ "\""
+ ^ ",label=<<B>" ^ typ ^ " " ^ ownidx ^ "</B>"
+ ^ "<BR/><BR/>" ^ (String.concat "<BR/>" formulaList)
^ ">];\n"
^ (String.concat "\n" parents)
+let stateToDot (state:state): string =
+ nodeToDot state.idxS "State" state.sortS state.bsS state.deferralS
+ state.statusS (List.map (fun c -> c.idxC) state.parentsS)
let coreToDot (core:core): string =
- let color = match core.statusC with
- | Sat -> "green"
- | Unsat -> "red"
- | Open -> "yellow"
- | Expandable -> "white"
- in
- let toFormula (lf:localFormula) (lst: string list) : string list =
- let formula: C.formula = lfGetFormula core.sortC lf in
- if (bsetMem core.deferralC lf)
- then ("<B>"^(escapeHtml (C.string_of_formula formula))^"</B>") :: lst
- else (escapeHtml (C.string_of_formula formula)) :: lst
- in
- let formulaList = bsetFold toFormula core.bsC [] in
- let ownidx = (string_of_int core.idxC) in
- let parents =
- List.map (fun (st,_:state*int) ->
- "Node"^string_of_int st.idxS^" -> Node"^ownidx^";")
- core.parentsC
- in
- "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
- ^ ",label=<Core " ^ ownidx
- ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
- ^ ">];\n"
- ^ (String.concat "\n" parents)
-
+ nodeToDot core.idxC "Core" core.sortC core.bsC core.deferralC
+ core.statusC (List.map (fun (s,_) -> s.idxS) core.parentsC)
+
+let graphToDot () : string =
+ let lines = ref ["digraph reasonerstate {"] in
+ graphIterCores (fun core -> lines := (coreToDot core)::!lines);
+ graphIterStates (fun state -> lines := (stateToDot state)::!lines);
+
+ let legend =
+ "subgraph legend {\n"
+ ^ "key [label=<<TABLE CELLBORDER=\"0\" BGCOLOR=\"#d3d7cf\">\n"
+ ^ "<TR><TD>Color:</TD><TD BGCOLOR=\"#8ae234\">sat</TD><TD BGCOLOR=\"#ef2929\">unsat</TD><TD BGCOLOR=\"#729fcf\">open</TD><TD BGCOLOR=\"white\">expandable</TD></TR>"
+ ^ "<TR><TD>Rounded:</TD><TD>cores</TD></TR>"
+ ^ "<TR><TD>Boxed:</TD><TD>states</TD></TR>"
+ ^ "<TR><TD>Underlined:</TD><TD>focus</TD></TR>"
+ ^ "</TABLE>>, shape=none];}" in
+
+ lines := "}"::legend::!lines;
+ String.concat "\n" (List.rev !lines)
let queuePrettyStatus () =
let printList (sl : int list) : string =
diff --git a/src/lib/CoAlgMisc.mli b/src/lib/CoAlgMisc.mli
index 3187932aabb83dfcc9cd143a713e04fb44ba496a..b38722f508fda56701adccfe04381727a07918f0 100644
--- a/src/lib/CoAlgMisc.mli
+++ b/src/lib/CoAlgMisc.mli
@@ -195,6 +195,9 @@ val graphSizeCnstr : unit -> int
val graphAddRoot : core -> unit
val graphGetRoot : unit -> core
+(** Generate a graphviz dot description of the current reasoner graph *)
+val graphToDot : unit -> string
+
(*****************************************************************************)
(* "Module type" and a specific implementation of sets of constraints *)
@@ -231,7 +234,6 @@ val stateGetConstraints : state -> csetSet
val stateSetConstraints : state -> csetSet -> unit
val stateNextRule : state -> ruleEnumeration
val stateToString : state -> string
-val stateToDot : state -> string
val stateGetIdx : state -> int
@@ -264,7 +266,6 @@ val coreGetIdx : core -> int
val coreGetConstraintParents : core -> cset list
val coreAddConstraintParent : core -> cset -> unit
val coreToString : core -> string
-val coreToDot : core -> string
(*****************************************************************************)