CVC3::Rational Class Reference

#include <rational.h>

List of all members.

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)
  

---

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

Referenced by CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArithNew::computeNormalFactor(), CVC3::TheoryArith3::computeNormalFactor(), CVC3::Translator::preprocessRec(), CVC3::TheoryArith::printRational(), CVC3::ratRoot(), and LFSCObj::what_is_proven().

Rational CVC3::Rational::getDenominator

(

)

const

Referenced by CVC3::TheoryArithOld::computeNormalFactor(), CVC3::TheoryArithNew::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::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

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().

bool CVC3::Rational::isUnsigned

(

)

const [inline]

Definition at line 126 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().

Unsigned CVC3::Rational::getUnsignedMP

(

)

const

Referenced by CVC3::TheoryBitvector::finiteTypeInfo().

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:

• rational.h