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 e0d7c8e980144839785508d299824f4b9621e6d6..6079f146eeeb033cc052b522d6e7ad118d417347 100644 (file)
--- 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<DatatypeType>& 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 5c383071a3ae223800655afe67a18910a52077cc..b2ac0b88626fcd22d29ff1a60b7562f22afeea77 100644 (file)
--- 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<Command*> 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