Proof Rules for the Search Engines

Classes

Functions


Function Documentation

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:

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

.

Parameters:
thm is 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 
) [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]


Generated on Thu Oct 15 22:17:16 2009 for CVC3 by  doxygen 1.5.8