22 #ifndef _cvc3__bitvector_theorem_producer_h_
23 #define _cvc3__bitvector_theorem_producer_h_
30 class TheoryBitvector;
74 std::vector<Expr> & result);
80 const std::vector<Expr>& elements);
176 const Theorem& rhs_i,
int kind);
248 const std::vector<Theorem>& t2,
249 const Expr& bvPlusTerm,
int i);
253 const Expr& bvPlusTerm,
504 const std::vector<Theorem>& t2BitExtractThms,
510 int precomputedFlag);
601 const std::vector<Theorem>& b_bits,
602 const Expr& a_times_b,
603 std::vector<Theorem>& output_bits);
612 const std::vector<Theorem>& b_bits,
613 const Expr& a_plus_b,
614 std::vector<Theorem>& output_bits);