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
theorem_producer.h
CVC3::Expr
Data structure of expressions in CVC3.
Definition:
expr.h:133
CVC3::Theorem
Definition:
theorem.h:76
CVC3::SimulateTheoremProducer::~SimulateTheoremProducer
virtual ~SimulateTheoremProducer()
Definition:
simulate_theorem_producer.h:35
CVC3::TheoremProducer
Definition:
theorem_producer.h:91
CVC3::SimulateTheoremProducer::expandSimulate
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)
Definition:
simulate_theorem_producer.cpp:46
CVC3::SimulateTheoremProducer
Definition:
simulate_theorem_producer.h:30
CVC3::SimulateProofRules
Definition:
simulate_proof_rules.h:30
simulate_proof_rules.h
Abstract interface to the symbolic simulator proof rules.
CVC3::SimulateTheoremProducer::SimulateTheoremProducer
SimulateTheoremProducer(TheoremManager *tm)
Constructor.
Definition:
simulate_theorem_producer.h:34
CVC3::TheoremManager
Definition:
theorem_manager.h:39
Generated on Wed Aug 27 2014 16:11:37 for CVC3 by
1.8.7