CVC3
2.4.1
|
#include <search_theorem_producer.h>
Public Member Functions | |
SearchEngineTheoremProducer (TheoremManager *tm) | |
virtual | ~SearchEngineTheoremProducer () |
virtual Theorem | proofByContradiction (const Expr &a, const Theorem &pfFalse) |
Proof by contradiction:
. More... | |
virtual Theorem | negIntro (const Expr ¬_a, const Theorem &pfFalse) |
Negation introduction:
. More... | |
virtual Theorem | caseSplit (const Expr &a, const Theorem &a_proves_c, const Theorem ¬_a_proves_c) |
Case split:
. More... | |
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:
. More... | |
virtual Theorem | cutRule (const std::vector< Theorem > &thmsA, const Theorem &as_prove_b) |
Cut rule:
. More... | |
virtual Theorem | unitProp (const std::vector< Theorem > &thms, const Theorem &clause, unsigned i) |
Unit propagation rule:
. More... | |
virtual Theorem | conflictRule (const std::vector< Theorem > &thms, const Theorem &clause) |
"Conflict" rule (all literals in a clause become 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]. More... | |
Theorem | orCNFRule (const Theorem &thm) |
OR(x1,...,xn) <=> v |- CNF[OR(x1,...,xn) <=> v]. More... | |
Theorem | impCNFRule (const Theorem &thm) |
(x1 => x2) <=> v |- CNF[(x1 => x2) <=> v] More... | |
Theorem | iffCNFRule (const Theorem &thm) |
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v] More... | |
Theorem | iteCNFRule (const Theorem &thm) |
ITE(c, x1, x2) <=> v |- CNF[ITE(c, x1, x2) <=> v]. More... | |
Theorem | iteToClauses (const Theorem &ite) |
ITE(c, f1, f2) |- (NOT c OR f1) AND (c OR f2) More... | |
Theorem | iffToClauses (const Theorem &iff) |
e1 <=> e2 |- (NOT e1 OR e2) AND (e1 OR NOT e2) More... | |
Theorem | satProof (const Expr &queryExpr, const Proof &satProof) |
![]() | |
virtual | ~SearchEngineRules () |
Destructor. More... | |
![]() | |
TheoremProducer (TheoremManager *tm) | |
virtual | ~TheoremProducer () |
bool | withProof () |
Testing whether to generate proofs. More... | |
bool | withAssumptions () |
Testing whether to generate assumptions. More... | |
Proof | newLabel (const Expr &e) |
Create a new proof label (bound variable) for an assumption (formula) More... | |
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) More... | |
Proof | newPf (const Proof &label, const Proof &pf) |
Creating LAMBDA-abstraction (LAMBDA label proof). More... | |
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) More... | |
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 More... | |
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. More... | |
Private Attributes | |
CommonProofRules * | d_commonRules |
Additional Inherited Members | |
![]() | |
Theorem | newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf) |
Create a new theorem. See also newRWTheorem() and newReflTheorem() More... | |
Theorem | newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) |
Create a rewrite theorem: lhs = rhs. More... | |
Theorem | newReflTheorem (const Expr &e) |
Create a reflexivity theorem. More... | |
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) |
![]() | |
TheoremManager * | d_tm |
ExprManager * | d_em |
const bool * | d_checkProofs |
Op | d_pfOp |
Expr | d_hole |
Definition at line 32 of file search_theorem_producer.h.
SearchEngineTheoremProducer::SearchEngineTheoremProducer | ( | TheoremManager * | tm | ) |
Definition at line 62 of file search_theorem_producer.cpp.
|
inlinevirtual |
Definition at line 48 of file search_theorem_producer.h.
|
private |
Definition at line 192 of file search_theorem_producer.cpp.
References CHECK_SOUND, and CVC3::Theorem::getAssumptionsRef().
Referenced by conflictClause().
|
private |
Definition at line 411 of file search_theorem_producer.cpp.
References CVC3::Expr::begin(), CHECK_SOUND, CVC3::ExprMap< Data >::count(), CVC3::Expr::end(), EXISTS, FORALL, CVC3::Expr::getBody(), CVC3::Expr::getKind(), and CVC3::Expr::toString().
Referenced by checkSoundNoSkolems(), and eliminateSkolemAxioms().
|
private |
Definition at line 429 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().
|
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::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isFalse(), lfsc_called, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), satProof(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().
|
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::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().
|
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 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().
|
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().
|
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 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(), OR, verifyConflict(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().
|
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 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().
|
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::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().
|
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::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().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 564 of file search_theorem_producer.cpp.
References 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().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 593 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), 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().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 623 of file search_theorem_producer.cpp.
References 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().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 651 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), 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().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 681 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), 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().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 711 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), 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().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 744 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), 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().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 782 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), IFF_R, CVC3::int2string(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 834 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(), IFF_R, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 881 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), ITE_R, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 923 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), ITE_R, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 970 of file search_theorem_producer.cpp.
References CVC3::Assumptions::add(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), ITE_R, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 1012 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(), ITE_R, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 1059 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(), ITE_R, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::proves(), CVC3::Theorem::refutes(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().
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().
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 IMPLIES, and opCNFRule().
(x1 <=> x2) <=> v |- CNF[(x1 <=> x2) <=> v]
Implements CVC3::SearchEngineRules.
Definition at line 1175 of file search_theorem_producer.cpp.
References IFF, and opCNFRule().
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().
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 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().
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::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().
|
virtual |
Implements CVC3::SearchEngineRules.
Definition at line 1419 of file search_theorem_producer.cpp.
References d_commonRules, CVC3::TheoremProducer::d_tm, CVC3::Assumptions::emptyAssump(), std::endl(), CVC3::Proof::getExpr(), CVC3::TheoremManager::getFlags(), CVC3::SearchEngine::getUserAssumptions(), lfsc_called, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), LFSCPrinter::print_LFSC(), search_engine, and CVC3::TheoremProducer::withProof().
Referenced by proofByContradiction().
|
private |
Definition at line 1226 of file search_theorem_producer.cpp.
References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, convertToCNF(), CVC3::TheoremProducer::d_em, DebugAssert, CVC3::Expr::end(), 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(), TRACE, and CVC3::TheoremProducer::withProof().
Referenced by andCNFRule(), iffCNFRule(), impCNFRule(), iteCNFRule(), and orCNFRule().
produces the CNF for the formula v <==> phi
Definition at line 1309 of file search_theorem_producer.cpp.
References AND, CVC3::andExpr(), CVC3::Expr::begin(), DebugAssert, CVC3::Expr::end(), CVC3::Expr::getKind(), IFF, IMPLIES, ITE, CVC3::Expr::negate(), OR, CVC3::Expr::orExpr(), CVC3::orExpr(), and CVC3::Expr::toString().
Referenced by opCNFRule().
|
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().
|
private |
Definition at line 36 of file search_theorem_producer.h.
Referenced by satProof().