From 0186edbf34058df9c3239bf14b14c7d8838a4ab1 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 6 Apr 2016 15:32:12 +0200
Subject: [PATCH] [feature] Adds proofs for atoms true at level 0

---
 solver/res.ml      | 10 ++++++++++
 solver/res_intf.ml |  9 +++++++--
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/solver/res.ml b/solver/res.ml
index 063e415b..03192e21 100644
--- a/solver/res.ml
+++ b/solver/res.ml
@@ -96,6 +96,16 @@ module Make(St : Solver_types.S) = struct
     St.make_clause (fresh_pcl_name ()) [] 0 true (St.History (c :: l))
       (List.fold_left (fun i c -> max i c.St.c_level) 0 l)
 
+  let prove_atom a =
+    if St.(a.is_true && a.var.v_level = 0) then begin
+      match St.(a.var.reason) with
+      | St.Bcp Some c ->
+        assert (Vec.size St.(c.atoms) = 1 && equal_atoms a (Vec.get St.(c.atoms) 0));
+        Some c
+      | _ -> assert false
+    end else
+      None
+
   (* Interface exposed *)
   type proof = clause
   and proof_node = {
diff --git a/solver/res_intf.ml b/solver/res_intf.ml
index 2cb995ee..fd224762 100644
--- a/solver/res_intf.ml
+++ b/solver/res_intf.ml
@@ -29,7 +29,8 @@ module type S = sig
     | Hypothesis
     | Lemma of lemma
     | Resolution of proof * proof * atom
-    (** Lazy type for proof trees. Proofs can be extended to proof nodes using functions defined later. *)
+  (** Lazy type for proof trees. Proofs are persistent objects, and can be
+      extended to proof nodes using functions defined later. *)
 
   (** {3 Resolution helpers} *)
   val to_list : clause -> atom list
@@ -46,12 +47,16 @@ module type S = sig
   (** {3 Proof building functions} *)
 
   val prove : clause -> proof
-  (** Same as 'learn', but works on single clauses instead of vectors. *)
+  (** Given a clause, return a proof of that clause.
+      @raise Insuficient_hyps if it does not succeed. *)
 
   val prove_unsat : clause -> proof
   (** Given a conflict clause [c], returns a proof of the empty clause.
       @raise Insuficient_hyps if it does not succeed. *)
 
+  val prove_atom : atom -> proof option
+  (** Given an atom [a], returns a proof of the clause [\[a\]] if [a] is true at level 0 *)
+
   (** {3 Proof Manipulation} *)
 
   val expand : proof -> proof_node