simulate_proof_rules.h

Go to the documentation of this file.
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

Generated on Thu Apr 13 16:57:33 2006 for CVC Lite by  doxygen 1.4.4