CVC3
Public Member Functions | List of all members
CVC3::ArrayProofRules Class Referenceabstract

#include <array_proof_rules.h>

Inherited by CVC3::ArrayTheoremProducer.

Collaboration diagram for CVC3::ArrayProofRules:
Collaboration graph

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]
 
virtual Theorem splitOnConstants (const Expr &a, const std::vector< Expr > &consts)=0
 
virtual Theorem propagateIndexDiseq (const Theorem &read1eqread2isFalse)=0
 

Detailed Description

Definition at line 35 of file array_proof_rules.h.

Constructor & Destructor Documentation

virtual CVC3::ArrayProofRules::~ArrayProofRules ( )
inlinevirtual

Definition at line 38 of file array_proof_rules.h.

Member Function Documentation

virtual Theorem CVC3::ArrayProofRules::rewriteSameStore ( const Expr e,
int  n 
)
pure virtual
virtual Theorem CVC3::ArrayProofRules::rewriteWriteWrite ( const Expr e)
pure virtual
virtual Theorem CVC3::ArrayProofRules::rewriteReadWrite ( const Expr e)
pure virtual
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
virtual Theorem CVC3::ArrayProofRules::rewriteRedundantWrite2 ( const Expr e)
pure virtual
virtual Theorem CVC3::ArrayProofRules::interchangeIndices ( const Expr e)
pure virtual
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().

virtual Theorem CVC3::ArrayProofRules::splitOnConstants ( const Expr a,
const std::vector< Expr > &  consts 
)
pure virtual

Implemented in CVC3::ArrayTheoremProducer.

virtual Theorem CVC3::ArrayProofRules::propagateIndexDiseq ( const Theorem read1eqread2isFalse)
pure virtual

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