27 #define BTOR_INIT_STACK(mem, stack) \  argument
30     (stack).mm    = mem;            \
31     (stack).start = 0;              \
32     (stack).top   = 0;              \
33     (stack).end   = 0;              \
36 #define BTOR_COUNT_STACK(stack) \  argument
37   (assert ((stack).mm), (size_t) ((stack).top - (stack).start))
39 #define BTOR_EMPTY_STACK(stack) \  argument
40   (assert ((stack).mm), (stack).top == (stack).start)
42 #define BTOR_RESET_STACK(stack)                       \  argument
45     assert ((stack).mm), (stack).top = (stack).start; \
48 #define BTOR_SIZE_STACK(stack) \  argument
49   (assert ((stack).mm), (size_t) ((stack).end - (stack).start))
51 #define BTOR_FULL_STACK(stack) (assert ((stack).mm), (stack).top == (stack).end)  argument
53 #define BTOR_RELEASE_STACK(stack)                                        \  argument
56     assert ((stack).mm);                                                 \
57     BTOR_DELETEN ((stack).mm, (stack).start, BTOR_SIZE_STACK ((stack))); \
58     BTOR_INIT_STACK ((stack).mm, (stack));                               \
61 #define BTOR_ENLARGE_STACK(stack)                                 \  argument
64     assert ((stack).mm);                                          \
65     size_t old_size  = BTOR_SIZE_STACK (stack), new_size;         \
66     size_t old_count = BTOR_COUNT_STACK (stack);                  \
67     BTOR_ENLARGE ((stack).mm, (stack).start, old_size, new_size); \
68     (stack).top = (stack).start + old_count;                      \
69     (stack).end = (stack).start + new_size;                       \
72 #define BTOR_ENLARGE_STACK_TO_SIZE(stack, new_size)               \  argument
75     assert ((stack).mm);                                          \
76     size_t old_size  = BTOR_SIZE_STACK (stack);                   \
77     size_t old_count = BTOR_COUNT_STACK (stack);                  \
78     BTOR_REALLOC ((stack).mm, (stack).start, old_size, new_size); \
79     (stack).top = (stack).start + old_count;                      \
80     (stack).end = (stack).start + new_size;                       \
105 #define BTOR_FIT_STACK(stack, idx)                                  \  argument
108     assert ((stack).mm);                                            \
109     size_t old_size = BTOR_SIZE_STACK (stack), old_count, new_size; \
111     old_count = BTOR_COUNT_STACK (stack);                           \
115     BTOR_REALLOC ((stack).mm, (stack).start, old_size, new_size);   \
116     (stack).top = (stack).start + old_count;                        \
117     (stack).end = (stack).start + new_size;                         \
118     BTOR_CLRN ((stack).top + old_size, new_size - old_size);        \
121 #define BTOR_PUSH_STACK(stack, elem)                             \  argument
124     assert ((stack).mm);                                         \
125     if (BTOR_FULL_STACK ((stack))) BTOR_ENLARGE_STACK ((stack)); \
126     *((stack).top++) = (elem);                                   \
129 #define BTOR_PUSH_STACK_IF(cond, stack, elem) \  argument
132     assert ((stack).mm);                      \
133     if (cond) BTOR_PUSH_STACK (stack, elem);  \
136 #define BTOR_POP_STACK(stack) \  argument
137   (assert ((stack).mm), assert (!BTOR_EMPTY_STACK (stack)), (*--(stack).top))
139 #define BTOR_DEQUEUE_STACK(stack, dequeued)   \  argument
142     typeof((stack).start[0]) *BTOR_DEQUEUE_P; \
143     assert (!BTOR_EMPTY_STACK (stack));       \
144   assert ((stack).mm));                       \
145     (dequeued)     = (stack).start[0];        \
146     BTOR_DEQUEUE_P = (stack).start;           \
147     while (++BTOR_DEQUEUE_P < (stack).top)    \
149     (stack).top--;                            \
152 #define BTOR_TOP_STACK(stack) \  argument
153   (assert ((stack).mm), assert (!BTOR_EMPTY_STACK (stack)), (stack).top[-1])
155 #define BTOR_PEEK_STACK(stack, idx)                    \  argument
156   (assert ((stack).mm),                                \
157    assert ((size_t) (idx) < BTOR_COUNT_STACK (stack)), \
158    (stack).start[idx])
160 #define BTOR_POKE_STACK(stack, idx, elem)               \  argument
163     assert ((stack).mm);                                \
164     assert ((size_t) (idx) < BTOR_COUNT_STACK (stack)); \
165     (stack).start[idx] = (elem);                        \