Topform build_reflex_eq(void);
BOOL eq_tautology(Topform c);This routine returns TRUE if the clause has any literals of the form t=t.
int equational_def(Topform c);
BOOL equational_def_2(Term alpha, Term beta);
void flip_eq(Term atom, int n);Flip an equality and update the justification of the containing clause.
Topform fold_denial(Topform c, int alpha_max);
void init_paramod(void);
Literals literal_flip(Literals a);
void mark_oriented_eq(Term atom);This routine marks an atom as an oriented equality.
void mark_renamable_flip(Term atom);This routine marks an atom as "renamable_flip".
Topform new_constant(Topform c, int new_sn);If the Topform is a positive equality unit a(x) = b(y) with two variables in which one variable occurs in each side, infer a clause a(x) = c with a new constant c. We could also infer b(y)=c, but that will come by other inference mechanisms.
If new_sn == INT_MAX, a new symbol will be generated; otherwise, new_sn will be used as the symbol number of the new symbol.
void orient_equalities(Topform c, BOOL allow_flips);For each equality literal (positive or negative) of Topform c, compare the arguments; if the left is greater, mark the atom as oriented, and if the the right is greater, flip the arguments (add an entry to the justification), and mark the atom as oriented.
BOOL oriented_eq(Term atom);This function checks if an atom is an oriented equality atom. (The terms are not actually compared. Only the mark is checked.)
BOOL renamable_flip_eq(Term atom);This function checks if an atom is a renamable_flip equality atom. (The terms are not actually compared. Only the mark is checked.)
BOOL renamable_flip_eq_test(Term atom);Test if a term is a renamable-flip equality atom. This does not check the flag; it does the complete test.
BOOL same_term_structure(Term t1, Term t2);Do terms t1 and t2 have the same structure? That is, if we rename all variables to x, are t1 and t2 identical?
Term top_flip(Term a);Given a binary term (or atom), return the flip. The two arguments are not copied. When done with it, call zap_top_flip(t) instead of zap_term so that the arguments are not zapped.
Ordertype unfold_order(Term alpha, Term beta);
void zap_literal_flip(Literals a);Free a literal created by literal_flip.
void zap_top_flip(Term a);Free a term created by top_flip.