| back_demod_indexed | back_demod_linear | index_clause_back_demod | rewritable_clause |
Plist back_demod_indexed(Topform demod, int type, Mindex idx, BOOL lex_order_vars);This routine returns a Plist: the set clauses that have terms that can be rewritten with Topform demod.
If demod is oriented, demodulation is assumed to be left-to-right. If demod is not oriented, either way is allowed.
The Plist which is returned is ordered by decreasing clause ID.
Plist back_demod_linear(Topform demod, Clist lst, Plist rewritables);This routine returns a Plist: the subset of Clist lst that can be rewritten with Topform demod (which is assumed to be an oriented equation). The Plist which is returned is ordered by decreasing clause ID.
void index_clause_back_demod(Topform c, Mindex idx, Indexop op);This routine indexes or unindexes a clause for back demodulation.
BOOL rewritable_clause(Topform demod, Topform c);This Boolean function checks if Topform c is can be rewritten by Topform demod, which is assumed to be an oriented (left-to-right) equation.