From ee13eb366b94b078ddb7c3755f84e64ae0e908ce Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 13 Mar 2015 14:48:20 +0100
Subject: [PATCH] Fix for incomplete proofs due to hypothesis not proved

---
 sat/sat.ml          | 1 +
 smt/mcsat.ml        | 1 +
 smt/smt.ml          | 1 +
 solver/mcsolver.ml  | 2 ++
 solver/mcsolver.mli | 4 ++++
 solver/solver.ml    | 2 ++
 solver/solver.mli   | 4 ++++
 7 files changed, 15 insertions(+)

diff --git a/sat/sat.ml b/sat/sat.ml
index 96c637db..e7d2fbcb 100644
--- a/sat/sat.ml
+++ b/sat/sat.ml
@@ -141,6 +141,7 @@ module Make(Log : Log_intf.S) = struct
   let eval = SatSolver.eval
 
   let get_proof () =
+    SatSolver.Proof.learn (SatSolver.hyps ());
     SatSolver.Proof.learn (SatSolver.history ());
     match SatSolver.unsat_conflict () with
     | None -> assert false
diff --git a/smt/mcsat.ml b/smt/mcsat.ml
index b79680d1..ddde97e7 100644
--- a/smt/mcsat.ml
+++ b/smt/mcsat.ml
@@ -135,6 +135,7 @@ module Make(Dummy:sig end) = struct
     with SmtSolver.Unsat -> ()
 
   let get_proof () =
+    SmtSolver.Proof.learn (SmtSolver.hyps ());
     SmtSolver.Proof.learn (SmtSolver.history ());
     match SmtSolver.unsat_conflict () with
     | None -> assert false
diff --git a/smt/smt.ml b/smt/smt.ml
index 70a9da5b..21cf68b7 100644
--- a/smt/smt.ml
+++ b/smt/smt.ml
@@ -84,6 +84,7 @@ module Make(Dummy:sig end) = struct
     with SmtSolver.Unsat -> ()
 
   let get_proof () =
+    SmtSolver.Proof.learn (SmtSolver.hyps ());
     SmtSolver.Proof.learn (SmtSolver.history ());
     match SmtSolver.unsat_conflict () with
     | None -> assert false
diff --git a/solver/mcsolver.ml b/solver/mcsolver.ml
index f88f2bb0..d0ad6a52 100644
--- a/solver/mcsolver.ml
+++ b/solver/mcsolver.ml
@@ -875,6 +875,8 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
     let truth = var.tag.pa.is_true in
     if negated then not truth else truth
 
+  let hyps () = env.clauses
+
   let history () = env.learnts
 
   let unsat_conflict () = env.unsat_conflict
diff --git a/solver/mcsolver.mli b/solver/mcsolver.mli
index 82040a90..d0e657dd 100644
--- a/solver/mcsolver.mli
+++ b/solver/mcsolver.mli
@@ -33,6 +33,10 @@ module Make (L : Log_intf.S)(E : Expr_intf.S)
   (** Returns the valuation of a formula in the current state
       of the sat solver. *)
 
+  val hyps : unit -> St.clause Vec.t
+  (** Returns the vector of assumptions used by the solver. May be slightly different
+      from the clauses assumed because of top-level simplification of clauses. *)
+
   val history : unit -> St.clause Vec.t
   (** Returns the history of learnt clauses, in the right order. *)
 
diff --git a/solver/solver.ml b/solver/solver.ml
index dc865d44..c40ee0f0 100644
--- a/solver/solver.ml
+++ b/solver/solver.ml
@@ -737,6 +737,8 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
     let truth = var.pa.is_true in
     if negated then not truth else truth
 
+  let hyps () = env.clauses
+
   let history () = env.learnts
 
   let unsat_conflict () = env.unsat_conflict
diff --git a/solver/solver.mli b/solver/solver.mli
index 492d6139..ab28c2b9 100644
--- a/solver/solver.mli
+++ b/solver/solver.mli
@@ -40,6 +40,10 @@ module Make (L : Log_intf.S)(F : Formula_intf.S)
   (** Returns the valuation of a formula in the current state
       of the sat solver. *)
 
+  val hyps : unit -> St.clause Vec.t
+  (** Returns the vector of assumptions used by the solver. May be slightly different
+      from the clauses assumed because of top-level simplification of clauses. *)
+
   val history : unit -> St.clause Vec.t
   (** Returns the history of learnt clauses, in the right order. *)