1063 lines
24 KiB
C
1063 lines
24 KiB
C
/*************************************************************************
|
|
* *
|
|
* YAP Prolog *
|
|
* *
|
|
* Yap Prolog was developed at NCCUP - Universidade do Porto *
|
|
* *
|
|
* Copyright L.Damas, V.S.Costa and Universidade do Porto 1985-1997 *
|
|
* *
|
|
**************************************************************************
|
|
* *
|
|
* File: unify.c *
|
|
* Last rev: *
|
|
* mods: *
|
|
* comments: Unification and other auxiliary routines for absmi *
|
|
* *
|
|
*************************************************************************/
|
|
/** @defgroup Rational_Trees Rational Trees
|
|
@ingroup extensions
|
|
@{
|
|
|
|
Prolog unification is not a complete implementation. For efficiency
|
|
considerations, Prolog systems do not perform occur checks while
|
|
unifying terms. As an example, `X = a(X)` will not fail but instead
|
|
will create an infinite term of the form `a(a(a(a(a(...)))))`, or
|
|
<em>rational tree</em>.
|
|
|
|
Rational trees are now supported by default in YAP. In previous
|
|
versions, this was not the default and these terms could easily lead
|
|
to infinite computation. For example, `X = a(X), X = X` would
|
|
enter an infinite loop.
|
|
|
|
The `RATIONAL_TREES` flag improves support for these
|
|
terms. Internal primitives are now aware that these terms can exist, and
|
|
will not enter infinite loops. Hence, the previous unification will
|
|
succeed. Another example, `X = a(X), ground(X)` will succeed
|
|
instead of looping. Other affected built-ins include the term comparison
|
|
primitives, numbervars/3, copy_term/2, and the internal
|
|
data base routines. The support does not extend to Input/Output routines
|
|
or to assert/1 YAP does not allow directly reading
|
|
rational trees, and you need to use `write_depth/2` to avoid
|
|
entering an infinite cycle when trying to write an infinite term.
|
|
|
|
|
|
*/
|
|
|
|
#define IN_UNIFY_C 1
|
|
|
|
#define HAS_CACHE_REGS 1
|
|
|
|
#include "absmi.h"
|
|
|
|
int Yap_rational_tree_loop(CELL *, CELL *, CELL **, CELL **);
|
|
|
|
static int OCUnify_complex(CELL *, CELL *, CELL *);
|
|
static int OCUnify(register CELL, register CELL);
|
|
static Int p_ocunify( USES_REGS1 );
|
|
|
|
/* support for rational trees and unification with occur checking */
|
|
|
|
#define to_visit_base ((struct v_record *)AuxSp)
|
|
|
|
int
|
|
Yap_rational_tree_loop(CELL *pt0, CELL *pt0_end, CELL **to_visit, CELL **to_visit_max)
|
|
{
|
|
CELL ** base = to_visit;
|
|
rtree_loop:
|
|
while (pt0 < pt0_end) {
|
|
register CELL *ptd0;
|
|
register CELL d0;
|
|
|
|
ptd0 = ++pt0;
|
|
pt0 = ptd0;
|
|
d0 = *ptd0;
|
|
deref_head(d0, rtree_loop_unk);
|
|
rtree_loop_nvar:
|
|
{
|
|
if (d0 == TermFoundVar)
|
|
goto cufail;
|
|
if (IsPairTerm(d0)) {
|
|
to_visit -= 3;
|
|
if (to_visit < to_visit_max) {
|
|
to_visit = Yap_shift_visit(to_visit, &to_visit_max, &base);
|
|
}
|
|
to_visit[0] = pt0;
|
|
to_visit[1] = pt0_end;
|
|
to_visit[2] = (CELL *)*pt0;
|
|
*pt0 = TermFoundVar;
|
|
pt0_end = (pt0 = RepPair(d0) - 1) + 2;
|
|
continue;
|
|
}
|
|
if (IsApplTerm(d0)) {
|
|
register Functor f;
|
|
register CELL *ap2;
|
|
|
|
/* store the terms to visit */
|
|
ap2 = RepAppl(d0);
|
|
f = (Functor) (*ap2);
|
|
/* compare functors */
|
|
if (IsExtensionFunctor(f)) {
|
|
continue;
|
|
}
|
|
to_visit -= 3;
|
|
if (to_visit < to_visit_max) {
|
|
to_visit = Yap_shift_visit(to_visit, &to_visit_max, &base);
|
|
}
|
|
to_visit[0] = pt0;
|
|
to_visit[1] = pt0_end;
|
|
to_visit[2] = (CELL *)*pt0;
|
|
*pt0 = TermFoundVar;
|
|
d0 = ArityOfFunctor(f);
|
|
pt0 = ap2;
|
|
pt0_end = ap2 + d0;
|
|
continue;
|
|
}
|
|
continue;
|
|
}
|
|
|
|
derefa_body(d0, ptd0, rtree_loop_unk, rtree_loop_nvar);
|
|
}
|
|
/* Do we still have compound terms to visit */
|
|
if (to_visit < base) {
|
|
pt0 = to_visit[0];
|
|
pt0_end = to_visit[1];
|
|
*pt0 = (CELL)to_visit[2];
|
|
to_visit += 3;
|
|
goto rtree_loop;
|
|
}
|
|
return FALSE;
|
|
|
|
cufail:
|
|
/* we found an infinite term */
|
|
while (to_visit < (CELL **)base) {
|
|
CELL *pt0;
|
|
pt0 = to_visit[0];
|
|
*pt0 = (CELL)to_visit[2];
|
|
to_visit += 3;
|
|
}
|
|
return TRUE;
|
|
}
|
|
|
|
static inline int
|
|
rational_tree(Term d0) {
|
|
CACHE_REGS
|
|
CELL **to_visit_max = (CELL **)AuxBase, **to_visit = (CELL **)AuxSp;
|
|
|
|
if (IsPairTerm(d0)) {
|
|
CELL *pt0 = RepPair(d0);
|
|
|
|
return Yap_rational_tree_loop(pt0-1, pt0+1, to_visit, to_visit_max);
|
|
} else if (IsApplTerm(d0)) {
|
|
CELL *pt0 = RepAppl(d0);
|
|
Functor f = (Functor)(*pt0);
|
|
|
|
if (IsExtensionFunctor(f))
|
|
return FALSE;
|
|
return Yap_rational_tree_loop(pt0, pt0+ArityOfFunctor(f), to_visit, to_visit_max);
|
|
} else
|
|
return FALSE;
|
|
}
|
|
|
|
static int
|
|
OCUnify_complex(CELL *pt0, CELL *pt0_end, CELL *pt1)
|
|
{
|
|
CACHE_REGS
|
|
#ifdef THREADS
|
|
#undef Yap_REGS
|
|
register REGSTORE *regp = Yap_regp;
|
|
#define Yap_REGS (*regp)
|
|
#elif defined(SHADOW_REGS)
|
|
#if defined(B) || defined(TR)
|
|
register REGSTORE *regp = &Yap_REGS;
|
|
|
|
#define Yap_REGS (*regp)
|
|
#endif /* defined(B) || defined(TR) || defined(HB) */
|
|
#endif
|
|
|
|
#ifdef SHADOW_HB
|
|
register CELL *HBREG = HB;
|
|
#endif /* SHADOW_HB */
|
|
|
|
struct unif_record *unif = (struct unif_record *)AuxBase;
|
|
struct v_record *to_visit = (struct v_record *)AuxSp;
|
|
#define unif_base ((struct unif_record *)AuxBase)
|
|
|
|
loop:
|
|
while (pt0 < pt0_end) {
|
|
register CELL *ptd0 = pt0+1;
|
|
register CELL d0;
|
|
|
|
++pt1;
|
|
pt0 = ptd0;
|
|
d0 = *ptd0;
|
|
deref_head(d0, unify_comp_unk);
|
|
unify_comp_nvar:
|
|
{
|
|
register CELL *ptd1 = pt1;
|
|
register CELL d1 = *ptd1;
|
|
|
|
deref_head(d1, unify_comp_nvar_unk);
|
|
unify_comp_nvar_nvar:
|
|
if (d0 == d1) {
|
|
if (Yap_rational_tree_loop(pt0-1, pt0, (CELL **)to_visit, (CELL **)unif))
|
|
goto cufail;
|
|
continue;
|
|
}
|
|
if (IsPairTerm(d0)) {
|
|
if (!IsPairTerm(d1)) {
|
|
goto cufail;
|
|
}
|
|
/* now link the two structures so that no one else will */
|
|
/* come here */
|
|
/* store the terms to visit */
|
|
if (RATIONAL_TREES || pt0 < pt0_end) {
|
|
to_visit --;
|
|
#ifdef RATIONAL_TREES
|
|
unif++;
|
|
#endif
|
|
if ((void *)to_visit < (void *)unif) {
|
|
CELL **urec = (CELL **)unif;
|
|
to_visit = (struct v_record *)Yap_shift_visit((CELL **)to_visit, &urec, NULL);
|
|
unif = (struct unif_record *)urec;
|
|
}
|
|
to_visit->start0 = pt0;
|
|
to_visit->end0 = pt0_end;
|
|
to_visit->start1 = pt1;
|
|
#ifdef RATIONAL_TREES
|
|
unif[-1].old = *pt0;
|
|
unif[-1].ptr = pt0;
|
|
*pt0 = d1;
|
|
#endif
|
|
}
|
|
pt0_end = (pt0 = RepPair(d0) - 1) + 2;
|
|
pt1 = RepPair(d1) - 1;
|
|
continue;
|
|
}
|
|
if (IsApplTerm(d0)) {
|
|
register Functor f;
|
|
register CELL *ap2, *ap3;
|
|
|
|
if (!IsApplTerm(d1)) {
|
|
goto cufail;
|
|
}
|
|
/* store the terms to visit */
|
|
ap2 = RepAppl(d0);
|
|
ap3 = RepAppl(d1);
|
|
f = (Functor) (*ap2);
|
|
/* compare functors */
|
|
if (f != (Functor) *ap3)
|
|
goto cufail;
|
|
if (IsExtensionFunctor(f)) {
|
|
if (unify_extension(f, d0, ap2, d1))
|
|
continue;
|
|
goto cufail;
|
|
}
|
|
/* now link the two structures so that no one else will */
|
|
/* come here */
|
|
/* store the terms to visit */
|
|
if (RATIONAL_TREES || pt0 < pt0_end) {
|
|
to_visit --;
|
|
#ifdef RATIONAL_TREES
|
|
unif++;
|
|
#endif
|
|
if ((void *)to_visit < (void *)unif) {
|
|
CELL **urec = (CELL **)unif;
|
|
to_visit = (struct v_record *)Yap_shift_visit((CELL **)to_visit, &urec, NULL);
|
|
unif = (struct unif_record *)urec;
|
|
}
|
|
to_visit->start0 = pt0;
|
|
to_visit->end0 = pt0_end;
|
|
to_visit->start1 = pt1;
|
|
#ifdef RATIONAL_TREES
|
|
unif[-1].old = *pt0;
|
|
unif[-1].ptr = pt0;
|
|
*pt0 = d1;
|
|
#endif
|
|
}
|
|
d0 = ArityOfFunctor(f);
|
|
pt0 = ap2;
|
|
pt0_end = ap2 + d0;
|
|
pt1 = ap3;
|
|
continue;
|
|
}
|
|
goto cufail;
|
|
|
|
derefa_body(d1, ptd1, unify_comp_nvar_unk, unify_comp_nvar_nvar);
|
|
/* d1 and pt2 have the unbound value, whereas d0 is bound */
|
|
Bind_Global(ptd1, d0);
|
|
if (Yap_rational_tree_loop(ptd1-1, ptd1, (CELL **)to_visit, (CELL **)unif))
|
|
goto cufail;
|
|
continue;
|
|
}
|
|
|
|
derefa_body(d0, ptd0, unify_comp_unk, unify_comp_nvar);
|
|
/* first arg var */
|
|
{
|
|
register CELL d1;
|
|
register CELL *ptd1;
|
|
|
|
ptd1 = pt1;
|
|
d1 = ptd1[0];
|
|
/* pt2 is unbound */
|
|
deref_head(d1, unify_comp_var_unk);
|
|
unify_comp_var_nvar:
|
|
/* pt2 is unbound and d1 is bound */
|
|
Bind_Global(ptd0, d1);
|
|
if (Yap_rational_tree_loop(ptd0-1, ptd0, (CELL **)to_visit, (CELL **)unif))
|
|
goto cufail;
|
|
continue;
|
|
|
|
derefa_body(d1, ptd1, unify_comp_var_unk, unify_comp_var_nvar);
|
|
/* ptd0 and ptd1 are unbound */
|
|
UnifyGlobalCells(ptd0, ptd1);
|
|
}
|
|
}
|
|
/* Do we still have compound terms to visit */
|
|
if (to_visit < to_visit_base) {
|
|
pt0 = to_visit->start0;
|
|
pt0_end = to_visit->end0;
|
|
pt1 = to_visit->start1;
|
|
to_visit++;
|
|
goto loop;
|
|
}
|
|
#ifdef RATIONAL_TREES
|
|
/* restore bindigs */
|
|
while (unif-- != unif_base) {
|
|
CELL *pt0;
|
|
|
|
pt0 = unif->ptr;
|
|
*pt0 = unif->old;
|
|
}
|
|
#endif
|
|
return TRUE;
|
|
|
|
cufail:
|
|
#ifdef RATIONAL_TREES
|
|
/* restore bindigs */
|
|
while (unif-- != unif_base) {
|
|
CELL *pt0;
|
|
|
|
pt0 = unif->ptr;
|
|
*pt0 = unif->old;
|
|
}
|
|
#endif
|
|
return FALSE;
|
|
#ifdef THREADS
|
|
#undef Yap_REGS
|
|
#define Yap_REGS (*Yap_regp)
|
|
#elif defined(SHADOW_REGS)
|
|
#if defined(B) || defined(TR)
|
|
#undef Yap_REGS
|
|
#endif /* defined(B) || defined(TR) */
|
|
#endif
|
|
#undef unif_base
|
|
#undef to_visit_base
|
|
}
|
|
|
|
static int
|
|
OCUnify(register CELL d0, register CELL d1)
|
|
{
|
|
CACHE_REGS
|
|
register CELL *pt0, *pt1;
|
|
|
|
#if SHADOW_HB
|
|
register CELL *HBREG = HB;
|
|
#endif
|
|
|
|
deref_head(d0, oc_unify_unk);
|
|
|
|
oc_unify_nvar:
|
|
/* d0 is bound */
|
|
deref_head(d1, oc_unify_nvar_unk);
|
|
oc_unify_nvar_nvar:
|
|
|
|
if (d0 == d1) {
|
|
return (!rational_tree(d0));
|
|
}
|
|
/* both arguments are bound */
|
|
if (IsPairTerm(d0)) {
|
|
if (!IsPairTerm(d1)) {
|
|
return (FALSE);
|
|
}
|
|
pt0 = RepPair(d0);
|
|
pt1 = RepPair(d1);
|
|
return (OCUnify_complex(pt0 - 1, pt0 + 1, pt1 - 1));
|
|
}
|
|
else if (IsApplTerm(d0)) {
|
|
if (!IsApplTerm(d1))
|
|
return (FALSE);
|
|
pt0 = RepAppl(d0);
|
|
d0 = *pt0;
|
|
pt1 = RepAppl(d1);
|
|
d1 = *pt1;
|
|
if (d0 != d1) {
|
|
return (FALSE);
|
|
} else {
|
|
if (IsExtensionFunctor((Functor)d0)) {
|
|
switch(d0) {
|
|
case (CELL)FunctorDBRef:
|
|
return(pt0 == pt1);
|
|
case (CELL)FunctorLongInt:
|
|
return(pt0[1] == pt1[1]);
|
|
case (CELL)FunctorDouble:
|
|
return(FloatOfTerm(AbsAppl(pt0)) == FloatOfTerm(AbsAppl(pt1)));
|
|
case (CELL)FunctorString:
|
|
return(strcmp( (const char *)(pt0+2), (const char *)(pt1+2)) == 0);
|
|
#ifdef USE_GMP
|
|
case (CELL)FunctorBigInt:
|
|
return(Yap_gmp_tcmp_big_big(AbsAppl(pt0),AbsAppl(pt0)) == 0);
|
|
#endif /* USE_GMP */
|
|
default:
|
|
return(FALSE);
|
|
}
|
|
}
|
|
return (OCUnify_complex(pt0, pt0 + ArityOfFunctor((Functor) d0),
|
|
pt1));
|
|
}
|
|
} else {
|
|
return(FALSE);
|
|
}
|
|
|
|
deref_body(d1, pt1, oc_unify_nvar_unk, oc_unify_nvar_nvar);
|
|
/* d0 is bound and d1 is unbound */
|
|
YapBind(pt1, d0);
|
|
/* local variables cannot be in a term */
|
|
if (pt1 > HR && pt1 < LCL0)
|
|
return TRUE;
|
|
if (rational_tree(d0))
|
|
return(FALSE);
|
|
return (TRUE);
|
|
|
|
deref_body(d0, pt0, oc_unify_unk, oc_unify_nvar);
|
|
/* pt0 is unbound */
|
|
deref_head(d1, oc_unify_var_unk);
|
|
oc_unify_var_nvar:
|
|
/* pt0 is unbound and d1 is bound */
|
|
YapBind(pt0, d1);
|
|
/* local variables cannot be in a term */
|
|
if (pt0 > HR && pt0 < LCL0)
|
|
return TRUE;
|
|
if (rational_tree(d1))
|
|
return(FALSE);
|
|
return (TRUE);
|
|
|
|
deref_body(d1, pt1, oc_unify_var_unk, oc_unify_var_nvar);
|
|
/* d0 and pt1 are unbound */
|
|
UnifyCells(pt0, pt1);
|
|
return (TRUE);
|
|
return (TRUE);
|
|
}
|
|
|
|
static Int
|
|
p_ocunify( USES_REGS1 )
|
|
{
|
|
return(OCUnify(ARG1,ARG2));
|
|
}
|
|
|
|
static Int
|
|
p_cyclic( USES_REGS1 )
|
|
{
|
|
Term t = Deref(ARG1);
|
|
if (IsVarTerm(t))
|
|
return(FALSE);
|
|
return rational_tree(t);
|
|
}
|
|
|
|
bool Yap_IsAcyclicTerm(Term t)
|
|
{
|
|
return !rational_tree(t);
|
|
}
|
|
|
|
static Int
|
|
p_acyclic( USES_REGS1 )
|
|
{
|
|
Term t = Deref(ARG1);
|
|
if (IsVarTerm(t))
|
|
return(TRUE);
|
|
return !rational_tree(t);
|
|
}
|
|
|
|
int
|
|
Yap_IUnify(register CELL d0, register CELL d1)
|
|
{
|
|
CACHE_REGS
|
|
#if THREADS
|
|
#undef Yap_REGS
|
|
register REGSTORE *regp = Yap_regp;
|
|
#define Yap_REGS (*regp)
|
|
#elif SHADOW_REGS
|
|
#if defined(B) || defined(TR)
|
|
register REGSTORE *regp = &Yap_REGS;
|
|
|
|
#define Yap_REGS (*regp)
|
|
#endif /* defined(B) || defined(TR) */
|
|
#endif
|
|
|
|
#if SHADOW_HB
|
|
register CELL *HBREG = HB;
|
|
#endif
|
|
|
|
register CELL *pt0, *pt1;
|
|
|
|
deref_head(d0, unify_unk);
|
|
|
|
unify_nvar:
|
|
/* d0 is bound */
|
|
deref_head(d1, unify_nvar_unk);
|
|
unify_nvar_nvar:
|
|
/* both arguments are bound */
|
|
if (d0 == d1)
|
|
return TRUE;
|
|
if (IsPairTerm(d0)) {
|
|
if (!IsPairTerm(d1)) {
|
|
return (FALSE);
|
|
}
|
|
pt0 = RepPair(d0);
|
|
pt1 = RepPair(d1);
|
|
return (IUnify_complex(pt0 - 1, pt0 + 1, pt1 - 1));
|
|
}
|
|
else if (IsApplTerm(d0)) {
|
|
pt0 = RepAppl(d0);
|
|
d0 = *pt0;
|
|
if (!IsApplTerm(d1))
|
|
return (FALSE);
|
|
pt1 = RepAppl(d1);
|
|
d1 = *pt1;
|
|
if (d0 != d1) {
|
|
return (FALSE);
|
|
} else {
|
|
if (IsExtensionFunctor((Functor)d0)) {
|
|
switch(d0) {
|
|
case (CELL)FunctorDBRef:
|
|
return(pt0 == pt1);
|
|
case (CELL)FunctorLongInt:
|
|
return(pt0[1] == pt1[1]);
|
|
case (CELL)FunctorString:
|
|
return(strcmp( (const char *)(pt0+2), (const char *)(pt1+2)) == 0);
|
|
case (CELL)FunctorDouble:
|
|
return(FloatOfTerm(AbsAppl(pt0)) == FloatOfTerm(AbsAppl(pt1)));
|
|
#ifdef USE_GMP
|
|
case (CELL)FunctorBigInt:
|
|
return(Yap_gmp_tcmp_big_big(AbsAppl(pt0),AbsAppl(pt0)) == 0);
|
|
#endif /* USE_GMP */
|
|
default:
|
|
return(FALSE);
|
|
}
|
|
}
|
|
return (IUnify_complex(pt0, pt0 + ArityOfFunctor((Functor) d0),
|
|
pt1));
|
|
}
|
|
} else {
|
|
return (FALSE);
|
|
}
|
|
|
|
deref_body(d1, pt1, unify_nvar_unk, unify_nvar_nvar);
|
|
/* d0 is bound and d1 is unbound */
|
|
YapBind(pt1, d0);
|
|
return (TRUE);
|
|
|
|
deref_body(d0, pt0, unify_unk, unify_nvar);
|
|
/* pt0 is unbound */
|
|
deref_head(d1, unify_var_unk);
|
|
unify_var_nvar:
|
|
/* pt0 is unbound and d1 is bound */
|
|
YapBind(pt0, d1);
|
|
return TRUE;
|
|
|
|
#if TRAILING_REQUIRES_BRANCH
|
|
unify_var_nvar_trail:
|
|
DO_TRAIL(pt0);
|
|
return TRUE;
|
|
#endif
|
|
|
|
deref_body(d1, pt1, unify_var_unk, unify_var_nvar);
|
|
/* d0 and pt1 are unbound */
|
|
UnifyCells(pt0, pt1);
|
|
return (TRUE);
|
|
|
|
#if THREADS
|
|
#undef Yap_REGS
|
|
#define Yap_REGS (*Yap_regp)
|
|
#elif SHADOW_REGS
|
|
#if defined(B) || defined(TR)
|
|
#undef Yap_REGS
|
|
#endif /* defined(B) || defined(TR) */
|
|
#endif
|
|
}
|
|
|
|
/**********************************************************************
|
|
* *
|
|
* Conversion from Label to Op *
|
|
* *
|
|
**********************************************************************/
|
|
|
|
#if USE_THREADED_CODE
|
|
|
|
/* mask a hash table that allows for fast reverse translation from
|
|
instruction address to corresponding opcode */
|
|
static void
|
|
InitReverseLookupOpcode(void)
|
|
{
|
|
op_entry *opeptr;
|
|
op_numbers i;
|
|
/* 2 K should be OK */
|
|
int hash_size_mask = OP_HASH_SIZE-1;
|
|
UInt sz = OP_HASH_SIZE*sizeof(struct opcode_tab_entry);
|
|
|
|
if ((OP_RTABLE = (op_entry *)Yap_AllocCodeSpace(sz)) == NULL) {
|
|
if (!Yap_growheap(FALSE, sz, NULL)) {
|
|
Yap_Error(SYSTEM_ERROR_INTERNAL, TermNil,
|
|
"Couldn't obtain space for the reverse translation opcode table");
|
|
}
|
|
}
|
|
memset(OP_RTABLE, 0, sz);
|
|
opeptr = OP_RTABLE;
|
|
/* clear up table */
|
|
{
|
|
int j;
|
|
for (j=0; j<OP_HASH_SIZE; j++) {
|
|
opeptr[j].opc = 0;
|
|
opeptr[j].opnum = _Ystop;
|
|
}
|
|
}
|
|
opeptr = OP_RTABLE;
|
|
opeptr[rtable_hash_op(Yap_opcode(_Ystop),hash_size_mask)].opc
|
|
= Yap_opcode(_Ystop);
|
|
/* now place entries */
|
|
for (i = _std_top; i > _Ystop; i--) {
|
|
OPCODE opc = Yap_opcode(i);
|
|
int j = rtable_hash_op(opc,hash_size_mask);
|
|
while (opeptr[j].opc) {
|
|
if (++j > hash_size_mask)
|
|
j = 0;
|
|
}
|
|
/* clear entry, no conflict */
|
|
opeptr[j].opnum = i;
|
|
opeptr[j].opc = opc;
|
|
}
|
|
}
|
|
#endif
|
|
|
|
#define UnifyAndTrailGlobalCells(a, b) \
|
|
if((a) > (b)) { \
|
|
*(a) = (CELL)(b); \
|
|
DO_TRAIL((a), (CELL)(b)); \
|
|
} else if((a) < (b)){ \
|
|
*(b) = (CELL)(a); \
|
|
DO_TRAIL((b), (CELL)(a)); \
|
|
}
|
|
|
|
static int
|
|
unifiable_complex(CELL *pt0, CELL *pt0_end, CELL *pt1)
|
|
{
|
|
CACHE_REGS
|
|
#ifdef THREADS
|
|
#undef Yap_REGS
|
|
register REGSTORE *regp = Yap_regp;
|
|
#define Yap_REGS (*regp)
|
|
#elif defined(SHADOW_REGS)
|
|
#if defined(B) || defined(TR)
|
|
register REGSTORE *regp = &Yap_REGS;
|
|
|
|
#define Yap_REGS (*regp)
|
|
#endif /* defined(B) || defined(TR) || defined(HB) */
|
|
#endif
|
|
|
|
#ifdef SHADOW_HB
|
|
register CELL *HBREG = HB;
|
|
#endif /* SHADOW_HB */
|
|
|
|
struct unif_record *unif = (struct unif_record *)AuxBase;
|
|
struct v_record *to_visit = (struct v_record *)AuxSp;
|
|
#define unif_base ((struct unif_record *)AuxBase)
|
|
#define to_visit_base ((struct v_record *)AuxSp)
|
|
|
|
loop:
|
|
while (pt0 < pt0_end) {
|
|
register CELL *ptd0 = pt0+1;
|
|
register CELL d0;
|
|
|
|
++pt1;
|
|
pt0 = ptd0;
|
|
d0 = *ptd0;
|
|
deref_head(d0, unifiable_comp_unk);
|
|
unifiable_comp_nvar:
|
|
{
|
|
register CELL *ptd1 = pt1;
|
|
register CELL d1 = *ptd1;
|
|
|
|
deref_head(d1, unifiable_comp_nvar_unk);
|
|
unifiable_comp_nvar_nvar:
|
|
if (d0 == d1)
|
|
continue;
|
|
if (IsPairTerm(d0)) {
|
|
if (!IsPairTerm(d1)) {
|
|
goto cufail;
|
|
}
|
|
/* now link the two structures so that no one else will */
|
|
/* come here */
|
|
/* store the terms to visit */
|
|
if (RATIONAL_TREES || pt0 < pt0_end) {
|
|
to_visit --;
|
|
#ifdef RATIONAL_TREES
|
|
unif++;
|
|
#endif
|
|
if ((void *)to_visit < (void *)unif) {
|
|
CELL **urec = (CELL **)unif;
|
|
to_visit = (struct v_record *)Yap_shift_visit((CELL **)to_visit, &urec, NULL);
|
|
unif = (struct unif_record *)urec;
|
|
}
|
|
to_visit->start0 = pt0;
|
|
to_visit->end0 = pt0_end;
|
|
to_visit->start1 = pt1;
|
|
#ifdef RATIONAL_TREES
|
|
unif[-1].old = *pt0;
|
|
unif[-1].ptr = pt0;
|
|
*pt0 = d1;
|
|
#endif
|
|
}
|
|
pt0_end = (pt0 = RepPair(d0) - 1) + 2;
|
|
pt1 = RepPair(d1) - 1;
|
|
continue;
|
|
}
|
|
if (IsApplTerm(d0)) {
|
|
register Functor f;
|
|
register CELL *ap2, *ap3;
|
|
|
|
if (!IsApplTerm(d1)) {
|
|
goto cufail;
|
|
}
|
|
/* store the terms to visit */
|
|
ap2 = RepAppl(d0);
|
|
ap3 = RepAppl(d1);
|
|
f = (Functor) (*ap2);
|
|
/* compare functors */
|
|
if (f != (Functor) *ap3)
|
|
goto cufail;
|
|
if (IsExtensionFunctor(f)) {
|
|
if (unify_extension(f, d0, ap2, d1))
|
|
continue;
|
|
goto cufail;
|
|
}
|
|
/* now link the two structures so that no one else will */
|
|
/* come here */
|
|
/* store the terms to visit */
|
|
if (RATIONAL_TREES || pt0 < pt0_end) {
|
|
to_visit --;
|
|
#ifdef RATIONAL_TREES
|
|
unif++;
|
|
#endif
|
|
if ((void *)to_visit < (void *)unif) {
|
|
CELL **urec = (CELL **)unif;
|
|
to_visit = (struct v_record *)Yap_shift_visit((CELL **)to_visit, &urec, NULL);
|
|
unif = (struct unif_record *)urec;
|
|
}
|
|
to_visit->start0 = pt0;
|
|
to_visit->end0 = pt0_end;
|
|
to_visit->start1 = pt1;
|
|
#ifdef RATIONAL_TREES
|
|
unif[-1].old = *pt0;
|
|
unif[-1].ptr = pt0;
|
|
*pt0 = d1;
|
|
#endif
|
|
}
|
|
d0 = ArityOfFunctor(f);
|
|
pt0 = ap2;
|
|
pt0_end = ap2 + d0;
|
|
pt1 = ap3;
|
|
continue;
|
|
}
|
|
goto cufail;
|
|
|
|
derefa_body(d1, ptd1, unifiable_comp_nvar_unk, unifiable_comp_nvar_nvar);
|
|
/* d1 and pt2 have the unbound value, whereas d0 is bound */
|
|
*(ptd1) = d0;
|
|
DO_TRAIL(ptd1, d0);
|
|
continue;
|
|
}
|
|
|
|
derefa_body(d0, ptd0, unifiable_comp_unk, unifiable_comp_nvar);
|
|
/* first arg var */
|
|
{
|
|
register CELL d1;
|
|
register CELL *ptd1;
|
|
|
|
ptd1 = pt1;
|
|
d1 = ptd1[0];
|
|
/* pt2 is unbound */
|
|
deref_head(d1, unifiable_comp_var_unk);
|
|
unifiable_comp_var_nvar:
|
|
/* pt2 is unbound and d1 is bound */
|
|
*ptd0 = d1;
|
|
DO_TRAIL(ptd0, d1);
|
|
continue;
|
|
|
|
derefa_body(d1, ptd1, unifiable_comp_var_unk, unifiable_comp_var_nvar);
|
|
/* ptd0 and ptd1 are unbound */
|
|
UnifyAndTrailGlobalCells(ptd0, ptd1);
|
|
}
|
|
}
|
|
/* Do we still have compound terms to visit */
|
|
if (to_visit < to_visit_base) {
|
|
pt0 = to_visit->start0;
|
|
pt0_end = to_visit->end0;
|
|
pt1 = to_visit->start1;
|
|
to_visit++;
|
|
goto loop;
|
|
}
|
|
#ifdef RATIONAL_TREES
|
|
/* restore bindigs */
|
|
while (unif-- != unif_base) {
|
|
CELL *pt0;
|
|
|
|
pt0 = unif->ptr;
|
|
*pt0 = unif->old;
|
|
}
|
|
#endif
|
|
return TRUE;
|
|
|
|
cufail:
|
|
#ifdef RATIONAL_TREES
|
|
/* restore bindigs */
|
|
while (unif-- != unif_base) {
|
|
CELL *pt0;
|
|
|
|
pt0 = unif->ptr;
|
|
*pt0 = unif->old;
|
|
}
|
|
#endif
|
|
return FALSE;
|
|
#ifdef THREADS
|
|
#undef Yap_REGS
|
|
#define Yap_REGS (*Yap_regp)
|
|
#elif defined(SHADOW_REGS)
|
|
#if defined(B) || defined(TR)
|
|
#undef Yap_REGS
|
|
#endif /* defined(B) || defined(TR) */
|
|
#endif
|
|
}
|
|
|
|
/* don't pollute name space */
|
|
#undef to_visit_base
|
|
#undef unif_base
|
|
|
|
|
|
static int
|
|
unifiable(CELL d0, CELL d1)
|
|
{
|
|
CACHE_REGS
|
|
#if THREADS
|
|
#undef Yap_REGS
|
|
register REGSTORE *regp = Yap_regp;
|
|
#define Yap_REGS (*regp)
|
|
#elif SHADOW_REGS
|
|
#if defined(B) || defined(TR)
|
|
register REGSTORE *regp = &Yap_REGS;
|
|
|
|
#define Yap_REGS (*regp)
|
|
#endif /* defined(B) || defined(TR) */
|
|
#endif
|
|
|
|
#if SHADOW_HB
|
|
register CELL *HBREG = HB;
|
|
#endif
|
|
|
|
register CELL *pt0, *pt1;
|
|
|
|
deref_head(d0, unifiable_unk);
|
|
|
|
unifiable_nvar:
|
|
/* d0 is bound */
|
|
deref_head(d1, unifiable_nvar_unk);
|
|
unifiable_nvar_nvar:
|
|
/* both arguments are bound */
|
|
if (d0 == d1)
|
|
return TRUE;
|
|
if (IsPairTerm(d0)) {
|
|
if (!IsPairTerm(d1)) {
|
|
return (FALSE);
|
|
}
|
|
pt0 = RepPair(d0);
|
|
pt1 = RepPair(d1);
|
|
return (unifiable_complex(pt0 - 1, pt0 + 1, pt1 - 1));
|
|
}
|
|
else if (IsApplTerm(d0)) {
|
|
pt0 = RepAppl(d0);
|
|
d0 = *pt0;
|
|
if (!IsApplTerm(d1))
|
|
return (FALSE);
|
|
pt1 = RepAppl(d1);
|
|
d1 = *pt1;
|
|
if (d0 != d1) {
|
|
return (FALSE);
|
|
} else {
|
|
if (IsExtensionFunctor((Functor)d0)) {
|
|
switch(d0) {
|
|
case (CELL)FunctorDBRef:
|
|
return(pt0 == pt1);
|
|
case (CELL)FunctorLongInt:
|
|
return(pt0[1] == pt1[1]);
|
|
case (CELL)FunctorString:
|
|
return(strcmp( (const char *)(pt0+2), (const char *)(pt1+2)) == 0);
|
|
case (CELL)FunctorDouble:
|
|
return(FloatOfTerm(AbsAppl(pt0)) == FloatOfTerm(AbsAppl(pt1)));
|
|
#ifdef USE_GMP
|
|
case (CELL)FunctorBigInt:
|
|
return(Yap_gmp_tcmp_big_big(AbsAppl(pt0),AbsAppl(pt0)) == 0);
|
|
#endif /* USE_GMP */
|
|
default:
|
|
return(FALSE);
|
|
}
|
|
}
|
|
return (unifiable_complex(pt0, pt0 + ArityOfFunctor((Functor) d0),
|
|
pt1));
|
|
}
|
|
} else {
|
|
return (FALSE);
|
|
}
|
|
|
|
deref_body(d1, pt1, unifiable_nvar_unk, unifiable_nvar_nvar);
|
|
/* d0 is bound and d1 is unbound */
|
|
*(pt1) = d0;
|
|
DO_TRAIL(pt1, d0);
|
|
return (TRUE);
|
|
|
|
deref_body(d0, pt0, unifiable_unk, unifiable_nvar);
|
|
/* pt0 is unbound */
|
|
deref_head(d1, unifiable_var_unk);
|
|
unifiable_var_nvar:
|
|
/* pt0 is unbound and d1 is bound */
|
|
*pt0 = d1;
|
|
DO_TRAIL(pt0, d1);
|
|
return TRUE;
|
|
|
|
deref_body(d1, pt1, unifiable_var_unk, unifiable_var_nvar);
|
|
/* d0 and pt1 are unbound */
|
|
UnifyAndTrailCells(pt0, pt1);
|
|
return (TRUE);
|
|
#if THREADS
|
|
#undef Yap_REGS
|
|
#define Yap_REGS (*Yap_regp)
|
|
#elif SHADOW_REGS
|
|
#if defined(B) || defined(TR)
|
|
#undef Yap_REGS
|
|
#endif /* defined(B) || defined(TR) */
|
|
#endif
|
|
}
|
|
|
|
|
|
static Int
|
|
p_unifiable( USES_REGS1 )
|
|
{
|
|
tr_fr_ptr trp, trp0 = TR;
|
|
Term tf = TermNil;
|
|
if (!unifiable(ARG1,ARG2)) {
|
|
return FALSE;
|
|
}
|
|
trp = TR;
|
|
while (trp != trp0) {
|
|
Term t[2];
|
|
--trp;
|
|
t[0] = TrailTerm(trp);
|
|
t[1] = *(CELL *)t[0];
|
|
tf = MkPairTerm(Yap_MkApplTerm(FunctorEq,2,t),tf);
|
|
RESET_VARIABLE(t[0]);
|
|
}
|
|
return Yap_unify(ARG3, tf);
|
|
}
|
|
|
|
int
|
|
Yap_Unifiable( Term d0, Term d1 )
|
|
{
|
|
CACHE_REGS
|
|
tr_fr_ptr trp, trp0 = TR;
|
|
|
|
if (!unifiable(d0,d1)) {
|
|
return FALSE;
|
|
}
|
|
trp = TR;
|
|
while (trp != trp0) {
|
|
Term t;
|
|
|
|
--trp;
|
|
t = TrailTerm(trp);
|
|
RESET_VARIABLE(t);
|
|
}
|
|
return TRUE;
|
|
}
|
|
|
|
void
|
|
Yap_InitUnify(void)
|
|
{
|
|
CACHE_REGS
|
|
Term cm = CurrentModule;
|
|
Yap_InitCPred("unify_with_occurs_check", 2, p_ocunify, SafePredFlag);
|
|
/** @pred unify_with_occurs_check(?T1,?T2) is iso
|
|
|
|
|
|
Obtain the most general unifier of terms _T1_ and _T2_, if there
|
|
is one.
|
|
|
|
This predicate implements the full unification algorithm. An example:n
|
|
|
|
~~~~~{.prolog}
|
|
unify_with_occurs_check(a(X,b,Z),a(X,A,f(B)).
|
|
~~~~~
|
|
will succeed with the bindings `A = b` and `Z = f(B)`. On the
|
|
other hand:
|
|
|
|
~~~~~{.prolog}
|
|
unify_with_occurs_check(a(X,b,Z),a(X,A,f(Z)).
|
|
~~~~~
|
|
would fail, because `Z` is not unifiable with `f(Z)`. Note that
|
|
`(=)/2` would succeed for the previous examples, giving the following
|
|
bindings `A = b` and `Z = f(Z)`.
|
|
|
|
|
|
*/
|
|
Yap_InitCPred("acyclic_term", 1, p_acyclic, SafePredFlag|TestPredFlag);
|
|
/** @pred acyclic_term( _T_) is iso
|
|
|
|
|
|
Succeeds if there are loops in the term _T_, that is, it is an infinite term.
|
|
|
|
|
|
*/
|
|
CurrentModule = TERMS_MODULE;
|
|
Yap_InitCPred("cyclic_term", 1, p_cyclic, SafePredFlag|TestPredFlag);
|
|
Yap_InitCPred("unifiable", 3, p_unifiable, 0);
|
|
CurrentModule = cm;
|
|
}
|
|
|
|
|
|
void
|
|
Yap_InitAbsmi(void)
|
|
{
|
|
/* initialize access to abstract machine instructions */
|
|
#if USE_THREADED_CODE
|
|
Yap_absmi(1);
|
|
InitReverseLookupOpcode();
|
|
#endif
|
|
}
|
|
|
|
void
|
|
Yap_TrimTrail(void)
|
|
{
|
|
CACHE_REGS
|
|
#ifdef saveregs
|
|
#undef saveregs
|
|
#define saveregs()
|
|
#endif
|
|
#ifdef setregs
|
|
#undef setregs
|
|
#define setregs()
|
|
#endif
|
|
#if SHADOW_HB
|
|
register CELL *HBREG = HB;
|
|
#endif
|
|
|
|
#include "trim_trail.h"
|
|
}
|
|
|
|
//! @}
|