/**********************************************************************
        Verish.cpp  -  a program for checking logical reasoning
                             version 0.95
                          -------------------
    begin             : circa August 1997
    release date      : 31 January 2013
    copyright         : (C) 1997 - 2013 by Chris Austin
    email             : chris@chrisaustin.info
 **********************************************************************/

/***************************************************************************
 *                                                                         *
 *   This program is free software; you can redistribute it and/or modify  *
 *   it under the terms of the GNU General Public License as published by  *
 *   the Free Software Foundation; either version 2 of the License, or     *
 *   (at your option) any later version.                                   *
 *                                                                         *
 ***************************************************************************/

#ifdef HAVE_CONFIG_H
#include <config.h>
#endif

#include "Verish.h"

using namespace std;

// argc is total number of words in command line
// argv[] is array of pointers to the command line words

int main(const int argc, const char* argv[])
{
  size_t pos;
  string infile = "", requestTit = "";
  string notQnt, buf, Wrd;
  char c;
  bool check_reasoning_flag = false;
  try
  {
    if ( argc == 2 ) check_reasoning_flag = true;
    if ( argc == 3 )
    {
      buf = "";
      pos = 0;
      do
      {
        c = argv[2][pos++];
        if ( ( c >= '!' ) && ( c < 0x7f ) ) buf += c;
      } while (c);
      if (argv[2][0] == '+')
      {
        pos = 1;
        while ( pos < buf.length() )
        {
          c = buf[pos++];
          if ( isCapital(c) ) throw 3;
        }
        requestTit = buf;
        check_reasoning_flag = true;
      }
    }
    if ( check_reasoning_flag )
    {
      buildDev(argv[1], infile);
      chkreas(infile, requestTit);
    }
    else VUtilsMain(argc, argv);
  }
  catch (int e)
  {
    if ( e == 0 ) cout << endl << endl;
    if ( e == 1 ) cout << endl;
    if ( e == 2 ) cout << endl << "Cannot Open " << argv[1] << endl << endl;
    if ( e == 3 ) cout << endl << "Command not recognised" << endl << endl;
  }
  catch (bad_alloc&)
  {
    cout << "Error allocating memory." << endl;
  }
  catch (exception& e)
  {
    cout << "Standard exception: " << e.what() << endl;
  }
  return 0;
}

// the first entry in strts[STSSZ] is 0, and the last entry that is not string::npos is an
// effective start position, for getSent, of the current Paragraph.  Any entries between
// that entry and the first entry are effective start positions of Method Applications
// that have not ended at least one Paragraph before the start of the current Paragraph

void initstrts(size_t strts[STSSZ])
{
  int n = 2;
  strts[0] = strts[1] = 0;
  while ( n < STSSZ ) strts[n++] = string::npos;
}

// return the index of the first occurrence of string::npos in strts[STSSZ]

int nxtstrt(const size_t strts[STSSZ])
{
  int n = 0;
  while ( n < STSSZ )
  {
    if ( strts[n] == string::npos ) break;
    n++;
  }
  if ( n == STSSZ )
  {
    cout << "\nNumber of nested Method Applications is at least " << (STSSZ - 1);
    throw 0;
  }
  return n;
}

void buildDev(const char* flnm, string& infile)
{
  char c;
  ifstream sourcefile;
  bool openflag = false;
  sourcefile.open(flnm, ios::binary);
  if ( sourcefile ) openflag = true;
  else throw 2;
  while (sourcefile.get(c) != 0)
    if (c >= '!' && c <= '~') infile += c;
  cout << endl << "infile.length() = " << infile.length() << endl;
  if ( openflag ) sourcefile.close();
}

// prepare infile and strts[STSSZ] for reasoning checking, starting at the position that is
// initially pos.  Includes the actions at the end of the chkreas loop, without the reas check

void prpflsts(string& infile, size_t strts[STSSZ], const size_t pos)
{
}

// prepare the list of Names.  It contains a - to mark the start of each Method Application

void prpNms(const string infile, const size_t stpos, string& Names)
{
  size_t pos = 0;
  while ( pos < stpos )
  {
    reviseNms(pos, infile, Names);
    nxtPar(infile, pos);
  }
}

// seek last Title occurrence of Tit in infile starting at pos, and set pos to that position if
// found, and otherwise set pos to string::npos

void sklstTit(const string infile, const string Tit, size_t& pos)
{
  size_t savepos, fpos = infile.length();
  seekTit(pos, infile, Tit, fpos);
  savepos = pos;
  while ( pos < fpos )
  {
    savepos = pos;
    seekTit(pos, infile, Tit, fpos);
  }
  pos = savepos;
  if ( pos == fpos ) pos = string::npos;
}

void chkreas(string& infile, const string requestTit)
{
  size_t pos = 0, strts[STSSZ], lpos;
  int n;
  string Sent, Names = "";
  initstrts(strts);
  if ( requestTit != "" )
  {
    sklstTit(infile, requestTit, pos);
    if ( pos == string::npos )
    {
      cout << endl << "Error seeking Title";
      throw 0;
    }
    prpflsts(infile, strts, pos);
    pos = strts[nxtstrt(strts) - 1];
    prpNms(infile, pos, Names);
  }
  do
  {
    pos = strts[nxtstrt(strts) - 1];
    getSent(Sent, pos, infile);
    if ( Sent == "" ) break;
    chkPar(infile, strts, Names);
    pos = strts[nxtstrt(strts) - 1];
    reviseNms(pos, infile, Names);
    if ( ( Sent != "+Df" ) && ( Sent != "+1Df" ) )
    {
      n = (nxtstrt(strts) - 1) - cntMthnfbAo(infile, pos);
      lpos = strts[n];
      infile.erase(lpos, pos - lpos);
      n++;
      while ( n < STSSZ )
      {
        if ( strts[n] == string::npos ) break;
        strts[n++] = string::npos;
      }
      getSent(Sent, lpos, infile);
      pos = lpos;
      getSent(Sent, pos, infile);
      while ( !isReason(Sent) )
      {
        infile.erase(lpos, pos - lpos);
        pos = lpos;
        getSent(Sent, pos, infile);
      }
    }
    n = nxtstrt(strts) - 1;
    lpos = pos = strts[n];
    nxtPar(infile, pos);
    getSent(Sent, lpos, infile);
    if ( isOpnTit(Sent) ) strts[n + 1] = pos;
    else strts[n] = pos;
  } while ( true );
  cout << endl;
}

// return the number of Methods not followed by +Ao in the Paragraph that starts at pos

int cntMthnfbAo(const string infile, const size_t pos)
{
  size_t getpos = pos;
  string Sent, Tit;
  int n = 0;
  getSent(Tit, getpos, infile);
  while ( getpos < infile.length() )
  {
    getSent(Sent, getpos, infile);
    if ( Sent == "" )
    {
      cout << "\nNo Reason found after Title\n\n" << Tit;
      throw 0;
    }
    if ( nmSbjBrf(Sent) < 0 )
    {
      cout << "\nNot a Brief where Brief expected after Title\n\n" << Tit;
      throw 0;
    }
    if ( isReason(Sent) ) break;
    n++;
  }
  if ( Sent == "+Ao" ) n--;
  if ( n < 0 )
  {
    cout << "\nReason +Ao not following Method found while counting Methods";
    throw 0;
  }
  return n;
}

// check the Paragraph for which an effective start position is strts[nxtstrt(strts) - 1]

void chkPar(const string infile, const size_t strts[STSSZ], const string Names)
{
  const int ns = nxtstrt(strts);
  int n1;
  const size_t stpos = strts[ns - 1];
  size_t pos = stpos, stscp[STSSZ];
  string Brf, chkSent, Sbjs[MXSBJ];
  getSent(Brf, pos, infile);
  display(Brf);
  if ( !isNoun(Brf) )
  {
    cout << endl << "Not a Title";
    throw 0;
  }
  if ( ( Brf != "+Df" ) && ( Brf != "+1Df" ) )
  {
    cout << endl << "Title" << endl;
    n1 = cntMthnfbAo(infile, stpos);
    if ( ( n1 == (ns - 2) ) && !isOpnTit(Brf) )
    {
      // this Paragraph is not in a Method Application
      
      initstrts(stscp);
      stscp[2] = strts[2];
      if ( skTitsts(infile, Brf, stscp) != string::npos )
      {
        cout << "\nRepeated Title not in a Method Application";
        throw 0;
      }
    }
    n1 = 0;
    while ( pos < infile.length() )
    {
      getSent(Brf, pos, infile);
      if ( Brf != "" ) display(Brf);
      if ( Brf == "" )
      {
        cout << "\nNo Reason found";
        throw 0;
      }
      if ( nmSbjBrf(Brf) < 0 )
      {
        cout << "\nNot a Brief where Brief expected";
        throw 0;
      }
      if ( isReason(Brf) ) break;
      cout << endl << "Method" << endl;
      n1++;
      if ( n1 == ns )
      {
        cout << "\nNumber of Methods not followed by +Ao exceeds number of Opening Titles by 2";
        throw 0;
      }
    }
    if ( Brf == "+Ao" )
    {
      if ( n1 == 0 ) cout << "\nReason +Ao not preceded by a Method";
      else cout << "\nApplication of preceding Method is omitted";
      throw 0;
    }
    if ( n1 == (ns - 1) )
    {
      cout << "\nNumber of Methods not followed by +Ao exceeded number of Opening Titles";
      throw 0;
    }
    cout << endl << "Reason" << endl;
    getSbjs(Brf, Sbjs);
    TittoFact(infile, Sbjs, strts);
    getSent(chkSent, pos, infile);
    if ( chkSent == "" )
    {
      cout << "\nNo Statement found";
      throw 0;
    }
    display(chkSent);
    pos = strts[(ns - 1) - cntMthnfbAo(infile, stpos)];
    while ( pos < stpos )
    {
      seekDef(pos, infile, stpos);
      if ( pos == stpos ) break;
      if ( hasRelocAb(infile, pos, chkSent) )
      {
        cout << "\nStatement has a Relevant occurrence of a Word Defined by a Definition\n";
        cout << "Paragraph within a Method Application that ended immediately before this\n";
        cout << "Paragraph. The Abbreviation and Definition in that Definition Paragraph are\n";
        getSent(Brf, pos, infile);
        getSent(Brf, pos, infile);
        display(Brf);
        getSent(chkSent, pos, infile);
        display(chkSent);
        throw 1;
      }
      nxtPar(infile, pos);
    }
    if ( isTb(Brf) >= 0 ) chkTb(chkSent, Sbjs);
    try
    {
      if ( isGn(Brf) >= 0 ) chkGn(chkSent, Sbjs, Names);
    }
    catch (int e)
    {
      if ( e == 4 )
      {
        pos = 0;
        putWord(chkSent, pos, Brf);
        Brf[0] = '+';
        pos = seekDfNm(infile, Brf, stpos);
        getSent(Brf, pos, infile);
        getSent(Brf, pos, infile);
        getSent(chkSent, pos, infile);
        cout << "\nThe Adverb Agrees with a Name, in consequence of the Definition";
        cout << "\nParagraph whose Abbreviation is\n";
        display(Brf);
        cout << "\nand whose Definition is\n";
        display(chkSent);
        throw 1;
      }
      throw;
    }
    if ( isSm(Brf) >= 0 ) chkSm(chkSent, Sbjs);
    if ( Brf == "+Ex" ) chkEx(chkSent, Sbjs);
    if ( isFc(Brf) >= 0 ) chkFc(chkSent, Sbjs);
    if ( isAb(Brf) >= 0 ) chkAb(chkSent, Sbjs, infile, stpos);
    if ( Brf == "+Ao" )
    {
      cout << "\nReason used after a Method whose Application is omitted";
      throw 0;
    }
    cout << endl << "Fact" << endl;
  }
  else
  {
    // Definition Paragraph
    
    cout << endl << "Title of Definition Paragraph" << endl;
    getSent(Brf, pos, infile);
    if ( Brf != "" ) display(Brf);
    if ( Brf == "" )
    {
      cout << "\nNo Abbreviation found";
      throw 0;
    }
    if ( nmSbjBrf(Brf) < 0 )
    {
      cout << "\nNot an Abbreviation";
      throw 0;
    }
    cout << endl << "Abbreviation" << endl;
    getSbjs(Brf, Sbjs);
    getSent(chkSent, pos, infile);
    if ( chkSent == "" )
    {
      cout << "\nNo Definition found";
      throw 0;
    }
    display(chkSent);
    chkDef(infile, stpos, Brf, chkSent);
    cout << endl << "Definition" << endl;
  }
}

// if the first Letter at or after getpos is an Initial, set Sent to the first Sentence
// starting at or after getpos, if there is one, with all non-Letters removed, and
// otherwise to the null string. This is where all syntax checking is done. getpos is
// called an effective start position of that Sentence, and is set to an effective start
// position of the next Sentence, if there is one, and otherwise to infile.length()

void getSent(string& Sent, size_t& getpos, const string infile)
{
  char c = ' ', firstchar = ' ', secondchar = ' ';
  bool inSentence = false, goodSentence = false, incomplete = false;
  bool inPhrase = false, needFormative = false, needCapital = false;
  long atstart = 2, endcomment = 0, Scount = 1, Pcount = 1;
  Sent = "";
  while ( ( !goodSentence ) && ( !incomplete ) && ( getpos < infile.length() ) )
  {
    c = ' ';
    while ( !( ( c >= '!' ) && ( c <= '~' ) ) && ( getpos < infile.length() ) )
      c = infile[getpos++];
    if ( ( c >= '!' ) && ( c <= '~' ) )
    {
      if ( atstart == 2 )
      {
        inSentence = inPhrase = needFormative = needCapital = false;
        endcomment = 0;
        firstchar = c;
        
        // provisionally assume it's a Sentence if first Letter is an Initial
        // change mind later if second Letter results in bad grammar
        
        if ( isInitial(c) ) inSentence = true;
        else
        {
          cout << endl << c << endl;
          cout << endl << "Not an Initial";
          throw 0;
        }
        Scount = 1;
        Sent = "";
      }
      if ( inSentence )
      {
        if ( needFormative && isCapital(c) ) incomplete = true;
        if ( needCapital && !isCapital(c) ) incomplete = true;
        needFormative = needCapital = false;
        if (c == '+' || c == '[' || c == ']') needFormative = true;
        if (c == '=' || c == '-' || c == '(' || c == ')' || c == '/')
          needCapital = true;
        if ( ( !inPhrase ) && c == '/') incomplete = true;
        if ( inPhrase && ( Pcount != 0 ) )
        {
          if (c == '=' || c == '-' || c == '(' || c == ')') incomplete = true;
          if (c == '[' || c == ']') incomplete = true;
        }
        if ( inPhrase && ( Pcount == 0 ) && isInitial(c) ) inPhrase = false;
        if ( ( !inPhrase ) && ( c == '+' ) )
        {
          inPhrase = true;
          Pcount = 1;
        }
        if ( inPhrase )
        {
          if (c == '=' || c == '(' || c == ')' || c == '/') Pcount++;
          if (c == '+') Pcount--;
        }
        if ( (Scount == 0 ) && ( !incomplete ) && isInitial(c) ) goodSentence = true;
        if ( ( !goodSentence ) && ( !incomplete ) )
        {
          if (c == '=' || c == '(' || c == ')' || c == '/') Scount++;
          if (c == '+') Scount--;
        }
        if ( ( atstart == 1 ) && incomplete )
        {
          inSentence = incomplete = false;
          secondchar = c;
        }
      }
      if ( ( !inSentence ) && ( atstart == 0 ) )
      {
        if ( endcomment == 1 )
        {
          if ( c == possreverse(firstchar) ) endcomment++;
          else endcomment = 0;
        }
        if ( endcomment == 0 )
          if ( c == possreverse(secondchar) ) endcomment++;
      }
      if ( inSentence && ( !goodSentence ) && ( !incomplete ) ) Sent += c;
      if ( atstart > 0 ) atstart--;
      if ( endcomment == 2 ) atstart = 2;
    }
    else
    {
      if ( atstart == 2 )
      {
        inSentence = false;
        Sent = "";
      }
      if ( inSentence )
      {
        if ( needFormative || needCapital || ( Scount != 0 ) ) incomplete = true;
        else goodSentence = true;
      }
    }
  }
  if ( atstart == 2 ) Sent = "";
  else if ( ( c >= '!' ) && ( c <= '~' ) && ( getpos < infile.length() ) ) getpos--;
  if ( incomplete )
  {
    display(Sent);
    cout << endl << "Incomplete Sentence";
    throw 0;
  }
}

// if getpos is start of a Statement Paragraph, get the Reason into Sent and set getpos to
// start of the Statement if the Reason is found, and otherwise set Sent to ""

void getReason(string& Sent, size_t& getpos, const string infile)
{
  string Tit;
  getSent(Tit, getpos, infile);
  do
  {
    getSent(Sent, getpos, infile);
    if ( Sent == "" ) break;
    if ( nmSbjBrf(Sent) < 0 )
    {
      cout << "Brief not found where Brief expected after Title\n\n" << Tit;
      throw 0;
    }
  } while ( !isReason(Sent) );
}

// if pos is an effective start position of a Paragraph, set pos to an effective start
// position of the next Paragraph if all expected Sentences in the current Paragraph are
// found, and otherwise to string::npos

void nxtPar(const string infile, size_t& pos)
{
  size_t savepos = pos;
  string Sent;
  getSent(Sent, pos, infile);
  if ( ( Sent != "+Df" ) && ( Sent != "+1Df" ) )
  {
    pos = savepos;
    getReason(Sent, pos, infile);
  }
  else getSent(Sent, pos, infile);
  getSent(Sent, pos, infile);
  if ( Sent == "" ) pos = string::npos;
}

// return true if an occurrence of a Noun or Prep starting at pos is an Object occurrence,
// and otherwise false

bool isObjoc(const string Sent, const size_t pos)
{
  size_t getpos = 0, savepos;
  bool flag = false;
  string buf;
  while ( getpos < pos )
  {
    savepos = getpos;
    putWord(Sent, getpos, buf);
    if ( buf[0] == '+' )
      if ( pos < afterScope(Sent, savepos) ) flag = true;
  }
  return flag;
}

// return true if Sent has an Object occurrence of Noun that is not Governed, and otherwise false

bool hasnGovObjoc(const string Noun, const string Sent)
{
  size_t pos = 0, savepos;
  bool flag = false;
  string buf;
  while ( ( pos < Sent.length() ) && !flag )
  {
    savepos = pos;
    putWord(Sent, pos, buf);
    if ( buf == Noun )
      if ( isObjoc(Sent, savepos) && ( !isGovpos(Sent, savepos) ) ) flag = true;
  }
  return flag;
}

//  return true if Sent has an Object occurrence of Preposition Prep, and otherwise false

bool hasObjoc(const string Prep, const string Sent)
{
  size_t pos = 0, savepos;
  bool flag = false;
  string buf;
  while ( ( pos < Sent.length() ) && !flag )
  {
    savepos = pos;
    putWord(Sent, pos, buf);
    if ( buf == Prep )
      if ( isObjoc(Sent, savepos) ) flag = true;
  }
  return flag;
}

// return true if Sent has a Verb occurrence of the Noun or Preposition Wrd, and otherwise false

bool hasVrboc(const string Wrd, const string Sent)
{
  string buf;
  size_t pos1 = 0, pos2;
  bool flag = false;
  while ( pos1 < Sent.length() )
  {
    if (Sent[pos1] == '+')
    {
      pos2 = pos1;
      putWord(Sent, pos2, buf);
      pos1 = afterScope(Sent, pos1);
      if ( buf == Wrd ) flag = 1;
    }
    else pos1++;
  }
  return flag;
}

// return true if Sentence Sent has a Relevant occurrence of the Abbreviation Defined by the
// Definition Paragraph that starts at pos in infile, and false otherwise

bool hasRelocAb(const string infile, const size_t pos, const string Sent)
{
  size_t getpos = pos;
  bool flag = false;
  string Abb, Def, Wrd;
  getSent(Abb, getpos, infile);
  getSent(Abb, getpos, infile);
  if ( Abb == "" )
  {
    cout << "\nAbbreviation not found";
    throw 0;
  }
  getSent(Def, getpos, infile);
  if ( Def == "" )
  {
    cout << "\nDefinition not found";
    throw 0;
  }
  getpos = 0;
  putWord(Abb, getpos, Wrd);
  if ( nmSbjPhrs(Def) >= 0 )
  {
    if ( isNoun(Wrd) )
    {
      if ( hasnGovObjoc(Wrd, Sent) ) flag = true;
    }
    else if ( hasObjoc(Wrd, Sent) ) flag = true;
  }
  if ( hasVrboc(Wrd, Sent) ) flag = true;
  return flag;
}

// return true if Sentence Sent1 is a Subject of Sentence Sent2, and otherwise false

bool isSbj(const string Sent1, const string Sent2)
{
  size_t pos = Sent2.find_first_of("=-()+[]", 1);
  bool flag = false;
  string Subj;
  if ( pos == string::npos ) pos = Sent2.length();
  while ( pos < Sent2.length() )
  {
    getSent(Subj, pos, Sent2);
    if ( Sent1 == Subj ) flag = true;
  }
  return flag;
}

// return -1 if Sent is not a Phrase, and its number of Subjects otherwise

int nmSbjPhrs(const string Sent)
{
  size_t pos = 0;
  int count = -1;
  if ( Sent.length() >= 2 )
  {
    if (Sent[pos++] == '+')
    {
      count++;
      while ( pos < Sent.length() )
      {
        if (Sent[pos] == '/') count++;
        if (Sent[pos++] == '+') break;
      }
    }
  }
  return count;
}

// return -1 if Sent is not a Brief, and the number of /'s otherwise.

int nmSbjBrf(const string Sent)
{
  size_t pos = 0;
  int count = -1;
  bool flag = false;
  if ( Sent.length() >= 2 )
  {
    if (Sent[pos++] == '+')
    {
      count++;
      while ( pos < Sent.length() )
      {
        if (Sent[pos] == '/')
        {
          if ( !flag ) count++;
          else count = -1;
        }
        if (Sent[pos++] == '+') flag = true;
      }
    }
  }
  return count;
}

// return -1 if the Sentence is not a +Tb/.../ Reason, and the number of /'s otherwise

int isTb(const string Sent)
{
  int count = nmSbjBrf(Sent);
  if ( Sent.length() >= 3 )
  {
    if ( Sent.substr(0, 3) != "+Tb" ) count = -1;
    if ( Sent.length() > 3 )
      if ( Sent[3] != '/' ) count = -1;
  }
  else count = -1;
  return count;
}

// return -1 if the Sentence is not a +Gn/ Reason, and 1 otherwise

int isGn(const string Sent)
{
  int count = nmSbjBrf(Sent);
  if (count != 1) count = -1;
  if ( Sent.length() < 4 ) count = -1;
  else if ( Sent.substr(0, 4) != "+Gn/" ) count = -1;
  return count;
}

// return -1 if the Sentence is not a +Sm/ Reason, and 1 otherwise

int isSm(const string Sent)
{
  int count = nmSbjBrf(Sent);
  if (count != 1) count = -1;
  if ( Sent.length() < 4 ) count = -1;
  else if ( Sent.substr(0, 4) != "+Sm/" ) count = -1;
  return count;
}

// return -1 if the Sentence is not a +Fc/ Reason, and 1 otherwise

int isFc(const string Sent)
{
  int count = nmSbjBrf(Sent);
  if (count != 1) count = -1;
  if ( Sent.length() < 4 ) count = -1;
  else if ( Sent.substr(0, 4) != "+Fc/" ) count = -1;
  return count;
}

// return -1 if the Sentence is not a +Ab/ Reason, and 1 otherwise

int isAb(const string Sent)
{
  int count = nmSbjBrf(Sent);
  if (count != 1) count = -1;
  if ( Sent.length() < 4 ) count = -1;
  else if ( Sent.substr(0, 4) != "+Ab/" ) count = -1;
  return count;
}

// return true if Sent is a Reason, otherwise false

bool isReason(const string Sent)
{
  int flag = false;
  if (isTb(Sent) != -1) flag = true;
  if (isGn(Sent) != -1) flag = true;
  if (isSm(Sent) != -1) flag = true;
  if ( Sent == "+Ex" ) flag = true;
  if (isFc(Sent) != -1) flag = true;
  if (isAb(Sent) != -1) flag = true;
  if ( Sent == "+Ao" ) flag = true;
  return flag;
}

// if buf is a Word or a Sentence, return true if buf is a Noun, and otherwise false

bool isNoun(const string buf)
{
  size_t pos = 1;
  bool flag = false;
  if ( buf.length() >= 2 )
  {
    if (buf[0] == '+')
    {
      flag = true;
      while ( pos < buf.length() ) if ( buf[pos++] == '/' ) flag = false;
    }
  }
  return flag;
}

// if Sent is a Noun, return true if Sent is an Opening Title, and otherwise false

bool isOpnTit(const string Sent)
{
  char c;
  bool flag = true;
  if ( Sent[1] != '1' ) flag = false;
  if ( Sent.length() > 2 )
  {
    c = Sent[2];
    if ( ( c >= '0' ) && ( c <= '9' ) ) flag = false;
  }
  return flag;
}

// return true if Noun is a Name, and otherwise false

bool isName(const string Names, const string Noun)
{
  size_t pos = 0;
  bool flag = false;
  string buf;
  while ( pos < Names.length() )
  {
    putWord(Names, pos, buf);
    if ( buf == Noun ) flag = true;
  }
  return flag;
}

// return the first position after the Scope that starts at startpos

size_t afterScope(const string Sent, size_t startpos)
{
  char c;
  int Scount = 1;
  bool flag = true;
  while ( flag )
  {
    c = Sent[startpos];
    if ( ( Scount == 0 ) && isInitial(c) ) flag = false;
    if (c == 0) flag = false;
    if ( flag )
    {
      if (c == '=' || c == '(' || c == ')' || c == '/') Scount++;
      if (c == '+') Scount--;
      startpos++;
    }
  }
  return startpos;
}

// copy Word starting at Sent[pos] into buf, and set pos to first position after Word

void putWord(const string Sent, size_t& pos, string& buf)
{
  char c;
  bool flag = true;
  buf = "";
  if ( pos < Sent.length() ) buf += Sent[pos++];
  while (flag)
  {
    if ( pos < Sent.length() )
    {
      c = Sent[pos];
      flag = !isInitial(c);
    }
    else flag = false;
    if (flag)
    {
      pos++;
      buf += c;
    }
  }
}

// if pos is the start of a Noun, return true if that Noun is Governed, else false

bool isGovpos(const string Sent, const size_t pos)
{
  string Wrd, buf;
  size_t n = pos, m;
  bool flag = false;
  putWord(Sent, n, Wrd);
  n = 0;
  while ( !flag && n < pos )
  {
    if (Sent[n] == '[' || Sent[n] == ']')
    {
      m = n;
      putWord(Sent, m, buf);
      buf[0] = '+';
      if ( ( buf == Wrd )  && ( pos < afterScope(Sent, n) ) ) flag = true;
      n = m;
    }
    else n++;
  }
  return flag;
}

// if pos is the position of a + Capital in Sent, return true if
// that is the start of a Noun, and false otherwise.

bool isNounpos(const string Sent, size_t pos)
{
  char c;
  bool wflag = true, rflag = true;
  pos++;
  while ( wflag && ( pos < Sent.length() ) )
  {
    c = Sent[pos++];
    if (c == '/') rflag = false;
    if ( isInitial(c) ) wflag = false;
  }
  return rflag;
}

// display Sent without endls

void dispNoNdl(const string Sent)
{
  size_t pos = 0;
  char c;
  if ( Sent != "" )
  {
    c = Sent[pos++];
    cout << c;
  }
  while ( pos < Sent.length() )
  {
    c = Sent[pos++];
    if ( isInitial(c) ) cout << " ";
    cout << c;
  }
}

// display Sent with initial and final endl

void display(const string Sent)
{
  cout << endl;
  dispNoNdl(Sent);
  cout << endl;
}

// search for Tit starting at pos and going up to immediately before fpos.  Set pos to 
// start position of Tit if successful, and otherwise to fpos

void seekTit(size_t& pos, const string infile, const string Tit, const size_t fpos)
{
  size_t savepos;
  string Sent;
  while ( pos < fpos )
  {
    savepos = pos;
    getSent(Sent, pos, infile);
    pos = savepos;
    if ( ( Sent == Tit ) || ( Sent == "" ) ) break;
    nxtPar(infile, pos);
    if ( pos == string::npos ) break;
  }
  if ( ( Sent == "" ) || ( pos == string::npos ) ) pos = fpos;
}

// search for first Definition Paragraph starting at pos and going up to immediately before 
// fpos.  Set pos to start position of that Paragraph if successful, and otherwise to fpos

void seekDef(size_t& pos, const string infile, const size_t fpos)
{
  size_t savepos1 = pos, savepos2;
  seekTit(pos, infile, "+Df", fpos);
  savepos2 = pos;
  pos = savepos1;
  seekTit(pos, infile, "+1Df", savepos2);
}

// search for Tit starting at the second last entry in strts[STSSZ] that is not string::npos
// and going up to immediately before the last entry, then if necessary starting at the third 
// from last entry, and so on, and finally if necessary starting at the first entry.  Return
// position of start of Tit if successful, and otherwise string::npos

size_t skTitsts(const string infile, const string Tit, const size_t strts[STSSZ])
{
  size_t pos, fpos;
  int n = nxtstrt(strts) - 2;
  while ( n >= 0 )
  {
    pos = strts[n];
    fpos = strts[n + 1];
    seekTit(pos, infile, Tit, fpos);
    if ( pos < fpos ) break;
    n--;
  }
  if ( n < 0 ) pos = string::npos;
  return pos;
}

// initialize Sbjs[MXSBJ] to null strings, then copy the Subjects of Brief Brf into Sbjs[MXSBJ]

void getSbjs(const string Brf, string Sbjs[MXSBJ])
{
  size_t pos = Brf.find_first_of("+", 1);
  int n1, n2;
  for (n1 = 0; n1 < MXSBJ; n1++) Sbjs[n1].resize(0);
  n2 = nmSbjPhrs(Brf);
  if ( n2 < 0 )
  {
    cout << "\nNot a Phrase";
    throw 0;
  }
  if ( n2 > MXSBJ )
  {
    cout << "\nReason, Method, or Abbreviation has more than " << MXSBJ << " Subjects";
    throw 0;
  }
  n1 = 0;
  while ( n1 < n2 ) getSent(Sbjs[n1++], pos, Brf);
}

// for each entry in Sbjs[MXSBJ] that is a Title that is not +Df or +1Df, as opposed to null,
// search for that Title, and if found, replace that entry in Sbjs[] by the Sentence after the
// next Reason

void TittoFact(const string infile, string Sbjs[MXSBJ], const size_t strts[STSSZ])
{
  size_t pos;
  int n = 0;
  string Tit;
  while ( n < MXSBJ )
  {
    Tit = Sbjs[n];
    if ( Tit == "" ) break;
    if ( ( Tit == "+Df" ) || ( Tit == "+1Df" ) )
    {
      cout << endl << Tit << " is a Title of a Definition Paragraph";
      throw 0;
    }
    pos = skTitsts(infile, Tit, strts);
    if ( pos == string::npos )
    {
      cout << "\nTitle\n\n" << Tit << "\n\nnot found";
      throw 0;
    }
    getReason(Sbjs[n], pos, infile);
    if ( Sbjs[n] == "" )
    {
      cout << "No Reason found after Title\n\n" << Tit;
      throw 0;
    }
    getSent(Sbjs[n], pos, infile);
    if ( Sbjs[n] == "" )
    {
      cout << "No Statement found after Title\n\n" << Tit;
      throw 0;
    }
    n++;
  }
}

// if Sbjs[0] is the Statement referred to by a +Ab/ Reason, then search through Definition
// Paragraphs until the Definition of the Abbreviation by which chkSent differs from
// Sbjs[0] is found, and copy the Abbreviation into Sbjs[1] and the Definition into Sbjs[2].
// Swap chkSent and Sbjs[0] if no suitable Definition Paragraph can be found otherwise

void getDef(const size_t stpos, const string infile, string& chkSent, string Sbjs[MXSBJ])
{
  size_t pos1, pos2, savepos; 
  bool sameflag = true, endflag = false, swapflag = false;
  string buf1, buf2;

  // identify the first Word at which chkSent differs from Sbjs[0]

  pos1 = pos2 = 0;
  while ( sameflag && !endflag )
  {
    if ( ( pos1 >= chkSent.length() ) || ( pos2 >= Sbjs[0].length() ) ) endflag = true;
    else
    {
      putWord(chkSent, pos1, buf1);
      putWord(Sbjs[0], pos2, buf2);
      if ( buf1 != buf2 ) sameflag = false;
    }
  }
  if ( endflag )
  {
    cout << "\nFact\n\nNo substitution made";
    throw 0;
  }
  if ( buf1[0] != '+' )
  {
    if ( buf2[0] == '+' )
    {
      chkSent.swap(Sbjs[0]);
      buf1.swap(buf2);
      swapflag = true;
    }
    else
    {
      cout << "\nThe earlier Statement differs from this Statement before the start of the";
      cout << "\nfirst Phrase of either Statement";
      throw 0;
    }
  }
  
  while ( true )
  {

    // seek the Definition Paragraph that Defines the Abbreviation in buf1

    savepos = pos1 = 0;
    while ( pos1 < stpos )
    {
      seekDef(pos1, infile, stpos);
      savepos = pos1;
      if ( pos1 < stpos )
      {
        getSent(Sbjs[1], pos1, infile);
        getSent(Sbjs[1], pos1, infile);
        getSent(Sbjs[2], pos1, infile);
        pos2 = 0;
        putWord(Sbjs[1], pos2, buf2);
        if ( buf1 == buf2 )
        {
          if ( nmSbjBrf(Sbjs[1]) != -1 ) break;
          else
          {
            cout << "\nErroneous Definition Paragraph found.  Its Abbreviation is\n\n";
            cout << Sbjs[1];
            throw 0;
          }
        }
      }
    }
    if ( savepos != stpos ) break;
    if ( ( swapflag ) || ( buf2[0] != '+' ) )
    {
      cout << "\nNo Definition of the Abbreviation found";
      throw 0;
    }
    chkSent.swap(Sbjs[0]);
    buf1.swap(buf2);
    swapflag = true;
  }
}

// return the Sentence obtained from Defn by replacing each unGoverned Noun occurrence
// in Defn, of any Word in DefSbjs, by the corresponding Phrase in DfSbjReps

string buildsubsDefn(string Defn, const string DefSbjs[MXSBJ], const string DfSbjReps[MXSBJ])
{
  string buildbuf, tempbuf;
  size_t n = 0, afterPhrase, newpos, aftr;
  int i;
  buildbuf = "";
  while ( n < Defn.length() )
  {
    afterPhrase = afterScope(Defn, n);
    putWord(Defn, n, tempbuf);
    buildbuf += tempbuf;
    if (tempbuf[0] == '+')
    while ( n < afterPhrase )
    {
      newpos = n;
      putWord(Defn, newpos, tempbuf);
      if (isNounpos(Defn, n))
        if (!isGovpos(Defn, n))
        {
          aftr = 0;
          for (i = 0; ( i < MXSBJ ) && ( aftr == 0 ); i++)
            if ( DefSbjs[i] == tempbuf )
              getSent(tempbuf, aftr, DfSbjReps[i]);
        }
      buildbuf += tempbuf;
      n = newpos;
    }
  }
  return buildbuf;
}

// check whether chkSent can be obtained from Sbjs[0] by precisely one
// +Ab/ application of the Definition contained in Sbjs[1] and Sbjs[2]

void chkAb(string chkSent, string Sbjs[MXSBJ], const string infile, const size_t stpos)
{
  size_t pos1 = 0, pos2 = 0, savepos;
  int n;
  string buf1, buf2;
  bool flag = true, swapflag = false;
  string Abbrv, Phrs, DefSbjs[MXSBJ], DfSbjReps[MXSBJ];
  while ( true )
  {
    buf1 = chkSent;
    getDef(stpos, infile, chkSent, Sbjs);        // will not return if chkSent == Sbjs[0]
    if ( buf1 != chkSent ) swapflag = true;
    while ( flag && ( pos1 < Sbjs[0].length() ) && ( pos2 < chkSent.length() ) )
    {
      savepos = pos1;
      putWord(Sbjs[0], pos1, buf1);
      putWord(chkSent, pos2, buf2);
      if ( buf1 != buf2 ) flag = false;
    }
    Abbrv = Sbjs[1];
    // copy the Subjects of the Abbreviation in the Definition Paragraph into DefSbjs
    getSbjs(Sbjs[1], DefSbjs);
    pos2 = savepos;
    // copy the Abbreviation Phrase in chkSent into Sbjs[1]
    getSent(Sbjs[1], pos2, chkSent);
    Phrs = Sbjs[1];
    // copy the Subjects of the Abbreviation Phrase in chkSent into DfSbjReps
    getSbjs(Sbjs[1], DfSbjReps);
    Sbjs[1] = buildsubsDefn(Sbjs[2], DefSbjs, DfSbjReps);
    pos1 = savepos;
    getSent(buf1, pos1, Sbjs[0]);
    if ( Sbjs[1] != buf1 )
    {
      if ( swapflag )
      {
        cout << "\nInvalid substitution";
        throw 0;
      }
      chkSent.swap(Sbjs[0]);
      swapflag = true;
      continue;
    }
    flag = true;
    if ( ( pos1 < Sbjs[0].length() ) && ( pos2 == chkSent.length() ) ) flag = false;
    if ( ( pos1 == Sbjs[0].length() ) && ( pos2 < chkSent.length() ) ) flag = false;
    if ( ( pos1 < Sbjs[0].length() ) && ( pos2 < chkSent.length() ) )
      if ( Sbjs[0].substr(pos1) != chkSent.substr(pos2) ) flag = false;
    if ( !flag )
    {
      cout << "\nSentence altered after the Abbreviation";
      throw 0;
    }
    n = 0;
    while ( n < MXSBJ )
    {
      if ( DefSbjs[n] != "" )
      {
        if ( !nGovforPhrs(Sbjs[2], DefSbjs[n], DfSbjReps[n]) )
        {
          cout << "\nThe formation of the Sentence\n";
          display(Sbjs[1]);
          cout << "\nfrom the Phrase\n\n";
          dispNoNdl(Phrs);
          cout << ",\n\nin Accordance with the Definition\n";
          display(Sbjs[2]);
          cout << "\nof the Abbreviation\n\n";
          dispNoNdl(Abbrv);
          cout << ",\n\nis not Legitimate, because in the Definition, there is an ";
          cout << "Object occurrence\nof the Noun\n";
          display(DefSbjs[n]);
          cout << "\nthat is not Governed, and lies within the Scope of an Adverb ";
          cout << "that Agrees with\na Noun in the Phrase\n";
          display(DfSbjReps[n]);
          throw 1;
        }
      }
      n++;
    }
    break;
  }
}

// if pos is an effective start of a Statement Paragraph that contains Methods, remove the
// last - and what follows it from the end of Names, as many times as there are Methods not
// followed by +Ao in that Paragraph. Then if the Title at or after pos is an Opening Title,
// add - to Names. Then if pos is an effective start of a Definition Paragraph, add each
// Name created by that Definition Paragraph to Names, if it is not already present

void reviseNms(const size_t pos, const string infile, string& Names)
{
  size_t getpos = pos, newpos, afterPhrase;
  bool flag;
  int n;
  string Wrd, Abb, Def, Sbjs[MXSBJ];
  getSent(Wrd, getpos, infile);
  if ( ( Wrd != "+Df" ) && ( Wrd != "+1Df" ) )
  {
    n = cntMthnfbAo(infile, pos);
    while ( n > 0 )
    {
      newpos = Names.rfind("-");
      Names.resize(newpos);
      n--;
    }
  }
  if ( isOpnTit(Wrd) ) Names += "-";
  if ( ( Wrd == "+Df" ) || ( Wrd == "+1Df" ) )
  {
    getSent(Abb, getpos, infile);
    if ( Abb == "" )
    {
      cout << "\nAbbreviation not found";
      throw 0;
    }
    getSent(Def, getpos, infile);
    if ( Def == "" )
    {
      cout << "\nDefinition not found";
      throw 0;
    }
    if ( isNoun(Abb) )
      if ( !isName(Names, Abb) ) Names += Abb;
    getSbjs(Abb, Sbjs);
    getpos = 0;
    while ( getpos < Def.length() )
    {
      getpos = Def.find_first_of("+", getpos);
      afterPhrase = afterScope(Def, getpos);
      putWord(Def, getpos, Wrd);
      while ( getpos < afterPhrase )
      {
        newpos = getpos;
        putWord(Def, newpos, Wrd);
        if (isNounpos(Def, getpos))
          if (!isGovpos(Def, getpos))
          {
            flag = true;
            for (n = 0; n < MXSBJ; n++) if ( Sbjs[n] == Wrd ) flag = false;
            if ( flag && !isName(Names, Wrd) ) Names += Wrd;
          }
        getpos = newpos;
      }
    }
  }
}

// if Abb has one or more Subjects, check they are all different.  And if stpos is an
// effective start position of a Definition Paragraph, whose Abbreviation and Definition
// are Abb and Def, check the 2nd, 3rd, and 4th requirements for a Regular Development

void chkDef(const string infile, const size_t stpos, const string Abb, const string Def)
{
  size_t pos = 0, getpos = 0;
  int n1, n2;
  bool flag = false;
  string Sbjs[MXSBJ], Wrd1, Wrd2, Brf, prvDf;
  getSbjs(Abb, Sbjs);
  for(n1 = 1; n1 < MXSBJ; n1++)
  {
    if ( Sbjs[n1] == "" ) break;
    for (n2 = 0; n2 < n1 ; n2++)
      if ( Sbjs[n2] == Sbjs[n1] )
      {
        cout << "\nSubjects of Abbreviation are not all different";
        throw 0;
      }
  }
  if ( isNoun(Def) )
  {
    display(Def);
    cout << "\nDefinition is a Noun";
    throw 0;
  }
  if ( hasRelocAb(infile, stpos, Def) )
  {
    display(Def);
    cout << "\nWord being Defined has a Relevant occurrence in its Definition";
    throw 0;
  }
  putWord(Abb, pos, Wrd1);
  while ( getpos < stpos )
  {
    seekDef(getpos, infile, stpos);
    if ( getpos == stpos ) break;
    getSent(Brf, getpos, infile);
    getSent(Brf, getpos, infile);
    if ( Brf == "" )
    {
      cout << "\nAn earlier Definition Paragraph is missing its Abbreviation";
      throw 0;
    }
    getSent(prvDf, getpos, infile);
    if ( prvDf == "" )
    {
      cout << "\nAn earlier Definition Paragraph is missing its Definition";
      throw 0;
    }
    pos = 0;
    putWord(Brf, pos, Wrd2);
    if ( Wrd1 == Wrd2 )
    {
      cout << "\nThe Word being Defined was Defined by an earlier Definition Paragraph\n";
      cout << "\nThe Abbreviation and Definition in that earlier Definition Paragraph are\n";
      display(Brf);
      display(prvDf);
      throw 1;
    }
    n1 = nmSbjBrf(Brf);
    if ( n1 < 0 )
    {
      cout << "\nThe second Sentence of an earlier Definition Paragraph is not a Brief";
      throw 0;
    }
    if ( n1 > MXSBJ )
    {
      cout << "\nThe Abbreviation in an earlier Definition Paragraph has more than ";
      cout << MXSBJ << " Subjects";
      throw 0;
    }
    getSbjs(Brf, Sbjs);
    if ( nmSbjPhrs(Def) >= 0 )
    {
      if ( isNoun(Wrd1) )
      {
        if ( hasnGovObjoc(Wrd1, prvDf) )
        {
          flag = true;
          for (n1 = 0; n1 < MXSBJ; n1++) if ( Sbjs[n1] == Wrd1 ) flag = false;
        }
      }
      else if ( hasObjoc(Wrd1, prvDf) ) flag = true;
    }
    if ( hasVrboc(Wrd1, prvDf) ) flag = true;
    if ( flag )
    {
      display(Def);
      if ( isNoun(Wrd1) )
      {
        cout << "\nThe Noun being Defined has a Relevant occurrence in the Definition of an";
        cout << "\nearlier Definition Paragraph, such that either the Noun being Defined is";
        cout << "\nnot a Subject of the Abbreviation of that earlier Definition Paragraph, or";
        cout << "\nthe Relevant occurrence is a Verb occurrence\n";
      }
      else
      {
        cout << "\nThe Preposition being Defined has a Relevant occurrence in the Definition";
        cout << "\nof an earlier Definition Paragraph\n";
      }
      cout << "\nThe Abbreviation and Definition in that earlier Definition Paragraph are\n";
      display(Brf);
      display(prvDf);
      throw 1;
    }
  }
}

// if Nm is a Name, return the start position of the first Definition Paragraph such that
// either the Abbreviation is Nm and the Definition is a Phrase, or Nm has an Object
// occurrence in the Definition that is not Governed, but is not a Subject of the Abbreviation

size_t seekDfNm(const string infile, const string Nm, const size_t stpos)
{
  size_t pos = 0, savepos = 0;
  string Brf, Def, Sbjs[MXSBJ];
  int n;
  bool flag = false;
  while ( pos < stpos )
  {
    seekDef(pos, infile, stpos);
    savepos = pos;
    getSent(Brf, pos, infile);
    getSent(Brf, pos, infile);
    getSent(Def, pos, infile);
    if ( ( Brf == Nm ) && ( nmSbjPhrs(Def) >= 0 ) ) break;
    getSbjs(Brf, Sbjs);
    for (n = 0; n < MXSBJ; n++) if ( Sbjs[n] == Nm ) flag = true;
    if ( !flag && hasnGovObjoc(Nm, Def) ) break;
  }
  return savepos;
}

// get the distinct Clauses in Sent into Cls[], if they are not already there

void oneSentgetCls(string Sent, string Cls[MXCLS])
{
  size_t pos = 0;
  string buf;
  int i;
  bool sflag, nflag;
  while ( pos < Sent.length() )
  {
    pos = Sent.find_first_of("+[]", pos);
    getSent(buf, pos, Sent);
    nflag = sflag = false;
    i = 0;
    while ( ( !nflag ) && ( !sflag ) && ( i < MXCLS ) )
    {
      if ( Cls[i] == buf ) sflag = true;
      if ( Cls[i] == "" ) nflag = true;
      else i++;
    }
    if ( !sflag )
    {
      if ( nflag ) Cls[i] = buf;
      else
      {
        cout << "\nMore than " << MXCLS << " distinct Clauses";
        throw 0;
      }
    }
  }
}

// get the distinct Clauses in chkSent, and in the Sentences in Sbjs[], into Cls[]

void getClauses(string chkSent, string Sbjs[MXSBJ], string Cls[MXCLS])
{
  int i;
  oneSentgetCls(chkSent, Cls);
  for (i = 0; i < MXSBJ; i++)
    if ( Sbjs[i] != "" ) oneSentgetCls(Sbjs[i], Cls);
}

// get the Clause summary of srcSent into Clsform[]. Each Clause is represented by
// the index of that Clause in Cls[], = is represented by -4, - by -5, ( by -6,
// and ) by -7, and the first position after the end by -1.

void makeClsform(string srcSent, string Cls[MXCLS], int Clsform[CLSSZ])
{
  size_t pos = 0;
  char c;
  string buf;
  int n = 0, Clfrm = -1;
  while ( pos < srcSent.length() )
  {
    c = srcSent[pos];
    if (c == '=') Clfrm = -4;
    if (c == '-') Clfrm = -5;
    if (c == '(') Clfrm = -6;
    if (c == ')') Clfrm = -7;
    if (c == '+' || c == '[' || c == ']')
    {
      getSent(buf, pos, srcSent);
      Clfrm = 0;
      while ( Clfrm < MXCLS )
      {
        if ( Cls[Clfrm] == buf ) break;
        Clfrm++;
      }
    }
    else pos++;
    Clsform[n++] = Clfrm;
    if ( n == CLSSZ )
    {
      cout << "\nLength of Clause form will exceed " << CLSSZ;
      throw 0;
    }
  }
  Clsform[n] = -1;
}

// for each entry i >= 0 in Clsform[], from the beginning until -1 is found,
// this function replaces i by TFvals[i]. Negative entries are unchanged.

void subsTFvals(int Clsform[CLSSZ], int TFvals[MXCLS])
{
  int m = 0;
  while (Clsform[m] != -1)
  {
    if (Clsform[m] >= 0 && Clsform[m] < MXCLS)
    Clsform[m] = TFvals[Clsform[m]];
    m++;
  }
}

// for each non-null Clause in Cls[], the corresponding entry in TFvals[] is
// initialised to 1, representing True, and any remaining entries are
// initialised to 2.

void initTFvals(string Cls[MXCLS], int TFvals[MXCLS])
{
  int i = 0;
  while (i < MXCLS)
  {
    if ( Cls[i] != "" ) TFvals[i] = 1;
    else TFvals[i] = 2;
    i++;
  }
}

// if there are any 1 entries in TFvals[], then the first 1 entry is set to
// 0, all the 0 entries before that are set to 1, and 1 is returned, while if
// there are no 1 entries, then 0 is returned.

int newTFvals(int TFvals[MXCLS])
{
  int i = 0, j = 0, flag = 0;
  while (!flag && i < MXCLS)
  {
    if (TFvals[i] == 1)
    {
      TFvals[i] = 0;
      flag = 1;
    }
    else i++;
  }
  if (flag)
  while (j < i)
  {
    if (TFvals[j] == 0) TFvals[j] = 1;
    j++;
  }
  return flag;
}

// if Clsform[] contains the result of substituting the current Truth values of the
// Clauses, for the corresponding Clause numbers in the Clause summary of a Sentence,
// then return the truth value of that Sentence for the current Truth values of the
// Clauses. The entries in Clsform[] initially consist of -4, -5, -6, and -7, coding
// for =, -, (, and ) respectively, 1, coding for True, 0, coding for False, and
// finally a -1 to indicate the first position after the end. When a 1 or 0 is "used",
// it is replaced by -2, and when a -4, -5, -6, or -7 is "evaluated", it is replaced
// by 1 or 0 as appropriate. An evaluation step consists of starting from the
// beginning of Clsform[], finding the first coded Sign such that sufficient 0's or
// 1's to serve as its Subjects are found before any further coded Sign occurs,
// evaluating that coded Sign and replacing it by 0 or 1 as appropriate, and
// replacing its Subjects by -2. This step is repeated until Clsform[0] is evaluated,
// and then Clsform[0] is returned

int evalClsform(int Clsform[CLSSZ])
{
  int flag, s, x, y = 1; // initializations of y and k are not used, they are to avoid
  int i; // index of Sign                                            compiler warnings
  int j; // index of first Subject
  int k = 0; // index of second Subject
  do
  {
    i = 0;
    do
    {
      s = Clsform[i];
      flag = 0;
      j = i + 1;
      if (Clsform[j] <= -4) flag = 1;
      if (flag == 0 && s != -5)
      {
        k = j + 1;
        while (Clsform[k] == -2) k++;
        if (Clsform[k] <= -4) flag = 1;
      }
      if (flag == 1)
      {
        do i++;
        while (Clsform[i] > -4);
      }
    } while (flag);
    x = Clsform[j];
    if (s != -5) y = Clsform[k];
    if (s == -4) Clsform[i] = x * y + (1 - x) * (1 - y); // equivalence
    if (s == -5) Clsform[i] = 1 - x; // not
    if (s == -6) Clsform[i] = x * y; // and
    if (s == -7) Clsform[i] = 1 - (1 - x) * (1 - y); // or
    Clsform[j] = -2;
    if (s != -5) Clsform[k] = -2;
  } while (i != 0);
  return Clsform[0];
}

// for each independent assignment of truth values to the distinct Clauses in chkSent,
// and in the Sentences in Sbjs[], the truth value of each Sentence in Sbjs[] is
// calculated. If all of these evaluate as true, then the truth value of chkSent is
// evaluated for that assignment of truth values to the Clauses. The function returns if
// the truth value of chkSent is true for each such assignment of truth values to the
// Clauses, while if the truth value of chkSent is found to be false for some such
// assignment of truth values to the Clauses, the function displays those truth values
// of the Clauses then throws an exception

void chkTb(string chkSent, string Sbjs[MXSBJ])
{
  string Cls[MXCLS];
  int TFvals[MXCLS];
  int i, tflag, Clsform[CLSSZ], numCls = 0;
  int wflag = 1;
  
  // the following 22 lines of code are a work-around for a seg fault that sometimes
  // occurred at a random point during the execution of makeClsform(...), when there
  // were about 10 or more Clauses, and the first of the previous Statements had only
  // one Clause, for example +sm// +a +a
  
  int n1, n2, n3, n4;
  for ( i = 0, n1 = 0; i < MXSBJ; i++) if ( Sbjs[i] != "" ) n1++;
  if ( n1 > 1 )
  {
    i = n1 = n2 = 0;
    while ( i < MXSBJ )
    {
      if ( Sbjs[i] != "" )
      {
        for (n3 = 0; n3 < MXCLS; n3++) Cls[n3].resize(0);
        oneSentgetCls(Sbjs[i], Cls);
        for ( n3 = 0, n4 = 0; n3 < MXCLS; n3++) if ( Cls[n3] != "" ) n4++;
        if ( n4 > n2 )
        {
          n2 = n4;
          n1 = i;
        }
      }
      i++;
    }
    if ( n1 != 0 ) Sbjs[0].swap(Sbjs[n1]);
  }
  
  for (i = 0; i < MXCLS; i++) Cls[i].resize(0);
  getClauses(chkSent, Sbjs, Cls);
  for (i = 0; i < MXCLS; i++) if ( Cls[i] != "" ) numCls++;
  if ( numCls >= WNCLS )
  {
    cout << "\nThere are " << numCls << " distinct Clauses.\n";
    cout << "\nThe time required to check a use of Tabulate approximately doubles with each\n";
    cout << "extra distinct Clause\n";
  }
  initTFvals(Cls, TFvals);
  while ( wflag )
  {
    i = 0;
    tflag = 1;
    while (tflag && i < MXSBJ)
    {
      if ( Sbjs[i] != "" )
      {
        makeClsform(Sbjs[i], Cls, Clsform);
        subsTFvals(Clsform, TFvals);
        tflag = evalClsform(Clsform);
      }
      i++;
    }
    if (tflag)
    {
      makeClsform(chkSent, Cls, Clsform);
      subsTFvals(Clsform, TFvals);
      tflag = evalClsform(Clsform);
      if ( !tflag )
      {
        cout << "\nThis Sentence is False, while all the Facts referred to in the Reason ";
        cout << "\nare True, when the truth values of the Clauses are as follows:";
        for(i = 0;i < MXCLS;i++)
          if ( Cls[i] != "" )
          {
            cout << "\n";
            display(Cls[i]);
            if ( TFvals[i] ) cout << "\ntrue";
            else cout << "\nfalse";
          }
        throw 0;
      }
    }
    wflag = newTFvals(TFvals);
  }
}

// check chkSent is equal to Sbjs[0], preceded by an Adverb that starts with [. Check no Name 
// Agrees with the first Adverb in chkSent

void chkGn(const string chkSent, const string Sbjs[MXSBJ], const string Names)
{
  size_t pos = 0;
  string buf, temp;
  if (chkSent[0] != '[')
  {
    cout << "\nStatement does not begin with [";
    throw 0;
  }
  putWord(chkSent, pos, buf);
  buf[0] = '+';
  if ( isName(Names, buf) ) throw 4;
  buf[0] = '[';
  buf += Sbjs[0];
  if ( buf != chkSent )
  {
    cout << "\nSentence after the Adverb differs from the earlier Sentence";
    throw 0;
  }
}

// check that chkSent and Sbjs[0] are related by replacing exactly one sequence of the
// form - A - in one of them, where A is an Adverb that starts with [, by the Adverb
// obtained from A by replacing its initial [ by ], in the other of them

void chkSm(string chkSent, string Sbjs[MXSBJ])
{
  size_t pos1 = 0, pos2 = 0, savepos;
  string buf1, buf2;
  bool flag = true;
  while ( flag && ( pos1 < Sbjs[0].length() ) && ( pos2 < chkSent.length() ) )
  {
    putWord(Sbjs[0], pos1, buf1);
    putWord(chkSent, pos2, buf2);
    flag = ( buf1 == buf2 );
  }
  if ( flag )
  {
    cout << "\nFact\n\nNo substitution made";
    throw 0;
  }
  if ( buf1 != "-")
  {
    if (buf2 != "-" )
    {
      cout << "\nThe first Word where the Statements differ is not - in either case";
      throw 0;
    }
    else
    {
      chkSent.swap(Sbjs[0]);
      buf2.swap(buf1);
      savepos = pos1;
      pos1 = pos2;
      pos2 = savepos;
    }
  }
  if ( buf2[0] != ']' )
  {
    cout << "\nThe first Letter where the Statements differ is not ] in either case";
    throw 0;
  }
  // Sbjs[0] has another Word, because Sbjs[0] is a Sentence
  putWord(Sbjs[0], pos1, buf1);
  if ( buf1[0] != '[' )
  {
    cout << "\nThe first Letter after the first - where the Statements differ is not [";
    throw 0;
  }
  buf1[0] = ']';
  if ( buf1 != buf2 )
  {
    cout << "\nThe [ Adverb and the ] Adverb differ after their first Letters";
    throw 0;
  }
  putWord(Sbjs[0], pos1, buf1);
  if ( buf1 != "-" )
  {
    cout << "\nThe first Word after the replaced or substituted [ Adverb is not -";
    throw 0;
  }
  flag = true;
  if ( ( pos1 < Sbjs[0].length() ) && ( pos2 == chkSent.length() ) ) flag = false;
  if ( ( pos1 == Sbjs[0].length() ) && ( pos2 < chkSent.length() ) ) flag = false;
  if ( ( pos1 < Sbjs[0].length() ) && ( pos2 < chkSent.length() ) )
    if ( Sbjs[0].substr(pos1) != chkSent.substr(pos2) ) flag = false;
  if ( !flag )
  {
    cout << "\nSentence altered after the Some substitution";
    throw 0;
  }
}

// return true if no Object occurrence of Noun1 in chkSent, that is not Governed, occurs
// within the Scope of an Adverb that Agrees with Noun2, and otherwise false

bool nGovforNoun(string chkSent, string Noun1, string Noun2)
{
  size_t pos1 = 0, newpos, pos2, afterPhrase, aftScpAdv;
  string buf;
  bool flag = true;
  while ( flag && ( pos1 < chkSent.length() ) )
  {
    afterPhrase = afterScope(chkSent, pos1);
    putWord(chkSent, pos1, buf);
    if ( buf[0] == '+' )
      while ( flag && ( pos1 < afterPhrase ) )
      {
        newpos = pos1;
        putWord(chkSent, newpos, buf);
        if ( buf == Noun1 )
          if ( !isGovpos(chkSent, pos1) )
          {
            pos2 = 0;
            while ( flag && ( pos2 < pos1 ) )
            {
              aftScpAdv = afterScope(chkSent, pos2);
              putWord(chkSent, pos2, buf);
              if (buf[0] == '[' || buf[0] == ']')
              {
                buf[0] = '+';
                if ( ( buf == Noun2 ) && ( pos1 < aftScpAdv ) ) flag = false;
              }
            }
          }
        pos1 = newpos;
      }
  }
  return flag;
}

// return true if no Object occurrence of Noun1 in chkSent, that is not Governed, occurs
// within the Scope of any Adverb that Agrees with a Noun in Phrase, and otherwise false

bool nGovforPhrs(const string chkSent, const string Noun1, const string Phrase)
{
  size_t pos = 0;
  bool flag = true;
  string Wrd;
  while ( pos < Phrase.length() )
  {
    putWord(Phrase, pos, Wrd);
    if ( isNoun(Wrd) )
      if ( !nGovforNoun(chkSent, Noun1, Wrd) ) flag = false;
  }
  return flag;
}

// check that chkSent has the form ) - A B C, where A is an Adverb that begins with [,
// B is a Sentence, and C is obtained from B by replacing every Object occurrence that
// is not Governed, of the Noun that Agrees with A, by a Phrase D, such that no Noun in
// D becomes Governed, when D replaces an occurrence in B of the Noun that Agrees with A

void chkEx(string chkSent, string Sbjs[MXSBJ])
{
  string Noun, Sent;
  size_t pos1 = 2, pos2 = 0, savepos;
  int n;
  string buf1, buf2;
  bool flag = true;
  string DefSbjs[MXSBJ], DfSbjReps[MXSBJ];
  for (n = 0; n < MXSBJ; n++) DefSbjs[n].resize(0);
  for (n = 0; n < MXSBJ; n++) DfSbjReps[n].resize(0);
  if ( chkSent.length() < 4 )
  {
    cout << "\nNot a Fact of type +Ex";
    throw 0;
  }
  if ( ( chkSent[0] != ')' ) || ( chkSent[1] != '-' ) || ( chkSent[2] != '[' ) )
  {
    cout << "\nNot a Fact of type +Ex";
    throw 0;
  }
  putWord(chkSent, pos1, Noun);
  Noun[0] = '+';
  getSent(Sbjs[0], pos1, chkSent);
  getSent(Sent, pos1, chkSent);
  pos1 = 0;
  while ( flag && ( pos1 < Sent.length() ) && ( pos2 < Sbjs[0].length() ) )
  {
    savepos = pos1;
    putWord(Sent, pos1, buf1);
    putWord(Sbjs[0], pos2, buf2);
    flag = ( buf1 == buf2 );
  }
  if (!flag)
  {
    if ( buf2 != Noun )
    {
      Noun[0] = '[';
      cout << "\nThe first Word in the Subject of\n\n" << Noun << endl << endl;
      Noun[0] = '+';
      cout << "that is replaced is not\n\n" << Noun;
      throw 0;
    }
    if ( ( !isObjoc(Sbjs[0], savepos) ) || isGovpos(Sbjs[0], savepos) )
    {
      cout << "\nThe first occurrence of\n\n" << Noun << endl << endl;
      Noun[0] = '[';
      cout << "in the Subject of\n\n" << Noun << endl << endl;
      cout << "that is replaced is not an Object occurrence that is not Governed";
      throw 0;
    }
    Sbjs[1] = buf2;
    DefSbjs[0] = buf2;
    pos1 = savepos;
    getSent(buf1, pos1, Sent);
    Sbjs[2] = buf1;
    DfSbjReps[0] = buf1;
    Sbjs[3] = buildsubsDefn(Sbjs[0], DefSbjs, DfSbjReps);
    if ( Sbjs[3] == "" )
    {
      Noun[0] = '[';
      cout << "\nFailed to build Subject of\n\n" << Noun;
      cout << "\n\nwith the appropriate substitutions";
      throw 0;
    }
    if ( !( Sent == Sbjs[3] ) )
    {
      cout << "\nInvalid substitution";
      throw 0;
    }
    // if this stage is reached, Sbjs[2] is a Phrase
    if ( !nGovforPhrs(Sbjs[0], Sbjs[1], Sbjs[2]) )
    {
      Sbjs[1].replace(0, 1, "[");
      cout << "\nIn the Subject of the Adverb\n\n"<< Sbjs[1];
      cout << ",\n\nthere is an Object occurrence of the Noun that Agrees with ";
      cout << "that Adverb, that is\nnot Governed within the Subject, and lies within";
      cout << " the Scope of an Adverb in the\n";
      cout << "Subject that Agrees with a Noun in the Phrase\n\n";
      cout << Sbjs[2];
      throw 0;
    }
  }
}

// check that chkSent has the form ) B A C, and Sbjs[0] has the form A ) B C, where A is
// an Adverb that begins with [, and B and C are Sentences such that the Noun that Agrees
// with A has no Object occurrence in B that is not Governed

void chkFc(const string chkSent, const string Sbjs[MXSBJ])
{
  size_t pos = 0;
  string Wrd, SbjB, SbjC, buf;
  putWord(chkSent, pos, buf);
  if ( buf != ")" )
  {
    cout << "\nThe first Word of the Statement is not )";
    throw 0;
  }
  getSent(SbjB, pos, chkSent);
  putWord(chkSent, pos, Wrd);
  if ( Wrd[0] != '[' )
  {
    cout << "\nThe first Letter of the second Subject of the first ) is not [";
    throw 0;
  }
  getSent(SbjC, pos, chkSent);
  pos = 0;
  putWord(Sbjs[0], pos, buf);
  if ( buf != Wrd )
  {
    cout << "\nThe first Word of the earlier Statement is not the same as the Adverb at the";
    cout << "\nstart of the second Subject of the first ) in the current Statement";
    throw 0;
  }
  putWord(Sbjs[0], pos, buf);
  if ( buf != ")" )
  {
    cout << "\nThe second Word of the earlier Statement is not )";
    throw 0;
  }
  getSent(buf, pos, Sbjs[0]);
  if ( buf != SbjB )
  {
    cout << "\nThe first Subject of the first ) in the earlier Statement is not the same as";
    cout << "\nthe first Subject of the first ) in the current Statement";
    throw 0;
  }
  getSent(buf, pos, Sbjs[0]);
  if ( buf != SbjC )
  {
    cout << "\nThe second Subject of the first ) in the earlier Statement is not the same as";
    cout << "\nthe Subject in the current Statement of the Adverb that moved";
    throw 0;
  }
  Wrd[0] = '+';
  if ( hasnGovObjoc(Wrd, SbjB) )
  {
    cout << "\nIn the first Subject of the first ), there is an Object occurrence, that is";
    cout << "\nnot Governed, of the Noun that Agrees with the Adverb that moved";
    throw 0;
  }
}

bool isInitial(char c)
{
  bool tst = false;
  if (c == '=' || c == '-' || c == '(' || c == ')') tst = true;
  if (c == '+' || c == '[' || c == ']') tst = true;
  return tst;
}

bool isCapital(char c)
{
  bool tst = false;
  if (c == '=' || c == '-' || c == '(' || c == ')') tst = true;
  if (c == '+' || c == '/' || c == '[' || c == ']') tst = true;
  return tst;
}

char possreverse(char c)
{
  char ch = c;
  if ( c == '(' ) ch = ')';
  if ( c == ')' ) ch = '(';
  if ( c == '[' ) ch = ']';
  if ( c == ']' ) ch = '[';
  if ( c == '<' ) ch = '>';
  if ( c == '>' ) ch = '<';
  if ( c == '{' ) ch = '}';
  if ( c == '}' ) ch = '{';
  return ch;
}