From 2ff61502c2df1db8fbdba3b2487fb72aa1e6d509 Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Fri, 9 Feb 2018 22:10:30 -0800 Subject: [PATCH] Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589) --- src/proof/proof_utils.h | 10 +-- src/theory/bv/bvgauss.cpp | 6 +- .../theory_bv_rewrite_rules_normalization.h | 15 ++--- src/theory/bv/theory_bv_utils.cpp | 46 ++++++------- src/theory/bv/theory_bv_utils.h | 11 ++-- src/theory/quantifiers/bv_inverter.cpp | 64 +++++++++---------- src/util/bitvector.h | 30 ++++++++- 7 files changed, 96 insertions(+), 86 deletions(-) diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h index 7c0660a83..c24897c8d 100644 --- 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(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& children) { inline Expr mkOnes(unsigned size) { - BitVector val = mkBitVectorOnes(size); + BitVector val = BitVector::mkOnes(size); return NodeManager::currentNM()->toExprManager()->mkConst(val); } 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::apply(TNode node) } } BitVector oValue = BitVector(size, static_cast(1)); - BitVector noValue = utils::mkBitVectorOnes(size); + BitVector noValue = BitVector::mkOnes(size); if (children.empty()) { @@ -1046,8 +1046,7 @@ inline Node RewriteRule::apply(TNode node) // this will remove duplicates std::unordered_map 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::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::const_iterator it = @@ -1200,9 +1199,9 @@ inline Node RewriteRule::apply(TNode node) std::vector 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::apply(TNode node) } std::vector 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(false); } -Node mkOnes(unsigned size) -{ - BitVector val = mkBitVectorOnes(size); - return NodeManager::currentNM()->mkConst(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 TNodeBoolMap; typedef std::unordered_set 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 be0e4bb31..f9f66a0be 100644 --- 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 0c4ea4c3f..114b111cb 100644 --- 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: -- 2.30.2