#include <rational.h>
List of all members.
Public Member Functions
Private Member Functions
Private Attributes
Friends
- 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)
- 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 41 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 |
( |
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
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 |
const Rational& CVC3::Rational::operator++ |
( |
|
) |
[inline] |
Rational CVC3::Rational::operator++ |
( |
int |
|
) |
[inline] |
const Rational& CVC3::Rational::operator-- |
( |
|
) |
[inline] |
Rational CVC3::Rational::operator-- |
( |
int |
|
) |
[inline] |
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::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 |
Referenced by CVC3::BitvectorTheoremProducer::bvashrToConcat(), CVC3::BitvectorTheoremProducer::bvlshrToConcat(), CVC3::BitvectorTheoremProducer::bvshlToConcat(), CVC3::ArithTheoremProducerOld::compactNonLinearTerm(), CVC3::SimulateTheoremProducer::expandSimulate(), CVC3::TheoryBitvector::getBitvectorTypeParam(), CVC3::TheoryBitvector::getBoolExtractIndex(), CVC3::TheoryBitvector::getBVIndex(), CVC3::TheoryBitvector::getBVMultParam(), CVC3::TheoryBitvector::getBVPlusParam(), CVC3::TheoryBitvector::getExtractHi(), CVC3::TheoryBitvector::getExtractLow(), CVC3::TheoryBitvector::getFixedLeftShiftParam(), CVC3::TheoryBitvector::getFixedRightShiftParam(), CVC3::TheoryRecords::getIndex(), CVC3::TheoryBitvector::getSXIndex(), CVC3::TheoryBitvector::parseExprOp(), CVC3::TheoryArithOld::print(), CVC3::ArithTheoremProducerOld::splitGrayShadowSmall(), and CVC3::TheoryArithOld::termDegree().
bool CVC3::Rational::isUnsigned |
( |
|
) |
const [inline] |
unsigned int CVC3::Rational::getUnsigned |
( |
|
) |
const |
void CVC3::Rational::print |
( |
|
) |
const |
Friends And Related Function Documentation
std::ostream& operator<< |
( |
std::ostream & |
os, |
|
|
const Rational & |
n | |
|
) |
| | [friend] |
Compute the floor of x (result is an integer).
Compute the ceiling of x (result is an integer).
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
The documentation for this class was generated from the following file: