Proof Rules for the Search Engines

Classes

virtual CVC3::CNF_Rules::~CNF_Rules ()
Destructor.
virtual void CVC3::CNF_Rules::learnedClauses (const Theorem &thm, std::vector< Theorem > &, bool newLemma)=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, _))
virtual Theorem CVC3::CNF_Rules::CNFAddUnit (const Theorem &thm)=0
virtual Theorem CVC3::CNF_Rules::CNFConvert (const Expr &e, const Theorem &thm)=0
virtual Theorem CVC3::CNF_Rules::CNFtranslate (const Expr &before, const Expr &after, std::string reason, int pos)=0
virtual Theorem CVC3::CNF_Rules::CNFITEtranslate (const Expr &before, const std::vector< Expr > &after, const std::vector< Theorem > &thms, int pos)=0

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

should be literals $B$

can also be $\mathrm{FALSE}$

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

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]`