/* ----------------------------------------------------------
%   (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
==================================================================== */
/*--------------------------------------------------------------------
*		<<<< tr_sub.c >>>>
* subroutines for constraint transformation (called by transform.c)
*  95.1.27  satisfiable (save global vars)
--------------------------------------------------------------------*/

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

extern struct cset *DEF_list;
extern struct cset *CSTR_list;
extern struct cset *INITDEF_list;
extern int CSTR_number;
extern int old_CSTR_number;
extern struct clause *CONST_literals, *REST_literals; 
extern struct itrace *newfsave;
extern jmp_buf trans_fail;

int cs_status_type(st)
int st;
{
  static char cs_status_list[9] = {
    'u','r','m','i','d','g','f','x','t'};

  if (st > TEMPORAL_DEFINED) return('?');
  else return(cs_status_list[st]);
}

void Pcset_def(cs)			/* print cset */
struct cset *cs;
{
	tprint3("[%d(%c,%d)] ",cs->cs_number,
		cs_status_type((int)cs->cs_status),
		Pred(cs->cs_clause->c_form)->f_setcount);
	P_dclause(cs->cs_clause,NULL_ENV);
}

void Pcset_cstr(cs)			/* print cset */
struct cset *cs;
{
	tprint2("<%d(%c)> ",cs->cs_number,
		cs_status_type((int)cs->cs_status));
	P_hclause(cs->cs_clause,NULL_ENV);
}

void P_csnumber(cs,mode)
struct cset *cs;
int mode;
{
	register struct cset *c;
	int i = 0;
	
	for (c = cs; c != NULL; c = c->cs_link)
	if ((mode == 1 && c->cs_status == DERIVATION) ||
	    (mode == 2 && c->cs_status == UNTOUCHED) ||
	    (mode == 3 && (c->cs_status == MODULAR_DEFINED || 
			   c->cs_status == UNIT_DEFINED)))
	{
		if (i != 0) {
		tputc(',');
		}
		i = 1;
		tprint1("%d",c->cs_number);
	}
}	

/* +++++++++++++++++++++++++++++++++++++++++++++++++++++++
   P_status()
   print DEF_list, CSTR_list

.   .   P_status+
.   .   .   P_csnumber+
.   .   .   Pcset_cstr+
.   .   .   .   cs_status_type.
.   .   .   .   d.
.   .   .   Pcset_def+
.   .   .   .   cs_status_type~
.   .   .   .   d~
++++++++++++++++++++++++++++++++++++++++++++++++++++++++ */
void P_status()  /* print DEF_list,CSTR_list (for debug) */
{
	register struct cset *cs;
	
	tprint0("****");
	tprint0("DEFS={");P_csnumber(DEF_list,1);tprint0("}  ");
	tprint0("NON-MODULAR={");P_csnumber(CSTR_list,2);tprint0("}  ");
	tprint0("MODULAR={");P_csnumber(CSTR_list,3);tprint0("}****");
	for (cs = DEF_list; cs != NULL; cs = cs->cs_link)
	if (cs->cs_status != FALSE_REGISTERED &&
            cs->cs_number >= old_CSTR_number)
	 {NL;Pcset_def(cs);}
/*		if (cs->cs_status == DERIVATION) {NL;Pcset_def(cs);}*/
	for (cs = CSTR_list; cs != NULL; cs = cs->cs_link)
	if (cs->cs_status != REMOVED &&
            cs->cs_number >= old_CSTR_number)
	  {NL;Pcset_cstr(cs);}
/*		if (cs->cs_status == UNTOUCHED) {NL;Pcset_cstr(cs);}*/
	old_CSTR_number=CSTR_number;
}


struct cset *Ncset(flag)	/* allocate cset structure */
int flag;
{
	register struct cset *s;
	MEMORY_ALLOC(s,cset,flag);
	s->cs_clause = NULL;
	s->cs_link = NULL;
	s->cs_vlist = NULL;
	s->cs_anumber = s->cs_cnum = 0;
	s->cs_status = UNTOUCHED; /* defalut status */
	s->cs_number = CSTR_number++;
	s->cs_mother = NULL;
	return(s);
}


/* ------- add c to CSTR_list (in apply_add_clause) -------*/
struct cset *CSTR_tail;	/* tail of CSTR_list used in add_clause() */

void add_clause(c, vlist, anum)
struct clause *c;
struct term *vlist;
int anum;
{
	register struct cset *cs;
	struct func *f;
	void set_temporal_def();
	
	f = Pred(c->c_form);
	f->f_setcount++;
	recalc_voccurrence(c,vlist);
	cs = Ncset(TEMPORAL);
	if (c->c_link == NULL)
	{
		f->f_unitcount++;
		cs->cs_status = UNIT_DEFINED;
		if (Is_Msolvable) set_temporal_def(f);
	}
	else if (is_modular_clause(c->c_link))
		cs->cs_status = MODULAR_DEFINED;
	else cs->cs_status = UNTOUCHED;
	cs->cs_clause = c;
	cs->cs_vlist = vlist;
	cs->cs_anumber = anum;
	cs->cs_link = CSTR_list;
	CSTR_list = cs;
}
/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
    add_cs_to_set(cs,flag)
    register new predicates

.   .   <add_cs_to_set> --> tr_sub.c
.   .   .   [variant]
.   .   .   add_set
.   .   .   .   setconcat+
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
void add_cs_to_set(cs,flag)	/* register new predicates  */
struct cset *cs;
int flag;
{
  register struct set *s;
  register struct variant *va;
  struct variant *variant();

  s = snew(set);
  va = variant(cs->cs_clause,ETERNAL);
  s->s_clause = va->v_clause;
  s->s_anumber = va->v_anum;
  s->s_vlist = va->v_var;
  s->s_constraint = NULL;
  s->s_bodynumber = 0;	/* set in add_set */
  add_set(s,flag);
}

/* ---------- reduction ----------------- */
/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
    struct eclause *reduce_clause(cl,e) 
    reduce predicates which have only one definition

.   reduce_clause
.   .   reduce_clause_m+
.   .   .   [tunify]
.   .   .   [system_function]
.   .   .   Neclause
.   .   .   one_def_literal+
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/

struct eclause *reduce_clause(cl,e) /* entry */
struct clause *cl;
struct pair *e;
{
	struct ustack *usave = usp;
	int *hsave = hp;
	struct pair *esave = ep;
	struct eclause *reduce_clause_m();
	register struct eclause *res;

	res = reduce_clause_m(cl,e);
	if (res == (struct eclause *)MFAIL)
	{
	    undo(usave);
	    hp = hsave;
	    ep = esave;
	}
	return(res);
}

struct eclause *reduce_clause_m(cl,e) /* reduce_clause sub */
struct clause *cl;
struct pair *e;
{
	register struct set *s;
	struct pair *e1;

	if (cl == NULL) return(NULL);
        if (is_functor(cl->c_form) &&
            ((Pred(cl->c_form)->f_mark & NON_UNFOLDABLE) == 0)) {
          if ((s = one_def_literal(Pred(cl->c_form))) != NULL) /* reduceable */
            {
		if (s == (struct set *)MFAIL) /* error in one_def_literal */
		    return((struct eclause *)MFAIL);
		e1 = Nenv(s->s_anumber);
		if (tunify(cl->c_form,e,s->s_clause->c_form,e1,1)==FALSE)
			return((struct eclause *)MFAIL);
		else 
                  return(
                         eclause_conc(
                               reduce_clause(cl->c_link,e),
                               eclause_conc(
                                    reduce_clause(s->s_constraint,e1),
				    reduce_clause(s->s_clause->c_link,e1))));
              }
          else if (is_funcsys(Pred(cl->c_form))) {
	    struct node *dummy;
	    dummy = Newnode(NULL,NULL,NULL,NULL,NULL);
	    if (system_function(cl->c_form,e,dummy) == SYSFAIL)
		    return((struct eclause *)MFAIL);
	    else return(reduce_clause(cl->c_link,e));
          }
        }
	return(Neclause(cl->c_form,e,reduce_clause(cl->c_link,e),MEDIUM));
}

struct set *one_def_literal(f)	/* reduce_clause_m sub */
struct func *f;
{
  if (isuser(f)) {
    switch (f->f_setcount) {
      case 1: return(f->def.f_set);
      case 0:
	if (Handle_Undefined == TRUE) {
	  sprintf(nbuf,">>> %s <<< is UNDEFINED!",f->f_name);
	  error(nbuf);
	  }
	else return((struct set *)MFAIL); 
      default: return(NULL);
      }
  }
  else return(NULL);
}

void reorder_clause(cl, tc)
struct clause *cl, *tc;
{
	register struct clause *c;

	for (c = cl; c != NULL; c = c->c_link)
		if (c->c_link == tc) break;
	if (c == NULL) return;
	c->c_link = tc->c_link;
	tc->c_link = cl->c_link;
	cl->c_link = tc;
	return;
}
/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++
  int satisfiable(cl,anum)   ---> TRUE/FALSE
  check satisfiability of constraint 

.   .   satisfiable
.   .   .   [refute]
+++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
int satisfiable(cl,anum)	/* satisfiability check */
struct clause *cl;
int anum;
{
  int tflagsave;			/* save tflag */
	struct ustack *usave = usp;
	struct node *Last_Node, *Initial_Goal,*lbsave,*lssave;

	tflagsave = tflag;	/* save prolog trace flag */
	Notrace_mode;		/* for satisfiable() */
	upush(&hp);upush(&ep);
	upush(&Last_BT);upush(&Last_SKIP);
	Initial_Goal = Last_Node = 
	  Newnode(cl, NULL_ECL, Nenv(anum),
		  (struct node *)NULL,(struct node *)NULL);
        lbsave=Last_BT;  lssave=Last_SKIP; /* 95.1.27 */
	Last_BT = Last_SKIP = NULL;
	if (refute(Initial_Goal, Last_Node, DOWN) == FALSE)
	{
		undo(usave);
		tflag = tflagsave;
		Last_BT = lbsave;
		Last_SKIP = lssave;
		return(FALSE);
	}
  undo(usave);
  Last_BT = lbsave;
  Last_SKIP = lssave;
  tflag = tflagsave;
  return(TRUE);
}
/* ++++++++++++++++++++++++++++++++++++++++++++++++++
struct clause *target_literal(cl)
   select unfolding target from cl

[target_literal]----------------------------------- 
.   Penergy+
.   energy
.   .   isconst
.   .   voccurrence.
.   .   isallunit+
.   greater_term
.   .   greater_arg
.   .   .   cmp_clause+
.   .   .   cmp_cplxt+
.   .   .   cmp_flt+
.   .   .   cmp_fp+
.   .   .   cmp_int+
.   .   .   cmp_list+
.   .   .   cmp_var
.   .   .   cmp_pst+
.   .   .   cmp_str+
.   .   .   arg_type+
++++++++++++++++++++++++++++++++++++++++++++++++++ */

void Penergy(cl)
struct clause *cl;
{
	register struct clause *c;
	for (c = cl; c != NULL; c = c->c_link)
	{
		Pterm(c->c_form,NULL);
		tprint1("<%d>,",energy(c->c_form));
	}
}

struct clause *target_literal(cl)
struct clause *cl;
{
	register struct clause *ct, *c;
	register int cte,ce;

#if DEBUG == 1
	printf("ENERGY: ");
	Penergy(cl);
	NL;
#endif
	if (cl->c_link == NULL) return(cl);
	ct = cl;
	cte = energy(ct->c_form);
	for (c = cl->c_link; c != NULL; c = c->c_link)
	{
		ce = energy(c->c_form);
		if (ce > cte)
		{
			cte = ce;
			ct = c;
		}
		else if (ce == cte && greater_term(ct->c_form,c->c_form))
				continue;
	}
	return(ct);
}

int     Hueristic_modified = 0;
int 	Factor_con, 
	Factor_funct, 
	Factor_vn, 
	Factor_defs, 
	Factor_units, 
	Factor_rec, 
	Factor_allunit;

/* +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
   int energy(term)
   energy of term 
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ */
int energy(tm)			/* enegy function of literal t */
struct term *tm;
{
	int arity = 0, con = 0, vn = 0, funct = 0, rec = 0, 
	allunit = 0, defs = 0, units = 0, energy;
	struct func *f;
	register struct term *t;
	register int i;

	f = Pred(tm);
	arity = f->f_arity;
	for (i = 0; i < arity; i++) {
		if (Component(f,i) == NULL) continue;
		t = Arg(tm,i);
		if (isconst(t)) con++;
		else if (isvar(t)) vn+=(voccurrence(t) - 1);
		else funct++;
	}
	rec = isrecursive(f);
	allunit = isallunit(f);
	defs = f->f_setcount;
	units = f->f_unitcount;
	energy = con * 7 - arity + funct * 4 + vn * 2 - defs*2 + units*2
	       - rec * 4 + allunit * 6;
	return(energy);
}

/* general predicates for transform.c */
struct clause *surface_copy_clause(cl,flag) /* make copy of cl */
struct clause *cl;
int flag;
{
	if (cl == NULL) return(NULL);
	return(Nclause(cl->c_form,
			surface_copy_clause(cl->c_link,flag),
			flag));
}

int is_modular_clause(cl)	/* check if clause cl is modular */
struct clause *cl;
{
	register struct clause *c;
	for (c = cl; c != NULL; c = c->c_link)
	{
		if (! is_modular_literal(c->c_form)) return(FALSE);
	}
	return(TRUE);
}

int is_modular_literal(t)	/* check if literal t is modular */
struct term *t;
{
	struct func *f;
	register int i;
	register struct term *arg;
	int has_common_label();	/* mainsub.c */

	if (! is_functor(t)) {
	  wfp = stderr;
	  Pterm(t,NULL_ENV);
	  error("Only Functors can be used as Constraints");
	}
	f = Pred(t);
	/* if (is_component_not_checked(f)) recalc_f_roles(f);*/
	for (i = 0; i < f->f_arity; i++)
	{
		if (Component(f,i) == NULL) continue;
		else {
			arg = Arg(t,i);		
			if (isvar(arg) && voccurrence(arg) <= 1)
				continue;
			if (is_pst(arg) && 
			    ! has_common_label(((struct pst *)arg)->p_lists,
					       Component(f,i)))
				continue;
			else 
				return(FALSE);
		}
	}
	return(TRUE);
}	

int has_no_var(t)		/* check if t contains no variable */
struct term *t;
{
	register int i;

	for (i = 0; i < Pred(t)->f_arity; i++)
		if (! novar(Arg(t,i))) return(FALSE);
	return(TRUE);
}

struct eclause *eclause_conc(ec1,ec2) /* concatenate eclauses */
struct eclause *ec1,*ec2;
{
	register struct eclause *ec;

	if (ec1 == NULL) return(ec2);
	if (ec2 == NULL) return(ec1);
	if (ec1 == (struct eclause *)MFAIL||ec2 == (struct eclause *)MFAIL)
		return((struct eclause *)MFAIL);
	ec = ec1;
	while (ec->c_link != NULL)
	  ec = ec->c_link;
	ec->c_link = ec2;
	return(ec1);
}

/*
* sort_clause
*   insert_clause
*        greater_term
*            greater_arg
*                  arg_type
*                  cmp_var,cmp_cplxt,cmp_list,cmp_flt,cmp_int,cmp_str,cmp_fp
*/
struct clause *sort_clause(cl)	/* sort clause for fold transformation */
struct clause *cl;
{
	if (cl == NULL) return(NULL);
	return(insert_clause(cl, sort_clause(cl->c_link)));
}

struct clause *insert_clause(ct, cl) /* insert ct into cl */
struct clause *ct,*cl;
{
	register struct clause *c,*cbefore;

	ct->c_link = NULL;
	if (cl == NULL) return(ct);
	if (greater_term(ct->c_form,cl->c_form)) { /* ct > top of cl? */
		ct->c_link = cl;
		return(ct);
	}
	for (c = cl; c != NULL; cbefore = c, c = c->c_link)
		if (greater_term(ct->c_form,c->c_form))	/* ct > c? */
			break;
	cbefore->c_link = ct;
	ct->c_link = c;
	return(cl);
}

#define ARG_EQ 0
#define ARG_TRUE 1
#define ARG_FALSE 2

/*  term comparator */
int greater_term(t1,t2)		/* t1 > t2 ?? */
struct term *t1,*t2;
{
  register int i,cp;

  if (Pred(t1)->f_number != Pred(t2)->f_number)
    return(Pred(t1)->f_number > Pred(t2)->f_number);
  for(i = 0; i < Pred(t1)->f_arity; i++)
    if ((cp = greater_arg(Arg(t1,i),Arg(t2,i))) != ARG_EQ)
      return(cp == ARG_TRUE);
  return(FALSE);
}

/*
argument type:
0 variable (cmp_var)
1 complex term that has a variable (cmp_cplxt)
2 list that has a variable (cmp_list)
3 complex term without variable (cmp_cplxt)
4 list without variable (cmp_list)
5 atom, floating number (cmp_flt)
6 atom, integer number (cmp_int)
7 atom, string  (cmp_str)
8 atom, filepointer (cmp_fp)
9 clause (cmp_clause)
10 pst (cmp_pst)
*/
int arg_type(a)			/* return argument type */
struct term *a;
{
  switch (a->type.ident) {
  case VAR_VOID_TYPE:
  case VAR_PST_TYPE:
  case VAR_GLOBAL_TYPE:
    return(0);
  case ATOMIC_TYPE:
    return(5 + a->t_arity);
  case LIST_TYPE:
    return(2);
  case CONST_LIST_TYPE:
    return(4);
  case CLAUSE_TYPE:
    return(9);
  case PST_TYPE:
    return(10);
  default:
    if (a->t_arity <= 0) return(3);
    return(1);
  }
}

int greater_arg(a1,a2)		/* a1 > a2 ? */
struct term *a1,*a2;
{
  int cp;
  int atype1 = arg_type(a1),atype2 = arg_type(a2);

  if ((cp = (atype1 - atype2)) != 0)
    if (cp > 0) return(ARG_TRUE);
    else return(ARG_FALSE);

  switch(atype1){
    case 0 : return(cmp_var(a1,a2));
    case 1 : return(cmp_cplxt(a1,a2));
    case 2 : return(cmp_list(a1,a2));
    case 3 : return(cmp_cplxt(a1,a2));
    case 4 : return(cmp_list(a1,a2));
    case 5 : return(cmp_flt(a1,a2));
    case 6 : return(cmp_int(a1,a2));
    case 7 : return(cmp_str(a1,a2));
    case 8 : return(cmp_fp(a1,a2));
    case 9 : return(cmp_clause(a1,a2));
    case 10: return(cmp_pst(a1,a2));
    }
    return(ARG_FALSE);
}

int cmp_var(a1,a2)		/* compare variable  a1 > a2??*/
struct term *a1,*a2;
{
	register int i;

	i = voccurrence(a1) - voccurrence(a2);
	if (i == 0) return(ARG_EQ);
	else if (i > 0) return(ARG_TRUE);
	else return(ARG_FALSE);
}

int cmp_cplxt(a1,a2)		/* compare complex terms */
struct term *a1,*a2;
{
	register int i,cp;

	if (Pred(a1)->f_number != Pred(a2)->f_number)
		return(Pred(a1)->f_number > Pred(a2)->f_number);
	for(i = 0; i < Pred(a1)->f_arity; i++)
		if ((cp = greater_arg(Arg(a1,i),Arg(a2,i))) != ARG_EQ)
			return(cp);
	return(ARG_EQ);
}

int cmp_list(a1,a2)		/* compare list */
struct term *a1,*a2;
{
	int cp;

	if (a1 == NIL || a2 == NIL)
		if (a1 == a2) return(ARG_EQ);
		else if (a1 == NIL) return(ARG_TRUE);
		else return(ARG_FALSE);

	if (isvar(a1)) { /* patch 1991-03-03 */
	  if (isvar(a2)) return(cmp_var(a1,a2));
	  else return(ARG_FALSE);
	}

	if (cp = greater_arg(head_of_list(a1), head_of_list(a2)) != ARG_EQ)
		return(cp);
	else return(cmp_list(tail_of_list(a1),tail_of_list(a2)));
}

int cmp_clause(a1,a2)		/* compare clause */
struct term *a1,*a2;
{
	int cp;
	if (a1 == NULL || a2 == NULL)
		if (a1 == a2) return(ARG_EQ);
		else if (a1 == NULL) return(ARG_TRUE);
		else return(ARG_FALSE);
	if (cp = greater_arg(head_of_list(a1), head_of_list(a2)) != ARG_EQ)
		return(cp);
	else return(cmp_clause(tail_of_list(a1),tail_of_list(a2)));
}

int cmp_flt(a1,a2)
struct term *a1,*a2;
{
	float cp;

	cp = num_value(a1) - num_value(a2);
	if (cp == 0) return(ARG_EQ);
	else if (cp > 0) return(ARG_TRUE);
	else return(ARG_FALSE);
}

int cmp_int(a1,a2)
struct term *a1,*a2;
{
	register int cp;
	cp = (int)num_value(a1) - (int)num_value(a2);
	if (cp == 0) return(ARG_EQ);
	else if (cp > 0) return(ARG_TRUE);
	else return(ARG_FALSE);
}

int cmp_str(a1,a2)
struct term *a1,*a2;
{
	register int cp;
	cp = strcmp(str_value(a1), str_value(a2));
	if (cp == 0) return(ARG_EQ);
	else if (cp > 0) return(ARG_TRUE);
	else return(ARG_FALSE);
}

int cmp_fp(a1,a2)
struct term *a1,*a2;
{
	register int cp;
	
	cp = filep_value(a1) - filep_value(a2);
	if (cp == 0) return(ARG_EQ);
	else if (cp > 0) return(ARG_TRUE);
	else return(ARG_FALSE);
}

int cmp_pst(a1,a2)
struct term *a1, *a2;
{
  register struct eclause *e1, *e2;
  int cp;

  e1 = ((struct pst *)a1)->p_lists;
  e2 = ((struct pst *)a2)->p_lists;

  while ((e1 != NULL_ECL) && (e2 != (struct eclause *)NULL)) {
    if ((cp = greater_arg(e1->c_form,e2->c_form)) != ARG_EQ)
      return(cp);
    e1 = e1->c_link;
    e2 = e2->c_link;
  }
  if (e1 == e2) return(ARG_EQ);
  else if (e2==NULL_ECL) return(ARG_TRUE);
  else return(ARG_FALSE);
}

/* c.t. step trace subroutine  */
/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
  int step_asking()

.   .   step_asking+
.   .   .   [apply]
.   .   .   nth_cset+
.   .   .   nth_literal+
.   .   .   quit_transformation+
.   .   .   reorder_clause+
.   .   .   skip_cr+
+++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
int step_asking()		/* c.t. step trace --> 0(auto),1(cont) */
{
    tprint0("\n@step <h,b,q,z,u,s,n,CR>?  ");
    while(1)
    {
	switch(getchar())
	{
	  case '?' :
	  case 'h' :
	    tprint0("NOTATION: [<clause No>(<status>,<literal No.>)]");
	    tprint0("New Predicate <=> unmodular body\n");
	    tprint0("\t<STATUS> : U=untouched, M=modular_defined,")
	    tprint0("I=unit_defined, D=Derived,\t\tG=registered,");
	    tprint0("F=False, R=Reduced, T=Temporary\n");
	    tprint0("COMMNAD: q:quit\tz:abort");
	    tprint0("\tn:normal trace\tx:trace off");
	    tprint0("\nb:break\tCR: continue");
	    tprint0("\tu <clausese No.> <literal No.>: manual unfolding\n");
	    skip_cr();
	    break;
	  case 'b': {
	    int  *hsave = hp;
	    struct pair *esave = ep;
	    struct ustack *usave = utop;
	    struct cset *deflist_save = DEF_list, *cstrlist_save = CSTR_list,
	    	*initdeflist_save = INITDEF_list;
	    struct clause *constliterals_save = CONST_literals,
	    	*restliterals_save = REST_literals;
	    int cstrnumber_save = CSTR_number;

	    utop = usp; 
	    if (setjmp(unbreak_reset)) {
	      utop = usave; hp = hsave; ep = esave;
	      DEF_list = deflist_save; CSTR_list = cstrlist_save;
	      INITDEF_list = initdeflist_save;
	      CONST_literals = constliterals_save;
	      REST_literals = restliterals_save;
	      CSTR_number = cstrnumber_save;
	      break;
	    }
	    while(1) {
	      prolog_execution();
	    }
	  }
	  case 'q' : quit_transformation(); /* quit */
	    longjmp(trans_fail,1);
	  case 'z' : abandon_transformation(); /* abort */
	    longjmp(trans_fail,1);
	  case 'u' : {int cnum,lnum; /* manual unfolding */
		      struct cset *tc;
		      struct clause *tl;
		      scanf("%d %d",&cnum,&lnum);
		      skip_cr();
		      tc = nth_cset(cnum);
		      if (tc == NULL) {
			tprint1("Error: no clause %d",cnum);
			break;
		      }
		      tl = nth_literal(tc->cs_clause->c_link,lnum);
		      if (tl == NULL)
			{
			  tprint0("Error: literal out of range");
			  break;
			}
		      tc->cs_status = REMOVED;
		      if (tc->cs_status != DERIVATION) /* in CSTR_list */
			      Pred(tc->cs_clause->c_form)->f_setcount--;
		      reorder_clause(tc->cs_clause, tl);
		      tprint1("manual_unfold [%d] ",lnum);
		      Pterm(tc->cs_clause->c_link->c_form,NULL);
		      if (apply(tl->c_form,tc->cs_clause->c_form,
				tl->c_link,tc->cs_anumber) 
			  == FALSE)
			tprint0(" ->FAIL\n")
		      else
			tprint0(" =>TRUE\n")
			  return(1);
		    }
	  case 'x' : CTnotrace; Notrace_mode;
	    skip_cr();return(0); /* no trace */
	  case 'n' : CTnormal; skip_cr();return(0);/* normal trace */
	  case '\n': return(0); /* continue in automode */
	  default  : break;
	}
   }
}

struct cset *nth_cset(n)	/* cset whose cs_number = n */
int n;
{
	register struct cset *c;
	for (c = DEF_list; c != NULL; c = c->cs_link)
		if (c->cs_status == DERIVATION && 
		    c->cs_number == n) return(c);
	for (c = CSTR_list; c != NULL; c = c->cs_link)
		if (c->cs_status != REMOVED &&
		    c->cs_number == n) return(c);
	return(NULL);
}

struct clause *nth_literal(cl,n)
struct clause *cl;
int n;
{
	register struct clause *c;
	register int i;

	for (c = cl, i = 1; c != NULL; c = c->c_link, i++)
		if (i == n) return(c);
	return(NULL);
}

void skip_cr()			/* skip user's input "....CR" */
{
	while( getchar() != '\n') ;
}

void show_newdefs()		/* show newly defined clauses */
{
	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);
		if isnoreduced(f)
			Showfunc(f);
	}
}