1 /*
2 * check.c -- code related to proof objects and proof checking
3 *
4 */
5
6 #include "header.h"
7 #include "check.h"
8
9 /* #define DEBUG */
10
11 #define ATTEMPT_FEB_9
12
13 /* Gen_tab is a general hash table method. You can insert (id,pointer)
14 * pairs and retrieve the pointer associated with a particular id.
15 */
16
17 #define GEN_TAB_SIZE 100
18
19 struct gen_node {
20 int id;
21 void *v;
22 struct gen_node *next;
23 };
24
25 struct gen_tab {
26 struct gen_node *a[GEN_TAB_SIZE];
27 };
28
29 /* Global variables */
30
31 static struct gen_tab *Old_proof_tab;
32 static struct gen_tab *New_proof_old_id_tab;
33 static struct gen_tab *New_proof_tab;
34
35 /*************
36 *
37 * get_gen_node()
38 *
39 *************/
40
get_gen_node(void)41 struct gen_node *get_gen_node(void)
42 {
43 struct gen_node *p;
44 p = (struct gen_node *) tp_alloc((int) sizeof(struct gen_node));
45 p->id = 0;
46 p->v = NULL;
47 return(p);
48 } /* get_gen_node */
49
50 /*************
51 *
52 * get_proof_object()
53 *
54 *************/
55
get_proof_object(void)56 struct proof_object *get_proof_object(void)
57 {
58 struct proof_object *p;
59 p = (struct proof_object *) tp_alloc((int) sizeof(struct proof_object));
60 p->steps = 0;
61 p->first = NULL;
62 p->last = NULL;
63 return(p);
64 } /* get_proof_object */
65
66 /*************
67 *
68 * get_proof_object_node()
69 *
70 *************/
71
get_proof_object_node(void)72 struct proof_object_node *get_proof_object_node(void)
73 {
74 struct proof_object_node *p;
75 int i;
76 p = (struct proof_object_node *) tp_alloc((int) sizeof(struct proof_object_node));
77 p->id = 0;
78 p->old_id = 0;
79 p->parent1 = 0;
80 p->parent2 = 0;
81 p->position1 = NULL;
82 p->position2 = NULL;
83 p->map = NULL;
84 p->rule = P_RULE_UNDEFINED;
85 p->backward_subst = FALSE;
86 for (i = 0; i < 2*MAX_VARS; i++)
87 p->subst[i] = NULL;
88 p->next = NULL;
89 return(p);
90 } /* get_proof_object_node */
91
92 /*************
93 *
94 * init_gen_tab()
95 *
96 *************/
97
init_gen_tab(void)98 static struct gen_tab *init_gen_tab(void)
99 {
100 int i;
101 struct gen_tab *p;
102 p = (struct gen_tab *) tp_alloc(GEN_TAB_SIZE * (int) sizeof(void *));
103 for (i = 0; i < GEN_TAB_SIZE; i++)
104 p->a[i] = NULL;
105 return(p);
106 } /* init_gen_tab */
107
108 /*************
109 *
110 * insert_into_gen_tab()
111 *
112 * If ok, return 1; if already there, return 0.
113 *
114 *************/
115
insert_into_gen_tab(struct gen_tab * tab,int id,void * v)116 static int insert_into_gen_tab(struct gen_tab *tab,
117 int id,
118 void *v)
119 {
120 struct gen_node *p1, *p2, *p3;
121
122 p1 = tab->a[id%GEN_TAB_SIZE];
123 p2 = NULL;
124 while (p1 && p1->id < id) {
125 p2 = p1;
126 p1 = p1->next;
127 }
128 if (p1 && p1->id == id)
129 abend("insert_into_gen_tab, key already there");
130 else {
131 p3 = get_gen_node();
132 p3->id = id;
133 p3->v = v;
134 p3->next = p1;
135 if (p2)
136 p2->next = p3;
137 else
138 tab->a[id%GEN_TAB_SIZE] = p3;
139 }
140 return(1);
141 } /* insert_into_gen_tab */
142
143 /*************
144 *
145 * retrieve_from_gen_tab()
146 *
147 * Return NULL if it is not there.
148 *
149 *************/
150
retrieve_from_gen_tab(struct gen_tab * tab,int id)151 static void * retrieve_from_gen_tab(struct gen_tab *tab,
152 int id)
153 {
154 struct gen_node *p;
155
156 p = tab->a[id%GEN_TAB_SIZE];
157 while (p && p->id < id)
158 p = p->next;
159 if (p && p->id == id)
160 return(p->v);
161 else
162 return((void *) NULL);
163 } /* retrieve_from_gen_tab */
164
p_gen_tab(struct gen_tab * tab)165 static void p_gen_tab(struct gen_tab *tab)
166 {
167 struct gen_node *p;
168 int i;
169 for (i = 0; i < GEN_TAB_SIZE; i++) {
170 for (p = tab->a[i]; p; p = p->next) {
171 printf("%d: ", i);
172 p_proof_object_node(p->v);
173 }
174 }
175 } /* p_gen_tab */
176
177 /*************
178 *
179 * int check_eq_lit(lit)
180 *
181 *************/
182
check_eq_lit(struct literal * lit)183 static int check_eq_lit(struct literal *lit)
184 {
185 return(lit->atom->varnum == POS_EQ ||
186 lit->atom->varnum == NEG_EQ ||
187 lit->atom->varnum == LEX_DEP_DEMOD);
188 } /* check_eq_lit */
189
190 /*************
191 *
192 * trivial_subst()
193 *
194 * A substitution is trivial if every (nonempty) entry is
195 * "vi -> vi (NULL context)"
196 *
197 *************/
198
trivial_subst(struct context * c)199 int trivial_subst(struct context *c)
200 {
201 int i, ok;
202
203 if (c->multiplier != 0)
204 ok = 0;
205 else for (i = 0, ok = 1; i < MAX_VARS && ok; i++) {
206 if (c->terms[i]) {
207 if (c->terms[i]->type != VARIABLE)
208 ok = 0;
209 else if (c->terms[i]->varnum != i)
210 ok = 0;
211 else
212 ok = (c->contexts[i] == NULL);
213 }
214 }
215 return(ok);
216 } /* trivial_subst */
217
218 /*************
219 *
220 * connect_new_node()
221 *
222 * Add a new node to the end of the proof object; return the node.
223 *
224 *************/
225
connect_new_node(struct proof_object * new_proof)226 struct proof_object_node *connect_new_node(struct proof_object *new_proof)
227 {
228 struct proof_object_node *pn;
229 int rc;
230
231 pn = get_proof_object_node();
232 if (new_proof->steps == 0) {
233 new_proof->first = pn;
234 new_proof->last = pn;
235 }
236 else {
237 new_proof->last->next = pn;
238 new_proof->last = pn;
239 }
240 new_proof->steps++;
241 pn->id = new_proof->steps;
242 rc = insert_into_gen_tab(New_proof_tab, pn->id, pn);
243 return(pn);
244 } /* connect_new_node */
245
246 /*************
247 *
248 * po_rule()
249 *
250 * Return a poitner to the char string corresponding to the integer
251 * code for a proof object rule.
252 *
253 *************/
254
po_rule(int rule)255 static char *po_rule(int rule)
256 {
257 switch (rule) {
258 case P_RULE_UNDEFINED: return("undefined");
259 case P_RULE_INPUT: return("input");
260 case P_RULE_EQ_AXIOM: return("eq-axiom");
261 case P_RULE_INSTANTIATE: return("instantiate");
262 case P_RULE_PROPOSITIONAL: return("propositional");
263 case P_RULE_RESOLVE: return("resolve");
264 case P_RULE_PARAMOD: return("paramod");
265 case P_RULE_FLIP: return("flip");
266 default: return("unknown");
267 }
268 } /* po_rule */
269
270 /*************
271 *
272 * print_term_s()
273 *
274 * Print a term, S-expression style.
275 *
276 *************/
277
print_term_s(FILE * fp,struct term * t)278 void print_term_s(FILE *fp,
279 struct term *t)
280 {
281 if (t->type == VARIABLE) {
282 if (t->sym_num != 0)
283 fprintf(fp, "%s", sn_to_str(t->sym_num));
284 else
285 fprintf(fp, "v%d", t->varnum);
286 }
287 else {
288 struct rel *r;
289 fprintf(fp, "(%s", sn_to_str(t->sym_num));
290 for (r = t->farg; r; r = r->narg) {
291 fprintf(fp, " ");
292 print_term_s(fp, r->argval);
293 }
294 fprintf(fp, ")");
295 }
296 } /* print_term_s */
297
298 /*************
299 *
300 * p_term_s()
301 *
302 *************/
303
p_term_s(struct term * t)304 void p_term_s(struct term *t)
305 {
306 print_term_s(stdout, t);
307 } /* print_term_s */
308
309 /*************
310 *
311 * print_clause_s()
312 *
313 * Print a clause, S-expression style (without a newline).
314 *
315 *************/
316
print_clause_s(FILE * fp,struct clause * c)317 void print_clause_s(FILE *fp,
318 struct clause *c)
319 {
320 struct literal *lit;
321 fprintf(fp, "(");
322 for (lit = c->first_lit; lit; lit = lit->next_lit) {
323 if (!lit->sign)
324 fprintf(fp, "(not ");
325 print_term_s(fp, lit->atom);
326 if (!lit->sign)
327 fprintf(fp, ")");
328 if (lit->next_lit)
329 fprintf(fp, " ");
330 }
331 fprintf(fp, ")");
332 fflush(fp);
333 } /* print_clause_s */
334
335 /*************
336 *
337 * p_clause_s()
338 *
339 *************/
340
p_clause_s(struct clause * c)341 void p_clause_s(struct clause *c)
342 {
343 print_clause_s(stdout, c);
344 } /* print_clause_s */
345
346 /*************
347 *
348 * print_clause_s2()
349 *
350 * Print a clause, S-expression style (without a newline).
351 *
352 *************/
353
print_clause_s2(FILE * fp,struct clause * c)354 void print_clause_s2(FILE *fp,
355 struct clause *c)
356 {
357 if (c->first_lit == NULL)
358 fprintf(fp, "false");
359 else {
360 struct literal *lit;
361
362 for (lit = c->first_lit; lit; lit = lit->next_lit) {
363 if (lit->next_lit)
364 fprintf(fp, "(or ");
365 if (!lit->sign)
366 fprintf(fp, "(not ");
367
368 if (is_symbol(lit->atom, "$T", 0))
369 fprintf(fp, "true");
370 else if (is_symbol(lit->atom, "$F", 0))
371 fprintf(fp, "false");
372 else
373 print_term_s(fp, lit->atom);
374
375 if (!lit->sign)
376 fprintf(fp, ")");
377 if (lit->next_lit)
378 fprintf(fp, " ");
379 }
380 for (lit = c->first_lit->next_lit; lit; lit = lit->next_lit)
381 fprintf(fp, ")");
382 }
383 fflush(fp);
384 } /* print_clause_s2 */
385
386 /*************
387 *
388 * p_clause_s2()
389 *
390 *************/
391
p_clause_s2(struct clause * c)392 void p_clause_s2(struct clause *c)
393 {
394 print_clause_s2(stdout, c);
395 } /* print_clause_s2 */
396
397 /*************
398 *
399 * print_proof_object_node()
400 *
401 *************/
402
print_proof_object_node(FILE * fp,struct proof_object_node * pn)403 void print_proof_object_node(FILE *fp,
404 struct proof_object_node *pn)
405 {
406 int i;
407
408 fprintf(fp, "(%d ", pn->id);
409 fprintf(fp, "(%s", po_rule(pn->rule));
410
411 switch (pn->rule) {
412 case P_RULE_INPUT:
413 case P_RULE_EQ_AXIOM:
414 fprintf(fp, ") ");
415 break;
416 case P_RULE_INSTANTIATE:
417 fprintf(fp, " %d (", pn->parent1);
418 for (i = 0; i < 2*MAX_VARS; i++) {
419 if (pn->subst[i]) {
420 if (pn->backward_subst) {
421 fprintf(fp, "(");
422 print_term_s(fp, pn->subst[i]);
423 fprintf(fp, " . v%d)", i);
424 }
425 else {
426 fprintf(fp, "(v%d . ", i);
427 print_term_s(fp, pn->subst[i]);
428 fprintf(fp, ")");
429 }
430 }
431 }
432 fprintf(fp, ")) ");
433 break;
434 case P_RULE_RESOLVE:
435 case P_RULE_PARAMOD:
436 fprintf(fp, " %d ", pn->parent1);
437 print_ilist(fp, pn->position1);
438 fprintf(fp, " %d ", pn->parent2);
439 print_ilist(fp, pn->position2);
440 fprintf(fp, ") ");
441 break;
442 case P_RULE_PROPOSITIONAL:
443 fprintf(fp, " %d) ", pn->parent1);
444 break;
445 case P_RULE_FLIP:
446 fprintf(fp, " %d ", pn->parent1);
447 print_ilist(fp, pn->position1);
448 fprintf(fp, ") ");
449 break;
450 default:
451 abend("print_proof_object_node, bad rule");
452 break;
453 }
454
455 if (Flags[BUILD_PROOF_OBJECT_2].val)
456 print_clause_s2(fp, pn->c);
457 else
458 print_clause_s(fp, pn->c);
459 if (pn->old_id != 0)
460 fprintf(fp, " (%d)", pn->old_id); /* Otter ID */
461 else
462 fprintf(fp, " NIL"); /* Otter ID */
463 fprintf(fp, ")\n");
464 fflush(fp);
465 } /* print_proof_object_node */
466
467 /*************
468 *
469 * p_proof_object_node()
470 *
471 *************/
472
p_proof_object_node(struct proof_object_node * pn)473 void p_proof_object_node(struct proof_object_node *pn)
474 {
475 print_proof_object_node(stdout, pn);
476 } /* print_proof_object_node */
477
478 /*************
479 *
480 * print_proof_object()
481 *
482 *************/
483
print_proof_object(FILE * fp,struct proof_object * po)484 void print_proof_object(FILE *fp,
485 struct proof_object *po)
486 {
487 struct proof_object_node *pn;
488 fprintf(fp, "(\n");
489 for (pn = po->first; pn; pn = pn->next)
490 print_proof_object_node(fp, pn);
491 fprintf(fp, ")\n");
492 } /* print_proof_object */
493
494 /*************
495 *
496 * p_proof_object()
497 *
498 *************/
499
p_proof_object(struct proof_object * po)500 void p_proof_object(struct proof_object *po)
501 {
502 print_proof_object(stdout, po);
503 } /* print_proof_object */
504
505 /*************
506 *
507 * new_literal_index()
508 *
509 * Given a list of integers and a value v, return the position of v.
510 *
511 *************/
512
new_literal_index(struct ilist * ip,int v)513 static int new_literal_index(struct ilist *ip,
514 int v)
515 {
516 int i;
517 for (i = 1; ip && abs(ip->i) != v; ip = ip->next, i++);
518 if (!ip)
519 abend("new_literal_index, bad map");
520 return(i);
521 } /* new_literal_index */
522
523 /*************
524 *
525 * copy_subst_to_proof_object()
526 *
527 *************/
528
copy_subst_to_proof_object(struct context * subst,struct proof_object_node * p)529 static void copy_subst_to_proof_object(struct context *subst,
530 struct proof_object_node *p)
531 {
532 struct term *t;
533 int i;
534
535 t = get_term();
536 t->type = VARIABLE;
537
538 /* If multiplier=0, only need to copy nonNULL entries, because the
539 * variables won't change.
540 */
541
542 if (subst->multiplier == 0) {
543 for (i = 0; i < MAX_VARS; i++) {
544 if (subst->terms[i]) {
545 t->varnum = i;
546 p->subst[i] = apply(t, subst);
547 }
548 }
549 }
550 else {
551 int max;
552 struct proof_object_node *parent;
553
554 parent = retrieve_from_gen_tab(New_proof_tab, p->parent1);
555 max = biggest_var_clause(parent->c);
556 for (i = 0; i <= max; i++) {
557 t->varnum = i;
558 p->subst[i] = apply(t, subst);
559 }
560
561 }
562 free_term(t);
563 } /* copy_subst_to_proof_object */
564
565 /*************
566 *
567 * cl_copy_delete_literal()
568 *
569 *************/
570
cl_copy_delete_literal(struct clause * c,int n)571 struct clause *cl_copy_delete_literal(struct clause *c,
572 int n)
573 {
574 struct clause *d;
575 struct literal *l1, *l2;
576 int i;
577
578 d = cl_copy(c);
579 for (l1 = d->first_lit, l2 = NULL, i = 1;
580 i < n;
581 l2 = l1, l1 = l1->next_lit, i++);
582
583 if (l2)
584 l2->next_lit = l1->next_lit;
585 else
586 d->first_lit = l1->next_lit;
587 return(d);
588 } /* cl_copy_delete_literal */
589
590 /*************
591 *
592 * int variant(t1, c1, t2, c2, trail_address, flip) -- alphabetic variant
593 *
594 * I take a shortcut and just call `match' twice. If speed is a
595 * concern, this routine should be rewritten.
596 *
597 * if (flip), t1 has arity 2 and should be flipped before test.
598 *
599 * WARNING!! if you use the substitutions for anything, use either one,
600 * but don't use both. This is because, for example, when given
601 * p(x), p(y), x is bound to y and y is bound to x!
602 *
603 * The use of the trail is the same as in `unify'.
604 *
605 *************/
606
variant(struct term * t1,struct context * c1,struct term * t2,struct context * c2,struct trail ** trp,int flip)607 int variant(struct term *t1,
608 struct context *c1,
609 struct term *t2,
610 struct context *c2,
611 struct trail **trp,
612 int flip)
613 {
614 struct trail *tpos;
615 struct term *tt;
616 int rc;
617
618 if (flip) {
619 t1 = copy_term(t1);
620 tt = t1->farg->argval;
621 t1->farg->argval = t1->farg->narg->argval;
622 t1->farg->narg->argval = tt;
623 }
624 tpos = *trp;
625 if (match(t1, c1, t2, trp)) {
626 if (match(t2, c2, t1, trp))
627 rc = 1;
628 else {
629 clear_subst_2(*trp, tpos);
630 *trp = tpos;
631 rc = 0;
632 }
633 }
634 else
635 rc = 0;
636
637 if (flip)
638 zap_term(t1);
639 return(rc);
640 } /* variant */
641
642 /*************
643 *
644 * match_literals()
645 *
646 * Note that literals are indexed starting with 1, not 0.
647 *
648 *************/
649
match_literals(struct clause * c1,struct context * s1,int * m1,struct clause * c2,struct context * s2,int * m2,struct trail ** trp)650 static int match_literals(struct clause *c1,
651 struct context *s1,
652 int *m1,
653 struct clause *c2,
654 struct context *s2,
655 int *m2,
656 struct trail **trp)
657 {
658 struct literal *l1, *l2;
659 int i1, i2, matched, flip;
660 struct trail *t_pos;
661
662 /* Find the first unmatched literal of c2. */
663 for (l2 = c2->first_lit, i2=1; l2 && m2[i2]!=0; l2 = l2->next_lit, i2++);
664 if (!l2)
665 return(1); /* Success. All literals matched. */
666 else {
667 matched = 0;
668 flip = 0;
669 i1 = 1;
670 l1 = c1->first_lit;
671 while (l1 && !matched) {
672 t_pos = *trp; /* save position in trail in case of failure */
673 if (m1[i1]==0 && l1->sign == l2->sign &&
674 variant(l1->atom, s1, l2->atom, s2, trp, flip)) {
675 m1[i1] = (flip ? -i2: i2);
676 m2[i2] = (flip ? -i1: i1);
677 if (match_literals(c1, s1, m1, c2, s2, m2, trp))
678 matched = 1;
679 else {
680 m1[i1] = 0;
681 m2[i2] = 0;
682 clear_subst_2(*trp, t_pos);
683 *trp = t_pos;
684 }
685 }
686 /* increment */
687 if (check_eq_lit(l1) && check_eq_lit(l2) && !flip) {
688 flip = 1;
689 }
690 else {
691 l1 = l1->next_lit;
692 i1++;
693 flip = 0;
694 }
695 }
696 return(matched);
697 }
698 } /* match_literals */
699
700 /*************
701 *
702 * match_clauses(c1, c2)
703 *
704 * This routine takes 2 clauses that are supposed to be
705 * alphabetic variants (if not, return NULL). The literals
706 * may be in different orders, and equality literals may
707 * be flipped. We find the correspondence and
708 * return it as a list of integers: the i-th integer is the
709 * index in c1 of the i-th literal in c2. If an equality
710 * literal is flipped, the index is negated.
711 *
712 *************/
713
match_clauses(struct clause * c1,struct clause * c2)714 struct ilist *match_clauses(struct clause *c1,
715 struct clause *c2)
716 {
717 int m1[MAX_LITS+1], m2[MAX_LITS+1];
718 struct context *s1, *s2;
719 struct trail *tr;
720 int i, rc, n1, n2;
721 struct ilist *ip1, *ip2;
722
723 n1 = num_literals(c1);
724 n2 = num_literals(c2);
725 if (n1 != n2)
726 abend("match_clauses, different numbers of literals");
727
728 s1 = get_context();
729 s2 = get_context();
730
731 for (i = 1; i <= MAX_LITS; i++) {
732 m1[i] = 0;
733 m2[i] = 0;
734 }
735
736 tr = NULL;
737 rc = match_literals(c1, s1, m1, c2, s2, m2, &tr);
738 if (!rc) {
739 abend("match_clauses, literals don't match");
740 }
741 clear_subst_1(tr);
742 free_context(s1);
743 free_context(s2);
744
745 #ifdef DEBUG
746 printf("\nmatch_clauses rc=%d\n", rc);
747 for (i = 1; i <= MAX_LITS; i++)
748 printf("%3d", m1[i]);
749 p_clause(c1);
750 for (i = 1; i <= MAX_LITS; i++)
751 printf("%3d", m2[i]);
752 p_clause(c2);
753 #endif
754
755 ip1 = NULL;
756 for (i = n1; i > 0; i--) {
757 ip2 = get_ilist();
758 ip2->i = m2[i];
759 ip2->next = ip1;
760 ip1 = ip2;
761 }
762 return(ip1);
763 } /* match_clauses */
764
765 /*************
766 *
767 * cl_append()
768 *
769 *************/
770
cl_append(struct clause * c1,struct clause * c2)771 struct clause *cl_append(struct clause *c1,
772 struct clause *c2)
773 {
774 struct literal *curr, *prev;
775
776 for (curr = c1->first_lit, prev = NULL;
777 curr;
778 prev = curr, curr = curr->next_lit);
779
780 if (prev)
781 prev->next_lit = c2->first_lit;
782 else
783 c1->first_lit = c2->first_lit;
784
785 for (curr = c2->first_lit; curr; curr = curr->next_lit)
786 curr->container = c1;
787
788 free_clause(c2);
789 return(c1);
790 } /* cl_append */
791
792 /*************
793 *
794 * identity_resolve()
795 *
796 *************/
797
identity_resolve(struct clause * c1,int i1,struct clause * c2,int i2)798 struct clause *identity_resolve(struct clause *c1,
799 int i1,
800 struct clause *c2,
801 int i2)
802 {
803 struct clause *d1, *d2, *res;
804
805 d1 = cl_copy_delete_literal(c1, i1);
806 d2 = cl_copy_delete_literal(c2, i2);
807 res = cl_append(d1, d2);
808 return(res);
809
810 } /* identity_resolve */
811
812 /*************
813 *
814 * identity_paramod()
815 *
816 *************/
817
identity_paramod(struct clause * from_cl,struct ilist * from_pos,struct clause * into_cl,struct ilist * into_pos)818 static struct clause *identity_paramod(struct clause *from_cl,
819 struct ilist *from_pos,
820 struct clause *into_cl,
821 struct ilist *into_pos)
822 {
823 struct clause *into_prime, *from_prime, *para;
824 struct literal *from_lit, *into_lit;
825 struct term *beta, *t;
826 struct ilist *ip;
827 struct rel *r;
828 int i;
829
830 from_lit = ith_literal(from_cl, from_pos->i);
831 if (from_pos->next->i == 1)
832 beta = from_lit->atom->farg->narg->argval;
833 else
834 beta = from_lit->atom->farg->argval;
835
836 into_prime = cl_copy(into_cl);
837 into_lit = ith_literal(into_prime, into_pos->i);
838
839 /* Get the into term. */
840
841 for (ip = into_pos->next, t = into_lit->atom; ip; ip = ip->next) {
842 for (i = 1, r = t->farg; i < ip->i; i++, r = r->narg);
843 t = r->argval;
844 }
845
846 /* Now r points at into term t. */
847
848 r->argval = copy_term(beta);
849
850 from_prime = cl_copy_delete_literal(from_cl, from_pos->i);
851 para = cl_append(from_prime, into_prime);
852
853 return(para);
854
855 } /* identity_paramod */
856
857 /*************
858 *
859 * void renumber_vars_subst()
860 *
861 *************/
862
renumber_vars_subst(struct clause * c,struct term ** terms)863 void renumber_vars_subst(struct clause *c,
864 struct term **terms)
865 {
866 struct literal *lit;
867 int varnums[MAX_VARS];
868 int i, ok;
869 struct term *t;
870
871 ok = 1;
872 for (i = 0; i < MAX_VARS; i++)
873 varnums[i] = -1;
874
875 lit = c->first_lit;
876 while (lit) {
877 if (renum_vars_term(lit->atom, varnums) == 0)
878 ok = 0;
879 lit = lit->next_lit;
880 }
881
882 for (i = 0; i < MAX_VARS; i++) {
883 if (varnums[i] != -1 && varnums[i] != i) {
884 t = get_term();
885 t->type = VARIABLE;
886 t->varnum = i;
887 terms[varnums[i]] = t;
888 }
889 }
890 } /* renumber_vars_subst */
891
892 /*************
893 *
894 * translate_unit_deletion()
895 *
896 *************/
897
translate_unit_deletion(struct proof_object_node * current,struct proof_object_node * unit,struct proof_object * new_proof)898 static int translate_unit_deletion(struct proof_object_node *current,
899 struct proof_object_node *unit,
900 struct proof_object *new_proof)
901 {
902 struct literal *l1, *l2;
903 struct proof_object_node *instance, *resolvent;
904 struct context *subst;
905 struct trail *tr;
906 int found, index;
907 struct ilist *ip1, *ip2;
908
909 /* First, find the literal that is deleted. */
910
911 subst = get_context(); subst->multiplier = 0;
912 l2 = unit->c->first_lit;
913 for (l1 = current->c->first_lit, found = 0, index = 0;
914 l1 && !found;
915 l1 = l1->next_lit, index++) {
916 tr = NULL;
917 if (l2->sign != l1->sign && match(l2->atom,subst,l1->atom,&tr)) {
918 found = 1;
919 }
920 }
921 if (!found)
922 abend("translate_unit_deletion, unit deletion not found");
923
924 /* Set up a new proof object node for the instantiation. */
925
926 if (trivial_subst(subst))
927 instance = unit;
928 else {
929 instance = connect_new_node(new_proof);
930 instance->rule = P_RULE_INSTANTIATE;
931 instance->parent1 = unit->id;
932 instance->c = apply_clause(unit->c, subst);
933 copy_subst_to_proof_object(subst, instance);
934 }
935
936 clear_subst_1(tr);
937 free_context(subst);
938
939 /* Set up a node for the resolution (negative lit. always first parent). */
940
941 resolvent = connect_new_node(new_proof);
942 resolvent->rule = P_RULE_RESOLVE;
943 ip1 = get_ilist(); resolvent->position1 = ip1;
944 ip2 = get_ilist(); resolvent->position2 = ip2;
945 if (l2->sign) { /* unit positive */
946 resolvent->parent1 = current->id;
947 resolvent->parent2 = instance->id;
948 ip1->i = index;
949 ip2->i = 1;
950 }
951 else {
952 resolvent->parent1 = instance->id;
953 resolvent->parent2 = current->id;
954 ip1->i = 1;
955 ip2->i = index;
956 }
957
958 /* Copy the clause then delete the correct literal. */
959
960 resolvent->c = cl_copy_delete_literal(current->c, index);
961
962 return(1);
963
964 } /* translate_unit_deletion */
965
966 /*************
967 *
968 * translate_factor_simp()
969 *
970 * Apply the first factor_simp operation. Note that a sequence of
971 * factor_simps may be applied in a different order in the new proof,
972 * because the order of literals can be different. This should be OK.
973 *
974 *************/
975
translate_factor_simp(struct proof_object_node * current,struct proof_object * new_proof)976 static int translate_factor_simp(struct proof_object_node *current,
977 struct proof_object *new_proof)
978 {
979 struct literal *lit1, *lit2;
980 struct clause *factor;
981 struct context *subst;
982 struct trail *tr;
983 struct proof_object_node *previous, *instance, *merge;
984 int rc;
985
986 /* May have to renumber the variables. */
987
988 if (biggest_var_clause(current->c) >= MAX_VARS) {
989 previous = current;
990 current = connect_new_node(new_proof);
991 current->rule = P_RULE_INSTANTIATE;
992 current->parent1 = previous->id;
993 current->c = cl_copy(previous->c);
994 renumber_vars_subst(current->c, current->subst);
995 }
996
997 lit1 = NULL; lit2 = NULL;
998 factor = first_or_next_factor(current->c, &lit1, &lit2);
999 while (factor && ! subsume(factor, current->c)) {
1000 cl_del_non(factor);
1001 factor = first_or_next_factor(current->c, &lit1, &lit2);
1002 }
1003 if (!factor)
1004 abend("translate_factor_simp, factor not found");
1005
1006 cl_del_non(factor);
1007
1008 subst = get_context();
1009 subst->multiplier = 0;
1010 tr = NULL;
1011 rc = unify(lit1->atom, subst, lit2->atom, subst, &tr);
1012 if (!rc)
1013 abend("translate_factor_simp, literals don't unify");
1014
1015 if (trivial_subst(subst))
1016 instance = current;
1017 else {
1018 instance = connect_new_node(new_proof);
1019 instance->rule = P_RULE_INSTANTIATE;
1020 instance->parent1 = current->id;
1021 instance->c = apply_clause(current->c, subst);
1022 copy_subst_to_proof_object(subst, instance);
1023 }
1024
1025 clear_subst_1(tr);
1026 free_context(subst);
1027
1028 /* Build the merge node. */
1029
1030 merge = connect_new_node(new_proof);
1031 merge->rule = P_RULE_PROPOSITIONAL;
1032 merge->parent1 = instance->id;
1033 merge->position1 = get_ilist();
1034 merge->position1->i = literal_number(lit2);
1035 merge->c = cl_copy_delete_literal(instance->c, literal_number(lit2));
1036
1037 if (num_literals(instance->c)-1 != num_literals(merge->c))
1038 abend("translate_factor_simp: merge failed");
1039
1040 return(1);
1041
1042 } /* translate_factor_simp */
1043
1044 /*************
1045 *
1046 * first_rewrite()
1047 *
1048 *************/
1049
first_rewrite(struct term * t,struct ilist * pos,struct clause * c,struct clause_ptr * demods,struct context * subst,struct trail ** trp,int * demod_id)1050 static struct ilist *first_rewrite(struct term *t,
1051 struct ilist *pos,
1052 struct clause *c,
1053 struct clause_ptr *demods,
1054 struct context *subst,
1055 struct trail **trp,
1056 int *demod_id)
1057 {
1058 struct ilist *prev, *last, *pos_ok;
1059 struct rel *r;
1060 struct clause_ptr *cp;
1061 int ok;
1062 struct term *atom;
1063
1064 if (t->type == COMPLEX) {
1065 for (prev = pos; prev->next; prev = prev->next);
1066 last = get_ilist();
1067 last->i = 1;
1068 prev->next = last;
1069 for (r = t->farg; r; r = r->narg, last->i++) {
1070 pos_ok = first_rewrite(r->argval,pos,c,demods,subst,trp,demod_id);
1071 if (pos_ok)
1072 return(pos_ok);
1073 }
1074 prev->next = NULL;
1075 free_ilist(last);
1076 }
1077 if (t->type != VARIABLE) {
1078 for (cp = demods, ok = 0; cp && !ok; cp = cp->next) {
1079 atom = cp->c->first_lit->atom;
1080 ok = match(atom->farg->argval, subst, t, trp);
1081
1082 if (ok && atom->varnum == LEX_DEP_DEMOD) {
1083 int mult_flag = 0;
1084 struct term *replacement;
1085
1086 replacement = apply_demod(atom->farg->narg->argval, subst, &mult_flag);
1087 if (Flags[LRPO].val)
1088 ok = lrpo_greater(t, replacement);
1089 else
1090 ok = lex_check(replacement, t) == LESS_THAN;
1091 zap_term_special(replacement);
1092 if (!ok) {
1093 clear_subst_1(*trp);
1094 *trp = NULL;
1095 }
1096 }
1097
1098 if (ok) {
1099 *demod_id = cp->c->id;
1100 return(pos);
1101 }
1102 }
1103 }
1104 return(NULL);
1105 } /* first_rewrite */
1106
1107 /*************
1108 *
1109 * first_rewrite_clause()
1110 *
1111 *************/
1112
first_rewrite_clause(struct clause * c,struct clause_ptr * demods,struct context * subst,struct trail ** trp,int * demod_id)1113 static struct ilist *first_rewrite_clause(struct clause *c,
1114 struct clause_ptr *demods,
1115 struct context *subst,
1116 struct trail **trp,
1117 int *demod_id)
1118 {
1119 struct ilist *ip1, *ip2;
1120 struct literal *lit;
1121
1122 ip1 = get_ilist();
1123 ip1->i = 1;
1124 for (lit = c->first_lit; lit; lit = lit->next_lit, ip1->i++) {
1125 ip2 = first_rewrite(lit->atom, ip1, c, demods, subst, trp, demod_id);
1126 if (ip2)
1127 return(ip2);
1128 }
1129 free_ilist(ip1);
1130 return(NULL);
1131 } /* first_rewrite_clause */
1132
1133 /*************
1134 *
1135 * translate_demod_nonunit()
1136 *
1137 * The sequence of demodulators that apply to the original clause
1138 * might not apply to the new clause in the same order, because
1139 * the literals might be rearranged. So we collect all of the
1140 * demodulators and keep applying the set. This method is still
1141 * not perfect, because at a given term, the set of demodulators
1142 * might be tried in a different order; an abend is possible.
1143 *
1144 *************/
1145
translate_demod_nonunit(struct proof_object_node * current,struct ilist * ip,struct proof_object * new_proof)1146 static int translate_demod_nonunit(struct proof_object_node *current,
1147 struct ilist *ip,
1148 struct proof_object *new_proof)
1149 {
1150 int count1, count2, demod_id;
1151 struct ilist *ip0, *ip1, *ip2, *ip3;
1152 struct clause_ptr *demods;
1153 struct clause *c;
1154 struct context *subst;
1155 struct trail *tr;
1156 struct proof_object_node *instance, *paramod, *pn;
1157
1158 #if 0
1159 printf("\ncurrent="); p_clause(current->c);
1160 #endif
1161 demods = NULL;
1162 for (ip1 = ip, count1 = 0; ip1 && ip1->i > 0; ip1 = ip1->next, count1++) {
1163 c = cl_find(ip1->i);
1164 /* The new versions of the demodulators have to be used, because
1165 the variables might be numbered differently. We have to copy
1166 the ID and the lex-dep flag into the new version. Sorry this
1167 is so messy.
1168 */
1169 pn = retrieve_from_gen_tab(New_proof_old_id_tab, c->id);
1170 pn->c->id = pn->id;
1171 pn->c->first_lit->atom->varnum = c->first_lit->atom->varnum;
1172 #if 0
1173 printf("old demod:"); p_clause(c);
1174 printf("new demod:"); p_clause(pn->c);
1175 #endif
1176 insert_clause(pn->c, &demods); /* If not already there. */
1177 }
1178
1179 subst = get_context(); subst->multiplier = 0;
1180 tr = NULL;
1181 count2 = 0;
1182 ip0 = first_rewrite_clause(current->c,demods,subst,&tr,&demod_id);
1183 while (ip0 && count2 < count1) {
1184 count2++;
1185 pn = retrieve_from_gen_tab(New_proof_tab, demod_id);
1186
1187 if (trivial_subst(subst))
1188 instance = pn;
1189 else {
1190 instance = connect_new_node(new_proof);
1191 instance->parent1 = pn->id;
1192 instance->rule = P_RULE_INSTANTIATE;
1193 instance->c = apply_clause(pn->c, subst);
1194 copy_subst_to_proof_object(subst, instance);
1195 }
1196
1197 paramod = connect_new_node(new_proof);
1198 paramod->rule = P_RULE_PARAMOD;
1199 paramod->parent1 = instance->id;
1200 ip2 = get_ilist(); ip2->i = 1; paramod->position1 = ip2;
1201 ip3 = get_ilist(); ip3->i = 1; ip2->next = ip3;
1202 paramod->parent2 = current->id;
1203 paramod->position2 = ip0;
1204 paramod->c = identity_paramod(instance->c, paramod->position1,
1205 current->c, paramod->position2);
1206
1207 /* If into literal is negated, must add element to position.
1208 * The position vector will no longer be valid for Otter terms.
1209 */
1210
1211 if (ith_literal(current->c, ip0->i)->sign == 0) {
1212 ip1 = get_ilist();
1213 ip1->i = 1;
1214 ip1->next = ip0->next;
1215 ip0->next = ip1;
1216 }
1217
1218 current = paramod;
1219 #if 0
1220 printf("after rewrite with %d: ", demod_id); p_clause(current->c);
1221 #endif
1222 clear_subst_1(tr);
1223 tr = NULL;
1224 ip0 = first_rewrite_clause(current->c, demods, subst, &tr, &demod_id);
1225 }
1226
1227 if (ip0 || count1 != count2) {
1228 #if 0
1229 fprintf(stdout, "%d rewrites in proof, %d trans.\n", count1, count2);
1230 fprintf(stdout, "clause is "); print_clause(stdout, current->c);
1231 #endif
1232 abend("translate_demod_nonunit, wrong number of rewrites");
1233 }
1234
1235 return(1);
1236 } /* translate_demod_nonunit */
1237
1238 /*************
1239 *
1240 * translate_demod_unit()
1241 *
1242 * With units, we can apply the demodulators in the same order.
1243 *
1244 *************/
1245
translate_demod_unit(struct proof_object_node * current,struct ilist * ip,struct proof_object * new_proof)1246 static int translate_demod_unit(struct proof_object_node *current,
1247 struct ilist *ip,
1248 struct proof_object *new_proof)
1249 {
1250 int count1, demod_id;
1251 struct ilist *ip0, *ip1, *ip2, *ip3;
1252 struct clause_ptr *demods;
1253 struct clause *c;
1254 struct context *subst;
1255 struct trail *tr;
1256 struct proof_object_node *instance, *paramod, *pn;
1257
1258 #if 0
1259 printf("\ncurrent="); p_clause(current->c);
1260 #endif
1261 subst = get_context(); subst->multiplier = 0;
1262 tr = NULL;
1263 for (ip1 = ip, count1 = 0; ip1 && ip1->i > 0; ip1 = ip1->next, count1++) {
1264 c = cl_find(ip1->i);
1265 /* The new versions of the demodulators have to be used, because
1266 the variables might be numbered differently. We have to copy
1267 the ID and the lex-dep flag into the new version. Sorry this
1268 is so messy.
1269 */
1270 pn = retrieve_from_gen_tab(New_proof_old_id_tab, c->id);
1271 pn->c->id = pn->id;
1272 pn->c->first_lit->atom->varnum = c->first_lit->atom->varnum;
1273 #if 0
1274 printf("old demod:"); p_clause(c);
1275 printf("new demod:"); p_clause(pn->c);
1276 #endif
1277 demods = NULL;
1278 insert_clause(pn->c, &demods);
1279 ip0 = first_rewrite_clause(current->c,demods,subst,&tr,&demod_id);
1280 free_clause_ptr(demods);
1281
1282 if (!ip0) {
1283 printf("\nABOUT TO ABEND!\n");
1284 printf("old demod: "); p_clause(c);
1285 printf("new demod: "); p_clause(pn->c);
1286 printf("clause: "); p_clause(current->c);
1287 abend("translate_demod_unit: cannot rewrite");
1288 }
1289
1290 pn = retrieve_from_gen_tab(New_proof_tab, demod_id);
1291
1292 if (trivial_subst(subst))
1293 instance = pn;
1294 else {
1295 instance = connect_new_node(new_proof);
1296 instance->parent1 = pn->id;
1297 instance->rule = P_RULE_INSTANTIATE;
1298 instance->c = apply_clause(pn->c, subst);
1299 copy_subst_to_proof_object(subst, instance);
1300 }
1301
1302 paramod = connect_new_node(new_proof);
1303 paramod->rule = P_RULE_PARAMOD;
1304 paramod->parent1 = instance->id;
1305 ip2 = get_ilist(); ip2->i = 1; paramod->position1 = ip2;
1306 ip3 = get_ilist(); ip3->i = 1; ip2->next = ip3;
1307 paramod->parent2 = current->id;
1308 paramod->position2 = ip0;
1309 paramod->c = identity_paramod(instance->c, paramod->position1,
1310 current->c, paramod->position2);
1311
1312 /* If into literal is negated, must add element to position.
1313 * The position vector will no longer be valid for Otter terms.
1314 */
1315
1316 if (ith_literal(current->c, ip0->i)->sign == 0) {
1317 ip2 = get_ilist();
1318 ip2->i = 1;
1319 ip2->next = ip0->next;
1320 ip0->next = ip2;
1321 }
1322
1323 current = paramod;
1324 #if 0
1325 printf("after rewrite with %d: ", demod_id); p_clause(current->c);
1326 #endif
1327 clear_subst_1(tr);
1328 tr = NULL;
1329 }
1330
1331 return(1);
1332 } /* translate_demod_unit */
1333
1334 /*************
1335 *
1336 * finish_translating()
1337 *
1338 * c: the clause from the original proof; The result of this routine
1339 * should be equivalent to c.
1340 *
1341 *************/
1342
finish_translating(struct clause * c,struct ilist * rest_of_history,struct proof_object_node * current,struct proof_object * new_proof)1343 int finish_translating(struct clause *c,
1344 struct ilist *rest_of_history,
1345 struct proof_object_node *current,
1346 struct proof_object *new_proof)
1347 {
1348 int i, j, rc, ok;
1349 struct proof_object_node *previous, *pn;
1350 struct literal *l1, *l2, *prev_lit;
1351 struct ilist *ip1;
1352 struct term *t;
1353
1354 /* Process rest of history here. This code depends on the order in
1355 * which Otter processes generated clauses.
1356 * If there is any demodulation, it is first.
1357 */
1358
1359 if (rest_of_history && rest_of_history->i == DEMOD_RULE) {
1360 rest_of_history = rest_of_history->next;
1361 if (num_literals(c) == 1)
1362 rc = translate_demod_unit(current, rest_of_history, new_proof);
1363 else
1364 rc = translate_demod_nonunit(current, rest_of_history, new_proof);
1365 while (rest_of_history && rest_of_history->i > 0)
1366 rest_of_history = rest_of_history->next;
1367 current = new_proof->last;
1368 }
1369
1370 /* Equality reordering. */
1371
1372 #ifndef ATTEMPT_FEB_9
1373 /* I think all equality reordering is reflected in the
1374 justification, so we don't have to do any of it here.
1375 */
1376 if (Flags[ORDER_EQ].val) {
1377 struct clause *copy;
1378
1379 copy = cl_copy(current->c);
1380 if (Flags[LRPO].val)
1381 order_equalities_lrpo(copy);
1382 else
1383 order_equalities(copy);
1384 for(l1 = copy->first_lit, i = 1; l1; l1 = l1->next_lit, i++) {
1385 if (TP_BIT(l1->atom->bits, SCRATCH_BIT)) {
1386 previous = current;
1387 current = connect_new_node(new_proof);
1388 current->parent1 = previous->id;
1389 current->position1 = get_ilist();
1390 current->position1->i = i;
1391 current->rule = P_RULE_FLIP;
1392 current->c = cl_copy(previous->c);
1393 for (l2=current->c->first_lit, j=1; j<i; l2=l2->next_lit, j++);
1394 t = l2->atom->farg->argval;
1395 l2->atom->farg->argval = l2->atom->farg->narg->argval;
1396 l2->atom->farg->narg->argval = t;
1397 }
1398 }
1399 cl_del_non(copy);
1400 }
1401 #endif
1402
1403 while (rest_of_history) {
1404 switch (rest_of_history->i) {
1405
1406 case UNIT_DEL_RULE:
1407 rest_of_history = rest_of_history->next;
1408 while (rest_of_history && rest_of_history->i > 0) {
1409 pn = retrieve_from_gen_tab(New_proof_old_id_tab,
1410 rest_of_history->i);
1411 rc = translate_unit_deletion(current, pn, new_proof);
1412 current = new_proof->last;
1413 rest_of_history = rest_of_history->next;
1414 }
1415 break;
1416
1417 case FACTOR_SIMP_RULE:
1418 rc = translate_factor_simp(current, new_proof);
1419 current = new_proof->last;
1420 rest_of_history = rest_of_history->next;
1421 break;
1422
1423 case FLIP_EQ_RULE:
1424 /* Handled elsewhere (ORDER_EQ above). */
1425 #ifdef ATTEMPT_FEB_9
1426 /* This is an attempted fix. */
1427 i = rest_of_history->next->next->i;
1428 l1 = ith_literal(current->c, i);
1429 previous = current;
1430 current = connect_new_node(new_proof);
1431 current->parent1 = previous->id;
1432 current->position1 = get_ilist();
1433 current->position1->i = 1;
1434 current->rule = P_RULE_FLIP;
1435 current->c = cl_copy(previous->c);
1436 l2 = ith_literal(current->c, i);
1437 t = l2->atom->farg->argval;
1438 l2->atom->farg->argval = l2->atom->farg->narg->argval;
1439 l2->atom->farg->narg->argval = t;
1440 #endif
1441 /* Move past flip,LIST_RULE-1,n. */
1442 rest_of_history = rest_of_history->next->next->next;
1443 break;
1444
1445 case DEMOD_RULE:
1446 /* There are cases like this:
1447 * [...,demod,...,flip,1,demod,...]
1448 * that arise when equality units are flipped.
1449 * Demodulation is handled at the beginning of this routine,
1450 * so the following should handle things.
1451 */
1452 rc = finish_translating(c, rest_of_history, current, new_proof);
1453 return(rc);
1454
1455 default:
1456 abend("finish_translating, bad rule");
1457 }
1458 }
1459
1460 /* If not ground, renumber variables. */
1461
1462 if (!ground_clause(current->c)) {
1463 struct clause *d;
1464 d = cl_copy(current->c);
1465 rc = renumber_vars(d);
1466 if (!clause_ident(current->c, d)) {
1467 previous = current;
1468 current = connect_new_node(new_proof);
1469 current->rule = P_RULE_INSTANTIATE;
1470 current->parent1 = previous->id;
1471 current->c = cl_copy(previous->c);
1472 renumber_vars_subst(current->c, current->subst);
1473 }
1474 cl_del_non(d);
1475 }
1476
1477 /* Merge identical literals (keep leftmost occurrence). */
1478
1479 while (num_literals(c) < num_literals(current->c)) {
1480 previous = current;
1481 current = connect_new_node(new_proof);
1482 current->parent1 = previous->id;
1483 current->rule = P_RULE_PROPOSITIONAL;
1484 current->c = cl_copy(previous->c);
1485 ok = 0; i = 1;
1486 for (l1 = current->c->first_lit; l1 && !ok; l1 = l1->next_lit, i++) {
1487 prev_lit = l1; j = i+1;
1488 for (l2 = l1->next_lit; l2 && !ok; prev_lit = l2, l2 = l2->next_lit, j++) {
1489 if (l1->sign == l2->sign && term_ident(l1->atom, l2->atom)) {
1490 ok = 1;
1491 prev_lit->next_lit = l2->next_lit;
1492 current->position1 = get_ilist();
1493 current->position1->i = j; /* position of deleted literal */
1494 }
1495 }
1496 }
1497 if (!ok)
1498 abend("finish_translating, merge not found.\n");
1499 }
1500
1501 /* Now we have to match up the original clause and the new one.
1502 * If it's an eq unit, it may be flipped; nonunits should be ok.
1503 */
1504
1505 ip1 = match_clauses(c, current->c);
1506
1507 if (num_literals(current->c) == 1 && check_eq_lit(current->c->first_lit) &&
1508 ip1->i == -1) {
1509 ip1->i = 1;
1510 previous = current;
1511 current = connect_new_node(new_proof);
1512 current->parent1 = previous->id;
1513 current->position1 = get_ilist();
1514 current->position1->i = 1;
1515 current->rule = P_RULE_FLIP;
1516 current->c = cl_copy(previous->c);
1517 l2 = current->c->first_lit;
1518 t = l2->atom->farg->argval;
1519 l2->atom->farg->argval = l2->atom->farg->narg->argval;
1520 l2->atom->farg->narg->argval = t;
1521 }
1522
1523 /* OK, finally we have the final clause corresponding to old clause c. */
1524
1525 current->map = ip1;
1526 current->old_id = c->id;
1527
1528 /* rc = insert_into_gen_tab(New_proof_tab, current->id, current); */
1529 rc = insert_into_gen_tab(New_proof_old_id_tab, c->id, current);
1530
1531 #if 1
1532 /* Sanity check: no other literals flipped, and each subsumes the other.
1533 */
1534 for (ip1 = current->map; ip1; ip1 = ip1->next)
1535 if (ip1->i < 0)
1536 abend("finish_translating, literal flipped");
1537 if (!subsume(c, current->c) || !subsume(current->c, c))
1538 abend("finish_translating, subsumption failure");
1539 #endif
1540
1541 return(1);
1542
1543 } /* finish_translating */
1544
1545 /*************
1546 *
1547 * translate_resolution()
1548 *
1549 *************/
1550
translate_resolution(struct clause * c,struct proof_object * new_proof)1551 static int translate_resolution(struct clause *c,
1552 struct proof_object *new_proof)
1553 {
1554 struct ilist *ip, *ip_save;
1555 struct proof_object_node *par1_node, *par2_node;
1556 int old_index1, old_index2, new_index1, new_index2;
1557 struct literal *new_lit1, *new_lit2;
1558 int i, rc;
1559 struct context *s1, *s2;
1560 struct trail *tr;
1561 struct proof_object_node *par1_instance_node, *par2_instance_node;
1562 struct proof_object_node *resolvent_node;
1563
1564 /* First get info from parent list of clause: */
1565 /* [binary, par1, list-1, lit1, par2, list-1, lit2, ...] */
1566
1567 ip = c->parents->next;
1568 par1_node = retrieve_from_gen_tab(New_proof_old_id_tab, ip->i);
1569 ip = ip->next;
1570 if (ip->i != LIST_RULE-1)
1571 abend("translate_resolution, can't find first list");
1572 ip = ip->next;
1573 old_index1 = ip->i;
1574
1575 ip = ip->next;
1576 par2_node = retrieve_from_gen_tab(New_proof_old_id_tab, ip->i);
1577 ip = ip->next;
1578 if (ip->i != LIST_RULE-1)
1579 abend("translate_resolution, can't find second list");
1580 ip = ip->next;
1581 old_index2 = ip->i;
1582
1583 ip_save = ip->next; /* save place for processing rest of parent list. */
1584
1585 /* Now find the corresp. indexes in the new_parents. */
1586
1587 new_index1 = new_literal_index(par1_node->map, old_index1);
1588 new_index2 = new_literal_index(par2_node->map, old_index2);
1589
1590 /* Get the resolving literals from the new_parents. */
1591
1592 new_lit1 = ith_literal(par1_node->c, new_index1);
1593 new_lit2 = ith_literal(par2_node->c, new_index2);
1594
1595 #ifdef DEBUG
1596 printf("\nBinary resolution: "); p_clause(c);
1597 printf("old_par1=%d, old_index1=%d, par1_node->c=%d, new_index1=%d\n",
1598 par1_node->old_id, old_index1, par1_node->id, new_index1);
1599 printf("old_par2=%d, old_index2=%d, par2_node->c=%d, new_index2=%d\n",
1600 par2_node->old_id, old_index2, par2_node->id, new_index2);
1601 #endif
1602
1603 /* If negative literal is par2, swap par1, par2. */
1604
1605 if (!new_lit2->sign) {
1606 struct literal *temp_lit;
1607 struct proof_object_node *temp_node;
1608
1609 temp_lit = new_lit1; new_lit1 = new_lit2; new_lit2 = temp_lit;
1610 temp_node = par1_node; par1_node = par2_node; par2_node = temp_node;
1611 i = new_index1; new_index1 = new_index2; new_index2 = i;
1612
1613 /* We shouldn't refer to old again, so don't bother to swap them. */
1614 }
1615
1616 if (new_lit1->sign || !new_lit2->sign)
1617 abend("translate_resolution: signs wrong.\n");
1618
1619 /* Unify the atoms. */
1620
1621 s1 = get_context(); s1->multiplier = 0;
1622 s2 = get_context(); s2->multiplier = 1;
1623 tr = NULL;
1624
1625 rc = unify(new_lit1->atom, s1, new_lit2->atom, s2, &tr);
1626 if (!rc) {
1627 p_term(new_lit1->atom);
1628 p_term(new_lit2->atom);
1629 abend("translate_resolution: unify fails on the preceding.\n");
1630 }
1631
1632 /* Buid the instance nodes. */
1633
1634 if (trivial_subst(s1))
1635 par1_instance_node = par1_node;
1636 else {
1637 par1_instance_node = connect_new_node(new_proof);
1638 par1_instance_node->parent1 = par1_node->id;
1639 par1_instance_node->rule = P_RULE_INSTANTIATE;
1640 par1_instance_node->c = apply_clause(par1_node->c, s1);
1641 copy_subst_to_proof_object(s1, par1_instance_node);
1642 }
1643
1644 if (ground_clause(par2_node->c))
1645 par2_instance_node = par2_node;
1646 else {
1647 par2_instance_node = connect_new_node(new_proof);
1648 par2_instance_node->parent1 = par2_node->id;
1649 par2_instance_node->rule = P_RULE_INSTANTIATE;
1650 par2_instance_node->c = apply_clause(par2_node->c, s2);
1651 copy_subst_to_proof_object(s2, par2_instance_node);
1652 }
1653
1654 clear_subst_1(tr); /* clears both substitution tables */
1655 free_context(s1);
1656 free_context(s2);
1657
1658
1659 /* Build the resolvent node. */
1660
1661 resolvent_node = connect_new_node(new_proof);
1662 resolvent_node->rule = P_RULE_RESOLVE;
1663
1664 resolvent_node->parent1 = par1_instance_node->id;
1665 resolvent_node->parent2 = par2_instance_node->id;
1666
1667 ip = get_ilist(); ip->i = new_index1; resolvent_node->position1 = ip;
1668 ip = get_ilist(); ip->i = new_index2; resolvent_node->position2 = ip;
1669
1670 resolvent_node->c = identity_resolve(par1_instance_node->c, new_index1,
1671 par2_instance_node->c, new_index2);
1672
1673 #ifdef DEBUG
1674 p_proof_object_node(par1_instance_node);
1675 p_proof_object_node(par2_instance_node);
1676 p_proof_object_node(resolvent_node);
1677 #endif
1678
1679 rc = finish_translating(c, ip_save, resolvent_node, new_proof);
1680
1681 return(1);
1682 } /* translate_resolution */
1683
1684 /*************
1685 *
1686 * order_new_lits_for_hyper()
1687 *
1688 * Return a permutation of 1--n, where n is the number of negative literals.
1689 * The permutation gives the relative order of negative literals in the
1690 * old clause to those in the new. Example:
1691 *
1692 * new: -q2 -q1 -q3 p1 p2 p3 p4.
1693 * map: 4 2 6 1 3 5 7
1694 *
1695 * return: 2 1 3.
1696 *
1697 *************/
1698
order_new_lits_for_hyper(struct proof_object_node * pn)1699 static struct ilist *order_new_lits_for_hyper(struct proof_object_node *pn)
1700 {
1701 struct ilist *ip1, *ip2, *ip3, *ip4, *ip_min;
1702 struct literal *lit;
1703 int n, i;
1704
1705 ip4 = NULL;
1706 for (lit = pn->c->first_lit, ip3 = pn->map, n = 0;
1707 lit && ip3;
1708 lit = lit->next_lit, ip3 = ip3->next) {
1709 if (!lit->sign) {
1710 n++;
1711 ip2 = get_ilist();
1712 ip2->i = -ip3->i;
1713 if (!ip4)
1714 ip1 = ip2;
1715 else
1716 ip4->next = ip2;
1717 ip4 = ip2;
1718 }
1719 }
1720
1721 for (i = 0; i < n; i++) {
1722 ip_min = NULL;
1723 for (ip2 = ip1; ip2; ip2 = ip2->next)
1724 if (!ip_min || ip2->i < ip_min->i)
1725 ip_min = ip2;
1726 ip_min->i = n-i;
1727 }
1728
1729 #if 0
1730 printf("\nCheck_order: "); p_clause(pn->c);
1731 for (ip2 = ip1; ip2; ip2 = ip2->next)
1732 printf("%d ", ip2->i);
1733 printf("\n\n");
1734 #endif
1735 return(ip1);
1736 } /* order_new_lits_for_hyper */
1737
1738 /*************
1739 *
1740 * translate_hyper()
1741 *
1742 *************/
1743
translate_hyper(struct clause * c,struct proof_object * new_proof)1744 static int translate_hyper(struct clause *c,
1745 struct proof_object *new_proof)
1746 {
1747 struct ilist *ip, *ip1, *ip2, *ip_save;
1748 struct proof_object_node *nuc_node, *sat_node, *result_node;
1749 struct proof_object_node *nuc_i_node, *sat_i_node, *result_i_node; /* instances */
1750 int i, sat_index, nuc_index, rc;
1751 struct literal *nuc_lit, *sat_lit;
1752 struct context *s1, *s2;
1753 struct trail *tr;
1754
1755 s1 = get_context(); s1->multiplier = 0;
1756 s2 = get_context(); s2->multiplier = 1;
1757
1758 /* [hyper, nuc, sat1, -1001, sat1_index, sat2, -1001, sat2_index, ... */
1759
1760 ip = c->parents->next;
1761 nuc_node = retrieve_from_gen_tab(New_proof_old_id_tab, ip->i);
1762 ip_save = ip->next;
1763
1764 for (ip1 = order_new_lits_for_hyper(nuc_node); ip1; ip1 = ip1->next) {
1765 for (ip2 = ip_save, i = 1; i < ip1->i; ip2 = ip2->next->next->next, i++);
1766
1767 sat_node = retrieve_from_gen_tab(New_proof_old_id_tab, ip2->i);
1768 sat_index = new_literal_index(sat_node->map, ip2->next->next->i);
1769 sat_lit = ith_literal(sat_node->c, sat_index);
1770
1771 /* Get index of first negative literal in nuc clause. */
1772
1773 for (nuc_lit = nuc_node->c->first_lit, nuc_index = 1;
1774 nuc_lit->sign;
1775 nuc_lit = nuc_lit->next_lit, nuc_index++);
1776
1777 tr = NULL;
1778
1779 rc = unify(nuc_lit->atom, s1, sat_lit->atom, s2, &tr);
1780 if (nuc_lit->sign == sat_lit->sign || !rc) {
1781 p_term(nuc_lit->atom);
1782 p_term(sat_lit->atom);
1783 abend("translate_hyper: unify fails on the preceding.\n");
1784 }
1785
1786 if (trivial_subst(s1))
1787 nuc_i_node = nuc_node;
1788 else {
1789 nuc_i_node = connect_new_node(new_proof);
1790 nuc_i_node->parent1 = nuc_node->id;
1791 nuc_i_node->rule = P_RULE_INSTANTIATE;
1792 nuc_i_node->c = apply_clause(nuc_node->c, s1);
1793 copy_subst_to_proof_object(s1, nuc_i_node);
1794 }
1795 if (ground_clause(sat_node->c))
1796 sat_i_node = sat_node;
1797 else {
1798 sat_i_node = connect_new_node(new_proof);
1799 sat_i_node->parent1 = sat_node->id;
1800 sat_i_node->rule = P_RULE_INSTANTIATE;
1801 sat_i_node->c = apply_clause(sat_node->c, s2);
1802 copy_subst_to_proof_object(s2, sat_i_node);
1803 }
1804 clear_subst_1(tr); /* clears both substitution tables */
1805
1806 /* Build the resolvent node. */
1807
1808 result_node = connect_new_node(new_proof);
1809 result_node->rule = P_RULE_RESOLVE;
1810
1811 result_node->parent1 = nuc_i_node->id;
1812 result_node->parent2 = sat_i_node->id;
1813
1814 ip = get_ilist(); ip->i = nuc_index; result_node->position1 = ip;
1815 ip = get_ilist(); ip->i = sat_index; result_node->position2 = ip;
1816
1817 result_node->c = identity_resolve(nuc_i_node->c, nuc_index,
1818 sat_i_node->c, sat_index);
1819
1820 if (ground_clause(result_node->c))
1821 result_i_node = result_node;
1822 else {
1823 struct clause *d;
1824 d = cl_copy(result_node->c);
1825 rc = renumber_vars(d);
1826 if (clause_ident(result_node->c, d))
1827 result_i_node = result_node;
1828 else {
1829 result_i_node = connect_new_node(new_proof);
1830 result_i_node->rule = P_RULE_INSTANTIATE;
1831 result_i_node->parent1 = result_node->id;
1832 result_i_node->c = cl_copy(result_node->c);
1833 renumber_vars_subst(result_i_node->c, result_i_node->subst);
1834 }
1835 cl_del_non(d);
1836 }
1837
1838 nuc_node = result_i_node;
1839 }
1840
1841 free_context(s1);
1842 free_context(s2);
1843
1844 while (ip_save && ip_save->i > 0)
1845 ip_save = ip_save->next->next->next;
1846
1847 rc = finish_translating(c, ip_save, nuc_node, new_proof);
1848
1849 return(1);
1850 } /* translate_hyper */
1851
1852 /*************
1853 *
1854 * ipx()
1855 *
1856 *************/
1857
ipx(struct ilist * ip,int n)1858 int ipx(struct ilist *ip,
1859 int n)
1860 {
1861 int i;
1862 for (i=1; ip && i < n; ip = ip->next, i++);
1863 if (ip)
1864 return(ip->i);
1865 else
1866 return(MAX_INT);
1867 } /* ipx */
1868
1869 /*************
1870 *
1871 * translate_ur()
1872 *
1873 *************/
1874
translate_ur(struct clause * c,struct proof_object * new_proof)1875 static int translate_ur(struct clause *c,
1876 struct proof_object *new_proof)
1877 {
1878 struct ilist *ip, *ip1, *ip2, *ip3, *sat_ids, *sat_map;
1879 struct proof_object_node *nuc_node, *sat_node, *result_node;
1880 struct proof_object_node *nuc_i_node, *sat_i_node, *result_i_node; /* instances */
1881 int box_pos, rc, i, skip_first, nuc_index;
1882 struct literal *nuc_lit, *sat_lit;
1883 struct context *s1, *s2;
1884 struct trail *tr;
1885
1886 s1 = get_context(); s1->multiplier = 0;
1887 s2 = get_context(); s2->multiplier = 1;
1888
1889 /* [ur, nuc, -1001, box_pos, sat1, sat2, sat3, ... */
1890
1891 ip = c->parents->next;
1892 nuc_node = retrieve_from_gen_tab(New_proof_old_id_tab, ip->i);
1893 ip = ip->next->next;
1894 box_pos = ip->i;
1895
1896 /* Get satellite ids from history list. */
1897
1898 ip2 = NULL; i = 0;
1899 for (ip = ip->next; ip && ip->i > 0; ip = ip->next) { /* for each sat. ID */
1900 i++;
1901 if (i == box_pos) { /* insert empty slot */
1902 ip1 = get_ilist();
1903 ip1->i = 0;
1904 if (ip2)
1905 ip2->next = ip1;
1906 else
1907 sat_ids = ip1;
1908 ip2 = ip1;
1909 }
1910 ip1 = get_ilist();
1911 ip1->i = ip->i;
1912 if (ip2)
1913 ip2->next = ip1;
1914 else
1915 sat_ids = ip1;
1916 ip2 = ip1;
1917 }
1918
1919 i++;
1920 if (i == box_pos) { /* insert empty slot */
1921 ip1 = get_ilist();
1922 ip1->i = 0;
1923 if (ip2)
1924 ip2->next = ip1;
1925 else
1926 sat_ids = ip1;
1927 ip2 = ip1;
1928 }
1929
1930 /* Use the map to permute sat_ids so that it matches the new nucleus. */
1931
1932 ip2 = NULL;
1933 for (ip3 = nuc_node->map; ip3; ip3 = ip3->next) {
1934 ip1 = get_ilist();
1935 ip1->i = ipx(sat_ids, ip3->i);
1936 if (ip2)
1937 ip2->next = ip1;
1938 else
1939 sat_map = ip1;
1940 ip2 = ip1;
1941 }
1942
1943 #if 1
1944 printf("\ntranslate_ur: sat_map for box=%d, orig= ", box_pos);
1945 p_clause(c);
1946 for (ip1 = sat_map; ip1; ip1 = ip1->next) printf("%d ", ip1->i);
1947 p_clause(nuc_node->c);
1948 #endif
1949
1950
1951 skip_first = 0;
1952 for (ip1 = sat_map; ip1; ip1 = ip1->next) {
1953 if (ip1->i == 0)
1954 skip_first = 1;
1955 else {
1956
1957 sat_node = retrieve_from_gen_tab(New_proof_old_id_tab, ip1->i);
1958 sat_lit = ith_literal(sat_node->c, 1);
1959
1960 /* Get index of clash literal in nuc clause. */
1961 nuc_index = (skip_first ? 2 : 1);
1962
1963 nuc_lit = ith_literal(nuc_node->c, nuc_index);
1964
1965 tr = NULL;
1966
1967 rc = unify(nuc_lit->atom, s1, sat_lit->atom, s2, &tr);
1968 if (nuc_lit->sign == sat_lit->sign || !rc) {
1969 p_term(nuc_lit->atom);
1970 p_term(sat_lit->atom);
1971 abend("translate_ur: unify fails on the preceding.\n");
1972 }
1973
1974 if (trivial_subst(s1))
1975 nuc_i_node = nuc_node;
1976 else {
1977 nuc_i_node = connect_new_node(new_proof);
1978 nuc_i_node->parent1 = nuc_node->id;
1979 nuc_i_node->rule = P_RULE_INSTANTIATE;
1980 nuc_i_node->c = apply_clause(nuc_node->c, s1);
1981 copy_subst_to_proof_object(s1, nuc_i_node);
1982 }
1983 if (ground_clause(sat_node->c))
1984 sat_i_node = sat_node;
1985 else {
1986 sat_i_node = connect_new_node(new_proof);
1987 sat_i_node->parent1 = sat_node->id;
1988 sat_i_node->rule = P_RULE_INSTANTIATE;
1989 sat_i_node->c = apply_clause(sat_node->c, s2);
1990 copy_subst_to_proof_object(s2, sat_i_node);
1991 }
1992 clear_subst_1(tr); /* clears both substitution tables */
1993
1994 /* Build the resolvent node. */
1995
1996 result_node = connect_new_node(new_proof);
1997 result_node->rule = P_RULE_RESOLVE;
1998
1999 result_node->parent1 = nuc_i_node->id;
2000 result_node->parent2 = sat_i_node->id;
2001
2002 ip2 =get_ilist(); ip2->i =nuc_index; result_node->position1 =ip2;
2003 ip2 =get_ilist(); ip2->i =1; result_node->position2 =ip2;
2004
2005 result_node->c = identity_resolve(nuc_i_node->c, nuc_index,
2006 sat_i_node->c, 1);
2007
2008 if (ground_clause(result_node->c))
2009 result_i_node = result_node;
2010 else {
2011 struct clause *d;
2012 d = cl_copy(result_node->c);
2013 rc = renumber_vars(d);
2014 if (clause_ident(result_node->c, d))
2015 result_i_node = result_node;
2016 else {
2017 result_i_node = connect_new_node(new_proof);
2018 result_i_node->rule = P_RULE_INSTANTIATE;
2019 result_i_node->parent1 = result_node->id;
2020 result_i_node->c = cl_copy(result_node->c);
2021 renumber_vars_subst(result_i_node->c, result_i_node->subst);
2022 }
2023 cl_del_non(d);
2024 }
2025
2026 nuc_node = result_i_node;
2027 }
2028 }
2029
2030 free_context(s1);
2031 free_context(s2);
2032
2033 rc = finish_translating(c, ip, nuc_node, new_proof);
2034
2035 return(1);
2036 } /* translate_ur */
2037
2038 /*************
2039 *
2040 * translate_factor()
2041 *
2042 *************/
2043
translate_factor(struct clause * c,struct proof_object * new_proof)2044 static int translate_factor(struct clause *c,
2045 struct proof_object *new_proof)
2046 {
2047 int i1, i2, j, k1, k2;
2048 struct literal *lit1, *lit2;
2049 struct context *subst;
2050 struct trail *tr;
2051 struct proof_object_node *parent, *instance, *factor;
2052
2053 /* Retrieve the proof object of the parent. */
2054
2055 parent = retrieve_from_gen_tab(New_proof_old_id_tab, c->parents->next->i);
2056
2057 /* Get the literal indexes in the old_parent. */
2058
2059 i1 = c->parents->next->next->next->i;
2060 i2 = c->parents->next->next->next->next->i;
2061
2062 /* Get corresponding indexes in new parent. */
2063
2064 k1 = new_literal_index(parent->map, i1);
2065 k2 = new_literal_index(parent->map, i2);
2066
2067 /* Get new literals. */
2068
2069 lit1 = ith_literal(parent->c, k1);
2070 lit2 = ith_literal(parent->c, k2);
2071
2072 /* Unify the literals. */
2073
2074 subst = get_context(); subst->multiplier = 0;
2075 tr = NULL;
2076 j = unify(lit1->atom, subst, lit2->atom, subst, &tr);
2077 if (!j)
2078 abend("translate_factor, literals don't unify");
2079
2080 /* Build the instance node. */
2081
2082 instance = connect_new_node(new_proof);
2083 instance->rule = P_RULE_INSTANTIATE;
2084 instance->parent1 = parent->id;
2085 instance->c = apply_clause(parent->c, subst);
2086 copy_subst_to_proof_object(subst, instance);
2087
2088 clear_subst_1(tr);
2089 free_context(subst);
2090
2091 /* Build the merge node. */
2092
2093 factor = connect_new_node(new_proof);
2094 factor->rule = P_RULE_PROPOSITIONAL;
2095 factor->parent1 = instance->id;
2096 factor->position1 = get_ilist(); factor->position1->i = k2;
2097 factor->c = cl_copy_delete_literal(instance->c, k2);
2098
2099 j = finish_translating(c, c->parents->next->next->next->next->next,
2100 factor, new_proof);
2101 return(1);
2102
2103 } /* translate_factor */
2104
2105 /*************
2106 *
2107 * para_position()
2108 *
2109 *************/
2110
para_position(struct clause * c,struct ilist * ip)2111 static struct term *para_position(struct clause *c,
2112 struct ilist *ip)
2113 {
2114 struct literal *l;
2115 struct term *t;
2116 struct rel *r;
2117 int i;
2118
2119 l = ith_literal(c, ip->i);
2120 t = l->atom;
2121 for (ip = ip->next; ip; ip = ip->next) {
2122 for (i = 1, r = t->farg; i < ip->i; i++, r = r->narg);
2123 t = r->argval;
2124 }
2125 return(t);
2126 } /* para_position */
2127
2128 /*************
2129 *
2130 * translate_paramod()
2131 *
2132 *************/
2133
translate_paramod(struct clause * c,struct proof_object * new_proof)2134 static int translate_paramod(struct clause *c,
2135 struct proof_object *new_proof)
2136 {
2137 struct ilist *ip, *ip_save, *from_pos, *into_pos;
2138 struct proof_object_node *from_node, *into_node;
2139 int i, rc, n, para_from;
2140 struct context *s1, *s2;
2141 struct trail *tr;
2142 struct proof_object_node *from_instance_node, *into_instance_node;
2143 struct proof_object_node *para_node;
2144 struct term *from_term, *into_term;
2145
2146 /* First get info from parent list of clause: */
2147 /* [rule, par1, list-1, pos1,..., par2, list-1, pos2,..., rest */
2148
2149 para_from = (c->parents->i == PARA_FROM_RULE);
2150
2151 ip = c->parents->next;
2152 if (para_from)
2153 from_node = retrieve_from_gen_tab(New_proof_old_id_tab, ip->i);
2154 else
2155 into_node = retrieve_from_gen_tab(New_proof_old_id_tab, ip->i);
2156 ip = ip->next;
2157 if (ip->i >= LIST_RULE)
2158 abend("translate_paramod, can't find first list");
2159 n = LIST_RULE - ip->i; /* length of position vector */
2160 ip = ip->next;
2161 if (para_from)
2162 from_pos = copy_ilist_segment(ip, n);
2163 else
2164 into_pos = copy_ilist_segment(ip, n);
2165 for (i = 0; i < n; i++, ip = ip->next);
2166
2167 if (para_from)
2168 into_node = retrieve_from_gen_tab(New_proof_old_id_tab, ip->i);
2169 else
2170 from_node = retrieve_from_gen_tab(New_proof_old_id_tab, ip->i);
2171 ip = ip->next;
2172 if (ip->i >= LIST_RULE)
2173 abend("translate_paramod, can't find second list");
2174 n = LIST_RULE - ip->i; /* length of position vector */
2175 ip = ip->next;
2176 if (para_from)
2177 into_pos = copy_ilist_segment(ip, n);
2178 else
2179 from_pos = copy_ilist_segment(ip, n);
2180 for (i = 0; i < n; i++, ip = ip->next);
2181
2182 ip_save = ip; /* save place for processing rest of parent list. */
2183
2184 /* Now modify the positions so that they corresp. to the new clauses.
2185 * Must translate literal index. (Eq literals should be in same direction.)
2186 * Same for both from and into.
2187 */
2188
2189 from_pos->i = new_literal_index(from_node->map, from_pos->i);
2190
2191 into_pos->i = new_literal_index(into_node->map, into_pos->i);
2192
2193 /* Get the unifying terms from the new_parents. */
2194
2195 from_term = para_position(from_node->c, from_pos);
2196 into_term = para_position(into_node->c, into_pos);
2197
2198 #ifdef DEBUG
2199 printf("\nParamodulation: "); p_clause(c);
2200 #endif
2201
2202 /* Unify the terms. */
2203
2204 s1 = get_context(); s1->multiplier = 0;
2205 s2 = get_context(); s2->multiplier = 1;
2206 tr = NULL;
2207
2208 rc = unify(from_term, s1, into_term, s2, &tr);
2209 if (!rc) {
2210 p_term(from_term);
2211 p_term(into_term);
2212 abend("translate_paramod: unify fails on the preceding.\n");
2213 }
2214
2215 /* Buid the instance nodes. */
2216
2217 if (trivial_subst(s1))
2218 from_instance_node = from_node;
2219 else {
2220 from_instance_node = connect_new_node(new_proof);
2221 from_instance_node->parent1 = from_node->id;
2222 from_instance_node->rule = P_RULE_INSTANTIATE;
2223 from_instance_node->c = apply_clause(from_node->c, s1);
2224 copy_subst_to_proof_object(s1, from_instance_node);
2225 }
2226
2227 if (ground_clause(into_node->c))
2228 into_instance_node = into_node;
2229 else {
2230 into_instance_node = connect_new_node(new_proof);
2231 into_instance_node->parent1 = into_node->id;
2232 into_instance_node->rule = P_RULE_INSTANTIATE;
2233 into_instance_node->c = apply_clause(into_node->c, s2);
2234 copy_subst_to_proof_object(s2, into_instance_node);
2235 }
2236
2237 clear_subst_1(tr); /* clears both substitution tables */
2238 free_context(s1);
2239 free_context(s2);
2240
2241 /* Build the para node. */
2242
2243 para_node = connect_new_node(new_proof);
2244 para_node->rule = P_RULE_PARAMOD;
2245
2246 para_node->parent1 = from_instance_node->id;
2247 para_node->parent2 = into_instance_node->id;
2248
2249 para_node->position1 = from_pos;
2250 para_node->position2 = into_pos;
2251
2252 para_node->c = identity_paramod(from_instance_node->c, from_pos,
2253 into_instance_node->c, into_pos);
2254
2255 /* If into literal is negated, must add element to position.
2256 * Note that the position vector will no longer be valid for Otter terms.
2257 */
2258
2259 if (ith_literal(into_node->c, into_pos->i)->sign == 0) {
2260 ip = get_ilist();
2261 ip->i = 1;
2262 ip->next = into_pos->next;
2263 into_pos->next = ip;
2264 }
2265
2266 #ifdef DEBUG
2267 p_proof_object_node(from_instance_node);
2268 p_proof_object_node(into_instance_node);
2269 p_proof_object_node(para_node);
2270 #endif
2271
2272 rc = finish_translating(c, ip_save, para_node, new_proof);
2273
2274 return(1);
2275 } /* translate_paramod */
2276
2277 /************************************************************/
2278
varmap(struct term * t,struct term ** vars)2279 static void varmap(struct term *t,
2280 struct term **vars)
2281 {
2282 if (t->type == VARIABLE)
2283 vars[t->varnum] = t;
2284 else if (t->type == COMPLEX) {
2285 struct rel *r;
2286 for (r = t->farg; r; r = r->narg)
2287 varmap(r->argval, vars);
2288 }
2289 } /* varmap */
2290
2291 /************************************************************/
2292
match2(struct clause * c1,struct clause * c2,struct term ** vars)2293 static BOOLEAN match2(struct clause *c1,
2294 struct clause *c2,
2295 struct term **vars)
2296 {
2297 int ok;
2298 struct literal *l1, *l2;
2299
2300 /* For variables, term_ident does not check sym_num field.
2301 So, we first check if the clauses are identical, then,
2302 get the "substitution".
2303 */
2304
2305 for (l1 = c1->first_lit, l2 = c2->first_lit, ok = 1;
2306 l1 && l2 && ok;
2307 l1 = l1->next_lit, l2 = l2->next_lit) {
2308 if (l1->sign != l2->sign)
2309 ok = 0;
2310 else
2311 ok = term_ident(l1->atom, l2->atom);
2312 }
2313 if (!ok || l1 || l2)
2314 return 0;
2315 else {
2316 int i;
2317 for (i = 0; i < MAX_VARS; i++)
2318 vars[i] = NULL;
2319 for (l1 = c1->first_lit; l1; l1 = l1->next_lit)
2320 varmap(l1->atom, vars);
2321 return 1;
2322 }
2323 } /* match2 */
2324
2325 /************************************************************/
2326
find_match2(struct clause * c,struct proof_object * obj,struct term ** vars)2327 struct proof_object_node *find_match2(struct clause *c,
2328 struct proof_object *obj,
2329 struct term **vars)
2330 {
2331 struct proof_object_node *pn = obj->first;
2332 while (pn && pn->rule == P_RULE_INPUT && !match2(pn->c, c, vars))
2333 pn = pn->next;
2334 return (pn && pn->rule == P_RULE_INPUT ? pn : NULL);
2335 } /* find_match2 */
2336
2337 /************************************************************/
2338
2339 /*************
2340 *
2341 * translate_step()
2342 *
2343 * Translate one step in an Otter proof into a sequene of detailed steps
2344 * and add them to New_proof.
2345 *
2346 * return (ok ? 1 : 0)
2347 *
2348 *************/
2349
translate_step(struct clause * c,struct proof_object * new_proof)2350 static int translate_step(struct clause *c,
2351 struct proof_object *new_proof)
2352 {
2353 int rc, rule, id;
2354 struct proof_object_node *pn;
2355
2356 #ifdef DEBUG
2357 printf("translating: "); p_clause(c);
2358 #endif
2359
2360 if (!c->parents) {
2361 pn = connect_new_node(new_proof);
2362 pn->c = cl_copy(c);
2363 pn->old_id = c->id;
2364 pn->map = match_clauses(c, pn->c); /* wasteful, but convenient */
2365 rc = insert_into_gen_tab(New_proof_old_id_tab, c->id, pn);
2366
2367 if (!retrieve_initial_proof_object()) {
2368 pn->rule = P_RULE_INPUT;
2369 rc = 1;
2370 }
2371 else {
2372 struct term *vars[MAX_VARS];
2373 struct proof_object_node *initial_step;
2374 initial_step = find_match2(c, new_proof, vars);
2375 if (!initial_step)
2376 abend("translate_step, clauses don't match");
2377 else {
2378 int i;
2379 pn->rule = P_RULE_INSTANTIATE;
2380 pn->parent1 = initial_step->id;
2381 for (i = 0; i < MAX_VARS; i++)
2382 pn->subst[i] = vars[i];
2383 pn->backward_subst = TRUE;
2384 }
2385 }
2386 }
2387 else if (c->parents->i == COPY_RULE &&
2388 c->parents->next->next->i == PROPOSITIONAL_RULE) {
2389 /* special case */
2390 struct proof_object_node *prop_node;
2391 id = c->parents->next->i;
2392 pn = retrieve_from_gen_tab(New_proof_old_id_tab, id);
2393 prop_node = connect_new_node(new_proof);
2394 prop_node->parent1 = pn->id;
2395 prop_node->c = cl_copy(c);
2396 prop_node->rule = P_RULE_PROPOSITIONAL;
2397 prop_node->old_id = c->id;
2398 prop_node->map = match_clauses(c, prop_node->c);
2399 rc = insert_into_gen_tab(New_proof_old_id_tab,c->id,prop_node);
2400 }
2401 else {
2402 rule = c->parents->i;
2403 switch (rule) {
2404 case NEW_DEMOD_RULE :
2405 /*
2406 * This is kludgey. The proof object doesn't have separate
2407 * steps for NEW_DEMOD, so we just refer to the regular copy.
2408 * This means that the old_id field is not quite correct.
2409 * Recall that new_demod has old_id 1 greater than its parent.
2410 */
2411 id = c->parents->next->i; /* ID of regular copy */
2412 pn = retrieve_from_gen_tab(New_proof_old_id_tab, id);
2413 rc = insert_into_gen_tab(New_proof_old_id_tab, c->id, pn);
2414 break;
2415 case COPY_RULE :
2416 id = c->parents->next->i;
2417 pn = retrieve_from_gen_tab(New_proof_old_id_tab, id);
2418 rc = finish_translating(c, c->parents->next->next,
2419 pn, new_proof);
2420 break;
2421 case BINARY_RES_RULE :
2422 case BACK_UNIT_DEL_RULE :
2423 rc = translate_resolution(c, new_proof);
2424 break;
2425 case HYPER_RES_RULE :
2426 rc = translate_hyper(c, new_proof);
2427 break;
2428 case UR_RES_RULE :
2429 rc = translate_ur(c, new_proof);
2430 break;
2431 case FACTOR_RULE :
2432 rc = translate_factor(c, new_proof);
2433 break;
2434 case PARA_INTO_RULE :
2435 case PARA_FROM_RULE :
2436 rc = translate_paramod(c, new_proof);
2437 break;
2438 case BACK_DEMOD_RULE :
2439 id = c->parents->next->i;
2440 pn = retrieve_from_gen_tab(New_proof_old_id_tab, id);
2441 rc = finish_translating(c, c->parents->next->next,
2442 pn, new_proof);
2443 break;
2444
2445 default :
2446 fprintf(stderr, "translate_step: rule %d not handled.\n", rule);
2447 rc = 0;
2448 break;
2449 }
2450 }
2451 return(rc);
2452 } /* translate_step */
2453
2454 /*************
2455 *
2456 * contains_answer_literal()
2457 *
2458 *************/
2459
contains_answer_literal(struct clause * c)2460 int contains_answer_literal(struct clause *c)
2461 {
2462 struct literal *lit;
2463 for (lit = c->first_lit; lit; lit = lit->next_lit)
2464 if (answer_lit(lit))
2465 return(1);
2466 return(0);
2467 } /* contains_answer_literal */
2468
2469 /*************
2470 *
2471 * contains_rule()
2472 *
2473 *************/
2474
contains_rule(struct clause * c,int rule)2475 int contains_rule(struct clause *c,
2476 int rule)
2477 {
2478 struct ilist *ip;
2479
2480 for (ip = c->parents; ip; ip = ip->next)
2481 if (ip->i == rule)
2482 return(1);
2483 return(0);
2484 } /* contains_rule */
2485
2486 /*************
2487 *
2488 * trans_2_pos()
2489 *
2490 *************/
2491
trans_2_pos(int id,struct ilist * pos)2492 struct ilist *trans_2_pos(int id,
2493 struct ilist *pos)
2494 {
2495 int n, i;
2496 struct clause *c;
2497 struct proof_object_node *pn;
2498 struct ilist *new, *p1;
2499
2500 if (pos == NULL)
2501 abend("trans_2_pos: NULL pos");
2502 pn = retrieve_from_gen_tab(New_proof_tab, id);
2503 if (pn == NULL)
2504 abend("trans_2_pos: proof node not found");
2505 c = pn->c;
2506 if (c == NULL)
2507 abend("trans_2_pos: clause not found");
2508 if (num_literals(c) == 0)
2509 abend("trans_2_pos: empty clause");
2510
2511 n = num_literals(c);
2512 new = copy_ilist(pos->next); /* copy all but first */
2513 if (pos->i != n) {
2514 p1 = get_ilist();
2515 p1->i = 1;
2516 p1->next = new;
2517 new = p1;
2518 }
2519 for (i = 2; i <= pos->i; i++) {
2520 p1 = get_ilist();
2521 p1->i = 2;
2522 p1->next = new;
2523 new = p1;
2524 }
2525 return new;
2526 } /* trans_2_pos */
2527
2528 /*************
2529 *
2530 * type_2_trans()
2531 *
2532 * Change the given proof object from type 1 to a type 2 by
2533 * changing the position vectors in the justifications.
2534 *
2535 *************/
2536
type_2_trans(struct proof_object * po)2537 void type_2_trans(struct proof_object *po)
2538 {
2539 struct proof_object_node *pn;
2540 struct ilist *ip;
2541 for (pn = po->first; pn; pn = pn->next) {
2542 if (pn->parent1 != 0 && pn->position1) {
2543 ip = trans_2_pos(pn->parent1, pn->position1);
2544 free_ilist_list(pn->position1);
2545 pn->position1 = ip;
2546 }
2547 if (pn->parent2 != 0 && pn->position2) {
2548 ip = trans_2_pos(pn->parent2, pn->position2);
2549 free_ilist_list(pn->position2);
2550 pn->position2 = ip;
2551 }
2552 }
2553 } /* type_2_trans */
2554
2555 /*************
2556 *
2557 * glist_subsume(c, g)
2558 *
2559 *************/
2560
glist_subsume(struct clause * c,struct glist * g)2561 int glist_subsume(struct clause *c, struct glist *g)
2562 {
2563 if (g == NULL)
2564 return 0;
2565 else if (subsume(g->v, c))
2566 return 1;
2567 else
2568 return (glist_subsume(c, g->next));
2569 } /* glist_subsume */
2570
2571 /*************
2572 *
2573 * p_proof_object_as_hints()
2574 *
2575 *************/
2576
p_proof_object_as_hints(struct proof_object * po)2577 void p_proof_object_as_hints(struct proof_object *po)
2578 {
2579 struct proof_object_node *pn;
2580 struct glist *h = NULL;
2581 struct glist *p;
2582
2583 for (pn = po->first; pn; pn = pn->next) {
2584 struct clause *d = cl_copy(pn->c);
2585
2586 if (Flags[ORDER_EQ].val) {
2587 if (Flags[LRPO].val)
2588 order_equalities_lrpo(d);
2589 else
2590 order_equalities(d);
2591 }
2592 renumber_vars(d);
2593 if (!glist_subsume(d, h)) {
2594 h = glist_tack_on(h, d);
2595 }
2596 else
2597 cl_del_non(d);
2598 }
2599 printf("list(%s). %% Hints from process %d, %s",
2600 Internal_flags[HINTS2_PRESENT] ? "hints2" : "hints",
2601 my_process_id(), get_time());
2602 for (p = h; p != NULL; p = p->next) {
2603 print_clause_bare(stdout, p->v); printf(".\n");
2604 cl_del_non(p->v);
2605 }
2606 printf("end_of_list.\n");
2607 free_glist_list(h);
2608 } /* p_proof_object_as_hints */
2609
2610 /*************
2611 *
2612 * remove_answer_literals()
2613 *
2614 *************/
2615
remove_answer_literals(struct literal * lit)2616 struct literal *remove_answer_literals(struct literal *lit)
2617 {
2618 if (lit == NULL)
2619 return NULL;
2620 else if (answer_lit(lit)) {
2621 struct literal *lit2 = lit->next_lit;
2622 lit->atom->occ.lit = NULL;
2623 zap_term(lit->atom);
2624 free_literal(lit);
2625 return remove_answer_literals(lit2);
2626 }
2627 else {
2628 lit->next_lit = remove_answer_literals(lit->next_lit);
2629 return lit;
2630 }
2631 } /* remove_answer_literals */
2632
2633 /*************
2634 *
2635 * build_proof_object()
2636 *
2637 * Given a clause (not necessarily empty), build and print the proof
2638 * object corresponding to the clause.
2639 *
2640 *************/
2641
build_proof_object(struct clause * c)2642 void build_proof_object(struct clause *c)
2643 {
2644 struct clause_ptr *cp1, *cp2;
2645 struct ilist *ip1;
2646 int level, i, rc;
2647 struct clause *d;
2648 struct proof_object *new_proof;
2649
2650 if (!Flags[ORDER_HISTORY].val)
2651 abend("build_proof_object: flag order_history must be set");
2652 else if (!Flags[DETAILED_HISTORY].val)
2653 abend("build_proof_object: flag detailed_history must be set");
2654
2655 cp1 = NULL;
2656 level = get_ancestors(c, &cp1, &ip1);
2657
2658 for (cp2 = cp1; cp2; cp2 = cp2->next) {
2659 if (contains_answer_literal(cp2->c)) {
2660 /* Copy the clause and remove answer literals.
2661 * We won't worry about freeing this copy when we're done.
2662 * This small memory leak shouldn't make much difference.
2663 */
2664 struct clause *c = cl_copy(cp2->c);
2665 c->parents = copy_ilist(cp2->c->parents);
2666 c->id = cp2->c->id;
2667 c->first_lit = remove_answer_literals(c->first_lit);
2668 cp2->c = c;
2669 }
2670 }
2671
2672 for (cp2 = cp1; cp2; cp2 = cp2->next) {
2673 if (contains_answer_literal(cp2->c))
2674 abend("build_proof_object: proof objects cannot contain answer literals");
2675 else if (contains_rule(cp2->c, NEG_HYPER_RES_RULE))
2676 abend("build_proof_object: neg_hyper_res not allowed");
2677 else if (contains_rule(cp2->c, GEO_RULE))
2678 abend("build_proof_object: gL rule not allowed");
2679 else if (contains_rule(cp2->c, GEO_ID_RULE))
2680 abend("build_proof_object: gL-id not allowed");
2681 else if (contains_rule(cp2->c, LINKED_UR_RES_RULE))
2682 abend("build_proof_object: linked_ur_res not allowed");
2683 else if (contains_rule(cp2->c, EVAL_RULE))
2684 abend("build_proof_object: eval rule not allowed");
2685 else if (contains_rule(cp2->c, CLAUSIFY_RULE))
2686 abend("build_proof_object: clausify rule not allowed");
2687 }
2688
2689 /* Old_proof_tab has the original clauses, indexed by their own IDs.
2690 New_proof_old_id_tab has proof nodes, indexed by original IDs.
2691 New_proof_tab has proof nodes, indexed by their own IDs.
2692 */
2693
2694 new_proof = retrieve_initial_proof_object();
2695
2696 /* If an intial proof object already exists, then New_proof_tab
2697 already exists also (it was built at the same time). Unfortunately,
2698 we have a problem if there is an initial proof object and this
2699 is the second call to build_proof object: New_proof_tab has
2700 been changed, so we cannot use it as we start building from
2701 the initial proof object. Therefore, we allow at most one proof
2702 when we are using initial proof objects. See abend below.
2703 (I think this can be fixed by keeping a copy of New_proof_tab
2704 when the initial proof object is created.
2705 */
2706
2707 /* If we don't have an initial proof object, start a new one. */
2708
2709 if (new_proof == NULL) {
2710 new_proof = get_proof_object();
2711 New_proof_tab = init_gen_tab();
2712 }
2713 else {
2714 if (Old_proof_tab != NULL)
2715 abend("build_proof_object, at most one proof object can be built when an initial proof object is given");
2716 }
2717 Old_proof_tab = init_gen_tab();
2718 New_proof_old_id_tab = init_gen_tab();
2719
2720 for (cp2 = cp1; cp2; cp2 = cp2->next) {
2721 i = insert_into_gen_tab(Old_proof_tab, cp2->c->id, cp2->c);
2722 }
2723
2724 for (cp2 = cp1, rc = 1; cp2 && rc; cp2 = cp2->next) {
2725 d = (struct clause *) retrieve_from_gen_tab(Old_proof_tab, cp2->c->id);
2726 rc = translate_step(cp2->c, new_proof);
2727 }
2728
2729 if (Flags[PRINT_PROOF_AS_HINTS].val)
2730 p_proof_object_as_hints(new_proof);
2731 else {
2732 if (Flags[BUILD_PROOF_OBJECT_2].val)
2733 type_2_trans(new_proof); /* translate to type 2 proof object */
2734 printf("\n;; BEGINNING OF PROOF OBJECT\n");
2735 p_proof_object(new_proof);
2736 printf(";; END OF PROOF OBJECT\n");
2737 }
2738 } /* build_proof_object */
2739
2740 /************************************************************/
2741
init_proof_object_environment(void)2742 void init_proof_object_environment(void)
2743 {
2744 New_proof_tab = init_gen_tab();
2745 }
2746
2747