///////////////////////////////////////////////////////////////////////////////
//                                                                           //
//  Copyright (C) 1995-2002 by the Board of Trustees of Leland Stanford      //
//  Junior University.  See LICENSE for details.                             //
//                                                                           //
///////////////////////////////////////////////////////////////////////////////

#include <string.h>
#include <yyexprmisc.h>
#include <expr.h>

extern int inputline;

int cmderror(char *s)
{
  cout << s << endl;
  return 1;
}


void Print_General_Help()
{
  cout << "SVC commands:" << endl;
  cout << "------------------------------------------------------------------------------" << endl;
  cout << "assert <expr>                           check_valid <expr>" << endl;
  cout << "continue" << endl;
  cout << "cva <expr> <expr>                       echo <string>" << endl;
  cout << "deny <expr>                             help [<command>]" << endl;
  cout << "mark_relevant <num>                     new_expr <expr>" << endl;
  cout << "pop                                     print <expr>" << endl;
  cout << "print_flags                             print_rewrite_flags" << endl;
  cout << "print_type <expr>                       push" << endl;
//  cout << "queryeq";
  cout << "quit" << endl;
  cout << "read <filename>                         reset" << endl;
  cout << "return                                  set_persistent <expr>" << endl;
  cout << "set <expr_abv> <expr>                   set_rewrite_flag <num> <num>"
       << endl;
  cout << "set_all_rewrites <num>                  set_splitter_flag <num> <num>"
       << endl;
  cout << "set_splitter_policy <policyname>        source <filename>" << endl;
  cout << "set_strict <num>                        show_progress <num>" << endl;
  cout << "verbosity <num>                         write <filename> <expr>" << endl;
IF_DEBUG(
  cout << endl
       << "print_debug_flags                       toggle_debug_flag <num|flagname>"
       << endl;
)
  cout << endl;
  cout << "For help with a specific command or piece of syntax, type" << endl;
  cout << "help <command|syntax>.  For example, \"help assert\" or \"help expr\"." << endl;
  cout << "------------------------------------------------------------------------------" << endl;
  cout << endl;
}


void Print_Specific_Help(const char *command)
{
  char firstchar = command[0];
  if (firstchar >= 'A' && firstchar <= 'Z') {
    firstchar += ('a' - 'A');
  }
  cout << "------------------------------------------------------------------------------" << endl;
  switch (firstchar) {
    case 'a':
      cout << "assert <expr>" << endl;
      cout << "a <expr>" << endl;
      cout << endl;
      cout << "This command asserts that the expression is TRUE in the current context." << endl;
      cout << "Note that if the expression is non-atomic, the results are not immediately" << endl;
      cout << "applied to the context, but are added as a condition to the context" << endl;
      cout << "which is required to be true before any counter-example is generated." << endl;
      cout << "If the context becomes inconsistent as a result of the assertion," << endl;
      cout << "INCONSISTENT is reported.  Otherwise, NORMAL is reported." << endl;
      break;
    case 'c':
      if (strcasecmp(command, "check_valid") == 0 ||
	  strcasecmp(command, "cv") == 0) {
	cout << "check_valid <expr>" << endl;
	cout << "cv <expr>" << endl;
	cout << endl;
	cout << "Check whether the expression is valid in the current context." << endl;
	cout << "If it is, VALID is reported.  Otherwise, INVALID is reported, and a" << endl;
	cout << "counter-example is given.  The number of case splits and generated" << endl;
	cout << "expressions is also reported." << endl;
      }
      else if (strcasecmp(command, "command") == 0) {
        cout << "For help with a specific command or piece of syntax," << endl;
        cout << "type help <command|syntax>.  For example, \"help assert\"" << endl;
        cout << "or \"help expr\"" << endl;
      }
      else if (strcasecmp(command, "continue") == 0 ||
	       strcasecmp(command, "c") == 0) {
	cout << "continue" << endl;
	cout << "c" << endl;
	cout << "If a call to check_valid returns a counter-example, you can use this command to" << endl;
	cout << "continue checking the expression as if the counter-example had not occurred." << endl;
      }
      else {
	cout << "cva <expr> <expr>" << endl;
	cout << "" << endl;
	cout << "Check valid with assumption: Check whether the first expression implies" << endl;
	cout << "the second expression.  This is done by asserting the first expression" << endl;
	cout << "in the context and then checking the validity of the second expression." << endl;
      }
      break;
    case 'd':
      cout << "deny <expr>" << endl;
      cout << "d <expr>" << endl;
      cout << "" << endl;
      cout << "This command asserts that the expression is FALSE in the current context." << endl;
      cout << "Note that if the expression is non-atomic, the results are not immediately" << endl;
      cout << "applied to the context, but are added as a condition to the context" << endl;
      cout << "which is required to be true before any counter-example is generated." << endl;
      cout << "If the context becomes inconsistent as a result of the assertion," << endl;
      cout << "INCONSISTENT is reported.  Otherwise, NORMAL is reported." << endl;
      break;
    case 'e':
      if (strcasecmp(command, "expr") == 0) {
	cout << "<expr>" << endl;
	cout << "" << endl;
	cout << "expr              :       expr_ref" << endl;
        cout << "                  |       ( constructed_expr )" << endl;
        cout << "                  |       ( svc-expr-function )" << endl;
	cout << "expr_ref          :       expr_abv" << endl;
	cout << "                  |       expr_num" << endl;
	cout << "expr_abv          :       $<identifier>" << endl;
	cout << "expr_num          :       $<num>" << endl;
        cout << "constructed_expr  :       ite" << endl;
	cout << "                  |       equal" << endl;
	cout << "                  |       expr_abv : constructed_expr" << endl;
	cout << "                  |       [ type expr ]" << endl;
	cout << "                  |       expr" << endl;
	cout << "                  |       function" << endl;
	cout << "                  |       constant" << endl;
	cout << "ite               :       ITE expr expr expr" << endl;
	cout << "equal             :       = expr expr" << endl;
	cout << "function          :       <identifier> expr-list" << endl;
	cout << "                  |       <identifier>" << endl;
	cout << "constant          :       FALSE" << endl;
	cout << "                  |       TRUE" << endl;
	cout << "                  |       rational" << endl;
	cout << "                  |       distinct" << endl;
        cout << "type              :       UNKNOWN | BOOL | RAT | CONST" << endl;
        cout << "                  |       ARRAY type type" << endl;
        cout << "                  |       RECORD {distinct type}+ ENDRECORD" << endl;
        cout << "                  |       BITVEC <num>" << endl;
	cout << "rational          :       <integer>" << endl;
	cout << "                  |       <integer> | <integer>" << endl;
	cout << "distinct          :       @<identifier>" << endl;
        cout << "svc-expr-function :       SVC-SUBST expr expr expr" << endl;
        cout << "                  |       SVC-FS expr" << endl;
        cout << "                  |       SVC-SIG expr" << endl;
        cout << "                  |       SVC-SIMP expr" << endl;
        cout << "                  |       SVC-CHILD <num> expr" << endl;
	cout << "                  |       SVC-READFILE <filename>" << endl;
	cout << "" << endl;
        cout << "Expressions are either expression references or constructed expressions (which" << endl;
        cout << "are always enclosed in parentheses).  An expression reference must begin with" << endl;
        cout << "$ and is either an abbreviation (see expr_abv) or the number of the expression" << endl;
        cout << "to which you want to refer.  For example, \"p $42\" will print expression" << endl;
        cout << "number 42.  Similarly, \"p $x\" will print the expression with abbreviation $x." << endl;
        cout << "In contrast, constructed expressions are created and canonized after parsing." << endl;
        cout << endl;
	cout << "See syntax.html (included in your distribution) for more detailed information." << endl;
      }
      else if (strcasecmp(command, "expr_abv") == 0) {
	cout << "<expr_abv>" << endl;
        cout << "" << endl;
        cout << "An expression abbreviation is basically a variable which the user can set" << endl;
        cout << "to refer to an expression.  Abbreviations begin with $ and a letter.  The" << endl;
        cout << "rest of the abbreviation may contain letters, numbers or a dash." << endl;
        cout << "Abbreviations can be set explicitly by using the set command, or implicitly" << endl;
        cout << "by labeling an expression with a label as it is created.  For example, the" << endl;
        cout << "following two commands both set $eqxy to be an abbreviation for (= x y):" << endl;
	cout << "new_expr ($eqxy : (= x y))" << endl;
	cout << "set $eqxy (= x y)" << endl;
      }
      else {
	cout << "echo <string>" << endl;
        cout << "e <string>" << endl;
        cout << "" << endl;
        cout << "This command simply prints the text of the string.  It is especially useful" << endl;
        cout << "in scripts." << endl;
      }
      break;
    case 'f':
      if (strcasecmp(command, "filename") == 0) {
	cout << "<filename>" << endl;
        cout << "" << endl;
        cout << "This is simply any legal file name.  If the complete path is not given," << endl;
	cout << "the path is taken as being relative to the directory from which SVC was run." << endl;
      }
      else {
	cout << "<flagname>" << endl;
        cout << "" << endl;
        cout << "Each debug flag has a name.  The name of each flag is shown when you execute" << endl;
        cout << "the print_debug_flags command." << endl;
      }
      break;
    case 'h':
      cout << "help" << endl;
      cout << "h" << endl;
      cout << "" << endl;
      cout << "Print a listing of all SVC commands." << endl;
      break;
    case 'l':
      cout << "license" << endl;
      cout << "l" << endl;
      cout << "" << endl;
      cout << "Print the distribution license information." << endl;
      break;
    case 'm':
      cout << "mark_relevant <num>" << endl;
      cout << "mr <num>" << endl;
      cout << endl;
      cout << "Set the mark_relevant flag to the value specified by <num>.  A value of 0" << endl;
      cout << "disables the flag.  A nonzero value enables an optimization in which" << endl;
      cout << "congruence closure is only performed on relevant expressions." << endl;
      break;
    case 'n':
      if (strcasecmp(command, "num") == 0) {
	cout << "<num>" << endl;
        cout << "" << endl;
        cout << "A nonnegative integer.  For flags, 0 is used to indicate that the flag is" << endl;
	cout << "disabled and 1 is used to indicate that the flag is enabled." << endl;
      }
      else {
	cout << "new_expr <expr>" << endl;
        cout << "ne <expr>" << endl;
        cout << "" << endl;
        cout << "This is the primary command for creating new expressions from the command" << endl;
        cout << "line.  The number of the new expression is returned by SVC." << endl;
      }
      break;
    case 'p':
      if (strcasecmp(command, "print_debug_flags") == 0 ||
	  strcasecmp(command, "pdf") == 0) {
	cout << "print_debug_flags" << endl;
        cout << "pdf" << endl;
        cout << "" << endl;
        cout << "Prints out a list of the debug flags with their current settings.  Note" << endl;
        cout << "that the executable must be compiled with DEBUG defined or the debug flags" << endl;
	cout << "will be disabled." << endl;
      }
      else if (strcasecmp(command, "print_flags") == 0 ||
	       strcasecmp(command, "pf") == 0) {
	cout << "print_flags" << endl;
        cout << "pf" << endl;
        cout << "" << endl;
        cout << "Print a list of the general-purpose flags with their current values." << endl;
        cout << "Also displays the current splitter policy and any flags associated" << endl;
        cout << "with that policy." << endl;
      }
      else if (strcasecmp(command, "print_rewrite_flags") == 0 ||
	       strcasecmp(command, "prf") == 0) {
	cout << "print_rewrite_flags" << endl;
        cout << "prf" << endl;
        cout << "" << endl;
        cout << "Print a list of the rewrite flags with their current values. " << endl;
      }
      else if (strcasecmp(command, "print_type") == 0 ||
	       strcasecmp(command, "pt") == 0) {
	cout << "print_type <expr>" << endl;
        cout << "pt <expr>" << endl;
        cout << "" << endl;
        cout << "Print the type of <expr>." << endl;
      }
      else if (strcasecmp(command, "pop") == 0) {
	cout << "pop" << endl;
        cout << "" << endl;
        cout << "Pop the current context.  This deletes any expressions and undoes any" << endl;
        cout << "assertions done since the last call to push, effectively restoring" << endl;
        cout << "the state of the program as it was at the last call to push.  Note that" << endl;
        cout << "the number in parentheses at the SVC prompt tells how many contexts" << endl;
        cout << "there are (including the current context).  Thus, pop decreases this" << endl;
        cout << "number by one." << endl;
      }
      else if (strcasecmp(command, "push") == 0) {
	cout << "push" << endl;
        cout << "" << endl;
        cout << "Push the current context onto the stack.  The current state of the program" << endl;
        cout << "can then be restored by a corresponding call to pop.  Note that the number" << endl;
        cout << "in parentheses at the SVC prompt tells how many contexts there are" << endl;
        cout << "(including the current context).  Thus, push increases this number by one." << endl;
      }
      else if (strcasecmp(command, "policyname") == 0) {
	cout << "<policyname>" << endl;
        cout << "" << endl;
        cout << "The available splitter policies are:" << endl;
        cout << "  default - Searches the tree depth-first looking for a boolean sub-expression" << endl;
        cout << "    to split on." << endl;
	cout << endl;
        cout << "  caching - Instead of using the default splitter, a splitter may be chosen" << endl;
        cout << "    from a cache of saved splitters.  The splitter from the cache is preferred" << endl;
        cout << "    if its *trust* level is larger than the depth of the current goal." << endl;
	cout << "    Each time a goal reduces to TRUE, the last few splitters are placed in the" << endl;
        cout << "    cache.  This policy has the following parameters which can be set:" << endl;
        cout << "      initial-trust-level - the initial trust one gives to a splitter that is" << endl;
        cout << "        saved in the cache.  The default is 2." << endl;
        cout << "      turnover-rate - This is the number of splitters that get placed into the" << endl;
        cout << "        cache each time the formula reduces to TRUE." << endl;
        cout << "      cache-size - The size of the cache--that is, the number of splitters it" << endl;
        cout << "        can hold." << endl;
        cout << "" << endl;
        cout << "  mbtf (move best to front) - This is a simplified version of caching which" << endl;
        cout << "    uses a set of conservative heuristics to give successful splitters priority" << endl;
        cout << "    over default splitters." << endl;
      }
      else {
	cout << "print <expr>" << endl;
        cout << "p <expr>" << endl;
        cout << "" << endl;
        cout << "Print the expression referred to by <expr>" << endl;
      }
      break;
    case 'q':
      if (strcasecmp(command, "queryeq") == 0) {
	cout << "queryeq <expr> <expr>" << endl;
        cout << "" << endl;
        cout << "This command has been disabled." << endl;
      }
      else {
	cout << "quit" << endl;
        cout << "q" << endl;
        cout << "exit" << endl;
        cout << "x" << endl;
        cout << "" << endl;
        cout << "Quit SVC." << endl;
      }
      break;
    case 'r':
      if (strcasecmp(command, "reset") == 0) {
	cout << "reset" << endl;
        cout << "" << endl;
        cout << "Pops all contexts and restores the initial empty context.  Note, however," << endl;
        cout << "that it does not change any flag settings." << endl;
      }
      else if (strcasecmp(command, "return") == 0 ||
	       strcasecmp(command, "ret") == 0) {
	cout << "return" << endl;
	cout << "ret" << endl;
	cout << endl;
	cout << "Return to the most recent context from which a call to check_valid was made." << endl;
      }
      else {
	cout << "read <filename>" << endl;
        cout << "r <filename>" << endl;
        cout << "" << endl;
        cout << "Create a new expression from the input contained in the file named" << endl;
        cout << "<filename>.  The number of the new expression is printed when done." << endl;
      }
      break;
    case 's':
      if (strcasecmp(command, "set_rewrite_flag") == 0 ||
	  strcasecmp(command, "srf") == 0) {
	cout << "set_rewrite_flag <num> <num>" << endl;
        cout << "srf <num> <num>" << endl;
        cout << "" << endl;
        cout << "Set the rewrite flag referred to by the first argument to the value" << endl;
        cout << "specified by the second argument.  The numbers of the rewrite flags" << endl;
        cout << "are given by the print_rewrite_flags command.  Note that a value of 1" << endl;
        cout << "means that the flag is enabled, while 0 means that the flag is disabled." << endl;
      }
      if (strcasecmp(command, "set_all_rewrites") == 0 ||
	  strcasecmp(command, "sa") == 0) {
	cout << "set_all_rewrites <num>" << endl;
        cout << "sa <num>" << endl;
        cout << "" << endl;
        cout << "Set all rewrite flags to the value specified by <num>.  If the value given is" << endl;
        cout << "0, then all flags are disabled.  If 1, all flags are enabled.  If greater than" << endl;
        cout << "1, then all flags are set to their default values." << endl;
      }
      else if (strcasecmp(command, "set_splitter_flag") == 0 ||
	       strcasecmp(command, "ssf") == 0) {
	cout << "set_splitter_flag <num> <num>" << endl;
        cout << "ssf <num> <num>" << endl;
        cout << "" << endl;
        cout << "Set the splitter flag referred to by the first argument to the value specified" << endl;
        cout << "by the second argument.  The numbers of the splitter flags are given by the" << endl;
        cout << "print_flags command.  The following flags are always available:" << endl;
	cout << "  0.  Prefer unit splitters" << endl;
        cout << "  1.  Split on finite domain subexpressions" << endl;
        cout << "  2.  Shuffle splitters to eliminate redundancy" << endl;
	cout << "Flag 0 causes SVC to choose unit splitters (splitters which are guaranteed to" << endl;
	cout << "terminate immediately on one of their branches) whenever possible.  Flag 1" << endl;
	cout << "overcomes an incompleteness in SVC when dealing with finite domains but" << endl;
        cout << "generally produces more case splits on examples with finite domain" << endl;
        cout << "expressions.  Flag 2 uses a sophisticated shuffling algorithm to eliminate" << endl;
        cout << "redundant splitters.  This usually results in (sometimes dramatically) fewer" << endl;
	cout << "case splits, but takes several times longer per case split than when turned" << endl;
	cout << "off.  Other flags may be available depending on which policy you are using" << endl;
        cout << "(see policyname for a description of which policies are available)." << endl;
      }
      else if (strcasecmp(command, "set_splitter_policy") == 0 ||
	       strcasecmp(command, "ssp") == 0) {
	cout << "set_splitter_policy <policyname>" << endl;
        cout << "ssp <policyname>" << endl;
        cout << "" << endl;
        cout << "Change the algorithm used by SVC for choosing which expression to split on." << endl;
        cout << "The different policies are described in the help for policyname." << endl;
      }
      else if (strcasecmp(command, "set_strict") == 0 ||
	       strcasecmp(command, "strict") == 0) {
	cout << "set_strict <num>" << endl;
        cout << "strict <num>" << endl;
        cout << "" << endl;
        cout << "Set the strict flag to the value specified by <num>.  A value of 1 enables" << endl;
        cout << "the flag.  A value of 0 disables the flag.  The strict flag controls how" << endl;
        cout << "SVC parses interpreted functions.  When the flag is enabled, interpreted" << endl;
        cout << "functions are required to be enclosed in curly braces: { }, and SVC will" << endl;
        cout << "also print interpreted expressions by enclosing them in curly braces." << endl;
        cout << "If the strict flag is not set, interpreted functions may be enclosed either" << endl;
        cout << "in curly braces, or in regular parentheses." << endl;
      }
      else if (strcasecmp(command, "show_progress") == 0 ||
	       strcasecmp(command, "sp") == 0) {
	cout << "show_progress <num>" << endl;
	cout << "sp <num>" << endl;
	cout << endl;
	cout << "Set the show_progress flag to the value specified by <num>.  A value of 0" << endl;
        cout << "disables the flag.  A nonzero value sets the case split interval at which" << endl;
	cout << "a progress report is printed." << endl;
      }
      else if (strcasecmp(command, "set_persistent") == 0 ||
	       strcasecmp(command, "setp") == 0) {
	cout << endl;
	cout << "Make this expression persistent, so that it does not get deleted when the" << endl;
        cout << "context in which it was created is popped." << endl;
      }
      else if (strcasecmp(command, "source") == 0) {
	cout << "source <filename>" << endl;
        cout << "" << endl;
        cout << "Read commands from the script file named <filename>" << endl;
      }
      else if (strcasecmp(command, "set") == 0) {
	cout << "set <expr_abv> <expr>" << endl;
        cout << "" << endl;
        cout << "This command parses the expression given by <expr> and sets the abbreviation" << endl;
        cout << "given by <expr_abv> to point to that expression.  If the abbreviation was" << endl;
        cout << "previously defined, the old value is lost (and a warning message is printed)." << endl;
      }
      else {
	cout << "<string>" << endl;
        cout << "" << endl;
        cout << "A string is simply text enclosed by double-quotes: \"text\"" << endl;
      }
      break;
    case 't':
      cout << "toggle_debug_flag <num|flagname>" << endl;
      cout << "tdf <num|flagname>" << endl;
      cout << "" << endl;
      cout << "Toggle the debug flag specified either by the number <num> or the name" << endl;
      cout << "<flagname>.  The print_debug_flags command gives both names and numbers" << endl;
      cout << "for all debug flags.  Note that the executable must be compiled with DEBUG" << endl;
      cout << "defined or the debug flags will be disabled." << endl;
      break;
    case 'v':
      cout << "verbosity <num>" << endl;
      cout << "v <num>" << endl;
      cout << "" << endl;
      cout << "Set the verbosity flag to the value given by <num>.  The default value is 2." << endl;
      cout << "When set to 1, expressions are printed without type information.  When set" << endl;
      cout << "to 0, only expression numbers are printed." << endl;
      break;
    case 'w':
      cout << "write <filename> <expr>" << endl;
      cout << "w <filename> <expr>" << endl;
      cout << "" << endl;
      cout << "This command dumps the expression given by <expr> to the file named" << endl;
      cout << "<filename>." << endl;
      break;
    default:
      cout << "Help for " << command << " not available" << endl;
      break;
  }
  cout << "------------------------------------------------------------------------------" << endl;
}


extern void cmdrestart(FILE *);

/* 
 * global variables set by readstring_cmd() or readfile_cmd()
 */
/* The next few variables are set by readstring_cmd() and used by the YY_INPUT
   macro in lexcmd.l */
char *str_to_read_cmd_from = NULL; /* the default is to read any
				      commands from the FILE *
				      cmdin (aka, yyin), but the
				      outside world can set this
				      variable to be a string from
				      which commands will be read. */
int len_str_to_read_cmd_from; /* the number of characters in
				 str_to_read_cmd_from*/
int cur_index_into_cmd_str; /* an index into str_to_read_cmd_from
			       (if that string is non-NULL) which
			       tells us where we should start reading
			       for the next call to YY_INPUT. */
/* setup_scanner()
 
   This function is called by readfile() and readstring().  f may be NULL. */
static void setup_scanner(FILE *f) {
  inputline = 1;
  cmdrestart(f);
}

/* cleanup_from_last_call()

   This function frees memory or closes files depending on whether the
   last call to read*() was to readstring_cmd() or readfile_cmd(). 
   If no read*() has been called yet, it does nothing. */
static void cleanup_from_last_call() {
  if (str_to_read_cmd_from) {
    /* we need to cleanup a string we allocated previously */
    delete [] str_to_read_cmd_from;
    str_to_read_cmd_from = NULL;
  }
}

/* readfile_cmd()
   
   The next call to cmdparse() will have the command parser draw its input
   from the given (FILE *), which should point to a descriptor for an open
   file. */
int readfile_cmd(FILE *file)
{
  cleanup_from_last_call();

  setup_scanner(file);

  return 1;
}

/* readstring()
   
   This function sets some global variables so that the next call to
   cmdparse() will read from a copy of the given string instead of from
   the (FILE *) cmdin (aka, yyin).  It returns 1 on success, and 0 on 
   failure.  If str is NULL, any old string allocated by a previous call
   to readstring() that hasn't yet been cleaned up will be freed. You
   must call readfile_cmd() explicitly after calling readstring_cmd() if
   you want the parser to read from a (FILE *) the next time it's called. */
int readstring_cmd(char *str) {
  cleanup_from_last_call();

  if (!str)
    /* the input string is null */
    return 1;

  len_str_to_read_cmd_from = strlen(str);

  /* copy str into str_to_read_cmd_from */
  str_to_read_cmd_from = new char[len_str_to_read_cmd_from+1];
  strcpy(str_to_read_cmd_from,str);

  /* we start reading at the first character of the string */
  cur_index_into_cmd_str = 0;

  setup_scanner(NULL);

  return 1;
}

/* chars_left_in_string_cmd()

   Return the number of characters in the input string that haven't
   been read by the parser yet. */
int chars_left_in_string_cmd() {
  int tmp = len_str_to_read_cmd_from - cur_index_into_cmd_str;
  return (tmp > 0) ? tmp : 0;
}