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