getting ready for slicing bitvectors

5 files changed, 145 insertions, 14 deletions

diff --git a/src/theory/bv/Makefile.am b/src/theory/bv/Makefile.am
index fdace42b4..db750575f 100644
--- a/src/theory/bv/Makefile.am
+++ b/src/theory/bv/Makefile.am
@@ -15,6 +15,7 @@ libbv_la_SOURCES = \
 	theory_bv_rewriter.h \
 	theory_bv_rewriter.cpp \
 	equality_engine.h \
-	equality_engine.cpp 
+	equality_engine.cpp \
+	slice_manager.h
 
 EXTRA_DIST = kinds
diff --git a/src/theory/bv/equality_engine.h b/src/theory/bv/equality_engine.h
index 8f596723c..000e93a7b 100644
--- a/src/theory/bv/equality_engine.h
+++ b/src/theory/bv/equality_engine.h
@@ -112,7 +112,6 @@ public:
    * Set the class representative.
    */
   inline void setFind(size_t findId) { d_findId = findId; }
-
 };
 
 
@@ -134,6 +133,9 @@ class EqualityEngine {
   /** Number of asserted equalities we have so far */
   context::CDO<size_t> d_assertedEqualitiesCount;
 
+  /** Number of functions in the system */
+  context::CDO<size_t> d_functionsCount;
+
   /**
    * We keep a list of asserted equalities. Not among original terms, but
    * among the class representatives.
@@ -262,7 +264,7 @@ public:
    * the owner information.
    */
   EqualityEngine(OwnerClass& owner, context::Context* context)
-  : d_notify(owner), d_assertedEqualitiesCount(context, 0) {
+  : d_notify(owner), d_assertedEqualitiesCount(context, 0), d_functionsCount(context, 0) {
     Debug("equality") << "EqualityEdge::EqualityEdge(): id_null = " << BitSizeTraits::id_null <<
         ", trigger_id_null = " << BitSizeTraits::trigger_id_null << std::endl;
   }
@@ -305,6 +307,11 @@ public:
    */
   size_t addTrigger(TNode t1, TNode t2);
 
+  /**
+   * Adds a new function to the equality engine. The funcions are not of fixed arity!
+   */
+  inline size_t newFunction() { d_functionsCount = d_functionsCount + 1; return d_functionsCount; }
+
 };
 
 template <typename OwnerClass, typename NotifyClass>
diff --git a/src/theory/bv/slice_manager.h b/src/theory/bv/slice_manager.h
new file mode 100644
index 000000000..b31f721a0
--- /dev/null
+++ b/src/theory/bv/slice_manager.h
@@ -0,0 +1,95 @@
+/*
+ * slice_manager.h
+ *
+ *  Created on: Feb 16, 2011
+ *      Author: dejan
+ */
+
+#pragma once
+
+#include "theory/bv/theory_bv_utils.h"
+#include "theory/bv/equality_engine.h"
+
+#include <vector>
+
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+/**
+ * Slice manager should keep the database of slices for the core theory leaf terms, for example
+ *
+ * term                           core leaf terms
+ * ----------------------------------------------
+ * (x + y)[31:0]                  x + y
+ * a[10:0]@a[11:10]@(b + c)[1:0]  a, b, (b + c)
+ * (a << 5)[10]                   (a << 5)
+ *
+ * If an (dis-)equality is added to the system, we refine the slicing in order to align the extracts, for example
+ *
+ * equality                       slicing
+ * ----------------------------------------------
+ * x = y                          x[32,0], y[32,0]
+ * x@y = z                        x[32,0], y[32,0], z[64,32,0]
+ * x@y = z, x[31:16] = y[15:0]    x[32,16,0], y[32,16,0], z[64,48,32,16,0]
+ *
+ * As a result of the slicing the slicing equalities are added to the equality engine, using the (associative)
+ * concat function that is generated for the equality manager, for example
+ *
+ * equality                       added equalities
+ * ----------------------------------------------
+ * x = y                          none
+ * x@y = z                        z = concat(z[63:32],z[31:0])
+ * x@y = z, x[31:16] = y[15:0]    z = concat(z[63:32],z[31:0]),
+ *                                z[63:32] = concat(z[63:48], z[47:32]),
+ *                                z[31:0] = concat(z[31:16], z[15:0])
+ *
+ * In the last example, since concat is associative, the equality engine will know that z = concat(z[63:48], z[47:32],
+ * z[31:16], z[15:0]).
+ *
+ */
+template <class TheoryBitvector>
+class SliceManager {
+
+  /** The equality engine theory of bit-vectors is using */
+  typedef typename TheoryBitvector::BvEqualityEngine EqualityEngine;
+
+  /** The theory of bitvectors */
+  TheoryBitvector& d_theoryBitvector;
+
+  /** The equality engine */
+  EqualityEngine& d_equalityEngine;
+
+  /** The id of the concatenation function */
+  size_t d_concatFunctionId;
+
+public:
+
+  SliceManager(TheoryBitvector& theoryBitvector)
+  : d_theoryBitvector(theoryBitvector), d_equalityEngine(theoryBitvector.getEqualityEngine()) {
+    // We register the concatentation with the equality engine
+    d_concatFunctionId = d_equalityEngine.newFunction();
+  }
+
+  inline size_t getConcatFunctionId() const { return d_concatFunctionId; }
+
+  /**
+   * Adds the equality (lhs = rhs) to the slice manager. This will not add the equalities to the equality manager,
+   * but will slice the equality according to the current slicing in order to align all the slices. The terms that
+   * get slices get sent to the theory engine as equalities, i.e if we slice x[10:0] into x[10:5]@x[4:0] equality
+   * engine gets the assertion x[10:0] = concat(x[10:5], x[4:0]).
+   */
+  inline void addEquality(TNode lhs, TNode rhs, std::vector<Node>& lhsSlices, std::vector<Node>& rhsSlices);
+};
+
+
+template <class TheoryBitvector>
+void SliceManager<TheoryBitvector>::addEquality(TNode lhs, TNode rhs, std::vector<Node>& lhsSlices, std::vector<Node>& rhsSlices) {
+  Debug("theory::bv::slicing") << "addEquality(" << lhs << "," << rhs << ")";
+  lhsSlices.push_back(lhs);
+  rhsSlices.push_back(rhs);
+}
+
+} // Namespace bv
+} // Namespace theory
+} // Namespace CVC4
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index c9e7c397e..cb8b95751 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -55,19 +55,36 @@ void TheoryBV::check(Effort e) {
     // Do the right stuff
     switch (assertion.getKind()) {
     case kind::EQUAL: {
-      bool ok = d_eqEngine.addEquality(assertion[0], assertion[1]);
-      if (!ok) return;
+
+      // Slice the equality
+      std::vector<Node> lhsSlices, rhsSlices;
+      d_sliceManager.addEquality(assertion[0], assertion[1], lhsSlices, rhsSlices);
+      Assert(lhsSlices.size() == rhsSlices.size());
+
+      // Add the equality to the equality engine
+      for (int i = 0, i_end = lhsSlices.size(); i != i_end; ++ i) {
+        bool ok = d_eqEngine.addEquality(lhsSlices[i], rhsSlices[i]);
+        if (!ok) return;
+      }
       break;
     }
     case kind::NOT: {
       // We need to check this as the equality trigger might have been true when we made it
       TNode equality = assertion[0];
-      if (d_eqEngine.areEqual(equality[0], equality[1])) {
-        vector<TNode> assertions;
-        d_eqEngine.getExplanation(equality[0], equality[1], assertions);
-        assertions.push_back(assertion);
-        d_out->conflict(mkAnd(assertions));
-        return;
+
+      // Slice the equality
+      std::vector<Node> lhsSlices, rhsSlices;
+      d_sliceManager.addEquality(equality[0], equality[1], lhsSlices, rhsSlices);
+      Assert(lhsSlices.size() == rhsSlices.size());
+
+      for (int i = 0, i_end = lhsSlices.size(); i != i_end; ++ i) {
+        if (d_eqEngine.areEqual(lhsSlices[i], rhsSlices[i])) {
+          vector<TNode> assertions;
+          d_eqEngine.getExplanation(lhsSlices[i], rhsSlices[i], assertions);
+          assertions.push_back(assertion);
+          d_out->conflict(mkAnd(assertions));
+          return;
+        }
       }
       break;
     }
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index dfae3b965..14a526e36 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -24,7 +24,8 @@
 #include "theory/theory.h"
 #include "context/context.h"
 #include "context/cdset.h"
-#include "equality_engine.h"
+#include "theory/bv/equality_engine.h"
+#include "theory/bv/slice_manager.h"
 
 namespace CVC4 {
 namespace theory {
@@ -45,10 +46,16 @@ public:
     }
   };
 
+  typedef EqualityEngine<TheoryBV, EqualityNotify> BvEqualityEngine;
+
 private:
 
+
   /** Equality reasoning engine */
-  EqualityEngine<TheoryBV, EqualityNotify> d_eqEngine;
+  BvEqualityEngine d_eqEngine;
+
+  /** Slice manager */
+  SliceManager<TheoryBV> d_sliceManager;
 
   /** Equality triggers indexed by ids from the equality manager */
   std::vector<Node> d_triggers;
@@ -62,7 +69,11 @@ private:
 public:
 
   TheoryBV(context::Context* c, OutputChannel& out) :
-    Theory(THEORY_BV, c, out), d_eqEngine(*this, c), d_assertions(c) {
+    Theory(THEORY_BV, c, out), d_eqEngine(*this, c), d_sliceManager(*this), d_assertions(c) {
+  }
+
+  BvEqualityEngine& getEqualityEngine() {
+    return d_eqEngine;
   }
 
   void preRegisterTerm(TNode n);