CVC3

#include <theory_arith_new.h>
EpsRational class ecapsulates the rationals with a symbolic small added. Each rational number is presented as a pair , where is treated symbolically. The operations on the new rationals are defined as
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 277 of file theory_arith_new.h.
enum CVC3::TheoryArithNew::EpsRational::RationalType [protected] 
Type of rationals, normal and the two infinities
Definition at line 282 of file theory_arith_new.h.
CVC3::TheoryArithNew::EpsRational::EpsRational  (  RationalType  type  )  [inline, protected] 
Private constructor to construt infinities.
Definition at line 296 of file theory_arith_new.h.
CVC3::TheoryArithNew::EpsRational::EpsRational  (  )  [inline] 
The blank constructor
Definition at line 351 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 354 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 361 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 370 of file theory_arith_new.h.
bool CVC3::TheoryArithNew::EpsRational::isRational  (  )  const [inline] 
Returns if the number is a plain rational.
Definition at line 305 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 312 of file theory_arith_new.h.
References CVC3::Rational::isInteger(), k, and q.
Referenced by CVC3::TheoryArithNew::checkSatInteger().
Rational CVC3::TheoryArithNew::EpsRational::getFloor  (  )  const [inline] 
Returns the floor of the number using the following formula
Definition at line 325 of file theory_arith_new.h.
References CVC3::Rational::isInteger(), k, and q.
Referenced by CVC3::TheoryArithNew::checkSatInteger().
Rational CVC3::TheoryArithNew::EpsRational::getRational  (  )  const [inline] 
Returns the rational part of the number
Definition at line 340 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 378 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 390 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 403 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 415 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 426 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 434 of file theory_arith_new.h.
bool CVC3::TheoryArithNew::EpsRational::operator<=  (  const EpsRational &  r  )  const [inline] 
Less than or equal comparison operator.
Definition at line 439 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] 
Less than comparison operator.
Definition at line 464 of file theory_arith_new.h.
bool CVC3::TheoryArithNew::EpsRational::operator>  (  const EpsRational &  r  )  const [inline] 
Greater than comparison operator.
Definition at line 469 of file theory_arith_new.h.
std::string CVC3::TheoryArithNew::EpsRational::toString  (  )  const [inline] 
Returns the string representation of the number.
Definition at line 476 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().
RationalType CVC3::TheoryArithNew::EpsRational::type [protected] 
The type of this rational
Definition at line 285 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 288 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 291 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 343 of file theory_arith_new.h.
Referenced by CVC3::TheoryArithNew::getUpperBound().
The negative infinity constant
Definition at line 345 of file theory_arith_new.h.
Referenced by CVC3::TheoryArithNew::getLowerBound().
const TheoryArithNew::EpsRational TheoryArithNew::EpsRational::Zero [static] 
The zero constant
Definition at line 347 of file theory_arith_new.h.
Referenced by CVC3::TheoryArithNew::getBeta().