First chunk of boolean-terms support.

Passes simple tests and doesn't break existing functionality.
Still need some work merged in for models.

This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV).  Tonight's nightly regression run should tell us if/how that hurts performance.

(this commit was certified error- and warning-free by the test-and-commit script.)

5 files changed, 351 insertions, 1 deletions

diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 82601e3c3..75f17326d 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -15,6 +15,8 @@ libsmt_la_SOURCES = \
 	command_list.cpp \
 	command_list.h \
 	modal_exception.h \
+	boolean_terms.h \
+	boolean_terms.cpp \
 	logic_exception.h \
 	simplification_mode.h \
 	simplification_mode.cpp
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
new file mode 100644
index 000000000..c332642f1
--- /dev/null
+++ b/src/smt/boolean_terms.cpp
@@ -0,0 +1,254 @@
+/*********************                                                        */
+/*! \file boolean_terms.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "smt/boolean_terms.h"
+#include "smt/smt_engine.h"
+#include "theory/theory_engine.h"
+#include "theory/model.h"
+#include "expr/kind.h"
+#include <string>
+#include <algorithm>
+
+using namespace std;
+using namespace CVC4::theory;
+
+namespace CVC4 {
+namespace smt {
+
+const Datatype& BooleanTermConverter::booleanTermsConvertDatatype(const Datatype& dt) throw() {
+  return dt;
+  // boolean terms not supported in datatypes, yet
+
+  Debug("boolean-terms") << "booleanTermsConvertDatatype: considering " << dt.getName() << endl;
+  for(Datatype::const_iterator c = dt.begin(); c != dt.end(); ++c) {
+    TypeNode t = TypeNode::fromType((*c).getConstructor().getType());
+    for(TypeNode::const_iterator a = t.begin(); a != t.end(); ++a) {
+      if((*a).isBoolean()) {
+        Datatype newDt(dt.getName() + "'");
+        Debug("boolean-terms") << "found a Boolean arg in constructor " << (*c).getName() << endl;
+        for(c = dt.begin(); c != dt.end(); ++c) {
+          DatatypeConstructor ctor((*c).getName() + "'", (*c).getTesterName() + "'");
+          t = TypeNode::fromType((*c).getConstructor().getType());
+          for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
+            if((*a).getType().getRangeType().isBoolean()) {
+              ctor.addArg((*a).getName() + "'", NodeManager::currentNM()->mkBitVectorType(1).toType());
+            } else {
+              Type argType = (*a).getType().getRangeType();
+              if(argType.isDatatype() && DatatypeType(argType).getDatatype() == dt) {
+                ctor.addArg((*a).getName() + "'", DatatypeSelfType());
+              } else {
+                ctor.addArg((*a).getName() + "'", argType);
+              }
+            }
+          }
+          newDt.addConstructor(ctor);
+        }
+        DatatypeType newDtt = NodeManager::currentNM()->toExprManager()->mkDatatypeType(newDt);
+        const Datatype& newD = newDtt.getDatatype();
+        for(c = dt.begin(); c != dt.end(); ++c) {
+          Debug("boolean-terms") << "constructor " << (*c).getConstructor() << ":" << (*c).getConstructor().getType() << " made into " << newD[(*c).getName() + "'"].getConstructor() << ":" << newD[(*c).getName() + "'"].getConstructor().getType() << endl;
+          d_booleanTermCache[make_pair(Node::fromExpr((*c).getConstructor()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getConstructor());
+          d_booleanTermCache[make_pair(Node::fromExpr((*c).getTester()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getTester());
+          for(DatatypeConstructor::const_iterator a = (*c).begin(); a != (*c).end(); ++a) {
+            d_booleanTermCache[make_pair(Node::fromExpr((*a).getSelector()), false)] = Node::fromExpr(newD[(*c).getName() + "'"].getSelector((*a).getName() + "'"));
+          }
+        }
+        return newD;
+      }
+    }
+  }
+  return dt;
+}/* BooleanTermConverter::booleanTermsConvertDatatype() */
+
+Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw() {
+  Debug("boolean-terms") << "rewriteBooleanTerms: " << top << " - boolParent=" << boolParent << endl;
+
+  BooleanTermCache::iterator i = d_booleanTermCache.find(make_pair<Node, bool>(top, boolParent));
+  if(i != d_booleanTermCache.end()) {
+    return (*i).second.isNull() ? Node(top) : (*i).second;
+  }
+
+  Kind k = top.getKind();
+  kind::MetaKind mk = top.getMetaKind();
+
+  NodeManager* nm = NodeManager::currentNM();
+
+  if(!boolParent && top.getType().isBoolean()) {
+    Node one = nm->mkConst(BitVector(1u, 1u));
+    Node zero = nm->mkConst(BitVector(1u, 0u));
+    // still need to rewrite e.g. function applications over boolean
+    Node topRewritten = rewriteBooleanTerms(top, true);
+    Node n = nm->mkNode(kind::ITE, topRewritten, one, zero);
+    Debug("boolean-terms") << "constructed ITE: " << n << endl;
+    return n;
+  }
+
+  if(mk == kind::metakind::CONSTANT) {
+    Assert(k != kind::STORE_ALL, "array store-all not yet supported by Boolean-term conversion");
+    return top;
+  } else if(mk == kind::metakind::VARIABLE) {
+    TypeNode t = top.getType();
+    if(t.isFunction()) {
+      for(unsigned i = 0; i < t.getNumChildren() - 1; ++i) {
+        if(t[i].isBoolean()) {
+          vector<TypeNode> argTypes = t.getArgTypes();
+          replace(argTypes.begin(), argTypes.end(), t[i], nm->mkBitVectorType(1));
+          TypeNode newType = nm->mkFunctionType(argTypes, t.getRangeType());
+          Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()) + "_bt",
+                                newType, "a function introduced by Boolean-term conversion",
+                                NodeManager::SKOLEM_EXACT_NAME);
+          Debug("boolean-terms") << "constructed func: " << n << " of type " << newType << endl;
+          top.setAttribute(BooleanTermAttr(), n);
+          d_booleanTermCache[make_pair(top, boolParent)] = n;
+          return n;
+        }
+      }
+    } else if(t.isArray()) {
+      TypeNode indexType = t.getArrayIndexType();
+      TypeNode constituentType = t.getArrayConstituentType();
+      bool rewrite = false;
+      if(indexType.isBoolean()) {
+        indexType = nm->mkBitVectorType(1);
+        rewrite = true;
+      }
+      if(constituentType.isBoolean()) {
+        constituentType = nm->mkBitVectorType(1);
+        rewrite = true;
+      }
+      if(rewrite) {
+        TypeNode newType = nm->mkArrayType(indexType, constituentType);
+        Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
+                              newType, "an array variable introduced by Boolean-term conversion",
+                              NodeManager::SKOLEM_EXACT_NAME);
+        top.setAttribute(BooleanTermAttr(), n);
+        Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+        d_booleanTermCache[make_pair(top, boolParent)] = n;
+        return n;
+      }
+      d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+      return top;
+    } else if(t.isTuple()) {
+      return top;
+    } else if(t.isRecord()) {
+      return top;
+    } else if(t.isDatatype()) {
+      const Datatype& dt = t.getConst<Datatype>();
+      const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+      if(dt != dt2) {
+        Assert(d_booleanTermCache.find(make_pair(top, boolParent)) == d_booleanTermCache.end(),
+               "Node `%s' already in cache ?!", top.toString().c_str());
+        Assert(top.isVar());
+        TypeNode newType = TypeNode::fromType(dt2.getDatatypeType());
+        Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
+                              newType, "an array variable introduced by Boolean-term conversion",
+                              NodeManager::SKOLEM_EXACT_NAME);
+        top.setAttribute(BooleanTermAttr(), n);
+        Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+        d_booleanTermCache[make_pair(top, boolParent)] = n;
+        return n;
+      } else {
+        d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+        return top;
+      }
+    } else if(t.isConstructor()) {
+      Assert(!boolParent);
+      const Datatype& dt = t[t.getNumChildren() - 1].getConst<Datatype>();
+      const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+      if(dt != dt2) {
+        Assert(d_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(),
+               "constructor `%s' not in cache", top.toString().c_str());
+        return d_booleanTermCache[make_pair(top, boolParent)];
+      } else {
+        d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+        return top;
+      }
+    } else if(t.isTester() || t.isSelector()) {
+      Assert(!boolParent);
+      const Datatype& dt = t[0].getConst<Datatype>();
+      const Datatype& dt2 = booleanTermsConvertDatatype(dt);
+      if(dt != dt2) {
+        Assert(d_booleanTermCache.find(make_pair(top, boolParent)) != d_booleanTermCache.end(),
+               "tester or selector `%s' not in cache", top.toString().c_str());
+        return d_booleanTermCache[make_pair(top, boolParent)];
+      } else {
+        d_booleanTermCache[make_pair(top, boolParent)] = Node::null();
+        return top;
+      }
+    } else if(t.getNumChildren() > 0) {
+      for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
+        if((*i).isBoolean()) {
+          vector<TypeNode> argTypes(t.begin(), t.end());
+          replace(argTypes.begin(), argTypes.end(), *i, nm->mkBitVectorType(1));
+          TypeNode newType = nm->mkTypeNode(t.getKind(), argTypes);
+          Node n = nm->mkSkolem(top.getAttribute(expr::VarNameAttr()),
+                                newType, "a variable introduced by Boolean-term conversion",
+                                NodeManager::SKOLEM_EXACT_NAME);
+          Debug("boolean-terms") << "constructed: " << n << " of type " << newType << endl;
+          top.setAttribute(BooleanTermAttr(), n);
+          d_booleanTermCache[make_pair(top, boolParent)] = n;
+          return n;
+        }
+      }
+    }/* else if(t.isRecord()) {
+      Unimplemented();
+    }*/
+    return top;
+  }
+  switch(k) {
+  case kind::LAMBDA:
+  case kind::FORALL:
+  case kind::EXISTS:
+  case kind::REWRITE_RULE:
+  case kind::RR_REWRITE:
+  case kind::RR_REDUCTION:
+  case kind::RR_DEDUCTION:
+    //Assert(false, "not yet supported");
+    return top;
+
+  default:
+    NodeBuilder<> b(k);
+    Debug("bt") << "looking at: " << top << std::endl;
+    if(mk == kind::metakind::PARAMETERIZED) {
+      if(kindToTheoryId(k) != THEORY_BV &&
+         k != kind::TUPLE_SELECT &&
+         k != kind::TUPLE_UPDATE &&
+         k != kind::RECORD_SELECT &&
+         k != kind::RECORD_UPDATE &&
+         k != kind::RECORD) {
+        Debug("bt") << "rewriting: " << top.getOperator() << std::endl;
+        b << rewriteBooleanTerms(top.getOperator(), kindToTheoryId(k) == THEORY_BOOL);
+        Debug("bt") << "got: " << b.getOperator() << std::endl;
+      } else {
+        b << top.getOperator();
+      }
+    }
+    for(TNode::const_iterator i = top.begin(); i != top.end(); ++i) {
+      Debug("bt") << "rewriting: " << *i << std::endl;
+      b << rewriteBooleanTerms(*i, kindToTheoryId(k) == THEORY_BOOL);
+      Debug("bt") << "got: " << b[b.getNumChildren() - 1] << std::endl;
+    }
+    Node n = b;
+    Debug("boolean-terms") << "constructed: " << n << endl;
+    d_booleanTermCache[make_pair(top, boolParent)] = n;
+    return n;
+  }
+}/* BooleanTermConverter::rewriteBooleanTerms() */
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
diff --git a/src/smt/boolean_terms.h b/src/smt/boolean_terms.h
new file mode 100644
index 000000000..dea9adcf7
--- /dev/null
+++ b/src/smt/boolean_terms.h
@@ -0,0 +1,62 @@
+/*********************                                                        */
+/*! \file boolean_terms.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "expr/attribute.h"
+#include "expr/node.h"
+#include "util/hash.h"
+#include <utility>
+
+namespace CVC4 {
+namespace smt {
+
+namespace attr {
+  struct BooleanTermAttrTag { };
+}/* CVC4::smt::attr namespace */
+
+typedef expr::Attribute<attr::BooleanTermAttrTag, Node> BooleanTermAttr;
+
+class BooleanTermConverter {
+  /** The type of the Boolean term conversion cache */
+  typedef std::hash_map< std::pair<Node, bool>, Node,
+                         PairHashFunction< Node, bool,
+                                           NodeHashFunction, std::hash<int> > > BooleanTermCache;
+
+  /** The cache used during Boolean term conversion */
+  BooleanTermCache d_booleanTermCache;
+
+  /**
+   * Scan a datatype for and convert as necessary.
+   */
+  const Datatype& booleanTermsConvertDatatype(const Datatype& dt) throw();
+
+public:
+
+  /**
+   * We rewrite Boolean terms in assertions as bitvectors of length 1.
+   */
+  Node rewriteBooleanTerms(TNode n, bool boolParent = true) throw();
+
+};/* class BooleanTermConverter */
+
+}/* CVC4::smt namespace */
+}/* CVC4 namespace */
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 68b7222d7..a3065f29b 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -82,7 +82,7 @@ assertions\n\
 + Output the assertions after preprocessing and before clausification.\n\
   Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
   where PASS is one of the preprocessing passes: definition-expansion\n\
-  constrain-subtypes substitution skolem-quant simplify\n\
+  boolean-terms constrain-subtypes substitution skolem-quant simplify\n\
   static-learning ite-removal repeat-simplify theory-preprocessing.\n\
   PASS can also be the special value \"everything\", in which case the\n\
   assertions are printed before any preprocessing (with\n\
@@ -176,6 +176,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
       }
       if(!strcmp(p, "everything")) {
       } else if(!strcmp(p, "definition-expansion")) {
+      } else if(!strcmp(p, "boolean-terms")) {
       } else if(!strcmp(p, "constrain-subtypes")) {
       } else if(!strcmp(p, "substitution")) {
       } else if(!strcmp(p, "skolem-quant")) {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 07e3439fc..8e6fcccb8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -50,6 +50,7 @@
 #include "util/configuration.h"
 #include "util/exception.h"
 #include "smt/command_list.h"
+#include "smt/boolean_terms.h"
 #include "smt/options.h"
 #include "options/option_exception.h"
 #include "util/output.h"
@@ -105,6 +106,8 @@ public:
 struct SmtEngineStatistics {
   /** time spent in definition-expansion */
   TimerStat d_definitionExpansionTime;
+  /** time spent in Boolean term rewriting */
+  TimerStat d_rewriteBooleanTermsTime;
   /** time spent in non-clausal simplification */
   TimerStat d_nonclausalSimplificationTime;
   /** Num of constant propagations found during nonclausal simp */
@@ -130,6 +133,7 @@ struct SmtEngineStatistics {
 
   SmtEngineStatistics() :
     d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
+    d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"),
     d_nonclausalSimplificationTime("smt::SmtEngine::nonclausalSimplificationTime"),
     d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
     d_staticLearningTime("smt::SmtEngine::staticLearningTime"),
@@ -143,6 +147,7 @@ struct SmtEngineStatistics {
     d_checkModelTime("smt::SmtEngine::checkModelTime") {
 
     StatisticsRegistry::registerStat(&d_definitionExpansionTime);
+    StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime);
     StatisticsRegistry::registerStat(&d_nonclausalSimplificationTime);
     StatisticsRegistry::registerStat(&d_numConstantProps);
     StatisticsRegistry::registerStat(&d_staticLearningTime);
@@ -158,6 +163,7 @@ struct SmtEngineStatistics {
 
   ~SmtEngineStatistics() {
     StatisticsRegistry::unregisterStat(&d_definitionExpansionTime);
+    StatisticsRegistry::unregisterStat(&d_rewriteBooleanTermsTime);
     StatisticsRegistry::unregisterStat(&d_nonclausalSimplificationTime);
     StatisticsRegistry::unregisterStat(&d_numConstantProps);
     StatisticsRegistry::unregisterStat(&d_staticLearningTime);
@@ -198,6 +204,9 @@ class SmtEnginePrivate : public NodeManagerListener {
   /** Size of assertions array when preprocessing starts */
   unsigned d_realAssertionsEnd;
 
+  /** The converter for Boolean terms -> BITVECTOR(1). */
+  BooleanTermConverter d_booleanTermConverter;
+
   /** A circuit propagator for non-clausal propositional deduction */
   booleans::CircuitPropagator d_propagator;
 
@@ -334,6 +343,7 @@ public:
     d_assertionsToPreprocess(),
     d_nonClausalLearnedLiterals(),
     d_realAssertionsEnd(0),
+    d_booleanTermConverter(),
     d_propagator(d_nonClausalLearnedLiterals, true, true),
     d_assertionsToCheck(),
     d_fakeContext(),
@@ -951,6 +961,13 @@ void SmtEngine::setLogicInternal() throw() {
       setOption("check-models", SExpr("false"));
     }
   }
+
+  // may need to force BV on to handle Boolean terms
+  if(!d_logic.isPure(theory::THEORY_ARITH)) {
+    d_logic = d_logic.getUnlockedCopy();
+    d_logic.enableTheory(theory::THEORY_BV);
+    d_logic.lock();
+  }
 }
 
 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
@@ -2063,6 +2080,20 @@ void SmtEnginePrivate::processAssertions() {
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
   Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
 
+  dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess);
+  {
+    Chat() << "rewriting Boolean terms..." << endl;
+    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteBooleanTermsTime);
+    for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
+      d_assertionsToPreprocess[i] =
+        d_booleanTermConverter.rewriteBooleanTerms(d_assertionsToPreprocess[i]);
+    }
+  }
+  dumpAssertions("post-boolean-terms", d_assertionsToPreprocess);
+
+  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
+  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+
   dumpAssertions("pre-constrain-subtypes", d_assertionsToPreprocess);
   {
     // Any variables of subtype types need to be constrained properly.