# Proof Rules for the Search Engines [Search Engine]

Collaboration diagram for Proof Rules for the Search Engines:

## Function Documentation

 virtual CVCL::SearchEngineRules::~SearchEngineRules ( )  [inline, virtual, inherited]
 Destructor. Definition at line 49 of file search_rules.h.

 virtual Theorem CVCL::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 CVCL::SearchEngineTheoremProducer. Referenced by CVCL::SearchImplBase::processResult().

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

.

does not have to be present in the assumptions.

Parameters:
 a is the assumption A pfFalse is the theorem

Implemented in CVCL::SearchEngineTheoremProducer.

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

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

Negation introduction:

.

Parameters:
 not_a is the formula . We pass the negation , and not just A, for efficiency: building is more expensive (due to uniquifying pointers in Expr package) than extracting A from . pfFalse is the theorem

Implemented in CVCL::SearchEngineTheoremProducer.

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

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

Case split:

.

Parameters:
 a is the assumption A to split on a_proves_c is the theorem not_a_proves_c is the theorem

Implemented in CVCL::SearchEngineTheoremProducer.

Referenced by CVCL::SearchSimple::checkValidRec().

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

Conflict clause rule:

.

Parameters:
 thm is the theorem lits is the vector of literals Ai. They must be present in the set of assumptions of thm. gamma FIXME: document this!!

Implemented in CVCL::SearchEngineTheoremProducer.

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

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

Cut rule:

.

Parameters:
 thmsA is a vector of theorems as_prove_b is the theorem (the name means "A's prove B")

Implemented in CVCL::SearchEngineTheoremProducer.

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

Unit propagation rule:

.

Parameters:
 clause is the proof of the clause i is the index (0..n-1) of the literal to be unit-propagated thms is the vector of theorems for all literals except Ai

Implemented in CVCL::SearchEngineTheoremProducer.

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

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

Parameters:
 clause is the proof of the clause thms is the vector of theorems

Implemented in CVCL::SearchEngineTheoremProducer.

 virtual Theorem CVCL::SearchEngineRules::propAndrAF ( const Theorem & andr_th, bool left, const Theorem & b_th )  [pure virtual, inherited]
 Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual Theorem CVCL::SearchEngineRules::propAndrAT ( const Theorem & andr_th, const Theorem & l_th, const Theorem & r_th )  [pure virtual, inherited]
 Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual void CVCL::SearchEngineRules::propAndrLRT ( const Theorem & andr_th, const Theorem & a_th, Theorem * l_th, Theorem * r_th )  [pure virtual, inherited]
 Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual Theorem CVCL::SearchEngineRules::propAndrLF ( const Theorem & andr_th, const Theorem & a_th, const Theorem & r_th )  [pure virtual, inherited]
 Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual Theorem CVCL::SearchEngineRules::propAndrRF ( const Theorem & andr_th, const Theorem & a_th, const Theorem & l_th )  [pure virtual, inherited]
 Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual Theorem CVCL::SearchEngineRules::confAndrAT ( const Theorem & andr_th, const Theorem & a_th, bool left, const Theorem & b_th )  [pure virtual, inherited]
 Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual Theorem CVCL::SearchEngineRules::confAndrAF ( const Theorem & andr_th, const Theorem & a_th, const Theorem & l_th, const Theorem & r_th )  [pure virtual, inherited]
 Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual Theorem CVCL::SearchEngineRules::propIffr ( const Theorem & iffr_th, int p, const Theorem & a_th, const Theorem & b_th )  [pure virtual, inherited]
 Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual Theorem CVCL::SearchEngineRules::confIffr ( const Theorem & iffr_th, const Theorem & i_th, const Theorem & l_th, const Theorem & r_th )  [pure virtual, inherited]
 Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual Theorem CVCL::SearchEngineRules::propIterIte ( const Theorem & iter_th, bool left, const Theorem & if_th, const Theorem & then_th )  [pure virtual, inherited]
 Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual void CVCL::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 CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual Theorem CVCL::SearchEngineRules::propIterThen ( const Theorem & iter_th, const Theorem & ite_th, const Theorem & if_th )  [pure virtual, inherited]
 Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual Theorem CVCL::SearchEngineRules::confIterThenElse ( const Theorem & iter_th, const Theorem & ite_th, const Theorem & then_th, const Theorem & else_th )  [pure virtual, inherited]
 Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual Theorem CVCL::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 CVCL::SearchEngineTheoremProducer. Referenced by CVCL::Circuit::propagate().

 virtual Theorem CVCL::SearchEngineRules::andCNFRule ( const Theorem & thm )  [pure virtual, inherited]
 AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v]. Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::SearchImplBase::applyCNFRules().

 virtual Theorem CVCL::SearchEngineRules::orCNFRule ( const Theorem & thm )  [pure virtual, inherited]
 OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v]. Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::SearchImplBase::applyCNFRules().

 virtual Theorem CVCL::SearchEngineRules::impCNFRule ( const Theorem & thm )  [pure virtual, inherited]
 (x1 => x2) <=> v |- CNF[(x1 => x2) <=> v] Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::SearchImplBase::applyCNFRules().

 virtual Theorem CVCL::SearchEngineRules::iffCNFRule ( const Theorem & thm )  [pure virtual, inherited]
 (x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v] Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::SearchImplBase::applyCNFRules().

 virtual Theorem CVCL::SearchEngineRules::iteCNFRule ( const Theorem & thm )  [pure virtual, inherited]
 ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v]. Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::SearchImplBase::applyCNFRules().

 virtual Theorem CVCL::SearchEngineRules::iteToClauses ( const Theorem & ite )  [pure virtual, inherited]
 ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2). Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::SearchImplBase::enqueueCNFrec().

 virtual Theorem CVCL::SearchEngineRules::iffToClauses ( const Theorem & iff )  [pure virtual, inherited]
 e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2) Implemented in CVCL::SearchEngineTheoremProducer. Referenced by CVCL::SearchImplBase::applyCNFRules().

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