Added Coq backend (not tested yet)

src/backend/coq.ml

@@ -0,0 +1,173 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2015 Guillaume Bury
+*)
+
+module type S = Backend_intf.S
+
+module type Arg = sig
+
+  type atom
+
+  type hyp
+  type lemma
+  type assumption
+
+  val print_atom : Format.formatter -> atom -> unit
+
+  val prove_hyp : Format.formatter -> string -> hyp -> unit
+  val prove_lemma : Format.formatter -> string -> lemma -> unit
+  val prove_assumption : Format.formatter -> string -> assumption -> unit
+
+end
+
+module Make(S : Res.S)(A : Arg with type atom := S.atom
+                                and type hyp := S.clause
+                                and type lemma := S.clause
+                                and type assumption := S.clause) = struct
+
+  module M = Map.Make(struct
+      type t = S.St.atom
+      let compare a b = compare a.S.St.aid b.S.St.aid
+    end)
+
+  let name c = c.S.St.name
+
+  let pp_atom fmt a =
+    if a == S.St.(a.var.pa) then
+      Format.fprintf fmt "~ %a" A.print_atom a
+    else
+      Format.fprintf fmt "~ ~ %a" A.print_atom a.S.St.neg
+
+  let pp_clause fmt c =
+    let rec aux fmt (a, i) =
+      if i < Array.length a then
+        Format.fprintf fmt "@[<h>%a ->@ @]%a"
+          pp_atom a.(i) aux (a, i + 1)
+      else
+        Format.fprintf fmt "False"
+    in
+    Format.fprintf fmt "@[<hov 1>(%a)@]" aux (c.S.St.atoms, 0)
+
+  let pp_clause_intro fmt c =
+    let rec aux fmt acc a i =
+      if i >= Array.length a then acc
+      else begin
+        let name = Format.sprintf "A%d" i in
+        Format.fprintf fmt "%s@ " name;
+        aux fmt (M.add a.(i) name acc) a (i + 1)
+      end
+    in
+    Format.fprintf fmt "intros @[<hov>";
+    let m = aux fmt M.empty c.S.St.atoms 0 in
+    Format.fprintf fmt "@].@\n";
+    m
+
+  let clausify 
+
+  let elim_duplicate fmt goal hyp _ =
+    (** Printing info comment in coq *)
+    Format.fprintf fmt "(* Eliminating doublons.@\n";
+    Format.fprintf fmt "   Goal : %s ; Hyp : %s *)@\n" (name goal) (name hyp);
+    (** Use 'assert' to introduce the clause we want to prove *)
+    Format.fprintf fmt "assert (%s: %a).@\n" (name goal) pp_clause goal;
+    (** Prove the goal: intro the atoms, then use them with the hyp *)
+    let m = pp_clause_intro fmt goal in
+    Format.fprintf fmt "exact (%s%a).@\n"
+      (name hyp) (fun fmt -> Array.iter (fun atom ->
+          Format.fprintf fmt " %s" (M.find atom m))) hyp.S.St.atoms
+
+  let resolution fmt goal hyp1 hyp2 atom =
+    let a = S.St.(atom.var.pa) in
+    let h1, h2 =
+      if Array.memq a hyp1.S.St.atoms then hyp1, hyp2
+      else (assert (Array.memq a hyp2.S.St.atoms); hyp2, hyp1)
+    in
+    (** Print some debug info *)
+    Format.fprintf fmt "(* Clausal resolution.@\n";
+    Format.fprintf fmt "   Goal : %s ; Hyps : %s, %s *)@\n"
+      (name goal) (name h1) (name h2);
+    (** use a cut to introduce the clause we want to prove *)
+    Format.fprintf fmt "assert (%s: %a).@\n" (name goal) pp_clause goal;
+    (** Prove the goal: intro the axioms, then perform resolution *)
+    let m = pp_clause_intro fmt goal in
+    Format.fprintf fmt "exact (%s%a).@\n"
+      (name h1) (fun fmt -> Array.iter (fun b ->
+          if b == a then begin
+            Format.fprintf fmt " (fun p => %s%a"
+              (name h2) (fun fmt -> (Array.iter (fun c ->
+                  if c == a.S.St.neg then
+                    Format.fprintf fmt " (fun np => np p)"
+                  else
+                    Format.fprintf fmt " %s" (M.find c m)))
+                ) h2.S.St.atoms
+          end else
+            Format.fprintf fmt " %s" (M.find b m))
+        ) h1.S.St.atoms
+
+
+  let prove_node t fmt node =
+    let clause = node.S.conclusion in
+    match node.S.step with
+    | S.Hypothesis ->
+      A.prove_hyp fmt (name clause) clause
+    | S.Assumption ->
+      A.prove_assumption fmt (name clause) clause
+    | S.Lemma _ ->
+      A.prove_lemma fmt (name clause) clause
+    | S.Duplicate (p, l) ->
+      let c = (S.expand p).S.conclusion in
+      elim_duplicate fmt clause c l
+    | S.Resolution (p1, p2, a) ->
+      let c1 = (S.expand p1).S.conclusion in
+      let c2 = (S.expand p2).S.conclusion in
+      resolution fmt clause c1 c2 a
+
+  (* Here the main idea is to always try and have exactly
+     one goal to prove, i.e False. So each  *)
+  let print fmt p =
+    let h = S.H.create 4013 in
+    let aux () node =
+      Format.fprintf fmt "%a@\n@\n" (prove_node h) node
+    in
+    Format.fprintf fmt "(* Coq proof generated by mSAT*)@\n";
+    S.fold aux () p
+
+end
+
+
+module Simple(S : Res.S)
+    (A : Arg with type atom := S.St.formula
+              and type hyp = S.St.formula list
+              and type lemma := S.lemma
+              and type assumption := S.St.formula) =
+  Make(S)(struct
+
+    (* Some helpers *)
+    let lit a = a.S.St.lit
+
+    let get_assumption c =
+      match S.to_list c with
+      | [ x ] -> x
+      | _ -> assert false
+
+    let get_lemma c =
+      match c.S.St.cpremise with
+      | S.St.Lemma p -> p
+      | _ -> assert false
+
+    (* Actual functions *)
+    let print_atom fmt a =
+      A.print_atom fmt a.S.St.lit
+
+    let prove_hyp fmt name c =
+      A.prove_hyp fmt name (List.map lit (S.to_list c))
+
+    let prove_lemma fmt name c =
+      A.prove_lemma fmt name (get_lemma c)
+
+    let prove_assumption fmt name c =
+      A.prove_assumption fmt name (lit (get_assumption c))
+
+  end)
+

src/backend/coq.mli

@@ -0,0 +1,50 @@
+(*
+MSAT is free software, using the Apache license, see file LICENSE
+Copyright 2015 Guillaume Bury
+*)
+
+(** Coq Backend
+
+    This module provides an easy way to produce coq scripts
+    corresponding to the resolution proofs output by the
+    sat solver. *)
+
+module type S = Backend_intf.S
+(** Interface for exporting proofs. *)
+
+module type Arg = sig
+  (** Term printing for Coq *)
+
+  type atom
+  (** The type of atomic formulas *)
+
+  type hyp
+  type lemma
+  type assumption
+  (** The types of hypotheses, lemmas, and assumptions *)
+
+  val print_atom : Format.formatter -> atom -> unit
+  (** Print the given atomic formula *)
+
+  val prove_hyp : Format.formatter -> string -> hyp -> unit
+  val prove_lemma : Format.formatter -> string -> lemma -> unit
+  val prove_assumption : Format.formatter -> string -> assumption -> unit
+  (** Proving function for hypotheses, lemmas and assumptions.
+      [prove_x fmt name x] should prove [x], and be such that after
+      executing it, [x] is among the coq hypotheses under the name [name]. *)
+
+end
+
+module Make(S : Res.S)(A : Arg with type atom := S.atom
+                                and type hyp := S.clause
+                                and type lemma := S.clause
+                                and type assumption := S.clause) : S with type t := S.proof
+(** Base functor to output Coq proofs *)
+
+
+module Simple(S : Res.S)(A : Arg with type atom := S.St.formula
+                                  and type hyp = S.St.formula list
+                                  and type lemma := S.lemma
+                                  and type assumption := S.St.formula) : S with type t := S.proof
+(** Simple functo to output Coq proofs *)
+

src/core/res_intf.ml

@@ -83,8 +83,8 @@ module type S = sig
 
   val expl : step -> string
   (** Returns a short string description for the proof step; for instance
-      ["hypothesis"] for a [Hypothesis] (generally, it currently is the
+      ["hypothesis"] for a [Hypothesis]
-      variant name in lowercase). *)
+      (it currently returns the variant name in lowercase). *)
 
   val parents : step -> proof list
   (** Returns the parents of a proof node. *)
@@ -97,8 +97,8 @@ module type S = sig
 
   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] is executed exactly once on each proof node in the tree, and that the execution of
-      [f] on a proof node happens after the execution on the children of the nodes. *)
+      [f] on a proof node happens after the execution on the parents 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.
@@ -113,4 +113,13 @@ module type S = sig
   val print_clause : Format.formatter -> clause -> unit
   (** A nice looking printer for clauses, which sort the atoms before printing. *)
 
+
+  (** {3 Unsafe} *)
+
+  module H : Hashtbl.S with type key = clause
+  (** Hashtable over clauses. Uses the details of the internal representation
+      to achieve the best performances, however hashtables from this module
+      become invalid when solving is restarted, so they should only be live
+      during inspection of a single proof. *)
+
 end

src/doc.txt

@@ -74,6 +74,7 @@ Backends for exporting proofs to different formats:
 
 {!modules:
 Dot
+Coq
 Dedukti
 Backend_intf
 }

src/msat.mlpack

@@ -22,6 +22,7 @@ Solver_types
 Res
 Backend_intf
 Dot
+Coq
 Dimacs
 Dedukti
 

src/msat.odocl

@@ -23,6 +23,7 @@ solver/Tseitin
 
 # Backends
 backend/Dot
+backend/Coq
 backend/Dedukti
 backend/Backend_intf