Virtualizing interface between CnfStream and SatSolver

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 25134b413a9afba82e3cf4910aa7161d23c1a7af..9abea4fcdea5f9571b16596a7a787a043d48934d 100644 (file)
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -29,11 +29,11 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace prop {
 
-CnfStream::CnfStream(SatSolver *satSolver) :
+CnfStream::CnfStream(SatInputInterface *satSolver) :
   d_satSolver(satSolver) {
 }
 
-TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver) :
+TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver) :
   CnfStream(satSolver) {
 }
 

diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 9a63c26f904c03b99250484c673c2de96e739523..6e4eaf047c66d0d3175fad8dea4fd980f522fbfd 100644 (file)
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -43,7 +43,7 @@ class CnfStream {
 private:
 
   /** The SAT solver we will be using */
-  SatSolver *d_satSolver;
+  SatInputInterface *d_satSolver;
 
   /** Cache of what literals have been registered to a node. */
   typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFunction> TranslationCache;
@@ -121,7 +121,7 @@ public:
    * and sends them to the given sat solver.
    * @param satSolver the sat solver to use
    */
-  CnfStream(SatSolver* satSolver);
+  CnfStream(SatInputInterface* satSolver);
 
   /**
    * Destructs a CnfStream.  This implementation does nothing, but we
@@ -179,7 +179,7 @@ public:
    * Constructs the stream to use the given sat solver.
    * @param satSolver the sat solver to use
    */
-  TseitinCnfStream(SatSolver* satSolver);
+  TseitinCnfStream(SatInputInterface* satSolver);
 
 private:
 

diff --git a/src/prop/sat.h b/src/prop/sat.h
index d5adedd2096f477a3d69b9be1f25a5d76497f116..33ab674c9e6934af77177199d77dcb99fad2da41 100644 (file)
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -73,12 +73,26 @@ hashSatLiteral(const SatLiteral& literal) {
 
 #endif /* __CVC4_USE_MINISAT */
 
+/** Interface encapsulating the "input" to the solver, e.g., from the 
+ * CNF converter. 
+ * 
+ * TODO: Is it possible to push the typedefs of SatClause and SatVariable
+ * into here, somehow?
+ */
+class SatInputInterface {
+public:
+  /** Assert a clause in the solver. */
+  virtual void addClause(SatClause& clause) = 0;
+  /** Create a new boolean variable in the solver. */
+  virtual SatVariable newVar(bool theoryAtom = false) = 0;
+};
+
 /**
  * The proxy class that allows us to modify the internals of the SAT solver.
  * It's only accessible from the PropEngine, and should be treated with major
  * care.
  */
-class SatSolver {
+class SatSolver : public SatInputInterface {
 
   /** The prop engine we are using */
   PropEngine* d_propEngine;