src/puresat/puresatIPRefine.c

Go to the documentation of this file.

#include "puresatInt.h"


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

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

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

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

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

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

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

#if UNSATCORE
void PureSat_GetSufAbsFromCoreRecur(mAig_Manager_t *manager,
                                    satManager_t * cm,
                                    RTnode_t RTnode,
                                    st_table *ctTable,
                                    st_table *refineTable,
                                    FILE * fp)
#else
void PureSat_GetSufAbsFromCoreRecur(mAig_Manager_t *manager,
                                    satManager_t * cm,
                                    RTnode_t RTnode,
                                    st_table *ctTable,
                                    st_table *refineTable)
#endif
{
  int i,ct;
  bAigTimeFrame_t *tf = manager->timeframeWOI;
  char *name;
  bAigEdge_t v,*lp;
  st_table *table;
  st_generator *stgen;
  RTManager_t * rm = cm->rm;

  if(RT_flag(RTnode)&RT_VisitedMask)
    return;

  RT_flag(RTnode) |= RT_VisitedMask;
  /*leaf*/
  if(RT_pivot(RTnode)==0){
#if DBG
    assert(RT_oriClsIdx(RTnode)==0);
#endif
    if(RT_oriClsIdx(RTnode)!=0)
      lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
    else

      lp = RT_formula(RTnode) + cm->rm->fArray;
    for(i=0;i<RT_fSize(RTnode);i++,lp++){
      if(RT_oriClsIdx(RTnode)!=0)
        v = SATgetNode(*lp);
      else
        v = *lp;
      if(*lp<0)
        continue;

#if UNSATCORE
      v = SATnormalNode(v);
      fprintf(fp,"%d_%d ",v,SATclass(v));
      if(SATflags(v)&DummyMask)
        fprintf(fp,"DM ");
      if(SATflags(v)&VisibleVarMask)
        fprintf(fp,"Visible  ");
      else
        if(SATflags(v)&StateBitMask)
          fprintf(fp, "InvSV  ");

#endif
      v = SATnormalNode(v);
      if((SATflags(v)&VisibleVarMask)){

        if(SATclass(v)==0){
          if(!st_lookup(tf->idx2name,(char*)v,&name)&&
             !st_lookup(tf->MultiLatchTable,(char*)v,&table))
            continue;
        }
#if 1
        /* at least 2 times to be choosen as a candidate*/
        if(st_lookup(ctTable,(char*)v,&ct)){
          if(ct<0)
            continue;
          if(ct>=1){

            if(!st_lookup(tf->MultiLatchTable,(char*)v,&table)){
              int retVal = st_lookup(tf->idx2name,(char*)v,&name);
              assert(retVal);
              st_insert(refineTable,(char*)name,(char*)0);
              st_insert(ctTable,(char*)v,(char*)-1);

            }
            else{
#ifdef TIMEFRAME_VERIFY_
              fprintf(vis_stdout,"%d is in MultiLatchTable: ",v);
#endif
              st_foreach_item(table,stgen,(char**)&name,
                              NIL(char*)){
#ifdef TIMEFRAME_VERIFY_
                fprintf(vis_stdout,"%s   ",name);
#endif
                st_insert(refineTable,(char*)name,(char*)0);
              }
#ifdef TIMEFRAME_VERIFY_
              fprintf(vis_stdout,"\n");
#endif
              st_insert(ctTable,(char*)v,(char*)-1);
            }
          }
        }
        else{
          ct=1;
          st_insert(ctTable,(char*)v,(char*)(long)ct);
        }
#else
        retVal = st_lookup(tf->idx2name,(char*)v,(char**)&name);
        assert(retVal);
        st_insert(refineTable,(char*)name,(char*)0);

#endif
      }/* if(SATflags(v)&StateBitMask){*/
    }
#if UNSATCORE
    fprintf(fp,"0\n");
#endif
  }
  /*non leaf*/
  else{
    assert(RT_left(RTnode)!=RT_NULL&&RT_right(RTnode)!=RT_NULL);
#if UNSATCORE
    PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_left(RTnode),
                                   ctTable,refineTable,fp);
    PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_right(RTnode),
                                   ctTable,refineTable,fp);
#else
    PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_left(RTnode),
                                   ctTable,refineTable);
    PureSat_GetSufAbsFromCoreRecur(manager,cm,RT_right(RTnode),
                                   ctTable,refineTable);
#endif
  }
  return;
}

//new pick latch
#if UNSATCORE
void PureSat_GetSufAbsFromCoreRecur_2side(mAig_Manager_t *manager,
                                          satManager_t * cm,
                                          RTnode_t RTnode,
                                          st_table *ctTable,
                                          st_table *refineTable,
                                          st_table *SufNameTable,
                                          FILE * fp)
#else
void PureSat_GetSufAbsFromCoreRecur_2side(mAig_Manager_t *manager,
                                          satManager_t * cm,
                                          RTnode_t RTnode,
                                          st_table *ctTable,
                                          st_table *refineTable,
                                          st_table *SufNameTable)
#endif
{
  int i,j,find,find1,times;
  bAigTimeFrame_t *tf = manager->timeframeWOI;
  char *name,*name1;
  bAigEdge_t v,v1,*lp,*lp1, *lp2, left,right;
  st_table *table;
  st_generator *stgen;
  RTManager_t * rm = cm->rm;
  long maxNode;

  if(RT_flag(RTnode)&RT_VisitedMask)
    return;

  RT_flag(RTnode) |= RT_VisitedMask;

  if(RT_pivot(RTnode)==0){
#if DBG
    assert(RT_oriClsIdx(RTnode)==0);
#endif
    if(RT_oriClsIdx(RTnode)!=0)
      lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
    else

      lp = RT_formula(RTnode) + cm->rm->fArray;
    lp1 = lp;
    (cm->line)++;
    for(i=0;i<RT_fSize(RTnode);i++,lp++){
      if(RT_oriClsIdx(RTnode)!=0)
        v = SATgetNode(*lp);
      else
        v = *lp;
      if(*lp<0)
        continue;
#if UNSATCORE
      v = SATnormalNode(v);
      fprintf(fp,"%d_%d ",v,SATclass(v));
      if(SATflags(v)&DummyMask)
        fprintf(fp,"DM ");
      if(SATflags(v)&VisibleVarMask)
        fprintf(fp,"Visible  ");
      else
        if(SATflags(v)&StateBitMask)
          fprintf(fp, "InvSV  ");

#endif
      v = SATnormalNode(v);
#if LAI
      /*mark every node in core for latch interface abs*/
      flags(v) |= VisitedMask;
#endif
      if(SATflags(v)&VisibleVarMask){
        if((SATclass(v)==0)&&
           (st_lookup(tf->idx2name,(char*)v,&name)==0)&&
           (st_lookup(tf->MultiLatchTable,(char*)v,&table)==0))
            continue;

        lp2 = lp1;
        left = SATnormalNode(leftChild(v));
        right = SATnormalNode(rightChild(v));
        //find largest node
        maxNode = -1;
        for(j=0;j<RT_fSize(RTnode);j++,lp2++){
          if(RT_oriClsIdx(RTnode)!=0)
            v1 = SATgetNode(*lp2);
          else
            v1 = *lp2;
          if(maxNode < SATnormalNode(v1))
            maxNode = SATnormalNode(v1);
        }
        if(maxNode == v){
#if DBG
          lp2 = lp1;
          for(j=0;j<RT_fSize(RTnode);j++,lp2++){
            if(RT_oriClsIdx(RTnode)!=0)
              v1 = SATgetNode(*lp2);
            else
              v1 = *lp2;
            if(*lp2<0||SATnormalNode(v1)==v)
              continue;
            assert((SATnormalNode(v1) == SATnormalNode(leftChild(v)))||
                   SATnormalNode(v1) == SATnormalNode(rightChild(v)));
          }
#endif
          SATflags(v) |= Visited2Mask; /*left side*/
        }
        else{
#if DBG
          lp2 = lp1;
          for(j=0;j<RT_fSize(RTnode);j++,lp2++){
            if(RT_oriClsIdx(RTnode)!=0)
              v1 = SATgetNode(*lp2);
            else
              v1 = *lp2;
            if(*lp2<0||SATnormalNode(v1)==maxNode)
              continue;
            assert((SATnormalNode(v1) == SATnormalNode(leftChild(maxNode)))||
                   (SATnormalNode(v1) == SATnormalNode(rightChild(maxNode))));
          }
#endif
          SATflags(v) |= Visited3Mask; /*right side*/
#if THROUGHPICK
          /*pick latch due to split*/
            if(SATflags(v)&VPGVMask){
              if(SATclass(maxNode)<=1)
                SATflags(v) |= NewMask; /*the same tf*/
              else
                SATflags(v) |= Visited4Mask; /* larger tf*/
            }
#endif
        }

      }

#if THROUGHPICK
      if((SATflags(v)&VisibleVarMask)&&
         (((SATflags(v)&Visited2Mask)&&(SATflags(v)&Visited3Mask))||
         ((SATflags(v)&Visited4Mask)&&(SATflags(v)&NewMask)))){
#else
      if((SATflags(v)&VisibleVarMask)&&
         ((SATflags(v)&Visited2Mask)&&(SATflags(v)&Visited3Mask))){
#endif
        times = 1;
        if(!st_lookup(tf->MultiLatchTable,(char*)v,&table)){
          int retVal = st_lookup(tf->idx2name,(char*)v,&name);
          assert(retVal);

          if(st_lookup(refineTable,(char*)name,&times))
            times++;
          st_insert(refineTable,(char*)name,(char*)(long)times);
        }

        /*for iden latches, we only add one, which is enough*/
        else{
          find = 0;
          find1 = 0;
          st_foreach_item(table,stgen,(char**)&name,
                          NIL(char*)){
            if(st_lookup(refineTable,name,NIL(char*))){
              find = 1;
              break;
            }
            if(find1==0){
              if(st_lookup(SufNameTable,name, NIL(char*))){
                name1 = name;
                find1 = 1;
              }
            }
          }
          if(find==0){
            times = 1;
            if(st_lookup(refineTable,(char*)name1,&times))
              times++;
            st_insert(refineTable,(char*)name1,(char*)(long)times);

          }
        }


      }
    }
#if UNSATCORE
   fprintf(fp,"0\n");
#endif
  }
    /*non leaf*/
  else{
    assert(RT_left(RTnode)!=RT_NULL&&RT_right(RTnode)!=RT_NULL);
#if UNSATCORE
    PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_left(RTnode),
                                   ctTable,refineTable,SufNameTable,fp);
    PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_right(RTnode),
                                   ctTable,refineTable,SufNameTable,fp);
#else
    PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_left(RTnode),
                                   ctTable,refineTable,SufNameTable);
    PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,RT_right(RTnode),
                                   ctTable,refineTable,SufNameTable);
#endif
  }
  return;
}



array_t * PureSat_GetSufAbsFromCore(Ntk_Network_t *network,
                                    satManager_t * cm,
                                    PureSat_Manager_t *pm,
                                    bAigEdge_t property,
                                    st_table * SufAbsNameTable)
{
  array_t * refArray = array_alloc(char *,0);
  char *name;
  st_generator *stgen;
  Ntk_Node_t *latch;
  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  st_table * ctTable = st_init_table(st_numcmp,st_numhash);
  st_table * refineTable = st_init_table(strcmp,st_strhash);
  int times;
#if UNSATCORE
  FILE * fp = fopen("unsatcore.txt","w");
#endif
#if LAI
  st_table * refineTable1 = st_init_table(strcmp,st_strhash);

#endif


  PureSat_CleanMask(manager,ResetVisited1234NewMask);
#if UNSATCORE
  fprintf(fp,"p cnf %d line, # nodes:%d\n",
          cm->initNumVariables,cm->nodesArraySize);
  cm->line = 0;
  PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,cm->rm->root,
                                 ctTable,refineTable,SufAbsNameTable,fp);
  fprintf(fp,"total lines: %d\n",cm->line);
#else
  PureSat_GetSufAbsFromCoreRecur_2side(manager,cm,cm->rm->root,
                                 ctTable,refineTable,SufAbsNameTable);

#endif
  PureSat_CleanMask(manager,ResetVisited1234NewMask);

#if LAI
  ResetRTree(cm->rm);
  PureSat_GetLIAForNode(manager,property);
  PureSat_GetSufAbsByLIA(manager,cm,cm->rm->root,
                        refineTable1);
#endif


  st_foreach_item(refineTable,stgen,&name,&times){
    latch = Ntk_NetworkFindNodeByName(network,name);

    if(!st_lookup(pm->vertexTable,(char*)name,NIL(char*))&&
      st_lookup(pm->SufAbsTable, (char*)latch,NIL(char*))){
      array_insert_last(char *,refArray,name);
      if(pm->verbosity>=2)
        fprintf(vis_stdout,"ref cand:%s %d\n",name,times);
    }
  }

#if LAI
  st_foreach_item(refineTable1,stgen,(char**)&name,NIL(char*)){
    latch = Ntk_NetworkFindNodeByName(network,name);
    if(!st_lookup(pm->vertexTable,(char*)name,NIL(char*))&&
       st_lookup(pm->CoiTable, (char*)latch,NIL(char*))){
      if(pm->verbosity>=2)
        fprintf(vis_stdout,"from LIA ref candidate:%s\n",name);

    }
  }
#endif

#if UNSATCORE
  fclose(fp);
#endif

  st_free_table(ctTable);
  st_free_table(refineTable);
#if LAI
  st_free_table(refineTable1);
#endif
  return refArray;
}



array_t *PureSat_RefineOnAbs(Ntk_Network_t *network,
                             PureSat_Manager_t *pm,
                             bAigEdge_t property,
                             array_t *previousResultArray,
                             int latchThreshHold,
                             int * sccArray,
                             array_t * sufArray)
{
  array_t * tmpRef,*tmpRef1,*tmpRef2,*tmpRef3;
  array_t * tmpModel = array_alloc(char *,0),*tmpArray1,*tmpArray2;
  satManager_t *cm;
  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  st_table *table;
  char * name;
  int i,j;
  int NumInSecondLevel;
  st_generator *stgen;
  Ntk_Node_t *latch;
  double t1,t2,t3,t4;
  st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
  st_table * junkTable;
  int noArosat = 1;


  tmpRef = array_alloc(char *,0);
  st_foreach_item(pm->SufAbsTable,stgen,&latch,NIL(char*)){
    name = Ntk_NodeReadName(latch);
    if(st_lookup(pm->vertexTable,name,NIL(char *)))
      array_insert_last(char *,tmpModel,name);
    array_insert_last(char *,tmpRef,name);
    st_insert(SufAbsNameTable,name,(char *)0);

  }

  t1 = util_cpu_ctime();
  manager->assertArray = sat_ArrayAlloc(1);
  sat_ArrayInsert(manager->assertArray,manager->InitState);
  cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
  if(pm->Arosat){
    cm->option->decisionHeuristic &= RESET_LC;
    cm->option->decisionHeuristic |= DVH_DECISION;
    cm->option->arosat = 1;
  }
  cm->option->coreGeneration = 1;
  cm->option->AbRf = 1;
  cm->property = property;
  cm->option->IP = 1;
  PureSat_CleanMask(manager,ResetVisibleVarMask);
  PuresatMarkVisibleVarWithVPGV(network,tmpRef,pm,0,pm->Length+1);
  array_free(tmpRef);
  t3 = util_cpu_ctime();
  PureSatPreprocess(network,cm,pm,SufAbsNameTable,pm->Length);
  t4 = util_cpu_ctime();
  pm->tPro += t4-t3;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"process time:%g,total:%g\n",
           (double)((t4-t3)/1000.0),pm->tPro/1000);

  if(cm->option->arosat){
    PureSatCreateLayer(network,pm,cm,tmpModel,sufArray);
    cm->Length = pm->Length;
    AS_Main(cm);
    noArosat = 0;
    st_foreach_item(cm->layerTable,stgen,&table,NIL(char*))
      st_free_table(table);
    st_free_table(cm->layerTable);
    FREE(cm->assignedArray);
    FREE(cm->numArray);
  }
  else
    sat_Main(cm);

  manager->NodesArray = cm->nodesArray;;
  assert(cm->status==SAT_UNSAT);
  t3 = util_cpu_ctime();
  PureSatPostprocess(manager,cm,pm);
  PureSatProcessDummy(manager,cm,cm->rm->root);
  ResetRTree(cm->rm);
  t4 = util_cpu_ctime();
  pm->tPro += t4-t3;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"process time:%g,total:%g\n",
           (double)((t4-t3)/1000.0),pm->tPro/1000);
  t2 = util_cpu_ctime();
  pm->tCoreGen += t2 - t1;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"time for UNsat core generation:%g,total:%g\n",
           (double)(t2-t1)/1000.0,pm->tCoreGen/1000.0);

  t1 = util_cpu_ctime();
  tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable);
  t2 = util_cpu_ctime();

  st_free_table(SufAbsNameTable);
  RT_Free(cm->rm);
  sat_ArrayFree(manager->assertArray);
  PureSat_SatFreeManager(cm);

  /*Get suff set*/
  tmpRef2 = array_alloc(char *,0);
  tmpRef3 = array_alloc(char *,0);
  tmpArray1 = array_alloc(char *,0);
  tmpArray2 = array_alloc(char *,0);

  if(noArosat){
    t1 = util_cpu_ctime();
    if(array_n(tmpRef1)){
      tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1,
                                        &NumInSecondLevel);
      array_free(pm->latchArray);
    }

  }
  else{
    if(array_n(tmpRef1)){
      tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1,
                                        &NumInSecondLevel);
      array_free(pm->latchArray);
    }
    else
      tmpRef = array_alloc(char*,0);
#if NOREFMIN
    if(pm->verbosity>=1){
      fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n");
      arrayForEachItem(char *,tmpRef,i,name)
        fprintf(vis_stdout,"%s\n",name);
    }
    PureSatAddIdenLatchToAbs(network,pm,tmpRef);
    array_free(tmpRef1);
    array_free(tmpModel);
    return tmpRef;
#endif
  }


  /*Ref Minimization
    //try all the candidates*/
  t1 = util_cpu_ctime();

  if(pm->CoreRefMin && array_n(tmpRef)>=5){
    if(pm->verbosity>=1)
      fprintf(vis_stdout,"Core Ref Min\n");
    junkTable = st_init_table(strcmp,st_strhash);
    for(i=array_n(tmpRef)-1;i>=0;i--)
      {
        array_t * tmpA;
        name = array_fetch(char *,tmpRef,i);
        if(pm->verbosity>=1)
          fprintf(vis_stdout,"RefMin: testing %s\n",name);
        tmpArray2 = PureSatRemove_char(tmpRef,i);
        if(st_lookup(junkTable,name,NIL(char))){
          array_free(tmpRef);
          tmpRef = tmpArray2;
          if(pm->verbosity>=1)
            fprintf(vis_stdout,"%s is junk\n",name);
          continue;
        }
        tmpA = array_dup(tmpModel);
        array_append(tmpA,tmpArray2);

        t3 = util_cpu_time();
        tmpArray1 = array_alloc(char*,0);
        arrayForEachItem(char*,tmpA,j,name)
          if(!st_lookup(junkTable,name,NIL(char)))
            array_insert_last(char*,tmpArray1,name);
        array_free(tmpA);

        if(!PureSat_ConcretTest_Core(network,pm,tmpArray1,property,
                                     previousResultArray,junkTable)){
          /*then the candidate can' be deleted*/
          t4 = util_cpu_time();
          if(pm->verbosity>=2)
            fprintf(vis_stdout," %g\n",(t4-t3)/1000);
          array_free(tmpArray2);
        }
        else /*delete it*/
          {
            t4 = util_cpu_time();
            if(pm->verbosity>=2)
              fprintf(vis_stdout,"time: %g\n",(t4-t3)/1000);
            array_free(tmpRef);
            tmpRef = tmpArray2;
          }
        array_free(tmpArray1);
      }
    st_free_table(junkTable);
  }
  else{
    for(i=array_n(tmpRef)-1;i>=0;i--)
      {
        name = array_fetch(char *,tmpRef,i);

        if(pm->verbosity>=1)
          fprintf(vis_stdout,"RefMin: testing %s\n",name);
        tmpArray2 = PureSatRemove_char(tmpRef,i);
        tmpArray1 = array_dup(tmpModel);
        array_append(tmpArray1,tmpArray2);

        t3 = util_cpu_time();
        if(!PureSat_ConcretTest(network,pm,tmpArray1,property,
                                previousResultArray,0,0,0)){
          t4 = util_cpu_time();
          if(pm->verbosity>=2)
            fprintf(vis_stdout," %g\n",(t4-t3)/1000);
          array_free(tmpArray2);
        }
        else /*delete it*/
          {
            t4 = util_cpu_time();
            if(pm->verbosity>=2)
              fprintf(vis_stdout,"time: %g\n",(t4-t3)/1000);
            array_free(tmpRef);
            tmpRef = tmpArray2;
          }
        array_free(tmpArray1);
      }
  }


  t2 = util_cpu_ctime();
  pm->tRefMin += t2 - t1;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"\ntime for Ref Min: %g, total:%g\n",
           (t2-t1)/1000,pm->tRefMin/1000);
  if(pm->verbosity>=1){
    fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n");
    arrayForEachItem(char *,tmpRef,i,name)
      fprintf(vis_stdout,"%s\n",name);
  }
  PureSatAddIdenLatchToAbs(network,pm,tmpRef);
  array_free(tmpRef1);
  array_free(tmpModel);
  return tmpRef;
}


array_t *PureSat_RefineOnAbs_DA(Ntk_Network_t *network,
                             PureSat_Manager_t *pm,
                             bAigEdge_t property,
                             array_t *previousResultArray,
                             int latchThreshHold,
                             int * sccArray,
                             array_t * sufArray)
{
  array_t * tmpRef,*tmpRef1,*tmpRef2,*tmpRef3; //= array_alloc(char *,0);
  array_t * tmpModel = array_alloc(char *,0),*tmpArray1,*tmpArray2;
  satManager_t *cm;
  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
  st_table *table;
  char * name;
  int i;
  int NumInSecondLevel;
  st_generator *stgen;
  Ntk_Node_t *latch;
  double t1,t2,t3,t4;
  st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
  int noArosat = 1;


  tmpRef = array_alloc(char *,0);
  st_foreach_item(pm->SufAbsTable,stgen,&latch,NIL(char*)){
    name = Ntk_NodeReadName(latch);
    if(st_lookup(pm->vertexTable,name,NIL(char *)))
      array_insert_last(char *,tmpModel,name);
    array_insert_last(char *,tmpRef,name);
    st_insert(SufAbsNameTable,name,(char *)0);

  }

  t1 = util_cpu_ctime();
  manager->assertArray = sat_ArrayAlloc(1);
  sat_ArrayInsert(manager->assertArray,manager->InitState);
  cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
#if AROSAT
  cm->option->decisionHeuristic &= RESET_LC;
  cm->option->decisionHeuristic |= DVH_DECISION;
  cm->option->arosat = 1;
#endif
  cm->option->coreGeneration = 1;
  cm->option->AbRf = 1;

  cm->option->IP = 1;
  cm->property = property;
  PureSat_CleanMask(manager,ResetVisibleVarMask);
  PuresatMarkVisibleVarWithVPGV(network,tmpRef,pm,0,pm->Length+1);
  array_free(tmpRef);
  t3 = util_cpu_ctime();
  PureSatPreprocess(network,cm,pm,SufAbsNameTable,pm->Length);
  t4 = util_cpu_ctime();
  pm->tPro += t4-t3;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"process time:%g,total:%g\n",
           (double)((t4-t3)/1000.0),pm->tPro/1000);
#if DBG
  PureSatCheckCoi(manager);
#endif
  if(cm->option->arosat){
    PureSatCreateLayer(network,pm,cm,tmpModel,sufArray);
    cm->Length = pm->Length;
    AS_Main(cm);
    noArosat = 0;
    st_foreach_item(cm->layerTable,stgen,&table,NIL(char*))
      st_free_table(table);
    st_free_table(cm->layerTable);
    FREE(cm->assignedArray);
    FREE(cm->numArray);
  }
  else
    sat_Main(cm);
  manager->NodesArray = cm->nodesArray;;
  assert(cm->status==SAT_UNSAT);
  t3 = util_cpu_ctime();
  PureSatPostprocess(manager,cm,pm);
  PureSatProcessDummy(manager,cm,cm->rm->root);
  ResetRTree(cm->rm);
  t4 = util_cpu_ctime();
  pm->tPro += t4-t3;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"process time:%g,total:%g\n",
           (double)((t4-t3)/1000.0),pm->tPro/1000);
  t2 = util_cpu_ctime();
  pm->tCoreGen += t2 - t1;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"time for UNsat core generation:%g,total:%g\n",
           (double)(t2-t1)/1000.0,pm->tCoreGen/1000.0);
#if DBG
  PureSat_CheckFanoutFanin(manager);
#endif
  t1 = util_cpu_ctime();
  tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable);
  t2 = util_cpu_ctime();

  st_free_table(SufAbsNameTable);
  RT_Free(cm->rm);
  sat_ArrayFree(manager->assertArray);
  PureSat_SatFreeManager(cm);

  /*Get suff set*/

  tmpRef2 = array_alloc(char *,0);
  tmpRef3 = array_alloc(char *,0);
  tmpArray1 = array_alloc(char *,0);
  tmpArray2 = array_alloc(char *,0);

  if(noArosat){
    t1 = util_cpu_ctime();
    if(array_n(tmpRef1)){
     tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1,
                                        &NumInSecondLevel);

      array_free(pm->latchArray);
    }
  }
  /*if arosat*/
  else{
    if(array_n(tmpRef1)){
      tmpRef = PureSatGenerateRCArray_2(network,pm,tmpRef1,
                                        &NumInSecondLevel);
      array_free(pm->latchArray);
    }
    else
      tmpRef = array_alloc(char*,0);

    if(pm->verbosity>=1){
      fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n");
      arrayForEachItem(char *,tmpRef,i,name)
        fprintf(vis_stdout,"%s\n",name);
    }
    PureSatAddIdenLatchToAbs(network,pm,tmpRef);
    array_free(tmpRef1);
    array_free(tmpModel);
    return tmpRef;
  }
}