/*                      logic_test.c                   11-11-89


************************************************************
************************************************************
  
     Procedures for testing matrices for satisfaction
     of postulates.  Good_matrix() called from transref().

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


int got_a_fail;             /*** Bad guy fails in matrix ***/

#define SETSKIP(x) { setskip(info,x); return(0); }


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


Good_matrix(info)  unsigned info[];  /***  Test the axioms  ***/
{ int ti;  

/** If compiling for serial execution check at this point whether
 ** any of the break conditions are met, and if so set DONE.
 ** In the parallel version this is done by the master process 
 ** when examining output queues and so is not needed here.
 **/

#ifndef PARALLEL
 int tim;
 if ( theJob->maxtime && !(tot%10) )
  {
     CLoCK(&tim);
     if ( tim > theJob->maxtime ) DONE = 1;
  }
  if ( theJob->maxmat && good == theJob->maxmat) DONE = 1;
  if ( DONE ) return(1);
#endif

/** Now turn the communication vector into the testable data
 ** structures such as C[][].
 **/
 
  vect_into_C(info);
  tot++;
  
/** Next test for satisfaction of the postulates.  Affixing is 
 ** done first because it gives efficient 2-refutations.  The 
 ** user-defined axioms are done last because they usually take
 ** longer to test than pre-defined ones.
 **/
 
  if ( theJob->logic > FD ) 
  if ( !test_affix(info) ) return(0);
    
  for ( ti = 1; ti < AXMAX; ti++ ) if ( theJob->axiom[ti] )
  switch(ti)
  { 
     case AxB:  if ( !Btest(info)  )  return(0);  break;
     case AxB2: if ( !B2test(info) )  return(0);  break;
     case AxW:  if ( !Wtest(info)  )  return(0);  break;
     case AxC2: if ( !C2test(info) )  return(0);  break;
     case AxC:  if ( !Ctest(info)  )  return(0);  break;
     case AxWB: if ( !WBtest(info) )  return(0);
  }
  
  if ( theJob->f_fus )
  if ( !fus_test(info) ) return(0);
  
  if ( !axtest(info) ) return(0);
  if ( theJob->failure && !got_a_fail ) return(1);
  
  if ( isomorphic(istak) ) return(1);

/** We now have a new good matrix.  At this point the serial 
 ** program calls the printup routine.  The parallel version 
 ** puts the matrix in a shared memory store for the master to 
 ** do the actual output later.
 **/
 
#ifdef PARALLEL
  store_mat();
#else
  mat_print();
#endif
  
  return(1);
}


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

vect_into_C(info)   unsigned info[];
{ register int i,j;

  FORALL(i) FORALL(j) C[i][j] = info[cc[i][j]];
  for (i = 0; i < V_LENGTH; i++) info[i] = 0;
}


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

test_affix(info)  unsigned info[];
{
  if ( theJob->f_fus )
  FORALL(ii) if ( maximal[ii] )
  FORALL(jj) if ( maximal[jj] )
  for ( kk = jj+1; kk <= siz; kk++ ) if ( maximal[kk] )
  if ( C[ii][jj] == C[ii][kk] )
  SETSKIP(4)
  
  FORaLL(jj) 
  for ( kk = siz; kk > jj; kk-- ) if ( ord[jj][kk] )
  { 
     FORaLL(ii) 
     {
        if ( !ord[C[kk][ii]][C[jj][ii]] )
        SETSKIP(0)
        if ( !ord[C[ii][jj]][C[ii][kk]] )
        SETSKIP(1)  
     }
  }
    
  if ( theJob->f_lat )
  { 
     FORaLL(jj)  for ( kk = siz-1; kk > jj; kk-- )
     if ( !ord[jj][kk] )
     FORaLL(ii)  
     {
        if ( K[C[ii][jj]][C[ii][kk]] != C[ii][K[jj][kk]] )
        SETSKIP(2)
        if ( K[C[jj][ii]][C[kk][ii]] != C[A[jj][kk]][ii] )
        SETSKIP(3)
     }
  }
  return(1);
}


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

Btest(info)  unsigned info[];
{
  FORaLL(ii)  FORaLL(jj)  FORaLL(kk)
  if ( !ord[C[jj][kk]][C[C[ii][jj]][C[ii][kk]]] )
  SETSKIP(AxB)
  return(1);
}

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

B2test(info)  unsigned info[];
{
  FORaLL(ii)  FORaLL(jj)  FORaLL(kk)
  if ( !ord[C[ii][jj]][C[C[jj][kk]][C[ii][kk]]] )
  SETSKIP(AxB2); 
  return(1);
}

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

C2test(info)  unsigned info[];
{
  FORaLL(ii)  FORaLL(jj)
  if ( !ord[ii][C[C[ii][jj]][jj]] )
  SETSKIP(AxC2)
  return(1);
}

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

Wtest(info)  unsigned info[];
{
  FORaLL(ii)  FORaLL(jj)
  if ( !ord[C[ii][C[ii][jj]]][C[ii][jj]] )
  SETSKIP(AxW)
  return(1);
}

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

Ctest(info)  unsigned info[];
{
  FORaLL(ii)  FORaLL(jj)  FORaLL(kk)
  if ( C[kk][C[ii][jj]] != C[ii][C[kk][jj]] )
  SETSKIP(AxC)
  return(1);
}

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

WBtest(info)  unsigned info[];
{
  FORaLL(ii)  FORaLL(jj)  FORaLL(kk)
  if ( !ord[K[C[ii][jj]][C[jj][kk]]][C[ii][kk]] )
  SETSKIP(AxWB)
  return(1);
}


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

fus_test(info)  unsigned info[];
                          /* Define fus[a][b] as the least x
                             such that ord[a][C[b][x]].
                             Check that this exists and is 
                             also least in the relation ord */
{ int i,j,k,m;

  if (( theJob->logic == RW || theJob->logic == R 
        || theJob->logic == CK ) && theJob->f_n )
  {
     FORALL(i) FORALL(j) fus[i][j] = N[C[i][N[j]]]; 
     return(1);
  }
  FORaLL(i) FORaLL(j)
  {
     FORALL(fus[i][j]) 
     if ( ord[i][C[j][fus[i][j]]] ) break;
     if ( fus[i][j] > siz )
     {
        FORALL(k) info[cc[j][k]] = 1;
        return(0);
     }
     for ( k = fus[i][j]+1; k <= siz; k++ )
     if ( ord[i][C[j][k]] && !ord[fus[i][j]][k] )
     {
        for ( m = 0; m <= fus[i][j]; m++ )
        info[cc[j][m]] = 1;
        info[cc[j][k]] = 1;
        return(0);
     }
  }
  return(1);
}



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

axtest(info)   unsigned info[];
                      /*** Test the user-defined axiom(s) ***/
{ register SBF *w;
  int i,j;
  
  got_a_fail = 0;
  if ( !*(theJob->root) && !theJob->failure ) return(1);
  if ( *(theJob->defcon) ) setcon();
  for ( i = 0; i < CMAX; i++ ) 
  subf[theJob->atom[0][i]].val = subf[theJob->atom[1][i]].val = 0;
  for ( i = 0; i < 4; i++ ) subf[i].val = siz;
  
WORK:  for ( w = subf+8+(CMAX*3); w != tx; w++ )
       w->val = *(w->mtx + *(w->lv)*SZ + *(w->rv));

       for ( i = 0; theJob->root[i]; i++ )
       if ( !true[subf[theJob->root[i]].val] )
       SETSKIP(-1-i)
       if ( !true[subf[theJob->failure].val] ) 
       {
          got_a_fail = 1;
          for ( i = 0; i < 4; i++ ) 
          badvalue[i] = rvu[i]? subf[i].val: SZ;
       }
  
       for ( i = 0; i < 4; i++ ) 
       if ( vu[i] )         
       { 
          if ( subf[i].val )
          { 
             subf[i].val--; 
             goto WORK;
          }
          subf[i].val = siz;
       }
       
  return(1);
}



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

setskip(info,x)  unsigned info[]; int x;
                    /*** Record test failure in info[]. ***/
{
  if ( x >= 0 )
  { 
     if ( x && x != 3 ) info[cc[ii][jj]] = 1;
     switch(x)
     { 
        case 0:    info[cc[kk][ii]] = 1;
                   info[cc[jj][ii]] = 1;               break;
        case 1:    info[cc[ii][kk]] = 1;               break;
        case 2:    info[cc[ii][kk]] = 1;
                   info[cc[ii][K[jj][kk]]] = 1;        break;
        case 3:    info[cc[jj][ii]] = 1;
                   info[cc[kk][ii]] = 1;
                   info[cc[A[jj][kk]][ii]] = 1;        break;
        case 4:    info[cc[ii][kk]] = 1;               break;
        case AxW:  info[cc[ii][C[ii][jj]]] = 1;        break;
        case AxB:  info[cc[ii][kk]] = 1;
                   info[cc[jj][kk]] = 1;
                   info[cc[C[ii][jj]][C[ii][kk]]] = 1; break;
        case AxB2: info[cc[ii][kk]] = 1;
                   info[cc[jj][kk]] = 1;
                   info[cc[C[jj][kk]][C[ii][kk]]] = 1; break;
        case AxC2: info[cc[C[ii][jj]][jj]] = 1;        break;
        case AxWB: info[cc[jj][kk]] = 1;
                   info[cc[ii][kk]] = 1;               break;
        case AxC:  info[cc[kk][jj]] = 1;
                   info[cc[ii][C[kk][jj]]] = 1;
                   info[cc[kk][C[ii][jj]]] = 1;
     }
  }
  else set_used(info,theJob->root[-1-x],1); 
}


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

set_used(info,x,topper)  unsigned info[];  int x, topper;
                                    /*** Recursive part ***/
{
  int i;
  SBF *sf;  WFF *wf;
  
  if ( x < 0 ) return(0);
  sf = subf+x;  wf = theJob->form+x;
  set_used(info,sf->lsb,0);
  set_used(info,sf->rsb,0);
  if ( wf->sym == '>' && !topper ) 
  info[cc[*(sf->lv)][*(sf->rv)]] = 1;
  else if ( wf->sym == 'o' )
  {
     if ( theJob->f_n && 
     ( theJob->logic == RW || theJob->logic == R || theJob->logic == CK ))
     info[cc[*(sf->lv)][N[*(sf->rv)]]] = 1; 
     else for ( i = 0; i <= sf->val; i++ ) 
     info[cc[*(sf->rv)][i]] = 1;
  }
  else for ( i = 0; theJob->dcs[i]; i++ ) 
  if ( theJob->dcs[i] == wf->sym )
  { 
     if ( theJob->adicity[i] == 2 )
     {
        subf[theJob->atom[0][i]].val = *(sf->lv);
        subf[theJob->atom[1][i]].val = *(sf->rv);
     }
     else if ( theJob->adicity[i] == 1 ) 
     subf[theJob->atom[0][i]].val = *(sf->rv);
     set_used(info,theJob->defcon[i],0);
     break;
  }
  if ( wf->rsub )
  sf->val = *(sf->mtx + ((*(sf->lv))*SZ + *(sf->rv)));
}

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

getval(x)  SBF *x;
{
  if ( x->rsb < 0 ) return(x->val);
  if ( x->lsb < 0 ) return(*(x->mtx + getval(subf+x->rsb)));
  return(*(x->mtx + SZ*getval(subf+x->lsb) + getval(subf+x->rsb)));
}
  
          /******************************************/

setcon()       /*** Derive matrices for defined connectives ***/
{ int i,j,k,m;

  for ( i = 0; theJob->defcon[i]; i++ )
  switch(theJob->adicity[i])
  { 
     case 0: nulladic[i] = subf[8+i].val = 
             getval(subf+theJob->defcon[i]); 
             break;
     case 1: FORALL(j)
             { 
                for ( m = 0; m < CMAX; m++ )
                subf[theJob->atom[0][m]].val = j;
                monadic[i][j] = getval(subf+theJob->defcon[i]);
             }
             break;
     case 2: FORALL(j)
             { 
                for  (m = 0; m < CMAX; m++ )
                subf[theJob->atom[0][m]].val = j;
                FORALL(k)
                { 
                   for ( m = 0; m < CMAX; m++ )
                   subf[theJob->atom[1][m]].val = k;
                   dyadic[i][j][k] = getval(subf+theJob->defcon[i]);
                }
             }
  }
}