virtual CVC3::CNF_Rules::~CNF_Rules | ( | ) | [inline, virtual, inherited] |
Destructor.
Definition at line 40 of file cnf_rules.h.
virtual void CVC3::CNF_Rules::learnedClauses | ( | const Theorem & | thm, | |
std::vector< Theorem > & | , | |||
bool | newLemma | |||
) | [pure virtual, inherited] |
Learned clause rule:
.
thm | is the theorem ![]() ![]() ![]() ![]() ![]() |
Referenced by SAT::CNF_Manager::addLemma(), and SAT::CNF_Manager::convertLemma().
virtual Theorem CVC3::CNF_Rules::ifLiftRule | ( | const Expr & | e, | |
int | itePos | |||
) | [pure virtual, inherited] |
|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))
Referenced by SAT::CNF_Manager::replaceITErec().
virtual Theorem CVC3::CNF_Rules::CNFAddUnit | ( | const Theorem & | thm | ) | [pure virtual, inherited] |
virtual Theorem CVC3::CNF_Rules::CNFConvert | ( | const Expr & | e, | |
const Theorem & | thm | |||
) | [pure virtual, inherited] |
Referenced by SAT::CNF_Manager::convertLemma().
virtual Theorem CVC3::CNF_Rules::CNFtranslate | ( | const Expr & | before, | |
const Expr & | after, | |||
std::string | reason, | |||
int | pos | |||
) | [pure virtual, inherited] |
Referenced by SAT::CNF_Manager::translateExprRec().
virtual Theorem CVC3::CNF_Rules::CNFITEtranslate | ( | const Expr & | before, | |
const std::vector< Expr > & | after, | |||
const std::vector< Theorem > & | thms, | |||
int | pos | |||
) | [pure virtual, inherited] |
Referenced by SAT::CNF_Manager::translateExprRec().