22 #ifndef _cvc3__sat__cnf_theorem_producer_h_
23 #define _cvc3__sat__cnf_theorem_producer_h_
54 const std::vector<Theorem>& thms) ;
56 const std::vector<Expr>& after,
57 const std::vector<Theorem>& thms,
Abstract proof rules for CNF conversion.
Data structure of expressions in CVC3.
CNF_TheoremProducer(TheoremManager *tm, const CLFlags &flags)
API to the CNF proof rules.
void getSmartClauses(const Theorem &thm, std::vector< Theorem > &clauses)
Theorem CNFITEtranslate(const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)
void learnedClauses(const Theorem &thm, std::vector< Theorem > &clauses, bool newLemma)
Learned clause rule: .
Theorem CNFConvert(const Expr &e, const Theorem &thm)
Theorem CNFtranslate(const Expr &before, const Expr &after, std::string reason, int pos, const std::vector< Theorem > &thms)
const bool & d_smartClauses
Theorem ifLiftRule(const Expr &e, int itePos)
|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))
Theorem CNFAddUnit(const Theorem &thm)