Classes | Functions

Proof Rules for the Search Engines



Function Documentation

virtual CVC3::CNF_Rules::~CNF_Rules ( ) [inline, virtual, inherited]


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:

\[\frac{A_1,\ldots,A_n\vdash B} {\vdash\neg A_1\vee\cdots\vee \neg A_n\vee B}\]


thmis the theorem $ A_1,\ldots,A_n\vdash B$ Each $A_i$ and $B$ should be literals $B$ can also be $\mathrm{FALSE}$

Implemented in CVC3::CNF_TheoremProducer.

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, _))

Implemented in CVC3::CNF_TheoremProducer.

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]
virtual Theorem CVC3::CNF_Rules::CNFtranslate ( const Expr before,
const Expr after,
std::string  reason,
int  pos,
const std::vector< Theorem > &  thms 
) [pure virtual, inherited]
virtual Theorem CVC3::CNF_Rules::CNFITEtranslate ( const Expr before,
const std::vector< Expr > &  after,
const std::vector< Theorem > &  thms,
int  pos 
) [pure virtual, inherited]