From: Morgan Deters Date: Wed, 1 May 2013 18:04:00 +0000 (-0400) Subject: Fix to dumping re: boolean terms, datatypes X-Git-Tag: cvc5-1.0.0~7290^2~1 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1ae217df1496f105db7d08859e8df2931d8f71dc;p=cvc5.git Fix to dumping re: boolean terms, datatypes --- diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 722d2604b..c59df6269 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -824,11 +824,11 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr const Datatype & d = i->getDatatype(); - out << "(" << d.getName() << " "; + out << "(" << maybeQuoteSymbol(d.getName()) << " "; for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end(); ctor != ctor_end; ++ctor){ if( ctor!=d.begin() ) out << " "; - out << "(" << ctor->getName(); + out << "(" << maybeQuoteSymbol(ctor->getName()); for(DatatypeConstructor::const_iterator arg = ctor->begin(), arg_end = ctor->end(); arg != arg_end; ++arg){ 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: