Merge branch 'master' of https://github.com/CVC4/CVC4

6 files changed, 99 insertions, 12 deletions

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index b155b3a1c..70f04be85 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -570,9 +570,11 @@ inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
 
     while (it != it_end){
       uint64_t id = (*it).first.first;
+      /*
       Debug("attrgc") << "id " << id
                       << " node_value: " << ((*it).first.second)
                       << std::endl;
+      */
       if(traits_t::cleanup[id] != NULL) {
         traits_t::cleanup[id]((*it).second);
       }
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index d7a61e32c..4893075c3 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -294,11 +294,13 @@ public:
     if(i == super::end()) {
       return BitIterator();
     }
+    /*
     Debug.printf("boolattr",
                  "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
                  &(*i).second,
                  (unsigned long long)((*i).second),
                  unsigned(k.first));
+    */
     return BitIterator(*i, k.first);
   }
 
@@ -316,11 +318,13 @@ public:
     if(i == super::end()) {
       return ConstBitIterator();
     }
+    /*
     Debug.printf("boolattr",
                  "underlying word at 0x%p looks like 0x%016llx, bit is %u\n",
                  &(*i).second,
                  (unsigned long long)((*i).second),
                  unsigned(k.first));
+    */
     return ConstBitIterator(*i, k.first);
   }
 
@@ -409,9 +413,11 @@ class CDAttrHash<bool> :
       d_key(key),
       d_word(word),
       d_bit(bit) {
+      /*
       Debug.printf("cdboolattr",
                    "CDAttrHash<bool>::BitAccessor(%p, %p, %016llx, %u)\n",
                    &map, key, (unsigned long long) word, bit);
+      */
     }
 
     BitAccessor& operator=(bool b) {
@@ -419,25 +425,31 @@ class CDAttrHash<bool> :
         // set the bit
         d_word |= (1 << d_bit);
         d_map.insert(d_key, d_word);
+        /*
         Debug.printf("cdboolattr",
                      "CDAttrHash<bool>::BitAccessor::set(%p, %p, %016llx, %u)\n",
                      &d_map, d_key, (unsigned long long) d_word, d_bit);
+        */
       } else {
         // clear the bit
         d_word &= ~(1 << d_bit);
         d_map.insert(d_key, d_word);
+        /*
         Debug.printf("cdboolattr",
                      "CDAttrHash<bool>::BitAccessor::clr(%p, %p, %016llx, %u)\n",
                      &d_map, d_key, (unsigned long long) d_word, d_bit);
+        */
       }
 
       return *this;
     }
 
     operator bool() const {
+      /*
       Debug.printf("cdboolattr",
                    "CDAttrHash<bool>::BitAccessor::toBool(%p, %p, %016llx, %u)\n",
                    &d_map, d_key, (unsigned long long) d_word, d_bit);
+      */
       return (d_word & (1 << d_bit)) ? true : false;
     }
   };/* class CDAttrHash<bool>::BitAccessor */
@@ -503,10 +515,12 @@ public:
     if(i == super::end()) {
       return ConstBitIterator();
     }
+    /*
     Debug.printf("cdboolattr",
                  "underlying word at address looks like 0x%016llx, bit is %u\n",
                  (unsigned long long)((*i).second),
                  unsigned(k.first));
+    */
     return ConstBitIterator(*i, k.first);
   }
 
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/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index f8f2330e1..0063035ff 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -111,6 +111,52 @@ static inline bool isBoolean(TNode top, unsigned i) {
   }
 }
 
+// This function rewrites "in" as an "as"---this is actually expected
+// to be for model-substitution, so the "in" is a Boolean-term-converted
+// node, and "as" is the original.  See how it's used in function
+// handling, below.
+Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as) throw() {
+  if(in.getType() == as) {
+    return in;
+  }
+  if(in.getType().isBoolean()) {
+    Assert(d_tt.getType() == as);
+    return NodeManager::currentNM()->mkNode(kind::ITE, in, d_tt, d_ff);
+  }
+  if(as.isBoolean() && in.getType().isBitVector() && in.getType().getBitVectorSize() == 1) {
+    return NodeManager::currentNM()->mkNode(kind::EQUAL, NodeManager::currentNM()->mkConst(BitVector(1u, 1u)), in);
+  }
+  if(in.getType().isDatatype()) {
+    if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
+      return NodeManager::currentNM()->mkNode(kind::EQUAL, d_ttDt, in);
+    }
+    Assert(as.isDatatype());
+    const Datatype* dt2 = &as.getDatatype();
+    const Datatype* dt1 = d_datatypeCache[dt2];
+    Assert(dt1 != NULL, "expected datatype in cache");
+    Assert(*dt1 == in.getType().getDatatype(), "improper rewriteAs() between datatypes");
+    Node out;
+    for(size_t i = 0; i < dt1->getNumConstructors(); ++i) {
+      DatatypeConstructor ctor = (*dt1)[i];
+      NodeBuilder<> appctorb(kind::APPLY_CONSTRUCTOR);
+      appctorb << (*dt2)[i].getConstructor();
+      for(size_t j = 0; j < ctor.getNumArgs(); ++j) {
+        appctorb << rewriteAs(NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR, ctor[j].getSelector(), in), TypeNode::fromType(SelectorType((*dt2)[i][j].getSelector().getType()).getRangeType()));
+      }
+      Node appctor = appctorb;
+      if(i == 0) {
+        out = appctor;
+      } else {
+        Node newOut = NodeManager::currentNM()->mkNode(kind::ITE, ctor.getTester(), appctor, out);
+        out = newOut;
+      }
+    }
+    return out;
+  }
+
+  Unhandled(in);
+}
+
 const Datatype& BooleanTermConverter::convertDatatype(const Datatype& dt) throw() {
   const Datatype*& out = d_datatypeCache[&dt];
   if(out != NULL) {
@@ -392,12 +438,20 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
       } else if(mk == kind::metakind::VARIABLE) {
         TypeNode t = top.getType();
         if(t.isFunction()) {
-          for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) {
+          for(unsigned i = 0; i < t.getNumChildren(); ++i) {
             TypeNode newType = convertType(t[i], false);
-            if(newType != t[i]) {
+            // is this the return type?  (allowed to be Bool)
+            bool returnType = (i == t.getNumChildren() - 1);
+            if(newType != t[i] && (!t[i].isBoolean() || !returnType)) {
               vector<TypeNode> argTypes = t.getArgTypes();
-              replace(argTypes.begin(), argTypes.end(), t[i], d_tt.getType());
-              TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType());
+              for(unsigned j = 0; j < argTypes.size(); ++j) {
+                argTypes[j] = convertType(argTypes[j], false);
+              }
+              TypeNode rangeType = t.getRangeType();
+              if(!rangeType.isBoolean()) {
+                rangeType = convertType(rangeType, false);
+              }
+              TypeNode newType = nm->mkFunctionType(argTypes, rangeType);
               Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "__boolterm__",
                                     newType, "a function introduced by Boolean-term conversion",
                                     NodeManager::SKOLEM_EXACT_NAME);
@@ -409,14 +463,18 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
               for(unsigned j = 0; j < t.getNumChildren() - 1; ++j) {
                 Node var = nm->mkBoundVar(t[j]);
                 boundVarsBuilder << var;
-                if(t[j].isBoolean()) {
-                  bodyBuilder << nm->mkNode(kind::ITE, var, d_tt, d_ff);
+                if(t[j] != argTypes[j]) {
+                  bodyBuilder << rewriteAs(var, argTypes[j]);
                 } else {
                   bodyBuilder << var;
                 }
               }
               Node boundVars = boundVarsBuilder;
               Node body = bodyBuilder;
+              if(t.getRangeType() != rangeType) {
+                Node convbody = rewriteAs(body, t.getRangeType());
+                body = convbody;
+              }
               Node lam = nm->mkNode(kind::LAMBDA, boundVars, body);
               Debug("boolean-terms") << "substituting " << top << " ==> " << lam << endl;
               d_smt.d_theoryEngine->getModel()->addSubstitution(top, lam);
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
index e5f18b68d..904d47b5f 100644
--- a/src/smt/boolean_terms.h
+++ b/src/smt/boolean_terms.h
@@ -65,6 +65,8 @@ class BooleanTermConverter {
   /** The cache used during Boolean term datatype conversion */
   BooleanTermDatatypeCache d_datatypeCache;
 
+  Node rewriteAs(TNode in, TypeNode as) throw();
+
   /**
    * Scan a datatype for and convert as necessary.
    */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 78f6e3dae..0d473a1a1 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;
@@ -390,7 +390,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(),
@@ -412,6 +412,10 @@ public:
       d_propagator.finish();
       d_propagatorNeedsFinish = false;
     }
+    if(d_booleanTermConverter != NULL) {
+      delete d_booleanTermConverter;
+      d_booleanTermConverter = NULL;
+    }
     d_smt.d_nodeManager->unsubscribeEvents(this);
   }
 
@@ -1213,7 +1217,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);
 
@@ -2680,8 +2685,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: