/**** 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;
nt 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 );
}
/************************************************************
************************************************************/
/*** 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;
}
/***********************************************************/
nvalue(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;
}
}
}
/***********************************************************/
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);
}
}
/***********************************************************/
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;
}
/***********************************************************/
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];
}
/***********************************************************/
/*** 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);
}
/**********************************************************/
{ 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];
}
}
/***********************************************************/
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;
}
}
/*********************************************************/
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;
}
/**********************************************************
**********************************************************/
{
printf("\n\n\n Aborting on detection of an error.\n\n");
printf(" %s.\n\n", s);
exit(0);
}
.
