CVC3
Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
CVC3::Rational Class Reference

#include <rational.h>

Collaboration diagram for CVC3::Rational:
Collaboration graph

Public Member Functions

 Rational ()
 
 Rational (const Rational &n)
 
 Rational (const Unsigned &n)
 
 Rational (int n, int d=1)
 
 Rational (const char *n, int base=10)
 
 Rational (const std::string &n, int base=10)
 
 Rational (const char *n, const char *d, int base=10)
 
 Rational (const std::string &n, const std::string &d, int base=10)
 
 ~Rational ()
 
Rationaloperator= (const Rational &n)
 
std::string toString (int base=10) const
 
size_t hash () const
 
Rational operator- () const
 
Rationaloperator+= (const Rational &n2)
 
Rationaloperator-= (const Rational &n2)
 
Rationaloperator*= (const Rational &n2)
 
Rationaloperator/= (const Rational &n2)
 
const Rationaloperator++ ()
 Prefix increment.
 
Rational operator++ (int)
 Postfix increment.
 
const Rationaloperator-- ()
 Prefix decrement.
 
Rational operator-- (int)
 Postfix decrement.
 
Rational getNumerator () const
 
Rational getDenominator () const
 
bool isInteger () const
 
int getInt () const
 
bool isUnsigned () const
 
unsigned int getUnsigned () const
 
Unsigned getUnsignedMP () const
 
void print () const
 

Private Member Functions

 Rational (const Impl &t)
 

Private Attributes

Impl * d_n
 

Friends

class Unsigned
 
CVC_DLL bool operator== (const Rational &n1, const Rational &n2)
 
CVC_DLL bool operator< (const Rational &n1, const Rational &n2)
 
CVC_DLL bool operator<= (const Rational &n1, const Rational &n2)
 
CVC_DLL bool operator> (const Rational &n1, const Rational &n2)
 
CVC_DLL bool operator>= (const Rational &n1, const Rational &n2)
 
CVC_DLL bool operator!= (const Rational &n1, const Rational &n2)
 
CVC_DLL Rational operator+ (const Rational &n1, const Rational &n2)
 
CVC_DLL Rational operator- (const Rational &n1, const Rational &n2)
 
CVC_DLL Rational operator* (const Rational &n1, const Rational &n2)
 
CVC_DLL Rational operator/ (const Rational &n1, const Rational &n2)
 
CVC_DLL Rational operator% (const Rational &n1, const Rational &n2)
 
std::ostream & operator<< (std::ostream &os, const Rational &n)
 
std::ostream & operator<< (std::ostream &os, const Impl &n)
 
CVC_DLL Rational gcd (const Rational &x, const Rational &y)
 
CVC_DLL Rational gcd (const std::vector< Rational > &v)
 
CVC_DLL Rational lcm (const Rational &x, const Rational &y)
 
CVC_DLL Rational lcm (const std::vector< Rational > &v)
 
CVC_DLL Rational abs (const Rational &x)
 
CVC_DLL Rational floor (const Rational &x)
 Compute the floor of x (result is an integer)
 
CVC_DLL Rational ceil (const Rational &x)
 Compute the ceiling of x (result is an integer)
 
CVC_DLL Rational mod (const Rational &x, const Rational &y)
 Compute non-negative remainder for integer x,y.
 
CVC_DLL Rational intRoot (const Rational &base, unsigned long int n)
 nth root: return 0 if no exact answer (base should be nonzero)
 

Detailed Description

Definition at line 43 of file rational.h.

Constructor & Destructor Documentation

CVC3::Rational::Rational ( const Impl &  t)
private
CVC3::Rational::Rational ( )
CVC3::Rational::Rational ( const Rational n)
CVC3::Rational::Rational ( const Unsigned n)
CVC3::Rational::Rational ( int  n,
int  d = 1 
)
CVC3::Rational::Rational ( const char *  n,
int  base = 10 
)
CVC3::Rational::Rational ( const std::string &  n,
int  base = 10 
)
CVC3::Rational::Rational ( const char *  n,
const char *  d,
int  base = 10 
)
CVC3::Rational::Rational ( const std::string &  n,
const std::string &  d,
int  base = 10 
)
CVC3::Rational::~Rational ( )

Member Function Documentation

Rational& CVC3::Rational::operator= ( const Rational n)
std::string CVC3::Rational::toString ( int  base = 10) const

Referenced by CVC3::BitvectorTheoremProducer::bvplusConst(), CVC3::ArithTheoremProducerOld::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducer3::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducer3::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::ArithTheoremProducer3::create_t3(), CVC3::TheoryArithOld::currentMaxCoefficient(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::ArithTheoremProducerOld::f(), CVC3::ArithTheoremProducer3::f(), CVC3::ArithTheoremProducer::f(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithOld::getLowerBound(), CVC3::TheoryArithOld::getUpperBound(), CVC3::ExprRational::hash(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArithTheoremProducerOld::modEq(), CVC3::ArithTheoremProducer::modEq(), CVC3::ArithTheoremProducer3::modEq(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducer3::monomialModM(), CVC3::ArithTheoremProducerOld::monomialMulF(), CVC3::ArithTheoremProducer3::monomialMulF(), CVC3::ArithTheoremProducer::monomialMulF(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::pow(), CVC3::TheoryArith::printRational(), CVC3::TheoryArithOld::registerAtom(), CVC3::ArithTheoremProducerOld::sumModM(), CVC3::ArithTheoremProducer::sumModM(), CVC3::ArithTheoremProducer3::sumModM(), CVC3::ArithTheoremProducerOld::sumMulF(), CVC3::ArithTheoremProducer3::sumMulF(), CVC3::ArithTheoremProducer::sumMulF(), CVC3::TheoryArithNew::EpsRational::toString(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString(), CVC3::TheoryArithNew::updateStats(), CVC3::TheoryArith3::updateStats(), and CVC3::TheoryArithOld::updateStats().

size_t CVC3::Rational::hash ( ) const
Rational CVC3::Rational::operator- ( ) const
Rational& CVC3::Rational::operator+= ( const Rational n2)
Rational& CVC3::Rational::operator-= ( const Rational n2)
Rational& CVC3::Rational::operator*= ( const Rational n2)
Rational& CVC3::Rational::operator/= ( const Rational n2)
const Rational& CVC3::Rational::operator++ ( )
inline

Prefix increment.

Definition at line 109 of file rational.h.

Rational CVC3::Rational::operator++ ( int  )
inline

Postfix increment.

Definition at line 111 of file rational.h.

const Rational& CVC3::Rational::operator-- ( )
inline

Prefix decrement.

Definition at line 113 of file rational.h.

Rational CVC3::Rational::operator-- ( int  )
inline

Postfix decrement.

Definition at line 115 of file rational.h.

Rational CVC3::Rational::getNumerator ( ) const
Rational CVC3::Rational::getDenominator ( ) const
bool CVC3::Rational::isInteger ( ) const

Referenced by CVC3::TheoryArithNew::assignVariables(), CVC3::TheoryArith3::assignVariables(), CVC3::TheoryArithOld::assignVariables(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer3::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryArith3::computeType(), CVC3::TheoryArithOld::computeType(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducer3::constRHSGrayShadow(), CVC3::ArithTheoremProducerOld::constRHSGrayShadow(), CVC3::ArithTheoremProducer::constRHSGrayShadow(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowRewrite(), CVC3::TheoryArithNew::EpsRational::getFloor(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getFloor(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::TheoryArithNew::EpsRational::isInteger(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::isInteger(), CVC3::isIntegerConst(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryRecords::parseExprOp(), CVC3::TheoryBitvector::parseExprOp(), CVC3::pow(), CVC3::Translator::preprocessRec(), CVC3::TheoryBitvector::print(), CVC3::TheoryArithOld::print(), CVC3::TheoryArith::printRational(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::ArithTheoremProducer3::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), CVC3::ArithTheoremProducer3::splitGrayShadow(), CVC3::ArithTheoremProducer::splitGrayShadow(), and CVC3::ArithTheoremProducerOld::splitGrayShadowSmall().

int CVC3::Rational::getInt ( ) const
bool CVC3::Rational::isUnsigned ( ) const
inline

Definition at line 126 of file rational.h.

unsigned int CVC3::Rational::getUnsigned ( ) const
Unsigned CVC3::Rational::getUnsignedMP ( ) const
void CVC3::Rational::print ( ) const

Friends And Related Function Documentation

friend class Unsigned
friend

Definition at line 44 of file rational.h.

CVC_DLL bool operator== ( const Rational n1,
const Rational n2 
)
friend
CVC_DLL bool operator< ( const Rational n1,
const Rational n2 
)
friend
CVC_DLL bool operator<= ( const Rational n1,
const Rational n2 
)
friend
CVC_DLL bool operator> ( const Rational n1,
const Rational n2 
)
friend
CVC_DLL bool operator>= ( const Rational n1,
const Rational n2 
)
friend
CVC_DLL bool operator!= ( const Rational n1,
const Rational n2 
)
friend
CVC_DLL Rational operator+ ( const Rational n1,
const Rational n2 
)
friend
CVC_DLL Rational operator- ( const Rational n1,
const Rational n2 
)
friend
CVC_DLL Rational operator* ( const Rational n1,
const Rational n2 
)
friend
CVC_DLL Rational operator/ ( const Rational n1,
const Rational n2 
)
friend
CVC_DLL Rational operator% ( const Rational n1,
const Rational n2 
)
friend
std::ostream& operator<< ( std::ostream &  os,
const Rational n 
)
friend
std::ostream& operator<< ( std::ostream &  os,
const Impl &  n 
)
friend
CVC_DLL Rational gcd ( const Rational x,
const Rational y 
)
friend
CVC_DLL Rational gcd ( const std::vector< Rational > &  v)
friend
CVC_DLL Rational lcm ( const Rational x,
const Rational y 
)
friend
CVC_DLL Rational lcm ( const std::vector< Rational > &  v)
friend
CVC_DLL Rational abs ( const Rational x)
friend
CVC_DLL Rational floor ( const Rational x)
friend

Compute the floor of x (result is an integer)

CVC_DLL Rational ceil ( const Rational x)
friend

Compute the ceiling of x (result is an integer)

CVC_DLL Rational mod ( const Rational x,
const Rational y 
)
friend

Compute non-negative remainder for integer x,y.

CVC_DLL Rational intRoot ( const Rational base,
unsigned long int  n 
)
friend

nth root: return 0 if no exact answer (base should be nonzero)

Member Data Documentation

Impl* CVC3::Rational::d_n
private

Definition at line 46 of file rational.h.


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