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

#include <ac.h>
#include <svc.h>
#include <store.h>
#include <add.h>
#include <ineq.h>
#include <bitvec.h>
#include <splitter_ext.h>
#include <record.h>
#include <flags.h>
#include <fstream.h>
#include <ctype.h>
#include <yyexprmisc.h>
#include <cmdparse.h>
#include <splitter.h>

static char* source_filename;
static char* status_filename;
static char* splitter_policy;
static char* splitter_flags;
static char* rewrite_flags;
static int printlicense = -1;

cmd_line_option cmd_line_options[] = {
  { CLO_STRING, "dump-result", "/dev/null", &status_filename,
    "Print the result" },
  { CLO_STRING, "dump-expression", "/dev/null", &source_filename, 
    "Print the parsed input expression" },
  { CLO_STRING, "splitter-policy", "default", &splitter_policy,
    "Select the splitter policy to be used" },
  { CLO_STRING, "splitter-flags", "", &splitter_flags,
    "Set splitter flag values: \"f1=v1,f2=v2,...,fn=vn\"" },
  { CLO_STRING, "rewrite-flags", "", &rewrite_flags,
    "Set rewrite flag values: \"f1=v1,f2=v2,...,fn=vn\"" },
  { CLO_INT, "set-verbosity", "2", &FLAGS::verbose, "Set verbosity level" },
  { CLO_INT, "set-abort-threshhold", "0", &FLAGS::abortthreshhold,
    "Set abort threshhold" },
  { CLO_INT, "set-strict", "0", &FLAGS::strictInterpSyntax,
    "Require strict syntax--{foo} instead of (foo)--for interpreted functions" },
  { CLO_NOARG, "license", "-1", &printlicense, "Print full copyright notice" },
};

int num_cmd_line_options = sizeof(cmd_line_options)/sizeof(cmd_line_option);


/* perhaps move this into cmdparse.cc  @JL */

int get_flag_value_pair(char *&flag_settings, int &flag, int &value)
{
  assert_msg(flag_settings, ("no flag_settings string"));
  char *s = &flag_settings[0];

  if (*s=='\0') return 0;
  if (!isdigit(*s)) goto error;
  flag = atoi(s);
  for (; isdigit(*s); s++);
  if (!(*s=='=' && isdigit(*++s))) goto error;
  value = atoi(s);
  for (; isdigit(*s); s++);
  if (*s!='\0' && *s++!=',') goto error;
  flag_settings=s;
  return 1;

error:
  flag_settings = NULL;
  return 0;
}


void Break() 
{
  cout << "INVALID\n"
       << "Falsifying Assumptions\n======================\n" 
       << AC::PrintAllSplitters << endl;
}


int main(int argc, char* argv[])
{
  ofstream source_file, status_file;
  char *prog_name = argv[0];
  char *file_name;
  Bool rc;

  parse_cmd_line(argc, argv, cmd_line_options, num_cmd_line_options);

  if (printlicense != -1) {
    cout << endl << Print_Full_Copyright_Notice << endl;
    exit(0);
  }

  if (argc!=2) {
    cerr << "Usage: " << prog_name << " [options] file\n";
    cmd_line_option_usage(num_cmd_line_options);
    goto error;
  }

  file_name = copy_string(argv[1]);

  // fire up SVC

  init_vc_library();
  init_store_library();
  init_add_library();
  init_ineq_library();
  init_bitvec_library();
  init_splitter_extensions_library();
  init_record_library();
  AC::Init();
  AC::RegisterBreakFunction(Break);

  cout << "\n" << Print_Short_Copyright_Notice
       << "Use '-license' option for details" << endl << endl;

  // open files from command line

  source_file.open(source_filename, ios::out);
  status_file.open(status_filename, ios::out);

  if (!(source_file && status_file)) {
    cerr << "***ERROR: couldn't open files: " << source_filename 
	 << ", " << status_filename << endl;
    goto error;
  }

  // set rewrie flags from command line

  int flag, value;
  for (flag=0, value=0; 
       get_flag_value_pair(rewrite_flags, flag, value);
       FLAGS::SetRewriteFlag(flag, value));
  if (!rewrite_flags) {
    cerr << "***ERROR: invalid argument for rewrite-flags" << endl;
    goto error;
  }

  // set splitter policy & flags from commmand line
  
  Splitter_Policy::InstallPolicy(splitter_policy);
  for (flag=0, value=0; 
       get_flag_value_pair(splitter_flags, flag, value);
       Splitter_Policy::SetFlag(flag, value));
  if (!splitter_flags) {
    cerr << "***ERROR: invalid argument for splitter-flags" << endl;
    goto error;
  }

  // parse formula and build expression

  if (!readfile(file_name)) {
    cerr << "error opening file: " << file_name << endl;
    goto error;
  }

  exprparse();

  if (!expr) {
    cerr << "parse error in file: " << file_name << endl;
    goto error;
  }

  source_file << expr << endl;

  cout << "file:\t\t " << file_name << endl;
  rc = AC::CurrentContext()->ValidateWithStats(expr);
  status_file << ((rc) ? "VALID" : "INVALID");
  return 0;


error:
  status_file << "ERROR";
  return 1;
}