CVC3  2.4.1
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 
40  private:
43  const CLFlags& d_flags;
48  unsigned d_flag; // used for setting flags in Theorems
49  bool d_active; //!< Whether TheoremManager is active. See also clear()
51 
56 
58 
59  public:
60  //! Constructor
62  ExprManager* em,
63  const CLFlags& flags);
64  //! Destructor
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() {
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) {
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) {
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) {
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
std::hash_map< long, int > d_cachedValues
size_type count(const _Key &key) const
Definition: hash_map.h:217
Description: Collection of debugging macros and functions.
ExprManager * getEM() const
std::hash_map< long, bool > d_reflFlags
TheoremManager(ContextManager *cm, ExprManager *em, const CLFlags &flags)
Constructor.
CommonProofRules * d_rules
MemoryManager * getMM() const
~TheoremManager()
Destructor.
iterator find(const key_type &key)
operations
Definition: hash_map.h:171
int getCachedValue(long ptr)
bool d_active
Whether TheoremManager is active. See also clear()
CommonProofRules * createProofRules()
bool isFlagged(long ptr)
ContextManager * d_cm
ContextManager * getCM() const
#define FatalAssert(cond, msg)
If something goes horribly wrong, print a message and abort immediately with exit(1).
Definition: debug.h:37
CommonProofRules * getRules() const
MemoryManager * getRWMM() const
MemoryManager * d_mm
std::hash_map< long, bool > d_expandFlags
void setExpandFlag(long ptr, bool value)
bool getLitFlag(long ptr)
void clear()
Definition: hash_map.h:161
void clear()
Deactivate TheoremManager.
MemoryManager * d_rwmm
void setCachedValue(long ptr, int value)
Expression Manager.
Definition: expr_manager.h:58
bool getExpandFlag(long ptr)
unsigned getFlag() const
const CLFlags & getFlags() const
Manager for multiple contexts. Also holds current context.
Definition: context.h:393
bool isActive()
Test whether the TheoremManager is still active.
const CLFlags & d_flags
void setFlag(long ptr)
iterator end()
Definition: hash_map.h:257
void setLitFlag(long ptr, bool value)
std::hash_map< long, bool > d_litFlags