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