00001 /*****************************************************************************/ 00002 /*! 00003 *\file simulate_proof_rules.h 00004 *\brief Abstract interface to the symbolic simulator proof rules 00005 * 00006 * Author: Sergey Berezin 00007 * 00008 * Created: Tue Oct 7 10:44:42 2003 00009 * 00010 * <hr> 00011 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford 00012 * Junior University and by New York University. 00013 * 00014 * License to use, copy, modify, sell and/or distribute this software 00015 * and its documentation for any purpose is hereby granted without 00016 * royalty, subject to the terms and conditions defined in the \ref 00017 * LICENSE file provided with this distribution. In particular: 00018 * 00019 * - The above copyright notice and this permission notice must appear 00020 * in all copies of the software and related documentation. 00021 * 00022 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES, 00023 * EXPRESSED OR IMPLIED. USE IT AT YOUR OWN RISK. 00024 * 00025 * <hr> 00026 * 00027 */ 00028 /*****************************************************************************/ 00029 00030 #ifndef _cvcl__theory_simulate__simulate_proof_rules_h_ 00031 #define _cvcl__theory_simulate__simulate_proof_rules_h_ 00032 00033 namespace CVCL { 00034 00035 class Expr; 00036 class Theorem; 00037 00038 class SimulateProofRules { 00039 public: 00040 //! Destructor 00041 virtual ~SimulateProofRules() { } 00042 00043 //! SIMULATE(f, s_0, i_1, ..., i_k, N) <=> f(...f(f(s_0, i_1), i_2), ... i_k) 00044 virtual Theorem expandSimulate(const Expr& e) = 0; 00045 00046 }; // end of class SimulateProofRules 00047 00048 } // end of namespace CVCL 00049 00050 #endif