From: Tim King Date: Sun, 28 Mar 2010 21:39:39 +0000 (+0000) Subject: Improved the documentation and testing for Rational. X-Git-Tag: cvc5-1.0.0~9166 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b19c6c93f12eab5ecbcb7d6c164cc9ca541313c;p=cvc5.git Improved the documentation and testing for Rational. --- diff --git a/src/util/rational.h b/src/util/rational.h index e3f760031..b22f44a2c 100644 --- a/src/util/rational.h +++ b/src/util/rational.h @@ -11,6 +11,12 @@ ** information. ** ** A multiprecision rational constant. + ** This stores the rational as a pair of multiprecision integers, + ** one for the numerator and one for the denominator. + ** The number is always stored so that the gcd of the numerator and denominator + ** is 1. (This is referred to as referred to as canonical form in GMP's + ** literature.) A consquence is that that the numerator and denominator may be + ** different than the values used to construct the Rational. **/ #include @@ -46,7 +52,7 @@ public: } /** - * Constructs a Rational from a C string. + * Constructs a Rational from a C string in a given base (defaults to 10). * 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(). @@ -58,10 +64,16 @@ public: d_value.canonicalize(); } + /** + * Creates a Rational from another Rational, q, by performing a deep copy. + */ Rational(const Rational& q) : d_value(q.d_value) { d_value.canonicalize(); } + /** + * Constructs a canonical Rational from a numerator and denominator. + */ Rational( signed int n, signed int d) : d_value(n,d) { d_value.canonicalize(); } @@ -84,10 +96,18 @@ public: ~Rational() {} + /** + * Returns the value of numerator of the Rational. + * Note that this makes a deep copy of the numerator. + */ Integer getNumerator() const { return Integer(d_value.get_num()); } + /** + * Returns the value of denominator of the Rational. + * Note that this makes a deep copy of the denominator. + */ Integer getDenominator() const{ return Integer(d_value.get_den()); } @@ -143,17 +163,14 @@ public: return Rational( d_value / y.d_value ); } + /** Returns a string representing the rational in the given base. */ 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. + * Computes the hash of the rational from hashes of the numerator and the + * denominator. */ size_t hash() const { size_t numeratorHash = gmpz_hash(d_value.get_num_mpz_t()); diff --git a/test/unit/util/rational_white.h b/test/unit/util/rational_white.h index 6acc5b71f..5e3f2868a 100644 --- a/test/unit/util/rational_white.h +++ b/test/unit/util/rational_white.h @@ -26,6 +26,333 @@ const char* canReduce = "4547897890548754897897897897890789078907890/54878902347 class RationalWhite : public CxxTest::TestSuite { public: + + void testDestructor(){ + Rational* q = new Rational(canReduce); + TS_ASSERT_THROWS_NOTHING( delete q ); + } + + void testConstructors(){ + Rational zero; //Default constructor + TS_ASSERT_EQUALS(0L, zero.getNumerator().getLong()); + TS_ASSERT_EQUALS(1L, zero.getDenominator().getLong()); + + Rational reduced_cstring_base_10(canReduce); + Integer tmp0("2273948945274377448948948948945394539453945"); + Integer tmp1("27439451173945117"); + TS_ASSERT_EQUALS(reduced_cstring_base_10.getNumerator(), tmp0); + TS_ASSERT_EQUALS(reduced_cstring_base_10.getDenominator(), tmp1); + + Rational reduced_cstring_base_16(canReduce, 16); + Integer tmp2("405008068100961292527303019616635131091442462891556",10); + Integer tmp3("24363950654420566157",10); + TS_ASSERT_EQUALS(tmp2, reduced_cstring_base_16.getNumerator()); + TS_ASSERT_EQUALS(tmp3, reduced_cstring_base_16.getDenominator()); + + string stringCanReduce(canReduce); + Rational reduced_cppstring_base_10(stringCanReduce); + TS_ASSERT_EQUALS(reduced_cppstring_base_10.getNumerator(), tmp0); + TS_ASSERT_EQUALS(reduced_cppstring_base_10.getDenominator(), tmp1); + Rational reduced_cppstring_base_16(stringCanReduce, 16); + TS_ASSERT_EQUALS(tmp2, reduced_cppstring_base_16.getNumerator()); + TS_ASSERT_EQUALS(tmp3, reduced_cppstring_base_16.getDenominator()); + + Rational cpy_cnstr(zero); + TS_ASSERT_EQUALS(0L, cpy_cnstr.getNumerator().getLong()); + TS_ASSERT_EQUALS(1L, cpy_cnstr.getDenominator().getLong()); + //Check that zero is unaffected + TS_ASSERT_EQUALS(0L, zero.getNumerator().getLong()); + TS_ASSERT_EQUALS(1L, zero.getDenominator().getLong()); + + + signed int nsi = -5478, dsi = 34783; + unsigned int nui = 5478u, dui = 347589u; + signed long int nsli = 2348905477690867690l, dsli = -3475765675789089l; + unsigned long int nuli = 8434689476905478ul, duli = 3234475234894569047ul; + + Rational qsi(nsi, dsi); + Rational qui(nui, dui); + Rational qsli(nsli, dsli); + Rational quli(nuli, duli); + + TS_ASSERT_EQUALS(nsi, qsi.getNumerator().getLong()); + TS_ASSERT_EQUALS(dsi, qsi.getDenominator().getLong()); + + + TS_ASSERT_EQUALS(nui/33, qui.getNumerator().getUnsignedLong()); + TS_ASSERT_EQUALS(dui/33, qui.getDenominator().getUnsignedLong()); + + + TS_ASSERT_EQUALS(-nsli, qsli.getNumerator().getLong()); + TS_ASSERT_EQUALS(-dsli, qsli.getDenominator().getLong()); + + TS_ASSERT_EQUALS(nuli, quli.getNumerator().getUnsignedLong()); + TS_ASSERT_EQUALS(duli, quli.getDenominator().getUnsignedLong()); + + Integer nz("942358903458908903485"); + Integer dz("547890579034790793457934807"); + Rational qz(nz, dz); + TS_ASSERT_EQUALS(nz, qz.getNumerator()); + TS_ASSERT_EQUALS(dz, qz.getDenominator()); + + //Not sure how to catch this... + //TS_ASSERT_THROWS(Rational div_0(0,0),__gmp_exception ); + } + + void testOperatorAssign(){ + Rational x(0,1); + Rational y(78,6); + Rational z(45789,1); + + TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 0); + TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 13); + TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789); + + x = y = z; + + TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789); + TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 45789); + TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789); + + Rational a(78,91); + + y = a; + + TS_ASSERT_EQUALS(a.getNumerator().getUnsignedLong(), 6); + TS_ASSERT_EQUALS(a.getDenominator().getUnsignedLong(), 7); + TS_ASSERT_EQUALS(y.getNumerator().getUnsignedLong(), 6); + TS_ASSERT_EQUALS(y.getDenominator().getUnsignedLong(), 7); + TS_ASSERT_EQUALS(x.getNumerator().getUnsignedLong(), 45789); + TS_ASSERT_EQUALS(z.getNumerator().getUnsignedLong(), 45789); + } + + void testToStringStuff(){ + stringstream ss; + Rational large (canReduce); + ss << large; + string res = ss.str(); + + TS_ASSERT_EQUALS(res, large.toString()); + } + void testOperatorEquals(){ + Rational a; + Rational b(canReduce); + Rational c("2273948945274377448948948948945394539453945/27439451173945117"); + Rational d(0,-237489); + + 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(){ + Rational a; + Rational b(canReduce); + Rational c("2273948945274377448948948948945394539453945/27439451173945117"); + Rational d(0,-237489); + + 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(){ + Rational x(3,2); + Rational y(7,8); + Rational z(-3,33); + + + Rational act0 = x - x; + Rational act1 = x - y; + Rational act2 = x - z; + Rational exp0(0,1); + Rational exp1(5,8); + Rational exp2(35,22); + + + Rational act3 = y - x; + Rational act4 = y - y; + Rational act5 = y - z; + Rational exp3(-5,8); + Rational exp4(0,1); + Rational exp5(85,88); + + + Rational act6 = z - x; + Rational act7 = z - y; + Rational act8 = z - z; + Rational exp6(-35,22); + Rational exp7(-85, 88); + Rational exp8(0, 1); + + + + 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(){ + Rational x(3,2); + Rational y(7,8); + Rational z(-3,33); + + + Rational act0 = x + x; + Rational act1 = x + y; + Rational act2 = x + z; + Rational exp0(3,1); + Rational exp1(19,8); + Rational exp2(31,22); + + + Rational act3 = y + x; + Rational act4 = y + y; + Rational act5 = y + z; + Rational exp3(19,8); + Rational exp4(7,4); + Rational exp5(69,88); + + + Rational act6 = z + x; + Rational act7 = z + y; + Rational act8 = z + z; + Rational exp6(31,22); + Rational exp7(69, 88); + Rational exp8(-2, 11); + + + + 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(){ + Rational x(3,2); + Rational y(7,8); + Rational z(-3,33); + + + Rational act0 = x * x; + Rational act1 = x * y; + Rational act2 = x * z; + Rational exp0(9,4); + Rational exp1(21,16); + Rational exp2(-3,22); + + + Rational act3 = y * x; + Rational act4 = y * y; + Rational act5 = y * z; + Rational exp3(21,16); + Rational exp4(49,64); + Rational exp5(-7,88); + + + Rational act6 = z * x; + Rational act7 = z * y; + Rational act8 = z * z; + Rational exp6(-3, 22); + Rational exp7(-7, 88); + Rational exp8(1, 121); + + + + 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 testOperatorDiv(){ + Rational x(3,2); + Rational y(7,8); + Rational z(-3,33); + + + Rational act0 = x / x; + Rational act1 = x / y; + Rational act2 = x / z; + Rational exp0(1,1); + Rational exp1(12,7); + Rational exp2(-33,2); + + + Rational act3 = y / x; + Rational act4 = y / y; + Rational act5 = y / z; + Rational exp3(7,12); + Rational exp4(1,1); + Rational exp5(-77,8); + + + Rational act6 = z / x; + Rational act7 = z / y; + Rational act8 = z / z; + Rational exp6(-2,33); + Rational exp7(-8, 77); + Rational exp8(1, 1); + + + + 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 testReductionAtConstructionTime(){ Rational reduce0(canReduce); Integer num0("2273948945274377448948948948945394539453945");