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

  FileName    [baigTimeframe.c]

  PackageName [baig]

  Synopsis    [Functions to manage timeframe expansion.]

  Author      [HoonSang Jin]

  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 "heap.h"
#include "sat.h"
#include "bmc.h"

static char rcsid[] UNUSED = "$ $";

/* #define TIMEFRAME_VERIFY_ */
/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/


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


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


/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

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


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

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

static int nameCompare(const void * node1, const void * node2);
static int NoOfBitEncode(int n);
static bAigEdge_t CaseNew(mAig_Manager_t *manager, bAigEdge_t *arr, array_t * encodeList, int index);

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


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

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

  Synopsis    [Expand timeframe n times]

  Description [Expand timeframe n times. If withInitialState flag is set then 
               unroll transition function considering initial states, otherwise
	       the state variables of 0'th timeframe are free variables]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_ExpandTimeFrame(
	Ntk_Network_t *network,
	mAig_Manager_t *manager,
	int bound,
	int withInitialState)
{
bAigTimeFrame_t *timeframe;
int nLatches, nInputs, nOutputs, nInternals;
int nbLatches, nbInputs;
int i, j;
int index, index1, bindex, tindex;
int mvfSize, lmvfSize;
int lmAigId;
array_t *iindexArray;
MvfAig_Function_t  *mvfAig, *lmvfAig;
bAigEdge_t *li, *bli;
bAigEdge_t *pre_li, *ori_li;
bAigEdge_t v, nv = bAig_NULL;
Ntk_Node_t *node, *latch;
st_table   *node2MvfAigTable, *old2new;
mAigMvar_t lmVar;
mAigBvar_t lbVar;
array_t   *bVarList, *mVarList;
lsGen gen;


  if(withInitialState) timeframe = manager->timeframe;
  else                 timeframe = manager->timeframeWOI;

  if(timeframe == 0) 
    timeframe = bAig_InitTimeFrame(network, manager, withInitialState);

  node2MvfAigTable = 
	(st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);

  nbLatches = timeframe->nbLatches;
  nbInputs = timeframe->nbInputs;
  nLatches = timeframe->nLatches;
  nInputs = timeframe->nInputs;
  nOutputs = timeframe->nOutputs;
  nInternals = timeframe->nInternals;

  iindexArray = timeframe->iindexArray;

  if(bound > timeframe->currentTimeframe) {
    timeframe->latchInputs = (bAigEdge_t **)
	realloc(timeframe->latchInputs, sizeof(bAigEdge_t *)*(bound+2));
    timeframe->inputs = (bAigEdge_t **)
      realloc(timeframe->inputs, sizeof(bAigEdge_t *)*(bound+1));
    timeframe->blatchInputs = (bAigEdge_t **)
	realloc(timeframe->blatchInputs, sizeof(bAigEdge_t *)*(bound+2));
    timeframe->binputs = (bAigEdge_t **)
      realloc(timeframe->binputs, sizeof(bAigEdge_t *)*(bound+1));
    timeframe->outputs = (bAigEdge_t **)
      realloc(timeframe->outputs, sizeof(bAigEdge_t *)*(bound+1));
    timeframe->internals = (bAigEdge_t **)
      realloc(timeframe->internals, sizeof(bAigEdge_t *)*(bound+1));
  }

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);

  for(j=timeframe->currentTimeframe+1; j<=bound; j++) {
    /** create new primary input node **/
    timeframe->inputs = (bAigEdge_t **)
        realloc(timeframe->inputs, sizeof(bAigEdge_t *)*(j+1));
    timeframe->binputs = (bAigEdge_t **)
        realloc(timeframe->binputs, sizeof(bAigEdge_t *)*(j+1));
    bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbInputs);
    timeframe->binputs[j] = bli;
    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
    timeframe->inputs[j] = li;
    index = 0;
    index1 = 0;
    bindex = 0;
    Ntk_NetworkForEachPrimaryInput(network, gen, node) {
      bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);

      st_lookup(node2MvfAigTable, node, &mvfAig);
      mvfSize = array_n(mvfAig);
      for(i=0; i< mvfSize; i++){
        v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
#ifdef TIMEFRAME_VERIFY_
	fprintf(vis_stdout, "IN(%d) %s(%d) : %d -> %d\n", j, Ntk_NodeReadName(node), i, v, li[index1]);
#endif
	index1++;
      }
    }
    Ntk_NetworkForEachPseudoInput(network, gen, node) {
      bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li,  &bindex, &index);

      st_lookup(node2MvfAigTable, node, &mvfAig);
      mvfSize = array_n(mvfAig);
      for(i=0; i< mvfSize; i++){
        v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
#ifdef TIMEFRAME_VERIFY_
	fprintf(vis_stdout, "PI(%d) %s(%d) : %d -> %d\n", j, Ntk_NodeReadName(node), i, v, li[index1]);
#endif
	index1++;
      }
    }

    /** map previous time frame into current **/
    old2new = st_init_table(st_ptrcmp, st_ptrhash);
    pre_li = timeframe->inputs[j];
    ori_li = timeframe->oriInputs;
    for(i=0; i<nInputs; i++)
      st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);

    pre_li = timeframe->latchInputs[j];
    ori_li = timeframe->oriLatchInputs;
    for(i=0; i<nLatches; i++)
      st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);

    pre_li = timeframe->binputs[j];
    ori_li = timeframe->oribInputs;
    for(i=0; i<nbInputs; i++)
      st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);

    pre_li = timeframe->blatchInputs[j];
    ori_li = timeframe->oribLatchInputs;
    for(i=0; i<nbLatches; i++)
      st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);

    /** create new time frame **/
    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
    bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
    timeframe->latchInputs[j+1] = li;
    timeframe->blatchInputs[j+1] = bli;
    bindex = index = 0;
    Ntk_NetworkForEachLatch(network, gen, latch) {
      node  = Ntk_LatchReadDataInput(latch);
      mvfAig = lmvfAig = 0;
      st_lookup(node2MvfAigTable, node, &mvfAig);
      mvfSize = array_n(mvfAig);
      st_lookup(node2MvfAigTable, latch, &lmvfAig);
      lmvfSize = array_n(lmvfAig);
      if(mvfSize != lmvfSize) {
	fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
	fprintf(vis_stdout, "          %s(%d), %s(%d)\n", 
		Ntk_NodeReadName(node), mvfSize, 
		Ntk_NodeReadName(latch), lmvfSize);
        for(i=0; i< mvfSize; i++){
          v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
          nv = bAig_ExpandForEachCone(manager, v, old2new);
          st_insert(old2new, (char *)v, (char *)nv);
          li[index++] = nv;
        }
        for(i=mvfSize; i< lmvfSize; i++){
          li[index++] = nv;
        }
      }
      else {
        for(i=0; i< mvfSize; i++){
          v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
	  /**
	    fprintf(vis_stdout, "-------------------------------\n");
            fprintf(vis_stdout, "      Latch input %d %d\n", v, manager->nodesArraySize);
            fprintf(vis_stdout, "-------------------------------\n");
            bAig_SatRebuildNodeVerifySub(v, manager->NodesArray);
	    **/

          nv = bAig_ExpandForEachCone(manager, v, old2new);
	  flags(nv) |= StateBitMask;
          st_insert(old2new, (char *)v, (char *)nv);
#ifdef TIMEFRAME_VERIFY_
	  fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n", 
		  j+1, Ntk_NodeReadName(latch), i, v, nv);
#endif
          li[index++] = nv;
        }
      }

      lmAigId = Ntk_NodeReadMAigId(node);
      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
      for(i=0, tindex=lmVar.bVars; i<lmVar.encodeLength; i++) {
        lbVar = array_fetch(mAigBvar_t, bVarList, tindex);
	tindex++;
        v = bAig_GetCanonical(manager, lbVar.node);
        nv = bAig_ExpandForEachCone(manager, v, old2new);
        flags(nv) |= StateBitMask;
        st_insert(old2new, (char *)v, (char *)nv);
        bli[bindex++] = nv;
      }
    }

    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nOutputs);
    timeframe->outputs[j] = li;
    index = 0;
    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));

	/**
	  fprintf(vis_stdout, "-------------------------------\n");
          fprintf(vis_stdout, "      Output %d\n", v);
          fprintf(vis_stdout, "-------------------------------\n");
          bAig_SatRebuildNodeVerifySub(v, manager->NodesArray);
	  **/

        nv = bAig_ExpandForEachCone(manager, v, old2new);
        st_insert(old2new, (char *)v, (char *)nv);
#ifdef TIMEFRAME_VERIFY_
	fprintf(vis_stdout, "PO(%d) %s(%d) : %d -> %d\n", j+1, Ntk_NodeReadName(node), i, v, li[index]);
#endif
      st_insert(old2new, (char *)v, (char *)nv);
        li[index++] = nv;
      }
    }
  
    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInternals);
    timeframe->internals[j] = li;
    for(i=0; i<array_n(iindexArray); i++) {
      v = array_fetch(bAigEdge_t, iindexArray, i);
      nv = bAig_ExpandForEachCone(manager, v, old2new);
      st_insert(old2new, (char *)v, (char *)nv);
      li[i] = nv;
    }
    st_free_table(old2new);
  }

  timeframe->currentTimeframe = bound;
}

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

  Synopsis    [Compare function for name ordering]

  Description [Compare function for name ordering]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
nameCompare(
  const void * node1,
  const void * node2)
{
  char *name1, *name2;
  
  name1 = Ntk_NodeReadName((Ntk_Node_t *)node1);
  name2 = Ntk_NodeReadName((Ntk_Node_t *)node2);
  return(strcmp(*(char**)name1, *(char **)name2));

} 


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

  Synopsis    [Make first timeframe]

  Description [Make first timeframe]

  SideEffects []

  SeeAlso     []

******************************************************************************/
bAigTimeFrame_t *
bAig_InitTimeFrame(
	Ntk_Network_t *network,
	mAig_Manager_t *manager,
	int withInitialState)
{
bAigTimeFrame_t *timeframe;
array_t *latchArr, *inputArr, *outputArr;
array_t *iindexArray;
st_table   *li2index, *o2index, *i2index, *pi2index;
st_table   *bli2index, *bpi2index;
Ntk_Node_t *node, *latch;
st_table   *node2MvfAigTable, *old2new;
lsGen gen;
int nLatches, nInputs, nOutputs, nInternals;
int nbLatches, nbInputs;
int i;
int index, index1, mvfSize, lmvfSize;
int bindex, tindex, tindex1;
MvfAig_Function_t  *mvfAig, *tmpMvfAig, *lmvfAig;
bAigEdge_t *li, *pre_li, *ori_li;
bAigEdge_t *bli, *ori_bli;
bAigEdge_t v=bAig_NULL, nv;
mAigMvar_t mVar;
mAigBvar_t bVar;
array_t   *bVarList, *mVarList;
int mAigId;
int lmAigId;
mAigMvar_t lmVar;
mAigBvar_t lbVar;

  node2MvfAigTable = 
	(st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);

  timeframe = ALLOC(bAigTimeFrame_t, 1);
  memset(timeframe, 0, sizeof(bAigTimeFrame_t));
  if(withInitialState) manager->timeframe = timeframe;
  else                 manager->timeframeWOI = timeframe;

  latchArr = array_alloc(Ntk_Node_t *, 0);
  inputArr = array_alloc(Ntk_Node_t *, 0);
  outputArr = array_alloc(Ntk_Node_t *, 0);
  timeframe->latchArr = latchArr;
  timeframe->inputArr = inputArr;
  timeframe->outputArr = outputArr;

  li2index = st_init_table(st_ptrcmp, st_ptrhash);
  o2index = st_init_table(st_ptrcmp, st_ptrhash);
  i2index = st_init_table(st_ptrcmp, st_ptrhash);
  pi2index = st_init_table(st_ptrcmp, st_ptrhash);

  bli2index = st_init_table(st_ptrcmp, st_ptrhash);
  bpi2index = st_init_table(st_ptrcmp, st_ptrhash);

  timeframe->li2index = li2index;
  timeframe->o2index = o2index;
  timeframe->pi2index = pi2index;
  timeframe->i2index = i2index;

  timeframe->bli2index = bli2index;
  timeframe->bpi2index = bpi2index;
  /** 
   * count total number, 
   * insert into node array 
   * and make table for bAigEdge_t to index
   **/

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);

  nLatches = 0;
  nbLatches = 0;
  Ntk_NetworkForEachLatch(network, gen, latch) {
    array_insert_last(Ntk_Node_t *, latchArr, latch);
    st_lookup(node2MvfAigTable, latch, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
      st_insert(li2index, (char *)v, (char *)(long)nLatches++);
    }

    mAigId = Ntk_NodeReadMAigId(latch);
    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
      bVar = array_fetch(mAigBvar_t, bVarList, index1);
      st_insert(bli2index, (char *)bVar.node, (char *)(long)nbLatches++);
      index1++;
    }
  }
  timeframe->nLatches = nLatches;
  timeframe->nbLatches = nbLatches;

  nOutputs = 0;
  Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
    array_insert_last(Ntk_Node_t *, outputArr, node);
    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
      st_insert(o2index, (char *)(long)v, (char *)(long)nOutputs++);
    }
  }
  timeframe->nOutputs = nOutputs;

  timeframe->iindexArray = iindexArray = array_alloc(bAigEdge_t, 0);
  nInternals = 0;
  Ntk_NetworkForEachNode(network, gen, node) {
    if(Ntk_NodeTestIsShadow(node))	continue;
    if(Ntk_NodeTestIsCombInput(node))	continue;
    if(Ntk_NodeTestIsCombOutput(node))continue;
    if(!st_lookup(node2MvfAigTable, node, &mvfAig)) {
      tmpMvfAig = Bmc_NodeBuildMVF(network, node);
      array_free(tmpMvfAig);
      mvfAig = Bmc_ReadMvfAig(node, node2MvfAigTable);
    }
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
      if(!st_lookup(i2index, (char *)v, &index1)) {
	array_insert_last(bAigEdge_t, iindexArray, v);
	st_insert(i2index, (char *)v, (char *)(long)nInternals++);
      }
    }
#ifdef TIMEFRAME_VERIFY_
      if(!strcmp(Ntk_NodeReadName(node), "v25") ||
	 !strcmp(Ntk_NodeReadName(node), "v27")) {
	  fprintf(stdout, "current error %d %d\n", v, nInternals);
      }
#endif
  }
  timeframe->nInternals = nInternals;

  nInputs = 0;
  nbInputs = 0;
  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
    array_insert_last(Ntk_Node_t *, inputArr, node);
    if(!st_lookup(node2MvfAigTable, node, &mvfAig)) {
      tmpMvfAig = Bmc_NodeBuildMVF(network, node);
      array_free(tmpMvfAig);
      mvfAig = Bmc_ReadMvfAig(node, node2MvfAigTable);
    }
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
	st_insert(pi2index, (char *)(long)v, (char *)(long)nInputs++);
    }

    mAigId = Ntk_NodeReadMAigId(node);
    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
      bVar = array_fetch(mAigBvar_t, bVarList, index1);
      st_insert(bpi2index, (char *)bVar.node, (char *)(long)nbInputs++);
      index1++;
    }
  }
  Ntk_NetworkForEachPseudoInput(network, gen, node)  {
    array_insert_last(Ntk_Node_t *, inputArr, node);
    if(!st_lookup(node2MvfAigTable, node, &mvfAig)) {
      tmpMvfAig = Bmc_NodeBuildMVF(network, node);
      array_free(tmpMvfAig);
      mvfAig = Bmc_ReadMvfAig(node, node2MvfAigTable);
    }
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
	st_insert(pi2index, (char *)(long)v, (char *)(long)nInputs++);
    }

    mAigId = Ntk_NodeReadMAigId(node);
    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
      bVar = array_fetch(mAigBvar_t, bVarList, index1);
      st_insert(bpi2index, (char *)bVar.node, (char *)(long)nbInputs++);
      index1++;
    }
  }
  timeframe->nInputs = nInputs;
  timeframe->nbInputs = nbInputs;

  array_sort(inputArr, nameCompare);
  array_sort(latchArr, nameCompare);
  array_sort(outputArr, nameCompare);

    /** make 0 index bAigEdge_t **/
  old2new = st_init_table(st_ptrcmp, st_ptrhash);
  bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbInputs);
  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
  index1 = index = 0;
  bindex = 0;
  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
    bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);

    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
#ifdef TIMEFRAME_VERIFY_
      fprintf(vis_stdout, "IN(%d) %s(%d) : %d -> %d\n", -1, Ntk_NodeReadName(node), i, v, li[index1]);
#endif
      st_insert(old2new, (char *)v, (char *)(li[index1++]));
    }
  }
  Ntk_NetworkForEachPseudoInput(network, gen, node) {
    bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);

    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
#ifdef TIMEFRAME_VERIFY_
      fprintf(vis_stdout, "PI(%d) %s(%d) : %d -> %d\n", -1, Ntk_NodeReadName(node), i, v, li[index1]);
#endif
      st_insert(old2new, (char *)v, (char *)(li[index1++]));
    }
  }

  timeframe->blatchInputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *)*(2));
  bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
  timeframe->blatchInputs[0] = bli;

  timeframe->latchInputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *)*(2));
  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
  timeframe->latchInputs[0] = li;

  ori_li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
  ori_bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
  timeframe->oriLatchInputs = ori_li;
  timeframe->oribLatchInputs = ori_bli;

  index1 = index = 0;
  bindex = tindex = tindex1 = 0;

  if(withInitialState == 0) {
    Ntk_NetworkForEachLatch(network, gen, latch) {
      bAig_CreateNewNode(manager, node2MvfAigTable, latch, bli, li, &bindex, &index);

      st_lookup(node2MvfAigTable, latch, &mvfAig);
      mvfSize = array_n(mvfAig);
      for(i=0; i< mvfSize; i++){
        v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
        st_insert(old2new, (char *)v, (char *)(li[index1]));
  #ifdef TIMEFRAME_VERIFY_
	fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(latch), i, v, li[index1]);
  #endif
	ori_li[index1++] = v;
      }

      lmAigId = Ntk_NodeReadMAigId(latch);
      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
	tindex1++;
        v = bAig_GetCanonical(manager, lbVar.node);
	ori_bli[tindex++] = v ;
      }
    }
  }
  else {
    Ntk_NetworkForEachLatch(network, gen, latch) {
      node  = Ntk_LatchReadInitialInput(latch);
      mvfAig = lmvfAig = 0;
      st_lookup(node2MvfAigTable, node, &mvfAig);
      mvfSize = array_n(mvfAig);
      if(!st_lookup(node2MvfAigTable, latch, &lmvfAig)) {
        tmpMvfAig = Bmc_NodeBuildMVF(network, latch);
        array_free(tmpMvfAig);
        lmvfAig = Bmc_ReadMvfAig(latch, node2MvfAigTable);
      }
      lmvfSize = array_n(lmvfAig);
      if(mvfSize != lmvfSize) {
	  fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
	  fprintf(vis_stdout, "          %s(%d), %s(%d)\n", 
		  Ntk_NodeReadName(node), mvfSize, 
		  Ntk_NodeReadName(latch), lmvfSize);
        for(i=0; i< mvfSize; i++){
          v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
          nv = bAig_ExpandForEachCone(manager, v, old2new);
          st_insert(old2new, (char *)v, (char *)nv);
	    li[index++] = nv;
        }
        for(i=mvfSize; i<lmvfSize; i++) {
          nv = bAig_ExpandForEachCone(manager, v, old2new);
          st_insert(old2new, (char *)v, (char *)nv);
	    li[index++] = nv;
        }
      }
      else {
        for(i=0; i< mvfSize; i++){
          v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
          nv = bAig_ExpandForEachCone(manager, v, old2new);
          st_insert(old2new, (char *)v, (char *)nv);
	    li[index++] = nv;
        }
      }
      for(i=0; i< lmvfSize; i++){
        v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(lmvfAig, i));
  #ifdef TIMEFRAME_VERIFY_
	  fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(latch), i, v, li[index1]);
  #endif
	  ori_li[index1++] = v;
      }
      lmAigId = Ntk_NodeReadMAigId(latch);
      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
	tindex1++;
        v = bAig_GetCanonical(manager, lbVar.node);
	ori_bli[tindex++]  = v;
      }
      node  = Ntk_LatchReadInitialInput(latch);
      lmAigId = Ntk_NodeReadMAigId(node);
      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
	tindex1++;
        v = bAig_GetCanonical(manager, lbVar.node);
        if(st_lookup(old2new, (char *)v, &nv))
	  bli[bindex++]  = nv;
	else
	  bli[bindex++]  = v;
      }
    }
  }
  st_free_table(old2new);

  timeframe->binputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
  bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbInputs);
  timeframe->binputs[0] = bli;

  timeframe->inputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
  ori_li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
  ori_bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
  timeframe->inputs[0] = li;
  timeframe->oriInputs = ori_li;
  timeframe->oribInputs = ori_bli;
  index1 = index = 0;
  tindex = bindex = tindex1 = 0;
  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
    bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);

    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
#ifdef TIMEFRAME_VERIFY_
	fprintf(vis_stdout, "IN(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(node), i, v, li[index1]);
#endif
	ori_li[index1++] = v;
    }
    lmAigId = Ntk_NodeReadMAigId(node);
    lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
    for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
      lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
      tindex1++;
      v = bAig_GetCanonical(manager, lbVar.node);
      ori_bli[tindex++] = v;
    }
  }
  Ntk_NetworkForEachPseudoInput(network, gen, node) {
    bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);

    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
#ifdef TIMEFRAME_VERIFY_
	fprintf(vis_stdout, "PI(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(node), i, v, li[index1]);
#endif
	ori_li[index1++] = v;
    }
    lmAigId = Ntk_NodeReadMAigId(node);
    lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
    for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
      lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
      tindex1++;
      v = bAig_GetCanonical(manager, lbVar.node);
      ori_bli[tindex++] = v;
    }
  }

    /** map node of previous timeframe into current timeframe **/
  old2new = st_init_table(st_ptrcmp, st_ptrhash);
  pre_li = timeframe->inputs[0];
  ori_li = timeframe->oriInputs;
  for(i=0; i<nInputs; i++)
    st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
  pre_li = timeframe->latchInputs[0];
  ori_li = timeframe->oriLatchInputs;
  for(i=0; i<nLatches; i++)
    st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);

  pre_li = timeframe->binputs[0];
  ori_li = timeframe->oribInputs;
  for(i=0; i<nbInputs; i++)
    st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
  pre_li = timeframe->blatchInputs[0];
  ori_li = timeframe->oribLatchInputs;
  for(i=0; i<nbLatches; i++)
    st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);

    /** create timeframe **/
  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
  timeframe->latchInputs[1] = li;
  bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
  timeframe->blatchInputs[1] = bli;
  bindex = index = 0;
  Ntk_NetworkForEachLatch(network, gen, latch) {
    node  = Ntk_LatchReadDataInput(latch);
    mvfAig = lmvfAig = 0;
    st_lookup(node2MvfAigTable, node, &mvfAig);
    mvfSize = array_n(mvfAig);
    st_lookup(node2MvfAigTable, latch, &lmvfAig);
    lmvfSize = array_n(lmvfAig);
    if(mvfSize != lmvfSize) {
	fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
	fprintf(vis_stdout, "          %s(%d), %s(%d)\n", 
		Ntk_NodeReadName(node), mvfSize, 
		Ntk_NodeReadName(latch), lmvfSize);
      for(i=0; i< mvfSize; i++){
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
        nv = bAig_ExpandForEachCone(manager, v, old2new);
        st_insert(old2new, (char *)v, (char *)nv);
        li[index++] = nv;
      }
      for(i=mvfSize; i< lmvfSize; i++){
        li[index++] = nv;
      }
    }
    else {
      for(i=0; i< mvfSize; i++){
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
        nv = bAig_ExpandForEachCone(manager, v, old2new);
/*	flags(nv) |= StateBitMask; */
        st_insert(old2new, (char *)v, (char *)nv);
#ifdef TIMEFRAME_VERIFY_
	fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n", 
		  1, Ntk_NodeReadName(latch), i, v, nv);
#endif
        li[index++] = nv;
      }
    }
    /* State bit mapping **/
    lmAigId = Ntk_NodeReadMAigId(node);
    lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
    for(i=0, tindex=lmVar.bVars; i<lmVar.encodeLength; i++) {
      lbVar = array_fetch(mAigBvar_t, bVarList, tindex);
      tindex++;
      v = bAig_GetCanonical(manager, lbVar.node);
      nv = bAig_ExpandForEachCone(manager, v, old2new);
      flags(nv) |= StateBitMask;
      st_insert(old2new, (char *)v, (char *)nv);
      bli[bindex++] = nv;
    }

  }

  timeframe->outputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nOutputs);
  timeframe->outputs[0] = li;
  index = 0;
  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));
      nv = bAig_ExpandForEachCone(manager, v, old2new);
#ifdef TIMEFRAME_VERIFY_
	fprintf(vis_stdout, "PO(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(node), i, v, li[index]);
#endif
      st_insert(old2new, (char *)v, (char *)nv);
      li[index++] = nv;
    }
  }

  index = 0;
  timeframe->internals = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInternals);
  timeframe->internals[0] = li;
  for(i=0; i<array_n(iindexArray); i++) {
    v = array_fetch(bAigEdge_t, iindexArray, i);
    nv = bAig_ExpandForEachCone(manager, v, old2new);
    st_insert(old2new, (char *)v, (char *)nv);
    li[i] = nv;
  }
  st_free_table(old2new);

  timeframe->currentTimeframe = 0;

  return(timeframe);

}

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

  Synopsis    [Create aig node for free variables]

  Description [Create aig node for free variables, 
               such as primary input and pseudo input]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_CreateNewNode(
	mAig_Manager_t *manager, 
	st_table *node2MvfAigTable,
	Ntk_Node_t *node, 
	bAigEdge_t *bli,
	bAigEdge_t *li,
	int *bindex, 
	int *index)
{
  int i, j, value, noBits;
  bAigEdge_t *arr, v, tv;
  MvfAig_Function_t  *mvfAig;
  array_t *encodeList;
  bAigEdge_t *ManagerNodesArray;
  bAigTimeFrame_t *timeframe;
 
  timeframe = manager->timeframe;

  value = Var_VariableReadNumValues(Ntk_NodeReadVariable(node));
  noBits = NoOfBitEncode(value);
  arr = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*noBits);
  mvfAig = 0;
  st_lookup(node2MvfAigTable, node, &mvfAig);
  for(i=0; i<noBits; i++) {
    arr[i] = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
    bli[(*bindex)++] = arr[i];

    flags(arr[i]) |= IsSystemMask;
  }

  for(i=0; i<value; i++) {
    v = MvfAig_FunctionReadComponent(mvfAig, i);
    /**
    if(v == bAig_Zero)		li[(*index)++] = bAig_Zero;
    else if(v == bAig_One)	li[(*index)++] = bAig_One;
    else {
    }
    **/
      encodeList = array_alloc(bAigEdge_t, 0);
      for(j=0; j<value; j++) {
        if(j == i)array_insert_last(bAigEdge_t, encodeList, mAig_One);
        else	array_insert_last(bAigEdge_t, encodeList, mAig_Zero);
      }
      tv = CaseNew(manager, arr, encodeList, noBits-1);
      li[(*index)++] = tv;

      ManagerNodesArray = manager->NodesArray;

      array_free(encodeList);
      if(v == bAig_Zero){
	flags(tv) |= StaticLearnMask;
	if(timeframe->assertedArray == 0)
	  timeframe->assertedArray = array_alloc(bAigEdge_t, 0);
	array_insert_last(bAigEdge_t, timeframe->assertedArray, bAig_Not(tv));
      }
      else if(v == bAig_One){
	flags(tv) |= StaticLearnMask;
	if(timeframe->assertedArray == 0)
	  timeframe->assertedArray = array_alloc(bAigEdge_t, 0);
	array_insert_last(bAigEdge_t, timeframe->assertedArray, tv);
      }
  }
  free(arr);
}
    
/**Function********************************************************************

  Synopsis    [Compute bits is needed for encode n]

  Description [Compute bits is needed for encode n]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static int
NoOfBitEncode( int n)
{
  int i = 0;
  int j = 1;

  if (n < 2) return 1; /* Takes care of mv.values <= 1 */

  while (j < n) {
    j = j * 2;
    i++;
  }
  return i;
}

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

  Synopsis    [Extract bit from multi valued array]

  Description [Extract bit from multi valued array]

  SideEffects []

  SeeAlso     []

******************************************************************************/
static bAigEdge_t 
CaseNew(mAig_Manager_t *manager,
  bAigEdge_t      *arr,
  array_t *       encodeList,
  int             index) 
{
  int encodeLen;
  int i, count;
  bAigEdge_t v;
  bAigEdge_t    andResult1, andResult2, orResult, result;
  bAigEdge_t    node1, node2;
  array_t *newEncodeList;

  encodeLen = array_n(encodeList);
  if (encodeLen == 1)
    return array_fetch(bAigEdge_t, encodeList, 0);
  newEncodeList =  array_alloc(bAigEdge_t, 0);

  v = arr[index];
  count = 0;
  for (i=0; i< (encodeLen/2); i++){
    node1 = array_fetch(bAigEdge_t, encodeList, count++);
    node2 = array_fetch(bAigEdge_t, encodeList, count++);
  
     /*  performs ITE operator */
    andResult1 = bAig_And(manager, v,           node2);
    andResult2 = bAig_And(manager, bAig_Not(v), node1);
    orResult   = bAig_Or (manager, andResult1,  andResult2);
    flags(andResult1) |= IsSystemMask;
    flags(andResult2) |= IsSystemMask;
    flags(orResult) |= IsSystemMask;
    
    array_insert_last(bAigEdge_t, newEncodeList, orResult);
  }

  if(encodeLen%2){
    node1 = array_fetch(bAigEdge_t, encodeList, count);
    array_insert_last(bAigEdge_t, newEncodeList, node1);
  }

  result = CaseNew(manager, arr, newEncodeList, index-1);
  array_free(newEncodeList);
  return(result);
}

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

  Synopsis    [Expand timeframe for aig node ]

  Description [Expand timeframe for aig node ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
bAigEdge_t 
bAig_ExpandForEachCone(
	mAig_Manager_t *manager,
	bAigEdge_t v,
	st_table *old2new)
{
  bAigEdge_t left, right, nv;

  v = bAig_GetCanonical(manager, v);
  if(v == bAig_One || v == bAig_Zero)	return(v);
  if(v == bAig_NULL)	{
      fprintf(vis_stdout, "current error\n");
      return(v);
  }


  if(st_lookup(old2new, (char *)v, &nv))
    return(nv);
  if(st_lookup(old2new, (char *)bAig_Not(v), &nv))
    return(bAig_Not(nv));

  left = bAig_ExpandForEachCone(manager, leftChild(v), old2new);
  right = bAig_ExpandForEachCone(manager, rightChild(v), old2new);

  nv = bAig_And(manager, left, right);

  flags(nv) |= IsSystemMask;
  
  if(bAig_IsInverted(v))	nv = bAig_Not(nv);
  st_insert(old2new, (char *)v, (char *)nv);

  return(nv);

}



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

  Synopsis    [Check connectivity between aig nodes]

  Description [Check connectivity between aig nodes]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_CheckConnect(
	bAig_Manager_t *manager,
	int from, int to)
{
int reached;

  reached = bAig_CheckConnectFanin(manager, from, leftChild(to));
  if(reached == 0)
    reached = bAig_CheckConnectFanin(manager, from, rightChild(to));

  if(reached == 0)
    fprintf(stdout, "Node %d is not (backward) reachable from node %d\n",
	    from, to);

  reached = bAig_CheckConnectFanout(manager, from, to);
  if(reached == 0)
    fprintf(stdout, "Node %d is not (forward) reachable from node %d\n",
	    to, from);

}


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

  Synopsis    [Check connectivity of each fanin aig nodes]

  Description [Check connectivity of each fanin aig nodes]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
bAig_CheckConnectFanin(bAig_Manager_t *manager,
	int from, int to)
{
int left, right;
int reached;

  if(bAig_NonInvertedEdge(from) == bAig_NonInvertedEdge(to))
    return(1);

  left = leftChild(to);
  if(left == 2)	
    return(0);

  right = leftChild(to);


  reached = bAig_CheckConnectFanin(manager, from, left);
  if(reached == 1)
    return(1);
  reached = bAig_CheckConnectFanin(manager, from, right);
  if(reached == 1)
    return(1);

  return(0);
}

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

  Synopsis    [Check connectivity of each fanout aig nodes]

  Description [Check connectivity of each fanout aig nodes]

  SideEffects []

  SeeAlso     []

******************************************************************************/
int
bAig_CheckConnectFanout(bAig_Manager_t *manager,
	int from, int to)
{
long *pfan, cur;
int size, j;
int reached;

  size = nFanout(from);
  for(j=0, pfan = (bAigEdge_t *)fanout(from); j<size; j++) {
    cur = pfan[j];
    cur = cur >> 1;
    reached = bAig_CheckConnectFanout(manager, cur, to);
    if(reached == 1)
      return(1);
  }
  return(0);
}

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

  Synopsis    [Get cone of influence nodes of given aig node]

  Description [Get cone of influence nodes of given aig node]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_GetCOIForNode(Ntk_Node_t *node, st_table *table)
{
int i;
Ntk_Node_t *faninNode;

  if(node == NIL(Ntk_Node_t)){
    return;
  }
  if (Ntk_NodeTestIsLatch(node)){
    st_insert(table, (char *)node, (char *)node);
    return;
  }

  Ntk_NodeForEachFanin(node, i, faninNode) {
    bAig_GetCOIForNode(faninNode, table);
  }
  return;
}

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

  Synopsis    [Print cone of influence nodes of given aig node]

  Description [Print cone of influence nodes of given aig node]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_GetCOIForNodeMain(Ntk_Network_t * network, char *name)
{
int i, found;
Ntk_Node_t *node, *faninNode;
lsGen gen;
st_generator *gen1;
st_table *table;

  node = Ntk_NetworkFindNodeByName(network, name);
  if(node == 0) {
    found = 0;
    Ntk_NetworkForEachNode(network, gen, node) {
      if(!strcmp(Ntk_NodeReadName(node), name)) {
	found = 1;
	break;
      }
    }

    if(found == 0)
      node = 0;
  }
  
  if(node == NIL(Ntk_Node_t)){
    return;
  }
  if (Ntk_NodeTestIsLatch(node)){
    fprintf(stdout, "%s\n", Ntk_NodeReadName(node));
    return;
  }

  table = st_init_table(st_ptrcmp, st_ptrhash);

  Ntk_NodeForEachFanin(node, i, faninNode) {
    bAig_GetCOIForNode(faninNode, table);
  }

  st_foreach_item(table, gen1, &node, &node) {
    fprintf(stdout, "%s\n", Ntk_NodeReadName(node));
  }

  st_free_table(table);
  return;
}


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

  Synopsis    [Check status of latch]

  Description [Check status of latch]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_CheckLatchStatus(Ntk_Network_t * network, bAig_Manager_t *manager)
{
Ntk_Node_t *node; 
Ntk_Node_t *data, *init;
lsGen gen;
mAigMvar_t lmVar;
mAigBvar_t lbVar;
int tindex1, v, i, lmAigId;
array_t   *mVarList, *bVarList;

  mVarList = mAigReadMulVarList(manager);
  bVarList = mAigReadBinVarList(manager);
  Ntk_NetworkForEachNode(network, gen, node) {
    if(Ntk_NodeTestIsPrimaryInput(node)) {
      fprintf(stdout, "Primary I %s :", Ntk_NodeReadName(node));
      lmAigId = Ntk_NodeReadMAigId(node);
      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
        v = bAig_GetCanonical(manager, lbVar.node);
	fprintf(stdout, "%d ", v);
      }
      fprintf(stdout, "\n");
    }
  }
  Ntk_NetworkForEachNode(network, gen, node) {
    if(Ntk_NodeTestIsPseudoInput(node)) {
      fprintf(stdout, "Pseudo I %s :", Ntk_NodeReadName(node));
      lmAigId = Ntk_NodeReadMAigId(node);
      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
        v = bAig_GetCanonical(manager, lbVar.node);
	fprintf(stdout, "%d ", v);
      }
      fprintf(stdout, "\n");
    }
  }
  Ntk_NetworkForEachNode(network, gen, node) {
    if (Ntk_NodeTestIsLatch(node)){
      fprintf(stdout, "Latch %s :", Ntk_NodeReadName(node));
      lmAigId = Ntk_NodeReadMAigId(node);
      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
        v = bAig_GetCanonical(manager, lbVar.node);
	fprintf(stdout, "%d ", v);
      }
      fprintf(stdout, "\n");

      data  = Ntk_LatchReadDataInput(node);
      fprintf(stdout, "  data input %s :", Ntk_NodeReadName(data));
      lmAigId = Ntk_NodeReadMAigId(data);
      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
        v = bAig_GetCanonical(manager, lbVar.node);
	fprintf(stdout, "%d ", v);
      }
      fprintf(stdout, "\n");

      init = Ntk_LatchReadInitialInput(node);
      fprintf(stdout, "  latch init %s :", Ntk_NodeReadName(init));
      lmAigId = Ntk_NodeReadMAigId(init);
      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
        v = bAig_GetCanonical(manager, lbVar.node);
	fprintf(stdout, "%d ", v);
      }
      fprintf(stdout, "\n");
    }
  }
  Ntk_NetworkForEachNode(network, gen, node) {
    lmAigId = Ntk_NodeReadMAigId(node);
    if(lmAigId == 2 || lmAigId == 0) {
      fprintf(stdout, "node aig id %s\n", Ntk_NodeReadName(node));
    }
  }
}

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

  Synopsis    [Print status of aig node]

  Description [Print status of aig node]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_PrintNodeAigStatus(bAig_Manager_t *manager, Ntk_Node_t *node)
{
mAigMvar_t lmVar;
mAigBvar_t lbVar;
int tindex1, v, i, lmAigId;
array_t   *mVarList, *bVarList;

  mVarList = mAigReadMulVarList(manager);
  bVarList = mAigReadBinVarList(manager);
  fprintf(stdout, "node %s :", Ntk_NodeReadName(node));
  lmAigId = Ntk_NodeReadMAigId(node);
  lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
  for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
    lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
    v = bAig_GetCanonical(manager, lbVar.node);
    fprintf(stdout, "%d ", v);
  }
  fprintf(stdout, "\n");
}

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

  Synopsis    [Check status of aig node]

  Description [Check status of aig node]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_PrintNodeAigStatusWithName(Ntk_Network_t * network, bAig_Manager_t *manager, char *name)
{
Ntk_Node_t *node;

  node = Ntk_NetworkFindNodeByName(network, name);
  bAig_PrintNodeAigStatus(manager, node);
}

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

  Synopsis    [ Free timeframe ]

  Description [ Free timeframe ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
void
bAig_FreeTimeFrame(bAigTimeFrame_t * timeframe)
{
int i; 
long *li;

   if(timeframe == 0)	return;

   if(timeframe->li2index)	st_free_table(timeframe->li2index);
   if(timeframe->o2index)	st_free_table(timeframe->o2index);
   if(timeframe->i2index)	st_free_table(timeframe->i2index);
   if(timeframe->pi2index)	st_free_table(timeframe->pi2index);
   if(timeframe->latchArr)	array_free(timeframe->latchArr);
   if(timeframe->inputArr)	array_free(timeframe->inputArr);
   if(timeframe->outputArr)	array_free(timeframe->outputArr);
   if(timeframe->iindexArray)	array_free(timeframe->iindexArray);
   if(timeframe->assertedArray)	array_free(timeframe->assertedArray);
   if(timeframe->oriLatchInputs)free(timeframe->oriLatchInputs);
   if(timeframe->oriInputs)     free(timeframe->oriInputs);
   if(timeframe->oribLatchInputs)free(timeframe->oribLatchInputs);
   if(timeframe->oribInputs)     free(timeframe->oribInputs);

   if(timeframe->inputs) {
     for(i=0; i<timeframe->currentTimeframe; i++) {
	li = timeframe->inputs[i];
	if(li)	free(li);
     }
     free(timeframe->inputs);
   }
   if(timeframe->binputs) {
     for(i=0; i<timeframe->currentTimeframe; i++) {
	li = timeframe->binputs[i];
	if(li)	free(li);
     }
     free(timeframe->binputs);
   }
   if(timeframe->outputs) {
     for(i=0; i<timeframe->currentTimeframe; i++) {
	li = timeframe->outputs[i];
	if(li)	free(li);
     }
     free(timeframe->outputs);
   }
   if(timeframe->latchInputs) {
     for(i=0; i<timeframe->currentTimeframe; i++) {
	li = timeframe->latchInputs[i];
	if(li)	free(li);
     }
     free(timeframe->latchInputs);
   }
   if(timeframe->blatchInputs) {
     for(i=0; i<timeframe->currentTimeframe; i++) {
	li = timeframe->blatchInputs[i];
	if(li)	free(li);
     }
     free(timeframe->blatchInputs);
   }
   if(timeframe->internals) {
     for(i=0; i<timeframe->currentTimeframe; i++) {
	li = timeframe->internals[i];
	if(li)	free(li);
     }
     free(timeframe->internals);
   }
}