]>
Commit | Line | Data |
---|---|---|
885824d3 | 1 | /* |
28bf4b0b | 2 | ** Copyright (C) University of Virginia, Massachusetts Institue of Technology 1994-2001. |
885824d3 | 3 | ** See ../LICENSE for license information. |
4 | ** | |
5 | */ | |
6 | /* | |
7 | ** clauseStack.h | |
8 | */ | |
9 | ||
10 | # ifndef clauseStack_H | |
11 | # define clauseStack_H | |
12 | ||
28bf4b0b | 13 | abst_typedef struct |
885824d3 | 14 | { |
15 | int nelements; | |
16 | int nspace; | |
17 | int current; | |
18 | /*@reldef@*/ clause *elements; | |
19 | } *clauseStack ; | |
20 | ||
21 | /*@iter clauseStack_elements (sef clauseStack s, yield clause el); @*/ | |
22 | # define clauseStack_elements(s, m_el) \ | |
23 | { int m_i; for (m_i = (s)->nelements - 1; m_i >= 0; m_i--) { clause m_el = (s)->elements[m_i]; | |
24 | ||
25 | # define end_clauseStack_elements }} | |
26 | ||
27 | extern int clauseStack_size (clauseStack p_s) /*@*/ ; | |
28 | extern bool clauseStack_isEmpty (clauseStack p_s) /*@*/ ; | |
29 | ||
30 | # define clauseStack_size(s) ((s)->nelements) | |
31 | # define clauseStack_isEmpty(s) (clauseStack_size(s) == 0) | |
32 | ||
33 | extern /*@only@*/ clauseStack clauseStack_new (void) /*@*/ ; | |
34 | ||
35 | extern void clauseStack_push (clauseStack p_s, clause p_el) /*@modifies p_s@*/ ; | |
36 | extern void clauseStack_pop (clauseStack p_s) /*@modifies p_s@*/ ; | |
37 | extern clause clauseStack_top (clauseStack p_s) /*@*/ ; | |
38 | ||
39 | extern /*@only@*/ cstring clauseStack_unparse (clauseStack p_s) /*@*/ ; | |
40 | extern void clauseStack_free (/*@only@*/ clauseStack p_s) ; | |
41 | extern void clauseStack_clear (clauseStack p_s) /*@modifies p_s@*/ ; | |
42 | extern void clauseStack_switchTop (clauseStack p_s, clause p_x) /*@modifies p_s@*/ ; | |
43 | extern void clauseStack_removeFirst (clauseStack p_s, clause p_key) | |
44 | /*@modifies p_s@*/ ; | |
45 | ||
46 | extern int clauseStack_controlDepth (clauseStack p_s) /*@*/ ; | |
47 | ||
48 | /*@constant int clauseStackBASESIZE;@*/ | |
49 | # define clauseStackBASESIZE MIDBASESIZE | |
50 | ||
51 | # else | |
52 | # error "Multiple include" | |
53 | # endif | |
54 | ||
55 | ||
56 | ||
57 |