#include "symbols.h"

Contents

• Public Routines
• Public Definitions
• Introduction

Public Routines in File symbols.c

Index

Details

void add_new_symbols(I2list syms);

void add_skolems_to_preliminary_precedence(void);

Ilist all_function_symbols(void);

Ilist all_relation_symbols(void);

char *all_sym();

void all_symbols_lrpo_status(Lrpo_status status);

char *and_sym();

Ilist arity_check(Ilist fsyms, Ilist rsyms);

void assign_greatest_precedence(int symnum);

BOOL assoc_comm_symbols(void);

char *attrib_sym();

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

void clear_parse_type(char *str);

void clear_parse_type_for_all_symbols(void);

BOOL comm_symbols(void);

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);

char *eq_sym();

BOOL exists_preliminary_precedence(Symbol_type type);

char *exists_sym();

char *false_sym();

void fprint_sym(FILE *fp, int symnum);

void fprint_syms(FILE *fp);

int fresh_symbol(char *prefix, int arity);

int function_or_relation_sn(char *str);

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);

BOOL has_greatest_precedence(int symnum);

char *iff_sym();

char *imp_sym();

char *impby_sym();

BOOL is_assoc_comm(int sn);

BOOL is_commutative(int sn);

BOOL is_eq_symbol(int symnum);

BOOL is_skolem(int symnum);

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

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));

void mark_for_new_symbols(void);

int min_lex_val(void);

char *neq_sym();

void new_constant_properties(int sn);

I2list new_symbols_since_mark(void);

int next_skolem_symbol(int arity);

Ilist not_in_preliminary_precedence(Ilist syms, Symbol_type type);

char *not_sym();

int not_symnum(void);

char *or_sym();

int or_symnum(void);

void p_sym(int symnum);

void p_syms(void);

char *parse_type_to_str(Parsetype type);

Ordertype preliminary_lex_compare(Symbol a, Symbol b);

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);

void set_assoc_comm(char *str, BOOL set);

void set_commutative(char *str, BOOL set);

void set_kb_weight(int symnum, int weight);

void set_lex_val(int symnum, int 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);

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

void set_skolem(int symnum);

void set_skolem_symbols(Ilist symnums);

void set_symbol_type(int symnum, Symbol_type type);

void set_unfold_symbol(int symnum);

void set_variable_style(Variable_style style);

void skolem_check(BOOL flag);

void skolem_reset(void);

Ilist skolem_symbols(void);

int sn_to_arity(int symnum);

int sn_to_kb_wt(int symnum);

int sn_to_lex_val(int sn);

Lrpo_status sn_to_lrpo_status(int sn);

int sn_to_occurrences(int symnum);

char *sn_to_str(int symnum);

Ilist sort_by_lex_val(Ilist p);

int special_parse_type(char *str);

void sprint_sym(String_buf sb, int symnum);

BOOL str_exists(char *str);

int str_to_sn(char *str, int arity);

Ordertype sym_precedence(int symnum_1, int symnum_2);

void symbol_for_variable(char *str, int varnum);

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);

char *true_sym(void);

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

BOOL variable_name(char *s);

Variable_style variable_style(void);

Ilist variable_symbols(Ilist syms);

BOOL zero_wt_kb(void);

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

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.