CVC3

simulate_theorem_producer.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  *\file simulate_theorem_producer.h
00004  *\brief Implementation of the symbolic simulator proof rules
00005  *
00006  * Author: Sergey Berezin
00007  *
00008  * Created: Tue Oct  7 10:49:14 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_theorem_producer_h_
00023 #define _cvc3__theory_simulate__simulate_theorem_producer_h_
00024 
00025 #include "theorem_producer.h"
00026 #include "simulate_proof_rules.h"
00027 
00028 namespace CVC3 {
00029 
00030 class SimulateTheoremProducer:
00031     public SimulateProofRules, public TheoremProducer {
00032 public:
00033   //! Constructor
00034   SimulateTheoremProducer(TheoremManager* tm): TheoremProducer(tm) { }
00035   virtual ~SimulateTheoremProducer() { }
00036 
00037   virtual Theorem expandSimulate(const Expr& e);
00038 
00039   /*
00040 private:
00041   Expr substFreeTerm(const Expr& e, const Expr& oldE, const Expr& newE);
00042   Expr recursiveSubst(const Expr& e, const Expr& oldE, const Expr& newE,
00043           ExprMap<Expr>& visited);
00044   */
00045 
00046 }; // end of class SimulateTheoremProducer
00047 
00048 } // end of namespace CVC3 
00049 
00050 #endif