commit for the version of bitvectors that passes all the unit tests

1 files changed, 28 insertions, 1 deletions

diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index ede98004f..fa9762cb7 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -46,7 +46,34 @@ public:
     }
   };
 
-  typedef EqualityEngine<TheoryBV, EqualityNotify, true, true> BvEqualityEngine;
+  struct BVEqualitySettings {
+    static inline bool descend(TNode node) {
+      return node.getKind() == kind::BITVECTOR_CONCAT || node.getKind() == kind::BITVECTOR_EXTRACT;
+    }
+
+    /** Returns true if node1 has preference to node2 as a representative, otherwise node2 is used */
+    static inline bool mergePreference(TNode node1, unsigned node1size, TNode node2, unsigned node2size) {
+      if (node1.getKind() == kind::CONST_BITVECTOR) {
+        Assert(node2.getKind() != kind::CONST_BITVECTOR);
+        return true;
+      }
+      if (node2.getKind() == kind::CONST_BITVECTOR) {
+        Assert(node1.getKind() != kind::CONST_BITVECTOR);
+        return false;
+      }
+      if (node1.getKind() == kind::BITVECTOR_CONCAT) {
+        Assert(node2.getKind() != kind::BITVECTOR_CONCAT);
+        return true;
+      }
+      if (node2.getKind() == kind::BITVECTOR_CONCAT) {
+        Assert(node1.getKind() != kind::BITVECTOR_CONCAT);
+        return false;
+      }
+      return node2size < node1size;
+    }
+  };
+
+  typedef EqualityEngine<TheoryBV, EqualityNotify, BVEqualitySettings> BvEqualityEngine;
 
 private: