CVC3
2.4.1
|
#include <array_proof_rules.h>
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 |
Definition at line 35 of file array_proof_rules.h.
|
inlinevirtual |
Definition at line 38 of file array_proof_rules.h.
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::rewrite().
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::rewrite().
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().
Implemented in CVC3::ArrayTheoremProducer.
|
pure virtual |
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::checkSat(), CVC3::TheoryArray::pullIndex(), CVC3::TheoryArray::rewrite(), and CVC3::TheoryArray::update().
Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg)
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::rewrite().
Lift ite over read.
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::rewrite().
a /= b |- exists i. a[i] /= b[i]
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::assertFact().
|
pure virtual |
Implemented in CVC3::ArrayTheoremProducer.
|
pure virtual |
Implemented in CVC3::ArrayTheoremProducer.
Referenced by CVC3::TheoryArray::checkSat().