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 35 of file theory_arith3.h.
|
inline |
Definition at line 40 of file theory_arith3.h.
|
inline |
Definition at line 41 of file theory_arith3.h.
|
inline |
Definition at line 42 of file theory_arith3.h.
References d_r.
Referenced by CVC3::TheoryArith3::isStale(), CVC3::operator<<(), and CVC3::TheoryArith3::updateSubsumptionDB().
|
inline |
Definition at line 43 of file theory_arith3.h.
References d_strict.
Referenced by CVC3::TheoryArith3::isStale(), CVC3::operator<<(), and CVC3::TheoryArith3::updateSubsumptionDB().
|
private |
Definition at line 37 of file theory_arith3.h.
Referenced by getConst().
|
private |
Definition at line 38 of file theory_arith3.h.
Referenced by strict().