#include "btm.h"

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

Public Routines
Public Definitions
Introduction

Public Routines in File btm.c

Index

fprint_btm_mem	match_bt_first	p_btm_mem
match_bt_cancel	match_bt_next	p_btm_state

Details

void fprint_btm_mem(FILE *fp, BOOL heading);

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

void match_bt_cancel(Btm_state bt);

This routine clears any substitution and frees memory associated with a backtrack matching state. This should be called if you get some, but not all, matching substitutions in backtrack matching. See match_bt_first().

Btm_state match_bt_first(Term t1, Context c1, Term t2, int partial);

This is backtracking matching, to be used when there can be more than one unifier. This version handles (any number of) commutative (C) and associative-commutative (AC) function symbols.

The flag `partial' says that if the top level is AC, then not all arguments of t2 have to be matched. The non-matched args are put in c1->partial_term. Partial matches are allowed for the top level only. This is useful for AC rewriting.

If any AC terms are in t1 or t2, then both t1 and t2 should be in `ac_canonical()' form before the call, that is, AC terms are right associated and sorted. C terms are in t1 or t2 need not be c_canonical. (Commutatvie matching is primitive, and you can get duplicate unifiers.)

Get first matching substitution. Return position for match_bt_next() calls. Here is an example. Assume we have terms t1 and t2.

  {
    Context c1 = get_context();
    Btm_state bt = match_bt_first(t1, c1, t2, 0);
    while (bt != NULL) {
        Term t3 = apply(t1, c1);
        zap_term(t3);
        bt = match_bt_next(bt);
        }
    free_context(c1);
  }

If you quit before NULL is returned, call match_bt_cancel(bt) to clear substitutions and free memory.

Btm_state match_bt_next(Btm_state bt1);

This routine gets the next matching substitution. See match_bt_first() for details.

void p_btm_mem();

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

void p_btm_state(Btm_state bt);

This routine prints (to stdout) a Btm_state. It is not pretty.

Public Definitions in File btm.h

typedef struct btm_state * Btm_state;

Introduction