#include <quant_theorem_producer.h>
Inheritance diagram for CVC3::QuantTheoremProducer:
Definition at line 29 of file quant_theorem_producer.h.
CVC3::QuantTheoremProducer::QuantTheoremProducer | ( | TheoremManager * | tm, | |
TheoryQuant * | theoryQuant | |||
) | [inline] |
void QuantTheoremProducer::recFindBoundVars | ( | const Expr & | e, | |
ExprMap< bool > & | boundVars, | |||
ExprMap< bool > & | visited | |||
) | [private] |
find all bound variables in e and maps them to true in boundVars
Definition at line 281 of file quant_theorem_producer.cpp.
References CVC3::Expr::begin(), CVC3::BOUND_VAR, CVC3::ExprMap< Data >::count(), CVC3::Expr::end(), CVC3::EXISTS, CVC3::FORALL, CVC3::Expr::getBody(), and CVC3::Expr::getKind().
Referenced by boundVarElim().
Implements CVC3::QuantProofRules.
Definition at line 64 of file quant_theorem_producer.cpp.
References CVC3::Assumptions::emptyAssump(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), and CVC3::TheoremProducer::withProof().
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
Implements CVC3::QuantProofRules.
Definition at line 74 of file quant_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::Assumptions::emptyAssump(), CVC3::FORALL, CVC3::Expr::getEM(), CVC3::Expr::isExists(), CVC3::Expr::isNot(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
==> 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, CVC3::Assumptions::emptyAssump(), CVC3::EXISTS, CVC3::Expr::getEM(), CVC3::Expr::isForall(), CVC3::Expr::isNot(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newRWTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Theorem QuantTheoremProducer::universalInst | ( | const Theorem & | t1, | |
const std::vector< Expr > & | terms, | |||
int | quantLevel | |||
) | [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 98 of file quant_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CHECK_PROOFS, CHECK_SOUND, d_theoryQuant, CVC3::Theorem::getAssumptionsRef(), CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Theory::getTypePred(), CVC3::Expr::getVars(), CVC3::Expr::impExpr(), CVC3::Expr::isForall(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::setQuantLevel(), CVC3::Expr::substExpr(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Theorem QuantTheoremProducer::universalInst | ( | const Theorem & | t1, | |
const std::vector< Expr > & | terms | |||
) | [virtual] |
Implements CVC3::QuantProofRules.
Definition at line 151 of file quant_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CHECK_PROOFS, CHECK_SOUND, d_theoryQuant, CVC3::Theorem::getAssumptionsRef(), CVC3::Theory::getBaseType(), CVC3::Expr::getBody(), CVC3::Expr::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::TheoryCore::getQuantLevelForTerm(), CVC3::Theory::getTypePred(), CVC3::Expr::getVars(), CVC3::Expr::impExpr(), CVC3::Expr::isForall(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::setQuantLevel(), CVC3::Expr::substExpr(), CVC3::Theory::theoryCore(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
Theorem QuantTheoremProducer::partialUniversalInst | ( | const Theorem & | t1, | |
const std::vector< Expr > & | terms, | |||
int | quantLevel | |||
) | [virtual] |
Implements CVC3::QuantProofRules.
Definition at line 204 of file quant_theorem_producer.cpp.
References CVC3::Expr::andExpr(), CHECK_PROOFS, CHECK_SOUND, d_theoryQuant, CVC3::FORALL, CVC3::Theorem::getAssumptionsRef(), CVC3::Theory::getBaseType(), CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Expr::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Theory::getTypePred(), CVC3::Expr::getVars(), CVC3::Expr::impExpr(), CVC3::Expr::isForall(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Theorem::setQuantLevel(), CVC3::Expr::substExpr(), CVC3::Expr::toString(), CVC3::ExprManager::trueExpr(), and CVC3::TheoremProducer::withProof().
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 494 of file quant_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, d_theoryQuant, CVC3::EXISTS, CVC3::FORALL, CVC3::Theorem::getAssumptionsRef(), CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getVars(), CVC3::Expr::isExists(), CVC3::Expr::isForall(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), recFindBoundVars(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Theorem QuantTheoremProducer::adjustVarUniv | ( | const Theorem & | t1, | |
const std::vector< Expr > & | newBvs | |||
) | [virtual] |
adjust the order of bound vars, newBvs begin first
Implements CVC3::QuantProofRules.
Definition at line 298 of file quant_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, CVC3::ExprMap< Data >::count(), d_theoryQuant, CVC3::FORALL, CVC3::Theorem::getAssumptionsRef(), CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getVars(), CVC3::ExprMap< Data >::insert(), CVC3::Expr::isForall(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
pack (forall (x) forall (y)) into (forall (x y))
Implements CVC3::QuantProofRules.
Definition at line 356 of file quant_theorem_producer.cpp.
References CHECK_PROOFS, CHECK_SOUND, d_theoryQuant, CVC3::FORALL, CVC3::Theorem::getAssumptionsRef(), CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::Theorem::getProof(), CVC3::Expr::getVars(), CVC3::Expr::isForall(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
pack (forall (x) ... forall (y)) into (forall (x y)...)
Implements CVC3::QuantProofRules.
Definition at line 398 of file quant_theorem_producer.cpp.
References CVC3::andExpr(), CHECK_PROOFS, CHECK_SOUND, d_theoryQuant, FatalAssert, CVC3::FORALL, CVC3::Expr::getBody(), CVC3::Theory::getEM(), CVC3::Theorem::getExpr(), CVC3::Expr::getVars(), CVC3::Expr::isForall(), CVC3::ExprManager::newClosureExpr(), CVC3::TheoremProducer::newPf(), CVC3::TheoremProducer::newTheorem(), CVC3::Expr::notExpr(), CVC3::orExpr(), CVC3::Expr::toString(), and CVC3::TheoremProducer::withProof().
Definition at line 30 of file quant_theorem_producer.h.
Referenced by adjustVarUniv(), boundVarElim(), packVar(), partialUniversalInst(), pullVarOut(), and universalInst().