00001 /*****************************************************************************/ 00002 /*! 00003 * \file quant_proof_rules.h 00004 * 00005 * Author: Daniel Wichs 00006 * 00007 * Created: Jul 07 22:22:38 GMT 2003 00008 * 00009 * <hr> 00010 * 00011 * License to use, copy, modify, sell and/or distribute this software 00012 * and its documentation for any purpose is hereby granted without 00013 * royalty, subject to the terms and conditions defined in the \ref 00014 * LICENSE file provided with this distribution. 00015 * 00016 * <hr> 00017 * 00018 */ 00019 /*****************************************************************************/ 00020 #ifndef _cvc3__quant_proof_rules_h_ 00021 #define _cvc3__quant_proof_rules_h_ 00022 00023 #include <vector> 00024 00025 namespace CVC3 { 00026 00027 class Expr; 00028 class Theorem; 00029 00030 class QuantProofRules { 00031 public: 00032 //! Destructor 00033 virtual ~QuantProofRules() { } 00034 00035 virtual Theorem addNewConst(const Expr& e) =0; 00036 00037 //! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e 00038 virtual Theorem rewriteNotExists(const Expr& e) = 0; 00039 00040 //! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e 00041 virtual Theorem rewriteNotForall(const Expr& e) = 0; 00042 00043 //! Instantiate a universally quantified formula 00044 /*! From T|-FORALL(var): e generate T|-e' where e' is obtained 00045 * from e by instantiating bound variables with terms in 00046 * vector<Expr>& terms. The vector of terms should be the same 00047 * size as the vector of bound variables in e. Also elements in 00048 * each position i need to have matching types. 00049 * \param t1 is the quantifier (a Theorem) 00050 * \param terms are the terms to instantiate. 00051 * \param quantLevel is the quantification level for the theorem. 00052 */ 00053 virtual Theorem universalInst(const Theorem& t1, 00054 const std::vector<Expr>& terms, int quantLevel) = 0; 00055 00056 virtual Theorem universalInst(const Theorem& t1, 00057 const std::vector<Expr>& terms) = 0; 00058 00059 00060 virtual Theorem partialUniversalInst(const Theorem& t1, 00061 const std::vector<Expr>& terms, 00062 int quantLevel) = 0; 00063 00064 /*! @brief From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e 00065 * where vars' is obtained from vars by removing all bound variables 00066 * not used in e. If vars' is empty the produced theorem is just T|-e 00067 */ 00068 virtual Theorem boundVarElim(const Theorem& t1) = 0; 00069 00070 virtual Theorem packVar(const Theorem& t1) = 0; 00071 00072 virtual Theorem pullVarOut(const Theorem& t1) = 0; 00073 00074 virtual Theorem adjustVarUniv(const Theorem& t1, 00075 const std::vector<Expr>& newBvs) = 0; 00076 00077 }; 00078 } 00079 #endif