CVC3

Private class for an inequality in the FourierMotzkin database. More...
Private class for an inequality in the FourierMotzkin database.
Definition at line 64 of file theory_arith_new.h.
CVC3::TheoryArithNew::Ineq::Ineq  (  )  [inline, private] 
Default constructor is disabled.
Definition at line 70 of file theory_arith_new.h.
CVC3::TheoryArithNew::Ineq::Ineq  (  const Theorem &  ineq, 
bool  varOnRHS,  
const FreeConst &  c  
)  [inline] 
Initial constructor. 'r' is taken from the subsumption database.
Definition at line 73 of file theory_arith_new.h.
const Theorem& CVC3::TheoryArithNew::Ineq::ineq  (  )  const [inline] 
Get the inequality.
Definition at line 76 of file theory_arith_new.h.
References d_ineq.
Referenced by CVC3::operator<<().
const FreeConst& CVC3::TheoryArithNew::Ineq::getConst  (  )  const [inline] 
Get the max/min constant.
Definition at line 78 of file theory_arith_new.h.
References d_const.
Referenced by CVC3::operator<<().
bool CVC3::TheoryArithNew::Ineq::varOnRHS  (  )  const [inline] 
Flag whether var is isolated on the RHS.
Definition at line 80 of file theory_arith_new.h.
References d_rhs.
Referenced by CVC3::operator<<().
bool CVC3::TheoryArithNew::Ineq::varOnLHS  (  )  const [inline] 
Flag whether var is isolated on the LHS.
Definition at line 82 of file theory_arith_new.h.
References d_rhs.
CVC3::TheoryArithNew::Ineq::operator Theorem  (  )  const [inline] 
Theorem CVC3::TheoryArithNew::Ineq::d_ineq [private] 
The inequality.
Definition at line 66 of file theory_arith_new.h.
Referenced by ineq(), and operator Theorem().
bool CVC3::TheoryArithNew::Ineq::d_rhs [private] 
Var is isolated on the RHS.
Definition at line 67 of file theory_arith_new.h.
Referenced by varOnLHS(), and varOnRHS().
const FreeConst* CVC3::TheoryArithNew::Ineq::d_const [private] 
The max/min const for subsumption check
Definition at line 68 of file theory_arith_new.h.
Referenced by getConst().