summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
authorAina Niemetz <aina.niemetz@gmail.com>2018-02-09 22:10:30 -0800
committerGitHub <noreply@github.com>2018-02-09 22:10:30 -0800
commit2ff61502c2df1db8fbdba3b2487fb72aa1e6d509 (patch)
tree5ccadc3415b0543c39b13f16de788f4c2afbfcdb /src/util
parenta70490bc79933a55041f35d5896f79004e578f05 (diff)
Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589)
Diffstat (limited to 'src/util')
-rw-r--r--src/util/bitvector.h30
1 files changed, 27 insertions, 3 deletions
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:
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback