Merged cryptominisat from experimental branch.

1 files changed, 8 insertions, 1 deletions

diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 92696ae25..81fb94242 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -49,6 +49,12 @@ public:
   virtual ClauseId addClause(SatClause& clause,
                              bool removable) = 0;
 
+  /** Return true if the solver supports native xor resoning */
+  virtual bool nativeXor() { return false; }
+
+  /** Add a clause corresponding to rhs = l1 xor .. xor ln  */
+  virtual ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) = 0;
+  
   /**
    * Create a new boolean variable in the solver.
    * @param isTheoryAtom is this a theory atom that needs to be asserted to theory
@@ -84,7 +90,8 @@ public:
 
   /** Check if the solver is in an inconsistent state */
   virtual bool ok() const = 0;
-
+  
+  virtual void setProofLog( BitVectorProof * bvp ) {}
   
 };/* class SatSolver */