Clean up bv utils (part one). (#1580)

This is part one of an effort to clean up bv utils. It addresses review comments not addressed in
#1566 (changes of moved code), removes unused functions and moves a helper to compute the
gcd over Index.

1 files changed, 27 insertions, 13 deletions

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index bf5152893..f70eed096 100644
--- a/src/theory/bv/slicer.cpp
+++ b/src/theory/bv/slicer.cpp
@@ -2,9 +2,9 @@
 /*! \file slicer.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Tim King, Paul Meng
+ **   Liana Hadarean, Aina Niemetz, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -39,15 +39,15 @@ Base::Base(uint32_t size)
   Assert (d_size > 0); 
 }
 
-  
-void Base::sliceAt(Index index) {
+void Base::sliceAt(Index index)
+{
   Index vector_index = index / 32;
   if (vector_index == d_repr.size())
     return;
-  
+
   Index int_index = index % 32;
-  uint32_t bit_mask = utils::pow2(int_index); 
-  d_repr[vector_index] = d_repr[vector_index] | bit_mask; 
+  uint32_t bit_mask = 1u << int_index;
+  d_repr[vector_index] = d_repr[vector_index] | bit_mask;
 }
 
 void Base::sliceWith(const Base& other) {
@@ -57,17 +57,18 @@ void Base::sliceWith(const Base& other) {
   }
 }
 
-bool Base::isCutPoint (Index index) const {
+bool Base::isCutPoint (Index index) const
+{
   // there is an implicit cut point at the end and begining of the bv
   if (index == d_size || index == 0)
     return true;
-    
+
   Index vector_index = index / 32;
-  Assert (vector_index < d_size); 
+  Assert (vector_index < d_size);
   Index int_index = index % 32;
-  uint32_t bit_mask = utils::pow2(int_index); 
+  uint32_t bit_mask = 1u << int_index;
 
-  return (bit_mask & d_repr[vector_index]) != 0; 
+  return (bit_mask & d_repr[vector_index]) != 0;
 }
 
 void Base::diffCutPoints(const Base& other, Base& res) const {
@@ -311,6 +312,19 @@ void UnionFind::getDecomposition(const ExtractTerm& term, Decomposition& decomp)
     getDecomposition(high_child, decomp); 
   }
 }
+
+/* Compute the greatest common divisor of two indices.  */
+static Index gcd(Index a, Index b)
+{
+  while (b != 0)
+  {
+    Index t = b;
+    b = a % t;
+    a = t;
+  }
+  return a;
+}
+
 /** 
  * May cause reslicings of the decompositions. Must not assume the decompositons
  * are the current normal form. 
@@ -347,7 +361,7 @@ void UnionFind::handleCommonSlice(const Decomposition& decomp1, const Decomposit
     Assert (overlap > 0);
     Index diff = common_size - overlap;
     Assert (diff >= 0);
-    Index granularity = utils::gcd(diff, overlap);
+    Index granularity = gcd(diff, overlap);
     // split the common part 
     for (unsigned i = 0; i < common_size; i+= granularity) {
       split(common, i);