///////////////////////////////////////////////////////////////////////////////
//                                                                           //
//  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 <fstream.h>
#include <yyexprmisc.h>
#include <cmdparse.h>
#include <flags.h>

PExpr ite_simplify(PExpr);
PExpr ite_reorder(PExpr e);

static int ite_simplify_flag;
static int ite_reorder_flag;
static int printlicense;

cmd_line_option cmd_line_options[] = {
  { CLO_NOARG, "ite-simplify", "1", &ite_simplify_flag, 
    "Simplify nested ite expressions" },
  { CLO_NOARG, "ite-reorder", "0", &ite_reorder_flag,
    "Put ite expressions in pesudo-normal form" },
  { 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);


int main(int argc, char** argv)
{
  char *prog_name = argv[0];
  char *infile, *outfile;

  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!=3) {
    cerr << "Usage: " << prog_name << " [options] infile outfile\n";
    cmd_line_option_usage(num_cmd_line_options);
    goto error;
  }

  infile = copy_string(argv[1]);
  outfile = copy_string(argv[2]);

  // 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();

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

  // run normalizing passes

  if (readfile(infile) && (!exprparse())) {
    extern PExpr expr;
    PExpr e = expr;

    do {
      AC::CurrentContext()->SetNewGoal(e);
      AC::CurrentContext()->MoveConditionsToGoal();
      e = AC::CurrentContext()->Goal();
      ASSERT_MSG(e, ("Unexpected NULL result"));

      if (ite_simplify_flag)
	e=ite_simplify(e);

      if (ite_reorder_flag)
	e=ite_reorder(e);

    } while (!AC::IsStable());

    ofstream os(outfile);

    if (!os) {
      cerr << "***ERROR: cannot open file \"" << outfile
	   << "\" for writing" << endl;
      goto error;
    }

    os << e << endl;

    return 0;
  }

error:
  return 1;
}