CVC3

memory_manager.h

Go to the documentation of this file.
00001 /*****************************************************************************/
00002 /*!
00003  * \file memory_manager.h
00004  * 
00005  * Author: Sergey Berezin
00006  * 
00007  * Created: Thu Apr  3 16:47:14 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 MemoryManager: allocates/deallocates memory for objects of a
00019  * requested size.  Some instanced of this class may be specialized to
00020  * a specific object size, and the actual memory may be allocated in
00021  * big chunks, for efficiency.
00022  *
00023  * Typical use of this class is to create 
00024  * MemoryManager* mm = new MemoryManagerChunks(sizeof(YourClass)); 
00025  * where YourClass has operators new and delete redefined:
00026  * void* YourClass::operator new(size_t size, MemoryManager* mm)
00027  * { return mm->newData(size); }
00028  * void YourClass::delete(void*) { } // do not deallocate memory here
00029  * Then, create objects with obj = new(mm) YourClass(), and destroy them with
00030  * delete obj; mm->deleteData(obj);
00031  */
00032 /*****************************************************************************/
00033 
00034 #ifndef _cvc3__memory_manager_h
00035 #define _cvc3__memory_manager_h
00036 
00037 namespace CVC3 {
00038 
00039 class MemoryManager {
00040  public:
00041   // Destructor
00042   virtual ~MemoryManager() { }
00043 
00044   virtual void* newData(size_t size) = 0;
00045 
00046   virtual void deleteData(void* d) = 0;
00047 }; // end of class MemoryManager
00048 
00049 }
00050 
00051 #endif