CVC3::ArrayTheoremProducer Class Reference

#include <array_theorem_producer.h>

Inheritance diagram for CVC3::ArrayTheoremProducer:

Inheritance graph
[legend]
Collaboration diagram for CVC3::ArrayTheoremProducer:

Collaboration graph
[legend]
List of all members.

Public Member Functions


Detailed Description

Definition at line 36 of file array_theorem_producer.h.


Constructor & Destructor Documentation

CVC3::ArrayTheoremProducer::ArrayTheoremProducer ( TheoremManager tm  )  [inline]

Definition at line 41 of file array_theorem_producer.h.


Member Function Documentation

Theorem ArrayTheoremProducer::rewriteSameStore ( const Expr e,
int  n 
) [virtual]

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().

Theorem ArrayTheoremProducer::rewriteWriteWrite ( const Expr e  )  [virtual]

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.

Theorem ArrayTheoremProducer::rewriteReadWrite ( const Expr e  )  [virtual]

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.

Theorem ArrayTheoremProducer::rewriteRedundantWrite2 ( const Expr e  )  [virtual]

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.

Theorem ArrayTheoremProducer::interchangeIndices ( const Expr e  )  [virtual]

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.

Theorem ArrayTheoremProducer::readArrayLiteral ( const Expr e  )  [virtual]

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().

Theorem ArrayTheoremProducer::liftReadIte ( const Expr e  )  [virtual]

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().


The documentation for this class was generated from the following files:
Generated on Tue Jul 3 14:41:35 2007 for CVC3 by  doxygen 1.5.1