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

Update for proof output in dot

Browse source
This commit is contained in:
Guillaume Bury 2015-01-29 15:00:52 +01:00
parent 676ed7eed9
commit 863a49a0a4
5 changed files with 10 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
smt/mcsat.ml
View file

@ -18,7 +18,7 @@ module Tsmt = struct
type proof = unit
let proof_debug () =
"Proof", ["..."], Some "PURPLE"
"Proof", [], ["..."], Some "PURPLE"
type assumption =
| Lit of formula

10
solver/mcproof.ml
View file

@ -347,13 +347,13 @@ module Make(St : Mcsolver_types.S) = struct
in
print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
| Lemma proof ->
let name, args, color = St.proof_debug proof in
assert (args <> []);
let name, f_args, t_args, color = St.proof_debug proof in
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>%a</TR>"
print_clause p.conclusion color (List.length args) name
(fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TD>%a</TD>" St.print_semantic_var v)) args
Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR><TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD>%a%a</TR>"
print_clause p.conclusion color (List.length f_args + List.length t_args) name
(fun fmt -> List.iter (fun a -> Format.fprintf fmt "<TD>%a</TD>" St.print_atom a)) f_args
(fun fmt -> List.iter (fun v -> Format.fprintf fmt "<TD>%a</TD>" St.print_semantic_var v)) t_args
in
print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
| Resolution (proof1, proof2, a) ->

4
solver/mcsolver_types.ml
View file

@ -214,8 +214,8 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
(* Proof debug info *)
let proof_debug p =
let name, l, color = Th.proof_debug p in
name, (List.map add_term l), color
let name, l, l', color = Th.proof_debug p in
name, (List.map add_atom l), (List.map add_term l'), color
(* Pretty printing for atoms and clauses *)
let print_semantic_var fmt v = E.Term.print fmt v.tag.term

2
solver/mcsolver_types_intf.ml
View file

@ -96,7 +96,7 @@ module type S = sig
val fresh_dname : unit -> string
(** Fresh names for clauses *)
val proof_debug : proof -> string * (semantic var list) * (string option)
val proof_debug : proof -> string * (atom list) * (semantic var list) * (string option)
(** Debugging info for proofs (see Plugin_intf). *)
val print_atom : Format.formatter -> atom -> unit

2
solver/plugin_intf.ml
View file

@ -78,7 +78,7 @@ module type S = sig
val eval : formula -> eval_res
(** Returns the evaluation of the formula in the current assignment *)
val proof_debug : proof -> string * (term list) * (string option)
val proof_debug : proof -> string * (formula list) * (term list) * (string option)
(** Returns debugging information on a proof, as a triplet consisting of
a name/identification string associated with the proof, arguments of the proof,
and an optional color for the proof background *)