diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/prop_engine.cpp | 11 | ||||
-rw-r--r-- | src/prop/prop_engine.h | 10 | ||||
-rw-r--r-- | src/prop/registrar.h | 10 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 4 |
4 files changed, 26 insertions, 9 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 2a2a60391..cb4a32ee7 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -69,7 +69,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_theoryEngine(te), d_decisionEngine(de), d_context(satContext), + d_theoryProxy(NULL), d_satSolver(NULL), + d_registrar(NULL), d_cnfStream(NULL), d_satTimer(*this), d_interrupted(false) { @@ -78,16 +80,17 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext d_satSolver = SatSolverFactory::createDPLLMinisat(); - theory::TheoryRegistrar* registrar = new theory::TheoryRegistrar(d_theoryEngine); + d_registrar = new theory::TheoryRegistrar(d_theoryEngine); d_cnfStream = new CVC4::prop::TseitinCnfStream - (d_satSolver, registrar, + (d_satSolver, d_registrar, userContext, // fullLitToNode Map = options::threads() > 1 || options::decisionMode() == decision::DECISION_STRATEGY_RELEVANCY ); - d_satSolver->initialize(d_context, 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_satSolver->initialize(d_context, d_theoryProxy); d_decisionEngine->setSatSolver(d_satSolver); d_decisionEngine->setCnfStream(d_cnfStream); @@ -97,7 +100,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext PropEngine::~PropEngine() { Debug("prop") << "Destructing the PropEngine" << endl; delete d_cnfStream; + delete d_registrar; delete d_satSolver; + delete d_theoryProxy; } void PropEngine::assertFormula(TNode node) { diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index 39182204c..753890087 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -32,6 +32,10 @@ namespace CVC4 { class DecisionEngine; class TheoryEngine; +namespace theory { + class TheoryRegistrar; +}/* CVC4::theory namespace */ + namespace prop { class CnfStream; @@ -132,12 +136,18 @@ class PropEngine { /** The context */ context::Context* d_context; + /** SAT solver's proxy back to theories; kept around for dtor cleanup */ + TheoryProxy* d_theoryProxy; + /** The SAT solver proxy */ DPLLSatSolverInterface* d_satSolver; /** List of all of the assertions that need to be made */ std::vector<Node> d_assertionList; + /** Theory registrar; kept around for destructor cleanup */ + theory::TheoryRegistrar* d_registrar; + /** The CNF converter in use */ CnfStream* d_cnfStream; diff --git a/src/prop/registrar.h b/src/prop/registrar.h index 0cb3accf1..4fe04f062 100644 --- a/src/prop/registrar.h +++ b/src/prop/registrar.h @@ -5,7 +5,7 @@ ** Major contributors: Tim King, Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -32,13 +32,11 @@ public: };/* class Registrar */ -class NullRegistrar: public Registrar { +class NullRegistrar : public Registrar { public: - void preRegister(Node n) {}; - -};/* class Registrar */ - + void preRegister(Node n) {} +};/* class NullRegistrar */ }/* CVC4::prop namespace */ }/* CVC4 namespace */ diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index f84aecbac..92c81616b 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -139,6 +139,10 @@ inline TheoryProxy::TheoryProxy(PropEngine* propEngine, d_queue(context) {} +inline TheoryProxy::~TheoryProxy() { + /* nothing to do for now */ +} + }/* CVC4::prop namespace */ }/* CVC4 namespace */ |