|
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().
1.7.3