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, 44 insertions, 0 deletions

diff --git a/src/theory/bv/bitblast_strategies_template.h b/src/theory/bv/bitblast_strategies_template.h
index 48221aad4..3a9106984 100644
--- a/src/theory/bv/bitblast_strategies_template.h
+++ b/src/theory/bv/bitblast_strategies_template.h
@@ -740,6 +740,50 @@ void DefaultAshrBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
 }
 
 template <class T>
+void DefaultUltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_ULTBV);
+  std::vector<T> a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+  Assert(a.size() == b.size());
+  
+  // construct bitwise comparison 
+  res.push_back(uLessThanBB(a, b, false));
+}
+
+template <class T>
+void DefaultSltbvBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_SLTBV);
+  std::vector<T> a, b;
+  bb->bbTerm(node[0], a);
+  bb->bbTerm(node[1], b);
+  Assert(a.size() == b.size());
+  
+  // construct bitwise comparison 
+  res.push_back(sLessThanBB(a, b, false));
+}
+
+template <class T>
+void DefaultIteBB (TNode node, std::vector<T>& res, TBitblaster<T>* bb) {
+  Debug("bitvector-bb") << "Bitblasting node " << node  << "\n";
+  Assert(node.getKind() == kind::BITVECTOR_ITE);
+  std::vector<T> cond, thenpart, elsepart;
+  bb->bbTerm(node[0], cond);
+  bb->bbTerm(node[1], thenpart);
+  bb->bbTerm(node[2], elsepart);
+  
+  Assert(cond.size() == 1);
+  Assert(thenpart.size() == elsepart.size());
+
+  for (unsigned i = 0; i < thenpart.size(); ++i) {
+    // (~cond OR thenpart) AND (cond OR elsepart)
+    res.push_back(mkAnd(mkOr(mkNot(cond[0]),thenpart[i]),mkOr(cond[0],elsepart[i])));
+  }
+}
+
+template <class T>
 void DefaultExtractBB (TNode node, std::vector<T>& bits, TBitblaster<T>* bb) {
   Assert (node.getKind() == kind::BITVECTOR_EXTRACT);
   Assert(bits.size() == 0);