CVCL::QuantProofRules Class Reference

#include <quant_proof_rules.h>

Inheritance diagram for CVCL::QuantProofRules:

[legend]List of all members.

Public Member Functions

• virtual ~QuantProofRules ()

  Destructor.
  

• virtual Theorem rewriteNotExists (const Expr &e)=0

  ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
  

• virtual Theorem rewriteNotForall (const Expr &e)=0

  ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
  

• virtual Theorem universalInst (const Theorem &t1, const std::vector< Expr > &terms)=0

  Instantiate a universally quantified formula.
  

• virtual Theorem boundVarElim (const Theorem &t1)=0

  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.
  

---

Detailed Description

Definition at line 38 of file quant_proof_rules.h.

---

Constructor & Destructor Documentation

virtual CVCL::QuantProofRules::~QuantProofRules (   )  [inline, virtual]

Destructor. Definition at line 41 of file quant_proof_rules.h.

---

Member Function Documentation

virtual Theorem CVCL::QuantProofRules::rewriteNotExists (  const Expr &  e  )  [pure virtual]

==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e Implemented in CVCL::QuantTheoremProducer. Referenced by CVCL::TheoryQuant::assertFact().

virtual Theorem CVCL::QuantProofRules::rewriteNotForall (  const Expr &  e  )  [pure virtual]

==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e Implemented in CVCL::QuantTheoremProducer. Referenced by CVCL::TheoryQuant::assertFact().

virtual Theorem CVCL::QuantProofRules::universalInst (  const Theorem &  t1, const std::vector< Expr > &  terms )  [pure 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. Implemented in CVCL::QuantTheoremProducer. Referenced by CVCL::TheoryQuant::recInstantiate(), CVCL::TheoryQuant::semInst(), and CVCL::TheoryQuant::synInst().

virtual Theorem CVCL::QuantProofRules::boundVarElim (  const Theorem &  t1  )  [pure 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. Implemented in CVCL::QuantTheoremProducer. Referenced by CVCL::TheoryQuant::assertFact().

---

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

• quant_proof_rules.h

---