diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-03-06 16:13:31 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-03-06 16:13:31 -0600 |
commit | 612bb0013f180a7d414f0a4b1e770aaa7ed09152 (patch) | |
tree | bfd2b723cfccb04ab3422351dae4630eaee35d7e /src/theory/theory_engine.cpp | |
parent | e0909efd64c96311c69dec223411ab6b7988d01d (diff) |
Simplify initialization of quantifiers engine (#1641)
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 16 |
1 files changed, 12 insertions, 4 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 0c2857b11..a6c42f584 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -214,12 +214,11 @@ void TheoryEngine::EngineOutputChannel::conflict(TNode conflictNode, } 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(); + // initialize the quantifiers engine + d_quantEngine = new QuantifiersEngine(d_context, d_userContext, this); Assert(d_masterEqualityEngine == 0); d_masterEqualityEngine = new eq::EqualityEngine(d_masterEENotify,getSatContext(), "theory::master", false); @@ -904,7 +903,14 @@ TheoryModel* TheoryEngine::getModel() { void TheoryEngine::getSynthSolutions(std::map<Node, Node>& sol_map) { - d_quantEngine->getSynthSolutions(sol_map); + if (d_quantEngine) + { + d_quantEngine->getSynthSolutions(sol_map); + } + else + { + Assert(false); + } } bool TheoryEngine::presolve() { @@ -1480,6 +1486,7 @@ void TheoryEngine::printInstantiations( std::ostream& out ) { d_quantEngine->printInstantiations( out ); }else{ out << "Internal error : instantiations not available when quantifiers are not present." << std::endl; + Assert(false); } } @@ -1488,6 +1495,7 @@ void TheoryEngine::printSynthSolution( std::ostream& out ) { d_quantEngine->printSynthSolution( out ); }else{ out << "Internal error : synth solution not available when quantifiers are not present." << std::endl; + Assert(false); } } |