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. 

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