arrayNotEq(const Theorem &e)=0 | CVC3::ArrayProofRules | [pure virtual] |
interchangeIndices(const Expr &e)=0 | CVC3::ArrayProofRules | [pure virtual] |
liftReadIte(const Expr &e)=0 | CVC3::ArrayProofRules | [pure virtual] |
readArrayLiteral(const Expr &e)=0 | CVC3::ArrayProofRules | [pure virtual] |
rewriteReadWrite(const Expr &e)=0 | CVC3::ArrayProofRules | [pure virtual] |
rewriteReadWrite2(const Expr &e)=0 | CVC3::ArrayProofRules | [pure virtual] |
rewriteRedundantWrite1(const Theorem &v_eq_r, const Expr &write)=0 | CVC3::ArrayProofRules | [pure virtual] |
rewriteRedundantWrite2(const Expr &e)=0 | CVC3::ArrayProofRules | [pure virtual] |
rewriteSameStore(const Expr &e, int n)=0 | CVC3::ArrayProofRules | [pure virtual] |
rewriteWriteWrite(const Expr &e)=0 | CVC3::ArrayProofRules | [pure virtual] |
~ArrayProofRules() | CVC3::ArrayProofRules | [inline, virtual] |