CVC3
2.4.1
|
#include <rational.h>
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 () | |
Rational & | operator= (const Rational &n) |
std::string | toString (int base=10) const |
size_t | hash () const |
Rational | operator- () const |
Rational & | operator+= (const Rational &n2) |
Rational & | operator-= (const Rational &n2) |
Rational & | operator*= (const Rational &n2) |
Rational & | operator/= (const Rational &n2) |
const Rational & | operator++ () |
Prefix increment. | |
Rational | operator++ (int) |
Postfix increment. | |
const Rational & | operator-- () |
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) |
Definition at line 43 of file rational.h.
|
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 | ( | ) |
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 |
|
inline |
Prefix increment.
Definition at line 109 of file rational.h.
|
inline |
Postfix increment.
Definition at line 111 of file rational.h.
|
inline |
Prefix decrement.
Definition at line 113 of file rational.h.
|
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 |
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(), CVC3::TheoryArithOld::termDegree(), and LFSCObj::what_is_proven().
|
inline |
Definition at line 126 of file rational.h.
unsigned int CVC3::Rational::getUnsigned | ( | ) | const |
Unsigned CVC3::Rational::getUnsignedMP | ( | ) | const |
Referenced by CVC3::TheoryBitvector::finiteTypeInfo().
void CVC3::Rational::print | ( | ) | const |
|
friend |
Definition at line 44 of file rational.h.
|
friend |
|
friend |
Compute non-negative remainder for integer x,y.
nth root: return 0 if no exact answer (base should be nonzero)
|
private |
Definition at line 46 of file rational.h.