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 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

Rational& CVC3::Rational::operator= ( const Rational n  ) 

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

Referenced by 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::ArithTheoremProducer3::elimPowerConst(), CVC3::ArithTheoremProducer::elimPowerConst(), 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::ArithTheoremProducer3::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer3::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer3::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArithTheoremProducer3::intEqIrrational(), CVC3::ArithTheoremProducer::intEqIrrational(), 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 105 of file rational.h.

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

Postfix increment.

Definition at line 107 of file rational.h.

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

Prefix decrement.

Definition at line 109 of file rational.h.

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

Postfix decrement.

Definition at line 111 of file rational.h.

Rational CVC3::Rational::getNumerator (  )  const

Referenced by CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArith3::computeNormalFactor(), CVC3::TheoryArith::printRational(), and CVC3::ratRoot().

Rational CVC3::Rational::getDenominator (  )  const

Referenced by CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArith3::computeNormalFactor(), CVC3::TheoryArith::printRational(), and CVC3::ratRoot().

bool CVC3::Rational::isInteger (  )  const

Referenced by CVC3::TheoryArithOld::assignVariables(), CVC3::TheoryArithNew::assignVariables(), CVC3::TheoryArith3::assignVariables(), 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::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer3::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::TheoryArithOld::DifferenceLogicGraph::EpsRational::isInteger(), CVC3::TheoryArithNew::EpsRational::isInteger(), CVC3::isIntegerConst(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::pow(), CVC3::Translator::preprocessRec(), CVC3::TheoryBitvector::print(), CVC3::TheoryArith::printRational(), CVC3::TheoryArithNew::rafineIntegerConstraints(), 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(), and CVC3::ArithTheoremProducerOld::splitGrayShadowSmall().

bool CVC3::Rational::isUnsigned (  )  const [inline]

Definition at line 122 of file rational.h.

unsigned int CVC3::Rational::getUnsigned (  )  const

Referenced by CVC3::TheoryArith3::doSolve(), CVC3::TheoryBitvector::finiteTypeInfo(), CVC3::TheoryArithOld::finiteTypeInfo(), CVC3::TheoryArithNew::finiteTypeInfo(), CVC3::TheoryArith3::finiteTypeInfo(), and CVC3::TheoryArithOld::rewrite().

void CVC3::Rational::print (  )  const


Friends And Related Function Documentation

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]

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 43 of file rational.h.


The documentation for this class was generated from the following file:
Generated on Wed Nov 18 16:15:37 2009 for CVC3 by  doxygen 1.5.2