cvc4-1.4
channel.h
Go to the documentation of this file.
1 /********************* */
18 #include "cvc4_public.h"
19 
20 #ifndef __CVC4__CHANNEL_H
21 #define __CVC4__CHANNEL_H
22 
23 #include <boost/circular_buffer.hpp>
24 #include <boost/thread/mutex.hpp>
25 #include <boost/thread/condition.hpp>
26 #include <boost/thread/thread.hpp>
27 #include <boost/call_traits.hpp>
28 #include <boost/progress.hpp>
29 #include <boost/bind.hpp>
30 
31 namespace CVC4 {
32 
33 template <typename T>
35 private:
36  int d_maxsize; // just call it size?
37 public:
39  SharedChannel(int maxsize) : d_maxsize(maxsize) {}
40  virtual ~SharedChannel() {}
41 
42  /* Tries to add element and returns true if successful */
43  virtual bool push(const T&) = 0;
44 
45  /* Removes an element from the channel */
46  virtual T pop() = 0;
47 
48  /* */
49  virtual bool empty() = 0;
50 
51  /* */
52  virtual bool full() = 0;
53 };/* class SharedChannel<T> */
54 
55 /*
56 This code is from
57 
58 http://live.boost.org/doc/libs/1_46_1/libs/circular_buffer/doc/circular_buffer.html#boundedbuffer
59 
60 and is covered by the Boost Software License, version 1.0.
61 */
62 template <typename T>
64 public:
65  typedef boost::circular_buffer<T> container_type;
66  typedef typename container_type::size_type size_type;
67  typedef typename container_type::value_type value_type;
68  typedef typename boost::call_traits<value_type>::param_type param_type;
69 
70  explicit SynchronizedSharedChannel(size_type capacity) : m_unread(0), m_container(capacity) {}
71 
72  bool push(param_type item){
73  // param_type represents the "best" way to pass a parameter of type value_type to a method
74 
75  boost::mutex::scoped_lock lock(m_mutex);
76  m_not_full.wait(lock, boost::bind(&SynchronizedSharedChannel<value_type>::is_not_full, this));
77  m_container.push_front(item);
78  ++m_unread;
79  lock.unlock();
80  m_not_empty.notify_one();
81  return true;
82  }//function definitions need to be moved to cpp
83 
84  value_type pop(){
85  value_type ret;
86  boost::mutex::scoped_lock lock(m_mutex);
87  m_not_empty.wait(lock, boost::bind(&SynchronizedSharedChannel<value_type>::is_not_empty, this));
88  ret = m_container[--m_unread];
89  lock.unlock();
90  m_not_full.notify_one();
91  return ret;
92  }
93 
94 
95  bool empty() { return not is_not_empty(); }
96  bool full() { return not is_not_full(); }
97 
98 private:
99  SynchronizedSharedChannel(const SynchronizedSharedChannel&); // Disabled copy constructor
100  SynchronizedSharedChannel& operator = (const SynchronizedSharedChannel&); // Disabled assign operator
101 
102  bool is_not_empty() const { return m_unread > 0; }
103  bool is_not_full() const { return m_unread < m_container.capacity(); }
104 
105  size_type m_unread;
106  container_type m_container;
107  boost::mutex m_mutex;
108  boost::condition m_not_empty;
109  boost::condition m_not_full;
110 };/* class SynchronizedSharedChannel<T> */
111 
112 }/* CVC4 namespace */
113 
114 #endif /* __CVC4__CHANNEL_H */
virtual ~SharedChannel()
Definition: channel.h:40
Definition: options.h:76
boost::circular_buffer< T > container_type
Definition: channel.h:65
SynchronizedSharedChannel(size_type capacity)
Definition: channel.h:70
#define CVC4_PUBLIC
Definition: cvc4_public.h:30
bool push(param_type item)
Definition: channel.h:72
Macros that should be defined everywhere during the building of the libraries and driver binary...
SharedChannel(int maxsize)
Definition: channel.h:39
container_type::value_type value_type
Definition: channel.h:67
container_type::size_type size_type
Definition: channel.h:66
boost::call_traits< value_type >::param_type param_type
Definition: channel.h:68