summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/Makefile.am1
-rw-r--r--src/util/abstract_value.cpp5
-rw-r--r--src/util/abstract_value.h2
-rw-r--r--src/util/bin_heap.h1
-rw-r--r--src/util/bitvector.h166
-rw-r--r--src/util/cardinality.cpp42
-rw-r--r--src/util/cardinality.h31
-rw-r--r--src/util/divisible.cpp3
-rw-r--r--src/util/divisible.h2
-rw-r--r--src/util/floatingpoint.cpp26
-rw-r--r--src/util/integer_cln_imp.cpp43
-rw-r--r--src/util/integer_cln_imp.h34
-rw-r--r--src/util/integer_gmp_imp.cpp37
-rw-r--r--src/util/integer_gmp_imp.h26
-rw-r--r--src/util/proof.h2
-rw-r--r--src/util/rational_cln_imp.cpp9
-rw-r--r--src/util/rational_gmp_imp.cpp9
-rw-r--r--src/util/subrange_bound.cpp63
-rw-r--r--src/util/subrange_bound.h42
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback