CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
theory_simulate.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
*\file theory_simulate.h
4
*\brief Implementation of a symbolic simulator
5
*
6
* Author: Sergey Berezin
7
*
8
* Created: Tue Oct 7 10:13:15 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__include__theory_simulate_h_
23
#define _cvc3__include__theory_simulate_h_
24
25
#include "
theory.h
"
26
27
namespace
CVC3 {
28
29
class
SimulateProofRules;
30
31
/*****************************************************************************/
32
/*!
33
* \class TheorySimulate
34
* \ingroup Theories
35
* \brief "Theory" of symbolic simulation.
36
*
37
* Author: Sergey Berezin
38
*
39
* Created: Tue Oct 7 10:13:15 2003
40
*
41
* This theory owns the SIMULATE operator. It's job is to replace the above
42
* expressions by their definitions using rewrite rules.
43
*/
44
/*****************************************************************************/
45
46
class
TheorySimulate
:
public
Theory
{
47
private
:
48
//! Our local proof rules
49
SimulateProofRules
*
d_rules
;
50
//! Create proof rules for this theory
51
SimulateProofRules
*
createProofRules
();
52
public
:
53
//! Constructor
54
TheorySimulate
(
TheoryCore
* core);
55
//! Destructor
56
~TheorySimulate
();
57
// The required Theory API functions
58
void
assertFact
(
const
Theorem
& e) { }
59
void
checkSat
(
bool
fullEffort) { }
60
Theorem
rewrite
(
const
Expr
& e);
61
void
computeType
(
const
Expr
& e);
62
Expr
computeTCC
(
const
Expr
& e);
63
Expr
parseExprOp
(
const
Expr
& e);
64
ExprStream
&
print
(
ExprStream
& os,
const
Expr
& e);
65
};
// end of class TheorySimulate
66
67
}
// end of namespace CVC3
68
69
#endif
Generated on Tue May 14 2013 09:02:11 for CVC3 by
1.8.3.1