CVC3
|
Data class for the strongest free constant in separation inqualities
Definition at line 51 of file theory_arith_new.h.
CVC3::TheoryArithNew::FreeConst::FreeConst | ( | ) | [inline] |
Definition at line 56 of file theory_arith_new.h.
CVC3::TheoryArithNew::FreeConst::FreeConst | ( | const Rational & | r, |
bool | strict | ||
) | [inline] |
Definition at line 57 of file theory_arith_new.h.
const Rational& CVC3::TheoryArithNew::FreeConst::getConst | ( | ) | const [inline] |
bool CVC3::TheoryArithNew::FreeConst::strict | ( | ) | const [inline] |
Definition at line 59 of file theory_arith_new.h.
References d_strict.
Referenced by CVC3::operator<<().
Rational CVC3::TheoryArithNew::FreeConst::d_r [private] |
Definition at line 53 of file theory_arith_new.h.
Referenced by getConst().
bool CVC3::TheoryArithNew::FreeConst::d_strict [private] |
Definition at line 54 of file theory_arith_new.h.
Referenced by strict().