/* gpchecksubwa.c   22.4.96.
 * 31/12/98 change to deal with fact that subwa now has state type
 * labeled.
 * 26/10/98 large scale reorganisation to omit globals, etc.
 * 5/2/98 change generators from type char to type `gen'.
 * 6.5.97. corrected bug - not enough space allocated for storedmult.
 * Check the correctness of the subgroup word acceptor output by gpsubwa.
 * If incorrect, output some words in the subgroup that are not
 * accepted by the word accpetor, so that gpsubwa can use them on re-running.
 *
 * SYNOPSIS:
 * gpchecksubwa [-ip d/s[dr]] [-op d/s] [-silent] [-v] [-l] [-f] [-s]
 *    [-m maxwords] groupname [subname]
 *
 * subname defaults to "sub".
 * autcos (or equaivalents) must already have been run on groupname.
 * groupname.subname should contain the definition of the subgroup,
 * in the standard format.
 * Input is from groupname.subname.wa and groupname.gm.
 * Output to (and input from) temporary files groupname.m* (for
 * multipliers) and groupname.subname.submult.
 * If word acceptor is wrong, output of original subgroup generators +
 * offending elements of subgroup to groupname.subname.words.
 *
 * OPTIONS:
 * -ip d/s[dr]  input in dense or sparse format - dense is default
 * -op d/s      output in dense or sparse format - sparse is default
 * -m  maxwords  Abort after finding maxwords offending words w
 *              default is MAXWORDS
 * -v           verbose
 * -silent      no diagnostics
 * -l/-h        large/huge hash-tables (for big examples)
 * -f           read the transition table repeatedly from file while minimizing,
 *              in calls of fsa_composite.
 *              This avoids storing large tables, but is a little slower.
 * -s  Throw away files immediately after use whenever possible, to
 *              save disk-space. This will slow things down considerably.
 */

#include <stdio.h>

#include "defs.h"
#include "fsa.h"
#include "rws.h"
#include "definitions.h"

#define MAXWORDLEN 2048
#define MAXSUBGENS 1024
#define MAXWORDS 16

static int maxsubgens = MAXSUBGENS, maxwordlen = MAXWORDLEN,
           maxwords = MAXWORDS;

static char gpname[100], subname[100], inf[100], outf[100], fsaname[100],
    tempfilename[100];
static fsa subwa, genmult, mult, mult1, mult2, *compmultptr, *submultptr,
    *existsptr;
static int ngens, nsubgens, numstoredmult, delim;
static char **names, **storedmult;
static gen *subgen[MAXSUBGENS], testword[MAXWORDLEN + 1], **badwords;
static storage_type ip_store = DENSE;
static int dr = 0;
static storage_type op_store = SPARSE;
static boolean readback = TRUE;
static boolean keepfiles = TRUE;
static FILE *rfile, *wfile;

/* Functions defined in this file */
static char *file_suffix(gen *w);
static int subgen_multiplier(gen *w, char *s);
static void read_subgpgens(void);
static int output_bad_words(void);
static void badusage(void);

int main(int argc, char *argv[])
{
  int arg, i, j, ct;
  char *suff;
  boolean gotsuff;

  setbuf(stdout, (char *)0);
  setbuf(stderr, (char *)0);

  arg = 1;
  while (argc > arg) {
    if (strcmp(argv[arg], "-ip") == 0) {
      arg++;
      if (arg >= argc)
        badusage();
      if (strcmp(argv[arg], "d") == 0)
        ip_store = DENSE;
      else if (argv[arg][0] == 's') {
        ip_store = SPARSE;
        if (stringlen(argv[arg]) > 1)
          dr = atoi(argv[arg] + 1);
      }
      else
        badusage();
    }
    else if (strcmp(argv[arg], "-op") == 0) {
      arg++;
      if (arg >= argc)
        badusage();
      if (strcmp(argv[arg], "d") == 0)
        op_store = DENSE;
      else if (strcmp(argv[arg], "s") == 0)
        op_store = SPARSE;
      else
        badusage();
    }
    else if (strcmp(argv[arg], "-silent") == 0)
      kbm_print_level = 0;
    else if (strcmp(argv[arg], "-v") == 0)
      kbm_print_level = 2;
    else if (strcmp(argv[arg], "-vv") == 0)
      kbm_print_level = 3;
    else if (strcmp(argv[arg], "-l") == 0)
      kbm_large = TRUE;
    else if (strcmp(argv[arg], "-h") == 0)
      kbm_huge = TRUE;
    else if (strcmp(argv[arg], "-f") == 0)
      readback = FALSE;
    else if (strcmp(argv[arg], "-s") == 0)
      keepfiles = FALSE;
    else if (strcmp(argv[arg], "-m") == 0) {
      arg++;
      if (arg >= argc)
        badusage();
      maxwords = atoi(argv[arg]);
    }
    else {
      if (argv[arg][0] == '-')
        badusage();
      if (strcmp(gpname, "") != 0 && strcmp(subname, "") != 0)
        badusage();
      if (strcmp(gpname, "") != 0)
        strcpy(subname, argv[arg]);
      else
        strcpy(gpname, argv[arg]);
    }
    arg++;
  }
  if (stringlen(gpname) == 0)
    badusage();
  if (stringlen(subname) == 0)
    strcpy(subname, "sub");

  sprintf(tempfilename, "%s_%stemp_axXXX", gpname, subname);


  /* First read in the candidate for the subgroup automaton. */
  sprintf(inf, "%s.%s.wa", gpname, subname);
  if ((rfile = fopen(inf, "r")) == 0) {
    fprintf(stderr, "Cannot open file %s.\n", inf);
    exit(1);
  }
  fsa_read(rfile, &subwa, DENSE, 0, 0, TRUE, fsaname);
  fclose(rfile);
  /* Since this now has states of type labeled, we need to remove this
   * structure, or fsa_equal will not work in the correctness test.
   */
  srec_clear(subwa.states->labels);
  tfree(subwa.states->labels);
  tfree(subwa.states->setToLabels);
  subwa.states->type = SIMPLE;
  fsa_minimize(&subwa);
  if (kbm_print_level > 1)
    printf("  #Number of states of subwa after minimisation = %d.\n",
           subwa.states->size);


  ngens = subwa.alphabet->size;
  names = subwa.alphabet->names;
  process_names(names, ngens);

  /* Now we read in the subgroup generators. */
  sprintf(inf, "%s.%s", gpname, subname);
  if ((rfile = fopen(inf, "r")) == 0) {
    fprintf(stderr, "Cannot open file %s.\n", inf);
    exit(1);
  }
  read_subgpgens();
  fclose(rfile);

  if (keepfiles) {
    /* Assign space for storedmult; storedmult[i] will be the file suffix where
     * the i-th multiplier automaton is stored.
     */
    ct = nsubgens;
    for (i = 0; i < nsubgens; i++)
      ct += 2 * genstrlen(subgen[i]);
    tmalloc(storedmult, char *, ct);
    numstoredmult = 0;
  }

  /* Now, for each subgroup generator, form the corresponding multiplier
   * automaton in the group, intersect its language with that of the
   * candidate subgroup word acceptor, and check its closure on multiplying
   * by that subgroup generator (on either side).
   */
  for (i = 0; i < nsubgens; i++) {
    if (kbm_print_level > 0) {
      kbm_buffer[0] = '\0';
      add_to_buffer(0, "#Processing subgroup generator:  ");
      add_word_to_buffer(stdout, subgen[i], names);
      printbuffer(stdout);
    }
    suff = file_suffix(subgen[i]);
    gotsuff = FALSE;
    if (keepfiles) {
      /* Check to see if we have of this multiplier already */
      for (j = 1; j <= numstoredmult; j++) {
        if (strcmp(suff, storedmult[j]) == 0)
          gotsuff = TRUE;
      }
    }
    if (!gotsuff) {
      if (subgen_multiplier(subgen[i], suff) == -1)
        exit(1);
    }

    sprintf(inf, "%s.m%s", gpname, suff);
    if ((rfile = fopen(inf, "r")) == 0) {
      fprintf(stderr, "Cannot open file %s.\n", inf);
      exit(1);
    }
    fsa_read(rfile, &mult, DENSE, 0, 0, TRUE, fsaname);
    fclose(rfile);
    if (kbm_print_level > 1) {
      printf("  #Number of states of multiplier = %d.\n", mult.states->size);
      printf("  #Intersecting with candidate subgroup word-acceptor.\n");
    }
    submultptr =
        fsa_submult(&subwa, &mult, op_store, FALSE, tempfilename, readback);
    if (submultptr == 0)
      exit(1);
    fsa_clear(&mult);
    if (kbm_print_level > 1)
      printf("  #Number of states of submultptr before minimisation = %d.\n",
             submultptr->states->size);
    if (readback) {
      if (fsa_minimize(submultptr) == -1)
        exit(1);
    }
    else {
      if (fsa_ip_minimize(submultptr) == -1)
        exit(1);
    }
    if (kbm_print_level > 1)
      printf("  #Number of states of submultptr after minimisation = %d.\n",
             submultptr->states->size);

    /* As usual, we output and input again, in case we want to change storage
     * types.
     */
    base_prefix(fsaname);
    strcat(fsaname, ".submult");
    sprintf(outf, "%s.%s.submult", gpname, subname);
    wfile = fopen(outf, "w");
    fsa_print(wfile, submultptr, fsaname);
    fclose(wfile);
    fsa_clear(submultptr);

    if ((rfile = fopen(outf, "r")) == 0) {
      fprintf(stderr, "Cannot open file %s.\n", outf);
      exit(1);
    }
    fsa_read(rfile, submultptr, DENSE, 0, 0, TRUE, fsaname);
    fclose(rfile);
    if (kbm_print_level > 1)
      printf("  #Projecting onto left side.\n");
    existsptr = fsa_exists(submultptr, op_store, FALSE, tempfilename);
    if (existsptr == 0)
      exit(1);
    if (kbm_print_level > 1)
      printf(
          "  #Number of states of left-projection before minimisation = %d.\n",
          existsptr->states->size);
    if (fsa_minimize(existsptr) == -1)
      exit(1);
    if (kbm_print_level > 1)
      printf(
          "  #Number of states of left-projection after minimisation = %d.\n",
          existsptr->states->size);
    if (!fsa_equal(&subwa, existsptr)) {
      kbm_buffer[0] = '\0';
      add_to_buffer(
          0, "#Subgroup automaton check (on left) fails for generator:  ");
      add_word_to_buffer(stdout, subgen[i], names);
      printbuffer(stdout);
      tfree(submultptr);
      unlink(outf);
      if (output_bad_words() == -1)
        exit(1);
      exit(2);
    }
    fsa_clear(existsptr);
    tfree(existsptr);

    if (kbm_print_level > 1)
      printf("  #Projecting onto right side.\n");
    if (fsa_swap_coords(submultptr) == -1)
      exit(1);
    existsptr = fsa_exists(submultptr, op_store, TRUE, tempfilename);
    if (existsptr == 0)
      exit(1);
    if (kbm_print_level > 1)
      printf(
          "  #Number of states of right-projection before minimisation = %d.\n",
          existsptr->states->size);
    if (fsa_minimize(existsptr) == -1)
      exit(1);
    if (kbm_print_level > 1)
      printf(
          "  #Number of states of right-projection after minimisation = %d.\n",
          existsptr->states->size);
    if (!fsa_equal(&subwa, existsptr)) {
      kbm_buffer[0] = '\0';
      add_to_buffer(
          0, "#Subgroup automaton check (on right) fails for generator:  ");
      add_word_to_buffer(stdout, subgen[i], names);
      printbuffer(stdout);
      tfree(submultptr);
      unlink(outf);
      if (output_bad_words() == -1)
        exit(1);
      exit(2);
    }
    fsa_clear(existsptr);
    tfree(existsptr);
    tfree(submultptr);
    unlink(outf);

    if (keepfiles) {
      if (gotsuff)
        tfree(suff) else storedmult[++numstoredmult] = suff;
    }
    else {
      sprintf(inf, "%s.m%s", gpname, suff);
      unlink(inf);
      tfree(suff);
    }
  }

  for (i = 0; i < nsubgens; i++)
    tfree(subgen[i]);
  fsa_clear(&subwa);
  tfree(badwords);
  if (keepfiles) {
    for (i = 1; i <= numstoredmult; i++) {
      sprintf(outf, "%s.m%s", gpname, storedmult[i]);
      unlink(outf);
      tfree(storedmult[i]);
    }
    tfree(storedmult);
  }
  if (kbm_print_level > 0)
    printf("#Subgroup automata validity checking succeeded.\n");
  exit(0);
}

/* For a word w in the generators, this function returns a corresponding
 * string with the terms of w replaced by integers separated by '_'.
 * This is used as a suffix in the filenames used for storing the
 * corresponding multiplier fsa's.
 */
char *file_suffix(gen *w)
{
  char *s;
  gen *p;
  boolean first;
  int len;
  /* First work out the length of the required string. */
  len = genstrlen(w);
  p = w - 1;
  while (*(++p) != 0)
    len += int_len((int)(*p));
  tmalloc(s, char, len);
  s[0] = '\0';
  first = TRUE;
  p = w - 1;
  while (*(++p) != 0) {
    if (first)
      first = FALSE;
    else
      sprintf(s + stringlen(s), "_");
    sprintf(s + stringlen(s), "%d", *p);
  }
  return s;
}

/* Calculate the multiplier associated with the word w.
 * s is the suffix of the file in which it will be stored.
 * (s has been derived from w by a call of file_suffix).
 */
int subgen_multiplier(gen *w, char *s)
{
  int i, l;
  gen *wl, *wlt, *wr, *wrt;
  char *suffl, *sufflt, *suffr, *suffrt;
  boolean gotl, gotr, gotlt, gotrt;
  if (kbm_print_level >= 3) {
    kbm_buffer[0] = '\0';
    add_to_buffer(0, "  #Calculating multiplier for word:  ");
    add_word_to_buffer(stdout, w, names);
    printbuffer(stdout);
  }
  l = genstrlen(w);

  if (l == 1) { /* Length 1 - use fsa_makemult */
    strcpy(inf, gpname);
    strcat(inf, ".gm");
    if ((rfile = fopen(inf, "r")) == 0) {
      fprintf(stderr, "Cannot open file %s.\n", inf);
      exit(1);
    }
    fsa_read(rfile, &genmult, op_store, 0, 0, TRUE, fsaname);
    fclose(rfile);
    if (fsa_makemult(&genmult, w[0]) == -1)
      return -1;
    if (fsa_minimize(&genmult) == -1)
      return -1;
    sprintf(outf, "%s.m%s", gpname, s);
    wfile = fopen(outf, "w");
    fsa_print(wfile, &genmult, fsaname);
    fclose(wfile);
    fsa_clear(&genmult);
  }
  else { /* general case - we have to split w up */
    if (l % 2 == 0) {
      tmalloc(wl, gen, l / 2 + 1);
      tmalloc(wr, gen, l / 2 + 1);
      for (i = 0; i < l / 2; i++)
        wl[i] = w[i];
      wl[l / 2] = '\0';
      genstrcpy(wr, w + l / 2);
      suffl = file_suffix(wl);
      suffr = file_suffix(wr);
    }
    else {
      tmalloc(wl, gen, l / 2 + 2);
      tmalloc(wr, gen, l / 2 + 1);
      for (i = 0; i <= l / 2; i++)
        wl[i] = w[i];
      wl[l / 2 + 1] = '\0';
      genstrcpy(wr, w + l / 2 + 1);
      suffl = file_suffix(wl);
      suffr = file_suffix(wr);
    }
    /* See whether we have either of them already */
    gotl = gotr = FALSE;
    if (keepfiles) {
      for (i = 1; i <= numstoredmult; i++) {
        if (strcmp(suffl, storedmult[i]) == 0)
          gotl = TRUE;
        if (strcmp(suffr, storedmult[i]) == 0)
          gotr = TRUE;
      }
    }

    if (keepfiles && l % 2 == 1 && (!gotl || !gotr)) {
      /* In this case, there are two possible ways to split w up -
       * we see if the other way has more multipliers already stored.
       */
      tmalloc(wlt, gen, l / 2 + 1);
      tmalloc(wrt, gen, l / 2 + 2);
      for (i = 0; i < l / 2; i++)
        wlt[i] = w[i];
      wlt[l / 2] = '\0';
      genstrcpy(wrt, w + l / 2);
      sufflt = file_suffix(wlt);
      suffrt = file_suffix(wrt);
      gotlt = gotrt = FALSE;
      for (i = 1; i <= numstoredmult; i++) {
        if (strcmp(sufflt, storedmult[i]) == 0)
          gotlt = TRUE;
        if (strcmp(suffrt, storedmult[i]) == 0)
          gotrt = TRUE;
      }
      if ((gotlt && gotrt) || ((gotlt || gotrt) && !gotl && !gotr)) {
        tfree(wl);
        tfree(wr);
        tfree(suffl);
        tfree(suffr);
        wl = wlt;
        wr = wrt;
        suffl = sufflt;
        suffr = suffrt;
        gotl = gotlt;
        gotr = gotrt;
      }
      else {
        tfree(wlt);
        tfree(wrt);
        tfree(sufflt);
        tfree(suffrt);
      }
    }
    if (!gotl) {
      if (subgen_multiplier(wl, suffl) == -1)
        return -1;
    }
    if (!gotr && genstrcmp(wl, wr) != 0) {
      if (keepfiles) {
        /* Check again to see if we have got it recently */
        for (i = 1; i <= numstoredmult; i++)
          if (strcmp(suffr, storedmult[i]) == 0)
            gotr = TRUE;
      }
      if (!gotr) {
        if (subgen_multiplier(wr, suffr) == -1)
          return -1;
      }
    }
    /* Read back in the two multipliers and form their composite */
    sprintf(inf, "%s.m%s", gpname, suffl);
    if ((rfile = fopen(inf, "r")) == 0) {
      fprintf(stderr, "Cannot open file %s.\n", inf);
      exit(1);
    }
    fsa_read(rfile, &mult1, ip_store, dr, 0, TRUE, fsaname);
    fclose(rfile);
    sprintf(inf, "%s.m%s", gpname, suffr);
    if ((rfile = fopen(inf, "r")) == 0) {
      fprintf(stderr, "Cannot open file %s.\n", inf);
      exit(1);
    }
    fsa_read(rfile, &mult2, ip_store, dr, 0, TRUE, fsaname);
    fclose(rfile);

    compmultptr =
        fsa_composite(&mult1, &mult2, op_store, TRUE, tempfilename, readback);
    if (compmultptr == 0)
      return -1;
    if (readback) {
      if (fsa_minimize(compmultptr) == -1)
        return -1;
    }
    else {
      if (fsa_ip_minimize(compmultptr) == -1)
        return -1;
    }
    sprintf(outf, "%s.m%s", gpname, s);
    wfile = fopen(outf, "w");
    fsa_print(wfile, compmultptr, fsaname);
    fclose(wfile);
    fsa_clear(compmultptr);
    tfree(compmultptr);

    if (keepfiles) {
      if (gotl)
        tfree(suffl) else storedmult[++numstoredmult] = suffl;
      if (gotr)
        tfree(suffr) else storedmult[++numstoredmult] = suffr;
    }
    else {
      sprintf(inf, "%s.m%s", gpname, suffl);
      unlink(inf);
      sprintf(inf, "%s.m%s", gpname, suffr);
      unlink(inf);
      tfree(suffl);
      tfree(suffr);
    }
    tfree(wl);
    tfree(wr);
  }

  return 0;
}

/* Read subgroup generators from rfile (assumed to be already open) */
void read_subgpgens(void)
{
  nsubgens = 0;
  read_ident(rfile, kbm_buffer, &delim, FALSE);
  /* this is the name of the record containing the subgenerators */
  if (delim != ':') {
    fprintf(stderr, "#Input error: file must contain a record assignment\n");
    exit(1);
  }
  check_next_char(rfile, '=');
  read_ident(rfile, kbm_buffer, &delim, FALSE);
  if (delim != '(' || strcmp(kbm_buffer, "rec") != 0) {
    fprintf(stderr, "#Input error: file must contain a record assignment\n");
    exit(1);
  }
  read_ident(rfile, kbm_buffer, &delim, FALSE);
  if (strcmp(kbm_buffer, "subGenerators") != 0) {
    fprintf(stderr, "Input error. 'subGenerators' list expected in subgroup "
                    "generator file.\n");
    exit(1);
  }
  if (delim != ':') {
    fprintf(stderr, "#Input error: bad 'subgens' list assignment\n");
    exit(1);
  }
  check_next_char(rfile, '=');
  check_next_char(rfile, '[');
  nsubgens = 0;
  do {
    if (!read_word(rfile, testword, testword + maxwordlen, &delim, names, ngens,
                   TRUE)) {
      fprintf(stderr,
              "#Input error: no subgroup generators or missing word.\n");
      exit(1);
    }
    if (nsubgens + 1 > maxsubgens) {
      fprintf(stderr, "#Input error: too many subgroup generators.\n");
      exit(1);
    }
    tmalloc(subgen[nsubgens], gen, genstrlen(testword) + 1);
    genstrcpy(subgen[nsubgens], testword);
    nsubgens++;
  } while (delim != ']');
}

/* *existsptr and subwa are unequal. We need to find some words accepted
 * by subwa but not by *existsptr.
 * The function words_and_not will do this.
 * We then output the words, along with the original subgroup generators,
 * so that they can be used in the next run of gpsubwa.
 */
int output_bad_words(void)
{
  int numwords, i;
  tmalloc(badwords, gen *, maxwords) numwords =
      words_and_not(&subwa, existsptr, badwords, maxwords);
  if (numwords == -1)
    return -1;
  if (numwords == 0) {
    fprintf(stderr, "Error: No offending subwords found!\n");
    return -1;
  }
  sprintf(outf, "%s.%s.words", gpname, subname);
  /* We first see if there is already a list of words in the output file.
   * If so, then we want to include them as well in the new output.
   */
  rfile = fopen(outf, "r");
  if (rfile) {
    /* We replace out existing list of subgroup generators with the one in this
     * file
     */
    for (i = 0; i < nsubgens; i++)
      tfree(subgen[i]) read_subgpgens();
    fclose(rfile);
  }
  if (kbm_print_level > 0)
    printf("  #Outputting %d subgroup generators + %d offending words.\n",
           nsubgens, numwords);
  wfile = fopen(outf, "w");
  fprintf(wfile, "_RWS_Sub_words := rec(\n  subGenerators:=[\n");
  /* First write the original subgroup generators */
  for (i = 0; i < nsubgens; i++) {
    kbm_buffer[0] = '\0';
    add_to_buffer(4, "");
    add_word_to_buffer(wfile, subgen[i], names);
    add_to_buffer(0, ",");
    printbuffer(wfile);
    tfree(subgen[i]);
  }
  /* And now the offending words */
  for (i = 0; i < numwords; i++) {
    kbm_buffer[0] = '\0';
    add_to_buffer(4, "");
    add_word_to_buffer(wfile, badwords[i], names);
    if (i != numwords - 1)
      add_to_buffer(0, ",");
    printbuffer(wfile);
    tfree(badwords[i]);
  }
  fprintf(wfile, "  ];\n);\n");
  fclose(wfile);
  fsa_clear(existsptr);
  tfree(existsptr);
  tfree(badwords);
  fsa_clear(&subwa);
  return 0;
}


void badusage(void)
{
  fprintf(
      stderr,
      "Usage: gpchecksubwa [-ip d/s[dr]] [-op d/s] [-silent] [-v] [-l] [-f]\n");
  fprintf(stderr, "\t\t[-m maxwords] groupname [subname].\n");
  exit(1);
}