src/puresat/puresatBMC.c

Go to the documentation of this file.

#include "puresatInt.h"

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

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

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

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

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

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


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


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

void PureSatInsertNewClauseForSimplePath(array_t *vertexArray,
                                         Ntk_Network_t *network,
                                         int step1,
                                         int step2,
                                         BmcCnfClauses_t *cnfClauses,
                                         st_table *nodeToMvfAigTable)
{
  int i,j,k,mvfSize,index1,index2, cnfIndex;
  Ntk_Node_t * latch;
  MvfAig_Function_t *latchMvfAig;
  bAigEdge_t * latchBAig;
  array_t * tmpclause, *clauseArray, * clause, * clause1,*latchClause;
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  char * Name;
  boolean nextLatch = FALSE;

  latchClause = array_alloc(int,0);
  arrayForEachItem(char *,vertexArray,j,Name)
    {
      nextLatch = FALSE;
      clause = array_alloc(int,0); /*(-A + -A1 + -A2 + -A3)*/
      clauseArray  = array_alloc(array_t *,0);/*(A + -A1)(A + -A2)(A + -A3)*/
      latch = Ntk_NetworkFindNodeByName(network,Name);
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
        array_free(latchMvfAig);
        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      }
      mvfSize   = array_n(latchMvfAig);
      latchBAig = ALLOC(bAigEdge_t, mvfSize); 

      for(i=0; i< mvfSize; i++){
        latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
        }
      for(i=0; i< mvfSize; i++){
        if (latchBAig[i] == bAig_One)
          nextLatch=TRUE;break;   /* the clause is always true */
      }

      if(!nextLatch)
        {
          for(i=0; i< mvfSize; i++){
            latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
            index1 = BmcGenerateCnfFormulaForAigFunction(manager,latchBAig[i],step1,cnfClauses);
            index2 = BmcGenerateCnfFormulaForAigFunction(manager,latchBAig[i],step2,cnfClauses);
            
            cnfIndex = cnfClauses->cnfGlobalIndex++; 
            tmpclause  = array_alloc(int, 3);
            array_insert(int, tmpclause, 0, -index2);
            array_insert(int, tmpclause, 1, -index1);
            array_insert(int, tmpclause, 2,  cnfIndex);
            BmcCnfInsertClause(cnfClauses, tmpclause);
            array_free(tmpclause);
            
            tmpclause  = array_alloc(int, 2);
            array_insert(int, tmpclause, 0, index2);
            array_insert(int, tmpclause, 1, -cnfIndex);
            BmcCnfInsertClause(cnfClauses, tmpclause);
            array_free(tmpclause);
            
            tmpclause  = array_alloc(int, 2);
            array_insert(int, tmpclause, 0, index1);
            array_insert(int, tmpclause, 1, -cnfIndex);
            BmcCnfInsertClause(cnfClauses, tmpclause);
            array_free(tmpclause);
            
            /*(-A + A1 + A2 + A3)*/
            array_insert_last(int,clause,cnfIndex);
            /*(A + -A1)(A + -A2)(A + -A3)*/
            clause1 = array_alloc(int,0);/*(A + -A1/2/3)*/
            array_insert_last(int,clause1,-cnfIndex);
            array_insert_last(array_t *,clauseArray,clause1);
            
          }
         
          cnfIndex = cnfClauses->cnfGlobalIndex++; /*A*/
          /*(A + -A1)(A + -A2)(A + -A3)*/
          arrayForEachItem(array_t *,clauseArray,k,clause1)
            {
              array_insert_last(int,clause1,cnfIndex);
              BmcCnfInsertClause(cnfClauses,clause1);
              array_free(clause1);
            }
          array_free(clauseArray);
          
          /*(-A + A1 + A2 + A3)*/
          array_insert_last(int,clause,-cnfIndex);
          BmcCnfInsertClause(cnfClauses,clause);
          array_free(clause);
          
          /*(C + -A + -B)*/
          array_insert_last(int,latchClause,-cnfIndex);
        }
      FREE(latchBAig);
    }
  cnfIndex = cnfClauses->cnfGlobalIndex++; /* C*/
  array_insert_last(int,latchClause,cnfIndex); /*(C + -A + -B)*/
  BmcCnfInsertClause(cnfClauses,latchClause);
  array_free(latchClause);
  
  /*(-C)*/
  latchClause = array_alloc(int,0);
  array_insert_last(int,latchClause,-cnfIndex);
  BmcCnfInsertClause(cnfClauses,latchClause);
  array_free(latchClause);
}


void PureSatInsertNewClauseForInit(array_t *vertexArray,
                               Ntk_Network_t *network,
                               int step1,
                               int step2,
                               BmcCnfClauses_t *cnfClauses,
                               st_table *nodeToMvfAigTable)
{
  int i,j,k,mvfSize,index1=0,index2=0, cnfIndex;
  Ntk_Node_t * latch, *latchInit;
  MvfAig_Function_t *initMvfAig,*latchMvfAig;
  bAigEdge_t * latchBAig,* initBAig;
  array_t * tmpclause, *clauseArray, * clause, * clause1,*latchClause;
  mAig_Manager_t    *manager = Ntk_NetworkReadMAigManager(network);
  char * Name;
  boolean nextLatch = FALSE;

  latchClause = array_alloc(int,0);
  arrayForEachItem(char *,vertexArray,j,Name)
    {
      nextLatch = FALSE;
      clause = array_alloc(int,0); /*(-A + -A1 + -A2 + -A3)*/
      clauseArray  = array_alloc(array_t *,0);/*(A + -A1)(A + -A2)(A + -A3)*/
      latch = Ntk_NetworkFindNodeByName(network,Name);
      latchInit  = Ntk_LatchReadInitialInput(latch);
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
        array_free(latchMvfAig);
        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      }
      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);

       
      mvfSize   = array_n(latchMvfAig);
      latchBAig = ALLOC(bAigEdge_t, mvfSize); 
      initBAig  = ALLOC(bAigEdge_t, mvfSize);
      /* printf("mvfSize = %d \n",mvfSize);*/

      for(i=0; i< mvfSize; i++){
        latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
        initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
        }
      
      for(i=0; i< mvfSize; i++){
        if ((initBAig[i] == bAig_One) && (latchBAig[i] == bAig_One))
         {
           nextLatch=TRUE;
           break;   /* the clause is always true */
         }
      }

      
      if(!nextLatch)
        {
          for(i=0; i< mvfSize; i++){
            initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
            latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
            if(initBAig[i]==bAig_Zero ||latchBAig[i]==bAig_Zero)
              {
                continue;
              }
            if(initBAig[i]!=bAig_One)
              {
                index1 = BmcGenerateCnfFormulaForAigFunction(manager,initBAig[i],step1,cnfClauses);
              }
            if(latchBAig[i]!=bAig_One)
              {
                index2 = BmcGenerateCnfFormulaForAigFunction(manager,latchBAig[i],step2,cnfClauses);
              }
            
            cnfIndex = cnfClauses->cnfGlobalIndex++;
            if (initBAig[i] == bAig_One){
              tmpclause  = array_alloc(int, 2);
              array_insert(int, tmpclause, 0, -index2);
              array_insert(int, tmpclause, 1, cnfIndex);
              BmcCnfInsertClause(cnfClauses, tmpclause);
              array_free(tmpclause); 
              
              tmpclause  = array_alloc(int, 2);
              array_insert(int, tmpclause, 0, index2);
              array_insert(int, tmpclause, 1, -cnfIndex);
              BmcCnfInsertClause(cnfClauses, tmpclause);
              array_free(tmpclause);       
              
            } else if (latchBAig[i] == bAig_One){
              tmpclause  = array_alloc(int, 2);
              array_insert(int, tmpclause, 0, -index1);
              array_insert(int, tmpclause, 1, cnfIndex);
              BmcCnfInsertClause(cnfClauses, tmpclause);
              array_free(tmpclause);
              
              tmpclause  = array_alloc(int, 2);
              array_insert(int, tmpclause, 0, index1);
              array_insert(int, tmpclause, 1, -cnfIndex);
              BmcCnfInsertClause(cnfClauses, tmpclause);
              array_free(tmpclause);
              
            } else {
            tmpclause  = array_alloc(int, 3);
            array_insert(int, tmpclause, 0, -index2);
            array_insert(int, tmpclause, 1, -index1);
            array_insert(int, tmpclause, 2,  cnfIndex);
            BmcCnfInsertClause(cnfClauses, tmpclause);
            array_free(tmpclause);
            
            tmpclause  = array_alloc(int, 2);
            array_insert(int, tmpclause, 0, index2);
            array_insert(int, tmpclause, 1, -cnfIndex);
            BmcCnfInsertClause(cnfClauses, tmpclause);
            array_free(tmpclause);
            
            tmpclause  = array_alloc(int, 2);
            array_insert(int, tmpclause, 0, index1);
            array_insert(int, tmpclause, 1, -cnfIndex);
            BmcCnfInsertClause(cnfClauses, tmpclause);
            array_free(tmpclause);
            }
            /*(-A + A1 + A2 + A3)*/
            array_insert_last(int,clause,cnfIndex);
            /*(A + -A1)(A + -A2)(A + -A3)*/
            clause1 = array_alloc(int,0);/*(A + -A1/2/3)*/
            array_insert_last(int,clause1,-cnfIndex);
            array_insert_last(array_t *,clauseArray,clause1);
            
          }/* for(i=0; i< mvfSize;*/
         
          cnfIndex = cnfClauses->cnfGlobalIndex++; /*A*/
          /*(A + -A1)(A + -A2)(A + -A3)*/
          arrayForEachItem(array_t *,clauseArray,k,clause1)
            {
              array_insert_last(int,clause1,cnfIndex);
              BmcCnfInsertClause(cnfClauses,clause1);
              array_free(clause1);
            }
          array_free(clauseArray);
          
          /*(-A + A1 + A2 + A3)*/
          array_insert_last(int,clause,-cnfIndex);
          BmcCnfInsertClause(cnfClauses,clause);
          array_free(clause);
          
          /*(C + -A + -B)*/
          array_insert_last(int,latchClause,-cnfIndex);
        }/* if(!nextLatch)*/
      FREE(latchBAig); 
      FREE(initBAig);
    }/*arrayForEach..*/
  cnfIndex = cnfClauses->cnfGlobalIndex++; /* C*/
  array_insert_last(int,latchClause,cnfIndex); /*(C + -A + -B)*/
  BmcCnfInsertClause(cnfClauses,latchClause);
  array_free(latchClause);
  
  /*(-C)*/
  latchClause = array_alloc(int,0);
  array_insert_last(int,latchClause,-cnfIndex);
  BmcCnfInsertClause(cnfClauses,latchClause);
  array_free(latchClause);
}


void PureSatSetInitStatesForSimplePath(array_t * vertexArray,
                          Ntk_Network_t *network,
                          BmcCnfClauses_t *cnfClauses,
                          st_table * nodeToMvfAigTable)
{
  mAig_Manager_t  *maigManager   = Ntk_NetworkReadMAigManager(network);
  Ntk_Node_t         *latch, *latchInit;
  MvfAig_Function_t  *initMvfAig, *latchMvfAig;
  bAigEdge_t         *initBAig, *latchBAig;
  int                i,j, mvfSize;
  char               *nodeName;
  
  for(j=0;j<array_n(vertexArray);j++)
    {
      nodeName = array_fetch(char *,vertexArray,j);
      latch = Ntk_NetworkFindNodeByName(network,nodeName);
      latchInit  = Ntk_LatchReadInitialInput(latch);
      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
        array_free(latchMvfAig);
        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      }
      
      mvfSize   = array_n(initMvfAig);
      initBAig  = ALLOC(bAigEdge_t, mvfSize);
      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
      
      for(i=0; i< mvfSize; i++){
        latchBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(latchMvfAig, i));
        initBAig[i]  = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(initMvfAig,  i));
      }
      BmcGenerateClausesFromStateTostate(maigManager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
      FREE(initBAig);
      FREE(latchBAig);
    } 
}


boolean PureSatExistASimplePath(Ntk_Network_t *network,
                              PureSat_IncreSATManager_t * pism,
                              array_t * vertexArray,
                              bAigEdge_t property,
                              PureSat_Manager_t * pm)
{
  mAig_Manager_t  *maigManager   = Ntk_NetworkReadMAigManager(network);
  Ntk_Node_t         *latch, *latchData, *latchInit;
  MvfAig_Function_t  *initMvfAig, *dataMvfAig, *latchMvfAig;
  bAigEdge_t         *initBAig, *latchBAig, *dataBAig;
  int                i,j, k, mvfSize,propertyIndex;
  char               *nodeName;
  array_t            * Pclause = array_alloc(int,0);
  st_table           *nodeToMvfAigTable;
  BmcCnfStates_t     *cnfstate1,*cnfstate2;
  array_t            *supportLatches;
  int                 status;
  int beginPosition = pism->beginPosition;
  int Length = pism->Length;
  int oldLength = pism->oldLength;
  BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
  satManager_t * cm = pism->cm;
  
  /* construct loopfree path;*/
  nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  if (nodeToMvfAigTable == NIL(st_table)){
    (void) fprintf(vis_stderr,"** bmc error: please run buid_partiton_maigs first");
    exit(0);
  }

  for(j=beginPosition;j<array_n(vertexArray);j++){
    nodeName = array_fetch(char *,vertexArray,j);
    latch = Ntk_NetworkFindNodeByName(network,nodeName);
    latchInit  = Ntk_LatchReadInitialInput(latch);
    latchData  = Ntk_LatchReadDataInput(latch);
    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
     array_free(latchMvfAig);
     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   }
    
    mvfSize   = array_n(initMvfAig);
    initBAig  = ALLOC(bAigEdge_t, mvfSize);
    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
    latchBAig = ALLOC(bAigEdge_t, mvfSize);
    
    for(i=0; i< mvfSize; i++){
      dataBAig[i]  = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
      latchBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(latchMvfAig, i));
      initBAig[i]  = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(initMvfAig,  i));
    }
    
    /* BmcGenerateClausesFromStateTostate(maigManager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);*/
    for (k=0; k < oldLength; k++){
      BmcGenerateClausesFromStateTostate(maigManager, dataBAig,latchBAig, mvfSize, k, k+1, cnfClauses, 0);
    }
    FREE(initBAig);
    FREE(dataBAig);
    FREE(latchBAig);
  } /*st_foreach_item(vertexTable,*/

  if(oldLength<Length){
    for(j=0;j<array_n(vertexArray);j++){
      nodeName = array_fetch(char *,vertexArray,j);
      latch = Ntk_NetworkFindNodeByName(network,nodeName);
      latchInit  = Ntk_LatchReadInitialInput(latch);
      latchData  = Ntk_LatchReadDataInput(latch);
      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
      dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
    
      mvfSize   = array_n(initMvfAig);
      initBAig  = ALLOC(bAigEdge_t, mvfSize);
      dataBAig  = ALLOC(bAigEdge_t, mvfSize);
      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
      
      for(i=0; i< mvfSize; i++){
        dataBAig[i]  = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
        latchBAig[i] = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(latchMvfAig, i));
        initBAig[i]  = bAig_GetCanonical(maigManager,MvfAig_FunctionReadComponent(initMvfAig,  i));
      }
      
      for (k=oldLength; k <Length; k++){
        BmcGenerateClausesFromStateTostate(maigManager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
      }
      FREE(initBAig);
      FREE(dataBAig);
      FREE(latchBAig);
    }
  }/*if(oldLength!=0){*/

  if(pm->verbosity>=1)
    fprintf(vis_stdout,"forward simple path testing...\n");
  cnfstate1 = BmcCnfClausesFreeze(cnfClauses);
  
  /*generate NODE(i)!=NODE(i+1)*/
  for(i=1;i<Length;i++)
    for(j=i+1;j<=Length;j++)
      PureSatInsertNewClauseForSimplePath(vertexArray,network,i,j,cnfClauses,nodeToMvfAigTable); /*Si!=Sj*/
  
  cnfstate2 = BmcCnfClausesFreeze(cnfClauses);
  supportLatches = PureSatGetImmediateSupportLatches(network, 0, vertexArray);
  /*I(S0)*/
  PureSatSetInitStatesForSimplePath(supportLatches/*vertexArray*/,network,cnfClauses,nodeToMvfAigTable);
  /*generate all.!I(S(1...i)), the first constraint*/
  for(i=1;i<=Length;i++)
    PureSatInsertNewClauseForInit(supportLatches/*vertexArray*/,network,-1,i,cnfClauses,nodeToMvfAigTable);
  array_free(supportLatches);

  pism->propertyPos = cnfstate1->nextIndex;
  PureSatReadClauses(pism,pm);
  /*no incremental */
  if(!pm->incre){
    if(cm->savedConflictClauses)
      sat_ArrayFree(cm->savedConflictClauses);
    cm->savedConflictClauses = 0;
  }
  sat_Main(cm);
  status = cm->status;
  PureSatCleanSat(cm);
  BmcCnfClausesRestore(cnfClauses, cnfstate1);

  if(status == SAT_SAT)
    {
      if(pm->verbosity>=1)
        fprintf(vis_stdout,"backward simple path testing...\n");
      cnfstate2 = BmcCnfClausesFreeze(cnfClauses);
      /*generate NODE(i)!=NODE(i+1)*/
      for(i=1;i<Length;i++)
        for(j=i+1;j<=Length;j++)
          PureSatInsertNewClauseForSimplePath(vertexArray,network,i,j,cnfClauses,nodeToMvfAigTable);
      propertyIndex =  BmcGenerateCnfFormulaForAigFunction(maigManager,property, Length, cnfClauses);
      array_insert_last(int, Pclause,propertyIndex);
      BmcCnfInsertClause(cnfClauses, Pclause);
      array_free(Pclause);
      /*all.P(S(0,...i-1))*/
      property = bAig_Not(property);
      for(k=0; k <= Length-1; k++){
        propertyIndex =  BmcGenerateCnfFormulaForAigFunction(maigManager,property,k, cnfClauses);
        Pclause = array_alloc(int,0);
        array_insert_last(int, Pclause, propertyIndex);
        BmcCnfInsertClause(cnfClauses, Pclause);
        array_free(Pclause);
      }

      pism->propertyPos = cnfstate2->nextIndex;
      PureSatReadClauses(pism,pm);
      /*no incremental */
      if(!pm->incre){
        if(cm->savedConflictClauses)
          sat_ArrayFree(cm->savedConflictClauses);
        cm->savedConflictClauses = 0;
      }
      sat_Main(cm);
      status = cm->status;
      PureSatCleanSat(cm);
      if(status == SAT_SAT)
        {
          BmcCnfClausesRestore(cnfClauses, cnfstate1);
          FREE(cnfstate1);
          FREE(cnfstate2);
          return TRUE;
        }
    }
  FREE(cnfstate1);
  FREE(cnfstate2);
  return  FALSE;
}

boolean PureSatExistCE(Ntk_Network_t * network,
                       PureSat_IncreSATManager_t * pism,
                       BmcOption_t *options,
                       array_t *vertexArray,
                       bAigEdge_t property,
                       PureSat_Manager_t * pm,
                       int extractCexInfo)
{
  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
  Ntk_Node_t         *latch, *latchData, *latchInit;
  MvfAig_Function_t  *initMvfAig, *dataMvfAig, *latchMvfAig;
  bAigEdge_t         *initBAig, *latchBAig, *dataBAig;
  int                i,j, k, mvfSize;
  char               *nodeName;
  array_t            *result;
  array_t            *Pclause = array_alloc(int, 0);
  FILE               *cnfFile;
  st_table           *nodeToMvfAigTable;
  BmcCnfStates_t    *cnfstate;
  int beginPosition = pism->beginPosition;
  int oldLength = pism->oldLength;
  int Length = pism->Length;
  BmcCnfClauses_t *cnfClauses = pism->cnfClauses;

  double t2, t1 = util_cpu_ctime();

  options->verbosityLevel = (Bmc_VerbosityLevel) pm->verbosity;
  nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  if (nodeToMvfAigTable == NIL(st_table)){
    (void) fprintf(vis_stderr,"** bmc error: please run buid_partiton_maigs first");
    exit(0);
  }


#if 1
 { 
   array_t *supportLatches = PureSatGetImmediateSupportLatches(network, beginPosition, vertexArray);
   arrayForEachItem(char *, supportLatches, j, nodeName) {
     latch = Ntk_NetworkFindNodeByName(network, nodeName);
    latchInit  = Ntk_LatchReadInitialInput(latch);
    latchData  = Ntk_LatchReadDataInput(latch);
    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
    if (latchMvfAig ==  NIL(MvfAig_Function_t)){
      latchMvfAig = Bmc_NodeBuildMVF(network, latch);
      array_free(latchMvfAig);
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
    }
    
    mvfSize   = array_n(initMvfAig);
    initBAig  = ALLOC(bAigEdge_t, mvfSize);
    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
    
    for(i=0; i< mvfSize; i++){
      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
    }
    
    BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
    FREE(initBAig);
    FREE(dataBAig);
    FREE(latchBAig);
  }    
   array_free(supportLatches);
 }

  
  for(j=beginPosition;j<array_n(vertexArray);j++){
    nodeName = array_fetch(char *,vertexArray,j);
    latch = Ntk_NetworkFindNodeByName(network,nodeName);
    latchInit  = Ntk_LatchReadInitialInput(latch);
    latchData  = Ntk_LatchReadDataInput(latch);
    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
     array_free(latchMvfAig);
     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   }
    
    mvfSize   = array_n(initMvfAig);
    initBAig  = ALLOC(bAigEdge_t, mvfSize);
    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
    
    for(i=0; i< mvfSize; i++){
      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
    }
    /* BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);*/
    for (k=0; k <oldLength; k++){
      BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
    }
    FREE(initBAig);
    FREE(dataBAig);
    FREE(latchBAig);
  } /*st_foreach_item(vertexTable,*/
#else
  /*build TR for more latches*/
  
  for(j=beginPosition;j<array_n(vertexArray);j++){
    nodeName = array_fetch(char *,vertexArray,j);
    latch = Ntk_NetworkFindNodeByName(network,nodeName);
    latchInit  = Ntk_LatchReadInitialInput(latch);
    latchData  = Ntk_LatchReadDataInput(latch);
    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
     array_free(latchMvfAig);
     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   }
    
    mvfSize   = array_n(initMvfAig);
    initBAig  = ALLOC(bAigEdge_t, mvfSize);
    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
    
    for(i=0; i< mvfSize; i++){
      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
    }
    BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
    for (k=0; k <oldLength; k++){
      BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
    }
    FREE(initBAig);
    FREE(dataBAig);
    FREE(latchBAig);
  } /*st_foreach_item(vertexTable,*/
#endif

  /* for more length*/
  if(oldLength<Length){
    for(j=0;j<array_n(vertexArray);j++){
      nodeName = array_fetch(char *,vertexArray,j);
      latch = Ntk_NetworkFindNodeByName(network,nodeName);
      latchInit  = Ntk_LatchReadInitialInput(latch);
      latchData  = Ntk_LatchReadDataInput(latch);
      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
      dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
        array_free(latchMvfAig);
        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      }
    
      mvfSize   = array_n(initMvfAig);
      initBAig  = ALLOC(bAigEdge_t, mvfSize);
      dataBAig  = ALLOC(bAigEdge_t, mvfSize);
      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
      
      for(i=0; i< mvfSize; i++){
        dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
        latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
        initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
      }
      
      for (k=oldLength; k<Length; k++){
        BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
      }
      FREE(initBAig);
      FREE(dataBAig);
      FREE(latchBAig);
    }
  }
  

   k=Length;
   cnfstate = BmcCnfClausesFreeze(cnfClauses);
   /* for(k=0; k <= Length; k++){*/
   array_insert_last(int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager, property,k, cnfClauses));
   /*    } */
   BmcCnfInsertClause(cnfClauses, Pclause);
   array_free(Pclause);
   cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
   BmcWriteClauses(manager, cnfFile, cnfClauses, options);
   (void) fclose(cnfFile);
   result = BmcCheckSAT(options);
   BmcCnfClausesRestore(cnfClauses, cnfstate);
   FREE(cnfstate);
   
  t2 = util_cpu_ctime();
  /*timeElapse_Sol += t2-t1;*/
  if(pm->verbosity>=2)
    fprintf(vis_stdout, "timeElapse_sol_noIncre: += %g\n", (double)((t2-t1)/1000.0));

  
  if(extractCexInfo && pm->dbgLevel>=1 && result!=NIL(array_t)){
    pm->result = array_dup(result);
  }
  
  if(result!=NIL(array_t))
    {
      if(pm->verbosity>=2)
        fprintf(vis_stdout, "find CEX\n");
      array_free(result);
      return TRUE;
    }
  else
    {
      if(pm->verbosity>=2)
        fprintf(vis_stdout, "didn't find CEX\n");
       return FALSE;
    }
}

boolean PureSatIncreExistCE(Ntk_Network_t * network,
                     PureSat_IncreSATManager_t *pism,
                     array_t *vertexArray,
                     bAigEdge_t property,
                     PureSat_Manager_t * pm)
{
  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
  Ntk_Node_t         *latch, *latchData, *latchInit;
  MvfAig_Function_t  *initMvfAig, *dataMvfAig, *latchMvfAig;
  bAigEdge_t         *initBAig, *latchBAig, *dataBAig;
  int                i,j, k, mvfSize;
  int                status;
  char               *nodeName;
  array_t            *Pclause = array_alloc(int, 0);
  st_table           *nodeToMvfAigTable;
  BmcCnfStates_t    *cnfstate;
  int beginPosition = pism->beginPosition;
  int Length = pism->Length;
  int oldLength = pism->oldLength;
  BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
  satManager_t * cm = pism->cm;

  nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  if (nodeToMvfAigTable == NIL(st_table)){
    (void) fprintf(vis_stderr,"** bmc error: please run buid_partiton_maigs first");
    exit(0);
  }

 { 
   array_t *supportLatches = PureSatGetImmediateSupportLatches(network, beginPosition, vertexArray);
   arrayForEachItem(char *, supportLatches, j, nodeName) {
     latch = Ntk_NetworkFindNodeByName(network, nodeName);
    latchInit  = Ntk_LatchReadInitialInput(latch);
    latchData  = Ntk_LatchReadDataInput(latch);
    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
    if (latchMvfAig ==  NIL(MvfAig_Function_t)){
      latchMvfAig = Bmc_NodeBuildMVF(network, latch);
      array_free(latchMvfAig);
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
    }
    
    mvfSize   = array_n(initMvfAig);
    initBAig  = ALLOC(bAigEdge_t, mvfSize);
    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
    
    for(i=0; i< mvfSize; i++){
      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
    }
    
    BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
    FREE(initBAig);
    FREE(dataBAig);
    FREE(latchBAig);
  }  
   array_free(supportLatches);
 }
  
  for(j=beginPosition;j<array_n(vertexArray);j++){
    nodeName = array_fetch(char *,vertexArray,j);
    latch = Ntk_NetworkFindNodeByName(network,nodeName);
    latchInit  = Ntk_LatchReadInitialInput(latch);
    latchData  = Ntk_LatchReadDataInput(latch);
    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
     array_free(latchMvfAig);
     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   }
    
    mvfSize   = array_n(initMvfAig);
    initBAig  = ALLOC(bAigEdge_t, mvfSize);
    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
    
    for(i=0; i< mvfSize; i++){
      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
    }
    BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
    for (k=0; k <oldLength; k++){
      BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
    }
    FREE(initBAig);
    FREE(dataBAig);
    FREE(latchBAig);
  }

  /* for more length*/
  if(oldLength<Length){
    for(j=0;j<array_n(vertexArray);j++){
      nodeName = array_fetch(char *,vertexArray,j);
      latch = Ntk_NetworkFindNodeByName(network,nodeName);
      latchInit  = Ntk_LatchReadInitialInput(latch);
      latchData  = Ntk_LatchReadDataInput(latch);
      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
      dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
        array_free(latchMvfAig);
        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      }
    
      mvfSize   = array_n(initMvfAig);
      initBAig  = ALLOC(bAigEdge_t, mvfSize);
      dataBAig  = ALLOC(bAigEdge_t, mvfSize);
      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
      
      for(i=0; i< mvfSize; i++){
        dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
        latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
        initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
      }
      
      for (k=oldLength; k<Length; k++){
        BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
      }
      FREE(initBAig);
      FREE(dataBAig);
      FREE(latchBAig);
    }
  }

   k=Length;
   cnfstate = BmcCnfClausesFreeze(cnfClauses);
   /* for(k=0; k <= Length; k++){*/
   array_insert_last(int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager, property,k, cnfClauses));
   /*    }*/
   BmcCnfInsertClause(cnfClauses, Pclause);
   array_free(Pclause);
   pism->propertyPos = cnfstate->nextIndex;
   PureSatReadClauses(pism, pm);
   
   /*no incremental */
  if(!pm->incre){
    if(cm->savedConflictClauses)
      sat_ArrayFree(cm->savedConflictClauses);
    cm->savedConflictClauses = 0;
  }
   cm->status = 0;
   sat_Main(cm);
   status = cm->status;
   PureSatCleanSat(cm);
   BmcCnfClausesRestore(cnfClauses, cnfstate);
   FREE(cnfstate);
   if(status == SAT_SAT)
     {
       if(pm->verbosity>=1)
         fprintf(vis_stdout, "find CEX\n");
       return TRUE;
     }
   else
     {
       if(pm->verbosity>=1)
         fprintf(vis_stdout, "didn't find CEX\n");
       return FALSE;
     }
}

boolean PureSatIncreExistCEForRefineOnAbs(Ntk_Network_t *network,
                                   PureSat_IncreSATManager_t *pism,
                                   array_t *vertexArray,
                                   bAigEdge_t property,
                                   boolean firstTime,
                                   PureSat_Manager_t * pm)

{
  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
  Ntk_Node_t         *latch, *latchData, *latchInit;
  MvfAig_Function_t  *initMvfAig, *dataMvfAig, *latchMvfAig;
  bAigEdge_t         *initBAig, *latchBAig, *dataBAig;
  int                i,j, k, mvfSize, status;
  char               *nodeName;
  array_t            *Pclause = array_alloc(int, 0);
  st_table           *nodeToMvfAigTable;
  int beginPosition = pism->beginPosition;
  int Length = pism->Length;
  int oldLength = pism->oldLength;
  BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
  satManager_t * cm = pism->cm;

  nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  if (nodeToMvfAigTable == NIL(st_table)){
    (void) fprintf(vis_stderr,"** bmc error: please run buid_partiton_maigs first");
    exit(0);
  }
  
 { 
   array_t *supportLatches = PureSatGetImmediateSupportLatches(network, beginPosition, vertexArray);
   arrayForEachItem(char *, supportLatches, j, nodeName) {
     latch = Ntk_NetworkFindNodeByName(network, nodeName);
    latchInit  = Ntk_LatchReadInitialInput(latch);
    latchData  = Ntk_LatchReadDataInput(latch);
    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
    if (latchMvfAig ==  NIL(MvfAig_Function_t)){
      latchMvfAig = Bmc_NodeBuildMVF(network, latch);
      array_free(latchMvfAig);
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
    }
    
    mvfSize   = array_n(initMvfAig);
    initBAig  = ALLOC(bAigEdge_t, mvfSize);
    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
    
    for(i=0; i< mvfSize; i++){
      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
    }
    
    BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
    FREE(initBAig);
    FREE(dataBAig);
    FREE(latchBAig);
  }  
   array_free(supportLatches);
 }

  
  for(j=beginPosition;j<array_n(vertexArray);j++){
    nodeName = array_fetch(char *,vertexArray,j);
    latch = Ntk_NetworkFindNodeByName(network,nodeName);
    latchInit  = Ntk_LatchReadInitialInput(latch);
    latchData  = Ntk_LatchReadDataInput(latch);
    initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
    dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
    latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
     array_free(latchMvfAig);
     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   }
    
    mvfSize   = array_n(initMvfAig);
    initBAig  = ALLOC(bAigEdge_t, mvfSize);
    dataBAig  = ALLOC(bAigEdge_t, mvfSize);
    latchBAig = ALLOC(bAigEdge_t, mvfSize);   
    
    for(i=0; i< mvfSize; i++){
      dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
      latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
      initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
    }
    
    /*BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);*/
    for (k=0; k <oldLength; k++){
      BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
    }
    FREE(initBAig);
    FREE(dataBAig);
    FREE(latchBAig);
  }

  /*for more length */
  if(oldLength<Length){
    for(j=0;j<array_n(vertexArray);j++){
      nodeName = array_fetch(char *,vertexArray,j);
      latch = Ntk_NetworkFindNodeByName(network,nodeName);
      latchInit  = Ntk_LatchReadInitialInput(latch);
      latchData  = Ntk_LatchReadDataInput(latch);
      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
      dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
        array_free(latchMvfAig);
        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      }
    
      mvfSize   = array_n(initMvfAig);
      initBAig  = ALLOC(bAigEdge_t, mvfSize);
      dataBAig  = ALLOC(bAigEdge_t, mvfSize);
      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
      
      for(i=0; i< mvfSize; i++){
        dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
        latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
        initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
      }
      
      for (k=oldLength; k<Length; k++){
        BmcGenerateClausesFromStateTostate(manager, dataBAig, latchBAig, mvfSize, k, k+1, cnfClauses, 0);
      }
      FREE(initBAig);
      FREE(dataBAig);
      FREE(latchBAig);
    }
  }
  
 
  /*cnfstate = BmcCnfClausesFreeze(cnfClauses);*/
  if(firstTime){
    /* pism->propertyPos = cnfstate->nextIndex;*/
    array_insert_last(int, Pclause, BmcGenerateCnfFormulaForAigFunction(manager,
                                                                 property,Length, cnfClauses));
    BmcCnfInsertClause(cnfClauses, Pclause);
    array_free(Pclause);
  }
  PureSatReadClauses(pism,pm);
  sat_Main(cm);
  if(pm->dbgLevel>=1 && cm->status==SAT_SAT){
    pm->result = array_alloc(int, 0);
    {
      int size, value;
      size = cm->initNumVariables * satNodeSize;
      for(i=satNodeSize; i<=size; i+=satNodeSize) {
        value = SATvalue(i);
        if(value == 1) {
          array_insert_last(int, pm->result, SATnodeID(i));
        }
        else if(value == 0) {
          array_insert_last(int, pm->result, -(SATnodeID(i)));
        }
      }
    }
  }
  status = cm->status;
  PureSatCleanSat(cm);
  /*FREE(cnfstate);*/
  if(status == SAT_SAT)
    {
      if(pm->verbosity>=1)
        fprintf(vis_stdout, "find CEX\n");
      return TRUE;
    }
  else
    {
      if(pm->verbosity>=1)
        fprintf(vis_stdout, "didn't find CEX\n");
      return FALSE;
    }
}


void
PureSatGenerateClausesFromStateTostateWithTable(
   bAig_Manager_t  *manager,
   bAigEdge_t      *fromAigArray,
   bAigEdge_t      *toAigArray,
   int             mvfSize, 
   int             fromState,
   int             toState,
   BmcCnfClauses_t *cnfClauses,
   int             outIndex,
   st_table        *ClsidxToLatchTable,
   char            *nodeName) 
{
  array_t    *clause, *tmpclause;
  int        toIndex, fromIndex, cnfIndex;
  int        i;
  
  toIndex =0;
  fromIndex = 0;
  
  for(i=0; i< mvfSize; i++){
    if ((fromAigArray[i] == bAig_One) && (toAigArray[i] == bAig_One)){
      return;   /* the clause is always true */
    }
  }
  clause  = array_alloc(int, 0);
  for(i=0; i< mvfSize; i++){
    if ((fromAigArray[i] != bAig_Zero) && (toAigArray[i] != bAig_Zero)){
      if (toAigArray[i] != bAig_One){ 
         toIndex = BmcGenerateCnfFormulaForAigFunction(manager,toAigArray[i],
                                                       toState,cnfClauses);
      }
      if (fromAigArray[i] != bAig_One){ 
         fromIndex = BmcGenerateCnfFormulaForAigFunction(manager,fromAigArray[i],
                                                         fromState,cnfClauses);
      }
     cnfIndex = cnfClauses->cnfGlobalIndex++;  /* index of the output of the OR of T(from, to) */
     if (toAigArray[i] == bAig_One){    
       tmpclause  = array_alloc(int, 2);
       array_insert(int, tmpclause, 0, -fromIndex);
       array_insert(int, tmpclause, 1, cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
       array_free(tmpclause); 

       tmpclause  = array_alloc(int, 2);
       array_insert(int, tmpclause, 0, fromIndex);
       array_insert(int, tmpclause, 1, -cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
       array_free(tmpclause);       

     } else if (fromAigArray[i] == bAig_One){
       tmpclause  = array_alloc(int, 2);
       array_insert(int, tmpclause, 0, -toIndex);
       array_insert(int, tmpclause, 1, cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
       array_free(tmpclause);

       tmpclause  = array_alloc(int, 2);
       array_insert(int, tmpclause, 0, toIndex);
       array_insert(int, tmpclause, 1, -cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
       array_free(tmpclause);
       
     } else {
       tmpclause  = array_alloc(int, 3);
       array_insert(int, tmpclause, 0, -toIndex);
       array_insert(int, tmpclause, 1, -fromIndex);
       array_insert(int, tmpclause, 2,  cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
       array_free(tmpclause);

       tmpclause  = array_alloc(int, 2);
       array_insert(int, tmpclause, 0, toIndex);
       array_insert(int, tmpclause, 1, -cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
       array_free(tmpclause);

       tmpclause  = array_alloc(int, 2);
       array_insert(int, tmpclause, 0, fromIndex);
       array_insert(int, tmpclause, 1, -cnfIndex);
       BmcCnfInsertClause(cnfClauses, tmpclause);
       st_insert(ClsidxToLatchTable,(char *)(long)(cnfClauses->noOfClauses-1),nodeName);
       array_free(tmpclause);
     }
     array_insert_last(int, clause, cnfIndex);
    } /* if */
      
  } /* for i loop */
  if (outIndex != 0 ){
    array_insert_last(int, clause, -outIndex);
  }
  BmcCnfInsertClause(cnfClauses, clause);
  array_free(clause);
  
  return;
}


void
PureSatGenerateClausesForPath_EnhanceInit(
   Ntk_Network_t   *network,
   int             from,
   int             to,
   PureSat_IncreSATManager_t * pism,
   PureSat_Manager_t *  pm,
   st_table        *nodeToMvfAigTable,
   st_table        *CoiTable)
{
  mAig_Manager_t  *manager   = Ntk_NetworkReadMAigManager(network);
  lsGen           gen;
  
  Ntk_Node_t         *latch, *latchData, *latchInit;
  MvfAig_Function_t  *initMvfAig, *dataMvfAig, *latchMvfAig;
  bAigEdge_t         *initBAig, *latchBAig, *dataBAig;
  int        i,j, k, mvfSize;
  array_t * vertexArray = array_alloc(char *,0);
  char * nodeName;
  BmcCnfClauses_t * cnfClauses = pism->cnfClauses;
  st_table * ClsidxToLatchTable = pm->ClsidxToLatchTable;

  if(from == 0){
    if(pm->verbosity>=2)
      fprintf(vis_stdout, "node in vertexArray: ");
    Ntk_NetworkForEachLatch(network, gen, latch) { 
      int tmp;
      if (!st_lookup_int(CoiTable, latch, &tmp)){
        continue;
      }
      nodeName = Ntk_NodeReadName(latch);
      array_insert_last(char *,vertexArray,nodeName);
      if(pm->verbosity>=2)
        fprintf(vis_stdout, "%s  ",nodeName);
    }
    if(pm->verbosity>=2)
      fprintf(vis_stdout, "\n");
   }

  if(from == 0){ 
    array_t *supportLatches = PureSatGetImmediateSupportLatches(network, 0, vertexArray);
    arrayForEachItem(char *, supportLatches, j, nodeName) {
      latch = Ntk_NetworkFindNodeByName(network, nodeName);
      latchInit  = Ntk_LatchReadInitialInput(latch);
      latchData  = Ntk_LatchReadDataInput(latch);
      initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
      dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
      latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      if (latchMvfAig ==  NIL(MvfAig_Function_t)){
        latchMvfAig = Bmc_NodeBuildMVF(network, latch);
        array_free(latchMvfAig);
        latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
      }
      
      mvfSize   = array_n(initMvfAig);
      initBAig  = ALLOC(bAigEdge_t, mvfSize);
      dataBAig  = ALLOC(bAigEdge_t, mvfSize);
      latchBAig = ALLOC(bAigEdge_t, mvfSize);   
      
      for(i=0; i< mvfSize; i++){
        dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
        latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
        initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
      }
      
      BmcGenerateClausesFromStateTostate(manager, initBAig, latchBAig, mvfSize, -1, 0, cnfClauses, 0);
      FREE(initBAig);
      FREE(dataBAig);
      FREE(latchBAig);
    }
    array_free(supportLatches);
    array_free(vertexArray);
  }
  
  Ntk_NetworkForEachLatch(network, gen, latch) { 
    int tmp;
    if (!st_lookup_int(CoiTable, latch, &tmp)){
      continue;
    }
    nodeName = Ntk_NodeReadName(latch);
   latchInit  = Ntk_LatchReadInitialInput(latch);
   latchData  = Ntk_LatchReadDataInput(latch);

   /* Get the multi-valued function for each node*/
   initMvfAig = Bmc_ReadMvfAig(latchInit, nodeToMvfAigTable);
   if (initMvfAig ==  NIL(MvfAig_Function_t)){
     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchInit));
     return;
   } 
   dataMvfAig = Bmc_ReadMvfAig(latchData, nodeToMvfAigTable);
   if (dataMvfAig ==  NIL(MvfAig_Function_t)){
     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \n", Ntk_NodeReadName(latchData));
     return;
   }
   latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   if (latchMvfAig ==  NIL(MvfAig_Function_t)){
     latchMvfAig = Bmc_NodeBuildMVF(network, latch);
     array_free(latchMvfAig);
     latchMvfAig = Bmc_ReadMvfAig(latch, nodeToMvfAigTable);
   }
      
   mvfSize   = array_n(initMvfAig);
   initBAig  = ALLOC(bAigEdge_t, mvfSize);
   dataBAig  = ALLOC(bAigEdge_t, mvfSize);
   latchBAig = ALLOC(bAigEdge_t, mvfSize);   

   for(i=0; i< mvfSize; i++){
     dataBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(dataMvfAig,  i));
     latchBAig[i] = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(latchMvfAig, i));
     initBAig[i]  = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(initMvfAig,  i));
   } 
   /* Generate the CNF for the transition functions */   
   for (k=from; k < to; k++){
     PureSatGenerateClausesFromStateTostateWithTable(manager, dataBAig,latchBAig, mvfSize, k,
                                                       k+1, cnfClauses,0,ClsidxToLatchTable, nodeName);
   } /* for k state loop */
   FREE(initBAig);
   FREE(dataBAig);
   FREE(latchBAig);
  } /* ForEachLatch loop*/

  return;
}