// MINIMO: multiple output logic function minimiser
//
//         Hamish Dewar 1981
//

// WARNING!!! This is a machine-translated source (by Perplexity AI)
// based on the minimo.imp in this directory.  It has been heavily
// modified by hand to allow it to compile and run, and the quality
// of the conversion cannot be relied on.  But it does seem to work.

// The comments are mostly Hamish's, a few are mine. (GT)

#define _GNU_SOURCE
#include <stdio.h>
#include <stdlib.h>
#include <stdbool.h>
#include <string.h>
#include <getopt.h>
#include <stdint.h>
#include <ctype.h>
#include <errno.h>
#include <error.h>
#include <stdarg.h>
#include <time.h>

#define UNASSIGNED  0x80808080

// Codes for logical operators
enum {
    OP_NOT = -1,
    OP_OR  = -2,  /* OR-1 == AND */
    OP_AND = -3
};

// Flag-bit
#define SIGN    0x80000000u
#define FORCED  0x40000000u

// Control parameters
int min = 4096;
int inc = 4096;

int mon = 0;           // monitoring selector (bits)

#ifdef bool
#undef bool
#endif
#define bool int
bool echo    = false;  // copy input to output stream
bool squash  = false;  // compress output tables
bool nin     = false;  // negate input variables
bool nout    = false;  // negate output variables
bool check   = false;  // check completeness
bool single  = false;  // apply single (rather than multiple) method (don't. currently doesn't seem to work.)
bool tabin   = false;  // tabular input

bool verbose = false;
bool debug   = false;

static int instream = 3;

static int negin_mask = UNASSIGNED, ignorin_mask = UNASSIGNED, negout_mask = UNASSIGNED, ignorout_mask = UNASSIGNED;
static int count = UNASSIGNED, aim = UNASSIGNED; // current,target score
static int minsep = UNASSIGNED;     // minimum free space in array W
static int sym = UNASSIGNED;
static int start_time_us = UNASSIGNED;

static int Rangecheck(int i, int low, int high, char *ra, int line) {
    if (debug && (i < low || i > high)) { fprintf(stderr, "Error: Index of %s[%d] out of range at line %d.\n", ra, i, line); return i/0; }
    return i;
}
#define RANGECHECK(i,low,high) Rangecheck(i,low,high,"w",__LINE__)
#define STOREBOUND  2000
static int dclim = UNASSIGNED, esslim = UNASSIGNED, sp1 = UNASSIGNED, sp = UNASSIGNED, np = UNASSIGNED, np1 = UNASSIGNED;  // index vars to array W
static int needsp;
typedef struct {
    int t;
    int f;
    int outs;
    int flags;
} Cell;
static Cell w[STOREBOUND]; // stack -> <- nest
#define W(x) w[RANGECHECK(x,1,STOREBOUND)]

#define NAMEBOUND    256
static int inmax = UNASSIGNED, outmin = UNASSIGNED, namemax = UNASSIGNED; // index vars to NAME,EXP
static char name[NAMEBOUND][8];
static int  exp[NAMEBOUND];

#define DEFBOUND    8192
static int dp = UNASSIGNED;
static int def[DEFBOUND];

static FILE *inputs[4] = { NULL, NULL, NULL, NULL };
static FILE *out_fp = NULL;

static int pend = 0;

static int bits(int v)
{
    int k = 0;
    if (v < 0) {
        k = 1;
        v = (v << 1) >> 1;
    }
    while (v != 0) {
        k++;
        v &= (v - 1);
    }
    return k;
}

static void out(int v)
{
    if (v >= 10) {
        out(v / 10);
        v -= (v / 10) * 10;
    }
    fputc('0' + v, out_fp);
}

static void croak(char *s, ...)
{
  va_list ap;
  fflush(out_fp);
  fprintf(stderr, "\n* ");

  va_start(ap, s);
  vfprintf(stderr, s, ap);
  va_end(ap);

  if (sym != '\n') {
    fprintf(stderr, "  Abandoned at: ");
    for (;;) {
      sym = fgetc(inputs[instream]);
      if (sym == '\n') break;
      fputc(sym, stderr);
    }
  }
  
  fprintf(stderr, "\n");
  exit(EXIT_FAILURE);
}

/* Timing stub; plug in real clock if desired. */
static int cputime_us(void) { return (clock()/(CLOCKS_PER_SEC/1000000)); }

static void print_time(void)
{
    int t = cputime_us();
    int dt = (t - start_time_us) /* / 1000 */;
    fprintf(out_fp, "     (%d us)", dt);
    //fprintf(out_fp, "%5d.%03d", dt, 0);
    start_time_us = t;
}

static void push(Cell v)
{
// Store V on (descending) nest
    np--;
    if (np < 0 || np >= STOREBOUND) croak("No space.");
    W(np) = v;
    if (np - sp >= minsep) return;
    minsep = np - sp;
    if (minsep > 2) return;
    croak("No space.");
}

static void stack(Cell v)
{
// Store V on (ascending) stack
    if (sp < 0 || sp >= STOREBOUND) croak("No space.");
    W(sp) = v;
    sp++;
    if (np - sp > minsep) return;
    minsep = np - sp;
    if (minsep > 2) return;
    croak("No space.");
}

static void read_sym(void)
{
    FILE *fp = inputs[instream];
    sym = pend; pend = 0;
    if (sym) return;
    for (;;) {
        sym = fgetc(fp);
        if (sym == EOF) {
          sym = '*';
          instream--;
          if (instream == 0) return;
          if (inputs[instream] == NULL) return;
          if (instream < 0) {
            sym = '\n';
            croak("Premature end of input.");
          }
          return read_sym();
        }
        if (echo) fputc(sym, out_fp);
        if (sym != '{') return;
        do {
            sym = fgetc(fp);
            if (echo) fputc(sym, out_fp);
        } while (sym != '}');
    }
}

static void read_name(char *curname)
{
// Read name (possibly null) to CURNAME leaving terminator in SYM
    int k, len = 0;
    do read_sym(); while (sym <= ' ');
    k = sym;
    //if (k >= 'a') k = k - 'a' + 'A';
    if (isalpha(k) && islower(k)) k = toupper(k);
    //if ('A' <= k && k <= 'Z') {
    if (isalpha(k)) {
        for (;;) {
            if (len < 6) curname[len++] = (char)k;
            read_sym();
            k = sym;
            if (isalpha(k) && islower(k)) k = toupper(k); 
            if (isdigit(k)) {
            } else if (isalpha(curname[len - 1]) && isupper(k)) {
            } else break;
        }
        if (sym == '?') {
            if (len < 7) curname[len++] = '?';
            read_sym();
        }
    }
    curname[len] = '\0';

    if (sym == ' ') {
        do read_sym(); while (sym == ' ');
        if (isalpha(sym)) {
            pend = sym;
            sym = ' ';
        }
    }
    fflush(out_fp); if (debug) fprintf(stderr, "[read_name:%s]", curname);
}

static int lookup(const char *curname)
{
    int pos = namemax + 1;
    while (--pos > 0) {
        if (strcmp(name[pos], curname) == 0) return pos;
    }
    return 0;
}

static void queryname(const char *curname)
{
    //if (echo) fputc('\n', out_fp);
    fprintf(out_fp, "%s not known\n", curname);
}

static void addname(const char *curname)
{
    if (namemax + 1 >= NAMEBOUND) croak("Too many names");
    ++namemax;
    strncpy(name[namemax], curname, 7);
    name[namemax][7] = '\0';
}

static void newname(const char *curname, int pos)
{
    if (pos != 0) croak("Duplicate: %s.", curname);
    addname(curname);
}

static void put(int v)
{
    if (dp >= DEFBOUND) croak("Definitions too long");
    def[dp++] = v;
}

static void read_int_simple(int *value)
{
    int sign = 1, c;
    *value = 0;
    do read_sym(); while (sym <= ' ');
    if (sym == '-') { sign = -1; read_sym(); }
    c = sym;
    while (isdigit(c)) {
        *value = *value * 10 + (c - '0');
        read_sym();
        c = sym;
    }
    *value *= sign;
    fflush(out_fp); if (debug) fprintf(stderr, "[read_int: %d]", *value);
}

static void init(int *v, int *found)
{
// Read asignment for mode variable V (default 1)
    *found = 1;
    *v = 1;
    if (sym == '=') {
        read_int_simple(v);
        out(*v);
    }
}

static void read_exp(void);

static void read_term(void)
{
    char curname[8];
    int pos;

    read_name(curname);
    if (curname[0] != '\0') {
        if (sym >= 'A' || sym == '(') pend = sym;
        pos = lookup(curname);
        if (pos == 0) {
            queryname(curname);
            pos = 1;
        }
        put(pos);
    } else if (sym == '\\') {
        put(OP_NOT);                   // fore ..
        read_term();
        put(OP_NOT);                   // .. as well as aft
    } else {
      if (sym != '(') croak("Faulty format. (Expecting '(', got '%c')", sym);
        read_exp();
        if (sym != ')') croak("Faulty format. (Expecting ')', got '%c')", sym);
        read_sym();
    }
}

static void read_exp1(void)
{
    read_term();
    while (sym == '&' || sym == '.' || sym >= 'A' || sym == '(') {
        read_term();
        put(OP_AND);
    }
}

static void read_exp(void)
{
// Read logic expression: store as Polish
//   operands represented as name index values (> 0)
//   operators < 0
//  eg A&B ! \A&\B  ==>  1 2 AND NOT 1 NOT NOT 2 NOT AND OR 0
//                       A B  &   \  A  \   \  B  \   &   !
//  note duplication of NOT before and after
  
    read_exp1();
    while (sym == '!' || sym == '+') {
        read_exp1();
        put(OP_OR);
    }
}

// R e a d   a n d   c h e c k   d a t a
//
static void readin(void)
{
    int bit, pos, pos1, found, first, dp1, outmax;
    char curname[8];

    namemax = 0;
    dp = 1;
    pend = 0;
// MODE settings (if any)
    for (;;) {
        read_name(curname);
        if (sym == '*') exit(EXIT_SUCCESS);
        if (strcmp(curname, "MODE") != 0) break;

        //fprintf(out_fp, "MODE ");
        //if (echo) fputc(pend, out_fp);
        //echo = !echo; // ?

        do {
            read_name(curname);
            found = 0;
            if (strcmp(curname, "NIN")    == 0) init(&nin, &found);
            if (strcmp(curname, "NOUT")   == 0) init(&nout, &found);
            if (strcmp(curname, "MIN")    == 0) init(&min, &found);
            if (strcmp(curname, "INC")    == 0) init(&inc, &found);
            if (strcmp(curname, "ECHO")   == 0) init(&echo, &found);
            if (strcmp(curname, "SQUASH") == 0) init(&squash, &found);
            if (strcmp(curname, "CHECK")  == 0) init(&check, &found);
            if (strcmp(curname, "MON")    == 0) init(&mon, &found);
            if (strcmp(curname, "SINGLE") == 0) init(&single, &found);
            // tabin and equin are mutually exclusive
            if (strcmp(curname, "TABIN")  == 0) init(&tabin, &found);
            if (strcmp(curname, "EQUIN")  == 0) { init(&tabin, &found); tabin = !tabin; }
            
            if (!found) fputc('?', out_fp);
        } while (sym == ',');

        //if (!echo) {
        //  echo = !echo; // ?
        //    if (echo) fputc('\n', out_fp);
        //}
    }
// INput list
    if (strcmp(curname, "IN") != 0) croak("Keyword %s? ", curname);

    if (pend == 0) pend = sym;
    bit = 1; negin_mask = 0; ignorin_mask = 0;

    for (;;) {
        if (bit == 0) croak("Too many inputs.");
        do read_sym(); while (sym <= ' ' && sym != ',');
        if (sym == '-') {
            ignorin_mask |= bit;
            strcpy(curname, "-");
            read_sym();
        } else {
            if (sym == '\\') {
                negin_mask |= bit;
            } else {
                pend = sym;
            }
            read_name(curname);
            pos = lookup(curname);
        }
        newname(curname, pos);
        exp[namemax] = bit;
        bit <<= 1;
        if (sym != ',') break;
    }

    inmax = namemax;
    if (nin) negin_mask = ~negin_mask;
// logic equations
    if (!tabin) {
        for (;;) {
            read_name(curname);
            if (sym != '=') break;
            pos = lookup(curname);
            if (pos <= inmax) pos = 0;
            newname(curname, pos);
            exp[namemax] = dp;   // start of Polish representation
            namemax--;           // hide LH name to exclude self-ref
            read_exp();
            namemax++;           // restore LH name
            put(0);              // terminator
            if (sym != '\n') croak("Faulty format.  Expecting end of line but got '%c'", sym);
        }
    } else {                     // tabular input
        pos1 = NAMEBOUND + 1;
        outmax = 0;
        for (;;) {
            do read_sym(); while (sym <= ' ');
            pend = sym;
            if ((sym & 95) == 'O') break;
            pos1--;
            if (pos1 == namemax) croak("Too many table entries");
            exp[pos1] = 0;
            first = 1;
            for (pos = 1; pos <= inmax; pos++) {
                if (((ignorin_mask >> (pos - 1)) & 1) == 0 &&
                    (sym == '0' || sym == '1')) {
                    if (sym == '1') {
                        put(pos);
                    } else {
                        put(OP_NOT);
                        put(pos);
                        put(OP_NOT);
                    }
                    if (!first) put(OP_AND);
                    first = 0;
                }
                do read_sym(); while (sym == ' ');
            }
            put(0);
            bit = 1;
            namemax = inmax;
            while (sym != '\n') {
                if ((sym != '0' && sym != '1') || namemax == outmax)
                    croak("Unexpected input '%c'.  (Was expecting '0' or '1'))", sym);
                if (sym == '1') exp[pos1] ^= bit;
                bit <<= 1;
                namemax++;
                do read_sym(); while (sym == ' ');
            }
            if (outmax == 0) outmax = namemax;
            if (outmax != namemax) croak("Faulty entry - outmax=%d namemax=%d.", outmax, namemax);
        }
        bit = 1;
        if (check) {
            bit = ~0;
            namemax = inmax + 1;
        }
        int initial_namemax = namemax;
        for (pos = inmax + 1; pos <= initial_namemax; pos++) {
            exp[pos] = dp;
            first = 1;
            int initial_pos1 = pos1;
            for (pos1 = NAMEBOUND; pos1 >= initial_pos1; pos1--) {
                if (exp[pos1] & bit) {
                    put(pos1);
                    if (!first) put(OP_OR);
                    first = 0;
                }
            }
            put(0);
            bit <<= 1;
        }
        dp1 = 1;
        int initial_pos1 = pos1;
        for (pos1 = NAMEBOUND; pos1 >= initial_pos1; pos1--) {
            exp[pos1] = dp1;
            do { dp1++; } while (def[dp1 - 1] != 0);
        }
        read_name(curname);
    }
// OUTput list
//  note that OUTput names are added again
//      to simplify treatment of "Don't cares"
    if (strcmp(curname, "OUT") != 0) croak("Keyword %s? (Expected 'OUT')", curname);

    pend = (pend == 0) ? sym : pend;
    outmin = namemax + 1;
    pos = inmax;
    negout_mask = 0;
    ignorout_mask = 0;
    bit = 1;

    for (;;) {
        if (namemax - outmin + 2 > 32) croak("Too many outputs.");
        do read_sym(); while (sym <= ' ' && sym != ',');
        if (sym == '-') {
            ignorout_mask |= bit;
            strcpy(curname, "-");
            read_sym();
        } else {
            if (sym == '\\') {
                negout_mask |= bit;
            } else {
                pend = sym;
            }
            read_name(curname);
        }
        if (!tabin) pos = lookup(curname); else pos = pos + 1;
        if (pos != 0) {                   // should be there
            addname(curname);
            exp[namemax] = dp;
            put(pos);
            if (!tabin) {
                strcat(curname, "?");     // any "Don't cares" for this one?
                pos = lookup(curname);
                if (pos != 0) {           // if so
                    put(pos);
                    put(OP_OR);
                }
            }
            put(0);
        } else {
            queryname(curname);
        }
        bit <<= 1;
        if (sym != ',') break;
    }
    if (outmin > namemax) exit(EXIT_SUCCESS);  // no (surviving) outputs
    if (sym != '\n') croak("Faulty format.");
    if (nout) negout_mask = ~negout_mask;
} /* READIN */

static void print_term(Cell v, int x)
{
    int i, l;
    int initial_inmax = inmax;
    for (i = 1; i <= initial_inmax; i++) {
        if (!squash) fputc(' ', out_fp);
        if (( (v.t | v.f) & 1 ) != 0) {
            l = ' ';
            if (v.f & 1) l = '\\';
            fputc(l, out_fp);
            fputs(name[i], out_fp);
        } else {
            l = (int)strlen(name[i]);
            for (int j = 0; j < (l + 1) / 2; j++) fputc(' ', out_fp);
            fputc('.', out_fp);
            for (int j = 0; j < l / 2; j++) fputc(' ', out_fp);
        }
        v.t >>= 1;
        v.f >>= 1;
    }
    if (!squash) fputc(' ', out_fp);
    fputc(':', out_fp);
    int initial_namemax = namemax;
    for (i = outmin; i <= initial_namemax; i++) {
        fputc(' ', out_fp);
        if (v.outs & 1) {
            fputs(name[i], out_fp);
        } else {
            l = (int)strlen(name[i]);
            for (int j = 0; j < (l - 1) / 2; j++) fputc(' ', out_fp);
            fputc((x & 1) == 0 ? '.' : '?', out_fp);
            for (int j = 0; j < l / 2; j++) fputc(' ', out_fp);
        }
        v.outs >>= 1;
        x >>= 1;
    }
    fputc('\n', out_fp);
}

static void monitor(int lim)
{
    int q;
    fputc('\n', out_fp);
    q = 1;
    while (q != lim) {
        if (mon & 4) fprintf(out_fp, "%2d", q);
        print_term(W(q), 0);
        q++;
    }
    fputc('\n', out_fp);
}

static void Copydown(int line)
{
    np1 = np;
    if (debug) fprintf(stderr, "line %d: while (sp != sp1) ...  sp=0x%x  sp1=0x%x\n", line, sp, sp1);
    while (sp != sp1) {
        sp -= 1; np -= 1;
        W(np) = W(sp);
    }
}
#define copydown() Copydown(__LINE__)

static void erase(int p)
{
    sp--;
    while (p != sp) {
        W(p) = W(p + 1);
        p++;
    }
}

static void merge(void)
{
    int p, k, same;
    static Cell v = {0,0,0,0}, n;
    n.t = n.f = n.outs = n.flags = 0;

    while (np != np1) {
        v = W(np);
        np++;
        p = sp1;
        same = 0;
        while (p != sp) {
            if ( ((W(p).t | v.t) == v.t) &&
                 ((W(p).f | v.f) == v.f) ) {  // V -> @P
                v.outs &= ~W(p).outs;
                if (v.outs == 0) break;
                if (W(p).t == v.t && W(p).f == v.f) same = p;
            }
            p++;
        }
        if (v.outs != 0) {
            while (p != sp1) {
                Cell n2 = n;
                p--;
                n2.outs = W(p).outs & v.outs;
                if (n2.outs != 0) {
                    n2.t = W(p).t | v.t;
                    n2.f = W(p).f | v.f;
                    k = (n2.t & n2.f);
                    if (k != 0 && ((k - 1) & k) == 0) {  // singleton
                        n2.t ^= k;
                        n2.f ^= k;
                        push(n2);
                        if ( ( (n2.t | v.t) == v.t ) &&
                             ( (n2.f | v.f) == v.f ) ) {  // V -> N
                            v.outs ^= n2.outs;
                        }
                        n2.t |= W(p).t;
                        n2.f |= W(p).f;
                    }
                    if (n2.t == W(p).t && n2.f == W(p).f) {  // @P -> N
                        W(p).outs ^= n2.outs;
                        if (W(p).outs == 0) {
                            erase(p);
                            if (same > p) same--;
                        }
                    }
                    if (v.outs == 0) break;
                }
            }
            if (v.outs != 0) {
                if (same == 0) {
                    W(sp) = v;
                    sp++;
                } else {
                    W(same).outs |= v.outs;
                }
            }
        }
    }
}

// C o n v e r t   f r o m   P o l i s h   t o   i n t e r n a l
//

#define HOLD(i) hold[Rangecheck(i,1,20,"hold",__LINE__)]
static void nested_convert(int j, int *p, int *hp, int *hold, int *inv, Cell *v)
{
    int defp = exp[j];
    for (;;) {
        j = def[defp++];       // get next item
        if (j == 0) return;    // terminator
        if (j > 0) {           // operand
            if (j > inmax) {   // start of sub-def
              nested_convert(j, p, hp, hold, inv, v);
            } else {
                *hp = (*hp) + 1;
                if (debug && ((*hp) < 1 || (*hp) > 20)) croak("*hp == %d out of range 1:20 at line %d\n", *hp, __LINE__);
                HOLD(*hp) = sp1;
                sp1 = sp;
                v->t = exp[j]; v->f = 0;
                if ((*inv ^ ((negin_mask >> (j - 1)) & 1)) != 0) { v->f = v->t; v->t = 0; }
                stack(*v);
            }
        } else if (j == OP_NOT) {
            *inv ^= 1;
        } else if (j - *inv == OP_AND) {  // 'AND' or inverted 'OR'
            np1 = np;          // Form pairwise intersection on nest
            while (sp != sp1) {
                sp--;
                *p = sp1;//                     <---------------  p !!!
                while (*p != HOLD(*hp)) {
                    //Cell v2;
                    (*p) -= 1;
                    v->t = W(sp).t | W(*p).t;
                    v->f = W(sp).f | W(*p).f;
                    if ((v->t & v->f) == 0) {
                      push(*v);  // intersection ok
                    }
                }
            }
            sp1 = HOLD(*hp);
            *hp = (*hp) - 1;
            if (debug && ((*hp) < 1 || (*hp) > 20)) croak("*hp == %d out of range 1:20 at line %d\n", *hp, __LINE__);
            sp = sp1;            // start with stack empty
            merge();
        } else {                 // 'OR' or inverted 'AND'
            copydown();          // one operand to nest
//if (debug && (*hp == 0)) *hp = 1;
            sp1 = HOLD(*hp);
            *hp = (*hp) - 1;
//if (debug && ((*hp) < 1 || (*hp) > 20)) fprintf(stderr, "*hp == %d out of range 1:20 at line %d\n", *hp, __LINE__);
            merge();
        }
    }
}

static void convert(void)
{
    int outbit = UNASSIGNED, oldsp = UNASSIGNED, i = UNASSIGNED, j = UNASSIGNED, k = UNASSIGNED, p = UNASSIGNED, q = UNASSIGNED, hp = UNASSIGNED, inv = UNASSIGNED;
    static Cell v = {0,0,0,0};
    int hold[21];

    sp = 1; np = STOREBOUND; minsep = np - sp;
    v.flags = 0;
    outbit = 1;
    int initial_namemax = namemax;
    for (i = outmin; i <= initial_namemax; i++) {
        if ((ignorout_mask & outbit) == 0) {
            k = def[exp[i] + 1]; // 2nd element of def
            if (k != 0) {        // "Don't cares" present
                sp1 = 1;  hp = 0;  inv = 0;
                if (debug) fprintf(stderr, "line %d: hp set to 0\n", __LINE__-1);
                v.outs = outbit;
                nested_convert(k, &p, &hp, hold, &inv, &v);
                copydown();
                sp1 = 1;
                merge();
            }
        }
        outbit <<= 1;
    }

    dclim = sp;
    outbit = 1;
    initial_namemax = namemax;
    for (i = outmin; i <= initial_namemax; i++) {
        if ((ignorout_mask & outbit) == 0) {
            sp1 = 1;  hp = 0;  inv = (negout_mask >> (i - outmin)) & 1;
            if (debug) fprintf(stderr, "line %d: hp set to 0\n", __LINE__-1);
            // BUG.  hp is used to index hold[] before it is ever set to 1 :-(
            v.outs = outbit;
            nested_convert(i, &p, &hp, hold, &inv, &v);
            copydown();
            sp1 = dclim;
            if (single) merge(); else {
                oldsp = sp;
                while (np != np1) {  // each element against rest
                    q = sp1 - 1;     //  and null (ie straight)
                    v = (Cell) {0,0,0,0};
                    while (1) {
                        v.t |= W(np).t;  v.f |= W(np).f;
                        if ((v.t & v.f) == 0) {
                            v.outs |= outbit;
                            p = sp;
                            while (p != sp1) {
                                p--;
                                if (W(p).t == v.t && W(p).f == v.f) v.outs |= W(p).outs;
                                j = W(p).t | v.t;  k = W(p).f | v.f;
                                if (j == v.t && k == v.f && (W(p).outs & v.outs) == v.outs) {
                                    break; // V -> @P
                                }
                                if (j == W(p).t && k == W(p).f && (W(p).outs & v.outs) == W(p).outs) {
                                    if (p < oldsp) oldsp -= 1;
                                    if (p <= q) q -= 1;
                                    erase(p);
                                }
                            }
                            if (p == sp1) stack(v);
                        }
                        q += 1;
                        if (q == oldsp) break;
                        v = W(q);
                    }
                    np += 1;
                }
            }
        }
        outbit <<= 1;
    }
} // convert

static int needed(int q, int testlim)
{
    int p;
    static Cell v = {0,0,0,0}, n={0,0,0,0};
    sp1 = sp; np1 = np;
    v = W(q);
    W(sp1).t = v.t;  W(sp1).f = v.f;
    W(sp1).outs = 0;
    sp += 1;
    p = 1;
    while (p != testlim) {
        if (W(p).flags >= 0) {
            n.outs = W(p).outs & v.outs;
            if (n.outs != 0 && p != q) {
                n.t = W(p).t | v.t; n.f = W(p).f | v.f;
                if ((n.t & n.f) == 0) {
                    np -= 1;  W(np) = n;
                    merge();
                    if (W(sp1).outs == v.outs) break;
                }
            }
        }
        p += 1;
    }
    needsp = sp;
    sp = sp1;
    return p;
}

static void print_all(void)
{
    int p, q;
    fprintf(out_fp, "\n\n");
    q = dclim; if (mon & 2) q = esslim;
    while (q != sp) {
        if (W(q).flags >= 0) {
            p = needed(q, sp);
            if (mon & 4) fprintf(out_fp, "%2d", q);
            W(sp1).outs = W(q).outs - W(sp1).outs;
            print_term(W(sp1), W(q).outs);
        }
        q += 1;
    }
    fputc('\n', out_fp);
    (void)p;
}

static void pcount(void)
{
    fprintf(out_fp, "%d", count >> 12);
    fputc('/', out_fp);
    out(count & 4095);
}

static void promote(int q, int past)
{
    Cell v = W(q);
    if (past == 0) {
        count += bits(v.t | v.f) + 4096;
        past = esslim++;
    }
    while (past != esslim && past != dclim) {
        if (W(past - 1).flags <= v.flags) break;
        past--;
    }
    while (q != past) {
        q -= 1;
        W(q + 1) = W(q);
    }
    W(q) = v;
}

// R e d u c e   n u m b e r   o f   i m p l i c a n t s
//
static void reduce1(void)
{
// Find first essentials and redundants
//   order by weight
    int p, q;
    q = dclim;
    esslim = q;
    while (q != sp) {
        W(q).flags = (bits(W(q).t | W(q).f) << 5) +
                     31 - bits(W(q).outs);
        p = needed(q, sp);
        if (p == sp) {
            promote(q, 0);
        } else if (p >= esslim) {
            promote(q, q);
        } else {
            erase(q);
            q--;
        }
        q++;
    }
}

static void reduce2(void)
{
// Find secondary essentials & redundants
    int p, q, bq, sphold, done;
    Cell v;

    do {
        done = 1;
        q = sp;
        while (q != esslim) {
            q--;
            p = needed(q, esslim);
            if (p == esslim) {  // not (simply) redundant
                W(q).outs ^= W(sp1).outs;
                W(sp1).outs = 0;
                bq = W(q).flags >> 5;
                sphold = sp;
                while (p != sp) {
                    if ((W(p).flags >> 5) - min < bq && p != q) {
                        int v_outs = W(p).outs & W(q).outs;
                        if (v_outs != 0) {
                            v.outs = v_outs;
                            v.t = W(p).t | W(q).t;
                            v.f = W(p).f | W(q).f;
                            if ((v.t & v.f) == 0) {
                                sp1 = sp;
                                sp = needsp;
                                while (sp1 != needsp) {
                                    W(sp) = W(sp1);
                                    sp++;
                                    sp1++;
                                }
                                push(v);
                                merge();
                                sp = sphold;
                                if (W(sp1).outs == W(q).outs) break;
                            }
                        }
                    }
                    p++;
                }
                if (p != sp) {          // redundant
                    erase(q);
                    if (p > q) p--;
                    if (p >= esslim) {  // P may now be essential
                        if (needed(p, sp) == sp) {
                            if (p >= q) q++;
                            promote(p, 0);
                            done = 0;
                        }
                    }
                }
            }
        }
    } while (!done);
}

static void order(void)
{
    int j, /*k,*/ p, q, r, poss, last;
    int *link;
    Cell v;

    link = (int *)calloc(sp+1, sizeof(int));
    if (!link) croak("No memory");

    q = sp; poss = 0; last = sp;
    while (q != esslim) {
        q--;
        p = needed(q, sp);
        link[q] = p;
        if (p > q && link[p] > p) {
            poss++;
            if (q != last) poss += 99;
            v = W(p);   // promote P before Q
            r = sp;
            do {
                r--;
                j = link[r];
                if (j == p) j = q;
                else if (q <= j && j < p) j = j + 1;

                if (r >= p) {
                    link[r] = j;
                } else {
                    link[r + 1] = j;
                    W(r + 1) = W(r);
                }
            } while (r != q);
            W(r) = v;
            q += 2;
            last = q - 1;  // try Q again
        }
    }
    fprintf(out_fp, "%d", poss);
// First pass
    do {
        v = W(q);
        v.flags >>= 5;
        p = needed(q, sp);
        if (p > q) {
            count = count + v.flags + 4096;
            W(q).flags = v.flags + (count << 5);
        } else {
            do { p++; } while (W(p).flags < 0);
            r = q;
            while (r != p) {
                r--;
                W(r + 1) = W(r);
            }
            v.flags = (W(r - 1).flags & 0x0FFFFFE0) + v.flags + (int)SIGN;
            W(r) = v;
        }
        q++;
    } while (q != sp);

    free(link);
} /* ORDER */

static void minimise(void)
{
// Find minimal selection
    int k, p, q, m;
    q = sp;
    while (1) {
        while (q != sp) {
            m = W(q).flags;
            p = needed(q, sp);
            if (p == sp) {           // mandatory
                m += (int)FORCED;
            } else {                 // optional or redundant
                if (p < q) m += (SIGN + FORCED); // redundant
            }
            if (m >= 0) {       // selected
                k = (m & 31) + count + 4096;
                if (k + inc > aim) break;
                if (k + inc > ((m >> 5) & 0x7FFFFF)) break;
                count = k;
            }
            W(q).flags = m;
            q++;
        }
        if (q == sp) {                // scan completed successfully
            pcount();
            if (inc == 0 || (mon & 1)) print_all();
            aim = count;
            q = esslim;
            while (q != sp) {         // save marker bits
                k = W(q).flags & 0xCFFFFFFF;
                W(q).flags = ((k & 0xC0000000) >> 2) + k;
                q++;
            }
        }
        for (;;) {                    // scan backward to de-select
            if (q == esslim) {        // scan completed
                while (q != sp) {     // restore marker bits 
                    k = W(q).flags & 0x3FFFFFFF;
                    W(q).flags = ((k & 0x30000000) << 2) + k;
                    q++;
                }
                if (inc <= min) return;  // all done
                count = aim;           // restore count
                inc >>= 1;
                if (inc == 0) print_all();
            }
            q--;
            m = W(q).flags;
            W(q).flags = m & 0x3FFFFFFF;
            if (m >= 0) {
                k = (m & 31) + 4096;
                count -= k;
                if (!(m & (int)FORCED)) break;
            }
        }
        W(q).flags += (int)SIGN;
        q++;
    }
} /* MINIMISE */


int main(int argc, char *argv[])
{
    /* up to 3 input filenames, stored in infilename[1..3] */
    const char *infilename[4] = { NULL, NULL, NULL, NULL };
    const char *outfilename = NULL;

    int input_count = 0;

    /* long options table */
    enum {
        OPT_MIN = 1000,
        OPT_INC,
        OPT_MON,
        OPT_ECHO,
        OPT_NO_ECHO,
        OPT_SQUASH,
        OPT_NO_SQUASH,
        OPT_NIN,
        OPT_NO_NIN,
        OPT_NOUT,
        OPT_NO_NOUT,
        OPT_CHECK,
        OPT_NO_CHECK,
        OPT_SINGLE,
        OPT_NO_SINGLE,
        OPT_TABIN,
        OPT_NO_TABIN,
        OPT_EQUIN,
        OPT_NO_EQUIN,
        OPT_INPUT,    /* --input, -i */
        OPT_OUTPUT    /* --output, -o */
    };

    static const struct option long_opts[] = {
        { "min",      required_argument, NULL, OPT_MIN      },
        { "inc",      required_argument, NULL, OPT_INC      },
        { "mon",      required_argument, NULL, OPT_MON      },

        { "echo",     no_argument,       NULL, OPT_ECHO     },
        { "no-echo",  no_argument,       NULL, OPT_NO_ECHO  },

        { "squash",   no_argument,       NULL, OPT_SQUASH   },
        { "no-squash",no_argument,       NULL, OPT_NO_SQUASH},

        { "nin",      no_argument,       NULL, OPT_NIN      },
        { "no-nin",   no_argument,       NULL, OPT_NO_NIN   },

        { "nout",     no_argument,       NULL, OPT_NOUT     },
        { "no-nout",  no_argument,       NULL, OPT_NO_NOUT  },

        { "check",    no_argument,       NULL, OPT_CHECK    },
        { "no-check", no_argument,       NULL, OPT_NO_CHECK },

        { "single",   no_argument,       NULL, OPT_SINGLE   },
        { "no-single",no_argument,       NULL, OPT_NO_SINGLE},

        { "tabin",    no_argument,       NULL, OPT_TABIN    },
        { "no-tabin", no_argument,       NULL, OPT_NO_TABIN },

        { "equin",    no_argument,       NULL, OPT_EQUIN    },
        { "no-equin", no_argument,       NULL, OPT_NO_EQUIN },

        { "input",    required_argument, NULL, OPT_INPUT    },
        { "output",   optional_argument, NULL, OPT_OUTPUT   },

        { "help",     no_argument,       NULL, 'h'          },
        { "verbose",  no_argument,       NULL, 'v'          },
        { "debug",    no_argument,       NULL, 'd'          },
        { 0,          0,                 0,    0            }
    };

    const char *prog = argv[0];

    /* Disable getopt's own error messages; handle ourselves. */
    opterr = 0;

    while (1) {
        int opt_index = 0;
        int c = getopt_long(argc, argv, "hvdi:o:", long_opts, &opt_index);
        if (c == -1)
            break;

        switch (c) {
        case 'h':
            printf("Usage: %s [options] [input1 [input2 [input3]]]\n\n", prog);
            printf("Options:\n");
            printf("  --input FILE, -i FILE, FILE  up to 3 inputs, none given defaults to stdin\n");
            printf("  --output FILE, -o FILE       defaults to stdout\n");
            printf("  --min N                      \n");
            printf("  --inc N                      \n");
            printf("  --mon N                      monitor features (bit array)\n");
            printf("  --echo / --no-echo           copy input to output stream\n");
            printf("  --squash / --no-squash       compress output tables\n");
            printf("  --nin / --no-nin             negate input variables\n");
            printf("  --nout / --no-nout           negate output variables\n");
            printf("  --check / --no-check         check completeness\n");
            printf("  --single / --no-single       apply single (rather than multiple) method\n");
            printf("  --tabin                      tabular format input\n");
            printf("  --equin                      equation format input\n");
            printf("  -v                           verbose output\n");
            printf("  -d                           debugging output\n");
            return 0;

        case 'd':
            debug = true;
            break;
            
        case 'v':
            verbose = true;
            break;
            
        case 'i':
        case OPT_INPUT:
            if (input_count >= 3) {
                fprintf(stderr, "%s: too many input files (maximum 3)\n", prog);
                return 1;
            }
            infilename[++input_count] = optarg;
            break;

        case 'o':
        case OPT_OUTPUT:
            outfilename = optarg;
            break;

        case OPT_MIN:
        case OPT_INC:
        case OPT_MON: {
            char *endp = NULL;
            long v = strtol(optarg, &endp, 10);
            if (!optarg[0] || *endp != '\0' || v <= 0) {
                fprintf(stderr, "%s: option --%s requires a positive integer\n",
                        prog, long_opts[opt_index].name);
                return 1;
            }
            if (c == OPT_MIN) min = (int)v;
            else if (c == OPT_INC) inc = (int)v;
            else mon = (int)v;
            break;
        }

        case OPT_ECHO:      echo   = true;  break;
        case OPT_NO_ECHO:   echo   = false; break;
        case OPT_SQUASH:    squash = true;  break;
        case OPT_NO_SQUASH: squash = false; break;
        case OPT_NIN:       nin    = true;  break;
        case OPT_NO_NIN:    nin    = false; break;
        case OPT_NOUT:      nout   = true;  break;
        case OPT_NO_NOUT:   nout   = false; break;
        case OPT_CHECK:     check  = true;  break;
        case OPT_NO_CHECK:  check  = false; break;
        case OPT_SINGLE:    single = true;  break;
        case OPT_NO_SINGLE: single = false; break;
        case OPT_TABIN:     tabin  = true;  break;
        case OPT_NO_TABIN:  tabin  = false; break;
        case OPT_EQUIN:     tabin  = false;  break;
        case OPT_NO_EQUIN:  tabin  = true; break;

        case '?':
        default:
            if (optopt) {
                fprintf(stderr, "%s: unknown option '-%c'\n", prog, optopt);
            } else if (optind <= argc && argv[optind - 1]) {
                fprintf(stderr, "%s: invalid option '%s'\n", prog,
                        argv[optind - 1]);
            } else {
                fprintf(stderr, "%s: invalid option\n", prog);
            }
            fprintf(stderr, "Try '%s --help' for usage.\n", prog);
            return 1;
        }
    }

    /* Collect positional input filenames (no -i/--input) */
    while (optind < argc && input_count < 3) {
        infilename[++input_count] = argv[optind++];
    }

    if (optind < argc && input_count >= 3) {
        fprintf(stderr, "%s: too many input files (maximum 3)\n", prog);
        return 1;
    }

    if (input_count == 0) {
        //fprintf(stderr, "%s: no input file specified\n", prog);
        //fprintf(stderr, "Try '%s --help' for usage.\n", prog);
        //return 1;
    } else if (input_count == 1) {
        infilename[3] = infilename[1];
        infilename[1] = infilename[2] = NULL;
    } else if (input_count == 2) {
        const char *a = infilename[1];
        const char *b = infilename[2];
        infilename[1] = NULL;
        infilename[2] = b;
        infilename[3] = a;
    } else if (input_count == 3) {
        const char *a = infilename[1];
        const char *b = infilename[2];
        const char *c = infilename[3];
        infilename[1] = c;
        infilename[2] = b;
        infilename[3] = a;
    }

    if (debug) {
      printf("Parameters:\n");
      printf("  min=%d inc=%d mon=%d\n", min, inc, mon);
      printf("  echo=%d squash=%d nin=%d nout=%d check=%d single=%d tabin=%d\n",
             echo, squash, nin, nout, check, single, tabin);
      printf("  inputs: %s %s %s\n",
             input_count == 0 || infilename[3] == NULL ? "<stdin>" : infilename[3],
             infilename[2] ? infilename[2] : "",
             infilename[1] ? infilename[1] : "");
      printf("  output: %s\n", outfilename ? outfilename : "<stdout>");
    }
    
    inputs[1] = NULL;
    inputs[2] = NULL;
    inputs[3] = stdin;

    if (infilename[1] != NULL) {
      inputs[1] = fopen(infilename[1], "r");
      if (inputs[1] == NULL) {
        fprintf(stderr, "%s: Cannot open input file \"%s\" - %s\n", prog, infilename[1], strerror(errno));
        exit(EXIT_FAILURE);
      }
    }

    if (infilename[2] != NULL) {
      inputs[2] = fopen(infilename[2], "r");
      if (inputs[2] == NULL) {
        fprintf(stderr, "%s: Cannot open input file \"%s\" - %s\n", prog, infilename[2], strerror(errno));
        exit(EXIT_FAILURE);
      }
    }

    if (infilename[3] != NULL) {
      inputs[3] = fopen(infilename[3], "r");
      if (inputs[3] == NULL) {
        fprintf(stderr, "%s: Cannot open input file \"%s\" - %s\n", prog, infilename[3], strerror(errno));
        exit(EXIT_FAILURE);
      }
    }

    out_fp = stdout;
    if (outfilename != NULL) {
      out_fp = fopen(outfilename, "w");
      if (out_fp == NULL) {
        fprintf(stderr, "%s: Cannot open output file \"%s\" - %s\n", prog, outfilename, strerror(errno));
        exit(EXIT_FAILURE);
      }
    }

    instream = 3;

    while (inputs[instream]) {
        start_time_us = cputime_us();
        readin();
        if (verbose) {
          fputs("Read in:", out_fp);
          print_time();
          fputc('\n', out_fp);
        }
        
        convert();
        aim = 999999;
        count = 0;

        if (verbose) {
          fputs("Implicants:", out_fp);
          fprintf(out_fp, "%3d", sp - dclim);
          print_time();
          fputc('\n', out_fp);
        }
        
        if (inc != 0 && (mon & 16)) print_all();

        reduce1();
        if (verbose) {
          fputs("Reduced(1):", out_fp);
          fprintf(out_fp, "%3d", sp - dclim);
          fputs(" (nucleus", out_fp);
          pcount();
          fputc(')', out_fp);
          print_time();
          fputc('\n', out_fp);
        }
        
        if (inc != 0 && (mon & 16)) print_all();

        if (sp != esslim) {
            reduce2();
            if (verbose) {
              fputs("Reduced(2):", out_fp);
              fprintf(out_fp, "%3d", sp - dclim);
              fputs(" (nucleus", out_fp);
              pcount();
              fputc(')', out_fp);
              if (sp != esslim) order();
              print_time();
              fputc('\n', out_fp);
            }
            if (inc != 0 && (mon & 16)) print_all();
        }

        if (verbose) {
          if (mon & 2) monitor(esslim);
          if (sp != esslim) {
              if (mon & 8) monitor(sp);
              fputs("Minimised:", out_fp);
              minimise();
          }
        }

        if (inc != 0 && (mon & 1) == 0) print_all();
        if (verbose) {
          fputs(" Cells used:", out_fp);
          fprintf(out_fp, "%d", STOREBOUND - 1 - minsep);
          print_time();
          fputc('\n', out_fp);
        }
    }

    if (out_fp != stdout) fclose(out_fp);
    for (int i = 1; i <= 3; i++)
        if (inputs[i] && inputs[i] != stdin) fclose(inputs[i]);

    return 0;

}