diff options
Diffstat (limited to 'src/prop/prop_engine.cpp')
-rw-r--r-- | src/prop/prop_engine.cpp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 2a1b05619..96ca7480f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -25,7 +25,6 @@ #include "decision/decision_engine.h" #include "expr/expr.h" #include "expr/resource_manager.h" -#include "expr/result.h" #include "options/base_options.h" #include "options/decision_options.h" #include "options/main_options.h" @@ -40,7 +39,7 @@ #include "smt_util/command.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" - +#include "util/result.h" using namespace std; using namespace CVC4::context; @@ -68,7 +67,7 @@ public: } }; -PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext) : +PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext, Context* userContext, SmtGlobals* globals) : d_inCheckSat(false), d_theoryEngine(te), d_decisionEngine(de), @@ -78,7 +77,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_registrar(NULL), d_cnfStream(NULL), d_interrupted(false), - d_resourceManager(NodeManager::currentResourceManager()) { + d_resourceManager(NodeManager::currentResourceManager()), + d_globals(globals) +{ Debug("prop") << "Constructing the PropEngine" << endl; @@ -86,14 +87,13 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream - (d_satSolver, d_registrar, - userContext, + (d_satSolver, d_registrar, userContext, d_globals, // fullLitToNode Map = options::threads() > 1 || options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY ); - d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream); + d_theoryProxy = new TheoryProxy(this, d_theoryEngine, d_decisionEngine, d_context, d_cnfStream, d_globals); d_satSolver->initialize(d_context, d_theoryProxy); d_decisionEngine->setSatSolver(d_satSolver); |