diff options
Diffstat (limited to 'src/util/rational_cln_imp.h')
-rw-r--r-- | src/util/rational_cln_imp.h | 286 |
1 files changed, 286 insertions, 0 deletions
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h new file mode 100644 index 000000000..347c1d195 --- /dev/null +++ b/src/util/rational_cln_imp.h @@ -0,0 +1,286 @@ +/********************* */ +/*! \file rational.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): dejan, mdeters, cconway + ** 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.\endverbatim + ** + ** \brief Multi-precision rational constants. + ** + ** Multi-precision rational constants. + **/ + +#ifdef __CVC4__USE_CLN_IMP + +#include "cvc4_public.h" + +#ifndef __CVC4__RATIONAL_H +#define __CVC4__RATIONAL_H + +#include <gmp.h> +#include <string> +#include <sstream> +#include <cln/rational.h> +#include <cln/input.h> +#include <cln/rational_io.h> +#include <cln/number_io.h> +#include "util/Assert.h" +#include "util/integer.h" + +namespace CVC4 { + +/** + ** A multi-precision rational constant. + ** This stores the rational as a pair of multi-precision 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 consequence is that that the numerator and denominator may be + ** different than the values used to construct the Rational. + ** + ** NOTE: The correct way to create a Rational from an int is to use one of the + ** int numerator/int denominator constructors with the denominator 1. Trying + ** to construct a Rational with a single int, e.g., Rational(0), will put you + ** in danger of invoking the char* constructor, from whence you will segfault. + **/ + +class CVC4_PUBLIC 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. + */ + cln::cl_RA 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) { } + Rational(const cln::cl_RA& val) : d_value(val) { } + +public: + + /** Creates a rational from a decimal string (e.g., <code>"1.5"</code>). + * + * @param dec a string encoding a decimal number in the format + * <code>[0-9]*\.[0-9]*</code> + */ + static Rational fromDecimal(const std::string& dec); + + /** Constructs a rational with the value 0/1. */ + Rational() : d_value(0){ + } + + /** + * Constructs a Rational from a C string in a given base (defaults to 10). + * Throws std::invalid_argument if the string is not a valid rational. + * For more information about what is a valid rational string, + * see GMP's documentation for mpq_set_str(). + */ + explicit Rational(const char * s, int base = 10) throw (std::invalid_argument){ + cln::cl_read_flags flags; + + flags.syntax = cln::syntax_rational; + flags.lsyntax = cln::lsyntax_standard; + flags.rational_base = base; + try{ + d_value = read_rational(flags, s, NULL, NULL); + }catch(...){ + std::stringstream ss; + ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base; + throw std::invalid_argument(ss.str()); + } + } + Rational(const std::string& s, int base = 10) throw (std::invalid_argument){ + cln::cl_read_flags flags; + + flags.syntax = cln::syntax_rational; + flags.lsyntax = cln::lsyntax_standard; + flags.rational_base = base; + try{ + d_value = read_rational(flags, s.c_str(), NULL, NULL); + }catch(...){ + std::stringstream ss; + ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base; + throw std::invalid_argument(ss.str()); + } + } + + /** + * Creates a Rational from another Rational, q, by performing a deep copy. + */ + Rational(const Rational& q) : d_value(q.d_value) { } + + /** + * Constructs a canonical Rational from a numerator. + */ + Rational(signed int n) : d_value(n) { } + Rational(unsigned int n) : d_value(n) { } + Rational(signed long int n) : d_value(n) { } + Rational(unsigned long int n) : d_value(n) { } + + /** + * Constructs a canonical Rational from a numerator and denominator. + */ + Rational(signed int n, signed int d) : d_value(n) { + d_value /= d; + } + Rational(unsigned int n, unsigned int d) : d_value(n) { + d_value /= d; + } + Rational(signed long int n, signed long int d) : d_value(n) { + d_value /= d; + } + Rational(unsigned long int n, unsigned long int d) : d_value(n) { + d_value /= d; + } + + Rational(const Integer& n, const Integer& d) : + d_value(n.get_cl_I()) + { + d_value /= d.get_cl_I(); + } + Rational(const Integer& n) : d_value(n.get_cl_I()){ } + + ~Rational() {} + + + /** + * Returns the value of numerator of the Rational. + * Note that this makes a deep copy of the numerator. + */ + Integer getNumerator() const { + return Integer(cln::numerator(d_value)); + } + + /** + * Returns the value of denominator of the Rational. + * Note that this makes a deep copy of the denominator. + */ + Integer getDenominator() const{ + return Integer(cln::denominator(d_value)); + } + + Rational inverse() const { + return Rational(cln::recip(d_value)); + } + + int cmp(const Rational& x) const { + //Don't use mpq_class's cmp() function. + //The name ends up conflicting with this function. + return cln::compare(d_value, x.d_value); + } + + + int sgn() { + cln::cl_RA sign = cln::signum(d_value); + if(sign == 0) + return 0; + else if(sign == -1) + return -1; + else if(sign == 1) + return 1; + else + Unreachable(); + } + + 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 ); + } + + Rational& operator+=(const Rational& y){ + d_value += y.d_value; + return (*this); + } + + Rational& operator*=(const Rational& y){ + d_value *= y.d_value; + return (*this); + } + + /** Returns a string representing the rational in the given base. */ + std::string toString(int base = 10) const { + std::stringstream ss; + fprint(ss, d_value); + return ss.str(); + } + + /** + * Computes the hash of the rational from hashes of the numerator and the + * denominator. + */ + size_t hash() const { + return equal_hashcode(d_value); + } + +};/* class Rational */ + +struct RationalHashStrategy { + static inline size_t hash(const CVC4::Rational& r) { + return r.hash(); + } +};/* struct RationalHashStrategy */ + +std::ostream& operator<<(std::ostream& os, const Rational& n); + +}/* CVC4 namespace */ + +#endif /* __CVC4__RATIONAL_H */ + +#endif /* __CVC4__USE_CLN_IMP */ |