22 #ifndef _cvc3__arith_theorem_producer_old_h_
23 #define _cvc3__arith_theorem_producer_old_h_
51 void sumModM(std::vector<Expr>& summands,
const Expr& sum,
55 void sumMulF(std::vector<Expr>& summands,
const Expr& sum,
220 const Expr& z,
int kind);
278 const Theorem& isIntRHS,
bool changeRight);
281 const Theorem& isIntRHS,
bool changeRight);
288 const std::vector<Theorem>& isIntVars);
337 std::vector<Theorem>& x_le_c2,
Rational c2);