CVCL::SearchEngineTheoremProducer Class Reference

#include <search_theorem_producer.h>

Inheritance diagram for CVCL::SearchEngineTheoremProducer:

[legend]Collaboration diagram for CVCL::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)

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 40 of file search_theorem_producer.h.

Constructor & Destructor Documentation

SearchEngineTheoremProducer::SearchEngineTheoremProducer ( TheoremManager * tm )

Definition at line 55 of file search_theorem_producer.cpp.

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

Definition at line 55 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 CVCL::Assumptions::begin(), CVCL::Assumptions::end(), and CVCL::Theorem::getAssumptions().

void SearchEngineTheoremProducer::checkSoundNoSkolems ( const Expr & e,

ExprMap< bool > & visited,

const ExprMap< bool > & skolems

) [private]

Definition at line 410 of file search_theorem_producer.cpp.
References CVCL::Expr::begin(), CVCL::ExprMap< Data >::count(), CVCL::Expr::end(), CVCL::EXISTS, CVCL::FORALL, CVCL::Expr::getBody(), CVCL::Expr::getKind(), and CVCL::Expr::toString().
Referenced by checkSoundNoSkolems(), and eliminateSkolemAxioms().

void SearchEngineTheoremProducer::checkSoundNoSkolems ( const Theorem & t,

ExprMap< bool > & visited,

const ExprMap< bool > & skolems

) [private]

Definition at line 428 of file search_theorem_producer.cpp.
References CVCL::Assumptions::begin(), checkSoundNoSkolems(), CVCL::Assumptions::end(), CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::isAssump(), CVCL::Theorem::isFlagged(), and CVCL::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 CVCL::SearchEngineRules.
Definition at line 67 of file search_theorem_producer.cpp.
References CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::Expr::isFalse(), CVCL::Proof::isNull(), CVCL::Theorem::isNull(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::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 CVCL::SearchEngineRules.
Definition at line 98 of file search_theorem_producer.cpp.
References CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::Expr::isFalse(), CVCL::Expr::isNot(), CVCL::Proof::isNull(), CVCL::Theorem::isNull(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::toString(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::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 CVCL::SearchEngineRules.
Definition at line 131 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::Theorem::getAssumptions(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::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 CVCL::SearchEngineRules.
Definition at line 453 of file search_theorem_producer.cpp.
References CVCL::Expr::begin(), checkSoundNoSkolems(), CVCL::Theorem::clearAllFlags(), CVCL::TheoremProducer::d_em, CVCL::Theorem::getAssumptionsCopy(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::Expr::getType(), CVCL::Expr::getVars(), CVCL::Type::isBool(), CVCL::Expr::isExists(), CVCL::Expr::isFalse(), CVCL::Expr::mkOp(), CVCL::ExprManager::newLeafExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::skolemExpr(), CVCL::TRACE, CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

virtual Theorem CVCL::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 CVCL::SearchEngineRules.

virtual Theorem CVCL::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 CVCL::SearchEngineRules.

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 CVCL::SearchEngineRules.
Definition at line 513 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::Expr::arity(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::int2string(), CVCL::Expr::isNot(), CVCL::Expr::isOr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::toString(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::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 CVCL::SearchEngineRules.
Definition at line 1138 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::Expr::arity(), CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::int2string(), CVCL::Expr::isNot(), CVCL::Expr::isOr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::toString(), CVCL::Theorem::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propAndrAF ( const Theorem & andr_th,

bool left,

const Theorem & b_th

) [virtual]

Implements CVCL::SearchEngineRules.
Definition at line 569 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::AND_R, CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::refutes(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propAndrAT ( const Theorem & andr_th,

const Theorem & l_th,

const Theorem & r_th

) [virtual]

Implements CVCL::SearchEngineRules.
Definition at line 602 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::AND_R, CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

void SearchEngineTheoremProducer::propAndrLRT ( const Theorem & andr_th,

const Theorem & a_th,

Theorem * l_th,

Theorem * r_th

) [virtual]

Implements CVCL::SearchEngineRules.
Definition at line 636 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::AND_R, CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propAndrLF ( const Theorem & andr_th,

const Theorem & a_th,

const Theorem & r_th

) [virtual]

Implements CVCL::SearchEngineRules.
Definition at line 668 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::AND_R, CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::Theorem::refutes(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propAndrRF ( const Theorem & andr_th,

const Theorem & a_th,

const Theorem & l_th

) [virtual]

Implements CVCL::SearchEngineRules.
Definition at line 702 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::AND_R, CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::Theorem::refutes(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::confAndrAT ( const Theorem & andr_th,

const Theorem & a_th,

bool left,

const Theorem & b_th

) [virtual]

Implements CVCL::SearchEngineRules.
Definition at line 736 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::AND_R, CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::Theorem::refutes(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::confAndrAF ( const Theorem & andr_th,

const Theorem & a_th,

const Theorem & l_th,

const Theorem & r_th

) [virtual]

Implements CVCL::SearchEngineRules.
Definition at line 773 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::AND_R, CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::Theorem::refutes(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propIffr ( const Theorem & iffr_th,

int p,

const Theorem & a_th,

const Theorem & b_th

) [virtual]

Implements CVCL::SearchEngineRules.
Definition at line 811 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), b, CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::IFF_R, CVCL::int2string(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::Theorem::refutes(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::confIffr ( const Theorem & iffr_th,

const Theorem & i_th,

const Theorem & l_th,

const Theorem & r_th

) [virtual]

Implements CVCL::SearchEngineRules.
Definition at line 863 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::IFF_R, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::Theorem::refutes(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propIterIte ( const Theorem & iter_th,

bool left,

const Theorem & if_th,

const Theorem & then_th

) [virtual]

Implements CVCL::SearchEngineRules.
Definition at line 910 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::ITE_R, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::Theorem::refutes(), CVCL::TheoremProducer::withAssumptions(), and CVCL::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 CVCL::SearchEngineRules.
Definition at line 952 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::ITE_R, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::Theorem::refutes(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::propIterThen ( const Theorem & iter_th,

const Theorem & ite_th,

const Theorem & if_th

) [virtual]

Implements CVCL::SearchEngineRules.
Definition at line 999 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::ITE_R, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::Theorem::refutes(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem SearchEngineTheoremProducer::confIterThenElse ( const Theorem & iter_th,

const Theorem & ite_th,

const Theorem & then_th,

const Theorem & else_th

) [virtual]

Implements CVCL::SearchEngineRules.
Definition at line 1041 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::ITE_R, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::Theorem::refutes(), CVCL::TheoremProducer::withAssumptions(), and CVCL::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 CVCL::SearchEngineRules.
Definition at line 1088 of file search_theorem_producer.cpp.
References CVCL::Assumptions::add(), CVCL::TheoremProducer::d_em, CVCL::ExprManager::falseExpr(), CVCL::Theorem::getExpr(), CVCL::Expr::getKind(), CVCL::Theorem::getProof(), CVCL::ITE_R, CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Theorem::proves(), CVCL::Theorem::refutes(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

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

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

Implements CVCL::SearchEngineRules.
Definition at line 1192 of file search_theorem_producer.cpp.
References CVCL::AND, and opCNFRule().

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

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

Implements CVCL::SearchEngineRules.
Definition at line 1197 of file search_theorem_producer.cpp.
References opCNFRule(), and CVCL::OR.

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

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

Implements CVCL::SearchEngineRules.
Definition at line 1202 of file search_theorem_producer.cpp.
References CVCL::IMPLIES, and opCNFRule().

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

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

Implements CVCL::SearchEngineRules.
Definition at line 1207 of file search_theorem_producer.cpp.
References CVCL::IFF, and opCNFRule().

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

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

Implements CVCL::SearchEngineRules.
Definition at line 1212 of file search_theorem_producer.cpp.
References CVCL::ITE, and opCNFRule().

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

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

Implements CVCL::SearchEngineRules.
Definition at line 1218 of file search_theorem_producer.cpp.
References CVCL::Theorem::getAssumptionsCopy(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Expr::isITE(), CVCL::Expr::negate(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

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

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

Implements CVCL::SearchEngineRules.
Definition at line 1240 of file search_theorem_producer.cpp.
References CVCL::Theorem::getAssumptionsCopy(), CVCL::Theorem::getExpr(), CVCL::Theorem::getLHS(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::Expr::getType(), CVCL::Type::isBool(), CVCL::Theorem::isRewrite(), CVCL::Expr::negate(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

Theorem CVCL::SearchEngineTheoremProducer::opCNFRule ( const Theorem & thm,

int kind,

const std::string & ruleName

) [private]

Referenced by andCNFRule(), iffCNFRule(), impCNFRule(), iteCNFRule(), and orCNFRule().

Expr SearchEngineTheoremProducer::convertToCNF ( const Expr & v,

const Expr & phi

) [private]

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

Definition at line 1347 of file search_theorem_producer.cpp.
References CVCL::AND, CVCL::andExpr(), CVCL::Expr::begin(), CVCL::Expr::end(), CVCL::Expr::getKind(), CVCL::IFF, CVCL::IMPLIES, CVCL::ITE, CVCL::Expr::negate(), CVCL::OR, CVCL::orExpr(), CVCL::Expr::orExpr(), and CVCL::Expr::toString().

Expr CVCL::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))

Member Data Documentation

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

Definition at line 44 of file search_theorem_producer.h.

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

Generated on Thu Apr 13 16:57:45 2006 for CVC Lite by

1.4.4