merge from arrays-clark branch

7 files changed, 386 insertions, 40 deletions

diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp
index edaf8c154..b579122e5 100644
--- a/src/theory/bv/bitblast_strategies.cpp
+++ b/src/theory/bv/bitblast_strategies.cpp
@@ -338,7 +338,7 @@ void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb) {
 }
 
 void DefaultVarBB (TNode node, Bits& bits, Bitblaster* bb) {
-  Assert (node.getKind() == kind::VARIABLE);
+  //  Assert (node.getKind() == kind::VARIABLE);
   Assert(bits.size() == 0);
   
   for (unsigned i = 0; i < utils::getSize(node); ++i) {
diff --git a/src/theory/bv/bv_sat.cpp b/src/theory/bv/bv_sat.cpp
index f5c43688a..2f4ac1324 100644
--- a/src/theory/bv/bv_sat.cpp
+++ b/src/theory/bv/bv_sat.cpp
@@ -83,6 +83,9 @@ void Bitblaster::bbAtom(TNode node) {
     return; 
   }
 
+  // make sure it is marked as an atom
+  addAtom(node); 
+
   BVDebug("bitvector-bitblast") << "Bitblasting node " << node <<"\n"; 
   ++d_statistics.d_numAtoms;
   // the bitblasted definition of the atom
@@ -298,12 +301,14 @@ void Bitblaster::initAtomBBStrategies() {
 }
 
 void Bitblaster::initTermBBStrategies() {
+  // Changed this to DefaultVarBB because any foreign kind should be treated as a variable
+  // TODO: check this is OK
   for (int i = 0 ; i < kind::LAST_KIND; ++i ) {
-    d_termBBStrategies[i] = UndefinedTermBBStrategy; 
+    d_termBBStrategies[i] = DefaultVarBB;
   }
   
   /// setting default bb strategies for terms:
-  d_termBBStrategies [ kind::VARIABLE ]               = DefaultVarBB;
+  //  d_termBBStrategies [ kind::VARIABLE ]               = DefaultVarBB;
   d_termBBStrategies [ kind::CONST_BITVECTOR ]        = DefaultConstBB;
   d_termBBStrategies [ kind::BITVECTOR_NOT ]          = DefaultNotBB;
   d_termBBStrategies [ kind::BITVECTOR_CONCAT ]       = DefaultConcatBB;
diff --git a/src/theory/bv/bv_sat.h b/src/theory/bv/bv_sat.h
index 647e4fe9f..2422da0b7 100644
--- a/src/theory/bv/bv_sat.h
+++ b/src/theory/bv/bv_sat.h
@@ -82,7 +82,9 @@ class Bitblaster {
                                                        currently asserted by the DPLL SAT solver. */
 
   /// helper methods
+  public:
   bool          hasBBAtom(TNode node);    
+  private:
   bool          hasBBTerm(TNode node); 
   void          getBBTerm(TNode node, Bits& bits);
 
@@ -101,6 +103,7 @@ class Bitblaster {
   Node bbOptimize(TNode node); 
   
   void bbAtom(TNode node);
+  void addAtom(TNode atom); 
   // division is bitblasted in terms of constraints
   // so it needs to use private bitblaster interface
   void bbUdiv(TNode node, Bits& bits);
@@ -116,7 +119,7 @@ public:
   bool solve(bool quick_solve = false);
   void bitblast(TNode node);
   void getConflict(std::vector<TNode>& conflict); 
-  void addAtom(TNode atom); 
+
   bool getPropagations(std::vector<TNode>& propagations);
   void explainPropagation(TNode atom, std::vector<Node>& explanation);
 private:
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 429e5ff19..a3f4364ba 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -20,8 +20,8 @@
 #include "theory/bv/theory_bv.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/valuation.h"
-
 #include "theory/bv/bv_sat.h"
+#include "theory/uf/equality_engine_impl.h"
 
 using namespace CVC4;
 using namespace CVC4::theory;
@@ -31,16 +31,67 @@ using namespace CVC4::context;
 using namespace std;
 using namespace CVC4::theory::bv::utils;
 
+
+const bool d_useEqualityEngine = true;
+const bool d_useSatPropagation = true;
+
+
 TheoryBV::TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation)
   : Theory(THEORY_BV, c, u, out, valuation),
     d_context(c),
     d_assertions(c),
     d_bitblaster(new Bitblaster(c) ),
     d_statistics(),
-    d_alreadyPropagatedSet(c)
-   {
+    d_alreadyPropagatedSet(c),
+    d_notify(*this),
+    d_equalityEngine(d_notify, c, "theory::bv::TheoryBV"),
+    d_conflict(c, false),
+    d_literalsToPropagate(c),
+    d_literalsToPropagateIndex(c, 0),
+    d_toBitBlast(c)
+  {
     d_true = utils::mkTrue();
+    d_false = utils::mkFalse();
+
+    if (d_useEqualityEngine) {
+      d_equalityEngine.addTerm(d_true);
+      d_equalityEngine.addTerm(d_false);
+      d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
+
+      // The kinds we are treating as function application in congruence
+      d_equalityEngine.addFunctionKind(kind::BITVECTOR_CONCAT);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_AND);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_OR);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XOR);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOT);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NAND);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NOR);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_XNOR);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_COMP);
+      d_equalityEngine.addFunctionKind(kind::BITVECTOR_MULT);
+      d_equalityEngine.addFunctionKind(kind::BITVECTOR_PLUS);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SUB);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_NEG);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UDIV);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UREM);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SDIV);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SREM);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SMOD);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SHL);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_LSHR);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ASHR);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULT);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_ULE);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGT);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_UGE);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLT);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SLE);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGT);
+      //    d_equalityEngine.addFunctionKind(kind::BITVECTOR_SGE);
+
+    }
   }
+
 TheoryBV::~TheoryBV() {
   delete d_bitblaster; 
 }
@@ -68,32 +119,99 @@ void TheoryBV::preRegisterTerm(TNode node) {
       node.getKind() == kind::BITVECTOR_SLT ||
       node.getKind() == kind::BITVECTOR_SLE) {
     d_bitblaster->bitblast(node);
-    d_bitblaster->addAtom(node); 
   }
+
+  if (d_useEqualityEngine) {
+    switch (node.getKind()) {
+      case kind::EQUAL:
+        // Add the terms
+        d_equalityEngine.addTerm(node);
+        // Add the trigger for equality
+        d_equalityEngine.addTriggerEquality(node[0], node[1], node);
+        d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode());
+        break;
+      default:
+        d_equalityEngine.addTerm(node);
+        break;
+    }
+  }
+
 }
 
-void TheoryBV::check(Effort e) {
-  BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
+void TheoryBV::check(Effort e)
+{
+  BVDebug("bitvector") << "TheoryBV::check " << e << "\n"; 
   BVDebug("bitvector")<< "TheoryBV::check(" << e << ")" << std::endl;
-  while (!done()) {
-    TNode assertion = get();
-    // make sure we do not assert things we propagated
-    if (!hasBeenPropagated(assertion)) {
-      BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << assertion << "\n";
-      bool ok = d_bitblaster->assertToSat(assertion, true);
+  while (!done() && !d_conflict) {
+    Assertion assertion = get();
+    TNode fact = assertion.assertion;
+
+    BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; 
+
+    // If the assertion doesn't have a literal, it's a shared equality
+    bool shared = !assertion.isPreregistered;
+    Assert(!d_useEqualityEngine || !shared ||
+           ((fact.getKind() == kind::EQUAL && d_equalityEngine.hasTerm(fact[0]) && d_equalityEngine.hasTerm(fact[1])) ||
+            (fact.getKind() == kind::NOT && fact[0].getKind() == kind::EQUAL &&
+             d_equalityEngine.hasTerm(fact[0][0]) && d_equalityEngine.hasTerm(fact[0][1]))));
+
+    // Notify the Equality Engine
+    switch (fact.getKind()) {
+      case kind::EQUAL:
+        if (d_useEqualityEngine) {
+          d_equalityEngine.addEquality(fact[0], fact[1], fact);
+        }
+        if (shared && !d_bitblaster->hasBBAtom(fact)) {
+          d_bitblaster->bitblast(fact);
+        }
+        break;
+      case kind::NOT:
+        if (fact[0].getKind() == kind::EQUAL) {
+          // Assert the dis-equality
+          if (d_useEqualityEngine) {
+            d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
+          }
+          if (shared && !d_bitblaster->hasBBAtom(fact[0])) {
+            d_bitblaster->bitblast(fact[0]);
+          }
+        } else {
+          if (d_useEqualityEngine) {
+            d_equalityEngine.addPredicate(fact[0], false, fact);
+          }
+          break;
+        }
+        break;
+      default:
+        if (d_useEqualityEngine) {
+          d_equalityEngine.addPredicate(fact, true, fact);
+        }
+        break;
+    }
+
+    // make sure we do not assert things we propagated 
+    if (!d_conflict && d_alreadyPropagatedSet.count(fact) == 0) {
+      bool ok = d_bitblaster->assertToSat(fact, d_useSatPropagation);
       if (!ok) {
         std::vector<TNode> conflictAtoms;
         d_bitblaster->getConflict(conflictAtoms);
         d_statistics.d_avgConflictSize.addEntry(conflictAtoms.size());
-        Node conflict = mkConjunction(conflictAtoms);
-        d_out->conflict(conflict);
-        BVDebug("bitvector") << "TheoryBV::check returns conflict: " <<conflict <<" \n ";
-        return;
+        d_conflict = true;
+        d_conflictNode = mkConjunction(conflictAtoms);
+        break;
       }
     }
   }
 
+  // If in conflict, output the conflict
+  if (d_conflict) {
+    Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::check(): conflict " << d_conflictNode << std::endl;
+    d_out->conflict(d_conflictNode);
+    return;
+  }
+
   if (e == EFFORT_FULL) {
+
+    Assert(done() && !d_conflict);
     BVDebug("bitvector") << "TheoryBV::check " << e << "\n";
     // in standard effort we only do boolean constraint propagation 
     bool ok = d_bitblaster->solve(false);
@@ -127,12 +245,36 @@ Node TheoryBV::getValue(TNode n) {
   }
 }
 
-bool TheoryBV::hasBeenPropagated(TNode node) {
-  return d_alreadyPropagatedSet.count(node); 
-}
 
 void TheoryBV::propagate(Effort e) {
-  BVDebug("bitvector") << "TheoryBV::propagate() \n";
+  BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate()" << std::endl;
+
+  if (d_conflict) {
+    return;
+  }
+
+  // get new propagations from the equality engine
+  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
+    TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
+    BVDebug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): propagating from equality engine: " << literal << std::endl;
+    bool satValue;
+    Node normalized = Rewriter::rewrite(literal);
+    if (!d_valuation.hasSatValue(normalized, satValue) || satValue) {
+      d_out->propagate(literal);
+    } else {
+      Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(): in conflict, normalized = " << normalized << std::endl;
+      Node negatedLiteral;
+      std::vector<TNode> assumptions;
+      if (normalized != d_false) {
+        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+        assumptions.push_back(negatedLiteral);
+      }
+      explain(literal, assumptions);
+      d_conflictNode = mkAnd(assumptions);
+      d_conflict = true;
+      return;
+    }
+  }
 
   // get new propagations from the sat solver
   std::vector<TNode> propagations; 
@@ -142,6 +284,10 @@ void TheoryBV::propagate(Effort e) {
   for (unsigned i = 0; i < propagations.size(); ++ i) {
     TNode node = propagations[i];
     BVDebug("bitvector") << "TheoryBV::propagate    " << node <<" \n";
+    if (!d_valuation.isSatLiteral(node)) {
+      // TODO: maybe propagate shared terms too?
+      continue;
+    }
     if (d_valuation.getSatValue(node) == Node::null()) {
       vector<Node> explanation;
       d_bitblaster->explainPropagation(node, explanation);
@@ -162,21 +308,21 @@ void TheoryBV::propagate(Effort e) {
 
 }
 
-Node TheoryBV::explain(TNode n) {
-  BVDebug("bitvector") << "TheoryBV::explain node " <<  n <<"\n";
-  std::vector<Node> explanation;
-  d_bitblaster->explainPropagation(n, explanation);
-  Node exp;
+// Node TheoryBV::explain(TNode n) {
+//   BVDebug("bitvector") << "TheoryBV::explain node " <<  n <<"\n";
+//   std::vector<Node> explanation;
+//   d_bitblaster->explainPropagation(n, explanation);
+//   Node exp;
 
-  if (explanation.size() == 0) {
-    return utils::mkTrue(); 
-  }
+//   if (explanation.size() == 0) {
+//     return utils::mkTrue(); 
+//   }
   
-  exp = utils::mkAnd(explanation);
+//   exp = utils::mkAnd(explanation);
   
-  BVDebug("bitvector") << "TheoryBV::explain with " <<  exp <<"\n";
-  return exp;
-}
+//   BVDebug("bitvector") << "TheoryBV::explain with " <<  exp <<"\n";
+//   return exp;
+// }
 
 Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitutions) {
   switch(in.getKind()) {
@@ -203,3 +349,108 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
   }
   return PP_ASSERT_STATUS_UNSOLVED;
 }
+
+
+bool TheoryBV::propagate(TNode literal)
+{
+  Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal  << ")" << std::endl;
+
+  // If already in conflict, no more propagation
+  if (d_conflict) {
+    Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << "): already in conflict" << std::endl;
+    return false;
+  }
+
+  // See if the literal has been asserted already
+  Node normalized = Rewriter::rewrite(literal);
+  bool satValue = false;
+  bool isAsserted = normalized == d_false || d_valuation.hasSatValue(normalized, satValue);
+
+  // If asserted, we might be in conflict
+  if (isAsserted) {
+    if (!satValue) {
+      Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
+      std::vector<TNode> assumptions;
+      Node negatedLiteral;
+      if (normalized != d_false) {
+        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+        assumptions.push_back(negatedLiteral);
+      }
+      explain(literal, assumptions);
+      d_conflictNode = mkAnd(assumptions);
+      d_conflict = true;
+      return false;
+    }
+    // Propagate even if already known in SAT - could be a new equation between shared terms
+    // (terms that weren't shared when the literal was asserted!)
+  }
+
+  // Nothing, just enqueue it for propagation and mark it as asserted already
+  Debug("bitvector") << spaces(getContext()->getLevel()) << "TheoryBV::propagate(" << literal << ") => enqueuing for propagation" << std::endl;
+  d_literalsToPropagate.push_back(literal);
+
+  return true;
+}/* TheoryBV::propagate(TNode) */
+
+
+void TheoryBV::explain(TNode literal, std::vector<TNode>& assumptions) {
+  TNode lhs, rhs;
+  switch (literal.getKind()) {
+    case kind::EQUAL:
+      lhs = literal[0];
+      rhs = literal[1];
+      break;
+    case kind::NOT:
+      if (literal[0].getKind() == kind::EQUAL) {
+        // Disequalities
+        d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
+        return;
+      } else {
+        // Predicates
+        lhs = literal[0];
+        rhs = d_false;
+        break;
+      }
+    case kind::CONST_BOOLEAN:
+      // we get to explain true = false, since we set false to be the trigger of this
+      lhs = d_true;
+      rhs = d_false;
+      break;
+    default:
+      Unreachable();
+  }
+  d_equalityEngine.explainEquality(lhs, rhs, assumptions);
+}
+
+
+Node TheoryBV::explain(TNode node) {
+  BVDebug("bitvector") << "TheoryBV::explain(" << node << ")" << std::endl;
+  std::vector<TNode> assumptions;
+  explain(node, assumptions);
+  return mkAnd(assumptions);
+}
+
+
+void TheoryBV::addSharedTerm(TNode t) {
+  Debug("bitvector::sharing") << spaces(getContext()->getLevel()) << "TheoryBV::addSharedTerm(" << t << ")" << std::endl;
+  if (d_useEqualityEngine) {
+    d_equalityEngine.addTriggerTerm(t);
+  }
+}
+
+
+EqualityStatus TheoryBV::getEqualityStatus(TNode a, TNode b)
+{
+  if (d_useEqualityEngine) {
+    if (d_equalityEngine.areEqual(a, b)) {
+      // The terms are implied to be equal
+      return EQUALITY_TRUE;
+    }
+    if (d_equalityEngine.areDisequal(a, b)) {
+      // The terms are implied to be dis-equal
+      return EQUALITY_FALSE;
+    }
+  }
+  return EQUALITY_UNKNOWN;
+}
+
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index d147c8bb5..940eaef56 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -27,6 +27,8 @@
 #include "context/cdhashset.h"
 #include "theory/bv/theory_bv_utils.h"
 #include "util/stats.h"
+#include "theory/uf/equality_engine.h"
+#include "context/cdqueue.h"
 
 namespace BVMinisat {
 class SimpSolver; 
@@ -40,6 +42,12 @@ namespace bv {
 /// forward declarations 
 class Bitblaster;
 
+static inline std::string spaces(int level)
+{
+  std::string indentStr(level, ' ');
+  return indentStr;
+}
+
 class TheoryBV : public Theory {
 
 
@@ -54,11 +62,11 @@ private:
   /** Bitblaster */
   Bitblaster* d_bitblaster; 
   Node d_true;
-
+  Node d_false;
+    
   /** Context dependent set of atoms we already propagated */
   context::CDHashSet<TNode, TNodeHashFunction> d_alreadyPropagatedSet;
 
-  bool hasBeenPropagated(TNode node); 
 public:
 
   TheoryBV(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation);
@@ -70,8 +78,6 @@ public:
 
   void check(Effort e);
 
-  void propagate(Effort e);
-
   Node explain(TNode n);
 
   Node getValue(TNode n);
@@ -93,6 +99,61 @@ private:
   
   Statistics d_statistics;
   
+  // Added by Clark
+  // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
+  class NotifyClass {
+    TheoryBV& d_bv;
+  public:
+    NotifyClass(TheoryBV& uf): d_bv(uf) {}
+
+    bool notify(TNode propagation) {
+      Debug("bitvector") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
+      // Just forward to bv
+      return d_bv.propagate(propagation);
+    }
+
+    void notify(TNode t1, TNode t2) {
+      Debug("arrays") << spaces(d_bv.getContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+      // Propagate equality between shared terms
+      Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
+      d_bv.propagate(t1.eqNode(t2));
+    }
+  };
+
+  /** The notify class for d_equalityEngine */
+  NotifyClass d_notify;
+
+  /** Equaltity engine */
+  uf::EqualityEngine<NotifyClass> d_equalityEngine;
+
+  // Are we in conflict?
+  context::CDO<bool> d_conflict;
+
+  /** The conflict node */
+  Node d_conflictNode;
+
+  /** Literals to propagate */
+  context::CDList<Node> d_literalsToPropagate;
+
+  /** Index of the next literal to propagate */
+  context::CDO<unsigned> d_literalsToPropagateIndex;
+
+  context::CDQueue<Node> d_toBitBlast;
+
+  /** Should be called to propagate the literal.  */
+  bool propagate(TNode literal);
+
+  /** Explain why this literal is true by adding assumptions */
+  void explain(TNode literal, std::vector<TNode>& assumptions);
+
+  void addSharedTerm(TNode t);
+
+  EqualityStatus getEqualityStatus(TNode a, TNode b);
+
+public:
+
+  void propagate(Effort e);
+  
 };/* class TheoryBV */
 
 }/* CVC4::theory::bv namespace */
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index cf8310e5a..530949de2 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -866,6 +866,9 @@ Node RewriteRule<UremPow2>::apply(Node node) {
   BVDebug("bv-rewrite") << "RewriteRule<UremPow2>(" << node << ")" << std::endl;
   TNode a = node[0];
   unsigned power = utils::isPow2Const(node[1]) - 1;
+  if (power == 0) {
+    return utils::mkConst(utils::getSize(node), 0);
+  }
   Node extract = utils::mkExtract(a, power - 1, 0);
   Node zeros = utils::mkConst(utils::getSize(node) - power, 0);
   return utils::mkNode(kind::BITVECTOR_CONCAT, zeros, extract); 
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 8b5dd0499..38547ad99 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -344,6 +344,29 @@ inline Node mkConjunction(const std::vector<TNode>& nodes) {
 }
 
 
+inline Node mkAnd(const std::vector<TNode>& conjunctions) {
+  Assert(conjunctions.size() > 0);
+
+  std::set<TNode> all;
+  all.insert(conjunctions.begin(), conjunctions.end());
+
+  if (all.size() == 1) {
+    // All the same, or just one
+    return conjunctions[0];
+  }
+
+  NodeBuilder<> conjunction(kind::AND);
+  std::set<TNode>::const_iterator it = all.begin();
+  std::set<TNode>::const_iterator it_end = all.end();
+  while (it != it_end) {
+    conjunction << *it;
+    ++ it;
+  }
+
+  return conjunction;
+}/* mkAnd() */
+
+
 // Turn a set into a string
 inline std::string setToString(const std::set<TNode>& nodeSet) {
   std::stringstream out;