Public Member Functions | Private Attributes

CVC3::ArrayTheoremProducer Class Reference

#include <array_theorem_producer.h>

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

Collaboration diagram for CVC3::ArrayTheoremProducer:
Collaboration graph

List of all members.

Public Member Functions

Private Attributes

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]
Theorem ArrayTheoremProducer::rewriteWriteWrite ( const Expr e) [virtual]
Theorem ArrayTheoremProducer::rewriteReadWrite ( const Expr e) [virtual]
Theorem ArrayTheoremProducer::rewriteReadWrite2 ( const Expr e) [virtual]
Theorem ArrayTheoremProducer::rewriteRedundantWrite1 ( const Theorem v_eq_r,
const Expr write 
) [virtual]
Theorem ArrayTheoremProducer::rewriteRedundantWrite2 ( const Expr e) [virtual]
Theorem ArrayTheoremProducer::interchangeIndices ( const Expr e) [virtual]
Theorem ArrayTheoremProducer::readArrayLiteral ( const Expr e) [virtual]
Theorem ArrayTheoremProducer::liftReadIte ( const Expr e) [virtual]
Theorem ArrayTheoremProducer::arrayNotEq ( const Theorem e) [virtual]
Theorem ArrayTheoremProducer::splitOnConstants ( const Expr a,
const std::vector< Expr > &  consts 
) [virtual]
Theorem ArrayTheoremProducer::propagateIndexDiseq ( const Theorem read1eqread2isFalse) [virtual]

Member Data Documentation

Definition at line 39 of file array_theorem_producer.h.

Referenced by arrayNotEq().

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