CVC3  2.4.1
simulate_theorem_producer.h
Go to the documentation of this file.
1 /*****************************************************************************/
2 /*!
3  *\file simulate_theorem_producer.h
4  *\brief Implementation of the symbolic simulator proof rules
5  *
6  * Author: Sergey Berezin
7  *
8  * Created: Tue Oct 7 10:49:14 2003
9  *
10  * <hr>
11  *
12  * License to use, copy, modify, sell and/or distribute this software
13  * and its documentation for any purpose is hereby granted without
14  * royalty, subject to the terms and conditions defined in the \ref
15  * LICENSE file provided with this distribution.
16  *
17  * <hr>
18  *
19  */
20 /*****************************************************************************/
21 
22 #ifndef _cvc3__theory_simulate__simulate_theorem_producer_h_
23 #define _cvc3__theory_simulate__simulate_theorem_producer_h_
24 
25 #include "theorem_producer.h"
26 #include "simulate_proof_rules.h"
27 
28 namespace CVC3 {
29 
31  public SimulateProofRules, public TheoremProducer {
32 public:
33  //! Constructor
36 
37  virtual Theorem expandSimulate(const Expr& e);
38 
39  /*
40 private:
41  Expr substFreeTerm(const Expr& e, const Expr& oldE, const Expr& newE);
42  Expr recursiveSubst(const Expr& e, const Expr& oldE, const Expr& newE,
43  ExprMap<Expr>& visited);
44  */
45 
46 }; // end of class SimulateTheoremProducer
47 
48 } // end of namespace CVC3
49 
50 #endif
Data structure of expressions in CVC3.
Definition: expr.h:133
virtual Theorem expandSimulate(const Expr &e)
SIMULATE(f, s_0, i_1, ..., i_k, N) <=> f(...f(f(s_0, i_1), i_2), ... i_k)
Abstract interface to the symbolic simulator proof rules.
SimulateTheoremProducer(TheoremManager *tm)
Constructor.