From: Morgan Deters Date: Mon, 12 Nov 2012 18:36:45 +0000 (+0000) Subject: Fix for bug 444, dealing with the placing of set-logic in dumping modes. X-Git-Tag: cvc5-1.0.0~7616 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ff1666905d56bf9dff0a22162688ac155200091c;p=cvc5.git Fix for bug 444, dealing with the placing of set-logic in dumping modes. CVC4 now produces equivalent output when dumping the SMT1 and SMT2 attachments to that bug report. This also fixes a memory leak in the new-variable-notification mechanism. (this commit was certified error- and warning-free by the test-and-commit script.) --- diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index e0d7c8e98..6079f146e 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -335,30 +335,26 @@ public: DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), 0, tn.toType()); - Dump("declarations") << c; - d_smt.addToModelCommand(c.clone()); + d_smt.addToModelCommandAndDump(c); } void nmNotifyNewSortConstructor(TypeNode tn) { DeclareTypeCommand c(tn.getAttribute(expr::VarNameAttr()), tn.getAttribute(expr::SortArityAttr()), tn.toType()); - Dump("declarations") << c; - d_smt.addToModelCommand(c.clone()); + d_smt.addToModelCommandAndDump(c); } void nmNotifyNewDatatypes(const std::vector& dtts) { DatatypeDeclarationCommand c(dtts); - Dump("declarations") << c; - d_smt.addToModelCommand(c.clone()); + d_smt.addToModelCommandAndDump(c); } void nmNotifyNewVar(TNode n) { DeclareFunctionCommand c(n.getAttribute(expr::VarNameAttr()), n.toExpr(), n.getType().toType()); - Dump("declarations") << c; - d_smt.addToModelCommand(c.clone()); + d_smt.addToModelCommandAndDump(c); } void nmNotifyNewSkolem(TNode n, const std::string& comment) { @@ -366,13 +362,10 @@ public: DeclareFunctionCommand c(id, n.toExpr(), n.getType().toType()); - if(Dump.isOn("skolems")) { - if(comment != "") { - Dump("skolems") << CommentCommand(id + " is " + comment); - } - Dump("skolems") << c; + if(Dump.isOn("skolems") && comment != "") { + Dump("skolems") << CommentCommand(id + " is " + comment); } - d_smt.addToModelCommand(c.clone()); + d_smt.addToModelCommandAndDump(c, "skolems"); } Node applySubstitutions(TNode node) const { @@ -475,6 +468,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() : d_assertionList(NULL), d_assignments(NULL), d_modelCommands(NULL), + d_dumpCommands(), d_logic(), d_pendingPops(0), d_fullyInited(false), @@ -537,6 +531,13 @@ void SmtEngine::finishInit() { d_assertionList = new(true) AssertionList(d_userContext); } + // dump out any pending declaration commands + for(unsigned i = 0; i < d_dumpCommands.size(); ++i) { + Dump("declarations") << *d_dumpCommands[i]; + delete d_dumpCommands[i]; + } + d_dumpCommands.clear(); + if(options::perCallResourceLimit() != 0) { setResourceLimit(options::perCallResourceLimit(), false); } @@ -629,6 +630,11 @@ SmtEngine::~SmtEngine() throw() { d_assertionList->deleteSelf(); } + for(unsigned i = 0; i < d_dumpCommands.size(); ++i) { + delete d_dumpCommands[i]; + } + d_dumpCommands.clear(); + if(d_modelCommands != NULL) { d_modelCommands->deleteSelf(); } @@ -2448,8 +2454,7 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { return SExpr(sexprs); } - -void SmtEngine::addToModelCommand(Command* c) { +void SmtEngine::addToModelCommandAndDump(const Command& c, const char* dumpTag) { Trace("smt") << "SMT addToModelCommand(" << c << ")" << endl; SmtScope smts(this); // If we aren't yet fully inited, the user might still turn on @@ -2460,9 +2465,16 @@ void SmtEngine::addToModelCommand(Command* c) { // decouple SmtEngine and ExprManager if the user does a few // ExprManager::mkSort() before SmtEngine::setOption("produce-models") // and expects to find their cardinalities in the model. - if( ! d_fullyInited || options::produceModels() ) { + if( !d_fullyInited || options::produceModels() ) { doPendingPops(); - d_modelCommands->push_back(c); + d_modelCommands->push_back(c.clone()); + } + if(Dump.isOn(dumpTag)) { + if(d_fullyInited) { + Dump(dumpTag) << c; + } else { + d_dumpCommands.push_back(c.clone()); + } } } diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 5c383071a..b2ac0b886 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -148,6 +148,14 @@ class CVC4_PUBLIC SmtEngine { */ smt::CommandList* d_modelCommands; + /** + * A vector of declaration commands waiting to be dumped out. + * Once the SmtEngine is fully initialized, we'll dump them. + * This ensures the declarations come after the set-logic and + * any necessary set-option commands are dumped. + */ + std::vector d_dumpCommands; + /** * The logic we're in. */ @@ -295,7 +303,7 @@ class CVC4_PUBLIC SmtEngine { * Add to Model command. This is used for recording a command * that should be reported during a get-model call. */ - void addToModelCommand(Command* c); + void addToModelCommandAndDump(const Command& c, const char* dumpTag = "declarations"); /** * Get the model (only if immediately preceded by a SAT