CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
include
theorem_manager.h
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file theorem_manager.h
4
*
5
* Author: Sergey Berezin, Tue Feb 4 14:29:25 2003
6
*
7
* Created: Feb 05 18:29:37 GMT 2003
8
*
9
* <hr>
10
*
11
* License to use, copy, modify, sell and/or distribute this software
12
* and its documentation for any purpose is hereby granted without
13
* royalty, subject to the terms and conditions defined in the \ref
14
* LICENSE file provided with this distribution.
15
*
16
* <hr>
17
*
18
* CLASS: TheoremManager
19
*
20
*
21
* Holds the shared data for the class Theorem
22
*/
23
/*****************************************************************************/
24
25
#ifndef _cvc3__theorem_manager_h_
26
#define _cvc3__theorem_manager_h_
27
28
#include "
debug.h
"
29
#include "
compat_hash_map.h
"
30
31
namespace
CVC3 {
32
33
class
ContextManager;
34
class
ExprManager;
35
class
CLFlags;
36
class
MemoryManager;
37
class
CommonProofRules;
38
39
class
TheoremManager
{
40
private
:
41
ContextManager
*
d_cm
;
42
ExprManager
*
d_em
;
43
const
CLFlags
&
d_flags
;
44
MemoryManager
*
d_mm
;
45
MemoryManager
*
d_rwmm
;
46
bool
d_withProof
;
47
bool
d_withAssump
;
48
unsigned
d_flag
;
// used for setting flags in Theorems
49
bool
d_active
;
//!< Whether TheoremManager is active. See also clear()
50
CommonProofRules
*
d_rules
;
51
52
std::hash_map<long, bool>
d_reflFlags
;
53
std::hash_map<long, int>
d_cachedValues
;
54
std::hash_map<long, bool>
d_expandFlags
;
55
std::hash_map<long, bool>
d_litFlags
;
56
57
CommonProofRules
*
createProofRules
();
58
59
public
:
60
//! Constructor
61
TheoremManager
(
ContextManager
* cm,
62
ExprManager
* em,
63
const
CLFlags
& flags);
64
//! Destructor
65
~TheoremManager
();
66
//! Deactivate TheoremManager
67
/*! No more Theorems can be created after this call, only deleted.
68
* The purpose of this call is to dis-entangle the mutual
69
* dependency of ExprManager and TheoremManager during destruction time.
70
*/
71
void
clear
();
72
//! Test whether the TheoremManager is still active
73
bool
isActive
() {
return
d_active
; }
74
75
ContextManager
*
getCM
()
const
{
return
d_cm
; }
76
ExprManager
*
getEM
()
const
{
return
d_em
; }
77
const
CLFlags
&
getFlags
()
const
{
return
d_flags
; }
78
MemoryManager
*
getMM
()
const
{
return
d_mm
; }
79
MemoryManager
*
getRWMM
()
const
{
return
d_rwmm
; }
80
CommonProofRules
*
getRules
()
const
{
return
d_rules
; }
81
82
unsigned
getFlag
()
const
{
83
return
d_flag
;
84
}
85
86
void
clearAllFlags
() {
87
d_reflFlags
.
clear
();
88
FatalAssert
(++
d_flag
,
"Theorem flag overflow."
);
89
}
90
91
bool
withProof
() {
92
return
d_withProof
;
93
}
94
bool
withAssumptions
() {
95
return
d_withAssump
;
96
}
97
98
// For Refl theorems
99
void
setFlag
(
long
ptr) {
d_reflFlags
[ptr] =
true
; }
100
bool
isFlagged
(
long
ptr) {
return
d_reflFlags
.
count
(ptr) > 0; }
101
void
setCachedValue
(
long
ptr,
int
value) {
d_cachedValues
[ptr] = value; }
102
int
getCachedValue
(
long
ptr) {
103
std::hash_map<long, int>::const_iterator
i =
d_cachedValues
.
find
(ptr);
104
if
(i !=
d_cachedValues
.
end
())
return
(*i).second;
105
else
return
0;
106
}
107
void
setExpandFlag
(
long
ptr,
bool
value) {
d_expandFlags
[ptr] = value; }
108
bool
getExpandFlag
(
long
ptr) {
109
std::hash_map<long, bool>::const_iterator
i =
d_expandFlags
.
find
(ptr);
110
if
(i !=
d_expandFlags
.
end
())
return
(*i).second;
111
else
return
false
;
112
}
113
void
setLitFlag
(
long
ptr,
bool
value) {
d_litFlags
[ptr] = value; }
114
bool
getLitFlag
(
long
ptr) {
115
std::hash_map<long, bool>::const_iterator
i =
d_litFlags
.
find
(ptr);
116
if
(i !=
d_litFlags
.
end
())
return
(*i).second;
117
else
return
false
;
118
}
119
120
121
};
// end of class TheoremManager
122
123
}
// end of namespace CVC3
124
125
#endif
Generated on Sat May 18 2013 12:01:26 for CVC3 by
1.8.3.1