/**CFile***********************************************************************

  FileName    [baigCmd.c]

  PackageName [baig]

  Synopsis    [Functions to initialize and shut down the bAig manager.]

  Author      [Mohammad Awedh]

  Copyright [ This file was created at the University of Colorado at
  Boulder.  The University of Colorado at Boulder makes no warranty
  about the suitability of this software for any purpose.  It is
  presented on an AS IS basis.]

******************************************************************************/

#include "maig.h"
#include "ntk.h"
#include "cmd.h"
#include "baig.h"
#include "baigInt.h"
#include "ctlsp.h"

static char rcsid[] UNUSED = "$Id: baigCmd.c,v 1.32 2009/04/12 00:14:03 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Stucture declarations                                                     */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/
static jmp_buf timeOutEnv;
static int bmcTimeOut;		/* timeout value */
static long alarmLapTime;	/* starting CPU time for timeout */


/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/


/**AutomaticStart*************************************************************/

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/

static int CommandPrintPartitionAig(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandPrintAigStats(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int CommandCheckInvariantSat(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static void TimeOutHandle(void);

/**AutomaticEnd***************************************************************/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Initialize baig package]

  SideEffects [none]

  SeeAlso     [bAig_End]

******************************************************************************/
void
bAig_Init(void)
{
  Cmd_CommandAdd("print_partition_aig_dot", CommandPrintPartitionAig, 0);
  Cmd_CommandAdd("print_aig_stats", CommandPrintAigStats, 0);
  Cmd_CommandAdd("check_invariant_sat", CommandCheckInvariantSat, 0);
}


/**Function********************************************************************

  Synopsis [End baig package]

  SideEffects []

  SeeAlso     [bAig_Init]

******************************************************************************/
void
bAig_End(void)
{
}

/**Function********************************************************************

  Synopsis    [Creates a new bAig manager.]

  Description [Creates a new bAig manager, Create a NodeArray of size equal to
  maxSize * bAigNodeSize. Returns a pointer to the manager if successful; 
  NULL otherwise.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
bAig_Manager_t *
bAig_initAig(
  int maxSize /* maximum number of nodes in the AIG graph */
)
{
  int i;

  bAig_Manager_t *manager = ALLOC(bAig_Manager_t,1);
  if (manager == NIL( bAig_Manager_t)){
    return NIL( bAig_Manager_t);
  }
  /*Bing:*/
  memset(manager,0,sizeof(bAig_Manager_t ));

  maxSize = maxSize * bAigNodeSize;  /* each node is a size of bAigNodeSize */

  /* ??? */
  /*  maxSize = (maxSize/bAigNodeSize)*bAigNodeSize;
  if (maxSize >  bAigArrayMaxSize ) {
  }*/
  manager->NodesArray = ALLOC(bAigEdge_t, maxSize);
  manager->maxNodesArraySize = maxSize;
  manager->nodesArraySize = bAigFirstNodeIndex;

  fanout(0) = 0;
  canonical(0) = 0;
  flags(0) = 0;
  aig_value(0) = 2;
  next(0) = bAig_NULL;
  /*Bing:*/
  memset(manager->NodesArray,0,maxSize*sizeof(bAigEdge_t));

  manager->SymbolTable = st_init_table(strcmp,st_strhash);
  manager->nameList = ALLOC(char *, manager->maxNodesArraySize/bAigNodeSize);
  manager->bddIdArray = ALLOC(int, manager->maxNodesArraySize/bAigNodeSize);
  manager->bddArray = ALLOC(bdd_t *, manager->maxNodesArraySize/bAigNodeSize);

  manager->HashTable =  ALLOC(bAigEdge_t, bAig_HashTableSize);
  for (i=0; i<bAig_HashTableSize; i++)
    manager->HashTable[i]= bAig_NULL; 

  manager->mVarList = array_alloc(mAigMvar_t, 0);
  manager->bVarList = array_alloc(mAigBvar_t, 0);
  manager->timeframe = 0;
  manager->timeframeWOI = 0;
  manager->literals = 0;
    
  /* Bing: for MultiCut */
  manager->SymbolTableArray = ALLOC(st_table *,100);
  manager->HashTableArray = ALLOC(bAigEdge_t *,100);
  manager->NumOfTable = 100;

  /* Bing: for interpolation */
  manager->class_ = 1;
  manager->InitState = bAig_One;
  manager->assertArray = (satArray_t *)0;

  return(manager);

} /* end of bAig_Init */


/**Function********************************************************************

  Synopsis [Quit bAig manager]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_quit(
  bAig_Manager_t *manager)
{
  char          *name;
  st_generator  *stGen;
  bAigEdge_t    varIndex;

  if (manager->mVarList != NIL(array_t)){
    array_free(manager->mVarList);
  }
  if (manager->bVarList != NIL(array_t)){
    array_free(manager->bVarList);
  }
  FREE(manager->HashTable);
  st_foreach_item(manager->SymbolTable, stGen, &name, &varIndex) {
    FREE(name);
  }
  st_free_table(manager->SymbolTable);
  /* i is too small to represent 80000
  for (i=0; i< manager->maxNodesArraySize/bAigNodeSize ; i++){
    FREE(manager->nameList[i]);
  }
  */
  FREE(manager->nameList);
  FREE(manager->NodesArray);
  bAig_FreeTimeFrame(manager->timeframe);
  bAig_FreeTimeFrame(manager->timeframeWOI);
  FREE(manager);

  /* Free SymbolTableArray and HashTableArray? */
}

/**Function********************************************************************

  Synopsis    []

  Description []

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
void 
bAig_NodePrint(
   bAig_Manager_t *manager,
   bAigEdge_t node)
{
  if (node == bAig_Zero) {
    printf("0");
    return;
  }
  if (node == bAig_One) {
    printf("1");
    return;
  }
  if (bAig_IsInverted(node)){
    printf(" NOT(");
  }
  if (bAigIsVar(manager,node)) {
    printf("Var Node");
  } else {
    printf("(");
    bAig_NodePrint(manager, leftChild(node));
    printf("AND");
    bAig_NodePrint(manager, rightChild(node));
    printf(")");
  }
  if (bAig_IsInverted(node)){
    printf(")");
  }

} /* bAig_NodePrint */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/

/**Function********************************************************************

  Synopsis    [Implements the print_partition_aig_dot command.]
  
  CommandName [print_partition_aig_dot]

  CommandSynopsis [Print a dot description of the AND/INVERTER graph that was
  built for the flattened network]

  CommandArguments [\[-h\] &lt;file_name&gt;]

  CommandDescription [Write a file in the format taken by the tool <tt>dot</tt>
  depicting the topology of the AND/INVERTER graph. 
  Dot is a tool that given a description of a graph in a certain format it 
  produces a postscript print of the graph. 
  For more information about <tt>dot</tt> look in <a
  href="http://www.research.att.com/orgs/ssr/book/reuse">
  http://www.research.att.com/orgs/ssr/book/reuse</a>. Once a dot file is
  produced with this command, the shell command <tt>dot -Tps <filename>
  &gt;<file>.ps</tt> will produce the postscript file depicting the network.<p>

  If no argument is specified on the command line, the description is written
  to the standard output.<p>

  Command options:<p>
  <dl><dt> -h
  <dd> Print the command usage.
  </dl>]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
CommandPrintPartitionAig(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  FILE *fp;
  int c, i, mvfSize;
  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  mAig_Manager_t *manager;
  MvfAig_Function_t  *mvfAig;
  bAigEdge_t v;
  Ntk_Node_t *node, *latch;
  st_table   *node2MvfAigTable;
  lsGen gen;

  util_getopt_reset();
  while ((c = util_getopt(argc,argv,"h")) != EOF){
    switch(c){
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }
  /* Check if the network has been read in */
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }

  if (argc == 1) {
    fp = stdout;
  }
  else if (argc == 2) {
    fp = Cmd_FileOpen(*(++argv), "w", NIL(char *), /* silent */ 1);
    if (fp == NIL(FILE)) {
      (void) fprintf(vis_stderr, "Cannot write to %s\n", *argv);
      return 1;
    }
  }
  else {
    goto usage;
  }

  manager = Ntk_NetworkReadMAigManager(network);

  if (manager == NIL(mAig_Manager_t)) {
    return 1;
  }
  node2MvfAigTable = 
	(st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);

  Ntk_NetworkForEachLatch(network, gen, latch) {
    node = Ntk_LatchReadDataInput(latch);
    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
      bAig_SetMaskTransitiveFanin(manager, v, VisitedMask);
    }
  }
  Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
      bAig_SetMaskTransitiveFanin(manager, v, VisitedMask);
    }
  }

  Ntk_NetworkForEachNode(network, gen, node) {
    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
      bAig_SetMaskTransitiveFanin(manager, v, VisitedMask);
    }
  }

  bAig_PrintDot(fp, manager);
  Ntk_NetworkForEachLatch(network, gen, latch) {
    node = Ntk_LatchReadInitialInput(latch);
    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
      bAig_ResetMaskTransitiveFanin(manager, v, VisitedMask, ResetVisitedMask);
    }
  }
  Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
      bAig_ResetMaskTransitiveFanin(manager, v, VisitedMask, ResetVisitedMask);
    }
  }
  Ntk_NetworkForEachNode(network, gen, node) {
    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
      bAig_ResetMaskTransitiveFanin(manager, v, VisitedMask, ResetVisitedMask);
    }
  }

  return 0;
usage:
  (void) fprintf(vis_stderr, "usage: print_partition_aig_dot [-h] [file]\n");
  (void) fprintf(vis_stderr, "    -h\t\tprint the command usage\n");
  return 1;
}

/**Function********************************************************************

  Synopsis    [Implements the print_aig_stats command.]
  CommandName [print_aig_stats]

  CommandSynopsis [print statistics about the AND/INVERTER graph.]

  CommandArguments [\[-h\] \[-n\]]

  CommandDescription [Print the following statistics about the AND/INVERTER 
  graph:

 <dl>
  <li> <b>Maximum number of nodes:</b> the maximum number of nodes in the AND/
  INVERTER graph.

  <li> <b>Current number of nodes:</b> the number of nodes in the AND/INVERTER
  graph that are used.

 </dl>

  Note that <tt>build_partition_maigs</tt> must be called before this command.<p>

  Command options:<p>

  <dl>
  <dt> -n
  <dd> Print the name of the nodes.<p>
  <dt> -h
  <dd> Print the command usage.<p>
  </dl>
  ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
CommandPrintAigStats(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  mAig_Manager_t *manager;
  int i;
  int printVar = 0;
  int c;

  /*
   * Parse command line options.
   */
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "hn")) != EOF) {
    switch(c) {
      case 'h':
        goto usage;
     case 'n':
       printVar = 1;
        break;
      default:
        goto usage;
    }
  }
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }

  manager = Ntk_NetworkReadMAigManager(network);

  if (manager == NIL(mAig_Manager_t)) {
    return 1;
  }
  (void) fprintf(vis_stdout,"And/Inverter graph Static Report\n");
  (void) fprintf(vis_stdout,"Maximum number of nodes: %ld\n", manager->maxNodesArraySize/bAigNodeSize);
  (void) fprintf(vis_stdout,"Current number of nodes: %ld\n\n", manager->nodesArraySize/bAigNodeSize);
  if (printVar == 1){
     (void) fprintf(vis_stdout,"Nodes name\n");
     for(i=1; i< manager->nodesArraySize/bAigNodeSize; i++){
        if (manager->nameList[i][0] != 'N'){
           (void) fprintf(vis_stdout,"%s\n", manager->nameList[i]);
        }
     }
  }
  return 0;
usage:
  (void) fprintf(vis_stderr, "usage: print_aig_stats [-h] [-n] \n");
  (void) fprintf(vis_stderr, "   -h print the command usage\n");
  (void) fprintf(vis_stderr, "   -n list of variables\n");
  return 1;		/* error exit */
}

/**Function********************************************************************

  Synopsis    [Implements the check_invariant_sat command.]
  CommandName [check_invariant_sat]

  CommandSynopsis [Check invariant property using sat based unmounded model checking]

  CommandArguments [\[-h\] \[-d\] 
                    \[-t &lt;timeOutPeriod&gt;\] 
		    \[-m &lt;method&gt;\]
		    \[-v &lt;verbosity_level&gt;\] 
		    &lt;inv_file&gt; ]

  CommandDescription [Perform SAT-based unbounded model checking on 
  And-Inverter-Graph. The command compute fixed point of AG using AX operation.
  AX is implemented using AllSAT enumeration algorithm.

  Command options:<p>

  <dl>
  <dt> -d 
  <dd> Disable inclusion test on initial states.<p>

  <dt> -v  <code>&lt;verbosity_level&gt;</code>
  <dd> Specify verbosity level. This sets the amount of feedback  on CPU usage and code status.

  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
  <dd> Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
  <p>

  <dt> -m  <code>&lt;method&gt;</code>
  <dd> Specify the method for AllSAT algorithm.
  <p>


  <dt> -h
  <dd> Print the command usage.<p>
  </dl>

  <dt> <code> &lt;inv_file&gt; </code>
  <dd> File containing Invariant formulae to be checked.
  ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
CommandCheckInvariantSat(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
char *filename;
FILE *fin;
array_t *invarArray;
Ntk_Network_t     *network;
bAig_Manager_t    *manager;
bAigTransition_t *t;
Ctlsp_Formula_t *formula;
char c;int i, property;
int timeOutPeriod;
int passFlag, method;
int interface, verbose;
int inclusion_test;
int constrain;
int reductionUsingUnsat;
int disableLifting;

  timeOutPeriod = -1;
  method = 1;
  interface = 0;
  inclusion_test = 1;
  verbose = 0;
  constrain = 1;
  reductionUsingUnsat = 0;
  disableLifting = 0;
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "hicdt:m:v:ul")) != EOF) {
    switch(c) {
      case 'h':
	goto usage;
      case 'i' :
	interface = 1;
	break;
      case 'd' :
	inclusion_test = 0;
	break;
      case 'c' :
	constrain = 0;
	break;
      case 'u' :
	reductionUsingUnsat = 1;
	break;
      case 'l' :
	disableLifting = 1;
	break;
      case 't' :
	timeOutPeriod = atoi(util_optarg);
	break;
      case 'v' :
	verbose = atoi(util_optarg);
	break;
      case 'm' :
	method = atoi(util_optarg);
	break;
    }
  }
  if (argc - util_optind == 0) {
    (void) fprintf(vis_stderr, "** ERROR : file containing property file not provided\n");
    goto usage;
  }
  else if (argc - util_optind > 1) {
    (void) fprintf(vis_stderr, "** ERROR : too many arguments\n");
    goto usage;
  }
  filename = util_strsav(argv[util_optind]);

  if(!(fin = fopen(filename, "r"))) {
    fprintf(vis_stdout, "Error : can't open invariant file %s\n", filename);
    return(1);
  }
  invarArray = Ctlsp_FileParseFormulaArray(fin);
  fclose(fin);

  if (timeOutPeriod > 0) {
    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
    (void) alarm(timeOutPeriod);
    if (setjmp(timeOutEnv) > 0) {
      (void) fprintf(vis_stderr,
		"** ERROR : timeout occurred after %d seconds.\n", timeOutPeriod);
      alarm(0);
      return 1;
    }
  }

  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  manager = Ntk_NetworkReadMAigManager(network);

  t = bAigCreateTransitionRelation(network, manager);
  t->method = method;
  t->interface = interface;
  t->inclusionInitial = inclusion_test;
  t->verbose = verbose;
  t->constrain = constrain;
  t->disableLifting = disableLifting;
  t->reductionUsingUnsat = reductionUsingUnsat;

  if(t->verbose > 1) 
    bAigPrintTransitionInfo(t);


  fprintf(vis_stdout, "# INV: Summary of invariant pass/fail\n");
  for(i=0; i<array_n(invarArray); i++) {
    formula = array_fetch(Ctlsp_Formula_t *, invarArray, i);
    Ctlsp_FormulaPrint(vis_stdout, formula);
    fprintf(vis_stdout, "\n");

    property = bAig_CreatebAigForInvariant(network, manager, formula);

    passFlag = bAigCheckInvariantWithAG(t, property);

    if(passFlag == 1) {
      fprintf(vis_stdout, "# INV: formula passed --- ");
      Ctlsp_FormulaPrint(vis_stdout, Ctlsp_FormulaReadOriginalFormula(formula));
      fprintf(vis_stdout, "\n");
    }
    else {
      fprintf(vis_stdout, "# INV: formula failed --- ");
      Ctlsp_FormulaPrint(vis_stdout, Ctlsp_FormulaReadOriginalFormula(formula));
      fprintf(vis_stdout, "\n");
    }
  }

  return(0);

  usage:
  (void) fprintf(vis_stderr, "usage: check_invariant_sat [-h] <inv_file>\n");
  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
  (void) fprintf(vis_stderr, "   -d \tdisable inclusion test on initial states\n");
  (void) fprintf(vis_stderr, "   -m : 0 disable lifting\n");
  (void) fprintf(vis_stderr, "        1 enable lifting (default)\n");
  (void) fprintf(vis_stderr, "   <inv_file> Invariant file to be checked.\n");

  return(1);
}


/**Function********************************************************************

  Synopsis    [Handle function for timeout.]

  Description [This function is called when the time out occurs.
  Since alarm is set with an elapsed time, this function checks if the
  CPU time corresponds to the timeout of the command.  If not, it
  reprograms the alarm to fire again later.]

  SideEffects []

******************************************************************************/
static void
TimeOutHandle(void)
{
  int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000);

  if (seconds < bmcTimeOut) {
    unsigned slack = (unsigned) (bmcTimeOut - seconds);
    (void) signal(SIGALRM, (void(*)(int)) TimeOutHandle);
    (void) alarm(slack);
  } else {
    longjmp(timeOutEnv, 1);
  }
} /* TimeOutHandle */