/**** Transferred Refutation procedures for generating
      structures satisfying finite constraints.  This 
      module is independent of the specific structures 
      being generated.
           
      The calling program must contain a header:
           
             #define V_LENGTH mmm
             #define SZ       nnn
             #define DONE     xxxx
       
       The constants V_LENGTH and SZ are used to set
       bounds on various arrays.  V_LENGTH is the number
       of variables to be assigned values, and SZ is the
       maximum number of values possible for a variable.
       A call to transref() passes a parameter of type 
       int representing the length of the actual vectors
       being searched for.  This must be less than V_LENGTH.
       The other parameters are pointers to case-relative 
       functions somewhere outside transref().  The 
       function (*Good)(vec) has to convert the vector vec
       of (unsigned) integers into whatever data structures 
       are testable, call some appropriate test routines 
       and fill in the vector as a boolean array recording 
       a refutation if one was discovered.  The function 
       (*setposs)(vec) must trim vec, now the vector of 
       possible-value sets, by removing unwanted values.  
       It must not add any possible values to it.  If 
       end-of-search status is raised (e.g. because time 
       runs out) this may be recorded by setting the 
       external variable DONE to a nonzero value.  DONE is
       defined in the header as some global variable such
       as  global_memory->problem_done.


*************************************************************
************************************************************/

#define STAK_MAX 7000
#define CUT_MAX  100
#define TOOBIG 350
#define MAXREF   (fixt/3)+2

#define REF struct ref

REF { int force, xyz; 
      REF *up, *back, *forth, *next, *last;
    } *dummy, *yonder;

int oldvect[V_LENGTH],      /* The Way We Were         */
    vpos[V_LENGTH],         /* Vector positions        */
    skip,                   /* Bottom of refutation    */
    ts,                     /* Cell totally suspended  */
    recs,                   /* Amount of stack used    */
    susguy,                 /* The suspended cell      */
    cells,                  /* Actual vector length    */
    maxval,                 /* Max. poss. values/cell  */
	poss_tot,               /* Not "toss_pot"!         */
    fixt,                   /* Active vector length    */
    notop,                  /* Topless refutation      */
    novect,                 /* No remaining good guy   */
    newcut,                 /* Cut made on this pass   */
    rpt,                    /* Repeating after cut     */
    cutptr;                 /* Depth of cut-and-guess  */

unsigned poss[V_LENGTH],    /* Poss. values in order   */
         val[V_LENGTH],     /* Actual values of cells  */
         used[V_LENGTH],    /* Latest refutation       */
         comvec[V_LENGTH],  /* communication vector    */
         cuts[CUT_MAX][3];  /* Cut-and-guess divisions */

REF Dum, Yon,               /* The actual dummies      */
    stak[STAK_MAX],         /* A chunk of memory       */
     inx[V_LENGTH][SZ];     /* Index to the stack      */


/************************************************************
************************************************************/

transref( length, Test, Setposs )  
          int length, (*Test)(), (*Setposs)();
{
   tr_initial(length);
   while ( prepared( Setposs ) )
   if ( poss_tot > TOOBIG ) cut_and_guess();
   else search( fixt-1, Test );
}


/************************************************************
************************************************************/

search(x,Test)  int x, (*Test)();
                          /*** Generate all vectors on 
                               the subspace up to x that
                               satisfy function Test     ***/
{ 
   int i;
   
   if ( x < 0 )                       /** Vector complete **/
   {
      for ( i = 0; i < cells; i++ ) comvec[vpos[i]] = val[i];
      if ( !(*Test)(comvec) ) addref();
      return(0);
   }
   
   for ( val[x] = rpt? oldvect[x]: 0; 
         val[x] <= maxval;  val[x]++ )
   if ( poss[x] & ( 1 << val[x] ))
   {
      invalue( x );
      if ( !ts ) search( x-1, Test );
      if ( DONE ) novect = 1;
      if ( ts && !novect ) totsus();
      if ( novect ) break;
      outvalue( x );
      if ( x < skip ) break;
   }
   val[x] = 0;
   if ( x == fixt-1 ) novect = 1;
}



/***********************************************************/

invalue(x)  int x;
                          /*** Insert val[x] in cell x.
                               Transfer all active
                               refutations downward.     ***/
{ register REF *ptr,*pd;
  
  ts = 0; susguy = 0;  skip = -1;
  if ( !x || val[x] > oldvect[x] ) rpt = 0;
  
  for ( ptr = inx[x][val[x]].next; 
        ptr!=dummy; ptr = ptr->next )
  { 
     pd = ptr->forth;
     if (( pd->force += ptr->force ) == ptr->force ) 
     { 
        pd->back = ptr;
        if ( pd->forth == dummy )
        { 
           if ( !(poss[pd->xyz/SZ] &= ~(1 << (pd->xyz%SZ)) ))
           { 
              ts = 1; 
              if ( pd->xyz/SZ > susguy ) susguy = pd->xyz/SZ;
           }
        }
        else
        { 
           pd->last = (*inx)+(pd->xyz);
           pd->next = pd->last->next;
           pd->last->next->last = pd;
           pd->last->next = pd;
        }
     }
  }
}



/***********************************************************/

outvalue(x)  int x;       /*** Opposite of invalue: take 
                               value out, undo transfers ***/
{ register REF *ptr,*pd;
  
  ptr = &inx[x][val[x]];
  if ( ptr->back == yonder ) 
  { 
     ptr->force = 0;
     poss[x] |= 1 << val[x];
  }
  while ( ptr->next != dummy )
  { 
     ptr = ptr->next;
     pd = ptr->forth;
     if ( !( pd->force -= ptr->force ))
     { 
        pd->back = dummy;
        if ( pd->forth == dummy )
        poss[pd->xyz/SZ] |= 1 << (pd->xyz%SZ);
        else
        { 
           pd->last->next = pd->next;
           if ( pd->next != dummy ) pd->next->last = pd->last;
        }
     }
     if ( ptr->back == yonder )
     { 
        ptr->force = 0;
        ptr->last->next = ptr->next;
        if ( ptr->next != dummy ) ptr->next->last = ptr->last;
     }
  }
} 



/***********************************************************/

setref()    /*** Trim the refutation as recorded in used[].
                 Remove the top if necessary. Return its 
                 cardinality.                            ***/
{ register int i,j;
  int k;

  k = notop = 0;
  for ( i=0; i<fixt; i++ ) if ( used[i] ) 
  {
     k++;
     if ( skip < 0 ) skip = i;
  }
  if ( !k ) novect = 1;
  else
  { 
     for ( i--; i>skip && used[i]; i-- )
     if ( i < fixt-1 )
     { 
        used[i+1] = 0;  notop = 1;
        k--;
     }
     j = i+1;
     while ( k > MAXREF )
     { 
        if ( used[--i] )
        { 
           used[j] = 0;
           notop = 1;  k--;  j = i;
        }
     }
     if ( notop && k==1 ) used[skip] = k = 0;
  }
  return(k);
}



/***********************************************************/

addref()
                    /*** Incorporate the refutation in the 
                         appropriate active lists.       ***/
{ register REF *here;
  register int i;
  int k,trunk;
  REF *there, *newguy();
  
  if ( skip < 0 )
  for ( i = 0; i < fixt; i++ ) used[i] = comvec[vpos[i]];
  k = setref();
  if (!k) return(0);
  trunk = 1;  i = skip;  
  here = &inx[i][val[i]];  here->force = 1;  
  if ( !(poss[i] &= ~(1 << val[i])) ) { ts = 1; susguy = i; }
  
  for (k-- ; k; k--)
  { 
     for ( used[i] = 0; !used[i]; i++ ) ;
     there = here;
     if (trunk)
     { 
        for ( here = &inx[i][val[i]];
              here->forth != there && here->up != dummy;
              here = here->up ) ;
        if (here->forth != there) trunk = 0;
     }
     if ( !trunk ) ( here = newguy(i) )->forth = there; 
     here->force++;
     if ( here->xyz > there->back->xyz ) there->back = here;
     if ( here->force == 1 )
     { 
        here->last = &inx[i][val[i]];
        if (( here->next = here->last->next ) != dummy )
        here->next->last = here;
        here->last->next = here;
     }
  }
  
  used[i] = 0;
  here->back = notop? yonder: here;
  if ( recs >= STAK_MAX-MAXREF ) cut_and_guess();
}



/***********************************************************/

REF *newguy(x) int x;    /*** Get next record ***/
{ REF *ng;

  ng = stak+recs++;
  ng->force = 0;
  ng->back = dummy;
  ng->xyz = (x*SZ)+val[x];
  ng->up = ((*inx)+(ng->xyz))->up;
  ((*inx)+(ng->xyz))->up = ng;
  return(ng);
}



/***********************************************************/

totsus()                          /*** Action on detection 
                                   of total suspension ***/
{ 
  while (ts)
  { 
     ts = 0;
     getsus();
     if ( !novect ) addref();
     if ( novect )  return(0);
  }
}



/***********************************************************/

getsus()                       /*** Use the "back" field to 
                                    find a subset doing the 
                                    suspending.  If no top 
                                    fill used[] ***/
{ register REF *ptr;
  register int i;
  int k;
  
  k = fixt;
  for ( i = 0; i <= maxval; i++ )
  { 
     for (ptr = &inx[susguy][i];
          ptr->back != ptr && ptr->back != yonder;
          ptr = ptr->back)
     used[ptr->back->xyz/SZ] = 1;
     if (ptr->back == yonder && k > ptr->xyz/SZ )
     for ( k--; k > ptr->xyz/SZ; k-- ) used[k] = 1;
  }
  for ( skip = susguy+1; skip < fixt; skip++ )
  if ( used[skip] ) return(0);
  novect = 1;
}



/***********************************************************/

cut_and_guess()   /*** Fix the present value in the most 
                       significant cell.  Stack the cut. ***/
{ int i;

  if ( cutptr++ == CUT_MAX ) skipout("Cut stack overflow");
  newcut = rpt = 1;
  for ( i = 0; i < cells; i++ ) oldvect[i] = val[i];
  cuts[cutptr][0] = vpos[fixt-1];
  cuts[cutptr][1] = 1 << val[fixt-1];
  cuts[cutptr][2] = poss[fixt-1];
  for ( i = 0; i <= val[fixt-1]; i++ )
  cuts[cutptr][2] &= ~(1 << i);
  novect = 1;
}



/***********************************************************/

do_cuts()        /*** If backing up after cut-and-guess, go 
                  through the cut stack to recover the old 
                  search space and prime the new.       ***/
{ int i;

  if ( !newcut )
  { 
     while ( cutptr && (!cuts[cutptr][2]) ) cutptr--;
     if ( !cutptr ) novect = 1; else
     {
        cuts[cutptr][1] = cuts[cutptr][2];
        cuts[cutptr][2] = 0;
     }
     rpt = 0;
  }
  newcut = 0;
  for ( i = 1; i <= cutptr; i++ )
  comvec[cuts[i][0]] = cuts[i][1];
}




/***********************************************************/

prepared(Setposs)  int (*Setposs)();
                                      /*** Poss initialised ***/
{ int i,j,k;
  
  if (( novect && !cutptr ) || DONE ) return(0);
  novect = 0;
  for ( i = 0; i < cells; i++ ) 
  comvec[i] = (1 << SZ) - 1;
  for ( i = cells; i < V_LENGTH; i++ ) comvec[i] = 0;
  if ( cutptr ) do_cuts();
  if ( novect ) return(0);
  (*Setposs)(comvec);
  maxval = 0;  poss_tot = 0;
  for ( i = 0; i < cells; i++ ) 
  {
     if ( !comvec[i] ) 
     {
        novect = 1;
        return( prepared(Setposs) );
     }
	 for ( j = 0; j < SZ; j++ ) if ( comvec[i] & (1 << j) )
	 {
		poss_tot++;
        if ( j > maxval ) maxval = j;
	 }
  }
  re_order();
  setinx();
  if ( rpt ) 
  { 
     if ( !set_old() ) 
     {
        novect = 1;
        return( prepared(Setposs) );
     }
  }
  for ( i = 0; i < cells; i++ )
  for ( val[i] = 0; !(poss[i] & (1 << val[i])); val[i]++ ) ;
  skip = -1; recs = 0;
  if ( !fixt ) novect = 1;
  return(1);
}



/**********************************************************/

re_order()                  /*** The old order changeth ***/
{ int i,j,k, newpos[V_LENGTH], newold[V_LENGTH];
  
  k = 0;  fixt = cells;
  for ( i = 0; i < cells; i++ )
  {
     for ( j = 0; !(comvec[i] & (1 << j)); j++ ) ;
     if ( comvec[i] == (1 << j) ) newpos[--fixt] = i;
     else newpos[k++] = i;
  }
  for ( i = 0; i < cells; i++ )
  {
     for ( j =0 ; vpos[j] != newpos[i]; j++ ) ;
     newold[i] = oldvect[j];
  }
  for ( i = 0; i < cells; i++ ) 
  {
     vpos[i] = newpos[i];
     poss[i] = comvec[vpos[i]];
     oldvect[i] = newold[i];
  }
}


/***********************************************************/

setinx()                  /*** Initialise the refutation 
                               lists starting from inx   ***/
{ 
  REF *p;
  int i,j;

  for ( i = 0; i < cells; i++ )
  for ( j = 0; j < SZ; j++ )
  {
     p = &inx[i][j];
     p->xyz = (SZ*i)+j;
     p->force = ( poss[i] & (1 << j) )? 0: 1;
     p->up = p->forth = p->last = p->next = dummy;
     p->back = p->force? p: dummy;
  }
}



/*********************************************************/

set_old()                    /*** Set oldvect[] to the 
                                  next possible vector ***/
{
  int i,j,k;
  
  for ( k = cells-1; k >= 0; k-- )
  {
     for ( i = 0; vpos[i] != k; i++ ) ;
     if ( !(poss[i] & (1 << oldvect[i])) ) break;
  }
  if ( k < 0 ) return(1);
  for ( j = 0; j < cells; j++ )
  if ( vpos[j] < k ) oldvect[j] = 0;
  while ( k < cells )
  {
     for ( i = 0; vpos[i] != k; i++ ) ;
     for ( j = oldvect[i]+1; j <= maxval; j++ )
     if ( poss[i] & (1 << j) )
     {
        oldvect[i] = j; return(1);
     }
     oldvect[i] = 0;
    k++; 
  }
  return(0);
}


/**********************************************************
**********************************************************/

tr_initial(length)  int length;  /*** Set up dummy, yonder, 
                                 cells, maxval, vpos, etc. ***/
{ 
  int i;
  
  if ( !(cells = length) ) 
  skipout("Attempt to search null space");
  Dum.force = Dum.xyz = 0;
  dummy = Dum.up = Dum.forth = Dum.back 
        = Dum.next = Dum.last = &Dum;
  Yon.force = Yon.xyz = 0;
  yonder = Yon.up = Yon.forth = Yon.back 
         = Yon.next = Yon.last = &Yon;
  for ( i = 0; i < cells; i++ ) vpos[i] = i;
  rpt = cutptr = newcut = 0;
  DONE = novect = 0;
}

/**********************************************************
**********************************************************/
skipout(s)  char *s;   /*** Abort job ***/
{ 
  printf("\n\n\n Aborting on detection of an error.\n\n");
  printf(" %s.\n\n", s);
  exit(0);
}