CVC3::QuantTheoremProducer Class Reference

#include <quant_theorem_producer.h>

Inheritance diagram for CVC3::QuantTheoremProducer:

Inheritance graph
[legend]
Collaboration diagram for CVC3::QuantTheoremProducer:

Collaboration graph
[legend]
List of all members.

Public Member Functions

Private Member Functions

Private Attributes


Detailed Description

Definition at line 29 of file quant_theorem_producer.h.


Constructor & Destructor Documentation

CVC3::QuantTheoremProducer::QuantTheoremProducer ( TheoremManager tm,
TheoryQuant theoryQuant 
) [inline]

Constructor.

Definition at line 37 of file quant_theorem_producer.h.


Member Function Documentation

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().

Theorem QuantTheoremProducer::addNewConst ( const Expr e  )  [virtual]

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().

Theorem QuantTheoremProducer::rewriteNotExists ( const Expr e  )  [virtual]

==> 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().

Theorem QuantTheoremProducer::rewriteNotForall ( const Expr e  )  [virtual]

==> 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.

Parameters:
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().

Theorem QuantTheoremProducer::boundVarElim ( const Theorem t1  )  [virtual]

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().

Theorem QuantTheoremProducer::packVar ( const Theorem t1  )  [virtual]

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().

Theorem QuantTheoremProducer::pullVarOut ( const Theorem t1  )  [virtual]

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().


Member Data Documentation

TheoryQuant* CVC3::QuantTheoremProducer::d_theoryQuant [private]

Definition at line 30 of file quant_theorem_producer.h.

Referenced by adjustVarUniv(), boundVarElim(), packVar(), partialUniversalInst(), pullVarOut(), and universalInst().


The documentation for this class was generated from the following files:
Generated on Tue Jul 3 14:42:09 2007 for CVC3 by  doxygen 1.5.1