# Checks for libraries.
AC_CHECK_LIB(gmp, __gmpz_init, , [AC_MSG_ERROR([GNU MP not found, see http://gmplib.org/])])
+AC_CHECK_LIB(gmpxx, __gmpz_init, , AC_MSG_ERROR(libgmpxx.a is not found))
+
# Check for antlr C++ runtime (defined in config/antlr.m4)
AC_LIB_ANTLR
output.h \
result.h \
unique_id.h \
- configuration.h
+ configuration.ha \
+ rational.h \
+ rational.cpp \
+ integer.h \
+ integer.cpp
--- /dev/null
+#include "util/integer.h"
+
+using namespace CVC4;
+
+std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n){
+ return os << n.toString();
+}
--- /dev/null
+/********************* */
+/** integer.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** A multiprecision integer constant.
+ **/
+#include <gmpxx.h>
+#include <string>
+
+
+#ifndef __CVC4__INTEGER_H
+#define __CVC4__INTEGER_H
+
+namespace CVC4 {
+
+/** Hashes the gmp integer primitive in a word by word fashion. */
+inline size_t gmpz_hash(const mpz_t toHash){
+ size_t hash = 0;
+ for (int i=0, n=mpz_size(toHash); i<n; ++i){
+ mp_limb_t limb = mpz_getlimbn(toHash, i);
+ hash = hash * 2;
+ hash = hash xor limb;
+ }
+ return hash;
+}
+
+class Rational;
+
+class Integer {
+private:
+ /**
+ * Stores the value of the rational is stored in a C++ GMP integer class.
+ * Using this instead of mpz_t allows for easier destruction.
+ */
+ mpz_class d_value;
+
+ /**
+ * Gets a reference to the gmp data that backs up the integer.
+ * Only accessible to friend classes.
+ */
+ const mpz_class& get_mpz() const { return d_value; }
+
+ /**
+ * Constructs an Integer by copying a GMP C++ primitive.
+ */
+ Integer(const mpz_class& val) : d_value(val) {}
+
+public:
+
+ /** Constructs a rational with the value 0. */
+ Integer() : d_value(0){}
+
+ /**
+ * Constructs a Integer from a C string.
+ * Throws std::invalid_argument if the stribng is not a valid rational.
+ * For more information about what is a vaid rational string,
+ * see GMP's documentation for mpq_set_str().
+ */
+ Integer(const char * s, int base = 10): d_value(s,base) {}
+ Integer(const std::string& s, unsigned base = 10) : d_value(s, base) {}
+
+ Integer(const Integer& q) : d_value(q.d_value) {}
+
+ Integer( signed int z) : d_value(z) {}
+ Integer(unsigned int z) : d_value(z) {}
+ Integer( signed long int z) : d_value(z) {}
+ Integer(unsigned long int z) : d_value(z) {}
+
+ ~Integer() {}
+
+
+ Integer& operator=(const Integer& x){
+ if(this == &x) return *this;
+ d_value = x.d_value;
+ return *this;
+ }
+
+ bool operator==(const Integer& y) const {
+ return d_value == y.d_value;
+ }
+
+ Integer operator-() const{
+ return Integer(-(d_value));
+ }
+
+
+ bool operator!=(const Integer& y) const {
+ return d_value != y.d_value;
+ }
+
+ bool operator< (const Integer& y) const {
+ return d_value < y.d_value;
+ }
+
+ bool operator<=(const Integer& y) const {
+ return d_value <= y.d_value;
+ }
+
+ bool operator> (const Integer& y) const {
+ return d_value > y.d_value;
+ }
+
+ bool operator>=(const Integer& y) const {
+ return d_value >= y.d_value;
+ }
+
+
+ Integer operator+(const Integer& y) const{
+ return Integer( d_value + y.d_value );
+ }
+
+ Integer operator-(const Integer& y) const {
+ return Integer( d_value - y.d_value );
+ }
+
+ Integer operator*(const Integer& y) const {
+ return Integer( d_value * y.d_value );
+ }
+ Integer operator/(const Integer& y) const {
+ return Integer( d_value / y.d_value );
+ }
+
+ std::string toString(int base = 10) const{
+ return d_value.get_str(base);
+ }
+
+ //friend std::ostream& operator<<(std::ostream& os, const Integer& n);
+
+ long getLong() const { return d_value.get_si(); }
+ unsigned long getUnsignedLong() const {return d_value.get_ui(); }
+
+ /**
+ * Computes the hash of the node from the first word of the
+ * numerator, the denominator.
+ */
+ size_t hash() const {
+ return gmpz_hash(d_value.get_mpz_t());
+ }
+
+ friend class CVC4::Rational;
+};/* class Integer */
+
+std::ostream& operator<<(std::ostream& os, const Integer& n);
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RATIONAL_H */
+
--- /dev/null
+
+#include "util/rational.h"
+
+using namespace CVC4;
+
+std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){
+ return os << q.toString();
+}
--- /dev/null
+/********************* */
+/** rational.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** A multiprecision rational constant.
+ **/
+
+#include <gmpxx.h>
+#include <string>
+#include "integer.h"
+
+#ifndef __CVC4__RATIONAL_H
+#define __CVC4__RATIONAL_H
+
+namespace CVC4 {
+
+class Rational {
+private:
+ /**
+ * Stores the value of the rational is stored in a C++ GMP rational class.
+ * Using this instead of mpq_t allows for easier destruction.
+ */
+ mpq_class d_value;
+
+ /**
+ * Constructs a Rational from a mpq_class object.
+ * Does a deep copy.
+ * Assumes that the value is in canonical form, and thus does not
+ * have to call canonicalize() on the value.
+ */
+ Rational(const mpq_class& val) : d_value(val) { }
+
+public:
+
+ /** Constructs a rational with the value 0/1. */
+ Rational() : d_value(0){
+ d_value.canonicalize();
+ }
+
+ /**
+ * Constructs a Rational from a C string.
+ * Throws std::invalid_argument if the stribng is not a valid rational.
+ * For more information about what is a vaid rational string,
+ * see GMP's documentation for mpq_set_str().
+ */
+ Rational(const char * s, int base = 10): d_value(s,base) {
+ d_value.canonicalize();
+ }
+ Rational(const std::string& s, unsigned base = 10) : d_value(s, base) {
+ d_value.canonicalize();
+ }
+
+ Rational(const Rational& q) : d_value(q.d_value) {
+ d_value.canonicalize();
+ }
+
+ Rational( signed int n, signed int d) : d_value(n,d) {
+ d_value.canonicalize();
+ }
+ Rational(unsigned int n, unsigned int d) : d_value(n,d) {
+ d_value.canonicalize();
+ }
+ Rational( signed long int n, signed long int d) : d_value(n,d) {
+ d_value.canonicalize();
+ }
+ Rational(unsigned long int n, unsigned long int d) : d_value(n,d) {
+ d_value.canonicalize();
+ }
+
+ Rational(const Integer& n, const Integer& d):
+ d_value(n.get_mpz(), d.get_mpz())
+ {
+ d_value.canonicalize();
+ }
+
+ ~Rational() {}
+
+
+ Integer getNumerator() const {
+ return Integer(d_value.get_num());
+ }
+
+ Integer getDenominator() const{
+ return Integer(d_value.get_den());
+ }
+
+
+ Rational& operator=(const Rational& x){
+ if(this == &x) return *this;
+ d_value = x.d_value;
+ return *this;
+ }
+
+ Rational operator-() const{
+ return Rational(-(d_value));
+ }
+
+ bool operator==(const Rational& y) const {
+ return d_value == y.d_value;
+ }
+
+ bool operator!=(const Rational& y) const {
+ return d_value != y.d_value;
+ }
+
+ bool operator< (const Rational& y) const {
+ return d_value < y.d_value;
+ }
+
+ bool operator<=(const Rational& y) const {
+ return d_value <= y.d_value;
+ }
+
+ bool operator> (const Rational& y) const {
+ return d_value > y.d_value;
+ }
+
+ bool operator>=(const Rational& y) const {
+ return d_value >= y.d_value;
+ }
+
+
+ Rational operator+(const Rational& y) const{
+ return Rational( d_value + y.d_value );
+ }
+
+ Rational operator-(const Rational& y) const {
+ return Rational( d_value - y.d_value );
+ }
+
+ Rational operator*(const Rational& y) const {
+ return Rational( d_value * y.d_value );
+ }
+ Rational operator/(const Rational& y) const {
+ return Rational( d_value / y.d_value );
+ }
+
+ std::string toString(int base = 10) const {
+ return d_value.get_str(base);
+ }
+
+
+ friend std::ostream& operator<<(std::ostream& os, const Rational& n);
+
+
+ /**
+ * Computes the hash of the node from the first word of the
+ * numerator, the denominator.
+ */
+ size_t hash() const {
+ size_t numeratorHash = gmpz_hash(d_value.get_num_mpz_t());
+ size_t denominatorHash = gmpz_hash(d_value.get_den_mpz_t());
+
+ return numeratorHash xor denominatorHash;
+ }
+
+};/* class Rational */
+
+std::ostream& operator<<(std::ostream& os, const Rational& n);
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__RATIONAL_H */
+
theory/theory_uf_white \
util/assert_white \
util/configuration_white \
- util/output_white
+ util/output_white \
+ util/integer_black \
+ util/integer_white \
+ util/rational_white
# Things that aren't tests but that tests rely on and need to
# go into the distribution
--- /dev/null
+/********************* */
+/** integer_black.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Black box testing of CVC4::Integer.
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <sstream>
+
+#include "util/integer.h"
+
+using namespace CVC4;
+using namespace std;
+
+const char* largeVal = "4547897890548754897897897897890789078907890";
+
+class IntegerBlack : public CxxTest::TestSuite {
+
+
+public:
+
+ void testConstructors() {
+ Integer z0(1);
+ TS_ASSERT_EQUALS(z0.getLong(), 1);
+
+ Integer z1(0);
+ TS_ASSERT_EQUALS(z1.getLong(), 0);
+
+ Integer z2(-1);
+ TS_ASSERT_EQUALS(z2.getLong(), -1);
+
+ Integer z3(0x890UL);
+ TS_ASSERT_EQUALS(z3.getUnsignedLong(), 0x890UL);
+
+ Integer z4;
+ TS_ASSERT_EQUALS(z4.getLong(), 0);
+
+ Integer z5("7896890");
+ TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890);
+
+ Integer z6(z5);
+ TS_ASSERT_EQUALS(z5.getUnsignedLong(), 7896890);
+ TS_ASSERT_EQUALS(z6.getUnsignedLong(), 7896890);
+
+
+ string bigValue("1536729");
+ Integer z7(bigValue);
+ TS_ASSERT_EQUALS(z7.getUnsignedLong(), 1536729);
+ }
+
+ void testOperatorAssign(){
+ Integer x(0);
+ Integer y(79);
+ Integer z(45789);
+
+ TS_ASSERT_EQUALS(x.getUnsignedLong(), 0);
+ TS_ASSERT_EQUALS(y.getUnsignedLong(), 79);
+ TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789);
+
+ x = y = z;
+
+ TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789);
+ TS_ASSERT_EQUALS(y.getUnsignedLong(), 45789);
+ TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789);
+
+ Integer a(2);
+
+ y = a;
+
+ TS_ASSERT_EQUALS(a.getUnsignedLong(), 2);
+ TS_ASSERT_EQUALS(y.getUnsignedLong(), 2);
+ TS_ASSERT_EQUALS(x.getUnsignedLong(), 45789);
+ TS_ASSERT_EQUALS(z.getUnsignedLong(), 45789);
+ }
+
+ void testOperatorEquals(){
+ Integer a(0);
+ Integer b(79);
+ Integer c("79");
+ Integer d;
+
+ TS_ASSERT( (a==a));
+ TS_ASSERT(!(a==b));
+ TS_ASSERT(!(a==c));
+ TS_ASSERT( (a==d));
+
+ TS_ASSERT(!(b==a));
+ TS_ASSERT( (b==b));
+ TS_ASSERT( (b==c));
+ TS_ASSERT(!(b==d));
+
+ TS_ASSERT(!(c==a));
+ TS_ASSERT( (c==b));
+ TS_ASSERT( (c==c));
+ TS_ASSERT(!(c==d));
+
+ TS_ASSERT( (d==a));
+ TS_ASSERT(!(d==b));
+ TS_ASSERT(!(d==c));
+ TS_ASSERT( (d==d));
+
+ }
+
+ void testOperatorNotEquals(){
+ Integer a(0);
+ Integer b(79);
+ Integer c("79");
+ Integer d;
+
+ TS_ASSERT(!(a!=a));
+ TS_ASSERT( (a!=b));
+ TS_ASSERT( (a!=c));
+ TS_ASSERT(!(a!=d));
+
+ TS_ASSERT( (b!=a));
+ TS_ASSERT(!(b!=b));
+ TS_ASSERT(!(b!=c));
+ TS_ASSERT( (b!=d));
+
+ TS_ASSERT( (c!=a));
+ TS_ASSERT(!(c!=b));
+ TS_ASSERT(!(c!=c));
+ TS_ASSERT( (c!=d));
+
+ TS_ASSERT(!(d!=a));
+ TS_ASSERT( (d!=b));
+ TS_ASSERT( (d!=c));
+ TS_ASSERT(!(d!=d));
+
+ }
+
+ void testOperatorSubtract(){
+ Integer x(0);
+ Integer y(79);
+ Integer z(-34);
+
+
+ Integer act0 = x - x;
+ Integer act1 = x - y;
+ Integer act2 = x - z;
+ Integer exp0(0);
+ Integer exp1(-79);
+ Integer exp2(34);
+
+
+ Integer act3 = y - x;
+ Integer act4 = y - y;
+ Integer act5 = y - z;
+ Integer exp3(79);
+ Integer exp4(0);
+ Integer exp5(113);
+
+
+ Integer act6 = z - x;
+ Integer act7 = z - y;
+ Integer act8 = z - z;
+ Integer exp6(-34);
+ Integer exp7(-113);
+ Integer exp8(0);
+
+
+
+ TS_ASSERT_EQUALS(act0, exp0);
+ TS_ASSERT_EQUALS(act1, exp1);
+ TS_ASSERT_EQUALS(act2, exp2);
+ TS_ASSERT_EQUALS(act3, exp3);
+ TS_ASSERT_EQUALS(act4, exp4);
+ TS_ASSERT_EQUALS(act5, exp5);
+ TS_ASSERT_EQUALS(act6, exp6);
+ TS_ASSERT_EQUALS(act7, exp7);
+ TS_ASSERT_EQUALS(act8, exp8);
+ }
+ void testOperatorAdd(){
+ Integer x(0);
+ Integer y(79);
+ Integer z(-34);
+
+
+ Integer act0 = x + x;
+ Integer act1 = x + y;
+ Integer act2 = x + z;
+ Integer exp0(0);
+ Integer exp1(79);
+ Integer exp2(-34);
+
+
+ Integer act3 = y + x;
+ Integer act4 = y + y;
+ Integer act5 = y + z;
+ Integer exp3(79);
+ Integer exp4(158);
+ Integer exp5(45);
+
+
+ Integer act6 = z + x;
+ Integer act7 = z + y;
+ Integer act8 = z + z;
+ Integer exp6(-34);
+ Integer exp7(45);
+ Integer exp8(-68);
+
+
+
+ TS_ASSERT_EQUALS(act0, exp0);
+ TS_ASSERT_EQUALS(act1, exp1);
+ TS_ASSERT_EQUALS(act2, exp2);
+ TS_ASSERT_EQUALS(act3, exp3);
+ TS_ASSERT_EQUALS(act4, exp4);
+ TS_ASSERT_EQUALS(act5, exp5);
+ TS_ASSERT_EQUALS(act6, exp6);
+ TS_ASSERT_EQUALS(act7, exp7);
+ TS_ASSERT_EQUALS(act8, exp8);
+ }
+
+ void testOperatorMult(){
+ Integer x(0);
+ Integer y(79);
+ Integer z(-34);
+
+
+ Integer act0 = x * x;
+ Integer act1 = x * y;
+ Integer act2 = x * z;
+ Integer exp0(0);
+ Integer exp1(0);
+ Integer exp2(0);
+
+
+ Integer act3 = y * x;
+ Integer act4 = y * y;
+ Integer act5 = y * z;
+ Integer exp3(0);
+ Integer exp4(6241);
+ Integer exp5(-2686);
+
+
+ Integer act6 = z * x;
+ Integer act7 = z * y;
+ Integer act8 = z * z;
+ Integer exp6(0);
+ Integer exp7(-2686);
+ Integer exp8(1156);
+
+
+
+ TS_ASSERT_EQUALS(act0, exp0);
+ TS_ASSERT_EQUALS(act1, exp1);
+ TS_ASSERT_EQUALS(act2, exp2);
+ TS_ASSERT_EQUALS(act3, exp3);
+ TS_ASSERT_EQUALS(act4, exp4);
+ TS_ASSERT_EQUALS(act5, exp5);
+ TS_ASSERT_EQUALS(act6, exp6);
+ TS_ASSERT_EQUALS(act7, exp7);
+ TS_ASSERT_EQUALS(act8, exp8);
+ }
+
+
+ void testToStringStuff(){
+ stringstream ss;
+ Integer large (largeVal);
+ ss << large;
+ string res = ss.str();
+
+ TS_ASSERT_EQUALS(res, large.toString());
+ }
+
+};
--- /dev/null
+/********************* */
+/** integer_white.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** White box testing of CVC4::Integer.
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <sstream>
+
+#include "util/integer.h"
+
+using namespace CVC4;
+using namespace std;
+
+const char* largeVal = "4547897890548754897897897897890789078907890";
+
+class IntegerWhite : public CxxTest::TestSuite {
+public:
+
+ void testHash(){
+ Integer large (largeVal);
+ Integer zero;
+ Integer one_word(75890);
+ Integer two_words("7890D789D33234027890D789D3323402", 16);
+
+ TS_ASSERT_EQUALS(zero.hash(), 0);
+ TS_ASSERT_EQUALS(one_word.hash(), 75890);
+ TS_ASSERT_EQUALS(two_words.hash(), 9921844058862803974UL);
+ TS_ASSERT_EQUALS(large.hash(), 772190219532412699UL);
+ }
+};
--- /dev/null
+/********************* */
+/** rational_white.h
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** White box testing of CVC4::Rational.
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <sstream>
+
+#include "util/rational.h"
+
+using namespace CVC4;
+using namespace std;
+
+const char* canReduce = "4547897890548754897897897897890789078907890/54878902347890234";
+
+class RationalWhite : public CxxTest::TestSuite {
+public:
+
+ void testReductionAtConstructionTime(){
+ Rational reduce0(canReduce);
+ Integer num0("2273948945274377448948948948945394539453945");
+ Integer den0("27439451173945117");
+
+ TS_ASSERT_EQUALS(reduce0.getNumerator(), num0);
+ TS_ASSERT_EQUALS(reduce0.getDenominator(), den0);
+
+ Rational reduce1(0, 454789);
+ Integer num1(0);
+ Integer den1(1);
+
+ TS_ASSERT_EQUALS(reduce1.getNumerator(), num1);
+ TS_ASSERT_EQUALS(reduce1.getDenominator(), den1);
+
+ Rational reduce2(0, -454789);
+ Integer num2(0);
+ Integer den2(1);
+
+
+ TS_ASSERT_EQUALS(reduce2.getNumerator(), num2);
+ TS_ASSERT_EQUALS(reduce2.getDenominator(), den2);
+
+
+ Rational reduce3( 454789890342L, 273L);
+ Integer num3(151596630114L);
+ Integer den3(91);
+
+ TS_ASSERT_EQUALS(reduce2.getNumerator(), num2);
+ TS_ASSERT_EQUALS(reduce2.getDenominator(), den2);
+
+ Rational reduce4( 454789890342L,-273L);
+ Integer num4(-151596630114L);
+ Integer den4(91);
+
+
+ TS_ASSERT_EQUALS(reduce4.getNumerator(), num4);
+ TS_ASSERT_EQUALS(reduce4.getDenominator(), den4);
+
+ Rational reduce5(-454789890342L, 273L);
+ Integer num5(-151596630114L);
+ Integer den5(91);
+
+
+ TS_ASSERT_EQUALS(reduce5.getNumerator(), num5);
+ TS_ASSERT_EQUALS(reduce5.getDenominator(), den5);
+
+ Rational reduce6(-454789890342L,-273L);
+ Integer num6(151596630114L);
+ Integer den6(91);
+
+
+ TS_ASSERT_EQUALS(reduce6.getNumerator(), num6);
+ TS_ASSERT_EQUALS(reduce6.getDenominator(), den6);
+
+ }
+
+ void testHash(){
+ Rational large (canReduce);
+ Rational zero;
+ Rational one_word(75890L,590L);
+ Rational two_words("7890D789D33234027890D789D3323402", 16);
+
+ TS_ASSERT_EQUALS(zero.hash(), 1);
+ TS_ASSERT_EQUALS(one_word.hash(), 7589 xor 59);
+ TS_ASSERT_EQUALS(two_words.hash(), 9921844058862803974UL ^ 1);
+ TS_ASSERT_EQUALS(large.hash(),
+ (large.getNumerator().hash())^(large.getDenominator().hash()));
+ }
+};
projects / cvc5.git / commitdiff