CVC3

# Proof Rules for the Search Engines

Search Engine
Collaboration diagram for Proof Rules for the Search Engines:

## 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:

.

does not have to be present in the assumptions.

Parameters:
 a is the assumption A pfFalse is the theorem

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:

.

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

.

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

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:

.

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

.

Parameters:
 thmsA is a vector of theorems as_prove_b is the theorem (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:

.

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 CVC3::SearchEngineTheoremProducer.

 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)

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

Implemented in CVC3::SearchEngineTheoremProducer.

 virtual Theorem CVC3::SearchEngineRules::propAndrAF ( const Theorem & andr_th, bool left, const Theorem & b_th )  [pure virtual, inherited]
 virtual Theorem CVC3::SearchEngineRules::propAndrAT ( const Theorem & andr_th, const Theorem & l_th, const Theorem & r_th )  [pure virtual, inherited]
 virtual void CVC3::SearchEngineRules::propAndrLRT ( const Theorem & andr_th, const Theorem & a_th, Theorem * l_th, Theorem * r_th )  [pure virtual, inherited]
 virtual Theorem CVC3::SearchEngineRules::propAndrLF ( const Theorem & andr_th, const Theorem & a_th, const Theorem & r_th )  [pure virtual, inherited]
 virtual Theorem CVC3::SearchEngineRules::propAndrRF ( const Theorem & andr_th, const Theorem & a_th, const Theorem & l_th )  [pure virtual, inherited]
 virtual Theorem CVC3::SearchEngineRules::confAndrAT ( const Theorem & andr_th, const Theorem & a_th, bool left, const Theorem & b_th )  [pure virtual, inherited]
 virtual Theorem CVC3::SearchEngineRules::confAndrAF ( const Theorem & andr_th, const Theorem & a_th, const Theorem & l_th, const Theorem & r_th )  [pure virtual, inherited]
 virtual Theorem CVC3::SearchEngineRules::propIffr ( const Theorem & iffr_th, int p, const Theorem & a_th, const Theorem & b_th )  [pure virtual, inherited]
 virtual Theorem CVC3::SearchEngineRules::confIffr ( const Theorem & iffr_th, const Theorem & i_th, const Theorem & l_th, const Theorem & r_th )  [pure virtual, inherited]
 virtual Theorem CVC3::SearchEngineRules::propIterIte ( const Theorem & iter_th, bool left, const Theorem & if_th, const Theorem & then_th )  [pure virtual, inherited]
 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]
 virtual Theorem CVC3::SearchEngineRules::propIterThen ( const Theorem & iter_th, const Theorem & ite_th, const Theorem & if_th )  [pure virtual, inherited]
 virtual Theorem CVC3::SearchEngineRules::confIterThenElse ( const Theorem & iter_th, const Theorem & ite_th, const Theorem & then_th, const Theorem & else_th )  [pure virtual, inherited]
 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]
 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]