1 /*
2 * share.c -- routines to manage the shared data structures
3 *
4 */
5
6 #include "header.h"
7
8 #define TERM_TAB_SIZE 3793
9
10 /* Hash table of shared terms */
11
12 static struct term_ptr *Term_tab[TERM_TAB_SIZE];
13
14 /* alphas and betas of pos eq lits are not shared, so they are put here */
15 /* so that back dedmodulation can find them */
16
17 static struct term_ptr *Bd_kludge;
18
19 /*************
20 *
21 * int hash_term(term)
22 *
23 * Return the hash value of a term. It is assumed that
24 * the subterms are already integrated. The hash value is
25 * constructed from the function symbol and the addresses of the
26 * subterms.
27 *
28 *************/
29
hash_term(struct term * t)30 static int hash_term(struct term *t)
31 {
32 struct rel *r;
33 int hashval;
34
35 if (t->type == NAME) /* name */
36 hashval = t->sym_num;
37 else if (t->type == VARIABLE) /* variable */
38 hashval = t->sym_num + t->varnum + 25;
39 else { /* complex */
40 hashval = t->sym_num;
41 r = t->farg;
42 while (r != NULL) {
43 hashval >>= 1; /* shift right one bit */
44 hashval ^= (int) r->argval; /* exclusive or */
45 r = r->narg;
46 }
47 }
48 return(abs(hashval) % TERM_TAB_SIZE);
49 } /* hash_term */
50
51 /*************
52 *
53 * int term_compare(t1, t2)
54 *
55 * Special purpose term comparison for term integration.
56 * Succeed iff functors are identical and subterm pointers are
57 * identical. (Note that this routine is not recursive.)
58 * (For general purpose routine, see `term_ident'.)
59 *
60 *************/
61
term_compare(struct term * t1,struct term * t2)62 static int term_compare(struct term *t1,
63 struct term *t2)
64 {
65 struct rel *r1, *r2;
66
67 if (t1->type != t2->type)
68 return(0);
69 else if (t1->type == NAME) /* name */
70 return(t1->sym_num == t2->sym_num);
71 else if (t1->type == VARIABLE) /* variable */
72 return(t1->varnum == t2->varnum && t1->sym_num == t2->sym_num);
73 else if (t1->sym_num != t2->sym_num)
74 return(0); /* both complex with different functors */
75 else {
76 r1 = t1->farg;
77 r2 = t2->farg;
78 while (r1 != NULL && r2 != NULL) {
79 if (r1->argval != r2->argval)
80 return(0);
81 else {
82 r1 = r1->narg;
83 r2 = r2->narg;
84 }
85 }
86 return(r1 == NULL && r2 == NULL);
87 }
88 } /* term_compare */
89
90 /*************
91 *
92 * struct term *integrate_term(term)
93 *
94 * Incorporate a term into the shared data structures.
95 * Either ther term itself is integrated and returned, or
96 * the term is deallocated and a previously integrated copy
97 * is returned. A good way to invoke it is
98 *
99 * t = integrate(t)
100 *
101 *************/
102
integrate_term(struct term * t)103 struct term *integrate_term(struct term *t)
104 {
105 int hashval, found;
106 struct term_ptr *p, *prev;
107 struct rel *r, *r2;
108
109 if (t->type == COMPLEX) { /* complex term */
110 r = t->farg;
111 while (r != NULL) {
112 r->argval = integrate_term(r->argval);
113 r = r->narg;
114 }
115 }
116
117 hashval = hash_term(t);
118
119 p = Term_tab[hashval];
120 prev = NULL;
121
122 found = 0;
123 while (found == 0 && p != NULL)
124 if (term_compare(t, p->term))
125 found = 1;
126 else {
127 prev = p;
128 p = p->next;
129 }
130
131 if (found) { /* p->term is integrated copy */
132 if (t == p->term) {
133 print_term_nl(stdout, t);
134 abend("integrate_term, already integrated.");
135 }
136 if (t->type == COMPLEX) { /* if complex, free rels */
137 r = t->farg;
138 while (r != NULL) {
139 r2 = r;
140 r = r->narg;
141 free_rel(r2);
142 }
143 }
144 free_term(t);
145 return(p->term);
146 }
147 else { /* not in bucket, so insert at end of bucket and return */
148 if (t->type == COMPLEX) { /* if complex, set up containment lists */
149 r = t->farg;
150 while (r != NULL) {
151 r->argof = t;
152 r->nocc = r->argval->occ.rel;
153 r->argval->occ.rel = r;
154 r = r->narg;
155 }
156 }
157 p = get_term_ptr();
158 p->term = t;
159 p->next = NULL;
160 if (prev == NULL)
161 Term_tab[hashval] = p;
162 else
163 prev->next = p;
164
165 if (Flags[BACK_DEMOD].val && Flags[INDEX_FOR_BACK_DEMOD].val)
166 fpa_insert(t, Parms[FPA_TERMS].val, Fpa_back_demod);
167 return(t);
168 }
169 } /* integrate_term */
170
171 /*************
172 *
173 * disintegrate_term(term)
174 *
175 * Remove a previously integrated term from the shared data
176 * structures. A warning is printed if the term has a list of
177 * superterms.
178 *
179 *************/
180
disintegrate_term(struct term * t)181 void disintegrate_term(struct term *t)
182 {
183 int hashval;
184 struct rel *r1, *r2, *r3;
185 struct term_ptr *p1, *p2;
186
187 if (t->occ.rel != NULL) {
188 fprintf(stderr, "WARNING, disintegrate_term, contained term.\n");
189 printf("WARNING, disintegrate_term, contained term: ");
190 print_term_nl(stdout, t);
191 }
192 else {
193 hashval = hash_term(t);
194 p1 = Term_tab[hashval];
195 p2 = NULL;
196
197 while (p1 != NULL && p1->term != t) {
198 p2 = p1;
199 p1 = p1->next;
200 }
201 if (p1 == NULL)
202 abend("disintegrate_term, cannot find term.");
203 else {
204 if (p2 == NULL)
205 Term_tab[hashval] = p1->next;
206 else
207 p2->next = p1->next;
208 free_term_ptr(p1);
209 if (Flags[BACK_DEMOD].val && Flags[INDEX_FOR_BACK_DEMOD].val) {
210 CLOCK_START(UN_INDEX_TIME);
211 fpa_delete(t, Parms[FPA_TERMS].val, Fpa_back_demod);
212 CLOCK_STOP(UN_INDEX_TIME);
213 }
214 if (t->type == COMPLEX) {
215 r1 = t->farg;
216 while (r1 != NULL) {
217 r2 = r1->argval->occ.rel;
218 r3 = NULL;
219 while (r2 != NULL && r2 != r1) {
220 r3 = r2;
221 r2 = r2->nocc;
222 }
223 if (r2 == NULL) {
224 print_term_nl(stdout, t);
225 abend("disintegrate_term, bad containment.");
226 }
227 else {
228 if (r3 == NULL)
229 r1->argval->occ.rel = r1->nocc;
230 else
231 r3->nocc = r1->nocc;
232 if (r1->argval->occ.rel == NULL)
233 disintegrate_term(r2->argval);
234 }
235 r3 = r1;
236 r1 = r1->narg;
237 free_rel(r3);
238 }
239 }
240 free_term(t);
241 }
242 }
243 } /* disintegrate_term */
244
245 /*************
246 *
247 * set_up_pointers(t)
248 *
249 *************/
250
set_up_pointers(struct term * t)251 void set_up_pointers(struct term *t)
252 {
253 struct rel *r;
254
255 for (r = t->farg; r; r = r->narg) {
256 r->argof = t;
257 r->argval->occ.rel = r;
258 set_up_pointers(r->argval);
259 }
260 } /* set_up_pointers */
261
262
263 /*************
264 *
265 * zap_term(term)
266 *
267 * Deallocate a nonshared term. A warning is printed
268 * the term or any of its subterms contains a list of superterms.
269 *
270 *************/
271
zap_term(struct term * t)272 void zap_term(struct term *t)
273 {
274 struct rel *r1, *r2;
275
276 if (t->occ.rel != NULL) {
277 fprintf(stderr, "WARNING, zap_term, contained term.\n");
278 printf("WARNING, zap_term, contained term: ");
279 print_term_nl(stdout, t);
280 printf("\n");
281 }
282 else {
283 if (t->type == COMPLEX) { /* complex term */
284 r1 = t->farg;
285 while (r1 != NULL) {
286 zap_term(r1->argval);
287 r2 = r1;
288 r1 = r1->narg;
289 free_rel(r2);
290 }
291 }
292 free_term(t);
293 }
294 } /* zap_term */
295
296 /*************
297 *
298 * print_term_tab(file_ptr) -- Print the table of integrated terms.
299 *
300 *************/
301
print_term_tab(FILE * fp)302 void print_term_tab(FILE *fp)
303 {
304 int i;
305 struct term_ptr *p;
306
307 for(i=0; i<TERM_TAB_SIZE; i++)
308 if(Term_tab[i] != NULL) {
309 fprintf(fp, "bucket %d: ",i);
310 p = Term_tab[i];
311
312 while(p != NULL) {
313 print_term(fp, p->term);
314 fprintf(fp, " ");
315 p = p->next;
316 }
317 fprintf(fp, "\n");
318 }
319 } /* print_term_tab */
320
321 /*************
322 *
323 * p_term_tab()
324 *
325 *************/
326
p_term_tab(void)327 void p_term_tab(void)
328 {
329 print_term_tab(stdout);
330 } /* p_term_tab */
331
332 /*************
333 *
334 * test_terms(file_ptr)
335 *
336 * Print the list of integrated terms. For each term, list its
337 * subterms and superterms.
338 *
339 *************/
340
test_terms(FILE * fp)341 void test_terms(FILE *fp)
342 {
343 int i;
344 struct term_ptr *p;
345 struct rel *r;
346
347 for(i=0; i<TERM_TAB_SIZE; i++)
348 if(Term_tab[i] != NULL) {
349 fprintf(fp, " bucket %d:\n",i);
350 p = Term_tab[i];
351 while(p != NULL) {
352 print_term(fp, p->term);
353 fprintf(fp, " containing terms: ");
354 r = p->term->occ.rel;
355 while (r != NULL) {
356 print_term(fp, r->argof);
357 fprintf(fp, " ");
358 r = r->nocc;
359 }
360 fprintf(fp, "\n");
361 p = p->next;
362 }
363 }
364 } /* test_terms */
365
366 /*************
367 *
368 * struct term_ptr *all_instances(atom)
369 *
370 * Get all terms (in table of shared terms) that can be rewritten
371 * with demodulator (atom). Handles lex-dependent demod correctly.
372 *
373 *************/
374
all_instances(struct term * atom)375 struct term_ptr *all_instances(struct term *atom)
376 {
377 struct term *alpha, *beta, *t;
378 struct term_ptr *tp, *tp1, *instances;
379 struct context *subst;
380 struct trail *tr;
381 int i, lex_dependent, ok;
382
383 alpha = atom->farg->argval;
384 beta = atom->farg->narg->argval;
385 lex_dependent = (atom->varnum == LEX_DEP_DEMOD);
386 instances = NULL;
387 subst = get_context();
388 subst->multiplier = 1;
389 for (i = 0; i <= TERM_TAB_SIZE; i++) {
390 tp = (i == TERM_TAB_SIZE ? Bd_kludge : Term_tab[i]);
391 while (tp != NULL) {
392 tr = NULL;
393 if (match(alpha, subst, tp->term, &tr)) {
394
395 if (lex_dependent == 0)
396 ok = 1;
397 else {
398 t = apply(beta, subst);
399 if (Flags[LRPO].val)
400 ok = lrpo_greater(tp->term, t);
401 else
402 ok = (lex_check(t, tp->term) == LESS_THAN);
403 zap_term(t);
404 }
405
406 if (ok) {
407 tp1 = get_term_ptr();
408 tp1->term = tp->term;
409 tp1->next = instances;
410 instances = tp1;
411 }
412
413 clear_subst_1(tr);
414 }
415 tp = tp->next;
416 }
417 }
418 free_context(subst);
419 return(instances);
420 } /* all_instances */
421
422 /*************
423 *
424 * struct term_ptr *all_instances_fpa(atom)
425 *
426 * Get all terms (in table of shared terms) that can be rewritten
427 * with demodulator (atom). Handles lex-dependent demod correctly.
428 *
429 *************/
430
all_instances_fpa(struct term * atom,struct fpa_index * fpa)431 struct term_ptr *all_instances_fpa(struct term *atom, struct fpa_index *fpa)
432 {
433 struct term *alpha, *beta, *t, *found;
434 struct term_ptr *tp1, *instances;
435 struct context *subst;
436 struct trail *tr;
437 int lex_dependent, ok;
438 struct fpa_tree *ut;
439
440 alpha = atom->farg->argval;
441 beta = atom->farg->narg->argval;
442 lex_dependent = (atom->varnum == LEX_DEP_DEMOD);
443 instances = NULL;
444 subst = get_context();
445 subst->multiplier = 1;
446
447 ut = build_tree(alpha, INSTANCE, Parms[FPA_TERMS].val, fpa);
448
449 found = next_term(ut, 0);
450 while (found != NULL) {
451 tr = NULL;
452 if (match(alpha, subst, found, &tr)) {
453
454 if (lex_dependent == 0)
455 ok = 1;
456 else {
457 t = apply(beta, subst);
458 if (Flags[LRPO].val)
459 ok = lrpo_greater(found, t);
460 else
461 ok = (lex_check(t, found) == LESS_THAN);
462 zap_term(t);
463 }
464
465 if (ok) {
466 tp1 = get_term_ptr();
467 tp1->term = found;
468 tp1->next = instances;
469 instances = tp1;
470 }
471
472 clear_subst_1(tr);
473 }
474 found = next_term(ut, 0);
475 }
476 free_context(subst);
477 return(instances);
478 } /* all_instances_fpa */
479
480 /*************
481 *
482 * bd_kludge_insert(t)
483 *
484 * This has to do with finding terms that can be back demodulated.
485 * Terms are made available (either indexed or in table of shared
486 * terms) when integrated. However, alphas and betas are not shared,
487 * so this routine makes them available, either indexed or inserted
488 * into the Bd_kludge list.
489 *
490 *************/
491
bd_kludge_insert(struct term * t)492 void bd_kludge_insert(struct term *t)
493 {
494 struct term_ptr *tp;
495
496 if (Flags[INDEX_FOR_BACK_DEMOD].val)
497 fpa_insert(t, Parms[FPA_TERMS].val, Fpa_back_demod);
498 else {
499
500 tp = get_term_ptr();
501 tp->term = t;
502
503 tp->next = Bd_kludge;
504 Bd_kludge = tp;
505 }
506 } /* bd_kludge_insert */
507
508 /*************
509 *
510 * bd_kludge_delete(t)
511 *
512 * See Bd_kludge_insert.
513 *
514 *************/
515
bd_kludge_delete(struct term * t)516 void bd_kludge_delete(struct term *t)
517 {
518 struct term_ptr *tp1, *tp2;
519
520 if (Flags[INDEX_FOR_BACK_DEMOD].val) {
521 CLOCK_START(UN_INDEX_TIME);
522 fpa_delete(t, Parms[FPA_TERMS].val, Fpa_back_demod);
523 CLOCK_STOP(UN_INDEX_TIME);
524 }
525 else
526 {
527 tp1 = Bd_kludge;
528 tp2 = NULL;
529 while (tp1 != NULL && tp1->term != t) {
530 tp2 = tp1;
531 tp1 = tp1->next;
532 }
533 if (tp1 == NULL) {
534 fprintf(stderr, "WARNING, bd_kludge_delete, term not found.\n");
535 printf("WARNING, bd_kludge_delete, term not found: ");
536 print_term_nl(stdout, t);
537 }
538 else if (tp2 != NULL)
539 tp2->next = tp1->next;
540 else
541 Bd_kludge = tp1->next;
542
543 free_term_ptr(tp1);
544 }
545
546 } /* bd_kludge_delete */
547