CVC3::TheoryArithNew::BoundInfo Struct Reference

Collaboration diagram for CVC3::TheoryArithNew::BoundInfo:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Public Attributes


Detailed Description

The structure necessaty to hold the bounds.

Definition at line 533 of file theory_arith_new.h.


Constructor & Destructor Documentation

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

Constructor

Definition at line 540 of file theory_arith_new.h.

CVC3::TheoryArithNew::BoundInfo::BoundInfo (  )  [inline]

The empty constructor for the map

Definition at line 543 of file theory_arith_new.h.

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

Constructor

Definition at line 544 of file theory_arith_new.mine.h.

CVC3::TheoryArithNew::BoundInfo::BoundInfo (  )  [inline]

The empty constructor for the map

Definition at line 547 of file theory_arith_new.mine.h.


Member Function Documentation

bool CVC3::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 548 of file theory_arith_new.h.

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

bool CVC3::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 552 of file theory_arith_new.mine.h.

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


Member Data Documentation

EpsRational CVC3::TheoryArithNew::BoundInfo::bound

The bound itself

Definition at line 535 of file theory_arith_new.h.

Referenced by operator<().

Theorem CVC3::TheoryArithNew::BoundInfo::theorem

The assertion theoreem of the bound

Definition at line 537 of file theory_arith_new.h.

Referenced by operator<().


The documentation for this struct was generated from the following files:
Generated on Tue Jul 3 14:38:16 2007 for CVC3 by  doxygen 1.5.1