/*
 * Solver for Mines (sub)games.
 *
 * Input takes the form of something like
 *
 *	3
 *	* * 2 3 * 4 * * *
 *	* 4 ? ? 2 ? ? ? 2
 *	1 2 ? ? ? ? ? ? *
 *
 * The first number, on a line by itself, is the number of mines to be
 *  filled in.  This may be a ? if it is not known.
 *
 * The rest is a grid, which must be at least 3x3, of symbols: * for a
 *  marked-as-mine square, ? for an unknown square, or a digit giving
 *  the number of mines adjacent to the square.  Counts do not have to
 *  be accurate unless they are adjacent to a ?.
 *
 * Whitespace is ignored, except for newlines, whihc delimit lines.
 *  For exmaple, the above input could also, though more confusingly,
 *  be specified as
 *
 *	3
 *	** 2  3 * 4 ***
 *	   *  4 ? ? 2??    ?2
 *	 1   2 ?    ? ? ??   ? *
 */

#include <stdio.h>
#include <ctype.h>
#include <stdlib.h>
#include <strings.h>

extern const char *__progname;

typedef enum {
	  CT_UNK = 1,
	  CT_MINE,
	  CT_SAFE,
	  } CELLTYPE;

typedef struct cell CELL;
typedef struct unk UNK;
typedef struct eqn EQN;

struct eqn {
  int nunk;
  UNK **unk;
  int sum;
  int done;
  int x;
  } ;

struct cell {
  unsigned char x;
  unsigned char y;
  char text;
  CELLTYPE type;
  union {
    int ux; // CT_UNK
    // nothing for CT_MINE
    int count; // CT_SAFE
    } u;
  } ;

struct unk {
  CELL *c;
  unsigned char set;
  unsigned char cur;
  unsigned char res;
#define UR_U 1
#define UR_0 2
#define UR_1 4
  } ;

static int mines;
static int gridx;
static int gridy;
static CELL **grid;
static int nunk;
static UNK *unk;
static int neqn;
static EQN **eqn;
static int possible;

static void nopuzzle(void) __attribute__((__noreturn__));
static void nopuzzle(void)
{
 fprintf(stderr,"%s: no input puzzle\n",__progname);
 exit(1);
}

static void badpuzzle(const char *) __attribute__((__noreturn__));
static void badpuzzle(const char *why)
{
 fprintf(stderr,"%s: bad input puzzle (%s)\n",__progname,why);
 exit(1);
}

static void loadpuzzle(void)
{
 int c;
 int n;
 int x;
 CELL cell;

 n = -1;
 do c = getchar(); while ((c != EOF) && isspace(c));
 if (c == EOF) nopuzzle();
 if (c == '?')
  { mines = -1;
  }
 else
  { ungetc(c,stdin);
    scanf("%d%n",&mines,&n);
    if (n < 0) badpuzzle("bad mine count");
  }
 do c = getchar(); while ((c != EOF) && isspace(c));
 if (c == EOF) nopuzzle();
 ungetc(c,stdin);
 gridx = -1;
 gridy = 0;
 x = 0;
 grid = 0;
 while (1)
  { c = getchar();
    if (c == EOF)
     { if (x == 0) break;
       badpuzzle("incomplete last line");
     }
    else if (c == '\n')
     { if (gridx < 0)
	{ if (x > 127) badpuzzle("too large, max 127x127");
	  gridx = x;
	  if (x < 3) badpuzzle("too small, min 3x3");
	}
       else if (x != gridx)
	{ badpuzzle("X size inconsistent");
	}
       x = 0;
       gridy ++;
     }
    else if (isspace(c))
     { continue;
     }
    else
     { if (x == 0)
	{ grid = realloc(grid,(gridy+1)*sizeof(CELL *));
	  if (gridy > 0)
	   { grid[gridy] = malloc(gridx*sizeof(CELL));
	   }
	  else
	   { grid[0] = 0;
	   }
	}
       if (gridy == 0) grid[0] = realloc(grid[0],(x+1)*sizeof(CELL));
       if (gridy > 127) badpuzzle("too large, max 127x127");
       cell.text = c;
       cell.x = x;
       cell.y = gridy;
       switch (c)
	{ case '*':
	     cell.type = CT_MINE;
	     break;
	  case '?':
	     cell.type = CT_UNK;
	     break;
	  case '0': cell.u.count = 0;   if (0) {
	  case '1': cell.u.count = 1; } if (0) {
	  case '2': cell.u.count = 2; } if (0) {
	  case '3': cell.u.count = 3; } if (0) {
	  case '4': cell.u.count = 4; } if (0) {
	  case '5': cell.u.count = 5; } if (0) {
	  case '6': cell.u.count = 6; } if (0) {
	  case '7': cell.u.count = 7; } if (0) {
	  case '8': cell.u.count = 8; }
	     cell.type = CT_SAFE;
	     break;
	  default:
	     badpuzzle("invalid character");
	     break;
	}
       grid[gridy][x] = cell;
       x ++;
     }
  }
}

static char xletter(int x)
{
 return("ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz"[x]);
}

static char yletter(int y)
{
 return("abcdefghijklmnopqrstuvwxyz"[y]);
}

static void dumppuzzle(void)
{
 int x;
 int y;
 CELL *c;

 printf("mines=%d grid %dx%d\n",mines,gridx,gridy);
 for (x=0;x<gridx;x++) printf(" %c",xletter(x));
 printf("\n");
 for (x=0;x<gridx;x++) printf(" |");
 printf("\n");
 for (y=0;y<gridy;y++)
  { for (x=0;x<gridx;x++)
     { c = &grid[y][x];
       switch (c->type)
	{ case CT_UNK:
	     printf(" ?");
	     break;
	  case CT_MINE:
	     printf(" *");
	     break;
	  case CT_SAFE:
	     printf(" %c","_12345678"[c->u.count]);
	     break;
	  default:
	     abort();
	     break;
	}
     }
    printf(" -- %c\n",yletter(y));
  }
}

static int walkcells(int (*fn)(CELL *))
{
 int x;
 int y;
 int fr;
 int rv;

 rv = 0;
 for (y=gridy-1;y>=0;y--) for (x=gridx-1;x>=0;x--)
  { fr = (*fn)(&grid[y][x]);
    if (fr < 0) return(fr);
    rv += fr;
  }
 return(rv);
}

static void sortunkv_(UNK **v, UNK **t, int n)
{
 int na;
 int nb;
 int ia;
 int ib;
 int it;
 UNK *u;

 if (n < 2) return;
 na = n >> 1;
 nb = n - na;
 sortunkv_(v,t,na);
 sortunkv_(v+na,t,nb);
 ia = 0;
 ib = 0;
 it = 0;
 while (1)
  { if (ia < na)
     { if (ib < nb)
	{ UNK *u1;
	  UNK *u2;
	  u1 = v[ia];
	  u2 = v[na+ib];
	  if ( (u1->c->x < u2->c->x) ||
	       ( (u1->c->x == u2->c->x) &&
		 (u1->c->y < u2->c->y) ) )
	   { u = u1;
	     ia ++;
	   }
	  else
	   { u = u2;
	     ib ++;
	   }
	}
       else
	{ u = v[ia++];
	}
     }
    else
     { if (ib < nb)
	{ u = v[na+(ib++)];
	}
       else
	{ break;
	}
     }
    t[it++] = u;
  }
 if (it != n) abort();
 bcopy(t,v,n*sizeof(UNK *));
}

static void sortunkv(UNK **v, int n)
{
 static UNK **t = 0;
 static int nt = 0;

 if (n > nt)
  { free(t);
    nt = n;
    t = malloc(nt*sizeof(UNK *));
  }
 sortunkv_(v,t,n);
}

static int walkneighbours(CELL *c, int (*fn)(CELL *))
{
 int dx;
 int dy;
 int x;
 int y;
 int fr;
 int rv;

 rv = 0;
 for (dy=1;dy>=-1;dy--)
  { y = c->y + dy;
    if ((y < 0) || (y >= gridy)) continue;
    for (dx=1;dx>=-1;dx--)
     { if ((dx == 0) && (dy == 0)) continue;
       x = c->x + dx;
       if ((x < 0) || (x >= gridx)) continue;
       fr = (*fn)(&grid[y][x]);
       if (fr < 0) return(fr);
       rv += fr;
     }
  }
 return(rv);
}

/*
 * Build the EQN, if any, based on the count for cell c.  If c isn't
 *  CT_SAFE at all, this quietly does nothing.
 */
static int buildeqn(CELL *c)
{
 int nunk;
 int nmine;
 int nsafe;
 UNK *uv[8];
 EQN *e;
 int i;
 int j;

 if (c->type != CT_SAFE) return(0);
 nunk = 0;
 nmine = 0;
 nsafe = 0;
 // Summarize c's neighbourhood.
 walkneighbours(c,({ int foo(CELL *n)
		      { switch (n->type)
			 { case CT_UNK:
			      uv[nunk++] = &unk[n->u.ux];
			      break;
			   case CT_MINE:
			      nmine ++;
			      break;
			   case CT_SAFE:
			      nsafe ++;
			      break;
			 }
			return(0);
		      }
		     &foo;
		   }));
 // No CT_UNKs next to c?  No equation.
 if (nunk == 0) return(0);
 // Sort uv for de-duping.
 sortunkv(&uv[0],nunk);
 // See if we have a duplicate.
 for <"i"> (i=neqn-1;i>=0;i--)
  { if (eqn[i]->nunk != nunk) continue;
    for (j=nunk-1;j>=0;j--)
     { if (eqn[i]->unk[j] != uv[j]) continue <"i">;
     }
    // Duplicate.  No equation.
    return(0);
  }
 // New equation.  Save it.
 e = malloc(sizeof(EQN));
 e->nunk = nunk;
 e->unk = malloc(nunk*sizeof(UNK *));
 e->sum = c->u.count - nmine;
 e->x = neqn;
 if (e->sum < 0) badpuzzle("safe value less than adjacent mine count");
 bcopy(&uv[0],e->unk,nunk*sizeof(UNK *));
 eqn = realloc(eqn,(neqn+1)*sizeof(EQN *));
 eqn[neqn++] = e;
 return(0);
}

static void dumpeqns(int full)
{
 int i;
 EQN *e;
 UNK *u;

 for (i=0;i<neqn;i++)
  { int j;
    e = eqn[i];
    printf("[%d]: ",i);
    for (j=0;j<e->nunk;j++)
     { u = e->unk[j];
       printf("%s %c%c",j?" +":"",xletter(u->c->x),yletter(u->c->y));
       if (full && u->set) printf("=%d",u->cur);
     }
    printf(" = %d",e->sum);
    if (full && e->done) printf("   DONE");
    printf("\n");
  }
}

static void setup(void)
{
 int i;

 // Construct the UNKs.  First count them...
 nunk = 0;
 nunk = walkcells(({ int foo(CELL *c)
		      { return(c->type==CT_UNK);
		      }
		     &foo;
		   }));
 if (nunk < 1) badpuzzle("no unknowns!");
 // ...allocate the list...
 unk = malloc(nunk*sizeof(UNK));
 printf("Unknown count = %d\n",nunk);
 // ...and fill it in.
 i = 0;
 walkcells(({ int foo(CELL *c)
	       { if (c->type == CT_UNK)
		  { grid[c->y][c->x].u.ux = i;
		    if (i >= nunk) abort();
		    unk[i].c = c;
		    i ++;
		  }
		 return(0);
	       }
	      &foo;
	    }));
 if (i != nunk) abort();
 // Construct the equations.
 neqn = 0;
 eqn = 0;
 walkcells(&buildeqn);
 printf("Equation count %d\n",neqn);
 // Dump the equations out.
 dumpeqns(0);
}

static void solveprep(void)
{
 int x;

 for (x=nunk-1;x>=0;x--)
  { unk[x].set = 0;
    unk[x].res = 0;
  }
 for (x=neqn-1;x>=0;x--) eqn[x]->done = 0;
 possible = 0;
}

static EQN *pickeqn(void)
{
 int i;
 int j;
 EQN *e;
 EQN *beste;
 int bestu;
 int nu;

 beste = 0;
 for (i=neqn-1;i>=0;i--)
  { e = eqn[i];
    if (e->done) continue;
    nu = 0;
    for (j=e->nunk-1;j>=0;j--)
     { if (! e->unk[j]->set) nu ++;
     }
    if (!beste || (nu < bestu))
     { bestu = nu;
       beste = e;
     }
  }
 return(beste);
}

static void solvenext(void); // forward

/*
 * Try all variable values for an EQN, from variable N down to 0.  For
 *  those that satisfy it, call solvenext() to try another one.
 */
static void trysolve(EQN *e, int n)
{
 int i;
 UNK *u;

 if (e->done) abort();
 while ((n >= 0) && e->unk[n]->set) n --;
 if (n < 0)
  { int sum;
    sum = 0;
    for (i=e->nunk-1;i>=0;i--)
     { u = e->unk[i];
       if (! u->set) abort();
       if (u->cur) sum ++;
     }
    if (sum == e->sum)
     { e->done = 1;
       solvenext();
       e->done = 0;
     }
    return;
  }
 u = e->unk[n];
 if (u->set) abort();
 u->set = 1;
 u->cur = 0;
 trysolve(e,n-1);
 u->cur = 1;
 trysolve(e,n-1);
 u->set = 0;
}

/*
 * Pick an unchecked equation - pick one of the ones with the fewest
 *  variables which don't yet have values - and try all values of the
 *  unset variables.  When we find a combination that makes the
 *  equation true, recurse.
 *
 * Redundant non-duplicate equations get handled as equations which
 *  just happen to have zero unset variables.
 */
static void solvenext(void)
{
 EQN *e;
 int ux;
 UNK *u;

 e = pickeqn();
 if (! e)
  { int allunk;
    if (mines >= 0)
     { int nm;
       int nu;
       nm = 0;
       nu = 0;
       for (ux=nunk-1;ux>=0;ux--)
	{ u = &unk[ux];
	  if (! u->set) nu ++; else if (u->cur) nm ++;
	}
       if ((nm > mines) || (nm+nu < mines)) return;
       if (mines == nm) allunk = 0; else if (mines == nm+nu) allunk = 1; else allunk = -1;
     }
    else
     { allunk = -1;
     }
    printf("Possible: ");
    for (ux=0;ux<nunk;ux++)
     { u = &unk[ux];
       printf(" %c%c=",xletter(u->c->x),yletter(u->c->y));
       if (u->set)
	{ printf("%d",u->cur);
	}
       else
	{ if (allunk == 0)
	   { printf("°");
	     u->set = 2;
	     u->cur = 0;
	   }
	  else if (allunk == 1)
	   { printf("¹");
	     u->set = 2;
	     u->cur = 1;
	   }
	  else
	   { printf("?");
	   }
	}
     }
    printf("\n");
    possible ++;
    for (ux=nunk-1;ux>=0;ux--)
     { u = &unk[ux];
       switch (u->set)
	{ case 0:
	     u->res |= UR_U;
	     break;
	  case 2:
	     u->set = 0;
	     // fall through
	  case 1:
	     u->res |= u->cur ? UR_1 : UR_0;
	     break;
	  default:
	     abort();
	     break;
	}
     }
    return;
  }
 trysolve(e,e->nunk-1);
}

static void solve(void)
{
 solveprep();
 solvenext();
}

static void printresults(void)
{
 int ux;
 UNK *u;
 int x;
 int y;
 CELL *c;

 printf("\nResults: ");
 if (possible < 1)
  { printf("no solution found\n");
    return;
  }
 for (ux=0;ux<nunk;ux++)
  { u = &unk[ux];
    printf(" %c%c=",xletter(u->c->x),yletter(u->c->y));
    switch (u->res)
     { case UR_U              :
	  printf("?");
	  break;
       case UR_U | UR_0       :
       case UR_U        | UR_1:
       case UR_U | UR_0 | UR_1:
	  printf("~");
	  break;
       case        UR_0       :
	  printf("0");
	  break;
       case               UR_1:
	  printf("1");
	  break;
       case        UR_0 | UR_1:
	  printf("-");
	  break;
       default:
	  abort();
	  break;
     }
  }
 printf("\n");
 printf("\n");
 for (x=0;x<gridx;x++) printf(" %c ",xletter(x));
 printf("\n");
 for (x=0;x<gridx;x++) printf(" | ");
 printf("\n");
 for (y=0;y<gridy;y++)
  { for (x=0;x<gridx;x++)
     { c = &grid[y][x];
       switch (c->type)
	{ case CT_UNK:
	     u = &unk[c->u.ux];
	     switch (u->res)
	      { case UR_U              :
		   printf(" ? ");
		   break;
		case UR_U | UR_0       :
		case UR_U        | UR_1:
		case UR_U | UR_0 | UR_1:
		   printf(" ~ ");
		   break;
		case        UR_0       :
		   printf("<0>");
		   break;
		case               UR_1:
		   printf("<1>");
		   break;
		case        UR_0 | UR_1:
		   printf(" - ");
		   break;
		default:
		   abort();
		   break;
	      }
	     break;
	  case CT_MINE:
	     printf(" * ");
	     break;
	  case CT_SAFE:
	     printf(" %c ","_12345678"[c->u.count]);
	     break;
	  default:
	     abort();
	     break;
	}
     }
    printf(" -- %c\n",yletter(y));
  }

}

int main(void);
int main(void)
{
 loadpuzzle();
 dumppuzzle();
 setup();
 solve();
 printresults();
 return(0);
}