CVC3::TheoryArithNew::TheoryArithNew::BoundInfo Struct Reference

Collaboration diagram for CVC3::TheoryArithNew::TheoryArithNew::BoundInfo:

[legend]

List of all members.

Public Member Functions

• BoundInfo (const EpsRational &bound, const Theorem &thm)
• BoundInfo ()
• bool operator< (const BoundInfo &bI) const

Public Attributes

• EpsRational bound
• Theorem theorem

---

Detailed Description

The structure necessaty to hold the bounds.

Definition at line 535 of file theory_arith_new.h.

---

Constructor & Destructor Documentation

CVC3::TheoryArithNew::TheoryArithNew::BoundInfo::BoundInfo	(	const EpsRational &	bound,
		const Theorem &	thm
	)			[inline]

Constructor

Definition at line 542 of file theory_arith_new.h.

CVC3::TheoryArithNew::TheoryArithNew::BoundInfo::BoundInfo

(

)

[inline]

The empty constructor for the map

Definition at line 545 of file theory_arith_new.h.

---

Member Function Documentation

bool CVC3::TheoryArithNew::TheoryArithNew::BoundInfo::operator<

(

const BoundInfo &

bI

)

const [inline]

The comparator, just if we need it. Compares first by expressions then by bounds

Definition at line 550 of file theory_arith_new.h.

References CVC3::TheoryArithNew::TheoryArithNew::BoundInfo::bound, std::endl(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), CVC3::LE, and CVC3::TheoryArithNew::TheoryArithNew::BoundInfo::theorem.

---

Member Data Documentation

EpsRational CVC3::TheoryArithNew::TheoryArithNew::BoundInfo::bound

The bound itself

Definition at line 537 of file theory_arith_new.h.

Referenced by CVC3::TheoryArithNew::TheoryArithNew::BoundInfo::operator<().

Theorem CVC3::TheoryArithNew::TheoryArithNew::BoundInfo::theorem

The assertion theoreem of the bound

Definition at line 539 of file theory_arith_new.h.

Referenced by CVC3::TheoryArithNew::TheoryArithNew::BoundInfo::operator<().

---

The documentation for this struct was generated from the following file:

• theory_arith_new.h