22 #ifndef _cvc3__bitvector_proof_rules_h_
23 #define _cvc3__bitvector_proof_rules_h_
116 const Theorem& e1,
int kind) = 0;
195 const std::vector<Theorem>& t2,
196 const Expr& bvPlusTerm,
int i) = 0;
201 const Expr& bvPlusTerm,
203 int precomputed) = 0;
369 int kind,
const std::string& name) = 0;
392 const std::vector<int>& idxs,
527 const std::vector<Theorem>& b_bits,
528 const Expr& a_times_b,
529 std::vector<Theorem>& output_bits) = 0;
538 const std::vector<Theorem>& b_bits,
539 const Expr& a_plus_b,
540 std::vector<Theorem>& output_bits) = 0;