CVC3  2.4.1
Public Member Functions | Static Public Attributes | Protected Types | Protected Member Functions | Protected Attributes | List of all members
CVC3::TheoryArithNew::EpsRational Class Reference

#include <theory_arith_new.h>

Public Member Functions

bool isRational () const
 
bool isInteger () const
 
Rational getFloor () const
 
Rational getRational () const
 
 EpsRational ()
 
 EpsRational (const EpsRational &r)
 
 EpsRational (const Rational q)
 
 EpsRational (const Rational q, const Rational k)
 
EpsRational operator+ (const EpsRational &r) const
 
EpsRationaloperator+= (const EpsRational &r)
 
EpsRational operator- (const EpsRational &r) const
 
EpsRational operator* (const Rational &a) const
 
EpsRational operator/ (const Rational &a) const
 
bool operator== (const EpsRational &r) const
 
bool operator<= (const EpsRational &r) const
 
bool operator< (const EpsRational &r) const
 
bool operator> (const EpsRational &r) const
 
std::string toString () const
 

Static Public Attributes

static const EpsRational PlusInfinity
 
static const EpsRational MinusInfinity
 
static const EpsRational Zero
 

Protected Types

enum  RationalType { FINITE, PLUS_INFINITY, MINUS_INFINITY }
 

Protected Member Functions

 EpsRational (RationalType type)
 

Protected Attributes

RationalType type
 
Rational q
 
Rational k
 

Detailed Description

EpsRational class ecapsulates the rationals with a symbolic small $\epsilon$ added. Each rational number is presented as a pair $(q, k) = q + k\epsilon$, where $\epsilon$ 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.

Member Enumeration Documentation

Type of rationals, normal and the two infinities

Enumerator
FINITE 
PLUS_INFINITY 
MINUS_INFINITY 

Definition at line 282 of file theory_arith_new.h.

Constructor & Destructor Documentation

CVC3::TheoryArithNew::EpsRational::EpsRational ( RationalType  type)
inlineprotected

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).

Parameters
qthe rational

Definition at line 361 of file theory_arith_new.h.

CVC3::TheoryArithNew::EpsRational::EpsRational ( const Rational  q,
const Rational  k 
)
inline

Constructor from a rational and a given epsilon multiplier, constructs a new pair (q, k).

Parameters
qthe rational
kthe epsilon multiplier

Definition at line 370 of file theory_arith_new.h.

Member Function Documentation

bool CVC3::TheoryArithNew::EpsRational::isRational ( ) const
inline

Returns if the number is a plain rational.

Returns
true if rational, false otherwise

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.

Returns
true if rational, false otherwise

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 $x = q + k \epsilon$ using the following formula

\[ \lfloor \beta(x) \rfloor = \left\{ \begin{tabular}{ll} $\lfloor q \rfloor$ & $\mathrm{if\ } q \notin Z$\\ $q$ & $\mathrm{if\ } q \in Z \mathrm{\ and\ } k \geq 0$\\ $q - 1$ & $\mathrm{if\ } q \in Z \mathrm{\ and\ } k < 0$ \end{tabular}\right. \]

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

Returns
the rational

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.

Parameters
rthe number to be added
Returns
the sum as defined in the class

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.

Parameters
rthe number to be added
Returns
the sum as defined in the class

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.

Parameters
rthe number to be added
Returns
the sum as defined in the class

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.

Parameters
athe number to be multiplied
Returns
the product as defined in the class

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.

Parameters
athe number to be multiplied
Returns
the product as defined in the class

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.

References k, and q.

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

Member Data Documentation

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
Rational CVC3::TheoryArithNew::EpsRational::k
protected
const TheoryArithNew::EpsRational TheoryArithNew::EpsRational::PlusInfinity
static

The infinity constant

Definition at line 343 of file theory_arith_new.h.

Referenced by CVC3::TheoryArithNew::getUpperBound().

const TheoryArithNew::EpsRational TheoryArithNew::EpsRational::MinusInfinity
static

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().


The documentation for this class was generated from the following files: