CVC3  2.4.1
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, "**");
57  "TheoremManager(): proofs without assumptions are not allowed");
58  if (flags["mm"].getString() == "chunks") {
61  } else {
62  d_mm = new MemoryManagerMalloc();
64  }
66 }
67 
68 
70 {
71  delete d_mm;
72  delete d_rwmm;
73 }
74 
75 
77  delete d_rules;
78  d_active=false;
79 }
CommonProofRules * d_rules
~TheoremManager()
Destructor.
#define DebugAssert(cond, str)
Definition: debug.h:408
bool d_active
Whether TheoremManager is active. See also clear()
CommonProofRules * createProofRules()
MemoryManager * d_mm
void newKind(int kind, const std::string &name, bool isType=false)
Register a new kind.
void clear()
Deactivate TheoremManager.
MemoryManager * d_rwmm
Expression Manager.
Definition: expr_manager.h:58
Definition: kinds.h:276
Manager for multiple contexts. Also holds current context.
Definition: context.h:393