# #include "symbols.h"

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

## Contents

- Public Routines
- Public Definitions
- Introduction

## Public Routines in File symbols.c

#### Index

add_new_symbols | function_or_relation_sn | not_sym | set_variable_style
add_skolems_to_preliminary_precedence | function_symbol | not_symnum | skolem_check
all_function_symbols | gen_new_symbol | or_sym | skolem_reset
all_relation_symbols | get_operation_symbol | or_symnum | skolem_symbols
all_sym | get_symbol_type | p_sym | sn_to_arity
all_symbols_lrpo_status | greatest_symnum | p_syms | sn_to_kb_wt
and_sym | has_greatest_precedence | parse_type_to_str | sn_to_lex_val
arity_check | iff_sym | preliminary_lex_compare | sn_to_lrpo_status
assign_greatest_precedence | imp_sym | print_fsym_precedence | sn_to_occurrences
assoc_comm_symbols | impby_sym | print_kbo_weights | sn_to_str
attrib_sym | is_assoc_comm | print_rsym_precedence | sort_by_lex_val
binary_parse_type | is_commutative | process_lex_list | special_parse_type
clear_parse_type | is_eq_symbol | process_skolem_list | sprint_sym
clear_parse_type_for_all_symbols | is_skolem | quant_sym | str_exists
comm_symbols | is_symbol | relation_symbol | str_to_sn
current_fsym_precedence | is_unfold_symbol | remove_variable_symbols | sym_precedence
current_rsym_precedence | lex_compare_arity_0123 | set_assoc_comm | symbol_for_variable
declare_base_symbols | lex_compare_arity_0213 | set_commutative | symbol_in_use
declare_functions_and_relations | lex_insert_after_initial_constants | set_kb_weight | symbol_with_string
decommission_skolem_symbols | lex_order | set_lex_val | symnums_of_arity
eq_sym | mark_for_new_symbols | set_lrpo_status | syms_with_lex_val
exists_preliminary_precedence | min_lex_val | set_operation_symbol | true_sym
exists_sym | neq_sym | set_parse_type | unary_parse_type
false_sym | new_constant_properties | set_skolem | variable_name
fprint_sym | new_symbols_since_mark | set_skolem_symbols | variable_style
fprint_syms | next_skolem_symbol | set_symbol_type | variable_symbols
fresh_symbol | not_in_preliminary_precedence | set_unfold_symbol | zero_wt_kb

#### Details

    void add_new_symbols(I2list syms);

    void add_skolems_to_preliminary_precedence(void);

If there is a preliminary precedence, add the skolem symbols to it in the following way. For each Skolem symbol of arity-n, add it to Preliminary_precedence just before the first symbol of higher arity (else at the end).

    Ilist all_function_symbols(void);

    Ilist all_relation_symbols(void);

    char *all_sym();

    void all_symbols_lrpo_status(Lrpo_status status);

Assign all symbols the given lrpo status: LRPO_LR_STATUS or LRPO_MULTISET_STATUS.

    char *and_sym();

    Ilist arity_check(Ilist fsyms, Ilist rsyms);

    void assign_greatest_precedence(int symnum);

    BOOL assoc_comm_symbols(void);

This function tells you if any symbol has been declared to be associative-commutative;

    char *attrib_sym();

    BOOL binary_parse_type(char *str, int *precedence, Parsetype *type);

This routine gets the parse/print properties for a binary symbol. If *str is a binary symbol, TRUE is returned and the properties are filled in. If *str is a not a binary symbol, FALSE is returned.

    void clear_parse_type(char *str);

    void clear_parse_type_for_all_symbols(void);

    BOOL comm_symbols(void);

This function tells you if any symbol has been declared to be commutative.

    Ilist current_fsym_precedence();

    Ilist current_rsym_precedence();

    void declare_base_symbols(void);

    void declare_functions_and_relations(Ilist fsyms, Ilist rsyms);

    void decommission_skolem_symbols(void);

For each symbol in the symbol table, if it is marked "skolem", unmark it and set the type to "unspecified".

    char *eq_sym();

    BOOL exists_preliminary_precedence(Symbol_type type);

    char *exists_sym();

    char *false_sym();

    void fprint_sym(FILE *fp, int symnum);

This routine prints (to FILE *fp) the string associated with a symbol ID. A newline is NOT printed.

    void fprint_syms(FILE *fp);

This routine prints (to FILE *fp) the symbol table, including many of the attributes of each symbol.

    int fresh_symbol(char *prefix, int arity);

This routine returns a symbol ID for a new symbol with the given arity. The symbol is made up of the given prefix followed by the smallest natural number that results in a new symbol (regardless of arity). The prefix must be less than MAX_NAME characters.

    int function_or_relation_sn(char *str);

If there is a function or relation symbol in the table with the given string, return the symnum; otherwise return -1. (If there is more than one, the first one found is returned.)

    BOOL function_symbol(int symnum);

    int gen_new_symbol(char *prefix, int arity, Ilist syms);

    char *get_operation_symbol(char *operation);

    Symbol_type get_symbol_type(int symnum);

    int greatest_symnum(void);

This function returns the greatest symnum (symbol ID) currently in use. This can be used if you need to dynamnically allocate an array of objects to be indexed by symnum.

    BOOL has_greatest_precedence(int symnum);

    char *iff_sym();

    char *imp_sym();

    char *impby_sym();

    BOOL is_assoc_comm(int sn);

This function checks if a symbol ID has the associative-commutative property. Note that set_assoc_comm() takes a string, but this routine takes a symbol ID. Recall that str_to_sn() and sn_to_str() translate between the two forms.

    BOOL is_commutative(int sn);

This function checks if a symbol ID has the commutative property. Note that set_commutative() takes a string, but this routine takes a symbol ID. Recall that str_to_sn() and sn_to_str() translate between the two forms.

    BOOL is_eq_symbol(int symnum);

This Boolean routine checks if a given symbol ID is for eq_sym()/2. One could use is_symbol(symnum, eq_sym(), 2) instead, but this should be a bit faster.

    BOOL is_skolem(int symnum);

    BOOL is_symbol(int symnum, char *str, int arity);

This Boolean routine checks if a given symbol ID matches a given (string,arity) pair.

    BOOL is_unfold_symbol(int symnum);

    Ordertype lex_compare_arity_0123(Symbol s1, Symbol s2);

    Ordertype lex_compare_arity_0213(Symbol s1, Symbol s2);

    void lex_insert_after_initial_constants(Ilist syms);

    void lex_order(Ilist fsyms, Ilist rsyms,
    	       I2list fsyms_multiset, I2list rsyms_multiset,
    	       Ordertype (*comp_proc) (Symbol, Symbol));

Assign a total order on lex_vals of (fsyms U rsyms). If a list of strings was previously given to set_preliminary_precedence, that order is maintained for symbols that have those strings. For the other rules, see *comp_proc (lex_compare*).

    void mark_for_new_symbols(void);

    int min_lex_val(void);

    char *neq_sym();

    void new_constant_properties(int sn);

In the symbol table entry for the given symbol number, set type=function, kb_weight=1, lex_val=(after initial constants)

    I2list new_symbols_since_mark(void);

    int next_skolem_symbol(int arity);

This routine returns a fresh symbol ID, which is intended to be used as a Skolem symbol. The symbols are c1, c2, c3, ... for arity 0 (constants) and f1, f2, f3, ... for arity != 0. If some of those symbols already exist in the symbol table (with any arity), they will be skipped.

    Ilist not_in_preliminary_precedence(Ilist syms, Symbol_type type);

    char *not_sym();

    int not_symnum(void);

Return the symnum for not_sym()/1.

    char *or_sym();

    int or_symnum(void);

Return the symnum for or_sym()/2.

    void p_sym(int symnum);

This routine prints (stdout) the string associated with a symbol ID. A newline is NOT printed.

    void p_syms(void);

This routine prints (to stdout) the symbol table, including all of the attributes of each symbol.

    char *parse_type_to_str(Parsetype type);

    Ordertype preliminary_lex_compare(Symbol a, Symbol b);

Compare the given strings with respect to the list of strings given to the set_preliminary_precedence call. Strings without preliminary_precedence are smaller than those with. Two different strings without preliminary_precedence are NOT_COMPARABLE.

Return LESS_THAN, GREATER_THAN, SAME_AS, NOT_COMPARABLE.

    void print_fsym_precedence(FILE *fp);

    void print_kbo_weights(FILE *fp);

    void print_rsym_precedence(FILE *fp);

    void process_lex_list(Plist lex_strings, Ilist syms, Symbol_type type);

    void process_skolem_list(Plist skolem_strings, Ilist fsyms);

    char *quant_sym();

    BOOL relation_symbol(int symnum);

    Ilist remove_variable_symbols(Ilist syms);

Given a Plist of symbols (symnums), remove the ones that are correspond to variables.

    void set_assoc_comm(char *str, BOOL set);

This routine declares a string to be a (binary) symbol with the logical property "associative-commutative". This property is used for AC unification/matching/identity. (If you wish to print AC expressions without parentheses, see set_parse_type().)

    void set_commutative(char *str, BOOL set);

This routine declares a string to be a (binary) symbol with the logical property "commutative". This property is used for commutative unification/matching/identity.

    void set_kb_weight(int symnum, int weight);

    void set_lex_val(int symnum, int lex_val);

This routine is used to assign a lexical value to a symbol. The value can be retrieved later with sn_to_lex_val();

    void set_lrpo_status(int symnum, Lrpo_status status);

    void set_operation_symbol(char *operation, char *symbol);

    void set_parse_type(char *str, int precedence, Parsetype type);

This routine sets the parse/print properties of a binary or unary symbol. The types for binary infix symbols are INFIX_LEFT, INFIX_RIGHT, INFIX. The types for prefix unary symbols are PREFIX, PREFIX_PAREN. The types for postfix unary symbols are POSTFIX, POSTFIX_PAREN.

If the precedence is out of range [MIN_PRECEDENCE ... MAX_PRECEDENCE], a fatal error occurs.

    void set_skolem(int symnum);

This routine declares that a symbol is a Skolem function (or constant).

    void set_skolem_symbols(Ilist symnums);

    void set_symbol_type(int symnum, Symbol_type type);

    void set_unfold_symbol(int symnum);

This routine declares that a symbol is a Skolem function (or constant).

    void set_variable_style(Variable_style style);

This routine determines how variables are parsed and printed.

    void skolem_check(BOOL flag);

    void skolem_reset(void);

Reset the Skolem symbol counters (constant and function) to 1.

    Ilist skolem_symbols(void);

Return the list of SYMNUMs (increasing) that have been declared to be Skolem symbols.

    int sn_to_arity(int symnum);

This routine returns the arity associated with a symbol ID.

    int sn_to_kb_wt(int symnum);

This routine returns the Knuth-Bendix weight associated with a symbol ID.

    int sn_to_lex_val(int sn);

This routine returns the lexical value associated with a symbol ID. The default value is INT_MAX. If the symbol ID is not valid, INT_MIN is returned.

    Lrpo_status sn_to_lrpo_status(int sn);

This routine returns the LRPO status associated with a symbol ID. The default value is LRPO_LR_STATUS. See order.h for the possible values. If the symbol ID is not valid, 0 is returned.

    int sn_to_occurrences(int symnum);

This routine returns the occurrences associated with a symbol ID.

    char *sn_to_str(int symnum);

This routine returns the string assocated with a symbol ID.

    Ilist sort_by_lex_val(Ilist p);

    int special_parse_type(char *str);

Is the string a unary or binary "special_parse_type" (e.g., PREFIX or INFIX)? If so, return the arity; otherwise return -1.

    void sprint_sym(String_buf sb, int symnum);

This routine appends, to String_buf sb, the string associated with a symbol ID. A newline is NOT printed.

    BOOL str_exists(char *str);

This function checks if the given string occurs in the symbol table (with any arity). This should be used judiciously, because the whole table is scanned.

    int str_to_sn(char *str, int arity);

This routine takes a string and an arity, and returns an integer identifier for the pair. If the pair is not already in the symbol table, a new entry is inserted into the table. A pair, say ("f",2), is sometimes written as f/2, which is a different symbol from f/3. There is no limit on the length of the string (which is copied).

    Ordertype sym_precedence(int symnum_1, int symnum_2);

This routine compares two symbol IDs by looking at their lex_val in the symbol table. The range of return values is
{SAME_AS, GREATER_THAN, LESS_THAN, NOT_COMPARABLE}.

    void symbol_for_variable(char *str, int varnum);

Given a pointer to a string and a variable index, fill in the string with the variable symbol. The variable symbol is determined by the current variable style (standard, prolog, integer, etc.), which can be changed with set_variable_style().

    BOOL symbol_in_use(char *str);

    int symbol_with_string(Ilist syms, char *str);

    Ilist symnums_of_arity(Ilist p, int i);

    Ilist syms_with_lex_val(void);

Return an Ilist containing symnums of symbols to which lex_vals have been assigned.

    char *true_sym(void);

    BOOL unary_parse_type(char *str, int *precedence, Parsetype *type);

This routine gets the parse/print properties for a unary symbol. If *str is a unary symbol, TRUE is returned and the properties are filled in. If *str is a not a unary symbol, FALSE is returned.

    BOOL variable_name(char *s);

Is the given name a variable? Formulas can have free variables (not explicitly quantified), so we have a rule to distinguish variables from constants. This is it.

    Variable_style variable_style(void);

This routine gives the current variable style.

    Ilist variable_symbols(Ilist syms);

Given a Plist of symbols (symnums), return a (new) list of the symnums that correspond to variables.

    BOOL zero_wt_kb(void);

Is there already a symbol with KB weight 0?

## Public Definitions in File symbols.h

    /* maximum number of chars in string part of symbol (includes '\0') */

    #define MAX_NAME      51

    /* parse/print properties of symbols */

    typedef enum {NOTHING_SPECIAL,
    	      INFIX,         /* xfx */
    	      INFIX_LEFT ,   /* yfx */
    	      INFIX_RIGHT,   /* xfy */
    	      PREFIX_PAREN,  /* fx  */
    	      PREFIX,        /* fy  */
    	      POSTFIX_PAREN, /* xf  */
    	      POSTFIX        /* yf  */
                 } Parsetype;

    #define MIN_PRECEDENCE      1
    #define MAX_PRECEDENCE    999

    /* Function/relation properties of symbols */

    typedef enum { UNSPECIFIED_SYMBOL,
    	       FUNCTION_SYMBOL,
    	       PREDICATE_SYMBOL
                 } Symbol_type;

    /* Unification properties of symbols */

    typedef enum { EMPTY_THEORY,
    	       COMMUTE,
    	       ASSOC_COMMUTE
                 } Unif_theory;

    /* LRPO status */

    typedef enum { LRPO_LR_STATUS,
    	       LRPO_MULTISET_STATUS
                 } Lrpo_status;

    /* Variable style */

    typedef enum { STANDARD_STYLE,      /* x,y,z,... */
    	       PROLOG_STYLE,        /* A,B,C,... */
    	       INTEGER_STYLE        /* 0,1,2,... */
                 } Variable_style;

    typedef struct symbol * Symbol;

## Introduction

This collection of routines manages the global symbol table. Each symbol is a pair (string,arity) and has a unique ID number. For example, ("f",2), sometimes written f/2, is a different symbol from f/3.

These symbols are used mostly as constant, function, and predicate symbols, but they can be used for variables and other things as well.

The symbol table routines call malloc() and free() directly. The LADR memory package (tp_alloc()) is not used.