Fixes lots of problems in bv rewrite rules and adds lots of assertions

to catch any that I may have missed

9 files changed, 220 insertions, 232 deletions

diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 76c4f0abc..e4a25e008 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -483,18 +483,33 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       op << "@";
       opType = INFIX;
       break;
-    case kind::BITVECTOR_PLUS:
+    case kind::BITVECTOR_PLUS: {
       //This interprets a BITVECTOR_PLUS as a bvadd in SMT-LIB
-      out << "BVPLUS(";
       Assert(n.getType().isBitVector());
+      unsigned numc = n.getNumChildren()-2;
+      unsigned child = 0;
+      while (child < numc) {
+        out << "BVPLUS(";
+        out << BitVectorType(n.getType().toType()).getSize();
+        out << ',';
+        toStream(out, n[child], depth, types, false);
+        out << ',';
+        ++child;
+      }
+      out << "BVPLUS(";
       out << BitVectorType(n.getType().toType()).getSize();
       out << ',';
-      toStream(out, n[0], depth, types, false);
-      out << ',';
-      toStream(out, n[1], depth, types, false);
+      toStream(out, n[child], depth, types, false);
+      out << ',';        
+      toStream(out, n[child+1], depth, types, false);
+      while (child > 0) {
+        out << ')';
+        --child;
+      }
       out << ')';
       return;
       break;
+    }
     case kind::BITVECTOR_SUB:
       out << "BVSUB(";
       Assert(n.getType().isBitVector());
@@ -506,17 +521,32 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo
       out << ')';
       return;
       break;
-    case kind::BITVECTOR_MULT:
-      out << "BVMULT(";
+    case kind::BITVECTOR_MULT: {
       Assert(n.getType().isBitVector());
+      unsigned numc = n.getNumChildren()-2;
+      unsigned child = 0;
+      while (child < numc) {
+        out << "BVMULT(";
+        out << BitVectorType(n.getType().toType()).getSize();
+        out << ',';
+        toStream(out, n[child], depth, types, false);
+        out << ',';
+        ++child;
+        }
+      out << "BVMULT(";
       out << BitVectorType(n.getType().toType()).getSize();
       out << ',';
-      toStream(out, n[0], depth, types, false);
-      out << ',';
-      toStream(out, n[1], depth, types, false);
+      toStream(out, n[child], depth, types, false);
+      out << ',';        
+      toStream(out, n[child+1], depth, types, false);
+      while (child > 0) {
+        out << ')';
+        --child;
+      }
       out << ')';
       return;
       break;
+    }
     case kind::BITVECTOR_EXTRACT:
       op << n.getOperator().getConst<BitVectorExtract>();
       opType = POSTFIX;
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 247d66d89..761c11e3d 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -65,7 +65,7 @@ public:
   std::string identify() const { return std::string("TheoryBV"); }
 
   PPAssertStatus ppAssert(TNode in, SubstitutionMap& outSubstitutions);
-  Node ppRewrite(TNode atom);
+  Node ppRewrite(TNode t);
 
 private:
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
index 620d33aea..2fd409313 100644
--- a/src/theory/bv/theory_bv_rewrite_rules.h
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -118,12 +118,7 @@ enum RewriteRuleId {
   UleMax,
   NotUlt,
   NotUle,
-  MultOne,
-  MultZero,
   MultPow2,
-  PlusZero,
-  PlusSelf,
-  PlusNegSelf,
   NegIdemp,
   UdivPow2,
   UdivOne,
@@ -242,12 +237,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) {
   case OrOne :       out << "OrOne";        return out;
   case XorOne :       out << "XorOne";        return out;
   case XorZero :       out << "XorZero";        return out;
-  case MultOne :       out << "MultOne";        return out;
-  case MultZero :       out << "MultZero";        return out;
   case MultPow2 :            out << "MultPow2";             return out;
-  case PlusZero :            out << "PlusZero";             return out;
-  case PlusSelf :            out << "PlusSelf";             return out;
-  case PlusNegSelf :            out << "PlusNegSelf";             return out;
   case NegIdemp :            out << "NegIdemp";             return out;
   case UdivPow2 :            out << "UdivPow2";             return out;
   case UdivOne :            out << "UdivOne";             return out;
@@ -465,12 +455,7 @@ struct AllRewriteRules {
   RewriteRule<SubEliminate> rule82; 
   RewriteRule<XorOne> rule83;
   RewriteRule<XorZero> rule84;
-  RewriteRule<MultOne> rule85;
-  RewriteRule<MultZero> rule86;
   RewriteRule<MultPow2> rule87;
-  RewriteRule<PlusZero> rule88;
-  RewriteRule<PlusSelf> rule89;
-  RewriteRule<PlusNegSelf> rule90;
   RewriteRule<NegIdemp> rule91;
   RewriteRule<UdivPow2> rule92;
   RewriteRule<UdivOne> rule93;
diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
index c695d20ab..82f4779c6 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h
@@ -135,10 +135,11 @@ bool RewriteRule<EvalMult>::applies(TNode node) {
 template<> inline
 Node RewriteRule<EvalMult>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalMult>(" << node << ")" << std::endl;
-  BitVector a = node[0].getConst<BitVector>();
-  BitVector b = node[1].getConst<BitVector>();
-  BitVector res = a * b;
-  
+  TNode::iterator child_it = node.begin();
+  BitVector res = (*child_it).getConst<BitVector>();
+  for(++child_it; child_it != node.end(); ++child_it) {
+    res = res * (*child_it).getConst<BitVector>();
+  }
   return utils::mkConst(res);
 }
 
@@ -151,10 +152,11 @@ bool RewriteRule<EvalPlus>::applies(TNode node) {
 template<> inline
 Node RewriteRule<EvalPlus>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<EvalPlus>(" << node << ")" << std::endl;
-  BitVector a = node[0].getConst<BitVector>();
-  BitVector b = node[1].getConst<BitVector>();
-  BitVector res = a + b;
-  
+  TNode::iterator child_it = node.begin();
+  BitVector res = (*child_it).getConst<BitVector>();
+  for(++child_it; child_it != node.end(); ++child_it) {
+    res = res + (*child_it).getConst<BitVector>();
+  }
   return utils::mkConst(res);
 }
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 6ac9da7cb..f8399041d 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -127,7 +127,7 @@ Node RewriteRule<ExtractArith2>::apply(TNode node) {
     children.push_back(utils::mkExtract(node[0][i], high, 0)); 
   }
   Kind kind = node[0].getKind(); 
-  Node op_children = utils::mkSortedNode(kind, children); 
+  Node op_children = utils::mkNode(kind, children); 
   
   return utils::mkExtract(op_children, high, low); 
 }
@@ -163,7 +163,13 @@ Node RewriteRule<FlattenAssocCommut>::apply(TNode node) {
       children.push_back(current); 
     }
   }
-  return utils::mkSortedNode(kind, children); 
+  if (node.getKind() == kind::BITVECTOR_PLUS ||
+      node.getKind() == kind::BITVECTOR_MULT) {
+    return utils::mkNode(kind, children);
+  }
+  else {
+    return utils::mkSortedNode(kind, children);
+  }
 }
 
 static inline void addToCoefMap(std::map<Node, BitVector>& map,
@@ -179,49 +185,65 @@ static inline void addToCoefMap(std::map<Node, BitVector>& map,
 static inline void updateCoefMap(TNode current, unsigned size,
                                  std::map<Node, BitVector>& factorToCoefficient,
                                  BitVector& constSum) {
-  // look for c * x, where c is a constant
-  if (current.getKind() == kind::BITVECTOR_MULT &&
-      (current[0].getKind() == kind::CONST_BITVECTOR ||
-       current[1].getKind() == kind::CONST_BITVECTOR)) {
-    // if we are multiplying by a constant
-    BitVector coeff;
-    TNode term;
-    // figure out which part is the constant
-    if (current[0].getKind() == kind::CONST_BITVECTOR) {
-      coeff = current[0].getConst<BitVector>();
-      term = current[1];
-    } else {
-      coeff = current[1].getConst<BitVector>();
-      term = current[0];
-    }
-    if(term.getKind() == kind::BITVECTOR_SUB) {
-      TNode a = term[0];
-      TNode b = term[1];
-      addToCoefMap(factorToCoefficient, a, coeff);
-      addToCoefMap(factorToCoefficient, b, -coeff); 
-    }
-    else if(term.getKind() == kind::BITVECTOR_NEG) {
-      addToCoefMap(factorToCoefficient, term[0], -BitVector(size, coeff));
+  switch (current.getKind()) {
+    case kind::BITVECTOR_MULT: {
+      // look for c * term, where c is a constant
+      BitVector coeff;
+      Node term;
+      if (current.getNumChildren() == 2) {
+        // Mult should be normalized with only one constant at end
+        Assert(!current[0].isConst());
+        if (current[1].isConst()) {
+          coeff = current[1].getConst<BitVector>();
+          term = current[0];
+        }
+      }
+      else if (current[current.getNumChildren()-1].isConst()) {
+        NodeBuilder<> nb(kind::BITVECTOR_MULT);
+        TNode::iterator child_it = current.begin();
+        for(; (child_it+1) != current.end(); ++child_it) {
+          Assert(!(*child_it).isConst());
+          nb << (*child_it);
+        }
+        term = nb;
+        coeff = (*child_it).getConst<BitVector>();
+      }
+      if (term.isNull()) {
+        coeff = BitVector(size, (unsigned)1);
+        term = current;
+      }
+      if(term.getKind() == kind::BITVECTOR_SUB) {
+        TNode a = term[0];
+        TNode b = term[1];
+        addToCoefMap(factorToCoefficient, a, coeff);
+        addToCoefMap(factorToCoefficient, b, -coeff); 
+      }
+      else if(term.getKind() == kind::BITVECTOR_NEG) {
+        addToCoefMap(factorToCoefficient, term[0], -BitVector(size, coeff));
+      }
+      else {
+        addToCoefMap(factorToCoefficient, term, coeff);
+      }
+      break;
     }
-    else {
-      addToCoefMap(factorToCoefficient, term, coeff);
+    case kind::BITVECTOR_SUB:
+      // turn into a + (-1)*b 
+      Assert(current.getNumChildren() == 2);
+      addToCoefMap(factorToCoefficient, current[0], BitVector(size, (unsigned)1)); 
+      addToCoefMap(factorToCoefficient, current[1], -BitVector(size, (unsigned)1)); 
+      break;
+    case kind::BITVECTOR_NEG:
+      addToCoefMap(factorToCoefficient, current[0], -BitVector(size, (unsigned)1)); 
+      break;
+    case kind::CONST_BITVECTOR: {
+      BitVector constValue = current.getConst<BitVector>(); 
+      constSum = constSum + constValue;
+      break;
     }
-  }
-  else if (current.getKind() == kind::BITVECTOR_SUB) {
-    // turn into a + (-1)*b 
-    addToCoefMap(factorToCoefficient, current[0], BitVector(size, (unsigned)1)); 
-    addToCoefMap(factorToCoefficient, current[1], -BitVector(size, (unsigned)1)); 
-  }
-  else if (current.getKind() == kind::BITVECTOR_NEG) {
-    addToCoefMap(factorToCoefficient, current[0], -BitVector(size, (unsigned)1)); 
-  }
-  else if (current.getKind() == kind::CONST_BITVECTOR) {
-    BitVector constValue = current.getConst<BitVector>(); 
-    constSum = constSum + constValue;
-  }
-  else {
-    // store as 1 * current
-    addToCoefMap(factorToCoefficient, current, BitVector(size, (unsigned)1)); 
+    default:
+      // store as 1 * current
+      addToCoefMap(factorToCoefficient, current, BitVector(size, (unsigned)1)); 
+      break;
   }
 }
 
@@ -237,9 +259,18 @@ static inline void addToChildren(TNode term, unsigned size, BitVector coeff, std
     // avoid introducing an extra multiplication
     children.push_back(utils::mkNode(kind::BITVECTOR_NEG, term)); 
   }
+  else if (term.getKind() == kind::BITVECTOR_MULT) {
+    NodeBuilder<> nb(kind::BITVECTOR_MULT);
+    TNode::iterator child_it = term.begin();
+    for(; child_it != term.end(); ++child_it) {
+      nb << *child_it;
+    }
+    nb << utils::mkConst(coeff);
+    children.push_back(Node(nb));
+  }
   else {
     Node coeffNode = utils::mkConst(coeff);
-    Node product = utils::mkSortedNode(kind::BITVECTOR_MULT, coeffNode, term); 
+    Node product = utils::mkNode(kind::BITVECTOR_MULT, term, coeffNode); 
     children.push_back(product); 
   }
 }
@@ -265,9 +296,6 @@ Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node) {
   }
     
   std::vector<Node> children; 
-  if ( constSum!= BitVector(size, (unsigned)0)) {
-    children.push_back(utils::mkConst(constSum)); 
-  }
 
   // construct result 
   std::map<Node, BitVector>::const_iterator it = factorToCoefficient.begin();
@@ -276,17 +304,36 @@ Node RewriteRule<PlusCombineLikeTerms>::apply(TNode node) {
     addToChildren(it->first, size, it->second, children);
   }
 
+  if (constSum != BitVector(size, (unsigned)0)) {
+    children.push_back(utils::mkConst(constSum)); 
+  }
+
   if(children.size() == 0) {
     return utils::mkConst(size, (unsigned)0); 
   }
-  
-  return utils::mkSortedNode(kind::BITVECTOR_PLUS, children);
+
+  return utils::mkNode(kind::BITVECTOR_PLUS, children);
 }
 
 
 template<> inline
 bool RewriteRule<MultSimplify>::applies(TNode node) {
-  return (node.getKind() == kind::BITVECTOR_MULT);
+  if (node.getKind() != kind::BITVECTOR_MULT) {
+    return false;
+  }
+  TNode::iterator child_it = node.begin();
+  TNode::iterator child_next = child_it + 1;
+  for(; child_next != node.end(); ++child_it, ++child_next) {
+    if ((*child_it).isConst() ||
+        !((*child_it) < (*child_next))) {
+      return true;
+    }
+  }
+  if ((*child_it).isConst() &&
+      (*child_it).getConst<BitVector>() == BitVector(utils::getSize(node), (unsigned) 0)) {
+    return true;
+  }
+  return false;
 }
 
 template<> inline
@@ -309,33 +356,30 @@ Node RewriteRule<MultSimplify>::apply(TNode node) {
     }
   }
 
+  std::sort(children.begin(), children.end());
 
   if(constant != BitVector(size, (unsigned)1)) {
     children.push_back(utils::mkConst(constant)); 
   }
-
   
   if(children.size() == 0) {
     return utils::mkConst(size, (unsigned)1); 
   }
 
-  return utils::mkSortedNode(kind::BITVECTOR_MULT, children); 
+  return utils::mkNode(kind::BITVECTOR_MULT, children); 
 }
 
 template<> inline
 bool RewriteRule<MultDistribConst>::applies(TNode node) {
-  if (node.getKind() != kind::BITVECTOR_MULT)
+  if (node.getKind() != kind::BITVECTOR_MULT ||
+      node.getNumChildren() != 2) {
     return false;
-
-  TNode factor;
-  if (node[0].getKind() == kind::CONST_BITVECTOR) {
-    factor = node[1];
-  } else if (node[1].getKind() == kind::CONST_BITVECTOR) {
-    factor = node[0];
-  } else {
-    return false; 
   }
-  
+  Assert(!node[0].isConst());
+  if (!node[1].isConst()) {
+    return false;
+  }
+  TNode factor = node[0];
   return (factor.getKind() == kind::BITVECTOR_PLUS ||
           factor.getKind() == kind::BITVECTOR_SUB ||
           factor.getKind() == kind::BITVECTOR_NEG); 
@@ -345,32 +389,24 @@ template<> inline
 Node RewriteRule<MultDistribConst>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<MultDistribConst>(" << node << ")" << std::endl;
 
-  TNode constant;
-  TNode factor;
-  if (node[0].getKind() == kind::CONST_BITVECTOR) {
-    constant = node[0];
-    factor = node[1]; 
-  } else {
-  Assert(node[1].getKind() == kind::CONST_BITVECTOR);
-  constant = node[1];
-  factor = node[0];
-  }
+  TNode constant = node[1];
+  TNode factor = node[0];
+  Assert(constant.getKind() == kind::CONST_BITVECTOR);
 
   if (factor.getKind() == kind::BITVECTOR_NEG) {
     // push negation on the constant part
     BitVector const_bv = constant.getConst<BitVector>();
-    return utils::mkSortedNode(kind::BITVECTOR_MULT,
-                               utils::mkConst(-const_bv),
-                               factor[0]); 
+    return utils::mkNode(kind::BITVECTOR_MULT,
+                         factor[0],
+                         utils::mkConst(-const_bv)); 
   }
 
   std::vector<Node> children;
   for(unsigned i = 0; i < factor.getNumChildren(); ++i) {
-    children.push_back(utils::mkSortedNode(kind::BITVECTOR_MULT, constant, factor[i])); 
+    children.push_back(utils::mkNode(kind::BITVECTOR_MULT, factor[i], constant));
   }
   
-  return utils::mkSortedNode(factor.getKind(), children); 
-                              
+  return utils::mkNode(factor.getKind(), children); 
 }
 
 
@@ -427,18 +463,6 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
 
   std::vector<Node> childrenLeft, childrenRight;
 
-  // If both constants are nonzero, combine on right, otherwise leave them where they are
-  if (rightConst != zero) {
-    rightConst = rightConst - leftConst;
-    leftConst = zero;
-    if (rightConst != zero) {
-      childrenRight.push_back(utils::mkConst(rightConst));
-    }
-  }
-  else if (leftConst != zero) {
-    childrenLeft.push_back(utils::mkConst(leftConst));
-  }
-
   std::map<Node, BitVector>::const_iterator iLeft = leftMap.begin(), iLeftEnd = leftMap.end();
   std::map<Node, BitVector>::const_iterator iRight = rightMap.begin(), iRightEnd = rightMap.end();
 
@@ -481,6 +505,7 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
     if (incLeft) {
       ++iLeft;
       if (iLeft != iLeftEnd) {
+        Assert(termLeft < iLeft->first);
         coeffLeft = iLeft->second;
         termLeft = iLeft->first;
       }
@@ -488,6 +513,7 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
     if (incRight) {
       ++iRight;
       if (iRight != iRightEnd) {
+        Assert(termRight < iRight->first);
         coeffRight = iRight->second;
         termRight = iRight->first;
       }
@@ -496,31 +522,41 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
 
   // construct result 
 
+  // If both constants are nonzero, combine on right, otherwise leave them where they are
+  if (rightConst != zero) {
+    rightConst = rightConst - leftConst;
+    leftConst = zero;
+    if (rightConst != zero) {
+      childrenRight.push_back(utils::mkConst(rightConst));
+    }
+  }
+  else if (leftConst != zero) {
+    childrenLeft.push_back(utils::mkConst(leftConst));
+  }
+
   Node newLeft, newRight;
 
   if(childrenRight.size() == 0 && leftConst != zero) {
-    Assert(childrenLeft[0].isConst() && childrenLeft[0].getConst<BitVector>() == leftConst);
+    Assert(childrenLeft.back().isConst() && childrenLeft.back().getConst<BitVector>() == leftConst);
     if (childrenLeft.size() == 1) {
       // c = 0 ==> false
       return utils::mkFalse();
     }
     // special case - if right is empty and left has a constant, move the constant
-    // TODO: this is inefficient - would be better if constant were at the end in the normal form
     childrenRight.push_back(utils::mkConst(-leftConst));
-    childrenLeft.erase(childrenLeft.begin());
+    childrenLeft.pop_back();
   }
 
   if(childrenLeft.size() == 0) {
     if (rightConst != zero) {
-      Assert(childrenRight[0].isConst() && childrenRight[0].getConst<BitVector>() == rightConst);
+      Assert(childrenRight.back().isConst() && childrenRight.back().getConst<BitVector>() == rightConst);
       if (childrenRight.size() == 1) {
         // 0 = c ==> false
         return utils::mkFalse();
       }
       // special case - if left is empty and right has a constant, move the constant
-      // TODO: this is inefficient - would be better if constant were at the end in the normal form
       newLeft = utils::mkConst(-rightConst);
-      childrenRight.erase(childrenRight.begin());
+      childrenRight.pop_back();
     }
     else {
       newLeft = utils::mkConst(size, (unsigned)0); 
@@ -530,7 +566,7 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
     newLeft = childrenLeft[0];
   }
   else {
-    newLeft = utils::mkSortedNode(kind::BITVECTOR_PLUS, childrenLeft);
+    newLeft = utils::mkNode(kind::BITVECTOR_PLUS, childrenLeft);
   }
 
   if (childrenRight.size() == 0) {
@@ -540,7 +576,7 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
     newRight = childrenRight[0];
   }
   else {
-    newRight = utils::mkSortedNode(kind::BITVECTOR_PLUS, childrenRight);
+    newRight = utils::mkNode(kind::BITVECTOR_PLUS, childrenRight);
   }
 
   //  Assert(newLeft == Rewriter::rewrite(newLeft));
@@ -552,9 +588,15 @@ Node RewriteRule<SolveEq>::apply(TNode node) {
   }
 
   if (newLeft < newRight) {
+    Assert((newRight == left && newLeft == right) ||
+           Rewriter::rewrite(newRight) != left ||
+           Rewriter::rewrite(newLeft) != right);
     return newRight.eqNode(newLeft);
   }
   
+  Assert((newLeft == left && newRight == right) ||
+         Rewriter::rewrite(newLeft) != left ||
+         Rewriter::rewrite(newRight) != right);
   return newLeft.eqNode(newRight);
 }
 
@@ -685,33 +727,26 @@ Node RewriteRule<BitwiseEq>::apply(TNode node) {
 template<> inline
 bool RewriteRule<NegMult>::applies(TNode node) {
   if(node.getKind()!= kind::BITVECTOR_NEG ||
-     node[0].getKind() != kind::BITVECTOR_MULT) {
-    return false; 
+     node[0].getKind() != kind::BITVECTOR_MULT) {                                
+    return false;
   }
-  TNode mult = node[0]; 
-  for (unsigned i = 0; i < mult.getNumChildren(); ++i) {
-    if (mult[i].getKind() == kind::CONST_BITVECTOR) {
-      return true; 
-    }
-  } 
-  return false; 
+  return node[node.getNumChildren()-1].isConst();
 }
 
 template<> inline
 Node RewriteRule<NegMult>::apply(TNode node) {
   BVDebug("bv-rewrite") << "RewriteRule<NegMult>(" << node << ")" << std::endl;
   TNode mult = node[0];
-  std::vector<Node> children;
+  NodeBuilder<> nb(kind::BITVECTOR_MULT);
   BitVector bv(utils::getSize(node), (unsigned)1);
-  for(unsigned i = 0; i < mult.getNumChildren(); ++i) {
-    if(mult[i].getKind() == kind::CONST_BITVECTOR) {
-      bv = bv * mult[i].getConst<BitVector>();
-    } else {
-      children.push_back(mult[i]); 
-    }
-  }
-  children.push_back(utils::mkConst(-bv));
-  return utils::mkSortedNode(kind::BITVECTOR_MULT, children);
+  TNode::iterator child_it = mult.begin();
+  for(; (child_it+1) != mult.end(); ++child_it) {
+    nb << (*child_it);
+  }
+  Assert((*child_it).isConst());
+  bv = (*child_it).getConst<BitVector>();
+  nb << utils::mkConst(-bv);
+  return Node(nb);
 }
 
 template<> inline
@@ -739,7 +774,7 @@ Node RewriteRule<NegPlus>::apply(TNode node) {
   for (unsigned i = 0; i < node[0].getNumChildren(); ++i) {
     children.push_back(utils::mkNode(kind::BITVECTOR_NEG, node[0][i])); 
   }
-  return utils::mkSortedNode(kind::BITVECTOR_PLUS, children);
+  return utils::mkNode(kind::BITVECTOR_PLUS, children);
 }
 
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
index ee0e0fc43..8e14980a7 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h
@@ -657,51 +657,6 @@ Node RewriteRule<NotUle>::apply(TNode node) {
 }
 
 /**
- * MultOne 
- *
- * (a * 1) ==> a
- */
-
-template<> inline
-bool RewriteRule<MultOne>::applies(TNode node) {
-  unsigned size = utils::getSize(node); 
-  return (node.getKind() == kind::BITVECTOR_MULT &&
-          (node[0] == utils::mkConst(size, 1) ||
-           node[1] == utils::mkConst(size, 1)));
-}
-
-template<> inline
-Node RewriteRule<MultOne>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<MultOne>(" << node << ")" << std::endl;
-  unsigned size = utils::getSize(node); 
-  if (node[0] == utils::mkConst(size, 1)) {
-    return node[1];
-  }
-  Assert(node[1] == utils::mkConst(size, 1));
-  return node[0]; 
-}
-
-/**
- * MultZero 
- *
- * (a * 0) ==> 0
- */
-
-template<> inline
-bool RewriteRule<MultZero>::applies(TNode node) {
-  unsigned size = utils::getSize(node); 
-  return (node.getKind() == kind::BITVECTOR_MULT &&
-          (node[0] == utils::mkConst(size, 0) ||
-           node[1] == utils::mkConst(size, 0)));
-}
-
-template<> inline
-Node RewriteRule<MultZero>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<MultZero>(" << node << ")" << std::endl;
-  return utils::mkConst(utils::getSize(node), 0); 
-}
-
-/**
  * MultPow2
  *
  * (a * 2^k) ==> a[n-k-1:0] 0_k
@@ -736,7 +691,7 @@ Node RewriteRule<MultPow2>::apply(TNode node) {
     }
   }
 
-  Node a = utils::mkSortedNode(kind::BITVECTOR_MULT, children); 
+  Node a = utils::mkNode(kind::BITVECTOR_MULT, children); 
 
   Node extract = utils::mkExtract(a, utils::getSize(node) - exponent - 1, 0);
   Node zeros = utils::mkConst(exponent, 0);
@@ -744,31 +699,6 @@ Node RewriteRule<MultPow2>::apply(TNode node) {
 }
 
 /**
- * PlusZero
- *   
- * (a + 0) ==> a
- */
-
-template<> inline
-bool RewriteRule<PlusZero>::applies(TNode node) {
-  Node zero = utils::mkConst(utils::getSize(node), 0); 
-  return (node.getKind() == kind::BITVECTOR_PLUS &&
-          (node[0] == zero ||
-           node[1] == zero));
-}
-
-template<> inline
-Node RewriteRule<PlusZero>::apply(TNode node) {
-  BVDebug("bv-rewrite") << "RewriteRule<PlusZero>(" << node << ")" << std::endl;
-  Node zero = utils::mkConst(utils::getSize(node), 0);
-  if (node[0] == zero) {
-    return node[1];
-  }
-  
-  return node[0]; 
-}
-
-/**
  * NegIdemp
  *
  * -(-a) ==> a 
@@ -966,7 +896,7 @@ Node RewriteRule<BBPlusNeg>::apply(TNode node) {
   Assert(neg_count!= 0); 
   children.push_back(utils::mkConst(utils::getSize(node), neg_count)); 
 
-  return utils::mkSortedNode(kind::BITVECTOR_PLUS, children); 
+  return utils::mkNode(kind::BITVECTOR_PLUS, children); 
 }
 
 // /**
diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h
index 60715ee60..bfd8a2897 100644
--- a/src/theory/bv/theory_bv_rewriter.h
+++ b/src/theory/bv/theory_bv_rewriter.h
@@ -84,7 +84,7 @@ public:
 
   static RewriteResponse preRewrite(TNode node);
 
-  static inline Node rewriteEquality(TNode node) {
+  static Node rewriteEquality(TNode node) {
     Debug("bitvector") << "TheoryBV::rewriteEquality(" << node << ")" << std::endl;
     return postRewrite(node).node;
   }
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index c456ef73f..a0d418c4b 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -95,12 +95,10 @@ inline Node mkAnd(std::vector<TNode>& children) {
 }
 
 inline Node mkSortedNode(Kind kind, std::vector<Node>& children) {
-  Assert (kind == kind::BITVECTOR_PLUS ||
-          kind == kind::BITVECTOR_MULT ||
-          kind == kind::BITVECTOR_AND ||
+  Assert (kind == kind::BITVECTOR_AND ||
           kind == kind::BITVECTOR_OR ||
           kind == kind::BITVECTOR_XOR);
-
+  Assert(children.size() > 0);
   if (children.size() == 1) {
     return children[0]; 
   }
@@ -126,9 +124,7 @@ inline Node mkNode(Kind kind, TNode child1, TNode child2) {
 
 
 inline Node mkSortedNode(Kind kind, TNode child1, TNode child2) {
-  Assert (kind == kind::BITVECTOR_PLUS ||
-          kind == kind::BITVECTOR_MULT ||
-          kind == kind::BITVECTOR_AND ||
+  Assert (kind == kind::BITVECTOR_AND ||
           kind == kind::BITVECTOR_OR ||
           kind == kind::BITVECTOR_XOR);
   
diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
index 2e8acfa89..e0b1458fb 100644
--- a/src/theory/rewriter.cpp
+++ b/src/theory/rewriter.cpp
@@ -26,6 +26,8 @@ using namespace std;
 namespace CVC4 {
 namespace theory {
 
+std::hash_set<Node, NodeHashFunction> d_rewriteStack;
+
 /**
  * TheoryEngine::rewrite() keeps a stack of things that are being pre-
  * and post-rewritten.  Each element of the stack is a
@@ -172,7 +174,15 @@ Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
         if (newTheoryId != (TheoryId) rewriteStackTop.theoryId || response.status == REWRITE_AGAIN_FULL) {
           // In the post rewrite if we've changed theories, we must do a full rewrite
           Assert(response.node != rewriteStackTop.node);
+          //TODO: this is not thread-safe - should make this assertion dependent on sequential build
+#ifdef CVC4_ASSERTIONS
+          Assert(d_rewriteStack.find(response.node) == d_rewriteStack.end());
+          d_rewriteStack.insert(response.node);
+#endif
           rewriteStackTop.node = rewriteTo(newTheoryId, response.node);
+#ifdef CVC4_ASSERTIONS
+          d_rewriteStack.erase(response.node);
+#endif
           break;
         } else if (response.status == REWRITE_DONE) {
 #ifdef CVC4_ASSERTIONS