src/puresat/puresatRefine.c

Go to the documentation of this file.

#include "puresatInt.h"

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

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

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

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

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

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


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


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

array_t * PureSatRefineOnAbs(Ntk_Network_t *network,
                      PureSat_Manager_t *pm,
                      bAigEdge_t  property,
                      int latchThreshHold)
{
  mAig_Manager_t    *maigManager       = Ntk_NetworkReadMAigManager(network);
  lsGen             gen;
  Ntk_Node_t        *latch;
  FILE              *fp, *fp1;
  BmcOption_t       *options,*option2;
  int        i,j,k,Length,beginPosition=0;
  int        NumInSecondLevel=0;
  array_t    * tmpRefinement,*tmpArray1,*tmpArray2;
  array_t    *tmpModel,*tmpRefinement1;
  /*st_table   * RefinementTable, *CandidateTable;*/
  array_t    *Pclause, *tmpRefinement2, *tmpRefinement3, *oriSufArray;
  char       buffer[1024],str[100];
  char       *name, *coreFile, *tmpCoreFile, *coreFile1=(char *)0;
  int         oldLength=0,oriCoreSize, CoreSize,weight;
  st_table          *nodeToMvfAigTable;
  BmcCnfStates_t    *cnfstate;
  int             oldNumOfLatchInCore;
  int             newNumOfLatchInCore,NumOfLatchInModel,round;
  boolean     VarInCoreIsEnough = FALSE, LatchFromCore = FALSE;
  boolean     firstTime = TRUE;
  long t1,t2,t3,t4;
  st_table * localSufAbsTable;
  PureSat_IncreSATManager_t * pism = PureSatIncreSATManagerAlloc(pm);
  satManager_t * cm = pism->cm;
  BmcCnfClauses_t   * cnfClauses = pism->cnfClauses;
  st_table *vertexTable = pm->vertexTable;
  st_table *SufAbsTable = pm->SufAbsTable;
  /*st_table *CoiTable = pm->CoiTable;*/
  /*st_table *supportTable = pm->supportTable;*/
  /* st_table *AbsTable = pm->AbsTable;*/
    
  t1 = util_cpu_ctime();

  cm->option->clauseDeletionHeuristic = 0;
  cm->option->incTraceObjective = 0;
  pism->Length = pm->Length;
  Length =  pm->Length;
  coreFile = BmcCreateTmpFile();
  tmpCoreFile = BmcCreateTmpFile();
  strcpy(str,"coreFile: ");
  strcat(str,coreFile);
  strcat(str,", tmpCoreFile: ");
  strcat(str,tmpCoreFile);
  strcat(str,"\n");
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"%s",str);
  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\n");
    exit (0);
  }
  
  option2 = BmcOptionAlloc();
  option2->satInFile = BmcCreateTmpFile();
  option2->satOutFile = BmcCreateTmpFile();
  options = BmcOptionAlloc();
  options->satInFile = BmcCreateTmpFile();
  options->satOutFile = BmcCreateTmpFile();

  newNumOfLatchInCore = 0;
  NumOfLatchInModel = 0;
  tmpModel = array_alloc(char *,0);
  oriSufArray = array_alloc(char *,0);
  Ntk_NetworkForEachLatch(network, gen, latch){
    name = Ntk_NodeReadName(latch);
    if(st_lookup(vertexTable,name,NIL(char *))){
      array_insert_last(char *,tmpModel,name);
      NumOfLatchInModel++;
    }
    else
      if(st_lookup(SufAbsTable,latch,NIL(char *))){
        newNumOfLatchInCore++;
        array_insert_last(char *,oriSufArray,name);
      }
  }
  
  localSufAbsTable = st_copy(SufAbsTable);
  //tmpRefinement2 = array_alloc(char *,0);
  tmpRefinement3 = array_alloc(char *,0);
  //tmpArray1 = array_alloc(char *,0);
  //tmpArray2 = array_alloc(char *,0);
  weight = (NumOfLatchInModel+newNumOfLatchInCore+1)*10000;
  round=0;
  
  round++;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"round: %d\n",round);
  oldNumOfLatchInCore = newNumOfLatchInCore;
  pm->ClsidxToLatchTable = st_init_table(st_numcmp,st_numhash);
  PureSatGenerateClausesForPath_EnhanceInit(network,0,Length,pism,pm,nodeToMvfAigTable,localSufAbsTable);
  Pclause = array_alloc(int,0);
  array_insert_last(int, Pclause, BmcGenerateCnfFormulaForAigFunction(maigManager,property,
                                                                      Length, cnfClauses));
  BmcCnfInsertClause(cnfClauses, Pclause);
  array_free(Pclause);
  CoreSize=cnfClauses->noOfClauses;
  
  oriCoreSize = CoreSize;
  cm->option->coreGeneration = 1;
  cm->fp = fopen(tmpCoreFile, "w");
  if(pm->verbosity>=2)
    PureSatWriteClausesToFile(pism,maigManager,coreFile1);
  t1 = util_cpu_ctime();
  PureSatReadClauses(pism,pm);
  sat_Main(cm);
  t2 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"time for SAT Solver(satMain): %g\n",(double)((t2-t1)/1000.0));
  
  fclose(cm->fp);
  if(cm->status == SAT_SAT){
    fprintf(vis_stderr,"This instance is supposed to be UNSAT, wrong and exit\n");
    exit(0);
  }
  cm->stdOut = vis_stdout; 
  cm->option->coreGeneration = 0;
  
  t2 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"time for satMain: %g\n",(double)((t2-t1)/1000.0));
  CoreSize = cm->numOfClsInCore;
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"CoreSize:%d/OriCoreSize:%d\n", CoreSize,oriCoreSize);
  
  fp1 = fopen(coreFile, "w");
  fp = fopen(tmpCoreFile, "r");
  sprintf(buffer,"p cnf %d %d 0\n", cm->initNumVariables, cm->numOfClsInCore);
  fputs(buffer, fp1);
  while(fgets(buffer,1024,fp)){
    fputs(buffer, fp1);
  }
  fclose(fp);
  fclose(fp1);

  //tmpRefinement1 = array_alloc(char *,0);
  /* generate sufficient refinement */
  st_free_table(localSufAbsTable);
  localSufAbsTable = st_init_table(st_ptrcmp,st_ptrhash);  
  t3 = util_cpu_ctime();
  tmpRefinement1 = PureSatGetLatchFromTable(network,pm,coreFile);
  t4 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"time for PureSatGetLatchFromTable: %g\n",(double)((t4-t3)/1000.0));
  
  if(array_n(tmpRefinement1)>array_n(oriSufArray)){
    array_free(tmpRefinement1);
    tmpRefinement1 = array_dup(oriSufArray);
  }
  else{
    array_free(oriSufArray);
    oriSufArray = array_dup(tmpRefinement1);
  }
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"All latches picked from UNSAT Proof:\n");
  arrayForEachItem(char *,tmpRefinement1,i,name){
    if(pm->verbosity>=2)
      fprintf(vis_stdout," %s  ",name);
    latch = Ntk_NetworkFindNodeByName(network,name);
    st_insert(localSufAbsTable,latch,(char *)0);
  }
  if(pm->verbosity>=2){
    fprintf(vis_stdout,"\n");
    fprintf(vis_stdout,"tmpModel: \n");
  }
  arrayForEachItem(char *,tmpModel,i,name){
    if(pm->verbosity>=2)
      fprintf(vis_stdout," %s  ",name);
    latch = Ntk_NetworkFindNodeByName(network,name);
    st_insert(localSufAbsTable,latch,(char *)0);
  }
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"\n");
  newNumOfLatchInCore = array_n(tmpRefinement1);
  BmcCnfClausesFree(pism->cnfClauses);
  
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"newNumOfLatchInCore/oldNumOfLatchInCore=%f\n",(double)newNumOfLatchInCore/(double)oldNumOfLatchInCore);
  
  /* Add the refinement to vertexTable*/
  arrayForEachItem(char *,tmpRefinement1,i,name){
    st_insert(vertexTable, name,(char*)0);
  }
  
  pism->cnfClauses = BmcCnfClausesAlloc();
  cnfClauses = pism->cnfClauses;
  if(array_n(tmpRefinement1)) 
    {
      tmpRefinement = PureSatGenerateRingFromAbs(network,pm,tmpRefinement1,&NumInSecondLevel);
      /* latchThreshHold = (latchThreshHold <= NumInSecondLevel) ? latchThreshHold:NumInSecondLevel;*/
      array_free(tmpRefinement1);
      LatchFromCore = TRUE;
      for(i=0;i<array_n(tmpRefinement);i=i+latchThreshHold)
        {
          for(j=0;j<latchThreshHold;j++)
            {
              if((i+j)<array_n(tmpRefinement))
                {
                  name = array_fetch(char *,tmpRefinement,i+j);
                  array_insert_last(char *,tmpRefinement3,name);
                  if(pm->verbosity>=1)
                    fprintf(vis_stdout, "picking %s\n",name);
                }
              else
                break;
            }
          tmpRefinement2=array_dup(tmpModel);
          array_append(tmpRefinement2,tmpRefinement3);
          if(!PureSatExistCE(network,pism,option2,tmpRefinement2,property,pm,0)){
            VarInCoreIsEnough = TRUE;
            array_free(tmpRefinement2);
            for(k=i+j;k<array_n(tmpRefinement);k++)
              {
                name = array_fetch(char *,tmpRefinement,k);
                if(st_lookup(vertexTable,name,NIL(char *))){
                  st_delete(vertexTable,&name,NIL(char *));
                }
              }
            break;
          }
          firstTime = FALSE;
          beginPosition = array_n(tmpRefinement2);
          array_free(tmpRefinement2);
          oldLength = Length;
        } 
      array_free(tmpRefinement);
      tmpRefinement = array_dup(tmpRefinement3); /* now tmpRefinement1 contains the
                                                   latches in Core*/
      array_free(tmpRefinement3);
      oldLength=0;
      beginPosition=0;
      BmcCnfClausesFree(pism->cnfClauses);
      pism->cnfClauses = BmcCnfClausesAlloc();
    }
  
#if 1
  if(!VarInCoreIsEnough){
    fprintf(vis_stderr,"this should never happen, wrong\n");
    exit(0);
  }
#endif
  
  //tmpRefinement = array_dup(tmpRefinement1);
  //array_free(tmpRefinement1);
  
# if 1
  /*Refinement Minimization
    try all the candidates*/
  for(i=array_n(tmpRefinement)-1;i>=0;i--)
    {
      name = array_fetch(char *,tmpRefinement,i);
      if(pm->verbosity>=1)
        fprintf(vis_stdout,"RefMin: testing %s\n",name);
      tmpArray2 = PureSatRemove_char(tmpRefinement,i);
      tmpArray1 = array_dup(tmpModel);
      array_append(tmpArray1,tmpArray2);
      cnfstate = BmcCnfClausesFreeze(pism->cnfClauses);
      if(PureSatExistCE(network,pism,option2,tmpArray1,property,pm,0))
        array_free(tmpArray2);
      else /*delete it*/
        {
          /*   i--;*/
          name = array_fetch(char *, tmpRefinement,i);
          if(st_lookup(vertexTable, name,NIL(char *)))
            st_delete(vertexTable, &name, NIL(char *));
          else
            fprintf(vis_stderr," %s should be in vertexTable, Wrong!!!\n",name);
          array_free(tmpRefinement);
          tmpRefinement = tmpArray2;
        }
      array_free(tmpArray1);
      BmcCnfClausesRestore(pism->cnfClauses, cnfstate);
      FREE(cnfstate);
    }
  //BmcCnfClausesFree(pism->cnfClauses);
#endif
  
  if(pm->verbosity>=1){
    fprintf(vis_stdout,"\n sufficient refinement candidates from CA\n");
    arrayForEachItem(char *,tmpRefinement,i,name)
      fprintf(vis_stdout,"%s\n",name);
  }
  BmcOptionFree(option2);
  BmcOptionFree(options);
  unlink(coreFile);
  unlink(tmpCoreFile);
  FREE(coreFile);
  FREE(tmpCoreFile);
  array_free(oriSufArray);
  st_free_table(pm->ClsidxToLatchTable);
  pm->ClsidxToLatchTable = NIL(st_table);
  PureSatIncreSATManagerFree(pm,pism);
  return tmpRefinement;
}


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/