/*****************************************************************************/
/*!
 * \file context.h
 * 
 * Author: Clark Barrett
 * 
 * Created: Tue Dec 31 19:07:38 2002
 *
 * <hr>
 *
 * 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.
 * 
 * <hr>
 * 
 */
/*****************************************************************************/


#ifndef _cvc3__include__context_h_
#define _cvc3__include__context_h_

#include <string>
#include <vector>
#include "debug.h"
#include "memory_manager_context.h"

namespace CVC3 {

/****************************************************************************/
/*! \defgroup Context Context Management
 *  \ingroup BuildingBlocks
 * Infrastructure for backtrackable data structures.
 * @{
 */
/****************************************************************************/

class Context;
class ContextManager;
class ContextNotifyObj;
class ContextObj;
class ContextObjChain;

/****************************************************************************/
/*! 
 * Author: Clark Barrett
 *
 * Created: Thu Feb 13 00:19:15 2003
 *
 * A scope encapsulates the portion of a context which has changed
 * since the last call to push().  Thus, when pop() is called,
 * everything in this scope is restored to its previous state.
 */
 /****************************************************************************/

class Scope {
  friend class ContextObj;
  friend class ContextObjChain;
  friend class CDFlags;
  //! Context that created this scope
  Context* d_context;

  //! Memory manager for this scope
  ContextMemoryManager* d_cmm;

  //! Previous scope in this context
  Scope* d_prevScope;

  //! Scope level
  int d_level;

  /*! @brief Linked list of objects which are "current" in this scope,
    and thus need to be restored when the scope is deleted */
  ContextObjChain* d_restoreChain;

  //! Called by ContextObj when created
  void addToChain(ContextObjChain* obj);

public:
  //! Constructor
  Scope(Context* context, ContextMemoryManager* cmm,
        Scope* prevScope = NULL)
    : d_context(context), d_cmm(cmm), d_prevScope(prevScope),
      d_restoreChain(NULL)
    { if (prevScope) d_level = prevScope->level() + 1; else d_level = 0; }
  //! Destructor
  ~Scope() {}

  //! Access functions
  Scope* prevScope() const { return d_prevScope; }
  int level(void) const { return d_level; }
  bool isCurrent(void) const;
  Scope* topScope() const;
  Context* getContext() const { return d_context; }
  ContextMemoryManager* getCMM() const { return d_cmm; }

  void* operator new(size_t size, MemoryManager* mm)
    { return mm->newData(size); }
  void operator delete(void* pMem, MemoryManager* mm) {
    mm->deleteData(pMem);
  }
  void operator delete(void*) { }

  //! Restore all the values
  void restore(void);

  //! Called by ~ContextManager
  void finalize(void);

  //! Check for memory leaks
  void check(void);
};

///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Class: ContextObjChain						     //
// Author: Sergey Berezin                                                    //
// Created: Wed Mar 12 11:25:22 2003					     //

/*! Description: An element of a doubly linked list holding a copy of
 * ContextObj in a scope.  It is made separate from ContextObj to keep
 * the list pointers valid in all scopes at all times, so that the
 * object can be easily removed from the list when the master
 * ContextObj is destroyed. */
///////////////////////////////////////////////////////////////////////////////
class ContextObjChain {
friend class Scope;
friend class ContextObj;
friend class CDFlags;
private:
  //! Next link in chain
  ContextObjChain* d_restoreChainNext;

  /*! @brief Pointer to the pointer of the previous object which
  points to us.  This makes a doubly-linked list for easy element
  deletion */
  ContextObjChain** d_restoreChainPrev;

  //! Pointer to the previous copy which belongs to the same master
  ContextObjChain* d_restore;

  //! Pointer to copy of master to be restored when restore() is called
  ContextObj* d_data;

  //! Pointer to the master object
  ContextObj* d_master;

  //! Private constructor (only friends can use it)
  ContextObjChain(ContextObj* data, ContextObj* master, 
		  ContextObjChain* restore)
    : d_restoreChainNext(NULL), d_restoreChainPrev(NULL),
      d_restore(restore), d_data(data), d_master(master)
  { }

  //! Restore from d_data to d_master
  ContextObjChain* restore(void);
public:
  //! Destructor
  ~ContextObjChain() {}

  void* operator new(size_t size, MemoryManager* mm) {
    return mm->newData(size);
  }
  void operator delete(void* pMem, MemoryManager* mm) {
    mm->deleteData(pMem);
  }

  void operator delete(void*) { }

  // If you use this operator, you have to call free yourself when the memory
  // is freed.
  void* operator new(size_t size, bool b) {
    return malloc(size);
  }
  void operator delete(void* pMem, bool b) {
    free(pMem);
  }

  IF_DEBUG(std::string name() const;)
};

///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Class: ContextObj							     //
// Author: Clark Barrett                                                     //
// Created: Thu Feb 13 00:21:13 2003					     //

/*!  Description: This is a generic class from which all objects that
 * are context-dependent should inherit.  Subclasses need to implement
 * makeCopy, restoreData, and setNull.
 */
///////////////////////////////////////////////////////////////////////////////
class CVC_DLL ContextObj {
friend class Scope;
friend class ContextObjChain;
friend class CDFlags;
private:
  //! Last scope in which this object was modified.
  Scope* d_scope;

  /*! @brief The list of values on previous scopes; our destructor
   *  should clean up those. */
  ContextObjChain* d_restore;

  IF_DEBUG(std::string d_name);
  IF_DEBUG(bool d_active);

  //! Update on the given scope, on the current scope if 'scope' == -1
  void update(int scope = -1);

protected:
  //! Copy constructor (defined mainly for debugging purposes)
  ContextObj(const ContextObj& co)
    : d_scope(co.d_scope), d_restore(co.d_restore) {
    IF_DEBUG(d_name=co.d_name);
    DebugAssert(co.d_active, "ContextObj["+co.name()+"] copy constructor");
    IF_DEBUG(d_active = co.d_active);
    //    TRACE("context verbose", "ContextObj()[", this, "]: copy constructor");
  }

  //! Assignment operator (defined mainly for debugging purposes)
  ContextObj& operator=(const ContextObj& co) {
    DebugAssert(false, "ContextObj::operator=(): shouldn't be called");
    return *this;
  }

  /*! @brief Make a copy of the current object so it can be restored
   * to its current state */
  virtual ContextObj* makeCopy(ContextMemoryManager* cmm) = 0;

  //! Restore the current object from the given data
  virtual void restoreData(ContextObj* data) {
    FatalAssert(false, 
                "ContextObj::restoreData(): call in the base abstract class");
  }

  const ContextObj* getRestore() {
    return d_restore ? d_restore->d_data : NULL;
  }

  //! Set the current object to be invalid
  virtual void setNull(void) = 0;

  //! Return our name (for debugging)
  IF_DEBUG(virtual std::string name() const { return d_name; });

  //! Get context memory manager
  ContextMemoryManager* getCMM() { return d_scope->getCMM(); }

public:
  //! Create a new ContextObj.
  /*!
   * The initial scope is set to the bottom scope by default, to
   * reduce the work of pop() (otherwise, if the object is defined
   * only on a very high scope, its scope will be moved down with each
   * pop).  If 'atBottomScope' == false, the scope is set to the
   * current scope. 
   */
  ContextObj(Context* context, bool atBottomScope = true);
  virtual ~ContextObj();

  int level() const { return (d_scope==NULL)? 0 : d_scope->level(); }
  bool isCurrent(int scope = -1) const {
    if(scope >= 0) return d_scope->level() == scope;
    else return d_scope->isCurrent();
  }
  void makeCurrent(int scope = -1) { if (!isCurrent(scope)) update(scope); }
  IF_DEBUG(void setName(const std::string& name) { d_name=name; });

  void* operator new(size_t size, MemoryManager* mm) {
    return mm->newData(size);
  }
  void operator delete(void* pMem, MemoryManager* mm) {
    mm->deleteData(pMem);
  }

  // If you use this operator, you have to call free yourself when the memory
  // is freed.
  void* operator new(size_t size, bool b) {
    return malloc(size);
  }
  void operator delete(void* pMem, bool b) {
    free(pMem);
  }

  void operator delete(void*) { }
};

///////////////////////////////////////////////////////////////////////////////
//                                                                           //
// Class: Context							     //
// Author: Clark Barrett                                                     //
// Created: Thu Feb 13 00:24:59 2003					     //
/*!
 * Encapsulates the general notion of stack-based saving and restoring
 * of a database.
 */
///////////////////////////////////////////////////////////////////////////////
class Context {
  //! Context Manager
  ContextManager* d_cm;

  //! Name of context
  std::string d_name;

  //! Context ID
  int d_id;

  //! Pointer to top and bottom scopes of context
  Scope* d_topScope;
  Scope* d_bottomScope;

  //! List of objects to notify with every pop
  std::vector<ContextNotifyObj*> d_notifyObjList;

  //! Stack of free ContextMemoryManager's
  std::vector<ContextMemoryManager*> d_cmmStack;

public:
  Context(ContextManager* cm, const std::string& name, int id);
  ~Context();

  //! Access methods
  ContextManager* getCM() const { return d_cm; }
  const std::string& name() const { return d_name; }
  int id() const { return d_id; }
  Scope* topScope() const { return d_topScope; }
  Scope* bottomScope() const { return d_bottomScope; }
  int level() const { return d_topScope->level(); }

  void push();
  void pop();
  void popto(int toLevel);
  void addNotifyObj(ContextNotifyObj* obj) { d_notifyObjList.push_back(obj); }
  void deleteNotifyObj(ContextNotifyObj* obj);
  unsigned long getMemory();
};

// Have to define after Context class
inline bool Scope::isCurrent(void) const
  { return this == d_context->topScope(); }

inline void Scope::addToChain(ContextObjChain* obj) {
  if(d_restoreChain != NULL)
    d_restoreChain->d_restoreChainPrev = &(obj->d_restoreChainNext);
  obj->d_restoreChainNext = d_restoreChain;
  obj->d_restoreChainPrev = &d_restoreChain;
  d_restoreChain = obj;
}

inline Scope* Scope::topScope() const { return d_context->topScope(); }

inline void Scope::restore(void) {
  //  TRACE_MSG("context verbose", "Scope::restore() {");
  while (d_restoreChain != NULL) d_restoreChain = d_restoreChain->restore();
  //  TRACE_MSG("context verbose", "Scope::restore() }");
}

// Create a new ContextObj.  The initial scope is set to the bottom
// scope by default, to reduce the work of pop() (otherwise, if the
// object is defined only on a very high scope, its scope will be
// moved down with each pop).  If 'atBottomScope' == false, the
// scope is set to the current scope.
inline ContextObj::ContextObj(Context* context, bool atBottomScope)
  IF_DEBUG(: d_name("ContextObj"))
{
  IF_DEBUG(d_active=true);
  DebugAssert(context != NULL, "NULL context pointer");
  if (atBottomScope) d_scope = context->bottomScope();
  else d_scope = context->topScope();
  d_restore = new(true) ContextObjChain(NULL, this, NULL);
  d_scope->addToChain(d_restore);
  //  if (atBottomScope) d_scope->addSpecialObject(d_restore);
  //  TRACE("context verbose", "ContextObj()[", this, "]");
}


/****************************************************************************/
//! Manager for multiple contexts.  Also holds current context.
/*!
 * Author: Clark Barrett
 *
 * Created: Thu Feb 13 00:26:29 2003
 */
/****************************************************************************/

class ContextManager {
  Context* d_curContext;
  std::vector<Context*> d_contexts;

public:
  ContextManager();
  ~ContextManager();

  void push() { d_curContext->push(); }
  void pop() { d_curContext->pop(); }
  void popto(int toLevel) { d_curContext->popto(toLevel); }
  int scopeLevel() { return d_curContext->level(); }
  Context* createContext(const std::string& name="");
  Context* getCurrentContext() { return d_curContext; }
  Context* switchContext(Context* context);
  unsigned long getMemory();
};

/****************************************************************************/
/*! Author: Clark Barrett                                                     
 *
 * Created: Sat Feb 22 16:21:47 2003					     
 *
 * Lightweight version of ContextObj: objects are simply notified
 * every time there's a pop. notifyPre() is called right before the
 * context is restored, and notify() is called after the context is
 * restored.
 */
/****************************************************************************/
 
class ContextNotifyObj {
  friend class Context;
protected:
  Context* d_context;
public:
  ContextNotifyObj(Context* context): d_context(context)
    { context->addNotifyObj(this); }
  virtual ~ContextNotifyObj() {
    // If we are being deleted before the context, remove ourselves
    // from the notify list.  However, if the context is deleted
    // before we are, then our d_context will be cleared from ~Context()
    if(d_context!=NULL) d_context->deleteNotifyObj(this);
  }
  virtual void notifyPre(void) {}
  virtual void notify(void) {}
};

/*@}*/  // end of group Context

}

#endif