/* ----------------------------------------------------------
%   (C)1992 Institute for New Generation Computer Technology
%       (Read COPYRIGHT for detailed information.)
----------------------------------------------------------- */
/*=====================================================================
*		cu-Prolog III (Constraint Unification Prolog)
*   Copyright: Institute for New Generation Computer Technology,Japan 
*                           1989--91
==================================================================== */
/*--------------------------------------------------------------------
*		   << trans.c >>
*              constriant transformation module
*  1992-Nov-4   sort bodies literals. (new_constraint, unfold_derivation)
--------------------------------------------------------------------*/

#include "include.h"
#define DEBUG 0			/* if debug, 1 */

struct cset *DEF_list;		/* sets of new predicate derivation clauses */
struct cset *CSTR_list;		/* sets of non-modular clauses */
struct cset *INITDEF_list;		/* sets of non-modular clauses */
int CSTR_number;
int old_CSTR_number;
struct clause *CONST_literals, *REST_literals; /* used in split, attach */
struct itrace *newfsave;	/* old newf_list */

jmp_buf trans_fail; /* transformation failure */

/*
[startmodular]----------------------------------- 
.   abandon_transformation
.   .   <index_newflist> --> new.c
.   .   reducedfun+
.   add_to_set+
.   .   index_newflist~
.   .   <add_cs_to_set> --> tr_sub.c
.   clear_up_DEF
.   .   remove_from_CSTR
.   end_unfoldfold+
.   .   <recalc_component>+ ---> mainsub.c
.   foldunfold+
.   .   <P_status>+ ------> tr_sub.c
.   .   set_temporal_def
.   .   <step_asking>+ ------> tr_sub.c
.   .   check_INITDEF+
.   .   is_modular_head+
.   .   .   vheadoccurrence.
.   .   unfold_cstr+
.   .   .   [apply]
.   .   .   [target_literal]
.   .   .   from_to+
.   .   .   insert_cs+
.   .   .   reorder.
.   .   unfold_derivation+
.   .   .   [apply]
.   .   .   [target_literal]
.   .   .   literalnumber~
.   .   .   reorder~
.   modular_form
.   .   <satisfiable> -------> tr_sub.c
.   .   <split>+  ---------> split.c
.   .   surface_copy_clause+
.   .   Pcmp+
.   .   new_constraint+
.   .   .   <try_fold>+ ---> modular.c
.   .   .   <variant_v>+ ---> tr_split.c
.   .   .   new_pred_set+
.   .   .   .   newpred+
.   .   .   .   set_new_def+
.   .   .   .   vpair_length+
.   .   set_const_pst+
.   init_unfoldfold+
*/

/* ------------  begin init & end unfoldfold --------------*/
void init_unfoldfold()
{
	newfsave = newf_list;	/* save newf_list */
	DEF_list = NULL;	/* derivation clauses */
	CSTR_list = NULL;	/* new clauses */
	old_CSTR_number = CSTR_number = 0;	/* initial clause number  */
	INITDEF_list = NULL;	/* initial derivation clauses */
}

void end_unfoldfold()
{
	void recalc_component(); /* mainsub.c */

	recalc_component();
	CSTR_list = NULL;	/* new clauses */
	old_CSTR_number = CSTR_number = 0;	/* initial clause number  */
	INITDEF_list = NULL;	/* initial derivation clauses */
}

				/* when transformation fails, */
void abandon_transformation()	/* abandon all new predicates */
{
	register struct cset *cs;
	register struct func *f;

	newf_list = newfsave;	/* restore newf_list (init_unfoldfold) */
	for (cs = INITDEF_list; cs != NULL; cs = cs->cs_link)
		if (cs->cs_status == FALSE_REGISTERED)
		{
			f = Pred(cs->cs_clause->c_form);
			if (f->f_integ == NULL) continue;
			index_func(f);
			reducedfun(f);
			f->def.f_set = NULL;
			f->f_unitcount = f->f_setcount = 0;
			f->f_integ->it_link = newf_list;
			newf_list = f->f_integ;
		}
	newf_list = index_newflist(newf_list,newfsave);
}

void quit_transformation()	/* quit transformation (in step trace) */
{
	register struct cset *cs;
	register struct func *f;

	for (cs = DEF_list; cs != NULL; cs = cs->cs_link)
	{
		f = Pred(cs->cs_clause->c_form);
		f->f_setcount = f->f_unitcount = 0; /* reset in add_cs_to_set*/
		if (cs->cs_status == REGISTERED || 
		    cs->cs_status == REMOVED)
			index_func(f); /* register into global hash table */
		else if (cs->cs_status == DERIVATION)
		{
			index_func(f); /* register into global hash table */
			add_cs_to_set(cs,'a');
		}
	}
	for (cs = CSTR_list; cs != NULL; cs = cs->cs_link)
		if (cs->cs_status != REMOVED)
			add_cs_to_set(cs,'a');
}
/* ------------  end init & end unfoldfold --------------*/


int check_INITDEF()		/* INITDEF_list is satisfiable ??*/
{
	register struct cset *cs;
	for(cs = INITDEF_list; cs != NULL; cs = cs->cs_link)
		if (cs->cs_status == FALSE_REGISTERED)
			return(FALSE);
	return(TRUE);
}

void remove_from_CSTR(f)	/* used in clear_up_DEF */
struct func *f;
{
	register struct cset *cs;
	register struct clause *c;
	
	for (cs = CSTR_list; cs != (struct cset *)NULL; cs = cs->cs_link)
		if (cs->cs_status == MODULAR_DEFINED ||
		    cs->cs_status == UNTOUCHED)
			for(c = cs->cs_clause; c != NULL_CL;
			    c = c->c_link)
 				if (Pred(c->c_form) == f) {
 				  cs->cs_status = REMOVED;
 				  Pred(cs->cs_clause->c_form)->f_setcount--;
 				  break;
				}
}


void clear_up_DEF()		/* delete useless clauses */
{
	register struct cset *cs;
	register struct func *f;
	int changed = 1;
	
	while(changed == 1)
	{
		changed = 0;
		for (cs = DEF_list; cs != NULL; cs = cs->cs_link)
		{
			if (cs->cs_status == REMOVED){
				f = Pred(cs->cs_clause->c_form);
				if (f->f_unitcount > 0)
					cs->cs_status = REGISTERED;
				else if (f->f_setcount == 0)
				{
					changed = 1;
					cs->cs_status = FALSE_REGISTERED;
					f->f_integ->it_clause->c_form = FAIL;
					remove_from_CSTR(f);
				}
			}
		}
	}
}	

void add_to_set()		/* register definition clauses */
{
	register struct cset *cs;
	register struct func *f;

	newf_list = index_newflist(newf_list,newfsave);
	for (cs = DEF_list; cs != NULL; cs = cs->cs_link)
	{
		f = Pred(cs->cs_clause->c_form);
		if (cs->cs_status == REGISTERED || 
		    cs->cs_status == REMOVED)
			index_func(f); /* register into global hash table */
		f->f_setcount = f->f_unitcount = 0; /* reset in add_cs_to_set*/
	}
	for (cs = CSTR_list; cs != NULL; cs = cs->cs_link)
		if (cs->cs_status == MODULAR_DEFINED ||
		    cs->cs_status == UNIT_DEFINED ||
		    (Is_Msolvable && (cs->cs_status == TEMPORAL_DEFINED)))
				add_cs_to_set(cs,'a');
}

/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
      startmodular(clist,vlist,anum)
      constraint transformation entry
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct clause *startmodular(clist, vlist, anum)	/* entry */
struct clause *clist;
struct term *vlist;
int anum;
{
	int result;
	register struct clause *c;
	
	init_unfoldfold();	/* reset gloval vars */
	if (clist != NULL)
	  clist = modular_form(clist,vlist,anum); /* set DEF_list */
	if (clist == NULL || clist == MFAIL ||DEF_list == NULL) 
	{
		end_unfoldfold();
		return(clist); /* no need for transformation */
	}
	INITDEF_list = DEF_list; /* initial derivation clauses */
TTB
	if (setjmp(trans_fail))	/* quit/abort transformation */
	{			/* <-- step_asking() */
		end_unfoldfold();
		/* if clist has defs  */
		for (c = clist; c != NULL; c = c->c_link) {
		  if (Pred(c->c_form)->def.f_set == (struct set *)NULL)
		    return(MFAIL);
		}
		return(clist);
	}
TTE
	result = foldunfold();
	if (result == TRUE)	/* transformation success */
	{
		clear_up_DEF();
		add_to_set();
		end_unfoldfold();
		return(clist);
	}
	else {			/* transformation failure */
		abandon_transformation();
		end_unfoldfold();
		return(MFAIL);
	}
}

void Pcmp(cmp)			/* print compartment */
struct compartment *cmp;
{
	for (; cmp != NULL; cmp = cmp->cmp_link)
	{
		Pclause(cmp->cmp_clause,NULL);NL;
	}
	if (CONST_literals != NULL) {
		printf("ground = ");
		Pclause(CONST_literals,NULL);NL;
	}
	if (REST_literals != NULL)
	{
		printf("rest = ");
		Pclause(REST_literals, NULL);NL;
	}
}

/* define new predicates */
struct clause *modular_form(clist, vlist, anum)
struct clause *clist;
struct term *vlist;
int anum;
{
	struct compartment *cmp,*cm;
	struct clause *crest, *cc;
	register struct clause *c;
	void set_const_pst();

	cmp = split(surface_copy_clause(clist,TEMPORAL), vlist, anum);
	if (cmp == (struct compartment *)MFAIL) return(MFAIL);

	/* global vars */
	crest = REST_literals;

/*	printf("split ");
	Pclause(clist,NULL);
	printf("into\n");
	Pcmp(cmp);
	NL;
*/	
	if (CONST_literals != NULL)
		if (! satisfiable(CONST_literals,anum)) return(MFAIL);
	for (cm = cmp; cm != NULL; cm = cm->cmp_link) {
	  cc = c = new_constraint(cm);
	  if (c == MFAIL) return(MFAIL);
	  if (c == NULL) continue;
	  while (c->c_link != NULL) c = c->c_link; /* c <- end of cc */
	  c->c_link = crest;
	  crest = cc;
	}
	return(crest);
}

/*++++++++++++++++++++++++++++++++++++++++++++++++++++++
  new_constraint(cmp)
  change cmp into surface modular form by
    making new predicates or folding

.   .   new_constraint+
.   .   .   try_fold+
.   .   .   .   match+
.   .   .   .   .   match_term+
.   .   .   .   termnumber
.   .   .   variant_v+
.   .   .   .   Pvariant+
.   .   .   new_pred_set+
.   .   .   .   newpred+
.   .   .   .   set_new_def+
.   .   .   .   vpair_length+
.   .   .   variables+
++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct clause *new_constraint(cmp) /* make new pred or folding */
struct compartment *cmp;
{
	struct term *t;
	struct clause *c,*new_pred_set();
	struct variant *ccopy,*variant_v();

	c = sort_clause(cmp->cmp_clause); /* 92/11/4 BUG fix */
	cmp->cmp_clause = c;

	if (c == NULL) return(NULL);
	if (is_modular_clause(c)) return(c);
/* here works in future */
/*	if (!need_trans(cmp))
          returnc(restore_head(c->c_form,cmp->cmp_vp,cmp->cmp_vp_size)); */
	ccopy = variant_v(c,MEDIUM);
	if (ccopy->v_anum > MODULARMAX)	/* heuristics  */
	{
		FILE *f = wfp;
		wfp = stderr;
		tprint0("Warning: Transformation failure by exceeding the");
		tprint0("limit of the number of variables (cf) %%M command\n");
		Pterm(c,NULL_ENV);NL;
		wfp = f;
		return(MFAIL);
	}
	t = try_fold(c, ccopy->v_anum);
	if (t != NULL)
	{
TTB
		tprint0("#folding "); Pclause(c,NULL); tprint0(" ==> ");
		Pterm(t,NULL);
TTE
                STAT_FOLD++;	/* statistics */
		if (t == FAIL) return(MFAIL);
		else return(Nclause(t,NULL,MEDIUM));
        }
	return(new_pred_set(ccopy));
}

struct clause *new_pred_set(cc)	/* set new pred & return */
struct variant *cc;
{
	struct func *newfunc;
	struct term *t1,*t2;
	struct clause *c1,*c2;
	register struct vpair *a;
	register int i;
	int arity,vpair_length();	/* tr_split.c */

	STAT_DEF++;		/* statistics */
	while (1) {
	  sprintf(nbuf, "%s%d", genname, GENSYM++);
	  if (exist_fname(nbuf) == NULL) break;
	}
	arity = vpair_length(cc->v_pair);
	newfunc = Nfunc(TEMPFUN, nbuf, arity);
	newpred(newfunc);
	(t1 = Nterm(arity,MEDIUM))->type.t_func = newfunc; /* orig. head */
	(t2 = Nterm(arity,MEDIUM))->type.t_func = newfunc; /* copy head */
	c1 = Nclause(t1,NULL,MEDIUM); /* new constraint */
	c2 = Nclause(t2,cc->v_clause,MEDIUM); /* new head == body */
	for (i = arity - 1, a = cc->v_pair; 0 <= i; i--,a=a->v_link)
	{
		Arg(t1,i) = a->v1;
		Arg(t2,i) = a->v2;
	}
	set_new_def(c2,cc->v_var,cc->v_anum); /* to DEF_list */
	return(c1);
}

void set_new_def(c,vl,anum)	/* add c to DEF_list */
struct clause *c;		/* head == body. */
struct term *vl;
int anum;
{
	register struct cset *s;

	s = Ncset(TEMPORAL);
	s->cs_status = DERIVATION;
	s->cs_clause = c;
	s->cs_link = DEF_list;
	s->cs_anumber = anum;
	s->cs_vlist = vl;
	DEF_list = s;		/* global var */
}

int is_modular_head(t)		/* check head t is modular or not */
struct term *t;
{
	struct func *f;
	register int i;
	register struct term *arg;

	if (! is_functor(t)) {
	  wfp = stderr;
	  Pterm(t,NULL_ENV);
	  error("Only Functors can be used as Constraints");
	}
	f = Pred(t);
	for (i = 0; i < f->f_arity; i++)
	{
		arg = Arg(t,i);
		if (isvar(arg))
		{
			if (vheadoccurrence(arg) > 1) /* double occurrence */
				return(FALSE); 
		}
		else if (is_pst(arg)) continue;	/* 91.10.1 ??? */
		else return(FALSE);
	}
	return(TRUE);
}
/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
   foldunfold()
   fold/unfold transformation loop
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
int foldunfold()		/* fold-unfold transformation main */
{
	register struct cset *cs;
	struct clause *body;
	register struct func *f;
	void unfold_derivation(),unfold_cstr(),set_temporal_def();

	for (;;)
	{
		clear_up_DEF();
		if (check_INITDEF() == FALSE) return(FALSE);
TTB
		P_status();	/* print stack */
		if Is_ctstep 
			if (step_asking() != 0) continue; /* user's input */
TTE

	/* target def-clause */
		for (cs = DEF_list; cs != NULL; cs = cs->cs_link)
			if (cs->cs_status == DERIVATION) break;
		if (cs != NULL) /* unfold def-clause */
		{
		    STAT_UNFOLD++;
			unfold_derivation(cs);
			continue;
		}
		/* get one clause from CSTR_list*/
		for (cs = CSTR_list; cs != NULL; cs = cs->cs_link)
			if (cs->cs_status == UNTOUCHED) break;

		if (cs == NULL) return(TRUE); /* no target --> fail */
		f = Pred(cs->cs_clause->c_form);
		if (is_modular_head(cs->cs_clause->c_form))
		{
		    STAT_UNFOLD++;
		  unfold_cstr(cs);
		  continue;
		}
		body = modular_form(cs->cs_clause->c_link, 
				    cs->cs_vlist, cs->cs_anumber);
		cs->cs_clause->c_link = body;
		if (body == MFAIL) /* fail transformation */
		{
			cs->cs_status = REMOVED;
			f->f_setcount--;
		}
		else if (body == NULL) /* unit definition */
		{
			cs->cs_status = UNIT_DEFINED;
			f->f_unitcount++;
		  /* M-solvability */
		  if (Is_Msolvable) set_temporal_def(f);
TTB
			tprint1("#reduce body <%d>",cs->cs_number);
TTE
		}
		else 
		{
			cs->cs_status = MODULAR_DEFINED;	
TTB
			tprint1("#modularize <%d>",cs->cs_number);
TTE
		}
	}
}

void set_temporal_def(f)
struct func *f;
{
  register struct cset *cs;

  for (cs = CSTR_list; cs != (struct cset *)NULL; cs = cs->cs_link) {
    switch (cs->cs_status) {
    case UNTOUCHED:
      if (f == Pred(cs->cs_clause->c_form))
      	cs->cs_status = TEMPORAL_DEFINED;
      break;
    case MODULAR_DEFINED:
      if (f == Pred(cs->cs_clause->c_link->c_form)) {
	cs->cs_status = TEMPORAL_DEFINED;
	set_temporal_def(Pred(cs->cs_clause->c_form));
      }
    }
  }
}

struct clause *reorder(cl,tc)	/* used in unfold_derivation, _cstr */
struct clause *cl,*tc;		/* cl:literals, tc:target literal */
{
	register struct clause *c;

	if (cl == NULL_CL) return(NULL_CL);
	for (c = cl; c != NULL_CL; c = c->c_link)
		if (c->c_link == tc) break;
	if (c == NULL_CL) return(cl);
	else {
		c->c_link = tc->c_link;
		tc->c_link = cl;
		return(tc);
	}
}

void unfold_derivation(cs)	/* unfold derivation clause (in unfoldfold) */
struct cset *cs;	
{
	struct clause *tc,*ccopy;
	struct func *f;
	struct itrace *it;
	int res;

	ccopy = surface_copy_clause(cs->cs_clause,ETERNAL);
	tc = target_literal(cs->cs_clause->c_link);
	cs->cs_clause->c_link = reorder(cs->cs_clause->c_link,tc);
	if (tc == NULL)	/* no need for transformation */
	{
		cs->cs_status = REGISTERED;
		return;
	}
	TTB /* print target literal */
	tprint1("#unfold-[%d] ",cs->cs_number);
	Pterm(tc->c_form,NULL);
	TTE
	res = apply(tc->c_form,cs->cs_clause->c_form,
		     tc->c_link,cs->cs_anumber);
	f = Pred(cs->cs_clause->c_form);
	f->f_integ = it = snew(itrace);
	it->it_clause = ccopy;	/* BUG 92/11/4 */
	it->it_anumber = cs->cs_anumber;
	it->it_cnumber = literalnumber(cs->cs_clause->c_link);
	it->it_link = newf_list; newf_list = it;
	if (res == FALSE)
	{
		it->it_clause->c_form = FAIL;
		cs->cs_status = FALSE_REGISTERED;
		remove_from_CSTR(f);
		TTB tprint0(" ->FAIL"); TTE
	}
	else
	{
		if (f->f_unitcount > 0)
			cs->cs_status = REGISTERED;
		else cs->cs_status = REMOVED;
		TTB tprint0(" =>TRUE"); TTE
	}
}

void insert_cs(cs,newcs)	/* used in unfold_cstr */
struct cset *cs, *newcs;	/* append newcs after cs */
{
	register struct cset *c;

	if (newcs == NULL) return;
	for (c = newcs; c->cs_link != NULL; c = c->cs_link); 
				/* c <= end of newcs */
	c->cs_link = cs->cs_link;
	cs->cs_link = newcs;
}

struct cset *from_to(s1,s2)	/* used in unfold_cstr */
struct cset *s1,*s2;		/* s1->..->c->s2 ===> s1->..->c->NULL*/
{
	struct cset *c;
	if (s1 == s2) return(NULL);
	for (c = s1; c->cs_link != s2; c= c->cs_link);
	c->cs_link = NULL;
	return(s1);
}

void unfold_cstr(cs)	/* unfold CSTR clause (in unfoldfold) */
struct cset *cs;	
{
	struct clause *tc;
	struct func *f;
	int res;
	struct cset *cstr_save;	/* old CSTR_list */

	f = Pred(cs->cs_clause->c_form);
	tc = target_literal(cs->cs_clause->c_link);
	cs->cs_clause->c_link = reorder(cs->cs_clause->c_link,tc);
	if (tc == NULL)	/* no need for transformation */
	{
		cs->cs_status = MODULAR_DEFINED;
		return;
	}
TTB /* print target literal */
	tprint1("#unfold=[%d] ",cs->cs_number);
	Pterm(tc->c_form,NULL);
TTE
	f->f_setcount--;
	cs->cs_status = REMOVED;
	cstr_save = CSTR_list;
	res = apply(tc->c_form,cs->cs_clause->c_form,
		     tc->c_link,cs->cs_anumber);
	if (res == FALSE)
	{
		TTB tprint0(" ->FAIL"); TTE
	}
	else
	{
		struct cset *newcs;
		newcs = from_to(CSTR_list,cstr_save); /* new defs */
		CSTR_list = cstr_save;
		insert_cs(cs,newcs); /* put newcs after cs */
		TTB tprint0(" =>TRUE"); TTE
	}
}

/*
[apply]--------------------  head unification & goal replacement
.   [system_function]
.   <system_pred>  ---> defsysp.c
.   <reduce_clause>  ---> tr_sub.c
.   apply_add_clause
.   .   <up_eclause>  ---> modular.c
.   .   <satisfiable~> ---> tr_sub.c
.   .   <add_clause>+ ---> tr_sub.c
.   extend_apply+
.   .   [tunify]
.   .   eclause_conc.
*/
int apply(target,head,rest,anum) /* head:-target,rest. */
struct term *target,*head;
struct clause *rest;
int anum;
{
  struct pair *e0;
  struct func *f = Pred(target);
  struct node *dummy;
  struct eclause *ec;
  struct pair *esave = ep;
  struct ustack *usave = usp;

  if (anum > 0) e0=Nenv(anum);
  else e0=NULL_ENV;
  if (issystem(f)) {
    dummy = Newnode(NULL,NULL,NULL,NULL,NULL);
    if (isfunc(f)) {
      if (system_function(target,e0,dummy) == SYSFAIL) {
	ep = esave;
	return(FALSE);
      }
      /* has solution */
      ec = reduce_clause(rest,e0);
      if (ec == (struct eclause *)MFAIL) 
      {
	      ep = esave; return(FALSE);
      }
      apply_add_clause(head,e0,ec);
      ep = esave;
      return(TRUE);
    }
    else  { /* isnonfunc */
     if (system_pred(target,e0,dummy,dummy,DOWN) == SYSFAIL)
	return(FALSE);
      /* has possibly many solutions */
      do {
	ec = reduce_clause(rest,e0);
	apply_add_clause(head,e0,ec);
	undo(usave);
	if (anum > 0) e0 = Nenv(anum);
	else e0=NULL_ENV;
      } while (system_pred(target,e0,dummy,dummy,BACKTRACK) == SYSTRUE);
      ep = esave;
      undo(usave);
      return(TRUE);
    }
  }
/* user predicate */
    return(extend_apply(target,head,rest,e0,f,f->def.f_set));
}

int extend_apply(target,head,rest,e0,f,s) /* in apply */
struct term *target,*head;
struct clause *rest;
struct pair *e0;
struct func *f;
register struct set *s;
{
  struct eclause *ec;
  struct ustack *usave = usp;
  int *hsave,cn;
  struct pair *e1;

  if (s == (struct set *)NULL) {
    if (Handle_Undefined == TRUE) {
      sprintf(nbuf,">>> %s <<< is UNDEFINED!",f->f_name);
      error(nbuf);
    }
    else return(FALSE);
  }

  for (cn = 0 ; s != NULL; s = s->s_link) {
    hsave = hp;
    if (s->s_ground_head)	/* no var/PST in the head */
    {
	if (tunify(target,e0,
			 s->s_clause->c_form,NULL,2)==FALSE) /* safe unify */
	{
	    hp = hsave;
	    continue;
	}
	if (s->s_anumber > 0) e1 = Nenv(s->s_anumber);
	else e1 = NULL_ENV;
    }
    else
    {
	if (s->s_anumber > 0) e1 = Nenv(s->s_anumber);
	else e1 = NULL_ENV;
	if (tunify(target,e0,
			 s->s_clause->c_form,e1,2)==FALSE) /* safe unify */
	{
	    hp = hsave;
	    continue;
	}
    }
    ec = eclause_conc(reduce_clause(s->s_clause->c_link, e1),
                      eclause_conc(reduce_clause(s->s_constraint,e1),
                                   reduce_clause(rest,e0)));
    if (apply_add_clause(head,e0,ec)!=FALSE)
	    cn++;		/* # of new clauses */
    undo(usave); /* restore environments */
  }
  if (cn == 0) return(FALSE);
  else return(TRUE);
}

int apply_add_clause(head,e0,ec) /* in apply, extend_apply */
struct term *head;
struct pair *e0;
struct eclause *ec;
{
  struct clause *newbody;
  struct term *newhead;
  struct pair *e1;
  int i;
  
  if (ec == (struct eclause *)MFAIL) return(FALSE);
  up_init();
  newhead = termset(head, e0,MEDIUM);
  newbody = up_eclause(ec,MEDIUM);
  if (p_number != 0) {
      renum_pvars((struct pstvar *)pv_list,v_number);
      if (p_number > 0) e1=Nenv(p_number);
      else e1=NULL_ENV;
      i = p_number;
      while (i > 0) {
	i--;
	e1[i].p_body = ((struct pstvar *)pv_list)->old_var;
	e1[i].p_env = e0;
	pv_list = ((struct pstvar *)pv_list)->v_link;
      }
    }
    up_restore();
    if (newbody != NULL && v_number == 0 && p_number == 0) 
    {   /* containts no variables */
      if (satisfiable(newbody,0)) newbody = NULL;
      else return(FALSE);
    }
  add_clause(Nclause(newhead,newbody,MEDIUM), v_list, v_number+p_number);
  return(TRUE);
}