diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-12-12 14:32:14 -0800 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-12-12 14:32:14 -0800 |
commit | 282f757fd1c9a5277e9d7053e9a20d792c8b81b0 (patch) | |
tree | 6be658b7a5b569f2ae9392614334453f8e7e126e /src/util | |
parent | 0b75194fc6feb6bd8989c7d3d85571a07af53d56 (diff) | |
parent | 62e9f6d0a34d4f6623381429b51b65ddfae1e86d (diff) |
Merge pull request #2 from CVC4/1.0.x
1.0.x
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/bitvector.h | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 2c178ec2e..4cbcba50e 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -178,23 +178,25 @@ public: Integer prod = d_value * y.d_value; return BitVector(d_size, prod); } - - BitVector unsignedDiv (const BitVector& y) const { + /** + * Total division function that returns 0 when the denominator is 0. + */ + BitVector unsignedDivTotal (const BitVector& y) const { 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)); + return BitVector(d_size, 0u); } 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 { + /** + * Total division function that returns 0 when the denominator is 0. + */ + BitVector unsignedRemTotal(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); - // TODO: decide whether we really want these semantics if (y.d_value == 0) { - return BitVector(d_size, d_value); + return BitVector(d_size, 0u); } CheckArgument(d_value >= 0, this); CheckArgument(y.d_value > 0, y); |