Collaboration diagram for CVCL::TheoryArith::Ineq:
Definition at line 112 of file theory_arith.h.
|
Default constructor is disabled.
Definition at line 118 of file theory_arith.h. |
|
Initial constructor. 'r' is taken from the subsumption database.
Definition at line 121 of file theory_arith.h. |
|
Get the inequality.
Definition at line 124 of file theory_arith.h. References d_ineq. Referenced by CVCL::TheoryArith::isStale(), CVCL::operator<<(), and CVCL::TheoryArith::projectInequalities(). |
|
Get the max/min constant.
Definition at line 126 of file theory_arith.h. References d_const. Referenced by CVCL::TheoryArith::isStale(), and CVCL::operator<<(). |
|
Flag whether var is isolated on the RHS.
Definition at line 128 of file theory_arith.h. References d_rhs. Referenced by CVCL::TheoryArith::isStale(), and CVCL::operator<<(). |
|
Flag whether var is isolated on the LHS.
Definition at line 130 of file theory_arith.h. References d_rhs. |
|
Auto-cast to Theorem.
Definition at line 132 of file theory_arith.h. References d_ineq. |
|
The inequality.
Definition at line 114 of file theory_arith.h. Referenced by ineq(), and operator Theorem(). |
|
Var is isolated on the RHS.
Definition at line 115 of file theory_arith.h. Referenced by varOnLHS(), and varOnRHS(). |
|
The max/min const for subsumption check Definition at line 116 of file theory_arith.h. Referenced by getConst(). |