adding ::getBooleanVariables to the PropEngine

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

1 files changed, 7 insertions, 2 deletions

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);
 }