CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theory_simulate
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
30
class
SimulateTheoremProducer
:
31
public
SimulateProofRules
,
public
TheoremProducer
{
32
public
:
33
//! Constructor
34
SimulateTheoremProducer
(
TheoremManager
* tm):
TheoremProducer
(tm) { }
35
virtual
~SimulateTheoremProducer
() { }
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
Generated on Tue May 14 2013 09:02:08 for CVC3 by
1.8.3.1