/* ************************ mk_book.c *********************************
  This program creates the files book1 and book2 from rfb1.  It first
  reads through rfb1.tex to find the largest form number n.  Then two
  arrays are created:  A char array im for book1 and an integer array
  **r1 for book2.  Then the file rfb1.tex is reread and the entries
  are transfered to im.  The next step is to close the array im under
  implication and add numbers for any non-implications that follow
  from known implications and known non-implications.  (We actually
  use the main body of the program closure.c.)  In addition (as in
  closure.c) the appropriate entries are made in r1.  Finally, im is
  written to the file book1 and r1 to the file book2.
  3/9/95 (First Version)
  3/17/95 revised so that it only places the odd implication codes
  from rfb1.tex into the array im.  (book2 wasn't being calculated
  properly.)
********************************************************************** */
#include <stdio.h>
#include <stdlib.h>
#include <string.h>
main()
{   /* Declarations */
    char  **im, code;                    /* char array for book1 */
    char s[100],c0[2],noalign[8], path1[20], path2[20], outpath[15],junk[8];
    char yes[2], v, path3[20], tl[100], path4[20], path5[20], path6[20];
    char reason2[100], reason[100], imp, srow[10], scol[10];
    int last, r, rpp, lr, rflag, response, rowf, rowl, colf, coll;
    int **r1, ro, co, form, temp, row, col,i, counter;
    int fi, fip, prow,nl, pcol,lrb,lcb,page, so, response2;
    int firstrow, lastrow, firstcol,lastcol, count;
    int k, n, rr, cc, e, c, d, *implyr, *cimply, j, dev, max;
    FILE *ifp, *ofp, *rfp, *entfp, *nrfp, *sumfp;
  /* End Declarations */


     /* Get the names of the implication array and supporting array and
     files from which data is to be read and written */
    printf("\n%s\n\%s\n%s\n%s\n",
	    "This program creates the data files book1 and book2 which",
	    "are used by other programs in the weak AC project.  The file",
	    "rfb1.tex must be present and if the files book1 and book2",
	    "are present they will be overwritten.");

L0: printf("\n\n%s\n",
	   "Do you want to continue? (y/n)");
    gets(junk);
    if(strcmp(junk,"y")== 0 || strcmp(junk,"Y")==0)
      goto N1;
    exit(1);
N1: strcpy(path1,"book1");
    strcpy(path2,"book2");
    strcpy(path3,"rfb1.tex");
    if((rfp=fopen(path3,"r"))==NULL)
      {printf("\n%s%s\n","Can't open ", path3);
       goto L0;
      }
/* Get largest form number from rfb1.tex */
   max = 0;

   while(!feof(rfp))
     {fgets(tl,100,rfp);
      k=0;
      while(tl[k]  == ' ')
	++k;
      if(tl[k] == '\\' && tl[k+1] == '+'
		  && tl[k+2] != '&')
	{while(!isdigit(tl[k]))             /* read up to row no. */
	   ++k;
	 j = 0;
	 while(isdigit(tl[k]))        /* put row no. in srow (as a string)*/
	  {srow[j] = tl[k];
	   ++j;
	   ++k;
	  }
	 srow[j] = NULL;
	 row = atoi(srow);      /* store row number in row as an integer */
	 while(!isdigit(tl[k]))  /* read up to the column number */
	   ++k;
	 j  = 0;
	 while(isdigit(tl[k]))        /* repeat for column no. */
	   {scol[j] = tl[k];
	    ++j;
	    ++k;
	   }
	 scol[j]  = NULL;
	 col = atoi(scol);
	 if(max < row) max = row;
	 if(max < col) max = col;
	}
    }  /* while not eof rfp */
    printf("\n%s%s%s%d\n",
	    "The largest form number in ",path3," is ",max);
    rewind(rfp);

    nl = max;
	   /* dimension the arrays implyr and cimply */
       if((implyr = calloc(nl + 1,sizeof(int)))==NULL)
	 {printf("\n%s\n","out of memory");
	  goto L0;
	 }
       if((cimply = calloc(nl + 1, sizeof(int)))==NULL)
	{printf("\n%s\n","out of memory");
	 goto L0;
	}

 /* Dimension the arrays im and r1 */
    im =calloc(nl+1,sizeof(char*));
    for(ro=0;ro<=nl;++ro)
     if((im[ro]=calloc(nl+1,sizeof(char)))==NULL)
	{printf("\n%s%d\n","out of memory at row ",ro);
	 goto L0;
	}

    r1 =calloc(nl+1,sizeof(int*));
    for(ro=0;ro<=nl;++ro)
     if((r1[ro]=calloc(nl+1,sizeof(int)))==NULL)
	{printf("\n%s%d\n","out of memory at row ",ro);
	 goto L0;
	}
	last = nl;

 /* initialize the arrays im and r1 */
    for(ro=0;ro<= nl;++ro)
    for(co=0;co<= nl;++co)
      {im[ro][co] = '0';
       r1[ro][co] = 0;
      }

 /* Reread rfb1.tex and put the implication numbers in rfb1.tex */
   while(!feof(rfp))
     {fgets(tl,100,rfp);
      k=0;
      while(tl[k]  == ' ')
	++k;
      if(tl[k] == '\\' && tl[k+1] == '+'
		  && tl[k+2] != '&')
	{while(!isdigit(tl[k]))             /* read up to row no. */
	   ++k;
	 j = 0;
	 while(isdigit(tl[k]))        /* put row no. in srow (as a string)*/
	  {srow[j] = tl[k];
	   ++j;
	   ++k;
	  }
	 srow[j] = NULL;
	 row = atoi(srow);     /* store row number in row as an integer */
	 while(!isdigit(tl[k]))
	   ++k;
	 j  = 0;
	 while(isdigit(tl[k]))        /* repeat for column no. */
	   {scol[j] = tl[k];
	    ++j;
	    ++k;
	   }
	 scol[j]  = NULL;
	 col = atoi(scol);

       while(!isdigit(tl[k]))        /* read up to the implication code */
	   ++k;
	 j  = 0;
	 code = tl[k];          /* get implication code for the line */
	 if(im[row][col] != '0' && im[row][col] != code)
	    printf("\n%s\n%s%d%s%d\n",
		   "There are two rows in rfb1",
		   "   for ",row,", ",col);

	  if(code=='1' || code=='3' || code=='5' || code=='7')
	    im[row][col] = code;
	}
    }  /* while not eof rfp */

     fclose(rfp);

     printf("\n%s\n%s\n","Calculating book1 and book2",
	     "This will take a while");

	   /* Begin the closure operation */

/* Begin update */
	 /* Put 1's in positions where implications always hold */
   for(row=0;row<=last;++row)
     {im[row][0]='1';
      im[1][row]='1';
      im[row][row] = '1';
     }
   for(row=0;row<=last;++row)
   for(col=0;col<=last;++col)
    {
     k = 0;
     n = 0;
     if( im[row][col] == '1')                /*for implications */
       {r1[row][col]=0;                       /* clear supporting array entry*/
        for(r = 0;r<=last;++r)
         {if((im[r][row] == '1')||(im[r][row]== '2'))
           {k = k + 1;
            implyr[k] = r;
           }
         }
       for(c = 0;c<= last; ++c)
         {if((im[col][c]== '1') || (im[col][c]== '2'))
           {n = n + 1;
            cimply[n] = c;
           }
	 }
       for(i=1;i<=k;++i)
         {ro = implyr[i];
          v=im[ro][col];
          if(v=='0' || v=='7')
            {im[ro][col]='2';
             r1[ro][col]= row;
            }
          if('2'< v && v <'7')
            {printf("\n%s%4d%s%4d%s%4d%s%4d\n%s%4d%s%4d",
                      "Problem:  ",ro," does not imply ",col," but ",ro,
                      " implies ",row, " and ", row," implies ",col);
             exit(1);
            }
         }

       for(i = 1;i<=k;++i)
       for(j = 1;j<=n;++j)
         {ro = implyr[i];
          co = cimply[j];
	  v = im[ro][co];
          if((v== '0') || (v == '7'))
            {im[ro][co] = '2';
             r1[ro][co] = col;
            }
         if(('2' < v) && (v < '7'))
           {printf("\n%s%4d%s%4d%s%4d%s%4d\n%s%4d%s%4d",
                      "Problem:  ",ro," does not imply ",co," but ",ro,
                      " implies ",col, " and ", col," implies ",co);
            exit(1);
           }
         /* update non implications */
         for(e = 0;e<=last;++e)
           {if((im[ro][e] == '3') || (im[ro][e] == '4'))
             {v = im[co][e];
              if((v== '0') || (('4' < v) && (v < '8')))
                {im[co][e] = '4';
                 r1[co][e] = ro;
                }
              if( (v == '1') || (v == '2'))
		{printf("\n%s%4d%s%4d%s%4d%s%4d\n%s%4d%s%4d",
                      "Problem:  ",ro," does not imply ",e," but ",ro,
                      " implies ",co, " and ", co," implies ",e);
                 exit(1);
                }
             }
            if((im[ro][e] == '5') || (im[ro][e] == '6'))
              {if((im[co][e] == '0') || (im[co][e] == '7'))
                 {im[co][e] = '6';
                  r1[co][e] = ro;
                 }
               if((im[co][e] == '1') || (im[co][e] == '2'))
                 {printf("\n%s%4d%s%4d%s%4d%s%4d\n%s%4d%s%4d",
                      "Problem:  ",ro," does not imply ",e," but ",ro,
                      " implies ",co, " and ", co," implies ",e);
                  exit(1);
                 }
               }

            if((im[e][co] == '3') || (im[e][co] == '4'))
	      {v = im[e][ro];
                if((v == '0') || (('4' < v) && (v < '8')))
                  {im[e][ro] = '4';
                   r1[e][ro] = co;
                  }
                if((v == '1') || (v == '2'))
                  {printf("\n%s%4d%s%4d%s%4d%s%4d\n%s%4d%s%4d",
                      "Problem:  ",e," does not imply ",co," but ",e,
                      " implies ",ro, " and ", ro," implies ",co);
                   exit(1);
                  }
              }

            if((im[e][co] == '5') || (im[e][co] == '6'))
              {if((im[e][ro] == '0') || (im[e][ro] == '7'))
                 {im[e][ro] = '6';
                  r1[e][ro] = co;
                 }
               if((im[e][ro] == '1') || (im[e][ro] == '2'))
                 {printf("\n%s%4d%s%4d%s%4d%s%4d\n%s%4d%s%4d",
		      "Problem:  ",e," does not imply ",co," but ",e,
                      " implies ",ro, " and ", ro," implies ",co);
                  exit(1);
                 }
              }
           }
         }
       }

/* now if row does not imply column */
     
     if((im[row][col] == '3') || (im[row][col] == '5'))
       {r1[row][col] = 0;   /* clear supporting array entry */
        k = 0;
        n = 0;
        for(c = 0;c<=last;++c)
          {if((im[row][c] == '1') || (im[row][c] == '2'))
             {k = k + 1;
              implyr[k] = c;
             }
	   }
        for(d = 0;d<=last;++d)
          {if((im[d][col] == '1') || (im[d][col] == '2'))
             {n = n + 1;
              cimply[n] = d;
             }
          }
   /* now update */
        for(i=1;i<=k;++i)
          {ro = implyr[i];
           v=im[ro][col];
           if(v=='1' || v=='2')
             {printf("\n%s%4d%s%4d%s%4d%s%4d\n%s%4d%s%4d",
                      "Problem:  ",row," does not imply ",col," but ",ro,
                      " implies ",col, " and ", row," implies ",ro);
              exit(1);
             }
           if(v == '0' || (v =='6' || v== '7'))
             {im[ro][col] = im[row][col] + 1;   /* this needs testing */
              r1[ro][col] = row;
	     }
           if( v =='5' && im[row][col] == '3')
             {im[ro][col] = '4';
              r1[ro][col] = row;
             }
          }

        for(i = 1;i<=k;++i)
        for(j = 1 ;j<=n;++j)
          {ro = implyr[i];
           co = cimply[j];
           v = im[ro][co];
           if((v == '1') || (v == '2'))
             {printf("\n%s%4d%s%4d%s%4d%s%4d\n%s%4d%s%4d%s%4d%s%4d",
                      "Problem:  ",row," does not imply ",col," but ",row,
                      " implies ",ro, " and ", ro," implies ",co,
                       " and ",co," implies ",col);
              exit(1);
             }

	   if(((v == '0') || ((v == '6') || (v == '7')))&& co != col)
	     {im[ro][co] = im[row][col] + 1;
              r1[ro][co] = col;
             }
           if((v == '5') && (im[row][col] == '3'))
             {im[ro][co] = '4';
              r1[ro][co] = col;
             }
          }
       }
     }
    printf("\n%s%s\n","Caluclation complete - ",
	      "now writing to book1 and book2");
L6: ofp = fopen(path1,"w");
    for(row=0;row<=last;++row)
     {count = 0;
      for(col=0;col<=last;++col)
	 {fprintf(ofp,"   %c",im[row][col]);
	  count = count + 1;
	  if(count==100)
	    {fprintf(ofp,"\n");
	      count = 0;
	    }
	 }
	  fprintf(ofp,"%4d\n",-1);
     }
    fclose(ofp);
    ofp=fopen(path2,"w");
    for(row=0;row<=last;++row)
     {count = 0;
      for(col=0;col<=last;++col)
	 {fprintf(ofp,"%4d",r1[row][col]);
	  count = count + 1;
	  if(count==100)
	    {fprintf(ofp,"\n");
	      count = 0;
	    }
	 }
	  fprintf(ofp,"%4d\n",-1);
      }
    fclose(ofp);
    printf("\n%s\n","Done");
   exit(1);
}