1 /*  Boolector: Satisfiability Modulo Theories (SMT) solver.
2  *
3  *  Copyright (C) 2007-2021 by the authors listed in the AUTHORS file.
4  *
5  *  This file is part of Boolector.
6  *  See COPYING for more information on using this software.
7  */
8 
9 #ifndef BTOR_QUEUE_H_INCLUDED
10 #define BTOR_QUEUE_H_INCLUDED
11 
12 #include "utils/btormem.h"
13 
14 #include <assert.h>
15 
16 #define BTOR_DECLARE_QUEUE(name, type)    \
17   typedef struct name##Queue name##Queue; \
18   struct name##Queue                      \
19   {                                       \
20     BtorMemMgr* mm;                       \
21     type* start;                          \
22     type* head;                           \
23     type* tail;                           \
24     type* end;                            \
25   }
26 
27 #define BTOR_INIT_QUEUE(mem, queue) \
28   do                                \
29   {                                 \
30     (queue).mm    = mem;            \
31     (queue).start = 0;              \
32     (queue).head  = 0;              \
33     (queue).tail  = 0;              \
34     (queue).end   = 0;              \
35   } while (0)
36 
37 #define BTOR_COUNT_QUEUE(queue) \
38   (assert ((queue).mm), (size_t) ((queue).tail - (queue).head))
39 #define BTOR_EMPTY_QUEUE(queue) \
40   (assert ((queue).mm), (queue).tail == (queue).head)
41 
42 #define BTOR_RESET_QUEUE(queue)                  \
43   do                                             \
44   {                                              \
45     assert ((queue).mm);                         \
46     (queue).head = (queue).tail = (queue).start; \
47   } while (0)
48 
49 #define BTOR_SIZE_QUEUE(queue) \
50   (assert ((queue).mm), (size_t) ((queue).end - (queue).start))
51 #define BTOR_FULL_QUEUE(queue) \
52   (assert ((queue).mm), (queue).tail == (queue).end)
53 
54 #define BTOR_RELEASE_QUEUE(queue)                                        \
55   do                                                                     \
56   {                                                                      \
57     assert ((queue).mm);                                                 \
58     BTOR_DELETEN ((queue).mm, (queue).start, BTOR_SIZE_QUEUE ((queue))); \
59     BTOR_INIT_QUEUE ((queue).mm, queue);                                 \
60   } while (0)
61 
62 #define BTOR_ENLARGE_QUEUE(queue)                                 \
63   do                                                              \
64   {                                                               \
65     assert ((queue).mm);                                          \
66     uint32_t old_size     = BTOR_SIZE_QUEUE (queue), new_size;    \
67     uint32_t old_tail_pos = (queue).tail - (queue).start;         \
68     uint32_t old_head_pos = (queue).head - (queue).start;         \
69     BTOR_ENLARGE ((queue).mm, (queue).start, old_size, new_size); \
70     (queue).tail = (queue).start + old_tail_pos;                  \
71     (queue).head = (queue).start + old_head_pos;                  \
72     (queue).end  = (queue).start + new_size;                      \
73   } while (0)
74 
75 #define BTOR_MOVE_QUEUE(queue)                                            \
76   do                                                                      \
77   {                                                                       \
78     assert ((queue).mm);                                                  \
79     uint32_t offset = (queue).head - (queue).start;                       \
80     uint32_t count  = BTOR_COUNT_QUEUE ((queue));                         \
81     memmove ((queue).start, (queue).head, count * sizeof *(queue).start); \
82     (queue).head = (queue).start;                                         \
83     (queue).tail -= offset;                                               \
84   } while (0)
85 
86 #define BTOR_ENQUEUE(queue, elem)                                 \
87   do                                                              \
88   {                                                               \
89     assert ((queue).mm);                                          \
90     if (BTOR_FULL_QUEUE ((queue)))                                \
91     {                                                             \
92       if (2 * BTOR_COUNT_QUEUE (queue) < BTOR_SIZE_QUEUE (queue)) \
93         BTOR_MOVE_QUEUE ((queue));                                \
94       else                                                        \
95         BTOR_ENLARGE_QUEUE ((queue));                             \
96     }                                                             \
97     assert ((queue).tail < (queue).end);                          \
98     *(queue).tail++ = (elem);                                     \
99   } while (0)
100 
101 #define BTOR_DEQUEUE(queue) (assert ((queue).mm), *(queue).head++)
102 
103 BTOR_DECLARE_QUEUE (BtorInt, int32_t);
104 
105 #endif
106