CVC3
Public Member Functions

CVC3::QuantProofRules Class Reference

#include <quant_proof_rules.h>

Inherited by CVC3::QuantTheoremProducer.

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]
virtual Theorem CVC3::QuantProofRules::newRWThm ( const Expr e,
const Expr newE 
) [pure virtual]

Implemented in CVC3::QuantTheoremProducer.

virtual Theorem CVC3::QuantProofRules::normalizeQuant ( const Expr e) [pure virtual]
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,
Expr  gterm 
) [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:
t1is the quantifier (a Theorem)
termsare the terms to instantiate.
quantLevelis the quantification level for the theorem.

Implemented in CVC3::QuantTheoremProducer.

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

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

Implemented in CVC3::QuantTheoremProducer.

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]
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]
virtual Theorem CVC3::QuantProofRules::pullVarOut ( const Theorem t1) [pure virtual]

Implemented in CVC3::QuantTheoremProducer.

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: