20 #ifndef _cvc3__quant_theorem_producer_h_
21 #define _cvc3__quant_theorem_producer_h_
63 const std::vector<Expr>& terms,
int quantLevel ,
67 const std::vector<Expr>& terms,
int quantLevel);
70 const std::vector<Expr>& terms);
74 const std::vector<Expr>& terms,
85 const std::vector<Expr>& newBvs);
Data structure of expressions in CVC3.
virtual Theorem pullVarOut(const Theorem &t1)
void recFindBoundVars(const Expr &e, ExprMap< bool > &boundVars, ExprMap< bool > &visited)
find all bound variables in e and maps them to true in boundVars
virtual Theorem rewriteNotExists(const Expr &e)
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
virtual Theorem universalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel, Expr gterm)
Instantiate a universally quantified formula.
virtual Theorem boundVarElim(const Theorem &t1)
From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e where vars' is obtained from vars by remo...
virtual Theorem adjustVarUniv(const Theorem &t1, const std::vector< Expr > &newBvs)
adjust the order of bound vars, newBvs begin first
virtual Theorem rewriteNotForall(const Expr &e)
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
virtual Theorem packVar(const Theorem &t1)
pack (forall (x) forall (y)) into (forall (x y))
virtual Theorem partialUniversalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel)
virtual Theorem newRWThm(const Expr &e, const Expr &newE)
do not use this rule, this is for debug only
QuantTheoremProducer(TheoremManager *tm, TheoryQuant *theoryQuant)
Constructor.
virtual Theorem addNewConst(const Expr &e)
TheoryQuant * d_theoryQuant
virtual Theorem normalizeQuant(const Expr &e)
std::map< Expr, int > d_typeFound
This theory handles quantifiers.