CVC3
Public Member Functions | Private Member Functions | Private Attributes | List of all members
CVC3::SearchEngineTheoremProducer Class Reference

#include <search_theorem_producer.h>

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

Collaboration diagram for CVC3::SearchEngineTheoremProducer:
Collaboration graph

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)
 
- Public Member Functions inherited from CVC3::SearchEngineRules
virtual ~SearchEngineRules ()
 Destructor.
 
- Public Member Functions inherited from CVC3::TheoremProducer
 TheoremProducer (TheoremManager *tm)
 
virtual ~TheoremProducer ()
 
bool withProof ()
 Testing whether to generate proofs.
 
bool withAssumptions ()
 Testing whether to generate assumptions.
 
Proof newLabel (const Expr &e)
 Create a new proof label (bound variable) for an assumption (formula)
 
Proof newPf (const std::string &name)
 
Proof newPf (const std::string &name, const Expr &e)
 
Proof newPf (const std::string &name, const Proof &pf)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2)
 
Proof newPf (const std::string &name, const Expr &e, const Proof &pf)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf)
 
Proof newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end)
 
Proof newPf (const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end)
 
Proof newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const std::vector< Expr > &args)
 
Proof newPf (const std::string &name, const Expr &e, const std::vector< Expr > &args)
 
Proof newPf (const std::string &name, const Expr &e, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const std::vector< Expr > &args, const Proof &pf)
 
Proof newPf (const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs)
 
Proof newPf (const Proof &label, const Expr &frm, const Proof &pf)
 Creating LAMBDA-abstraction (LAMBDA label formula proof)
 
Proof newPf (const Proof &label, const Proof &pf)
 Creating LAMBDA-abstraction (LAMBDA label proof).
 
Proof newPf (const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf)
 Similarly, multi-argument lambda-abstractions: (LAMBDA (u1,...,un): (f1,...,fn). pf)
 
Proof newPf (const std::vector< Proof > &labels, const Proof &pf)
 

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

CommonProofRulesd_commonRules
 

Additional Inherited Members

- Protected Member Functions inherited from CVC3::TheoremProducer
Theorem newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf)
 Create a new theorem. See also newRWTheorem() and newReflTheorem()
 
Theorem newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
 Create a rewrite theorem: lhs = rhs.
 
Theorem newReflTheorem (const Expr &e)
 Create a reflexivity theorem.
 
Theorem newAssumption (const Expr &thm, const Proof &pf, int scope=-1)
 
Theorem3 newTheorem3 (const Expr &thm, const Assumptions &assump, const Proof &pf)
 
Theorem3 newRWTheorem3 (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
 
void soundError (const std::string &file, int line, const std::string &cond, const std::string &msg)
 
- Protected Attributes inherited from CVC3::TheoremProducer
TheoremManagerd_tm
 
ExprManagerd_em
 
const bool * d_checkProofs
 
Op d_pfOp
 
Expr d_hole
 

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 ( )
inlinevirtual

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
void SearchEngineTheoremProducer::checkSoundNoSkolems ( const Theorem t,
ExprMap< bool > &  visited,
const ExprMap< bool > &  skolems 
)
private
Theorem SearchEngineTheoremProducer::proofByContradiction ( const Expr a,
const Theorem pfFalse 
)
virtual
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_ais 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$.
pfFalseis 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::Theorem::toString(), CVC3::Expr::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
ais the assumption A to split on
a_proves_cis the theorem $\Gamma_1, A\vdash C$
not_a_proves_cis 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 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
Theorem SearchEngineTheoremProducer::cutRule ( const std::vector< Theorem > &  thmsA,
const Theorem as_prove_b 
)
virtual
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
clauseis the proof of the clause $ \Gamma\vdash A_1\vee\cdots\vee A_n$
iis the index (0..n-1) of the literal to be unit-propagated
thmsis the vector of theorems $\Gamma_j\vdash\neg A_j$ for all literals except Ai

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
Theorem SearchEngineTheoremProducer::propAndrAF ( const Theorem andr_th,
bool  left,
const Theorem b_th 
)
virtual
Theorem SearchEngineTheoremProducer::propAndrAT ( const Theorem andr_th,
const Theorem l_th,
const Theorem r_th 
)
virtual
void SearchEngineTheoremProducer::propAndrLRT ( const Theorem andr_th,
const Theorem a_th,
Theorem l_th,
Theorem r_th 
)
virtual
Theorem SearchEngineTheoremProducer::propAndrLF ( const Theorem andr_th,
const Theorem a_th,
const Theorem r_th 
)
virtual
Theorem SearchEngineTheoremProducer::propAndrRF ( const Theorem andr_th,
const Theorem a_th,
const Theorem l_th 
)
virtual
Theorem SearchEngineTheoremProducer::confAndrAT ( const Theorem andr_th,
const Theorem a_th,
bool  left,
const Theorem b_th 
)
virtual
Theorem SearchEngineTheoremProducer::confAndrAF ( const Theorem andr_th,
const Theorem a_th,
const Theorem l_th,
const Theorem r_th 
)
virtual
Theorem SearchEngineTheoremProducer::propIffr ( const Theorem iffr_th,
int  p,
const Theorem a_th,
const Theorem b_th 
)
virtual
Theorem SearchEngineTheoremProducer::confIffr ( const Theorem iffr_th,
const Theorem i_th,
const Theorem l_th,
const Theorem r_th 
)
virtual
Theorem SearchEngineTheoremProducer::propIterIte ( const Theorem iter_th,
bool  left,
const Theorem if_th,
const Theorem then_th 
)
virtual
void SearchEngineTheoremProducer::propIterIfThen ( const Theorem iter_th,
bool  left,
const Theorem ite_th,
const Theorem then_th,
Theorem if_th,
Theorem else_th 
)
virtual
Theorem SearchEngineTheoremProducer::propIterThen ( const Theorem iter_th,
const Theorem ite_th,
const Theorem if_th 
)
virtual
Theorem SearchEngineTheoremProducer::confIterThenElse ( const Theorem iter_th,
const Theorem ite_th,
const Theorem then_th,
const Theorem else_th 
)
virtual
Theorem SearchEngineTheoremProducer::confIterIfThen ( const Theorem iter_th,
bool  left,
const Theorem ite_th,
const Theorem if_th,
const Theorem then_th 
)
virtual
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
Theorem SearchEngineTheoremProducer::iffToClauses ( const Theorem iff)
virtual
Theorem SearchEngineTheoremProducer::satProof ( const Expr queryExpr,
const Proof satProof 
)
virtual
Theorem SearchEngineTheoremProducer::opCNFRule ( const Theorem thm,
int  kind,
const std::string &  ruleName 
)
private
Expr SearchEngineTheoremProducer::convertToCNF ( const Expr v,
const Expr phi 
)
private
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: