/* setup.c
*
* These functions have nothing in common except that they
* are called near the outer levels of MaGIC and don't really
* fit into any other category.
*/
/**********************************************************************/
{
int i,j;
for ( i = 0; theJob->form[i].sym; i++ )
{
subf[i].val = 0;
if ( !theJob->form[i].lsub )
{
subf[i].lv = &zero;
subf[i].lsb = -1;
}
else for ( j = 0; j < i; j++ )
if ( theJob->form[i].lsub == theJob->form+j )
{
subf[i].lv = &(subf[j].val);
subf[i].lsb = j;
break;
}
if ( !theJob->form[i].rsub )
{
subf[i].rv = &zero;
subf[i].rsb = -1;
}
else for ( j = 0; j < i; j++ )
if ( theJob->form[i].rsub == theJob->form+j )
{
subf[i].rv = &(subf[j].val);
subf[i].rsb = j;
break;
}
subf[i].mtx = 0;
for ( j = 0; theJob->dcs[j]; j++ )
if ( theJob->dcs[j] == theJob->form[i].sym )
{
switch( theJob->adicity[j] )
{
case 1: subf[i].mtx = monadic[j]; break;
case 2: subf[i].mtx = *(dyadic[j]);
}
break;
}
if ( !subf[i].mtx )
{
switch( theJob->form[i].sym )
{
case '~': subf[i].mtx = N; break;
case 'v': subf[i].mtx = *A; break;
case '&': subf[i].mtx = *K; break;
case 'o': subf[i].mtx = *fus; break;
case '>': subf[i].mtx = *C;
}
}
}
tx = subf+i;
for ( i = 0; i < 4; i++ ) vu[i] = rvu[i] = 0;
if ( theJob->failure )
{
set_u(vu,theJob->failure);
set_u(rvu,theJob->failure);
}
for ( i = 0; theJob->root[i]; i++ ) set_u(vu,theJob->root[i]);
}
/*******************************************************************/
in formula rooted at x ***/
{
if ( x < 0 ) return(0);
if ( x < 4 ) *(arr+x) = 1;
else
{
set_u(arr,subf[x].lsb);
set_u(arr,subf[x].rsb);
}
}
/******************************************************************/
{
char infil_name[50];
set_orders(infil_name);
infil = fopen(infil_name,"r");
if ( *(theJob->outfil_name) && !filing )
{
outfil = fopen(theJob->outfil_name,"a");
filing = 1;
}
if ( theJob->fil_out==PRETTY || theJob->fil_out==SUMMARY )
disp(outfil);
#ifdef PARALLEL
lm_initial();
old_siz = 0;
#endif
CLoCK(&start_time);
if ( theJob->maxtime )
{
theJob->maxtime *= TICK;
theJob->maxtime += start_time;
}
#ifdef HASTIMES
begin_timer = time_buffer.tms_utime;
#endif
good = tot = isoms = 0;
siz = 0;
}
/**********************************************************/
{
if ( theJob->tty_out == UGLY ) printf(" -1\n");
if (theJob->fil_out == UGLY ) fprintf(outfil, " -1\n");
stats_print();
paws();
if ( theJob->maxtime )
{
theJob->maxtime -= start_time;
theJob->maxtime /= TICK;
}
if ( filing ) { fclose(outfil); filing = 0; }
#ifdef PARALLEL
if ( infil ) { fclose(infil); infil = 0; }
DONE = 1;
lm_initial(); /*** That's in case of hanging slaves ***/
#else
fclose(infil);
#endif
logic_axioms(0);
}
/***********************************************************/
/*** Extend the infil_name string
with the input file name ***/
{ int i = 0;
char *s;
if ( theJob->totord ) s = (theJob->f_n? "tn.16": "to.12");
else if ( theJob->f_lat )
{
if ( *(theJob->logic_name) == 'L' )
s = (theJob->f_n? "ln.10": "l.8");
else if ( theJob->axiom[AxBA] ||
( theJob->logic==S4 && theJob->f_n )) s = "ba.16";
else s = (theJob->f_n? "dln.14": "dl.10");
}
else
{
if ( theJob->f_n && theJob->f_t ) s = "pont.8";
else if ( theJob->f_n ) s = "pon.7";
else if ( theJob->f_t ) s = "pot.7";
else s = "po.6";
}
while ( infil_name[i] = DATA_DIR[i] ) i++;
while ( infil_name[i++] = *(s++) ) ;
}
.
