CVC3  2.4.1
Public Member Functions | Private Attributes | List of all members
CVC3::ArrayTheoremProducer Class Reference

#include <array_theorem_producer.h>

Inheritance diagram for CVC3::ArrayTheoremProducer:
CVC3::ArrayProofRules CVC3::TheoremProducer

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) More...
 
Theorem liftReadIte (const Expr &e)
 Lift ite over read. More...
 
Theorem arrayNotEq (const Theorem &e)
 a /= b |- exists i. a[i] /= b[i] More...
 
Theorem splitOnConstants (const Expr &a, const std::vector< Expr > &consts)
 
Theorem propagateIndexDiseq (const Theorem &read1eqread2isFalse)
 
- Public Member Functions inherited from CVC3::ArrayProofRules
virtual ~ArrayProofRules ()
 
- Public Member Functions inherited from CVC3::TheoremProducer
 TheoremProducer (TheoremManager *tm)
 
virtual ~TheoremProducer ()
 
bool withProof ()
 Testing whether to generate proofs. More...
 
bool withAssumptions ()
 Testing whether to generate assumptions. More...
 
Proof newLabel (const Expr &e)
 Create a new proof label (bound variable) for an assumption (formula) More...
 
Proof newPf (const std::string &name)
 
Proof newPf (const std::string &name, const Expr &e)
 
Proof newPf (const std::string &name, const Proof &pf)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2)
 
Proof newPf (const std::string &name, const Expr &e, const Proof &pf)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const Expr &e3)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const Proof &pf)
 
Proof newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end)
 
Proof newPf (const std::string &name, const Expr &e, Expr::iterator begin, const Expr::iterator &end)
 
Proof newPf (const std::string &name, Expr::iterator begin, const Expr::iterator &end, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const std::vector< Expr > &args)
 
Proof newPf (const std::string &name, const Expr &e, const std::vector< Expr > &args)
 
Proof newPf (const std::string &name, const Expr &e, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const Expr &e1, const Expr &e2, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const std::vector< Proof > &pfs)
 
Proof newPf (const std::string &name, const std::vector< Expr > &args, const Proof &pf)
 
Proof newPf (const std::string &name, const std::vector< Expr > &args, const std::vector< Proof > &pfs)
 
Proof newPf (const Proof &label, const Expr &frm, const Proof &pf)
 Creating LAMBDA-abstraction (LAMBDA label formula proof) More...
 
Proof newPf (const Proof &label, const Proof &pf)
 Creating LAMBDA-abstraction (LAMBDA label proof). More...
 
Proof newPf (const std::vector< Proof > &labels, const std::vector< Expr > &frms, const Proof &pf)
 Similarly, multi-argument lambda-abstractions: (LAMBDA (u1,...,un): (f1,...,fn). pf) More...
 
Proof newPf (const std::vector< Proof > &labels, const Proof &pf)
 

Private Attributes

TheoryArrayd_theoryArray
 

Additional Inherited Members

- Protected Member Functions inherited from CVC3::TheoremProducer
Theorem newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf)
 Create a new theorem. See also newRWTheorem() and newReflTheorem() More...
 
Theorem newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
 Create a rewrite theorem: lhs = rhs. More...
 
Theorem newReflTheorem (const Expr &e)
 Create a reflexivity theorem. More...
 
Theorem newAssumption (const Expr &thm, const Proof &pf, int scope=-1)
 
Theorem3 newTheorem3 (const Expr &thm, const Assumptions &assump, const Proof &pf)
 
Theorem3 newRWTheorem3 (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf)
 
void soundError (const std::string &file, int line, const std::string &cond, const std::string &msg)
 
- Protected Attributes inherited from CVC3::TheoremProducer
TheoremManagerd_tm
 
ExprManagerd_em
 
const bool * d_checkProofs
 
Op d_pfOp
 
Expr d_hole
 

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

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: