mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Add support for ref_buffers with different initial sizes. Add shrink and operator= methods.

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-01-03 17:45:28 -08:00
parent f324724abc
commit ed5b106574
1 changed files with 19 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/util/ref_buffer.h
View file

@ -30,10 +30,10 @@ Revision History:
- void dec_ref(T * obj) - void dec_ref(T * obj)
- void inc_ref(T * obj) - void inc_ref(T * obj)
*/ */
template<typename T, typename Ref> template<typename T, typename Ref, unsigned INITIAL_SIZE=16>
class ref_buffer_core : public Ref { class ref_buffer_core : public Ref {
protected: protected:
ptr_buffer<T> m_buffer; ptr_buffer<T, INITIAL_SIZE> m_buffer;
void inc_ref(T * o) { Ref::inc_ref(o); } void inc_ref(T * o) { Ref::inc_ref(o); }
void dec_ref(T * o) { Ref::dec_ref(o); } void dec_ref(T * o) { Ref::dec_ref(o); }
@ -126,6 +126,11 @@ public:
m_buffer.resize(sz, 0); m_buffer.resize(sz, 0);
} }
void shrink(unsigned sz) {
SASSERT(sz <= m_buffer.size());
resize(sz);
}
// set pos idx with elem. If idx >= size, then expand. // set pos idx with elem. If idx >= size, then expand.
void setx(unsigned idx, T * elem) { void setx(unsigned idx, T * elem) {
if (idx >= size()) { if (idx >= size()) {
@ -133,19 +138,22 @@ public:
} }
set(idx, elem); set(idx, elem);
} }
private: ref_buffer_core & operator=(ref_buffer_core const & other) {
// prevent abuse: if (this == &other)
ref_buffer_core& operator=(ref_buffer_core const & other); return *this;
reset();
append(other);
}
}; };
/** /**
\brief Buffer of managed references \brief Buffer of managed references
*/ */
template<typename T, typename TManager> template<typename T, typename TManager, unsigned INITIAL_SIZE=16>
class ref_buffer : public ref_buffer_core<T, ref_manager_wrapper<T, TManager> > { class ref_buffer : public ref_buffer_core<T, ref_manager_wrapper<T, TManager>, INITIAL_SIZE> {
typedef ref_buffer_core<T, ref_manager_wrapper<T, TManager> > super; typedef ref_buffer_core<T, ref_manager_wrapper<T, TManager>, INITIAL_SIZE> super;
public: public:
ref_buffer(TManager & m): ref_buffer(TManager & m):
super(ref_manager_wrapper<T, TManager>(m)) { super(ref_manager_wrapper<T, TManager>(m)) {
@ -161,8 +169,8 @@ public:
/** /**
\brief Buffer of unmanaged references \brief Buffer of unmanaged references
*/ */
template<typename T> template<typename T, unsigned INITIAL_SIZE=16>
class sref_buffer : public ref_buffer_core<T, ref_unmanaged_wrapper<T> > { class sref_buffer : public ref_buffer_core<T, ref_unmanaged_wrapper<T>, INITIAL_SIZE> {
public: public:
}; };