1 /*
2 * This file is part of the Yices SMT Solver.
3 * Copyright (C) 2017 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 * EQUALITY ABSTRACT DOMAIN
21 */
22
23 /*
24 * This module provides support for computing the equalities implied by a
25 * formula F. This uses abstract interpretation ideas:
26 * - the abstraction of a formula F is the set of equalities (t_1 == t_2)
27 * implied by F
28 * - to compute abs(F) we represent the set of equalities as a term partition
29 * - this module implements the computation of 'meets' and 'joins' in the
30 * abstract domain.
31 *
32 * TODO? improve the implementation to take advantage of the new term
33 * indexing (i.e., terms are now (index + polarity)).
34 */
35
36 #ifndef __EQ_ABSTRACTION_H
37 #define __EQ_ABSTRACTION_H
38
39 #include <stdint.h>
40
41 #include "terms/terms.h"
42 #include "utils/int_vectors.h"
43
44
45 /*
46 * Compact representation of a term partition:
47 * - we just store the classes in an array
48 * - each class is separated from the next by an end marker (NULL_TERM)
49 * - the partition header contains the number of classes
50 * and the array size
51 */
52 typedef struct epartition_s {
53 uint32_t nclasses;
54 uint32_t size; // size of the array data = nterms + nclasses
55 term_t data[0];
56 } epartition_t;
57
58
59 /*
60 * Maximal size of a partition
61 */
62 #define EPARTITION_MAX_SIZE ((UINT32_MAX-sizeof(epartition_t))/sizeof(term_t))
63
64
65 /*
66 * Auxiliary structure for computing meet and join
67 * - for a term t, label[t] = an integer index
68 * - each class is stored as a circular list of terms
69 * next[t] = successor of t in its class
70 * - for each class i, root[i] is the root of the class
71 * some classes may be marked as empty by setting root[i] to NULL_TERM
72 * - subclass = array used for join (to split a class c)
73 * The label is interpreted in different ways during meet and join
74 * - during a join operation, label[t] = the index of the class of t,
75 * if t is not in any class, we set label[t] = -1
76 * - during a meet operation, label[t] = index of t in an epartition object p.
77 * = index of the class of p that contains t.
78 */
79 typedef struct epartition_manager_s {
80 uint32_t e_size; // size of arrays label and next
81 uint32_t nterms; // number of terms such that label[t] >= 0
82 int32_t *label; // maps term to a class index
83 term_t *next;
84
85 uint32_t c_size; // size of the class array
86 uint32_t nclasses; // number of classes (<= csize)
87 uint32_t order; // number of nonempty classes
88 term_t *root; // root of each class
89
90 uint32_t sc_size; // size of the subclass array
91 int32_t *subclass; // maps labels to class id
92
93 // internal buffer
94 ivector_t buffer;
95
96 // cache for the empty partition
97 epartition_t *empty;
98 } epartition_manager_t;
99
100
101 /*
102 * Maximal and default sizes of these arrays
103 */
104 #define EQABS_DEF_ESIZE 5
105 #define EQABS_MAX_ESIZE (UINT32_MAX/4)
106 #define EQABS_DEF_CSIZE 2
107 #define EQABS_MAX_CSIZE (UINT32_MAX/4)
108 #define EQABS_DEF_SCSIZE EQABS_DEF_CSIZE
109 #define EQABS_MAX_SCSIZE EQABS_MAX_CSIZE
110
111 /*
112 * Initial buffer size
113 */
114 #define EQABS_BUFFER_SIZE 1
115
116
117
118 /*
119 * Initialize manager m:
120 * - allocate arrays of default sizes and create the empty partition
121 */
122 extern void init_epartition_manager(epartition_manager_t *m);
123
124 /*
125 * Deletion: free all data
126 */
127 extern void delete_epartition_manager(epartition_manager_t *m);
128
129
130 /*
131 * SIMPLE PARTITIONS
132 */
133
134 /*
135 * Get the empty partition (m must be initialized first)
136 */
empty_epartition(epartition_manager_t * m)137 static inline epartition_t *empty_epartition(epartition_manager_t *m) {
138 return m->empty;
139 }
140
141 /*
142 * Create a basic partition for (x == y)
143 * - one class with two elements x and y (x and y must be distinct)
144 */
145 extern epartition_t *basic_epartition(term_t x, term_t y);
146
147
148 /*
149 * Delete a partition
150 */
delete_epartition(epartition_manager_t * m,epartition_t * p)151 static inline void delete_epartition(epartition_manager_t *m, epartition_t *p) {
152 if (p != m->empty) {
153 safe_free(p);
154 }
155 }
156
157
158 /*
159 * MEET COMPUTATION
160 */
161
162 /*
163 * Initialize m for a meet operation, p = first partition
164 * - m must be empty
165 */
166 extern void epartition_init_for_meet(epartition_manager_t *m, epartition_t *p);
167
168 /*
169 * Store in m the meet of m and p:
170 * - the result is the smallest partition that satisfies:
171 * (t == u) in m implies t == u in result
172 * (t == u) in p implies t == u in result
173 */
174 extern void epartition_meet(epartition_manager_t *m, epartition_t *p);
175
176 /*
177 * Convert the partition in m into an epartition object
178 * - also reset m to the empty partition
179 */
180 extern epartition_t *epartition_get_meet(epartition_manager_t *m);
181
182
183
184
185 /*
186 * JOIN COMPUTATION
187 */
188
189 /*
190 * Initialize m for a join operation, p = first partition
191 * - m must be empty
192 */
193 extern void epartition_init_for_join(epartition_manager_t *m, epartition_t *p);
194
195 /*
196 * Store in m the join of m and p:
197 * - the result is the coarsest partition that satisfies:
198 * (t == u) in m and (t == u) in p implies (t == u) in result
199 */
200 extern void epartition_join(epartition_manager_t *m, epartition_t *p);
201
202 /*
203 * Convert the partition in m into an epartition object
204 * - also reset m to the empty partition
205 */
206 extern epartition_t *epartition_get_join(epartition_manager_t *m);
207
208
209
210
211 #endif /* __EQ_ABSTRACTION_H */
212