22 #ifndef _cvc3__arith_proof_rules_h_
23 #define _cvc3__arith_proof_rules_h_
159 const Expr& y,
const Expr& z,
int kind) = 0;
283 const Theorem& isIntRHS,
bool changeRight) = 0;
343 virtual Theorem cANDaIffcANDb(const Theorem& thm,
344 const Expr& solvedEq) = 0;
345 virtual Theorem substSolvedFormRule(const Expr& e1,
346 ExprMap<Expr>& eMap) = 0;
347 virtual Theorem aANDcIffbANDc(const Theorem& thm, const Expr& newEq) = 0;
396 const std::vector<Theorem>& isIntVars) = 0;
453 std::vector<Theorem>& x_le_c2,
Rational c2) = 0;