22 #ifndef _cvc3__sat__cnf_rules_h_
23 #define _cvc3__sat__cnf_rules_h_
53 std::vector<Theorem>&,
64 const std::vector<Theorem>& thms) = 0;
67 const std::vector<Expr>& after,
68 const std::vector<Theorem>& thms,
Data structure of expressions in CVC3.
virtual Theorem CNFtranslate(const Expr &before, const Expr &after, std::string reason, int pos, const std::vector< Theorem > &thms)=0
virtual void learnedClauses(const Theorem &thm, std::vector< Theorem > &, bool newLemma)=0
Learned clause rule: .
API to the CNF proof rules.
virtual Theorem CNFAddUnit(const Theorem &thm)=0
virtual Theorem ifLiftRule(const Expr &e, int itePos)=0
|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))
virtual Theorem CNFITEtranslate(const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)=0
virtual Theorem CNFConvert(const Expr &e, const Theorem &thm)=0
virtual ~CNF_Rules()
Destructor.