|
CVC3
|

Public Member Functions | |
| BoundInfo (const EpsRational &bound, const Theorem &thm) | |
| BoundInfo () | |
| bool | operator< (const BoundInfo &bI) const |
Public Attributes | |
| EpsRational | bound |
| Theorem | theorem |
The structure necessaty to hold the bounds.
Definition at line 535 of file theory_arith_new.h.
|
inline |
Constructor
Definition at line 542 of file theory_arith_new.h.
|
inline |
The empty constructor for the map
Definition at line 545 of file theory_arith_new.h.
|
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 bound, std::endl(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), CVC3::LE, and theorem.
| EpsRational CVC3::TheoryArithNew::BoundInfo::bound |
| Theorem CVC3::TheoryArithNew::BoundInfo::theorem |
The assertion theoreem of the bound
Definition at line 539 of file theory_arith_new.h.
Referenced by operator<().
1.8.2