summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/options/options_handler.cpp3
-rw-r--r--src/smt/smt_engine.cpp20
-rw-r--r--test/unit/prop/cnf_stream_white.h4
-rw-r--r--test/unit/theory/theory_arith_white.h5
-rw-r--r--test/unit/theory/theory_bv_white.h4
-rw-r--r--test/unit/theory/theory_engine_white.h4
-rw-r--r--test/unit/theory/theory_white.h4
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<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() );
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index 7e04bb7c5..35eb240a2 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -136,6 +136,10 @@ class CnfStreamWhite : public CxxTest::TestSuite {
d_nodeManager = NodeManager::fromExprManager(d_exprManager);
d_scope = new SmtScope(d_smt);
+ // 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;
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<TheoryBV*>(
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];
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback