CVC3
|
#include <quant_proof_rules.h>
Inherited by CVC3::QuantTheoremProducer.
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 |
Definition at line 30 of file quant_proof_rules.h.
|
inlinevirtual |
Destructor.
Definition at line 33 of file quant_proof_rules.h.
Implemented in CVC3::QuantTheoremProducer.
Referenced by CVC3::TheoryQuant::checkSat(), and CVC3::TheoryQuant::theoryPreprocess().
Implemented in CVC3::QuantTheoremProducer.
Implemented in CVC3::QuantTheoremProducer.
Referenced by CVC3::TheoryQuant::rewrite().
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
Implemented in CVC3::QuantTheoremProducer.
Referenced by CVC3::TheoryQuant::assertFact().
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
Implemented in CVC3::QuantTheoremProducer.
Referenced by CVC3::TheoryQuant::assertFact().
|
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.
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().
|
pure virtual |
Implemented in CVC3::QuantTheoremProducer.
|
pure virtual |
Implemented in CVC3::QuantTheoremProducer.
|
pure virtual |
Implemented in CVC3::QuantTheoremProducer.
Referenced by CVC3::TheoryQuant::enqueueInst().
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().
Implemented in CVC3::QuantTheoremProducer.
Referenced by CVC3::TheoryQuant::assertFact(), and CVC3::CompleteInstPreProcessor::simplifyQuant().
Implemented in CVC3::QuantTheoremProducer.
|
pure virtual |
Implemented in CVC3::QuantTheoremProducer.