1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2018 SRI International.
4 *
5 * Yices is free software: you can redistribute it and/or modify
6 * it under the terms of the GNU General Public License as published by
7 * the Free Software Foundation, either version 3 of the License, or
8 * (at your option) any later version.
9 *
10 * Yices is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
14 *
15 * You should have received a copy of the GNU General Public License
16 * along with Yices. If not, see <http://www.gnu.org/licenses/>.
17 */
18
19 /*
20 * STACK TO STORE ASSUMPTIONS IN A CONTEXT
21 */
22
23 /*
24 * To deal with assumptions, the context provides three main
25 * functions:
26 *
27 * 1) add_assumption(context_t *ctx, term_t t) returns a literal
28 * (if this literal is set to true then term t is assumed in
29 * the context).
30 *
31 * 2) check_context_with_assumptions that take an array of assumed
32 * literals
33 *
34 * 3) context_build_unsat_core that computes an inconsistent subset
35 * of the assumed literals.
36 *
37 * To support this and properly work with push and pop, we use a
38 * stack to store all assumptions and keep track of the term they
39 * represent. Assumption literals are deleted on a call to push.
40 */
41
42 #ifndef __ASSUMPTION_STACK_H
43 #define __ASSUMPTION_STACK_H
44
45 #include <stdint.h>
46
47 #include "solvers/cdcl/smt_core_base_types.h"
48 #include "terms/terms.h"
49
50
51 /*
52 * Elements in the stack:
53 * - term = assumed term (Boolean)
54 * - lit = corresponding literal in the CDCL solver
55 * - level = base level when the assumption was added
56 */
57 typedef struct assumption_elem_s {
58 term_t term;
59 literal_t lit;
60 uint32_t level;
61 } assumption_elem_t;
62
63
64 /*
65 * Index structure:
66 * - a hash table that maps term/literal to an int32 index
67 * - size = size of the table (a power of 2)
68 * - nelems = number of elements stored in the table
69 * - ndeleted = number of deleted elements
70 * - resize and cleanup thresholds
71 */
72 typedef struct hash_index_s {
73 int32_t *data;
74 uint32_t size;
75 uint32_t nelems;
76 uint32_t ndeleted;
77 uint32_t resize_threshold;
78 uint32_t cleanup_threshold;
79 } hash_index_t;
80
81 #define DEF_ASSUMPTION_INDEX_SIZE 64
82 #define MAX_ASSUMPTION_INDEX_SIZE (UINT32_MAX/sizeof(int32_t))
83
84 #define ASSUMPTION_INDEX_RESIZE_RATIO 0.65
85 #define ASSUMPTION_INDEX_CLEANUP_RATIO 0.20
86
87
88 /*
89 * Stack + two indexes
90 * - data = stack content
91 * - size = size of the data array
92 * - top = index of the top of the stack
93 * the stack is data[0 ... top-1]
94 * - level is incremented on push and decremented on pop
95 *
96 * - lit_index maps literal --> assumption element
97 * - term_index maps terms --> assumption element
98 */
99 typedef struct assumption_stack_s {
100 assumption_elem_t *data;
101 hash_index_t lit_index;
102 hash_index_t term_index;
103 uint32_t size;
104 uint32_t top;
105 uint32_t level ;
106 } assumption_stack_t;
107
108 #define DEF_ASSUMPTION_STACK_SIZE 64
109 #define MAX_ASSUMPTION_STACK_SIZE (UINT32_MAX/sizeof(assumption_elem_t))
110
111
112 /*
113 * Initialize the stack:
114 * - nothing is allocated yet
115 * - level is set to 0
116 */
117 extern void init_assumption_stack(assumption_stack_t *stack);
118
119 /*
120 * Free memory
121 */
122 extern void delete_assumption_stack(assumption_stack_t *stack);
123
124 /*
125 * Empty the stack and the index arrays
126 */
127 extern void reset_assumption_stack(assumption_stack_t *stack);
128
129 /*
130 * Start a new level
131 */
assumption_stack_push(assumption_stack_t * stack)132 static inline void assumption_stack_push(assumption_stack_t *stack) {
133 stack->level ++;
134 }
135
136 /*
137 * Close the current level and remove all assumptions added at this
138 * level. stack->nlevels must be positive.
139 */
140 extern void assumption_stack_pop(assumption_stack_t *stack);
141
142 /*
143 * Add a pair (t, l) on top of the stack: at the current level
144 */
145 extern void assumption_stack_add(assumption_stack_t *stack, term_t t, literal_t l);
146
147 /*
148 * Search for a term t attached to literal l in the stack:
149 * - this searches for an element of the form (t, l, k) in the stack
150 * and return t;
151 * - if several terms are mapped to l, the function returns the first one
152 * (i.e., with the lowest level k).
153 * - if there's no such element, the function returns NULL_TERM (i.e., -1)
154 */
155 extern term_t assumption_term_for_literal(const assumption_stack_t *stack, literal_t l);
156
157 /*
158 * Search for a literal l attached to term t in the stack:
159 * - search for a triple (t, l, k) in the stack and return l
160 * - return null_literal if there's no such triple
161 */
162 extern literal_t assumption_literal_for_term(const assumption_stack_t *stack, term_t t);
163
164
165 #endif /* __ASSUMPTION_STACK_H */
166