summaryrefslogtreecommitdiff
path: root/src/util/rational_cln_imp.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/rational_cln_imp.h')
-rw-r--r--src/util/rational_cln_imp.h286
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback