diff options
author | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
---|---|---|
committer | Tim King <taking@google.com> | 2015-12-24 05:38:43 -0500 |
commit | a39ad6584c1d61e22e72b53c3838f4f675ed2e19 (patch) | |
tree | ed40cb371c41ac285ca2bf41a82254a36134e132 /src/util | |
parent | 87b0fe9ce10d1e5e9ed5a3e7db77f46bf3f68922 (diff) |
Miscellaneous fixes
- Splitting the two instances of CheckArgument. The template version is now always defined in base/exception.h and is available in a cvc4_public header. This version has lost its variadic version (due to swig not supporting va_list's). The CPP macro version has been renamed PrettyCheckArgument. (Taking suggestions for a better name.) This is now only defined in base/cvc4_assert.h. Only use this in cvc4_private headers and in .cpp files that can use cvc4_private headers. To use a variadic version of CheckArguments, outside of this scope, you need to duplicate this macro locally. See cvc3_compat.cpp for an example.
- Making fitsSignedInt() and fitsUnsignedInt() work more robustly for CLN on 32 bit systems.
- Refactoring ArrayStoreAll to avoid potential problems with circular header inclusions.
- Changing some headers to use iosfwd when possible.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/Makefile.am | 1 | ||||
-rw-r--r-- | src/util/abstract_value.cpp | 5 | ||||
-rw-r--r-- | src/util/abstract_value.h | 2 | ||||
-rw-r--r-- | src/util/bin_heap.h | 1 | ||||
-rw-r--r-- | src/util/bitvector.h | 166 | ||||
-rw-r--r-- | src/util/cardinality.cpp | 42 | ||||
-rw-r--r-- | src/util/cardinality.h | 31 | ||||
-rw-r--r-- | src/util/divisible.cpp | 3 | ||||
-rw-r--r-- | src/util/divisible.h | 2 | ||||
-rw-r--r-- | src/util/floatingpoint.cpp | 26 | ||||
-rw-r--r-- | src/util/integer_cln_imp.cpp | 43 | ||||
-rw-r--r-- | src/util/integer_cln_imp.h | 34 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.cpp | 37 | ||||
-rw-r--r-- | src/util/integer_gmp_imp.h | 26 | ||||
-rw-r--r-- | src/util/proof.h | 2 | ||||
-rw-r--r-- | src/util/rational_cln_imp.cpp | 9 | ||||
-rw-r--r-- | src/util/rational_gmp_imp.cpp | 9 | ||||
-rw-r--r-- | src/util/subrange_bound.cpp | 63 | ||||
-rw-r--r-- | src/util/subrange_bound.h | 42 |
19 files changed, 329 insertions, 215 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 914d6e7d2..55f1a14da 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -45,6 +45,7 @@ libutil_la_SOURCES = \ regexp.h \ smt2_quote_string.cpp \ smt2_quote_string.h \ + subrange_bound.cpp \ subrange_bound.h \ tuple.h \ unsafe_interrupt_exception.h \ diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp index e401661eb..c9dc0251d 100644 --- a/src/util/abstract_value.cpp +++ b/src/util/abstract_value.cpp @@ -15,10 +15,13 @@ **/ #include "util/abstract_value.h" + #include <iostream> #include <sstream> #include <string> +#include "base/cvc4_assert.h" + using namespace std; namespace CVC4 { @@ -29,7 +32,7 @@ std::ostream& operator<<(std::ostream& out, const AbstractValue& val) { AbstractValue::AbstractValue(Integer index) throw(IllegalArgumentException) : d_index(index) { - CheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str()); + PrettyCheckArgument(index >= 1, index, "index >= 1 required for abstract value, not `%s'", index.toString().c_str()); } }/* CVC4 namespace */ diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h index d597edc8b..f02df2e66 100644 --- a/src/util/abstract_value.h +++ b/src/util/abstract_value.h @@ -18,7 +18,7 @@ #pragma once -#include <iostream> +#include <iosfwd> #include "util/integer.h" diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h index d057bcf84..ed6192cf7 100644 --- a/src/util/bin_heap.h +++ b/src/util/bin_heap.h @@ -26,6 +26,7 @@ #include <limits> #include <functional> +#include "base/cvc4_assert.h" #include "base/exception.h" namespace CVC4 { diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 762753795..041cae38e 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -20,7 +20,7 @@ #ifndef __CVC4__BITVECTOR_H #define __CVC4__BITVECTOR_H -#include <iostream> +#include <iosfwd> #include "base/exception.h" #include "util/integer.h" @@ -28,34 +28,13 @@ namespace CVC4 { class CVC4_PUBLIC BitVector { - -private: - - /* - Class invariants: - * no overflows: 2^d_size < d_value - * no negative numbers: d_value >= 0 - */ - unsigned d_size; - Integer d_value; - - Integer toSignedInt() const { - // returns Integer corresponding to two's complement interpretation of bv - unsigned size = d_size; - Integer sign_bit = d_value.extractBitRange(1,size-1); - Integer val = d_value.extractBitRange(size-1, 0); - Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val; - return res; - } - - public: BitVector(unsigned size, const Integer& val): d_size(size), d_value(val.modByPow2(size)) {} - + BitVector(unsigned size = 0) : d_size(size), d_value(0) {} @@ -63,7 +42,7 @@ public: : d_size(size), d_value(z) { d_value = d_value.modByPow2(size); } - + BitVector(unsigned size, unsigned long int z) : d_size(size), d_value(z) { d_value = d_value.modByPow2(size); @@ -71,7 +50,7 @@ public: BitVector(unsigned size, const BitVector& q) : d_size(size), d_value(q.d_value) {} - + BitVector(const std::string& num, unsigned base = 2); ~BitVector() {} @@ -79,7 +58,7 @@ public: Integer toInteger() const { return d_value; } - + BitVector& operator =(const BitVector& x) { if(this == &x) return *this; @@ -89,12 +68,12 @@ public: } bool operator ==(const BitVector& y) const { - if (d_size != y.d_size) return false; + if (d_size != y.d_size) return false; return d_value == y.d_value; } bool operator !=(const BitVector& y) const { - if (d_size != y.d_size) return true; + if (d_size != y.d_size) return true; return d_value != y.d_value; } @@ -113,24 +92,24 @@ public: // xor BitVector operator ^(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); - return BitVector(d_size, d_value.bitwiseXor(y.d_value)); + return BitVector(d_size, d_value.bitwiseXor(y.d_value)); } - + // or BitVector operator |(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); - return BitVector(d_size, d_value.bitwiseOr(y.d_value)); + return BitVector(d_size, d_value.bitwiseOr(y.d_value)); } - + // and BitVector operator &(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); - return BitVector(d_size, d_value.bitwiseAnd(y.d_value)); + return BitVector(d_size, d_value.bitwiseAnd(y.d_value)); } // not BitVector operator ~() const { - return BitVector(d_size, d_value.bitwiseNot()); + return BitVector(d_size, d_value.bitwiseNot()); } /* @@ -139,7 +118,7 @@ public: bool operator <(const BitVector& y) const { - return d_value < y.d_value; + return d_value < y.d_value; } bool operator >(const BitVector& y) const { @@ -147,14 +126,14 @@ public: } bool operator <=(const BitVector& y) const { - return d_value <= y.d_value; + return d_value <= y.d_value; } - + bool operator >=(const BitVector& y) const { return d_value >= y.d_value ; } - + BitVector operator +(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); Integer sum = d_value + y.d_value; @@ -165,12 +144,12 @@ public: 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)); + BitVector one(d_size, Integer(1)); return *this + ~y + one; } BitVector operator -() const { - BitVector one(d_size, Integer(1)); + BitVector one(d_size, Integer(1)); return ~(*this) + one; } @@ -183,16 +162,16 @@ public: BitVector setBit(uint32_t i) const { CheckArgument(i < d_size, i); Integer res = d_value.setBit(i); - return BitVector(d_size, res); + return BitVector(d_size, res); } bool isBitSet(uint32_t i) const { - CheckArgument(i < d_size, i); - return d_value.isBitSet(i); + CheckArgument(i < d_size, i); + return d_value.isBitSet(i); } - - /** - * Total division function that returns 0 when the denominator is 0. + + /** + * Total division function that returns 0 when the denominator is 0. */ BitVector unsignedDivTotal (const BitVector& y) const { @@ -203,11 +182,11 @@ public: } CheckArgument(d_value >= 0, this); CheckArgument(y.d_value > 0, y); - return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); + return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); } - - /** - * Total division function that returns 0 when the denominator is 0. + + /** + * Total division function that returns 0 when the denominator is 0. */ BitVector unsignedRemTotal(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); @@ -216,25 +195,25 @@ public: } CheckArgument(d_value >= 0, this); CheckArgument(y.d_value > 0, y); - return BitVector(d_size, d_value.floorDivideRemainder(y.d_value)); + return BitVector(d_size, d_value.floorDivideRemainder(y.d_value)); } - - + + bool signedLessThan(const BitVector& y) const { 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(); - - return a < b; + Integer b = y.toSignedInt(); + + return a < b; } bool unsignedLessThan(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); CheckArgument(d_value >= 0, this); CheckArgument(y.d_value >= 0, y); - return d_value < y.d_value; + return d_value < y.d_value; } bool signedLessThanEq(const BitVector& y) const { @@ -242,100 +221,98 @@ public: CheckArgument(d_value >= 0, this); CheckArgument(y.d_value >= 0, y); Integer a = (*this).toSignedInt(); - Integer b = y.toSignedInt(); - - return a <= b; + Integer b = y.toSignedInt(); + + return a <= b; } bool unsignedLessThanEq(const BitVector& y) const { CheckArgument(d_size == y.d_size, this); CheckArgument(d_value >= 0, this); CheckArgument(y.d_value >= 0, y); - return d_value <= y.d_value; + return d_value <= y.d_value; } - + /* Extend operations */ - BitVector zeroExtend(unsigned amount) const { - return BitVector(d_size + amount, d_value); + return BitVector(d_size + amount, d_value); } BitVector signExtend(unsigned amount) const { Integer sign_bit = d_value.extractBitRange(1, d_size -1); if(sign_bit == Integer(0)) { - return BitVector(d_size + amount, d_value); + return BitVector(d_size + amount, d_value); } else { Integer val = d_value.oneExtend(d_size, amount); return BitVector(d_size+ amount, val); } } - + /* Shifts on BitVectors */ - BitVector leftShift(const BitVector& y) const { if (y.d_value > Integer(d_size)) { - return BitVector(d_size, Integer(0)); + return BitVector(d_size, Integer(0)); } if (y.d_value == 0) { - return *this; + return *this; } // making sure we don't lose information casting CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); - uint32_t amount = y.d_value.toUnsignedInt(); + uint32_t amount = y.d_value.toUnsignedInt(); Integer res = d_value.multiplyByPow2(amount); return BitVector(d_size, res); } BitVector logicalRightShift(const BitVector& y) const { if(y.d_value > Integer(d_size)) { - return BitVector(d_size, Integer(0)); + return BitVector(d_size, Integer(0)); } // making sure we don't lose information casting CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); - uint32_t amount = y.d_value.toUnsignedInt(); - Integer res = d_value.divByPow2(amount); + uint32_t amount = y.d_value.toUnsignedInt(); + Integer res = d_value.divByPow2(amount); return BitVector(d_size, res); } BitVector arithRightShift(const BitVector& y) const { - Integer sign_bit = d_value.extractBitRange(1, d_size - 1); + Integer sign_bit = d_value.extractBitRange(1, d_size - 1); if(y.d_value > Integer(d_size)) { if(sign_bit == Integer(0)) { - return BitVector(d_size, Integer(0)); + return BitVector(d_size, Integer(0)); } else { - return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 ); + return BitVector(d_size, Integer(d_size).multiplyByPow2(d_size) -1 ); } } - + if (y.d_value == 0) { - return *this; + return *this; } // making sure we don't lose information casting CheckArgument(y.d_value < Integer(1).multiplyByPow2(32), y); - + uint32_t amount = y.d_value.toUnsignedInt(); Integer rest = d_value.divByPow2(amount); - + if(sign_bit == Integer(0)) { - return BitVector(d_size, rest); + return BitVector(d_size, rest); } Integer res = rest.oneExtend(d_size - amount, amount); return BitVector(d_size, res); } - + /* Convenience functions */ - + size_t hash() const { return d_value.hash() + d_size; } @@ -367,9 +344,26 @@ public: @return k if the integer is equal to 2^{k-1} and zero otherwise */ unsigned isPow2() { - return d_value.isPow2(); + return d_value.isPow2(); } +private: + /* + Class invariants: + * no overflows: 2^d_size < d_value + * no negative numbers: d_value >= 0 + */ + unsigned d_size; + Integer d_value; + + Integer toSignedInt() const { + // returns Integer corresponding to two's complement interpretation of bv + unsigned size = d_size; + Integer sign_bit = d_value.extractBitRange(1,size-1); + Integer val = d_value.extractBitRange(size-1, 0); + Integer res = Integer(-1) * sign_bit.multiplyByPow2(size - 1) + val; + return res; + } };/* class BitVector */ @@ -428,7 +422,7 @@ struct CVC4_PUBLIC BitVectorExtractHashFunction { /** - * The structure representing the extraction of one Boolean bit. + * The structure representing the extraction of one Boolean bit. */ struct CVC4_PUBLIC BitVectorBitOf { /** The index of the bit */ @@ -437,7 +431,7 @@ struct CVC4_PUBLIC BitVectorBitOf { : bitIndex(i) {} bool operator == (const BitVectorBitOf& other) const { - return bitIndex == other.bitIndex; + return bitIndex == other.bitIndex; } };/* struct BitVectorBitOf */ diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index dfee0aae2..07e094a38 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -16,6 +16,9 @@ #include "util/cardinality.h" +#include "base/cvc4_assert.h" + + namespace CVC4 { const Integer Cardinality::s_unknownCard(0); @@ -27,6 +30,45 @@ const Cardinality Cardinality::INTEGERS(CardinalityBeth(0)); const Cardinality Cardinality::REALS(CardinalityBeth(1)); const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown())); +CardinalityBeth::CardinalityBeth(const Integer& beth) + : d_index(beth) +{ + PrettyCheckArgument(beth >= 0, beth, + "Beth index must be a nonnegative integer, not %s.", + beth.toString().c_str()); +} + +Cardinality::Cardinality(long card) + : d_card(card) +{ + PrettyCheckArgument(card >= 0, card, + "Cardinality must be a nonnegative integer, not %ld.", + card); + d_card += 1; +} + +Cardinality::Cardinality(const Integer& card) + : d_card(card) +{ + PrettyCheckArgument(card >= 0, card, + "Cardinality must be a nonnegative integer, not %s.", + card.toString().c_str()); + d_card += 1; +} + + +Integer Cardinality::getFiniteCardinality() const throw(IllegalArgumentException) { + PrettyCheckArgument(isFinite(), *this, "This cardinality is not finite."); + PrettyCheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent."); + return d_card - 1; +} + +Integer Cardinality::getBethNumber() const throw(IllegalArgumentException) { + PrettyCheckArgument(!isFinite() && !isUnknown(), *this, + "This cardinality is not infinite (or is unknown)."); + return -d_card - 1; +} + Cardinality& Cardinality::operator+=(const Cardinality& c) throw() { if(isUnknown()) { return *this; diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 1cb4454e0..8b0d85980 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -36,11 +36,7 @@ class CVC4_PUBLIC CardinalityBeth { Integer d_index; public: - CardinalityBeth(const Integer& beth) : d_index(beth) { - CheckArgument(beth >= 0, beth, - "Beth index must be a nonnegative integer, not %s.", - beth.toString().c_str()); - } + CardinalityBeth(const Integer& beth); const Integer& getNumber() const throw() { return d_index; @@ -112,22 +108,13 @@ public: * "unsigned" argument to enforce the restriction, we mask some * errors that automatically convert, like "Cardinality(-1)". */ - Cardinality(long card) : d_card(card) { - CheckArgument(card >= 0, card, - "Cardinality must be a nonnegative integer, not %ld.", card); - d_card += 1; - } + Cardinality(long card); /** * Construct a finite cardinality equal to the integer argument. * The argument must be nonnegative. */ - Cardinality(const Integer& card) : d_card(card) { - CheckArgument(card >= 0, card, - "Cardinality must be a nonnegative integer, not %s.", - card.toString().c_str()); - d_card += 1; - } + Cardinality(const Integer& card); /** * Construct an infinite cardinality equal to the given Beth number. @@ -187,22 +174,14 @@ public: * cardinality. (If this cardinality is infinite, this function * throws an IllegalArgumentException.) */ - Integer getFiniteCardinality() const throw(IllegalArgumentException) { - CheckArgument(isFinite(), *this, "This cardinality is not finite."); - CheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent."); - return d_card - 1; - } + Integer getFiniteCardinality() const throw(IllegalArgumentException); /** * In the case that this cardinality is infinite, return its Beth * number. (If this cardinality is finite, this function throws an * IllegalArgumentException.) */ - Integer getBethNumber() const throw(IllegalArgumentException) { - CheckArgument(!isFinite() && !isUnknown(), *this, - "This cardinality is not infinite (or is unknown)."); - return -d_card - 1; - } + Integer getBethNumber() const throw(IllegalArgumentException); /** Assigning addition of this cardinality with another. */ Cardinality& operator+=(const Cardinality& c) throw(); diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp index 4a8b7a2e7..85824a77f 100644 --- a/src/util/divisible.cpp +++ b/src/util/divisible.cpp @@ -17,6 +17,7 @@ #include "util/divisible.h" +#include "base/cvc4_assert.h" #include "base/exception.h" using namespace std; @@ -24,7 +25,7 @@ using namespace std; namespace CVC4 { Divisible::Divisible(const Integer& n) : k(n) { - CheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N"); + PrettyCheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N"); } }/* CVC4 namespace */ diff --git a/src/util/divisible.h b/src/util/divisible.h index 5f62def02..56178e604 100644 --- a/src/util/divisible.h +++ b/src/util/divisible.h @@ -20,7 +20,7 @@ #ifndef __CVC4__DIVISIBLE_H #define __CVC4__DIVISIBLE_H -#include <iostream> +#include <iosfwd> #include "base/exception.h" #include "util/integer.h" diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index d3bb1967a..d1164133a 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -19,20 +19,20 @@ namespace CVC4 { - FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s) - { - CheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e); - CheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s); - } +FloatingPointSize::FloatingPointSize (unsigned _e, unsigned _s) : e(_e), s(_s) +{ + PrettyCheckArgument(validExponentSize(_e),_e,"Invalid exponent size : %d",_e); + PrettyCheckArgument(validSignificandSize(_s),_s,"Invalid significand size : %d",_s); +} - FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s) - { - CheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e); - CheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s); - } +FloatingPointSize::FloatingPointSize (const FloatingPointSize &old) : e(old.e), s(old.s) +{ + PrettyCheckArgument(validExponentSize(e),e,"Invalid exponent size : %d",e); + PrettyCheckArgument(validSignificandSize(s),s,"Invalid significand size : %d",s); +} - void FloatingPointLiteral::unfinished (void) const { - Unimplemented("Floating-point literals not yet implemented."); - } +void FloatingPointLiteral::unfinished (void) const { + Unimplemented("Floating-point literals not yet implemented."); +} }/* CVC4 namespace */ diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index 1cb4349eb..27a4b7d06 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -26,8 +26,34 @@ # error "This source should only ever be built if CVC4_CLN_IMP is on !" #endif /* CVC4_CLN_IMP */ +#include "base/cvc4_assert.h" + using namespace std; -using namespace CVC4; + +namespace CVC4 { + +signed int Integer::s_fastSignedIntMin = -(1<<29); +signed int Integer::s_fastSignedIntMax = (1<<29)-1; +signed long Integer::s_slowSignedIntMin = (signed long) std::numeric_limits<signed int>::min(); +signed long Integer::s_slowSignedIntMax = (signed long) std::numeric_limits<signed int>::max(); + +unsigned int Integer::s_fastUnsignedIntMax = (1<<29)-1; +unsigned long Integer::s_slowUnsignedIntMax = (unsigned long) std::numeric_limits<unsigned int>::max(); + +Integer Integer::oneExtend(uint32_t size, uint32_t amount) const { + DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); + cln::cl_byte range(amount, size); + cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1 + Integer temp(allones); + + return Integer(cln::deposit_field(allones, d_value, range)); +} + + +Integer Integer::exactQuotient(const Integer& y) const { + DebugCheckArgument(y.divides(*this), y); + return Integer( cln::exquo(d_value, y.d_value) ); +} void Integer::parseInt(const std::string& s, unsigned base) throw(std::invalid_argument) { @@ -78,14 +104,21 @@ void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, uns } bool Integer::fitsSignedInt() const { + // http://www.ginac.de/CLN/cln.html#Conversions // TODO improve performance - return d_value <= std::numeric_limits<signed int>::max() && - d_value >= std::numeric_limits<signed int>::min(); + Assert(s_slowSignedIntMin <= s_fastSignedIntMin); + Assert(s_fastSignedIntMin <= s_fastSignedIntMax); + Assert(s_fastSignedIntMax <= s_slowSignedIntMax); + + return (d_value <= s_fastSignedIntMax || d_value <= s_slowSignedIntMax) && + (d_value >= s_fastSignedIntMin || d_value >= s_slowSignedIntMax); } bool Integer::fitsUnsignedInt() const { // TODO improve performance - return sgn() >= 0 && d_value <= std::numeric_limits<unsigned int>::max(); + Assert(s_fastUnsignedIntMax <= s_slowUnsignedIntMax); + return sgn() >= 0 && + (d_value <= s_fastUnsignedIntMax || d_value <= s_slowUnsignedIntMax); } signed int Integer::getSignedInt() const { @@ -99,3 +132,5 @@ unsigned int Integer::getUnsignedInt() const { CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()"); return cln::cl_I_to_uint(d_value); } + +} /* namespace CVC4 */ diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 6df8d3b8e..9e5e6c2ae 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -20,14 +20,13 @@ #ifndef __CVC4__INTEGER_H #define __CVC4__INTEGER_H -#include <string> -#include <sstream> -#include <iostream> - -#include <cln/integer.h> #include <cln/input.h> +#include <cln/integer.h> #include <cln/integer_io.h> +#include <iostream> #include <limits> +#include <sstream> +#include <string> #include "base/exception.h" @@ -57,6 +56,17 @@ private: void parseInt(const std::string& s, unsigned base) throw(std::invalid_argument); + + // These constants are to help with CLN conversion in 32 bit. + // See http://www.ginac.de/CLN/cln.html#Conversions + static signed int s_fastSignedIntMax; /* 2^29 - 1 */ + static signed int s_fastSignedIntMin; /* -2^29 */ + static unsigned int s_fastUnsignedIntMax; /* 2^29 - 1 */ + + static signed long s_slowSignedIntMax; /* std::numeric_limits<signed int>::max() */ + static signed long s_slowSignedIntMin; /* std::numeric_limits<signed int>::min() */ + static unsigned long s_slowUnsignedIntMax; /* std::numeric_limits<unsigned int>::max() */ + public: /** Constructs a rational with the value 0. */ @@ -186,14 +196,7 @@ public: return Integer(cln::logior(d_value, mask)); } - Integer oneExtend(uint32_t size, uint32_t amount) const { - DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); - cln::cl_byte range(amount, size); - cln::cl_I allones = (cln::cl_I(1) << (size + amount))- 1; // 2^size - 1 - Integer temp(allones); - - return Integer(cln::deposit_field(allones, d_value, range)); - } + Integer oneExtend(uint32_t size, uint32_t amount) const; uint32_t toUnsignedInt() const { return cln::cl_I_to_uint(d_value); @@ -300,10 +303,7 @@ public: /** * If y divides *this, then exactQuotient returns (this/y) */ - Integer exactQuotient(const Integer& y) const { - DebugCheckArgument(y.divides(*this), y); - return Integer( cln::exquo(d_value, y.d_value) ); - } + Integer exactQuotient(const Integer& y) const; Integer modByPow2(uint32_t exp) const { cln::cl_byte range(exp, 0); diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index bde759219..df1bd297a 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -21,16 +21,18 @@ #include <string> #include "cvc4autoconfig.h" + +#include "base/cvc4_assert.h" #include "util/rational.h" #ifndef CVC4_GMP_IMP # error "This source should only ever be built if CVC4_GMP_IMP is on !" #endif /* CVC4_GMP_IMP */ -using namespace std; -using namespace CVC4; +using namespace std; +namespace CVC4 { Integer::Integer(const char* s, unsigned base) : d_value(s, base) @@ -52,10 +54,11 @@ bool Integer::fitsUnsignedInt() const { signed int Integer::getSignedInt() const { // ensure there isn't overflow CheckArgument(d_value <= std::numeric_limits<int>::max(), this, - "Overflow detected in Integer::getSignedInt()"); + "Overflow detected in Integer::getSignedInt()."); CheckArgument(d_value >= std::numeric_limits<int>::min(), this, - "Overflow detected in Integer::getSignedInt()"); - CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()"); + "Overflow detected in Integer::getSignedInt()."); + CheckArgument(fitsSignedInt(), this, + "Overflow detected in Integer::getSignedInt()."); return (signed int) d_value.get_si(); } @@ -65,6 +68,28 @@ unsigned int Integer::getUnsignedInt() const { "Overflow detected in Integer::getUnsignedInt()"); CheckArgument(d_value >= std::numeric_limits<unsigned int>::min(), this, "Overflow detected in Integer::getUnsignedInt()"); - CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()"); + CheckArgument(fitsSignedInt(), this, + "Overflow detected in Integer::getUnsignedInt()"); return (unsigned int) d_value.get_ui(); } + +Integer Integer::oneExtend(uint32_t size, uint32_t amount) const { + // check that the size is accurate + DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); + mpz_class res = d_value; + + for (unsigned i = size; i < size + amount; ++i) { + mpz_setbit(res.get_mpz_t(), i); + } + + return Integer(res); +} + +Integer Integer::exactQuotient(const Integer& y) const { + DebugCheckArgument(y.divides(*this), y); + mpz_class q; + mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); + return Integer( q ); +} + +} /* namespace CVC4 */ diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 0d3122cd8..9cae16222 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -21,7 +21,7 @@ #define __CVC4__INTEGER_H #include <string> -#include <iostream> +#include <iosfwd> #include <limits> #include "base/exception.h" @@ -190,17 +190,7 @@ public: * Returns the integer with the binary representation of size bits * extended with amount 1's */ - Integer oneExtend(uint32_t size, uint32_t amount) const { - // check that the size is accurate - DebugCheckArgument((*this) < Integer(1).multiplyByPow2(size), size); - mpz_class res = d_value; - - for (unsigned i = size; i < size + amount; ++i) { - mpz_setbit(res.get_mpz_t(), i); - } - - return Integer(res); - } + Integer oneExtend(uint32_t size, uint32_t amount) const; uint32_t toUnsignedInt() const { return mpz_get_ui(d_value.get_mpz_t()); @@ -319,12 +309,7 @@ public: /** * If y divides *this, then exactQuotient returns (this/y) */ - Integer exactQuotient(const Integer& y) const { - DebugCheckArgument(y.divides(*this), y); - mpz_class q; - mpz_divexact(q.get_mpz_t(), d_value.get_mpz_t(), y.d_value.get_mpz_t()); - return Integer( q ); - } + Integer exactQuotient(const Integer& y) const; /** * Returns y mod 2^exp @@ -430,14 +415,15 @@ public: long si = d_value.get_si(); // ensure there wasn't overflow CheckArgument(mpz_cmp_si(d_value.get_mpz_t(), si) == 0, this, - "Overflow detected in Integer::getLong()"); + "Overflow detected in Integer::getLong()."); return si; } + unsigned long getUnsignedLong() const { unsigned long ui = d_value.get_ui(); // ensure there wasn't overflow CheckArgument(mpz_cmp_ui(d_value.get_mpz_t(), ui) == 0, this, - "Overflow detected in Integer::getUnsignedLong()"); + "Overflow detected in Integer::getUnsignedLong()."); return ui; } diff --git a/src/util/proof.h b/src/util/proof.h index be1e2a8e2..22d9f97d5 100644 --- a/src/util/proof.h +++ b/src/util/proof.h @@ -20,7 +20,7 @@ #ifndef __CVC4__PROOF_H #define __CVC4__PROOF_H -#include <iostream> +#include <iosfwd> namespace CVC4 { diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index 5044aff18..608b33f2b 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -24,8 +24,11 @@ # error "This source should only ever be built if CVC4_CLN_IMP is on !" #endif /* CVC4_CLN_IMP */ +#include "base/cvc4_assert.h" + using namespace std; -using namespace CVC4; + +namespace CVC4 { /* Computes a rational given a decimal string. The rational * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>. @@ -48,7 +51,7 @@ Rational Rational::fromDecimal(const std::string& dec) { } } -std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){ +std::ostream& operator<<(std::ostream& os, const Rational& q){ return os << q.toString(); } @@ -105,3 +108,5 @@ RationalFromDoubleException::RationalFromDoubleException(double d) throw() ss << ")"; setMessage(ss.str()); } + +} /* namespace CVC4 */ diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index f0f7d46eb..63fb8e05c 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -21,15 +21,18 @@ #include "cvc4autoconfig.h" -#ifndef CVC4_GMP_IMP +#ifndef CVC4_GMP_IMP // Make sure this comes after cvc4autoconfig.h # error "This source should only ever be built if CVC4_GMP_IMP is on !" #endif /* CVC4_GMP_IMP */ -std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){ +#include "base/cvc4_assert.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& os, const Rational& q){ return os << q.toString(); } -namespace CVC4 { /* Computes a rational given a decimal string. The rational * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>. diff --git a/src/util/subrange_bound.cpp b/src/util/subrange_bound.cpp new file mode 100644 index 000000000..5d66b75ad --- /dev/null +++ b/src/util/subrange_bound.cpp @@ -0,0 +1,63 @@ +/********************* */ +/*! \file subrange_bound.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2015 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Representation of subrange bounds + ** + ** Simple class to represent a subrange bound, either infinite + ** (no bound) or finite (an arbitrary precision integer). + **/ + +#include "util/subrange_bound.h" + +#include <limits> + +#include "base/cvc4_assert.h" +#include "base/exception.h" +#include "util/integer.h" + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) +throw() { + out << bounds.lower << ".." << bounds.upper; + + return out; +} + +/** Get the finite SubrangeBound, failing an assertion if infinite. */ +const Integer& SubrangeBound::getBound() const throw(IllegalArgumentException) { + PrettyCheckArgument(!d_nobound, this, "SubrangeBound is infinite"); + return d_bound; +} + +SubrangeBounds::SubrangeBounds(const SubrangeBound& l, + const SubrangeBound& u) + : lower(l) + , upper(u) +{ + PrettyCheckArgument(!l.hasBound() || !u.hasBound() || + l.getBound() <= u.getBound(), + l, "Bad subrange bounds specified"); +} + +bool SubrangeBounds::joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){ + return (a.lower.hasBound() && b.lower.hasBound()) || + (a.upper.hasBound() && b.upper.hasBound()); +} + +SubrangeBounds SubrangeBounds::join(const SubrangeBounds& a, const SubrangeBounds& b){ + DebugCheckArgument(joinIsBounded(a,b), a); + SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower); + SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper); + return SubrangeBounds(newLower, newUpper); +} + +} /* namespace CVC4 */ diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h index 6cff7133c..d5b50bf4c 100644 --- a/src/util/subrange_bound.h +++ b/src/util/subrange_bound.h @@ -34,9 +34,6 @@ namespace CVC4 { * has a lower bound of -5 and an infinite upper bound. */ class CVC4_PUBLIC SubrangeBound { - bool d_nobound; - Integer d_bound; - public: /** Construct an infinite SubrangeBound. */ @@ -55,10 +52,7 @@ public: } /** Get the finite SubrangeBound, failing an assertion if infinite. */ - const Integer& getBound() const throw(IllegalArgumentException) { - CheckArgument(!d_nobound, this, "SubrangeBound is infinite"); - return d_bound; - } + const Integer& getBound() const throw(IllegalArgumentException); /** Returns true iff this is a finite SubrangeBound. */ bool hasBound() const throw() { @@ -145,6 +139,9 @@ public: } } +private: + bool d_nobound; + Integer d_bound; };/* class SubrangeBound */ class CVC4_PUBLIC SubrangeBounds { @@ -153,13 +150,7 @@ public: SubrangeBound lower; SubrangeBound upper; - SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u) : - lower(l), - upper(u) { - CheckArgument(!l.hasBound() || !u.hasBound() || - l.getBound() <= u.getBound(), - l, "Bad subrange bounds specified"); - } + SubrangeBounds(const SubrangeBound& l, const SubrangeBound& u); bool operator==(const SubrangeBounds& bounds) const { return lower == bounds.lower && upper == bounds.upper; @@ -210,21 +201,13 @@ public: /** * Returns true if the join of two subranges is not (- infinity, + infinity). */ - static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b){ - return (a.lower.hasBound() && b.lower.hasBound()) || - (a.upper.hasBound() && b.upper.hasBound()); - } + static bool joinIsBounded(const SubrangeBounds& a, const SubrangeBounds& b); /** * Returns the join of two subranges, a and b. * precondition: joinIsBounded(a,b) is true */ - static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b){ - DebugCheckArgument(joinIsBounded(a,b), a); - SubrangeBound newLower = SubrangeBound::min(a.lower, b.lower); - SubrangeBound newUpper = SubrangeBound::max(a.upper, b.upper); - return SubrangeBounds(newLower, newUpper); - } + static SubrangeBounds join(const SubrangeBounds& a, const SubrangeBounds& b); };/* class SubrangeBounds */ @@ -252,15 +235,8 @@ operator<<(std::ostream& out, const SubrangeBound& bound) throw() { return out; } -inline std::ostream& -operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() CVC4_PUBLIC; - -inline std::ostream& -operator<<(std::ostream& out, const SubrangeBounds& bounds) throw() { - out << bounds.lower << ".." << bounds.upper; - - return out; -} +std::ostream& operator<<(std::ostream& out, const SubrangeBounds& bounds) +throw() CVC4_PUBLIC; }/* CVC4 namespace */ |