Prolog unification is not a complete implementation. More...

Detailed Description

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 rational tree

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

Class Documentation

◆ unify_with_occurs_check/2

class unify_with_occurs_check/2

Definition at line 997 of file unify.c.

◆ acyclic_term/1

class acyclic_term/1

Macro Definition Documentation

◆ HAS_CACHE_REGS

#define HAS_CACHE_REGS 1

Definition at line 48 of file unify.c.

◆ IN_UNIFY_C

#define IN_UNIFY_C 1

Definition at line 46 of file unify.c.

◆ tovisit_base [1/2]

#define tovisit_base ((struct v_record *)AuxSp)

Definition at line 60 of file unify.c.

◆ tovisit_base [2/2]

#define tovisit_base ((struct v_record *)AuxSp)

Definition at line 60 of file unify.c.

◆ UnifyAndTrailGlobalCells

#define UnifyAndTrailGlobalCells	(	a,
		b
	)

Value:

     if((a) > (b)) {                                                  \
       *(a) = (CELL)(b);                                              \
        DO_TRAIL((a), (CELL)(b));                                     \
     } else if((a) < (b)){                                            \
       *(b) = (CELL)(a);                                              \
        DO_TRAIL((b), (CELL)(a));                                     \
     }

Definition at line 643 of file unify.c.

Function Documentation

◆ Yap_InitAbsmi()

void Yap_InitAbsmi ( void )

Definition at line 1036 of file unify.c.

◆ Yap_IsAcyclicTerm()

bool Yap_IsAcyclicTerm ( Term t )

Definition at line 466 of file unify.c.

◆ Yap_IUnify()

int Yap_IUnify	(	register CELL	d0,
		register CELL	d1
	)

Definition at line 481 of file unify.c.

◆ Yap_rational_tree_loop()

int Yap_rational_tree_loop	(	CELL *	pt0,
		CELL *	pt0_end,
		CELL **	tovisit,
		CELL **	tovisit_max
	)

Definition at line 63 of file unify.c.

◆ Yap_TrimTrail()

void Yap_TrimTrail ( void )

Definition at line 1046 of file unify.c.

◆ Yap_Unifiable()

int Yap_Unifiable	(	Term	d0,
		Term	d1
	)

Definition at line 972 of file unify.c.

Macros
#define	IN_UNIFY_C 1

#define	HAS_CACHE_REGS 1

#define	tovisit_base ((struct v_record *)AuxSp)

#define	tovisit_base ((struct v_record *)AuxSp)

#define	UnifyAndTrailGlobalCells(a, b)

Functions
int	Yap_rational_tree_loop (CELL , CELL , CELL , CELL )

bool	Yap_IsAcyclicTerm (Term t)

int	Yap_IUnify (register CELL d0, register CELL d1)

int	Yap_Unifiable (Term d0, Term d1)

void	Yap_InitAbsmi (void)

void	Yap_TrimTrail (void)