CVC3::TheoryArithNew::TheoryArithNew::EpsRational Class Reference

#include <theory_arith_new.h>

Collaboration diagram for CVC3::TheoryArithNew::TheoryArithNew::EpsRational:

[legend]

List of all members.

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
EpsRational & operator+= (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

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

$(q_1, k_1) + (q_2, k_2) \equiv (q_1 + q_2, k_1 + k_2)$
$a \times (q, k) \equiv (a \times q, a \times k)$
$(q_1, k_1) \leq (q_2, k_2) \equiv (q_1 < q_2) \vee (q_1 = q_2 \wedge k_1 \leq k_2)$

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

enum CVC3::TheoryArithNew::EpsRational::RationalType [protected]

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::TheoryArithNew::EpsRational::EpsRational ( RationalType type ) [inline, protected]

Private constructor to construt infinities.

Definition at line 296 of file theory_arith_new.h.

CVC3::TheoryArithNew::TheoryArithNew::EpsRational::EpsRational ( ) [inline]

The blank constructor

Definition at line 351 of file theory_arith_new.h.

Referenced by CVC3::TheoryArithNew::TheoryArithNew::EpsRational::operator*(), CVC3::TheoryArithNew::TheoryArithNew::EpsRational::operator+(), CVC3::TheoryArithNew::TheoryArithNew::EpsRational::operator-(), and CVC3::TheoryArithNew::TheoryArithNew::EpsRational::operator/().

CVC3::TheoryArithNew::TheoryArithNew::EpsRational::EpsRational ( const EpsRational & r ) [inline]

Copy constructor

Definition at line 354 of file theory_arith_new.h.

CVC3::TheoryArithNew::TheoryArithNew::EpsRational::EpsRational ( const Rational q ) [inline]

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

Parameters:

q

the rational

Definition at line 361 of file theory_arith_new.h.

CVC3::TheoryArithNew::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:

	q	the rational
	k	the epsilon multiplier

Definition at line 370 of file theory_arith_new.h.

Member Function Documentation

bool CVC3::TheoryArithNew::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 CVC3::TheoryArithNew::TheoryArithNew::EpsRational::k.

bool CVC3::TheoryArithNew::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(), CVC3::TheoryArithNew::TheoryArithNew::EpsRational::k, and CVC3::TheoryArithNew::TheoryArithNew::EpsRational::q.

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

Rational CVC3::TheoryArithNew::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.$