CVC3
Public Member Functions | Private Member Functions | Private Attributes | Friends

CVC3::Rational Class Reference

#include <rational.h>

List of all members.

Public Member Functions

Private Member Functions

Private Attributes

Friends


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::ArithTheoremProducer3::create_t(), CVC3::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer3::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer3::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::TheoryArithOld::currentMaxCoefficient(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::TheoryArithOld::extractTermsFromInequality(), CVC3::ArithTheoremProducerOld::f(), CVC3::ArithTheoremProducer3::f(), CVC3::ArithTheoremProducer::f(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::TheoryArith3::findBounds(), CVC3::TheoryArithOld::getLowerBound(), CVC3::TheoryArithOld::getUpperBound(), CVC3::ExprRational::hash(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArithTheoremProducerOld::modEq(), CVC3::ArithTheoremProducer3::modEq(), CVC3::ArithTheoremProducer::modEq(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer3::monomialModM(), CVC3::ArithTheoremProducer::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::ArithTheoremProducer3::sumModM(), CVC3::ArithTheoremProducer::sumModM(), CVC3::ArithTheoremProducerOld::sumMulF(), CVC3::ArithTheoremProducer3::sumMulF(), CVC3::ArithTheoremProducer::sumMulF(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::toString(), CVC3::TheoryArithNew::EpsRational::toString(), CVC3::TheoryArithOld::updateStats(), CVC3::TheoryArithNew::updateStats(), and CVC3::TheoryArith3::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::TheoryArithOld::assignVariables(), CVC3::TheoryArithNew::assignVariables(), CVC3::TheoryArith3::assignVariables(), CVC3::ArithTheoremProducerOld::canonPowConst(), CVC3::ArithTheoremProducer3::canonPowConst(), CVC3::ArithTheoremProducer::canonPowConst(), CVC3::TheoryArithOld::checkIntegerEquality(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::TheoryArith3::computeType(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constRHSGrayShadow(), CVC3::ArithTheoremProducer3::constRHSGrayShadow(), CVC3::ArithTheoremProducer::constRHSGrayShadow(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer3::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer3::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer3::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::ArithTheoremProducerOld::expandGrayShadowRewrite(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::getFloor(), CVC3::TheoryArithNew::EpsRational::getFloor(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer3::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArithTheoremProducerOld::intVarEqnConst(), CVC3::ArithTheoremProducer3::intVarEqnConst(), CVC3::ArithTheoremProducer::intVarEqnConst(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::isInteger(), CVC3::TheoryArithNew::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::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer3::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: