CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes
CVC3::QuantTheoremProducer Class Reference

#include <quant_theorem_producer.h>

Inheritance diagram for CVC3::QuantTheoremProducer:
CVC3::QuantProofRules CVC3::TheoremProducer

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)
- Public Member Functions inherited from CVC3::QuantProofRules
virtual ~QuantProofRules ()
 Destructor.
- Public Member Functions inherited from CVC3::TheoremProducer
 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 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

TheoryQuantd_theoryQuant
std::map< Expr, int > d_typeFound

Additional Inherited Members

- Protected Member Functions inherited from CVC3::TheoremProducer
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)
- Protected Attributes inherited from CVC3::TheoremProducer
TheoremManagerd_tm
ExprManagerd_em
const bool * d_checkProofs
Op d_pfOp
Expr d_hole

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
Theorem QuantTheoremProducer::rewriteNotForall ( const Expr e)
virtual
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:
t1is the quantifier (a Theorem)
termsare the terms to instantiate.
quantLevelthe 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:
t1the quantifier (a Theorem)
termsthe terms to instantiate.
quantLevelthe 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().

Theorem QuantTheoremProducer::adjustVarUniv ( const Theorem t1,
const std::vector< Expr > &  newBvs 
)
virtual
Theorem QuantTheoremProducer::packVar ( const Theorem t1)
virtual
Theorem QuantTheoremProducer::pullVarOut ( const Theorem t1)
virtual

Member Data Documentation

TheoryQuant* CVC3::QuantTheoremProducer::d_theoryQuant
private

Definition at line 30 of file quant_theorem_producer.h.

std::map<Expr,int> CVC3::QuantTheoremProducer::d_typeFound
private

Definition at line 31 of file quant_theorem_producer.h.

Referenced by QuantTheoremProducer().


The documentation for this class was generated from the following files: