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

  FileName    [puresatTFrame.c]

  PackageName [puresat]

  Synopsis    [Abstraction refinement for large scale invariant checking.]

  Description [This file contains the functions to check invariant properties
  by the PureSAT abstraction refinement algorithm, which is entirely based on
  SAT solver, the input of which could be either CNF or AIG. It has several
  parts:

  * Localization-reduction base Abstraction
  * K-induction or interpolation to prove the truth of a property
  * Bounded Model Checking to find bugs
  * Incremental concretization based methods to verify abstract bugs
  * Incremental SAT solver to improve efficiency
  * UNSAT proof based method to obtain refinement
  * AROSAT to bring in only necessary latches into unsat proofs
  * Bridge abstraction to get compact coarse refinement
  * Refinement minization to guarrantee minimal refinements
  * Unsat proof-based refinement minimization to eliminate multiple candidate
    by on SAT test
  * Refinement prediction to decrease the number of refinement iterations
  * Dynamic switching to redistribute computional resources to improve
    efficiency

  For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05
  paper of Li et al., "A satisfiability-based appraoch to abstraction
  refinement in model checking", " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure", "Efficient computation
  of small abstraction refinements", and "Efficient abstraction refinement in
  interpolation-based unbounded model checking"]

  Author      [Bing Li]

  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
  All rights reserved.

  Permission is hereby granted, without written agreement and without
  license or royalty fees, to use, copy, modify, and distribute this
  software and its documentation for any purpose, provided that the
  above copyright notice and the following two paragraphs appear in
  all copies of this software.]

******************************************************************************/
#include "puresatInt.h"


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

/*---------------------------------------------------------------------------*/
/* Structure 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);


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

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

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

  Synopsis    [build conncetion between binary variables and
	       multi-valued variables]

  Description []

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Create new aig node in expanding timeframes with initial states]

  Description []

  SideEffects []

  SeeAlso     []

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


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

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

  Synopsis    [Build timeframed coi for each variable]

  Description []

  SideEffects []

  SeeAlso     []

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


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

}

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

  Synopsis    [Initialize aig timeframes]

  Description []

  SideEffects []

  SeeAlso     []

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

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;
  /**
   * 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) {

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

    /** make 0 index bAigEdge_t **/
  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;
    }
  }

    /** 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) {
    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);

}

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

  Synopsis    [build more aig timeframes]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
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;


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

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

    /** 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) {
      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;
}

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

  Synopsis    [Name comparison function.]

  Description [Name comparison function.]

  SideEffects [none]

  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    [Compute number of encoding bits.]

  Description [Compute number of encoding bits.]

  SideEffects [none]

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