Mark deferrals bold in graphviz export

src/lib/CoAlgMisc.ml

@@ -727,6 +727,11 @@ let lfToInt lf = lf
 let lfFromInt num = num
 let lfGetFormula sort f = !arrayFormula.(sort).(f)
 
+let escapeHtml (input : string) : string =
+  List.fold_right (fun (x, y) (str : string) -> Str.global_replace (Str.regexp x) y str)
+    [("<", "&lt;") ; (">", "&gt;") ; ("&", "&amp;")]
+    input
+
 let bsetToString sort bset : string =
     let toFormula (lf:localFormula) (lst: string list) : string list =
         let formula: C.formula = lfGetFormula sort lf in
@@ -797,6 +802,13 @@ let stateToDot (state:state): string =
     | Open -> "yellow"
     | 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
+    else (escapeHtml (C.string_of_formula formula)) :: lst
+  in
+  let formulaList = bsetFold toFormula state.bsS [] in
   let ownidx = (string_of_int state.idx) in
   let parents =
     List.map (fun (co:core) ->
@@ -804,10 +816,9 @@ let stateToDot (state:state): string =
              state.parentsS
   in
   "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
-  ^ ",label=\"State "  ^ ownidx
-  ^ "\\n" ^ (Str.global_replace (Str.regexp ", ") "\\n"
-                                (bsetToString state.sortS state.bsS))
-  ^ "\"];\n"
+  ^ ",label=<State "  ^ ownidx
+  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
+  ^ ">];\n"
   ^ (String.concat "\n" parents)
 
 
@@ -818,6 +829,13 @@ let coreToDot (core:core): string =
     | 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.idx) in
   let parents =
     List.map (fun (st,_:state*int) ->
@@ -825,10 +843,9 @@ let coreToDot (core:core): string =
              core.parentsC
   in
   "Node" ^ ownidx ^ " [shape=ellipse,style=filled,fillcolor=" ^ color
-  ^ ",label=\"Core "  ^ ownidx
-  ^ "\\n" ^ (Str.global_replace (Str.regexp ", ") "\\n"
-                                (bsetToString core.sortC core.bsC))
-  ^ "\"];\n"
+  ^ ",label=<Core "  ^ ownidx
+  ^ "<BR/>" ^ (String.concat "<BR/>" formulaList)
+  ^ ">];\n"
   ^ (String.concat "\n" parents)