diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-10-15 11:42:28 -0500 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-10-15 09:42:28 -0700 |
commit | d828df78c39000b54c2a7824482e206f6761664f (patch) | |
tree | 1c3f2f6cd119ce6bd3a9d59593d22d895801ab44 /src | |
parent | de7798ebbc351046d7b5ae7e6379ffd61be0f1c4 (diff) |
Delay initialization of theory engine (#2621)
This implements solution number 2 for issue #2613.
Diffstat (limited to 'src')
-rw-r--r-- | src/options/options_handler.cpp | 3 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 20 |
2 files changed, 14 insertions, 9 deletions
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp index 6eed732e2..9cf5180e8 100644 --- a/src/options/options_handler.cpp +++ b/src/options/options_handler.cpp @@ -86,8 +86,7 @@ void OptionsHandler::notifyBeforeSearch(const std::string& option) d_options->d_beforeSearchListeners.notify(); } catch (ModalException&){ std::stringstream ss; - ss << "cannot change option `" << option - << "' after final initialization (i.e., after logic has been set)"; + ss << "cannot change option `" << option << "' after final initialization"; throw ModalException(ss.str()); } } diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index b1d6df852..38c9e7ee2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -849,6 +849,14 @@ SmtEngine::SmtEngine(ExprManager* em) d_proofManager = new ProofManager(d_userContext); #endif + d_definedFunctions = new (true) DefinedFunctionMap(d_userContext); + d_fmfRecFunctionsDefined = new (true) NodeList(d_userContext); + d_modelCommands = new (true) smt::CommandList(d_userContext); +} + +void SmtEngine::finishInit() +{ + Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; // We have mutual dependency here, so we add the prop engine to the theory // engine later (it is non-essential there) d_theoryEngine = new TheoryEngine(d_context, @@ -873,13 +881,6 @@ SmtEngine::SmtEngine(ExprManager* em) d_userContext->push(); d_context->push(); - d_definedFunctions = new(true) DefinedFunctionMap(d_userContext); - d_fmfRecFunctionsDefined = new(true) NodeList(d_userContext); - d_modelCommands = new(true) smt::CommandList(d_userContext); -} - -void SmtEngine::finishInit() { - Trace("smt-debug") << "SmtEngine::finishInit" << std::endl; // ensure that our heuristics are properly set up setDefaults(); @@ -4467,6 +4468,7 @@ const Proof& SmtEngine::getProof() void SmtEngine::printInstantiations( std::ostream& out ) { SmtScope smts(this); + finalOptionsAreSet(); if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){ out << "% SZS output start Proof for " << d_filename.c_str() << std::endl; } @@ -4482,6 +4484,7 @@ void SmtEngine::printInstantiations( std::ostream& out ) { void SmtEngine::printSynthSolution( std::ostream& out ) { SmtScope smts(this); + finalOptionsAreSet(); if( d_theoryEngine ){ d_theoryEngine->printSynthSolution( out ); }else{ @@ -4492,6 +4495,7 @@ void SmtEngine::printSynthSolution( std::ostream& out ) { void SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map) { SmtScope smts(this); + finalOptionsAreSet(); map<Node, Node> sol_mapn; Assert(d_theoryEngine != nullptr); d_theoryEngine->getSynthSolutions(sol_mapn); @@ -4504,6 +4508,7 @@ void SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map) Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) { SmtScope smts(this); + finalOptionsAreSet(); if(!d_logic.isPure(THEORY_ARITH) && strict){ Warning() << "Unexpected logic for quantifier elimination " << d_logic << endl; } @@ -4831,6 +4836,7 @@ void SmtEngine::setUserAttribute(const std::string& attr, const std::string& str_value) { SmtScope smts(this); + finalOptionsAreSet(); std::vector<Node> node_values; for( unsigned i=0; i<expr_values.size(); i++ ){ node_values.push_back( expr_values[i].getNode() ); |