bitvector rewriting for the core theory and testcases

17 files changed, 541 insertions, 25 deletions

diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 4a6dd794e..422cb47a8 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -902,13 +902,13 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() {
   // check that there are the right # of children for this kind
   Assert(getMetaKind() != kind::metakind::CONSTANT,
          "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds");
-  Assert(d_nv->d_nchildren >= kind::metakind::getLowerBoundForKind(getKind()),
+  Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind()),
          "Nodes with kind %s must have at least %u children (the one under "
          "construction has %u)",
          kind::kindToString(getKind()).c_str(),
          kind::metakind::getLowerBoundForKind(getKind()),
          getNumChildren());
-  Assert(d_nv->d_nchildren <= kind::metakind::getUpperBoundForKind(getKind()),
+  Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind()),
          "Nodes with kind %s must have at most %u children (the one under "
          "construction has %u)",
          kind::kindToString(getKind()).c_str(),
@@ -1073,13 +1073,13 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() const {
   // check that there are the right # of children for this kind
   Assert(getMetaKind() != kind::metakind::CONSTANT,
          "Cannot make Nodes with NodeBuilder that have CONSTANT-kinded kinds");
-  Assert(d_nv->d_nchildren >= kind::metakind::getLowerBoundForKind(getKind()),
+  Assert(getNumChildren() >= kind::metakind::getLowerBoundForKind(getKind()),
          "Nodes with kind %s must have at least %u children (the one under "
          "construction has %u)",
          kind::kindToString(getKind()).c_str(),
          kind::metakind::getLowerBoundForKind(getKind()),
          getNumChildren());
-  Assert(d_nv->d_nchildren <= kind::metakind::getUpperBoundForKind(getKind()),
+  Assert(getNumChildren() <= kind::metakind::getUpperBoundForKind(getKind()),
          "Nodes with kind %s must have at most %u children (the one under "
          "construction has %u)",
          kind::kindToString(getKind()).c_str(),
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 37ed4fe20..b7bbe2ff8 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -277,7 +277,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
     case kind::STORE:
       typeNode = CVC4::theory::arrays::ArrayStoreTypeRule::computeType(this, n, check);
       break;
-    case kind::BITVECTOR_CONST:
+    case kind::CONST_BITVECTOR:
       typeNode = CVC4::theory::bv::BitVectorConstantTypeRule::computeType(this, n, check);
       break;
     case kind::BITVECTOR_AND:
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index baa8de5aa..5c6a05a03 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -916,7 +916,6 @@ template <bool ref_count>
 inline Node NodeManager::mkNode(TNode opNode,
                                 const std::vector<NodeTemplate<ref_count> >&
                                 children) {
-  Assert(kind::metaKindOf(opNode.getKind()) == kind::metakind::PARAMETERIZED);
   NodeBuilder<> nb(this, kind::operatorKindToKind(opNode.getKind()));
   nb << opNode;
   nb.append(children);
diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h
index 940835a7e..82b15d199 100644
--- a/src/parser/antlr_input.h
+++ b/src/parser/antlr_input.h
@@ -175,6 +175,9 @@ public:
   /** Retrieve a Rational from the text of a token */
   static Rational tokenToRational(pANTLR3_COMMON_TOKEN token);
 
+  /** Get a bitvector constant from the text of the number and the size token */
+  static BitVector tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size);
+
 protected:
   /** Create an input. This input takes ownership of the given input stream,
    * and will delete it at destruction time.
@@ -230,9 +233,9 @@ inline std::string AntlrInput::tokenTextSubstr(pANTLR3_COMMON_TOKEN token,
   }
   start += index;
   if( n==0 || n >= (size_t) end - start ) {
-    return std::string( (const char *)start + index, end-start+1 );
+    return std::string( (const char *)start, end-start+1 );
   } else {
-    return std::string( (const char *)start + index, n );
+    return std::string( (const char *)start, n );
   }
 }
 
@@ -252,6 +255,11 @@ inline Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) {
   return Rational::fromDecimal( tokenText(token) );
 }
 
+inline BitVector AntlrInput::tokenToBitvector(pANTLR3_COMMON_TOKEN number, pANTLR3_COMMON_TOKEN size) {
+  std::string number_str = tokenTextSubstr(number, 2);
+  return BitVector(tokenToUnsigned(size), Integer(number_str));
+}
+
 }/* CVC4::parser namespace */
 }/* CVC4 namespace */
 
diff --git a/src/parser/smt/Smt.g b/src/parser/smt/Smt.g
index ecb3d39b6..55c158a6f 100644
--- a/src/parser/smt/Smt.g
+++ b/src/parser/smt/Smt.g
@@ -216,12 +216,6 @@ annotatedFormula[CVC4::Expr& expr]
     RPAREN_TOK
     { PARSER_STATE->popScope(); }
 
-  | /* a variable */
-    ( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
-      | let_identifier[name,CHECK_DECLARED] 
-      | flet_identifier[name,CHECK_DECLARED] )
-    { expr = PARSER_STATE->getVariable(name); }
-
     /* constants */
   | TRUE_TOK          { expr = MK_CONST(true); }
   | FALSE_TOK         { expr = MK_CONST(false); }
@@ -230,8 +224,17 @@ annotatedFormula[CVC4::Expr& expr]
   | RATIONAL_TOK
     { // FIXME: This doesn't work because an SMT rational is not a valid GMP rational string
       expr = MK_CONST( AntlrInput::tokenToRational($RATIONAL_TOK) ); }
+  | n = BITVECTOR_BV_CONST '[' size = NUMERAL_TOK  ']' 
+    { expr = MK_CONST( AntlrInput::tokenToBitvector($n, $size) ); }
     // NOTE: Theory constants go here
     /* TODO: quantifiers, arithmetic constants */
+
+  | /* a variable */
+    ( identifier[name,CHECK_DECLARED,SYM_VARIABLE]
+      | let_identifier[name,CHECK_DECLARED] 
+      | flet_identifier[name,CHECK_DECLARED] )
+    { expr = PARSER_STATE->getVariable(name); }
+
   ;
 
 /**
@@ -553,6 +556,7 @@ XOR_TOK           : 'xor';
 
 // Bitvector tokens 
 BITVECTOR_TOK     : 'BitVec';
+BV_TOK            : 'bv';
 CONCAT_TOK        : 'concat';
 EXTRACT_TOK       : 'extract';
 BVAND_TOK         : 'bvand';
@@ -590,6 +594,14 @@ ROTATE_LEFT_TOK   : 'rotate_left';
 ROTATE_RIGHT_TOK  : 'rotate_right';
 
 /**
+ * Mathces a bit-vector constant of the form bv123
+ */
+BITVECTOR_BV_CONST
+  : 'bv' DIGIT+
+  ;
+
+
+/**
  * Matches an identifier from the input. An identifier is a sequence of letters,
  * digits and "_", "'", "." symbols, starting with a letter.
  */
diff --git a/src/parser/smt/smt.cpp b/src/parser/smt/smt.cpp
index fe7d77455..2e0e0087c 100644
--- a/src/parser/smt/smt.cpp
+++ b/src/parser/smt/smt.cpp
@@ -110,6 +110,9 @@ void Smt::addTheory(Theory theory) {
     addArithmeticOperators();
     break;
 
+  case THEORY_BITVECTORS:
+    break;
+
   default:
     Unhandled(theory);
   }
@@ -170,6 +173,10 @@ void Smt::setLogic(const std::string& name) {
     addUf();
     break;
 
+  case QF_BV:
+    addTheory(THEORY_BITVECTORS);
+    break;
+
   case AUFLIA:
   case AUFLIRA:
   case AUFNIRA:
@@ -177,7 +184,6 @@ void Smt::setLogic(const std::string& name) {
   case UFNIA:
   case QF_AUFBV:
   case QF_AUFLIA:
-  case QF_BV:
     Unhandled(name);
   }
 }
diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index cab90bbdb..ad858ab53 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -7,6 +7,10 @@ noinst_LTLIBRARIES = libbv.la
 
 libbv_la_SOURCES = \
 	theory_bv.h \
+	theory_bv.cpp \
+	theory_bv_utils.h \
+	theory_bv_rewrite_rules.h \
+	theory_bv_rewrite_rules.cpp \
 	theory_bv_type_rules.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/bv/kinds b/src/theory/bv/kinds
index f1b926d24..54f861b76 100644
--- a/src/theory/bv/kinds
+++ b/src/theory/bv/kinds
@@ -12,13 +12,13 @@ constant BITVECTOR_TYPE \
 	"util/bitvector.h" \
 	"bit-vector type"
 
-constant BITVECTOR_CONST \
+constant CONST_BITVECTOR \
     ::CVC4::BitVector \
     ::CVC4::BitVectorHashStrategy \
     "util/bitvector.h" \
     "a fixed-width bit-vector constant"
     
-operator BITVECTOR_CONCAT 2 "bit-vector concatenation"
+operator BITVECTOR_CONCAT 2: "bit-vector concatenation"
 operator BITVECTOR_AND 2 "bitwise and"
 operator BITVECTOR_OR 2 "bitwise or"      
 operator BITVECTOR_XOR 2 "bitwise xor"      
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
new file mode 100644
index 000000000..849740c9a
--- /dev/null
+++ b/src/theory/bv/theory_bv.cpp
@@ -0,0 +1,60 @@
+#include "theory_bv.h"
+#include "theory_bv_utils.h"
+#include "theory_bv_rewrite_rules.h"
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+using namespace CVC4::theory::bv::utils;
+
+RewriteResponse TheoryBV::postRewrite(TNode node, bool topLevel) {
+
+  Debug("bitvector") << "postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ")" << std::endl;
+
+  Node result;
+
+  if (node.getKind() == kind::CONST_BITVECTOR /* || isLeaf(n)) */)
+    result = node;
+  else {
+    switch (node.getKind()) {
+    case kind::BITVECTOR_CONCAT:
+      result = LinearRewriteStrategy<
+                  // Flatten the top level concatenations
+                  CoreRewriteRules::ConcatFlatten,
+                  // Merge the adjacent extracts on non-constants
+                  CoreRewriteRules::ConcatExtractMerge,
+                  // Merge the adjacent extracts on constants
+                  CoreRewriteRules::ConcatConstantMerge,
+                  // At this point only Extract-Whole could apply, if the result is only one extract
+                  // or at some sub-expression if the result is a concatenation.
+                  ApplyRuleToChildren<kind::BITVECTOR_CONCAT, CoreRewriteRules::ExtractWhole>
+               >::apply(node);
+      break;
+    case kind::BITVECTOR_EXTRACT:
+      result = LinearRewriteStrategy<
+                  // Extract over a constant gives a constant
+                  CoreRewriteRules::ExtractConstant,
+                  // Extract over an extract is simplified to one extract
+                  CoreRewriteRules::ExtractExtract,
+                  // Extract over a concatenation is distributed to the appropriate concatenations
+                  CoreRewriteRules::ExtractConcat,
+                  // At this point only Extract-Whole could apply
+                  CoreRewriteRules::ExtractWhole
+                >::apply(node);
+      break;
+    case kind::EQUAL:
+      if (node[0] == node[1]) result = mkTrue();
+      else result = node;
+      break;
+    default:
+      // TODO: figure out when this is an operator
+      result = node;
+      break;
+      // Unhandled();
+    }
+  }
+
+  Debug("bitvector") << "postRewrite(" << node << ", topLevel = " << (topLevel? "true" : "false") << ") => " << result << std::endl;
+
+  return RewriteComplete(result);
+}
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index 537e7f5fe..ee331af02 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -33,12 +33,12 @@ public:
   TheoryBV(int id, context::Context* c, OutputChannel& out) :
     Theory(id, c, out) {
   }
-
-  void preRegisterTerm(TNode n) { Unimplemented(); }
-  void registerTerm(TNode n) { Unimplemented(); }
+  void preRegisterTerm(TNode n) { }
+  void registerTerm(TNode n) { }
   void check(Effort e) {}
   void propagate(Effort e) {}
-  void explain(TNode n, Effort e) { Unimplemented(); }
+  void explain(TNode n, Effort e) { }
+  RewriteResponse postRewrite(TNode n, bool topLevel);
   std::string identify() const { return std::string("TheoryBV"); }
 };/* class TheoryBV */
 
diff --git a/src/theory/bv/theory_bv_rewrite_rules.cpp b/src/theory/bv/theory_bv_rewrite_rules.cpp
new file mode 100644
index 000000000..5473768bb
--- /dev/null
+++ b/src/theory/bv/theory_bv_rewrite_rules.cpp
@@ -0,0 +1,249 @@
+#include <vector>
+#include "expr/node_builder.h"
+#include "theory_bv_rewrite_rules.h"
+#include "theory_bv_utils.h"
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+using namespace CVC4::theory::bv::utils;
+
+bool CoreRewriteRules::ConcatFlatten::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_CONCAT);
+}
+
+Node CoreRewriteRules::ConcatFlatten::apply(Node node) {
+  Assert(applies(node));
+
+  Debug("bitvector") << "ConcatFlatten(" << node << ")" << endl;
+
+  NodeBuilder<> result(kind::BITVECTOR_CONCAT);
+  vector<Node> processing_stack;
+  processing_stack.push_back(node);
+  while (!processing_stack.empty()) {
+    Node current = processing_stack.back();
+    processing_stack.pop_back();
+    if (current.getKind() == kind::BITVECTOR_CONCAT) {
+      for (int i = current.getNumChildren() - 1; i >= 0; i--)
+        processing_stack.push_back(current[i]);
+    } else {
+      result << current;
+    }
+  }
+
+  Debug("bitvector") << "ConcatFlatten(" << node << ") => " << result << endl;
+
+  return result;
+}
+
+bool CoreRewriteRules::ConcatExtractMerge::applies(Node node) {
+  return (node.getKind() == kind::BITVECTOR_CONCAT);
+}
+
+Node CoreRewriteRules::ConcatExtractMerge::apply(Node node) {
+  Assert(applies(node));
+
+  Debug("bitvector") << "ConcatExtractMerge(" << node << ")" << endl;
+
+  vector<Node> mergedExtracts;
+
+  Node current = node[0];
+  bool mergeStarted = false;
+  unsigned currentHigh = 0;
+  unsigned currentLow  = 0;
+
+  for(size_t i = 1, end = node.getNumChildren(); i < end; ++ i) {
+    // The next candidate for merging
+    Node next = node[i];
+    // If the current is not an extract we just go to the next
+    if (current.getKind() != kind::BITVECTOR_EXTRACT) {
+      mergedExtracts.push_back(current);
+      current = next;
+      continue;
+    }
+    // If it is an extract and the first one, get the extract parameters
+    else if (!mergeStarted) {
+      currentHigh = getExtractHigh(current);
+      currentLow = getExtractLow(current);
+    }
+
+    // If the next one can be merged, try to merge
+    bool merged = false;
+    if (next.getKind() == kind::BITVECTOR_EXTRACT && current[0] == next[0]) {
+      //x[i : j] @ x[j − 1 : k] -> c x[i : k]
+      unsigned nextHigh = getExtractHigh(next);
+      unsigned nextLow  = getExtractLow(next);
+      if(nextHigh + 1 == currentLow) {
+        currentLow = nextLow;
+        mergeStarted = true;
+        merged = true;
+      }
+    }
+    // If we haven't merged anything, add the previous merge and continue with the next
+    if (!merged) {
+      if (!mergeStarted) mergedExtracts.push_back(current);
+      else mergedExtracts.push_back(mkExtract(current[0], currentHigh, currentLow));
+      current = next;
+      mergeStarted = false;
+    }
+  }
+
+  // Add the last child
+  if (!mergeStarted) mergedExtracts.push_back(current);
+  else mergedExtracts.push_back(mkExtract(current[0], currentHigh, currentLow));
+
+  // Create the result
+  Node result = mkConcat(mergedExtracts);
+
+  Debug("bitvector") << "ConcatExtractMerge(" << node << ") =>" << result << endl;
+
+  // Return the result
+  return result;
+}
+
+bool CoreRewriteRules::ConcatConstantMerge::applies(Node node) {
+  return node.getKind() == kind::BITVECTOR_CONCAT;
+}
+
+Node CoreRewriteRules::ConcatConstantMerge::apply(Node node) {
+  Assert(applies(node));
+
+  Debug("bitvector") << "ConcatConstantMerge(" << node << ")" << endl;
+
+  vector<Node> mergedConstants;
+  for (unsigned i = 0, end = node.getNumChildren(); i < end;) {
+    if (node[i].getKind() != kind::CONST_BITVECTOR) {
+      // If not a constant, just add it
+      mergedConstants.push_back(node[i]);
+      ++i;
+    } else {
+      // Find the longest sequence of constants
+      unsigned j = i + 1;
+      while (j < end) {
+        if (node[j].getKind() != kind::CONST_BITVECTOR) {
+          break;
+        } else {
+          ++ j;
+        }
+      }
+      // Append all the constants
+      BitVector current = node[i].getConst<BitVector>();
+      for (unsigned k = i + 1; k < j; ++ k) {
+        current = current.concat(node[k].getConst<BitVector>());
+      }
+      // Add the new merged constant
+      mergedConstants.push_back(mkConst(current));
+      i = j + 1;
+    }
+  }
+
+  Node result = mkConcat(mergedConstants);
+
+  Debug("bitvector") << "ConcatConstantMerge(" << node << ") => " << result << endl;
+
+  return result;
+}
+
+bool CoreRewriteRules::ExtractWhole::applies(Node node) {
+  if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
+  unsigned length = getSize(node[0]);
+  unsigned extractHigh = getExtractHigh(node);
+  if (extractHigh != length - 1) return false;
+  unsigned extractLow  = getExtractLow(node);
+  if (extractLow != 0) return false;
+  return true;
+}
+
+Node CoreRewriteRules::ExtractWhole::apply(Node node) {
+  Assert(applies(node));
+
+  Debug("bitvector") << "ExtractWhole(" << node << ")" << endl;
+  Debug("bitvector") << "ExtractWhole(" << node << ") => " << node[0] << endl;
+
+  return node[0];
+}
+
+bool CoreRewriteRules::ExtractConstant::applies(Node node) {
+  if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
+  if (node[0].getKind() != kind::CONST_BITVECTOR) return false;
+  return true;
+}
+
+Node CoreRewriteRules::ExtractConstant::apply(Node node) {
+  Assert(applies(node));
+
+  Debug("bitvector") << "ExtractConstant(" << node << ")" << endl;
+
+  Node child = node[0];
+  BitVector childValue = child.getConst<BitVector>();
+
+  Node result = mkConst(childValue.extract(getExtractHigh(node), getExtractLow(node)));
+
+  Debug("bitvector") << "ExtractConstant(" << node << ") => " << result << endl;
+
+  return result;
+}
+
+bool CoreRewriteRules::ExtractConcat::applies(Node node) {
+  if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
+  if (node[0].getKind() != kind::BITVECTOR_CONCAT) return false;
+  return true;
+}
+
+Node CoreRewriteRules::ExtractConcat::apply(Node node) {
+  Assert(applies(node));
+
+  Debug("bitvector") << "ExtractConcat(" << node << ")" << endl;
+
+  int extract_high = getExtractHigh(node);
+  int extract_low = getExtractLow(node);
+
+  vector<Node> resultChildren;
+
+  Node concat = node[0];
+  for (int i = concat.getNumChildren() - 1; i >= 0 && extract_high >= 0; i--) {
+    Node concatChild = concat[i];
+    int concatChildSize = getSize(concatChild);
+    if (extract_low < concatChildSize) {
+      int extract_start = extract_low < 0 ? 0 : extract_low;
+      int extract_end = extract_high < concatChildSize ? extract_high : concatChildSize - 1;
+      resultChildren.push_back(mkExtract(concatChild, extract_end, extract_start));
+    }
+    extract_low -= concatChildSize;
+    extract_high -= concatChildSize;
+  }
+
+  std::reverse(resultChildren.begin(), resultChildren.end());
+
+  Node result = mkConcat(resultChildren);
+
+  Debug("bitvector") << "ExtractConcat(" << node << ") => " << result << endl;
+
+  return result;
+}
+
+bool CoreRewriteRules::ExtractExtract::applies(Node node) {
+  if (node.getKind() != kind::BITVECTOR_EXTRACT) return false;
+  if (node[0].getKind() != kind::BITVECTOR_EXTRACT) return false;
+  return true;
+}
+
+Node CoreRewriteRules::ExtractExtract::apply(Node node) {
+  Assert(applies(node));
+
+  Debug("bitvector") << "ExtractExtract(" << node << ")" << endl;
+
+  // x[i:j][k:l] ~>  x[k+j:l+j]
+  Node child = node[0];
+  unsigned k = getExtractHigh(node);
+  unsigned l = getExtractLow(node);
+  unsigned j = getExtractLow(child);
+
+  Node result = mkExtract(child[0], k + j, l + j);
+
+  Debug("bitvector") << "ExtractExtract(" << node << ") => " << result << endl;
+
+  return result;
+
+}
diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h
new file mode 100644
index 000000000..48696ce33
--- /dev/null
+++ b/src/theory/bv/theory_bv_rewrite_rules.h
@@ -0,0 +1,104 @@
+#pragma once 
+
+#include "cvc4_private.h"
+#include "theory/theory.h"
+#include "context/context.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+struct CoreRewriteRules {
+
+  struct EmptyRule {
+    static inline Node apply(Node node) { return node; }
+    static inline bool applies(Node node) { return false; }
+  };
+
+  struct ConcatFlatten {
+    static Node apply(Node node);
+    static bool applies(Node node);
+  };
+
+  struct ConcatExtractMerge {
+    static Node apply(Node node);
+    static bool applies(Node node);
+  };
+
+  struct ConcatConstantMerge {
+    static Node apply(Node node);
+    static bool applies(Node node);
+  };
+
+  struct ExtractExtract {
+    static Node apply(Node node);
+    static bool applies(Node node);
+  };
+
+  struct ExtractWhole {
+    static Node apply(Node node);
+    static bool applies(Node node);
+  };
+
+  struct ExtractConcat {
+    static Node apply(Node node);
+    static bool applies(Node node);
+  };
+
+  struct ExtractConstant {
+    static Node apply(Node node);
+    static bool applies(Node node);
+  };
+
+};
+
+template<Kind kind, typename Rule>
+struct ApplyRuleToChildren {
+
+  static Node apply(Node node) {
+    if (node.getKind() != kind) {
+      if (Rule::applies(node)) return Rule::apply(node);
+      else return node;
+    }
+    NodeBuilder<> result(kind);
+    for (unsigned i = 0, end = node.getNumChildren(); i < end; ++ i) {
+      if (Rule::applies(node[i])) result << Rule::apply(node[i]);
+      else result << node[i];
+    }
+    return result;
+  }
+
+  static bool applies(Node node) {
+    if (node.getKind() == kind) return true;
+    return Rule::applies(node);
+  }
+
+};
+
+
+template <
+  typename R1,
+  typename R2,
+  typename R3 = CoreRewriteRules::EmptyRule,
+  typename R4 = CoreRewriteRules::EmptyRule,
+  typename R5 = CoreRewriteRules::EmptyRule,
+  typename R6 = CoreRewriteRules::EmptyRule,
+  typename R7 = CoreRewriteRules::EmptyRule
+  >
+struct LinearRewriteStrategy {
+  static Node apply(Node node) {
+    Node current = node;
+    if (R1::applies(current)) current = R1::apply(current);
+    if (R2::applies(current)) current = R2::apply(current);
+    if (R3::applies(current)) current = R3::apply(current);
+    if (R4::applies(current)) current = R4::apply(current);
+    if (R5::applies(current)) current = R5::apply(current);
+    if (R6::applies(current)) current = R6::apply(current);
+    if (R7::applies(current)) current = R7::apply(current);
+    return current;
+  }
+};
+
+} // End namespace bv
+} // End namespace theory
+} // End namespace CVC4
diff --git a/src/theory/bv/theory_bv_type_rules.h b/src/theory/bv/theory_bv_type_rules.h
index 9bb9e61df..7c4ff495e 100644
--- a/src/theory/bv/theory_bv_type_rules.h
+++ b/src/theory/bv/theory_bv_type_rules.h
@@ -142,7 +142,7 @@ public:
     TNode::iterator it = n.begin();
     TNode::iterator it_end = n.end();
     for (; it != it_end; ++ it) {
-       TypeNode t = n[0].getType(check);
+       TypeNode t = (*it).getType(check);
        // NOTE: We're throwing a type-checking exception here even
        // when check is false, bc if we don't check that the arguments
        // are bit-vectors the result type will be inaccurate
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
new file mode 100644
index 000000000..fa948465d
--- /dev/null
+++ b/src/theory/bv/theory_bv_utils.h
@@ -0,0 +1,53 @@
+#pragma once 
+
+#include <vector>
+#include "expr/node_manager.h"
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+namespace utils {
+
+inline unsigned getExtractHigh(TNode node) {
+  return node.getOperator().getConst<BitVectorExtract>().high;
+}
+
+inline unsigned getExtractLow(TNode node) {
+  return node.getOperator().getConst<BitVectorExtract>().low;
+}
+
+inline unsigned getSize(TNode node) {
+  return node.getType().getBitVectorSize();
+}
+
+inline Node mkTrue() {
+  return NodeManager::currentNM()->mkConst<bool>(true);
+}
+
+inline Node mkFalse() {
+  return NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+inline Node mkExtract(TNode node, unsigned high, unsigned low) {
+  Node extractOp = NodeManager::currentNM()->mkConst<BitVectorExtract>(BitVectorExtract(high, low));
+  std::vector<Node> children;
+  children.push_back(node);
+  return NodeManager::currentNM()->mkNode(extractOp, children);
+}
+
+inline Node mkConcat(std::vector<Node>& children) {
+  if (children.size() > 1)
+    return NodeManager::currentNM()->mkNode(kind::BITVECTOR_CONCAT, children);
+  else
+    return children[0];
+}
+
+inline Node mkConst(const BitVector& value) {
+  return NodeManager::currentNM()->mkConst<BitVector>(value);
+}
+
+
+}
+}
+}
+}
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 0b5952481..5c05bd6a7 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -35,10 +35,11 @@ private:
   unsigned d_size;
   Integer d_value;
 
-  BitVector(unsigned size, const Integer& val) : d_size(size), d_value(val) {}
-
 public:
 
+  BitVector(unsigned size, const Integer& val)
+  : d_size(size), d_value(val) {}
+
   BitVector(unsigned size = 0)
   : d_size(size), d_value(0) {}
 
@@ -58,6 +59,7 @@ public:
   BitVector& operator =(const BitVector& x) {
     if(this == &x)
       return *this;
+    d_size = x.d_size;
     d_value = x.d_value;
     return *this;
   }
@@ -92,8 +94,16 @@ public:
     return BitVector(d_size, d_value);
   }
 
+  BitVector concat (const BitVector& other) const {
+    return BitVector(d_size + other.d_size, (d_value * Integer(2).pow(other.d_size)) + other.d_value);
+  }
+
+  BitVector extract(unsigned high, unsigned low) {
+    return BitVector(high - low + 1, (d_value % (Integer(2).pow(high + 1))) / Integer(2).pow(low));
+  }
+
   size_t hash() const {
-    return d_value.hash();
+    return d_value.hash() + d_size;
   }
 
   std::string toString(unsigned int base = 2) const {
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index 8551d0a6a..233b3aa08 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -152,6 +152,14 @@ public:
     return Integer( d_value * y.d_value );
   }
 
+  Integer operator/(const Integer& y) const {
+    return Integer( cln::floor1(d_value, y.d_value) );
+  }
+
+  Integer operator%(const Integer& y) const {
+    return Integer( cln::floor2(d_value, y.d_value).remainder );
+  }
+
   /** Raise this Integer to the power <code>exp</code>.
    *
    * @param exp the exponent
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index b065dca23..4b2ab1a79 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -123,6 +123,9 @@ public:
   Integer operator/(const Integer& y) const {
     return Integer( d_value / y.d_value );
   }
+  Integer operator%(const Integer& y) const {
+    return Integer( d_value % y.d_value );
+  }
 
   /** Raise this Integer to the power <code>exp</code>.
    *