/*                      logic_set.c                   11-11-89 


************************************************************
************************************************************

 *****  The procedures going with set_poss() called    *****
 *****  from the search.  Also pre_set() called from
 *****  job_initial().                                 *****


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

#define BADVAL(x,y,z) info[cc[x][y]] &= ~(1 << z);

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


pre_set()
{ int i;

  logic_axioms(1);
  for ( i = 0; i < AXMAX; i++ )
  if ( theJob->axiom[i] )
  switch(i)
  {
     case AxX:   if ( !Exmid() ) return(0);    break;
     case AxBA:  if ( !Boolalg() ) return(0);  break;
     case AxSBA: if ( !SemiBool() ) return(0); break;
     case AxK2:  if ( !paradox() ) return(0);
  }
  if ( theJob->f_T ) FORALL(i) if ( !ord[i][siz] ) return(0);
  if ( theJob->f_F ) FORALL(i) if ( !ord[0][i] ) return(0); 
  return(1);
}


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



set_poss(info)  unsigned info[];
                    /*** Trim poss, according to the logic ***/
{ int i,j,k;
  
  FORALL(i) FORALL(j)
  {
     for ( k = siz+1; k < SZ; k++ )
     BADVAL(i,j,k)
     FORALL(k) if IFF( (ord[i][j]),(!true[k]) )
     BADVAL(i,j,k)
  }
  
  if ( !logic_poss(info) ) return(0);
  if ( theJob->logic > FD ) 
  {
     if ( theJob->f_fus ) fusion(info);
     affix(info);
  }
  efficient_logic_set();
    
  return(1); 
}



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

fusion(info)  unsigned info[];
{ int i,j,k;

  FORALL(i) if ( maximal[i] )
  FORALL(j) if ( !maximal[j] )
  FORALL(k) BADVAL(k,i,j)
}

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

affix(info)   unsigned info[];
{ register int k,m;
  int i,j;

  FORALL(i)  FORALL(j)
  for ( k = 0; k <= i; k++ )
  if ( ord[k][i] )
  { 
     for ( m = j; m <= siz; m++ ) 
     if ( ord[j][m] ) squeeze( info, i, j, k, m );
  }
}



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

squeeze(info,a,b,c,d)  unsigned info[];  int a,b,c,d;
                                  /*** Affixing: ab < cd ***/
{ register int i,j;
  int k,m;

  k = cc[a][b]; m = cc[c][d];
  FORALL(i)
  { 
     if ( info[k] & (1 << i) )
     { 
        for ( j = i; 
              j <= siz && !(ord[i][j] && (info[m] & (1<<j)));
              j++) ;
      if ( j > siz ) BADVAL(a,b,i)
     }
     if ( info[m] & (1 << i) )
     { 
        for ( j = i; 
              j >= 0 && !(ord[j][i] && (info[k] & (1 << j)) );
              j--) ;
        if ( j < 0 ) BADVAL(c,d,i)
     }
  }
}


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


permutable(a,b,c,info)  int a,b,c;  unsigned info[];
                                         /*** Permutation ***/
{ register int i,j;
  int k, m, All=1, None=1;
  
  k = cc[a][c];  m = cc[b][c];
  FORALL(i)
  if ( info[m] & (1 << i) )
  {
     if ( ord[a][i] ) None = 0; else All = 0;
  }
  if ( All )
  {
     FORALL(i)
     if ( !ord[b][i] ) BADVAL(a,c,i)
  }
  if ( None )
  {
     FORALL(i)
     if ( ord[b][i] ) BADVAL(a,c,i)
  }
  if ( !info[k] ) return(0);
  return(1);
}



/***********************************************************
*****                                                  *****
*****  Now the highly logic-specific axiom tests etc   *****
*****                                                  ****/


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

Exmid()                /***   a v ~a   ***/
{ int i;

  FORALL(i)
  if ( !true[A[i][N[i]]]) return(0);
  return(1);
}

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

Boolalg()              /***   a&~a -> b   ***/
{ int i;

  FORALL(i)
  if ( A[i][N[i]] != siz ) return(0);
  return(1);
}

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

SemiBool()             /***   a&~a -> bv~b   ***/
{ int i,j;

  FORALL(i) FORALL(j)
  if ( !ord[K[i][N[i]]][A[j][N[j]]] ) return(0);
  return(1);
}

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

paradox()              /***   des = T   ***/
{ int i;

  FORALL(i) if ( !ord[i][des] ) return(0);
  return(1);
}


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

E_assertion(info)  unsigned info[];  /***   t->a -> a   ***/
{ int i,j,k;

  FORALL(i) FORALL(j)
  if ( !ord[j][i] )
  FORALL(k)
  if ( true[k] ) BADVAL(k,i,j)
}


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

contraction(info)   unsigned info[];
{
  if ( theJob->f_lat ) Wstar(info);
  if ( theJob->f_n ) Reductio(info);
}


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

Wstar(info)   unsigned info[]; /***   a & (a->b) -> b   ***/
{ int i,j,k;

  FORALL(i) FORALL(j) FORALL(k)
  if ( !ord[K[i][k]][j] )
  BADVAL(i,j,k)
}

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

Reductio(info)  unsigned info[];  /***   a->~a -> ~a   ***/
{ int i,j;

  if ( theJob->f_lat ) Exmid();
  FORALL(i) FORALL(j)
  if ( !ord[j][N[i]] )
  BADVAL(i,N[i],j)
}


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

assertion(info)  unsigned info[];   /***   0->a = T
                                     t->a = a   ***/
{ int i,j;
  
  FORALL(i) FORALL(j)
  { 
     if ( j < siz ) BADVAL(0,i,j)
     if ( j != i ) BADVAL(des,i,j)
  }
}


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

ata(info)   unsigned info[];  /***   a ->. t->a   ***/
{ int i,j;

  FORALL(i) FORALL(j)
  if (!ord[i][j])
  BADVAL(des,i,j)
}


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

TaT(info)   unsigned info[];  /***   T ->. a->T   ***/
{ int i,j;

  FORALL(i) if ( !ord[i][siz] ) return(*info = 0);
  FORALL(i) FORALL(j)
  if ( j < siz ) BADVAL(i,siz,j)
}


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

mingle(info) unsigned info[];  /***   a ->. a->a   ***/
{ int i,j;

  FORALL(i) FORALL(j)
  if ( !ord[i][j] )
  BADVAL(i,i,j)
}

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

f_arrow_t(info)  unsigned *info;  /***   f -> t   ***/
{
  if ( !ord[N[des]][des] ) *info = 0;
}

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

t_atomic(info)  unsigned info[]; /***   p v (p -> q)   ***/
{
  int i,j,k;
  
  FORALL(i) FORALL(k) if ( !true[A[i][k]] ) 
  FORALL(j) BADVAL(i,j,k)
}

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

FF_T(info)  unsigned info[];  /***   T ->. F -> F   ***/
{
  int i,j;
  
  FORALL(i) if ( !ord[0][i] || !ord[i][siz] ) *info = 0;
  FORALL(i) FORALL(j)
  if ( j < siz ) BADVAL(0,i,j)
  if ( F_N || theJob->axiom[AxB] || theJob->axiom[AxB2] )
  FORALL(i) FORALL(j)
  if ( j < siz ) BADVAL(i,siz,j)
}

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

PARADOX(info)  unsigned info[];  /***   a ->. b->a   ***/
{ int i,j,k;

  if ( !paradox() ) *info = 0;
  FORALL(i)  FORALL(j)  FORALL(k)
  if ( !ord[j][k] )
  BADVAL(i,j,k)
}


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

RWX(info)  unsigned info[];     /*** If LEM holds,  
                                 a+1 & (a+1->0) = 0 ***/
{ int i,j;

  FORALL(i) if ( !true[A[i][N[i]]] ) return(1);
  FORALL(i) if ( i )
  FORALL(j) if ( K[i][j] ) BADVAL(i,0,j)
}



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

logic_poss(info)   unsigned info[];
{ int i,j,k;

  if ( theJob->logic==R ) TaT(info);
  if ( theJob->logic==RW && theJob->f_n && theJob->f_lat ) RWX(info);
  for ( i = 1; i < 20; i++)  if ( theJob->axiom[i] )
  {
     switch(i)
     { 
        case AxW2:  Wstar(info);       break;
        case AxK:   PARADOX(info);     break;
        case AxM:   mingle(info);      break;
        case AxRED: Reductio(info);    break;
        case AxC3:  E_assertion(info); break;
        case AxCt:  ata(info);         break;
        case Axat:  t_atomic(info);    break;
        case AxTF:  FF_T(info);
     }
     if ( !*info ) return(0);
  }
  if ( theJob->logic==RW || theJob->logic==R || theJob->logic==CK 
                 || theJob->axiom[AxC] || theJob->axiom[AxC2] )
  FORALL(i) FORALL(j) FORALL(k) 
  if ( !permutable( i, j, k, info ) ) return(0);
  
  return(*info);
}



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

logic_axioms(x)   /*** Set or unset axioms for the logic ***/
{
  if ( theJob->logic > DW ) theJob->axiom[AxB] = theJob->axiom[AxB2] = x;
  switch(theJob->logic)
  { 
     case EW: theJob->axiom[AxC3]  = x; break;
     case RW: theJob->axiom[AxC3]  = theJob->axiom[AxCt]  = x;
              theJob->axiom[AxC2]  = theJob->axiom[AxC]   = x;
                                     theJob->axiom[AxTF]  = x;  break;
     case  T: theJob->axiom[AxRED] = theJob->axiom[AxW2]  = x;
              theJob->axiom[AxX]   = theJob->axiom[AxW]   = x;
                                     theJob->axiom[AxWB]  = x;  break;
     case  E: theJob->axiom[AxRED] = theJob->axiom[AxC3]  = x;
              theJob->axiom[AxW]   = theJob->axiom[AxW2]  = x;
              theJob->axiom[AxWB]  = theJob->axiom[AxX]   = x;  break;
     case  R: theJob->axiom[AxRED] = theJob->axiom[AxW2]  = x;
              theJob->axiom[AxC3]  = theJob->axiom[AxCt]  = x;
              theJob->axiom[AxW]   = theJob->axiom[AxWB]  = x;
              theJob->axiom[AxC2]  = theJob->axiom[AxC]   = x;
              theJob->axiom[AxTF]  = theJob->axiom[AxX]   = x;  break;
     case CK: theJob->axiom[AxK]   = theJob->axiom[AxC3]  = x;
              theJob->axiom[AxK2]  = theJob->axiom[AxCt]  = x;
              theJob->axiom[AxC2]  = theJob->axiom[AxC]   = x;
              theJob->axiom[AxTF]  = theJob->axiom[AxM]   = x;  break;
     case S4: theJob->axiom[AxK2]  = theJob->axiom[AxRED] = x;
              theJob->axiom[AxW2]  = theJob->axiom[AxW]   = x;
              theJob->axiom[AxBA]  = theJob->axiom[AxSBA]   = x;
              theJob->axiom[AxC3]  = theJob->axiom[AxX]   = x;
              theJob->axiom[AxTF]  = theJob->axiom[AxM]   = x;
                                     theJob->axiom[AxWB]  = x;
  }
  if ( !theJob->f_n )
  {
     theJob->axiom[AxX]   = theJob->axiom[AxBA]  = 0;
     theJob->axiom[AxSBA] = theJob->axiom[AxRED] = 0;
  }
  if ( !theJob->f_t )
  {
     theJob->axiom[AxK]  = theJob->axiom[AxK2]  = 0;
     theJob->axiom[AxCt] = 0;
  }
  if ( !theJob->f_lat )
  {
     theJob->axiom[AxX]   = theJob->axiom[AxBA] = 0;
     theJob->axiom[AxSBA] = theJob->axiom[AxW2] = 0;
     theJob->axiom[AxWB]  = theJob->axiom[Axat] = 0;
  }
  if ( !theJob->f_T || !theJob->f_F ) theJob->axiom[AxTF] = 0;
}

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

efficient_logic_set()              /*** Remove some redundant axioms ***/
{
   switch(theJob->logic)
   {
      case R:  theJob->axiom[AxW] = 0;
      case RW: 
      case CK: theJob->axiom[AxB2] = 0;
      case S4: 
      case E:  theJob->axiom[AxWB] = theJob->axiom[AxB] = 0;
   }
}