source: vis_dev/vis-2.3/src/puresat/puresatIPAbRf.c @ 74

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

vis2.3
File size: 37.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [puresatAbRf.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 "maigInt.h"
49#include "puresatInt.h"
50
51/*---------------------------------------------------------------------------*/
52/* Constant declarations                                                     */
53/*---------------------------------------------------------------------------*/
54
55/*---------------------------------------------------------------------------*/
56/* Type declarations                                                         */
57/*---------------------------------------------------------------------------*/
58
59
60/*---------------------------------------------------------------------------*/
61/* Structure declarations                                                    */
62/*---------------------------------------------------------------------------*/
63
64
65/*---------------------------------------------------------------------------*/
66/* Variable declarations                                                     */
67/*---------------------------------------------------------------------------*/
68
69/*---------------------------------------------------------------------------*/
70/* Macro declarations                                                        */
71/*---------------------------------------------------------------------------*/
72
73/**AutomaticStart*************************************************************/
74
75/*---------------------------------------------------------------------------*/
76/* Static function prototypes                                                */
77/*---------------------------------------------------------------------------*/
78
79
80/**AutomaticEnd***************************************************************/
81
82/*---------------------------------------------------------------------------*/
83/* Definition of exported functions                                          */
84/*---------------------------------------------------------------------------*/
85
86
87/*---------------------------------------------------------------------------*/
88/* Definition of internal functions                                          */
89/*---------------------------------------------------------------------------*/
90
91/**Function********************************************************************
92
93  Synopsis    [Interpolation test for concrete model]
94
95  Description [used by dynamic switching]
96
97  SideEffects []
98
99  SeeAlso     []
100
101******************************************************************************/
102
103boolean PureSatIPOnCon(Ntk_Network_t * network,
104                       Ctlsp_Formula_t *ltlFormula,
105                       PureSat_Manager_t *pm)
106{
107  int k;
108  bAig_Manager_t    *manager;
109  bAigEdge_t        property;
110  double t1,t2;
111  array_t           *previousResultArray=0;
112  boolean firstTime;
113  int round;
114  st_table * tmpTable;
115  int oldPos1,nodes_in_coi=0;
116  satManager_t * cm;
117  bAigEdge_t state, tmpState;
118  double tCon=0;
119  RTManager_t *rm;
120
121  manager = Ntk_NetworkReadMAigManager(network);
122
123  if(pm->verbosity>=1)
124    fprintf(vis_stdout,"go to concrete model\n");
125
126 k = pm->Length;
127 round = 1;
128 PureSat_CleanMask(manager,ResetGlobalVarMask);
129 PureSat_MarkGlobalVar(manager,1);
130 while(1){
131   k += round-1;
132   pm->Length = k;
133
134   if(pm->verbosity>=1)
135     fprintf(vis_stdout,"\nk = %d InitState = %ld\n",k,manager->InitState);
136   manager->test2LevelMini = 1;
137   t1 = util_cpu_ctime();
138   bAig_PureSat_ExpandTimeFrame(network, manager,pm, k, BMC_NO_INITIAL_STATES);
139   t2 = util_cpu_ctime();
140   pm->tExp += t2-t1;
141   if(pm->verbosity>=2)
142     fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
143            (double)((t2-t1)/1000.0),pm->tExp/1000);
144   manager->test2LevelMini = 0;
145   if(pm->verbosity>=1){
146     fprintf(vis_stdout,"After expand TF\n");
147     PureSat_PrintAigStatus(manager);
148   }
149   manager->class_ = k+1;
150   property = BmcCirCUsCreatebAigOfPropFormula(network,
151                     manager, k, ltlFormula, BMC_NO_INITIAL_STATES);
152   property = bAig_Not(property);
153   if(property==0){
154     return TRUE;
155   }
156   if(property==1){
157     return FALSE;
158   }
159   oldPos1 = manager->nodesArraySize-bAigNodeSize;
160   if(pm->verbosity>=1){
161     fprintf(vis_stdout,"After expanding TF and building property\n");
162     PureSat_PrintAigStatus(manager);
163   }
164   firstTime = TRUE;
165   round = 0;
166   state = manager->InitState;
167
168   while(1){
169     round++;
170     if(pm->verbosity>=1)
171       fprintf(vis_stdout,"round:%d for k = %d\n",round,k);
172     manager->assertArray = sat_ArrayAlloc(1);
173     if(state!=bAig_One)
174       sat_ArrayInsert(manager->assertArray,state);
175     cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
176     cm->option->IP = 1;
177
178
179     if(cm->status==0){
180       if(pm->verbosity>=1)
181         fprintf(vis_stdout,"normal COI:\n");
182       if(pm->verbosity>=1) {
183         nodes_in_coi = PureSat_CountNodesInCoi(cm);
184         fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
185       }
186       t1 = util_cpu_ctime();
187       sat_Main(cm);
188
189       rm = cm->rm;
190       cm->option->IP = 0;
191       if(manager->NodesArray!=cm->nodesArray)
192         /*cm->nodesArray may be reallocated */
193         manager->NodesArray = cm->nodesArray;
194       t2 = util_cpu_ctime();
195       pm->tIPUnsat += t2 - t1;
196       if(pm->verbosity>=2)
197         fprintf(vis_stdout,"time for Unsat:%g, total:%g\n",
198                (double)((t2-t1)/1000.0),pm->tIPUnsat/1000);
199     }
200
201     if(cm->status == SAT_SAT){
202       /*SAT: first time->find bug, otherwise increase length*/
203       if(firstTime){
204         fprintf(vis_stdout,"found CEX of length %d\n",k);
205
206         sat_ArrayFree(manager->assertArray);
207         manager->assertArray = 0;
208         RT_Free(cm->rm);
209         PureSat_SatFreeManager(cm);
210         return FALSE;
211       }
212       else{
213
214         if(pm->verbosity>=1)
215           fprintf(vis_stdout,"find bogus bug at length k=%d,round=%d,increase length\n",k,round);
216
217         sat_ArrayFree(manager->assertArray);
218         RT_Free(cm->rm);
219         PureSat_SatFreeManager(cm);
220         break;
221       }
222     }
223     else{
224       /*UNSAT: get IP, add to init states, until reach convergence, which
225       means property is true
226       Bing: IP generation*/
227       assert(cm->currentDecision>=-1);
228       if(cm->currentDecision!=-1)
229         sat_Backtrack(cm, -1);
230       /*get rid of Conflict Clauses*/
231       PureSat_ResetManager(manager,cm,1);
232
233       if(cm->option->coreGeneration&&cm->status == SAT_UNSAT){
234         manager->class_ = 1;
235         t1 = util_cpu_ctime();
236         tmpState = sat_GenerateFwdIP(manager,cm,cm->rm->root,1);
237         manager->IPState = PureSat_MapIP(manager,tmpState,1,0);
238
239         /*Wheneven there is baigNode generated, Reset_Manager is necessary,
240           //since NodeArray may be reallocated, # of Nodes changed*/
241         PureSat_ResetManager(manager,cm,0);
242         t2 = util_cpu_ctime();
243         pm->tIPGen += t2 -t1;
244         if(pm->verbosity>=2)
245           fprintf(vis_stdout,"time for generating and mapping IP:%g, total:%g\n",
246                  (double)((t2-t1)/1000.0),pm->tIPGen/1000);
247         if(pm->verbosity>=1){
248           fprintf(vis_stdout,"After generate IP,IP2:%ld,%ld:\n",manager->IPState,tmpState);
249           PureSat_PrintAigStatus(manager);
250         }
251         manager->class_ = 2;
252
253         t1 = util_cpu_ctime();
254
255         RT_Free(cm->rm);
256         if(pm->verbosity>=1)
257           PureSat_PrintAigStatus(manager);
258       }
259
260       t1 = util_cpu_ctime();
261       if(PureSat_TestConvergeForIP(manager,pm,cm,state,manager->IPState)){
262         t2 = util_cpu_ctime();
263         tCon = tCon+t2-t1;
264         if(pm->verbosity>=2)
265           fprintf(vis_stdout,"time for generating Convergence:%g, Total:%g\n",
266                  (double)((t2-t1)/1000.0),tCon/1000);
267         if(pm->verbosity>=1){
268           fprintf(vis_stdout,"After test convergence:\n");
269           PureSat_PrintAigStatus(manager);
270         }
271         fprintf(vis_stdout,"property is true\n");
272         PureSat_SatFreeManager(cm);
273         sat_ArrayFree(manager->assertArray);
274         return TRUE;
275       }
276       else{
277         t2 = util_cpu_ctime();
278         pm->tIPCon += t2-t1;
279         if(pm->verbosity>=2)
280           fprintf(vis_stdout,"time for generating Convergence:%g, total:%g\n",
281                  (double)((t2-t1)/1000.0),pm->tIPCon/1000);
282         if(pm->verbosity>=1){
283           fprintf(vis_stdout,"After test convergence:\n");
284           PureSat_PrintAigStatus(manager);
285         }
286
287         manager->class_ = 0;
288         state = PureSat_Or(manager,state,manager->IPState);
289         PureSat_ResetManager(manager,cm,0);
290         if(pm->verbosity>=1)
291           fprintf(vis_stdout,"new InitState:%ld\n",state);
292
293       }
294     }/*else*/
295     sat_ArrayFree(manager->assertArray);
296     manager->assertArray = 0;
297     PureSat_SatFreeManager(cm);
298     firstTime = FALSE;
299   }/*inner While(1){*/
300   /*sat_ArrayInsert(previousResultArray, bAig_Not(property)); */
301 }/*outer While(1){*/
302 st_free_table(tmpTable);
303
304 sat_ArrayFree(manager->EqArray);
305 return TRUE;
306}
307
308
309/**Function********************************************************************
310
311  Synopsis    [Using interpolation on abstractions]
312
313  Description []
314
315  SideEffects []
316
317  SeeAlso     []
318
319******************************************************************************/
320
321boolean PureSat_CheckAceByIP(Ntk_Network_t *network,
322                             PureSat_Manager_t * pm,
323                             PureSat_IncreSATManager_t *pism,
324                             array_t *vertexArray,
325                             int * k,
326                             Ctlsp_Formula_t *ltlFormula,
327                             bAigEdge_t * returnProp,
328                             array_t *previousResultArray)
329{
330  int oldPos;
331  boolean firstTime,fork=0,ExistACE;
332  int round,oldLength,coiCon,coiAbs;
333  bAigEdge_t property;
334  double t1,t2,t3,t4,t5, threshold_sw=0;
335  satManager_t * cm;
336  array_t *bVarList,*mVarList;
337  bAigEdge_t state, tmpState;
338  BmcOption_t  *options = BmcOptionAlloc();
339  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
340
341  bVarList = mAigReadBinVarList(manager);
342  mVarList = mAigReadMulVarList(manager);
343  options->printInputs = TRUE;
344  options->verbosityLevel = BmcVerbosityMax_c;
345
346  assert(*k>=1);
347  manager->test2LevelMini = 1;
348  bAig_PureSat_ExpandTimeFrame(network, manager, pm,*k,
349                               BMC_NO_INITIAL_STATES);
350  manager->test2LevelMini = 0;
351  PureSat_CleanMask(manager,ResetVisibleVarMask);
352  PuresatMarkVisibleVar(network,vertexArray,pm,0,*k+1);
353  PureSat_CleanMask(manager,ResetGlobalVarMask);
354
355  PureSat_MarkGlobalVar_AbRf(manager,1);
356  oldLength = *k;
357
358  while(1){
359    if(fork){
360      oldLength = pm->Length;
361      (*k) += round-1;
362      pm->Length = *k;
363    }
364    fork=1;
365    if(pm->verbosity>=1)
366      fprintf(vis_stdout,"\nk = %d InitState = %ld\n",*k,manager->InitState);
367    manager->test2LevelMini = 1;
368    t1 = util_cpu_ctime();
369    bAig_PureSat_ExpandTimeFrame(network, manager, pm,*k,
370                                 BMC_NO_INITIAL_STATES);
371    t2 = util_cpu_ctime();
372    pm->tExp += t2-t1;
373    if(pm->verbosity>=2)
374      fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
375             (double)((t2-t1)/1000.0),pm->tExp/1000);
376    manager->test2LevelMini = 0;
377    PureSat_CleanMask(manager,ResetVisibleVarMask);
378    PuresatMarkVisibleVar(network,vertexArray,pm,0,*k+1);
379    manager->class_ = *k+1;
380    property = PureSatCreatebAigOfPropFormula(network,
381                manager, *k, ltlFormula, BMC_NO_INITIAL_STATES);
382    property = bAig_Not(property);
383    *returnProp = property;
384    if(pm->verbosity>=1)
385      fprintf(vis_stdout,"property is %ld\n",property);
386    oldPos = manager->nodesArraySize-bAigNodeSize;
387    if(pm->verbosity>=1){
388      fprintf(vis_stdout,"After expanding TF and building property\n");
389      PureSat_PrintAigStatus(manager);
390    }
391    firstTime = TRUE;
392    round = 0;
393    state = manager->InitState;
394    /*for one length*/
395    while(1){
396      round++;
397      if(pm->verbosity>=1)
398        fprintf(vis_stdout,"round:%d for k = %d\n",round,*k);
399      manager->assertArray = sat_ArrayAlloc(1);
400      if(state!=bAig_One)
401        sat_ArrayInsert(manager->assertArray,state);
402      cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
403      cm->option->IP = 1;
404      cm->option->AbRf = 1;
405
406
407      if(round == 1){
408        PureSat_ResetCoi(cm);
409        sat_SetConeOfInfluence(cm);
410        if(pm->verbosity>=1)
411          fprintf(vis_stdout,"COI nodes if check concrete model:\n");
412        coiCon = PureSat_CountNodesInCoi(cm);
413        if(pm->verbosity>=1)
414          fprintf(vis_stdout,"There are %d node in COI\n",coiCon);
415      }
416
417      t1 = util_cpu_ctime();
418
419      PureSatSetCOI(network,pm,cm,pm->vertexTable,0, *k,*k);
420      t2 = util_cpu_ctime();
421      pm->tPro += t2-t1;
422      if(pm->verbosity>=2)
423        fprintf(vis_stdout,"process time:%g,total:%g\n",
424               (double)((t2-t1)/1000.0),pm->tPro/1000);
425      /*switch to concrete model*/
426      if(pm->verbosity>=1)
427        fprintf(vis_stdout,"normal COI:\n");
428      coiAbs = PureSat_CountNodesInCoi(cm);
429      if(round == 1){
430        if(pm->verbosity>=1)
431          fprintf(vis_stdout,"Coi of abs divided by Coi of con: %g\n",
432                 (double)coiAbs/(double)coiCon);
433#if SWITCH_DA
434        if((double)coiAbs/(double)coiCon >= 0.68&&*k>=5){
435          if(pm->switch_da == 0){
436            if(pm->verbosity>=1)
437              fprintf(vis_stdout,"Switch to DirAdd mode\n");
438            pm->switch_da = 1;
439          }
440        }
441#endif
442
443        if(pm->Switch)
444          threshold_sw = 0.68;
445        else
446          threshold_sw = 1.1;
447
448        if(((double)coiAbs/(double)coiCon) >= threshold_sw&&*k>=5){
449
450          t3 = util_cpu_ctime();
451          sat_ArrayFree(manager->assertArray);
452          manager->assertArray = 0;
453          if(pm->verbosity>=1)
454            fprintf(vis_stdout,"Abs model is large, go to Concrete model\n");
455          ExistACE = PureSatIPOnCon(network,ltlFormula,pm);
456          PureSat_SatFreeManager(cm);
457          t1 = util_cpu_ctime();
458          if(pm->verbosity>=1)
459            fprintf(vis_stdout,"Run on concrete model: %g\n",(double)((t1-t3)/1000.0));
460          if(ExistACE){
461            pm->returnVal = 1;
462            return FALSE;
463          }
464          else{
465            pm->returnVal = -1;
466            return TRUE;
467          }
468        }
469      }
470
471      PureSatKillPseudoGV(network,pm,pm->vertexTable,1,*k);
472      PureSat_ResetManager(manager,cm,0);
473      PureSatProcessFanout(cm);
474
475      t1 = util_cpu_ctime();
476      sat_Main(cm);
477      if(pm->verbosity>=2)
478        sat_ReportStatistics(cm,cm->each);
479      cm->option->IP = 0;
480      if(manager->NodesArray!=cm->nodesArray)
481        /*cm->nodesArray may be reallocated*/
482        manager->NodesArray = cm->nodesArray;
483      t2 = util_cpu_ctime();
484      pm->tIPUnsat += t2 - t1;
485      if(pm->verbosity>=2)
486        fprintf(vis_stdout,"time for Unsat:%g, total:%g\n",
487               (double)((t2-t1)/1000.0),pm->tIPUnsat/1000);
488      t1 = util_cpu_ctime();
489      PureSatPostprocess(manager,cm,pm);
490      /*clean masks*/
491      sat_CleanDatabase(cm);
492
493      if(cm->status==SAT_UNSAT){
494        PureSatProcessDummy(manager,cm,cm->rm->root);
495        ResetRTree(cm->rm);
496      }
497      t2 = util_cpu_ctime();
498      pm->tPro += t2-t1;
499      if(pm->verbosity>=2)
500        fprintf(vis_stdout,"process time:%g,total:%g\n",
501               (double)((t2-t1)/1000.0),pm->tPro/1000);
502
503      if(cm->status == SAT_SAT){
504        /*SAT: first time->find bug, otherwise increase length*/
505        if(firstTime){
506          if(pm->verbosity>=1)
507            fprintf(vis_stdout,"found abstract CEX of length %d\n",*k);
508
509
510          PureSat_UnMarkGlobalVar(manager,1);
511          RT_Free(cm->rm);
512          PureSat_SatFreeManager(cm);
513          sat_ArrayFree(manager->assertArray);
514          return TRUE;
515       }
516        else{
517
518          if(pm->verbosity>=1)
519            fprintf(vis_stdout,"find bogus bug at length k=%d,round=%d,increase length\n",*k,round);
520          sat_ArrayFree(manager->assertArray);
521          RT_Free(cm->rm);
522          PureSat_SatFreeManager(cm);
523          break;
524        }
525      }
526     else{
527       /*UNSAT: get IP, add to init states, until reach convergence, which
528       //means property is true
529       //Bing: IP generation*/
530       assert(cm->currentDecision>=-1);
531       if(cm->currentDecision!=-1)
532         sat_Backtrack(cm, -1);
533       PureSat_ResetManager(manager,cm,1);//get rid of Conflict Clauses
534       if(cm->option->coreGeneration&&cm->status == SAT_UNSAT){
535         manager->class_ = 1;
536         t1 = util_cpu_ctime();
537         tmpState = sat_GenerateFwdIP(manager,cm,cm->rm->root,1);
538         manager->IPState = PureSat_MapIP(manager,tmpState,1,0);
539
540         /*Wheneven there is baigNode generated, Reset_Manager is necessary,
541           //since NodeArray may be reallocated, # of Nodes changed*/
542         PureSat_ResetManager(manager,cm,0);
543         t2 = util_cpu_ctime();
544
545         pm->tIPGen += t2 -t1;
546         if(pm->verbosity>=2)
547           fprintf(vis_stdout,"time for generating and mapping IP:%g, total:%g\n",
548                  (double)((t2-t1)/1000.0),pm->tIPGen/1000);
549         if(pm->verbosity>=1){
550           fprintf(vis_stdout,"After generate IP,%ld:\n",manager->IPState);
551           PureSat_PrintAigStatus(manager);
552         }
553         manager->class_ = 2;
554         if(pm->verbosity>=1)
555           fprintf(vis_stdout,"After generate IP2:%ld\n",tmpState);
556         t4 = util_cpu_ctime();
557         RT_Free(cm->rm);
558         t5 = util_cpu_ctime();
559         pm->tGFree += (t5-t4);
560         if(pm->verbosity>=2)
561           fprintf(vis_stdout,"GFree time :%g\n",(t5-t4)/1000);
562         if(pm->verbosity>=1)
563           PureSat_PrintAigStatus(manager);
564         }
565
566       t1 = util_cpu_ctime();
567       if(PureSat_TestConvergeForIP_AbRf(network,cm,pm,vertexArray,
568                                         state,manager->IPState)){
569         t2 = util_cpu_ctime();
570         pm->tIPCon += t2-t1;
571         if(pm->verbosity>=2)
572           fprintf(vis_stdout,"time for generating Convergence:%g, total:%g\n",
573                  (double)((t2-t1)/1000.0),pm->tIPCon/1000);
574         if(pm->verbosity>=1){
575           fprintf(vis_stdout,"After test convergence:\n");
576           PureSat_PrintAigStatus(manager);
577         }
578         fprintf(vis_stdout,"property is true\n");
579         PureSat_SatFreeManager(cm);
580         sat_ArrayFree(manager->assertArray);
581         return FALSE;
582       }
583       else{
584         t2 = util_cpu_ctime();
585         pm->tIPCon += t2-t1;
586         if(pm->verbosity>=2)
587           fprintf(vis_stdout,"time for generating Convergence:%g, total:%g\n",
588                  (double)((t2-t1)/1000.0),pm->tIPCon/1000);
589         if(pm->verbosity>=1){
590           fprintf(vis_stdout,"After test convergence:\n");
591           PureSat_PrintAigStatus(manager);
592         }
593         manager->class_ = 0;
594         state = PureSat_Or(manager,state,manager->IPState);
595         if(pm->verbosity>=1)
596           fprintf(vis_stdout,"new InitState:%ld\n",state);
597       }
598     }/*else */
599     sat_ArrayFree(manager->assertArray);
600     PureSat_SatFreeManager(cm);
601     firstTime = FALSE;
602    }/*inner While(1){*/
603  }/*outer While(1){*/
604 return FALSE;
605}
606
607
608
609/**Function********************************************************************
610
611  Synopsis    [Main procedure of interpolation-based PureSat]
612
613  Description []
614
615  SideEffects []
616
617  SeeAlso     []
618
619******************************************************************************/
620
621boolean PureSatCheckInv_IP(Ntk_Network_t * network,
622                             Ctlsp_Formula_t *ltlFormula,
623                             PureSat_Manager_t *pm)
624{
625  lsGen     gen;
626  st_generator      *stGen;
627  int NumofCurrentLatch=0,Length=0,tmp=0,NumofLatch=0,i,j,k;
628  int addtoAbs,latchThreshHold;
629  int NumInSecondLevel=0;
630  array_t * visibleArray = array_alloc(char *,0);
631  array_t * invisibleArray = array_alloc(char *,0);
632  array_t * refinement= array_alloc(char *,0);
633  array_t * CoiArray = array_alloc(char *,0);
634  array_t * arrayRC = array_alloc(char *,0);
635  array_t *tmpRefinement = array_alloc(char *,0);
636  array_t *tmpRefinement1 = array_alloc(char *,0),*previousResultArray ;
637  char * nodeName;
638  Ntk_Node_t * node, *latch;
639  boolean ExistACE = FALSE,realRefine=TRUE;
640  boolean firstTime = TRUE;
641  bAig_Manager_t    *manager;
642  BmcOption_t * options;
643  bAigEdge_t   property;
644  st_table * nodeToMvfAigTable;
645  double t1,t2,t5, t0,t3,t4,t4total=0;
646  PureSat_IncreSATManager_t * pism1;
647  IP_Manager_t * ipm = IPManagerAlloc();
648  satManager_t *cm;
649  int * sccArray=NULL, orderCt, satStat=0;
650  st_table * tmpTable;
651
652
653  manager = Ntk_NetworkReadMAigManager(network);
654  if (manager == NIL(bAig_Manager_t)) {
655    (void) fprintf(vis_stdout,
656    "** bmc error: run build_partition_maigs command first\n");
657    return 1;
658  }
659  nodeToMvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
660                                                          MVFAIG_NETWORK_APPL_KEY);
661
662  pm->supportTable = st_init_table(st_ptrcmp,st_ptrhash);
663  pm->CoiTable = st_init_table(st_ptrcmp,st_ptrhash);
664  pm->oldCoiTable = st_init_table(st_ptrcmp,st_ptrhash);
665  pm->vertexTable = st_init_table(strcmp, st_strhash);
666  pism1 = PureSatIncreSATManagerAlloc(pm);
667  t0 = util_cpu_ctime();
668
669  options = BmcOptionAlloc();
670  options->verbosityLevel = BmcVerbosityMax_c;
671  options->printInputs = TRUE;
672
673  t1 = util_cpu_ctime();
674  previousResultArray    = array_alloc(bAigEdge_t, 0);
675  manager->class_ = 0;
676  manager->ipm = ipm;
677  manager->test2LevelMini = 1;
678  t3 = util_cpu_ctime();
679  bAig_PureSat_InitTimeFrame(network,manager,pm,0);
680  t5 = util_cpu_ctime();
681  pm->tExp += t5-t3;
682  if(pm->verbosity>=2)
683    fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
684            (double)((t5-t3)/1000.0),pm->tExp/1000);
685  manager->test2LevelMini = 0;
686  if(pm->verbosity>=1){
687    fprintf(vis_stdout,"after Init timeframe:\n");
688    PureSat_PrintAigStatus(manager);
689  }
690  manager->class_ = 1;
691  property = PureSatCreatebAigOfPropFormula(network,
692    manager, 0, ltlFormula, BMC_NO_INITIAL_STATES);
693  property = bAig_Not(property);
694  if(pm->verbosity>=1)
695    fprintf(vis_stdout,"property is %ld\n",property);
696  if(property==0)
697    return TRUE;
698  if(property==1)
699    return FALSE;
700  manager->assertArray = sat_ArrayAlloc(1);
701  sat_ArrayInsert(manager->assertArray,manager->InitState);
702  cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
703  sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
704  cm->option->coreGeneration = 0;
705  cm->option->IP = 0;
706  if(pm->verbosity>=1)
707    fprintf(vis_stdout,"test length 0\n");
708  sat_Main(cm);
709  manager->NodesArray = cm->nodesArray;
710  if(cm->status==SAT_SAT){
711    fprintf(vis_stdout,"find counter example of length 0\n");
712    BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
713                                 0, 0,options, BMC_NO_INITIAL_STATES);
714    return FALSE;
715  }
716  cm->option->coreGeneration = 1;
717  PureSat_SatFreeManager(cm);
718
719  manager->test2LevelMini = 1;
720  t3 = util_cpu_ctime();
721  bAig_PureSat_ExpandTimeFrame(network, manager,pm,1, BMC_NO_INITIAL_STATES);
722  t5 = util_cpu_ctime();
723  pm->tExp += t5-t3;
724  if(pm->verbosity>=2)
725    fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
726            (double)((t5-t3)/1000.0),pm->tExp/1000);
727  manager->class_ = 2;
728  manager->test2LevelMini = 0;
729  property = PureSatCreatebAigOfPropFormula(network,
730    manager, 1, ltlFormula, BMC_NO_INITIAL_STATES);
731  property = bAig_Not(property);
732
733  if(pm->verbosity>=1)
734    fprintf(vis_stdout,"property is %ld\n",property);
735  if(property==0)
736    return TRUE;
737  if(property==1)
738    return FALSE;
739  manager->assertArray = sat_ArrayAlloc(1);
740  sat_ArrayInsert(manager->assertArray,manager->InitState);
741  cm = PureSat_SatManagerAlloc(manager,pm,property,previousResultArray);
742  sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
743  cm->option->coreGeneration = 0;
744  cm->option->IP = 0;
745  if(pm->verbosity>=1)
746    fprintf(vis_stdout,"test length 1\n");
747  sat_Main(cm);
748  manager->NodesArray = cm->nodesArray;
749  if(cm->status==SAT_SAT){
750    fprintf(vis_stdout,"find counter example of length 1\n");
751    BmcCirCUsPrintCounterExample(network, nodeToMvfAigTable, pm->CoiTable,
752                                 1, 0,options, BMC_NO_INITIAL_STATES);
753    return FALSE;
754  }
755  t2 = util_cpu_ctime();
756  if(pm->verbosity>=2)
757    fprintf(vis_stdout,"Time for testing Length 0 and 1: %g\n",(double)((t2-t1)/1000.0));
758  cm->option->coreGeneration = 1;
759  PureSat_SatFreeManager(cm);
760  Length = 2;
761  pm->Length = Length;
762  pism1->Length = Length;
763
764  manager->test2LevelMini = 1;
765  t3 = util_cpu_ctime();
766  bAig_PureSat_ExpandTimeFrame(network, manager,pm,2, BMC_NO_INITIAL_STATES);
767  t5 = util_cpu_ctime();
768  pm->tExp += t5-t3;
769  if(pm->verbosity>=2)
770    fprintf(vis_stdout,"Expansion time:%g,total:%g\n",
771            (double)((t5-t3)/1000.0),pm->tExp/1000);
772  manager->class_ = 3;
773  manager->test2LevelMini = 0;
774  property = PureSatCreatebAigOfPropFormula(network,
775    manager, 2, ltlFormula, BMC_NO_INITIAL_STATES);
776  property = bAig_Not(property);
777  if(property==0)
778    return TRUE;
779  if(property==1)
780    return FALSE;
781
782  if(pm->verbosity>=1)
783    fprintf(vis_stdout,"property is %ld\n",property);
784  manager->test2LevelMini = 1;
785
786
787  NumofCurrentLatch=0;
788  t3 = util_cpu_ctime();
789  PureSatBmcGetCoiForLtlFormula_New(network, ltlFormula,pm->oldCoiTable);
790  t5 = util_cpu_ctime();
791  if(pm->verbosity>=2)
792    fprintf(vis_stdout,"Compute NTK COI :%g\n",(t5-t3)/1000);
793
794  pm->CoiTable = st_copy(pm->oldCoiTable);
795
796  /*new COI computation*/
797  t3 = util_cpu_ctime();
798  tmpTable = PureSatGetAigCoi(network,pm,property);
799  st_foreach_item(tmpTable,stGen,&nodeName,NIL(char*)){
800    latch = Ntk_NetworkFindNodeByName(network,nodeName);
801#if 1
802    if(!st_lookup(pm->CoiTable,latch,NIL(char*)))
803      if(pm->verbosity>=2)
804        fprintf(vis_stdout,"%s is not in CoiTable\n",nodeName);
805#endif
806    st_insert(pm->CoiTable,latch,(char*)0);
807  }
808#if 1
809  st_foreach_item(pm->CoiTable,stGen,&latch,NIL(char*)){
810    nodeName = Ntk_NodeReadName(latch);
811    if(!st_lookup(tmpTable,nodeName,NIL(char*)))
812      if(pm->verbosity>=2)
813        fprintf(vis_stdout,"%s is not in Aig CoiTable\n",nodeName);
814  }
815#endif
816  st_free_table(tmpTable);
817  t5 = util_cpu_ctime();
818  if(pm->verbosity>=2)
819    fprintf(vis_stdout,"Compute AIG COI :%g\n",(t5-t3)/1000);
820
821
822  t3 = util_cpu_ctime();
823  pm->vertexTable = PureSatCreateInitialAbstraction(network,
824                      ltlFormula,&NumofCurrentLatch,pm);
825  t5 = util_cpu_ctime();
826  if(pm->verbosity>=2)
827    fprintf(vis_stdout,"the time to create init abs:%g\n",(t5-t3)/1000);
828  tmpTable = st_init_table(strcmp,st_strhash);
829  PureSatCreateInitAbsByAIG(manager,pm,property,tmpTable);
830  st_foreach_item(tmpTable,stGen,&nodeName,NIL(char*)){
831    if(!st_lookup(pm->vertexTable,nodeName,NIL(char*))){
832      st_insert(pm->vertexTable,nodeName,(char*)0);
833      if(pm->verbosity>=1)
834        fprintf(vis_stdout,"insert %s into init abs model\n",nodeName);
835    }
836  }
837  st_free_table(tmpTable);
838  t3 = util_cpu_ctime();
839  if(pm->verbosity>=2)
840    fprintf(vis_stdout,"the time to create init AIG abs:%g\n",(t3-t5)/1000);
841
842  PureSatPreProcLatch(network,pm);
843  t5 = util_cpu_ctime();
844  if(pm->verbosity>=2)
845    fprintf(vis_stdout,"the time to preproc:%g\n",(t5-t3)/1000);
846
847  /*put indentical latches of visible latch into abs*/
848  t3 = util_cpu_ctime();
849  PureSatGetIndenticalLatch(network,pm);
850  st_foreach_item(pm->vertexTable,stGen,&nodeName,NIL(char*))
851    array_insert_last(char*,visibleArray,nodeName);
852  PureSatAddIdenLatchToAbs(network,pm,visibleArray);
853  arrayForEachItem(char*,visibleArray,i,nodeName)
854    st_insert(pm->vertexTable,nodeName,(char*)0);
855  array_free(visibleArray);
856  visibleArray = array_alloc(char*,0);
857  t5 = util_cpu_ctime();
858  if(pm->verbosity>=2)
859    fprintf(vis_stdout,"Merge identical latch:%g\n",(t5-t3)/1000);
860
861  NumofCurrentLatch = st_count(pm->vertexTable);
862
863  t3 = util_cpu_ctime();
864  pm->AbsTable = st_init_table(st_ptrcmp,st_ptrhash);
865
866  Ntk_NetworkForEachLatch(network, gen, node){
867    if (st_lookup_int(pm->CoiTable, (char *) node, &tmp)){
868      NumofLatch++;
869      nodeName = Ntk_NodeReadName(node);
870      if(st_lookup(pm->vertexTable,nodeName,NIL(char *)))
871        {
872          array_insert_last(char *,visibleArray,nodeName);
873          latch = Ntk_NetworkFindNodeByName(network,nodeName);
874          PureSatComputeTableForLatch(network,pm->AbsTable,latch);
875        }
876      else
877        array_insert_last(char *,invisibleArray,nodeName);
878    }
879  }
880  t5 = util_cpu_ctime();
881  if(pm->verbosity>=2)
882    fprintf(vis_stdout,"the time to cmpute abs table:%g\n",(t5-t3)/1000);
883  if(pm->verbosity>=1){
884    fprintf(vis_stdout,"visiblearray has %d latches\n",array_n(visibleArray));
885    fprintf(vis_stdout,"invisibleArray has %d latches\n",array_n(invisibleArray));
886  }
887  CoiArray = array_dup(visibleArray);
888  array_append(CoiArray,invisibleArray);
889
890  pm->nicTable = st_init_table(strcmp,st_strhash);
891  pm->niaTable = st_init_table(strcmp,st_strhash);
892  PureSatComputeNumGatesInCone(network,pm,CoiArray);
893  t3 = util_cpu_ctime();
894  if(pm->verbosity>=2)
895    fprintf(vis_stdout,"the time to cmpute gates in cone:%g\n",(t3-t5)/1000);
896
897  /*Using DFS + Dir Cone in abs*/
898  pm->node2dfsTable = st_init_table(st_ptrcmp,st_ptrhash);
899
900
901  while(NumofCurrentLatch < NumofLatch)
902    {
903      t3 = util_cpu_ctime();
904      if(pm->verbosity>=1)
905        fprintf(vis_stdout,"Current Latches: %d, COI latches:%d,NEW Length:%d,\n",
906                NumofCurrentLatch,NumofLatch,pm->Length);
907      if(pm->verbosity>=2)
908        fprintf(vis_stdout,"General time: %g\n",(double)((t3-t0)/1000.0));
909      t1 = util_cpu_ctime();
910      tmpRefinement = array_alloc(char *,0);
911
912      memset(manager->ipm,0,sizeof(IP_Manager_t));
913      firstTime = TRUE;
914      pm->SufAbsTable = st_init_table(st_ptrcmp,st_ptrhash);
915      if(realRefine){
916        arrayForEachItem(char *,refinement,i,nodeName)
917          {
918            latch = Ntk_NetworkFindNodeByName(network,nodeName);
919            PureSatComputeTableForLatch(network,pm->AbsTable,latch);
920            st_insert(pm->vertexTable,nodeName,(char*)0);
921          }
922        array_append(visibleArray,refinement);
923        array_free(invisibleArray);
924        invisibleArray = array_alloc(char *,0);
925        st_foreach_item(pm->CoiTable,stGen,&latch,&i)
926          {
927            nodeName = Ntk_NodeReadName(latch);
928            if(!st_lookup(pm->vertexTable,nodeName,(char **)0)){
929              array_insert_last(char *,invisibleArray,nodeName);
930            }
931          }
932        st_free_table(pm->node2dfsTable);
933        pm->node2dfsTable = st_init_table(st_ptrcmp,st_ptrhash);
934        arrayRC = PureSatComputeOrder_2(network,pm,visibleArray,invisibleArray,sccArray,&NumInSecondLevel);
935        t4 = util_cpu_ctime();
936        if(pm->verbosity>=2)
937          fprintf(vis_stdout,"time for compute order: %g\n",(t4-t1)/1000);
938
939        if(pm->RefPredict){
940          orderCt=0;
941          if(array_n(pm->latchArray)>0){
942            if(pm->verbosity>=1)
943              fprintf(vis_stdout,"\n%d: Adding high RC value latch into abs model\n",orderCt++);
944            PureSatAddIdenLatchToAbs(network,pm,pm->latchArray);
945            NumofCurrentLatch+=array_n(pm->latchArray);
946            arrayForEachItem(char *,pm->latchArray,i,nodeName){
947              latch = Ntk_NetworkFindNodeByName(network,nodeName);
948              PureSatComputeTableForLatch(network,pm->AbsTable,latch);
949              st_insert(pm->vertexTable,nodeName,(char*)0);
950            }
951            array_append(visibleArray,pm->latchArray);
952            array_free(pm->latchArray);
953            array_free(invisibleArray);
954            invisibleArray = array_alloc(char *,0);
955            st_foreach_item(pm->CoiTable,stGen,&latch,&i)
956              {
957                nodeName = Ntk_NodeReadName(latch);
958                if(!st_lookup(pm->vertexTable,nodeName,(char **)0)){
959                  array_insert_last(char *,invisibleArray,nodeName);
960                }
961              }
962            st_free_table(pm->node2dfsTable);
963            pm->node2dfsTable = st_init_table(st_ptrcmp,st_ptrhash);
964            arrayRC = PureSatComputeOrder_2(network,pm,visibleArray,invisibleArray,sccArray,&NumInSecondLevel);
965
966          }
967          array_free(pm->latchArray);
968        }
969
970        PureSat_CleanMask(manager,ResetVisibleVarMask);
971        PuresatMarkVisibleVar(network,visibleArray,pm,0,pm->Length);
972
973        addtoAbs =(int)((double)(array_n(CoiArray)-array_n(visibleArray))/(double)5)+1;
974        addtoAbs = addtoAbs >50 ? 50: addtoAbs;
975
976        array_free(invisibleArray);
977        invisibleArray = array_alloc(char *,0);
978        st_foreach_item(pm->CoiTable,stGen,&latch,&i)
979          {
980            nodeName = Ntk_NodeReadName(latch);
981            if(!st_lookup(pm->vertexTable,nodeName,(char **)0)){
982              array_insert_last(char *,invisibleArray,nodeName);
983            }
984          }
985        if(pm->verbosity>=1){
986          fprintf(vis_stdout,"After adding high RC latches:\n");
987          fprintf(vis_stdout,"visiblearray has %d latches\n",array_n(visibleArray));
988          fprintf(vis_stdout,"invisibleArray has %d latches\n",array_n(invisibleArray));
989        }
990        t4 = util_cpu_ctime();
991        t4total += t4-t3;
992        if(pm->verbosity>=2)
993          fprintf(vis_stdout,"compute and add high RC latch and recompute order:%g,total:%g\n",
994                 (t4-t3)/1000,(t4total/1000.0));
995
996        if(pm->verbosity>=1)
997          fprintf(vis_stdout,"NumInSecondLevel is %d  ",NumInSecondLevel);
998        latchThreshHold = NumInSecondLevel;
999        if(pm->verbosity>=2){
1000          fprintf(vis_stdout,"New latchThreshHold is %d\n",latchThreshHold);
1001        }
1002        t2 = util_cpu_ctime();
1003        if(pm->verbosity>=2){
1004          fprintf(vis_stdout,"Recompute Order: %g\n",(double)((t2-t1)/1000.0));
1005        }
1006        array_free(refinement);
1007        refinement = array_alloc(char *,0);
1008     }/* if(realRefine)*/
1009
1010     /* means no ref, just Length++.*/
1011      realRefine =FALSE;
1012      t1 = util_cpu_ctime();
1013
1014      ExistACE = PureSat_CheckAceByIP(network,pm,pism1, visibleArray,&Length,
1015                              ltlFormula, &property,previousResultArray);
1016      if(ExistACE)
1017        {
1018          if(pm->returnVal == -1){
1019             PureSatIncreSATManagerFree(pm,pism1);
1020             /*PureSatManagerFree(pm);*/
1021             array_free(CoiArray);
1022             BmcOptionFree(options);
1023             return FALSE;
1024          }
1025          pm->Length = Length;
1026          pism1->Length = Length;
1027          t2 = util_cpu_ctime();
1028          pm->tIP += t2-t1;
1029          if(pm->verbosity>=2)
1030            fprintf(vis_stdout,"Solve on IP: %g, total: %g\n",
1031                   (double)((t2-t1)/1000.0),(double)pm->tIP/1000.0);
1032
1033
1034          if(ExistACE)
1035            {
1036              int Con=0;
1037              if(pm->verbosity>=1)
1038                fprintf(vis_stdout,"found Abstract Counterexample at length %d\n", pm->Length);
1039              realRefine = TRUE;
1040
1041              /*incrementally check Concrete Model*/
1042              if(pm->verbosity>=1)
1043                fprintf(vis_stdout,"Begin building a new abstract model\n");
1044              for(i=0;i<array_n(arrayRC);i=i+latchThreshHold)
1045                {
1046                  Con = 0;
1047                  if(i>0)
1048                    latchThreshHold = array_n(arrayRC)-latchThreshHold;
1049                  for(j=0;j<latchThreshHold;j++)
1050                    {
1051                      if((i+j)<array_n(arrayRC))
1052                        {
1053                          nodeName = array_fetch(char *,arrayRC,i+j);
1054                          array_insert_last(char *,tmpRefinement,nodeName);
1055                          if(pm->verbosity>=2)
1056                            if(pm->verbosity>=2)
1057                              fprintf(vis_stdout, "picking %s\n",nodeName);
1058                          if((i+j)==(array_n(arrayRC)-1))
1059                            Con = 1;
1060                        }
1061                      else{
1062                        Con = 1;
1063                        break;
1064                      }
1065                    }/* for(j=0;*/
1066                  tmpRefinement1=array_dup(visibleArray);
1067                  array_append(tmpRefinement1,tmpRefinement);
1068
1069                  t1 = util_cpu_ctime();
1070
1071                  if(pm->verbosity>=2)
1072                    satStat = 1;
1073                  if(!PureSat_ConcretTest(network,pm,tmpRefinement1,property,previousResultArray,Con,satStat,1)){
1074
1075                    t2 = util_cpu_ctime();
1076                    pm->tCon = pm->tCon+t2-t1;
1077                    if(pm->verbosity>=2)
1078                      fprintf(vis_stdout,"time for finding a sufficient set on model: %g, total:%g\n",
1079                             (double)((t2-t1)/1000.0),(double)pm->tCon/1000.0);
1080                    if((i+j)>=array_n(arrayRC)){
1081                      fprintf(vis_stdout,"found real counterexamples\n");
1082
1083                      PureSatIncreSATManagerFree(pm, pism1);
1084                      /*PureSatManagerFree(pm);*/
1085                      array_free(CoiArray);
1086                      BmcOptionFree(options);
1087                      return FALSE;
1088                    }
1089                    /* else{
1090                      ;
1091                      }*/
1092                  }
1093                  else{
1094                    t2 = util_cpu_ctime();
1095                    pm->tCon = pm->tCon+t2-t1;
1096                    if(pm->verbosity>=1)
1097                      fprintf(vis_stdout,"found a sufficient model\n");
1098                    if(pm->verbosity>=2)
1099                      fprintf(vis_stdout,"time for finding a sufficient set on model: %g, total:%g\n",
1100                             (double)((t2-t1)/1000.0),(double)pm->tCon/1000.0);
1101                    firstTime = FALSE;
1102                    arrayForEachItem(char *,tmpRefinement1,k,nodeName){
1103                      node = Ntk_NetworkFindNodeByName(network, nodeName);
1104                      if(!st_lookup(pm->SufAbsTable,(char *)node,NIL(char *)))
1105                        st_insert(pm->SufAbsTable,(char *)node, (char *)0);
1106                      else{
1107                        fprintf(vis_stdout,"wrong in sufabstable \n");
1108                        exit(0);
1109                      }
1110                    }
1111                    array_free(tmpRefinement1);
1112                    break;
1113                  }
1114                  array_free(tmpRefinement1);
1115                }
1116
1117              t1 = util_cpu_ctime();
1118
1119#if 1
1120              if(pm->savedConCls){
1121                sat_ArrayFree(pm->savedConCls);
1122                pm->savedConCls = 0;
1123              }
1124#endif
1125#if SWITCH_DA
1126              refinement = PureSat_RefineOnAbs_DA(network,pm,property,previousResultArray,
1127                                                  latchThreshHold,sccArray,tmpRefinement);
1128#else
1129              refinement = PureSat_RefineOnAbs(network,pm,property,previousResultArray,
1130                                               latchThreshHold,sccArray,tmpRefinement);
1131#endif
1132              array_free(tmpRefinement);
1133              t2 = util_cpu_ctime();
1134              pm->tRef = pm->tRef+t2-t1;
1135              if(pm->verbosity>=2)
1136                fprintf(vis_stdout,"time for RefOnAbs: %g, total:%g\n",
1137                       (t2-t1)/1000.0,pm->tRef/1000);
1138              st_free_table(pm->SufAbsTable);
1139              pm->SufAbsTable = 0;
1140
1141              /*adjust parameters*/
1142              NumofCurrentLatch+=array_n(refinement);
1143              pm->Length++;
1144              pism1->Length++;
1145              Length++;
1146            }/* if(pism2->cm->status == SAT_SAT)*/
1147        } /*if(ExistACE)*/
1148      else /* if TRUE from IP*/
1149        {
1150          t2 = util_cpu_ctime();
1151          pm->tIP = pm->tIP+t2-t1;
1152          if(pm->verbosity>=2)
1153            fprintf(vis_stdout,"Solve on IP: %g, total: %g\n",
1154                   (t2-t1)/1000.0,pm->tIP/1000.0);
1155          fprintf(vis_stdout,"Convergence reached, exit\n");
1156          PureSatIncreSATManagerFree(pm,pism1);
1157          /*PureSatManagerFree(pm);*/
1158          array_free(CoiArray);
1159          BmcOptionFree(options);
1160          return TRUE;
1161        }
1162    }/* while(NumofCurrentLatch < NumofLatch)*/
1163  /*st_free_table(AbsTable);*/
1164
1165  /*Now go to the concrete model*/
1166  if(pm->verbosity>=1)
1167    fprintf(vis_stdout,"reach concrete model\n");
1168  array_append(visibleArray,refinement);
1169  array_free(refinement);
1170
1171
1172  ExistACE = PureSatIPOnCon(network,ltlFormula,pm);
1173  ExistACE = !ExistACE;
1174  PureSatIncreSATManagerFree(pm,pism1);
1175  /*PureSatManagerFree(pm);*/
1176  array_free(CoiArray);
1177  BmcOptionFree(options);
1178  if(ExistACE)
1179    return FALSE;
1180  else
1181    return TRUE;
1182}
Note: See TracBrowser for help on using the repository browser.