CVC3
2.4.1
|
#include <quant_theorem_producer.h>
Public Member Functions | |
QuantTheoremProducer (TheoremManager *tm, TheoryQuant *theoryQuant) | |
Constructor. More... | |
virtual Theorem | addNewConst (const Expr &e) |
virtual Theorem | newRWThm (const Expr &e, const Expr &newE) |
do not use this rule, this is for debug only More... | |
virtual Theorem | normalizeQuant (const Expr &e) |
virtual Theorem | rewriteNotExists (const Expr &e) |
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e More... | |
virtual Theorem | rewriteNotForall (const Expr &e) |
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e More... | |
virtual Theorem | universalInst (const Theorem &t1, const std::vector< Expr > &terms, int quantLevel, Expr gterm) |
Instantiate a universally quantified formula. More... | |
virtual Theorem | universalInst (const Theorem &t1, const std::vector< Expr > &terms, int quantLevel) |
Instantiate a universally quantified formula. More... | |
virtual Theorem | universalInst (const Theorem &t1, const std::vector< Expr > &terms) |
virtual Theorem | partialUniversalInst (const Theorem &t1, const std::vector< Expr > &terms, int quantLevel) |
virtual Theorem | boundVarElim (const Theorem &t1) |
From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e where vars' is obtained from vars by removing all bound variables not used in e. If vars' is empty the produced theorem is just T|-e. More... | |
virtual Theorem | adjustVarUniv (const Theorem &t1, const std::vector< Expr > &newBvs) |
adjust the order of bound vars, newBvs begin first More... | |
virtual Theorem | packVar (const Theorem &t1) |
pack (forall (x) forall (y)) into (forall (x y)) More... | |
virtual Theorem | pullVarOut (const Theorem &t1) |
![]() | |
virtual | ~QuantProofRules () |
Destructor. More... | |
![]() | |
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 Member Functions | |
void | recFindBoundVars (const Expr &e, ExprMap< bool > &boundVars, ExprMap< bool > &visited) |
find all bound variables in e and maps them to true in boundVars More... | |
Private Attributes | |
TheoryQuant * | d_theoryQuant |
std::map< Expr, int > | d_typeFound |
Additional Inherited Members | |
![]() | |
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) |
![]() | |
TheoremManager * | d_tm |
ExprManager * | d_em |
const bool * | d_checkProofs |
Op | d_pfOp |
Expr | d_hole |
Definition at line 29 of file quant_theorem_producer.h.
|
inline |
|
private |
find all bound variables in e and maps them to true in boundVars
Definition at line 493 of file quant_theorem_producer.cpp.
References CVC3::Expr::begin(), BOUND_VAR, CVC3::ExprMap< Data >::count(), CVC3::Expr::end(), EXISTS, FORALL, CVC3::Expr::getBody(), and CVC3::Expr::getKind().
Implements CVC3::QuantProofRules.
Definition at line 64 of file quant_theorem_producer.cpp.
do not use this rule, this is for debug only
Implements CVC3::QuantProofRules.
Definition at line 73 of file quant_theorem_producer.cpp.
Implements CVC3::QuantProofRules.
Definition at line 82 of file quant_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, EXISTS, FORALL, CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Type::getExpr(), CVC3::Expr::getTriggers(), CVC3::Expr::getVars(), CVC3::int2string(), CVC3::Expr::isExists(), CVC3::Expr::isForall(), CVC3::ExprManager::newBoundVarExpr(), CVC3::ExprManager::newClosureExpr(), CVC3::Expr::setType(), CVC3::Expr::substExpr(), and CVC3::Expr::toString().
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
Implements CVC3::QuantProofRules.
Definition at line 139 of file quant_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, FORALL, CVC3::Expr::getEM(), CVC3::Expr::isExists(), CVC3::Expr::isNot(), CVC3::ExprManager::newClosureExpr(), and CVC3::Expr::toString().
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
Implements CVC3::QuantProofRules.
Definition at line 49 of file quant_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, EXISTS, CVC3::Expr::getEM(), CVC3::Expr::isForall(), CVC3::Expr::isNot(), CVC3::ExprManager::newClosureExpr(), and CVC3::Expr::toString().
|
virtual |
Instantiate a universally quantified formula.
From T|-FORALL(var): e generate T|-e' where e' is obtained from e by instantiating bound variables with terms in vector<Expr>& terms. The vector of terms should be the same size as the vector of bound variables in e. Also elements in each position i need to have matching types.
t1 | is the quantifier (a Theorem) |
terms | are the terms to instantiate. |
quantLevel | the quantification level for the theorem. |
Implements CVC3::QuantProofRules.
Definition at line 154 of file quant_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Theorem::getQuantLevel(), CVC3::Expr::getVars(), CVC3::Expr::impExpr(), CVC3::Expr::isForall(), CVC3::Expr::isNull(), RAW_LIST, CVC3::Theorem::setQuantLevel(), CVC3::Expr::substExpr(), CVC3::Expr::toString(), and CVC3::ExprManager::trueExpr().
|
virtual |
Instantiate a universally quantified formula.
From T|-FORALL(var): e generate T|-psi => e' where e' is obtained from e by instantiating bound variables with terms in vector<Expr>& terms. The vector of terms should be the same size as the vector of bound variables in e. Also elements in each position i need to have matching base types. psi is the conjunction of subtype predicates for the bound variables of the quanitfied expression.
t1 | the quantifier (a Theorem) |
terms | the terms to instantiate. |
quantLevel | the quantification level for the formula |
Implements CVC3::QuantProofRules.
Definition at line 258 of file quant_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Theorem::getQuantLevel(), CVC3::Expr::getVars(), CVC3::Expr::impExpr(), CVC3::Expr::isForall(), RAW_LIST, CVC3::Theorem::setQuantLevel(), CVC3::Expr::substExpr(), CVC3::Expr::toString(), and CVC3::ExprManager::trueExpr().
|
virtual |
Implements CVC3::QuantProofRules.
Definition at line 332 of file quant_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CHECK_PROOFS, CHECK_SOUND, CVC3::Theorem::getAssumptionsRef(), CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Theorem::getQuantLevel(), CVC3::Expr::getVars(), CVC3::Expr::impExpr(), CVC3::Expr::isForall(), RAW_LIST, CVC3::Theorem::setQuantLevel(), CVC3::Expr::substExpr(), CVC3::Expr::toString(), and CVC3::ExprManager::trueExpr().
|
virtual |
Implements CVC3::QuantProofRules.
Definition at line 408 of file quant_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CHECK_PROOFS, CHECK_SOUND, std::endl(), FORALL, CVC3::Theorem::getAssumptionsRef(), CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Theorem::getQuantLevel(), CVC3::Expr::getVars(), CVC3::Expr::impExpr(), CVC3::Expr::isForall(), CVC3::ExprManager::newClosureExpr(), CVC3::Theorem::setQuantLevel(), CVC3::Expr::substExpr(), CVC3::Expr::toString(), and CVC3::ExprManager::trueExpr().
From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e where vars' is obtained from vars by removing all bound variables not used in e. If vars' is empty the produced theorem is just T|-e.
Implements CVC3::QuantProofRules.
Definition at line 748 of file quant_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::ExprMap< Data >::count(), EXISTS, FORALL, CVC3::Theorem::getAssumptionsRef(), CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getVars(), CVC3::Expr::isExists(), CVC3::Expr::isForall(), CVC3::ExprManager::newClosureExpr(), and CVC3::Expr::toString().
|
virtual |
adjust the order of bound vars, newBvs begin first
Implements CVC3::QuantProofRules.
Definition at line 510 of file quant_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::ExprMap< Data >::count(), FORALL, CVC3::Theorem::getAssumptionsRef(), CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getVars(), CVC3::Expr::isForall(), CVC3::ExprManager::newClosureExpr(), and CVC3::Expr::toString().
pack (forall (x) forall (y)) into (forall (x y))
Implements CVC3::QuantProofRules.
Definition at line 568 of file quant_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, FORALL, CVC3::Theorem::getAssumptionsRef(), CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getVars(), CVC3::Expr::isForall(), CVC3::ExprManager::newClosureExpr(), and CVC3::Expr::toString().
convert (forall (x) ... forall (y)) into (forall (x y)...) convert (exists (x) ... exists (y)) into (exists (x y)...)
Implements CVC3::QuantProofRules.
Definition at line 612 of file quant_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CHECK_PROOFS, CHECK_SOUND, EXISTS, FORALL, CVC3::Theorem::getAssumptionsRef(), CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getVars(), CVC3::Expr::impExpr(), CVC3::Expr::isAnd(), CVC3::Expr::isExists(), CVC3::Expr::isForall(), CVC3::Expr::isImpl(), CVC3::Expr::isNot(), CVC3::ExprManager::newClosureExpr(), CVC3::Expr::notExpr(), CVC3::orExpr(), and CVC3::Expr::toString().
|
private |
Definition at line 30 of file quant_theorem_producer.h.
|
private |
Definition at line 31 of file quant_theorem_producer.h.
Referenced by QuantTheoremProducer().