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 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford 00011 * Junior University and by New York University. 00012 * 00013 * License to use, copy, modify, sell and/or distribute this software 00014 * and its documentation for any purpose is hereby granted without 00015 * royalty, subject to the terms and conditions defined in the \ref 00016 * LICENSE file provided with this distribution. In particular: 00017 * 00018 * - The above copyright notice and this permission notice must appear 00019 * in all copies of the software and related documentation. 00020 * 00021 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, 00022 * EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK. 00023 * 00024 * <hr> 00025 * 00026 */ 00027 /*****************************************************************************/ 00028 #ifndef _CVC_lite__quant_proof_rules_h_ 00029 #define _CVC_lite__quant_proof_rules_h_ 00030 00031 #include <vector> 00032 00033 namespace CVCL { 00034 00035 class Expr; 00036 class Theorem; 00037 00038 class QuantProofRules { 00039 public: 00040 //! Destructor 00041 virtual ~QuantProofRules() { } 00042 00043 //! ==> NOT EXISTS (vars): e IFF FORALL (vars) NOT e 00044 virtual Theorem rewriteNotExists(const Expr& e) = 0; 00045 00046 //! ==> NOT FORALL (vars): e IFF EXISTS (vars) NOT e 00047 virtual Theorem rewriteNotForall(const Expr& e) = 0; 00048 00049 //! Instantiate a universally quantified formula 00050 /*! From T|-FORALL(var): e generate T|-e' where e' is obtained 00051 * from e by instantiating bound variables with terms in 00052 * vector<Expr>& terms. The vector of terms should be the same 00053 * size as the vector of bound variables in e. Also elements in 00054 * each position i need to have matching types. 00055 * \param t1 is the quantifier (a Theorem) 00056 * \param terms are the terms to instantiate. 00057 */ 00058 virtual Theorem universalInst(const Theorem& t1, 00059 const std::vector<Expr>& terms) = 0; 00060 00061 /*! @brief From T|- QUANTIFIER (vars): e we get T|-QUANTIFIER(vars') e 00062 * where vars' is obtained from vars by removing all bound variables 00063 * not used in e. If vars' is empty the produced theorem is just T|-e 00064 */ 00065 virtual Theorem boundVarElim(const Theorem& t1) = 0; 00066 00067 }; 00068 } 00069 #endif