ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Macros | Functions
stack.h File Reference
#include <stdlib.h>
#include "global.h"
Include dependency graph for stack.h:
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Macros

#define STACK(TYPE)
 
#define FULL_STACK(S)
 
#define EMPTY_STACK(S)
 
#define SIZE_STACK(S)
 
#define CAPACITY_STACK(S)
 
#define INIT_STACK(S)
 
#define TOP_STACK(S)
 
#define PEEK_STACK(S, N)
 
#define POKE_STACK(S, N, E)
 
#define POP_STACK(S)
 
#define ENLARGE_STACK(S)
 
#define SHRINK_STACK(S)
 
#define PUSH_STACK(S, E)
 
#define BEGIN_STACK(S)
 
#define END_STACK(S)
 
#define CLEAR_STACK(S)
 
#define RESIZE_STACK(S, NEW_SIZE)
 
#define SET_END_OF_STACK(S, P)
 
#define RELEASE_STACK(S)
 
#define REMOVE_STACK(T, S, E)
 
#define REVERSE_STACK(T, S)
 
#define all_stack(T, E, S)
 
#define all_pointers(T, E, S)
 

Functions

typedef STACK (char) chars
 
typedef STACK (int) ints
 
typedef STACK (size_t) sizes
 
typedef STACK (unsigned) unsigneds
 
void kissat_stack_enlarge (struct kissat *, chars *, size_t size_of_element)
 
void kissat_shrink_stack (struct kissat *, chars *, size_t size_of_element)
 

Macro Definition Documentation

◆ all_pointers

#define all_pointers ( T,
E,
S )
Value:
T *E, *const *E##_PTR = BEGIN_STACK (S), \
*const *const E##_END = END_STACK (S); \
E##_PTR != E##_END && (E = *E##_PTR, true); \
++E##_PTR
BEGIN_STACK
#define BEGIN_STACK(S)
Definition stack.h:46
END_STACK
#define END_STACK(S)
Definition stack.h:48

Definition at line 122 of file stack.h.

122#define all_pointers(T, E, S) \
123 T *E, *const *E##_PTR = BEGIN_STACK (S), \
124 *const *const E##_END = END_STACK (S); \
125 E##_PTR != E##_END && (E = *E##_PTR, true); \
126 ++E##_PTR

◆ all_stack

#define all_stack ( T,
E,
S )
Value:
T E, *E##_PTR = BEGIN_STACK (S), *const E##_END = END_STACK (S); \
E##_PTR != E##_END && (E = *E##_PTR, true); \
++E##_PTR

Definition at line 117 of file stack.h.

117#define all_stack(T, E, S) \
118 T E, *E##_PTR = BEGIN_STACK (S), *const E##_END = END_STACK (S); \
119 E##_PTR != E##_END && (E = *E##_PTR, true); \
120 ++E##_PTR

◆ BEGIN_STACK

#define BEGIN_STACK ( S)
Value:
(S).begin

Definition at line 57 of file stack.h.

◆ CAPACITY_STACK

#define CAPACITY_STACK ( S)
Value:
((size_t) ((S).allocated - (S).begin))

Definition at line 19 of file stack.h.

◆ CLEAR_STACK

#define CLEAR_STACK ( S)
Value:
do { \
(S).end = (S).begin; \
} while (0)

Definition at line 61 of file stack.h.

61#define CLEAR_STACK(S) \
62 do { \
63 (S).end = (S).begin; \
64 } while (0)

◆ EMPTY_STACK

#define EMPTY_STACK ( S)
Value:
((S).begin == (S).end)

Definition at line 17 of file stack.h.

◆ END_STACK

#define END_STACK ( S)
Value:
(S).end

Definition at line 59 of file stack.h.

◆ ENLARGE_STACK

#define ENLARGE_STACK ( S)
Value:
do { \
KISSAT_assert (FULL_STACK (S)); \
kissat_stack_enlarge (solver, (chars *) &(S), sizeof *(S).begin); \
} while (0)
FULL_STACK
#define FULL_STACK(S)
Definition stack.h:17
solver
#define solver
Definition kitten.c:211

Definition at line 38 of file stack.h.

38#define ENLARGE_STACK(S) \
39 do { \
40 KISSAT_assert (FULL_STACK (S)); \
41 kissat_stack_enlarge (solver, (chars *) &(S), sizeof *(S).begin); \
42 } while (0)

◆ FULL_STACK

#define FULL_STACK ( S)
Value:
((S).end == (S).allocated)

Definition at line 16 of file stack.h.

◆ INIT_STACK

#define INIT_STACK ( S)
Value:
do { \
(S).begin = (S).end = (S).allocated = 0; \
} while (0)

Definition at line 21 of file stack.h.

21#define INIT_STACK(S) \
22 do { \
23 (S).begin = (S).end = (S).allocated = 0; \
24 } while (0)

◆ PEEK_STACK

#define PEEK_STACK ( S,
N )
Value:
(BEGIN_STACK (S)[KISSAT_assert ((N) < SIZE_STACK (S)), (N)])
SIZE_STACK
#define SIZE_STACK(S)
Definition stack.h:19
KISSAT_assert
#define KISSAT_assert(ignore)
Definition global.h:13

Definition at line 28 of file stack.h.

28#define PEEK_STACK(S, N) \
29 (BEGIN_STACK (S)[KISSAT_assert ((N) < SIZE_STACK (S)), (N)])

◆ POKE_STACK

#define POKE_STACK ( S,
N,
E )
Value:
do { \
PEEK_STACK (S, N) = (E); \
} while (0)

Definition at line 31 of file stack.h.

31#define POKE_STACK(S, N, E) \
32 do { \
33 PEEK_STACK (S, N) = (E); \
34 } while (0)

◆ POP_STACK

#define POP_STACK ( S)
Value:
(KISSAT_assert (!EMPTY_STACK (S)), *--(S).end)
EMPTY_STACK
#define EMPTY_STACK(S)
Definition stack.h:18

Definition at line 36 of file stack.h.

◆ PUSH_STACK

#define PUSH_STACK ( S,
E )
Value:
do { \
if (FULL_STACK (S)) \
ENLARGE_STACK (S); \
*(S).end++ = (E); \
} while (0)

Definition at line 50 of file stack.h.

50#define PUSH_STACK(S, E) \
51 do { \
52 if (FULL_STACK (S)) \
53 ENLARGE_STACK (S); \
54 *(S).end++ = (E); \
55 } while (0)

◆ RELEASE_STACK

#define RELEASE_STACK ( S)
Value:
do { \
DEALLOC ((S).begin, CAPACITY_STACK (S)); \
INIT_STACK (S); \
} while (0)
CAPACITY_STACK
#define CAPACITY_STACK(S)
Definition stack.h:20

Definition at line 82 of file stack.h.

82#define RELEASE_STACK(S) \
83 do { \
84 DEALLOC ((S).begin, CAPACITY_STACK (S)); \
85 INIT_STACK (S); \
86 } while (0)

◆ REMOVE_STACK

#define REMOVE_STACK ( T,
S,
E )
Value:
do { \
KISSAT_assert (!EMPTY_STACK (S)); \
T *END_REMOVE_STACK = END_STACK (S); \
T *P_REMOVE_STACK = BEGIN_STACK (S); \
while (*P_REMOVE_STACK != (E)) { \
P_REMOVE_STACK++; \
KISSAT_assert (P_REMOVE_STACK != END_REMOVE_STACK); \
} \
P_REMOVE_STACK++; \
while (P_REMOVE_STACK != END_REMOVE_STACK) { \
P_REMOVE_STACK[-1] = *P_REMOVE_STACK; \
P_REMOVE_STACK++; \
} \
(S).end--; \
} while (0)

Definition at line 88 of file stack.h.

88#define REMOVE_STACK(T, S, E) \
89 do { \
90 KISSAT_assert (!EMPTY_STACK (S)); \
91 T *END_REMOVE_STACK = END_STACK (S); \
92 T *P_REMOVE_STACK = BEGIN_STACK (S); \
93 while (*P_REMOVE_STACK != (E)) { \
94 P_REMOVE_STACK++; \
95 KISSAT_assert (P_REMOVE_STACK != END_REMOVE_STACK); \
96 } \
97 P_REMOVE_STACK++; \
98 while (P_REMOVE_STACK != END_REMOVE_STACK) { \
99 P_REMOVE_STACK[-1] = *P_REMOVE_STACK; \
100 P_REMOVE_STACK++; \
101 } \
102 (S).end--; \
103 } while (0)

◆ RESIZE_STACK

#define RESIZE_STACK ( S,
NEW_SIZE )
Value:
do { \
const size_t TMP_NEW_SIZE = (NEW_SIZE); \
KISSAT_assert (TMP_NEW_SIZE <= SIZE_STACK (S)); \
(S).end = (S).begin + TMP_NEW_SIZE; \
} while (0)

Definition at line 66 of file stack.h.

66#define RESIZE_STACK(S, NEW_SIZE) \
67 do { \
68 const size_t TMP_NEW_SIZE = (NEW_SIZE); \
69 KISSAT_assert (TMP_NEW_SIZE <= SIZE_STACK (S)); \
70 (S).end = (S).begin + TMP_NEW_SIZE; \
71 } while (0)

◆ REVERSE_STACK

#define REVERSE_STACK ( T,
S )
Value:
do { \
if (SIZE_STACK (S) < 2) \
break; \
T *HEAD = (S).begin, *TAIL = (S).end - 1; \
while (HEAD < TAIL) { \
T TMP = *HEAD; \
*HEAD++ = *TAIL; \
*TAIL-- = TMP; \
} \
} while (0)
HEAD
@ HEAD
Definition inflate.h:23

Definition at line 105 of file stack.h.

105#define REVERSE_STACK(T, S) \
106 do { \
107 if (SIZE_STACK (S) < 2) \
108 break; \
109 T *HEAD = (S).begin, *TAIL = (S).end - 1; \
110 while (HEAD < TAIL) { \
111 T TMP = *HEAD; \
112 *HEAD++ = *TAIL; \
113 *TAIL-- = TMP; \
114 } \
115 } while (0)

◆ SET_END_OF_STACK

#define SET_END_OF_STACK ( S,
P )
Value:
do { \
KISSAT_assert (BEGIN_STACK (S) <= (P)); \
KISSAT_assert ((P) <= END_STACK (S)); \
if ((P) == END_STACK (S)) \
break; \
(S).end = (P); \
} while (0)

Definition at line 73 of file stack.h.

73#define SET_END_OF_STACK(S, P) \
74 do { \
75 KISSAT_assert (BEGIN_STACK (S) <= (P)); \
76 KISSAT_assert ((P) <= END_STACK (S)); \
77 if ((P) == END_STACK (S)) \
78 break; \
79 (S).end = (P); \
80 } while (0)

◆ SHRINK_STACK

#define SHRINK_STACK ( S)
Value:
do { \
if (!FULL_STACK (S)) \
kissat_shrink_stack (solver, (chars *) &(S), sizeof *(S).begin); \
} while (0)

Definition at line 44 of file stack.h.

44#define SHRINK_STACK(S) \
45 do { \
46 if (!FULL_STACK (S)) \
47 kissat_shrink_stack (solver, (chars *) &(S), sizeof *(S).begin); \
48 } while (0)

◆ SIZE_STACK

#define SIZE_STACK ( S)
Value:
((size_t) ((S).end - (S).begin))

Definition at line 18 of file stack.h.

◆ STACK

#define STACK ( TYPE)
Value:
struct { \
TYPE *begin; \
TYPE *end; \
TYPE *allocated; \
}
TYPE
@ TYPE
Definition inflate.h:34

Definition at line 9 of file stack.h.

9#define STACK(TYPE) \
10 struct { \
11 TYPE *begin; \
12 TYPE *end; \
13 TYPE *allocated; \
14 }

◆ TOP_STACK

#define TOP_STACK ( S)
Value:
(END_STACK (S)[KISSAT_assert (!EMPTY_STACK (S)), -1])

Definition at line 26 of file stack.h.

Function Documentation

◆ kissat_shrink_stack()

void kissat_shrink_stack ( struct kissat * solver,
chars * s,
size_t size_of_element )

Definition at line 26 of file stack.c.

26 {
27 KISSAT_assert (bytes > 0);
28 const size_t old_bytes_capacity = CAPACITY_STACK (*s);
29 KISSAT_assert (kissat_aligned_word (old_bytes_capacity));
30 KISSAT_assert (!(old_bytes_capacity % bytes));
31 KISSAT_assert (kissat_is_zero_or_power_of_two (old_bytes_capacity / bytes));
32 const size_t old_bytes_size = SIZE_STACK (*s);
33 KISSAT_assert (!(old_bytes_size % bytes));
34 const size_t old_size = old_bytes_size / bytes;
35 size_t new_capacity;
36 if (old_size) {
37 const unsigned ld_old_size = kissat_log2_ceiling_of_word (old_size);
38 new_capacity = ((size_t) 1) << ld_old_size;
39 } else
40 new_capacity = 0;
41 KISSAT_assert (kissat_is_zero_or_power_of_two (new_capacity));
42 size_t new_bytes_capacity = new_capacity * bytes;
43 while (!kissat_aligned_word (new_bytes_capacity))
44 new_bytes_capacity <<= 1;
45 if (new_bytes_capacity == old_bytes_capacity)
46 return;
47 KISSAT_assert (new_bytes_capacity < old_bytes_capacity);
48 s->begin = (char*)kissat_realloc (solver, s->begin, old_bytes_capacity,
49 new_bytes_capacity);
50 s->allocated = s->begin + new_bytes_capacity;
51 s->end = s->begin + old_bytes_size;
52 KISSAT_assert (s->end <= s->allocated);
53}
kissat_realloc
void * kissat_realloc(kissat *solver, void *p, size_t old_bytes, size_t new_bytes)
Definition allocate.c:123
Here is the call graph for this function:

◆ kissat_stack_enlarge()

void kissat_stack_enlarge ( struct kissat * solver,
chars * s,
size_t size_of_element )

Definition at line 9 of file stack.c.

9 {
10 const size_t size = SIZE_STACK (*s);
11 const size_t old_bytes = CAPACITY_STACK (*s);
12 KISSAT_assert (MAX_SIZE_T / 2 >= old_bytes);
13 size_t new_bytes;
14 if (old_bytes)
15 new_bytes = 2 * old_bytes;
16 else {
17 new_bytes = bytes;
18 while (!kissat_aligned_word (new_bytes))
19 new_bytes <<= 1;
20 }
21 s->begin = (char*)kissat_realloc (solver, s->begin, old_bytes, new_bytes);
22 s->allocated = s->begin + new_bytes;
23 s->end = s->begin + size;
24}
NewBdd::size
unsigned long long size
Definition giaNewBdd.h:39
MAX_SIZE_T
#define MAX_SIZE_T
Definition utilities.h:45
Here is the call graph for this function:
Here is the caller graph for this function:

◆ STACK() [1/4]

typedef STACK ( char )

◆ STACK() [2/4]

typedef STACK ( int )

◆ STACK() [3/4]

typedef STACK ( size_t )

◆ STACK() [4/4]

typedef STACK ( unsigned )

Definition at line 89 of file cadical_kitten.c.

94 {
95 unsigned level;
96 unsigned reason;
97};