#include <search_theorem_producer.h>

Inherits CVC3::SearchEngineRules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::SearchEngineTheoremProducer:

[legend]

List of all members.

Public Member Functions

SearchEngineTheoremProducer (TheoremManager *tm)
virtual ~SearchEngineTheoremProducer ()
virtual Theorem proofByContradiction (const Expr &a, const Theorem &pfFalse)
Proof by contradiction:

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

.
virtual Theorem negIntro (const Expr &not_a, const Theorem &pfFalse)
Negation introduction:

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

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

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

.
virtual Theorem eliminateSkolemAxioms (const Theorem &tFalse, const std::vector< Theorem > &delta)
virtual Theorem conflictClause (const Theorem &thm, const std::vector< Theorem > &lits, const std::vector< Theorem > &gamma)
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 cutRule (const std::vector< Theorem > &thmsA, const Theorem &as_prove_b)
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 unitProp (const std::vector< Theorem > &thms, const Theorem &clause, unsigned i)
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 conflictRule (const std::vector< Theorem > &thms, const Theorem &clause)
"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 propAndrAF (const Theorem &andr_th, bool left, const Theorem &b_th)
virtual Theorem propAndrAT (const Theorem &andr_th, const Theorem &l_th, const Theorem &r_th)
virtual void propAndrLRT (const Theorem &andr_th, const Theorem &a_th, Theorem *l_th, Theorem *r_th)
virtual Theorem propAndrLF (const Theorem &andr_th, const Theorem &a_th, const Theorem &r_th)
virtual Theorem propAndrRF (const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th)
virtual Theorem confAndrAT (const Theorem &andr_th, const Theorem &a_th, bool left, const Theorem &b_th)
virtual Theorem confAndrAF (const Theorem &andr_th, const Theorem &a_th, const Theorem &l_th, const Theorem &r_th)
virtual Theorem propIffr (const Theorem &iffr_th, int p, const Theorem &a_th, const Theorem &b_th)
virtual Theorem confIffr (const Theorem &iffr_th, const Theorem &i_th, const Theorem &l_th, const Theorem &r_th)
virtual Theorem propIterIte (const Theorem &iter_th, bool left, const Theorem &if_th, const Theorem &then_th)
virtual void propIterIfThen (const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &then_th, Theorem *if_th, Theorem *else_th)
virtual Theorem propIterThen (const Theorem &iter_th, const Theorem &ite_th, const Theorem &if_th)
virtual Theorem confIterThenElse (const Theorem &iter_th, const Theorem &ite_th, const Theorem &then_th, const Theorem &else_th)
virtual Theorem confIterIfThen (const Theorem &iter_th, bool left, const Theorem &ite_th, const Theorem &if_th, const Theorem &then_th)
Theorem andCNFRule (const Theorem &thm)
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].
Theorem orCNFRule (const Theorem &thm)
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v].
Theorem impCNFRule (const Theorem &thm)
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
Theorem iffCNFRule (const Theorem &thm)
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
Theorem iteCNFRule (const Theorem &thm)
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v].
Theorem iteToClauses (const Theorem &ite)
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
Theorem iffToClauses (const Theorem &iff)
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
Theorem satProof (const Expr &queryExpr, const Proof &satProof)

Private Member Functions

void verifyConflict (const Theorem &thm, TheoremMap &m)
void checkSoundNoSkolems (const Expr &e, ExprMap< bool > &visited, const ExprMap< bool > &skolems)
void checkSoundNoSkolems (const Theorem &t, ExprMap< bool > &visited, const ExprMap< bool > &skolems)
Theorem opCNFRule (const Theorem &thm, int kind, const std::string &ruleName)
Expr convertToCNF (const Expr &v, const Expr &phi)
produces the CNF for the formula v <==> phi
Expr findInLocalCache (const Expr &i, ExprMap< Expr > &localCache, std::vector< Expr > &boundVars)
checks if phi has v in local cache of opCNFRule, if so reuse v.

Private Attributes

CommonProofRules * d_commonRules

Detailed Description

Definition at line 32 of file search_theorem_producer.h.

Constructor & Destructor Documentation

SearchEngineTheoremProducer::SearchEngineTheoremProducer ( TheoremManager * tm )

Definition at line 62 of file search_theorem_producer.cpp.

virtual CVC3::SearchEngineTheoremProducer::~SearchEngineTheoremProducer ( ) [inline, virtual]

Definition at line 48 of file search_theorem_producer.h.

Member Function Documentation

void SearchEngineTheoremProducer::verifyConflict	(	const Theorem &	thm,
		TheoremMap &	m
	)		`[private]`

Definition at line 192 of file search_theorem_producer.cpp.

References CHECK_SOUND, and CVC3::Theorem::getAssumptionsRef().

Referenced by conflictClause().

void SearchEngineTheoremProducer::checkSoundNoSkolems	(	const Expr &	e,
		ExprMap< bool > &	visited,
		const ExprMap< bool > &	skolems
	)		`[private]`

Definition at line 411 of file search_theorem_producer.cpp.

References CVC3::Expr::begin(), CHECK_SOUND, CVC3::ExprMap< Data >::count(), CVC3::Expr::end(), EXISTS, FORALL, CVC3::Expr::getBody(), CVC3::Expr::getKind(), and CVC3::Expr::toString().

Referenced by checkSoundNoSkolems(), and eliminateSkolemAxioms().

void SearchEngineTheoremProducer::checkSoundNoSkolems	(	const Theorem &	t,
		ExprMap< bool > &	visited,
		const ExprMap< bool > &	skolems
	)		`[private]`

Definition at line 429 of file search_theorem_producer.cpp.

References checkSoundNoSkolems(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::isAssump(), CVC3::Theorem::isFlagged(), CVC3::Theorem::isRefl(), and CVC3::Theorem::setFlag().

Theorem SearchEngineTheoremProducer::proofByContradiction	(	const Expr &	a,
		const Theorem &	pfFalse
	)		`[virtual]`

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}$

Implements CVC3::SearchEngineRules.

Definition at line 74 of file search_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isFalse(), lfsc_called, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), satProof(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::negIntro	(	const Expr &	not_a,
		const Theorem &	pfFalse
	)		`[virtual]`

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}$

Implements CVC3::SearchEngineRules.

Definition at line 105 of file search_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::caseSplit	(	const Expr &	a,
		const Theorem &	a_proves_c,
		const Theorem &	not_a_proves_c
	)		`[virtual]`

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$

Implements CVC3::SearchEngineRules.

Definition at line 135 of file search_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::eliminateSkolemAxioms	(	const Theorem &	tFalse,
		const std::vector< Theorem > &	delta
	)		`[virtual]`

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.

Implements CVC3::SearchEngineRules.

Definition at line 454 of file search_theorem_producer.cpp.

References CVC3::ExprMap< Data >::begin(), CHECK_PROOFS, CHECK_SOUND, checkSoundNoSkolems(), CVC3::Theorem::clearAllFlags(), CVC3::TheoremProducer::d_em, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isFalse(), CVC3::ExprManager::newLeafExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), TRACE, and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::conflictClause	(	const Theorem &	thm,
		const std::vector< Theorem > &	lits,
		const std::vector< Theorem > &	gamma
	)		`[virtual]`

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!!

Implements CVC3::SearchEngineRules.

Definition at line 221 of file search_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::clearAllFlags(), CVC3::TheoremProducer::d_em, DebugAssert, CVC3::ExprHashMap< Data >::empty(), std::endl(), CVC3::Proof::getExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), IF_DEBUG, CVC3::Expr::isFalse(), CVC3::Expr::isVar(), CVC3::TheoremProducer::newLabel(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), OR, verifyConflict(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::cutRule	(	const std::vector< Theorem > &	thmsA,
		const Theorem &	as_prove_b
	)		`[virtual]`

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")

Implements CVC3::SearchEngineRules.

Definition at line 375 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

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

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

Implements CVC3::SearchEngineRules.

Definition at line 511 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::int2string(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::conflictRule	(	const std::vector< Theorem > &	thms,
		const Theorem &	clause
	)		`[virtual]`

"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$

Implements CVC3::SearchEngineRules.

Definition at line 1109 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::int2string(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propAndrAF	(	const Theorem &	andr_th,
		bool	left,
		const Theorem &	b_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 564 of file search_theorem_producer.cpp.

References AND_R, CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::refutes(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propAndrAT	(	const Theorem &	andr_th,
		const Theorem &	l_th,
		const Theorem &	r_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 593 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), AND_R, CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), and CVC3::TheoremProducer::withProof().

void SearchEngineTheoremProducer::propAndrLRT	(	const Theorem &	andr_th,
		const Theorem &	a_th,
		Theorem *	l_th,
		Theorem *	r_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 623 of file search_theorem_producer.cpp.

References AND_R, CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propAndrLF	(	const Theorem &	andr_th,
		const Theorem &	a_th,
		const Theorem &	r_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 651 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), AND_R, CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propAndrRF	(	const Theorem &	andr_th,
		const Theorem &	a_th,
		const Theorem &	l_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 681 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), AND_R, CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::confAndrAT	(	const Theorem &	andr_th,
		const Theorem &	a_th,
		bool	left,
		const Theorem &	b_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 711 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), AND_R, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::confAndrAF	(	const Theorem &	andr_th,
		const Theorem &	a_th,
		const Theorem &	l_th,
		const Theorem &	r_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 744 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), AND_R, CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propIffr	(	const Theorem &	iffr_th,
		int	p,
		const Theorem &	a_th,
		const Theorem &	b_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 782 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), IFF_R, CVC3::int2string(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::confIffr	(	const Theorem &	iffr_th,
		const Theorem &	i_th,
		const Theorem &	l_th,
		const Theorem &	r_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 834 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), IFF_R, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propIterIte	(	const Theorem &	iter_th,
		bool	left,
		const Theorem &	if_th,
		const Theorem &	then_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 881 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), ITE_R, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

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

Implements CVC3::SearchEngineRules.

Definition at line 923 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), ITE_R, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propIterThen	(	const Theorem &	iter_th,
		const Theorem &	ite_th,
		const Theorem &	if_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 970 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), ITE_R, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::confIterThenElse	(	const Theorem &	iter_th,
		const Theorem &	ite_th,
		const Theorem &	then_th,
		const Theorem &	else_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 1012 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), ITE_R, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::confIterIfThen	(	const Theorem &	iter_th,
		bool	left,
		const Theorem &	ite_th,
		const Theorem &	if_th,
		const Theorem &	then_th
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 1059 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), ITE_R, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::andCNFRule ( const Theorem & thm ) [virtual]

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

Implements CVC3::SearchEngineRules.

Definition at line 1160 of file search_theorem_producer.cpp.

References AND, and opCNFRule().

Theorem SearchEngineTheoremProducer::orCNFRule ( const Theorem & thm ) [virtual]

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

Implements CVC3::SearchEngineRules.

Definition at line 1165 of file search_theorem_producer.cpp.

References opCNFRule(), and OR.

Theorem SearchEngineTheoremProducer::impCNFRule ( const Theorem & thm ) [virtual]

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

Implements CVC3::SearchEngineRules.

Definition at line 1170 of file search_theorem_producer.cpp.

References IMPLIES, and opCNFRule().

Theorem SearchEngineTheoremProducer::iffCNFRule ( const Theorem & thm ) [virtual]

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

Implements CVC3::SearchEngineRules.

Definition at line 1175 of file search_theorem_producer.cpp.

References IFF, and opCNFRule().

Theorem SearchEngineTheoremProducer::iteCNFRule ( const Theorem & thm ) [virtual]

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

Implements CVC3::SearchEngineRules.

Definition at line 1180 of file search_theorem_producer.cpp.

References ITE, and opCNFRule().

Theorem SearchEngineTheoremProducer::iteToClauses ( const Theorem & ite ) [virtual]

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

Implements CVC3::SearchEngineRules.

Definition at line 1186 of file search_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::iffToClauses ( const Theorem & iff ) [virtual]

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

Implements CVC3::SearchEngineRules.

Definition at line 1206 of file search_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Theorem::isRewrite(), CVC3::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::satProof	(	const Expr &	queryExpr,
		const Proof &	satProof
	)		`[virtual]`

Implements CVC3::SearchEngineRules.

Definition at line 1419 of file search_theorem_producer.cpp.

References d_commonRules, CVC3::TheoremProducer::d_tm, CVC3::Assumptions::emptyAssump(), std::endl(), CVC3::Proof::getExpr(), CVC3::TheoremManager::getFlags(), CVC3::SearchEngine::getUserAssumptions(), lfsc_called, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), LFSCPrinter::print_LFSC(), search_engine, and CVC3::TheoremProducer::withProof().

Referenced by proofByContradiction().

Theorem SearchEngineTheoremProducer::opCNFRule	(	const Theorem &	thm,
		int	kind,
		const std::string &	ruleName
	)		`[private]`

Expr SearchEngineTheoremProducer::convertToCNF	(	const Expr &	v,
		const Expr &	phi
	)		`[private]`

produces the CNF for the formula v <==> phi

Definition at line 1309 of file search_theorem_producer.cpp.

References AND, CVC3::andExpr(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), IFF, IMPLIES, ITE, CVC3::Expr::negate(), OR, CVC3::Expr::orExpr(), CVC3::orExpr(), and CVC3::Expr::toString().

Referenced by opCNFRule().

Expr SearchEngineTheoremProducer::findInLocalCache	(	const Expr &	i,
		ExprMap< Expr > &	localCache,
		std::vector< Expr > &	boundVars
	)		`[private]`

checks if phi has v in local cache of opCNFRule, if so reuse v.

similarly for ( ! ... ! (phi))

Definition at line 1382 of file search_theorem_producer.cpp.

References CVC3::TheoremProducer::d_em, CVC3::ExprMap< Data >::end(), CVC3::ExprMap< Data >::find(), CVC3::Expr::getType(), IF_DEBUG, CVC3::Expr::iffExpr(), CVC3::Expr::isNot(), CVC3::ExprManager::newBoundVarExpr(), CVC3::Expr::toString(), and TRACE.

Referenced by opCNFRule().

Member Data Documentation

CommonProofRules* CVC3::SearchEngineTheoremProducer::d_commonRules [private]

Definition at line 36 of file search_theorem_producer.h.

Referenced by satProof().

The documentation for this class was generated from the following files:

CVC3::SearchEngineTheoremProducer Class Reference

Public Member Functions

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation