src/puresat/puresatIPAbRf.c

Go to the documentation of this file.

#include "maigInt.h"
#include "puresatInt.h"

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

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


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


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

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

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


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


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

boolean PureSatIPOnCon(Ntk_Network_t * network,
                       Ctlsp_Formula_t *ltlFormula,
                       PureSat_Manager_t *pm)
{
  int k;
  bAig_Manager_t    *manager;
  bAigEdge_t        property;
  double t1,t2;
  array_t           *previousResultArray=0;
  boolean firstTime;
  int round;
  st_table * tmpTable;
  int oldPos1,nodes_in_coi=0;
  satManager_t * cm;
  bAigEdge_t state, tmpState;
  double tCon=0;
  RTManager_t *rm;

  manager = Ntk_NetworkReadMAigManager(network);

  if(pm->verbosity>=1)
    fprintf(vis_stdout,"go to concrete model\n");

 k = pm->Length;
 round = 1;
 PureSat_CleanMask(manager,ResetGlobalVarMask);
 PureSat_MarkGlobalVar(manager,1);
 while(1){
   k += round-1;
   pm->Length = k;

   if(pm->verbosity>=1)
     fprintf(vis_stdout,"\nk = %d InitState = %ld\n",k,manager->InitState);
   manager->test2LevelMini = 1;
   t1 = util_cpu_ctime();
   bAig_PureSat_ExpandTimeFrame(network, manager,pm, k, BMC_NO_INITIAL_STATES);
   t2 = util_cpu_ctime();
   pm->tExp += t2-t1;
   if(pm->verbosity>=2)
     fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
            (double)((t2-t1)/1000.0),pm->tExp/1000);
   manager->test2LevelMini = 0;
   if(pm->verbosity>=1){
     fprintf(vis_stdout,"After expand TF\n");
     PureSat_PrintAigStatus(manager);
   }
   manager->class_ = k+1;
   property = BmcCirCUsCreatebAigOfPropFormula(network,
                     manager, k, ltlFormula, BMC_NO_INITIAL_STATES);
   property = bAig_Not(property);
   if(property==0){
     return TRUE;
   }
   if(property==1){
     return FALSE;
   }
   oldPos1 = manager->nodesArraySize-bAigNodeSize;
   if(pm->verbosity>=1){
     fprintf(vis_stdout,"After expanding TF and building property\n");
     PureSat_PrintAigStatus(manager);
   }
   firstTime = TRUE;
   round = 0;
   state = manager->InitState;

   while(1){
     round++;
     if(pm->verbosity>=1)
       fprintf(vis_stdout,"round:%d for k = %d\n",round,k);
     manager->assertArray = sat_ArrayAlloc(1);
     if(state!=bAig_One)
       sat_ArrayInsert(manager->assertArray,state);
     cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
     cm->option->IP = 1;


     if(cm->status==0){
       if(pm->verbosity>=1)
         fprintf(vis_stdout,"normal COI:\n");
       if(pm->verbosity>=1) {
         nodes_in_coi = PureSat_CountNodesInCoi(cm);
         fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
       }
       t1 = util_cpu_ctime();
       sat_Main(cm);

       rm = cm->rm;
       cm->option->IP = 0;
       if(manager->NodesArray!=cm->nodesArray)
         /*cm->nodesArray may be reallocated */
         manager->NodesArray = cm->nodesArray;
       t2 = util_cpu_ctime();
       pm->tIPUnsat += t2 - t1;
       if(pm->verbosity>=2)
         fprintf(vis_stdout,"time for Unsat:%g, total:%g\n",
                (double)((t2-t1)/1000.0),pm->tIPUnsat/1000);
     }

     if(cm->status == SAT_SAT){
       /*SAT: first time->find bug, otherwise increase length*/
       if(firstTime){
         fprintf(vis_stdout,"found CEX of length %d\n",k);

         sat_ArrayFree(manager->assertArray);
         manager->assertArray = 0;
         RT_Free(cm->rm);
         PureSat_SatFreeManager(cm);
         return FALSE;
       }
       else{

         if(pm->verbosity>=1)
           fprintf(vis_stdout,"find bogus bug at length k=%d,round=%d,increase length\n",k,round);

         sat_ArrayFree(manager->assertArray);
         RT_Free(cm->rm);
         PureSat_SatFreeManager(cm);
         break;
       }
     }
     else{
       /*UNSAT: get IP, add to init states, until reach convergence, which
       means property is true
       Bing: IP generation*/
       assert(cm->currentDecision>=-1);
       if(cm->currentDecision!=-1)
         sat_Backtrack(cm, -1);
       /*get rid of Conflict Clauses*/
       PureSat_ResetManager(manager,cm,1);

       if(cm->option->coreGeneration&&cm->status == SAT_UNSAT){
         manager->class_ = 1;
         t1 = util_cpu_ctime();
         tmpState = sat_GenerateFwdIP(manager,cm,cm->rm->root,1);
         manager->IPState = PureSat_MapIP(manager,tmpState,1,0);

         /*Wheneven there is baigNode generated, Reset_Manager is necessary,
           //since NodeArray may be reallocated, # of Nodes changed*/
         PureSat_ResetManager(manager,cm,0);
         t2 = util_cpu_ctime();
         pm->tIPGen += t2 -t1;
         if(pm->verbosity>=2)
           fprintf(vis_stdout,"time for generating and mapping IP:%g, total:%g\n",
                  (double)((t2-t1)/1000.0),pm->tIPGen/1000);
         if(pm->verbosity>=1){
           fprintf(vis_stdout,"After generate IP,IP2:%ld,%ld:\n",manager->IPState,tmpState);
           PureSat_PrintAigStatus(manager);
         }
         manager->class_ = 2;

         t1 = util_cpu_ctime();

         RT_Free(cm->rm);
         if(pm->verbosity>=1)
           PureSat_PrintAigStatus(manager);
       }

       t1 = util_cpu_ctime();
       if(PureSat_TestConvergeForIP(manager,pm,cm,state,manager->IPState)){
         t2 = util_cpu_ctime();
         tCon = tCon+t2-t1;
         if(pm->verbosity>=2)
           fprintf(vis_stdout,"time for generating Convergence:%g, Total:%g\n",
                  (double)((t2-t1)/1000.0),tCon/1000);
         if(pm->verbosity>=1){
           fprintf(vis_stdout,"After test convergence:\n");
           PureSat_PrintAigStatus(manager);
         }
         fprintf(vis_stdout,"property is true\n");
         PureSat_SatFreeManager(cm);
         sat_ArrayFree(manager->assertArray);
         return TRUE;
       }
       else{
         t2 = util_cpu_ctime();
         pm->tIPCon += t2-t1;
         if(pm->verbosity>=2)
           fprintf(vis_stdout,"time for generating Convergence:%g, total:%g\n",
                  (double)((t2-t1)/1000.0),pm->tIPCon/1000);
         if(pm->verbosity>=1){
           fprintf(vis_stdout,"After test convergence:\n");
           PureSat_PrintAigStatus(manager);
         }

         manager->class_ = 0;
         state = PureSat_Or(manager,state,manager->IPState);
         PureSat_ResetManager(manager,cm,0);
         if(pm->verbosity>=1)
           fprintf(vis_stdout,"new InitState:%ld\n",state);

       }
     }/*else*/
     sat_ArrayFree(manager->assertArray);
     manager->assertArray = 0;
     PureSat_SatFreeManager(cm);
     firstTime = FALSE;
   }/*inner While(1){*/
   /*sat_ArrayInsert(previousResultArray, bAig_Not(property)); */
 }/*outer While(1){*/
 st_free_table(tmpTable);

 sat_ArrayFree(manager->EqArray);
 return TRUE;
}


boolean PureSat_CheckAceByIP(Ntk_Network_t *network,
                             PureSat_Manager_t * pm,
                             PureSat_IncreSATManager_t *pism,
                             array_t *vertexArray,
                             int * k,
                             Ctlsp_Formula_t *ltlFormula,
                             bAigEdge_t * returnProp,
                             array_t *previousResultArray)
{
  int oldPos;
  boolean firstTime,fork=0,ExistACE;
  int round,oldLength,coiCon,coiAbs;
  bAigEdge_t property;
  double t1,t2,t3,t4,t5, threshold_sw=0;
  satManager_t * cm;
  array_t *bVarList,*mVarList;
  bAigEdge_t state, tmpState;
  BmcOption_t  *options = BmcOptionAlloc();
  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);

  bVarList = mAigReadBinVarList(manager);
  mVarList = mAigReadMulVarList(manager);
  options->printInputs = TRUE;
  options->verbosityLevel = BmcVerbosityMax_c;

  assert(*k>=1);
  manager->test2LevelMini = 1;
  bAig_PureSat_ExpandTimeFrame(network, manager, pm,*k,
                               BMC_NO_INITIAL_STATES);
  manager->test2LevelMini = 0;
  PureSat_CleanMask(manager,ResetVisibleVarMask);
  PuresatMarkVisibleVar(network,vertexArray,pm,0,*k+1);
  PureSat_CleanMask(manager,ResetGlobalVarMask);

  PureSat_MarkGlobalVar_AbRf(manager,1);
  oldLength = *k;

  while(1){
    if(fork){
      oldLength = pm->Length;
      (*k) += round-1;
      pm->Length = *k;
    }
    fork=1;
    if(pm->verbosity>=1)
      fprintf(vis_stdout,"\nk = %d InitState = %ld\n",*k,manager->InitState);
    manager->test2LevelMini = 1;
    t1 = util_cpu_ctime();
    bAig_PureSat_ExpandTimeFrame(network, manager, pm,*k,
                                 BMC_NO_INITIAL_STATES);
    t2 = util_cpu_ctime();
    pm->tExp += t2-t1;
    if(pm->verbosity>=2)
      fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
             (double)((t2-t1)/1000.0),pm->tExp/1000);
    manager->test2LevelMini = 0;
    PureSat_CleanMask(manager,ResetVisibleVarMask);
    PuresatMarkVisibleVar(network,vertexArray,pm,0,*k+1);
    manager->class_ = *k+1;
    property = PureSatCreatebAigOfPropFormula(network,
                manager, *k, ltlFormula, BMC_NO_INITIAL_STATES);
    property = bAig_Not(property);
    *returnProp = property;
    if(pm->verbosity>=1)
      fprintf(vis_stdout,"property is %ld\n",property);
    oldPos = manager->nodesArraySize-bAigNodeSize;
    if(pm->verbosity>=1){
      fprintf(vis_stdout,"After expanding TF and building property\n");
      PureSat_PrintAigStatus(manager);
    }
    firstTime = TRUE;
    round = 0;
    state = manager->InitState;
    /*for one length*/
    while(1){
      round++;
      if(pm->verbosity>=1)
        fprintf(vis_stdout,"round:%d for k = %d\n",round,*k);
      manager->assertArray = sat_ArrayAlloc(1);
      if(state!=bAig_One)
        sat_ArrayInsert(manager->assertArray,state);
      cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
      cm->option->IP = 1;
      cm->option->AbRf = 1;


      if(round == 1){
        PureSat_ResetCoi(cm);
        sat_SetConeOfInfluence(cm);
        if(pm->verbosity>=1)
          fprintf(vis_stdout,"COI nodes if check concrete model:\n");
        coiCon = PureSat_CountNodesInCoi(cm);
        if(pm->verbosity>=1)
          fprintf(vis_stdout,"There are %d node in COI\n",coiCon);
      }

      t1 = util_cpu_ctime();

      PureSatSetCOI(network,pm,cm,pm->vertexTable,0, *k,*k);
      t2 = util_cpu_ctime();
      pm->tPro += t2-t1;
      if(pm->verbosity>=2)
        fprintf(vis_stdout,"process time:%g,total:%g\n",
               (double)((t2-t1)/1000.0),pm->tPro/1000);
      /*switch to concrete model*/
      if(pm->verbosity>=1)
        fprintf(vis_stdout,"normal COI:\n");
      coiAbs = PureSat_CountNodesInCoi(cm);
      if(round == 1){
        if(pm->verbosity>=1)
          fprintf(vis_stdout,"Coi of abs divided by Coi of con: %g\n",
                 (double)coiAbs/(double)coiCon);
#if SWITCH_DA
        if((double)coiAbs/(double)coiCon >= 0.68&&*k>=5){
          if(pm->switch_da == 0){
            if(pm->verbosity>=1)
              fprintf(vis_stdout,"Switch to DirAdd mode\n");
            pm->switch_da = 1;
          }
        }
#endif

        if(pm->Switch)
          threshold_sw = 0.68;
        else
          threshold_sw = 1.1;

        if(((double)coiAbs/(double)coiCon) >= threshold_sw&&*k>=5){

          t3 = util_cpu_ctime();
          sat_ArrayFree(manager->assertArray);
          manager->assertArray = 0;
          if(pm->verbosity>=1)
            fprintf(vis_stdout,"Abs model is large, go to Concrete model\n");
          ExistACE = PureSatIPOnCon(network,ltlFormula,pm);
          PureSat_SatFreeManager(cm);
          t1 = util_cpu_ctime();
          if(pm->verbosity>=1)
            fprintf(vis_stdout,"Run on concrete model: %g\n",(double)((t1-t3)/1000.0));
          if(ExistACE){
            pm->returnVal = 1;
            return FALSE;
          }
          else{
            pm->returnVal = -1;
            return TRUE;
          }
        }
      }

      PureSatKillPseudoGV(network,pm,pm->vertexTable,1,*k);
      PureSat_ResetManager(manager,cm,0);
      PureSatProcessFanout(cm);

      t1 = util_cpu_ctime();
      sat_Main(cm);
      if(pm->verbosity>=2)
        sat_ReportStatistics(cm,cm->each);
      cm->option->IP = 0;
      if(manager->NodesArray!=cm->nodesArray)
        /*cm->nodesArray may be reallocated*/
        manager->NodesArray = cm->nodesArray;
      t2 = util_cpu_ctime();
      pm->tIPUnsat += t2 - t1;
      if(pm->verbosity>=2)
        fprintf(vis_stdout,"time for Unsat:%g, total:%g\n",
               (double)((t2-t1)/1000.0),pm->tIPUnsat/1000);
      t1 = util_cpu_ctime();
      PureSatPostprocess(manager,cm,pm);
      /*clean masks*/
      sat_CleanDatabase(cm);

      if(cm->status==SAT_UNSAT){
        PureSatProcessDummy(manager,cm,cm->rm->root);
        ResetRTree(cm->rm);
      }
      t2 = util_cpu_ctime();
      pm->tPro += t2-t1;
      if(pm->verbosity>=2)
        fprintf(vis_stdout,"process time:%g,total:%g\n",
               (double)((t2-t1)/1000.0),pm->tPro/1000);

      if(cm->status == SAT_SAT){
        /*SAT: first time->find bug, otherwise increase length*/
        if(firstTime){
          if(pm->verbosity>=1)
            fprintf(vis_stdout,"found abstract CEX of length %d\n",*k);


          PureSat_UnMarkGlobalVar(manager,1);
          RT_Free(cm->rm);
          PureSat_SatFreeManager(cm);
          sat_ArrayFree(manager->assertArray);
          return TRUE;
       }
        else{

          if(pm->verbosity>=1)
            fprintf(vis_stdout,"find bogus bug at length k=%d,round=%d,increase length\n",*k,round);
          sat_ArrayFree(manager->assertArray);
          RT_Free(cm->rm);
          PureSat_SatFreeManager(cm);
          break;
        }
      }
     else{
       /*UNSAT: get IP, add to init states, until reach convergence, which
       //means property is true
       //Bing: IP generation*/
       assert(cm->currentDecision>=-1);
       if(cm->currentDecision!=-1)
         sat_Backtrack(cm, -1);
       PureSat_ResetManager(manager,cm,1);//get rid of Conflict Clauses
       if(cm->option->coreGeneration&&cm->status == SAT_UNSAT){
         manager->class_ = 1;
         t1 = util_cpu_ctime();
         tmpState = sat_GenerateFwdIP(manager,cm,cm->rm->root,1);
         manager->IPState = PureSat_MapIP(manager,tmpState,1,0);

         /*Wheneven there is baigNode generated, Reset_Manager is necessary,
           //since NodeArray may be reallocated, # of Nodes changed*/
         PureSat_ResetManager(manager,cm,0);
         t2 = util_cpu_ctime();

         pm->tIPGen += t2 -t1;
         if(pm->verbosity>=2)
           fprintf(vis_stdout,"time for generating and mapping IP:%g, total:%g\n",
                  (double)((t2-t1)/1000.0),pm->tIPGen/1000);
         if(pm->verbosity>=1){
           fprintf(vis_stdout,"After generate IP,%ld:\n",manager->IPState);
           PureSat_PrintAigStatus(manager);
         }
         manager->class_ = 2;
         if(pm->verbosity>=1)
           fprintf(vis_stdout,"After generate IP2:%ld\n",tmpState);
         t4 = util_cpu_ctime();
         RT_Free(cm->rm);
         t5 = util_cpu_ctime();
         pm->tGFree += (t5-t4);
         if(pm->verbosity>=2)
           fprintf(vis_stdout,"GFree time :%g\n",(t5-t4)/1000);
         if(pm->verbosity>=1)
           PureSat_PrintAigStatus(manager);
         }

       t1 = util_cpu_ctime();
       if(PureSat_TestConvergeForIP_AbRf(network,cm,pm,vertexArray,
                                         state,manager->IPState)){
         t2 = util_cpu_ctime();
         pm->tIPCon += t2-t1;
         if(pm->verbosity>=2)
           fprintf(vis_stdout,"time for generating Convergence:%g, total:%g\n",
                  (double)((t2-t1)/1000.0),pm->tIPCon/1000);
         if(pm->verbosity>=1){
           fprintf(vis_stdout,"After test convergence:\n");
           PureSat_PrintAigStatus(manager);
         }
         fprintf(vis_stdout,"property is true\n");
         PureSat_SatFreeManager(cm);
         sat_ArrayFree(manager->assertArray);
         return FALSE;
       }
       else{
         t2 = util_cpu_ctime();
         pm->tIPCon += t2-t1;
         if(pm->verbosity>=2)
           fprintf(vis_stdout,"time for generating Convergence:%g, total:%g\n",
                  (double)((t2-t1)/1000.0),pm->tIPCon/1000);
         if(pm->verbosity>=1){
           fprintf(vis_stdout,"After test convergence:\n");
           PureSat_PrintAigStatus(manager);
         }
         manager->class_ = 0;
         state = PureSat_Or(manager,state,manager->IPState);
         if(pm->verbosity>=1)
           fprintf(vis_stdout,"new InitState:%ld\n",state);
       }
     }/*else */
     sat_ArrayFree(manager->assertArray);
     PureSat_SatFreeManager(cm);
     firstTime = FALSE;
    }/*inner While(1){*/
  }/*outer While(1){*/
 return FALSE;
}



boolean PureSatCheckInv_IP(Ntk_Network_t * network,
                             Ctlsp_Formula_t *ltlFormula,
                             PureSat_Manager_t *pm)
{
  lsGen     gen;
  st_generator      *stGen;
  int NumofCurrentLatch=0,Length=0,tmp=0,NumofLatch=0,i,j,k;
  int addtoAbs,latchThreshHold;
  int NumInSecondLevel=0;
  array_t * visibleArray = array_alloc(char *,0);
  array_t * invisibleArray = array_alloc(char *,0);
  array_t * refinement= array_alloc(char *,0);
  array_t * CoiArray = array_alloc(char *,0);
  array_t * arrayRC = array_alloc(char *,0);
  array_t *tmpRefinement = array_alloc(char *,0);
  array_t *tmpRefinement1 = array_alloc(char *,0),*previousResultArray ;
  char * nodeName;
  Ntk_Node_t * node, *latch;
  boolean ExistACE = FALSE,realRefine=TRUE;
  boolean firstTime = TRUE;
  bAig_Manager_t    *manager;
  BmcOption_t * options;
  bAigEdge_t   property;
  st_table * nodeToMvfAigTable;
  double t1,t2,t5, t0,t3,t4,t4total=0;
  PureSat_IncreSATManager_t * pism1;
  IP_Manager_t * ipm = IPManagerAlloc();
  satManager_t *cm;
  int * sccArray=NULL, orderCt, satStat=0;
  st_table * tmpTable;


  manager = Ntk_NetworkReadMAigManager(network);
  if (manager == NIL(bAig_Manager_t)) {
    (void) fprintf(vis_stdout,
    "** bmc error: run build_partition_maigs command first\n");
    return 1;
  }
  nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
                                                          MVFAIG_NETWORK_APPL_KEY);

  pm->supportTable = st_init_table(st_ptrcmp,st_ptrhash);
  pm->CoiTable = st_init_table(st_ptrcmp,st_ptrhash);
  pm->oldCoiTable = st_init_table(st_ptrcmp,st_ptrhash);
  pm->vertexTable = st_init_table(strcmp, st_strhash);
  pism1 = PureSatIncreSATManagerAlloc(pm);
  t0 = util_cpu_ctime();

  options = BmcOptionAlloc();
  options->verbosityLevel = BmcVerbosityMax_c;
  options->printInputs = TRUE;

  t1 = util_cpu_ctime();
  previousResultArray    = array_alloc(bAigEdge_t, 0);
  manager->class_ = 0;
  manager->ipm = ipm;
  manager->test2LevelMini = 1;
  t3 = util_cpu_ctime();
  bAig_PureSat_InitTimeFrame(network,manager,pm,0);
  t5 = util_cpu_ctime();
  pm->tExp += t5-t3;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
            (double)((t5-t3)/1000.0),pm->tExp/1000);
  manager->test2LevelMini = 0;
  if(pm->verbosity>=1){
    fprintf(vis_stdout,"after Init timeframe:\n");
    PureSat_PrintAigStatus(manager);
  }
  manager->class_ = 1;
  property = PureSatCreatebAigOfPropFormula(network,
    manager, 0, ltlFormula, BMC_NO_INITIAL_STATES);
  property = bAig_Not(property);
  if(pm->verbosity>=1)
    fprintf(vis_stdout,"property is %ld\n",property);
  if(property==0)
    return TRUE;
  if(property==1)
    return FALSE;
  manager->assertArray = sat_ArrayAlloc(1);
  sat_ArrayInsert(manager->assertArray,manager->InitState);
  cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
  sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
  cm->option->coreGeneration = 0;
  cm->option->IP = 0;
  if(pm->verbosity>=1)
    fprintf(vis_stdout,"test length 0\n");
  sat_Main(cm);
  manager->NodesArray = cm->nodesArray;
  if(cm->status==SAT_SAT){
    fprintf(vis_stdout,"find counter example of length 0\n");
    BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
                                 0, 0,options, BMC_NO_INITIAL_STATES);
    return FALSE;
  }
  cm->option->coreGeneration = 1;
  PureSat_SatFreeManager(cm);

  manager->test2LevelMini = 1;
  t3 = util_cpu_ctime();
  bAig_PureSat_ExpandTimeFrame(network, manager,pm,1, BMC_NO_INITIAL_STATES);
  t5 = util_cpu_ctime();
  pm->tExp += t5-t3;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
            (double)((t5-t3)/1000.0),pm->tExp/1000);
  manager->class_ = 2;
  manager->test2LevelMini = 0;
  property = PureSatCreatebAigOfPropFormula(network,
    manager, 1, ltlFormula, BMC_NO_INITIAL_STATES);
  property = bAig_Not(property);

  if(pm->verbosity>=1)
    fprintf(vis_stdout,"property is %ld\n",property);
  if(property==0)
    return TRUE;
  if(property==1)
    return FALSE;
  manager->assertArray = sat_ArrayAlloc(1);
  sat_ArrayInsert(manager->assertArray,manager->InitState);
  cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
  sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
  cm->option->coreGeneration = 0;
  cm->option->IP = 0;
  if(pm->verbosity>=1)
    fprintf(vis_stdout,"test length 1\n");
  sat_Main(cm);
  manager->NodesArray = cm->nodesArray;
  if(cm->status==SAT_SAT){
    fprintf(vis_stdout,"find counter example of length 1\n");
    BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
                                 1, 0,options, BMC_NO_INITIAL_STATES);
    return FALSE;
  }
  t2 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"Time for testing Length 0 and 1: %g\n",(double)((t2-t1)/1000.0));
  cm->option->coreGeneration = 1;
  PureSat_SatFreeManager(cm);
  Length = 2;
  pm->Length = Length;
  pism1->Length = Length;

  manager->test2LevelMini = 1;
  t3 = util_cpu_ctime();
  bAig_PureSat_ExpandTimeFrame(network, manager,pm,2, BMC_NO_INITIAL_STATES);
  t5 = util_cpu_ctime();
  pm->tExp += t5-t3;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
            (double)((t5-t3)/1000.0),pm->tExp/1000);
  manager->class_ = 3;
  manager->test2LevelMini = 0;
  property = PureSatCreatebAigOfPropFormula(network,
    manager, 2, ltlFormula, BMC_NO_INITIAL_STATES);
  property = bAig_Not(property);
  if(property==0)
    return TRUE;
  if(property==1)
    return FALSE;

  if(pm->verbosity>=1)
    fprintf(vis_stdout,"property is %ld\n",property);
  manager->test2LevelMini = 1;


  NumofCurrentLatch=0;
  t3 = util_cpu_ctime();
  PureSatBmcGetCoiForLtlFormula_New(network, ltlFormula,pm->oldCoiTable);
  t5 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"Compute NTK COI :%g\n",(t5-t3)/1000);

  pm->CoiTable = st_copy(pm->oldCoiTable);

  /*new COI computation*/
  t3 = util_cpu_ctime();
  tmpTable = PureSatGetAigCoi(network,pm,property);
  st_foreach_item(tmpTable,stGen,&nodeName,NIL(char*)){
    latch = Ntk_NetworkFindNodeByName(network,nodeName);
#if 1
    if(!st_lookup(pm->CoiTable,latch,NIL(char*)))
      if(pm->verbosity>=2)
        fprintf(vis_stdout,"%s is not in CoiTable\n",nodeName);
#endif
    st_insert(pm->CoiTable,latch,(char*)0);
  }
#if 1
  st_foreach_item(pm->CoiTable,stGen,&latch,NIL(char*)){
    nodeName = Ntk_NodeReadName(latch);
    if(!st_lookup(tmpTable,nodeName,NIL(char*)))
      if(pm->verbosity>=2)
        fprintf(vis_stdout,"%s is not in Aig CoiTable\n",nodeName);
  }
#endif
  st_free_table(tmpTable);
  t5 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"Compute AIG COI :%g\n",(t5-t3)/1000);


  t3 = util_cpu_ctime();
  pm->vertexTable = PureSatCreateInitialAbstraction(network,
                      ltlFormula,&NumofCurrentLatch,pm);
  t5 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"the time to create init abs:%g\n",(t5-t3)/1000);
  tmpTable = st_init_table(strcmp,st_strhash);
  PureSatCreateInitAbsByAIG(manager,pm,property,tmpTable);
  st_foreach_item(tmpTable,stGen,&nodeName,NIL(char*)){
    if(!st_lookup(pm->vertexTable,nodeName,NIL(char*))){
      st_insert(pm->vertexTable,nodeName,(char*)0);
      if(pm->verbosity>=1)
        fprintf(vis_stdout,"insert %s into init abs model\n",nodeName);
    }
  }
  st_free_table(tmpTable);
  t3 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"the time to create init AIG abs:%g\n",(t3-t5)/1000);

  PureSatPreProcLatch(network,pm);
  t5 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"the time to preproc:%g\n",(t5-t3)/1000);

  /*put indentical latches of visible latch into abs*/
  t3 = util_cpu_ctime();
  PureSatGetIndenticalLatch(network,pm);
  st_foreach_item(pm->vertexTable,stGen,&nodeName,NIL(char*))
    array_insert_last(char*,visibleArray,nodeName);
  PureSatAddIdenLatchToAbs(network,pm,visibleArray);
  arrayForEachItem(char*,visibleArray,i,nodeName)
    st_insert(pm->vertexTable,nodeName,(char*)0);
  array_free(visibleArray);
  visibleArray = array_alloc(char*,0);
  t5 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"Merge identical latch:%g\n",(t5-t3)/1000);

  NumofCurrentLatch = st_count(pm->vertexTable);

  t3 = util_cpu_ctime();
  pm->AbsTable = st_init_table(st_ptrcmp,st_ptrhash);

  Ntk_NetworkForEachLatch(network, gen, node){
    if (st_lookup_int(pm->CoiTable, (char *) node, &tmp)){
      NumofLatch++;
      nodeName = Ntk_NodeReadName(node);
      if(st_lookup(pm->vertexTable,nodeName,NIL(char *)))
        {
          array_insert_last(char *,visibleArray,nodeName);
          latch = Ntk_NetworkFindNodeByName(network,nodeName);
          PureSatComputeTableForLatch(network,pm->AbsTable,latch);
        }
      else
        array_insert_last(char *,invisibleArray,nodeName);
    }
  }
  t5 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"the time to cmpute abs table:%g\n",(t5-t3)/1000);
  if(pm->verbosity>=1){
    fprintf(vis_stdout,"visiblearray has %d latches\n",array_n(visibleArray));
    fprintf(vis_stdout,"invisibleArray has %d latches\n",array_n(invisibleArray));
  }
  CoiArray = array_dup(visibleArray);
  array_append(CoiArray,invisibleArray);

  pm->nicTable = st_init_table(strcmp,st_strhash);
  pm->niaTable = st_init_table(strcmp,st_strhash);
  PureSatComputeNumGatesInCone(network,pm,CoiArray);
  t3 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"the time to cmpute gates in cone:%g\n",(t3-t5)/1000);

  /*Using DFS + Dir Cone in abs*/
  pm->node2dfsTable = st_init_table(st_ptrcmp,st_ptrhash);


  while(NumofCurrentLatch < NumofLatch)
    {
      t3 = util_cpu_ctime();
      if(pm->verbosity>=1)
        fprintf(vis_stdout,"Current Latches: %d, COI latches:%d,NEW Length:%d,\n",
                NumofCurrentLatch,NumofLatch,pm->Length);
      if(pm->verbosity>=2)
        fprintf(vis_stdout,"General time: %g\n",(double)((t3-t0)/1000.0));
      t1 = util_cpu_ctime();
      tmpRefinement = array_alloc(char *,0);

      memset(manager->ipm,0,sizeof(IP_Manager_t));
      firstTime = TRUE;
      pm->SufAbsTable = st_init_table(st_ptrcmp,st_ptrhash);
      if(realRefine){
        arrayForEachItem(char *,refinement,i,nodeName)
          {
            latch = Ntk_NetworkFindNodeByName(network,nodeName);
            PureSatComputeTableForLatch(network,pm->AbsTable,latch);
            st_insert(pm->vertexTable,nodeName,(char*)0);
          }
        array_append(visibleArray,refinement);
        array_free(invisibleArray);
        invisibleArray = array_alloc(char *,0);
        st_foreach_item(pm->CoiTable,stGen,&latch,&i)
          {
            nodeName = Ntk_NodeReadName(latch);
            if(!st_lookup(pm->vertexTable,nodeName,(char **)0)){
              array_insert_last(char *,invisibleArray,nodeName);
            }
          }
        st_free_table(pm->node2dfsTable);
        pm->node2dfsTable = st_init_table(st_ptrcmp,st_ptrhash);
        arrayRC = PureSatComputeOrder_2(network,pm,visibleArray,invisibleArray,sccArray,&NumInSecondLevel);
        t4 = util_cpu_ctime();
        if(pm->verbosity>=2)
          fprintf(vis_stdout,"time for compute order: %g\n",(t4-t1)/1000);

        if(pm->RefPredict){
          orderCt=0;
          if(array_n(pm->latchArray)>0){
            if(pm->verbosity>=1)
              fprintf(vis_stdout,"\n%d: Adding high RC value latch into abs model\n",orderCt++);
            PureSatAddIdenLatchToAbs(network,pm,pm->latchArray);
            NumofCurrentLatch+=array_n(pm->latchArray);
            arrayForEachItem(char *,pm->latchArray,i,nodeName){
              latch = Ntk_NetworkFindNodeByName(network,nodeName);
              PureSatComputeTableForLatch(network,pm->AbsTable,latch);
              st_insert(pm->vertexTable,nodeName,(char*)0);
            }
            array_append(visibleArray,pm->latchArray);
            array_free(pm->latchArray);
            array_free(invisibleArray);
            invisibleArray = array_alloc(char *,0);
            st_foreach_item(pm->CoiTable,stGen,&latch,&i)
              {
                nodeName = Ntk_NodeReadName(latch);
                if(!st_lookup(pm->vertexTable,nodeName,(char **)0)){
                  array_insert_last(char *,invisibleArray,nodeName);
                }
              }
            st_free_table(pm->node2dfsTable);
            pm->node2dfsTable = st_init_table(st_ptrcmp,st_ptrhash);
            arrayRC = PureSatComputeOrder_2(network,pm,visibleArray,invisibleArray,sccArray,&NumInSecondLevel);

          }
          array_free(pm->latchArray);
        }

        PureSat_CleanMask(manager,ResetVisibleVarMask);
        PuresatMarkVisibleVar(network,visibleArray,pm,0,pm->Length);

        addtoAbs =(int)((double)(array_n(CoiArray)-array_n(visibleArray))/(double)5)+1;
        addtoAbs = addtoAbs >50 ? 50: addtoAbs;

        array_free(invisibleArray);
        invisibleArray = array_alloc(char *,0);
        st_foreach_item(pm->CoiTable,stGen,&latch,&i)
          {
            nodeName = Ntk_NodeReadName(latch);
            if(!st_lookup(pm->vertexTable,nodeName,(char **)0)){
              array_insert_last(char *,invisibleArray,nodeName);
            }
          }
        if(pm->verbosity>=1){
          fprintf(vis_stdout,"After adding high RC latches:\n");
          fprintf(vis_stdout,"visiblearray has %d latches\n",array_n(visibleArray));
          fprintf(vis_stdout,"invisibleArray has %d latches\n",array_n(invisibleArray));
        }
        t4 = util_cpu_ctime();
        t4total += t4-t3;
        if(pm->verbosity>=2)
          fprintf(vis_stdout,"compute and add high RC latch and recompute order:%g,total:%g\n",
                 (t4-t3)/1000,(t4total/1000.0));

        if(pm->verbosity>=1)
          fprintf(vis_stdout,"NumInSecondLevel is %d  ",NumInSecondLevel);
        latchThreshHold = NumInSecondLevel;
        if(pm->verbosity>=2){
          fprintf(vis_stdout,"New latchThreshHold is %d\n",latchThreshHold);
        }
        t2 = util_cpu_ctime();
        if(pm->verbosity>=2){
          fprintf(vis_stdout,"Recompute Order: %g\n",(double)((t2-t1)/1000.0));
        }
        array_free(refinement);
        refinement = array_alloc(char *,0);
     }/* if(realRefine)*/

     /* means no ref, just Length++.*/
      realRefine =FALSE;
      t1 = util_cpu_ctime();

      ExistACE = PureSat_CheckAceByIP(network,pm,pism1, visibleArray,&Length,
                              ltlFormula, &property,previousResultArray);
      if(ExistACE)
        {
          if(pm->returnVal == -1){
             PureSatIncreSATManagerFree(pm,pism1);
             /*PureSatManagerFree(pm);*/
             array_free(CoiArray);
             BmcOptionFree(options);
             return FALSE;
          }
          pm->Length = Length;
          pism1->Length = Length;
          t2 = util_cpu_ctime();
          pm->tIP += t2-t1;
          if(pm->verbosity>=2)
            fprintf(vis_stdout,"Solve on IP: %g, total: %g\n",
                   (double)((t2-t1)/1000.0),(double)pm->tIP/1000.0);


          if(ExistACE)
            {
              int Con=0;
              if(pm->verbosity>=1)
                fprintf(vis_stdout,"found Abstract Counterexample at length %d\n", pm->Length);
              realRefine = TRUE;

              /*incrementally check Concrete Model*/
              if(pm->verbosity>=1)
                fprintf(vis_stdout,"Begin building a new abstract model\n");
              for(i=0;i<array_n(arrayRC);i=i+latchThreshHold)
                {
                  Con = 0;
                  if(i>0)
                    latchThreshHold = array_n(arrayRC)-latchThreshHold;
                  for(j=0;j<latchThreshHold;j++)
                    {
                      if((i+j)<array_n(arrayRC))
                        {
                          nodeName = array_fetch(char *,arrayRC,i+j);
                          array_insert_last(char *,tmpRefinement,nodeName);
                          if(pm->verbosity>=2)
                            if(pm->verbosity>=2)
                              fprintf(vis_stdout, "picking %s\n",nodeName);
                          if((i+j)==(array_n(arrayRC)-1))
                            Con = 1;
                        }
                      else{
                        Con = 1;
                        break;
                      }
                    }/* for(j=0;*/
                  tmpRefinement1=array_dup(visibleArray);
                  array_append(tmpRefinement1,tmpRefinement);

                  t1 = util_cpu_ctime();

                  if(pm->verbosity>=2)
                    satStat = 1;
                  if(!PureSat_ConcretTest(network,pm,tmpRefinement1,property,previousResultArray,Con,satStat,1)){

                    t2 = util_cpu_ctime();
                    pm->tCon = pm->tCon+t2-t1;
                    if(pm->verbosity>=2)
                      fprintf(vis_stdout,"time for finding a sufficient set on model: %g, total:%g\n",
                             (double)((t2-t1)/1000.0),(double)pm->tCon/1000.0);
                    if((i+j)>=array_n(arrayRC)){
                      fprintf(vis_stdout,"found real counterexamples\n");

                      PureSatIncreSATManagerFree(pm, pism1);
                      /*PureSatManagerFree(pm);*/
                      array_free(CoiArray);
                      BmcOptionFree(options);
                      return FALSE;
                    }
                    /* else{
                      ;
                      }*/
                  }
                  else{
                    t2 = util_cpu_ctime();
                    pm->tCon = pm->tCon+t2-t1;
                    if(pm->verbosity>=1)
                      fprintf(vis_stdout,"found a sufficient model\n");
                    if(pm->verbosity>=2)
                      fprintf(vis_stdout,"time for finding a sufficient set on model: %g, total:%g\n",
                             (double)((t2-t1)/1000.0),(double)pm->tCon/1000.0);
                    firstTime = FALSE;
                    arrayForEachItem(char *,tmpRefinement1,k,nodeName){
                      node = Ntk_NetworkFindNodeByName(network, nodeName);
                      if(!st_lookup(pm->SufAbsTable,(char *)node,NIL(char *)))
                        st_insert(pm->SufAbsTable,(char *)node, (char *)0);
                      else{
                        fprintf(vis_stdout,"wrong in sufabstable \n");
                        exit(0);
                      }
                    }
                    array_free(tmpRefinement1);
                    break;
                  }
                  array_free(tmpRefinement1);
                }

              t1 = util_cpu_ctime();

#if 1
              if(pm->savedConCls){
                sat_ArrayFree(pm->savedConCls);
                pm->savedConCls = 0;
              }
#endif
#if SWITCH_DA
              refinement = PureSat_RefineOnAbs_DA(network,pm,property,previousResultArray,
                                                  latchThreshHold,sccArray,tmpRefinement);
#else
              refinement = PureSat_RefineOnAbs(network,pm,property,previousResultArray,
                                               latchThreshHold,sccArray,tmpRefinement);
#endif
              array_free(tmpRefinement);
              t2 = util_cpu_ctime();
              pm->tRef = pm->tRef+t2-t1;
              if(pm->verbosity>=2)
                fprintf(vis_stdout,"time for RefOnAbs: %g, total:%g\n",
                       (t2-t1)/1000.0,pm->tRef/1000);
              st_free_table(pm->SufAbsTable);
              pm->SufAbsTable = 0;

              /*adjust parameters*/
              NumofCurrentLatch+=array_n(refinement);
              pm->Length++;
              pism1->Length++;
              Length++;
            }/* if(pism2->cm->status == SAT_SAT)*/
        } /*if(ExistACE)*/
      else /* if TRUE from IP*/
        {
          t2 = util_cpu_ctime();
          pm->tIP = pm->tIP+t2-t1;
          if(pm->verbosity>=2)
            fprintf(vis_stdout,"Solve on IP: %g, total: %g\n",
                   (t2-t1)/1000.0,pm->tIP/1000.0);
          fprintf(vis_stdout,"Convergence reached, exit\n");
          PureSatIncreSATManagerFree(pm,pism1);
          /*PureSatManagerFree(pm);*/
          array_free(CoiArray);
          BmcOptionFree(options);
          return TRUE;
        }
    }/* while(NumofCurrentLatch < NumofLatch)*/
  /*st_free_table(AbsTable);*/

  /*Now go to the concrete model*/
  if(pm->verbosity>=1)
    fprintf(vis_stdout,"reach concrete model\n");
  array_append(visibleArray,refinement);
  array_free(refinement);


  ExistACE = PureSatIPOnCon(network,ltlFormula,pm);
  ExistACE = !ExistACE;
  PureSatIncreSATManagerFree(pm,pism1);
  /*PureSatManagerFree(pm);*/
  array_free(CoiArray);
  BmcOptionFree(options);
  if(ExistACE)
    return FALSE;
  else
    return TRUE;
}