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.

diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp
index bf51528931bc5b69cb6d73fd7af59a5e6b5330f0..f70eed09670fee98e54b3e903ec844f2557dd18f 100644 (file)
--- 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); 

diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index 9e05ef516cdc2066b7c3f080e4c7d8ee538fd859..affdd05bbdcc26d163dca469e916275da93a0d5a 100644 (file)
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -27,15 +27,6 @@ namespace utils {
 
 /* ------------------------------------------------------------------------- */
 
-uint32_t pow2(uint32_t n)
-{
-  Assert(n < 32);
-  uint32_t one = 1;
-  return one << n;
-}
-
-/* ------------------------------------------------------------------------- */
-
 BitVector mkBitVectorOnes(unsigned size)
 {
   Assert(size > 0);
@@ -63,7 +54,7 @@ unsigned getSize(TNode node)
 
 const bool getBit(TNode node, unsigned i)
 {
-  Assert(i < utils::getSize(node) && node.getKind() == kind::CONST_BITVECTOR);
+  Assert(i < getSize(node) && node.getKind() == kind::CONST_BITVECTOR);
   Integer bit = node.getConst<BitVector>().extract(i, i).getValue();
   return (bit == 1u);
 }
@@ -90,7 +81,7 @@ unsigned getSignExtendAmount(TNode node)
 bool isZero(TNode node)
 {
   if (!node.isConst()) return false;
-  return node == utils::mkConst(utils::getSize(node), 0u);
+  return node == mkZero(getSize(node));
 }
 
 unsigned isPow2Const(TNode node, bool& isNeg)
@@ -136,35 +127,23 @@ bool isBvConstTerm(TNode node)
 
 bool isBVPredicate(TNode node)
 {
-  if (node.getKind() == kind::EQUAL || node.getKind() == kind::BITVECTOR_ULT
-      || node.getKind() == kind::BITVECTOR_SLT
-      || node.getKind() == kind::BITVECTOR_UGT
-      || node.getKind() == kind::BITVECTOR_UGE
-      || node.getKind() == kind::BITVECTOR_SGT
-      || node.getKind() == kind::BITVECTOR_SGE
-      || node.getKind() == kind::BITVECTOR_ULE
-      || node.getKind() == kind::BITVECTOR_SLE
-      || node.getKind() == kind::BITVECTOR_REDOR
-      || node.getKind() == kind::BITVECTOR_REDAND
-      || (node.getKind() == kind::NOT
-          && (node[0].getKind() == kind::EQUAL
-              || node[0].getKind() == kind::BITVECTOR_ULT
-              || node[0].getKind() == kind::BITVECTOR_SLT
-              || node[0].getKind() == kind::BITVECTOR_UGT
-              || node[0].getKind() == kind::BITVECTOR_UGE
-              || node[0].getKind() == kind::BITVECTOR_SGT
-              || node[0].getKind() == kind::BITVECTOR_SGE
-              || node[0].getKind() == kind::BITVECTOR_ULE
-              || node[0].getKind() == kind::BITVECTOR_SLE
-              || node[0].getKind() == kind::BITVECTOR_REDOR
-              || node[0].getKind() == kind::BITVECTOR_REDAND)))
+  Kind k = node.getKind();
+  if (k == kind::NOT)
   {
-    return true;
-  }
-  else
-  {
-    return false;
-  }
+    node = node[0];
+    k = node.getKind();
+  }
+  return k == kind::EQUAL
+         || k == kind::BITVECTOR_ULT
+         || k == kind::BITVECTOR_SLT
+         || k == kind::BITVECTOR_UGT
+         || k == kind::BITVECTOR_UGE
+         || k == kind::BITVECTOR_SGT
+         || k == kind::BITVECTOR_SGE
+         || k == kind::BITVECTOR_ULE
+         || k == kind::BITVECTOR_SLE
+         || k == kind::BITVECTOR_REDOR
+         || k == kind::BITVECTOR_REDAND;
 }
 
 bool isCoreTerm(TNode term, TNodeBoolMap& cache)
@@ -394,18 +373,16 @@ Node mkSignExtend(TNode node, unsigned amount)
 
 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);
+  NodeManager *nm = NodeManager::currentNM();
+  Node extractOp = nm->mkConst<BitVectorExtract>(BitVectorExtract(high, low));
+  return nm->mkNode(extractOp, node);
 }
 
 Node mkBitOf(TNode node, unsigned index)
 {
-  Node bitOfOp =
-      NodeManager::currentNM()->mkConst<BitVectorBitOf>(BitVectorBitOf(index));
-  return NodeManager::currentNM()->mkNode(bitOfOp, node);
+  NodeManager *nm = NodeManager::currentNM();
+  Node bitOfOp = nm->mkConst<BitVectorBitOf>(BitVectorBitOf(index));
+  return nm->mkNode(bitOfOp, node);
 }
 
 /* ------------------------------------------------------------------------- */
@@ -444,13 +421,13 @@ Node mkConcat(TNode node, unsigned repeat)
 Node mkInc(TNode t)
 {
   return NodeManager::currentNM()->mkNode(
-      kind::BITVECTOR_PLUS, t, bv::utils::mkOne(bv::utils::getSize(t)));
+      kind::BITVECTOR_PLUS, t, mkOne(getSize(t)));
 }
 
 Node mkDec(TNode t)
 {
   return NodeManager::currentNM()->mkNode(
-      kind::BITVECTOR_SUB, t, bv::utils::mkOne(bv::utils::getSize(t)));
+      kind::BITVECTOR_SUB, t, mkOne(getSize(t)));
 }
 
 /* ------------------------------------------------------------------------- */
@@ -500,29 +477,6 @@ Node mkConjunction(const std::vector<TNode>& nodes)
 
 /* ------------------------------------------------------------------------- */
 
-void getConjuncts(TNode node, std::set<TNode>& conjuncts)
-{
-  if (node.getKind() != kind::AND)
-  {
-    conjuncts.insert(node);
-  }
-  else
-  {
-    for (unsigned i = 0; i < node.getNumChildren(); ++i)
-    {
-      getConjuncts(node[i], conjuncts);
-    }
-  }
-}
-
-void getConjuncts(std::vector<TNode>& nodes, std::set<TNode>& conjuncts)
-{
-  for (unsigned i = 0, i_end = nodes.size(); i < i_end; ++i)
-  {
-    getConjuncts(nodes[i], conjuncts);
-  }
-}
-
 Node flattenAnd(std::vector<TNode>& queue)
 {
   TNodeSet nodes;
@@ -555,42 +509,6 @@ Node flattenAnd(std::vector<TNode>& queue)
 
 /* ------------------------------------------------------------------------- */
 
-std::string setToString(const std::set<TNode>& nodeSet) {
-  std::stringstream out;
-  out << "[";
-  std::set<TNode>::const_iterator it = nodeSet.begin();
-  std::set<TNode>::const_iterator it_end = nodeSet.end();
-  bool first = true;
-  while (it != it_end) {
-    if (!first) {
-      out << ",";
-    }
-    first = false;
-    out << *it;
-    ++ it;
-  }
-  out << "]";
-  return out.str();
-}
-
-std::string vectorToString(const std::vector<Node>& nodes)
-{
-  std::stringstream out;
-  out << "[";
-  for (unsigned i = 0; i < nodes.size(); ++i)
-  {
-    if (i > 0)
-    {
-      out << ",";
-    }
-    out << nodes[i];
-  }
-  out << "]";
-  return out.str();
-}
-
-/* ------------------------------------------------------------------------- */
-
 // FIXME: dumb code
 void intersect(const std::vector<uint32_t>& v1,
                       const std::vector<uint32_t>& v2,

diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 6f13006323f87230569e91dd085a8c4058115d00..727f5040fe625a323fed36ecc03ecdf0ec9bc8dd 100644 (file)
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -38,22 +38,6 @@ namespace utils {
 typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
 typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 
-/* Compute 2^n. */
-uint32_t pow2(uint32_t n);
-
-/* Compute the greatest common divisor for two objects of Type T.  */
-template <class T>
-T gcd(T a, T b)
-{
-  while (b != 0)
-  {
-    T t = b;
-    b = a % t;
-    a = t;
-  }
-  return a;
-}
-
 /* Create bit-vector of ones of given size. */
 BitVector mkBitVectorOnes(unsigned size);
 /* Create bit-vector representing the minimum signed value of given size. */
@@ -193,18 +177,9 @@ Node mkUmulo(TNode t1, TNode t2);
 /* Create conjunction.  */
 Node mkConjunction(const std::vector<TNode>& nodes);
 
-/* Get a set of all operands of nested and nodes.  */
-void getConjuncts(TNode node, std::set<TNode>& conjuncts);
-void getConjuncts(std::vector<TNode>& nodes, std::set<TNode>& conjuncts);
 /* Create a flattened and node.  */
 Node flattenAnd(std::vector<TNode>& queue);
 
-/* Create a string representing a set of nodes.  */
-std::string setToString(const std::set<TNode>& nodeSet);
-
-/* Create a string representing a vector of nodes.  */
-std::string vectorToString(const std::vector<Node>& nodes);
-
 /* Create the intersection of two vectors of uint32_t. */
 void intersect(const std::vector<uint32_t>& v1,
                const std::vector<uint32_t>& v2,