void assign_order_method(Order_method method);
BOOL flat_greater(Flatterm alpha, Flatterm beta, BOOL lex_order_vars);
int flat_kbo_weight(Flatterm f);
BOOL flat_lrpo(Flatterm s, Flatterm t, BOOL lex_order_vars);
Ordertype flatterm_compare_vr(Flatterm a, Flatterm b);This routine compares two flatterms. variable < nonvariable; within type, the order is by VARNUM and lexigocgaphic by symbol precedence. The range of return values is
BOOL greater_multiset_current_ordering(Term t1, Term t2);
void init_kbo_weights(Plist weights);Plist should be a list of terms, e.g., a=3, g=0. Symbols are written as constants; arity is deduced from the symbol table.
BOOL kbo(Term alpha, Term beta, BOOL lex_order_vars);Is alpha kbo-greater-than beta?
int kbo_weight(Term t);
BOOL lrpo(Term s, Term t, BOOL lex_order_vars);This routine checks if Term s > Term t in the Lexicographic Recursive Path Ordering (LRPO), also known as Recursive Path Ordering with Status (RPOS).
Function symbols can have either multiset or left-to-right status (see symbols.c). If all symbols are multiset, this reduces to the Recursive Path Ordering (RPO). If all symbols are left-to-right, this reduces to Lexicographic Path Ordering (LPO).
BOOL lrpo_multiset(Term t1, Term t2, BOOL lex_order_vars);This routine
Ordertype term_compare_ncv(Term t1, Term t2);This routine compares two terms. The ordering is total: CONSTANT < COMPLEX < VARIABLE; within type, the order is by VARNUM and lexigocgaphic by SYMNUM. The range of return values is
Ordertype term_compare_vcp(Term t1, Term t2);This routine compares two terms. The ordering is total: VARIABLE < CONSTANT < COMPLEX; within type, the order is by VARNUM and lexigocgaphic by SYMNUM. The range of return values is
Ordertype term_compare_vr(Term t1, Term t2);This routine compares two terms. variable < nonvariable; within type, the order is by VARNUM and lexigocgaphic by symbol precedence. The range of return values is
BOOL term_greater(Term alpha, Term beta, BOOL lex_order_vars);Is alpha > beta in the current term ordering? (LPR, RPO, KBO)
Ordertype term_order(Term alpha, Term beta);Compare two terms with the current term ordering (LPR, RPO, KBO) Return GREATER_THAN, LESS_THAN, or NOT_COMPARABLE.
/* Term ordering method */
typedef enum { LRPO_METHOD,
LPO_METHOD,
RPO_METHOD,
KBO_METHOD
} Order_method;