CVCL::ArrayTheoremProducer Class Reference

#include <array_theorem_producer.h>

Inheritance diagram for CVCL::ArrayTheoremProducer:

[legend]Collaboration diagram for CVCL::ArrayTheoremProducer:

[legend]List of all members.

Public Member Functions

• ArrayTheoremProducer (TheoremManager *tm)
• Theorem rewriteSameStore (const Expr &e, int n)
• Theorem rewriteWriteWrite (const Expr &e)
• Theorem rewriteReadWrite (const Expr &e)
• Theorem rewriteRedundantWrite1 (const Theorem &v_eq_r, const Expr &write)
• Theorem rewriteRedundantWrite2 (const Expr &e)
• Theorem interchangeIndices (const Expr &e)
• Theorem readArrayLiteral (const Expr &e)

  Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg).
  

---

Detailed Description

Definition at line 44 of file array_theorem_producer.h.

---

Constructor & Destructor Documentation

CVCL::ArrayTheoremProducer::ArrayTheoremProducer (  TheoremManager *  tm  )  [inline]

Definition at line 49 of file array_theorem_producer.h.

---

Member Function Documentation

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

Implements CVCL::ArrayProofRules. Definition at line 72 of file array_theorem_producer.cpp. References CVCL::Expr::eqExpr(), CVCL::Expr::getType(), IF_DEBUG(), CVCL::Expr::iffExpr(), CVCL::Expr::impExpr(), CVCL::Type::isBool(), CVCL::Expr::isEq(), CVCL::Expr::isNull(), CVCL::isWrite(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::READ, and CVCL::TheoremProducer::withProof().

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

Implements CVCL::ArrayProofRules. Definition at line 125 of file array_theorem_producer.cpp. References CVCL::Expr::andExpr(), CVCL::Expr::eqExpr(), CVCL::Expr::getType(), IF_DEBUG(), CVCL::Expr::iffExpr(), CVCL::Type::isBool(), CVCL::Expr::isEq(), CVCL::isWrite(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::READ, CVCL::TheoremProducer::withProof(), and CVCL::WRITE.

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

Implements CVCL::ArrayProofRules. Definition at line 153 of file array_theorem_producer.cpp. References CVCL::Expr::eqExpr(), CVCL::Expr::getType(), IF_DEBUG(), CVCL::Expr::iffExpr(), CVCL::Type::isBool(), CVCL::isRead(), CVCL::isWrite(), CVCL::Expr::iteExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::READ, and CVCL::TheoremProducer::withProof().

Theorem ArrayTheoremProducer::rewriteRedundantWrite1 (  const Theorem &  v_eq_r, const Expr &  write )  [virtual]

Implements CVCL::ArrayProofRules. Definition at line 176 of file array_theorem_producer.cpp. References CVCL::Assumptions::copy(), CVCL::Theorem::getAssumptions(), CVCL::Theorem::getLHS(), CVCL::Theorem::getProof(), CVCL::Theorem::getRHS(), CVCL::isRead(), CVCL::Theorem::isRewrite(), CVCL::isWrite(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

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

Implements CVCL::ArrayProofRules. Definition at line 197 of file array_theorem_producer.cpp. References CVCL::isWrite(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::TheoremProducer::withProof(), and CVCL::WRITE.

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

Implements CVCL::ArrayProofRules. Definition at line 218 of file array_theorem_producer.cpp. References CVCL::Expr::eqExpr(), CVCL::Expr::getType(), CVCL::Expr::iffExpr(), CVCL::Type::isBool(), CVCL::isWrite(), CVCL::Expr::iteExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::TheoremProducer::withProof(), and CVCL::WRITE.

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

Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg). Implements CVCL::ArrayProofRules. Definition at line 239 of file array_theorem_producer.cpp. References CVCL::ARRAY_LITERAL, CVCL::Expr::getBody(), CVCL::Expr::getKind(), CVCL::Expr::getVars(), CVCL::Expr::isClosure(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::READ, CVCL::Expr::substExpr(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

---

The documentation for this class was generated from the following files:

• array_theorem_producer.h
• array_theorem_producer.cpp

---