CVC3
2.4.1
|
Private class for an inequality in the Fourier-Motzkin database. More...
Public Member Functions | |
Ineq (const Theorem &ineq, bool varOnRHS, const FreeConst &c) | |
Initial constructor. 'r' is taken from the subsumption database. | |
const Theorem | ineq () const |
Get the inequality. | |
const FreeConst & | getConst () const |
Get the max/min constant. | |
bool | varOnRHS () const |
Flag whether var is isolated on the RHS. | |
bool | varOnLHS () const |
Flag whether var is isolated on the LHS. | |
operator Theorem () const | |
Auto-cast to Theorem. |
Private Member Functions | |
Ineq () | |
Default constructor is disabled. |
Private Attributes | |
Theorem | d_ineq |
The inequality. | |
bool | d_rhs |
Var is isolated on the RHS. | |
const FreeConst * | d_const |
Private class for an inequality in the Fourier-Motzkin database.
Definition at line 52 of file theory_arith_old.h.
|
inlineprivate |
Default constructor is disabled.
Definition at line 58 of file theory_arith_old.h.
|
inline |
Initial constructor. 'r' is taken from the subsumption database.
Definition at line 61 of file theory_arith_old.h.
|
inline |
Get the inequality.
Definition at line 64 of file theory_arith_old.h.
References d_ineq.
Referenced by CVC3::TheoryArithOld::computeTermBounds(), CVC3::TheoryArithOld::isStale(), CVC3::operator<<(), and CVC3::TheoryArithOld::projectInequalities().
|
inline |
Get the max/min constant.
Definition at line 66 of file theory_arith_old.h.
References d_const.
Referenced by CVC3::TheoryArithOld::isStale(), and CVC3::operator<<().
|
inline |
Flag whether var is isolated on the RHS.
Definition at line 68 of file theory_arith_old.h.
References d_rhs.
Referenced by CVC3::TheoryArithOld::isStale(), and CVC3::operator<<().
|
inline |
Flag whether var is isolated on the LHS.
Definition at line 70 of file theory_arith_old.h.
References d_rhs.
|
inline |
|
private |
The inequality.
Definition at line 54 of file theory_arith_old.h.
Referenced by ineq(), and operator Theorem().
|
private |
Var is isolated on the RHS.
Definition at line 55 of file theory_arith_old.h.
Referenced by varOnLHS(), and varOnRHS().
|
private |
The max/min const for subsumption check
Definition at line 56 of file theory_arith_old.h.
Referenced by getConst().