20 #ifndef _cvc3__quant_proof_rules_h_
21 #define _cvc3__quant_proof_rules_h_
60 const std::vector<Expr>& terms,
int quantLevel) = 0;
63 const std::vector<Expr>& terms) = 0;
67 const std::vector<Expr>& terms,
81 const std::vector<Expr>& newBvs) = 0;
virtual Theorem pullVarOut(const Theorem &t1)=0
Data structure of expressions in CVC3.
virtual Theorem adjustVarUniv(const Theorem &t1, const std::vector< Expr > &newBvs)=0
virtual Theorem addNewConst(const Expr &e)=0
virtual Theorem rewriteNotForall(const Expr &e)=0
==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e
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 remo...
virtual Theorem universalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel, Expr gterm)=0
Instantiate a universally quantified formula.
virtual Theorem rewriteNotExists(const Expr &e)=0
==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e
virtual Theorem partialUniversalInst(const Theorem &t1, const std::vector< Expr > &terms, int quantLevel)=0
virtual ~QuantProofRules()
Destructor.
virtual Theorem newRWThm(const Expr &e, const Expr &newE)=0
virtual Theorem packVar(const Theorem &t1)=0
virtual Theorem normalizeQuant(const Expr &e)=0