|
CVC3
|
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
1.7.3