#include <search_theorem_producer.h>
Definition at line 32 of file search_theorem_producer.h.
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.
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::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] |
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] |
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] |
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.
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::isFalse(), CVC3::ExprManager::newLeafExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().
Theorem SearchEngineTheoremProducer::conflictClause | ( | const Theorem & | thm, | |
const std::vector< Theorem > & | lits, | |||
const std::vector< Theorem > & | gamma | |||
) | [virtual] |
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(), 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] |
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] |
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::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] |
Definition at line 1088 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::int2string(), CVC3::Expr::isNot(), 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] |
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] |
Definition at line 572 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), 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] |
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] |
Definition at line 630 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), 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] |
Definition at line 660 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), 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] |
Definition at line 690 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), 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] |
Definition at line 723 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), 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] |
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::int2string(), 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] |
Definition at line 813 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::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] |
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] |
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] |
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] |
Definition at line 991 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::confIterIfThen | ( | const Theorem & | iter_th, | |
bool | left, | |||
const Theorem & | ite_th, | |||
const Theorem & | if_th, | |||
const Theorem & | then_th | |||
) | [virtual] |
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().
Definition at line 1139 of file search_theorem_producer.cpp.
References CVC3::AND, and opCNFRule().
Definition at line 1144 of file search_theorem_producer.cpp.
References opCNFRule(), and CVC3::OR.
Definition at line 1149 of file search_theorem_producer.cpp.
References CVC3::IMPLIES, and opCNFRule().
Definition at line 1154 of file search_theorem_producer.cpp.
References CVC3::IFF, and opCNFRule().
Definition at line 1159 of file search_theorem_producer.cpp.
References CVC3::ITE, and opCNFRule().
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::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
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().
Definition at line 1559 of file search_theorem_producer.cpp.
References CVC3::ExprMap< Data >::begin(), collectVars(), CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), 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::Expr::isNot(), CVC3::Expr::isPropAtom(), 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().
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::orExpr(), CVC3::Expr::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().
Definition at line 36 of file search_theorem_producer.h.