From 1ae217df1496f105db7d08859e8df2931d8f71dc Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 1 May 2013 14:04:00 -0400
Subject: [PATCH] Fix to dumping re: boolean terms, datatypes

---
 src/printer/smt2/smt2_printer.cpp |  4 ++--
 src/smt/smt_engine.cpp            | 19 +++++++++++++++----
 2 files changed, 17 insertions(+), 6 deletions(-)

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:
-- 
2.30.2