CVC3::QuantProofRules Class Reference

#include <quant_proof_rules.h>

Inheritance diagram for CVC3::QuantProofRules:

Inheritance graph
[legend]
List of all members.

Public Member Functions


Detailed Description

Definition at line 30 of file quant_proof_rules.h.


Constructor & Destructor Documentation

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

Destructor.

Definition at line 33 of file quant_proof_rules.h.


Member Function Documentation

virtual Theorem CVC3::QuantProofRules::addNewConst ( const Expr e  )  [pure virtual]

Implemented in CVC3::QuantTheoremProducer.

Referenced by CVC3::TheoryQuant::checkSat().

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

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

Implemented in CVC3::QuantTheoremProducer.

Referenced by CVC3::TheoryQuant::assertFact().

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

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

Implemented in CVC3::QuantTheoremProducer.

Referenced by CVC3::TheoryQuant::assertFact().

virtual Theorem CVC3::QuantProofRules::universalInst ( const Theorem t1,
const std::vector< Expr > &  terms,
int  quantLevel 
) [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.
quantLevel is the quantification level for the theorem.

Implemented in CVC3::QuantTheoremProducer.

Referenced by CVC3::TheoryQuant::enqueueInst(), and CVC3::TheoryQuant::recInstantiate().

virtual Theorem CVC3::QuantProofRules::universalInst ( const Theorem t1,
const std::vector< Expr > &  terms 
) [pure virtual]

Implemented in CVC3::QuantTheoremProducer.

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

Implemented in CVC3::QuantTheoremProducer.

Referenced by CVC3::TheoryQuant::enqueueInst().

virtual Theorem CVC3::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 CVC3::QuantTheoremProducer.

Referenced by CVC3::TheoryQuant::assertFact().

virtual Theorem CVC3::QuantProofRules::packVar ( const Theorem t1  )  [pure virtual]

Implemented in CVC3::QuantTheoremProducer.

Referenced by CVC3::TheoryQuant::assertFact().

virtual Theorem CVC3::QuantProofRules::pullVarOut ( const Theorem t1  )  [pure virtual]

Implemented in CVC3::QuantTheoremProducer.

Referenced by CVC3::TheoryQuant::assertFact().

virtual Theorem CVC3::QuantProofRules::adjustVarUniv ( const Theorem t1,
const std::vector< Expr > &  newBvs 
) [pure virtual]

Implemented in CVC3::QuantTheoremProducer.


The documentation for this class was generated from the following file:
Generated on Tue Jul 3 14:42:04 2007 for CVC3 by  doxygen 1.5.1