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