Dot output is now available through independent backend

backend/backend_intf.ml

@@ -0,0 +1,15 @@
+
+module type Arg = sig
+  type proof
+  type formula
+  val prove : Format.formatter -> formula list -> unit
+  val context : Format.formatter -> proof -> unit
+  val translate : Format.formatter -> formula -> unit
+end
+
+module type S = sig
+  type t
+  val print : Format.formatter -> t -> unit
+end
+
+

backend/dedukti.ml

@@ -0,0 +1,30 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2014 Guillaume Bury
+Copyright 2014 Simon Cruanes
+*)
+
+module type S = Backend_intf.S
+
+module Make(S : Res.S)(A : Backend_intf.Arg with type formula := S.atom and type proof := S.proof) = struct
+
+  let print_aux fmt = Format.fprintf fmt "@\n"
+
+  let fprintf fmt format = Format.kfprintf print_aux fmt format
+
+  let context fmt () =
+    fprintf fmt "(; Embedding ;)";
+    fprintf fmt "Prop : Type.";
+    fprintf fmt "_proof : Prop -> Type.";
+    fprintf fmt "(; Notations for clauses ;)";
+    fprintf fmt "_pos : Prop -> Prop -> Type.";
+    fprintf fmt "_neg : Prop -> Prop -> Type.";
+    fprintf fmt "[b: Prop, p: Prop] _pos b p --> _proof p -> _proof b.";
+    fprintf fmt "[b: Prop, p: Prop] _neg b p --> _pos b p -> _proof b."
+
+  let print fmt _ =
+    context fmt ();
+    ()
+
+end
+

backend/dedukti.mli

@@ -0,0 +1,8 @@
+
+module type S = Backend_intf.S
+
+module Make :
+  functor(S : Res.S) ->
+  functor(A : Backend_intf.Arg with type formula := S.atom and type proof := S.proof) ->
+    S with type t := S.proof
+(** Functor to generate a backend to output proofs for the dedukti type checker. *)

backend/dot.ml

@@ -0,0 +1,79 @@
+
+module type S = Backend_intf.S
+
+module Make
+    (St : Solver_types.S)
+    (S : Res.S with type clause = St.clause
+                and type lemma = St.proof
+                and type atom = St.atom) = struct
+
+  let clause_id c = St.(c.name)
+
+  let node_id n = clause_id S.(n.conclusion)
+
+  let res_node_id n = (node_id n) ^ "_res"
+
+  let proof_id p = node_id (S.expand p)
+
+  let print_edge fmt i j =
+    Format.fprintf fmt "%s -> %s;@\n" i j
+
+  let print_edges fmt n =
+    match S.(n.step) with
+    | S.Resolution (p1, p2, _) ->
+      print_edge fmt (res_node_id n) (proof_id p1);
+      print_edge fmt (res_node_id n) (proof_id p2)
+    | _ -> ()
+
+  let table_options fmt color =
+    Format.fprintf fmt "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\" BGCOLOR=\"%s\"" color
+
+  let table fmt (c, rule, color, l) =
+    Format.fprintf fmt "<TR><TD colspan=\"2\">%a</TD></TR>" S.print_clause c;
+    match l with
+    | [] ->
+      Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" colspan=\"2\">%s</TD></TR>" color rule
+    | f :: r ->
+      Format.fprintf fmt "<TR><TD BGCOLOR=\"%s\" rowspan=\"%d\">%s</TD><TD>%a</TD></TR>"
+        color (List.length l) rule f ();
+      List.iter (fun f -> Format.fprintf fmt "<TR><TD></TD><TD>%a</TD></TR>" f ()) r
+
+  let print_dot_node fmt id color c rule rule_color l =
+    Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %a>%a</TABLE>>];@\n"
+      id table_options color table (c, rule, rule_color, l)
+
+  let print_dot_res_node fmt id a =
+    Format.fprintf fmt "%s [label=\"%a\"];@\n" id St.print_atom a
+
+  let ttify f c = fun fmt () -> f fmt c
+
+  let print_contents fmt n =
+    match S.(n.step) with
+    | S.Hypothesis ->
+      print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) "Hypothesis" "LIGHTBLUE"
+        [(fun fmt () -> (Format.fprintf fmt "%s" n.S.conclusion.St.name))];
+    | S.Lemma lemma ->
+      let rule, f_args, t_args, color = St.proof_debug lemma in
+      let color = match color with None -> "YELLOW" | Some c -> c in
+      let l = List.map (ttify St.print_atom) f_args @
+              List.map (ttify St.print_lit) t_args in
+      print_dot_node fmt (node_id n) "LIGHTBLUE" S.(n.conclusion) rule color l
+    | S.Resolution (_, _, a) ->
+      print_dot_node fmt (node_id n) "GREY" S.(n.conclusion) "Resolution" "GREY"
+        [(fun fmt () -> (Format.fprintf fmt "%s" n.S.conclusion.St.name))];
+      print_dot_res_node fmt (res_node_id n) a;
+      print_edge fmt (node_id n) (res_node_id n)
+
+  let print_node fmt n =
+    print_contents fmt n;
+    print_edges fmt n
+
+  let print fmt p =
+    Format.fprintf fmt "digraph proof {@\n";
+    S.fold (fun () -> print_node fmt) () p;
+    Format.fprintf fmt "}@."
+
+end
+
+
+

msat.mlpack

@@ -17,6 +17,7 @@ Mcsolver
 Solver_types
 
 # Backends
+Dot
 Dedukti
 
 # Auxiliary modules

sat/sat.ml

@@ -88,7 +88,9 @@ module Tsat = struct
 end
 
 module Make(Log : Log_intf.S) = struct
+
   module SatSolver = Solver.Make(Log)(Fsat)(Tsat)
+  module Dot = Dot.Make(SatSolver.St)(SatSolver.Proof)
 
   exception Bad_atom
 
@@ -150,6 +152,6 @@ module Make(Log : Log_intf.S) = struct
 
   let print_atom = Fsat.print
   let print_clause = SatSolver.St.print_clause
-  let print_proof = SatSolver.Proof.print_dot
+  let print_proof = Dot.print
 
 end

smt/.merlin

@@ -1,10 +0,0 @@
-S ./
-S ../sat/
-S ../util/
-S ../solver/
-
-B ../_build/
-B ../_build/sat/
-B ../_build/smt/
-B ../_build/util/
-B ../_build/solver/

smt/mcsat.ml

@@ -113,7 +113,9 @@ module Tsmt = struct
 end
 
 module Make(Dummy:sig end) = struct
+
   module SmtSolver = Mcsolver.Make(Log)(Fsmt)(Tsmt)
+  module Dot = Dot.Make(SmtSolver.St)(SmtSolver.Proof)
 
   type atom = Fsmt.t
   type clause = SmtSolver.St.clause
@@ -146,5 +148,5 @@ module Make(Dummy:sig end) = struct
 
   let print_atom = Fsmt.print
   let print_clause = SmtSolver.St.print_clause
-  let print_proof = SmtSolver.Proof.print_dot
+  let print_proof = Dot.print
 end

smt/smt.ml

@@ -59,7 +59,9 @@ module Tsmt = struct
 end
 
 module Make(Dummy:sig end) = struct
+
   module SmtSolver = Solver.Make(Log)(Fsmt)(Tsmt)
+  module Dot = Dot.Make(SmtSolver.St)(SmtSolver.Proof)
 
   type atom = Fsmt.t
   type clause = SmtSolver.St.clause
@@ -91,5 +93,5 @@ module Make(Dummy:sig end) = struct
 
   let print_atom = Fsmt.print
   let print_clause = SmtSolver.St.print_clause
-  let print_proof = SmtSolver.Proof.print_dot
+  let print_proof = Dot.print
 end

solver/.merlin

@@ -1,6 +0,0 @@
-S ./
-S ../util/
-
-B ../_build/
-B ../_build/solver/
-B ../_build/util/

solver/internal.ml

@@ -521,10 +521,9 @@ module Make (L : Log_intf.S)(St : Solver_types.S)
       | [] ->
         report_unsat init0;
       | a::b::_ ->
-        let name = fresh_name () in
         let clause =
           if init then init0
-          else make_clause ?tag name atoms size true (History [init0])
+          else make_clause ?tag (fresh_name ()) atoms size true (History [init0])
         in
         L.debug 1 "New clause : %a" St.pp_clause clause;
         attach_clause clause;

solver/mcsolver.mli

@@ -13,6 +13,7 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
   module St : Solver_types.S
     with type term = E.Term.t
      and type formula = E.Formula.t
+     and type proof = Th.proof
 
   module Proof : Res.S
     with type atom = St.atom

solver/res.ml

@@ -91,6 +91,8 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
       L.debug 3 "Input clause is a tautology";
     res
 
+  let print_clause fmt c = print_cl fmt (to_list c)
+
   (* Adding hyptoheses *)
   let has_been_proved c = H.mem proof (to_list c)
 
@@ -225,7 +227,6 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
     | Resolution of proof * proof * atom
 
   let expand (c, cl) =
-    L.debug 8 "Returning proof for : %a" St.pp_clause c;
     let st = match H.find proof cl with
       | Assumption -> Hypothesis
       | Lemma l -> Lemma l
@@ -261,6 +262,38 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
     in
     sort_uniq compare_cl (aux [] proof)
 
+  (* Iter on proofs *)
+  type task =
+    | Enter of proof
+    | Leaving of proof
+
+  let pop s = try Some (Stack.pop s) with Stack.Empty -> None
+
+  let rec fold_aux s h f acc =
+    match pop s with
+    | None -> acc
+    | Some (Leaving ((_, cl) as p)) ->
+      H.add h cl true;
+      fold_aux s h f (f acc (expand p))
+    | Some (Enter ((_, cl) as p)) ->
+      if not (H.mem h cl) then begin
+        Stack.push (Leaving p) s;
+        let node = expand p in
+        begin match node.step with
+        | Resolution (p1, p2, _) ->
+          Stack.push (Enter p2) s;
+          Stack.push (Enter p1) s
+        | _ -> ()
+        end
+      end;
+      fold_aux s h f acc
+
+  let fold f acc p =
+    let h = H.create 42 in
+    let s = Stack.create () in
+    Stack.push (Enter p) s;
+    fold_aux s h f acc
+
   (* Dot proof printing *)
   module Dot = struct
     let _i = ref 0
@@ -289,10 +322,6 @@ module Make(L : Log_intf.S)(St : Solver_types.S) = struct
       else
         ()
 
-    (* We use a custom function instead of the functions in Solver_type,
-       so that atoms are sorted before printing. *)
-    let print_clause fmt c = print_cl fmt (to_list c)
-
     let print_dot_rule opt f arg fmt cl =
       Format.fprintf fmt "%s [shape=plaintext, label=<<TABLE %s %s>%a</TABLE>>];@\n"
         (c_id cl) "BORDER=\"0\" CELLBORDER=\"1\" CELLSPACING=\"0\"" opt f arg

solver/res_intf.ml

@@ -72,13 +72,20 @@ module type S = sig
   val expand : proof -> proof_node
   (** Return the proof step at the root of a given proof. *)
 
+  val fold : ('a -> proof_node -> 'a) -> 'a -> proof -> 'a
+  (** [fold f acc p], fold [f] over the proof [p] and all its node. It is guaranteed that
+      [f] is executed exactly once on each proof ndoe in the tree, and that the execution of
+      [f] on a proof node happens after the execution on the children of the nodes. *)
+
   val unsat_core : proof -> clause list
   (** Returns the unsat_core of the given proof, i.e the lists of conclusions of all leafs of the proof. *)
 
   val print_dot : Format.formatter -> proof -> unit
   (** Print the given proof in dot format on the given formatter.
-      @deprecated *)
+      @deprecated use the Dot backend module instead. *)
 
-  module Dot : Backend_intf.S with type t := proof
+  (** {3 Misc} *)
+  val print_clause : Format.formatter -> clause -> unit
+  (** A nice looking printer for clauses, which sort the atoms before printing. *)
 
 end

solver/solver.mli

@@ -20,6 +20,7 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
 
   module St : Solver_types.S
     with type formula = F.t
+     and type proof = Th.proof
 
   module Proof : Res.S
     with type atom = St.atom

solver/solver_types.ml

@@ -259,11 +259,15 @@ module McMake (L : Log_intf.S)(E : Expr_intf.S)(Th : Plugin_intf.S with
   let print_atom fmt a = E.Formula.print fmt a.lit
 
   let print_atoms fmt v =
-    print_atom fmt (Vec.get v 0);
-    if (Vec.size v) > 1 then begin
-      for i = 1 to (Vec.size v) - 1 do
-        Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i)
-      done
+    if Vec.size v = 0 then
+      Format.fprintf fmt "∅"
+    else begin
+      print_atom fmt (Vec.get v 0);
+      if (Vec.size v) > 1 then begin
+        for i = 1 to (Vec.size v) - 1 do
+          Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i)
+        done
+      end
     end
 
   let print_clause fmt c =
@@ -518,7 +522,7 @@ module SatMake (L : Log_intf.S)(E : Formula_intf.S)
   let iter_sub _ _ = ()
 
   (* Proof debug info *)
-  let proof_debug _ = assert false
+  let proof_debug _ = "lemma", [], [], None
 
   (* Pretty printing for atoms and clauses *)
   let print_lit _ _ = assert false
@@ -526,11 +530,15 @@ module SatMake (L : Log_intf.S)(E : Formula_intf.S)
   let print_atom fmt a = E.print fmt a.lit
 
   let print_atoms fmt v =
-    print_atom fmt (Vec.get v 0);
-    if (Vec.size v) > 1 then begin
-      for i = 1 to (Vec.size v) - 1 do
-        Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i)
-      done
+    if Vec.size v = 0 then
+      Format.fprintf fmt "∅"
+    else begin
+      print_atom fmt (Vec.get v 0);
+      if (Vec.size v) > 1 then begin
+        for i = 1 to (Vec.size v) - 1 do
+          Format.fprintf fmt " ∨ %a" print_atom (Vec.get v i)
+        done
+      end
     end
 
   let print_clause fmt c =

solver/solver_types_intf.ml

@@ -16,7 +16,6 @@ module type S = sig
 
   val mcsat : bool
 
-
   (** {2 Type definitions} *)
 
   type term