CVC3
|
Data class for the strongest free constant in separation inqualities. More...
Public Member Functions | |
FreeConst () | |
FreeConst (const Rational &r, bool strict) | |
const Rational & | getConst () const |
bool | strict () const |
Private Attributes | |
Rational | d_r |
bool | d_strict |
Data class for the strongest free constant in separation inqualities.
Definition at line 38 of file theory_arith_old.h.
|
inline |
Definition at line 43 of file theory_arith_old.h.
|
inline |
Definition at line 44 of file theory_arith_old.h.
|
inline |
Definition at line 45 of file theory_arith_old.h.
References d_r.
Referenced by CVC3::TheoryArithOld::isStale(), CVC3::operator<<(), and CVC3::TheoryArithOld::updateSubsumptionDB().
|
inline |
Definition at line 46 of file theory_arith_old.h.
References d_strict.
Referenced by CVC3::TheoryArithOld::isStale(), CVC3::operator<<(), and CVC3::TheoryArithOld::updateSubsumptionDB().
|
private |
Definition at line 40 of file theory_arith_old.h.
Referenced by getConst().
|
private |
Definition at line 41 of file theory_arith_old.h.
Referenced by strict().