Proof Rules for the Search Engines

Classes

class CVCL::CNF_Rules
API to the CNF proof rules. More...

Functions

virtual CVCL::CNF_Rules::~CNF_Rules ()
Destructor.
virtual Theorem CVCL::CNF_Rules::learnedClause (const Theorem &thm)=0
Learned clause rule:
$\frac{A_1,\ldots,A_n\vdash B} {\vdash\neg A_1\vee\cdots\vee \neg A_n\vee B}$
.
virtual Theorem CVCL::CNF_Rules::ifLiftRule (const Expr &e, int itePos)=0
|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))

Function Documentation

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

Destructor.

Definition at line 48 of file cnf_rules.h.

virtual Theorem CVCL::CNF_Rules::learnedClause ( const Theorem & thm ) [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 CVCL::CNF_TheoremProducer.
Referenced by SAT::CNF_Manager::addLemma(), and SAT::CNF_Manager::convertLemma().

virtual Theorem CVCL::CNF_Rules::ifLiftRule ( const Expr & e,

int itePos

) [pure virtual, inherited]

|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))

Implemented in CVCL::CNF_TheoremProducer.
Referenced by SAT::CNF_Manager::replaceITErec().

Generated on Thu Apr 13 16:57:40 2006 for CVC Lite by

1.4.4