27 #ifndef _cvc3__theory_array__array_theorem_producer_h_
28 #define _cvc3__theory_array__array_theorem_producer_h_
TheoryArray * d_theoryArray
Data structure of expressions in CVC3.
Theorem readArrayLiteral(const Expr &e)
Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg)
Theorem rewriteReadWrite2(const Expr &e)
Theorem interchangeIndices(const Expr &e)
Theorem propagateIndexDiseq(const Theorem &read1eqread2isFalse)
Theorem rewriteRedundantWrite2(const Expr &e)
Theorem rewriteSameStore(const Expr &e, int n)
Theorem rewriteWriteWrite(const Expr &e)
This theory handles arrays.
Theorem liftReadIte(const Expr &e)
Lift ite over read.
ArrayTheoremProducer(TheoryArray *theoryArray)
Theorem rewriteRedundantWrite1(const Theorem &v_eq_r, const Expr &write)
Theorem rewriteReadWrite(const Expr &e)
Theorem splitOnConstants(const Expr &a, const std::vector< Expr > &consts)
Theorem arrayNotEq(const Theorem &e)
a /= b |- exists i. a[i] /= b[i]