#include <array_theorem_producer.h>

Inherits CVC3::ArrayProofRules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::ArrayTheoremProducer:

[legend]

List of all members.

Public Member Functions

ArrayTheoremProducer (TheoryArray *theoryArray)
Theorem rewriteSameStore (const Expr &e, int n)
Theorem rewriteWriteWrite (const Expr &e)
Theorem rewriteReadWrite (const Expr &e)
Theorem rewriteReadWrite2 (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)
Theorem liftReadIte (const Expr &e)
Lift ite over read.
Theorem arrayNotEq (const Theorem &e)
a /= b |- exists i. a[i] /= b[i]
Theorem splitOnConstants (const Expr &a, const std::vector< Expr > &consts)
Theorem propagateIndexDiseq (const Theorem &read1eqread2isFalse)

Private Attributes

TheoryArray * d_theoryArray

Detailed Description

Definition at line 37 of file array_theorem_producer.h.

Constructor & Destructor Documentation

ArrayTheoremProducer::ArrayTheoremProducer ( TheoryArray * theoryArray )

Definition at line 46 of file array_theorem_producer.cpp.

Member Function Documentation

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

Implements CVC3::ArrayProofRules.

Definition at line 70 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]

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

Implements CVC3::ArrayProofRules.

Definition at line 149 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::rewriteReadWrite2 ( const Expr & e ) [virtual]

Implements CVC3::ArrayProofRules.

Definition at line 173 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::newTheorem(), CVC3::READ, and CVC3::TheoremProducer::withProof().

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

Implements CVC3::ArrayProofRules.

Definition at line 205 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 244 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 264 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 284 of file array_theorem_producer.cpp.

References CVC3::ARRAY_LITERAL, CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getBody(), CVC3::Expr::getKind(), CVC3::Expr::getVars(), CVC3::Expr::isClosure(), 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 319 of file array_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), ITE, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::READ, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArrayTheoremProducer::arrayNotEq ( const Theorem & e ) [virtual]

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

Implements CVC3::ArrayProofRules.

Definition at line 338 of file array_theorem_producer.cpp.

References CHECK_PROOFS, CHECK_SOUND, d_theoryArray, EQ, CVC3::Expr::eqExpr(), EXISTS, CVC3::Theory::getBaseType(), CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::isArray(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), NOT, CVC3::READ, CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().

Theorem ArrayTheoremProducer::splitOnConstants	(	const Expr &	a,
		const std::vector< Expr > &	consts
	)		`[virtual]`

Implements CVC3::ArrayProofRules.

Definition at line 363 of file array_theorem_producer.cpp.

References CVC3::andExpr(), CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::notExpr(), CVC3::orExpr(), CVC3::Expr::orExpr(), and CVC3::TheoremProducer::withProof().

Theorem ArrayTheoremProducer::propagateIndexDiseq ( const Theorem & read1eqread2isFalse ) [virtual]

Implements CVC3::ArrayProofRules.

Definition at line 388 of file array_theorem_producer.cpp.

References CVC3::Expr::eqExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::notExpr(), and CVC3::TheoremProducer::withProof().

Member Data Documentation

TheoryArray* CVC3::ArrayTheoremProducer::d_theoryArray [private]

Definition at line 39 of file array_theorem_producer.h.

Referenced by arrayNotEq().

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

CVC3::ArrayTheoremProducer Class Reference

Public Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

Member Function Documentation

Member Data Documentation