Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589)

4 files changed, 34 insertions, 44 deletions

diff --git a/src/theory/bv/bvgauss.cpp b/src/theory/bv/bvgauss.cpp
index 0e2088541..e36ef3aef 100644
--- a/src/theory/bv/bvgauss.cpp
+++ b/src/theory/bv/bvgauss.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Aina Niemetz
  ** 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
@@ -114,7 +114,7 @@ unsigned BVGaussElim::getMinBwExpr(Node expr)
             }
             else
             {
-              maxval *= utils::mkBitVectorOnes(visited[nn]).getValue();
+              maxval *= BitVector::mkOnes(visited[nn]).getValue();
             }
           }
           unsigned w = maxval.length();
@@ -181,7 +181,7 @@ unsigned BVGaussElim::getMinBwExpr(Node expr)
             }
             else
             {
-              maxval += utils::mkBitVectorOnes(visited[nn]).getValue();
+              maxval += BitVector::mkOnes(visited[nn]).getValue();
             }
           }
           unsigned w = maxval.length();
diff --git a/src/theory/bv/theory_bv_rewrite_rules_normalization.h b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
index 6a36b61a4..c2f6620aa 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_normalization.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_normalization.h
@@ -451,7 +451,7 @@ inline Node RewriteRule<MultSimplify>::apply(TNode node)
     }
   }
   BitVector oValue = BitVector(size, static_cast<unsigned>(1));
-  BitVector noValue = utils::mkBitVectorOnes(size);
+  BitVector noValue = BitVector::mkOnes(size);
 
   if (children.empty())
   {
@@ -1046,8 +1046,7 @@ inline Node RewriteRule<AndSimplify>::apply(TNode node)
   // this will remove duplicates
   std::unordered_map<TNode, Count, TNodeHashFunction> subterms;
   unsigned size = utils::getSize(node);
-  BitVector constant = utils::mkBitVectorOnes(size);
-
+  BitVector constant = BitVector::mkOnes(size);
   for (unsigned i = 0; i < node.getNumChildren(); ++i)
   {
     TNode current = node[i];
@@ -1077,9 +1076,9 @@ inline Node RewriteRule<AndSimplify>::apply(TNode node)
     return utils::mkZero(size);
   }
 
-  if (constant != utils::mkBitVectorOnes(size))
+  if (constant != BitVector::mkOnes(size))
   {
-    children.push_back(utils::mkConst(constant));
+    children.push_back(utils::mkConst(constant)); 
   }
 
   std::unordered_map<TNode, Count, TNodeHashFunction>::const_iterator it =
@@ -1200,9 +1199,9 @@ inline Node RewriteRule<OrSimplify>::apply(TNode node)
 
   std::vector<Node> children;
 
-  if (constant == utils::mkBitVectorOnes(size))
+  if (constant == BitVector::mkOnes(size))
   {
-    return utils::mkOnes(size);
+    return utils::mkOnes(size); 
   }
 
   if (constant != BitVector(size, (unsigned)0))
@@ -1326,7 +1325,7 @@ inline Node RewriteRule<XorSimplify>::apply(TNode node)
   }
 
   std::vector<BitVector> xorConst;
-  BitVector true_bv = utils::mkBitVectorOnes(size);
+  BitVector true_bv = BitVector::mkOnes(size);
   BitVector false_bv(size, (unsigned)0);
 
   if (true_count)
diff --git a/src/theory/bv/theory_bv_utils.cpp b/src/theory/bv/theory_bv_utils.cpp
index acd3beee3..9e8a1f7dc 100644
--- a/src/theory/bv/theory_bv_utils.cpp
+++ b/src/theory/bv/theory_bv_utils.cpp
@@ -27,26 +27,6 @@ namespace utils {
 
 /* ------------------------------------------------------------------------- */
 
-BitVector mkBitVectorOnes(unsigned size)
-{
-  Assert(size > 0);
-  return BitVector(1, Integer(1)).signExtend(size - 1);
-}
-
-BitVector mkBitVectorMinSigned(unsigned size)
-{
-  Assert(size > 0);
-  return BitVector(size).setBit(size - 1);
-}
-
-BitVector mkBitVectorMaxSigned(unsigned size)
-{
-  Assert(size > 0);
-  return ~mkBitVectorMinSigned(size);
-}
-
-/* ------------------------------------------------------------------------- */
-
 unsigned getSize(TNode node)
 {
   return node.getType().getBitVectorSize();
@@ -235,22 +215,36 @@ Node mkFalse()
   return NodeManager::currentNM()->mkConst<bool>(false);
 }
 
-Node mkOnes(unsigned size)
-{
-  BitVector val = mkBitVectorOnes(size);
-  return NodeManager::currentNM()->mkConst<BitVector>(val);
-}
-
 Node mkZero(unsigned size)
 {
+  Assert(size > 0);
   return mkConst(size, 0u);
 }
 
 Node mkOne(unsigned size)
 {
+  Assert(size > 0);
   return mkConst(size, 1u);
 }
 
+Node mkOnes(unsigned size)
+{
+  Assert(size > 0);
+  return mkConst(BitVector::mkOnes(size));
+}
+
+Node mkMinSigned(unsigned size)
+{
+  Assert(size > 0);
+  return mkConst(BitVector::mkMinSigned(size));
+}
+
+Node mkMaxSigned(unsigned size)
+{
+  Assert(size > 0);
+  return mkConst(BitVector::mkMaxSigned(size));
+}
+
 /* ------------------------------------------------------------------------- */
 
 Node mkConst(unsigned size, unsigned int value)
diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h
index 54b0cedab..553ffaf51 100644
--- a/src/theory/bv/theory_bv_utils.h
+++ b/src/theory/bv/theory_bv_utils.h
@@ -38,13 +38,6 @@ namespace utils {
 typedef std::unordered_map<TNode, bool, TNodeHashFunction> TNodeBoolMap;
 typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
 
-/* Create bit-vector of ones of given size. */
-BitVector mkBitVectorOnes(unsigned size);
-/* Create bit-vector representing the minimum signed value of given size. */
-BitVector mkBitVectorMinSigned(unsigned size);
-/* Create bit-vector representing the maximum signed value of given size. */
-BitVector mkBitVectorMaxSigned(unsigned size);
-
 /* Get the bit-width of given node. */
 unsigned getSize(TNode node);
 
@@ -86,6 +79,10 @@ Node mkOnes(unsigned size);
 Node mkZero(unsigned size);
 /* Create bit-vector node representing a bit-vector value one of given size. */
 Node mkOne(unsigned size);
+/* Create bit-vector node representing the min signed value of given size. */
+Node mkMinSigned(unsigned size);
+/* Create bit-vector node representing the max signed value of given size. */
+Node mkMaxSigned(unsigned size);
 
 /* Create bit-vector constant of given size and value. */
 Node mkConst(unsigned size, unsigned int value);