CVC3
|
Public Member Functions | |
ExprBoundInfo (const EpsRational &bound, const Expr &e) | |
ExprBoundInfo () | |
bool | operator< (const ExprBoundInfo &bI) const |
Public Attributes | |
EpsRational | bound |
Expr | e |
The structure necessaty to hold the bounds on expressions (for theory propagation).
Definition at line 574 of file theory_arith_new.h.
|
inline |
Constructor
Definition at line 581 of file theory_arith_new.h.
|
inline |
The empty constructor for the map
Definition at line 584 of file theory_arith_new.h.
|
inline |
The comparator, just if we need it. Compares first by expressions then by bounds
Definition at line 589 of file theory_arith_new.h.
References bound, e, CVC3::Expr::getKind(), and CVC3::LE.
EpsRational CVC3::TheoryArithNew::ExprBoundInfo::bound |
Expr CVC3::TheoryArithNew::ExprBoundInfo::e |
The assertion theoreem of the bound
Definition at line 578 of file theory_arith_new.h.
Referenced by operator<().