CVC3  2.4.1
Public Member Functions | Private Member Functions | Private Attributes | List of all members
CVC3::QuantTheoremProducer Class Reference

#include <quant_theorem_producer.h>

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

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

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

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.


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