CVC3::ArrayProofRules Class Reference

#include <array_proof_rules.h>

Inheritance diagram for CVC3::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 rewriteReadWrite2 (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).
  

• virtual Theorem liftReadIte (const Expr &e)=0

  Lift ite over read.
  

• virtual Theorem arrayNotEq (const Theorem &e)=0

  a /= b |- exists i. a[i] /= b[i]
  

---

Detailed Description

Definition at line 33 of file array_proof_rules.h.

---

Constructor & Destructor Documentation

virtual CVC3::ArrayProofRules::~ArrayProofRules

(

)

[inline, virtual]

Definition at line 36 of file array_proof_rules.h.

---

Member Function Documentation

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

Implemented in CVC3::ArrayTheoremProducer.

Referenced by CVC3::TheoryArray::rewrite().

virtual Theorem CVC3::ArrayProofRules::rewriteWriteWrite

(

const Expr &

e

)

[pure virtual]

Implemented in CVC3::ArrayTheoremProducer.

Referenced by CVC3::TheoryArray::rewrite().

virtual Theorem CVC3::ArrayProofRules::rewriteReadWrite

(

const Expr &

e

)

[pure virtual]

Implemented in CVC3::ArrayTheoremProducer.

Referenced by CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().

virtual Theorem CVC3::ArrayProofRules::rewriteReadWrite2

(

const Expr &

e

)

[pure virtual]

Implemented in CVC3::ArrayTheoremProducer.

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

Implemented in CVC3::ArrayTheoremProducer.

Referenced by CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().

virtual Theorem CVC3::ArrayProofRules::rewriteRedundantWrite2

(

const Expr &

e

)

[pure virtual]

Implemented in CVC3::ArrayTheoremProducer.

Referenced by CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().

virtual Theorem CVC3::ArrayProofRules::interchangeIndices

(

const Expr &

e

)

[pure virtual]

Implemented in CVC3::ArrayTheoremProducer.

Referenced by CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::pullIndex(), CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().

virtual Theorem CVC3::ArrayProofRules::readArrayLiteral

(

const Expr &

e

)

[pure virtual]

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

Implemented in CVC3::ArrayTheoremProducer.

Referenced by CVC3::TheoryArray::rewrite().

virtual Theorem CVC3::ArrayProofRules::liftReadIte

(

const Expr &

e

)

[pure virtual]

Lift ite over read.

Implemented in CVC3::ArrayTheoremProducer.

Referenced by CVC3::TheoryArray::rewrite().

virtual Theorem CVC3::ArrayProofRules::arrayNotEq

(

const Theorem &

e

)

[pure virtual]

a /= b |- exists i. a[i] /= b[i]

Implemented in CVC3::ArrayTheoremProducer.

Referenced by CVC3::TheoryArray::assertFact().

---

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

• array_proof_rules.h

---