diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-28 17:29:01 +0000 |
commit | 65f720aac2d497c6e829d9c76638073a10060e7d (patch) | |
tree | 357035797e31f96a37dce30cb97ddb0aaf8f3bb7 /src/util/bitvector.h | |
parent | c0c351a89871e0a6881668fa1a8d87349ab8af8e (diff) |
Public interface review items:
* Internal uses of CheckArgument changed to AssertArgument/AlwaysAssertArgument()
* Make util/Assert.h cvc4_private instead of public, so AssertionException and friends are now internal-only
* CheckArgument() throws non-AssertionException
* things outside the core library (parsers, driver) use regular C-style assert,
or a public exception type.
* auto-generated documentation for Smt options and internal options
Also, a small fix to SMT-LIBv1 QF_ABV and QF_AUFBV definitions, which were nonstandard.
Diffstat (limited to 'src/util/bitvector.h')
-rw-r--r-- | src/util/bitvector.h | 64 |
1 files changed, 34 insertions, 30 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 185bb55d9..a3d4f1b60 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -23,7 +23,7 @@ #define __CVC4__BITVECTOR_H #include <iostream> -#include "util/Assert.h" +#include "util/exception.h" #include "util/integer.h" namespace CVC4 { @@ -99,8 +99,8 @@ public: return d_value != y.d_value; } - BitVector equals(const BitVector& y) const { - Assert(d_size == y.d_size); + BitVector equals(const BitVector& y) const { + CheckArgument(d_size == y.d_size, y); return d_value == y.d_value; } @@ -118,19 +118,19 @@ public: // xor BitVector operator ^(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); return BitVector(d_size, d_value.bitwiseXor(y.d_value)); } // or BitVector operator |(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); return BitVector(d_size, d_value.bitwiseOr(y.d_value)); } // and BitVector operator &(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); return BitVector(d_size, d_value.bitwiseAnd(y.d_value)); } @@ -162,13 +162,13 @@ public: BitVector operator +(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); Integer sum = d_value + y.d_value; return BitVector(d_size, sum); } BitVector operator -(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); // to maintain the invariant that we are only adding BitVectors of the // same size BitVector one(d_size, Integer(1)); @@ -181,35 +181,38 @@ public: } BitVector operator *(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); Integer prod = d_value * y.d_value; return BitVector(d_size, prod); } BitVector unsignedDiv (const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); // TODO: decide whether we really want these semantics if (y.d_value == 0) { return BitVector(d_size, Integer(0)); } - Assert (d_value >= 0 && y.d_value > 0); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value > 0, y); return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); } BitVector unsignedRem(const BitVector& y) const { - Assert (d_size == y.d_size); + CheckArgument(d_size == y.d_size, y); // TODO: decide whether we really want these semantics if (y.d_value == 0) { return BitVector(d_size, Integer(0)); } - Assert (d_value >= 0 && y.d_value > 0); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value > 0, y); return BitVector(d_size, d_value.floorDivideRemainder(y.d_value)); } bool signedLessThan(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, y); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); Integer a = (*this).toSignedInt(); Integer b = y.toSignedInt(); @@ -217,14 +220,16 @@ public: } bool unsignedLessThan(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, y); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); return d_value < y.d_value; } bool signedLessThanEq(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, y); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); Integer a = (*this).toSignedInt(); Integer b = y.toSignedInt(); @@ -232,8 +237,9 @@ public: } bool unsignedLessThanEq(const BitVector& y) const { - Assert(d_size == y.d_size); - Assert(d_value >= 0 && y.d_value >= 0); + CheckArgument(d_size == y.d_size, this); + CheckArgument(d_value >= 0, this); + CheckArgument(y.d_value >= 0, y); return d_value <= y.d_value; } @@ -269,7 +275,7 @@ public: } // making sure we don't lose information casting - Assert(y.d_value < Integer(1).multiplyByPow2(32)); + CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); uint32_t amount = y.d_value.toUnsignedInt(); Integer res = d_value.multiplyByPow2(amount); return BitVector(d_size, res); @@ -281,7 +287,7 @@ public: } // making sure we don't lose information casting - Assert(y.d_value < Integer(1).multiplyByPow2(32)); + CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); uint32_t amount = y.d_value.toUnsignedInt(); Integer res = d_value.divByPow2(amount); return BitVector(d_size, res); @@ -302,7 +308,7 @@ public: } // making sure we don't lose information casting - Assert(y.d_value < Integer(1).multiplyByPow2(32)); + CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); uint32_t amount = y.d_value.toUnsignedInt(); Integer rest = d_value.divByPow2(amount); @@ -310,7 +316,7 @@ public: if(sign_bit == Integer(0)) { return BitVector(d_size, rest); } - Integer res = rest.oneExtend(d_size - amount, amount); + Integer res = rest.oneExtend(d_size - amount, amount); return BitVector(d_size, res); } @@ -358,17 +364,15 @@ public: inline BitVector::BitVector(const std::string& num, unsigned base) { - AlwaysAssert( base == 2 || base == 16 ); + CheckArgument(base == 2 || base == 16, base); if( base == 2 ) { d_size = num.size(); - } else if( base == 16 ) { - d_size = num.size() * 4; } else { - Unreachable("Unsupported base in BitVector(std::string&, unsigned int)."); + d_size = num.size() * 4; } - d_value = Integer(num,base); + d_value = Integer(num, base); }/* BitVector::BitVector() */ |