#include "term.h"

Contents

• Public Routines
• Public Definitions
• Introduction

Public Routines in File term.c

Index

Details

BOOL all_args_vars(Term t);

int arg_position(Term parent, Term child);

BOOL args_distinct_vars(Term t);

int biggest_variable(Term t);

Term build_binary_term(int sn, Term a1, Term a2);

WARNING: if sn is not a binary symbol, bad things will happen!

Term build_binary_term_safe(char *str, Term a1, Term a2);

If you know the symnum, and you're certain it has arity 2, you can use the faster routine build_binary_term() instead;

Term build_unary_term(int sn, Term a);

WARNING: if sn is not a unary symbol, bad things will happen!

Term build_unary_term_safe(char *str, Term a);

If you know the symnum, and you're certain it has arity 1, you can use the faster routine build_unary_term() instead;

BOOL check_upward_term_links(Term t, void *p);

BOOL contains_skolem_function(Term t);

BOOL contains_skolem_term(Term t);

Plist copy_plist_of_terms(Plist terms);

Term copy_term(Term t);

BOOL eq_term(Term a);

void fprint_term(FILE *fp, Term t);

void fprint_term_mem(FILE *fp, BOOL heading);

void free_term(Term p);

Plist free_vars_term(Term t, Plist vars);

Ilist fsym_set_in_term(Term t);

Term get_rigid_term(char *sym, int arity);

Term get_rigid_term_dangerously(int symnum, int arity);

If you have a similar term, use get_rigid_term_like() instead. If you can afford the time to access the symbol table, use sn_to_str() and get_rigid_term() instead.

Term get_rigid_term_like(Term t);

Term get_variable_term(int var_num);

int greatest_symnum_in_term(Term t);

int greatest_variable(Term t);

BOOL ground_term(Term t);

unsigned hash_term(Term t);

Term int_to_term(int i);

BOOL is_constant(Term t, char *str);

BOOL is_term(Term t, char *str, int arity);

I2list multiset_of_vars(Term t, I2list vars);

I2list multiset_vars(Term t);

Term nat_to_term(int n);

int natural_constant_term(Term t);

int occurrences(Term t, Term target);

BOOL occurs_in(Term t1, Term t2);

void p_term(Term t);

void p_term_mem(void);

Plist plist_of_subterms(Term t);

Ilist position_of_subterm(Term t, Term subterm);

int position_of_term_in_tlist(Term t, Plist lst);

Term renum_vars_recurse(Term t, int vmap[], int max_vars);

This returns a Term instead of being void, in case the given term is itself a variable. (Recall that variables may be shared, so we can't just change a variable's index.

BOOL same_structure(Term a, Term b);

Ilist set_of_ivariables(Term t);

Ilist set_of_ivars(Term t, Ilist ivars);

Plist set_of_variables(Term t);

Plist set_of_vars(Term t, Plist vars);

Term set_vars_recurse(Term t, char *vnames[], int max_vars);

This returns a Term instead of being void, in case the given term is itself becomes a variable.

BOOL skolem_term(Term t);

void sprint_term(String_buf sb, Term t);

Term subst_term(Term t, Term target, Term replacement);

Term subst_var_term(Term t, int symnum, int varnum);

int symbol_count(Term t);

BOOL symbol_in_term(int symnum, Term t);

int symbol_occurrences(Term t, int symnum);

I2list symbols_in_term(Term t, I2list g);

Term term0(char *sym);

Term term1(char *sym, Term arg);

Term term2(char *sym, Term arg1, Term arg2);

Term term_at_pos(Term t, Ilist pos);

int term_depth(Term t);

BOOL term_ident(Term t1, Term t2);

void term_set_variables(Term t, int max_vars);

A fatal error occurs if there are more than max_vars variables.

If you are dealing with clauses, use clause_set_variables() instead.

char *term_symbol(Term t);

BOOL term_to_int(Term t, int *result);

The term representation of a negative integer is the function symbol "-" applied to a nonnegative integer.

BOOL tlist_member(Term t, Plist lst);

BOOL tlist_set(Plist a);

BOOL tlist_subset(Plist a, Plist b);

void upward_term_links(Term t, void *p);

BOOL variables_multisubset(Term a, Term b);

BOOL variables_subset(Term t1, Term t2);

void zap_plist_of_terms(Plist lst);

void zap_term(Term t);

Public Definitions in File term.h

#define MAX_VARS  100   /* max number of (distinct) variables per term */
#define MAX_VNUM  5000  /* maximum variable ID, for array of vars */

#define MAX_VAR   INT_MAX     /* max var ID that fits in sym field of term */
#define MAX_SYM   INT_MAX     /* max ID of any rigid symbol */
#define MAX_ARITY UCHAR_MAX   /* max arity of any term (don't make this big) */

#define FLAGS_TYPE unsigned char  /* for private_flags field of Term */

typedef struct term * Term;     /* Term is a pointer to a term struct */

struct term {
  int            private_symbol; /* const/func/pred/var symbol ID */
  unsigned char  arity;          /* number of auguments */
  FLAGS_TYPE     private_flags;  /* for marking terms in various ways */
  Term           *args;          /* array (size arity) of pointers to args */
  void           *container;     /* containing object */
  union {
    unsigned     id;             /* unique ID, probably for FPA indexing */
    void         *vp;            /* auxiliary pointer */
  } u;
};

/* to check type of term */
#define VARIABLE(t) ((t)->private_symbol >= 0)
#define CONSTANT(t) ((t)->private_symbol < 0 && (t)->arity == 0)
#define COMPLEX(t)  ((t)->private_symbol < 0 && (t)->arity > 0)

/* to get symbol ID from a CONSTANT or COMPLEX term */
#define SYMNUM(t)   (-((t)->private_symbol))

/* to get the variable number of a VARIABLE term */
#define VARNUM(t)   ((t)->private_symbol)

/* to get the arity of a term (VARIABLE terms have arity 0) */
#define ARITY(t)    ((t)->arity)

/* to get the i-th argument of a term (make sure i is in [0..arity-1]) */
#define ARG(t,i)    ((t)->args[i])

/* to get the array of arguments */
#define ARGS(t)    ((t)->args)

Introduction

No term structure sharing is supported at this level of abstraction. (Higher-level packagers can build terms with shared structure if they wish.) Because we envision applications with tens of millions of terms, small size for the individual nodes is important. So we have some overloaded fields, and macros are provided to get some of the information from from term nodes.

There are three types of term, and the Boolean macros VARIABLE(t), CONSTANT(t), and COMPLEX(t) should be used to find out what type a term is. If you have a CONSTANT or COMPLEX term t, you can get its symbol id with SYMNUM(t) (from which you can get other information about the symbol such as the print string and any special properties). If you have a variable t, you can get its index with VARNUM(t), which is a signed integral type in the range [0..MAX_VAR]. Warning: MAX_VAR is a big number---a higher-level unification package will typically have a much smaller MAX_VARS defined for array sizes, because it does array indexing with VARNUM(t).

The macro ARITY(t) gets the arity of a term (constants and variables have arity 0), and ARG(t,i) gets the i-th argument (counting from 0) of a term. When using ARG(t,i), make sure that i is in range [0..ARITY(t)-1], because ARG does not check.

Here is an example of recursing through a term.

int symbol_count(Term t)
{
  int count = 0;
  int i;
  for (i = 0; i < ARITY(t); i++)
    count += symbol_count(ARG(t,i));
  return count+1;
}