src/puresat/puresatTFrame.c

Go to the documentation of this file.

#include "puresatInt.h"


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

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

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

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

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

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

static int nameCompare(const void * node1, const void * node2);
static int NoOfBitEncode( int n);


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

bAigEdge_t
PureSat_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 = PureSat_And(manager, v,           node2);
    andResult2 = PureSat_And(manager, bAig_Not(v), node1);
    orResult   = PureSat_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 = PureSat_CaseNew(manager, arr, newEncodeList, index-1);
  array_free(newEncodeList);
  return(result);
}

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


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

  value = Var_VariableReadNumValues(Ntk_NodeReadVariable(node));
  noBits = NoOfBitEncode(value);
  arr = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*noBits);
  mvfAig = 0;
  st_lookup(node2MvfAigTable, (char *) 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);

    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 = PureSat_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);
}

bAigEdge_t
PureSat_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 = PureSat_ExpandForEachCone(manager, leftChild(v), old2new);
  right = PureSat_ExpandForEachCone(manager, rightChild(v), old2new);

  nv = PureSat_And(manager, left, right);

  flags(nv) |= IsSystemMask;

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


  return(nv);

}

bAigTimeFrame_t *
bAig_PureSat_InitTimeFrame(
        Ntk_Network_t *network,
        mAig_Manager_t *manager,
        PureSat_Manager_t *pm,
        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, nv;
mAigMvar_t mVar;
mAigBvar_t bVar;
array_t   *bVarList, *mVarList;
int mAigId;
int lmAigId;
mAigMvar_t lmVar;
mAigBvar_t lbVar;

bAigEdge_t vi, tmpv1, tmpv2,tmpv3;
char * name, *name1;
int imvfSize;
st_table *idx2name,*MultiLatchTable,*table;

  manager->class_ = 1;

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

  idx2name = st_init_table(st_ptrcmp,st_ptrhash);
  timeframe->idx2name = idx2name;
  MultiLatchTable = st_init_table(st_ptrcmp,st_ptrhash);
  timeframe->MultiLatchTable = MultiLatchTable;

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

  timeframe->bli2index = bli2index;
  timeframe->bpi2index = bpi2index;
  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);

  nLatches = 0;
  nbLatches = 0;
  Ntk_NetworkForEachLatch(network, gen, latch) {

    name = Ntk_NodeReadName(latch);
    array_insert_last(Ntk_Node_t *, latchArr, latch);
    st_lookup(node2MvfAigTable, (char *)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++);

#ifdef TIMEFRAME_VERIFY_
      fprintf(vis_stdout,"Latch:%s v-->idx:%d-->%d\n",name,v,nLatches-1);
#endif
    }


    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, (char *)node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
      st_insert(o2index, (char *)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, (char *)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++);
      }
    }
  }
  timeframe->nInternals = nInternals;

  nInputs = 0;
  nbInputs = 0;
  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
    array_insert_last(Ntk_Node_t *, inputArr, node);
    if(!st_lookup(node2MvfAigTable, (char *)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 *)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, (char *)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 *)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);

  manager->SymbolTableArray[0] = st_init_table(strcmp,st_strhash);
  manager->HashTableArray[0] = ALLOC(bAigEdge_t, bAig_HashTableSize);
  for (i=0; i<bAig_HashTableSize; i++)
       manager->HashTableArray[0][i]= bAig_NULL;
  manager->SymbolTableArray[1] = st_init_table(strcmp,st_strhash);
  manager->HashTableArray[1] = ALLOC(bAigEdge_t, bAig_HashTableSize);
  for (i=0; i<bAig_HashTableSize; i++)
       manager->HashTableArray[1][i]= bAig_NULL;

  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) {

    PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);

    st_lookup(node2MvfAigTable, (char *) 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) {

    PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);

    st_lookup(node2MvfAigTable, (char *) 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) {
    manager->InitState = bAig_One;
    Ntk_NetworkForEachLatch(network, gen, latch) {

      manager->class_ = 0;

      PureSat_CreateNewNode(manager, node2MvfAigTable, latch, bli, li, &bindex, &index,withInitialState);
      node =  Ntk_LatchReadInitialInput(latch);
      st_lookup(node2MvfAigTable,(char*)node,&tmpMvfAig);

      st_lookup(node2MvfAigTable, (char *) latch, &mvfAig);
      mvfSize = array_n(mvfAig);
      imvfSize = array_n(tmpMvfAig);
      if(mvfSize!=imvfSize){
        fprintf(vis_stdout,"mvfSize:%d!=imvSize:%d, exit\n",mvfSize, imvfSize);
        exit(0);
      }
      tmpv3=0;
      for(i=0; i< mvfSize; i++){
        bAigEdge_t tmpvvv;
        tmpvvv = manager->InitState;
        v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
        st_insert(old2new, (char *)v, (char *)(li[index1]));
        flags(li[index1]) |= StateBitMask;
#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;
        if(tmpv3!=SATnormalNode(li[index1-1])){

          vi = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(tmpMvfAig,i));

          if(vi == bAig_One){
            manager->InitState =
              PureSat_And(manager,manager->InitState,li[index1-1]);
#ifdef TIMEFRAME_VERIFY_
            fprintf(vis_stdout,"%d AND %d = %d\n",li[index1-1],tmpvvv,manager->InitState);
#endif
          }
          else if(vi == bAig_Zero){
            manager->InitState =
              PureSat_And(manager,manager->InitState,bAig_Not(li[index1-1]));
#ifdef TIMEFRAME_VERIFY_
            fprintf(vis_stdout,"%d AND %d = %d\n",bAig_Not(li[index1-1]),tmpvvv,manager->InitState);
#endif
          }
          else{
            tmpv1 = PureSat_ExpandForEachCone(manager,vi,old2new);
            tmpv2 = PureSat_Eq(manager,li[index1-1],tmpv1);
            manager->InitState = PureSat_And(manager,manager->InitState,tmpv2);
#ifdef TIMEFRAME_VERIFY_

            fprintf(vis_stdout,"%d AND %d = %d, %d is EQ node for funct node %d<-->%d\n",
                   tmpvvv,tmpv2,manager->InitState,tmpv2,tmpv1,li[index1-1] );
#endif
          }
        }
        tmpv3 = SATnormalNode(li[index1-1]);
      }

      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);
        flags(bli[tindex])|=StateBitMask;
        ori_bli[tindex++] = v;
      }

    }

#if DBG
    assert(tindex==bindex&&index1==index);
#endif
  }

  st_free_table(old2new);

  manager->class_ = 1;

  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) {

    PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);

    st_lookup(node2MvfAigTable, (char *) 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) {

    PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);

    st_lookup(node2MvfAigTable, (char *) 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;
    }
  }

  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]);

  }


  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) {
    char * name = Ntk_NodeReadName(latch);
    node  = Ntk_LatchReadDataInput(latch);
    mvfAig = lmvfAig = 0;
    st_lookup(node2MvfAigTable, (char *)node, &mvfAig);
    mvfSize = array_n(mvfAig);
    st_lookup(node2MvfAigTable, (char *)latch, &lmvfAig);
    lmvfSize = array_n(lmvfAig);
    if(mvfSize != lmvfSize) {
        fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
        exit(0);
    }

    else {
      for(i=0; i< mvfSize; i++){
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));

        nv = PureSat_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;
        if(nv==bAig_Zero||nv==bAig_One)
          continue;
        if(!st_lookup(idx2name,(char*)bAig_NonInvertedEdge(nv),(char**)&name1)){
          st_insert(idx2name,(char*)bAig_NonInvertedEdge(nv),(char*)name);
#ifdef TIMEFRAME_VERIFY_
        fprintf(vis_stdout,"idx2name:%d-->%s\n",bAig_NonInvertedEdge(nv),name);
#endif
        }
        else{
          /*if they are not equal, resort to MultiLatchTable*/
          if(strcmp(name,name1)){
            if(st_lookup(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),&table)){
#ifdef TIMEFRAME_VERIFY_
              fprintf(vis_stdout,"found entry In MultiLatchTable for %d,insert %s \n",
                     bAig_NonInvertedEdge(nv),name);
#endif
              st_insert(table,(char*)name,(char*)0);
            }
            else{
              table = st_init_table(strcmp,st_strhash);
#ifdef TIMEFRAME_VERIFY_
              fprintf(vis_stdout,"NO entry In MultiLatchTable for %d,insert %s, %s \n",
                     bAig_NonInvertedEdge(nv),name,name1);
#endif
              st_insert(table,(char*)name1,(char*)0);
              st_insert(table,(char*)name,(char*)0);
              st_insert(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),(char*)table);
            }
          }
        }

      }
    }


    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);
      v = bAig_GetCanonical(manager, lbVar.node);

      nv = PureSat_ExpandForEachCone(manager, v, old2new);
      flags(nv) |= StateBitMask;
      st_insert(old2new, (char *)v, (char *)nv);
#ifdef TIMEFRAME_VERIFY_
        ffprintf(vis_stdout,vis_stdout, "BLI(%d) %s(%d) : %d -> %d\n",
              1, Ntk_NodeReadName(latch), i, v, nv);
#endif
      bli[bindex++] = nv;

      tindex++;
      if(nv==bAig_Zero||nv==bAig_One)
        continue;
      if(!st_lookup(idx2name,(char*)bAig_NonInvertedEdge(nv),(char**)&name1)){
        st_insert(idx2name,(char*)bAig_NonInvertedEdge(nv),(char*)name);
#ifdef TIMEFRAME_VERIFY_
        fprintf(vis_stdout,"idx2name:%d-->%s\n",bAig_NonInvertedEdge(nv),name);
#endif
      }
      else{
        /*if they are not equal, resort to MultiLatchTable*/
        if(strcmp(name,name1)){
          if(st_lookup(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),&table)){
#ifdef TIMEFRAME_VERIFY_
            fprintf(vis_stdout,"found entry In MultiLatchTable for %d,insert %s \n",
                   bAig_NonInvertedEdge(nv),name);
#endif
            st_insert(table,(char*)name,(char*)0);
          }
          else{
            table = st_init_table(strcmp,st_strhash);
#ifdef TIMEFRAME_VERIFY_
            fprintf(vis_stdout,"NO entry In MultiLatchTable for %d,insert %s, %s \n",
                   bAig_NonInvertedEdge(nv),name,name1);
#endif
            st_insert(table,(char*)name1,(char*)0);
            st_insert(table,(char*)name,(char*)0);
            st_insert(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),(char*)table);
          }
        }
      }
    }/*for(i=0, tindex=lmVar.bVars; i<lmVar.en...*/
  }/*Ntk_NetworkForEachLatch(network, gen, latch) {*/


#ifdef TIMEFRAME_VERIFY_

  fprintf(vis_stdout,"after build latches of TF 1\n");
#endif


  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, (char *) node, &mvfAig);
    mvfSize = array_n(mvfAig);
    for(i=0; i< mvfSize; i++){
      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));

      nv = PureSat_ExpandForEachCone(manager, v, old2new);
      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 = PureSat_ExpandForEachCone(manager, v, old2new);
    st_insert(old2new, (char *)v, (char *)nv);
    li[i] = nv;
  }

  /*change the class of latch vars of tf */
  st_free_table(old2new);

  timeframe->currentTimeframe = 0;

  return(timeframe);

}

void
bAig_PureSat_ExpandTimeFrame(
        Ntk_Network_t *network,
        mAig_Manager_t *manager,
        PureSat_Manager_t *pm,
        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;
Ntk_Node_t *node, *latch;
st_table   *node2MvfAigTable, *old2new;
mAigMvar_t lmVar;
mAigBvar_t lbVar;
array_t   *bVarList, *mVarList;
lsGen gen;

st_table *idx2name, *table, *MultiLatchTable;
char *name, *name1;


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

  if(timeframe == 0)
    timeframe = bAig_PureSat_InitTimeFrame(network, manager, pm,withInitialState);


  idx2name = timeframe->idx2name;
  MultiLatchTable = timeframe->MultiLatchTable;

  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++) {
    manager->class_ = j+1;
    if(j>=manager->NumOfTable){
      manager->NumOfTable *= 2;
      manager->SymbolTableArray = REALLOC(st_table *,
                 manager->SymbolTableArray,manager->NumOfTable);
      manager->HashTableArray = REALLOC(bAigEdge_t *,
                 manager->HashTableArray,manager->NumOfTable);
    }
    manager->SymbolTableArray[manager->class_] = st_init_table(strcmp,st_strhash);
    manager->HashTableArray[manager->class_] = ALLOC(bAigEdge_t, bAig_HashTableSize);
    for (i=0; i<bAig_HashTableSize; i++)
      manager->HashTableArray[manager->class_][i]= bAig_NULL;


    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) {

      PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);

      st_lookup(node2MvfAigTable, (char *) 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) {

      PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li,  &bindex, &index,withInitialState);

      st_lookup(node2MvfAigTable, (char *) 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++;
      }
    }

    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]);

    }


    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) {
      name = Ntk_NodeReadName(latch);

      node  = Ntk_LatchReadDataInput(latch);
      mvfAig = lmvfAig = 0;
      st_lookup(node2MvfAigTable, (char *)node, &mvfAig);
      mvfSize = array_n(mvfAig);
      st_lookup(node2MvfAigTable, (char *)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);
        exit(0);
      }
      else {
        for(i=0; i< mvfSize; i++){
          v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
          nv = PureSat_ExpandForEachCone(manager, v, old2new);
          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;
          flags(nv) |= StateBitMask;
          if(nv==bAig_Zero||nv==bAig_One)
            continue;

          if(!st_lookup(idx2name,(char*)bAig_NonInvertedEdge(nv),(char**)&name1)){
            st_insert(idx2name,(char*)bAig_NonInvertedEdge(nv),(char*)name);
#ifdef TIMEFRAME_VERIFY_
            fprintf(vis_stdout,"idx2name:%d-->%s\n",bAig_NonInvertedEdge(nv),name);
#endif
          }
          else{
            /*if they are not equal, resort to MultiLatchTable*/
            if(strcmp(name,name1)){
              if(st_lookup(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),&table)){
#ifdef TIMEFRAME_VERIFY_
                fprintf(vis_stdout,"found entry In MultiLatchTable for %d,insert %s \n",
                       bAig_NonInvertedEdge(nv),name);
#endif
                st_insert(table,(char*)name,(char*)0);
              }
              else{
                table = st_init_table(strcmp,st_strhash);
#ifdef TIMEFRAME_VERIFY_
                fprintf(vis_stdout,"NO entry In MultiLatchTable for %d,insert %s, %s \n",
                       bAig_NonInvertedEdge(nv),name,name1);
#endif
                st_insert(table,(char*)name1,(char*)0);
                st_insert(table,(char*)name,(char*)0);
                st_insert(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),(char*)table);
              }
            }
          }

        }/* for(i=0; i< mvfSize; i++){*/
      }/*else {*/

      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);
        v = bAig_GetCanonical(manager, lbVar.node);
        nv = PureSat_ExpandForEachCone(manager, v, old2new);
        flags(nv) |= StateBitMask;
        st_insert(old2new, (char *)v, (char *)nv);
#ifdef TIMEFRAME_VERIFY_
        fprintf(vis_stdout, "BLI(%d) %s(%d) : %d -> %d\n",
              j+1, Ntk_NodeReadName(latch), i, v, nv);
#endif
        bli[bindex++] = nv;
        if(nv==bAig_Zero||nv==bAig_One)
          continue;

        if(!st_lookup(idx2name,(char*)bAig_NonInvertedEdge(nv),(char**)&name1)){
          st_insert(idx2name,(char*)bAig_NonInvertedEdge(nv),(char*)name);
#ifdef TIMEFRAME_VERIFY_
          fprintf(vis_stdout,"idx2name:%d-->%s\n",bAig_NonInvertedEdge(nv),name);
#endif
        }
        else{
          /*if they are not equal, resort to MultiLatchTable*/
          if(strcmp(name,name1)){
            if(st_lookup(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),&table)){
#ifdef TIMEFRAME_VERIFY_
              fprintf(vis_stdout,"found entry In MultiLatchTable for %d,insert %s \n",
                     bAig_NonInvertedEdge(nv),name);
#endif
              st_insert(table,(char*)name,(char*)0);
            }
            else{
              table = st_init_table(strcmp,st_strhash);
#ifdef TIMEFRAME_VERIFY_
              fprintf(vis_stdout,"NO entry In MultiLatchTable for %d,insert %s, %s \n",
                     bAig_NonInvertedEdge(nv),name,name1);
#endif
              st_insert(table,(char*)name1,(char*)0);
              st_insert(table,(char*)name,(char*)0);
              st_insert(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),(char*)table);
            }
          }
        }

        tindex++;
      }
    }

    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nOutputs);
    timeframe->outputs[j] = li;
    index = 0;
    Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
      st_lookup(node2MvfAigTable, (char *)node, &mvfAig);
      mvfSize = array_n(mvfAig);
      for(i=0; i< mvfSize; i++){
        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
        nv = PureSat_ExpandForEachCone(manager, v, old2new);
        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 = PureSat_ExpandForEachCone(manager, v, old2new);
      st_insert(old2new, (char *)v, (char *)nv);
      li[i] = nv;
    }
    st_free_table(old2new);


  }


  timeframe->currentTimeframe = bound;
}

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

}

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;
}