CVC3
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