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_Rules [pure virtual]
CNFConvert(const Expr &e, const Theorem &thm)=0CVC3::CNF_Rules [pure virtual]
CNFITEtranslate(const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)=0CVC3::CNF_Rules [pure virtual]
CNFtranslate(const Expr &before, const Expr &after, std::string reason, int pos, const std::vector< Theorem > &thms)=0CVC3::CNF_Rules [pure virtual]
ifLiftRule(const Expr &e, int itePos)=0CVC3::CNF_Rules [pure virtual]
learnedClauses(const Theorem &thm, std::vector< Theorem > &, bool newLemma)=0CVC3::CNF_Rules [pure virtual]
~CNF_Rules()CVC3::CNF_Rules [inline, virtual]