CVC3
|
This is the complete list of members for CVC3::CNF_Rules, including all inherited members.
CNFAddUnit(const Theorem &thm)=0 | CVC3::CNF_Rules | pure virtual |
CNFConvert(const Expr &e, const Theorem &thm)=0 | CVC3::CNF_Rules | pure virtual |
CNFITEtranslate(const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)=0 | CVC3::CNF_Rules | pure virtual |
CNFtranslate(const Expr &before, const Expr &after, std::string reason, int pos, const std::vector< Theorem > &thms)=0 | CVC3::CNF_Rules | pure virtual |
ifLiftRule(const Expr &e, int itePos)=0 | CVC3::CNF_Rules | pure virtual |
learnedClauses(const Theorem &thm, std::vector< Theorem > &, bool newLemma)=0 | CVC3::CNF_Rules | pure virtual |
~CNF_Rules() | CVC3::CNF_Rules | inlinevirtual |