Data class for the strongest free constant in separation inqualities. More...
Data class for the strongest free constant in separation inqualities.
Definition at line 32 of file theory_arith3.h.
CVC3::TheoryArith3::FreeConst::FreeConst | ( | ) | [inline] |
Definition at line 37 of file theory_arith3.h.
CVC3::TheoryArith3::FreeConst::FreeConst | ( | const Rational & | r, | |
bool | strict | |||
) | [inline] |
Definition at line 38 of file theory_arith3.h.
const Rational& CVC3::TheoryArith3::FreeConst::getConst | ( | ) | const [inline] |
Definition at line 39 of file theory_arith3.h.
Referenced by CVC3::TheoryArith3::isStale(), CVC3::operator<<(), and CVC3::TheoryArith3::updateSubsumptionDB().
bool CVC3::TheoryArith3::FreeConst::strict | ( | ) | const [inline] |
Definition at line 40 of file theory_arith3.h.
Referenced by CVC3::TheoryArith3::isStale(), CVC3::operator<<(), and CVC3::TheoryArith3::updateSubsumptionDB().
Rational CVC3::TheoryArith3::FreeConst::d_r [private] |
Definition at line 34 of file theory_arith3.h.
bool CVC3::TheoryArith3::FreeConst::d_strict [private] |
Definition at line 35 of file theory_arith3.h.