CVC3::Rational Class Reference

#include <rational.h>

List of all members.

Public Member Functions

• Rational ()
• Rational (const Rational &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
• void print () const

Private Member Functions

• Rational (const Impl &t)

Private Attributes

• Impl * d_n

Friends

• bool operator== (const Rational &n1, const Rational &n2)
• bool operator< (const Rational &n1, const Rational &n2)
• bool operator<= (const Rational &n1, const Rational &n2)
• bool operator> (const Rational &n1, const Rational &n2)
• bool operator>= (const Rational &n1, const Rational &n2)
• bool operator!= (const Rational &n1, const Rational &n2)
• Rational operator+ (const Rational &n1, const Rational &n2)
• Rational operator- (const Rational &n1, const Rational &n2)
• Rational operator * (const Rational &n1, const Rational &n2)
• Rational operator/ (const Rational &n1, const Rational &n2)
• Rational operator% (const Rational &n1, const Rational &n2)
• std::ostream & operator<< (std::ostream &os, const Rational &n)
• Rational gcd (const Rational &x, const Rational &y)
• Rational gcd (const std::vector< Rational > &v)
• Rational lcm (const Rational &x, const Rational &y)
• Rational lcm (const std::vector< Rational > &v)
• Rational abs (const Rational &x)
• Rational floor (const Rational &x)

  Compute the floor of x (result is an integer).
  

• Rational ceil (const Rational &x)

  Compute the ceiling of x (result is an integer).
  

• Rational mod (const Rational &x, const Rational &y)

  Compute non-negative remainder for *integer* x,y.
  

---

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::ArithTheoremProducer::create_t(), CVC3::ArithTheoremProducerOld::create_t2(), CVC3::ArithTheoremProducer::create_t2(), CVC3::ArithTheoremProducerOld::create_t3(), CVC3::ArithTheoremProducer::create_t3(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::f(), CVC3::ArithTheoremProducer::f(), CVC3::TheoryArithOld::findBounds(), CVC3::TheoryArithNew::findBounds(), CVC3::ExprRational::hash(), CVC3::ArithTheoremProducerOld::implyNegatedInequality(), CVC3::ArithTheoremProducer::implyNegatedInequality(), CVC3::ArithTheoremProducerOld::implyWeakerInequality(), CVC3::ArithTheoremProducer::implyWeakerInequality(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArithTheoremProducerOld::modEq(), CVC3::ArithTheoremProducer::modEq(), CVC3::ArithTheoremProducerOld::monomialModM(), CVC3::ArithTheoremProducer::monomialModM(), CVC3::ArithTheoremProducerOld::monomialMulF(), CVC3::ArithTheoremProducer::monomialMulF(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::TheoryBitvector::normalizeBVArith(), CVC3::pow(), CVC3::TheoryArith::printRational(), CVC3::ArithTheoremProducerOld::sumModM(), CVC3::ArithTheoremProducer::sumModM(), CVC3::ArithTheoremProducerOld::sumMulF(), CVC3::ArithTheoremProducer::sumMulF(), CVC3::TheoryArithNew::EpsRational::toString(), CVC3::TheoryArithOld::updateStats(), and CVC3::TheoryArithNew::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(), and CVC3::TheoryArith::printRational().

Rational CVC3::Rational::getDenominator

(

)

const

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

bool CVC3::Rational::isInteger

(

)

const

Referenced by CVC3::TheoryArithOld::assignVariables(), CVC3::TheoryArithNew::assignVariables(), CVC3::TheoryArithOld::computeType(), CVC3::TheoryArithNew::computeType(), CVC3::BitvectorTheoremProducer::constMultToPlus(), CVC3::ArithTheoremProducerOld::constRHSGrayShadow(), CVC3::ArithTheoremProducer::constRHSGrayShadow(), CVC3::ArithTheoremProducerOld::eqElimIntRule(), CVC3::ArithTheoremProducer::eqElimIntRule(), CVC3::ArithTheoremProducerOld::expandGrayShadow(), CVC3::ArithTheoremProducer::expandGrayShadow(), CVC3::ArithTheoremProducerOld::expandGrayShadowConst(), CVC3::ArithTheoremProducer::expandGrayShadowConst(), CVC3::TheoryArithNew::EpsRational::getFloor(), CVC3::ArithTheoremProducerOld::grayShadowConst(), CVC3::ArithTheoremProducer::grayShadowConst(), CVC3::ArithTheoremProducerOld::integerSplit(), CVC3::ArithTheoremProducer::integerSplit(), CVC3::ArithTheoremProducerOld::isIntConst(), CVC3::ArithTheoremProducer::isIntConst(), CVC3::TheoryArithNew::EpsRational::isInteger(), CVC3::isIntegerConst(), CVC3::TheoryBitvector::newBVConstExpr(), CVC3::pow(), CVC3::TheoryBitvector::print(), CVC3::TheoryArith::printRational(), CVC3::TheoryArithNew::rafineIntegerConstraints(), CVC3::ArithTheoremProducerOld::rafineStrictInteger(), CVC3::ArithTheoremProducer::rafineStrictInteger(), CVC3::ArithTheoremProducerOld::splitGrayShadow(), and CVC3::ArithTheoremProducer::splitGrayShadow().

int CVC3::Rational::getInt

(

)

const

Referenced by 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(), and CVC3::TheoryBitvector::parseExprOp().

bool CVC3::Rational::isUnsigned

(

)

const [inline]

Definition at line 122 of file rational.h.

unsigned int CVC3::Rational::getUnsigned

(

)

const

void CVC3::Rational::print

(

)

const

---

Friends And Related Function Documentation

bool operator==	(	const Rational &	n1,
		const Rational &	n2
	)			[friend]

bool operator<	(	const Rational &	n1,
		const Rational &	n2
	)			[friend]

bool operator<=	(	const Rational &	n1,
		const Rational &	n2
	)			[friend]

bool operator>	(	const Rational &	n1,
		const Rational &	n2
	)			[friend]

bool operator>=	(	const Rational &	n1,
		const Rational &	n2
	)			[friend]

bool operator!=	(	const Rational &	n1,
		const Rational &	n2
	)			[friend]

Rational operator+	(	const Rational &	n1,
		const Rational &	n2
	)			[friend]

Rational operator-	(	const Rational &	n1,
		const Rational &	n2
	)			[friend]

Rational operator *	(	const Rational &	n1,
		const Rational &	n2
	)			[friend]

Rational operator/	(	const Rational &	n1,
		const Rational &	n2
	)			[friend]

Rational operator%	(	const Rational &	n1,
		const Rational &	n2
	)			[friend]

std::ostream& operator<<	(	std::ostream &	os,
		const Rational &	n
	)			[friend]

Rational gcd	(	const Rational &	x,
		const Rational &	y
	)			[friend]

Rational gcd

(

const std::vector< Rational > &

v

)

[friend]

Rational lcm	(	const Rational &	x,
		const Rational &	y
	)			[friend]

Rational lcm

(

const std::vector< Rational > &

v

)

[friend]

Rational abs

(

const Rational &

x

)

[friend]

Rational floor

(

const Rational &

x

)

[friend]

Compute the floor of x (result is an integer).

Rational ceil

(

const Rational &

x

)

[friend]

Compute the ceiling of x (result is an integer).

Rational mod	(	const Rational &	x,
		const Rational &	y
	)			[friend]

Compute non-negative remainder for *integer* x,y.

---

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:

• rational.h

---