Changeset 41


Ignore:
Timestamp:
Jan 10, 2012, 6:51:23 PM (12 years ago)
Author:
cecile
Message:

new command generate cnf from network

Location:
vis_dev/vis-2.3
Files:
8 edited

Legend:

Unmodified
Added
Removed

  • vis_dev/vis-2.3/models/debug/and2.ltl

    r39 r41  
    1 X(c = 1);
     1X(c = 0);

  • vis_dev/vis-2.3/models/debug/test.script

    r40 r41  
    1 rlmv and2.mv
     1rlmv new_and.mv
    22init
    33_createAbn
    44aig
    5 _sat_debug  -k 1 -p and2.ltl -o and2_prop.cnf -v 1 
     5_sat_debug  -k 1  -v 1  -o new_and_prop.cnf and2.ltl

  • vis_dev/vis-2.3/src/bmc/bmcInt.h

    r14 r41  
    184184EXTERN Ltl_Automaton_t * BmcAutLtlToAutomaton(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula);
    185185EXTERN void BmcAutTerminationFree(BmcCheckForTermination_t *result);
    186 EXTERN int BmcBddSat(Ntk_Network_t *network, array_t *formulaArray, BmcOption_t *options);
     186EXTERN int BmcBddSat(Ntk_Network_t *network, array_t *formulaArray, BmcOption_t *savons);
    187187EXTERN Bmc_PropertyStatus BmcBddSatCheckLtlFormula(Ntk_Network_t *network, mdd_t *initialStates, mdd_t *targetStates, BmcOption_t *options, st_table *CoiTable);
    188188EXTERN void BmcLtlVerifyProp(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, st_table *CoiTable, BmcOption_t *options);

  • vis_dev/vis-2.3/src/debug/debug.c

    r40 r41  
    6565static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
    6666static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
     67static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
    6768
    6869
    … …  
    9495  Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
    9596  Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
     97  Cmd_CommandAdd("print_network_cnf",  CommandGenerateNetworkCNF, 0);
    9698
    9799}
    … …  
    176178
    177179******************************************************************************/
    178 static int
    179 checkIndex(
    180   int             index,
    181   BmcCnfClauses_t *cnfClauses)
    182 {
    183   int     rtnValue = -1; /* it is not TRUE or FALSE*/
    184 
    185   if (index == 0){ /* TRUE or FALSE*/
    186     if (cnfClauses->emptyClause){   /* last added clause was empty = FALSE*/
    187       rtnValue = 0; /* FALSE */
    188     } else {
    189       /*
    190         if (cnfClauses->noOfClauses == 0)
    191         rtnValue = 1;
    192         }
    193       */
    194       rtnValue = 1; /* TRUE */
    195     }
    196   }
    197   return rtnValue;
    198 }
    199 
    200 
    201180static int
    202181CommandSatDebug(
    … …  
    206185int            c,i;
    207186int            verbose = 0;              /* default value */
    208 BmcOption_t  *options = BmcOptionAlloc();
    209 Ntk_Network_t * network;
    210 bAig_Manager_t    *manager;
    211 array_t           *formulaArray;
    212 array_t           *LTLformulaArray;
    213 char *ltlFileName     = NIL(char);
     187BmcOption_t      * options = BmcOptionAlloc();
     188Ntk_Network_t    * network;
     189bAig_Manager_t   * manager;
     190array_t          * formulaArray;
     191array_t          * LTLformulaArray;
     192char             * ltlFileName     = NIL(char);
     193
    214194
    215195/*
    216196 * Parse command line options.
    217197 */
    218 util_getopt_reset();
    219 while ((c = util_getopt(argc, argv, "vhp:m:k:o:")) != EOF) {
    220   switch(c) {
    221     case 'v':
    222       verbose = 1;
    223           options->verbosityLevel =  verbose;
    224       break;
    225     case 'h':
    226       goto usage;
    227         case 'm':
    228       for (i = 0; i < strlen(util_optarg); i++) {
    229                 if (!isdigit((int)util_optarg[i])) {
    230                         goto usage;
    231                 }
    232       }
    233       options->minK = atoi(util_optarg);
    234       break;
    235     case 'k':
    236       for (i = 0; i < strlen(util_optarg); i++) {
    237                 if (!isdigit((int)util_optarg[i])) {
    238                         goto usage;
    239                 }
    240       }
    241           options->maxK = atoi(util_optarg);
    242           break;
    243         case 'o':
    244       options->cnfFileName = util_strsav(util_optarg);
    245       break;
    246     case 'p':
    247       ltlFileName     = util_strsav(util_optarg);
    248     break;
    249 
    250     default:
    251       goto usage;
    252   }
    253 }
     198if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
     199     return 1;
     200}
     201
     202
    254203printf("MAX K %d", options->maxK);
    255  if (options->minK > options->maxK){
    256     (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");   
    257     goto usage;
    258   }
    259204
    260205if (verbose) {
    261206  (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
    262207}
    263  /* create SAT Solver input file */
    264  if (options->cnfFileName == NIL(char)) {
    265     options->satInFile = BmcCreateTmpFile();
    266 }
    267  else {
    268     options->satInFile = options->cnfFileName;
    269  }
    270 
    271 /* create SAT Solver output file */
    272 options->satOutFile = BmcCreateTmpFile();
    273 if (options->satOutFile == NIL(char)){
     208/*
     209 *  Read the network
     210 */
     211network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
     212if (network == NIL(Ntk_Network_t)) {
     213  (void) fprintf(vis_stdout, "** _sat_debug error: No network\n");
    274214  BmcOptionFree(options);
    275  (void) fprintf(vis_stdout, "The _sat_debug problem.\n");
    276215  return 1;
    277216}
    278 
    279 options->verbosityLevel =  1;
    280 //options->satSolver
    281 //options->clauses
    282 
    283  /*
    284    * Read the network
    285    */
    286   network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
    287   if (network == NIL(Ntk_Network_t)) {
    288     (void) fprintf(vis_stdout, "** bmc error: No network\n");
    289     BmcOptionFree(options);
    290     return 1;
    291   }
    292   manager = Ntk_NetworkReadMAigManager(network);
    293   if (manager == NIL(mAig_Manager_t)) {
    294     (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
    295     BmcOptionFree(options);
    296     return 1;
    297   }
    298 
    299   /*
    300     We need the bdd when building the transition relation of the automaton
    301   */
    302   if(options->inductiveStep !=0){
    303     Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
    304  
    305     designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
    306     if (designFsm == NIL(Fsm_Fsm_t)) {
    307          (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n");
    308       return 1;
    309     }
    310   }
     217manager = Ntk_NetworkReadMAigManager(network);
     218if (manager == NIL(mAig_Manager_t)) {
     219  (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n");
     220  BmcOptionFree(options);
     221  return 1;
     222}
     223
    311224Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
    312 printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
    313 /*
    314  * Read the formula
    315  */
    316  /* Read LTL Formulae */
    317   if (!ltlFileName)
    318       goto usage;
    319 
    320   options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
    321   if (options->ltlFile == NIL(FILE)) {
    322     (void) fprintf(vis_stdout,"** _sat_debug error: Cannot open the file %s\n", ltlFileName);
    323     FREE(ltlFileName);
    324     BmcOptionFree(options);
    325   }
    326   FREE(ltlFileName);
    327 
    328  formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
    329   if (formulaArray == NIL(array_t)) {
    330     (void) fprintf(vis_stderr,
    331                    "** bmc error: error in parsing CTL* Fromula from file\n");
    332     BmcOptionFree(options);
    333     return 1;
    334   }
    335   if (array_n(formulaArray) == 0) {
    336     (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
    337     BmcOptionFree(options);
    338     Ctlsp_FormulaArrayFree(formulaArray);
    339     return 1;
    340   }
    341   LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
     225if(abn == NIL(Dbg_Abnormal_t)){
     226  (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n");
     227  return 1;
     228}
     229if(verbose)
     230  printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
     231
     232
     233formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
     234if (formulaArray == NIL(array_t)) {
     235  (void) fprintf(vis_stderr,
     236           "** bmc error: error in parsing CTL* Fromula from file\n");
     237  BmcOptionFree(options);
     238  return 1;
     239}
     240if (array_n(formulaArray) == 0) {
     241  (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
     242  BmcOptionFree(options);
    342243  Ctlsp_FormulaArrayFree(formulaArray);
    343   if (LTLformulaArray ==  NIL(array_t)){
    344     (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
    345     BmcOptionFree(options);
    346     return 1;
    347   }
    348     Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
     244  return 1;
     245}
     246LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
     247Ctlsp_FormulaArrayFree(formulaArray);
     248if (LTLformulaArray ==  NIL(array_t)){
     249  (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
     250  BmcOptionFree(options);
     251  return 1;
     252}
     253Ctlsp_Formula_t *ltlFormula  = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
    349254
    350255
    … …  
    353258    Compute the cone of influence
    354259        here : a list of state variables (latches)
     260    TODO refine to COI of the property
    355261  */
    356262        st_table        *CoiTable =  generateAllLatches(network);
    … …  
    359265      clauses in BMC.
    360266    */
    361     st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
    362         BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
    363     FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
    364         /*
    365     nodeToMvfAigTable maps each node to its multi-function And/Inv graph
    366     */
    367         nodeToMvfAigTable =
    368         (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
    369         assert(nodeToMvfAigTable != NIL(st_table));
    370 
    371         if(verbose)
     267        if(verbose)
    372268        {       
    373                 (void) fprintf(vis_stdout, "------ node to mvfaig ----\n");
    374                 printLatch(nodeToMvfAigTable);
    375269                (void) fprintf(vis_stdout, "------      COI       ----\n");
    376270                printLatch(CoiTable);
    377271                (void) fprintf(vis_stdout, "--------------------------\n");
    378272    }
    379     /*
    380       Create a clause database
    381      */
    382     cnfClauses = BmcCnfClausesAlloc();
    383     /*
    384       Generate clauses for an initialized path of length k
    385      */
    386     Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
    387      fprintf(vis_stdout, "\n");
    388     BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
    389                                  cnfClauses, nodeToMvfAigTable, CoiTable);
     273    BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
     274
    390275
    391276    //Generate ltl CNF
    … …  
    393278    // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ...
    394279    // cf. BmcLtlVerifyGeneralLtl
     280    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
     281    fprintf(vis_stdout, "\n");
    395282    int k = options->maxK;
    396283    int l;
    … …  
    398285    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);
    399286   
    400     int leftValue   = checkIndex(noLoopIndex, cnfClauses);
    401     printf("noLoopIndex %d , leftValue %d \n", noLoopIndex,leftValue);
     287
    402288        array_t           *objClause = NIL(array_t);
    403289        objClause = array_alloc(int, 0);   
    … …  
    406292    array_free(objClause);
    407293
    408        
    409 //TODO Add abnormal formula
    410 
    411 
    412 
    413 
     294        //Add Abnormal
     295    st_table * nodeToMvfAigTable =  NIL(st_table);
     296    nodeToMvfAigTable =
     297(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
     298assert(nodeToMvfAigTable != NIL(st_table));
     299
     300    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses);
     301
     302      //loop abnormal
     303    int aIndex;
     304    Ntk_Node_t * abnNode;
     305     Dbg_ForEachAbnormal(abn,aIndex,abnNode){
     306     if(aIndex<=0){
     307     //set abnormal
     308      int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex);
     309      bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
     310      int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],0,cnfClauses);
     311      array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
     312
     313      FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
     314      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
     315      fclose(cnfFile);
     316
     317      //SAT procedure
     318      int res = Dbg_SatCheck("assig",options->cnfFileName);
     319
     320        array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
     321        }
     322     }
    414323
    415324         if(verbose)
    … …  
    417326                latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
    418327       
    419  Ctlsp_FormulaArrayFree(LTLformulaArray);   
    420         BmcWriteClauses(manager, cnfFile, cnfClauses, options);
    421 fclose(cnfFile);
     328Ctlsp_FormulaArrayFree(LTLformulaArray);   
    422329BmcCnfClausesFree(cnfClauses);
    423330BmcOptionFree(options);
    424331return 0;
    425   usage:
    426   (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
    427   minimum length] [-o cnf_file] [-p ltl_file]\n");
    428   (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
    429   (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
    430   (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n"); 
     332 
     333}
     334/**Function********************************************************************
     335
     336  Synopsis    [Implements the generate_network_cnf.]
     337
     338  CommandName [generate_network_cnf]
     339
     340  CommandSynopsis [generate a CNF view of the network]
     341
     342  CommandArguments [\[-h\] \[-v\] \[-k\]  [fileName] ]
     343 
     344  CommandDescription [This command geerate a CNF of the network in DMACS form.
     345  The network may be unroll within k steps.
     346  <p>
     347
     348  Command options:<p> 
     349
     350  <dl>
     351  <dt> -h
     352  <dd> Print the command usage.
     353  </dl>
     354
     355  <dt> -v
     356  <dd> Verbose mode.
     357  </dl>
     358
     359  <dt> -k
     360  <dd> number of steps (default 1).
     361  </dl>
     362  ]
     363
     364  SideEffects []
     365
     366******************************************************************************/
     367
     368static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
     369{
     370  BmcOption_t  *options = BmcOptionAlloc();
     371  int c;
     372  unsigned int i;
     373  Ntk_Network_t * network;
     374  bAig_Manager_t   * manager;
     375  char *  outName = NIL(char);
     376   FILE *cnfFile;
     377  if (!options){
     378    return 1;
     379  }
     380  options->dbgOut = 0;
     381  /*
     382   * Parse command line options.
     383   */
     384  util_getopt_reset();
     385  while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) {
     386    switch(c) {
     387    case 'h':
     388      goto usage;
     389    case 'k':
     390      options->maxK = atoi(util_optarg);
     391      break;
     392    case 'v':
     393      for (i = 0; i < strlen(util_optarg); i++) {
     394        if (!isdigit((int)util_optarg[i])) {
     395          goto usage;
     396        }
     397      }
     398      options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
     399      break;
     400    default:
     401      goto usage;
     402    }
     403  }
     404   if (argc - util_optind != 0)
     405   {
     406      outName  = util_strsav(argv[util_optind]);
     407      /* create SAT Solver input file */
     408     options->cnfFileName= outName;
     409    options->satInFile = options->cnfFileName;
     410    cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
     411  }
     412 
     413 
     414/*
     415 *  Read the network
     416 */
     417network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
     418if (network == NIL(Ntk_Network_t)) {
     419  (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n");
     420  BmcOptionFree(options);
     421  return 1;
     422}
     423manager = Ntk_NetworkReadMAigManager(network);
     424if (manager == NIL(mAig_Manager_t)) {
     425  (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n");
     426  BmcOptionFree(options);
     427  return 1;
     428}
     429
     430 /*
     431    Compute the cone of influence
     432        here : a list of state variables (latches)
     433  */
     434st_table        *CoiTable =  generateAllLatches(network);
     435
     436if(options->verbosityLevel)
     437{       
     438        (void) fprintf(vis_stdout, "------      COI       ----\n");
     439        printLatch(CoiTable);
     440        (void) fprintf(vis_stdout, "--------------------------\n");
     441}
     442BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
     443  if(outName != NIL(char))
     444  {
     445    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
     446    fclose(cnfFile);
     447  }
     448  else
     449     BmcWriteClauses(manager, vis_stdout, cnfClauses, options);
     450
     451if(options->verbosityLevel)
     452{       
     453        (void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK);
     454    (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses,
     455    st_count(CoiTable));
     456}
     457   
     458BmcOptionFree(options);
     459 return 0;
     460 usage:
     461  (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] <cnf_file>\n");
     462  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
    431463  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
    432   (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the debug instance\n"); 
    433   (void) fprintf(vis_stderr, "   -p <ltl_file> contains the ltl formula\n"); 
    434   return 1;             /* error exit */
    435 
    436 }
     464  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
     465  (void) fprintf(vis_stderr, "       verbosity_level = 0 => no feedback (Default)\n");
     466  (void) fprintf(vis_stderr, "       verbosity_level = 1 => code status\n");
     467  (void) fprintf(vis_stderr, "       verbosity_level = 2 => code status and CPU usage profile\n");
     468  (void) fprintf(vis_stderr, "   <cnf_file> The output file containing CNF of the network.\n");
     469
     470  BmcOptionFree(options);
     471  return 1;
     472}
     473
    437474/**Function********************************************************************
    438475

  • vis_dev/vis-2.3/src/debug/debug.h

    r40 r41  
    132132EXTERN array_t* Dbg_ReadAbn(Dbg_Abnormal_t *abnormal);
    133133EXTERN Dbg_Abnormal_t * Dbg_NetworkReadAbnormal(Ntk_Network_t * network);
     134EXTERN void Dbg_InitAbn(Dbg_Abnormal_t * abn, bAig_Manager_t   * manager,
     135st_table * nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses);
     136EXTERN int Dbg_SatCheck(char * forceAssigName, char * cnfFileName);
     137EXTERN BmcCnfClauses_t* Dbg_GenerateCNF(Ntk_Network_t * network,
     138BmcOption_t * option, st_table  *CoiTable);
     139
     140
     141
    134142/**AutomaticEnd***************************************************************/
    135143

  • vis_dev/vis-2.3/src/debug/debugAbnormal.c

    r40 r41  
    138138         abn->abnormal = array_alloc(Ntk_Node_t*,0);
    139139         abn->freeInputs = array_alloc(Ntk_Node_t*,0);
     140     abn->abnAigArray = NIL(array_t);
     141     abn->abnCnfIndexArray = NIL(array_t);
    140142         abn->verbose = 0;
    141143         return abn;
    … …  
    158160         array_free(abn->abnormal);
    159161         array_free(abn->freeInputs);
     162     array_free(abn->abnCnfIndexArray);
     163     array_free(abn->abnAigArray);
    160164         FREE(abn);
    161165}       
    … …  
    267271        return abn;
    268272}
     273/**Function********************************************************************
     274 
     275  Synopsis    [Initialize the abnormal predicate in the clauses array abni =0]
     276
     277  Description [Fill the Dbg data structure, abnAigArray conains the set of Aig
     278  for the set of abnormal perdicate. Each abnormal are set to zero in the clause
     279  array.predicabnCnfIndexArray is the cnf index. The   correspondance is made by
     280  the index in the table, the index of a node in   abnArray is the same in
     281  abnAigArray and in abnIndexArray. If this array were  alredy computed nothing
     282  is done, if the aig or index information either.]
     283
     284  SideEffects [Fill abnAigArray and abnCnfIndexArray]
     285
     286  SeeAlso     []
     287
     288******************************************************************************/
     289void Dbg_InitAbn(Dbg_Abnormal_t * abn,
     290bAig_Manager_t   * manager,
     291st_table * nodeToMvfAigTable,
     292BmcCnfClauses_t *cnfClauses)
     293{
     294  if(abn->abnAigArray != NIL(array_t))
     295    (void) fprintf(vis_stdout, "Abnormal aig alredy filled\n");
     296  if(abn->abnCnfIndexArray != NIL(array_t)){
     297    (void) fprintf(vis_stdout, "Abnormal index alredy filled\n");
     298     return;
     299  }
     300  //Fill
     301   int size = array_n(abn->abnormal);
     302   array_t * abnAigArray = array_alloc(bAigEdge_t *,size);
     303   array_t * abnIndexArray = array_alloc(int,size);
     304   int aIndex;
     305   Ntk_Node_t * abnNode;
     306   Dbg_ForEachAbnormal(abn, aIndex,abnNode){
     307   MvfAig_Function_t * abnMvfAig = Bmc_ReadMvfAig(abnNode, nodeToMvfAigTable);
     308    if (abnMvfAig ==  NIL(MvfAig_Function_t)){
     309     (void) fprintf(vis_stdout, "No multi-valued function for this node %s \
     310     create abnormal predicate firs \n", Ntk_NodeReadName(abnNode));
     311     return ;
     312    }
     313    int mvfSize   = array_n(abnMvfAig);
     314    int i;
     315    bAigEdge_t         * abnBAig  = ALLOC(bAigEdge_t, mvfSize);
     316
     317    for(i=0; i< mvfSize; i++)
     318    {
     319      abnBAig[i] = bAig_GetCanonical(manager,
     320      MvfAig_FunctionReadComponent(abnMvfAig,  i));
     321    }
     322    array_insert(bAigEdge_t*,abnAigArray,aIndex,abnBAig);
     323    int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[0],0,cnfClauses);
     324    array_insert(int,abnIndexArray,aIndex,cnfClauses->nextIndex);
     325    // Create clause
     326     array_t           *abnClause = NIL(array_t);
     327         abnClause = array_alloc(int, 0);   
     328         array_insert_last(int, abnClause, abnIndex);
     329         BmcCnfInsertClause(cnfClauses, abnClause);
     330     array_free(abnClause);
     331   }
     332   abn->abnAigArray = abnAigArray;
     333   abn->abnCnfIndexArray = abnIndexArray;
     334}

  • vis_dev/vis-2.3/src/debug/debugInt.h

    r36 r41  
    5555        array_t * abnormal; /* Array of Ntk_Node_t* */
    5656        array_t * freeInputs; /* Array of Ntk_Node_t* */
     57        array_t * abnAigArray; /* Array of bAigEdge_t* as many entries as possible value */
     58        array_t * abnCnfIndexArray; /* Array of int */
    5759        int verbose;
    5860};

  • vis_dev/vis-2.3/src/debug/debugUtilities.c

    r35 r41  
    8787  return;
    8888}
     89/**Function********************************************************************
     90 
     91  Synopsis    [Performs the sat call]
     92
     93  Description [Retrun the result of SAT call, avec positionnement des options]
     94  SideEffects []
     95
     96  SeeAlso     []
     97
     98******************************************************************************/
     99
     100int Dbg_SatCheck(char * forceAssigName, char * cnfFileName
     101)
     102{
     103 satManager_t *cm;
     104 cm = sat_InitManager(0);
     105 cm->comment = ALLOC(char, 2);
     106 cm->comment[0] = ' ';
     107 cm->comment[1] = '\0';
     108 cm->stdOut = stdout;
     109 cm->stdErr = stderr;
     110
     111 
     112  satOption_t  *satOption;
     113  array_t      *result = NIL(array_t);
     114  int          maxSize;
     115
     116  satOption = sat_InitOption();
     117  satOption->verbose = 2;
     118  //satOption->unsatCoreFileName = "Ucore.txt";
     119  satOption->clauseDeletionHeuristic = 0;
     120  //satOption->coreGeneration = 1 ;
     121  //satOption->minimizeConflictClause = 1;
     122  if(forceAssigName != NULL)
     123    satOption->forcedAssignArr = sat_ReadForcedAssignment(forceAssigName);
     124   cm->option = satOption;
     125   cm->each = sat_InitStatistics();
     126
     127  cm->unitLits = sat_ArrayAlloc(16);
     128  cm->pureLits = sat_ArrayAlloc(16);
     129
     130  maxSize = 1024 << 8;
     131  cm->nodesArray = ALLOC(long, maxSize);
     132  cm->maxNodesArraySize = maxSize;
     133  cm->nodesArraySize = satNodeSize;
     134
     135  sat_AllocLiteralsDB(cm);
     136
     137   sat_ReadCNF(cm,cnfFileName);
     138   sat_Main(cm);
     139
     140   if(cm->status == SAT_UNSAT) {
     141    if(cm->option->forcedAssignArr)
     142      fprintf(cm->stdOut, "%s UNSAT under given assignment\n",
     143              cm->comment);
     144    fprintf(cm->stdOut, "%s UNSATISFIABLE\n", cm->comment);
     145    fflush(cm->stdOut);
     146    sat_ReportStatistics(cm, cm->each);
     147    sat_FreeManager(cm);
     148  }
     149  else if(cm->status == SAT_SAT) {
     150    fprintf(cm->stdOut, "%s SATISFIABLE\n", cm->comment);
     151    fflush(cm->stdOut);
     152    sat_PrintSatisfyingAssignment(cm);
     153    sat_ReportStatistics(cm, cm->each);
     154    sat_FreeManager(cm);
     155  }
     156return cm->status;
     157}
     158/**Function********************************************************************
     159 
     160  Synopsis    [Generate a CNF of the network]
     161
     162  Description [Generate the set of clauses of the unroll network for a given
     163  length and for a given cone of influence]
     164  SideEffects []
     165
     166  SeeAlso     []
     167
     168******************************************************************************/
     169BmcCnfClauses_t*
     170Dbg_GenerateCNF(Ntk_Network_t * network,
     171BmcOption_t * options,
     172st_table  *CoiTable
     173){
     174st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
     175BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
     176/*
     177 *nodeToMvfAigTable maps each node to its multi-function And/Inv graph
     178 */
     179nodeToMvfAigTable =
     180(st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
     181assert(nodeToMvfAigTable != NIL(st_table));
     182/*
     183 * Create a clause database
     184 */
     185cnfClauses = BmcCnfClausesAlloc();
     186/*
     187 * Generate clauses for an initialized path of length k
     188 */
     189BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
     190                         cnfClauses, nodeToMvfAigTable, CoiTable);
     191return cnfClauses;
     192
     193}
Note: See TracChangeset for help on using the changeset viewer.