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