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

  FileName    [puresatMain.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                                                */
/*---------------------------------------------------------------------------*/


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

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


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

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

  Synopsis    [Insert clauses of (Si!=Sj) for k-induction checking]

  Description [Insert clauses of (Si!=Sj) for k-induction checking]

  SideEffects []

  SeeAlso     []

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

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


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

  Synopsis    [Insert clauses of (Si!=I) for k-induction checking]

  Description [Insert clauses of (Si!=I) for k-induction checking]

  SideEffects []

  SeeAlso     []

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

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


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

  Synopsis    [Insert clauses of initial states for k-induction checking]

  Description [Insert clauses of initial states for k-induction checking]

  SideEffects []

  SeeAlso     []

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


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

  Synopsis    [k-induction checking from SSS'00 FMCAD paper ]

  Description [k-induction checking from SSS'00 FMCAD paper ]

  SideEffects []

  SeeAlso     []

******************************************************************************/
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);
      /*!P(S(i))*/
      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;
}

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

  Synopsis    [checking the existence of a path of certain length]

  Description [checking the existence of a path of certain length ]

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Incrementally checking the existence of a path of certain length]

  Description [Incrementally checking the existence of a path of certain length ]

  SideEffects []

  SeeAlso     []

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

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

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

  Synopsis    [Incrementally checking the existence of a path of certain length
  used by incremental concretization. For more information of incremental
  concretization, please check the BMC'03 and STTT'05
  paper of Li et al., "A satisfiability-based appraoch to abstraction
  refinement in model checking", and " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure"]

  Description [Incrementally checking the existence of a path of certain length
  used by incremental concretization. For more information of incremental
  concretization, please check the BMC'03 and STTT'05
  paper of Li et al., "A satisfiability-based appraoch to abstraction
  refinement in model checking", and " Abstraction in symbolic model checking
  using satisfiability as the only decision procedure"]

  SideEffects []

  SeeAlso     []

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

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


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

  Synopsis    [Building the path together with ClsidxToLatchTable for later use
  by refinement extraction]

  Description [Building the path together with ClsidxToLatchTable for later use
  by refinement extraction]

  SideEffects []

  SeeAlso     []

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

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


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

  Synopsis    [Building the path with enhanced initail states]

  Description [Building the path with enhanced initail states]

  SideEffects []

  SeeAlso     []

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

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