From: Tim King Date: Fri, 26 Mar 2010 22:37:12 +0000 (+0000) Subject: Added GMP backed Rational and Integer classes, and white box tests for them. You... X-Git-Tag: cvc5-1.0.0~9169 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b8d92b17c17aadfa920f36a1ab631e36c70e00e;p=cvc5.git Added GMP backed Rational and Integer classes, and white box tests for them. You may have to reconfigure after this update. --- diff --git a/configure.ac b/configure.ac index f540cab11..b3af2153b 100644 --- a/configure.ac +++ b/configure.ac @@ -418,6 +418,8 @@ fi # 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 diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 76414ebe1..f6f8323be 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -20,4 +20,8 @@ libutil_la_SOURCES = \ output.h \ result.h \ unique_id.h \ - configuration.h + configuration.ha \ + rational.h \ + rational.cpp \ + integer.h \ + integer.cpp diff --git a/src/util/integer.cpp b/src/util/integer.cpp new file mode 100644 index 000000000..8fc788eb8 --- /dev/null +++ b/src/util/integer.cpp @@ -0,0 +1,7 @@ +#include "util/integer.h" + +using namespace CVC4; + +std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n){ + return os << n.toString(); +} diff --git a/src/util/integer.h b/src/util/integer.h new file mode 100644 index 000000000..1ac8eab78 --- /dev/null +++ b/src/util/integer.h @@ -0,0 +1,157 @@ +/********************* */ +/** 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 +#include + + +#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 (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 */ + diff --git a/src/util/rational.cpp b/src/util/rational.cpp new file mode 100644 index 000000000..2f33ed859 --- /dev/null +++ b/src/util/rational.cpp @@ -0,0 +1,8 @@ + +#include "util/rational.h" + +using namespace CVC4; + +std::ostream& CVC4::operator<<(std::ostream& os, const Rational& q){ + return os << q.toString(); +} diff --git a/src/util/rational.h b/src/util/rational.h new file mode 100644 index 000000000..e3f760031 --- /dev/null +++ b/src/util/rational.h @@ -0,0 +1,172 @@ +/********************* */ +/** 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 +#include +#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 */ + diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index f78171dac..1d5bcc230 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -14,7 +14,10 @@ UNIT_TESTS = \ 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 diff --git a/test/unit/util/integer_black.h b/test/unit/util/integer_black.h new file mode 100644 index 000000000..afd2145e3 --- /dev/null +++ b/test/unit/util/integer_black.h @@ -0,0 +1,276 @@ +/********************* */ +/** 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 +#include + +#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()); + } + +}; diff --git a/test/unit/util/integer_white.h b/test/unit/util/integer_white.h new file mode 100644 index 000000000..739715ac2 --- /dev/null +++ b/test/unit/util/integer_white.h @@ -0,0 +1,40 @@ +/********************* */ +/** 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 +#include + +#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); + } +}; diff --git a/test/unit/util/rational_white.h b/test/unit/util/rational_white.h new file mode 100644 index 000000000..6acc5b71f --- /dev/null +++ b/test/unit/util/rational_white.h @@ -0,0 +1,98 @@ +/********************* */ +/** 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 +#include + +#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())); + } +};