From d828df78c39000b54c2a7824482e206f6761664f Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 15 Oct 2018 11:42:28 -0500 Subject: [PATCH] Delay initialization of theory engine (#2621) This implements solution number 2 for issue #2613. --- src/options/options_handler.cpp | 3 +-- src/smt/smt_engine.cpp | 20 +++++++++++++------- test/unit/prop/cnf_stream_white.h | 4 ++++ test/unit/theory/theory_arith_white.h | 5 +++++ test/unit/theory/theory_bv_white.h | 4 ++++ test/unit/theory/theory_engine_white.h | 4 ++++ test/unit/theory/theory_white.h | 4 ++++ 7 files changed, 35 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& sol_map) { SmtScope smts(this); + finalOptionsAreSet(); map sol_mapn; Assert(d_theoryEngine != nullptr); d_theoryEngine->getSynthSolutions(sol_mapn); @@ -4504,6 +4508,7 @@ void SmtEngine::getSynthSolutions(std::map& 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_values; for( unsigned i=0; ifinalOptionsAreSet(); d_theoryEngine = d_smt->d_theoryEngine; d_satSolver = new FakeSatSolver(); diff --git a/test/unit/theory/theory_arith_white.h b/test/unit/theory/theory_arith_white.h index 7661c08b5..d81406dac 100644 --- a/test/unit/theory/theory_arith_white.h +++ b/test/unit/theory/theory_arith_white.h @@ -109,6 +109,11 @@ public: d_outputChannel.clear(); d_logicInfo.lock(); + // Notice that this unit test uses the theory engine of a created SMT + // engine d_smt. We must ensure that d_smt is properly initialized via + // the following call, which constructs its underlying theory engine. + d_smt->finalOptionsAreSet(); + // guard against duplicate statistics assertion errors delete d_smt->d_theoryEngine->d_theoryTable[THEORY_ARITH]; delete d_smt->d_theoryEngine->d_theoryOut[THEORY_ARITH]; diff --git a/test/unit/theory/theory_bv_white.h b/test/unit/theory/theory_bv_white.h index bc5b36a0b..9b0d56998 100644 --- a/test/unit/theory/theory_bv_white.h +++ b/test/unit/theory/theory_bv_white.h @@ -70,6 +70,10 @@ public: void testBitblasterCore() { d_smt->setOption("bitblast", SExpr("eager")); d_smt->setOption("incremental", SExpr("false")); + // Notice that this unit test uses the theory engine of a created SMT + // engine d_smt. We must ensure that d_smt is properly initialized via + // the following call, which constructs its underlying theory engine. + d_smt->finalOptionsAreSet(); EagerBitblaster* bb = new EagerBitblaster( dynamic_cast( d_smt->d_theoryEngine->d_theoryTable[THEORY_BV]), diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index 620fcd92e..50057f9fd 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -251,6 +251,10 @@ public: d_nullChannel = new FakeOutputChannel(); + // Notice that this unit test uses the theory engine of a created SMT + // engine d_smt. We must ensure that d_smt is properly initialized via + // the following call, which constructs its underlying theory engine. + d_smt->finalOptionsAreSet(); d_theoryEngine = d_smt->d_theoryEngine; for(TheoryId id = THEORY_FIRST; id != THEORY_LAST; ++id) { delete d_theoryEngine->d_theoryOut[id]; diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h index c8265a755..4ff11014b 100644 --- a/test/unit/theory/theory_white.h +++ b/test/unit/theory/theory_white.h @@ -166,6 +166,10 @@ class TheoryBlack : public CxxTest::TestSuite { d_logicInfo = new LogicInfo(); d_logicInfo->lock(); + // Notice that this unit test uses the theory engine of a created SMT + // engine d_smt. We must ensure that d_smt is properly initialized via + // the following call, which constructs its underlying theory engine. + d_smt->finalOptionsAreSet(); // guard against duplicate statistics assertion errors delete d_smt->d_theoryEngine->d_theoryTable[THEORY_BUILTIN]; delete d_smt->d_theoryEngine->d_theoryOut[THEORY_BUILTIN]; -- 2.30.2