CVC3
2.4.1
|
#include <search_theorem_producer.h>
SearchEngineTheoremProducer::SearchEngineTheoremProducer | ( | TheoremManager * | tm | ) |
Definition at line 62 of file search_theorem_producer.cpp.
virtual CVC3::SearchEngineTheoremProducer::~SearchEngineTheoremProducer | ( | ) | [inline, virtual] |
Definition at line 48 of file search_theorem_producer.h.
void SearchEngineTheoremProducer::verifyConflict | ( | const Theorem & | thm, |
TheoremMap & | m | ||
) | [private] |
Definition at line 192 of file search_theorem_producer.cpp.
References CVC3::Theorem::getAssumptionsRef(), CVC3::Assumptions::end(), and CHECK_SOUND.
Referenced by conflictClause().
void SearchEngineTheoremProducer::checkSoundNoSkolems | ( | const Expr & | e, |
ExprMap< bool > & | visited, | ||
const ExprMap< bool > & | skolems | ||
) | [private] |
Definition at line 411 of file search_theorem_producer.cpp.
References CVC3::ExprMap::count(), CHECK_SOUND, CVC3::Expr::toString(), CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::getKind(), FORALL, EXISTS, and CVC3::Expr::getBody().
Referenced by checkSoundNoSkolems(), and eliminateSkolemAxioms().
void SearchEngineTheoremProducer::checkSoundNoSkolems | ( | const Theorem & | t, |
ExprMap< bool > & | visited, | ||
const ExprMap< bool > & | skolems | ||
) | [private] |
Definition at line 429 of file search_theorem_producer.cpp.
References CVC3::Theorem::isRefl(), CVC3::Theorem::isFlagged(), CVC3::Theorem::setFlag(), CVC3::Theorem::isAssump(), checkSoundNoSkolems(), CVC3::Theorem::getExpr(), CVC3::Theorem::getAssumptionsRef(), and CVC3::Assumptions::begin().
Theorem SearchEngineTheoremProducer::proofByContradiction | ( | const Expr & | a, |
const Theorem & | pfFalse | ||
) | [virtual] |
Proof by contradiction:
.
does not have to be present in the assumptions.
a | is the assumption A |
pfFalse | is the theorem ![]() |
Implements CVC3::SearchEngineRules.
Definition at line 74 of file search_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Expr::isFalse(), CVC3::Theorem::toString(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::Theorem::getProof(), lfsc_called, satProof(), and CVC3::TheoremProducer::newTheorem().
Theorem SearchEngineTheoremProducer::negIntro | ( | const Expr & | not_a, |
const Theorem & | pfFalse | ||
) | [virtual] |
Negation introduction:
.
not_a | is the formula ![]() ![]() ![]() ![]() |
pfFalse | is the theorem ![]() |
Implements CVC3::SearchEngineRules.
Definition at line 105 of file search_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Expr::isFalse(), CVC3::Theorem::toString(), CVC3::Expr::isNot(), CVC3::Expr::toString(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::Theorem::getProof(), and CVC3::TheoremProducer::newTheorem().
Theorem SearchEngineTheoremProducer::caseSplit | ( | const Expr & | a, |
const Theorem & | a_proves_c, | ||
const Theorem & | not_a_proves_c | ||
) | [virtual] |
Case split:
.
a | is the assumption A to split on |
a_proves_c | is the theorem ![]() |
not_a_proves_c | is the theorem ![]() |
Implements CVC3::SearchEngineRules.
Definition at line 135 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::toString(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::Theorem::getProof(), and CVC3::TheoremProducer::newTheorem().
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 TRACE, CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::isFalse(), CVC3::TheoremProducer::d_em, CVC3::ExprManager::newLeafExpr(), CVC3::Theorem::clearAllFlags(), checkSoundNoSkolems(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::Theorem::getAssumptionsRef().
Theorem SearchEngineTheoremProducer::conflictClause | ( | const Theorem & | thm, |
const std::vector< Theorem > & | lits, | ||
const std::vector< Theorem > & | gamma | ||
) | [virtual] |
Conflict clause rule:
.
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!! |
Implements CVC3::SearchEngineRules.
Definition at line 221 of file search_theorem_producer.cpp.
References IF_DEBUG, std::endl(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::withAssumptions(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::clearAllFlags(), verifyConflict(), CVC3::Theorem::getExpr(), CVC3::Expr::isFalse(), DebugAssert, CVC3::Proof::getExpr(), CVC3::Expr::isVar(), CVC3::TheoremProducer::newLabel(), CVC3::Theorem::getProof(), CVC3::ExprHashMap::empty(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), OR, and CVC3::TheoremProducer::d_em.
Theorem SearchEngineTheoremProducer::cutRule | ( | const std::vector< Theorem > & | thmsA, |
const Theorem & | as_prove_b | ||
) | [virtual] |
Cut rule:
.
thmsA | is a vector of theorems ![]() |
as_prove_b | is the theorem ![]() |
Implements CVC3::SearchEngineRules.
Definition at line 375 of file search_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::withAssumptions(), CVC3::Assumptions::add(), CVC3::Theorem::getAssumptionsRef(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), and CVC3::TheoremProducer::newTheorem().
Theorem SearchEngineTheoremProducer::unitProp | ( | const std::vector< Theorem > & | thms, |
const Theorem & | clause, | ||
unsigned | i | ||
) | [virtual] |
Unit propagation rule:
.
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 ![]() |
Implements CVC3::SearchEngineRules.
Definition at line 511 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::int2string(), CVC3::Theorem::toString(), CVC3::Expr::isNot(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), and CVC3::TheoremProducer::newTheorem().
Theorem SearchEngineTheoremProducer::conflictRule | ( | const std::vector< Theorem > & | thms, |
const Theorem & | clause | ||
) | [virtual] |
"Conflict" rule (all literals in a clause become FALSE)
clause | is the proof of the clause ![]() |
thms | is the vector of theorems ![]() |
Implements CVC3::SearchEngineRules.
Definition at line 1109 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::toString(), CVC3::int2string(), CVC3::Expr::isNot(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::d_em, and CVC3::ExprManager::falseExpr().
Theorem SearchEngineTheoremProducer::propAndrAF | ( | const Theorem & | andr_th, |
bool | left, | ||
const Theorem & | b_th | ||
) | [virtual] |
Implements CVC3::SearchEngineRules.
Definition at line 564 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, AND_R, CVC3::Theorem::refutes(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), and CVC3::TheoremProducer::newTheorem().
Theorem SearchEngineTheoremProducer::propAndrAT | ( | const Theorem & | andr_th, |
const Theorem & | l_th, | ||
const Theorem & | r_th | ||
) | [virtual] |
Implements CVC3::SearchEngineRules.
Definition at line 593 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, AND_R, CVC3::Theorem::proves(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), and CVC3::TheoremProducer::newTheorem().
void SearchEngineTheoremProducer::propAndrLRT | ( | const Theorem & | andr_th, |
const Theorem & | a_th, | ||
Theorem * | l_th, | ||
Theorem * | r_th | ||
) | [virtual] |
Implements CVC3::SearchEngineRules.
Definition at line 623 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, AND_R, CVC3::Theorem::proves(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), and CVC3::TheoremProducer::newTheorem().
Theorem SearchEngineTheoremProducer::propAndrLF | ( | const Theorem & | andr_th, |
const Theorem & | a_th, | ||
const Theorem & | r_th | ||
) | [virtual] |
Implements CVC3::SearchEngineRules.
Definition at line 651 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, AND_R, CVC3::Theorem::refutes(), CVC3::Theorem::proves(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), and CVC3::TheoremProducer::newTheorem().
Theorem SearchEngineTheoremProducer::propAndrRF | ( | const Theorem & | andr_th, |
const Theorem & | a_th, | ||
const Theorem & | l_th | ||
) | [virtual] |
Implements CVC3::SearchEngineRules.
Definition at line 681 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, AND_R, CVC3::Theorem::refutes(), CVC3::Theorem::proves(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), and CVC3::TheoremProducer::newTheorem().
Theorem SearchEngineTheoremProducer::confAndrAT | ( | const Theorem & | andr_th, |
const Theorem & | a_th, | ||
bool | left, | ||
const Theorem & | b_th | ||
) | [virtual] |
Implements CVC3::SearchEngineRules.
Definition at line 711 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, AND_R, CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::d_em, and CVC3::ExprManager::falseExpr().
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 744 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, AND_R, CVC3::Theorem::refutes(), CVC3::Theorem::proves(), CVC3::TheoremProducer::withAssumptions(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::d_em, and CVC3::ExprManager::falseExpr().
Theorem SearchEngineTheoremProducer::propIffr | ( | const Theorem & | iffr_th, |
int | p, | ||
const Theorem & | a_th, | ||
const Theorem & | b_th | ||
) | [virtual] |
Implements CVC3::SearchEngineRules.
Definition at line 782 of file search_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::int2string(), CVC3::Theorem::getExpr(), CVC3::Theorem::proves(), IFF_R, CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), and CVC3::TheoremProducer::newTheorem().
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 834 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CVC3::Theorem::proves(), CHECK_PROOFS, CHECK_SOUND, IFF_R, CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::d_em, and CVC3::ExprManager::falseExpr().
Theorem SearchEngineTheoremProducer::propIterIte | ( | const Theorem & | iter_th, |
bool | left, | ||
const Theorem & | if_th, | ||
const Theorem & | then_th | ||
) | [virtual] |
Implements CVC3::SearchEngineRules.
Definition at line 881 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CVC3::Theorem::proves(), CHECK_PROOFS, CHECK_SOUND, ITE_R, CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), and CVC3::TheoremProducer::newTheorem().
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 923 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CVC3::Theorem::proves(), CHECK_PROOFS, CHECK_SOUND, ITE_R, CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), and CVC3::TheoremProducer::newTheorem().
Theorem SearchEngineTheoremProducer::propIterThen | ( | const Theorem & | iter_th, |
const Theorem & | ite_th, | ||
const Theorem & | if_th | ||
) | [virtual] |
Implements CVC3::SearchEngineRules.
Definition at line 970 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CVC3::Theorem::proves(), CHECK_PROOFS, CHECK_SOUND, ITE_R, CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), and CVC3::TheoremProducer::newTheorem().
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 1012 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CVC3::Theorem::proves(), CHECK_PROOFS, CHECK_SOUND, ITE_R, CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::d_em, and CVC3::ExprManager::falseExpr().
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 1059 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CVC3::Theorem::proves(), CHECK_PROOFS, CHECK_SOUND, ITE_R, CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), CVC3::Assumptions::add(), CVC3::TheoremProducer::withProof(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::TheoremProducer::d_em, and CVC3::ExprManager::falseExpr().
AND(x1,...,xn) <=> v |- CNF[AND(x1,...,xn) <=> v].
Implements CVC3::SearchEngineRules.
Definition at line 1160 of file search_theorem_producer.cpp.
References opCNFRule(), and AND.
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.
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v]
Implements CVC3::SearchEngineRules.
Definition at line 1170 of file search_theorem_producer.cpp.
References opCNFRule(), and IMPLIES.
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
Implements CVC3::SearchEngineRules.
Definition at line 1175 of file search_theorem_producer.cpp.
References opCNFRule(), and IFF.
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 opCNFRule(), and ITE.
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2)
Implements CVC3::SearchEngineRules.
Definition at line 1186 of file search_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::isITE(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::toString(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::negate(), and CVC3::Theorem::getAssumptionsRef().
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2)
Implements CVC3::SearchEngineRules.
Definition at line 1206 of file search_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::isRewrite(), CVC3::Theorem::getLHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Theorem::getExpr(), CVC3::Expr::toString(), CVC3::Theorem::getRHS(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::negate(), and CVC3::Theorem::getAssumptionsRef().
Theorem SearchEngineTheoremProducer::satProof | ( | const Expr & | queryExpr, |
const Proof & | satProof | ||
) | [virtual] |
Implements CVC3::SearchEngineRules.
Definition at line 1419 of file search_theorem_producer.cpp.
References CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::d_tm, CVC3::TheoremManager::getFlags(), lfsc_called, search_engine, CVC3::SearchEngine::getUserAssumptions(), CVC3::Proof::getExpr(), std::endl(), d_commonRules, LFSCPrinter::print_LFSC(), CVC3::TheoremProducer::newTheorem(), and CVC3::Assumptions::emptyAssump().
Referenced by proofByContradiction().
Theorem SearchEngineTheoremProducer::opCNFRule | ( | const Theorem & | thm, |
int | kind, | ||
const std::string & | ruleName | ||
) | [private] |
Definition at line 1226 of file search_theorem_producer.cpp.
References TRACE, CVC3::TheoremProducer::d_em, CVC3::ExprManager::getKindName(), CVC3::Theorem::getExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::isIff(), CVC3::Expr::toString(), CVC3::Expr::end(), CVC3::Expr::begin(), CVC3::Expr::isNot(), CVC3::Expr::isPropAtom(), findInLocalCache(), CVC3::ExprMap::begin(), DebugAssert, CVC3::Expr::arity(), CVC3::Expr::getOp(), convertToCNF(), CVC3::ExprManager::newClosureExpr(), EXISTS, CVC3::andExpr(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newTheorem(), and CVC3::Theorem::getAssumptionsRef().
Referenced by andCNFRule(), orCNFRule(), impCNFRule(), iffCNFRule(), and iteCNFRule().
produces the CNF for the formula v <==> phi
Definition at line 1309 of file search_theorem_producer.cpp.
References CVC3::Expr::begin(), CVC3::Expr::end(), CVC3::Expr::getKind(), AND, CVC3::Expr::negate(), CVC3::orExpr(), OR, CVC3::Expr::orExpr(), IFF, IMPLIES, ITE, DebugAssert, CVC3::Expr::toString(), and CVC3::andExpr().
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 1382 of file search_theorem_producer.cpp.
References TRACE, CVC3::Expr::toString(), CVC3::Expr::isNot(), CVC3::ExprMap::find(), CVC3::ExprMap::end(), IF_DEBUG, CVC3::TheoremProducer::d_em, CVC3::ExprManager::newBoundVarExpr(), CVC3::Expr::getType(), and CVC3::Expr::iffExpr().
Referenced by opCNFRule().
Definition at line 36 of file search_theorem_producer.h.
Referenced by satProof().