CVC3
2.4.1
|
#include <array_theorem_producer.h>
ArrayTheoremProducer::ArrayTheoremProducer | ( | TheoryArray * | theoryArray | ) |
Definition at line 46 of file array_theorem_producer.cpp.
Implements CVC3::ArrayProofRules.
Definition at line 70 of file array_theorem_producer.cpp.
References IF_DEBUG, DebugAssert, CVC3::Expr::isEq(), CVC3::isWrite(), CVC3::READ, CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::iffExpr(), CVC3::Expr::eqExpr(), CVC3::Expr::impExpr(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::Assumptions::emptyAssump().
Implements CVC3::ArrayProofRules.
Definition at line 122 of file array_theorem_producer.cpp.
References IF_DEBUG, DebugAssert, CVC3::Expr::isEq(), CVC3::isWrite(), MiniSat::left(), MiniSat::right(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::iffExpr(), CVC3::WRITE, CVC3::READ, CVC3::Expr::eqExpr(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::andExpr(), and CVC3::Assumptions::emptyAssump().
Implements CVC3::ArrayProofRules.
Definition at line 149 of file array_theorem_producer.cpp.
References IF_DEBUG, DebugAssert, CVC3::isRead(), CVC3::isWrite(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::iffExpr(), CVC3::Expr::eqExpr(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::iteExpr(), CVC3::READ, and CVC3::Assumptions::emptyAssump().
Implements CVC3::ArrayProofRules.
Definition at line 173 of file array_theorem_producer.cpp.
References IF_DEBUG, DebugAssert, CVC3::isRead(), CVC3::isWrite(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::iffExpr(), CVC3::Expr::eqExpr(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::iteExpr(), CVC3::READ, and CVC3::Assumptions::emptyAssump().
Theorem ArrayTheoremProducer::rewriteRedundantWrite1 | ( | const Theorem & | v_eq_r, |
const Expr & | write | ||
) | [virtual] |
Implements CVC3::ArrayProofRules.
Definition at line 205 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::Theorem::isRewrite(), CVC3::isRead(), CVC3::Theorem::getLHS(), CVC3::Theorem::getRHS(), CVC3::isWrite(), CVC3::WRITE, CVC3::Expr::eqExpr(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::Theorem::getAssumptionsRef().
Implements CVC3::ArrayProofRules.
Definition at line 244 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::isWrite(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::WRITE, and CVC3::Assumptions::emptyAssump().
Implements CVC3::ArrayProofRules.
Definition at line 264 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::isWrite(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::WRITE, CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::Expr::eqExpr(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::Assumptions::emptyAssump().
Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg)
Implements CVC3::ArrayProofRules.
Definition at line 284 of file array_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getKind(), CVC3::READ, CVC3::Expr::toString(), CVC3::Expr::isClosure(), CVC3::ARRAY_LITERAL, CVC3::Expr::getBody(), CVC3::Expr::getVars(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::Assumptions::emptyAssump().
Lift ite over read.
Implements CVC3::ArrayProofRules.
Definition at line 319 of file array_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Expr::getKind(), CVC3::READ, ITE, CVC3::Expr::toString(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), and CVC3::Assumptions::emptyAssump().
a /= b |- exists i. a[i] /= b[i]
Implements CVC3::ArrayProofRules.
Definition at line 338 of file array_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), NOT, EQ, CVC3::isArray(), d_theoryArray, CVC3::Theory::getBaseType(), CVC3::Theorem::toString(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::Theorem::getProof(), CVC3::Theory::getEM(), CVC3::ExprManager::newBoundVarExpr(), CVC3::READ, CVC3::Expr::eqExpr(), CVC3::TheoremProducer::newTheorem(), CVC3::ExprManager::newClosureExpr(), and EXISTS.
Theorem ArrayTheoremProducer::splitOnConstants | ( | const Expr & | a, |
const std::vector< Expr > & | consts | ||
) | [virtual] |
Implements CVC3::ArrayProofRules.
Definition at line 363 of file array_theorem_producer.cpp.
References CVC3::Expr::eqExpr(), CVC3::Expr::notExpr(), CVC3::andExpr(), CVC3::orExpr(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::Assumptions::emptyAssump().
Implements CVC3::ArrayProofRules.
Definition at line 388 of file array_theorem_producer.cpp.
References CVC3::Theorem::getLHS(), CVC3::TheoremProducer::withProof(), CVC3::TheoremProducer::newPf(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::eqExpr(), and CVC3::Expr::notExpr().
Definition at line 39 of file array_theorem_producer.h.
Referenced by arrayNotEq().