diff options
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index ff84e63b7..47ba50aad 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -60,6 +60,9 @@ using namespace CVC4; using namespace CVC4::theory; void TheoryEngine::finishInit() { + // initialize the quantifiers engine + d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); + if (d_logicInfo.isQuantified()) { d_quantEngine->finishInit(); Assert(d_masterEqualityEngine == 0); @@ -67,10 +70,17 @@ void TheoryEngine::finishInit() { for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { if (d_theoryTable[theoryId]) { + d_theoryTable[theoryId]->setQuantifiersEngine(d_quantEngine); d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine); } } } + + for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) { + if (d_theoryTable[theoryId]) { + d_theoryTable[theoryId]->finishInit(); + } + } } void TheoryEngine::eqNotifyNewClass(TNode t){ @@ -146,9 +156,6 @@ TheoryEngine::TheoryEngine(context::Context* context, d_theoryOut[theoryId] = NULL; } - // initialize the quantifiers engine - d_quantEngine = new QuantifiersEngine(context, userContext, this); - // build model information if applicable d_curr_model = new theory::TheoryModel(userContext, "DefaultModel", true); d_curr_model_builder = new theory::TheoryEngineModelBuilder(this); |