/usr/include/cvc3/smartcdo.h is in libcvc3-dev 2.4.1-4ubuntu1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 | /*****************************************************************************/
/*!
*\file smartcdo.h
*\brief Smart context-dependent object wrapper
*
* Author: Clark Barrett
*
* Created: Fri Nov 12 17:28:58 2004
*
* <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__smartcdo_h_
#define _cvc3__include__smartcdo_h_
#include "cdo.h"
namespace CVC3 {
/*****************************************************************************/
/*!
*\class SmartCDO
*\brief SmartCDO
*
* Author: Clark Barrett
*
* Created: Fri Nov 12 17:33:31 2004
*
* Wrapper for CDO which automatically allocates and deletes a pointer to a
* CDO. This allows the copy constructor and operator= to be defined which are
* especially useful for storing CDO's in vectors. All operations are const to
* enable use as a member of CDLists.
*
* Be careful not to delete RefCDO during pop(), since this messes up
* the backtracking data structures. We delay the deletion by
* registering each RefCDO to be notified before and after each pop().
* This makes the use of SmartCDO somewhat more expensive, so use it
* with care.
*
*/
/*****************************************************************************/
template <class T>
class SmartCDO {
template <class U>
class RefCDO {
friend class SmartCDO;
unsigned d_refCount;
CDO<U> d_cdo;
bool d_delay; //!< Whether to delay our own deletion
class RefNotifyObj : public ContextNotifyObj {
friend class RefCDO;
RefCDO<U>* d_ref;
//! Constructor
RefNotifyObj(RefCDO<U>* ref, Context* context)
: ContextNotifyObj(context), d_ref(ref) { }
void notifyPre() { d_ref->d_delay = true; }
void notify() {
d_ref->d_delay = false;
d_ref->kill();
}
};
RefNotifyObj* d_notifyObj;
friend class RefNotifyObj;
RefCDO(Context* context): d_refCount(0), d_cdo(context), d_delay(false),
d_notifyObj(new RefNotifyObj(this, context)) {}
RefCDO(Context* context, const U& cdo, int scope = -1)
: d_refCount(0), d_cdo(context, cdo, scope), d_delay(false),
d_notifyObj(new RefNotifyObj(this, context)) {}
~RefCDO() { delete d_notifyObj; }
//! Delete itself, unless delayed (then we'll be called again later)
void kill() { if(d_refCount==0 && !d_delay) delete this; }
};
RefCDO<T>* d_data;
public:
//! Check if the SmartCDO object is Null
bool isNull() const { return (d_data==NULL); }
//! Default constructor: create a Null SmartCDO object
SmartCDO(): d_data(NULL) { }
//! Create and initialize SmartCDO object at the current scope
SmartCDO(Context* context)
{ d_data = new RefCDO<T>(context); d_data->d_refCount++; }
//! Create and initialize SmartCDO object at the given scope
SmartCDO(Context* context, const T& data, int scope = -1)
{ d_data = new RefCDO<T>(context, data, scope); d_data->d_refCount++; }
//! Delete
~SmartCDO()
{ if (isNull()) return;
if (--d_data->d_refCount == 0) d_data->kill(); }
SmartCDO(const SmartCDO<T>& cdo) : d_data(cdo.d_data)
{ if (!isNull()) d_data->d_refCount++; }
SmartCDO<T>& operator=(const SmartCDO<T>& cdo)
{
if (this == &cdo) return *this;
if (!isNull() && --(d_data->d_refCount)) d_data->kill();
d_data = cdo.d_data;
if (!isNull()) ++(d_data->d_refCount);
return *this;
}
void set(const T& data, int scope=-1) const {
DebugAssert(!isNull(), "SmartCDO::set: we are Null");
d_data->d_cdo.set(data, scope);
}
const T& get() const {
DebugAssert(!isNull(), "SmartCDO::get: we are Null");
return d_data->d_cdo.get();
}
operator T() const { return get(); }
const SmartCDO<T>& operator=(const T& data) const {set(data); return *this;}
};
}
#endif
|