Better proof output for dot format

smt/mcsat.ml

@@ -17,6 +17,9 @@ module Tsmt = struct
 
   type proof = unit
 
+  let proof_debug () =
+      "Proof", ["..."], Some "PURPLE"
+
   type assumption =
     | Lit of formula
     | Assign of term * term

solver/mcproof.ml

@@ -346,10 +346,14 @@ module Make(St : Mcsolver_types.S) = struct
             print_clause p.conclusion St.(p.conclusion.name)
         in
         print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
-      | Lemma _ ->
+      | Lemma proof ->
+        let name, args, color = St.proof_debug proof in
+        assert (args <> []);
+        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=\"YELLOW\">Lemma</TD><TD>%s</TD></TR>"
-            print_clause p.conclusion St.(p.conclusion.name)
+          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
         in
         print_dot_rule "BGCOLOR=\"LIGHTBLUE\"" aux () fmt p.conclusion
       | Resolution (proof1, proof2, a) ->

solver/mcsolver_types.ml

@@ -212,6 +212,11 @@ module Make (E : Expr_intf.S)(Th : Plugin_intf.S with
           iter_map := Mi.add v.vid !l !iter_map;
           List.iter f !l
 
+  (* Proof debug info *)
+  let proof_debug p =
+      let name, l, color = Th.proof_debug p in
+      name, (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
 

solver/mcsolver_types_intf.ml

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

solver/plugin_intf.ml

@@ -78,5 +78,10 @@ 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)
+  (** 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 *)
+
 end