CVC3

theorem_manager.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file theorem_manager.h
00004  * 
00005  * Author: Sergey Berezin, Tue Feb  4 14:29:25 2003
00006  * 
00007  * Created: Feb 05 18:29:37 GMT 2003
00008  *
00009  * <hr>
00010  *
00011  * License to use, copy, modify, sell and/or distribute this software
00012  * and its documentation for any purpose is hereby granted without
00013  * royalty, subject to the terms and conditions defined in the \ref
00014  * LICENSE file provided with this distribution.
00015  * 
00016  * <hr>
00017  * 
00018  * CLASS: TheoremManager
00019  * 
00020  * 
00021  * Holds the shared data for the class Theorem
00022  */
00023 /*****************************************************************************/
00024 
00025 #ifndef _cvc3__theorem_manager_h_
00026 #define _cvc3__theorem_manager_h_
00027 
00028 #include "debug.h"
00029 #include "compat_hash_map.h"
00030 
00031 namespace CVC3 {
00032 
00033   class ContextManager;
00034   class ExprManager;
00035   class CLFlags;
00036   class MemoryManager;
00037   class CommonProofRules;
00038   
00039   class TheoremManager {
00040   private:
00041     ContextManager* d_cm;
00042     ExprManager* d_em;
00043     const CLFlags& d_flags;
00044     MemoryManager* d_mm;
00045     MemoryManager* d_rwmm;
00046     bool d_withProof;
00047     bool d_withAssump;
00048     unsigned d_flag; // used for setting flags in Theorems
00049     bool d_active; //!< Whether TheoremManager is active.  See also clear()
00050     CommonProofRules* d_rules;
00051 
00052     std::hash_map<long, bool> d_reflFlags;
00053     std::hash_map<long, int> d_cachedValues;
00054     std::hash_map<long, bool> d_expandFlags;
00055     std::hash_map<long, bool> d_litFlags;
00056 
00057     CommonProofRules* createProofRules();
00058 
00059   public:
00060     //! Constructor
00061     TheoremManager(ContextManager* cm,
00062                    ExprManager* em,
00063                    const CLFlags& flags);
00064     //! Destructor
00065     ~TheoremManager();
00066     //! Deactivate TheoremManager
00067     /*! No more Theorems can be created after this call, only deleted.
00068      * The purpose of this call is to dis-entangle the mutual
00069      * dependency of ExprManager and TheoremManager during destruction time.
00070      */
00071     void clear();
00072     //! Test whether the TheoremManager is still active
00073     bool isActive() { return d_active; }
00074 
00075     ContextManager* getCM() const { return d_cm; }
00076     ExprManager* getEM() const { return d_em; }
00077     const CLFlags& getFlags() const { return d_flags; }
00078     MemoryManager* getMM() const { return d_mm; }
00079     MemoryManager* getRWMM() const { return d_rwmm; }
00080     CommonProofRules* getRules() const { return d_rules; }
00081 
00082     unsigned getFlag() const {
00083       return d_flag;
00084     }
00085     
00086     void clearAllFlags() {
00087       d_reflFlags.clear();
00088       FatalAssert(++d_flag, "Theorem flag overflow.");
00089     }
00090 
00091     bool withProof() {
00092       return d_withProof;
00093     }
00094     bool withAssumptions() {
00095       return d_withAssump;
00096     }
00097 
00098     // For Refl theorems
00099     void setFlag(long ptr) { d_reflFlags[ptr] = true; }
00100     bool isFlagged(long ptr) { return d_reflFlags.count(ptr) > 0; }
00101     void setCachedValue(long ptr, int value) { d_cachedValues[ptr] = value; }
00102     int getCachedValue(long ptr) {
00103       std::hash_map<long, int>::const_iterator i = d_cachedValues.find(ptr);
00104       if (i != d_cachedValues.end()) return (*i).second;
00105       else return 0;
00106     }
00107     void setExpandFlag(long ptr, bool value) { d_expandFlags[ptr] = value; }
00108     bool getExpandFlag(long ptr) {
00109       std::hash_map<long, bool>::const_iterator i = d_expandFlags.find(ptr);
00110       if (i != d_expandFlags.end()) return (*i).second;
00111       else return false;
00112     }
00113     void setLitFlag(long ptr, bool value) { d_litFlags[ptr] = value; }
00114     bool getLitFlag(long ptr) {
00115       std::hash_map<long, bool>::const_iterator i = d_litFlags.find(ptr);
00116       if (i != d_litFlags.end()) return (*i).second;
00117       else return false;
00118     }
00119     
00120 
00121   }; // end of class TheoremManager
00122 
00123 } // end of namespace CVC3
00124 
00125 #endif