/* Program to take a list of test vectors of nonnegative integers
   (specifying the entropies of all nonempty combinations of
   a given number of random variables), and try to determine
   whether the vectors are linearly realizable (over the reals, or over all
   sufficiently large finite fields); the output of the
   program is the list of vectors for which it could _not_ make
   this determination (plus further information about successful
   realizations if preprocessor variable VERBOSE is set)
   [Note: the program may not work correctly if given input vectors
      that do not satisfy the Shannon inequalities] */

#include <stdio.h>
#include <stdlib.h>
#include <string.h>

/* The number of random variables to work with */
#define NVAR 6
/* The factorial of NVAR (verified later) */
#define NVARFACT 720
/* Two to the power NVAR */
#define TWOTONVAR (1 << NVAR)

/* The permutations on TWOTONVAR combined variables induced by
   the NVARFACT permutations of NVAR original random variables */
int permarray[NVARFACT][TWOTONVAR];

/* A list of linear rank inequalities to be assumed as known
   (including the trivial zero inequality as a terminator) */
int knownineqs[][TWOTONVAR] = {
   {0,0,0,0,0,0,0,0, 0,0,0,0,0,0,0,0,
      0,0,0,0,0,0,0,0, 0,0,0,0,0,0,0,0,
      0,0,0,0,0,0,0,0, 0,0,0,0,0,0,0,0,
      0,0,0,0,0,0,0,0, 0,0,0,0,0,0,0,0}};
/* The number of known inequalities (including the trivial one */
#define NKI (sizeof(knownineqs)/(TWOTONVAR*sizeof(int)))

#define MAXPROOF 10000



int main(int argc, char **argv)
{
   int i,j,k,m,n,jj,ii;
   int v[TWOTONVAR];
      /* The current input vector to be tested for linear realizability */
   int mark[TWOTONVAR];
      /* For a particular value of k (a power of 2), the value of
         mark[i] for i <= k is initially pv[i] (pv is a permuted
         version of v) but is gradually decreased as vectors are
         selected and "used up" (actually modded out by) */
   int scr[TWOTONVAR];
      /* For k as above, the value of scr[i] is initially
         pv[i+k]-pv[i] (i.e., the amount that the new random
         variable should augment the dimension of subspace i)
         but is gradually decreased as vectors are allocated
         to the new random variable */
   int scr2[TWOTONVAR];
      /* Initially a saved copy of the mark[] array, but then
         is used as an array of pairs of bits.  If we are
         trying to adjoin an additional vector to the new
         random variable, scr2[i]&1 is set when it is determined
         that the additional vector must be in subspace i, and
         scr2[i]&2 is set when it is determined that the additional
         vector must not be in subspace i. */
   char buffer[20000];
      /* An input buffer for the test vectors */
   int perm[NVAR];
      /* The current permutation of the original random variables
         (represented as bit masks -- (1<<j) for variable number j);
         used only when generating permarray */
   int inner,outer;
      /* The program sets inner to 1 when it verifies that the current
         test vector is linearly realizable, and it sets outer to 1
         when it verifies that the test vector is linearly unrealizable */
   int prooflen;
      /* The length of the sequence of integers constituting a proof
         of the realizability of the vector */
   int savedprooflen;
      /* A previous value of prooflen that one can go back to */
   int proof[MAXPROOF];
      /* The sequence of integers constituting the proof */
   int lastgoodvar;
      /* Any variables other than the first lastgoodvar variables are
         marked as auxiliary variables when a proof is printed */
#if defined(ALTERNATIVE1)
   int jx,jjx;
      /* In the loop where k is its largest value, instead of picking
         one value j or pair (j,jj) to try, on the first step loop
         through all plausible pairs (j,jj), where "plausible" means
         scr[j],scr[jj] < scr[0] and each of j,jj is minimal
         under "bitwise <=" with this property */
   int changej = 0;
      /* only alter j and jj if this flag is set */
#endif

   lastgoodvar = 30;
   if (argc > 1) lastgoodvar = atoi(argv[1]);

   /* Verify that NVARFACT is set correctly */
   i = 1;
   for (j = 1; j <= NVAR; j++) i *= j;
   if (i != NVARFACT) {
      printf("Bad NVARFACT\n");
      exit(1);
   }

   /* Generate the array of permutations of combined random variables */
   for (m = 0; m < NVARFACT; m++) {
      for (j = 0; j < NVAR; j++) perm[j] = (1<<j);
      k = m;
      for (j = 2; j <= NVAR; j++) {
         i = perm[j-1];
         perm[j-1] = perm[j-1-(k%j)];
         perm[j-1-(k%j)] = i;
         k /= j;
      }
      for (i = 0; i < TWOTONVAR; i++) {
         j = 0;
         for (k = 0; k < NVAR; k++) {
            if (i&(1<<k)) j |= perm[k];
         }
         permarray[m][i] = j;
      }
   }

#if PRINTINEQS
   /* Print out all permutations of the known inequalities */
   for (j = 0; j < NKI-1; j++) {
      for (m = 0; m < NVARFACT; m++) {
         for (i = 0; i < TWOTONVAR; i++) {
            printf(" %d",knownineqs[j][permarray[m][i]]);
         }
         printf("\n");
      }
   }
   exit(0);
#endif

   /* Main loop on test vectors */
   for ( ; ; ) {
      /* Read in the next vector */
      if (fgets(buffer,sizeof(buffer),stdin) == NULL) break;
      k = 0;
      for (j = 0; j < TWOTONVAR; j++) {
         i = sscanf(buffer+k," %d%n",v+j,&m);
         if (i == 0) break;
         k += m;
      }
      v[0] = 0;
      if (i == 0) break;
      inner = outer = 0;

#if 0
      /* Skip vectors that are redundant in that the same
         combined random variable has two disjoint names */
      for (i = 1; i < TWOTONVAR; i <<= 1) {
         for (j = 0; j < TWOTONVAR; j++) {
            if (i&j) continue;
            if ((v[i] == v[j]) && (v[i] == v[i|j])) goto skip;
         }
      }
#endif

      /* Check whether the test vector violates any of the
         known inequalities */
      for (i = 0; i < NKI; i++) {
         for (m = 0; m < NVARFACT; m++) {
            k = 0;
            for (j = 0; j < TWOTONVAR; j++)
               k += v[permarray[m][j]]*knownineqs[i][j];
            if (k < 0) outer = 1;
         }
      }

      /* Loop on possible orderings of the given random variables,
         trying to construct a linear realization */
      n = 0;
      for (m = 0; m < NVARFACT; m++) {
         // if (permarray[m][TWOTONVAR>>1] & n) continue;
         prooflen = 0;
#if defined(VERBOSE)
         printf("Start\n");
#endif
         for (k = 1; k < TWOTONVAR; k <<= 1) {
            savedprooflen = prooflen;
#if defined(VERBOSE)
            if (permarray[m][k] <= 32) printf("  %c:\n",
               "xABxCxxxDxxxxxxxExxxxxxxxxxxxxxxF"[permarray[m][k]]);
#endif
#if defined(ALTERNATIVE1)
            j = -1;
            for (jx = (k == TWOTONVAR/2)?1:(k-1); jx < k; jx++) {
            if (k == TWOTONVAR/2) {
               if (v[permarray[m][k+jx]] - v[permarray[m][jx]] ==
                     v[permarray[m][k]] - v[permarray[m][0]])
                  continue;
               for (i = 1; i <= jx; i <<= 1) {
                  if ((jx & i) == i &&
                        v[permarray[m][k+(jx^i)]] - v[permarray[m][jx^i]] <
                        v[permarray[m][k]] - v[permarray[m][0]])
                     break;
               }
               if (i <= jx) continue;
            }
            for (jjx = (k == TWOTONVAR/2)?jx+1:(k-1); jjx < k; jjx++) {
            if (k == TWOTONVAR/2) {
               if (v[permarray[m][k+jjx]] - v[permarray[m][jjx]] ==
                     v[permarray[m][k]] - v[permarray[m][0]])
                  continue;
               for (i = 1; i <= jjx; i <<= 1) {
                  if ((jjx & i) == i &&
                        v[permarray[m][k+(jjx^i)]] - v[permarray[m][jjx^i]] <
                        v[permarray[m][k]] - v[permarray[m][0]])
                     break;
               }
               if (i <= jjx) continue;
#if defined(VERBOSE)
               printf(" substart\n");
#endif
               changej = 1;
               prooflen = savedprooflen;
            }
#endif
            /* Set up the mark[] and scr[] arrays to respectively
               the sizes of the subspaces from the previous random
               variables and the amount that these should be
               augmented when the new random variable is adjoined */
            for (i = 0; i < k; i++) {
               mark[i] = v[permarray[m][i]];
               scr[i] = v[permarray[m][k+i]] - mark[i];
            }
            if (prooflen + 1 + scr[0] > MAXPROOF) {
               printf("ERROR: proof too long\n");
               exit(1);
            }
            for ( ; ; ) {
#if defined(VERBOSE)
               // for (i = 0; i < k; i++) printf("%d ",mark[i]);
               // printf("\n");
               // for (i = 0; i < k; i++) printf("%d ",scr[i]);
               // printf("\n");
#endif
               /* Select a value of j such that we will try to adjoin
                  a generic vector from subspace j to the new
                  random variable (checking to see that certain
                  contradictions have not yet been reached) */
               j = k;
               jj = mark[k-1] + scr[0] + 1;
               for (i = 1; i < k; i++) {
                  if ((scr[i] > scr[0]) || (scr[i] < 0)) {
                     j = -1;
                     break;
                  }
                  if ((scr[i] < scr[0]) && (mark[i]+scr[i] < jj)) {
                     j = i;
                     jj = mark[j];
                  }
               }
#if defined(VERBOSE)
               // printf(" %d\n",j);
#endif
               if ((j == -1) || (j == k)) break;
#if defined(ALTERNATIVE1)
               if (changej) j = jx;
#endif
               if (mark[j] <= 0) break;
               proof[prooflen++] = j;
#if defined(VERBOSE)
               printf("     %d",j);
#endif
               jj = k;
               /* Update the mark[] and scr[] arrays to reflect removal
                  of (actually modding out by) the generic vector; if
                  it looks as though there is a problem, select a second
                  subspace jj to work with; save the old mark[] array
                  in scr2[] */
               for (i = 0; i < k; i++) {
                  scr2[i] = mark[i];
                  if (mark[i|j] > mark[i]) {
                     scr[i]--;
                     if (scr[i] < scr[i|j]) {
                        if (jj == k || mark[i] < mark[jj]) jj = i;
                     }
                  } else mark[i]--;
               }
#if defined(ALTERNATIVE1)
               if (changej) jj = jjx, changej = 0;
#endif
               if (jj < k) {
                  proof[prooflen-1] += jj*k;
#if defined(VERBOSE)
                  printf("   %d",jj);
#endif
                  /* Forget the generic vector from subspace j, and
                     restore the preceding mark[] and scr[] arrays */
                  for (i = 0; i < k; i++) {
                     if (scr2[i|j] > scr2[i]) scr[i]++;
                     else mark[i]++;
                  }
                  /* Try to adjoin a generic vector from the intersection
                     of subspace j and subspace jj; see whether it is
                     possible to determine whether this vector is or
                     is not in each of the other subspaces (i.e., whether
                     subspace i includes the intersection of subspaces
                     j and jj) */
                  for (i = 0; i < k; i++) {
                     /* Note: if we write <i> for subspace i, so that
                        mark[i] is dim(<i>), then
                              mark[i|i'] - mark[i]
                                 = dim(<i|i'>) - dim(<i>)
                                 = dim(<i'>) - dim(<i> intersect <i'>)
                        so to check whether
                           dim(<i>intersect<i'>) <,=,> dim(<i>intersect<i''>),
                        it suffices to check whether
                           mark[i|i']-mark[i'] >,=,< mark[i|i'']-mark[i'']. */
                     scr2[i] = 0;
                     /* Don't bother adding the null vector */
                     if (i == 0) scr2[i] |= 2;
                     /* The generic vector is in subspace i if subspace i
                        includes subspace j */
                     if (mark[i|j] == mark[i]) scr2[i] |= 1;
                     /* It's in if subspace i includes subspace jj */
                     if (mark[i|jj] == mark[i]) scr2[i] |= 1;
                     /* It's in if
                            dim(<i> intersect <j>)
                               = dim(<i> intersect <jj>)
                               = dim(<i> intersect <j|jj>)
                               = dim(<j> intersect <jj>)
                        because the first two equalities give
                           <i> intersect <j>
                              = <i> intersect <j|jj>
                              = <i> intersect <jj>
                              = <i> intersect (<j> intersect <jj>) */
                     if ((mark[j]-mark[i|j] == mark[jj]-mark[i|jj]) &&
                        (mark[j]-mark[i|j] == mark[j|jj]-mark[i|j|jj]) &&
                        (mark[i]-mark[i|j] == mark[jj]-mark[j|jj]))
                        scr2[i] |= 1;
                     /* It's in if
                            dim(<j> intersect <jj>)
                               = dim(<j> intersect <jj|i>)
                               = dim(<j> intersect <i>)
                        because these give
                           <j> intersect <jj>
                              = <j> intersect <jj|i>
                              = <j> intersect <i>
                              = <j> intersect (<jj> intersect <i>).
                        Similarly with j and jj interchanged. */
                     if ((mark[jj]-mark[j|jj] == mark[i]-mark[j|i]) &&
                        (mark[jj]-mark[j|jj] == mark[i|jj]-mark[j|i|jj]))
                        scr2[i] |= 1;
                     if ((mark[j]-mark[j|jj] == mark[i]-mark[jj|i]) &&
                        (mark[j]-mark[j|jj] == mark[i|j]-mark[j|i|jj]))
                        scr2[i] |= 1;
                     /* It's out if dim(<i> intersect <j>) <
                        dim(<jj> intersect <j>) */
                     if (mark[i|j]-mark[i] > mark[jj|j]-mark[jj])
                        scr2[i] |= 2;
                     /* It's out if dim(<i> intersect <j>) <
                        dim(<jj> intersect <j>) */
                     if (mark[i|jj]-mark[i] > mark[j|jj]-mark[j])
                        scr2[i] |= 2;
                     /* It's out if subspace i does not include
                        subspace j&jj */
                     if (mark[i|(j&jj)] > mark[i]) scr2[i] |= 2;
                     /* Note that if we have spaces U,V,W with
                        V included in U, then
                           U intersect VW = (U intersect W)V.
                        [Right-to-left inclusion is easy.  For
                        left-to-right, if u = v+w, then v is in V
                        and w = u-v is in U intersect W.]
                        So if <i> includes <j>intersect<jj>, then we
                        can't have
                           dim(<i>intersect<j>) <
                              dim(<j> intersect <(i&j)|jj>)
                        because
                           <j> intersect <(i&j)|jj>
                              = (<j> intersect <jj>)<i&j>
                        and the latter is included in <i>intersect<j>. */
                     if (mark[i|j]+mark[(i&j)|jj] > mark[j|jj]+mark[i])
                        scr2[i] |= 2;
                     /* Same with j and jj interchanged */
                     if (mark[i|jj]+mark[(i&jj)|j] > mark[j|jj]+mark[i])
                        scr2[i] |= 2;
                     /* If dim(<i>intersect<j>)=dim(<j>intersect<jj>)
                        and we have an inclusion between these two
                        subspaces, then we get
                           <i>intersect<j>=<j>intersect<jj>
                        and hence <i> includes <j>intersect<jj>.  */
                     if (mark[i|j]-mark[i] == mark[j|jj]-mark[jj]) {
                        /* Inclusion holds if <j> is included in <jj>
                           (because <j>intersect<jj> is just <j>) */
                        if (mark[j|jj] == mark[jj]) scr2[i] |= 1;
                        /* Inclusion holds if <i> is included in <jj> */
                        if (mark[i|jj] == mark[jj]) scr2[i] |= 1;
                     }
                     /* Same with j and jj interchanged */
                     if (mark[i|jj]-mark[i] == mark[j|jj]-mark[j]) {
                        if (mark[j|jj] == mark[j]) scr2[i] |= 1;
                        if (mark[j|i] == mark[j]) scr2[i] |= 1;
                     }
                     /* If <(j&~jj)|(jj&~j)> (i.e., <j^jj>) is independent
                        of <j&jj>, then we have
                           <j>intersect<jj> = (<j&~jj>intersect<jj&~j>)<j&jj>.
                        [The right-to-left inclusion is easy.  For the
                        left-to-right inclusion, if x is in
                        <j> = <(j&~jj)|(j&jj)> and in <jj> = <(jj&~j)|(j&jj)>,
                        then x = y1 + z1 = y2 + z2 with y1 in <j&~jj>,
                        y2 in <jj&~j>, and z1,z2 in <j&jj>.  By the
                        independence assumption, we must have y1=y2 and z1=z2,
                        and y1=y2 is in <j&~jj>intersect<jj&~j>,
                        so we are done.]
                        So, in this case, if we also have <j&jj> included
                        in <i>, then to get <j>intersect<jj> included in <i>
                        it suffices to have <j&~jj>intersect<jj&~j> included
                        in <i>.  */
                     if ((mark[j|jj] == mark[j&jj]+mark[j^jj]) &&
                           (mark[(j&jj)|i] == mark[i])) {
                        /* The next three are just copies of previous tests
                           with  j  and  jj  changed to  j&~jj  and  jj&~j  */
                        if (mark[(j&~jj)|i] == mark[i]) scr2[i] |= 1;
                        if (mark[(jj&~j)|i] == mark[i]) scr2[i] |= 1;
                        if ((mark[j&~jj]-mark[i|(j&~jj)] ==
                              mark[jj&~j]-mark[i|(jj&~j)]) &&
                           (mark[j&~jj]-mark[i|(j&~jj)] ==
                              mark[j^jj]-mark[i|(j^jj)]) &&
                           (mark[i]-mark[i|(j&~jj)] ==
                              mark[jj&~j]-mark[j^jj]))
                           scr2[i] |= 1;
                        /* Now repeat the previous test with  i  changed to
                           i&~(j&jj)  */
                        if ((mark[j&~jj]-mark[(i&~(j&jj))|(j&~jj)] ==
                              mark[jj&~j]-mark[(i&~(j&jj))|(jj&~j)]) &&
                           (mark[j&~jj]-mark[(i&~(j&jj))|(j&~jj)] ==
                              mark[j^jj]-mark[(i&~(j&jj))|(j^jj)]) &&
                           (mark[(i&~(j&jj))]-mark[(i&~(j&jj))|(j&~jj)] ==
                              mark[jj&~j]-mark[j^jj]))
                           scr2[i] |= 1;
                     }
                     /* Apply monotonicity conditions: if the generic vector
                        is not in subspace i and subspace ii is included in
                        subspace ii, then the generic vector is not in
                        subspace ii */
                     for (ii = 1; ii < i; ii++) {
                        if ((i & ii) == ii) {
                           scr2[i] |= scr2[ii]&1;
                           scr2[ii] |= scr2[i]&2;
                        }
                     }
                  }
                  /* Check whether the determination succeeded */
                  for (i = 0; i < k; i++) {
                     if ((scr2[i] == 0) || (scr2[i] == 3)) {
#if defined(VERBOSE)
                        printf("\n");
#endif
                        break;
                     }
                  }
                  if (i < k) {
#if defined(VERBOSE)
                     //for (i = 0; i < k; i++) printf("%d ",mark[i]);
                     //printf("\n");
                     //for (i = 0; i < k; i++) printf("%d ",scr[i]);
                     //printf("\n");
                     //for (i = 0; i < k; i++) printf("%d ",scr2[i]);
                     //printf("\n");
                     //printf(" %d %d\n",j,jj);
                     printf("\n");
#endif
                     break;
                  }
                  /* Determination succeeded -- update mark[] and scr[] */
                  for (i = 0; i < k; i++) {
                     if (scr2[i] == 1) mark[i]--;
                     else scr[i]--;
                  }
               }
#if defined(VERBOSE)
               printf("\n");
#endif
            }
#if defined(ALTERNATIVE1)
            if (j == k) break;
            }
            if (j == k) break;
            }
#endif
            if (j != k) break;
            for (i = 0; i < scr[0]; i++) proof[prooflen++] = 0;
            if (permarray[m][k] < (1 << lastgoodvar)) proof[prooflen++] = -1;
            else proof[prooflen++] = -2;
#if defined(VERBOSE)
            /* See how many entirely new vectors are in the new random
               variable */
            if (scr[0]) {
               printf("     and %d new\n",scr[0]);
            }
#endif
         }
         if (k == TWOTONVAR) {
#if defined(VERBOSE)
            printf("--------------SUCCESS---------------\n");
#endif
            inner = 1;
            break;
         } else if (k == (TWOTONVAR>>1)) {
            n |= permarray[m][TWOTONVAR>>1];
         }
      }

      /* Try a second test for realizability (which really shouldn't
         give anything not given by the first test) -- ADD HERE */
      for (i = 0; i < TWOTONVAR; i++) mark[i] = (v[i]>0);
      for (i = 1; i < TWOTONVAR; i <<= 1) mark[i] = 0;
      for (i = 1; i < TWOTONVAR; i++) {
         for (j = i+1; j < TWOTONVAR; j++) {
            if (((j&i)==i) && (v[i]==v[j])) mark[i] = 0;
            k = (i|j);
            if ((v[k]>v[i]) && (v[k]>v[j]) && (v[k]==v[i]+v[j]-v[i&j]))
               mark[k] = 0;
         }
      }

#if 0
/* This doesn't work!! */
      for (i = 0; i < NVAR; i++) scr[i] = v[1<<i];
      for (i = 0; i < NVAR; i++) {
         for (j = i+1; j < NVAR; j++) {
            m = v[1<<i] + v[1<<j] - v[(1<<i)|(1<<j)];
            if ((m <= scr[i]) && (m <= scr[j]) && (mark[(1<<i)|(1<<j)])) {
               scr[i] -= m;
               scr[j] -= m;
               mark[(1<<i)|(1<<j)] = 2;
            }
         }
      }
#endif

      for (i = 1; i < TWOTONVAR; i++) {
         if (mark[i] != 1) continue;
         for (j = i+1; j < TWOTONVAR; j++) {
            if (((j&i) != i) && (mark[j] == 1)) break;
         }
         if (j < TWOTONVAR) break;
      }
      if (i == TWOTONVAR) {
         if (inner == 0) printf("WEIRD\n"),fprintf(stderr,"WEIRD\n");
         inner = 1;
      }

#if defined(REVERSE)
      /* Check the results for this vector -- print an error message
         if there is a contradiction, and print the vector if it
         is linearly realizable */
#else
      /* Check the results for this vector -- print an error message
         if there is a contradiction, and print the vector if it
         is still undetermined */
#endif
      if (inner && outer) {
         printf("ERROR\n");
         fprintf(stderr,"ERROR\n");
         exit(1);
      }
#if defined(REVERSE) || defined(SHOWPROOF)
      if (inner) {
#else
      if (!inner && !outer) {
#endif
#if defined(SHOWPROOF)
         for (i = 0; i < prooflen; i++) printf(" %d",proof[i]);
#else
         for (k = 0; k < TWOTONVAR; k++) {
            /* if (k > 1) */ printf(" ");
            printf("%d",v[k] /*," *x"[mark[k]]*/ );
         }
#endif
         printf("\n");
      }
skip: ;
   }
}