src/puresat/puresatMain.c

Go to the documentation of this file.

#include "puresatInt.h"


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

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

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

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

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

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

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

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


void
PureSat_CheckInvariant(
  Ntk_Network_t *network,
  array_t *InvariantFormulaArray,
  int verbosity,
  int dbgLevel,
  FILE *dbgOut,
  boolean printInputs,
  boolean incremental,
  boolean sss,
  boolean flatIP,
  int speed)
{
  int result,i;
  Ctlp_Formula_t  *invFormula;
  Ctlsp_Formula_t *invFormula_sp;
  PureSat_Manager_t * pm = PureSatManagerAlloc();

  pm->incre = incremental;
  pm->verbosity = verbosity;
  pm->dbgLevel = dbgLevel;
  pm->sss = sss;
  pm->printInputs = printInputs;
  pm->dbgOut = dbgOut;

  switch(speed){
  case 0:
    break;
  case 1:
    pm->Switch = 0;
    break;
  case 2:
    pm->Switch = 0;
    pm->CoreRefMin = 0;
    break;
  case 3:
    pm->Switch = 0;
    pm->CoreRefMin = 0;
    pm->RefPredict = 0;
    break;
  case 4:
    pm->Switch = 0;
    pm->CoreRefMin = 0;
    pm->RefPredict = 0;
    pm->Arosat = 0;
    break;
  default:
    pm->Switch = 0;
    pm->CoreRefMin = 0;
    pm->RefPredict = 0;
    pm->Arosat = 0;
    break;
  }
    
  arrayForEachItem(Ctlp_Formula_t *, InvariantFormulaArray, i, invFormula) {
    /* if(Ctlsp_isCtlFormula(invFormula))*/
    invFormula_sp = Ctlsp_CtlFormulaToCtlsp(invFormula);
    if(sss)
      /*SSS-base Puresat algorithm*/
      result = PureSatCheckInv_SSS(network,invFormula_sp,pm);
    else
      if(flatIP)
        /*Interpolation algorithm without abstraction refinement*/
        result = PureSatCheckInv_FlatIP(network,invFormula_sp,pm);
      else
        /*Interpolation-based Puresat algorithm*/
        result = PureSatCheckInv_IP(network,invFormula_sp,pm);
    if(result){
        (void) fprintf(vis_stdout, "# INV: formula passed --- ");
        Ctlsp_FormulaPrint(vis_stdout, (invFormula_sp));
        fprintf(vis_stdout, "\n");
    }
    else{
      if(pm->dbgLevel != 2)
      {
        (void) fprintf(vis_stdout, "# INV: formula failed --- ");
        Ctlsp_FormulaPrint(vis_stdout, (invFormula_sp));
        fprintf(vis_stdout, "\n");
      }
    }
  }
  PureSatManagerFree(pm);
}



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

boolean PureSatCheckInv_SSS(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=0,latchThreshHold=10000,RingPosition=0;
  int oldLength=0, beginPosition=0;
  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,* ConClsArray;
  array_t * arrayRC = NULL;
  array_t *tmpRefinement;
  array_t *tmpRefinement1;
  char * nodeName;
  Ntk_Node_t * node, *latch;
  boolean ExistSimplePath = TRUE,ExistACE = FALSE;
  boolean realRefine=TRUE;
  boolean needSorting = FALSE, firstTime = TRUE;
  mAig_Manager_t    *maigManager;
  BmcOption_t * options;
  BmcCnfStates_t    *cnfstate;
  bAigEdge_t        property;
  st_table * nodeToMvfAigTable;
  double t1,t2, t0,t3;
  long *space;
  PureSat_IncreSATManager_t * pism1,*pism2;
  satArray_t *saved;

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

  options = BmcOptionAlloc();
  options->satInFile = BmcCreateTmpFile();
  options->satOutFile = BmcCreateTmpFile();
  NumofCurrentLatch=0;
  t1 = util_cpu_ctime();
  PureSatBmcGetCoiForLtlFormula(network, ltlFormula,pm->CoiTable);
  PureSatGenerateSupportTable(network,pm);
  t2 = util_cpu_ctime();
  if(pm->verbosity>=2)
    fprintf(vis_stdout,"Generate DFS: %g\n",(double)((t2-t1)/1000.0));
  
  pm->vertexTable = (st_table *)PureSatCreateInitialAbstraction(network,ltlFormula,&NumofCurrentLatch,pm);
 
  pm->AbsTable = st_init_table(st_ptrcmp,st_ptrhash);
  
  Ntk_NetworkForEachLatch(network, gen, node){
    if (st_lookup_int(pm->CoiTable, 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);
    }
   }
  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);
   
  maigManager = Ntk_NetworkReadMAigManager(network);
  if (maigManager == NIL(mAig_Manager_t)) {
    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
    BmcOptionFree(options);
    return 1;
  }
 nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
                                                         MVFAIG_NETWORK_APPL_KEY);
  
 /*build property clauses*/
 if (Ctlsp_isPropositionalFormula(ltlFormula))
   property = BmcCreateMaigOfPropFormula(network, maigManager, ltlFormula);
 else
   property = BmcCreateMaigOfPropFormula(network, maigManager, ltlFormula->left);
 
 if (property == mAig_NULL){
   fprintf(vis_stderr,"property = NULL\n");
   exit(0);
 }
 
 property = bAig_Not(property);
 
 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));
     //tmpRefinement1 = array_alloc(char *,0);
     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);
         }
       array_append(visibleArray,refinement);
       latchThreshHold=(int)((double)(array_n(CoiArray)-array_n(visibleArray))/(double)4)+1;
       
       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_int(pm->CoiTable,stGen,&latch,&i)
         {
           nodeName = Ntk_NodeReadName(latch);
           if(!st_lookup(pm->vertexTable,nodeName,0))
             array_insert_last(char *,invisibleArray,nodeName);
         }
       t1 = util_cpu_ctime();
       PureSatGetCoiForVisibleArray_Ring(network, visibleArray,RingPosition, pm->CoiTable);
       RingPosition = array_n(visibleArray);
       arrayRC = PureSatGenerateRingFromAbs(network,pm,invisibleArray,&NumInSecondLevel);
       if(pm->verbosity>=2){
         fprintf(vis_stdout,"NumInSecondLevel is %d  ",NumInSecondLevel);
         fprintf(vis_stdout,"latchThreshHold is %d\n",latchThreshHold);
       }
       latchThreshHold = (latchThreshHold <= 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,"Generate Ring: %g\n",(double)((t2-t1)/1000.0));
       }
       array_free(refinement);
     }/* if(realRefine)*/
     
     realRefine =FALSE; /* means no ref, just Length++.*/
     t1 = util_cpu_ctime();
     if((ExistSimplePath =
        PureSatExistASimplePath(network,pism1,visibleArray,property,pm)))
       {
         t2 = util_cpu_ctime();
         if(pm->verbosity>=2)
           fprintf(vis_stdout,"Solve on Simple Path: %g\n",(double)((t2-t1)/1000.0));
         pism1->oldLength = pm->Length;
         pism1->Length = pm->Length;
         pism1->beginPosition = array_n(visibleArray);
         if(pm->verbosity>=1)
           fprintf(vis_stdout, "Simple Path Exists, length = %d\n",pm->Length);
         
         /*check Abs Model*/
         t1 = util_cpu_ctime();
         ExistACE = PureSatIncreExistCE(network,pism2,visibleArray,property,pm);
         if(pm->verbosity>=2)
           fprintf(vis_stdout,"beginPosition2: %d, oldLength2 %d\n",pism2->beginPosition, pism2->oldLength);
         t2 = util_cpu_ctime();
         if(pm->verbosity>=2)
           fprintf(vis_stdout,"Solve on Abs model: %g\n",(double)((t2-t1)/1000.0));
         pism2->oldLength = pm->Length;
         pism2->Length = pm->Length;
         pism2->beginPosition = array_n(visibleArray);
         needSorting = FALSE;
         
         /*keep a record of previous position for refine's use*/
         oldLength = pism2->oldLength;
         beginPosition = pism2->beginPosition;
         
         /* while(ExistACE)
             loop until find sufficient set*/
         if(ExistACE)
           {
             if(pm->verbosity>=1)
               fprintf(vis_stdout,"found Abstract Counterexample at length %d\n", pm->Length);
             cnfstate = BmcCnfClausesFreeze(pism2->cnfClauses);
             pism2->propertyPos = cnfstate->nextIndex;
             
             /*store the conflict clauses*/
             ConClsArray = array_alloc(int,0);
             
             /*if incremental */
             if(pm->incre){
               if(pism2->cm->savedConflictClauses){
                 saved = pism2->cm->savedConflictClauses;
                 for(i=0, space=saved->space; i<saved->num; i++, space++){
                   array_insert_last(int,ConClsArray,*space);
                 }
               }
             }
             realRefine = TRUE;
             
             /*incrementally check Concrete Model*/
             tmpRefinement = array_alloc(char *,0);
             if(pm->verbosity>=2)
               fprintf(vis_stdout,"Begin building a new abstract model\n");
             for(i=0;i<array_n(arrayRC);i=i+latchThreshHold)
               {
                 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)
                           fprintf(vis_stdout, "picking %s\n",nodeName);
                       }
                     else
                       break;
                   }/* for(j=0;*/
                 tmpRefinement1=array_dup(visibleArray);
                 array_append(tmpRefinement1,tmpRefinement);
                 
                 t1 = util_cpu_ctime();
                 pism2->cm->option->incAll = 1;
                 pism2->cm->option->incTraceObjective = 0;
                 pism2->cm->option->incPreserveNonobjective = 0;
                 if(PureSatIncreExistCEForRefineOnAbs(network,pism2,tmpRefinement1,property,firstTime,pm)) {
                   t2 = util_cpu_ctime();
                   if(pm->verbosity>=2)
                     fprintf(vis_stdout,"time for finding a sufficient set on model: %g\n",(double)((t2-t1)/1000.0));
                   if((i+j)>=array_n(arrayRC)){
                     if(pm->verbosity>=1)
                       fprintf(vis_stdout,"found real counterexamples\n");
                     if(pm->dbgLevel>=1){
                       options->printInputs = TRUE;
                       BmcPrintCounterExample(network, nodeToMvfAigTable, pism2->cnfClauses,
                                              pm->result, pm->Length, pm->CoiTable, options, 
                                              NIL(array_t));
                       array_free(pm->result);
                       pm->result = NIL(array_t);
                     }
                     array_free(tmpRefinement1);
                     array_free(tmpRefinement);
                     BmcOptionFree(options);
                     PureSatIncreSATManagerFree(pm,pism1);
                     PureSatIncreSATManagerFree(pm,pism2);
                     /*PureSatManagerFree(pm);*/
                     array_free(CoiArray);
                     array_free(visibleArray);
                     return FALSE;
                   }
                   else{
                     if(pm->result!=NIL(array_t)){
                       array_free(pm->result);
                       pm->result = NIL(array_t);
                     }
                   }
                 }
                 else{
                   t2 = util_cpu_ctime();
                   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\n",(double)((t2-t1)/1000.0));
                   firstTime = FALSE;
                   arrayForEachItem(char *,tmpRefinement1,k,nodeName){
                     node = Ntk_NetworkFindNodeByName(network, nodeName);
                     if(!st_lookup(pm->SufAbsTable,node,NIL(char *)))
                       st_insert(pm->SufAbsTable,node, (char *)0);
                     else{
                       fprintf(vis_stderr,"wrong in sufabstable \n");
                       exit(0);
                     }
                   }
                   pism2->beginPosition = array_n(tmpRefinement1);
                   pism2->oldLength = Length;
                   array_free(tmpRefinement1);
                   break;
                 }
                 pism2->beginPosition = array_n(tmpRefinement1);
                 array_free(tmpRefinement1);
                 pism2->oldLength = Length;
               } /*for(i=0;i<array_n(arrayRC)*/
             
             /*recover the conflict clauses and incremental SAT option*/
             pism2->cm->option->incAll = 0;
             pism2->cm->option->incTraceObjective = 1;
             pism2->cm->option->incPreserveNonobjective = 1;
             
             /*if incremental*/
             if(pm->incre){
               if(pism2->cm->savedConflictClauses)
                 sat_ArrayFree(pism2->cm->savedConflictClauses);
               pism2->cm->savedConflictClauses = sat_ArrayAlloc(16);
               arrayForEachItem(int, ConClsArray,i,tmp)
                 sat_ArrayInsert(pism2->cm->savedConflictClauses,tmp);
             }
             array_free(tmpRefinement);
             t1 = util_cpu_ctime();
             refinement = PureSatRefineOnAbs(network,pm,property,addtoAbs);
             t2 = util_cpu_ctime();
             if(pm->verbosity>=2)
               fprintf(vis_stdout,"time for RefOnAbs: %g\n",(double)((t2-t1)/1000.0));
             st_free_table(pm->SufAbsTable);
             pm->SufAbsTable = NIL(st_table);
             
             /*adjust parameters*/
             NumofCurrentLatch+=array_n(refinement);
             pm->Length++;
             pism1->Length++;
             pism2->Length++;
             BmcCnfClausesRestore(pism2->cnfClauses, cnfstate);
             pism2->beginPosition = beginPosition;
             pism2->oldLength = oldLength;
             FREE(cnfstate);
           }/* if(pism2->cm->status == SAT_SAT)*/
         else /*if(pism2->cm->status != SAT_SAT)*/
           {
             if(pm->verbosity>=1)
               fprintf(vis_stdout,"no Abstract Counterexample at length %d \n",pm->Length);
             pm->Length++;
             pism1->Length++;
             pism2->Length++;
             st_free_table(pm->SufAbsTable);
             pm->SufAbsTable = NIL(st_table);
           }
       } /*if(ExistSimplePath)*/
     else /* if no simple path*/
       {
         t2 = util_cpu_ctime();
         if(pm->verbosity>=2)
           fprintf(vis_stdout,"Solve on Simple Path: %g\n",(double)((t2-t1)/1000.0));
         if(pm->verbosity>=1)
           fprintf(vis_stdout,"simple Path doesn't exist, exit\n");
         BmcOptionFree(options);
         PureSatIncreSATManagerFree(pm,pism1);
         PureSatIncreSATManagerFree(pm,pism2);
         PureSatManagerFree(pm);
         array_free(CoiArray);
         array_free(visibleArray);
         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);
 while(PureSatExistASimplePath(network,pism1,visibleArray,property,pm))
   {
     pism1->oldLength = pism1->Length;
     pism1->beginPosition = array_n(visibleArray);
     if(PureSatExistCE(network,pism2,options,visibleArray,property,pm,1)) {
       if(pm->verbosity>=1)
         fprintf(vis_stdout,"found real counterexample of length:%d\n",pm->Length);
       if(pm->dbgLevel>=1){
         options->printInputs = TRUE;
         BmcPrintCounterExample(network, nodeToMvfAigTable, pism2->cnfClauses,
                                pm->result, pm->Length, pm->CoiTable, options, 
                                NIL(array_t));
       }
       BmcOptionFree(options);
       PureSatIncreSATManagerFree(pm,pism1);
       PureSatIncreSATManagerFree(pm,pism2);
       /*PureSatManagerFree(pm);*/
       array_free(CoiArray);
       array_free(visibleArray);
       return FALSE;
     }
     else
       {
         pism2->oldLength = Length;
         pm->Length++;
         pism1->Length++;
         pism2->Length++;
         pism2->beginPosition = array_n(visibleArray);
       }
   }
 
 BmcOptionFree(options);
 PureSatIncreSATManagerFree(pm,pism1);
 PureSatIncreSATManagerFree(pm,pism2);  
 /*PureSatManagerFree(pm);*/
 array_free(CoiArray);
 array_free(visibleArray);
 return TRUE;
}

void PureSatCmdParse(int argc,
                     char **argv,
                     PureSat_Manager_t *pm)

{
  int c, incre;
  
  util_getopt_reset();
  while ((c = util_getopt(argc, argv, "t:i:h:v:I:")) != EOF) {
    switch(c) {
      case 'i':
        strcpy(pm->ltlFileName,util_strsav(util_optarg));
        break;  
      case 't' :
        pm->timeOutPeriod = atoi(util_optarg);
        break;  
      case 'v':
        pm->verbosity = atoi(util_optarg);
        break;
      case 'I':
        incre = atoi(util_optarg);
        pm->incre = (incre==0)? FALSE:TRUE;
        break;
      case 'h':
        goto usage;
      default:
        goto usage;
    }
  }
  return;
 usage:
  (void) fprintf(vis_stderr, "usage: abrf [-h][-i ltlfile][-t timeout]\n");
  (void) fprintf(vis_stderr, "   -i \tName of LTL file.\n");
  (void) fprintf(vis_stderr, "   -t \ttimeout.\n");
  (void) fprintf(vis_stderr, "   -v \tverbosity for more information. \n");
  (void) fprintf(vis_stderr, "   -I \tincremental SAT switch. \n");
  (void) fprintf(vis_stderr, "\t\t0 for non-incremental, other values for incremental\n");
  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");

}

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