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  *
00012  * License to use, copy, modify, sell and/or distribute this software
00013  * and its documentation for any purpose is hereby granted without
00014  * royalty, subject to the terms and conditions defined in the \ref
00015  * LICENSE file provided with this distribution.
00016  * 
00017  * <hr>
00018  * 
00019  */
00020 /*****************************************************************************/
00021 
00022 #ifndef _cvc3__theory_simulate__simulate_proof_rules_h_
00023 #define _cvc3__theory_simulate__simulate_proof_rules_h_
00024 
00025 namespace CVC3 {
00026 
00027   class Expr;
00028   class Theorem;
00029 
00030 class SimulateProofRules {
00031 public:
00032   //! Destructor
00033   virtual ~SimulateProofRules() { }
00034 
00035   //! SIMULATE(f, s_0, i_1, ..., i_k, N) <=> f(...f(f(s_0, i_1), i_2), ... i_k)
00036   virtual Theorem expandSimulate(const Expr& e) = 0;
00037 
00038 }; // end of class SimulateProofRules
00039 
00040 } // end of namespace CVC3
00041 
00042 #endif

Generated on Wed Nov 18 16:13:31 2009 for CVC3 by  doxygen 1.5.2