diff options
author | Tim King <taking@google.com> | 2017-03-27 12:26:14 -0700 |
---|---|---|
committer | Tim King <taking@google.com> | 2017-03-27 12:26:14 -0700 |
commit | f49ddf87046793972a7f6a1bdae15003709f08d2 (patch) | |
tree | b008e40a4e29be9455bc09a65bf2437588900104 /src/theory/theory_engine.cpp | |
parent | 4930de53415ffbf614d6965af59b1f44e405451c (diff) |
Making the ExtTheory object a private member of Theory.
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index d297595e1..c7d200a90 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -213,7 +213,7 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, Proof* pf) void TheoryEngine::finishInit() { // initialize the quantifiers engine d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); - + //initialize the quantifiers engine, master equality engine, model, model builder if( d_logicInfo.isQuantified() ) { d_quantEngine->finishInit(); @@ -226,7 +226,7 @@ void TheoryEngine::finishInit() { d_theoryTable[theoryId]->setMasterEqualityEngine(d_masterEqualityEngine); } } - + d_curr_model_builder = d_quantEngine->getModelBuilder(); d_curr_model = d_quantEngine->getModel(); } else { |