CVCL::ArrayProofRules Class Reference

#include <array_proof_rules.h>

Inheritance diagram for CVCL::ArrayProofRules:

[legend]List of all members.

Public Member Functions

• virtual ~ArrayProofRules ()
• virtual Theorem rewriteSameStore (const Expr &e, int n)=0
• virtual Theorem rewriteWriteWrite (const Expr &e)=0
• virtual Theorem rewriteReadWrite (const Expr &e)=0
• virtual Theorem rewriteRedundantWrite1 (const Theorem &v_eq_r, const Expr &write)=0
• virtual Theorem rewriteRedundantWrite2 (const Expr &e)=0
• virtual Theorem interchangeIndices (const Expr &e)=0
• virtual Theorem readArrayLiteral (const Expr &e)=0

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

---

Detailed Description

Definition at line 41 of file array_proof_rules.h.

---

Constructor & Destructor Documentation

virtual CVCL::ArrayProofRules::~ArrayProofRules (   )  [inline, virtual]

Definition at line 44 of file array_proof_rules.h.

---

Member Function Documentation

virtual Theorem CVCL::ArrayProofRules::rewriteSameStore (  const Expr &  e, int  n )  [pure virtual]

Implemented in CVCL::ArrayTheoremProducer.

virtual Theorem CVCL::ArrayProofRules::rewriteWriteWrite (  const Expr &  e  )  [pure virtual]

Implemented in CVCL::ArrayTheoremProducer.

virtual Theorem CVCL::ArrayProofRules::rewriteReadWrite (  const Expr &  e  )  [pure virtual]

Implemented in CVCL::ArrayTheoremProducer. Referenced by CVCL::TheoryArray::update().

virtual Theorem CVCL::ArrayProofRules::rewriteRedundantWrite1 (  const Theorem &  v_eq_r, const Expr &  write )  [pure virtual]

Implemented in CVCL::ArrayTheoremProducer.

virtual Theorem CVCL::ArrayProofRules::rewriteRedundantWrite2 (  const Expr &  e  )  [pure virtual]

Implemented in CVCL::ArrayTheoremProducer.

virtual Theorem CVCL::ArrayProofRules::interchangeIndices (  const Expr &  e  )  [pure virtual]

Implemented in CVCL::ArrayTheoremProducer.

virtual Theorem CVCL::ArrayProofRules::readArrayLiteral (  const Expr &  e  )  [pure virtual]

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

---

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

• array_proof_rules.h

---