simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

Small modifications to colors in dot proof output

Browse source
This commit is contained in:
Guillaume Bury 2014-11-20 00:39:37 +01:00
parent 4636a94ce2
commit 8f2ae64b1a
1 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
sat/res.ml
View file

@ -329,6 +329,11 @@ module Make(St : Solver_types.S) = struct
(print_dot_edge id) (c_id p1)
(print_dot_edge id) (c_id p2)
let color s = match s.[0] with
| 'E' -> ""
| 'L' -> ""
| _ -> "BGCOLOR=\"GREY\""
let rec print_dot_proof fmt p =
if not (is_drawn p.conclusion) then begin
has_drawn p.conclusion;
@ -341,10 +346,10 @@ module Make(St : Solver_types.S) = struct
print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
| Lemma _ ->
let aux fmt () =
Format.fprintf fmt "<TR><TD colspan=\"2\" BGCOLOR=\"LIGHTBLUE\">%a</TD></TR><TR><TD>Lemma</TD><TD>%s</TD></TR>"
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"YELLOW\">Lemma</TD><TD>%s</TD></TR>"
print_clause p.conclusion St.(p.conclusion.name)
in
print_dot_rule "BGCOLOR=\"RED\"" aux () fmt p.conclusion
print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
| Resolution (proof1, proof2, a) ->
let aux fmt () =
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD>%s</TD><TD>%s</TD></TR>"
@ -354,7 +359,7 @@ module Make(St : Solver_types.S) = struct
let p1 = proof1 () in
let p2 = proof2 () in
Format.fprintf fmt "%a%a%a%a"
(print_dot_rule "" aux ()) p.conclusion
(print_dot_rule (color p.conclusion.St.name) aux ()) p.conclusion
(print_res_node p.conclusion p1.conclusion p2.conclusion) a
print_dot_proof p1
print_dot_proof p2