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
}
Generated on Tue May 14 2013 09:02:08 for CVC3 by
1.8.3.1