| discrim_flat_cancel | discrim_flat_retrieve_next | fdemod_clause | |
| discrim_flat_retrieve_first | fapply_demod | fdemod_rewrites | |
| discrim_flat_retrieve_leaf | fdemod_attempts | fdemodulate |
void discrim_flat_cancel(Discrim_pos pos);
void *discrim_flat_retrieve_first(Flatterm f, Discrim root, Context subst, Discrim_pos *ppos);
Plist discrim_flat_retrieve_leaf(Flatterm fin, Discrim root, Context subst, Flatterm *ppos);
void *discrim_flat_retrieve_next(Discrim_pos pos);
Flatterm fapply_demod(Term t, Context c);Special-purpose apply for Flatterm demodulation. Apply a substitution to a (ordinary) Term, building a Flatterm. Assumptions: (1) the terms in the substitution are Flatterms; (2) every variable in the term is bound. In the result, Flatterms that are copied from the substitution have the "reduced_flag" set.
int fdemod_attempts();Return the number of flatterm rewrite attempts so far.
void fdemod_clause(Topform c, Mindex idx, int *step_limit, int size_limit, BOOL lex_order_vars);Demodulate Topform c, using demodulators in Mindex idx. If any rewriting occurs, the justification is appended to the clause's existing justification.
This version uses flatterm retrievel.
int fdemod_rewrites();Return the number of successful flatterm rewrites so far.
Term fdemodulate(Term t, Discrim root, int *step_limit, int size_limit, int *sequence, I3list *just_head, BOOL lex_order_vars);This routine demodulates a term. ID numbers of demodulators are put on the front of just_head, so you'll probably want to reverse the list before putting it into the clause justification.
This version uses flatterm retrieval.