CVC3
CVC3::CNF_Rules Member List

This is the complete list of members for CVC3::CNF_Rules, including all inherited members.

CNFAddUnit(const Theorem &thm)=0CVC3::CNF_Rulespure virtual
CNFConvert(const Expr &e, const Theorem &thm)=0CVC3::CNF_Rulespure virtual
CNFITEtranslate(const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)=0CVC3::CNF_Rulespure virtual
CNFtranslate(const Expr &before, const Expr &after, std::string reason, int pos, const std::vector< Theorem > &thms)=0CVC3::CNF_Rulespure virtual
ifLiftRule(const Expr &e, int itePos)=0CVC3::CNF_Rulespure virtual
learnedClauses(const Theorem &thm, std::vector< Theorem > &, bool newLemma)=0CVC3::CNF_Rulespure virtual
~CNF_Rules()CVC3::CNF_Rulesinlinevirtual