bitvector rewriting for the core theory and testcases

8 files changed, 477 insertions, 7 deletions

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);
+}
+
+
+}
+}
+}
+}