Moved and simplified bv::utils::intersect. (#1614)

Tested against the recursive implementation with a temporary assertion on regression tests
with --bv-eq-slicer=auto.

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index 851db1526f92c7ceb5b83051cb74fb7df3e3b884..fa234fcde7d8e60cfcdf76a8e7505ca89794639a 100644 (file)
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -20,13 +20,35 @@
 #include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::bv;
 using namespace std; 
 
 
-const TermId CVC4::theory::bv::UndefinedId = -1; 
+namespace CVC4 {
+namespace theory {
+namespace bv {
+
+const TermId UndefinedId = -1;
+
+namespace {
+
+void intersect(const std::vector<TermId>& v1,
+               const std::vector<TermId>& v2,
+               std::vector<TermId>& intersection)
+{
+  for (const TermId id1 : v1)
+  {
+    for (const TermId id2 : v2)
+    {
+      if (id2 == id1)
+      {
+        intersection.push_back(id1);
+        break;
+      }
+    }
+  }
+}
+
+}  // namespace
 
 /**
  * Base
@@ -375,18 +397,19 @@ void UnionFind::alignSlicings(const ExtractTerm& term1, const ExtractTerm& term2
   Debug("bv-slicer") << "                         " << term2.debugPrint() << endl;
   NormalForm nf1(term1.getBitwidth());
   NormalForm nf2(term2.getBitwidth());
-  
+
   getNormalForm(term1, nf1);
   getNormalForm(term2, nf2);
 
   Assert (nf1.base.getBitwidth() == nf2.base.getBitwidth());
-  
-  // first check if the two have any common slices 
-  std::vector<TermId> intersection; 
-  utils::intersect(nf1.decomp, nf2.decomp, intersection); 
-  for (unsigned i = 0; i < intersection.size(); ++i) {
-    // handle common slice may change the normal form 
-    handleCommonSlice(nf1.decomp, nf2.decomp, intersection[i]); 
+
+  // first check if the two have any common slices
+  std::vector<TermId> intersection;
+  intersect(nf1.decomp, nf2.decomp, intersection);
+  for (TermId id : intersection)
+  {
+    /* handleCommonSlice() may change the normal form */
+    handleCommonSlice(nf1.decomp, nf2.decomp, id);
   }
   // propagate cuts to a fixpoint 
   bool changed;
@@ -638,3 +661,7 @@ UnionFind::Statistics::~Statistics() {
   smtStatisticsRegistry()->unregisterStat(&d_avgFindDepth);
   smtStatisticsRegistry()->unregisterStat(&d_numAddedEqualities);
 }
+
+}  // namespace bv
+}  // namespace theory
+}  // namespace CVC4

diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 5e9133932b69967ba312517f78687cff2253353a..0e54063864ed3770d5bfbc6e76b83cf3a8cb123c 100644 (file)
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -457,26 +457,6 @@ Node flattenAnd(std::vector<TNode>& queue)
 
 /* ------------------------------------------------------------------------- */
 
-// FIXME: dumb code
-void intersect(const std::vector<uint32_t>& v1,
-                      const std::vector<uint32_t>& v2,
-                      std::vector<uint32_t>& intersection) {
-  for (unsigned i = 0; i < v1.size(); ++i) {
-    bool found = false;
-    for (unsigned j = 0; j < v2.size(); ++j) {
-      if (v2[j] == v1[i]) {
-        found = true;
-        break;
-      }
-    }
-    if (found) {
-      intersection.push_back(v1[i]);
-    }
-  }
-}
-
-/* ------------------------------------------------------------------------- */
-
 }/* CVC4::theory::bv::utils namespace */
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */