#include <theory_arith_new.h>
Collaboration diagram for CVC3::TheoryArithNew::EpsRational:
Note that the operations on the infinite values are not defined, as they are never used currently. Infinities can only be asigned or compared.
Definition at line 275 of file theory_arith_new.h.
enum CVC3::TheoryArithNew::EpsRational::RationalType [protected] |
Type of rationals, normal and the two infinities
Definition at line 280 of file theory_arith_new.h.
enum CVC3::TheoryArithNew::EpsRational::RationalType [protected] |
Type of rationals, normal and the two infinities
Definition at line 284 of file theory_arith_new.mine.h.
CVC3::TheoryArithNew::EpsRational::EpsRational | ( | RationalType | type | ) | [inline, protected] |
Private constructor to construt infinities.
Definition at line 294 of file theory_arith_new.h.
CVC3::TheoryArithNew::EpsRational::EpsRational | ( | ) | [inline] |
The blank constructor
Definition at line 349 of file theory_arith_new.h.
Referenced by operator *(), operator+(), operator-(), and operator/().
CVC3::TheoryArithNew::EpsRational::EpsRational | ( | const EpsRational & | r | ) | [inline] |
Copy constructor
Definition at line 352 of file theory_arith_new.h.
CVC3::TheoryArithNew::EpsRational::EpsRational | ( | const Rational | q | ) | [inline] |
Constructor from a rational, constructs a new pair (q, 0).
q | the rational |
Definition at line 359 of file theory_arith_new.h.
Constructor from a rational and a given epsilon multiplier, constructs a new pair (q, k).
q | the rational | |
k | the epsilon multiplier |
Definition at line 368 of file theory_arith_new.h.
CVC3::TheoryArithNew::EpsRational::EpsRational | ( | RationalType | type | ) | [inline, protected] |
Private constructor to construt infinities.
Definition at line 298 of file theory_arith_new.mine.h.
CVC3::TheoryArithNew::EpsRational::EpsRational | ( | ) | [inline] |
The blank constructor
Definition at line 353 of file theory_arith_new.mine.h.
CVC3::TheoryArithNew::EpsRational::EpsRational | ( | const EpsRational & | r | ) | [inline] |
Copy constructor
Definition at line 356 of file theory_arith_new.mine.h.
CVC3::TheoryArithNew::EpsRational::EpsRational | ( | const Rational | q | ) | [inline] |
Constructor from a rational, constructs a new pair (q, 0).
q | the rational |
Definition at line 363 of file theory_arith_new.mine.h.
Constructor from a rational and a given epsilon multiplier, constructs a new pair (q, k).
q | the rational | |
k | the epsilon multiplier |
Definition at line 372 of file theory_arith_new.mine.h.
bool CVC3::TheoryArithNew::EpsRational::isRational | ( | ) | const [inline] |
Returns if the number is a plain rational.
Definition at line 303 of file theory_arith_new.h.
References k.
bool CVC3::TheoryArithNew::EpsRational::isInteger | ( | ) | const [inline] |
Returns if the number is a plain integer.
Definition at line 310 of file theory_arith_new.h.
References CVC3::Rational::isInteger(), k, and q.
Rational CVC3::TheoryArithNew::EpsRational::getFloor | ( | ) | const [inline] |
Returns the floor of the number using the following fomula
Definition at line 323 of file theory_arith_new.h.
References CVC3::Rational::isInteger(), k, and q.
Rational CVC3::TheoryArithNew::EpsRational::getRational | ( | ) | const [inline] |
Returns the rational part of the number
Definition at line 338 of file theory_arith_new.h.
References q.
Referenced by CVC3::TheoryArithNew::deriveGomoryCut().
EpsRational CVC3::TheoryArithNew::EpsRational::operator+ | ( | const EpsRational & | r | ) | const [inline] |
Addition operator for two EpsRational numbers.
r | the number to be added |
Definition at line 376 of file theory_arith_new.h.
References DebugAssert, EpsRational(), FINITE, k, q, and type.
EpsRational& CVC3::TheoryArithNew::EpsRational::operator+= | ( | const EpsRational & | r | ) | [inline] |
Addition operator for two EpsRational numbers.
r | the number to be added |
Definition at line 388 of file theory_arith_new.h.
References DebugAssert, FINITE, k, q, and type.
EpsRational CVC3::TheoryArithNew::EpsRational::operator- | ( | const EpsRational & | r | ) | const [inline] |
Subtraction operator for two EpsRational numbers.
r | the number to be added |
Definition at line 401 of file theory_arith_new.h.
References DebugAssert, EpsRational(), FINITE, k, q, and type.
EpsRational CVC3::TheoryArithNew::EpsRational::operator * | ( | const Rational & | a | ) | const [inline] |
Multiplication operator EpsRational number and a rational number.
a | the number to be multiplied |
Definition at line 413 of file theory_arith_new.h.
References DebugAssert, EpsRational(), FINITE, k, q, and type.
EpsRational CVC3::TheoryArithNew::EpsRational::operator/ | ( | const Rational & | a | ) | const [inline] |
Division operator EpsRational number and a rational number.
a | the number to be multiplied |
Definition at line 424 of file theory_arith_new.h.
References DebugAssert, EpsRational(), FINITE, k, q, and type.
bool CVC3::TheoryArithNew::EpsRational::operator== | ( | const EpsRational & | r | ) | const [inline] |
Equality comparison operator.
Definition at line 432 of file theory_arith_new.h.
bool CVC3::TheoryArithNew::EpsRational::operator<= | ( | const EpsRational & | r | ) | const [inline] |
Les then or equal comparison operator.
Definition at line 437 of file theory_arith_new.h.
References FatalAssert, FINITE, k, MINUS_INFINITY, PLUS_INFINITY, q, and type.
bool CVC3::TheoryArithNew::EpsRational::operator< | ( | const EpsRational & | r | ) | const [inline] |
Les then comparison operator.
Definition at line 462 of file theory_arith_new.h.
bool CVC3::TheoryArithNew::EpsRational::operator> | ( | const EpsRational & | r | ) | const [inline] |
Bigger then equal comparison operator.
Definition at line 467 of file theory_arith_new.h.
std::string CVC3::TheoryArithNew::EpsRational::toString | ( | ) | const [inline] |
Returns the string representation of the number.
the | string representation of the number |
Definition at line 474 of file theory_arith_new.h.
References FatalAssert, FINITE, k, MINUS_INFINITY, PLUS_INFINITY, q, CVC3::Rational::toString(), and type.
Referenced by CVC3::TheoryArithNew::assertLower(), CVC3::TheoryArithNew::assertUpper(), CVC3::TheoryArithNew::boundsAsString(), CVC3::TheoryArithNew::pivotAndUpdate(), CVC3::TheoryArithNew::propagateTheory(), and CVC3::TheoryArithNew::update().
bool CVC3::TheoryArithNew::EpsRational::isRational | ( | ) | const [inline] |
Returns if the number is a plain rational.
Definition at line 307 of file theory_arith_new.mine.h.
References k.
bool CVC3::TheoryArithNew::EpsRational::isInteger | ( | ) | const [inline] |
Returns if the number is a plain integer.
Definition at line 314 of file theory_arith_new.mine.h.
References CVC3::Rational::isInteger(), k, and q.
Rational CVC3::TheoryArithNew::EpsRational::getFloor | ( | ) | const [inline] |
Returns the floor of the number using the following fomula
Definition at line 327 of file theory_arith_new.mine.h.
References CVC3::Rational::isInteger(), k, and q.
Rational CVC3::TheoryArithNew::EpsRational::getRational | ( | ) | const [inline] |
Returns the rational part of the number
Definition at line 342 of file theory_arith_new.mine.h.
References q.
EpsRational CVC3::TheoryArithNew::EpsRational::operator+ | ( | const EpsRational & | r | ) | const [inline] |
Addition operator for two EpsRational numbers.
r | the number to be added |
Definition at line 380 of file theory_arith_new.mine.h.
References DebugAssert, EpsRational(), FINITE, k, q, and type.
EpsRational& CVC3::TheoryArithNew::EpsRational::operator+= | ( | const EpsRational & | r | ) | [inline] |
Addition operator for two EpsRational numbers.
r | the number to be added |
Definition at line 392 of file theory_arith_new.mine.h.
References DebugAssert, FINITE, k, q, and type.
EpsRational CVC3::TheoryArithNew::EpsRational::operator- | ( | const EpsRational & | r | ) | const [inline] |
Subtraction operator for two EpsRational numbers.
r | the number to be added |
Definition at line 405 of file theory_arith_new.mine.h.
References DebugAssert, EpsRational(), FINITE, k, q, and type.
EpsRational CVC3::TheoryArithNew::EpsRational::operator * | ( | const Rational & | a | ) | const [inline] |
Multiplication operator EpsRational number and a rational number.
a | the number to be multiplied |
Definition at line 417 of file theory_arith_new.mine.h.
References DebugAssert, EpsRational(), FINITE, k, q, and type.
EpsRational CVC3::TheoryArithNew::EpsRational::operator/ | ( | const Rational & | a | ) | const [inline] |
Division operator EpsRational number and a rational number.
a | the number to be multiplied |
Definition at line 428 of file theory_arith_new.mine.h.
References DebugAssert, EpsRational(), FINITE, k, q, and type.
bool CVC3::TheoryArithNew::EpsRational::operator== | ( | const EpsRational & | r | ) | const [inline] |
Equality comparison operator.
Definition at line 436 of file theory_arith_new.mine.h.
bool CVC3::TheoryArithNew::EpsRational::operator<= | ( | const EpsRational & | r | ) | const [inline] |
Les then or equal comparison operator.
Definition at line 441 of file theory_arith_new.mine.h.
References FatalAssert, FINITE, k, MINUS_INFINITY, PLUS_INFINITY, q, and type.
bool CVC3::TheoryArithNew::EpsRational::operator< | ( | const EpsRational & | r | ) | const [inline] |
Les then comparison operator.
Definition at line 466 of file theory_arith_new.mine.h.
bool CVC3::TheoryArithNew::EpsRational::operator> | ( | const EpsRational & | r | ) | const [inline] |
Bigger then equal comparison operator.
Definition at line 471 of file theory_arith_new.mine.h.
std::string CVC3::TheoryArithNew::EpsRational::toString | ( | ) | const [inline] |
Returns the string representation of the number.
the | string representation of the number |
Definition at line 478 of file theory_arith_new.mine.h.
References FatalAssert, FINITE, k, MINUS_INFINITY, PLUS_INFINITY, q, CVC3::Rational::toString(), and type.
RationalType CVC3::TheoryArithNew::EpsRational::type [protected] |
The type of this rational
Definition at line 283 of file theory_arith_new.h.
Referenced by operator *(), operator+(), operator+=(), operator-(), operator/(), operator<=(), and toString().
Rational CVC3::TheoryArithNew::EpsRational::q [protected] |
The rational part
Definition at line 286 of file theory_arith_new.h.
Referenced by getFloor(), getRational(), isInteger(), operator *(), operator+(), operator+=(), operator-(), operator/(), operator<=(), operator==(), and toString().
Rational CVC3::TheoryArithNew::EpsRational::k [protected] |
The epsilon multiplier
Definition at line 289 of file theory_arith_new.h.
Referenced by getFloor(), isInteger(), isRational(), operator *(), operator+(), operator+=(), operator-(), operator/(), operator<=(), operator==(), and toString().
The infinity constant
Definition at line 341 of file theory_arith_new.h.
Referenced by CVC3::TheoryArithNew::getUpperBound().
The negative infinity constant
Definition at line 343 of file theory_arith_new.h.
Referenced by CVC3::TheoryArithNew::getLowerBound().
const TheoryArithNew::EpsRational TheoryArithNew::EpsRational::Zero [static] |
The zero constant
Definition at line 345 of file theory_arith_new.h.
Referenced by CVC3::TheoryArithNew::getBeta().