summaryrefslogtreecommitdiff
path: root/src/util/rational_gmp_imp.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/util/rational_gmp_imp.h')
-rw-r--r--src/util/rational_gmp_imp.h252
1 files changed, 116 insertions, 136 deletions
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index ff8a0f776..6054cd793 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -2,9 +2,9 @@
/*! \file rational_gmp_imp.h
** \verbatim
** Top contributors (to current version):
- ** Tim King, Morgan Deters, Christopher L. Conway
+ ** Tim King, Gereon Kremer, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
** in the top-level source directory) and their institutional affiliations.
** All rights reserved. See the file COPYING in the top-level source
** directory for licensing information.\endverbatim
@@ -25,9 +25,9 @@
* cause errors: https://gcc.gnu.org/gcc-4.9/porting_to.html
* Including <cstddef> is a workaround for this issue.
*/
-#include <cstddef>
-
#include <gmp.h>
+
+#include <cstddef>
#include <string>
#include "base/exception.h"
@@ -51,23 +51,16 @@ namespace CVC4 {
** 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.
- */
- mpq_class d_value;
-
+class CVC4_PUBLIC Rational
+{
+ public:
/**
* 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:
+ Rational(const mpq_class& val) : d_value(val) {}
/**
* Creates a rational from a decimal string (e.g., <code>"1.5"</code>).
@@ -78,9 +71,7 @@ public:
static Rational fromDecimal(const std::string& dec);
/** Constructs a rational with the value 0/1. */
- Rational() : d_value(0){
- d_value.canonicalize();
- }
+ Rational() : d_value(0) { d_value.canonicalize(); }
/**
* Constructs a Rational from a C string in a given base (defaults to 10).
@@ -89,41 +80,35 @@ public:
* For more information about what is a valid rational string,
* see GMP's documentation for mpq_set_str().
*/
- explicit Rational(const char* s, unsigned base = 10): d_value(s, base) {
+ explicit Rational(const char* s, unsigned base = 10) : d_value(s, base)
+ {
d_value.canonicalize();
}
- Rational(const std::string& s, unsigned base = 10) : d_value(s, base) {
+ Rational(const std::string& s, unsigned base = 10) : d_value(s, base)
+ {
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();
- }
+ Rational(const Rational& q) : d_value(q.d_value) { d_value.canonicalize(); }
/**
* Constructs a canonical Rational from a numerator.
*/
- Rational(signed int n) : d_value(n,1) {
- d_value.canonicalize();
- }
- Rational(unsigned int n) : d_value(n,1) {
- d_value.canonicalize();
- }
- Rational(signed long int n) : d_value(n,1) {
- d_value.canonicalize();
- }
- Rational(unsigned long int n) : d_value(n,1) {
- d_value.canonicalize();
- }
+ Rational(signed int n) : d_value(n, 1) { d_value.canonicalize(); }
+ Rational(unsigned int n) : d_value(n, 1) { d_value.canonicalize(); }
+ Rational(signed long int n) : d_value(n, 1) { d_value.canonicalize(); }
+ Rational(unsigned long int n) : d_value(n, 1) { d_value.canonicalize(); }
#ifdef CVC4_NEED_INT64_T_OVERLOADS
- Rational(int64_t n) : d_value(static_cast<long>(n), 1) {
+ Rational(int64_t n) : d_value(static_cast<long>(n), 1)
+ {
d_value.canonicalize();
}
- Rational(uint64_t n) : d_value(static_cast<unsigned long>(n), 1) {
+ Rational(uint64_t n) : d_value(static_cast<unsigned long>(n), 1)
+ {
d_value.canonicalize();
}
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
@@ -131,63 +116,60 @@ public:
/**
* Constructs a canonical Rational from a numerator and denominator.
*/
- Rational(signed int n, signed int d) : d_value(n,d) {
+ 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) {
+ 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) {
+ 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) {
+ Rational(unsigned long int n, unsigned long int d) : d_value(n, d)
+ {
d_value.canonicalize();
}
#ifdef CVC4_NEED_INT64_T_OVERLOADS
- Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n), static_cast<long>(d)) {
+ Rational(int64_t n, int64_t d)
+ : d_value(static_cast<long>(n), static_cast<long>(d))
+ {
d_value.canonicalize();
}
- Rational(uint64_t n, uint64_t d) : d_value(static_cast<unsigned long>(n), static_cast<unsigned long>(d)) {
+ Rational(uint64_t n, uint64_t d)
+ : d_value(static_cast<unsigned long>(n), static_cast<unsigned long>(d))
+ {
d_value.canonicalize();
}
#endif /* CVC4_NEED_INT64_T_OVERLOADS */
- Rational(const Integer& n, const Integer& d) :
- d_value(n.get_mpz(), d.get_mpz())
- {
- d_value.canonicalize();
- }
- Rational(const Integer& n) :
- d_value(n.get_mpz())
+ Rational(const Integer& n, const Integer& d)
+ : d_value(n.get_mpz(), d.get_mpz())
{
d_value.canonicalize();
}
+ Rational(const Integer& n) : d_value(n.get_mpz()) { d_value.canonicalize(); }
~Rational() {}
/**
* Returns a copy of d_value to enable public access of GMP data.
*/
- mpq_class getValue() const
- {
- return d_value;
- }
+ const mpq_class& 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(d_value.get_num());
- }
+ 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());
- }
+ Integer getDenominator() const { return Integer(d_value.get_den()); }
static Maybe<Rational> fromDouble(double d);
@@ -196,166 +178,164 @@ public:
* approximate: truncation may occur, overflow may result in
* infinity, and underflow may result in zero.
*/
- double getDouble() const {
- return d_value.get_d();
- }
+ double getDouble() const { return d_value.get_d(); }
- Rational inverse() const {
+ Rational inverse() const
+ {
return Rational(getDenominator(), getNumerator());
}
- 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 mpq_cmp(d_value.get_mpq_t(), x.d_value.get_mpq_t());
}
- int sgn() const {
- return mpq_sgn(d_value.get_mpq_t());
- }
+ int sgn() const { return mpq_sgn(d_value.get_mpq_t()); }
- bool isZero() const {
- return sgn() == 0;
- }
+ bool isZero() const { return sgn() == 0; }
- bool isOne() const {
- return mpq_cmp_si(d_value.get_mpq_t(), 1, 1) == 0;
- }
+ bool isOne() const { return mpq_cmp_si(d_value.get_mpq_t(), 1, 1) == 0; }
- bool isNegativeOne() const {
+ bool isNegativeOne() const
+ {
return mpq_cmp_si(d_value.get_mpq_t(), -1, 1) == 0;
}
- Rational abs() const {
- if(sgn() < 0){
+ Rational abs() const
+ {
+ if (sgn() < 0)
+ {
return -(*this);
- }else{
+ }
+ else
+ {
return *this;
}
}
- Integer floor() const {
+ Integer floor() const
+ {
mpz_class q;
mpz_fdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t());
return Integer(q);
}
- Integer ceiling() const {
+ Integer ceiling() const
+ {
mpz_class q;
mpz_cdiv_q(q.get_mpz_t(), d_value.get_num_mpz_t(), d_value.get_den_mpz_t());
return Integer(q);
}
- 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);
}
- bool isIntegral() const{
- return getDenominator() == 1;
- }
+ bool isIntegral() const { return getDenominator() == 1; }
/** Returns a string representing the rational in the given base. */
- std::string toString(int base = 10) const {
- return d_value.get_str(base);
- }
+ std::string toString(int base = 10) const { return d_value.get_str(base); }
/**
* Computes the hash of the rational from hashes of the numerator and the
* denominator.
*/
- size_t hash() const {
+ 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;
}
- uint32_t complexity() const {
+ uint32_t complexity() const
+ {
uint32_t numLen = getNumerator().length();
uint32_t denLen = getDenominator().length();
- return numLen + denLen;
+ return numLen + denLen;
}
/** Equivalent to calling (this->abs()).cmp(b.abs()) */
int absCmp(const Rational& q) const;
-};/* 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;
-struct RationalHashFunction {
- inline size_t operator()(const CVC4::Rational& r) const {
- return r.hash();
- }
-};/* struct RationalHashFunction */
+}; /* class Rational */
+
+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