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)=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 | [inline, virtual] |