theorem_manager.h

Go to the documentation of this file.

/*****************************************************************************/
/*!
 * \file theorem_manager.h
 * 
 * Author: Sergey Berezin, Tue Feb  4 14:29:25 2003
 * 
 * Created: Feb 05 18:29:37 GMT 2003
 *
 * <hr>
 * Copyright (C) 2003 by the Board of Trustees of Leland Stanford
 * Junior University and by New York University. 
 *
 * License to use, copy, modify, sell and/or distribute this software
 * and its documentation for any purpose is hereby granted without
 * royalty, subject to the terms and conditions defined in the \ref
 * LICENSE file provided with this distribution.  In particular:
 *
 * - The above copyright notice and this permission notice must appear
 * in all copies of the software and related documentation.
 *
 * - THE SOFTWARE IS PROVIDED "AS-IS", WITHOUT ANY WARRANTIES,
 * EXPRESSED OR IMPLIED.  USE IT AT YOUR OWN RISK.
 * 
 * <hr>
 * 
 * CLASS: TheoremManager
 * 
 * 
 * Holds the shared data for the class Theorem
 */
/*****************************************************************************/

#ifndef _CVC_lite__theorem_manager_h_
#define _CVC_lite__theorem_manager_h_

#include "debug.h"

namespace CVCL {

  class ContextManager;
  class ExprManager;
  class CLFlags;
  class MemoryManager;
  class CommonProofRules;
  
  class TheoremManager {
  private:
    ContextManager* d_cm;
    ExprManager* d_em;
    const CLFlags& d_flags;
    MemoryManager* d_mm;
    MemoryManager* d_rwmm;
    MemoryManager* d_reflmm;
    bool d_withProof;
    bool d_withAssump;
    unsigned d_flag; // used for setting flags in Theorems
    bool d_active; //!< Whether TheoremManager is active.  See also clear()
    CommonProofRules* d_rules;

    CommonProofRules* createProofRules();

  public:
    //! Constructor
    TheoremManager(ContextManager* cm,
                   ExprManager* em,
                   const CLFlags& flags);
    //! Destructor
    ~TheoremManager();
    //! Deactivate TheoremManager
    /*! No more Theorems can be created after this call, only deleted.
     * The purpose of this call is to dis-entangle the mutual
     * dependency of ExprManager and TheoremManager during destruction time.
     */
    void clear();
    //! Test whether the TheoremManager is still active
    bool isActive() { return d_active; }

    ContextManager* getCM() const { return d_cm; }
    ExprManager* getEM() const { return d_em; }
    const CLFlags& getFlags() const { return d_flags; }
    MemoryManager* getMM() const { return d_mm; }
    MemoryManager* getRWMM() const { return d_rwmm; }
    MemoryManager* getReflMM() const { return d_reflmm; }
    CommonProofRules* getRules() const { return d_rules; }

    unsigned getFlag() const {
      return d_flag;
    }
    
    void clearAllFlags() {
      FatalAssert(++d_flag, "Theorem flag overflow.");
    }

    bool withProof() {
      return d_withProof;
    }
    bool withAssumptions() {
      return d_withAssump;
    }

  }; // end of class TheoremManager

} // end of namespace CVCL

#endif

---