source: vis_dev/vis-2.3/src/puresat/puresatMain.c @ 40

Last change on this file since 40 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 21.9 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [puresatMain.c]
4
5  PackageName [puresat]
6
7  Synopsis    [Abstraction refinement for large scale invariant checking.]
8
9  Description [This file contains the functions to check invariant properties
10  by the PureSAT abstraction refinement algorithm, which is entirely based on
11  SAT solver, the input of which could be either CNF or AIG. It has several
12  parts:
13
14  * Localization-reduction base Abstraction
15  * K-induction or interpolation to prove the truth of a property
16  * Bounded Model Checking to find bugs
17  * Incremental concretization based methods to verify abstract bugs
18  * Incremental SAT solver to improve efficiency
19  * UNSAT proof based method to obtain refinement
20  * AROSAT to bring in only necessary latches into unsat proofs
21  * Bridge abstraction to get compact coarse refinement
22  * Refinement minization to guarrantee minimal refinements
23  * Unsat proof-based refinement minimization to eliminate multiple candidate
24    by on SAT test
25  * Refinement prediction to decrease the number of refinement iterations
26  * Dynamic switching to redistribute computional resources to improve
27    efficiency
28 
29  For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05
30  paper of Li et al., "A satisfiability-based appraoch to abstraction
31  refinement in model checking", " Abstraction in symbolic model checking
32  using satisfiability as the only decision procedure", "Efficient computation
33  of small abstraction refinements", and "Efficient abstraction refinement in
34  interpolation-based unbounded model checking"]
35 
36  Author      [Bing Li]
37
38  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
39  All rights reserved.
40
41  Permission is hereby granted, without written agreement and without
42  license or royalty fees, to use, copy, modify, and distribute this
43  software and its documentation for any purpose, provided that the
44  above copyright notice and the following two paragraphs appear in
45  all copies of this software.]
46
47******************************************************************************/
48#include "puresatInt.h"
49
50
51/*---------------------------------------------------------------------------*/
52/* Constant declarations                                                     */
53/*---------------------------------------------------------------------------*/
54
55/*---------------------------------------------------------------------------*/
56/* Structure declarations                                                    */
57/*---------------------------------------------------------------------------*/
58
59/*---------------------------------------------------------------------------*/
60/* Type declarations                                                         */
61/*---------------------------------------------------------------------------*/
62
63/*---------------------------------------------------------------------------*/
64/* Variable declarations                                                     */
65/*---------------------------------------------------------------------------*/
66
67/*---------------------------------------------------------------------------*/
68/* Macro declarations                                                        */
69/*---------------------------------------------------------------------------*/
70
71/**AutomaticStart*************************************************************/
72
73/*---------------------------------------------------------------------------*/
74/* Static function prototypes                                                */
75/*---------------------------------------------------------------------------*/
76
77/**AutomaticEnd***************************************************************/
78
79/*---------------------------------------------------------------------------*/
80/* Definition of exported functions                                          */
81/*---------------------------------------------------------------------------*/
82
83/*---------------------------------------------------------------------------*/
84/* Definition of internal functions                                          */
85/*---------------------------------------------------------------------------*/
86
87
88/**Function********************************************************************
89
90  Synopsis    [PURESAT command interface function]
91
92  Description [PURESAT command interface function]
93
94  SideEffects []
95
96  SeeAlso     []
97
98******************************************************************************/
99
100void
101PureSat_CheckInvariant(
102  Ntk_Network_t *network,
103  array_t *InvariantFormulaArray,
104  int verbosity,
105  int dbgLevel,
106  FILE *dbgOut,
107  boolean printInputs,
108  boolean incremental,
109  boolean sss,
110  boolean flatIP,
111  int speed)
112{
113  int result,i;
114  Ctlp_Formula_t  *invFormula;
115  Ctlsp_Formula_t *invFormula_sp;
116  PureSat_Manager_t * pm = PureSatManagerAlloc();
117
118  pm->incre = incremental;
119  pm->verbosity = verbosity;
120  pm->dbgLevel = dbgLevel;
121  pm->sss = sss;
122  pm->printInputs = printInputs;
123  pm->dbgOut = dbgOut;
124
125  switch(speed){
126  case 0:
127    break;
128  case 1:
129    pm->Switch = 0;
130    break;
131  case 2:
132    pm->Switch = 0;
133    pm->CoreRefMin = 0;
134    break;
135  case 3:
136    pm->Switch = 0;
137    pm->CoreRefMin = 0;
138    pm->RefPredict = 0;
139    break;
140  case 4:
141    pm->Switch = 0;
142    pm->CoreRefMin = 0;
143    pm->RefPredict = 0;
144    pm->Arosat = 0;
145    break;
146  default:
147    pm->Switch = 0;
148    pm->CoreRefMin = 0;
149    pm->RefPredict = 0;
150    pm->Arosat = 0;
151    break;
152  }
153   
154  arrayForEachItem(Ctlp_Formula_t *, InvariantFormulaArray, i, invFormula) {
155    /* if(Ctlsp_isCtlFormula(invFormula))*/
156    invFormula_sp = Ctlsp_CtlFormulaToCtlsp(invFormula);
157    if(sss)
158      /*SSS-base Puresat algorithm*/
159      result = PureSatCheckInv_SSS(network,invFormula_sp,pm);
160    else
161      if(flatIP)
162        /*Interpolation algorithm without abstraction refinement*/
163        result = PureSatCheckInv_FlatIP(network,invFormula_sp,pm);
164      else
165        /*Interpolation-based Puresat algorithm*/
166        result = PureSatCheckInv_IP(network,invFormula_sp,pm);
167    if(result){
168        (void) fprintf(vis_stdout, "# INV: formula passed --- ");
169        Ctlsp_FormulaPrint(vis_stdout, (invFormula_sp));
170        fprintf(vis_stdout, "\n");
171    }
172    else{
173      if(pm->dbgLevel != 2)
174      {
175        (void) fprintf(vis_stdout, "# INV: formula failed --- ");
176        Ctlsp_FormulaPrint(vis_stdout, (invFormula_sp));
177        fprintf(vis_stdout, "\n");
178      }
179    }
180  }
181  PureSatManagerFree(pm);
182}
183
184
185
186/*---------------------------------------------------------------------------*/
187/* Definition of internal functions                                          */
188/*---------------------------------------------------------------------------*/
189
190/**Function********************************************************************
191
192  Synopsis    [Main procedure of K-induction based PURESAT algorithm]
193
194  Description [Main procedure of K-induction based PURESAT algorithm]
195
196  SideEffects []
197
198  SeeAlso     []
199
200******************************************************************************/
201
202
203boolean PureSatCheckInv_SSS(Ntk_Network_t * network,
204                        Ctlsp_Formula_t *ltlFormula,
205                        PureSat_Manager_t *pm)
206{
207  lsGen     gen;
208  st_generator      *stGen;
209  int NumofCurrentLatch=0,Length=0,tmp=0,NumofLatch=0,i,j,k;
210  int addtoAbs=0,latchThreshHold=10000,RingPosition=0;
211  int oldLength=0, beginPosition=0;
212  int NumInSecondLevel =0;
213  array_t * visibleArray = array_alloc(char *,0);
214  array_t * invisibleArray = array_alloc(char *,0);
215  array_t * refinement = array_alloc(char*,0);
216  array_t * CoiArray,* ConClsArray;
217  array_t * arrayRC = NULL;
218  array_t *tmpRefinement;
219  array_t *tmpRefinement1;
220  char * nodeName;
221  Ntk_Node_t * node, *latch;
222  boolean ExistSimplePath = TRUE,ExistACE = FALSE;
223  boolean realRefine=TRUE;
224  boolean needSorting = FALSE, firstTime = TRUE;
225  mAig_Manager_t    *maigManager;
226  BmcOption_t * options;
227  BmcCnfStates_t    *cnfstate;
228  bAigEdge_t        property;
229  st_table * nodeToMvfAigTable;
230  double t1,t2, t0,t3;
231  long *space;
232  PureSat_IncreSATManager_t * pism1,*pism2;
233  satArray_t *saved;
234
235  pm->supportTable = st_init_table(st_ptrcmp,st_ptrhash);
236  pm->CoiTable = st_init_table(st_ptrcmp,st_ptrhash);
237  pm->vertexTable = st_init_table(strcmp, st_strhash);
238  pism1 = PureSatIncreSATManagerAlloc(pm);
239  pism2 = PureSatIncreSATManagerAlloc(pm);
240  t0 = util_cpu_ctime();
241
242  options = BmcOptionAlloc();
243  options->satInFile = BmcCreateTmpFile();
244  options->satOutFile = BmcCreateTmpFile();
245  NumofCurrentLatch=0;
246  t1 = util_cpu_ctime();
247  PureSatBmcGetCoiForLtlFormula(network, ltlFormula,pm->CoiTable);
248  PureSatGenerateSupportTable(network,pm);
249  t2 = util_cpu_ctime();
250  if(pm->verbosity>=2)
251    fprintf(vis_stdout,"Generate DFS: %g\n",(double)((t2-t1)/1000.0));
252 
253  pm->vertexTable = (st_table *)PureSatCreateInitialAbstraction(network,ltlFormula,&NumofCurrentLatch,pm);
254 
255  pm->AbsTable = st_init_table(st_ptrcmp,st_ptrhash);
256 
257  Ntk_NetworkForEachLatch(network, gen, node){
258    if (st_lookup_int(pm->CoiTable, node, &tmp)){
259      NumofLatch++;
260      nodeName = Ntk_NodeReadName(node);
261      if(st_lookup(pm->vertexTable,nodeName,NIL(char *)))
262        {
263          array_insert_last(char *,visibleArray,nodeName);
264          latch = Ntk_NetworkFindNodeByName(network,nodeName);
265          PureSatComputeTableForLatch(network,pm->AbsTable,latch);
266        }
267      else
268        array_insert_last(char *,invisibleArray,nodeName);
269    }
270   }
271  if(pm->verbosity>=1){
272    fprintf(vis_stdout,"visiblearray has %d latches\n",array_n(visibleArray));
273    fprintf(vis_stdout,"invisibleArray has %d latches\n",array_n(invisibleArray));
274  }
275  CoiArray = array_dup(visibleArray);
276  array_append(CoiArray,invisibleArray);
277   
278  maigManager = Ntk_NetworkReadMAigManager(network);
279  if (maigManager == NIL(mAig_Manager_t)) {
280    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
281    BmcOptionFree(options);
282    return 1;
283  }
284 nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
285                                                         MVFAIG_NETWORK_APPL_KEY);
286 
287 /*build property clauses*/
288 if (Ctlsp_isPropositionalFormula(ltlFormula))
289   property = BmcCreateMaigOfPropFormula(network, maigManager, ltlFormula);
290 else
291   property = BmcCreateMaigOfPropFormula(network, maigManager, ltlFormula->left);
292 
293 if (property == mAig_NULL){
294   fprintf(vis_stderr,"property = NULL\n");
295   exit(0);
296 }
297 
298 property = bAig_Not(property);
299 
300 while(NumofCurrentLatch < NumofLatch)
301   {
302     t3 = util_cpu_ctime();
303     if(pm->verbosity>=1)
304       fprintf(vis_stdout,"Current Latches: %d, COI latches:%d,NEW Length:%d,\n",
305               NumofCurrentLatch,NumofLatch,pm->Length);
306     if(pm->verbosity>=2)
307       fprintf(vis_stdout,"General time: %g\n",(double)((t3-t0)/1000.0));
308     //tmpRefinement1 = array_alloc(char *,0);
309     firstTime = TRUE;
310     pm->SufAbsTable = st_init_table(st_ptrcmp,st_ptrhash);
311     if(realRefine){
312       arrayForEachItem(char *,refinement,i,nodeName)
313         {
314           latch = Ntk_NetworkFindNodeByName(network,nodeName);
315           PureSatComputeTableForLatch(network,pm->AbsTable,latch);
316         }
317       array_append(visibleArray,refinement);
318       latchThreshHold=(int)((double)(array_n(CoiArray)-array_n(visibleArray))/(double)4)+1;
319       
320       addtoAbs =(int)((double)(array_n(CoiArray)-array_n(visibleArray))/(double)5)+1;
321       addtoAbs = addtoAbs >50 ? 50: addtoAbs;
322       
323       array_free(invisibleArray);
324       invisibleArray = array_alloc(char *,0);
325       st_foreach_item_int(pm->CoiTable,stGen,&latch,&i)
326         {
327           nodeName = Ntk_NodeReadName(latch);
328           if(!st_lookup(pm->vertexTable,nodeName,0))
329             array_insert_last(char *,invisibleArray,nodeName);
330         }
331       t1 = util_cpu_ctime();
332       PureSatGetCoiForVisibleArray_Ring(network, visibleArray,RingPosition, pm->CoiTable);
333       RingPosition = array_n(visibleArray);
334       arrayRC = PureSatGenerateRingFromAbs(network,pm,invisibleArray,&NumInSecondLevel);
335       if(pm->verbosity>=2){
336         fprintf(vis_stdout,"NumInSecondLevel is %d  ",NumInSecondLevel);
337         fprintf(vis_stdout,"latchThreshHold is %d\n",latchThreshHold);
338       }
339       latchThreshHold = (latchThreshHold <= NumInSecondLevel) ? latchThreshHold:NumInSecondLevel;
340       if(pm->verbosity>=2){
341         fprintf(vis_stdout,"New latchThreshHold is %d\n",latchThreshHold);
342       }
343       t2 = util_cpu_ctime();
344       if(pm->verbosity>=2){
345         fprintf(vis_stdout,"Generate Ring: %g\n",(double)((t2-t1)/1000.0));
346       }
347       array_free(refinement);
348     }/* if(realRefine)*/
349     
350     realRefine =FALSE; /* means no ref, just Length++.*/
351     t1 = util_cpu_ctime();
352     if((ExistSimplePath =
353        PureSatExistASimplePath(network,pism1,visibleArray,property,pm)))
354       {
355         t2 = util_cpu_ctime();
356         if(pm->verbosity>=2)
357           fprintf(vis_stdout,"Solve on Simple Path: %g\n",(double)((t2-t1)/1000.0));
358         pism1->oldLength = pm->Length;
359         pism1->Length = pm->Length;
360         pism1->beginPosition = array_n(visibleArray);
361         if(pm->verbosity>=1)
362           fprintf(vis_stdout, "Simple Path Exists, length = %d\n",pm->Length);
363         
364         /*check Abs Model*/
365         t1 = util_cpu_ctime();
366         ExistACE = PureSatIncreExistCE(network,pism2,visibleArray,property,pm);
367         if(pm->verbosity>=2)
368           fprintf(vis_stdout,"beginPosition2: %d, oldLength2 %d\n",pism2->beginPosition, pism2->oldLength);
369         t2 = util_cpu_ctime();
370         if(pm->verbosity>=2)
371           fprintf(vis_stdout,"Solve on Abs model: %g\n",(double)((t2-t1)/1000.0));
372         pism2->oldLength = pm->Length;
373         pism2->Length = pm->Length;
374         pism2->beginPosition = array_n(visibleArray);
375         needSorting = FALSE;
376         
377         /*keep a record of previous position for refine's use*/
378         oldLength = pism2->oldLength;
379         beginPosition = pism2->beginPosition;
380         
381         /* while(ExistACE)
382             loop until find sufficient set*/
383         if(ExistACE)
384           {
385             if(pm->verbosity>=1)
386               fprintf(vis_stdout,"found Abstract Counterexample at length %d\n", pm->Length);
387             cnfstate = BmcCnfClausesFreeze(pism2->cnfClauses);
388             pism2->propertyPos = cnfstate->nextIndex;
389             
390             /*store the conflict clauses*/
391             ConClsArray = array_alloc(int,0);
392             
393             /*if incremental */
394             if(pm->incre){
395               if(pism2->cm->savedConflictClauses){
396                 saved = pism2->cm->savedConflictClauses;
397                 for(i=0, space=saved->space; i<saved->num; i++, space++){
398                   array_insert_last(int,ConClsArray,*space);
399                 }
400               }
401             }
402             realRefine = TRUE;
403             
404             /*incrementally check Concrete Model*/
405             tmpRefinement = array_alloc(char *,0);
406             if(pm->verbosity>=2)
407               fprintf(vis_stdout,"Begin building a new abstract model\n");
408             for(i=0;i<array_n(arrayRC);i=i+latchThreshHold)
409               {
410                 if(i>0)
411                   latchThreshHold = array_n(arrayRC)-latchThreshHold;
412                 for(j=0;j<latchThreshHold;j++)
413                   {
414                     if((i+j)<array_n(arrayRC))
415                       {
416                         nodeName = array_fetch(char *,arrayRC,i+j);
417                         array_insert_last(char *,tmpRefinement,nodeName);
418                         if(pm->verbosity>=2)
419                           fprintf(vis_stdout, "picking %s\n",nodeName);
420                       }
421                     else
422                       break;
423                   }/* for(j=0;*/
424                 tmpRefinement1=array_dup(visibleArray);
425                 array_append(tmpRefinement1,tmpRefinement);
426                 
427                 t1 = util_cpu_ctime();
428                 pism2->cm->option->incAll = 1;
429                 pism2->cm->option->incTraceObjective = 0;
430                 pism2->cm->option->incPreserveNonobjective = 0;
431                 if(PureSatIncreExistCEForRefineOnAbs(network,pism2,tmpRefinement1,property,firstTime,pm)) {
432                   t2 = util_cpu_ctime();
433                   if(pm->verbosity>=2)
434                     fprintf(vis_stdout,"time for finding a sufficient set on model: %g\n",(double)((t2-t1)/1000.0));
435                   if((i+j)>=array_n(arrayRC)){
436                     if(pm->verbosity>=1)
437                       fprintf(vis_stdout,"found real counterexamples\n");
438                     if(pm->dbgLevel>=1){
439                       options->printInputs = TRUE;
440                       BmcPrintCounterExample(network, nodeToMvfAigTable, pism2->cnfClauses,
441                                              pm->result, pm->Length, pm->CoiTable, options, 
442                                              NIL(array_t));
443                       array_free(pm->result);
444                       pm->result = NIL(array_t);
445                     }
446                     array_free(tmpRefinement1);
447                     array_free(tmpRefinement);
448                     BmcOptionFree(options);
449                     PureSatIncreSATManagerFree(pm,pism1);
450                     PureSatIncreSATManagerFree(pm,pism2);
451                     /*PureSatManagerFree(pm);*/
452                     array_free(CoiArray);
453                     array_free(visibleArray);
454                     return FALSE;
455                   }
456                   else{
457                     if(pm->result!=NIL(array_t)){
458                       array_free(pm->result);
459                       pm->result = NIL(array_t);
460                     }
461                   }
462                 }
463                 else{
464                   t2 = util_cpu_ctime();
465                   if(pm->verbosity>=1)
466                     fprintf(vis_stdout,"found a sufficient model\n");
467                   if(pm->verbosity>=2)
468                     fprintf(vis_stdout,"time for finding a sufficient set on model: %g\n",(double)((t2-t1)/1000.0));
469                   firstTime = FALSE;
470                   arrayForEachItem(char *,tmpRefinement1,k,nodeName){
471                     node = Ntk_NetworkFindNodeByName(network, nodeName);
472                     if(!st_lookup(pm->SufAbsTable,node,NIL(char *)))
473                       st_insert(pm->SufAbsTable,node, (char *)0);
474                     else{
475                       fprintf(vis_stderr,"wrong in sufabstable \n");
476                       exit(0);
477                     }
478                   }
479                   pism2->beginPosition = array_n(tmpRefinement1);
480                   pism2->oldLength = Length;
481                   array_free(tmpRefinement1);
482                   break;
483                 }
484                 pism2->beginPosition = array_n(tmpRefinement1);
485                 array_free(tmpRefinement1);
486                 pism2->oldLength = Length;
487               } /*for(i=0;i<array_n(arrayRC)*/
488             
489             /*recover the conflict clauses and incremental SAT option*/
490             pism2->cm->option->incAll = 0;
491             pism2->cm->option->incTraceObjective = 1;
492             pism2->cm->option->incPreserveNonobjective = 1;
493             
494             /*if incremental*/
495             if(pm->incre){
496               if(pism2->cm->savedConflictClauses)
497                 sat_ArrayFree(pism2->cm->savedConflictClauses);
498               pism2->cm->savedConflictClauses = sat_ArrayAlloc(16);
499               arrayForEachItem(int, ConClsArray,i,tmp)
500                 sat_ArrayInsert(pism2->cm->savedConflictClauses,tmp);
501             }
502             array_free(tmpRefinement);
503             t1 = util_cpu_ctime();
504             refinement = PureSatRefineOnAbs(network,pm,property,addtoAbs);
505             t2 = util_cpu_ctime();
506             if(pm->verbosity>=2)
507               fprintf(vis_stdout,"time for RefOnAbs: %g\n",(double)((t2-t1)/1000.0));
508             st_free_table(pm->SufAbsTable);
509             pm->SufAbsTable = NIL(st_table);
510             
511             /*adjust parameters*/
512             NumofCurrentLatch+=array_n(refinement);
513             pm->Length++;
514             pism1->Length++;
515             pism2->Length++;
516             BmcCnfClausesRestore(pism2->cnfClauses, cnfstate);
517             pism2->beginPosition = beginPosition;
518             pism2->oldLength = oldLength;
519             FREE(cnfstate);
520           }/* if(pism2->cm->status == SAT_SAT)*/
521         else /*if(pism2->cm->status != SAT_SAT)*/
522           {
523             if(pm->verbosity>=1)
524               fprintf(vis_stdout,"no Abstract Counterexample at length %d \n",pm->Length);
525             pm->Length++;
526             pism1->Length++;
527             pism2->Length++;
528             st_free_table(pm->SufAbsTable);
529             pm->SufAbsTable = NIL(st_table);
530           }
531       } /*if(ExistSimplePath)*/
532     else /* if no simple path*/
533       {
534         t2 = util_cpu_ctime();
535         if(pm->verbosity>=2)
536           fprintf(vis_stdout,"Solve on Simple Path: %g\n",(double)((t2-t1)/1000.0));
537         if(pm->verbosity>=1)
538           fprintf(vis_stdout,"simple Path doesn't exist, exit\n");
539         BmcOptionFree(options);
540         PureSatIncreSATManagerFree(pm,pism1);
541         PureSatIncreSATManagerFree(pm,pism2);
542         PureSatManagerFree(pm);
543         array_free(CoiArray);
544         array_free(visibleArray);
545         return TRUE;
546       }
547   }/* while(NumofCurrentLatch < NumofLatch)*/
548 /*st_free_table(AbsTable);*/
549 
550 /*Now go to the concrete model*/
551 if(pm->verbosity>=1)
552   fprintf(vis_stdout,"reach concrete model\n");
553 array_append(visibleArray,refinement);
554 array_free(refinement);
555 while(PureSatExistASimplePath(network,pism1,visibleArray,property,pm))
556   {
557     pism1->oldLength = pism1->Length;
558     pism1->beginPosition = array_n(visibleArray);
559     if(PureSatExistCE(network,pism2,options,visibleArray,property,pm,1)) {
560       if(pm->verbosity>=1)
561         fprintf(vis_stdout,"found real counterexample of length:%d\n",pm->Length);
562       if(pm->dbgLevel>=1){
563         options->printInputs = TRUE;
564         BmcPrintCounterExample(network, nodeToMvfAigTable, pism2->cnfClauses,
565                                pm->result, pm->Length, pm->CoiTable, options, 
566                                NIL(array_t));
567       }
568       BmcOptionFree(options);
569       PureSatIncreSATManagerFree(pm,pism1);
570       PureSatIncreSATManagerFree(pm,pism2);
571       /*PureSatManagerFree(pm);*/
572       array_free(CoiArray);
573       array_free(visibleArray);
574       return FALSE;
575     }
576     else
577       {
578         pism2->oldLength = Length;
579         pm->Length++;
580         pism1->Length++;
581         pism2->Length++;
582         pism2->beginPosition = array_n(visibleArray);
583       }
584   }
585 
586 BmcOptionFree(options);
587 PureSatIncreSATManagerFree(pm,pism1);
588 PureSatIncreSATManagerFree(pm,pism2); 
589 /*PureSatManagerFree(pm);*/
590 array_free(CoiArray);
591 array_free(visibleArray);
592 return TRUE;
593}
594
595/**Function********************************************************************
596
597  Synopsis    [PURESAT command parser]
598
599  Description [PURESAT command parser]
600
601  SideEffects []
602
603  SeeAlso     []
604
605******************************************************************************/
606
607
608
609void PureSatCmdParse(int argc,
610                     char **argv,
611                     PureSat_Manager_t *pm)
612
613{
614  int c, incre;
615 
616  util_getopt_reset();
617  while ((c = util_getopt(argc, argv, "t:i:h:v:I:")) != EOF) {
618    switch(c) {
619      case 'i':
620        strcpy(pm->ltlFileName,util_strsav(util_optarg));
621        break; 
622      case 't' :
623        pm->timeOutPeriod = atoi(util_optarg);
624        break; 
625      case 'v':
626        pm->verbosity = atoi(util_optarg);
627        break;
628      case 'I':
629        incre = atoi(util_optarg);
630        pm->incre = (incre==0)? FALSE:TRUE;
631        break;
632      case 'h':
633        goto usage;
634      default:
635        goto usage;
636    }
637  }
638  return;
639 usage:
640  (void) fprintf(vis_stderr, "usage: abrf [-h][-i ltlfile][-t timeout]\n");
641  (void) fprintf(vis_stderr, "   -i \tName of LTL file.\n");
642  (void) fprintf(vis_stderr, "   -t \ttimeout.\n");
643  (void) fprintf(vis_stderr, "   -v \tverbosity for more information. \n");
644  (void) fprintf(vis_stderr, "   -I \tincremental SAT switch. \n");
645  (void) fprintf(vis_stderr, "\t\t0 for non-incremental, other values for incremental\n");
646  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
647
648}
649
650/*---------------------------------------------------------------------------*/
651/* Definition of static functions                                            */
652/*---------------------------------------------------------------------------*/
Note: See TracBrowser for help on using the repository browser.