#include "btu.h"

This page has information from files btu.h and btu.c.

Public Routines
Public Definitions
Introduction

Public Routines in File btu.c

Index

fprint_btu_mem	p_btu_mem	unify_bt_first
p_bt_tree	unify_bt_cancel	unify_bt_next

Details

void fprint_btu_mem(FILE *fp, BOOL heading);

This routine prints (to FILE *fp) memory usage statistics for data types associated with the btu package. The Boolean argument heading tells whether to print a heading on the table.

void p_bt_tree(Btu_state bt, int n);

This (recursive) routine prints (to stdout) a backtrack unification state. Parameter n should be 0 on the top call.

void p_btu_mem();

This routine prints (to stdout) memory usage statistics for data types associated with the btu package.

void unify_bt_cancel(Btu_state bt);

This routine frees the memory associated with a state in backtrack unification. This should be called if you decide to get some, but not all, unifiers from unify_bt_first() and unify_bt_next().

Btu_state unify_bt_first(Term t1, Context c1,
			Term t2, Context c2);

This routine gets the first unifier for a pair of terms and returns a Btu_state (or NULL if there are no unifiers) to be used for calls to unify_bt_next() to get the rest of the unifiers. This unification handles associative-commutative (AC) and commutative (C) symbols, so there can be more than one unifier. (Commutatvie unification is primitive, and you can get duplicate unifiers.)

This is called "backtrack unification", because the unifiers are constructed incrementally, as needed. Here is an example of how to do it. Assume we have Terms t1 and t2.

  {
    Context c1 = get_context();
    Context c2 = get_context();
    bt = unify_bt_first(t1, c1, t2, c2);
    while (bt != NULL) {
      t3 = apply(t1, c1);
      t4 = apply(t2, c2);
      
      zap_term(t4);
      bt = unify_bt_next(bt);
      }
    free_context(c1);
    free_context(c2);
  }

The routine unify_bt_next() takes care of clearing the substitutions before getting the next unifier. If you decide not to get all of the unifiers, you should call unify_bt_cancel() to free the memory used by the Btu_state.

If there are no AC or C symbols, it is a little bit faster to use unify() (ordinary unification) instead of backtrack unification.

Btu_state unify_bt_next(Btu_state bt1);

This routine gets the next unifier for "backtrack unification". See unify_bt_first() for an explanation.

Public Definitions in File btu.h

typedef struct btu_state * Btu_state;

Introduction