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.h273
1 files changed, 129 insertions, 144 deletions
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index f4394bbee..9b391008a 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -20,19 +20,19 @@
#ifndef CVC4__RATIONAL_H
#define CVC4__RATIONAL_H
-#include <gmp.h>
-#include <string>
-#include <sstream>
-#include <cassert>
-#include <cln/rational.h>
+#include <cln/dfloat.h>
#include <cln/input.h>
#include <cln/io.h>
+#include <cln/number_io.h>
#include <cln/output.h>
+#include <cln/rational.h>
#include <cln/rational_io.h>
-#include <cln/number_io.h>
-#include <cln/dfloat.h>
#include <cln/real.h>
+#include <cassert>
+#include <sstream>
+#include <string>
+
#include "base/exception.h"
#include "util/integer.h"
#include "util/maybe.h"
@@ -54,24 +54,14 @@ namespace CVC4 {
** in danger of invoking the char* constructor, from whence you will segfault.
**/
-class CVC4_PUBLIC Rational {
-private:
+class CVC4_PUBLIC Rational
+{
+ public:
/**
- * 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.
+ * Constructs a Rational from a cln::cl_RA 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:
+ Rational(const cln::cl_RA& val) : d_value(val) {}
/**
* Creates a rational from a decimal string (e.g., <code>"1.5"</code>).
@@ -82,14 +72,13 @@ public:
static Rational fromDecimal(const std::string& dec);
/** Constructs a rational with the value 0/1. */
- Rational() : d_value(0){
- }
+ 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().
+ * see CLN's documentation for read_rational.
*/
explicit Rational(const char* s, unsigned base = 10)
{
@@ -98,11 +87,14 @@ public:
flags.syntax = cln::syntax_rational;
flags.lsyntax = cln::lsyntax_standard;
flags.rational_base = base;
- try{
+ try
+ {
d_value = read_rational(flags, s, NULL, NULL);
- }catch(...){
+ }
+ catch (...)
+ {
std::stringstream ss;
- ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base;
+ ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
throw std::invalid_argument(ss.str());
}
}
@@ -113,11 +105,14 @@ public:
flags.syntax = cln::syntax_rational;
flags.lsyntax = cln::lsyntax_standard;
flags.rational_base = base;
- try{
+ try
+ {
d_value = read_rational(flags, s.c_str(), NULL, NULL);
- }catch(...){
+ }
+ catch (...)
+ {
std::stringstream ss;
- ss << "Rational() failed to parse value \"" <<s << "\" in base=" <<base;
+ ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
throw std::invalid_argument(ss.str());
}
}
@@ -125,78 +120,76 @@ public:
/**
* Creates a Rational from another Rational, q, by performing a deep copy.
*/
- Rational(const Rational& q) : d_value(q.d_value) { }
+ Rational(const Rational& q) : d_value(q.d_value) {}
/**
* Constructs a canonical Rational from a numerator.
*/
- Rational(signed int n) : d_value((signed long int)n) { }
- Rational(unsigned int n) : d_value((unsigned long int)n) { }
- Rational(signed long int n) : d_value(n) { }
- Rational(unsigned long int n) : d_value(n) { }
+ Rational(signed int n) : d_value((signed long int)n) {}
+ Rational(unsigned int n) : d_value((unsigned long int)n) {}
+ Rational(signed long int n) : d_value(n) {}
+ Rational(unsigned long int n) : d_value(n) {}
#ifdef CVC4_NEED_INT64_T_OVERLOADS
- Rational(int64_t n) : d_value(static_cast<long>(n)) { }
- Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) { }
+ Rational(int64_t n) : d_value(static_cast<long>(n)) {}
+ Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) {}
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
/**
* Constructs a canonical Rational from a numerator and denominator.
*/
- Rational(signed int n, signed int d) : d_value((signed long int)n) {
+ Rational(signed int n, signed int d) : d_value((signed long int)n)
+ {
d_value /= cln::cl_I(d);
}
- Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n) {
+ Rational(unsigned int n, unsigned int d) : d_value((unsigned long int)n)
+ {
d_value /= cln::cl_I(d);
}
- Rational(signed long int n, signed long int d) : d_value(n) {
+ Rational(signed long int n, signed long int d) : d_value(n)
+ {
d_value /= cln::cl_I(d);
}
- Rational(unsigned long int n, unsigned long int d) : d_value(n) {
+ Rational(unsigned long int n, unsigned long int d) : d_value(n)
+ {
d_value /= cln::cl_I(d);
}
#ifdef CVC4_NEED_INT64_T_OVERLOADS
- Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n)) {
+ Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n))
+ {
d_value /= cln::cl_I(d);
}
- Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n)) {
+ Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n))
+ {
d_value /= cln::cl_I(d);
}
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
- Rational(const Integer& n, const Integer& d) :
- d_value(n.get_cl_I())
+ 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(const Integer& n) : d_value(n.get_cl_I()) {}
~Rational() {}
/**
* Returns a copy of d_value to enable public access of CLN data.
*/
- cln::cl_RA getValue() const
- {
- return d_value;
- }
+ const cln::cl_RA& getValue() const { return d_value; }
/**
* 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));
- }
+ 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));
- }
+ Integer getDenominator() const { return Integer(cln::denominator(d_value)); }
/** Return an exact rational for a double d. */
static Maybe<Rational> fromDouble(double d);
@@ -206,138 +199,126 @@ public:
* approximate: truncation may occur, overflow may result in
* infinity, and underflow may result in zero.
*/
- double getDouble() const {
- return cln::double_approx(d_value);
- }
+ double getDouble() const { return cln::double_approx(d_value); }
- Rational inverse() const {
- return Rational(cln::recip(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.
+ 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() const {
- if(cln::zerop(d_value)){
- return 0;
- }else if(cln::minusp(d_value)){
- return -1;
- }else{
+ int sgn() const
+ {
+ if (cln::zerop(d_value))
+ {
+ return 0;
+ }
+ else if (cln::minusp(d_value))
+ {
+ return -1;
+ }
+ else
+ {
assert(cln::plusp(d_value));
return 1;
}
}
- bool isZero() const {
- return cln::zerop(d_value);
- }
+ bool isZero() const { return cln::zerop(d_value); }
- bool isOne() const {
- return d_value == 1;
- }
+ bool isOne() const { return d_value == 1; }
- bool isNegativeOne() const {
- return d_value == -1;
- }
+ bool isNegativeOne() const { return d_value == -1; }
- Rational abs() const {
- if(sgn() < 0){
+ Rational abs() const
+ {
+ if (sgn() < 0)
+ {
return -(*this);
- }else{
+ }
+ else
+ {
return *this;
}
}
- bool isIntegral() const{
- return getDenominator() == 1;
- }
+ bool isIntegral() const { return getDenominator() == 1; }
- Integer floor() const {
- return Integer(cln::floor1(d_value));
- }
+ Integer floor() const { return Integer(cln::floor1(d_value)); }
- Integer ceiling() const {
- return Integer(cln::ceiling1(d_value));
- }
+ Integer ceiling() const { return Integer(cln::ceiling1(d_value)); }
- Rational floor_frac() const {
- return (*this) - Rational(floor());
- }
+ Rational floor_frac() const { return (*this) - Rational(floor()); }
- Rational& operator=(const Rational& x){
- if(this == &x) return *this;
+ Rational& operator=(const Rational& x)
+ {
+ if (this == &x) return *this;
d_value = x.d_value;
return *this;
}
- Rational operator-() const{
- return Rational(-(d_value));
- }
+ 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; }
- 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) 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){
+ Rational& operator+=(const Rational& y)
+ {
d_value += y.d_value;
return (*this);
}
- Rational& operator-=(const Rational& y){
+ Rational& operator-=(const Rational& y)
+ {
d_value -= y.d_value;
return (*this);
}
- Rational& operator*=(const Rational& y){
+ Rational& operator*=(const Rational& y)
+ {
d_value *= y.d_value;
return (*this);
}
- Rational& operator/=(const Rational& y){
+ 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::string toString(int base = 10) const
+ {
cln::cl_print_flags flags;
flags.rational_base = base;
flags.rational_readably = false;
@@ -350,27 +331,31 @@ public:
* Computes the hash of the rational from hashes of the numerator and the
* denominator.
*/
- size_t hash() const {
- return equal_hashcode(d_value);
- }
+ size_t hash() const { return equal_hashcode(d_value); }
- uint32_t complexity() const {
+ uint32_t complexity() const
+ {
return getNumerator().length() + getDenominator().length();
}
/** Equivalent to calling (this->abs()).cmp(b.abs()) */
int absCmp(const Rational& q) const;
-};/* class Rational */
+ private:
+ /**
+ * Stores the value of the rational in a C++ CLN rational class.
+ */
+ cln::cl_RA d_value;
+
+}; /* class Rational */
-struct RationalHashFunction {
- inline size_t operator()(const CVC4::Rational& r) const {
- return r.hash();
- }
-};/* struct RationalHashFunction */
+struct RationalHashFunction
+{
+ inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); }
+}; /* struct RationalHashFunction */
CVC4_PUBLIC std::ostream& operator<<(std::ostream& os, const Rational& n);
-}/* CVC4 namespace */
+} // namespace CVC4
#endif /* CVC4__RATIONAL_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback