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. More... | |
const Theorem & | ineq () const |
Get the inequality. More... | |
const FreeConst & | getConst () const |
Get the max/min constant. More... | |
bool | varOnRHS () const |
Flag whether var is isolated on the RHS. More... | |
bool | varOnLHS () const |
Flag whether var is isolated on the LHS. More... | |
operator Theorem () const | |
Auto-cast to Theorem. More... | |
Private Member Functions | |
Ineq () | |
Default constructor is disabled. More... | |
Private Attributes | |
Theorem | d_ineq |
The inequality. More... | |
bool | d_rhs |
Var is isolated on the RHS. More... | |
const FreeConst * | d_const |
Private class for an inequality in the Fourier-Motzkin database.
Definition at line 49 of file theory_arith3.h.
|
inlineprivate |
Default constructor is disabled.
Definition at line 55 of file theory_arith3.h.
Initial constructor. 'r' is taken from the subsumption database.
Definition at line 58 of file theory_arith3.h.
|
inline |
Get the inequality.
Definition at line 61 of file theory_arith3.h.
References d_ineq.
Referenced by CVC3::TheoryArith3::isStale(), CVC3::operator<<(), and CVC3::TheoryArith3::projectInequalities().
|
inline |
Get the max/min constant.
Definition at line 63 of file theory_arith3.h.
References d_const.
Referenced by CVC3::TheoryArith3::isStale(), and CVC3::operator<<().
|
inline |
Flag whether var is isolated on the RHS.
Definition at line 65 of file theory_arith3.h.
References d_rhs.
Referenced by CVC3::TheoryArith3::isStale(), and CVC3::operator<<().
|
inline |
Flag whether var is isolated on the LHS.
Definition at line 67 of file theory_arith3.h.
References d_rhs.
|
inline |
|
private |
The inequality.
Definition at line 51 of file theory_arith3.h.
Referenced by ineq(), and operator Theorem().
|
private |
Var is isolated on the RHS.
Definition at line 52 of file theory_arith3.h.
Referenced by varOnLHS(), and varOnRHS().
|
private |
The max/min const for subsumption check
Definition at line 53 of file theory_arith3.h.
Referenced by getConst().