22 #ifndef _cvc3__search__search_rules_h_
23 #define _cvc3__search__search_rules_h_
49 const std::vector<Theorem>& delta) = 0;
91 const Theorem& not_a_proves_c) = 0;
108 const std::vector<Theorem>& lits,
109 const std::vector<Theorem>& gamma) = 0;
126 const Theorem& as_prove_b) = 0;
145 const Theorem& clause,
unsigned i) = 0;