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

  FileName    [ntmaigCmd.c]

  PackageName [ntmaig]

  Synopsis    [Command interface for the Aig partition package]

  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 "ntmaigInt.h"

static char rcsid[] UNUSED = "$Id: ntmaigCmd.c,v 1.26 2009/01/18 01:54:51 fabio Exp $";

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

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

static int CommandBuildPartitionMAigs(Hrc_Manager_t ** hmgr, int argc, char ** argv);
static int nodenameCompare(const void * node1, const void * node2);

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


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/
extern void bAig_BuildAigBFSManner( Ntk_Network_t *network, mAig_Manager_t *manager, st_table *leaves, int sweep);
extern void bAig_BddSweepMain(Ntk_Network_t *network, array_t *nodeArray);

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

  Synopsis    [Initializes the network to MAIG package.]

  SideEffects []

  SeeAlso     [ntmaig_End]

******************************************************************************/
void
ntmaig_Init(void)
{
  Cmd_CommandAdd("build_partition_maigs", CommandBuildPartitionMAigs, /* doesn't changes_network */ 0);
}

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

  Synopsis    [Ends the network to MAIG package.]

  SideEffects []

  SeeAlso     [ntmaig_Init]

******************************************************************************/
void
ntmaig_End(void)
{
}

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


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


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

  Synopsis    []

  Description []
  
  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
nodenameCompare(
  const void * node1,
  const void * node2)
{
Ntk_Node_t *v1, *v2;
char *name1, *name2;

  v1 = *(Ntk_Node_t **)(node1);
  v2 = *(Ntk_Node_t **)(node2);
  name1 = Ntk_NodeReadName(v1);
  name2 = Ntk_NodeReadName(v2);
  
  return (strcmp(name1, name2));
} 

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

  Synopsis    [Implements the build_partition_maigs command.]

  Description []
  
  CommandName [build_partition_maigs]

  CommandSynopsis [build a partition of MAIGs for the flattened network]

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

  CommandDescription [
   Build the multi-valued AND/INVERTER graph (MAIG) of a flattened network. 
   It builds the MAIG for the combinational outputs (COs) in terms of the 
   combinational inputs (CIs). The pointer to this graph is stored in the
   network to be used by other commands, such as bounded_model_check.

   This command  must be preceded by the commands flatten_hierarchy. This
   command will remove any previous build to this graph.

   <p>

  Command options:
  <p>

  <dl>

  <dt> -n
  <dd> Disable BDD sweeping.

  <p>
  <dt> -d 
  <dd> Build aig structure in depth first manner.
  <p>
  ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
CommandBuildPartitionMAigs(
  Hrc_Manager_t ** hmgr,
  int  argc,
  char ** argv)
{
  Ntk_Node_t    *node, *latch;
  lsGen          gen;
  array_t       *result; /* array of MvfAig_Function_t* */
  array_t       *roots;
  st_table      *leaves;
  array_t *inputs;
  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
  mAig_Manager_t *manager;
  MvfAig_Function_t  *mvfAig;
  st_table       *nodeToMvfAigTable;  /* mapes each node with its mvfAig */
  int c, sweepFlag, DFSFlag;
  int i;

  sweepFlag = 1;
  DFSFlag = 0;
  util_getopt_reset();
  while ((c = util_getopt(argc,argv,"sdnh")) != EOF){
    switch(c){
      case 's':
	sweepFlag = 1;
	break;
      case 'd':
	DFSFlag = 1;
	break;
      case 'n':
	sweepFlag = 0;
	break;
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }
  if (network == NIL(Ntk_Network_t)) {
    return 1;
  }

  manager = Ntk_NetworkReadMAigManager(network);

  if (manager == NIL(mAig_Manager_t)) {
      manager = mAig_initAig();
      Ntk_NetworkSetMAigManager(network, manager);
      /*
      mAig_mAigSetNetwork(manager, network);
      */
  }

  /* Check if there is already a MvfAigs Table attached to the network */
  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, 
						  MVFAIG_NETWORK_APPL_KEY);

  if (nodeToMvfAigTable != NIL(st_table)){
    /* 
    st_foreach_item(nodeToMvfAigTable, stGen, (char **) &node, (char **) &MvfAig) {
       printf("\nNode name = %s :",Ntk_NodeReadName(node));
       for (j=0; j< array_n(MvfAig); j++){
        printf(" %d ",array_fetch(bAigEdge_t, (array_t *) MvfAig, j));
       }
    }
    */
    (void) fprintf(vis_stderr, "maig partition already built; reinvoke\n");
    (void) fprintf(vis_stderr, "flatten_hierarchy to remove the current maig partition\n");
     return 1;
  }

  roots = array_alloc(Ntk_Node_t *, 0);
  Ntk_NetworkForEachCombOutput(network, gen, node) {
    array_insert_last(Ntk_Node_t *, roots, node);
  }
  Ntk_NetworkForEachNode(network, gen, node) {
    if(Ntk_NodeTestIsShadow(node))	continue;
    if(Ntk_NodeTestIsCombInput(node))	continue;
    if(Ntk_NodeTestIsCombOutput(node))continue;

    if(Ntk_NodeReadNumFanouts(node) == 0 && Ntk_NodeReadNumFanins(node)) {
	/**
      fprintf(vis_stdout, "WARNING : dangling node %s\n", Ntk_NodeReadName(node));
      **/
      array_insert_last(Ntk_Node_t *, roots, node);
    }
  }

  leaves = st_init_table(st_ptrcmp, st_ptrhash);

  inputs = array_alloc(Ntk_Node_t *, 16);
  Ntk_NetworkForEachCombInput(network, gen, node) {
    array_insert_last(Ntk_Node_t *, inputs, node);
  }
  array_sort(inputs, nodenameCompare);
  for(i=0; i<array_n(inputs); i++) {
    node = array_fetch(Ntk_Node_t *, inputs, i);
    st_insert(leaves,  node, (char *) ntmaig_UNUSED);
    Ntk_NodeSetMAigId(node, 
                       mAig_CreateVar(manager,
		                      Ntk_NodeReadName(node),
                                      Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
  }

  if(DFSFlag == 0)
    bAig_BuildAigBFSManner(network, manager, leaves, sweepFlag);

  result = ntmaig_NetworkBuildMvfAigs(network, roots, leaves);

  nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, 
						  MVFAIG_NETWORK_APPL_KEY);
  Ntk_NetworkForEachLatch(network, gen, latch) {
    node  = Ntk_LatchReadDataInput(latch);
    st_lookup(nodeToMvfAigTable, node,  &mvfAig);
    Ntk_NodeSetMAigId(node, 
            mAig_CreateVarFromAig(manager, Ntk_NodeReadName(node), mvfAig));
    node  = Ntk_LatchReadInitialInput(latch);
    st_lookup(nodeToMvfAigTable, node,  &mvfAig);
    Ntk_NodeSetMAigId(node, 
            mAig_CreateVarFromAig(manager, Ntk_NodeReadName(node), mvfAig));
  }

  roots->num = 0;
  Ntk_NetworkForEachLatch(network, gen, latch) {
    if(!st_lookup(nodeToMvfAigTable, latch,  &mvfAig))
      array_insert_last(Ntk_Node_t *, roots, latch);
  }
  result = ntmaig_NetworkBuildMvfAigs(network, roots, leaves);

  array_free(roots);
  array_free(inputs);
  st_free_table(leaves);

  /*
   * Free the array of MvfAigs.
   */
  MvfAig_FunctionArrayFree(result);

  if(sweepFlag) 
    bAig_BddSweepMain(network, 0);
  
  return 0;
  
usage:
  (void) fprintf(vis_stderr, "usage: build_partition_maig [-h]\n");
  (void) fprintf(vis_stderr, "   -h print the command usage\n");
  (void) fprintf(vis_stderr, "   -n disable bdd sweeping\n");
  (void) fprintf(vis_stderr, "   -d build AIG DFS manner\n");
  return 1;		/* error exit */
}