CVC3
2.4.1
Main Page
Related Pages
Modules
Namespaces
Classes
Files
File List
File Members
src
theorem
theorem_manager.cpp
Go to the documentation of this file.
1
/*****************************************************************************/
2
/*!
3
* \file theorem_manager.cpp
4
*
5
* Author: Sergey Berezin
6
*
7
* Created: Feb 11 02:39:35 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
*/
19
/*****************************************************************************/
20
// File: theorem_manager.cpp
21
//
22
// AUTHOR: Sergey Berezin, 07/05/02
23
//
24
// Defines some functions for class TheoremManager. They are not
25
// inlined becaule they use ExprManager (expr_manager.h), which
26
// includes theorem_manager.h.
27
//
28
///////////////////////////////////////////////////////////////////////////////
29
30
31
#include "
theorem_value.h
"
32
#include "
memory_manager_chunks.h
"
33
#include "
memory_manager_malloc.h
"
34
#include "
command_line_flags.h
"
35
#include "
common_proof_rules.h
"
36
37
38
using namespace
std
;
39
using namespace
CVC3
;
40
41
42
// ExprManager is not initialized in vcl yet when we are created; we
43
// use d_em as our local cache to fetch the EM when our getEM() is
44
// first called.
45
46
TheoremManager::TheoremManager(
ContextManager
* cm,
47
ExprManager
* em,
48
const
CLFlags
& flags)
49
: d_cm(cm), d_em(em), d_flags(flags),
50
d_withProof(flags[
"proofs"
].getBool()),
51
d_withAssump(true), d_flag(1),
52
d_active(true)
53
{
54
d_em
->
newKind
(
PF_APPLY
,
"|-"
);
55
d_em
->
newKind
(
PF_HOLE
,
"**"
);
56
DebugAssert
(!
d_withProof
||
d_withAssump
,
57
"TheoremManager(): proofs without assumptions are not allowed"
);
58
if
(flags[
"mm"
].getString() ==
"chunks"
) {
59
d_mm
=
new
MemoryManagerChunks
(
sizeof
(
RegTheoremValue
));
60
d_rwmm
=
new
MemoryManagerChunks
(
sizeof
(
RWTheoremValue
));
61
}
else
{
62
d_mm
=
new
MemoryManagerMalloc
();
63
d_rwmm
=
new
MemoryManagerMalloc
();
64
}
65
d_rules
=
createProofRules
();
66
}
67
68
69
TheoremManager::~TheoremManager
()
70
{
71
delete
d_mm
;
72
delete
d_rwmm
;
73
}
74
75
76
void
TheoremManager::clear
() {
77
delete
d_rules
;
78
d_active
=
false
;
79
}
CVC3::MemoryManagerMalloc
Definition:
memory_manager_malloc.h:39
PF_APPLY
Definition:
kinds.h:275
CVC3::TheoremManager::d_withAssump
bool d_withAssump
Definition:
theorem_manager.h:47
std
STL namespace.
CVC3::TheoremManager::d_rules
CommonProofRules * d_rules
Definition:
theorem_manager.h:50
CVC3::TheoremManager::~TheoremManager
~TheoremManager()
Destructor.
Definition:
theorem_manager.cpp:69
memory_manager_malloc.h
DebugAssert
#define DebugAssert(cond, str)
Definition:
debug.h:408
theorem_value.h
memory_manager_chunks.h
CVC3::TheoremManager::d_active
bool d_active
Whether TheoremManager is active. See also clear()
Definition:
theorem_manager.h:49
CVC3::TheoremManager::createProofRules
CommonProofRules * createProofRules()
Definition:
common_theorem_producer.cpp:35
command_line_flags.h
CVC3::TheoremManager::d_mm
MemoryManager * d_mm
Definition:
theorem_manager.h:44
CVC3::ExprManager::newKind
void newKind(int kind, const std::string &name, bool isType=false)
Register a new kind.
Definition:
expr_manager.cpp:367
CVC3::TheoremManager::clear
void clear()
Deactivate TheoremManager.
Definition:
theorem_manager.cpp:76
CVC3::TheoremManager::d_rwmm
MemoryManager * d_rwmm
Definition:
theorem_manager.h:45
CVC3::ExprManager
Expression Manager.
Definition:
expr_manager.h:58
CVC3::TheoremManager::d_withProof
bool d_withProof
Definition:
theorem_manager.h:46
CVC3::MemoryManagerChunks
Definition:
memory_manager_chunks.h:42
CVC3::RegTheoremValue
Definition:
theorem_value.h:343
CVC3::RWTheoremValue
Definition:
theorem_value.h:432
PF_HOLE
Definition:
kinds.h:276
common_proof_rules.h
CVC3::CLFlags
Definition:
command_line_flags.h:246
CVC3::ContextManager
Manager for multiple contexts. Also holds current context.
Definition:
context.h:393
CVC3
Definition:
expr.cpp:35
CVC3::TheoremManager::d_em
ExprManager * d_em
Definition:
theorem_manager.h:42
Generated on Thu Feb 19 2015 14:51:09 for CVC3 by
1.8.9.1