#include <array_theorem_producer.h>
Inheritance diagram for CVC3::ArrayTheoremProducer:
Definition at line 36 of file array_theorem_producer.h.
CVC3::ArrayTheoremProducer::ArrayTheoremProducer | ( | TheoremManager * | tm | ) | [inline] |
Definition at line 41 of file array_theorem_producer.h.
Implements CVC3::ArrayProofRules.
Definition at line 64 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getType(), IF_DEBUG, CVC3::Expr::iffExpr(), CVC3::Expr::impExpr(), CVC3::Type::isBool(), CVC3::Expr::isEq(), CVC3::isWrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::READ, and CVC3::TheoremProducer::withProof().
Implements CVC3::ArrayProofRules.
Definition at line 116 of file array_theorem_producer.cpp.
References CVC3::Expr::andExpr(), DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getType(), IF_DEBUG, CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::Expr::isEq(), CVC3::isWrite(), MiniSat::left(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::READ, MiniSat::right(), CVC3::TheoremProducer::withProof(), and CVC3::WRITE.
Implements CVC3::ArrayProofRules.
Definition at line 143 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getType(), IF_DEBUG, CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::isRead(), CVC3::isWrite(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::READ, and CVC3::TheoremProducer::withProof().
Theorem ArrayTheoremProducer::rewriteRedundantWrite1 | ( | const Theorem & | v_eq_r, | |
const Expr & | write | |||
) | [virtual] |
Implements CVC3::ArrayProofRules.
Definition at line 174 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::isRead(), CVC3::Theorem::isRewrite(), CVC3::isWrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoremProducer::withProof(), and CVC3::WRITE.
Implements CVC3::ArrayProofRules.
Definition at line 213 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::isWrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoremProducer::withProof(), and CVC3::WRITE.
Implements CVC3::ArrayProofRules.
Definition at line 233 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::isWrite(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoremProducer::withProof(), and CVC3::WRITE.
Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg).
Implements CVC3::ArrayProofRules.
Definition at line 253 of file array_theorem_producer.cpp.
References CVC3::ARRAY_LITERAL, CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::READ, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Lift ite over read.
Implements CVC3::ArrayProofRules.
Definition at line 288 of file array_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), CVC3::ITE, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::READ, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().