Merged bit-vector and uf proof branch.

1 files changed, 17 insertions, 2 deletions

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 1c1dae410..1383308a3 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -30,10 +30,15 @@
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+  
+class BitVectorProof;
+
 namespace prop {
 
 class TheoryProxy;
 
+typedef unsigned ClauseId;
+
 class SatSolver {
 
 public:
@@ -42,7 +47,8 @@ public:
   virtual ~SatSolver() throw(AssertionException) { }
 
   /** Assert a clause in the solver. */
-  virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0;
+  virtual ClauseId addClause(SatClause& clause,
+                             bool removable) = 0;
 
   /**
    * Create a new boolean variable in the solver.
@@ -77,6 +83,10 @@ public:
   /** Get the current assertion level */
   virtual unsigned getAssertionLevel() const = 0;
 
+  /** Check if the solver is in an inconsistent state */
+  virtual bool ok() const = 0;
+
+  
 };/* class SatSolver */
 
 
@@ -121,6 +131,10 @@ public:
 
   virtual void popAssumption() = 0;
 
+  virtual bool ok() const = 0;
+  
+  virtual void setProofLog( BitVectorProof * bvp ) {}
+
 };/* class BVSatSolverInterface */
 
 
@@ -139,7 +153,8 @@ public:
   virtual bool flipDecision() = 0;
 
   virtual bool isDecision(SatVariable decn) const = 0;
-
+  
+  virtual bool ok() const = 0;
 };/* class DPLLSatSolverInterface */
 
 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {