1 /*-----------------------------------------------------------------------
2
3 File : ccl_global_indices.c
4
5 Author: Stephan Schulz (schulz@eprover.org)
6
7 Contents
8
9 Code handling several simple indices.
10
11 Copyright 2010 by the author.
12 This code is released under the GNU General Public Licence and
13 the GNU Lesser General Public License.
14 See the file COPYING in the main E directory for details..
15 Run "eprover -h" for contact information.
16
17 Changes
18
19 <1> Fri May 7 21:19:48 CEST 2010
20 New
21
22 -----------------------------------------------------------------------*/
23
24 #include "ccl_global_indices.h"
25
26
27
28 /*---------------------------------------------------------------------*/
29 /* Global Variables */
30 /*---------------------------------------------------------------------*/
31
32 PERF_CTR_DEFINE(PMIndexTimer);
33 PERF_CTR_DEFINE(BWRWIndexTimer);
34
35 /*---------------------------------------------------------------------*/
36 /* Forward Declarations */
37 /*---------------------------------------------------------------------*/
38
39
40 /*---------------------------------------------------------------------*/
41 /* Internal Functions */
42 /*---------------------------------------------------------------------*/
43
44
45
46 /*---------------------------------------------------------------------*/
47 /* Exported Functions */
48 /*---------------------------------------------------------------------*/
49
50
51 /*-----------------------------------------------------------------------
52 //
53 // Function: GlobalIndicesNull()
54 //
55 // Set the global indices to NULL.
56 //
57 // Global Variables: -
58 //
59 // Side Effects : -
60 //
61 /----------------------------------------------------------------------*/
62
GlobalIndicesNull(GlobalIndices_p indices)63 void GlobalIndicesNull(GlobalIndices_p indices)
64 {
65 indices->bw_rw_index = NULL;
66 indices->pm_into_index = NULL;
67 indices->pm_negp_index = NULL;
68 indices->pm_from_index = NULL;
69 }
70
71
72 /*-----------------------------------------------------------------------
73 //
74 // Function: GlobalIndicesInit()
75 //
76 // Initialize the global indices as required by the parameters.
77 //
78 // Global Variables: -
79 //
80 // Side Effects : Memory operations
81 //
82 /----------------------------------------------------------------------*/
83
GlobalIndicesInit(GlobalIndices_p indices,Sig_p sig,char * rw_bw_index_type,char * pm_from_index_type,char * pm_into_index_type)84 void GlobalIndicesInit(GlobalIndices_p indices,
85 Sig_p sig,
86 char* rw_bw_index_type,
87 char* pm_from_index_type,
88 char* pm_into_index_type)
89 {
90 FPIndexFunction indexfun;
91
92 // fprintf(GlobalOut, "# GlobalIndicesInit(%p, <>, %s, %s, %s)\n", indices, rw_bw_index_type, pm_from_index_type, pm_into_index_type);
93
94 indices->sig = sig;
95 indexfun = GetFPIndexFunction(rw_bw_index_type);
96 strcpy(indices->rw_bw_index_type, rw_bw_index_type);
97 if(indexfun)
98 {
99 indices->bw_rw_index = FPIndexAlloc(indexfun, sig, SubtermBWTreeFreeWrapper);
100 }
101 indexfun = GetFPIndexFunction(pm_from_index_type);
102 strcpy(indices->pm_from_index_type, pm_from_index_type);
103 if(indexfun)
104 {
105 indices->pm_from_index = FPIndexAlloc(indexfun, sig, SubtermOLTreeFreeWrapper);
106 }
107 indexfun = GetFPIndexFunction(pm_into_index_type);
108 strcpy(indices->pm_into_index_type, pm_into_index_type);
109 if(indexfun)
110 {
111 indices->pm_into_index = FPIndexAlloc(indexfun, sig, SubtermOLTreeFreeWrapper);
112 }
113 indexfun = GetFPIndexFunction(pm_into_index_type);
114 strcpy(indices->pm_negp_index_type, pm_into_index_type);
115 if(indexfun)
116 {
117 indices->pm_negp_index = FPIndexAlloc(indexfun, sig, SubtermOLTreeFreeWrapper);
118 }
119 }
120
121
122 /*-----------------------------------------------------------------------
123 //
124 // Function: GlobalIndicesFreeIndices()
125 //
126 // Free the existing indices.
127 //
128 // Global Variables: -
129 //
130 // Side Effects : Memory operations
131 //
132 /----------------------------------------------------------------------*/
133
GlobalIndicesFreeIndices(GlobalIndices_p indices)134 void GlobalIndicesFreeIndices(GlobalIndices_p indices)
135 {
136 if(indices->bw_rw_index)
137 {
138 FPIndexFree(indices->bw_rw_index);
139 indices->bw_rw_index = NULL;
140 }
141 if(indices->pm_from_index)
142 {
143 FPIndexFree(indices->pm_from_index);
144 indices->pm_from_index = NULL;
145 }
146 if(indices->pm_into_index)
147 {
148 FPIndexFree(indices->pm_into_index);
149 indices->pm_into_index = NULL;
150 }
151 if(indices->pm_negp_index)
152 {
153 FPIndexFree(indices->pm_negp_index);
154 indices->pm_negp_index = NULL;
155 }
156 }
157
158
159 /*-----------------------------------------------------------------------
160 //
161 // Function: GlobalIndicesReset()
162 //
163 // Reset all exisiting indices.
164 //
165 // Global Variables: -
166 //
167 // Side Effects : Memory operations
168 //
169 /----------------------------------------------------------------------*/
170
GlobalIndicesReset(GlobalIndices_p indices)171 void GlobalIndicesReset(GlobalIndices_p indices)
172 {
173 GlobalIndicesFreeIndices(indices);
174
175 GlobalIndicesInit(indices,
176 indices->sig,
177 indices->rw_bw_index_type,
178 indices->pm_from_index_type,
179 indices->pm_into_index_type);
180 }
181
182
183 /*-----------------------------------------------------------------------
184 //
185 // Function: GlobalIndicesInsertClause()
186 //
187 // Add a clause to all exisiting global indices.
188 //
189 // Global Variables: -
190 //
191 // Side Effects : Memory operations
192 //
193 /----------------------------------------------------------------------*/
194
GlobalIndicesInsertClause(GlobalIndices_p indices,Clause_p clause)195 void GlobalIndicesInsertClause(GlobalIndices_p indices, Clause_p clause)
196 {
197 assert(!ClauseQueryProp(clause, CPIsGlobalIndexed));
198
199 ClauseSetProp(clause, CPIsGlobalIndexed);
200
201 // printf("# Inserting clause %p in index %p: ", clause, indices);ClausePrint(stdout, clause, true); printf("\n");
202
203 if(indices->bw_rw_index)
204 {
205 PERF_CTR_ENTRY(BWRWIndexTimer);
206 SubtermIndexInsertClause(indices->bw_rw_index, clause);
207 PERF_CTR_EXIT(BWRWIndexTimer);
208 }
209
210 if(indices->pm_into_index)
211 {
212 PERF_CTR_ENTRY(PMIndexTimer);
213 //OverlapIndexInsertIntoClause(indices->pm_into_index, clause);
214 OverlapIndexInsertIntoClause2(indices->pm_into_index,
215 indices->pm_negp_index,
216 clause);
217 PERF_CTR_EXIT(PMIndexTimer);
218 }
219 if(indices->pm_from_index)
220 {
221 PERF_CTR_ENTRY(PMIndexTimer);
222 OverlapIndexInsertFromClause(indices->pm_from_index, clause);
223 PERF_CTR_EXIT(PMIndexTimer);
224 }
225 }
226
227
228
229 /*-----------------------------------------------------------------------
230 //
231 // Function: GlobalIndicesDeleteClause()
232 //
233 // Remove a clause from all exisiting global indices.
234 //
235 // Global Variables: -
236 //
237 // Side Effects : Memory operations
238 //
239 /----------------------------------------------------------------------*/
240
GlobalIndicesDeleteClause(GlobalIndices_p indices,Clause_p clause)241 void GlobalIndicesDeleteClause(GlobalIndices_p indices, Clause_p clause)
242 {
243 // printf("# XXX GlobalIndicesDeleteClause()... (set=%p): ", clause->set);ClausePrint(GlobalOut, clause, true);printf("\n");
244
245 assert(ClauseQueryProp(clause, CPIsGlobalIndexed));
246
247 ClauseDelProp(clause, CPIsGlobalIndexed);
248
249 if(indices->bw_rw_index)
250 {
251 PERF_CTR_ENTRY(BWRWIndexTimer);
252 SubtermIndexDeleteClause(indices->bw_rw_index, clause);
253 PERF_CTR_EXIT(BWRWIndexTimer);
254 }
255
256 if(indices->pm_into_index)
257 {
258 PERF_CTR_ENTRY(PMIndexTimer);
259 // OverlapIndexDeleteIntoClause(indices->pm_into_index, clause);
260 OverlapIndexDeleteIntoClause2(indices->pm_into_index,
261 indices->pm_negp_index,
262 clause);
263 PERF_CTR_EXIT(PMIndexTimer);
264 }
265 if(indices->pm_from_index)
266 {
267 PERF_CTR_ENTRY(PMIndexTimer);
268 OverlapIndexDeleteFromClause(indices->pm_from_index, clause);
269 PERF_CTR_EXIT(PMIndexTimer);
270 }
271 // printf("# ...GlobalIndicesDeleteClause()\n");
272 }
273
274
275 /*-----------------------------------------------------------------------
276 //
277 // Function: GlobalIndicesInsertClauseSet()
278 //
279 // Insert all clause in set into the indices.
280 //
281 // Global Variables: -
282 //
283 // Side Effects : Memory operations
284 //
285 /----------------------------------------------------------------------*/
286
GlobalIndicesInsertClauseSet(GlobalIndices_p indices,ClauseSet_p set)287 void GlobalIndicesInsertClauseSet(GlobalIndices_p indices,
288 ClauseSet_p set)
289 {
290 Clause_p handle;
291
292 // fprintf(GlobalOut, "GlobalIndicesInsertClauseSet(%p, %p)\n", indices, set);
293
294 if(!indices->bw_rw_index)
295 {
296 return;
297 }
298 for(handle=set->anchor->succ; handle!=set->anchor; handle=handle->succ)
299 {
300 GlobalIndicesInsertClause(indices, handle);
301 }
302 }
303
304
305
306 /*---------------------------------------------------------------------*/
307 /* End of File */
308 /*---------------------------------------------------------------------*/
309
310
311