Collaboration diagram for Proof Rules for the Search Engines:

Classes

class CVC3::SearchEngineRules
API to the proof rules for the Search Engines. More...

Functions

virtual CVC3::SearchEngineRules::~SearchEngineRules ()
Destructor.
virtual Theorem CVC3::SearchEngineRules::eliminateSkolemAxioms (const Theorem &tFalse, const std::vector< Theorem > &delta)=0
virtual Theorem CVC3::SearchEngineRules::proofByContradiction (const Expr &a, const Theorem &pfFalse)=0
Proof by contradiction:

$\frac{\Gamma, \neg A \vdash\mathrm{FALSE}}{\Gamma \vdash A}$

.
virtual Theorem CVC3::SearchEngineRules::negIntro (const Expr &not_a, const Theorem &pfFalse)=0
Negation introduction:

$\frac{\Gamma, A \vdash\mathrm{FALSE}}{\Gamma\vdash\neg A}$

.
virtual Theorem CVC3::SearchEngineRules::caseSplit (const Expr &a, const Theorem &a_proves_c, const Theorem &not_a_proves_c)=0
Case split:

$\frac{\Gamma_1, A\vdash C \quad \Gamma_2, \neg A\vdash C} {\Gamma_1\cup\Gamma_2\vdash C}$

.
virtual Theorem CVC3::SearchEngineRules::conflictClause (const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)=0
Conflict clause rule:

$\frac{\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}} {\Gamma\vdash\neg A_1\vee\cdots\vee \neg A_n}$

.
virtual Theorem CVC3::SearchEngineRules::cutRule (const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)=0
Cut rule:

$\frac{\Gamma_1\vdash A_1\quad\cdots\quad\Gamma_n\vdash A_n \quad \Gamma', A_1,\ldots,A_n\vdash B} {\bigcup_{i=1}^n\Gamma_i\cup\Gamma'\vdash B}$

.
virtual Theorem CVC3::SearchEngineRules::unitProp (const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)=0
Unit propagation rule:

$\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n]-\{i\} \quad \Gamma\vdash A_1\vee\cdots\vee A_n} {\bigcup_{j\in[1\ldots n]-\{i\}}\Gamma_j\cup\Gamma\vdash A_i}$

.
virtual Theorem CVC3::SearchEngineRules::conflictRule (const std::vector< Theorem > &thms, const Theorem &clause)=0
"Conflict" rule (all literals in a clause become FALSE)

$\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n] \quad \Gamma\vdash A_1\vee\cdots\vee A_n} {\bigcup_{j\in[1\ldots n]}\Gamma_j\cup\Gamma \vdash\mathrm{FALSE}}$
virtual Theorem CVC3::SearchEngineRules::propAndrAF (const Theorem &andr_th, bool left, const Theorem &b_th)=0
virtual Theorem CVC3::SearchEngineRules::propAndrAT (const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)=0
virtual void CVC3::SearchEngineRules::propAndrLRT (const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)=0
virtual Theorem CVC3::SearchEngineRules::propAndrLF (const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)=0
virtual Theorem CVC3::SearchEngineRules::propAndrRF (const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)=0
virtual Theorem CVC3::SearchEngineRules::confAndrAT (const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)=0
virtual Theorem CVC3::SearchEngineRules::confAndrAF (const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)=0
virtual Theorem CVC3::SearchEngineRules::propIffr (const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)=0
virtual Theorem CVC3::SearchEngineRules::confIffr (const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)=0
virtual Theorem CVC3::SearchEngineRules::propIterIte (const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)=0
virtual void CVC3::SearchEngineRules::propIterIfThen (const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)=0
virtual Theorem CVC3::SearchEngineRules::propIterThen (const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)=0
virtual Theorem CVC3::SearchEngineRules::confIterThenElse (const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)=0
virtual Theorem CVC3::SearchEngineRules::confIterIfThen (const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)=0
virtual Theorem CVC3::SearchEngineRules::andCNFRule (const Theorem &thm)=0
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].
virtual Theorem CVC3::SearchEngineRules::orCNFRule (const Theorem &thm)=0
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].
virtual Theorem CVC3::SearchEngineRules::impCNFRule (const Theorem &thm)=0
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
virtual Theorem CVC3::SearchEngineRules::iffCNFRule (const Theorem &thm)=0
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
virtual Theorem CVC3::SearchEngineRules::iteCNFRule (const Theorem &thm)=0
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].
virtual Theorem CVC3::SearchEngineRules::iteToClauses (const Theorem &ite)=0
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
virtual Theorem CVC3::SearchEngineRules::iffToClauses (const Theorem &iff)=0
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
virtual Theorem CVC3::SearchEngineRules::satProof (const Expr &queryExpr, const Proof &satProof)=0

Function Documentation

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

Destructor.

Definition at line 41 of file search_rules.h.

virtual Theorem CVC3::SearchEngineRules::eliminateSkolemAxioms	(	const Theorem &	tFalse,
		const std::vector< Theorem > &	delta
	)		`[pure virtual, inherited]`

Eliminate skolem axioms: Gamma, Delta |- false => Gamma|- false where Delta is a set of skolem axioms {|-Exists(x) phi (x) => phi(c)} and gamma does not contain any of the skolem constants c.

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::processResult().

virtual Theorem CVC3::SearchEngineRules::proofByContradiction	(	const Expr &	a,
		const Theorem &	pfFalse
	)		`[pure virtual, inherited]`

Proof by contradiction:

$\frac{\Gamma, \neg A \vdash\mathrm{FALSE}}{\Gamma \vdash A}$

.

$\neg A$ does not have to be present in the assumptions.

Parameters:

a	is the assumption A
pfFalse	is the theorem $\Gamma, \neg A \vdash\mathrm{FALSE}$

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::processResult().

virtual Theorem CVC3::SearchEngineRules::negIntro	(	const Expr &	not_a,
		const Theorem &	pfFalse
	)		`[pure virtual, inherited]`

Negation introduction:

$\frac{\Gamma, A \vdash\mathrm{FALSE}}{\Gamma\vdash\neg A}$

.

Parameters:

not_a	is the formula $\neg A$ . We pass the negation $\neg A$ , and not just A, for efficiency: building $\neg A$ is more expensive (due to uniquifying pointers in Expr package) than extracting A from $\neg A$ .
pfFalse	is the theorem $\Gamma, A \vdash\mathrm{FALSE}$

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::processResult().

virtual Theorem CVC3::SearchEngineRules::caseSplit	(	const Expr &	a,
		const Theorem &	a_proves_c,
		const Theorem &	not_a_proves_c
	)		`[pure virtual, inherited]`

Case split:

$\frac{\Gamma_1, A\vdash C \quad \Gamma_2, \neg A\vdash C} {\Gamma_1\cup\Gamma_2\vdash C}$

.

Parameters:

a	is the assumption A to split on
a_proves_c	is the theorem $\Gamma_1, A\vdash C$
not_a_proves_c	is the theorem $\Gamma_2, \neg A\vdash C$

Implemented in CVC3::SearchEngineTheoremProducer.

virtual Theorem CVC3::SearchEngineRules::conflictClause	(	const Theorem &	thm,
		const std::vector< Theorem > &	lits,
		const std::vector< Theorem > &	gamma
	)		`[pure virtual, inherited]`

Conflict clause rule:

$\frac{\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}} {\Gamma\vdash\neg A_1\vee\cdots\vee \neg A_n}$

.

Parameters:

thm	is the theorem $\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}$
lits	is the vector of literals A_i. They must be present in the set of assumptions of thm.
gamma	FIXME: document this!!

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchEngineFast::analyzeUIPs().

virtual Theorem CVC3::SearchEngineRules::cutRule	(	const std::vector< Theorem > &	thmsA,
		const Theorem &	as_prove_b
	)		`[pure virtual, inherited]`

Cut rule:

$\frac{\Gamma_1\vdash A_1\quad\cdots\quad\Gamma_n\vdash A_n \quad \Gamma', A_1,\ldots,A_n\vdash B} {\bigcup_{i=1}^n\Gamma_i\cup\Gamma'\vdash B}$

.

Parameters:

thmsA	is a vector of theorems $\Gamma_i\vdash A_i$
as_prove_b	is the theorem $\Gamma', A_1,\ldots,A_n\vdash B$ (the name means "A's prove B")

Implemented in CVC3::SearchEngineTheoremProducer.

virtual Theorem CVC3::SearchEngineRules::unitProp	(	const std::vector< Theorem > &	thms,
		const Theorem &	clause,
		unsigned	i
	)		`[pure virtual, inherited]`

Unit propagation rule:

$\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n]-\{i\} \quad \Gamma\vdash A_1\vee\cdots\vee A_n} {\bigcup_{j\in[1\ldots n]-\{i\}}\Gamma_j\cup\Gamma\vdash A_i}$

.

Parameters:

clause	is the proof of the clause $\Gamma\vdash A_1\vee\cdots\vee A_n$
i	is the index (0..n-1) of the literal to be unit-propagated
thms	is the vector of theorems $\Gamma_j\vdash\neg A_j$ for all literals except A_i

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::Variable::deriveThmRec(), and CVC3::SearchEngineFast::unitPropagation().

virtual Theorem CVC3::SearchEngineRules::conflictRule	(	const std::vector< Theorem > &	thms,
		const Theorem &	clause
	)		`[pure virtual, inherited]`

"Conflict" rule (all literals in a clause become FALSE)

$\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n] \quad \Gamma\vdash A_1\vee\cdots\vee A_n} {\bigcup_{j\in[1\ldots n]}\Gamma_j\cup\Gamma \vdash\mathrm{FALSE}}$

Parameters:

clause	is the proof of the clause $\Gamma\vdash A_1\vee\cdots\vee A_n$
thms	is the vector of theorems $\Gamma_j\vdash\neg A_j$

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchEngineFast::addNonLiteralFact(), CVC3::Variable::deriveThmRec(), and CVC3::SearchEngineFast::propagate().

virtual Theorem CVC3::SearchEngineRules::propAndrAF	(	const Theorem &	andr_th,
		bool	left,
		const Theorem &	b_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual Theorem CVC3::SearchEngineRules::propAndrAT	(	const Theorem &	andr_th,
		const Theorem &	l_th,
		const Theorem &	r_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual void CVC3::SearchEngineRules::propAndrLRT	(	const Theorem &	andr_th,
		const Theorem &	a_th,
		Theorem *	l_th,
		Theorem *	r_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual Theorem CVC3::SearchEngineRules::propAndrLF	(	const Theorem &	andr_th,
		const Theorem &	a_th,
		const Theorem &	r_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual Theorem CVC3::SearchEngineRules::propAndrRF	(	const Theorem &	andr_th,
		const Theorem &	a_th,
		const Theorem &	l_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual Theorem CVC3::SearchEngineRules::confAndrAT	(	const Theorem &	andr_th,
		const Theorem &	a_th,
		bool	left,
		const Theorem &	b_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual Theorem CVC3::SearchEngineRules::confAndrAF	(	const Theorem &	andr_th,
		const Theorem &	a_th,
		const Theorem &	l_th,
		const Theorem &	r_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual Theorem CVC3::SearchEngineRules::propIffr	(	const Theorem &	iffr_th,
		int	p,
		const Theorem &	a_th,
		const Theorem &	b_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual Theorem CVC3::SearchEngineRules::confIffr	(	const Theorem &	iffr_th,
		const Theorem &	i_th,
		const Theorem &	l_th,
		const Theorem &	r_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual Theorem CVC3::SearchEngineRules::propIterIte	(	const Theorem &	iter_th,
		bool	left,
		const Theorem &	if_th,
		const Theorem &	then_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual void CVC3::SearchEngineRules::propIterIfThen	(	const Theorem &	iter_th,
		bool	left,
		const Theorem &	ite_th,
		const Theorem &	then_th,
		Theorem *	if_th,
		Theorem *	else_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual Theorem CVC3::SearchEngineRules::propIterThen	(	const Theorem &	iter_th,
		const Theorem &	ite_th,
		const Theorem &	if_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual Theorem CVC3::SearchEngineRules::confIterThenElse	(	const Theorem &	iter_th,
		const Theorem &	ite_th,
		const Theorem &	then_th,
		const Theorem &	else_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual Theorem CVC3::SearchEngineRules::confIterIfThen	(	const Theorem &	iter_th,
		bool	left,
		const Theorem &	ite_th,
		const Theorem &	if_th,
		const Theorem &	then_th
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::Circuit::propagate().

virtual Theorem CVC3::SearchEngineRules::andCNFRule ( const Theorem & thm ) [pure virtual, inherited]

AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules().

virtual Theorem CVC3::SearchEngineRules::orCNFRule ( const Theorem & thm ) [pure virtual, inherited]

OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules().

virtual Theorem CVC3::SearchEngineRules::impCNFRule ( const Theorem & thm ) [pure virtual, inherited]

(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules().

virtual Theorem CVC3::SearchEngineRules::iffCNFRule ( const Theorem & thm ) [pure virtual, inherited]

(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules().

virtual Theorem CVC3::SearchEngineRules::iteCNFRule ( const Theorem & thm ) [pure virtual, inherited]

ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules().

virtual Theorem CVC3::SearchEngineRules::iteToClauses ( const Theorem & ite ) [pure virtual, inherited]

ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::enqueueCNFrec().

virtual Theorem CVC3::SearchEngineRules::iffToClauses ( const Theorem & iff ) [pure virtual, inherited]

e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)

Implemented in CVC3::SearchEngineTheoremProducer.

Referenced by CVC3::SearchImplBase::applyCNFRules().

virtual Theorem CVC3::SearchEngineRules::satProof	(	const Expr &	queryExpr,
		const Proof &	satProof
	)		`[pure virtual, inherited]`

Implemented in CVC3::SearchEngineTheoremProducer.