Adding support for bool-to-bv

Squashed commit of the following:

commit 5197a663eb262afbeb7740f53b5bd27479dccea0
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Mon Mar 6 00:16:16 2017 -0800

    Remove IFF case

commit 2119b25a30ed42eca54f632e7232c9f76ae5755a
Author: guykatzz <katz911@gmail.com>
Date:   Mon Feb 20 12:37:06 2017 -0800

    proof support for bvcomp

commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Fri Feb 17 21:09:04 2017 -0800

    Added missing cases to operator<< for bv rewrite rules.

commit 0ed797c31d0e66cadc35b2397716c841d1aff270
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Fri Feb 17 11:43:51 2017 -0800

    Added rewrite rules for new bitvector kinds.

commit 3b23dffb317de5559f8a95118fef633f711c114a
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Mon Feb 13 14:41:49 2017 -0800

    First draft of bool-to-bv pass.

1 files changed, 122 insertions, 1 deletions

diff --git a/src/theory/bv/bv_to_bool.cpp b/src/theory/bv/bv_to_bool.cpp
index b38352b77..5b7fe160c 100644
--- a/src/theory/bv/bv_to_bool.cpp
+++ b/src/theory/bv/bv_to_bool.cpp
@@ -226,7 +226,6 @@ Node BvToBoolPreprocessor::liftNode(TNode current) {
   return result; 
 }
 
-
 void BvToBoolPreprocessor::liftBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
   for (unsigned i = 0; i < assertions.size(); ++i) {
     Node new_assertion = liftNode(assertions[i]);
@@ -239,14 +238,136 @@ BvToBoolPreprocessor::Statistics::Statistics()
   : d_numTermsLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsLifted", 0)
   , d_numAtomsLifted("theory::bv::BvToBoolPreprocess::NumberOfAtomsLifted", 0)
   , d_numTermsForcedLifted("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLifted", 0)
+  , d_numTermsLowered("theory::bv::BvToBoolPreprocess::NumberOfTermsLowered", 0)
+  , d_numAtomsLowered("theory::bv::BvToBoolPreprocess::NumberOfAtomsLowered", 0)    
+  , d_numTermsForcedLowered("theory::bv::BvToBoolPreprocess::NumberOfTermsForcedLowered", 0)
 {
   smtStatisticsRegistry()->registerStat(&d_numTermsLifted);
   smtStatisticsRegistry()->registerStat(&d_numAtomsLifted);
   smtStatisticsRegistry()->registerStat(&d_numTermsForcedLifted);
+  smtStatisticsRegistry()->registerStat(&d_numTermsLowered);
+  smtStatisticsRegistry()->registerStat(&d_numAtomsLowered);
+  smtStatisticsRegistry()->registerStat(&d_numTermsForcedLowered);
 }
 
 BvToBoolPreprocessor::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&d_numTermsLifted);
   smtStatisticsRegistry()->unregisterStat(&d_numAtomsLifted);
   smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLifted);
+  smtStatisticsRegistry()->unregisterStat(&d_numTermsLowered);
+  smtStatisticsRegistry()->unregisterStat(&d_numAtomsLowered);
+  smtStatisticsRegistry()->unregisterStat(&d_numTermsForcedLowered);
+}
+
+void BvToBoolPreprocessor::addToLowerCache(TNode term, Node new_term) {
+  Assert (new_term != Node());
+  Assert (!hasLowerCache(term));
+  d_lowerCache[term] = new_term; 
+}
+
+Node BvToBoolPreprocessor::getLowerCache(TNode term) const {
+  Assert(hasLowerCache(term)); 
+  return d_lowerCache.find(term)->second; 
+}
+
+bool BvToBoolPreprocessor::hasLowerCache(TNode term) const {
+  return d_lowerCache.find(term) != d_lowerCache.end(); 
+}
+
+Node BvToBoolPreprocessor::lowerNode(TNode current, bool topLevel) {
+  Node result;
+  if (hasLowerCache(current)) {
+    result = getLowerCache(current); 
+  } else {
+    if (current.getNumChildren() == 0) {
+      if (current.getKind() == kind::CONST_BOOLEAN) {
+        result = (current == utils::mkTrue()) ? d_one : d_zero;
+      } else {
+        result = current;
+      }
+    } else {
+      Kind kind = current.getKind();
+      Kind new_kind = kind;
+      switch(kind) {
+        case kind::EQUAL:
+          new_kind = kind::BITVECTOR_COMP;
+          break;
+        case kind::AND:
+          new_kind = kind::BITVECTOR_AND;
+          break;
+        case kind::OR:
+          new_kind = kind::BITVECTOR_OR;
+          break;
+        case kind::NOT:
+          new_kind = kind::BITVECTOR_NOT;
+          break;
+        case kind::XOR:
+          new_kind = kind::BITVECTOR_XOR;
+          break;
+        case kind::ITE:
+          if (current.getType().isBitVector() || current.getType().isBoolean()) {
+            new_kind = kind::BITVECTOR_ITE;
+          }
+          break;
+        case kind::BITVECTOR_ULT:
+          new_kind = kind::BITVECTOR_ULTBV;
+          break;
+        case kind::BITVECTOR_SLT:
+          new_kind = kind::BITVECTOR_SLTBV;
+          break;
+        case kind::BITVECTOR_ULE:
+        case kind::BITVECTOR_UGT:
+        case kind::BITVECTOR_UGE:
+        case kind::BITVECTOR_SLE:
+        case kind::BITVECTOR_SGT:
+        case kind::BITVECTOR_SGE:
+          // Should have been removed by rewriting.
+          Unreachable();
+        default:
+          break;
+      }
+      NodeBuilder<> builder(new_kind);
+      if (kind != new_kind) {
+        ++(d_statistics.d_numTermsLowered);
+      }
+      if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+        builder << current.getOperator();
+      }
+      Node converted;
+      if (new_kind == kind::ITE) {
+        // Special-case ITE because need condition to be Boolean.
+        converted = lowerNode(current[0], true);
+        builder << converted;
+        converted = lowerNode(current[1]);
+        builder << converted;
+        converted = lowerNode(current[2]);
+        builder << converted;
+      } else {
+        for (unsigned i = 0; i < current.getNumChildren(); ++i) {
+          converted = lowerNode(current[i]);
+          builder << converted; 
+        }
+      }
+      result = builder;
+    }
+    if (result.getType().isBoolean()) {
+      ++(d_statistics.d_numTermsForcedLowered);
+      result = utils::mkNode(kind::ITE, result, d_one, d_zero);
+    }
+    addToLowerCache(current, result);
+  }
+  if (topLevel) {
+    result = utils::mkNode(kind::EQUAL, result, d_one);
+  }
+  Assert (result != Node());
+  Debug("bool-to-bv") << "BvToBoolPreprocessor::lowerNode " << current << " => \n" << result << "\n"; 
+  return result; 
+}
+
+void BvToBoolPreprocessor::lowerBoolToBv(const std::vector<Node>& assertions, std::vector<Node>& new_assertions) {
+  for (unsigned i = 0; i < assertions.size(); ++i) {
+    Node new_assertion = lowerNode(assertions[i], true);
+    new_assertions.push_back(new_assertion);
+    Trace("bool-to-bv") << "  " << assertions[i] <<" => " << new_assertions[i] <<"\n"; 
+  }
 }