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

diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index 7c0660a8301e40ac187e19fc955954e1096ac2e6..c24897c8d46ca59756a9e948b6189687c05892bc 100644 (file)
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -2,9 +2,9 @@
 /*! \file proof_utils.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Guy Katz, Andres Noetzli
+ **   Liana Hadarean, Guy Katz, 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
@@ -118,10 +118,6 @@ inline Expr mkTrue() {
 inline Expr mkFalse() {
   return NodeManager::currentNM()->toExprManager()->mkConst<bool>(false);
 }
-inline BitVector mkBitVectorOnes(unsigned size) {
-  Assert(size > 0);
-  return BitVector(1, Integer(1)).signExtend(size - 1);
-}
 
 inline Expr mkExpr(Kind k , Expr expr) {
   return NodeManager::currentNM()->toExprManager()->mkExpr(k, expr);
@@ -135,7 +131,7 @@ inline Expr mkExpr(Kind k , std::vector<Expr>& children) {
 
 
 inline Expr mkOnes(unsigned size) {
-  BitVector val = mkBitVectorOnes(size);
+  BitVector val = BitVector::mkOnes(size);
   return NodeManager::currentNM()->toExprManager()->mkConst<BitVector>(val);
 }
 

diff --git a/src/theory/bv/bvgauss.cpp b/src/theory/bv/bvgauss.cpp
index 0e20885417b78912b6b1ed36e2ee48a0bf036279..e36ef3aef4b81ac4fd966a15888c9f2f7f5a8ea5 100644 (file)
--- 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 6a36b61a4b070363a71073c937ccb5ebd469f9eb..c2f6620aadd9f4372ac527fb3f19fe02562ea901 100644 (file)
--- 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 acd3beee37fb1039747d45e6142953a5790b5cd3..9e8a1f7dc2e9d5244d3938347f01c5b6309e37af 100644 (file)
--- 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 54b0cedab9d9c0e985eef5c4c6fe67b63ad2e340..553ffaf51dd3850f35e05565828033bb10231178 100644 (file)
--- 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);

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index be0e4bb31b865f60a8d30088116be2d3cecbf8d3..f9f66a0befbabd84a8dc02d7e0e26b2c4eabbf67 100644 (file)
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -286,7 +286,7 @@ static Node getScBvSltSgt(bool pol, Kind k, Node x, Node t)
        * (distinct t min)
        * where
        * min is the minimum signed value with getSize(min) = w  */
-      Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+      Node min = bv::utils::mkMinSigned(w);
       Node scl = nm->mkNode(DISTINCT, min, t);
       Node scr = nm->mkNode(k, x, t);
       sc = nm->mkNode(IMPLIES, scl, scr);
@@ -309,7 +309,7 @@ static Node getScBvSltSgt(bool pol, Kind k, Node x, Node t)
        * (distinct t max)
        * where
        * max is the signed maximum value with getSize(max) = w  */
-      Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w));
+      Node max = bv::utils::mkMaxSigned(w);
       Node scl = nm->mkNode(DISTINCT, t, max);
       Node scr = nm->mkNode(k, x, t);
       sc = nm->mkNode(IMPLIES, scl, scr);
@@ -433,7 +433,7 @@ static Node getScBvMult(bool pol,
        * (bvsge (bvand (bvor (bvneg s) s) max) t)
        * where
        * max is the signed maximum value with getSize(max) = w  */
-      Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w));
+      Node max = bv::utils::mkMaxSigned(w);
       Node o = nm->mkNode(BITVECTOR_OR, nm->mkNode(BITVECTOR_NEG, s), s);
       Node a = nm->mkNode(BITVECTOR_AND, o, max);
       scl = nm->mkNode(BITVECTOR_SGE, a, t);
@@ -715,7 +715,7 @@ static Node getScBvUrem(bool pol,
          * where
          * z = 0 with getSize(z) = w
          * and max is the maximum signed value with getSize(max) = w  */
-        Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w));
+        Node max = bv::utils::mkMaxSigned(w);
         Node nt = nm->mkNode(BITVECTOR_NOT, nm->mkNode(BITVECTOR_NEG, s));
         Node i1 = nm->mkNode(IMPLIES,
             nm->mkNode(BITVECTOR_SGT, s, z), nm->mkNode(BITVECTOR_SLT, t, nt));
@@ -766,7 +766,7 @@ static Node getScBvUrem(bool pol,
          * (or (bvult t min) (bvsge t s))
          * where
          * min is the minimum signed value with getSize(min) = w  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+        Node min = bv::utils::mkMinSigned(w);
         Node o1 = nm->mkNode(BITVECTOR_ULT, t, min);
         Node o2 = nm->mkNode(BITVECTOR_SGE, t, s);
         scl = nm->mkNode(OR, o1, o2);
@@ -992,7 +992,7 @@ static Node getScBvUdiv(bool pol,
          * where
          * z = 0 with getSize(z) = w
          * and min is the minimum signed value with getSize(min) = w  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+        Node min = bv::utils::mkMinSigned(w);
         Node sle = nm->mkNode(BITVECTOR_SLE, t, z);
         Node div = nm->mkNode(BITVECTOR_UDIV_TOTAL, min, s);
         Node slt = nm->mkNode(BITVECTOR_SLT, div, t);
@@ -1008,7 +1008,7 @@ static Node getScBvUdiv(bool pol,
          * where
          * ones = ~0 with getSize(ones) = w
          * and max is the maximum signed value with getSize(max) = w  */
-        Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w));
+        Node max = bv::utils::mkMaxSigned(w);
         Node ones = bv::utils::mkOnes(w);
         Node udiv1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s);
         Node udiv2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, max, s);
@@ -1077,7 +1077,7 @@ static Node getScBvUdiv(bool pol,
          * where
          * ones = ~0 with getSize(ones) = w
          * and max is the maximum signed value with getSize(max) = w  */
-        Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w));
+        Node max = bv::utils::mkMaxSigned(w);
         Node ones = bv::utils::mkOnes(w);
         Node div1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, ones, s);
         Node sgt1 = nm->mkNode(BITVECTOR_SGT, div1, t);
@@ -1098,7 +1098,7 @@ static Node getScBvUdiv(bool pol,
         Node mul = nm->mkNode(BITVECTOR_MULT, s, t);
         Node div1 = nm->mkNode(BITVECTOR_UDIV_TOTAL, mul, s);
         Node o1 = nm->mkNode(EQUAL, div1, t);
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+        Node min = bv::utils::mkMinSigned(w);
         Node sle = nm->mkNode(BITVECTOR_SLE, t, z);
         Node div2 = nm->mkNode(BITVECTOR_UDIV_TOTAL, min, s);
         Node slt = nm->mkNode(BITVECTOR_SLT, div2, t);
@@ -1350,7 +1350,7 @@ static Node getScBvAndOr(bool pol,
        * (bvslt t (bvor s max))
        * where
        * max is the signed maximum value with getSize(max) = w  */
-      Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w));
+      Node max = bv::utils::mkMaxSigned(w);
       scl = nm->mkNode(BITVECTOR_SLT, t, nm->mkNode(k, s, max));
     }
     else
@@ -1362,7 +1362,7 @@ static Node getScBvAndOr(bool pol,
          * (bvuge s (bvand t min))
          * where
          * min is the signed minimum value with getSize(min) = w  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+        Node min = bv::utils::mkMinSigned(w);
         scl = nm->mkNode(BITVECTOR_UGE, s, nm->mkNode(BITVECTOR_AND, t, min));
       }
       else
@@ -1372,7 +1372,7 @@ static Node getScBvAndOr(bool pol,
          * (bvsge t (bvor s min))
          * where
          * min is the signed minimum value with getSize(min) = w  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+        Node min = bv::utils::mkMinSigned(w);
         scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_OR, s, min));
       }
     }
@@ -1623,7 +1623,7 @@ static Node getScBvLshr(bool pol,
          * (bvslt t (bvlshr (bvshl max s) s))
          * where
          * max is the signed maximum value with getSize(max) = w  */
-        Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w));
+        Node max = bv::utils::mkMaxSigned(w);
         Node shl = nm->mkNode(BITVECTOR_SHL, max, s);
         Node lshr = nm->mkNode(BITVECTOR_LSHR, shl, s);
         scl = nm->mkNode(BITVECTOR_SLT, t, lshr);
@@ -1661,7 +1661,7 @@ static Node getScBvLshr(bool pol,
          * (or (bvult t min) (bvsge t s))
          * where
          * min is the minimum signed value with getSize(min) = w  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+        Node min = bv::utils::mkMinSigned(w);
         Node ult = nm->mkNode(BITVECTOR_ULT, t, min);
         Node sge = nm->mkNode(BITVECTOR_SGE, t, s);
         scl = ult.orNode(sge);
@@ -1839,7 +1839,7 @@ static Node getScBvAshr(bool pol,
          * (or (bvult s min) (bvuge t s))
          * where
          * min is the minimum signed value with getSize(min) = w  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+        Node min = bv::utils::mkMinSigned(w);
         Node ult = nm->mkNode(BITVECTOR_ULT, s, min);
         Node uge = nm->mkNode(BITVECTOR_UGE, t, s);
         scl = ult.orNode(uge);
@@ -1857,7 +1857,7 @@ static Node getScBvAshr(bool pol,
          * (bvslt (bvashr min s) t)
          * where
          * min is the minimum signed value with getSize(min) = w  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+        Node min = bv::utils::mkMinSigned(w);
         scl = nm->mkNode(BITVECTOR_SLT, nm->mkNode(BITVECTOR_ASHR, min, s), t);
       }
       else
@@ -1867,7 +1867,7 @@ static Node getScBvAshr(bool pol,
          * (bvsge (bvlshr max s) t)
          * where
          * max is the signed maximum value with getSize(max) = w  */
-        Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w));
+        Node max = bv::utils::mkMaxSigned(w);
         scl = nm->mkNode(BITVECTOR_SGE, nm->mkNode(BITVECTOR_LSHR, max, s), t);
       }
     }
@@ -1898,7 +1898,7 @@ static Node getScBvAshr(bool pol,
   else
   {
     Assert(litk == BITVECTOR_SGT);
-    Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w));
+    Node max = bv::utils::mkMaxSigned(w);
     if (idx == 0)
     {
       Node lshr = nm->mkNode(BITVECTOR_LSHR, max, s);
@@ -2114,7 +2114,7 @@ static Node getScBvShl(bool pol,
          * (bvslt (bvshl (bvlshr min s) s) t)
          * where
          * min is the signed minimum value with getSize(min) = w  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+        Node min = bv::utils::mkMinSigned(w);
         Node lshr = nm->mkNode(BITVECTOR_LSHR, min, s);
         Node shl = nm->mkNode(BITVECTOR_SHL, lshr, s);
         scl = nm->mkNode(BITVECTOR_SLT, shl, t);
@@ -2126,7 +2126,7 @@ static Node getScBvShl(bool pol,
          * (bvsge (bvand (bvshl max s) max) t)
          * where
          * max is the signed maximum value with getSize(max) = w  */
-        Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w));
+        Node max = bv::utils::mkMaxSigned(w);
         Node shl = nm->mkNode(BITVECTOR_SHL, max, s);
         scl = nm->mkNode(BITVECTOR_SGE, nm->mkNode(BITVECTOR_AND, shl, max), t);
       }
@@ -2140,7 +2140,7 @@ static Node getScBvShl(bool pol,
          * (bvult (bvshl min s) (bvadd t min))
          * where
          * min is the signed minimum value with getSize(min) = w  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+        Node min = bv::utils::mkMinSigned(w);
         Node shl = nm->mkNode(BITVECTOR_SHL, min, s);
         Node add = nm->mkNode(BITVECTOR_PLUS, t, min);
         scl = nm->mkNode(BITVECTOR_ULT, shl, add);
@@ -2167,7 +2167,7 @@ static Node getScBvShl(bool pol,
          * (bvslt t (bvand (bvshl max s) max))
          * where
          * max is the signed maximum value with getSize(max) = w  */
-        Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w));
+        Node max = bv::utils::mkMaxSigned(w);
         Node shl = nm->mkNode(BITVECTOR_SHL, max, s);
         scl = nm->mkNode(BITVECTOR_SLT, t, nm->mkNode(BITVECTOR_AND, shl, max));
       }
@@ -2178,7 +2178,7 @@ static Node getScBvShl(bool pol,
          * (bvult (bvlshr t (bvlshr t s)) min)
          * where
          * min is the signed minimum value with getSize(min) = w  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+        Node min = bv::utils::mkMinSigned(w);
         Node ts = nm->mkNode(BITVECTOR_LSHR, t, s);
         scl = nm->mkNode(BITVECTOR_ULT, nm->mkNode(BITVECTOR_LSHR, t, ts), min);
       }
@@ -2200,7 +2200,7 @@ static Node getScBvShl(bool pol,
          * (bvult (bvlshr t s) min)
          * where
          * min is the signed minimum value with getSize(min) = w  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w));
+        Node min = bv::utils::mkMinSigned(w);
         scl = nm->mkNode(BITVECTOR_ULT, nm->mkNode(BITVECTOR_LSHR, t, s), min);
       }
     }
@@ -2500,7 +2500,7 @@ static Node getScBvConcat(bool pol,
          * (=> (= tx min) (bvult s2 t2))
          * where
          * min is the signed minimum value with getSize(min) = wx  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(wx));
+        Node min = bv::utils::mkMinSigned(wx);
         Node ult = nm->mkNode(BITVECTOR_ULT, s2, t2);
         scl = nm->mkNode(IMPLIES, tx.eqNode(min), ult);
       }
@@ -2510,7 +2510,7 @@ static Node getScBvConcat(bool pol,
          * (=> (= tx max) (bvuge s2 t2))
          * where
          * max is the signed maximum value with getSize(max) = wx  */
-        Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(wx));
+        Node max = bv::utils::mkMaxSigned(wx);
         Node uge = nm->mkNode(BITVECTOR_UGE, s2, t2);
         scl = nm->mkNode(IMPLIES, tx.eqNode(max), uge);
       }
@@ -2583,7 +2583,7 @@ static Node getScBvConcat(bool pol,
          * (=> (= tx max) (bvugt s2 t2))
          * where
          * max is the signed maximum value with getSize(max) = wx  */
-        Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(wx));
+        Node max = bv::utils::mkMaxSigned(wx);
         Node ugt = nm->mkNode(BITVECTOR_UGT, s2, t2);
         scl = nm->mkNode(IMPLIES, tx.eqNode(max), ugt);
       }
@@ -2594,7 +2594,7 @@ static Node getScBvConcat(bool pol,
          * (=> (= tx min) (bvule s2 t2))
          * where
          * min is the signed minimum value with getSize(min) = wx  */
-        Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(wx));
+        Node min = bv::utils::mkMinSigned(wx);
         Node ule = nm->mkNode(BITVECTOR_ULE, s2, t2);
         scl = nm->mkNode(IMPLIES, tx.eqNode(min), ule);
       }
@@ -2753,7 +2753,7 @@ static Node getScBvSext(bool pol,
        * (bvslt ((_ sign_extend ws) min) t)
        * where
        * min is the signed minimum value with getSize(min) = w - ws  */
-      Node min = bv::utils::mkConst(bv::utils::mkBitVectorMinSigned(w - ws));
+      Node min = bv::utils::mkMinSigned(w - ws);
       Node ext = bv::utils::mkSignExtend(min, ws);
       scl = nm->mkNode(BITVECTOR_SLT, ext, t);
     }
@@ -2776,7 +2776,7 @@ static Node getScBvSext(bool pol,
       Node z = bv::utils::mkZero(ws + 1);
       Node n = bv::utils::mkOnes(ws + 1);
       Node o1 = nm->mkNode(OR, ext1.eqNode(z), ext1.eqNode(n));
-      Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w - ws));
+      Node max = bv::utils::mkMaxSigned(w - ws);
       Node ext2 = bv::utils::mkConcat(bv::utils::mkZero(ws), max);
       Node o2 = nm->mkNode(BITVECTOR_SLT, t, ext2);
       scl = nm->mkNode(OR, o1, o2);
@@ -2792,7 +2792,7 @@ static Node getScBvSext(bool pol,
        * (bvslt t ((_ zero_extend ws) max))
        * where
        * max is the signed maximum value with getSize(max) = w - ws  */
-      Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w - ws));
+      Node max = bv::utils::mkMaxSigned(w - ws);
       Node ext = bv::utils::mkConcat(bv::utils::mkZero(ws), max);
       scl = nm->mkNode(BITVECTOR_SLT, t, ext);
     }
@@ -2803,7 +2803,7 @@ static Node getScBvSext(bool pol,
        * (bvsge t (bvnot ((_ zero_extend ws) max)))
        * where
        * max is the signed maximum value with getSize(max) = w - ws  */
-      Node max = bv::utils::mkConst(bv::utils::mkBitVectorMaxSigned(w - ws));
+      Node max = bv::utils::mkMaxSigned(w - ws);
       Node ext = bv::utils::mkConcat(bv::utils::mkZero(ws), max);
       scl = nm->mkNode(BITVECTOR_SGE, t, nm->mkNode(BITVECTOR_NOT, ext));
     }

diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 0c4ea4c3f9c6970adda07d876a4b95e13238584c..114b111cb462b8c20bb4b8d563bf8b0e9befc024 100644 (file)
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -2,9 +2,9 @@
 /*! \file bitvector.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Dejan Jovanovic, Morgan Deters
+ **   Aina Niemetz, Liana Hadarean, Dejan Jovanovic
  ** 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
@@ -375,8 +375,32 @@ public:
     return BitVector(d_size, res);
   }
 
+  /* -----------------------------------------------------------------------
+   ** Static helpers.
+   * ----------------------------------------------------------------------- */
+
+  /* Create bit-vector of ones of given size. */
+  static BitVector mkOnes(unsigned size)
+  {
+    CheckArgument(size > 0, size);
+    return BitVector(1, Integer(1)).signExtend(size - 1);
+  }
+
+  /* Create bit-vector representing the minimum signed value of given size. */
+  static BitVector mkMinSigned(unsigned size)
+  {
+    CheckArgument(size > 0, size);
+    return BitVector(size).setBit(size - 1);
+  }
+
+  /* Create bit-vector representing the maximum signed value of given size. */
+  static BitVector mkMaxSigned(unsigned size)
+  {
+    CheckArgument(size > 0, size);
+    return ~BitVector::mkMinSigned(size);
+  }
 
-private:
+ private:
 
   /**
    * Class invariants: