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

Fix for empty arguments lemma printing in dot proofs

Browse source
This commit is contained in:
Guillaume Bury 2015-02-06 14:33:35 +01:00
parent 5067274b4c
commit 0d66605afd
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
solver/mcproof.ml
View file

@ -351,14 +351,16 @@ module Make(St : Mcsolver_types.S) = struct
let color = match color with None -> "YELLOW" | Some c -> c in
let aux fmt () =
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD>"
print_clause p.conclusion color (List.length f_args + List.length t_args) name;
print_clause p.conclusion color (min (List.length f_args + List.length t_args) 1) name;
if f_args <> [] then
Format.fprintf fmt "<TD>%a</TD></TR>%a%a" St.print_atom (List.hd f_args)
(fun fmt -> List.iter (fun a -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_atom a)) (List.tl f_args)
(fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_semantic_var v)) t_args
else
else if t_args <> [] then
Format.fprintf fmt "<TD>%a</TD></TR>%a" St.print_semantic_var (List.hd t_args)
(fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TR><TD>%a</TD></TR>" St.print_semantic_var v)) (List.tl t_args)
else
Format.fprintf fmt "<TD></TD></TR>"
in
print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
| Resolution (proof1, proof2, a) ->