CVC3

Private class for an inequality in the FourierMotzkin database. More...
Private class for an inequality in the FourierMotzkin database.
Definition at line 50 of file theory_arith3.h.
CVC3::TheoryArith3::Ineq::Ineq  (  )  [inline, private] 
Default constructor is disabled.
Definition at line 56 of file theory_arith3.h.
CVC3::TheoryArith3::Ineq::Ineq  (  const Theorem &  ineq, 
bool  varOnRHS,  
const FreeConst &  c  
)  [inline] 
Initial constructor. 'r' is taken from the subsumption database.
Definition at line 59 of file theory_arith3.h.
const Theorem& CVC3::TheoryArith3::Ineq::ineq  (  )  const [inline] 
Get the inequality.
Definition at line 62 of file theory_arith3.h.
References d_const.
Referenced by CVC3::TheoryArith3::isStale(), CVC3::operator<<(), and CVC3::TheoryArith3::projectInequalities().
const FreeConst& CVC3::TheoryArith3::Ineq::getConst  (  )  const [inline] 
Get the max/min constant.
Definition at line 64 of file theory_arith3.h.
References d_rhs.
Referenced by CVC3::TheoryArith3::isStale(), and CVC3::operator<<().
bool CVC3::TheoryArith3::Ineq::varOnRHS  (  )  const [inline] 
Flag whether var is isolated on the RHS.
Definition at line 66 of file theory_arith3.h.
References d_rhs.
Referenced by CVC3::TheoryArith3::isStale(), and CVC3::operator<<().
bool CVC3::TheoryArith3::Ineq::varOnLHS  (  )  const [inline] 
Flag whether var is isolated on the LHS.
Definition at line 68 of file theory_arith3.h.
References d_ineq.
CVC3::TheoryArith3::Ineq::operator Theorem  (  )  const [inline] 
Autocast to Theorem.
Definition at line 70 of file theory_arith3.h.
Theorem CVC3::TheoryArith3::Ineq::d_ineq [private] 
bool CVC3::TheoryArith3::Ineq::d_rhs [private] 
Var is isolated on the RHS.
Definition at line 53 of file theory_arith3.h.
Referenced by getConst(), and varOnRHS().
const FreeConst* CVC3::TheoryArith3::Ineq::d_const [private] 
The max/min const for subsumption check
Definition at line 54 of file theory_arith3.h.
Referenced by ineq().