1 /*************************************************************************
2 * *
3 * YAP Prolog *
4 * *
5 * Yap Prolog was developed at NCCUP - Universidade do Porto *
6 * *
7 * Copyright L.Damas, V.S.Costa and Universidade do Porto 1985-1997 *
8 * *
9 **************************************************************************
10 * *
11 * File: unify.c *
12 * Last rev: *
13 * mods: *
14 * comments: Unification and other auxiliary routines for absmi *
15 * *
16 *************************************************************************/
17 #define IN_UNIFY_C 1
18
19 #include "absmi.h"
20
21 STD_PROTO(int Yap_rational_tree_loop, (CELL *, CELL *, CELL **, CELL **));
22
23 STATIC_PROTO(int OCUnify_complex, (CELL *, CELL *, CELL *));
24 STATIC_PROTO(int OCUnify, (register CELL, register CELL));
25 STATIC_PROTO(Int p_ocunify, (void));
26 #ifdef THREADED_CODE
27 STATIC_PROTO(int rtable_hash_op, (OPCODE));
28 STATIC_PROTO(void InitReverseLookupOpcode, (void));
29 #endif
30
31 /* support for rational trees and unification with occur checking */
32
33 #define to_visit_base ((struct v_record *)AuxSp)
34
35 int
Yap_rational_tree_loop(CELL * pt0,CELL * pt0_end,CELL ** to_visit,CELL ** to_visit_max)36 Yap_rational_tree_loop(CELL *pt0, CELL *pt0_end, CELL **to_visit, CELL **to_visit_max)
37 {
38
39 CELL ** base = to_visit;
40 rtree_loop:
41 while (pt0 < pt0_end) {
42 register CELL *ptd0;
43 register CELL d0;
44
45 ptd0 = ++pt0;
46 pt0 = ptd0;
47 d0 = *ptd0;
48 deref_head(d0, rtree_loop_unk);
49 rtree_loop_nvar:
50 {
51 if (d0 == TermFoundVar)
52 goto cufail;
53 if (IsPairTerm(d0)) {
54 to_visit -= 3;
55 if (to_visit < to_visit_max) {
56 to_visit = Yap_shift_visit(to_visit, &to_visit_max);
57 }
58 to_visit[0] = pt0;
59 to_visit[1] = pt0_end;
60 to_visit[2] = (CELL *)*pt0;
61 *pt0 = TermFoundVar;
62 pt0_end = (pt0 = RepPair(d0) - 1) + 2;
63 continue;
64 }
65 if (IsApplTerm(d0)) {
66 register Functor f;
67 register CELL *ap2;
68
69 /* store the terms to visit */
70 ap2 = RepAppl(d0);
71 f = (Functor) (*ap2);
72 /* compare functors */
73 if (IsExtensionFunctor(f)) {
74 continue;
75 }
76 to_visit -= 3;
77 if (to_visit < to_visit_max) {
78 to_visit = Yap_shift_visit(to_visit, &to_visit_max);
79 }
80 to_visit[0] = pt0;
81 to_visit[1] = pt0_end;
82 to_visit[2] = (CELL *)*pt0;
83 *pt0 = TermFoundVar;
84 d0 = ArityOfFunctor(f);
85 pt0 = ap2;
86 pt0_end = ap2 + d0;
87 continue;
88 }
89 continue;
90 }
91
92 derefa_body(d0, ptd0, rtree_loop_unk, rtree_loop_nvar);
93 }
94 /* Do we still have compound terms to visit */
95 if (to_visit < base) {
96 pt0 = to_visit[0];
97 pt0_end = to_visit[1];
98 *pt0 = (CELL)to_visit[2];
99 to_visit += 3;
100 goto rtree_loop;
101 }
102 return FALSE;
103
104 cufail:
105 /* we found an infinite term */
106 while (to_visit < (CELL **)base) {
107 CELL *pt0;
108 pt0 = to_visit[0];
109 *pt0 = (CELL)to_visit[2];
110 to_visit += 3;
111 }
112 return TRUE;
113 }
114
115 static inline int
rational_tree(Term d0)116 rational_tree(Term d0) {
117 CELL **to_visit_max = (CELL **)AuxBase, **to_visit = (CELL **)AuxSp;
118
119 if (IsPairTerm(d0)) {
120 CELL *pt0 = RepPair(d0);
121
122 return Yap_rational_tree_loop(pt0-1, pt0+1, to_visit, to_visit_max);
123 } else if (IsApplTerm(d0)) {
124 CELL *pt0 = RepAppl(d0);
125 Functor f = (Functor)(*pt0);
126
127 if (IsExtensionFunctor(f))
128 return FALSE;
129 return Yap_rational_tree_loop(pt0, pt0+ArityOfFunctor(f), to_visit, to_visit_max);
130 } else
131 return FALSE;
132 }
133
134 static int
OCUnify_complex(CELL * pt0,CELL * pt0_end,CELL * pt1)135 OCUnify_complex(CELL *pt0, CELL *pt0_end, CELL *pt1)
136 {
137 #ifdef THREADS
138 #undef Yap_REGS
139 register REGSTORE *regp = Yap_regp;
140 #define Yap_REGS (*regp)
141 #elif defined(SHADOW_REGS)
142 #if defined(B) || defined(TR)
143 register REGSTORE *regp = &Yap_REGS;
144
145 #define Yap_REGS (*regp)
146 #endif /* defined(B) || defined(TR) || defined(HB) */
147 #endif
148
149 #ifdef SHADOW_HB
150 register CELL *HBREG = HB;
151 #endif /* SHADOW_HB */
152
153 struct unif_record *unif = (struct unif_record *)AuxBase;
154 struct v_record *to_visit = (struct v_record *)AuxSp;
155 #define unif_base ((struct unif_record *)AuxBase)
156
157 loop:
158 while (pt0 < pt0_end) {
159 register CELL *ptd0 = pt0+1;
160 register CELL d0;
161
162 ++pt1;
163 pt0 = ptd0;
164 d0 = *ptd0;
165 deref_head(d0, unify_comp_unk);
166 unify_comp_nvar:
167 {
168 register CELL *ptd1 = pt1;
169 register CELL d1 = *ptd1;
170
171 deref_head(d1, unify_comp_nvar_unk);
172 unify_comp_nvar_nvar:
173 if (d0 == d1) {
174 if (Yap_rational_tree_loop(pt0-1, pt0, (CELL **)to_visit, (CELL **)unif))
175 goto cufail;
176 continue;
177 }
178 if (IsPairTerm(d0)) {
179 if (!IsPairTerm(d1)) {
180 goto cufail;
181 }
182 /* now link the two structures so that no one else will */
183 /* come here */
184 /* store the terms to visit */
185 if (RATIONAL_TREES || pt0 < pt0_end) {
186 to_visit --;
187 #ifdef RATIONAL_TREES
188 unif++;
189 #endif
190 if ((void *)to_visit < (void *)unif) {
191 CELL **urec = (CELL **)unif;
192 to_visit = (struct v_record *)Yap_shift_visit((CELL **)to_visit, &urec);
193 unif = (struct unif_record *)urec;
194 }
195 to_visit->start0 = pt0;
196 to_visit->end0 = pt0_end;
197 to_visit->start1 = pt1;
198 #ifdef RATIONAL_TREES
199 unif[-1].old = *pt0;
200 unif[-1].ptr = pt0;
201 *pt0 = d1;
202 #endif
203 }
204 pt0_end = (pt0 = RepPair(d0) - 1) + 2;
205 pt1 = RepPair(d1) - 1;
206 continue;
207 }
208 if (IsApplTerm(d0)) {
209 register Functor f;
210 register CELL *ap2, *ap3;
211
212 if (!IsApplTerm(d1)) {
213 goto cufail;
214 }
215 /* store the terms to visit */
216 ap2 = RepAppl(d0);
217 ap3 = RepAppl(d1);
218 f = (Functor) (*ap2);
219 /* compare functors */
220 if (f != (Functor) *ap3)
221 goto cufail;
222 if (IsExtensionFunctor(f)) {
223 if (unify_extension(f, d0, ap2, d1))
224 continue;
225 goto cufail;
226 }
227 /* now link the two structures so that no one else will */
228 /* come here */
229 /* store the terms to visit */
230 if (RATIONAL_TREES || pt0 < pt0_end) {
231 to_visit --;
232 #ifdef RATIONAL_TREES
233 unif++;
234 #endif
235 if ((void *)to_visit < (void *)unif) {
236 CELL **urec = (CELL **)unif;
237 to_visit = (struct v_record *)Yap_shift_visit((CELL **)to_visit, &urec);
238 unif = (struct unif_record *)urec;
239 }
240 to_visit->start0 = pt0;
241 to_visit->end0 = pt0_end;
242 to_visit->start1 = pt1;
243 #ifdef RATIONAL_TREES
244 unif[-1].old = *pt0;
245 unif[-1].ptr = pt0;
246 *pt0 = d1;
247 #endif
248 }
249 d0 = ArityOfFunctor(f);
250 pt0 = ap2;
251 pt0_end = ap2 + d0;
252 pt1 = ap3;
253 continue;
254 }
255 goto cufail;
256
257 derefa_body(d1, ptd1, unify_comp_nvar_unk, unify_comp_nvar_nvar);
258 /* d1 and pt2 have the unbound value, whereas d0 is bound */
259 BIND_GLOBAL(ptd1, d0, bind_ocunify1);
260 #ifdef COROUTINING
261 DO_TRAIL(ptd1, d0);
262 if (IsAttVar(ptd1)) Yap_WakeUp(ptd1);
263 bind_ocunify1:
264 #endif
265 if (Yap_rational_tree_loop(ptd1-1, ptd1, (CELL **)to_visit, (CELL **)unif))
266 goto cufail;
267 continue;
268 }
269
270 derefa_body(d0, ptd0, unify_comp_unk, unify_comp_nvar);
271 /* first arg var */
272 {
273 register CELL d1;
274 register CELL *ptd1;
275
276 ptd1 = pt1;
277 d1 = ptd1[0];
278 /* pt2 is unbound */
279 deref_head(d1, unify_comp_var_unk);
280 unify_comp_var_nvar:
281 /* pt2 is unbound and d1 is bound */
282 BIND_GLOBAL(ptd0, d1, bind_ocunify2);
283 #ifdef COROUTINING
284 DO_TRAIL(ptd0, d1);
285 if (IsAttVar(ptd0)) Yap_WakeUp(ptd0);
286 bind_ocunify2:
287 #endif
288 if (Yap_rational_tree_loop(ptd0-1, ptd0, (CELL **)to_visit, (CELL **)unif))
289 goto cufail;
290 continue;
291
292 derefa_body(d1, ptd1, unify_comp_var_unk, unify_comp_var_nvar);
293 /* ptd0 and ptd1 are unbound */
294 UnifyGlobalCells(ptd0, ptd1);
295 }
296 }
297 /* Do we still have compound terms to visit */
298 if (to_visit < to_visit_base) {
299 pt0 = to_visit->start0;
300 pt0_end = to_visit->end0;
301 pt1 = to_visit->start1;
302 to_visit++;
303 goto loop;
304 }
305 #ifdef RATIONAL_TREES
306 /* restore bindigs */
307 while (unif-- != unif_base) {
308 CELL *pt0;
309
310 pt0 = unif->ptr;
311 *pt0 = unif->old;
312 }
313 #endif
314 return TRUE;
315
316 cufail:
317 #ifdef RATIONAL_TREES
318 /* restore bindigs */
319 while (unif-- != unif_base) {
320 CELL *pt0;
321
322 pt0 = unif->ptr;
323 *pt0 = unif->old;
324 }
325 #endif
326 return FALSE;
327 #ifdef THREADS
328 #undef Yap_REGS
329 #define Yap_REGS (*Yap_regp)
330 #elif defined(SHADOW_REGS)
331 #if defined(B) || defined(TR)
332 #undef Yap_REGS
333 #endif /* defined(B) || defined(TR) */
334 #endif
335 #undef unif_base
336 #undef to_visit_base
337 }
338
339 static int
OCUnify(register CELL d0,register CELL d1)340 OCUnify(register CELL d0, register CELL d1)
341 {
342
343 register CELL *pt0, *pt1;
344
345 #if SHADOW_HB
346 register CELL *HBREG = HB;
347 #endif
348
349 deref_head(d0, oc_unify_unk);
350
351 oc_unify_nvar:
352 /* d0 is bound */
353 deref_head(d1, oc_unify_nvar_unk);
354 oc_unify_nvar_nvar:
355
356 if (d0 == d1) {
357 return (!rational_tree(d0));
358 }
359 /* both arguments are bound */
360 if (IsPairTerm(d0)) {
361 if (!IsPairTerm(d1)) {
362 return (FALSE);
363 }
364 pt0 = RepPair(d0);
365 pt1 = RepPair(d1);
366 return (OCUnify_complex(pt0 - 1, pt0 + 1, pt1 - 1));
367 }
368 else if (IsApplTerm(d0)) {
369 if (!IsApplTerm(d1))
370 return (FALSE);
371 pt0 = RepAppl(d0);
372 d0 = *pt0;
373 pt1 = RepAppl(d1);
374 d1 = *pt1;
375 if (d0 != d1) {
376 return (FALSE);
377 } else {
378 if (IsExtensionFunctor((Functor)d0)) {
379 switch(d0) {
380 case (CELL)FunctorDBRef:
381 return(pt0 == pt1);
382 case (CELL)FunctorLongInt:
383 return(pt0[1] == pt1[1]);
384 case (CELL)FunctorDouble:
385 return(FloatOfTerm(AbsAppl(pt0)) == FloatOfTerm(AbsAppl(pt1)));
386 #ifdef USE_GMP
387 case (CELL)FunctorBigInt:
388 return(Yap_gmp_tcmp_big_big(AbsAppl(pt0),AbsAppl(pt0)) == 0);
389 #endif /* USE_GMP */
390 default:
391 return(FALSE);
392 }
393 }
394 return (OCUnify_complex(pt0, pt0 + ArityOfFunctor((Functor) d0),
395 pt1));
396 }
397 } else {
398 return(FALSE);
399 }
400
401 deref_body(d1, pt1, oc_unify_nvar_unk, oc_unify_nvar_nvar);
402 /* d0 is bound and d1 is unbound */
403 BIND(pt1, d0, bind_ocunify4);
404 #ifdef COROUTINING
405 DO_TRAIL(pt1, d0);
406 if (IsAttVar(pt1)) Yap_WakeUp(pt1);
407 bind_ocunify4:
408 #endif
409 /* local variables cannot be in a term */
410 if (pt1 > H && pt1 < LCL0)
411 return TRUE;
412 if (rational_tree(d0))
413 return(FALSE);
414 return (TRUE);
415
416 deref_body(d0, pt0, oc_unify_unk, oc_unify_nvar);
417 /* pt0 is unbound */
418 deref_head(d1, oc_unify_var_unk);
419 oc_unify_var_nvar:
420 /* pt0 is unbound and d1 is bound */
421 BIND(pt0, d1, bind_ocunify5);
422 #ifdef COROUTINING
423 DO_TRAIL(pt0, d1);
424 if (IsAttVar(pt0)) Yap_WakeUp(pt0);
425 bind_ocunify5:
426 #endif
427 /* local variables cannot be in a term */
428 if (pt0 > H && pt0 < LCL0)
429 return TRUE;
430 if (rational_tree(d1))
431 return(FALSE);
432 return (TRUE);
433
434 deref_body(d1, pt1, oc_unify_var_unk, oc_unify_var_nvar);
435 /* d0 and pt1 are unbound */
436 UnifyCells(pt0, pt1, uc1, uc2);
437 #ifdef COROUTINING
438 DO_TRAIL(pt0, (CELL)pt1);
439 if (IsAttVar(pt0)) Yap_WakeUp(pt0);
440 uc1:
441 #endif
442 return (TRUE);
443 #ifdef COROUTINING
444 uc2:
445 DO_TRAIL(pt1, (CELL)pt0);
446 if (IsAttVar(pt1)) {
447 Yap_WakeUp(pt1);
448 }
449 #endif
450 return (TRUE);
451 }
452
453 static Int
p_ocunify(void)454 p_ocunify(void)
455 {
456 return(OCUnify(ARG1,ARG2));
457 }
458
459 static Int
p_cyclic(void)460 p_cyclic(void)
461 {
462 Term t = Deref(ARG1);
463 if (IsVarTerm(t))
464 return(FALSE);
465 return rational_tree(t);
466 }
467
468 static Int
p_acyclic(void)469 p_acyclic(void)
470 {
471 Term t = Deref(ARG1);
472 if (IsVarTerm(t))
473 return(TRUE);
474 return !rational_tree(t);
475 }
476
477 int
Yap_IUnify(register CELL d0,register CELL d1)478 Yap_IUnify(register CELL d0, register CELL d1)
479 {
480 #if THREADS
481 #undef Yap_REGS
482 register REGSTORE *regp = Yap_regp;
483 #define Yap_REGS (*regp)
484 #elif SHADOW_REGS
485 #if defined(B) || defined(TR)
486 register REGSTORE *regp = &Yap_REGS;
487
488 #define Yap_REGS (*regp)
489 #endif /* defined(B) || defined(TR) */
490 #endif
491
492 #if SHADOW_HB
493 register CELL *HBREG = HB;
494 #endif
495
496 register CELL *pt0, *pt1;
497
498 deref_head(d0, unify_unk);
499
500 unify_nvar:
501 /* d0 is bound */
502 deref_head(d1, unify_nvar_unk);
503 unify_nvar_nvar:
504 /* both arguments are bound */
505 if (d0 == d1)
506 return TRUE;
507 if (IsPairTerm(d0)) {
508 if (!IsPairTerm(d1)) {
509 return (FALSE);
510 }
511 pt0 = RepPair(d0);
512 pt1 = RepPair(d1);
513 return (IUnify_complex(pt0 - 1, pt0 + 1, pt1 - 1));
514 }
515 else if (IsApplTerm(d0)) {
516 pt0 = RepAppl(d0);
517 d0 = *pt0;
518 if (!IsApplTerm(d1))
519 return (FALSE);
520 pt1 = RepAppl(d1);
521 d1 = *pt1;
522 if (d0 != d1) {
523 return (FALSE);
524 } else {
525 if (IsExtensionFunctor((Functor)d0)) {
526 switch(d0) {
527 case (CELL)FunctorDBRef:
528 return(pt0 == pt1);
529 case (CELL)FunctorLongInt:
530 return(pt0[1] == pt1[1]);
531 case (CELL)FunctorDouble:
532 return(FloatOfTerm(AbsAppl(pt0)) == FloatOfTerm(AbsAppl(pt1)));
533 #ifdef USE_GMP
534 case (CELL)FunctorBigInt:
535 return(Yap_gmp_tcmp_big_big(AbsAppl(pt0),AbsAppl(pt0)) == 0);
536 #endif /* USE_GMP */
537 default:
538 return(FALSE);
539 }
540 }
541 return (IUnify_complex(pt0, pt0 + ArityOfFunctor((Functor) d0),
542 pt1));
543 }
544 } else {
545 return (FALSE);
546 }
547
548 deref_body(d1, pt1, unify_nvar_unk, unify_nvar_nvar);
549 /* d0 is bound and d1 is unbound */
550 BIND(pt1, d0, bind_unify3);
551 #ifdef COROUTINING
552 DO_TRAIL(pt1, d0);
553 if (IsAttVar(pt1)) Yap_WakeUp(pt1);
554 bind_unify3:
555 #endif
556 return (TRUE);
557
558 deref_body(d0, pt0, unify_unk, unify_nvar);
559 /* pt0 is unbound */
560 deref_head(d1, unify_var_unk);
561 unify_var_nvar:
562 /* pt0 is unbound and d1 is bound */
563 BIND(pt0, d1, bind_unify4);
564 #ifdef COROUTINING
565 DO_TRAIL(pt0, d1);
566 if (IsAttVar(pt0)) Yap_WakeUp(pt0);
567 bind_unify4:
568 #endif
569 return TRUE;
570
571 #if TRAILING_REQUIRES_BRANCH
572 unify_var_nvar_trail:
573 DO_TRAIL(pt0);
574 return TRUE;
575 #endif
576
577 deref_body(d1, pt1, unify_var_unk, unify_var_nvar);
578 /* d0 and pt1 are unbound */
579 UnifyCells(pt0, pt1, uc1, uc2);
580 #ifdef COROUTINING
581 DO_TRAIL(pt0, (CELL)pt1);
582 if (IsAttVar(pt0)) Yap_WakeUp(pt0);
583 uc1:
584 #endif
585 return (TRUE);
586 #ifdef COROUTINING
587 uc2:
588 DO_TRAIL(pt1, (CELL)pt0);
589 if (IsAttVar(pt1)) {
590 Yap_WakeUp(pt1);
591 }
592 return (TRUE);
593 #endif
594 #if THREADS
595 #undef Yap_REGS
596 #define Yap_REGS (*Yap_regp)
597 #elif SHADOW_REGS
598 #if defined(B) || defined(TR)
599 #undef Yap_REGS
600 #endif /* defined(B) || defined(TR) */
601 #endif
602 }
603
604 /**********************************************************************
605 * *
606 * Conversion from Label to Op *
607 * *
608 **********************************************************************/
609
610 #if USE_THREADED_CODE
611
612 /* mask a hash table that allows for fast reverse translation from
613 instruction address to corresponding opcode */
614 static void
InitReverseLookupOpcode(void)615 InitReverseLookupOpcode(void)
616 {
617 opentry *opeptr;
618 op_numbers i;
619 /* 2 K should be OK */
620 int hash_size_mask = OP_HASH_SIZE-1;
621 UInt sz = OP_HASH_SIZE*sizeof(struct opcode_tab_entry);
622
623 while (OP_RTABLE == NULL) {
624 if ((OP_RTABLE = (opentry *)Yap_AllocCodeSpace(sz)) == NULL) {
625 if (!Yap_growheap(FALSE, sz, NULL)) {
626 Yap_Error(INTERNAL_ERROR, TermNil,
627 "Couldn't obtain space for the reverse translation opcode table");
628 }
629 }
630 }
631 opeptr = OP_RTABLE;
632 /* clear up table */
633 {
634 int j;
635 for (j=0; j<OP_HASH_SIZE; j++) {
636 opeptr[j].opc = 0;
637 opeptr[j].opnum = _Ystop;
638 }
639 }
640 opeptr = OP_RTABLE;
641 opeptr[rtable_hash_op(Yap_opcode(_Ystop),hash_size_mask)].opc
642 = Yap_opcode(_Ystop);
643 /* now place entries */
644 for (i = _std_top; i > _Ystop; i--) {
645 OPCODE opc = Yap_opcode(i);
646 int j = rtable_hash_op(opc,hash_size_mask);
647 while (opeptr[j].opc) {
648 if (++j > hash_size_mask)
649 j = 0;
650 }
651 /* clear entry, no conflict */
652 opeptr[j].opnum = i;
653 opeptr[j].opc = opc;
654 }
655 }
656 #endif
657
658 #define UnifiableGlobalCells(a, b) \
659 if((a) > (b)) { \
660 BIND_GLOBALCELL_NONATT((a),(CELL)(b)); \
661 } else if((a) < (b)){ \
662 BIND_GLOBALCELL_NONATT((b),(CELL) (a)); \
663 }
664
665 static int
unifiable_complex(CELL * pt0,CELL * pt0_end,CELL * pt1)666 unifiable_complex(CELL *pt0, CELL *pt0_end, CELL *pt1)
667 {
668 #ifdef THREADS
669 #undef Yap_REGS
670 register REGSTORE *regp = Yap_regp;
671 #define Yap_REGS (*regp)
672 #elif defined(SHADOW_REGS)
673 #if defined(B) || defined(TR)
674 register REGSTORE *regp = &Yap_REGS;
675
676 #define Yap_REGS (*regp)
677 #endif /* defined(B) || defined(TR) || defined(HB) */
678 #endif
679
680 #ifdef SHADOW_HB
681 register CELL *HBREG = HB;
682 #endif /* SHADOW_HB */
683
684 struct unif_record *unif = (struct unif_record *)AuxBase;
685 struct v_record *to_visit = (struct v_record *)AuxSp;
686 #define unif_base ((struct unif_record *)AuxBase)
687 #define to_visit_base ((struct v_record *)AuxSp)
688
689 loop:
690 while (pt0 < pt0_end) {
691 register CELL *ptd0 = pt0+1;
692 register CELL d0;
693
694 ++pt1;
695 pt0 = ptd0;
696 d0 = *ptd0;
697 deref_head(d0, unifiable_comp_unk);
698 unifiable_comp_nvar:
699 {
700 register CELL *ptd1 = pt1;
701 register CELL d1 = *ptd1;
702
703 deref_head(d1, unifiable_comp_nvar_unk);
704 unifiable_comp_nvar_nvar:
705 if (d0 == d1)
706 continue;
707 if (IsPairTerm(d0)) {
708 if (!IsPairTerm(d1)) {
709 goto cufail;
710 }
711 /* now link the two structures so that no one else will */
712 /* come here */
713 /* store the terms to visit */
714 if (RATIONAL_TREES || pt0 < pt0_end) {
715 to_visit --;
716 #ifdef RATIONAL_TREES
717 unif++;
718 #endif
719 if ((void *)to_visit < (void *)unif) {
720 CELL **urec = (CELL **)unif;
721 to_visit = (struct v_record *)Yap_shift_visit((CELL **)to_visit, &urec);
722 unif = (struct unif_record *)urec;
723 }
724 to_visit->start0 = pt0;
725 to_visit->end0 = pt0_end;
726 to_visit->start1 = pt1;
727 #ifdef RATIONAL_TREES
728 unif[-1].old = *pt0;
729 unif[-1].ptr = pt0;
730 *pt0 = d1;
731 #endif
732 }
733 pt0_end = (pt0 = RepPair(d0) - 1) + 2;
734 pt1 = RepPair(d1) - 1;
735 continue;
736 }
737 if (IsApplTerm(d0)) {
738 register Functor f;
739 register CELL *ap2, *ap3;
740
741 if (!IsApplTerm(d1)) {
742 goto cufail;
743 }
744 /* store the terms to visit */
745 ap2 = RepAppl(d0);
746 ap3 = RepAppl(d1);
747 f = (Functor) (*ap2);
748 /* compare functors */
749 if (f != (Functor) *ap3)
750 goto cufail;
751 if (IsExtensionFunctor(f)) {
752 if (unify_extension(f, d0, ap2, d1))
753 continue;
754 goto cufail;
755 }
756 /* now link the two structures so that no one else will */
757 /* come here */
758 /* store the terms to visit */
759 if (RATIONAL_TREES || pt0 < pt0_end) {
760 to_visit --;
761 #ifdef RATIONAL_TREES
762 unif++;
763 #endif
764 if ((void *)to_visit < (void *)unif) {
765 CELL **urec = (CELL **)unif;
766 to_visit = (struct v_record *)Yap_shift_visit((CELL **)to_visit, &urec);
767 unif = (struct unif_record *)urec;
768 }
769 to_visit->start0 = pt0;
770 to_visit->end0 = pt0_end;
771 to_visit->start1 = pt1;
772 #ifdef RATIONAL_TREES
773 unif[-1].old = *pt0;
774 unif[-1].ptr = pt0;
775 *pt0 = d1;
776 #endif
777 }
778 d0 = ArityOfFunctor(f);
779 pt0 = ap2;
780 pt0_end = ap2 + d0;
781 pt1 = ap3;
782 continue;
783 }
784 goto cufail;
785
786 derefa_body(d1, ptd1, unifiable_comp_nvar_unk, unifiable_comp_nvar_nvar);
787 /* d1 and pt2 have the unbound value, whereas d0 is bound */
788 BIND(ptd1, d0, bind_unifiable3);
789 #ifdef COROUTINING
790 DO_TRAIL(ptd1, d0);
791 bind_unifiable3:
792 #endif
793 continue;
794 }
795
796 derefa_body(d0, ptd0, unifiable_comp_unk, unifiable_comp_nvar);
797 /* first arg var */
798 {
799 register CELL d1;
800 register CELL *ptd1;
801
802 ptd1 = pt1;
803 d1 = ptd1[0];
804 /* pt2 is unbound */
805 deref_head(d1, unifiable_comp_var_unk);
806 unifiable_comp_var_nvar:
807 /* pt2 is unbound and d1 is bound */
808 BIND(ptd0, d1, bind_unifiable4);
809 #ifdef COROUTINING
810 DO_TRAIL(ptd0, d1);
811 bind_unifiable4:
812 #endif
813 continue;
814
815 derefa_body(d1, ptd1, unifiable_comp_var_unk, unifiable_comp_var_nvar);
816 /* ptd0 and ptd1 are unbound */
817 UnifiableGlobalCells(ptd0, ptd1);
818 }
819 }
820 /* Do we still have compound terms to visit */
821 if (to_visit < to_visit_base) {
822 pt0 = to_visit->start0;
823 pt0_end = to_visit->end0;
824 pt1 = to_visit->start1;
825 to_visit++;
826 goto loop;
827 }
828 #ifdef RATIONAL_TREES
829 /* restore bindigs */
830 while (unif-- != unif_base) {
831 CELL *pt0;
832
833 pt0 = unif->ptr;
834 *pt0 = unif->old;
835 }
836 #endif
837 return TRUE;
838
839 cufail:
840 #ifdef RATIONAL_TREES
841 /* restore bindigs */
842 while (unif-- != unif_base) {
843 CELL *pt0;
844
845 pt0 = unif->ptr;
846 *pt0 = unif->old;
847 }
848 #endif
849 return FALSE;
850 #ifdef THREADS
851 #undef Yap_REGS
852 #define Yap_REGS (*Yap_regp)
853 #elif defined(SHADOW_REGS)
854 #if defined(B) || defined(TR)
855 #undef Yap_REGS
856 #endif /* defined(B) || defined(TR) */
857 #endif
858 }
859
860 /* don't pollute name space */
861 #undef to_visit_base
862 #undef unif_base
863
864
865 static int
unifiable(CELL d0,CELL d1)866 unifiable(CELL d0, CELL d1)
867 {
868 #if THREADS
869 #undef Yap_REGS
870 register REGSTORE *regp = Yap_regp;
871 #define Yap_REGS (*regp)
872 #elif SHADOW_REGS
873 #if defined(B) || defined(TR)
874 register REGSTORE *regp = &Yap_REGS;
875
876 #define Yap_REGS (*regp)
877 #endif /* defined(B) || defined(TR) */
878 #endif
879
880 #if SHADOW_HB
881 register CELL *HBREG = HB;
882 #endif
883
884 register CELL *pt0, *pt1;
885
886 deref_head(d0, unifiable_unk);
887
888 unifiable_nvar:
889 /* d0 is bound */
890 deref_head(d1, unifiable_nvar_unk);
891 unifiable_nvar_nvar:
892 /* both arguments are bound */
893 if (d0 == d1)
894 return TRUE;
895 if (IsPairTerm(d0)) {
896 if (!IsPairTerm(d1)) {
897 return (FALSE);
898 }
899 pt0 = RepPair(d0);
900 pt1 = RepPair(d1);
901 return (unifiable_complex(pt0 - 1, pt0 + 1, pt1 - 1));
902 }
903 else if (IsApplTerm(d0)) {
904 pt0 = RepAppl(d0);
905 d0 = *pt0;
906 if (!IsApplTerm(d1))
907 return (FALSE);
908 pt1 = RepAppl(d1);
909 d1 = *pt1;
910 if (d0 != d1) {
911 return (FALSE);
912 } else {
913 if (IsExtensionFunctor((Functor)d0)) {
914 switch(d0) {
915 case (CELL)FunctorDBRef:
916 return(pt0 == pt1);
917 case (CELL)FunctorLongInt:
918 return(pt0[1] == pt1[1]);
919 case (CELL)FunctorDouble:
920 return(FloatOfTerm(AbsAppl(pt0)) == FloatOfTerm(AbsAppl(pt1)));
921 #ifdef USE_GMP
922 case (CELL)FunctorBigInt:
923 return(Yap_gmp_tcmp_big_big(AbsAppl(pt0),AbsAppl(pt0)) == 0);
924 #endif /* USE_GMP */
925 default:
926 return(FALSE);
927 }
928 }
929 return (unifiable_complex(pt0, pt0 + ArityOfFunctor((Functor) d0),
930 pt1));
931 }
932 } else {
933 return (FALSE);
934 }
935
936 deref_body(d1, pt1, unifiable_nvar_unk, unifiable_nvar_nvar);
937 /* d0 is bound and d1 is unbound */
938 BIND(pt1, d0, bind_unifiable3);
939 #ifdef COROUTINING
940 DO_TRAIL(pt1, d0);
941 bind_unifiable3:
942 #endif
943 return (TRUE);
944
945 deref_body(d0, pt0, unifiable_unk, unifiable_nvar);
946 /* pt0 is unbound */
947 deref_head(d1, unifiable_var_unk);
948 unifiable_var_nvar:
949 /* pt0 is unbound and d1 is bound */
950 BIND(pt0, d1, bind_unifiable4);
951 #ifdef COROUTINING
952 DO_TRAIL(pt0, d1);
953 bind_unifiable4:
954 #endif
955 return TRUE;
956
957 #if TRAILING_REQUIRES_BRANCH
958 unifiable_var_nvar_trail:
959 DO_TRAIL(pt0);
960 return TRUE;
961 #endif
962
963 deref_body(d1, pt1, unifiable_var_unk, unifiable_var_nvar);
964 /* d0 and pt1 are unbound */
965 UnifyCells(pt0, pt1, uc1, uc2);
966 #ifdef COROUTINING
967 DO_TRAIL(pt0, (CELL)pt1);
968 uc1:
969 #endif
970 return (TRUE);
971 #ifdef COROUTINING
972 uc2:
973 DO_TRAIL(pt1, (CELL)pt0);
974 return (TRUE);
975 #endif
976 #if THREADS
977 #undef Yap_REGS
978 #define Yap_REGS (*Yap_regp)
979 #elif SHADOW_REGS
980 #if defined(B) || defined(TR)
981 #undef Yap_REGS
982 #endif /* defined(B) || defined(TR) */
983 #endif
984 }
985
986
987 static Int
p_unifiable(void)988 p_unifiable(void)
989 {
990 tr_fr_ptr trp;
991 Term tf = TermNil;
992 if (!unifiable(ARG1,ARG2)) {
993 return FALSE;
994 }
995 trp = TR;
996 while (trp != B->cp_tr) {
997 Term t[2];
998 --trp;
999 t[0] = TrailTerm(trp);
1000 t[1] = *(CELL *)t[0];
1001 tf = MkPairTerm(Yap_MkApplTerm(FunctorEq,2,t),tf);
1002 RESET_VARIABLE(t[0]);
1003 }
1004 return Yap_unify(ARG3, tf);
1005 }
1006
1007 void
Yap_InitUnify(void)1008 Yap_InitUnify(void)
1009 {
1010 Term cm = CurrentModule;
1011 Yap_InitCPred("unify_with_occurs_check", 2, p_ocunify, SafePredFlag);
1012 Yap_InitCPred("acyclic_term", 1, p_acyclic, SafePredFlag|TestPredFlag);
1013 CurrentModule = TERMS_MODULE;
1014 Yap_InitCPred("cyclic_term", 1, p_cyclic, SafePredFlag|TestPredFlag);
1015 Yap_InitCPred("protected_unifiable", 3, p_unifiable, 0);
1016 CurrentModule = cm;
1017 }
1018
1019
1020 void
Yap_InitAbsmi(void)1021 Yap_InitAbsmi(void)
1022 {
1023 /* initialise access to abstract machine instructions */
1024 #if USE_THREADED_CODE
1025 Yap_absmi(1);
1026 InitReverseLookupOpcode();
1027 #endif
1028 }
1029
1030 void
Yap_TrimTrail(void)1031 Yap_TrimTrail(void)
1032 {
1033 #ifdef saveregs
1034 #undef saveregs
1035 #define saveregs()
1036 #endif
1037 #ifdef setregs
1038 #undef setregs
1039 #define setregs()
1040 #endif
1041 #if SHADOW_HB
1042 register CELL *HBREG = HB;
1043 #endif
1044
1045 #include "trim_trail.h"
1046 }
1047