/*                           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.
 */

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

subf_set()            /***  Set up subf and perm  ***/
{
   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]);
}

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

set_u(arr,x)  int arr[], x;          /*** Record variables used
                                          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);
   }
}

/******************************************************************/
 
job_start()
{
  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;
}

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

job_stop()
{
  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);
}



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

set_orders(infil_name)   char infil_name[];
                          /*** 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++) ) ;
}