#include "mindex.h"

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

Public Routines
Public Definitions
Introduction

Public Routines in File mindex.c

Index

fprint_mindex	mindex_empty	mindex_retrieve_cancel	mindex_update
fprint_mindex_mem	mindex_free	mindex_retrieve_first	p_mindex_mem
mindex_destroy	mindex_init	mindex_retrieve_next

Details

void fprint_mindex(FILE *fp, Mindex mdx);

This routine prints (to FILE *fp) Mindex mdx.

void fprint_mindex_mem(FILE *fp, BOOL heading);

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

void mindex_destroy(Mindex mdx);

This frees all the memory associated with an Mindex. Do not refer to the Mindex after calling this routine.

BOOL mindex_empty(Mindex mdx);

This Boolean routine checks if an Mindex is empty, that is, has no terms. It must exist (be non-NULL).

void mindex_free(Mindex mdx);

This routine frees an empty Mindex. (If the Mindex is not empty, nothing happens.)

Mindex mindex_init(Mindextype mtype, Uniftype utype, int fpa_depth);

This routine allocates and returns an (empty) Mindex, which is used to retrieve unifiable terms.

index_type: {LINEAR, FPA, DISCRIM_WILD, DISCRIM_BIND}
unif_type: {ORDINARY_UNIF, BACKTRACK_UNIF}
fpa_depth: depth of FPA indexing (ignored for other index types).

Types of retrieval. LINEAR and FPA indexes support all types of retrieval (FPA is slow for GENERALIZATION). DISCRIM_WILD and DISCRIM_BIND indexes support GENERALIZATION retrieval only. See mindex_retrieve_first().

Associative-commutative (AC) and commutative (C) symbols. DISCRIM_BIND does not support AC symbols. All other combinations are okay. If you have any AC or C symbols, you must specify unif_type BACKTRACK_UNIF. (BACKTRACK_UNIF is also okay with no AC or C symbols, but it is a little bit slower than ORDINARY_UNIF.)

AC symbols must be declared (with set_assoc_comm()) before calling mindex_update(). C symbols need not be declared before mindex_update(), but they must be declared (with set_commutative()) before calling mindex_retrieve_first().

void mindex_retrieve_cancel(Mindex_pos pos);

This routine should be called if you get some, but not all, answers to a query. For example, if you need only one answer you can do something like the following:

{
  Mindex_pos pos;
  Term t2;
  Context cf = get_context();
  
  t2 = mindex_retrieve_first(t, mdx, GENERALIZATION, (Context) NULL, cf, &pos);
  if (t2 != NULL) {
    printf("we found a mate!\n");
    mindex_retrieve_cancel(pos);
  }
  else
    printf("no answer\n");
  free_context(cf);
}

If you fail to call this routine, then the memory associated with an Mindex_pos will be forever lost, that is, you will have a memory leak.

Term mindex_retrieve_first(Term t, Mindex mdx, Querytype qtype,
			   Context query_subst, Context found_subst,
			   BOOL partial_match,
			   Mindex_pos *ppos);

This routine finds and returns the first answer to a query (returning NULL if there are no answers).

Term t: the query term;
Mindex mdx: the Mindex;
int query_type: UNIFY, INSTANCE, GENERALIZATION, VARIANT, or IDENTICAL;
Context query_subst: subsitution for variables in query term t; this can be NULL for GENERALIZATION, and IDENTICAL;
Context found_subst: subsitution for variables in the answer term; this can be NULL for INSTANCE, VARIANT, and IDENTICAL;
BOOL partial_match: If TRUE, then for GENERALIZATION, with BACKTRACK_UNIF, when t has an AC symbol at the root, allow the retrieved term to match only part of t, with the remainder of the retrieved term placed in fond_subst->partial_term. This is used for AC rewriting, for example, to let x+x=x rewrite a+a+b.
Mindex_pos *ppos (output parameter): If an answer is returned, this address is set to a pointer to a structure that holds the position so you can get the rest of the answers.

If you ask for a type of retrieval not supported by the Mindex mdx, you will get no answers (and no error message).

Here is an example of how to retrieve all answers. Assume we have Term t and Mindex mdx.

{
  Mindex_pos pos;
  Term t2;
  Context cq = get_context();
  Context cf = get_context();
  int n = 0;
  
  t2 = mindex_retrieve_first(t, mdx, UNIFY, cq, cf, FALSE, &pos);
  while (t2 != NULL) {
    t2 = mindex_retrieve_next(pos);
    n++;
  }
  free_context(cq);
  free_context(cf);
  printf("there are %d mates\n", n);
}

Term mindex_retrieve_next(Mindex_pos pos);

This routine finds and returns the next answer to a query. See mindex_retrieve_first() for an explanation.

void mindex_update(Mindex mdx, Term t, Indexop op);

This routine inserts (op==INSERT) or deletes (op==DELETE) a Term t into/from an Mindex mdx.

It is your responsibility to remember that t is in the index, because we don't currently have a routine "mindex_member()".

void p_mindex_mem();

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

Public Definitions in File mindex.h

/* types of index */

typedef enum { LINEAR,
	       FPA,
	       DISCRIM_WILD,
	       DISCRIM_BIND
             } Mindextype;

/* types of unification */

typedef enum { ORDINARY_UNIF,
	       BACKTRACK_UNIF
             } Uniftype;

typedef struct mindex * Mindex;
typedef struct mindex_pos * Mindex_pos;

struct mindex {
  Mindextype index_type;
  Uniftype   unif_type;

  /* FPA */
  Fpa_index  fpa;

  /* LINEAR */
  Plist   linear_first;
  Plist   linear_last;

  /* DISCRIM_WILD and DISCRIM_BIND */
  Discrim   discrim_tree;

  Mindex     next;  /* for avail list */
};

Introduction

This is an indexing/unification package to store terms and to retrieve unifiable terms. (It is really just an interface to the various indexing and unification packages.) Several types of indexing and unification are supported. When you allocate an index (with mindex_init()), you specify the type of index and the type of unification.

Types of Retrieval

UNIFY, INSTANCE, GENERALIZATION, VARIANT, IDENTICAL.

Types of Unification

Associative-commutative (AC) and commutative/symmetric (C) symbols are supported in most cases. If you have any AC or C symbols, you must use backtrack unification, which handles more than one unifier for a pair of terms; otherwise, you can use ordinary unification, which assumes at most one unifier for a pair of terms. (For the empty theory, ordinary unification is a bit faster than backtrack unification.)

Types of Indexing