#include <core_theorem_producer.h>
Definition at line 40 of file core_theorem_producer.h.
CVC3::CoreTheoremProducer::CoreTheoremProducer | ( | TheoremManager * | tm, | |
TheoryCore * | core | |||
) | [inline] |
Definition at line 46 of file core_theorem_producer.h.
virtual CVC3::CoreTheoremProducer::~CoreTheoremProducer | ( | ) | [inline, virtual] |
Definition at line 48 of file core_theorem_producer.h.
Definition at line 52 of file core_theorem_producer.cpp.
References d_core, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getType(), CVC3::Theory::getTypePred(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().
Definition at line 64 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 75 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::isAnd(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 93 of file core_theorem_producer.cpp.
References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::isNot(), CVC3::Expr::isOr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 110 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isIff(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
Definition at line 123 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
Definition at line 136 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Type::isNull(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().
Definition at line 161 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, DebugAssert, CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Type::isNull(), CVC3::Theorem::isRewrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::TheoremProducer::withAssumptions(), and CVC3::TheoremProducer::withProof().
Definition at line 186 of file core_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::orExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
|= (A & B1) | (A & B2) | ... | (A & bn) <=> A & (B1 | B2 | ...| Bn)
Definition at line 202 of file core_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::isAnd(), CVC3::Expr::isOr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::orExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
|= (A | B1) & (A | B2) & ... & (A | bn) <=> A | (B1 & B2 & ...& Bn)
Definition at line 245 of file core_theorem_producer.cpp.
References CVC3::andExpr(), CVC3::Expr::arity(), CVC3::Expr::begin(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::end(), CVC3::Expr::isAnd(), CVC3::Expr::isOr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::orExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 285 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isImpl(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::TheoremProducer::withProof().
Definition at line 297 of file core_theorem_producer.cpp.
References CVC3::AND, CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getEM(), CVC3::Expr::getKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Definition at line 328 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, d_core, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Theory::getCommonRules(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isNot(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::CommonProofRules::rewriteNotFalse(), CVC3::CommonProofRules::rewriteNotTrue(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Definition at line 345 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::getKids(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::Type::isNull(), CVC3::Expr::isOr(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Definition at line 383 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::getKids(), CVC3::Expr::getType(), CVC3::int2string(), CVC3::Expr::isAnd(), CVC3::Type::isNull(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Definition at line 423 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, d_core, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Theory::getCommonRules(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::CommonProofRules::reflexivityRule(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Definition at line 439 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, d_core, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::Theory::getCommonRules(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isImpl(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::CommonProofRules::reflexivityRule(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Definition at line 455 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isFalse(), CVC3::Expr::isITE(), CVC3::Expr::isTrue(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 467 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), CVC3::Expr::isTrue(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 479 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isFalse(), CVC3::Expr::isITE(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 491 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), CVC3::Expr::negate(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 503 of file core_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::isITE(), CVC3::Expr::isTrue(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 516 of file core_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::isITE(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Definition at line 588 of file core_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOp(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::isITE(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 543 of file core_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::iffExpr(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 565 of file core_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::iffExpr(), CVC3::Expr::isIff(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 621 of file core_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getOp(), CVC3::ExprHashMap< Data >::insert(), CVC3::int2string(), CVC3::Expr::isAnd(), CVC3::TheoremProducer::newPf(), CVC3::ExprManager::newRatExpr(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Definition at line 647 of file core_theorem_producer.cpp.
References CVC3::Expr::arity(), CHECK_PROOFS, CHECK_SOUND, CVC3::TheoremProducer::d_em, CVC3::Assumptions::emptyAssump(), CVC3::ExprManager::falseExpr(), CVC3::Expr::getOp(), CVC3::ExprHashMap< Data >::insert(), CVC3::int2string(), CVC3::Expr::isOr(), CVC3::TheoremProducer::newPf(), CVC3::ExprManager::newRatExpr(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 670 of file core_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), and CVC3::TheoremProducer::newTheorem().
TheoryCore* CVC3::CoreTheoremProducer::d_core [private] |
pointer to theory core
Definition at line 43 of file core_theorem_producer.h.
Referenced by IffToIte(), ImpToIte(), NotToIte(), and typePred().