andr3/scyther
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

- Improved code for new preferred order swapping of substitutions. Also

Browse Source 
included more comments.
This commit is contained in:
ccremers 2005-10-08 20:22:24 +00:00
parent 2e495099bb
commit 2ead7ab2ff
1 changed files with 33 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

42
src/mgu.c
View File

@ -139,24 +139,22 @@ termMguTerm (Term t1, Term t2)
} }
} }
/* symmetrical tests for single variable */
/* /*
* I broke symmetry later, for the special case where both are unbound * Distinguish a special case where both are unbound variables that will be
* variables that will be connected, and I want to give one priority over the * connected, and I want to give one priority over the other for readability.
* other for readability. *
* Because t1 and t2 have been deVar'd means that if they are variables, they
* are also unbound.
*/ */
if (realTermVariable (t2))
if (realTermVariable (t1) && realTermVariable (t2) && goodsubst (t1, t2))
{ {
if (termSubTerm (t1, t2) || !goodsubst (t2, t1)) /* Both are unbound variables. Decide.
return MGUFAIL; *
else * The plan: t1->subst will point to t2. But maybe we prefer the other
{ * way around?
// Symmetry break starts here */
if (isTermVariable (t1)) if (preferSubstitutionOrder (t2, t1))
{
// Both are variables. Decide.
// The plan: t2->subst will point to t1. Is that desired?
if (preferSubstitutionOrder (t1,t2))
{ {
Term t3; Term t3;
@ -165,8 +163,22 @@ termMguTerm (Term t1, Term t2)
t1 = t2; t1 = t2;
t2 = t3; t2 = t3;
} }
t1->subst = t2;
#ifdef DEBUG
showSubst (t1);
#endif
return termlistAdd (NULL, t1);
} }
/* symmetrical tests for single variable.
*/
if (realTermVariable (t2))
{
if (termSubTerm (t1, t2) || !goodsubst (t2, t1))
return MGUFAIL;
else
{
t2->subst = t1; t2->subst = t1;
#ifdef DEBUG #ifdef DEBUG
showSubst (t2); showSubst (t2);