22 #ifndef _cvc3__arith_theorem_producer_h_
23 #define _cvc3__arith_theorem_producer_h_
52 void sumModM(std::vector<Expr>& summands,
const Expr& sum,
56 void sumMulF(std::vector<Expr>& summands,
const Expr& sum,
221 const Expr& z,
int kind);
279 const Theorem& isIntRHS,
bool changeRight);
282 const Theorem& isIntRHS,
bool changeRight);
288 const std::vector<Theorem>& isIntVars);
337 std::vector<Theorem>& x_le_c2,
Rational c2);