diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 19 |
1 files changed, 15 insertions, 4 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cc11147ed..52bc0c4d3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -235,7 +235,7 @@ class SmtEnginePrivate : public NodeManagerListener { unsigned d_realAssertionsEnd; /** The converter for Boolean terms -> BITVECTOR(1). */ - BooleanTermConverter d_booleanTermConverter; + BooleanTermConverter* d_booleanTermConverter; /** A circuit propagator for non-clausal propositional deduction */ booleans::CircuitPropagator d_propagator; @@ -388,7 +388,7 @@ public: d_assertionsToPreprocess(), d_nonClausalLearnedLiterals(), d_realAssertionsEnd(0), - d_booleanTermConverter(d_smt), + d_booleanTermConverter(NULL), d_propagator(d_nonClausalLearnedLiterals, true, true), d_propagatorNeedsFinish(false), d_assertionsToCheck(), @@ -410,6 +410,10 @@ public: d_propagator.finish(); d_propagatorNeedsFinish = false; } + if(d_booleanTermConverter != NULL) { + delete d_booleanTermConverter; + d_booleanTermConverter = NULL; + } d_smt.d_nodeManager->unsubscribeEvents(this); } @@ -1211,7 +1215,8 @@ void SmtEngine::defineFunction(Expr func, stringstream ss; ss << Expr::setlanguage(Expr::setlanguage::getLanguage(Dump.getStream())) << func; - Dump("declarations") << DefineFunctionCommand(ss.str(), func, formals, formula); + DefineFunctionCommand c(ss.str(), func, formals, formula); + addToModelCommandAndDump(c, false, true, "declarations"); } SmtScope smts(this); @@ -2662,8 +2667,14 @@ void SmtEnginePrivate::processAssertions() { { Chat() << "rewriting Boolean terms..." << endl; TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime); + if(d_booleanTermConverter == NULL) { + // This needs to be initialized _after_ the whole SMT framework is in place, subscribed + // to ExprManager notifications, etc. Otherwise we might miss the "BooleanTerm" datatype + // definition, and not dump it properly. + d_booleanTermConverter = new BooleanTermConverter(d_smt); + } for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) { - Node n = d_booleanTermConverter.rewriteBooleanTerms(d_assertionsToPreprocess[i]); + Node n = d_booleanTermConverter->rewriteBooleanTerms(d_assertionsToPreprocess[i]); if(n != d_assertionsToPreprocess[i]) { switch(booleans::BooleanTermConversionMode mode = options::booleanTermConversionMode()) { case booleans::BOOLEAN_TERM_CONVERT_TO_BITVECTORS: |