1 /********************* */
4 ** Original author: Morgan Deters
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 project but is excluded from the
8 ** standard CVC4 licensing because it is a derivative work of
9 ** circular_buffer.hpp in the BOOST 1.46.1 distribution.
10 ** Thus this file is covered by the Boost Software License, version 1.0.
13 ** The combined work is:
14 ** Copyright (c) 2009-2014 New York University and The University of Iowa
15 ** Copyright (c) 2003-2008 Jan Gaspar
17 ** \brief [[ Add one-line brief description here ]]
19 ** [[ Add lengthier description here ]]
20 ** \todo document this file
23 #include "cvc4_public.h"
25 #ifndef __CVC4__CHANNEL_H
26 #define __CVC4__CHANNEL_H
28 #include <boost/circular_buffer.hpp>
29 #include <boost/thread/mutex.hpp>
30 #include <boost/thread/condition.hpp>
31 #include <boost/thread/thread.hpp>
32 #include <boost/call_traits.hpp>
33 #include <boost/progress.hpp>
34 #include <boost/bind.hpp>
39 class CVC4_PUBLIC SharedChannel
{
41 int d_maxsize
; // just call it size?
44 SharedChannel(int maxsize
) : d_maxsize(maxsize
) {}
45 virtual ~SharedChannel() {}
47 /* Tries to add element and returns true if successful */
48 virtual bool push(const T
&) = 0;
50 /* Removes an element from the channel */
54 virtual bool empty() = 0;
57 virtual bool full() = 0;
58 };/* class SharedChannel<T> */
63 http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.html#boundedbuffer
65 and is covered by the Boost Software License, version 1.0.
68 class CVC4_PUBLIC SynchronizedSharedChannel
: public SharedChannel
<T
> {
70 typedef boost::circular_buffer
<T
> container_type
;
71 typedef typename
container_type::size_type size_type
;
72 typedef typename
container_type::value_type value_type
;
73 typedef typename
boost::call_traits
<value_type
>::param_type param_type
;
75 explicit SynchronizedSharedChannel(size_type capacity
) : m_unread(0), m_container(capacity
) {}
77 bool push(param_type item
){
78 // param_type represents the "best" way to pass a parameter of type value_type to a method
80 boost::mutex::scoped_lock
lock(m_mutex
);
81 m_not_full
.wait(lock
, boost::bind(&SynchronizedSharedChannel
<value_type
>::is_not_full
, this));
82 m_container
.push_front(item
);
85 m_not_empty
.notify_one();
87 }//function definitions need to be moved to cpp
91 boost::mutex::scoped_lock
lock(m_mutex
);
92 m_not_empty
.wait(lock
, boost::bind(&SynchronizedSharedChannel
<value_type
>::is_not_empty
, this));
93 ret
= m_container
[--m_unread
];
95 m_not_full
.notify_one();
100 bool empty() { return not is_not_empty(); }
101 bool full() { return not is_not_full(); }
104 SynchronizedSharedChannel(const SynchronizedSharedChannel
&); // Disabled copy constructor
105 SynchronizedSharedChannel
& operator = (const SynchronizedSharedChannel
&); // Disabled assign operator
107 bool is_not_empty() const { return m_unread
> 0; }
108 bool is_not_full() const { return m_unread
< m_container
.capacity(); }
111 container_type m_container
;
112 boost::mutex m_mutex
;
113 boost::condition m_not_empty
;
114 boost::condition m_not_full
;
115 };/* class SynchronizedSharedChannel<T> */
117 }/* CVC4 namespace */
119 #endif /* __CVC4__CHANNEL_H */