CVC3::SearchEngineTheoremProducer

CVC3::SearchEngineTheoremProducer Class Reference

#include <search_theorem_producer.h>

Inheritance diagram for CVC3::SearchEngineTheoremProducer:

Inheritance graph
[legend]
Collaboration diagram for CVC3::SearchEngineTheoremProducer:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Member Functions

Private Attributes

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::getVars(), CVC3::Expr::isExists(), CVC3::Expr::isFalse(), CVC3::ExprManager::newLeafExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::skolemExpr(), 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 Ai. 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 Ai

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

Definition at line 1205 of file search_theorem_producer.cpp.

References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, convertToCNF(), CVC3::TheoremProducer::d_em, DebugAssert, CVC3::Expr::end(), CVC3::EXISTS, findInLocalCache(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::ExprManager::getKindName(), CVC3::Expr::getOp(), CVC3::Theorem::getProof(), CVC3::Expr::isIff(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().

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 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::Expr::orExpr(), CVC3::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:
Generated on Wed Nov 18 16:18:00 2009 for CVC3 by  doxygen 1.5.2