src/puresat/puresatFlatIP.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 PureSatCheckInv_FlatIP(Ntk_Network_t * network,
                               Ctlsp_Formula_t *ltlFormula,
                               PureSat_Manager_t *pm)
{
  int NumofCurrentLatch=0,k;
  bAig_Manager_t    *manager;
  bAigEdge_t        property;
  st_table * nodeToMvfAigTable;
  double t1,t2,t0;
  int first;
  array_t           *previousResultArray;
  BmcOption_t  *options = BmcOptionAlloc();
  IP_Manager_t * ipm = IPManagerAlloc();
  boolean firstTime;
  int round=0, oldLength=0, nodes_in_coi=0;
  st_table * tmpTable;
  int oldPos1;
  satManager_t * cm;
  bAigEdge_t state, tmpState;
  double tIP=0,tCon=0,tUnsat=0;
  RTManager_t *rm;


  pm->CoiTable = st_init_table(st_ptrcmp,st_ptrhash);
  PureSatBmcGetCoiForLtlFormula(network, ltlFormula,pm->CoiTable);
  ipm->CoiTable = pm->CoiTable;

  options->printInputs = pm->printInputs;
  options->dbgOut = pm->dbgOut;
  pm->CoiTable = st_init_table(st_ptrcmp,st_ptrhash);
  t0 = util_cpu_ctime();
  NumofCurrentLatch=0;
  t1 = util_cpu_ctime();
  PureSatBmcGetCoiForLtlFormula_New(network, ltlFormula,pm->CoiTable);
  t2 = util_cpu_ctime();

  manager = Ntk_NetworkReadMAigManager(network);
  if (manager == 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);

 previousResultArray    = array_alloc(bAigEdge_t, 0);
 first = 0;
 manager->ipm = ipm;
 t1 = util_cpu_ctime();
 manager->test2LevelMini = 1;
 bAig_PureSat_InitTimeFrame(network,manager,pm,0);
 manager->test2LevelMini = 0;
 if(pm->verbosity>=1) {
   fprintf(vis_stdout,"after Init timeframe:\n");
   PureSat_PrintAigStatus(manager);
 }
 manager->class_ = 1;
 manager->test2LevelMini = 0;
 property = PureSatCreatebAigOfPropFormula(network,
            manager, 0, ltlFormula, BMC_NO_INITIAL_STATES);
 property = bAig_Not(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);
 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){
   if(pm->dbgLevel == 1){
     fprintf(vis_stdout,"find counter example of length 0\n");
     BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
                                0, 0,options, BMC_NO_INITIAL_STATES);
   }
   if(pm->dbgLevel == 2){
     BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, pm->CoiTable,
                                0, 0,options, BMC_NO_INITIAL_STATES);
   }
   return FALSE;
 }
 cm->option->coreGeneration = 1;
 PureSat_SatFreeManager(cm);

 manager->test2LevelMini = 1;
 bAig_PureSat_ExpandTimeFrame(network, manager,pm,1, BMC_NO_INITIAL_STATES);
  manager->class_ = 2;
 manager->test2LevelMini = 0;
 property = PureSatCreatebAigOfPropFormula(network,
                manager, 1, 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,"after Init timeframe:\n");
   PureSat_PrintAigStatus(manager);
 }
 state = manager->InitState;


 cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
 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){
   if(pm->dbgLevel == 1){
     fprintf(vis_stdout,"find counter example of length 1\n");
     BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
                        1, 0,options, BMC_NO_INITIAL_STATES);
   }
   if(pm->dbgLevel == 2){
     BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, pm->CoiTable,
                        1, 0,options, BMC_NO_INITIAL_STATES);
   }
   return FALSE;
 }
 cm->option->coreGeneration = 1;
 PureSat_SatFreeManager(cm);

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

 pm->Length = k;
 k = 1;
 PureSat_CleanMask(manager,ResetGlobalVarMask);
 PureSat_MarkGlobalVar(manager,1);
 while(1){
   oldLength = k;
   if(k==1)
     k++;
   else
     k += round-1;
   pm->Length = k;
   if(pm->verbosity>=1)
     fprintf(vis_stdout,"\nk = %d InitState = %ld\n",k,manager->InitState);
   manager->test2LevelMini = 1;
   bAig_PureSat_ExpandTimeFrame(network, manager,pm, k, BMC_NO_INITIAL_STATES);
   manager->test2LevelMini = 0;
   if(pm->verbosity>=1) {
     fprintf(vis_stdout,"After expand TF\n");
     PureSat_PrintAigStatus(manager);
   }

   /*build property aig nodes*/
   manager->class_ = k+1;
   property = PureSatCreatebAigOfPropFormula(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);

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

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

     if(cm->status == SAT_SAT){
       /*SAT: first time->find bug, otherwise increase length*/
       if(firstTime){
         if(pm->dbgLevel == 1){
           fprintf(vis_stdout,"found CEX of length %d\n",k);
           BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
                      k, 0,options, BMC_NO_INITIAL_STATES);
         }
         if(pm->dbgLevel == 2){
           BmcCirCUsPrintCounterExampleAiger(network, nodeToMvfAigTable, pm->CoiTable,
                      k, 0,options, BMC_NO_INITIAL_STATES);
         }
         sat_ArrayFree(manager->assertArray);
         manager->assertArray = 0;
         RT_Free(cm->rm);
         PureSat_SatFreeManager(cm);
         return FALSE;
       }
       /*find bogus bug, abort, increase length*/
       else{
         /* BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
                                      k, 0,options, BMC_NO_INITIAL_STATES);*/
         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
         IP generation*/
       assert(cm->currentDecision>=-1);
       if(cm->currentDecision!=-1)
         sat_Backtrack(cm, -1);
       /*get rid of Conflict Clauses*/
       PureSat_ResetManager(manager,cm,0);

       /*Generate interpolant and test convergence*/
       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);
         ResetRTree(rm);

         /*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();
         tIP = tIP+t2-t1;
         if(pm->verbosity>=2)
           fprintf(vis_stdout,"time for generating IP:%g, Total:%g\n",
                  (double)((t2-t1)/1000.0),tIP/1000);
         if(pm->verbosity>=1){
           fprintf(vis_stdout,"After generate IP,%ld:\n",manager->IPState);
           PureSat_PrintAigStatus(manager);
         }
         manager->class_ = 2;
         t1 = util_cpu_ctime();
         RT_Free(cm->rm);
         if(pm->verbosity>=1)
           PureSat_PrintAigStatus(manager);

         PureSat_ResetManager(manager,cm,0);
       }

       t1 = util_cpu_ctime();

       /*Convergence test for interpolation*/
       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);
         return TRUE;
       }
       else{
         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);
         }
         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){*/
 }/*outer While(1){*/
 st_free_table(tmpTable);

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