#include <common_theorem_producer.h>
Inheritance diagram for CVC3::CommonTheoremProducer:
Definition at line 40 of file common_theorem_producer.h.
CommonTheoremProducer::CommonTheoremProducer | ( | TheoremManager * | tm | ) |
Definition at line 40 of file common_theorem_producer.cpp.
virtual CVC3::CommonTheoremProducer::~CommonTheoremProducer | ( | ) | [inline, virtual] |
Definition at line 57 of file common_theorem_producer.h.
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().
Theorem3 CommonTheoremProducer::implIntro3 | ( | const Theorem3 & | phi, | |
const std::vector< Expr > & | assump, | |||
const std::vector< Theorem > & | tccs | |||
) | [virtual] |
3-valued implication introduction rule:
phi | is the formula | |
assump | is the vector of assumptions | |
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::Theorem3::getProof(), CVC3::Expr::impExpr(), 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::Theorem::getAssumptionsRef(), 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().
Theorem CommonTheoremProducer::transitivityRule | ( | const Theorem & | a1_eq_a2, | |
const Theorem & | a2_eq_a3 | |||
) | [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::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::Debug::counter(), CVC3::debugger, CVC3::Theorem::getAssumptionsRef(), 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::Debug::newTimer(), CVC3::Debug::setCurrentTime(), CVC3::Debug::timer(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Referenced by substitutivityRule().
Theorem CommonTheoremProducer::substitutivityRule | ( | const Expr & | e, | |
const Theorem & | thm1, | |||
const Theorem & | thm2 | |||
) | [virtual] |
Optimized case for expr with two children.
Implements CVC3::CommonProofRules.
Definition at line 330 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Debug::counter(), CVC3::debugger, 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::Debug::newTimer(), CVC3::Debug::setCurrentTime(), CVC3::Debug::timer(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Theorem CommonTheoremProducer::substitutivityRule | ( | const Op & | op, | |
const std::vector< Theorem > & | thms | |||
) | [virtual] |
Implements CVC3::CommonProofRules.
Definition at line 369 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Debug::counter(), CVC3::TheoremProducer::d_tm, CVC3::debugger, CVC3::TheoremManager::getEM(), IF_DEBUG, CVC3::ExprManager::newLeafExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Debug::newTimer(), reflexivityRule(), CVC3::Debug::setCurrentTime(), CVC3::Debug::setElapsed(), CVC3::Debug::timer(), CVC3::Op::toString(), and CVC3::TheoremProducer::withProof().
Theorem CommonTheoremProducer::substitutivityRule | ( | const Expr & | e, | |
const std::vector< unsigned > & | changed, | |||
const std::vector< Theorem > & | thms | |||
) | [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 for the changed kids. |
Implements CVC3::CommonProofRules.
Definition at line 419 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Debug::counter(), DebugAssert, CVC3::debugger, CVC3::Expr::getOp(), CVC3::Debug::getOS(), IF_DEBUG, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Debug::newTimer(), reflexivityRule(), CVC3::Debug::setCurrentTime(), CVC3::Debug::setElapsed(), substitutivityRule(), CVC3::Debug::timer(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Theorem CommonTheoremProducer::substitutivityRule | ( | const Expr & | e, | |
const int | changed, | |||
const Theorem & | thm | |||
) | [virtual] |
Implements CVC3::CommonProofRules.
Definition at line 503 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::debugger, std::endl(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Expr::getOp(), CVC3::Debug::getOS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), IF_DEBUG, CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Theorem CommonTheoremProducer::contradictionRule | ( | const Theorem & | e, | |
const Theorem & | not_e | |||
) | [virtual] |
Implements CVC3::CommonProofRules.
Definition at line 553 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 572 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 583 of file common_theorem_producer.cpp.
References CVC3::TheoremProducer::d_em, CVC3::Theorem::getAssumptionsRef(), 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 594 of file common_theorem_producer.cpp.
References CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 604 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), 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 618 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), 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 633 of file common_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::newRWTheorem(), CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 647 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), 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 659 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 684 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 710 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), 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 725 of file common_theorem_producer.cpp.
Implements CVC3::CommonProofRules.
Definition at line 733 of file common_theorem_producer.cpp.
References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().
Theorem CommonTheoremProducer::implIntro | ( | const Theorem & | phi, | |
const std::vector< Expr > & | assump | |||
) | [virtual] |
Implication introduction rule:
.
phi | is the formula | |
assump | is the vector of assumptions |
Implements CVC3::CommonProofRules.
Definition at line 757 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::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 807 of file common_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::isImpl(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Implements CVC3::CommonProofRules.
Definition at line 822 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::ExprManager::falseExpr(), CVC3::Theorem::getAssumptionsRef(), 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 838 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 853 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::FALSE_EXPR, CVC3::ExprManager::falseExpr(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::NOT, reflexivityRule(), rewriteReflexivity(), rewriteUsingSymmetry(), CVC3::TRUE_EXPR, and CVC3::TheoremProducer::withProof().
==> AND(e1,e2) IFF [simplified expr]
Implements CVC3::CommonProofRules.
Definition at line 901 of file common_theorem_producer.cpp.
References CVC3::andExpr(), 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::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 940 of file common_theorem_producer.cpp.
References 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::isOr(), 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 978 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 990 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 1002 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 1014 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::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 1029 of file common_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::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 1043 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 1057 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(), CVC3::TRACE, and CVC3::TheoremProducer::withProof().
Referenced by skolemize().
Special version of skolemizeRewrite for "EXISTS x. t = x".
Implements CVC3::CommonProofRules.
Definition at line 1075 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 1112 of file common_theorem_producer.cpp.
References CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::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 1133 of file common_theorem_producer.cpp.
References d_skolem_axioms, d_skolemized_thms, CVC3::Theorem::getExpr(), CVC3::Expr::getVars(), iffMP(), CVC3::Expr::isExists(), CVC3::Expr::skolemExpr(), skolemizeRewrite(), and CVC3::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 1159 of file common_theorem_producer.cpp.
References d_skolem_axioms, d_skolemized_thms, d_skolemVars, DebugAssert, CVC3::Theorem::getExpr(), CVC3::Expr::getVars(), iffMP(), CVC3::Expr::isExists(), skolemizeRewriteVar(), CVC3::Expr::toString(), and varIntroRule().
Theorem CommonTheoremProducer::trueTheorem | ( | ) | [virtual] |
==> TRUE
Implements CVC3::CommonProofRules.
Definition at line 1189 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 1195 of file common_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), iffMP(), and rewriteAnd().
OR(e1,...,en) ==> [simplified expr].
Implements CVC3::CommonProofRules.
Definition at line 1201 of file common_theorem_producer.cpp.
References CVC3::Theorem::getExpr(), iffMP(), and rewriteOr().
Implements CVC3::CommonProofRules.
Definition at line 1207 of file common_theorem_producer.cpp.
References CVC3::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().
std::vector<Theorem>& CVC3::CommonTheoremProducer::getSkolemAxioms | ( | ) | [inline, virtual] |
Implements CVC3::CommonProofRules.
Definition at line 119 of file common_theorem_producer.h.
References d_skolem_axioms.
void CVC3::CommonTheoremProducer::clearSkolemAxioms | ( | ) | [inline, virtual] |
Implements CVC3::CommonProofRules.
Definition at line 120 of file common_theorem_producer.h.
References d_skolem_axioms.
std::vector<Theorem> CVC3::CommonTheoremProducer::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().
CDMap<Expr, Theorem> CVC3::CommonTheoremProducer::d_skolemVars [private] |
Mapping of e to "|- e = v" for fresh Skolem vars v.
Definition at line 53 of file common_theorem_producer.h.
Referenced by varIntroSkolem().