CVC3  2.4.1
Public Member Functions | Static Public Attributes | Protected Types | Protected Member Functions | Protected Attributes
CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational Class Reference

#include <theory_arith_old.h>

List of all members.

Public Member Functions

Static Public Attributes

Protected Types

Protected Member Functions

Protected Attributes


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.


Member Enumeration Documentation

Type of rationals, normal and the two infinities

Enumerator:
FINITE 
PLUS_INFINITY 
MINUS_INFINITY 

Definition at line 478 of file theory_arith_old.h.


Constructor & Destructor Documentation

CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::EpsRational ( RationalType  type) [inline, protected]

Private constructor to construt infinities.

Definition at line 492 of file theory_arith_old.h.

CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::EpsRational ( ) [inline]

The blank constructor

Definition at line 559 of file theory_arith_old.h.

Referenced by operator+(), operator-(), operator*(), and operator/().

CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::EpsRational ( const EpsRational r) [inline]

Copy constructor

Definition at line 562 of file theory_arith_old.h.

CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::EpsRational ( const Rational q) [inline]

Constructor from a rational, constructs a new pair (q, 0).

Parameters:
qthe rational

Definition at line 569 of file theory_arith_old.h.

CVC3::TheoryArithOld::DifferenceLogicGraph::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 578 of file theory_arith_old.h.


Member Function Documentation

bool CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::isFinite ( ) const [inline]
bool CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::isRational ( ) const [inline]

Returns if the number is a plain rational.

Returns:
true if rational, false otherwise

Definition at line 506 of file theory_arith_old.h.

References k.

bool CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::isInteger ( ) const [inline]

Returns if the number is a plain integer.

Returns:
true if rational, false otherwise

Definition at line 513 of file theory_arith_old.h.

References k, q, and CVC3::Rational::isInteger().

Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::tryUpdate().

Rational CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getFloor ( ) const [inline]

Returns the floor of the number $x = q + k \epsilon$ using the following fomula

\[ \lfloor \beta(x) \rfloor = \begin{cases} \lfloor q \rfloor & \text{ if } q \notin Z\\ q & \text{ if } q \in Z \text{ and } k \geq 0\\ q - 1 & \text{ if } q \in Z \text{ and } k < 0 \end{cases} \]

Definition at line 526 of file theory_arith_old.h.

References q, CVC3::Rational::isInteger(), and k.

Rational CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getRational ( ) const [inline]

Returns the rational part of the number

Returns:
the rational

Definition at line 541 of file theory_arith_old.h.

References q.

Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::tryUpdate(), and CVC3::TheoryArithOld::DifferenceLogicGraph::getValuation().

Rational CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getEpsilon ( ) const [inline]

Returns the epsilon part of the number

Returns:
the epsilon

Definition at line 548 of file theory_arith_old.h.

References k.

Referenced by CVC3::TheoryArithOld::DifferenceLogicGraph::addEdge(), CVC3::TheoryArithOld::DifferenceLogicGraph::tryUpdate(), and CVC3::TheoryArithOld::DifferenceLogicGraph::getValuation().

EpsRational CVC3::TheoryArithOld::DifferenceLogicGraph::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 586 of file theory_arith_old.h.

References DebugAssert, type, FINITE, EpsRational(), q, and k.

EpsRational& CVC3::TheoryArithOld::DifferenceLogicGraph::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 598 of file theory_arith_old.h.

References DebugAssert, type, FINITE, q, and k.

EpsRational CVC3::TheoryArithOld::DifferenceLogicGraph::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 611 of file theory_arith_old.h.

References DebugAssert, type, FINITE, EpsRational(), q, and k.

EpsRational CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::operator- ( ) [inline]

Unary minus operator

Definition at line 620 of file theory_arith_old.h.

References DebugAssert, type, FINITE, q, and k.

EpsRational CVC3::TheoryArithOld::DifferenceLogicGraph::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 634 of file theory_arith_old.h.

References DebugAssert, type, FINITE, EpsRational(), q, and k.

EpsRational CVC3::TheoryArithOld::DifferenceLogicGraph::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 645 of file theory_arith_old.h.

References DebugAssert, type, FINITE, EpsRational(), q, and k.

bool CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::operator== ( const EpsRational r) const [inline]

Equality comparison operator.

Definition at line 653 of file theory_arith_old.h.

References q, and k.

bool CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::operator<= ( const EpsRational r) const [inline]

Less than or equal comparison operator.

Definition at line 658 of file theory_arith_old.h.

References FINITE, type, q, k, MINUS_INFINITY, PLUS_INFINITY, and FatalAssert.

bool CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::operator< ( const EpsRational r) const [inline]

Less than comparison operator.

Definition at line 683 of file theory_arith_old.h.

bool CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::operator> ( const EpsRational r) const [inline]

Greater than comparison operator.

Definition at line 688 of file theory_arith_old.h.

std::string CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString ( ) const [inline]

Member Data Documentation

The type of this rational

Definition at line 481 of file theory_arith_old.h.

Referenced by isFinite(), operator+(), operator+=(), operator-(), operator*(), operator/(), operator<=(), and toString().

The infinity constant

Definition at line 551 of file theory_arith_old.h.

The negative infinity constant

Definition at line 553 of file theory_arith_old.h.

The zero constant

Definition at line 555 of file theory_arith_old.h.


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