CVC3::SearchEngineTheoremProducer Class Reference

#include <search_theorem_producer.h>

Inheritance diagram for CVC3::SearchEngineTheoremProducer:

[legend]

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 46 of file search_theorem_producer.cpp.

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

Definition at line 47 of file search_theorem_producer.h.

Member Function Documentation

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

Definition at line 171 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 390 of file search_theorem_producer.cpp.

References CVC3::Expr::begin(), CHECK_SOUND, CVC3::ExprMap< Data >::count(), CVC3::Expr::end(), CVC3::EXISTS, CVC3::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 408 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 58 of file search_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isFalse(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), 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 85 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 114 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 433 of file search_theorem_producer.cpp.

References 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(), CVC3::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 200 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(), CVC3::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 354 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 490 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 1088 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 543 of file search_theorem_producer.cpp.

References CVC3::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 572 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CVC3::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 602 of file search_theorem_producer.cpp.

References CVC3::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 630 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CVC3::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 660 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CVC3::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 690 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CVC3::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 723 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CVC3::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 761 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::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 813 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::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 860 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::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 902 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::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 949 of file search_theorem_producer.cpp.

References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::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 991 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::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 1038 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::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 1139 of file search_theorem_producer.cpp.

References CVC3::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 1144 of file search_theorem_producer.cpp.

References opCNFRule(), and CVC3::OR.

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

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

Implements CVC3::SearchEngineRules.

Definition at line 1149 of file search_theorem_producer.cpp.

References CVC3::IMPLIES, and opCNFRule().

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

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

Implements CVC3::SearchEngineRules.

Definition at line 1154 of file search_theorem_producer.cpp.

References CVC3::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 1159 of file search_theorem_producer.cpp.

References CVC3::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 1165 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 1185 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 1559 of file search_theorem_producer.cpp.

References CVC3::ExprMap< Data >::begin(), collectVars(), CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), std::endl(), CVC3::Expr::getEM(), CVC3::Proof::getExpr(), CVC3::TheoremProducer::newPf(), CVC3::ExprManager::newStringExpr(), CVC3::TheoremProducer::newTheorem(), LFSCPrinter::print(), CVC3::ExprMap< Data >::size(), and CVC3::TheoremProducer::withProof().

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 1288 of file search_theorem_producer.cpp.

References CVC3::AND, CVC3::andExpr(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), CVC3::IFF, CVC3::IMPLIES, CVC3::ITE, CVC3::Expr::negate(), CVC3::OR, CVC3::orExpr(), CVC3::Expr::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 1362 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 CVC3::TRACE.

Referenced by opCNFRule().

Member Data Documentation

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

Definition at line 36 of file search_theorem_producer.h.

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