#include "demod.h"

This page has information from files demod.h and demod.c.

Contents

Public Routines in File demod.c

Index

demod1demod_rewritesdemodulator_typeparticular_demod
demod_attemptsdemodulateidx_demodulator

Details

void demod1(Topform c, Topform demodulator, int direction,
	    Ilist *fpos, Ilist *ipos,
	    BOOL lex_order_vars);
Special purpose demodulation routine.

Given a clause and a demodulator that rewrites the clause, rewrite the innermost leftmost subterm to which the demodulator applies. Return the rewritten term and the position vectors of the from and into terms. 

int demod_attempts();
Return the number of rewrite attempts so far (for the whole process). 
int demod_rewrites();
Return the number of successful rewrites so far (for the whole process). 
Term demodulate(Term t, Mindex demods, Ilist *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. 
int demodulator_type(Topform c, int lex_dep_demod_lim, BOOL sane);
Return NOT_DEMODULATOR, ORIENTED, LEX_DEP_LR, LEX_DEP_RL, or LEX_DEP_BOTH. 
void idx_demodulator(Topform c, int type, Indexop operation, Mindex idx);

void particular_demod(Topform c, Topform demodulator, int target, int direction,
		      Ilist *fpos, Ilist *ipos);
Special purpose demodulation routine.

Given a clause and which applies to the clause, return the rewritten clause and the position vectors of the from and into terms.

Public Definitions in File demod.h

Introduction