diogo/yap-6.3
Archived
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

use unification, not wakeup, to verify if two terms are unifiable. Fixes Ulrich Neumerkel #306

Browse Source 
Also renitent
This commit is contained in:
Vítor Santos Costa 2015-11-09 11:25:55 +00:00
parent 50c04116c8
commit ca81e5d8ea
2 changed files with 229 additions and 237 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

142
C/corout.c
View File

@ -30,23 +30,20 @@ static char SccsId[]="%W% %G%";
#ifdef COROUTINING
/* check if variable was there */
static Term AddVarIfNotThere(Term var , Term dest USES_REGS)
{
static Term AddVarIfNotThere(Term var, Term dest USES_REGS) {
Term test = dest;
while (test != TermNil) {
if ((RepPair(test))[0] == var) return(dest);
else test = (RepPair(test))[1];
if ((RepPair(test))[0] == var)
return (dest);
else
test = (RepPair(test))[1];
}
return (MkPairTerm(var, dest));
}
/* This routine verifies whether two complex structures can unify. */
static int can_unify_complex(register CELL *pt0,
register CELL *pt0_end,
register CELL *pt1,
Term *Vars USES_REGS)
{
static int can_unify_complex(register CELL *pt0, register CELL *pt0_end,
register CELL *pt1, Term *Vars USES_REGS) {
/* This is really just unification, folks */
tr_fr_ptr saved_TR;
@ -73,39 +70,41 @@ static int can_unify_complex(register CELL *pt0,
if (IsVarTerm(d1)) {
if (d0 != d1) {
/* we need to suspend on both variables ! */
*Vars = AddVarIfNotThere(d0, AddVarIfNotThere(d1,*Vars PASS_REGS) PASS_REGS);
*Vars = AddVarIfNotThere(d0, AddVarIfNotThere(d1, *Vars PASS_REGS)
PASS_REGS);
/* bind the two variables, we would have to do that to unify
them */
if (d1 > d0) { /* youngest */
/* we don't want to wake up goals */
Bind_Global((CELL *)d1, d0);
Bind_Global_NonAtt((CELL *)d1, d0);
} else {
Bind_Global((CELL *)d0, d1);
Bind_Global_NonAtt((CELL *)d0, d1);
}
}
/* continue the loop */
continue;
}
else {
} else {
/* oh no, some more variables! */
*Vars = AddVarIfNotThere(d0, *Vars PASS_REGS);
}
/* now bind it */
Bind_Global((CELL *)d0, d1);
Bind_Global_NonAtt((CELL *)d0, d1);
/* continue the loop */
} else if (IsVarTerm(d1)) {
*Vars = AddVarIfNotThere(d1, *Vars PASS_REGS);
/* and bind it */
Bind_Global((CELL *)d1, d0);
Bind_Global_NonAtt((CELL *)d1, d0);
/* continue the loop */
} else {
if (d0 == d1) continue;
if (d0 == d1)
continue;
if (IsAtomOrIntTerm(d0) || IsAtomOrIntTerm(d1)) {
if (d0 != d1) goto comparison_failed;
if (d0 != d1)
goto comparison_failed;
/* else continue the loop */
}
else if (IsPairTerm(d0)) {
if (!IsPairTerm(d1)) goto comparison_failed;
} else if (IsPairTerm(d0)) {
if (!IsPairTerm(d1))
goto comparison_failed;
#ifdef RATIONAL_TREES
to_visit[0] = pt0;
to_visit[1] = pt0_end;
@ -126,8 +125,7 @@ static int can_unify_complex(register CELL *pt0,
pt0_end = RepPair(d0) + 1;
pt1 = RepPair(d1) - 1;
continue;
}
else if (IsApplTerm(d0)) {
} else if (IsApplTerm(d0)) {
register Functor f;
register CELL *ap2, *ap3;
if (!IsApplTerm(d1)) {
@ -144,20 +142,26 @@ static int can_unify_complex(register CELL *pt0,
if (IsExtensionFunctor(f)) {
switch ((CELL)f) {
case (CELL) FunctorDBRef:
if (d0 == d1) continue;
if (d0 == d1)
continue;
goto comparison_failed;
case (CELL) FunctorLongInt:
if (ap2[1] == ap3[1]) continue;
if (ap2[1] == ap3[1])
continue;
goto comparison_failed;
case (CELL) FunctorDouble:
if (FloatOfTerm(d0) == FloatOfTerm(d1)) continue;
if (FloatOfTerm(d0) == FloatOfTerm(d1))
continue;
goto comparison_failed;
case (CELL) FunctorString:
if (strcmp((char *)StringOfTerm(d0), (char *)StringOfTerm(d1)) == 0) continue;
if (strcmp((char *)StringOfTerm(d0), (char *)StringOfTerm(d1)) ==
0)
continue;
goto comparison_failed;
#ifdef USE_GMP
case (CELL) FunctorBigInt:
if (Yap_gmp_tcmp_big_big(d0,d1) == 0) continue;
if (Yap_gmp_tcmp_big_big(d0, d1) == 0)
continue;
goto comparison_failed;
#endif /* USE_GMP */
default:
@ -187,9 +191,7 @@ static int can_unify_complex(register CELL *pt0,
continue;
}
}
}
}
/* Do we still have compound terms to visit */
if (to_visit > (CELL **)to_visit_base) {
@ -234,13 +236,16 @@ static int can_unify_complex(register CELL *pt0,
/* restore B, and later HB */
B = saved_B;
HB = saved_HB;
/* untrail all bindings made by IUnify */
while (TR != saved_TR) {
pt1 = (CELL *)(TrailTerm(--TR));
RESET_VARIABLE(pt1);
}
/* the system will take care of TR for me, no need to worry here! */
return (FALSE);
}
static int
can_unify(Term t1, Term t2, Term *Vars USES_REGS)
{
static int can_unify(Term t1, Term t2, Term *Vars USES_REGS) {
t1 = Deref(t1);
t2 = Deref(t2);
if (t1 == t2) {
@ -278,7 +283,8 @@ can_unify(Term t1, Term t2, Term *Vars USES_REGS)
if (IsPairTerm(t2)) {
return (can_unify_complex(RepPair(t1) - 1, RepPair(t1) + 1,
RepPair(t2) - 1, Vars PASS_REGS));
} else return FALSE;
} else
return FALSE;
} else {
Functor f = FunctorOfTerm(t1);
if (f != FunctorOfTerm(t2))
@ -286,20 +292,25 @@ can_unify(Term t1, Term t2, Term *Vars USES_REGS)
if (IsExtensionFunctor(f)) {
switch ((CELL)f) {
case (CELL) FunctorDBRef:
if (t1 == t2) return FALSE;
if (t1 == t2)
return FALSE;
return FALSE;
case (CELL) FunctorLongInt:
if (RepAppl(t1)[1] == RepAppl(t2)[1]) return(TRUE);
if (RepAppl(t1)[1] == RepAppl(t2)[1])
return (TRUE);
return FALSE;
case (CELL) FunctorString:
if (strcmp((char *)StringOfTerm(t1), (char *)StringOfTerm(t2)) == 0) return(TRUE);
if (strcmp((char *)StringOfTerm(t1), (char *)StringOfTerm(t2)) == 0)
return (TRUE);
return FALSE;
case (CELL) FunctorDouble:
if (FloatOfTerm(t1) == FloatOfTerm(t2)) return(TRUE);
if (FloatOfTerm(t1) == FloatOfTerm(t2))
return (TRUE);
return FALSE;
#ifdef USE_GMP
case (CELL) FunctorBigInt:
if (Yap_gmp_tcmp_big_big(t1,t2) == 0) return(TRUE);
if (Yap_gmp_tcmp_big_big(t1, t2) == 0)
return (TRUE);
return (FALSE);
#endif /* USE_GMP */
default:
@ -307,17 +318,14 @@ can_unify(Term t1, Term t2, Term *Vars USES_REGS)
}
}
/* Two complex terms with the same functor */
return can_unify_complex(RepAppl(t1),
RepAppl(t1)+ArityOfFunctor(f),
return can_unify_complex(RepAppl(t1), RepAppl(t1) + ArityOfFunctor(f),
RepAppl(t2), Vars PASS_REGS);
}
}
/* This routine verifies whether a complex has variables. */
static int non_ground_complex(register CELL *pt0,
register CELL *pt0_end,
Term *Var USES_REGS)
{
static int non_ground_complex(register CELL *pt0, register CELL *pt0_end,
Term *Var USES_REGS) {
register CELL **to_visit = (CELL **)Yap_PreAllocCodeSpace();
CELL **to_visit_base = to_visit;
@ -351,8 +359,7 @@ static int non_ground_complex(register CELL *pt0,
#endif
pt0 = RepPair(d0) - 1;
pt0_end = RepPair(d0) + 1;
}
else if (IsApplTerm(d0)) {
} else if (IsApplTerm(d0)) {
register Functor f;
register CELL *ap2;
@ -433,9 +440,7 @@ static int non_ground_complex(register CELL *pt0,
return -1;
}
static int
non_ground(Term t, Term *Var USES_REGS)
{
static int non_ground(Term t, Term *Var USES_REGS) {
int out = -1;
while (out < 0) {
t = Deref(t);
@ -473,8 +478,7 @@ non_ground(Term t, Term *Var USES_REGS)
/* check whether the two terms unify and return what variables should
be bound before the terms are exactly equal */
static Int p_can_unify( USES_REGS1 )
{
static Int p_can_unify(USES_REGS1) {
#ifdef COROUTINING
Term r = TermNil;
if (!can_unify(ARG1, ARG2, &r PASS_REGS))
@ -486,8 +490,7 @@ static Int p_can_unify( USES_REGS1 )
}
/* if the term is not ground return a variable in the term */
static Int p_non_ground( USES_REGS1 )
{
static Int p_non_ground(USES_REGS1) {
#ifdef COROUTINING
Term r = TermNil;
if (!non_ground(ARG1, &r PASS_REGS))
@ -499,8 +502,7 @@ static Int p_non_ground( USES_REGS1 )
}
/* if the term is not ground return a variable in the term */
static Int p_coroutining( USES_REGS1 )
{
static Int p_coroutining(USES_REGS1) {
#ifdef COROUTINING
return (TRUE);
#else
@ -509,21 +511,18 @@ static Int p_coroutining( USES_REGS1 )
}
#if COROUTINING
static Term
ListOfWokenGoals( USES_REGS1 ) {
static Term ListOfWokenGoals(USES_REGS1) {
return Yap_ReadTimedVar(LOCAL_WokenGoals);
}
Term
Yap_ListOfWokenGoals(void) {
Term Yap_ListOfWokenGoals(void) {
CACHE_REGS
return ListOfWokenGoals(PASS_REGS1);
}
#endif
/* return a list of awoken goals */
static Int p_awoken_goals( USES_REGS1 )
{
static Int p_awoken_goals(USES_REGS1) {
#ifdef COROUTINING
Term WGs = Yap_ReadTimedVar(LOCAL_WokenGoals);
if (WGs == TermNil) {
@ -537,9 +536,7 @@ static Int p_awoken_goals( USES_REGS1 )
#endif
}
static Int
p_yap_has_rational_trees( USES_REGS1 )
{
static Int p_yap_has_rational_trees(USES_REGS1) {
#if RATIONAL_TREES
return TRUE;
#else
@ -547,9 +544,7 @@ p_yap_has_rational_trees( USES_REGS1 )
#endif
}
static Int
p_yap_has_coroutining( USES_REGS1 )
{
static Int p_yap_has_coroutining(USES_REGS1) {
#if COROUTINING
return TRUE;
#else
@ -557,9 +552,7 @@ p_yap_has_coroutining( USES_REGS1 )
#endif
}
void
Yap_InitCoroutPreds( void )
{
void Yap_InitCoroutPreds(void) {
#ifdef COROUTINING
Atom at;
PredEntry *pred;
@ -569,12 +562,11 @@ Yap_InitCoroutPreds( void )
WakeUpCode = pred;
#endif
Yap_InitAttVarPreds();
Yap_InitCPred("$yap_has_rational_trees", 0, p_yap_has_rational_trees, SafePredFlag);
Yap_InitCPred("$yap_has_rational_trees", 0, p_yap_has_rational_trees,
SafePredFlag);
Yap_InitCPred("$yap_has_coroutining", 0, p_yap_has_coroutining, SafePredFlag);
Yap_InitCPred("$can_unify", 3, p_can_unify, SafePredFlag);
Yap_InitCPred("$non_ground", 2, p_non_ground, SafePredFlag);
Yap_InitCPred("$coroutining", 0, p_coroutining, SafePredFlag);
Yap_InitCPred("$awoken_goals", 1, p_awoken_goals, SafePredFlag);
}