Proof Rules for the Search Engines

Classes

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

Functions

virtual CVC3::CNF_Rules::~CNF_Rules ()
Destructor.
virtual Theorem CVC3::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 CVC3::CNF_Rules::ifLiftRule (const Expr &e, int itePos)=0
|- P(_, ITE(cond,a,b), _) <=> ITE(cond,Pred(_, a, _),Pred(_, b, _))

Function Documentation

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

Destructor.

Definition at line 40 of file cnf_rules.h.

virtual Theorem CVC3::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$

$A_i$

and

$B$

should be literals $B$

$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().

Generated on Tue Jul 3 14:35:23 2007 for CVC3 by

doxygen

1.5.1