CVC3
2.4.1
|
API to the CNF proof rules. More...
#include <cnf_rules.h>
Public Member Functions | |
virtual | ~CNF_Rules () |
Destructor. More... | |
virtual void | learnedClauses (const Theorem &thm, std::vector< Theorem > &, bool newLemma)=0 |
Learned clause rule:
. More... | |
virtual Theorem | ifLiftRule (const Expr &e, int itePos)=0 |
|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _)) More... | |
virtual Theorem | CNFAddUnit (const Theorem &thm)=0 |
virtual Theorem | CNFConvert (const Expr &e, const Theorem &thm)=0 |
virtual Theorem | CNFtranslate (const Expr &before, const Expr &after, std::string reason, int pos, const std::vector< Theorem > &thms)=0 |
virtual Theorem | CNFITEtranslate (const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)=0 |
API to the CNF proof rules.
Definition at line 34 of file cnf_rules.h.