#include <quant_theorem_producer.h>

Inherits CVC3::QuantProofRules, and CVC3::TheoremProducer.

Collaboration diagram for CVC3::QuantTheoremProducer:

[legend]

List of all members.

Public Member Functions

QuantTheoremProducer (TheoremManager *tm, TheoryQuant *theoryQuant)
Constructor.
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
virtual Theorem normalizeQuant (const Expr &e)
virtual Theorem rewriteNotExists (const Expr &e)
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
virtual Theorem rewriteNotForall (const Expr &e)
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
virtual Theorem universalInst (const Theorem &t1, const std::vector< Expr > &terms, int quantLevel, Expr gterm)
Instantiate a universally quantified formula.
virtual Theorem universalInst (const Theorem &t1, const std::vector< Expr > &terms, int quantLevel)
Instantiate a universally quantified formula.
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.
virtual Theorem adjustVarUniv (const Theorem &t1, const std::vector< Expr > &newBvs)
adjust the order of bound vars, newBvs begin first
virtual Theorem packVar (const Theorem &t1)
pack (forall (x) forall (y)) into (forall (x y))
virtual Theorem pullVarOut (const Theorem &t1)

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

Private Attributes

TheoryQuant * d_theoryQuant
std::map< Expr, int > d_typeFound

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 39 of file quant_theorem_producer.h.

References d_typeFound.

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

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

Implements CVC3::QuantProofRules.

Definition at line 64 of file quant_theorem_producer.cpp.

Theorem QuantTheoremProducer::newRWThm	(	const Expr &	e,
		const Expr &	newE
	)		`[virtual]`

do not use this rule, this is for debug only

Implements CVC3::QuantProofRules.

Definition at line 73 of file quant_theorem_producer.cpp.

Theorem QuantTheoremProducer::normalizeQuant ( const Expr & e ) [virtual]

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

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

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, EXISTS, CVC3::Expr::getEM(), CVC3::Expr::isForall(), CVC3::Expr::isNot(), CVC3::ExprManager::newClosureExpr(), and CVC3::Expr::toString().

Theorem QuantTheoremProducer::universalInst	(	const Theorem &	t1,
		const std::vector< Expr > &	terms,
		int	quantLevel,
		Expr	gterm
	)		`[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 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().

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

Parameters:

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

Theorem QuantTheoremProducer::universalInst	(	const Theorem &	t1,
		const std::vector< Expr > &	terms
	)		`[virtual]`

Theorem QuantTheoremProducer::partialUniversalInst	(	const Theorem &	t1,
		const std::vector< Expr > &	terms,
		int	quantLevel
	)		`[virtual]`

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