CVC3
2.4.1
|
#include <common_theorem_producer.h>
Public Member Functions | |
CommonTheoremProducer (TheoremManager *tm) | |
virtual | ~CommonTheoremProducer () |
Theorem3 | queryTCC (const Theorem &phi, const Theorem &D_phi) |
Convert 2-valued formula to 3-valued by discharging its TCC ( ![]()
| |
Theorem3 | implIntro3 (const Theorem3 &phi, const std::vector< Expr > &assump, const std::vector< Theorem > &tccs) |
3-valued implication introduction rule:
| |
Theorem | assumpRule (const Expr &a, int scope=-1) |
| |
Theorem | reflexivityRule (const Expr &a) |
| |
Theorem | rewriteReflexivity (const Expr &t) |
==> (a == a) IFF TRUE | |
Theorem | symmetryRule (const Theorem &a1_eq_a2) |
| |
Theorem | rewriteUsingSymmetry (const Expr &a1_eq_a2) |
| |
Theorem | transitivityRule (const Theorem &a1_eq_a2, const Theorem &a2_eq_a3) |
| |
Theorem | substitutivityRule (const Expr &e, const Theorem &thm) |
Optimized case for expr with one child. | |
Theorem | substitutivityRule (const Expr &e, const Theorem &thm1, const Theorem &thm2) |
Optimized case for expr with two children. | |
Theorem | substitutivityRule (const Op &op, const std::vector< Theorem > &thms) |
| |
Theorem | substitutivityRule (const Expr &e, const std::vector< unsigned > &changed, const std::vector< Theorem > &thms) |
| |
Theorem | substitutivityRule (const Expr &e, const int changed, const Theorem &thm) |
Theorem | contradictionRule (const Theorem &e, const Theorem ¬_e) |
| |
Theorem | excludedMiddle (const Expr &e) |
Theorem | iffTrue (const Theorem &e) |
| |
Theorem | iffNotFalse (const Theorem &e) |
| |
Theorem | iffTrueElim (const Theorem &e) |
| |
Theorem | iffFalseElim (const Theorem &e) |
| |
Theorem | iffContrapositive (const Theorem &thm) |
e1 <=> e2 ==> ~e1 <=> ~e2 | |
Theorem | notNotElim (const Theorem &e) |
| |
Theorem | iffMP (const Theorem &e1, const Theorem &e1_iff_e2) |
| |
Theorem | implMP (const Theorem &e1, const Theorem &e1_impl_e2) |
| |
Theorem | andElim (const Theorem &e, int i) |
| |
Theorem | andIntro (const Theorem &e1, const Theorem &e2) |
e1, e2 ==> AND(e1, e2) | |
Theorem | andIntro (const std::vector< Theorem > &es) |
| |
Theorem | implIntro (const Theorem &phi, const std::vector< Expr > &assump) |
Implication introduction rule:
| |
Theorem | implContrapositive (const Theorem &thm) |
e1 => e2 ==> ~e2 => ~e1 | |
Theorem | rewriteIteTrue (const Expr &e) |
==> ITE(TRUE, e1, e2) == e1 | |
Theorem | rewriteIteFalse (const Expr &e) |
==> ITE(FALSE, e1, e2) == e2 | |
Theorem | rewriteIteSame (const Expr &e) |
==> ITE(c, e, e) == e | |
Theorem | notToIff (const Theorem ¬_e) |
| |
Theorem | xorToIff (const Expr &e) |
| |
Theorem | rewriteIff (const Expr &e) |
==> (e1 <=> e2) <=> [simplified expr] | |
Theorem | rewriteAnd (const Expr &e) |
==> AND(e1,e2) IFF [simplified expr] | |
Theorem | rewriteOr (const Expr &e) |
==> OR(e1,...,en) IFF [simplified expr] | |
Theorem | rewriteNotTrue (const Expr &e) |
==> NOT TRUE IFF FALSE | |
Theorem | rewriteNotFalse (const Expr &e) |
==> NOT FALSE IFF TRUE | |
Theorem | rewriteNotNot (const Expr &e) |
==> NOT NOT e IFF e, takes !!e | |
Theorem | rewriteNotForall (const Expr &forallExpr) |
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e | |
Theorem | rewriteNotExists (const Expr &existsExpr) |
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e | |
Expr | skolemize (const Expr &e) |
Theorem | skolemizeRewrite (const Expr &e) |
Theorem | skolemizeRewriteVar (const Expr &e) |
Special version of skolemizeRewrite for "EXISTS x. t = x". | |
Theorem | varIntroRule (const Expr &e) |
|- EXISTS x. e = x | |
Theorem | skolemize (const Theorem &thm) |
If thm is (EXISTS x: phi(x)), create the Skolemized version and add it to the database. Otherwise returns just thm. | |
Theorem | varIntroSkolem (const Expr &e) |
Retrun a theorem "|- e = v" for a new Skolem constant v. | |
Theorem | trueTheorem () |
==> TRUE | |
Theorem | rewriteAnd (const Theorem &e) |
AND(e1,e2) ==> [simplified expr]. | |
Theorem | rewriteOr (const Theorem &e) |
OR(e1,...,en) ==> [simplified expr]. | |
Theorem | ackermann (const Expr &e1, const Expr &e2) |
Theorem | liftOneITE (const Expr &e) |
std::vector< Theorem > & | getSkolemAxioms () |
void | clearSkolemAxioms () |
![]() | |
virtual | ~CommonProofRules () |
Destructor. | |
![]() | |
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 | findITE (const Expr &e, Expr &condition, Expr &thenpart, Expr &elsepart) |
Helper function for liftOneITE. |
Private Attributes | |
std::vector< Theorem > | d_skolem_axioms |
CDMap< Expr, Theorem > | d_skolemized_thms |
CDMap< Expr, Theorem > | d_skolemVars |
Mapping of e to "|- e = v" for fresh Skolem vars v. |
Additional Inherited Members | |
![]() | |
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) |
![]() | |
TheoremManager * | d_tm |
ExprManager * | d_em |
const bool * | d_checkProofs |
Op | d_pfOp |
Expr | d_hole |
Definition at line 40 of file common_theorem_producer.h.
CommonTheoremProducer::CommonTheoremProducer | ( | TheoremManager * | tm | ) |
Definition at line 40 of file common_theorem_producer.cpp.
|
inlinevirtual |
Definition at line 60 of file common_theorem_producer.h.
|
private |
Helper function for liftOneITE.
Definition at line 1322 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::containsTermITE(), CVC3::Expr::getOp(), CVC3::Expr::getType(), CVC3::Type::isBool(), and CVC3::Expr::isITE().
Referenced by liftOneITE().
Convert 2-valued formula to 3-valued by discharging its TCC ( ):
.
Implements CVC3::CommonProofRules.
Definition at line 55 of file common_theorem_producer.cpp.
References CVC3::Assumptions::add(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem3(), and CVC3::TheoremProducer::withProof().
|
virtual |
3-valued implication introduction rule:
\param phi is the formula \form#0 \param assump is the vector of assumptions \form#235 \param tccs is the vector of TCCs for assumptions
Implements CVC3::CommonProofRules.
Definition at line 85 of file common_theorem_producer.cpp.
References CVC3::Assumptions::add(), CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem3::getAssumptionsRef(), CVC3::Theorem3::getExpr(), CVC3::Theorem::getProof(), CVC3::Theorem3::getProof(), CVC3::Expr::impExpr(), CVC3::int2string(), CVC3::Theorem::isAssump(), CVC3::Theorem::isNull(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem3(), CVC3::Expr::toString(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 154 of file common_theorem_producer.cpp.
References CVC3::TheoremProducer::newAssumption(), CVC3::TheoremProducer::newLabel(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 162 of file common_theorem_producer.cpp.
References CVC3::TheoremProducer::newReflTheorem().
Referenced by rewriteIff(), rewriteUsingSymmetry(), substitutivityRule(), symmetryRule(), transitivityRule(), and trueTheorem().
==> (a == a) IFF TRUE
Implements CVC3::CommonProofRules.
Definition at line 168 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isEq(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Referenced by rewriteIff().
(same for IFF)
Implements CVC3::CommonProofRules.
Definition at line 187 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Type::getExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), IF_DEBUG, CVC3::Type::isBool(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 221 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Type::getExpr(), CVC3::Expr::iffExpr(), CVC3::Expr::isEq(), CVC3::Expr::isIff(), CVC3::Type::isNull(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), reflexivityRule(), and CVC3::TheoremProducer::withProof().
Referenced by rewriteIff().
|
virtual |
(same for IFF)
Implements CVC3::CommonProofRules.
Definition at line 245 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Type::getExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Type::isNull(), CVC3::Theorem::isNull(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), reflexivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Optimized case for expr with one child.
Implements CVC3::CommonProofRules.
Definition at line 302 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Expr::getOp(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), IF_DEBUG, CVC3::Theorem::isRefl(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theorem::setSubst(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by substitutivityRule().
|
virtual |
Optimized case for expr with two children.
Implements CVC3::CommonProofRules.
Definition at line 332 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Expr::getOp(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), IF_DEBUG, CVC3::Theorem::isRefl(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theorem::setSubst(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::CommonProofRules.
Definition at line 373 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_tm, CVC3::TheoremManager::getEM(), IF_DEBUG, CVC3::ExprManager::newLeafExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), reflexivityRule(), CVC3::Theorem::setSubst(), CVC3::Op::toString(), and CVC3::TheoremProducer::withProof().
|
virtual |
except that only those arguments are given that .
e | is the original expression ![]() |
changed | is the vector of indices of changed kids |
thms | are the theorems ![]() |
Implements CVC3::CommonProofRules.
Definition at line 424 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Expr::getOp(), IF_DEBUG, CVC3::Theorem::isRefl(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), reflexivityRule(), CVC3::Theorem::setSubst(), substitutivityRule(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::CommonProofRules.
Definition at line 509 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, DebugAssert, std::endl(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Expr::getOp(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), IF_DEBUG, CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theorem::setSubst(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::CommonProofRules.
Definition at line 561 of file common_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().
Implements CVC3::CommonProofRules.
Definition at line 580 of file common_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::orExpr(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 591 of file common_theorem_producer.cpp.
References CVC3::TheoremProducer::d_em, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 602 of file common_theorem_producer.cpp.
References CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 612 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), CVC3::Expr::isTrue(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().
Referenced by trueTheorem().
Implements CVC3::CommonProofRules.
Definition at line 626 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::isFalse(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().
e1 <=> e2 ==> ~e1 <=> ~e2
Where ~e is the inverse of e (that is, ~(!e') = e').
Implements CVC3::CommonProofRules.
Definition at line 641 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, 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::newRWTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 655 of file common_theorem_producer.cpp.
References 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().
Implements CVC3::CommonProofRules.
Definition at line 667 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().
Referenced by rewriteAnd(), rewriteOr(), skolemize(), and varIntroSkolem().
Implements CVC3::CommonProofRules.
Definition at line 692 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isImpl(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 718 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::int2string(), CVC3::Expr::isAnd(), CVC3::TheoremProducer::newPf(), CVC3::ExprManager::newRatExpr(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().
e1, e2 ==> AND(e1, e2)
Implements CVC3::CommonProofRules.
Definition at line 733 of file common_theorem_producer.cpp.
Implements CVC3::CommonProofRules.
Definition at line 741 of file common_theorem_producer.cpp.
References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().
|
virtual |
Implication introduction rule:
.
phi | is the formula ![]() |
assump | is the vector of assumptions ![]() |
Implements CVC3::CommonProofRules.
Definition at line 775 of file common_theorem_producer.cpp.
References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::impExpr(), CVC3::int2string(), CVC3::Theorem::isAssump(), CVC3::Theorem::isNull(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().
e1 => e2 ==> ~e2 => ~e1
Where ~e is the inverse of e (that is, ~(!e') = e').
Implements CVC3::CommonProofRules.
Definition at line 825 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isImpl(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
==> ITE(TRUE, e1, e2) == e1
Implements CVC3::CommonProofRules.
Definition at line 841 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Type::getExpr(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Type::isNull(), CVC3::Expr::isTrue(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
==> ITE(FALSE, e1, e2) == e2
Implements CVC3::CommonProofRules.
Definition at line 863 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Type::getExpr(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isFalse(), CVC3::Expr::isITE(), CVC3::Type::isNull(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
==> ITE(c, e, e) == e
Implements CVC3::CommonProofRules.
Definition at line 885 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Type::getExpr(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Type::isNull(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 906 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 922 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isXor(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
==> (e1 <=> e2) <=> [simplified expr]
Rewrite formulas like FALSE/TRUE <=> e, e <=> NOT e, etc.
Implements CVC3::CommonProofRules.
Definition at line 941 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), FALSE_EXPR, CVC3::ExprManager::falseExpr(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), NOT, reflexivityRule(), rewriteReflexivity(), rewriteUsingSymmetry(), TRUE_EXPR, and CVC3::TheoremProducer::withProof().
==> AND(e1,e2) IFF [simplified expr]
Implements CVC3::CommonProofRules.
Definition at line 989 of file common_theorem_producer.cpp.
References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::ExprMap< Data >::count(), CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), CVC3::ExprManager::falseExpr(), CVC3::Expr::isAnd(), CVC3::Expr::isFalse(), CVC3::Expr::isTrue(), CVC3::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::ExprMap< Data >::size(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Referenced by rewriteAnd().
==> OR(e1,...,en) IFF [simplified expr]
Implements CVC3::CommonProofRules.
Definition at line 1028 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CVC3::ExprMap< Data >::begin(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::ExprMap< Data >::count(), CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprMap< Data >::end(), CVC3::Expr::end(), CVC3::ExprManager::falseExpr(), CVC3::Expr::isFalse(), CVC3::Expr::isOr(), CVC3::Expr::isTrue(), CVC3::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), CVC3::ExprMap< Data >::size(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Referenced by rewriteOr().
==> NOT TRUE IFF FALSE
Implements CVC3::CommonProofRules.
Definition at line 1066 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::isNot(), CVC3::Expr::isTrue(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
==> NOT FALSE IFF TRUE
Implements CVC3::CommonProofRules.
Definition at line 1078 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isFalse(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
==> NOT NOT e IFF e, takes !!e
Implements CVC3::CommonProofRules.
Definition at line 1090 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
Implements CVC3::CommonProofRules.
Definition at line 1102 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), EXISTS, CVC3::Expr::getBody(), CVC3::Expr::getVars(), CVC3::Expr::isForall(), CVC3::Expr::isNot(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
Implements CVC3::CommonProofRules.
Definition at line 1117 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), FORALL, CVC3::Expr::getBody(), CVC3::Expr::getVars(), CVC3::Expr::isExists(), CVC3::Expr::isNot(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 1131 of file common_theorem_producer.cpp.
References CVC3::Expr::getBody(), CVC3::Expr::getVars(), CVC3::Expr::skolemExpr(), and CVC3::Expr::substExpr().
Referenced by skolemizeRewrite().
skolem rewrite rule: Introduces axiom |- Exists(x) phi(x) <=> phi(c) where c is a constant defined by the expression Exists(x) phi(x)
Implements CVC3::CommonProofRules.
Definition at line 1145 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::iffExpr(), CVC3::Expr::isExists(), CVC3::TheoremProducer::newLabel(), CVC3::TheoremProducer::newRWTheorem(), skolemize(), CVC3::Expr::toString(), TRACE, and CVC3::TheoremProducer::withProof().
Referenced by skolemize().
Special version of skolemizeRewrite for "EXISTS x. t = x".
Implements CVC3::CommonProofRules.
Definition at line 1165 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getBody(), CVC3::Expr::getOp(), CVC3::Expr::getVars(), CVC3::Expr::iffExpr(), CVC3::Expr::isEq(), CVC3::Expr::isExists(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newLabel(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::skolemExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by varIntroSkolem().
|- EXISTS x. e = x
Implements CVC3::CommonProofRules.
Definition at line 1202 of file common_theorem_producer.cpp.
References CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), EXISTS, CVC3::Expr::getType(), CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().
Referenced by varIntroSkolem().
If thm is (EXISTS x: phi(x)), create the Skolemized version and add it to the database. Otherwise returns just thm.
thm | is the Theorem(EXISTS x: phi(x)) |
Implements CVC3::CommonProofRules.
Definition at line 1223 of file common_theorem_producer.cpp.
References d_skolem_axioms, d_skolemized_thms, CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::Theorem::getExpr(), CVC3::Expr::getVars(), iffMP(), CVC3::CDMap< Key, Data, HashFcn >::insert(), CVC3::Expr::isExists(), CVC3::Expr::skolemExpr(), skolemizeRewrite(), and TRACE.
Retrun a theorem "|- e = v" for a new Skolem constant v.
This is equivalent to skolemize(d_core->varIntroRule(e)), only more efficient.
Implements CVC3::CommonProofRules.
Definition at line 1250 of file common_theorem_producer.cpp.
References d_skolem_axioms, d_skolemized_thms, d_skolemVars, DebugAssert, CVC3::CDMap< Key, Data, HashFcn >::end(), CVC3::CDMap< Key, Data, HashFcn >::find(), CVC3::Expr::getVars(), iffMP(), CVC3::CDMap< Key, Data, HashFcn >::insert(), CVC3::Expr::isExists(), skolemizeRewriteVar(), CVC3::Expr::toString(), and varIntroRule().
|
virtual |
==> TRUE
Implements CVC3::CommonProofRules.
Definition at line 1280 of file common_theorem_producer.cpp.
References CVC3::TheoremProducer::d_em, iffTrueElim(), reflexivityRule(), and CVC3::ExprManager::trueExpr().
AND(e1,e2) ==> [simplified expr].
Implements CVC3::CommonProofRules.
Definition at line 1286 of file common_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), iffMP(), and rewriteAnd().
OR(e1,...,en) ==> [simplified expr].
Implements CVC3::CommonProofRules.
Definition at line 1292 of file common_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), iffMP(), and rewriteOr().
Implements CVC3::CommonProofRules.
Definition at line 1298 of file common_theorem_producer.cpp.
References AND, CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getOp(), CVC3::Expr::isApply(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 1359 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::containsTermITE(), CVC3::Assumptions::emptyAssump(), findITE(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
|
inlinevirtual |
Implements CVC3::CommonProofRules.
Definition at line 126 of file common_theorem_producer.h.
References d_skolem_axioms.
|
inlinevirtual |
Implements CVC3::CommonProofRules.
Definition at line 127 of file common_theorem_producer.h.
References d_skolem_axioms.
|
private |
Definition at line 46 of file common_theorem_producer.h.
Referenced by clearSkolemAxioms(), getSkolemAxioms(), skolemize(), and varIntroSkolem().
Definition at line 50 of file common_theorem_producer.h.
Referenced by skolemize(), and varIntroSkolem().
Mapping of e to "|- e = v" for fresh Skolem vars v.
Definition at line 53 of file common_theorem_producer.h.
Referenced by varIntroSkolem().