/* ----------------------------------------------------------
%   (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_split.c >>
*          divide constraint into equivalence classes
*      93.8.2 speedup copy_term
*      93.8.2 speedup copy_term
--------------------------------------------------------------------*/

#include "include.h"
#define DEBUG 0
extern struct cset *DEF_list;
extern struct cset *CSTR_list;
extern struct cset *INITDEF_list;
extern int CSTR_number;
extern struct clause *CONST_literals, *REST_literals; 
extern struct itrace *newfsave;
extern jmp_buf trans_fail;

/* sub functions for transform.c (divide clause into equivalence classes)*/
/* this modulue uses global vars: CONST_literals, REST_literals
*
.   .   split+
.   .   .   vconstraint.
.   .   .   attach+
.   .   .   .   is_modular_literal~
.   .   .   .   attach_arg+
.   .   .   .   .   novar
.   .   .   .   .   replace_terms+
.   .   .   .   has_no_var+
.   .   .   .   .   novar~
.   .   .   divide_consts
.   .   .   .   has_no_pst+
.   .   .   delete_constraint+
.   .   .   remove_modular_literals+
.   .   .   .   is_modular_literal~
*/

/* ------------- begin 'split' ------------------ */
struct clause *CONST_PST_literals; /* used in split, divide_consts */

/*+++++++++++++++++++++++++++++++++++++++++++++++++++++++
    split(clist,vlist,anum)
  split a clause clist into equivalence class
     vlist = variable list of clist
     anum = # of variables + # of PSTs in clist
  global vars:
      CONST_literals : no vars and no psts
      REST_literal : modular literals
+++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct compartment *split(clist, vlist, anum)
struct clause *clist;
struct term *vlist;
int anum;
{
	register struct term *v;
	register struct compartment *cmp,*cmplast;
	struct clause *cnext,*remove_modular_literals();
	void divide_consts();

	CONST_literals = NULL; /* global vars */
	REST_literals = NULL;
	CONST_PST_literals = NULL;
	
	clist = remove_modular_literals(clist);
	if (clist == NULL) return(NULL);
	else if (vlist == NULL)	/* no variable */
		divide_consts(clist); /* CONST or CONST_PST? */
	else 
	{
		/* clear_vconstraint(vlist) */
		for (v = vlist; v != NULL; v = vlink(v))
			vconstraint(v) = NULL;
		if (attach(clist, vlist,anum) == FALSE)
		    return((struct compartment *)MFAIL);
		delete_constraint(vlist);
	}

	for (cmplast = NULL; CONST_PST_literals != NULL;
	     CONST_PST_literals = cnext)
	{
		cnext = CONST_PST_literals->c_link;
		CONST_PST_literals->c_link = NULL;
		MEMORY_ALLOC(cmp,compartment,TEMPORAL);
		cmp->cmp_clause = CONST_PST_literals;
		cmp->cmp_link = cmplast;
		cmplast = cmp;
	}
	for (v = vlist; v != NULL; v = vlink(v))
		if (vconstraint(v) != NULL){
			MEMORY_ALLOC(cmp,compartment,TEMPORAL);
			cmp->cmp_clause = vconstraint(v);
			cmp->cmp_link = cmplast;
			cmplast = cmp;
		}
	return(cmplast);
}

/* remove modular literals in cl into REST_literals */
struct clause *remove_modular_literals(cl)
struct clause *cl;
{
	register struct clause *cnext;
	
	if (cl == NULL) return(NULL);
	if (is_modular_literal(cl->c_form))
	{
		cnext = cl->c_link;
		cl->c_link = REST_literals;
		REST_literals = cl;
		return(remove_modular_literals(cnext));
	}
	else 
	{
		cnext = cl->c_link;
		cl->c_link = remove_modular_literals(cnext);
		return(cl);
	}
}

void delete_constraint(vl)	/* vconstraint(v)=NULL for all vl */
struct term *vl;
{
	register struct term *v1, *v2;
	register struct clause *c;

	for (v1 = vl; v1 != NULL; v1 = vlink(v1))
	{
	  if (vconstraint(v1) == NULL) continue;
	  c = vconstraint(v1);
	  for (v2 = vlink(v1); v2 != NULL; v2 = vlink(v2))
	    if (vconstraint(v2) == c) vconstraint(v2) = NULL;
	}
}


int has_no_pst(t)		/* check pst in arguments */
struct term *t;
{
	register int i;

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

void divide_consts(cl)		/* cl: constraint clauses */
struct clause *cl;
{
	register struct clause *c,*cnext;
	for (c = cl; c != NULL; c = cnext)
	{
		cnext = c->c_link;
		c->c_link = NULL;
		if (has_no_pst(c->c_form)) 
		{
			c->c_link = CONST_literals;
			CONST_literals = c;
		}
		else
		{
			c->c_link = CONST_PST_literals;
			CONST_PST_literals = c;
		}
	}
}


int Attached;			/* used in attach, attach_arg */

int attach(c, vl,anum)	/* split main */
register struct clause *c;
struct term *vl;
int anum;
{
	struct clause *cnext;
	register struct term *t;
	register int i, j;

	while (c != NULL) {
	  cnext = c->c_link;
	  c->c_link = NULL;

          t = c->c_form; j = Pred(t)->f_mark;
          if (has_no_var(t)) 
	  {
		  c->c_link = CONST_literals;
		  CONST_literals = c;
	  }
          else if ((j & NON_UNFOLDABLE) != 0) {
            i = satisfiable(c,anum);
            j &= STAY_IF;
            if (((i == TRUE) && (j != 0)) ||
                ((i == FALSE) && (j == 0))) {
              j = Pred(t)->f_arity;
              for (i = 0; i < j; i++)
                attach_arg(Arg(t,i),c,vl);
            }
            else if ((i == TRUE) && (j == 0))
              /* do nothing */ ;
            else /* in case of FAIL */
		return(FALSE);
          }
	  else if (is_modular_literal(t)) {
	    c->c_link = REST_literals;
	    REST_literals = c;
	  }
	  else {
	    /* attach_term(c,vl); */
	    Attached = 0;
	    j = Pred(t)->f_arity;
	    for (i = 0; i < j; i++)
	      attach_arg(Arg(t,i),c,vl);
	    if (Attached == 0) divide_consts(c);
	  }
	  c = cnext;
	}
	return(TRUE);
}

void attach_arg(arg,c,vl)	/* sub of attach */
struct term *arg,*vl;
struct clause *c;
{
  register int i;

  if (novar(arg)) return;

/*  printf("attach_arg arg=");Pterm(arg,NULL);
  printf(" c=");Pclause(c,NULL);
  NL;  
*/  
  if (isvar(arg)) {
    if (arg->type.ident == VAR_GLOBAL_TYPE) {  /* 1991-03-02 */
      if (vconstraint(arg) == NULL) vconstraint(arg) = c;
      else replace_terms(vconstraint(arg),c,vl);
      Attached = 1;		/* global var */
      return;
    }
    else return;
  }

  if (is_list(arg) || is_clause(arg)) {
    attach_arg(head_of_list(arg),c,vl);
    attach_arg(tail_of_list(arg),c,vl);
    return;
  }
  if (is_pst(arg)) {
    struct eclause *plists;
    plists = ((struct pst *)arg)->p_lists;
    while (plists != NULL_ECL) {
      attach_arg(Arg2(plists->c_form),c,vl);
      plists = plists->c_link;
    }
    return;
  }
  for (i = 0; i < Pred(arg)->f_arity; i++)
    attach_arg(Arg(arg,i),c,vl);
}


void replace_terms(c1,c2,vl)
struct clause *c1;
register struct clause *c2;
struct term *vl;
{
  register struct term *v;

  if (c1 == c2) return;
  for (v = vl; v != NULL; v = vlink(v))
    if (vconstraint(v) == c1) vconstraint(v) = c2;
  while (c2->c_link != NULL)
    c2 = c2->c_link;
  c2->c_link = c1;
}
/* ------------- end of 'split' ------------------ */



/* --------------- begin 'variant' ---------------- */
struct vpair *VPAIR;		/* vpair of var,pst */
int Consider_Vacuous,		/* consider vacuous or not */
	PST_level;		/* depth of pst */

#define TPHASHSIZE 59
struct vpair *Tpair[TPHASHSIZE];	/* hashed vpair for terms */

int termpairtype(t)
struct term *t;
{
    return(((int)t) % TPHASHSIZE); 
}

void print_Tpair_length()	/* for debug */
{
    int i;
    for (i=0; i<TPHASHSIZE; i++) printf("%d ",vpair_length(Tpair[i]));
    printf(":%d \n",vpair_length(VPAIR));
}

void clear_Tpair()
{
    register int i;
/*    print_Tpair_length();  (for debug) */
    for (i=0; i<TPHASHSIZE; i++) Tpair[i]=(struct vpair *)NULL;
}

void Pvariant(va)
struct variant *va;
{
	struct vpair *vp;
	Pclause(va->v_clause,NULL);
	if (va->v_pair == NULL) return;
	putchar('\n');
	for (vp=va->v_pair; vp != NULL; vp=vp->v_link)
	{
		printf("<");
		Pterm(vp->v1,NULL);putchar(',');
		Pterm(vp->v2,NULL);putchar('>');
	}
}

void Pvpair(va)
struct vpair *va;
{
	register struct vpair *vp;
	for (vp=va; vp != NULL; vp=vp->v_link)
	{
		printf("<");
		Pterm(vp->v1,NULL);putchar(':');
		Pterm(vp->v2,NULL);printf("> ");
	}
}

int vpair_length(vp)
struct vpair *vp;
{
	register int i;
	for(i = 0; vp != NULL; i++, vp=vp->v_link);
	return(i);
}

/*
[variant]----------------------------------- 
.   copy_clause
.   .   copy_term
.   .   .   Npstobj~
.   .   .   in_sheap~
.   .   .   copy_arg+
.   .   .   .   has_common_label
.   .   .   .   store_vpair
.   .   .   exist_termpair.
.   .   .   exist_vpair.
.   .   .   copy_pst+
.   .   .   .   Npst
.   .   .   .   store_vpair~
.   .   .   .   copy_eclause+
.   .   .   store_termpair
.   .   .   var_trans+
.   .   .   .   store_vpair~
*/
/*++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
  variant(cl,flag)      : normal copy
  variant_v(cl,flag)	: consider vacuous arguments
  make a variant of a clause cl
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++*/
struct variant *variant_main(cl,flag)
struct clause *cl;
int flag;
{
	struct variant *ccopy;
	
	VPAIR = (struct vpair *)NULL;		/* global vars */
	clear_Tpair();
	v_list = pv_list = NULL;
	v_number = p_number = 0;
	PST_level = 0;
	MEMORY_ALLOC(ccopy,variant,TEMPORAL);
	ccopy->v_clause = copy_clause(cl,flag);
	ccopy->v_var = v_list;
	ccopy->v_anum = v_number + p_number;
	ccopy->v_pair = VPAIR;
	if (p_number != 0)
		renum_pvars((struct pstvar *)pv_list,v_number);
/* 	print_Tpair_length();  */
	return(ccopy);
}

struct variant *variant(cl,flag)
struct clause *cl;
int flag;
{
	Consider_Vacuous = 0;
	return(variant_main(cl,flag));
}    


struct variant *variant_v(cl,flag) /* variant considering vacuous args */
struct clause *cl;
int flag;
{
	Consider_Vacuous = 1; 
	return(variant_main(cl,flag));
}

void store_vpair(told,tnew)	/* store told->tnew (var,pst)in VPAIR */
struct term *told,*tnew;
{
	register struct vpair *vp,*p,*op;
	
	MEMORY_ALLOC(vp,vpair,TEMPORAL);
	vp->v1 = told; vp->v2 = tnew;

	if (VPAIR==NULL || VPAIR->v1 > told) 
	{
	    vp->v_link = VPAIR;
	    VPAIR = vp;
	    return;
	}
	for (p=VPAIR; p != NULL; op=p,p=p->v_link)
	    if (told < p->v1) break;
	vp->v_link = p;		/* ...op->vp->p->... */
	op->v_link = vp;
}

struct term *exist_vpair(t)	/* check if t is in VPAIR */
struct term *t;
{
	register struct vpair *vp;
	for (vp = VPAIR; vp != NULL; vp = vp->v_link)
	    if (t <= vp->v1) 
	    {
		if (vp->v1 == t) return(vp->v2);
		else return(NULL);
	    }
	return(NULL);
}

void store_termpair(told,tnew)	/* store told->tnew (term) to TermPAIR */
struct term *told,*tnew;
{
	register struct vpair *vp;
	register int tt;

	MEMORY_ALLOC(vp,vpair,TEMPORAL);
	vp->v1 = told; vp->v2 = tnew;
	tt = termpairtype(told);
	vp->v_link = Tpair[tt];
	Tpair[tt] = vp; 
}

struct term *exist_termpair(t)	/* check if t is in TermPAIR */
struct term *t;
{
	register struct vpair *vp;
	for (vp = Tpair[termpairtype(t)]; vp != NULL; vp = vp->v_link)
		if (vp->v1 == t) return(vp->v2);
	return(NULL);
}

struct clause *copy_clause(cl,flag) /* sub. of variant */
struct clause *cl;
int flag;
{
	struct term *copy_term();
	
	if (cl == NULL) return(NULL);
	return(Nclause(copy_term(cl->c_form,flag),
		       copy_clause(cl->c_link,flag),
		       flag)
	       );
}

struct term *copy_term(t,flag)	/* variant of t */
struct term *t;
int flag;
{
  struct term *nt, *copy_pst(), *copy_arg();
  register int i;

  if (t == NULL_TERM || is_atomic(t)) return(t);
  else if (isvar(t)) {
      if ((nt = exist_vpair(t)) != NULL) return(nt); /* check history */
      return(var_trans(t,flag)); /* t is var */
  }
  else if (is_pst(t)) {
      if ((nt = exist_vpair(t)) != NULL) return(nt); /* check history */
      PST_level++;
      nt = copy_pst((struct pst *)t,flag); /* t is PST */
      PST_level--;
      return(nt);
  }
  else if ((nt = exist_termpair(t)) != NULL) return(nt); /* check history */

  switch(t->type.ident) {	/* atom, complex term, eclause */
  case CONST_LIST_TYPE:
	  if (in_sheap(t) || flag != ETERNAL) return(t);
  case LIST_TYPE:
    nt = (struct term *)Nlist(copy_term(head_of_list(t),flag),
		 (struct clause *)copy_term(tail_of_list(t),flag), flag);
    break;
  case CLAUSE_TYPE:
    nt = (struct term *)Nclause(copy_term(head_of_list(t),flag),
		(struct clause *)copy_term(tail_of_list(t),flag),flag);
    break;
  case ECLAUSE_TYPE: /* pst object */
    nt = (struct term *)Npstobj(copy_term(((struct eclause *)t)->c_form,flag),
		 NULL_ENV,
		 (struct eclause *)
		   copy_term((struct term *)((struct eclause *)t)->c_link,
		   	    flag),
		 flag);
    break;
/*  case VAR_VOID_TYPE:
    return(Anonymous_var);
  case VAR_PST_TYPE:
    error("System error occurrs at 'copy_term'"); */
  default:
    if (isconst_functor(t))
	    nt = up_const_functor(t,flag);
    else 
    {
	    nt = Nterm(t->t_arity,flag);
	    Pred(nt) = Pred(t);
	    if (Consider_Vacuous == 1)
		    for (i = 0; i < t->t_arity; i++)
			    Arg(nt,i) = copy_arg(t,i,flag);
	    else 
		    for (i = 0; i < t->t_arity; i++)
			    Arg(nt,i) = copy_term(Arg(t,i),flag);
    }
  }
  store_termpair(t,nt);
  return(nt);
}

struct term *copy_pst(pt,flag)	/* copy pst */
struct pst *pt;
int flag;
{
  register struct pst *p;
  register struct term *nt;
  struct eclause *copy_eclause();

  nt = exist_termpair((struct term *)pt);
  if (nt != NULL)
  {
	  if (PST_level == 1) store_vpair((struct term *)pt,nt);
	  return(nt);
  }
  p = Npst(flag);
  ((struct pstvar *)(p->p_var))->old_var = pt->p_var;
  p->p_lists=(struct eclause *)copy_term((struct term *)pt->p_lists,flag);
  if (PST_level == 1)		/* top level PST */
	  store_vpair((struct term *)pt,(struct term *)p);
  else
	  store_termpair((struct term *)pt,(struct term *)p);
  return((struct term *)p);
}


struct term *var_trans(v, flag)	/* var that corresponds to v */
struct term *v;
int flag;
{
	register struct term *nv;

	if is_voidvar(v) return(Anonymous_var);
	sprintf(nbuf,"V%d",v_number);
	nv = Nvar(nbuf,flag);
	voccurrence(nv) = voccurrence(v);
	vheadoccurrence(nv) = vheadoccurrence(v);
	store_vpair(v,nv);
	return(nv);
}	


struct term *copy_arg(t,i,flag)	/* copy ith argument of t with vacuity check */
struct term *t;
int i,flag;
{
	register struct term *arg,*nt;

	arg = Arg(t,i);
	if (is_pst(arg) && (PST_level == 1) && 
	    !has_common_label(
		       ((struct pst *)arg)->p_lists,Component(Pred(t),i)))
	{
		struct term *nv;
		if ((nt = exist_vpair(arg)) != NULL) 
		    return(nt); /* check history */
		if ((nt = exist_termpair(arg)) != NULL) 
		    return(nt); /* check history */
		sprintf(nbuf,"P%d",v_number);
		nv = Nvar(nbuf,flag);
		store_vpair(arg,nv);
		return(nv);
	}
	else return(copy_term(arg,flag));
}

/* ---------- end of 'variant' ----------------- */