CVC3
2.4.1
|
#include <array_theorem_producer.h>
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) | |
Theorem | liftReadIte (const Expr &e) |
Lift ite over read. | |
Theorem | arrayNotEq (const Theorem &e) |
a /= b |- exists i. a[i] /= b[i] | |
Theorem | splitOnConstants (const Expr &a, const std::vector< Expr > &consts) |
Theorem | propagateIndexDiseq (const Theorem &read1eqread2isFalse) |
![]() | |
virtual | ~ArrayProofRules () |
![]() | |
TheoremProducer (TheoremManager *tm) | |
virtual | ~TheoremProducer () |
bool | withProof () |
Testing whether to generate proofs. | |
bool | withAssumptions () |
Testing whether to generate assumptions. | |
Proof | newLabel (const Expr &e) |
Create a new proof label (bound variable) for an assumption (formula) | |
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) | |
Proof | newPf (const Proof &label, const Proof &pf) |
Creating LAMBDA-abstraction (LAMBDA label proof). | |
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) | |
Proof | newPf (const std::vector< Proof > &labels, const Proof &pf) |
Private Attributes | |
TheoryArray * | d_theoryArray |
Additional Inherited Members | |
![]() | |
Theorem | newTheorem (const Expr &thm, const Assumptions &assump, const Proof &pf) |
Create a new theorem. See also newRWTheorem() and newReflTheorem() | |
Theorem | newRWTheorem (const Expr &lhs, const Expr &rhs, const Assumptions &assump, const Proof &pf) |
Create a rewrite theorem: lhs = rhs. | |
Theorem | newReflTheorem (const Expr &e) |
Create a reflexivity theorem. | |
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) |
![]() | |
TheoremManager * | d_tm |
ExprManager * | d_em |
const bool * | d_checkProofs |
Op | d_pfOp |
Expr | d_hole |
Definition at line 37 of file array_theorem_producer.h.
ArrayTheoremProducer::ArrayTheoremProducer | ( | TheoryArray * | theoryArray | ) |
Definition at line 46 of file array_theorem_producer.cpp.
Implements CVC3::ArrayProofRules.
Definition at line 70 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getType(), IF_DEBUG, CVC3::Expr::iffExpr(), CVC3::Expr::impExpr(), CVC3::Type::isBool(), CVC3::Expr::isEq(), CVC3::isWrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::READ, and CVC3::TheoremProducer::withProof().
Implements CVC3::ArrayProofRules.
Definition at line 122 of file array_theorem_producer.cpp.
References CVC3::Expr::andExpr(), DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getType(), IF_DEBUG, CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::Expr::isEq(), CVC3::isWrite(), MiniSat::left(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::READ, MiniSat::right(), CVC3::TheoremProducer::withProof(), and CVC3::WRITE.
Implements CVC3::ArrayProofRules.
Definition at line 149 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getType(), IF_DEBUG, CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::isRead(), CVC3::isWrite(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::READ, and CVC3::TheoremProducer::withProof().
Implements CVC3::ArrayProofRules.
Definition at line 173 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getType(), IF_DEBUG, CVC3::Expr::iffExpr(), CVC3::Type::isBool(), CVC3::isRead(), CVC3::isWrite(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::READ, and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::ArrayProofRules.
Definition at line 205 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::Expr::eqExpr(), CVC3::Theorem::getAssumptionsRef(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::Theorem::getRHS(), CVC3::isRead(), CVC3::Theorem::isRewrite(), CVC3::isWrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoremProducer::withProof(), and CVC3::WRITE.
Implements CVC3::ArrayProofRules.
Definition at line 244 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::isWrite(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoremProducer::withProof(), and CVC3::WRITE.
Implements CVC3::ArrayProofRules.
Definition at line 264 of file array_theorem_producer.cpp.
References DebugAssert, CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::Expr::getType(), CVC3::Type::isBool(), CVC3::isWrite(), CVC3::Expr::iteExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::TheoremProducer::withProof(), and CVC3::WRITE.
Beta reduction of array literal: |- (array x. f(x))[arg] = f(arg)
Implements CVC3::ArrayProofRules.
Definition at line 284 of file array_theorem_producer.cpp.
References CVC3::ARRAY_LITERAL, CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getBody(), CVC3::Expr::getKind(), CVC3::Expr::getVars(), CVC3::Expr::isClosure(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::READ, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Lift ite over read.
Implements CVC3::ArrayProofRules.
Definition at line 319 of file array_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::Expr::getKind(), ITE, CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::READ, CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
a /= b |- exists i. a[i] /= b[i]
Implements CVC3::ArrayProofRules.
Definition at line 338 of file array_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, d_theoryArray, EQ, CVC3::Expr::eqExpr(), EXISTS, CVC3::Theory::getBaseType(), CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::Expr::getKind(), CVC3::Theorem::getProof(), CVC3::isArray(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), NOT, CVC3::READ, CVC3::Theorem::toString(), and CVC3::TheoremProducer::withProof().
|
virtual |
Implements CVC3::ArrayProofRules.
Definition at line 363 of file array_theorem_producer.cpp.
References CVC3::andExpr(), CVC3::Assumptions::emptyAssump(), CVC3::Expr::eqExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::notExpr(), CVC3::orExpr(), and CVC3::TheoremProducer::withProof().
Implements CVC3::ArrayProofRules.
Definition at line 388 of file array_theorem_producer.cpp.
References CVC3::Expr::eqExpr(), CVC3::Theorem::getLHS(), CVC3::Theorem::getProof(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::notExpr(), and CVC3::TheoremProducer::withProof().
|
private |
Definition at line 39 of file array_theorem_producer.h.
Referenced by arrayNotEq().