CVC3  2.4.1
Public Member Functions
CVC3::QuantProofRules Class Reference

#include <quant_proof_rules.h>

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

List of all members.

Public Member Functions

virtual ~QuantProofRules ()
 Destructor.
virtual Theorem addNewConst (const Expr &e)=0
virtual Theorem newRWThm (const Expr &e, const Expr &newE)=0
virtual Theorem normalizeQuant (const Expr &e)=0
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, int quantLevel, Expr gterm)=0
 Instantiate a universally quantified formula.
virtual Theorem universalInst (const Theorem &t1, const std::vector< Expr > &terms, int quantLevel)=0
virtual Theorem universalInst (const Theorem &t1, const std::vector< Expr > &terms)=0
virtual Theorem partialUniversalInst (const Theorem &t1, const std::vector< Expr > &terms, int quantLevel)=0
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.
virtual Theorem packVar (const Theorem &t1)=0
virtual Theorem pullVarOut (const Theorem &t1)=0
virtual Theorem adjustVarUniv (const Theorem &t1, const std::vector< Expr > &newBvs)=0

Detailed Description

Definition at line 30 of file quant_proof_rules.h.


Constructor & Destructor Documentation

virtual CVC3::QuantProofRules::~QuantProofRules ( )
inlinevirtual

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: