simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-07 19:55:41 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(dot): proper labelling of hyper-res nodes

Browse source
This commit is contained in:
Simon Cruanes 2019-02-16 12:33:43 -06:00 • committed by Guillaume Bury
parent cdb52ee757
commit 596034d16a
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/backend/Dot.ml
View file

@ -79,11 +79,12 @@ module Make(S : Msat.S)(A : Arg with type atom := S.atom
let print_edges fmt n =
match P.(n.step) with
| P.Hyper_res {P.hr_init; hr_steps} ->
print_edge fmt (res_np_id n hr_init) (proof_id hr_init);
| P.Hyper_res {P.hr_steps=[];_} -> () (* NOTE: should never happen *)
| P.Hyper_res {P.hr_init; hr_steps=((_,p0)::_) as l} ->
print_edge fmt (res_np_id n p0) (proof_id hr_init);
List.iter
(fun (_,p2) -> print_edge fmt (res_np_id n p2) (proof_id p2))
hr_steps;
l;
| _ -> ()
let table_options fmt color =
@ -130,15 +131,14 @@ module Make(S : Msat.S)(A : Arg with type atom := S.atom
((fun fmt () -> (Format.fprintf fmt "%s" (node_id n))) ::
List.map (ttify A.print_atom) l);
print_edge fmt (node_id n) (node_id (P.expand p))
| P.Hyper_res {P.hr_init; hr_steps} ->
| P.Hyper_res {P.hr_steps=l; _} ->
print_dot_node fmt (node_id n) "GREY" P.(n.conclusion) "Resolution" "GREY"
[(fun fmt () -> (Format.fprintf fmt "%s" (node_id n)))];
print_edge fmt (node_id n) (res_np_id n hr_init);
List.iter
(fun (a,p2) ->
print_dot_res_node fmt (res_np_id n p2) a;
print_edge fmt (node_id n) (res_np_id n p2))
hr_steps
l
let print_node fmt n =
print_contents fmt n;