CVCL::QuantTheoremProducer Class Reference

#include <quant_theorem_producer.h>

Inheritance diagram for CVCL::QuantTheoremProducer:

[legend]Collaboration diagram for CVCL::QuantTheoremProducer:

[legend]List of all members.

Public Member Functions

• QuantTheoremProducer (TheoremManager *tm, TheoryQuant *theoryQuant)

  Constructor.
  

• 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)

  Instantiate a universally quantified formula.
  

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

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

---

Detailed Description

Definition at line 37 of file quant_theorem_producer.h.

---

Constructor & Destructor Documentation

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

Constructor. Definition at line 45 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 154 of file quant_theorem_producer.cpp. References CVCL::Expr::begin(), CVCL::BOUND_VAR, CVCL::ExprMap< Data >::count(), CVCL::Expr::end(), CVCL::EXISTS, CVCL::FORALL, CVCL::Expr::getBody(), and CVCL::Expr::getKind(). Referenced by boundVarElim().

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

==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e Implements CVCL::QuantProofRules. Definition at line 75 of file quant_theorem_producer.cpp. References CVCL::FORALL, CVCL::Expr::getEM(), CVCL::Expr::isExists(), CVCL::Expr::isNot(), CVCL::ExprManager::newClosureExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

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

==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e Implements CVCL::QuantProofRules. Definition at line 57 of file quant_theorem_producer.cpp. References CVCL::EXISTS, CVCL::Expr::getEM(), CVCL::Expr::isForall(), CVCL::Expr::isNot(), CVCL::ExprManager::newClosureExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newRWTheorem(), CVCL::Expr::toString(), and CVCL::TheoremProducer::withProof().

virtual Theorem CVCL::QuantTheoremProducer::universalInst (  const Theorem &  t1, const std::vector< Expr > &  terms )  [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. Implements CVCL::QuantProofRules.

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 CVCL::QuantProofRules. Definition at line 174 of file quant_theorem_producer.cpp. References CVCL::ExprMap< Data >::count(), d_theoryQuant, CVCL::EXISTS, CVCL::FORALL, CVCL::Theorem::getAssumptionsCopy(), CVCL::Expr::getBody(), CVCL::Theory::getEM(), CVCL::Theorem::getExpr(), CVCL::Theorem::getProof(), CVCL::Expr::getVars(), CVCL::Expr::isExists(), CVCL::Expr::isForall(), CVCL::ExprManager::newClosureExpr(), CVCL::TheoremProducer::newPf(), CVCL::TheoremProducer::newTheorem(), recFindBoundVars(), CVCL::Expr::toString(), CVCL::TheoremProducer::withAssumptions(), and CVCL::TheoremProducer::withProof().

---

Member Data Documentation

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

Definition at line 38 of file quant_theorem_producer.h. Referenced by boundVarElim().

---

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

• quant_theorem_producer.h
• quant_theorem_producer.cpp

---