CVC3::QuantProofRules Class Reference

#include <quant_proof_rules.h>

Inherited by 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

(

)

[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(), and CVC3::TheoryQuant::theoryPreprocess().

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]

Implemented in CVC3::QuantTheoremProducer.

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

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:

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::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]

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(), and CVC3::CompleteInstPreProcessor::simplifyQuant().

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:

• quant_proof_rules.h