adding ::getBooleanVariables to the PropEngine

you can get the Boolean variables in the TheoryEngine now by using d_propEngine->getBooleanVariables

6 files changed, 43 insertions, 19 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 0f1161a06..f47637b72 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -44,8 +44,9 @@ namespace CVC4 {
 namespace prop {
 
 
-CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, bool fullLitToNodeMap) :
+CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) :
   d_satSolver(satSolver),
+  d_booleanVariables(context),
   d_fullLitToNodeMap(fullLitToNodeMap),
   d_registrar(registrar) {
 }
@@ -66,8 +67,8 @@ void CnfStream::recordTranslation(TNode node, bool alwaysRecord) {
   }
 }
 
-TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap) :
-  CnfStream(satSolver, registrar, fullLitToNodeMap) {
+TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) :
+  CnfStream(satSolver, registrar, context, fullLitToNodeMap) {
 }
 
 void CnfStream::assertClause(TNode node, SatClause& c) {
@@ -230,22 +231,26 @@ TNode CnfStream::getNode(const SatLiteral& literal) {
   return find->second;
 }
 
+void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const {
+  context::CDList<TNode>::const_iterator it, it_end;
+  for (it = d_booleanVariables.begin(); it != d_booleanVariables.end(); ++ it) {
+    outputVariables.push_back(*it);
+  }
+}
+
 SatLiteral CnfStream::convertAtom(TNode node) {
   Debug("cnf") << "convertAtom(" << node << ")" << endl;
 
   Assert(!isTranslated(node), "atom already mapped!");
-  // boolean variables are not theory literals
-  bool theoryLiteral = node.getKind() != kind::VARIABLE;
-  SatLiteral lit = newLiteral(node, theoryLiteral);
 
-  if(node.getKind() == kind::CONST_BOOLEAN) {
-    if(node.getConst<bool>()) {
-      assertClause(node, lit);
-    } else {
-      assertClause(node, ~lit);
-    }
+  // Is this a variable add it to the list
+  if (node.isVar()) {
+    d_booleanVariables.push_back(node);
   }
 
+  // Make a new literal (variables are not considered theory literals)
+  SatLiteral lit = newLiteral(node, !node.isVar());
+
   // We have a literal, so it has to be recorded.  The definitional clauses
   // go away on user-pop, so this literal will have to be re-vivified if it's
   // used subsequently.
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 69db89086..5efedd4ca 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -67,6 +67,9 @@ protected:
   /** The SAT solver we will be using */
   SatSolver *d_satSolver;
 
+  /** Boolean variables that we translated */
+  context::CDList<TNode> d_booleanVariables;
+
   TranslationCache d_translationCache;
   NodeCache d_nodeCache;
 
@@ -187,10 +190,11 @@ public:
    * set of clauses and sends them to the given sat solver.
    * @param satSolver the sat solver to use
    * @param registrar the entity that takes care of preregistration of Nodes
+   * @param context the context that the CNF should respect
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
    */
-  CnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap = false);
+  CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap = false);
 
   /**
    * Destructs a CnfStream.  This implementation does nothing, but we
@@ -245,6 +249,11 @@ public:
    */
   SatLiteral getLiteral(TNode node);
 
+  /**
+   * Returns the Boolean variables from the input problem.
+   */
+  void getBooleanVariables(std::vector<TNode>& outputVariables) const;
+
   const TranslationCache& getTranslationCache() const {
     return d_translationCache;
   }
@@ -290,7 +299,7 @@ public:
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
    */
-  TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, bool fullLitToNodeMap = false);
+  TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap = false);
 
 private:
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index f115aa6d0..fe25caf29 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -65,11 +65,11 @@ public:
   }
 };
 
-PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) :
+PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext) :
   d_inCheckSat(false),
   d_theoryEngine(te),
   d_decisionEngine(de),
-  d_context(context),
+  d_context(satContext),
   d_satSolver(NULL),
   d_cnfStream(NULL),
   d_satTimer(*this),
@@ -82,6 +82,7 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* context) :
   theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine);
   d_cnfStream = new CVC4::prop::TseitinCnfStream
     (d_satSolver, registrar, 
+     userContext,
      // fullLitToNode Map = 
      options::threads() > 1 || 
      options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY);
@@ -246,6 +247,10 @@ bool PropEngine::hasValue(TNode node, bool& value) const {
   }
 }
 
+void PropEngine::getBooleanVariables(std::vector<TNode>& outputVariables) const {
+  d_cnfStream->getBooleanVariables(outputVariables);
+}
+
 void PropEngine::ensureLiteral(TNode n) {
   d_cnfStream->ensureLiteral(n);
 }
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index 2d4e08db7..f3b1ccaf3 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -157,7 +157,7 @@ public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(TheoryEngine*, DecisionEngine*, context::Context*);
+  PropEngine(TheoryEngine*, DecisionEngine*, context::Context* satContext, context::Context* userContext);
 
   /**
    * Destructor.
@@ -260,6 +260,11 @@ public:
   bool hasValue(TNode node, bool& value) const;
 
   /**
+   * Returns the Boolean variables known to the SAT solver.
+   */
+  void getBooleanVariables(std::vector<TNode>& outputVariables) const;
+
+  /**
    * Ensure that the given node will have a designated SAT literal
    * that is definitionally equal to it.  The result of this function
    * is that the Node can be queried via getSatValue().
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a857351a5..d3806199b 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -427,7 +427,7 @@ void SmtEngine::finishInit() {
   d_decisionEngine = new DecisionEngine(d_context, d_userContext);
   d_decisionEngine->init();   // enable appropriate strategies
 
-  d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context);
+  d_propEngine = new PropEngine(d_theoryEngine, d_decisionEngine, d_context, d_userContext);
 
   d_theoryEngine->setPropEngine(d_propEngine);
   d_theoryEngine->setDecisionEngine(d_decisionEngine);
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index eb5f3e155..2c45fb603 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -61,7 +61,7 @@ Bitblaster::Bitblaster(context::Context* c, bv::TheoryBV* bv) :
     d_statistics()
   {
     d_satSolver = prop::SatSolverFactory::createMinisat(c);
-    d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar());
+    d_cnfStream = new TseitinCnfStream(d_satSolver, new NullRegistrar(), new Context());
 
     MinisatNotify* notify = new MinisatNotify(d_cnfStream, bv);
     d_satSolver->setNotify(notify);