source: vis_dev/vis-2.3/src/puresat/puresatIPUtil.c @ 38

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

vis2.3
File size: 95.6 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [puresatIPUtil.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
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    []
94
95  Description []
96
97  SideEffects []
98
99  SeeAlso     []
100
101******************************************************************************/
102
103/**Function********************************************************************
104
105  Synopsis    [Comparison function for sorting]
106
107  Description [Comparison function for sorting]
108
109  SideEffects []
110
111  SeeAlso     []
112
113******************************************************************************/
114
115static int
116NodeIndexCompare(const void *x, const void *y)
117{
118int n1, n2;
119
120  n1 = *(int *)x;
121  n2 = *(int *)y;
122  return(n1 > n2);
123}
124
125/**Function********************************************************************
126
127  Synopsis    []
128
129  Description []
130
131  SideEffects []
132
133  SeeAlso     []
134
135******************************************************************************/
136
137static int
138StringCheckIsInteger(
139  char *string,
140  int *value)
141{
142  char *ptr;
143  long l;
144
145  l = strtol (string, &ptr, 0) ;
146  if(*ptr != '\0')
147    return 0;
148  if ((l > MAXINT) || (l < -1 - MAXINT))
149    return 1 ;
150  *value = (int) l;
151  return 2 ;
152}
153
154
155/**AutomaticEnd***************************************************************/
156
157/*---------------------------------------------------------------------------*/
158/* Definition of exported functions                                          */
159/*---------------------------------------------------------------------------*/
160/**Function********************************************************************
161
162  Synopsis    [Create a node for resolution tree]
163
164  Description [Create a node for resolution tree]
165
166  SideEffects []
167
168  SeeAlso     []
169
170******************************************************************************/
171
172
173RTnode_t RTCreateNode(RTManager_t * rm)
174{
175  RTnode_t node;
176
177  if(rm->nArray==0){
178    rm->nArray = ALLOC(long, RTnodeSize*RT_BLOCK);
179    rm->maxSize = RTnodeSize*RT_BLOCK;
180    rm->aSize = 0;
181  }
182
183  if(rm->maxSize<=rm->aSize+RTnodeSize){
184    rm->nArray = REALLOC(long, rm->nArray,rm->maxSize+RTnodeSize*RT_BLOCK);
185    if(rm->nArray == 0){
186      fprintf(vis_stdout,"memout when alloc %ld bytes\n",
187             (rm->maxSize+RTnodeSize*RT_BLOCK)*4);
188      exit(0);
189    }
190    rm->maxSize = rm->maxSize+RTnodeSize*1000;
191  }
192  rm->aSize += RTnodeSize;
193  node = rm->aSize;
194
195  RT_fSize(node) = 0;
196  RT_formula(node) = 0;
197  RT_oriClsIdx(node) = 0;
198  RT_pivot(node) = 0;
199  RT_flag(node) = 0;
200  RT_IPnode(node) = -1;
201  RT_left(node) = 0;
202  RT_right(node) = 0;
203
204  if(rm->fArray==0){
205    rm->fArray = ALLOC(long,FORMULA_BLOCK);
206
207    rm->cpos = 0;
208    rm->maxpos = FORMULA_BLOCK;
209  }
210
211  return node;
212}
213
214/**Function********************************************************************
215
216  Synopsis    [Allocate an interpolation manager]
217
218  Description [Allocate an interpolation manager]
219
220  SideEffects []
221
222  SeeAlso     []
223
224******************************************************************************/
225
226
227IP_Manager_t * IPManagerAlloc()
228{
229  IP_Manager_t * ipm = ALLOC(IP_Manager_t, 1);
230  memset(ipm,0,sizeof(IP_Manager_t));
231  return ipm;
232}
233
234
235/**Function********************************************************************
236
237  Synopsis    [Free an interpolation manager]
238
239  Description [Free an interpolation manager]
240
241  SideEffects []
242
243  SeeAlso     []
244
245******************************************************************************/
246
247
248void IPManagerFree(IP_Manager_t *ipm)
249{
250  FREE(ipm);
251}
252
253/**Function********************************************************************
254
255  Synopsis    [Find the type of conflict, return the value to caller]
256
257  Description [
258
259
260           0       1       1       1       1      1
261           |       |       |       |       |      |
262        20---33,49--- 9,13---  17 ---  5  ---   1---
263          / \     / \     / \     / \     / \    / \
264         1   1   X   0   0   X   1   0   0   1  0   0
265
266   Bing note: For case 1, maybe solving conflict with both childern is
267   better, but in sat package, only conflict with left child is solved ]
268
269  SideEffects []
270
271  SeeAlso     []
272
273******************************************************************************/
274
275
276
277int PureSat_IdentifyConflict(
278  satManager_t *cm,
279  long left,
280  bAigEdge_t right,
281  bAigEdge_t node)
282{
283  int result; /*1:left 2:right 3:both*/
284  int value = SATgetValue(left,right,node);
285  switch(value){
286  case 1:
287  case 5:
288  case 9:
289  case 13:
290    result = 1;
291    break;
292  case 17:
293  case 33:
294  case 49:
295    result = 2;
296    break;
297  case 20:
298    result = 3;
299    break;
300  default:
301    fprintf(vis_stdout,"can't identify the conflict, exit\n");
302    exit(0);
303  }
304
305  return result;
306}
307
308/**Function********************************************************************
309
310  Synopsis    [Get COI for a network node]
311
312  Description [Get COI for a network node]
313
314  SideEffects []
315
316  SeeAlso     []
317
318******************************************************************************/
319
320
321void
322PureSatBmcGetCoiForNtkNode_New(
323  Ntk_Node_t  *node,
324  st_table    *CoiTable,
325  st_table    *visited)
326{
327  int        i;
328  Ntk_Node_t *faninNode;
329
330  if(node == NIL(Ntk_Node_t)){
331    return;
332  }
333
334
335  if (st_lookup_int(visited, (char *) node, NIL(int))){
336    return;
337  }
338  st_insert(visited, (char *) node, (char *) 0);
339
340  if(Ntk_NodeTestIsInput(node))
341    return;
342
343  if (Ntk_NodeTestIsLatch(node)){
344    st_insert(CoiTable, (char *) node, (char *)0);
345  }
346
347  Ntk_NodeForEachFanin(node, i, faninNode) {
348    PureSatBmcGetCoiForNtkNode_New(faninNode, CoiTable, visited);
349  }
350
351  return;
352}
353
354/**Function********************************************************************
355
356  Synopsis    [Recursively get COI nodes for a LTL formula]
357
358  Description [Recursively get COI nodes for a LTL formula]
359
360  SideEffects []
361
362  SeeAlso     []
363
364******************************************************************************/
365
366void
367PureSatBmcGetCoiForLtlFormulaRecursive_New(
368  Ntk_Network_t   *network,
369  Ctlsp_Formula_t *formula,
370  st_table        *ltlCoiTable,
371  st_table        *visited)
372{
373  if (formula == NIL(Ctlsp_Formula_t)) {
374    return;
375  }
376  /* leaf node */
377  if (formula->type == Ctlsp_ID_c){
378    char       *name = Ctlsp_FormulaReadVariableName(formula);
379    Ntk_Node_t *node = Ntk_NetworkFindNodeByName(network, name);
380    int        tmp;
381
382    if (st_lookup_int(visited, (char *) node, &tmp)){
383      /* Node already visited */
384      return;
385    }
386    PureSatBmcGetCoiForNtkNode_New(node, ltlCoiTable, visited);
387    return;
388  }
389  PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula->left,  ltlCoiTable, visited);
390  PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula->right, ltlCoiTable, visited);
391
392  return;
393}
394
395/**Function********************************************************************
396
397  Synopsis    [Get COI nodes for a LTL formula]
398
399  Description [Get COI nodes for a LTL formula]
400
401  SideEffects []
402
403  SeeAlso     []
404
405******************************************************************************/
406
407void
408PureSatBmcGetCoiForLtlFormula_New(
409  Ntk_Network_t   *network,
410  Ctlsp_Formula_t *formula,
411  st_table        *ltlCoiTable)
412{
413  st_table *visited = st_init_table(st_ptrcmp, st_ptrhash);
414
415  PureSatBmcGetCoiForLtlFormulaRecursive_New(network, formula, ltlCoiTable, visited);
416  st_free_table(visited);
417  return;
418} /* BmcGetCoiForLtlFormula() */
419
420
421/**Function********************************************************************
422
423  Synopsis    [Mark transitive fanin for an aig node]
424
425  Description [Mark transitive fanin for an aig node]
426
427  SideEffects []
428
429  SeeAlso     []
430
431******************************************************************************/
432
433
434void PureSat_MarkTransitiveFaninForNode(
435        satManager_t *cm,
436        bAigEdge_t v,
437        unsigned int mask)
438{
439  if(v == bAig_NULL)    return;
440
441  v = SATnormalNode(v);
442
443  if(SATflags(v) & mask)        return;
444
445  SATflags(v) |= mask;
446  if(SATflags(v) & Visited3Mask) return;
447
448  PureSat_MarkTransitiveFaninForNode(cm, SATleftChild(v), mask);
449  PureSat_MarkTransitiveFaninForNode(cm, SATrightChild(v), mask);
450}
451
452/**Function********************************************************************
453
454  Synopsis    [Mark transitive fanin for an array of aig nodes]
455
456  Description [Mark transitive fanin for an array of aig nodes]
457
458  SideEffects []
459
460  SeeAlso     []
461
462******************************************************************************/
463
464
465void PureSat_MarkTransitiveFaninForArray(
466        satManager_t *cm,
467        satArray_t *arr,
468        unsigned int mask)
469{
470  int  i, size;
471  bAigEdge_t v;
472
473  if(arr == 0)  return;
474  size = arr->num;
475
476  for(i=0; i<size; i++) {
477    v = arr->space[i];
478    PureSat_MarkTransitiveFaninForNode(cm, v, mask);
479  }
480}
481
482/**Function********************************************************************
483
484  Synopsis    [Mark transitive fanin for an aig node]
485
486  Description [Mark transitive fanin for an aig node]
487
488  SideEffects []
489
490  SeeAlso     []
491
492******************************************************************************/
493
494void PureSat_MarkTransitiveFaninForNode2(
495        mAig_Manager_t *manager,
496        bAigEdge_t v,
497        unsigned int mask)
498{
499  if(v == bAig_NULL)    return;
500
501  v = SATnormalNode(v);
502
503  if(flags(v) & mask)   return;
504
505  flags(v) |= mask;
506  if(flags(v) & Visited3Mask) return;
507
508  PureSat_MarkTransitiveFaninForNode2(manager, leftChild(v), mask);
509  PureSat_MarkTransitiveFaninForNode2(manager, rightChild(v), mask);
510}
511
512/**Function********************************************************************
513
514  Synopsis    [Mark transitive fanin for an array of aig nodes]
515
516  Description [Mark transitive fanin for an array of aig nodes]
517
518  SideEffects []
519
520  SeeAlso     []
521
522******************************************************************************/
523
524
525void PureSat_MarkTransitiveFaninForArray2(
526        mAig_Manager_t *manager,
527        satArray_t *arr,
528        unsigned int mask)
529{
530bAigEdge_t v;
531int i, size;
532
533  if(arr == 0)  return;
534  size = arr->num;
535
536  for(i=0; i<size; i++) {
537    v = arr->space[i];
538    PureSat_MarkTransitiveFaninForNode2(manager, v, mask);
539  }
540}
541
542/**Function********************************************************************
543
544  Synopsis    [Mark transitive fanin for an array of aig nodes]
545
546  Description [Mark transitive fanin for an array of aig nodes]
547
548  SideEffects []
549
550  SeeAlso     []
551
552******************************************************************************/
553
554
555
556void PureSat_MarkTransitiveFaninForNode3(
557        mAig_Manager_t *manager,
558        bAigEdge_t v,
559        unsigned int mask)
560{
561  if(v == 2)    return;
562
563  v = SATnormalNode(v);
564
565  if(flags(v) & mask)   return;
566
567  flags(v) |= mask;
568
569  PureSat_MarkTransitiveFaninForNode3(manager, leftChild(v), mask);
570  PureSat_MarkTransitiveFaninForNode3(manager, rightChild(v), mask);
571}
572
573/**Function********************************************************************
574
575  Synopsis    [Mark transitive fanin for an array of aig nodes]
576
577  Description [Mark transitive fanin for an array of aig nodes]
578
579  SideEffects []
580
581  SeeAlso     []
582
583******************************************************************************/
584
585void PureSat_MarkTransitiveFaninForArray3(
586        mAig_Manager_t *manager,
587        satArray_t *arr,
588        unsigned int mask)
589{
590bAigEdge_t v;
591int i, size;
592
593  if(arr == 0)  return;
594  size = arr->num;
595
596  for(i=0; i<size; i++) {
597    v = arr->space[i];
598    PureSat_MarkTransitiveFaninForNode3(manager, v, mask);
599  }
600}
601
602
603/**Function********************************************************************
604
605  Synopsis    [Mark transitive fanin for an array of aig nodes]
606
607  Description [Mark transitive fanin for an array of aig nodes]
608
609  SideEffects []
610
611  SeeAlso     []
612
613******************************************************************************/
614
615
616void PureSat_MarkTransitiveFaninForNode4(
617        mAig_Manager_t *manager,
618        bAigEdge_t v,
619        unsigned int mask,
620        int bound)
621{
622  if(v == bAig_NULL)    return;
623
624  v = SATnormalNode(v);
625
626  if(flags(v) & mask)   return;
627
628  flags(v) |= mask;
629
630  if((flags(v)&StateBitMask)&&
631     !(flags(v)&VisibleVarMask)&&
632     (bAig_Class(v)>0)){
633
634    return;
635  }
636
637  PureSat_MarkTransitiveFaninForNode4(manager, leftChild(v), mask,bound);
638  PureSat_MarkTransitiveFaninForNode4(manager, rightChild(v), mask,bound);
639}
640
641/**Function********************************************************************
642
643  Synopsis    [Mark transitive fanin for an array of aig nodes]
644
645  Description [Mark transitive fanin for an array of aig nodes]
646
647  SideEffects []
648
649  SeeAlso     []
650
651******************************************************************************/
652
653void PureSat_MarkTransitiveFaninForArray4(
654        mAig_Manager_t *manager,
655        satArray_t *arr,
656        unsigned int mask,
657        int bound)
658{
659bAigEdge_t v;
660int i, size;
661
662  if(arr == 0)  return;
663  size = arr->num;
664
665  for(i=0; i<size; i++) {
666    v = arr->space[i];
667
668    v = SATnormalNode(v);
669    PureSat_MarkTransitiveFaninForNode4(manager,v,mask,bound);
670
671  }
672}
673
674/**Function********************************************************************
675
676  Synopsis    [clean a certain mask for all the aig nodes]
677
678  Description [clean a certain mask for all the aig nodes]
679
680  SideEffects []
681
682  SeeAlso     []
683
684******************************************************************************/
685
686
687
688void PureSat_CleanMask(mAig_Manager_t *manager,
689                       unsigned int mask)
690{
691  bAigEdge_t i;
692
693  for(i=bAigNodeSize; i<manager->nodesArraySize;i+=bAigNodeSize)
694    flags(i)&=mask;
695
696}
697
698/**Function********************************************************************
699
700  Synopsis    [Set COI mask for SAT solver]
701
702  Description [Set COI mask for SAT solver]
703
704  SideEffects []
705
706  SeeAlso     []
707
708******************************************************************************/
709
710
711void PureSat_SetCOI(satManager_t *cm)
712{
713
714  PureSat_MarkTransitiveFaninForArray(cm, cm->auxObj, CoiMask);
715  PureSat_MarkTransitiveFaninForArray(cm, cm->obj, CoiMask);
716  PureSat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
717
718}
719
720
721/**Function********************************************************************
722
723  Synopsis    [Reset COI mask for all nodes]
724
725  Description [Reset COI mask for all nodes]
726
727  SideEffects []
728
729  SeeAlso     []
730
731******************************************************************************/
732
733void PureSat_ResetCoi(satManager_t *cm)
734{
735  bAigEdge_t i;
736  for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
737    if(SATflags(i) & CoiMask)
738      SATflags(i) &= ResetCoiMask;
739  }
740}
741
742/**Function********************************************************************
743
744  Synopsis    [Set COI for latch nodes]
745
746  Description [Set COI for latch nodes]
747
748  SideEffects []
749
750  SeeAlso     []
751
752******************************************************************************/
753
754void PureSatSetLatchCOI(Ntk_Network_t * network,
755                        PureSat_Manager_t *pm,
756                        satManager_t * cm,
757                        /*deletable*/
758                        st_table * AbsTable,
759                        int from,
760                        int to)
761{
762
763  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
764
765  bAigTimeFrame_t *tf = manager->timeframeWOI;
766  int i,j;
767  bAigEdge_t *L0,*L1,*bL0,*bL1;
768  satArray_t * assert;
769  int nLatches = tf->nLatches, nbLatches = tf->nbLatches;
770
771  if(from>=to) return;
772
773  PureSat_ResetCoi(cm);
774
775  assert = sat_ArrayAlloc(1);
776  sat_ArrayInsert(assert,manager->InitState);
777  PureSat_MarkTransitiveFaninForArray3(manager,assert,CoiMask);
778  sat_ArrayFree(assert);
779
780  for(i=from; i<to; i++){
781    assert = sat_ArrayAlloc(1);
782
783    L0 = tf->latchInputs[i];
784    L1 = tf->latchInputs[i+1];
785    bL0 = tf->blatchInputs[i];
786    bL1 = tf->blatchInputs[i+1];
787
788    for(j=0;j<nLatches;j++){
789      if(L1[j]!=bAig_One&&L1[j]!=bAig_Zero){
790        if(flags(L1[j])&VisibleVarMask)
791          sat_ArrayInsert(assert,L1[j]);
792      }
793      if(L0[j]!=bAig_One&&L0[j]!=bAig_Zero&&
794         !(flags(L0[j])&VisibleVarMask))
795        flags(L0[j]) |= Visited3Mask;
796    }
797
798    for(j=0;j<nbLatches;j++){
799      if(bL1[j]!=bAig_One&&bL1[j]!=bAig_Zero){
800        if(flags(bL1[j])&VisibleVarMask)
801          sat_ArrayInsert(assert,bL1[j]);
802      }
803      if(bL0[j]!=bAig_One&&bL0[j]!=bAig_Zero&&
804         !(flags(bL0[j])&VisibleVarMask))
805        flags(bL0[j]) |= Visited3Mask;
806    }
807
808    PureSat_MarkTransitiveFaninForArray2(manager,assert,CoiMask);
809    sat_ArrayFree(assert);
810  }
811
812}
813
814/**Function********************************************************************
815
816  Synopsis    [Set COI for latch nodes]
817
818  Description [Set COI for latch nodes]
819
820  SideEffects []
821
822  SeeAlso     []
823
824******************************************************************************/
825
826
827void PureSatSetLatchCOI2(Ntk_Network_t * network,
828                         PureSat_Manager_t *pm,
829                         satManager_t * cm,
830                         bAigEdge_t obj,
831                         int bound)
832{
833
834  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
835  satArray_t * assert;
836
837  PureSat_ResetCoi(cm);
838
839  assert = sat_ArrayAlloc(1);
840  sat_ArrayInsert(assert,obj);
841  PureSat_MarkTransitiveFaninForArray4(manager,assert,CoiMask,bound);
842  PureSat_MarkTransitiveFaninForArray4(manager,cm->assertArray,CoiMask,bound);
843  sat_ArrayFree(assert);
844
845}
846
847/**Function********************************************************************
848
849  Synopsis    [Set COI for form the SAT problem]
850
851  Description [Set COI for form the SAT problem]
852
853  SideEffects []
854
855  SeeAlso     []
856
857******************************************************************************/
858
859void PureSatSetCOI(Ntk_Network_t * network,
860                   PureSat_Manager_t *pm,
861                   satManager_t * cm,
862                   st_table * AbsTable,
863                   int from,
864                   int to,
865                   int bound)
866{
867  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
868  bAigEdge_t property;
869
870  if(cm->obj->num>0){
871    property = cm->obj->space[0];
872    PureSatSetLatchCOI2(network,pm,cm,property,bound);
873  }
874  else{
875    PureSatSetLatchCOI(network,pm,cm,AbsTable,from,to);
876    PureSat_CleanMask(manager,ResetVisited3Mask);
877  }
878
879
880}
881
882/**Function********************************************************************
883
884  Synopsis    [Build abstraction from concrete model]
885
886  Description [Build abstraction from concrete model]
887
888  SideEffects []
889
890  SeeAlso     []
891
892******************************************************************************/
893
894void PureSatAbstractLatch(bAig_Manager_t *manager,
895                          bAigEdge_t v,
896                          st_table * tmpTable)
897{
898  bAigEdge_t nv;
899
900  /*fanin: set left and right to bAig_NULL*/
901  nv = bAig_NonInvertedEdge(v);
902
903  if(leftChild(nv)!=bAig_NULL){
904    if(!(flags(leftChild(nv))&CoiMask))
905      flags(leftChild(nv)) |= Visited3Mask;
906    manager->NodesArray[nv+bAigLeft]=bAig_NULL;
907  }
908
909  if(rightChild(nv)!=bAig_NULL){
910    if(!(flags(rightChild(nv))&CoiMask))
911      flags(rightChild(nv)) |= Visited3Mask;
912    manager->NodesArray[nv+bAigRight]=bAig_NULL;
913  }
914
915}
916
917/**Function********************************************************************
918
919  Synopsis    [Kill all pseudo global variables for one node for interpolation computation]
920
921  Description [Kill all pseudo global variables for one node for interpolation computation]
922
923  SideEffects []
924
925  SeeAlso     []
926
927******************************************************************************/
928
929void PureSatKillPseudoGVNode(bAig_Manager_t *manager,
930                             bAigEdge_t v,
931                             st_table * tmpTable)
932{
933  long size = nFanout(v),i,inv=0;
934  bAigEdge_t v1,v2,nv;
935  bAigEdge_t  * fan = (bAigEdge_t *)fanout(v),left;
936
937  /*fanin: set left and right to bAig_NULL*/
938  nv = bAig_NonInvertedEdge(v);
939  flags(nv) |= PGVMask;
940
941  if(leftChild(nv)!=bAig_NULL){
942    if(!(flags(leftChild(nv))&CoiMask))
943      flags(leftChild(nv)) |= Visited3Mask;
944    manager->NodesArray[nv+bAigLeft]=bAig_NULL;
945  }
946
947  if(rightChild(nv)!=bAig_NULL){
948    if(!(flags(rightChild(nv))&CoiMask))
949      flags(rightChild(nv)) |= Visited3Mask;
950    manager->NodesArray[nv+bAigRight]=bAig_NULL;
951  }
952
953
954  manager->class_ = 2;
955
956  /*fanout: connection to vars in next tf is disconnected, and a new pseudo var
957    is created, and used as a replacement*/
958  for(i=0;i<size;i++){
959    v1 = bAig_NonInvertedEdge(fan[i]>>1);
960    if(!(flags(v1)&CoiMask))
961      continue;
962    if(bAig_Class(v1)>1){
963      /*igonre invSV since its left and right will be processed to 2*/
964      if(!(flags(v1)&VisibleVarMask)&&(flags(v1)&StateBitMask))
965        continue;
966      /*if nonSV, create new Node as replacement*/
967      if(!st_lookup(tmpTable,(char*)nv,&v2)){
968        v2 = bAig_CreateNode(manager,bAig_NULL, bAig_NULL);
969
970        flags(v2) |= DummyMask;
971        st_insert(tmpTable,(char*)nv,(char*)v2);
972      }
973
974      left = 1;
975      if(bAig_IsInverted(fan[i]))
976        left = 0;
977      inv = bAig_IsInverted(fan[i]>>1)?1:0;
978      v2 = inv ? bAig_Not(v2) : v2;
979      if(left){
980#if DBG
981        assert(manager->NodesArray[v1+bAigLeft] != v2);
982#endif
983        manager->NodesArray[v1+bAigLeft] = v2;
984        PureSat_connectOutput(manager, v2, v1,0);
985        flags(v2) |= CoiMask;
986      }
987      else{
988#if DBG
989        assert(manager->NodesArray[v1+bAigRight] != v2);
990#endif
991        manager->NodesArray[v1+bAigRight] = v2;
992        PureSat_connectOutput(manager, v2, v1,1);
993        flags(v2) |= CoiMask;
994      }
995    }
996  }
997
998}
999
1000
1001/**Function********************************************************************
1002
1003  Synopsis    [Kill all pseudo global variables for interpolation computation]
1004
1005  Description [Kill all pseudo global variables for interpolation computation]
1006
1007  SideEffects []
1008
1009  SeeAlso     []
1010
1011******************************************************************************/
1012
1013void PureSatKillPseudoGV(Ntk_Network_t * network,
1014                         PureSat_Manager_t *pm,
1015                         st_table * AbsTable,
1016                         int from,
1017                         int to)
1018{
1019  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
1020  bAigTimeFrame_t *tf = manager->timeframeWOI;
1021  array_t *bVarList,*mVarList;
1022  bAigEdge_t * li, *bli,node;
1023  int i,j;
1024  st_table * tmpTable, *DoneTable;
1025
1026
1027  pm->oldPos = manager->nodesArraySize-bAigNodeSize;
1028
1029  bVarList = mAigReadBinVarList(manager);
1030  mVarList = mAigReadMulVarList(manager);
1031
1032  if(from < 1)
1033    from = 1;
1034
1035  if(to>pm->Length)
1036    to=pm->Length;
1037
1038  li = tf->latchInputs[1];
1039  bli = tf->blatchInputs[1];
1040  for(j=0;j<tf->nLatches;j++)
1041    flags(li[j])&=ResetPGVMask;
1042  for(j=0;j<tf->nbLatches;j++)
1043    flags(bli[j])&=ResetPGVMask;
1044
1045  for(i=from;i<=to;i++){
1046    li = tf->latchInputs[i];
1047    bli = tf->blatchInputs[i];
1048    manager->class_ = i;
1049    tmpTable = st_init_table(st_numcmp,st_numhash);
1050    DoneTable = st_init_table(st_numcmp,st_numhash);
1051
1052    for(j=0; j<tf->nLatches; j++){
1053      node = bAig_NonInvertedEdge(li[j]);
1054      if(st_lookup(DoneTable,(char*)node,NIL(char*)))
1055        continue;
1056      st_insert(DoneTable,(char*)node,(char*)0);
1057      if((flags(node)&StateBitMask)&&
1058         !(flags(node)&VisibleVarMask)&&
1059         (flags(node)&CoiMask)){
1060        if(i==1)
1061          PureSatKillPseudoGVNode(manager,node,tmpTable);
1062        else
1063          PureSatAbstractLatch(manager,node,tmpTable);
1064      }
1065    }
1066
1067    for(j=0; j<tf->nbLatches; j++){
1068      node = bAig_NonInvertedEdge(bli[j]);
1069      if(st_lookup(DoneTable,(char*)node,NIL(char*)))
1070        continue;
1071      st_insert(DoneTable,(char*)node,(char*)0);
1072      if((flags(node)&StateBitMask)&&
1073         !(flags(node)&VisibleVarMask)&&
1074         (flags(node)&CoiMask)){
1075        if(i==1)
1076          PureSatKillPseudoGVNode(manager,node,tmpTable);
1077        else
1078          PureSatAbstractLatch(manager,node,tmpTable);
1079      }
1080    }
1081    st_free_table(tmpTable);
1082    st_free_table(DoneTable);
1083  }
1084}
1085
1086
1087/**Function********************************************************************
1088
1089  Synopsis    [Count number of nodes in COI]
1090
1091  Description [Count number of nodes in COI]
1092
1093  SideEffects []
1094
1095  SeeAlso     []
1096
1097******************************************************************************/
1098
1099
1100int PureSat_CountNodesInCoi(satManager_t* cm)
1101{
1102  int ct=0;
1103  bAigEdge_t i;
1104
1105  for(i=satNodeSize;i<cm->nodesArraySize;i+=satNodeSize){
1106    if(SATflags(i) & CoiMask){
1107      ct++;
1108
1109    }
1110  }
1111  /*fprintf(vis_stdout,"There are %d node in COI\n",ct);*/
1112  return ct;
1113}
1114
1115/**Function********************************************************************
1116
1117  Synopsis    [Sanity check for one node for abstraction processsing]
1118
1119  Description [Sanity check for one node for abstraction processsing]
1120
1121  SideEffects []
1122
1123  SeeAlso     []
1124
1125******************************************************************************/
1126
1127
1128void PureSat_Check(bAig_Manager_t *manager, bAigEdge_t v)
1129{
1130  bAigEdge_t *fan,*fan1,nfan1;
1131  bAigEdge_t nfan,cur,child,tmpchild,v1,other,cur1;
1132  int size,i,j,find=0,inver,left,left1;
1133
1134  nfan = nFanout(v);
1135  fan = (bAigEdge_t *)fanout(v);
1136  if(fan == 0){
1137    assert(nfan==0);
1138    return;
1139  }
1140
1141  size = 0;
1142
1143  for(i=0; fan[i]!=0; i++){
1144    size++;
1145    cur = fan[i];
1146    left = 1;
1147    inver = 0;
1148    if(SATisInverted(cur))
1149      left = 0;
1150    cur >>= 1;
1151    if(SATisInverted(cur))
1152      inver = 1;
1153    cur = SATnormalNode(cur);
1154    child = inver? SATnormalNode(v)+1:SATnormalNode(v);
1155    if(left)
1156      tmpchild = leftChild(cur);
1157    else
1158      tmpchild = rightChild(cur);
1159    assert(tmpchild == child);
1160
1161    /*check the other child*/
1162    find = 0;
1163    other = left?rightChild(cur):leftChild(cur);
1164    assert(other!=bAig_NULL);
1165    v1 = SATnormalNode(other);
1166    nfan1 = nFanout(v1);
1167    fan1 = (bAigEdge_t *)fanout(v1);
1168    assert(nfan1!=0&&fan1!=0);
1169    for(j=0; fan1[j]!=0; j++){
1170      cur1 = fan1[j];
1171      left1 = 1;
1172      if(SATisInverted(cur1))
1173        left1 = 0;
1174      assert(j<nfan1);
1175      if((SATnormalNode(cur1>>1)==cur)&&(left1!=left)){
1176        find = 1;
1177
1178        break;
1179      }
1180    }
1181    assert(find);
1182  }
1183
1184  assert(nfan==size);
1185}
1186
1187
1188/**Function********************************************************************
1189
1190  Synopsis    [Sanity check for abstraction processsing]
1191
1192  Description [Sanity check for abstraction processsing]
1193
1194  SideEffects []
1195
1196  SeeAlso     []
1197
1198******************************************************************************/
1199
1200
1201void PureSat_CheckFanoutFanin(bAig_Manager_t *manager)
1202{
1203  bAigEdge_t  i,v;
1204
1205  for(i=bAigNodeSize;i<manager->nodesArraySize;i+=bAigNodeSize){
1206    v = i;
1207    if((flags(v) & IsCNFMask))
1208      continue;
1209    PureSat_Check(manager,v);
1210  }
1211}
1212
1213/**Function********************************************************************
1214
1215  Synopsis    [Reset a sat manager]
1216
1217  Description [Reset a sat manager]
1218
1219  SideEffects []
1220
1221  SeeAlso     []
1222
1223******************************************************************************/
1224
1225/*1. eliminate concls, 2. free variableArray
1226  3. adjust nodeArray(size and new nodes)*/
1227void PureSat_ResetManager(mAig_Manager_t *manager,
1228                          satManager_t *cm, int clean)
1229{
1230
1231  int i;
1232  satVariable_t var;
1233  satLevel_t *d;
1234
1235  if(cm->variableArray) {
1236    for(i=0; i<cm->initNumVariables; i++) {
1237      var = cm->variableArray[i];
1238      if(var.wl[0]) {
1239        sat_ArrayFree(var.wl[0]);
1240        var.wl[0] = 0;
1241      }
1242      if(var.wl[1]) {
1243        sat_ArrayFree(var.wl[1]);
1244        var.wl[1] = 0;
1245      }
1246    }
1247    free(cm->variableArray);
1248    cm->variableArray = 0;
1249  }
1250
1251  if(cm->decisionHead) {
1252    for(i=0; i<cm->decisionHeadSize; i++) {
1253      d = &(cm->decisionHead[i]);
1254      if(d->implied)
1255        sat_ArrayFree(d->implied);
1256      if(d->satisfied)
1257        sat_ArrayFree(d->satisfied);
1258    }
1259    free(cm->decisionHead);
1260    cm->decisionHead = 0;
1261    cm->decisionHeadSize = 0;
1262    cm->currentDecision = 0;
1263  }
1264
1265  if(cm->literals){
1266    sat_FreeLiteralsDB(cm->literals);
1267    cm->literals=0;
1268    sat_AllocLiteralsDB(cm);
1269  }
1270  if(cm->each){
1271    FREE(cm->each);
1272    cm->each = sat_InitStatistics();
1273  }
1274
1275  if(cm->queue)         sat_FreeQueue(cm->queue);
1276  if(cm->BDDQueue)      sat_FreeQueue(cm->BDDQueue);
1277  if(cm->unusedAigQueue)sat_FreeQueue(cm->unusedAigQueue);
1278  cm->queue = 0;
1279  cm->BDDQueue = 0;
1280  cm->unusedAigQueue = 0;
1281
1282
1283  if(cm->nonobjUnitLitArray)   sat_ArrayFree(cm->nonobjUnitLitArray);
1284  if(cm->objUnitLitArray)      sat_ArrayFree(cm->objUnitLitArray);
1285  if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray);
1286  if(cm->dormantConflictArray) sat_ArrayFree(cm->dormantConflictArray);
1287  if(cm->shrinkArray)          sat_ArrayFree(cm->shrinkArray);
1288
1289  cm->nonobjUnitLitArray = 0;
1290  cm->objUnitLitArray = 0;
1291  cm->orderedVariableArray = 0;
1292  cm->dormantConflictArray = 0;
1293  cm->shrinkArray = 0;
1294
1295  /*change initNumVariable after cm->variableArray has been freed,
1296    otherwise, initNumVariable may change*/
1297  cm->nodesArray = manager->NodesArray;
1298  cm->nodesArraySize = manager->nodesArraySize;
1299  cm->initNodesArraySize = manager->nodesArraySize;
1300  cm->maxNodesArraySize = manager->maxNodesArraySize;
1301  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1;
1302  cm->initNumClauses = 0;
1303  cm->initNumLiterals = 0;
1304
1305  cm->ipm = manager->ipm;
1306  cm->assertArray = manager->assertArray;
1307  cm->assertArray2 = manager->assertArray2;
1308  cm->InitState = manager->InitState;
1309  cm->CoiAssertArray = manager->CoiAssertArray;
1310  cm->EqArray = manager->EqArray;
1311
1312  cm->currentVarPos = 0;
1313  cm->currentTopConflict = 0;
1314  cm->currentTopConflictCount = 0;
1315  cm->lowestBacktrackLevel = 0;
1316  cm->implicatedSoFar = 0;
1317  //cm->status = 0;
1318
1319  if(clean){
1320    for(i=bAigNodeSize;i<cm->nodesArraySize;i+=bAigNodeSize)
1321      cm->nodesArray[i] = 2;
1322  }
1323}
1324
1325
1326/**Function********************************************************************
1327
1328  Synopsis    [Restore AIG to get rid of Dummy nodes]
1329
1330  Description [Restore AIG to get rid of Dummy nodes]
1331
1332  SideEffects []
1333
1334  SeeAlso     []
1335
1336******************************************************************************/
1337
1338void PureSat_RestoreAigForDummyNode(mAig_Manager_t *manager,
1339                                    int oldPosition)
1340{
1341
1342  bAigEdge_t  i;
1343
1344  for(i=manager->nodesArraySize-bAigNodeSize;
1345      i>oldPosition;i=i-bAigNodeSize){
1346#if DBG
1347    assert(leftChild(i)==bAig_NULL&&
1348           rightChild(i)==bAig_NULL);
1349    assert(flags(i)&DummyMask);
1350#endif
1351    FREE(fanout(i));
1352  }
1353
1354  manager->nodesArraySize = oldPosition+bAigNodeSize;
1355
1356  return;
1357
1358}
1359
1360/**Function********************************************************************
1361
1362  Synopsis    [Process fanout nodes to generate abstraction]
1363
1364  Description [Process fanout nodes to generate abstraction]
1365
1366  SideEffects []
1367
1368  SeeAlso     []
1369
1370******************************************************************************/
1371
1372/*after this funct, all nodes' fanout, either COI or not
1373  are in COI, not InvSV, and if this node is InvSV, not to a node in the next tf*/
1374void PureSatProcessFanout(satManager_t * cm)
1375{
1376
1377long bufSize, bufIndex;
1378bAigEdge_t *buf,left,right,*fan,v,cur;
1379int i, j;
1380long size, tsize;
1381
1382int InvStateVar,l;
1383
1384
1385  bufSize = 1024;
1386  bufIndex = 0;
1387  buf = malloc(sizeof(bAigEdge_t) * bufSize);
1388  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
1389    v = i;
1390
1391    if(!(SATflags(v) & CoiMask))
1392      continue;
1393
1394    InvStateVar = 0;
1395    if((SATflags(v)&StateBitMask)&&
1396       !(SATflags(v)&VisibleVarMask))
1397      InvStateVar = 1;
1398
1399    size = SATnFanout(v);
1400    if(size >= bufSize) {
1401      bufSize <<= 1;
1402      if(size >= bufSize)
1403        bufSize = size + 1;
1404      buf = realloc(buf, sizeof(bAigEdge_t) * bufSize);
1405    }
1406
1407    bufIndex = 0;
1408    for(j=0, fan = SATfanout(v); j<size; j++) {
1409      cur = fan[j];
1410      cur >>= 1;
1411      cur = SATnormalNode(cur);
1412      /*Not in COI , pass */
1413      if(!(SATflags(cur) & CoiMask))
1414        continue;
1415      /*cur is invisible var*/
1416      left = SATleftChild(cur);
1417      right = SATrightChild(cur);
1418      if(left==bAig_NULL||right==bAig_NULL){
1419#if DBG
1420
1421        assert(left==bAig_NULL&&right==bAig_NULL);
1422        assert((SATflags(cur)&StateBitMask)&&
1423               !(SATflags(cur)&VisibleVarMask));
1424#endif
1425        continue;
1426      }
1427      /*v itself is InvStateVar and cur is not InvSV*/
1428
1429      if(SATflags(v)&PGVMask){
1430
1431         if(SATclass(cur)>=2){
1432          l = SATisInverted(fan[j]) ? 0 : 1;
1433          if(l){
1434#if DBG
1435            bAigEdge_t v1 = SATnormalNode(SATleftChild(cur));
1436            assert(v1!=v);
1437            assert(SATflags(v1)&DummyMask);
1438#endif
1439          }
1440          else{
1441#if DBG
1442            bAigEdge_t v1 = SATnormalNode(SATrightChild(cur));
1443            assert(v1!=v);
1444            assert(SATflags(v1)&DummyMask);
1445#endif
1446          }
1447          continue;
1448        }
1449      }
1450      buf[bufIndex++] = fan[j];
1451    }
1452
1453    if(bufIndex > 0) {
1454      tsize = bufIndex;
1455      for(j=0, fan=SATfanout(v); j<size; j++) {
1456        cur = fan[j];
1457        cur >>= 1;
1458        cur = SATnormalNode(cur);
1459        if(!(SATflags(cur) & CoiMask))  {
1460          buf[bufIndex++] = fan[j];
1461          continue;
1462        }
1463
1464        left = SATleftChild(cur);
1465        right = SATrightChild(cur);
1466
1467        if(left==bAig_NULL||right==bAig_NULL){
1468          buf[bufIndex++] = fan[j];
1469          continue;
1470        }
1471
1472
1473        if(SATflags(v)&PGVMask){
1474          if(SATclass(cur)>=2){
1475            buf[bufIndex++] = fan[j];
1476            continue;
1477          }
1478        }
1479
1480      }/*for(j=0, fan=SATfanout(v); j<size; j++) {*/
1481      buf[bufIndex] = 0;
1482      memcpy(fan, buf, sizeof(bAigEdge_t)*(size+1));
1483      SATnFanout(v) = tsize;
1484    }
1485    else
1486      SATnFanout(v) = 0;
1487  }
1488
1489  free(buf);
1490
1491  for(i=satNodeSize; i<cm->nodesArraySize; i+=satNodeSize) {
1492    v = i;
1493    if(!(SATflags(v) & CoiMask))
1494      continue;
1495    fan = SATfanout(v);
1496    size = SATnFanout(v);
1497    qsort(fan, size, sizeof(bAigEdge_t), NodeIndexCompare);
1498  }
1499}
1500/**Function********************************************************************
1501
1502  Synopsis    [Recover from abstractions]
1503
1504  Description [Recover from abstractions]
1505
1506  SideEffects []
1507
1508  SeeAlso     []
1509
1510******************************************************************************/
1511
1512long PureSatRecoverFanoutNode(satManager_t * cm,
1513                              bAigEdge_t v)
1514{
1515  bAigEdge_t *fan,nfan,child,cur;
1516  long i;
1517  int left,inver;
1518  int InvStateVar = 0;
1519
1520  if(!(SATflags(v)&VisibleVarMask)&&(SATflags(v)&StateBitMask))
1521    InvStateVar = 1;
1522
1523  nfan = SATnFanout(v);
1524
1525  fan = SATfanout(v);
1526  if(fan == 0)  return(0);
1527
1528  /*recover left and right children for latch nodes*/
1529
1530  for(i=nfan; fan[i]!=0; i++){
1531    cur = fan[i];
1532    if(!(SATflags(SATnormalNode(cur>>1))&CoiMask))
1533      continue;
1534    /*cur is InvSV*/
1535    if((SATleftChild(SATnormalNode(cur>>1))==bAig_NULL)||
1536       (SATrightChild(SATnormalNode(cur>>1))==bAig_NULL)){
1537#if DBG
1538      assert((SATflags(SATnormalNode(cur>>1))&StateBitMask)&&
1539             !(SATflags(SATnormalNode(cur>>1))&VisibleVarMask));
1540#endif
1541      left = 1;
1542      inver = 0;
1543      if(SATisInverted(cur))
1544        left = 0;
1545      cur >>= 1;
1546      if(SATisInverted(cur))
1547        inver = 1;
1548      cur = SATnormalNode(cur);
1549      child = inver? SATnormalNode(v)+1:SATnormalNode(v);
1550      if(left)
1551        SATleftChild(cur)=child;
1552      else
1553        SATrightChild(cur)=child;
1554      continue;
1555    }
1556
1557    /*v is InvSV, cur is not InvSV*/
1558
1559    if(SATflags(v)&PGVMask){
1560
1561      if(SATclass(SATnormalNode(cur>>1))>=2){
1562        left = 1;
1563        inver = 0;
1564        if(SATisInverted(cur))
1565          left = 0;
1566        cur >>= 1;
1567        if(SATisInverted(cur))
1568          inver = 1;
1569        cur = SATnormalNode(cur);
1570        child = inver? SATnormalNode(v)+1:SATnormalNode(v);
1571        if(left)
1572          SATleftChild(cur)=child;
1573        else
1574          SATrightChild(cur)=child;
1575      }
1576    }
1577  }
1578  //recover all fanout
1579  return(i);
1580}
1581
1582/**Function********************************************************************
1583
1584  Synopsis    [Recover invisible state variable node]
1585
1586  Description [Recover invisible state variable node]
1587
1588  SideEffects []
1589
1590  SeeAlso     []
1591
1592******************************************************************************/
1593void
1594PureSatRecoverISVNode(satManager_t *cm,
1595                      bAigEdge_t v)
1596{
1597
1598  bAigEdge_t size = SATnFanout(v),cur,node,child;
1599  bAigEdge_t  * fan = SATfanout(v);
1600  int inv,i,left;
1601
1602  for(i=0;i<size;i++){
1603    cur = fan[i]>>1;
1604    node = SATnormalNode(cur);
1605    /*not in coi*/
1606    if(!(SATflags(node)&CoiMask))
1607      continue;
1608    /*not invisible var*/
1609    if(!((SATflags(node)&StateBitMask)&&
1610         !(SATflags(node)&VisibleVarMask)))
1611      continue;
1612
1613    left=SATisInverted(fan[i])?0:1;
1614    inv=SATisInverted(cur)?1:0;
1615    child = inv?SATnormalNode(v)+1:SATnormalNode(v);
1616    if(left)
1617      SATleftChild(node) = child;
1618    else
1619      SATrightChild(node) = child;
1620  }
1621}
1622
1623/**Function********************************************************************
1624
1625  Synopsis    [Recover fanout of nodes]
1626
1627  Description [Recover fanout of nodes]
1628
1629  SideEffects []
1630
1631  SeeAlso     []
1632
1633******************************************************************************/
1634
1635void PureSatRecoverFanout(satManager_t * cm,
1636                          PureSat_Manager_t *pm)
1637{
1638  bAigEdge_t i, v;
1639
1640  /*dummy node can't be recovered*/
1641  for(i=satNodeSize; i<=pm->oldPos; i+=satNodeSize) {
1642    v = i;
1643    if(SATflags(v) & IsCNFMask)
1644      continue;
1645
1646    if((SATflags(v)&CoiMask)){
1647       SATnFanout(v) = PureSatRecoverFanoutNode(cm, v);
1648       continue;
1649    }
1650    /*for some node not in coi, but a child of one coi(ISV) node*/
1651    if(SATflags(v)&Visited3Mask){
1652      PureSatRecoverISVNode(cm,v);
1653      continue;
1654    }
1655  }
1656
1657}
1658
1659/**Function********************************************************************
1660
1661  Synopsis    [sanity check for one node for abstraction processing]
1662
1663  Description [sanity check for one node for abstraction processing]
1664
1665  SideEffects []
1666
1667  SeeAlso     []
1668
1669******************************************************************************/
1670
1671void PureSatCheckCoiNode(bAig_Manager_t * manager,
1672                         bAigEdge_t node)
1673{
1674  int i;
1675  long *fan;
1676  long  nfan,child, cur;
1677  int left,inv;
1678
1679  nfan = nFanout(node);
1680  fan = (bAigEdge_t*)fanout(node);
1681  if(fan==0) return;
1682  /*check child*/
1683  assert((leftChild(node)==bAig_NULL)||
1684   (flags(leftChild(node))&CoiMask));
1685  assert((rightChild(node)==bAig_NULL)||
1686   (flags(rightChild(node))&CoiMask));
1687  if((leftChild(node)==bAig_NULL)||(rightChild(node)==bAig_NULL))
1688    assert((leftChild(node)==bAig_NULL)&&(rightChild(node)==bAig_NULL));
1689  /*check fanout*/
1690  for(i=0; i<nfan; i++){
1691    cur = fan[i]>>1;
1692    assert(flags(cur)&CoiMask);
1693    left=SATisInverted(fan[i])?0:1;
1694    inv=SATisInverted(cur)?1:0;
1695    child = inv?SATnormalNode(node)+1:SATnormalNode(node);
1696    if(left){
1697     assert(child==leftChild(cur));
1698    }
1699    else{
1700      assert(child==rightChild(cur));
1701    }
1702  }
1703
1704}
1705
1706/**Function********************************************************************
1707
1708  Synopsis    [sanity check for abstraction processing]
1709
1710  Description [sanity check for abstraction processing]
1711
1712  SideEffects []
1713
1714  SeeAlso     []
1715
1716******************************************************************************/
1717
1718void PureSatCheckCoi(bAig_Manager_t *manager)
1719{
1720  long i;
1721  for(i=bAigNodeSize;i<manager->nodesArraySize;i+=bAigNodeSize){
1722    if(flags(i) & IsCNFMask)
1723      continue;
1724    if(!(flags(i) & CoiMask))
1725      continue;
1726    PureSatCheckCoiNode(manager,i);
1727  }
1728
1729}
1730
1731/**Function********************************************************************
1732
1733  Synopsis    [Preprocess to form SAT instances]
1734
1735  Description [Preprocess to form SAT instances]
1736
1737  SideEffects []
1738
1739  SeeAlso     []
1740
1741******************************************************************************/
1742
1743
1744void PureSatPreprocess(Ntk_Network_t * network,
1745                       satManager_t *cm,
1746                       PureSat_Manager_t *pm,
1747                       st_table *vertexTable,
1748                       int Length)
1749
1750{
1751  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
1752
1753  PureSatSetCOI(network,pm,cm,vertexTable,0, Length,Length);
1754  /*for interpolation*/
1755  PureSatKillPseudoGV(network,pm,vertexTable,1,Length);
1756  PureSat_ResetManager(manager,cm,0);
1757  /*for abstraction*/
1758  PureSatProcessFanout(cm);
1759}
1760
1761/**Function********************************************************************
1762
1763  Synopsis    [Recovery step after SAT solving]
1764
1765  Description [Recovery step after SAT solving]
1766
1767  SideEffects []
1768
1769  SeeAlso     []
1770
1771******************************************************************************/
1772
1773
1774void PureSatPostprocess(bAig_Manager_t *manager,
1775                        satManager_t *cm,
1776                        PureSat_Manager_t *pm)
1777{
1778
1779  PureSatRecoverFanout(cm,pm);
1780  PureSat_RestoreAigForDummyNode(manager,pm->oldPos);
1781  PureSat_CleanMask(manager,ResetVisited3Mask);
1782}
1783
1784
1785/**Function********************************************************************
1786
1787  Synopsis    [Convergence test for flat interpolation algorithm]
1788
1789  Description [Convergence test for flat interpolation algorithm]
1790
1791  SideEffects []
1792
1793  SeeAlso     []
1794
1795******************************************************************************/
1796
1797
1798/*test if state1 contains state2*/
1799int PureSat_TestConvergeForIP(mAig_Manager_t *manager,
1800                              PureSat_Manager_t *pm,
1801                              satManager_t *cm,
1802                              bAigEdge_t state1,
1803                              bAigEdge_t state2)
1804{
1805  satArray_t * tmp1,*tmp2,*tmp3, *tmp4,*tmp5, *tmp6, *tmp7;
1806  int status, nodes_in_coi = 0;
1807
1808 if(state2 == bAig_Zero)
1809    return 1;
1810  if(state1 == bAig_One)
1811    return 1;
1812  if(state1 == bAig_Zero && state2 != bAig_Zero)
1813    return 0;
1814  if(state1 != bAig_One && state2 == bAig_One)
1815    return 0;
1816
1817  if(pm->verbosity>=1)
1818    fprintf(vis_stdout,"Test convergence:\n");
1819  PureSat_ResetCoi(cm);
1820  if(pm->verbosity>=1){
1821    fprintf(vis_stdout,"after reset COI\n");
1822    nodes_in_coi = PureSat_CountNodesInCoi(cm);
1823    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
1824  }
1825  tmp1 = cm->obj;
1826  tmp2 = cm->auxObj;
1827  tmp3 = cm->assertion;
1828  tmp4 = cm->assertArray;
1829  //Bing:
1830  tmp5 = cm->unitLits;
1831  tmp6 = cm->pureLits;
1832  tmp7 = cm->nonobjUnitLitArray;
1833  cm->obj = 0;
1834  cm->auxObj = 0;
1835  cm->assertion = 0;
1836  //cm->assertArray2 = 0;
1837  cm->assertArray = sat_ArrayAlloc(1);
1838  sat_ArrayInsert(cm->assertArray,SATnot(state1));
1839  sat_ArrayInsert(cm->assertArray,state2);
1840  sat_SetConeOfInfluence(cm);
1841  if(pm->verbosity>=1){
1842    fprintf(vis_stdout,"after add new init states:\n");
1843    nodes_in_coi = PureSat_CountNodesInCoi(cm);
1844    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
1845  }
1846  cm->option->coreGeneration = 0;
1847  //cm->option->effIP = 0;
1848  cm->option->IP = 0;
1849  cm->status = 0;
1850  sat_Main(cm);
1851  if(manager->NodesArray!=cm->nodesArray)
1852    /*cm->nodesArray may be reallocated*/
1853    manager->NodesArray = cm->nodesArray;
1854  cm->obj = tmp1;
1855  cm->auxObj = tmp2;
1856  cm->assertion = tmp3;
1857  sat_ArrayFree(cm->assertArray);
1858  cm->assertArray = tmp4;
1859
1860  cm->unitLits = tmp5;
1861  cm->pureLits = tmp6;
1862  cm->nonobjUnitLitArray = tmp7;
1863
1864  cm->option->coreGeneration = 1;
1865
1866  cm->option->IP = 1;
1867  status = cm->status;
1868#if DBG
1869  assert(cm->currentDecision>=-1);
1870#endif
1871  if(cm->currentDecision!=-1)
1872    sat_Backtrack(cm,-1);
1873  cm->status = 0;
1874
1875  if(status == SAT_UNSAT)
1876    /*state2 contains state1, reach convergence*/
1877    return 1;
1878  else
1879    return 0;
1880}
1881
1882/**Function********************************************************************
1883
1884  Synopsis    [Convergence test for interpolation algorithm with abstraction
1885              refinement ]
1886
1887  Description [Convergence test for flat interpolation algorithmwith abstraction
1888              refinement ]
1889
1890  SideEffects []
1891
1892  SeeAlso     []
1893
1894******************************************************************************/
1895
1896
1897
1898/*test if state1 contains state2 for abstract refinement*/
1899int PureSat_TestConvergeForIP_AbRf(Ntk_Network_t *network,
1900                                   satManager_t *cm,
1901                                   PureSat_Manager_t *pm,
1902                                   array_t  * CoiArray,
1903                                   bAigEdge_t state1,
1904                                   bAigEdge_t state2)
1905{
1906  satArray_t * tmp1,*tmp2,*tmp3, *tmp4,*tmp5, *tmp6, *tmp7;
1907  int status, nodes_in_coi = 0;
1908  mAig_Manager_t * manager;
1909
1910
1911  if(state2 == bAig_Zero)
1912    return 1;
1913  if(state1 == bAig_One)
1914    return 1;
1915  if(state1 == bAig_Zero && state2 != bAig_Zero)
1916    return 0;
1917  if(state1 != bAig_One && state2 == bAig_One)
1918    return 0;
1919
1920
1921  manager = Ntk_NetworkReadMAigManager(network);
1922
1923  if(pm->verbosity>=1)
1924    fprintf(vis_stdout,"Test convergence:\n");
1925  PureSat_ResetCoi(cm);
1926  if(pm->verbosity>=1){
1927    fprintf(vis_stdout,"after reset COI\n");
1928    nodes_in_coi = PureSat_CountNodesInCoi(cm);
1929    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
1930  }
1931  tmp1 = cm->obj;
1932  tmp2 = cm->auxObj;
1933  tmp3 = cm->assertion;
1934  tmp4 = cm->assertArray;
1935
1936  tmp5 = cm->unitLits;
1937  tmp6 = cm->pureLits;
1938  tmp7 = cm->nonobjUnitLitArray;
1939  cm->obj = 0;
1940  cm->auxObj = 0;
1941  cm->assertion = 0;
1942  cm->unitLits = 0;
1943  cm->pureLits = 0;
1944  cm->nonobjUnitLitArray = 0;
1945  cm->assertArray = sat_ArrayAlloc(1);
1946  sat_ArrayInsert(cm->assertArray,SATnot(state1));
1947  sat_ArrayInsert(cm->assertArray,state2);
1948
1949  sat_MarkTransitiveFaninForArray(cm, cm->assertArray, CoiMask);
1950
1951  if(pm->verbosity>=1){
1952    fprintf(vis_stdout,"after add new init states:\n");
1953    nodes_in_coi = PureSat_CountNodesInCoi(cm);
1954    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
1955  }
1956  cm->option->coreGeneration = 0;
1957  cm->status = 0;
1958  cm->option->AbRf = 0;
1959  sat_Main(cm);
1960  cm->option->AbRf = 1;
1961  if(manager->NodesArray!=cm->nodesArray)
1962    /*cm->nodesArray may be reallocated*/
1963    manager->NodesArray = cm->nodesArray;
1964  sat_ArrayFree(cm->assertArray);
1965  manager->assertArray = tmp4;
1966  cm->obj = tmp1;
1967  cm->auxObj = tmp2;
1968  cm->assertion = tmp3;
1969  cm->assertArray = tmp4;
1970
1971  cm->unitLits = tmp5;
1972  cm->pureLits = tmp6;
1973  cm->nonobjUnitLitArray = tmp7;
1974  cm->option->coreGeneration = 1;
1975  status = cm->status;
1976  if(cm->currentDecision!=-1)
1977    sat_Backtrack(cm,-1);
1978  cm->status = 0;
1979
1980  if(status == SAT_UNSAT)
1981    /*state2 contains state1, reach convergence*/
1982    return 1;
1983  else
1984    return 0;
1985}
1986
1987/**Function********************************************************************
1988
1989  Synopsis    [Allocate a PureSAT Manager]
1990
1991  Description [Allocate a PureSAT Manager]
1992
1993  SideEffects []
1994
1995  SeeAlso     []
1996
1997******************************************************************************/
1998
1999satManager_t * PureSat_SatManagerAlloc(bAig_Manager_t *manager,
2000                                       PureSat_Manager_t *pm,
2001                                       bAigEdge_t     object,
2002                                       array_t        *auxObjectArray)
2003{
2004  satManager_t * cm;
2005  satOption_t *option;
2006  int i,size;
2007  bAigEdge_t tv;
2008
2009  cm = ALLOC(satManager_t, 1);
2010  memset(cm, 0, sizeof(satManager_t));
2011  cm->nodesArraySize = manager->nodesArraySize;
2012  cm->initNodesArraySize = manager->nodesArraySize;
2013  cm->maxNodesArraySize = manager->maxNodesArraySize;
2014  cm->nodesArray = manager->NodesArray;
2015
2016  cm->HashTable = manager->HashTable;
2017  cm->literals = manager->literals;
2018
2019  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1;
2020  cm->initNumClauses = 0;
2021  cm->initNumLiterals = 0;
2022  cm->comment = ALLOC(char, 2);
2023  cm->comment[0] = ' ';
2024  cm->comment[1] = '\0';
2025  cm->stdErr = vis_stderr;
2026  cm->stdOut = vis_stdout;
2027  cm->status = 0;
2028  cm->orderedVariableArray = 0;
2029  cm->unitLits = sat_ArrayAlloc(16);
2030  cm->pureLits = sat_ArrayAlloc(16);
2031  cm->option = 0;
2032  cm->each = 0;
2033  cm->decisionHead = 0;
2034  cm->variableArray = 0;
2035  cm->queue = 0;
2036  cm->BDDQueue = 0;
2037  cm->unusedAigQueue = 0;
2038
2039  cm->ipm = manager->ipm;
2040  cm->assertArray = manager->assertArray;
2041  cm->assertArray2 = manager->assertArray2;
2042  cm->InitState = manager->InitState;
2043  cm->CoiAssertArray = manager->CoiAssertArray;
2044  cm->EqArray = manager->EqArray;
2045
2046  if(auxObjectArray) {
2047    cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
2048    size = auxObjectArray->num;
2049    for(i=0; i<size; i++) {
2050      tv = array_fetch(bAigEdge_t, auxObjectArray, i);
2051      if(tv == 1)       continue;
2052      else if(tv == 0) {
2053        cm->status = SAT_UNSAT;
2054        break;
2055      }
2056      sat_ArrayInsert(cm->auxObj, tv);
2057    }
2058  }
2059  if(object == 0)      cm->status = SAT_UNSAT;
2060  else if(object == 1) cm->status = SAT_SAT;
2061
2062
2063  if(cm->status == 0) {
2064    if(object!=-1){
2065      cm->obj = sat_ArrayAlloc(1);
2066      sat_ArrayInsert(cm->obj, object);
2067    }
2068    /* initialize option*/
2069    option = sat_InitOption();
2070
2071    option->coreGeneration = 1;
2072    option->ForceFinish = 1;
2073
2074    option->clauseDeletionHeuristic = 0;
2075    option->includeLevelZeroLiteral = 1;
2076    option->minimizeConflictClause = 0;
2077    option->IP = 1;
2078    option->RT = 1;
2079    option->verbose = pm->verbosity;
2080
2081    cm->anteTable = st_init_table(st_numcmp,st_numhash);
2082    cm->RTreeTable = st_init_table(st_ptrcmp,st_ptrhash);
2083
2084    cm->option = option;
2085    cm->each = sat_InitStatistics();
2086
2087    BmcRestoreAssertion(manager,cm);
2088
2089    /* value reset..*/
2090    sat_CleanDatabase(cm);
2091
2092    /* set cone of influence*/
2093    sat_SetConeOfInfluence(cm);
2094    sat_AllocLiteralsDB(cm);
2095  }
2096  return cm;
2097}
2098
2099
2100/**Function********************************************************************
2101
2102  Synopsis    [Allocate a PureSAT Manager without setting COI]
2103
2104  Description [Allocate a PureSAT Manager without setting COI]
2105
2106  SideEffects []
2107
2108  SeeAlso     []
2109
2110******************************************************************************/
2111satManager_t * PureSat_SatManagerAlloc_WOCOI(mAig_Manager_t *manager,
2112                                             PureSat_Manager_t *pm,
2113                                             bAigEdge_t     object,
2114                                             array_t        *auxObjectArray)
2115{
2116  satManager_t * cm;
2117  satOption_t *option;
2118  int i,size;
2119  bAigEdge_t tv;
2120
2121  cm = ALLOC(satManager_t, 1);
2122  memset(cm, 0, sizeof(satManager_t));
2123  cm->nodesArraySize = manager->nodesArraySize;
2124  cm->initNodesArraySize = manager->nodesArraySize;
2125  cm->maxNodesArraySize = manager->maxNodesArraySize;
2126  cm->nodesArray = manager->NodesArray;
2127
2128  cm->HashTable = manager->HashTable;
2129  cm->literals = manager->literals;
2130
2131  cm->initNumVariables = (manager->nodesArraySize/bAigNodeSize)-1;
2132  cm->initNumClauses = 0;
2133  cm->initNumLiterals = 0;
2134  cm->comment = ALLOC(char, 2);
2135  cm->comment[0] = ' ';
2136  cm->comment[1] = '\0';
2137  cm->stdErr = vis_stderr;
2138  cm->stdOut = vis_stdout;
2139  cm->status = 0;
2140  cm->orderedVariableArray = 0;
2141  cm->unitLits = sat_ArrayAlloc(16);
2142  cm->pureLits = sat_ArrayAlloc(16);
2143  cm->option = 0;
2144  cm->each = 0;
2145  cm->decisionHead = 0;
2146  cm->variableArray = 0;
2147  cm->queue = 0;
2148  cm->BDDQueue = 0;
2149  cm->unusedAigQueue = 0;
2150
2151  cm->ipm = manager->ipm;
2152  cm->assertArray = manager->assertArray;
2153  cm->assertArray2 = manager->assertArray2;
2154  cm->InitState = manager->InitState;
2155  cm->CoiAssertArray = manager->CoiAssertArray;
2156  cm->EqArray = manager->EqArray;
2157
2158  if(auxObjectArray) {
2159    cm->auxObj = sat_ArrayAlloc(auxObjectArray->num+1);
2160    size = auxObjectArray->num;
2161    for(i=0; i<size; i++) {
2162      tv = array_fetch(bAigEdge_t, auxObjectArray, i);
2163      if(tv == 1)       continue;
2164      else if(tv == 0) {
2165        cm->status = SAT_UNSAT;
2166        break;
2167      }
2168      sat_ArrayInsert(cm->auxObj, tv);
2169    }
2170  }
2171  if(object == 0)      cm->status = SAT_UNSAT;
2172  else if(object == 1) cm->status = SAT_SAT;
2173
2174
2175  if(cm->status == 0) {
2176    if(object!=-1){
2177      cm->obj = sat_ArrayAlloc(1);
2178      sat_ArrayInsert(cm->obj, object);
2179    }
2180
2181    option = sat_InitOption();
2182    option->ForceFinish = 1;
2183
2184    option->coreGeneration = 1;
2185    option->clauseDeletionHeuristic = 0;
2186    option->includeLevelZeroLiteral = 1;
2187    option->minimizeConflictClause = 0;
2188    option->IP = 0;
2189    option->RT = 1;
2190    option->verbose = pm->verbosity;
2191
2192    cm->anteTable = st_init_table(st_numcmp,st_numhash);
2193    cm->RTreeTable = st_init_table(st_ptrcmp,st_ptrhash);
2194
2195    cm->option = option;
2196    cm->each = sat_InitStatistics();
2197
2198    BmcRestoreAssertion(manager,cm);
2199
2200    sat_CleanDatabase(cm);
2201
2202    /* WOCOI: NO set cone of influence*/
2203    sat_AllocLiteralsDB(cm);
2204  }
2205  return cm;
2206}
2207
2208/**Function********************************************************************
2209
2210  Synopsis    [Free a PureSAT manager]
2211
2212  Description [Free a PureSAT manager]
2213
2214  SideEffects []
2215
2216  SeeAlso     []
2217
2218******************************************************************************/
2219
2220
2221void PureSat_SatFreeManager(satManager_t*cm)
2222{
2223satVariable_t var;
2224satLevel_t *d;
2225int i;
2226
2227
2228  if(cm->option->coreGeneration){
2229    st_free_table(cm->anteTable);
2230    st_free_table(cm->RTreeTable);
2231
2232    cm->anteTable=0;
2233    cm->RTreeTable=0;
2234  }
2235
2236  /*timeframe, timeframeWOI,HashTable can't be freed*/
2237
2238  if(cm->option)        sat_FreeOption(cm->option);
2239  if(cm->total)         sat_FreeStatistics(cm->total);
2240  if(cm->each)          sat_FreeStatistics(cm->each);
2241
2242  if(cm->literals)      sat_FreeLiteralsDB(cm->literals);
2243
2244  cm->option=0;
2245  cm->total=0;
2246  cm->each=0;
2247  cm->literals=0;
2248
2249  if(cm->decisionHead) {
2250    for(i=0; i<cm->decisionHeadSize; i++) {
2251      d = &(cm->decisionHead[i]);
2252      if(d->implied)
2253        sat_ArrayFree(d->implied);
2254      if(d->satisfied)
2255        sat_ArrayFree(d->satisfied);
2256    }
2257    free(cm->decisionHead);
2258    cm->decisionHead = 0;
2259    cm->decisionHeadSize = 0;
2260  }
2261
2262  if(cm->queue)         sat_FreeQueue(cm->queue);
2263  if(cm->BDDQueue)      sat_FreeQueue(cm->BDDQueue);
2264  if(cm->unusedAigQueue)sat_FreeQueue(cm->unusedAigQueue);
2265  cm->queue = 0;
2266  cm->BDDQueue = 0;
2267  cm->unusedAigQueue = 0;
2268
2269  if(cm->auxObj)               sat_ArrayFree(cm->auxObj);
2270  if(cm->obj)                  sat_ArrayFree(cm->obj);
2271  if(cm->unitLits)             sat_ArrayFree(cm->unitLits);
2272  if(cm->pureLits)             sat_ArrayFree(cm->pureLits);
2273  if(cm->assertion)            sat_ArrayFree(cm->assertion);
2274  if(cm->auxArray)             sat_ArrayFree(cm->auxArray);
2275  if(cm->nonobjUnitLitArray)   sat_ArrayFree(cm->nonobjUnitLitArray);
2276  if(cm->objUnitLitArray)      sat_ArrayFree(cm->objUnitLitArray);
2277  if(cm->orderedVariableArray) sat_ArrayFree(cm->orderedVariableArray);
2278  if(cm->savedConflictClauses) sat_ArrayFree(cm->savedConflictClauses);
2279
2280  cm->auxObj = 0;
2281  cm->obj = 0;
2282  cm->unitLits = 0;
2283  cm->pureLits = 0;
2284  cm->assertion = 0;
2285  cm->auxArray = 0;
2286  cm->nonobjUnitLitArray = 0;
2287  cm->objUnitLitArray = 0;
2288  cm->orderedVariableArray = 0;
2289
2290  if(cm->variableArray) {
2291    for(i=0; i<cm->initNumVariables; i++) {
2292      var = cm->variableArray[i];
2293      if(var.wl[0]) {
2294        sat_ArrayFree(var.wl[0]);
2295        var.wl[0] = 0;
2296      }
2297      if(var.wl[1]) {
2298        sat_ArrayFree(var.wl[1]);
2299        var.wl[1] = 0;
2300      }
2301    }
2302    free(cm->variableArray);
2303    cm->variableArray = 0;
2304  }
2305
2306  if(cm->comment)       free(cm->comment);
2307  cm->comment=0;
2308
2309  FREE(cm);
2310}
2311
2312/**Function********************************************************************
2313
2314  Synopsis    [Print the status of AIG]
2315
2316  Description [Print the status of AIG]
2317
2318  SideEffects []
2319
2320  SeeAlso     []
2321
2322******************************************************************************/
2323
2324
2325void PureSat_PrintAigStatus(mAig_Manager_t *manager)
2326{
2327  (void) fprintf(vis_stdout,"Maximum number of nodes: %ld\n",
2328                 manager->maxNodesArraySize/bAigNodeSize);
2329  (void) fprintf(vis_stdout,"Current number of nodes: %ld\n",
2330                 manager->nodesArraySize/bAigNodeSize);
2331  fprintf(vis_stdout,"Current Max Node Index: %ld\n\n",
2332          manager->nodesArraySize);
2333}
2334
2335/**Function********************************************************************
2336
2337  Synopsis    [Mark global variables]
2338
2339  Description [Mark global variables]
2340
2341  SideEffects []
2342
2343  SeeAlso     []
2344
2345******************************************************************************/
2346
2347void PureSat_MarkGlobalVar(bAig_Manager_t *manager,
2348                           int length)
2349{
2350  bAigTimeFrame_t * tf = manager->timeframeWOI;
2351  bAigEdge_t * li,* bli,node;
2352  int i;
2353
2354  li = tf->latchInputs[length];
2355  bli = tf->blatchInputs[length];
2356
2357  for(i=0; i<tf->nLatches; i++){
2358    node = bAig_NonInvertedEdge(li[i]);
2359    manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
2360  }
2361
2362  for(i=0; i<tf->nbLatches; i++){
2363    node = bAig_NonInvertedEdge(bli[i]);
2364    manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
2365  }
2366}
2367
2368/**Function********************************************************************
2369
2370  Synopsis    [UnMark global variables]
2371
2372  Description [UnMark global variables]
2373
2374  SideEffects []
2375
2376  SeeAlso     []
2377
2378******************************************************************************/
2379
2380void PureSat_UnMarkGlobalVar(bAig_Manager_t *manager,
2381                           int length)
2382{
2383  bAigTimeFrame_t * tf = manager->timeframeWOI;
2384  bAigEdge_t * li,* bli,node;
2385  int i;
2386
2387  li = tf->latchInputs[length];
2388  bli = tf->blatchInputs[length];
2389
2390  for(i=0; i<tf->nLatches; i++){
2391    node = bAig_NonInvertedEdge(li[i]);
2392    manager->NodesArray[node+bAigFlags] &= ResetGlobalVarMask;
2393  }
2394
2395  for(i=0; i<tf->nbLatches; i++){
2396    node = bAig_NonInvertedEdge(bli[i]);
2397    manager->NodesArray[node+bAigFlags] &= ResetGlobalVarMask;
2398  }
2399}
2400
2401
2402/**Function********************************************************************
2403
2404  Synopsis    [Makr global variable for abstraction refinement]
2405
2406  Description []
2407
2408  SideEffects []
2409
2410  SeeAlso     []
2411
2412******************************************************************************/
2413
2414void PureSat_MarkGlobalVar_AbRf(bAig_Manager_t *manager,
2415                                int length)
2416{
2417  bAigTimeFrame_t * tf = manager->timeframeWOI;
2418  bAigEdge_t * li,* bli,node;
2419  int i;
2420
2421
2422  li = tf->latchInputs[length];
2423  bli = tf->blatchInputs[length];
2424
2425  for(i=0; i<tf->nLatches; i++){
2426    node = bAig_NonInvertedEdge(li[i]);
2427    if(flags(node)&VisibleVarMask)
2428      manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
2429  }
2430
2431  for(i=0; i<tf->nbLatches; i++){
2432    node = bAig_NonInvertedEdge(bli[i]);
2433    if(flags(node)&VisibleVarMask)
2434      manager->NodesArray[node+bAigFlags] |= IsGlobalVarMask;
2435  }
2436
2437}
2438
2439
2440/**Function********************************************************************
2441
2442  Synopsis    [Mark visible variable and also mark visible pseudo global variable]
2443
2444  Description []
2445
2446  SideEffects []
2447
2448  SeeAlso     []
2449
2450******************************************************************************/
2451
2452void PuresatMarkVisibleVarWithVPGV(Ntk_Network_t *network,
2453                                  array_t * visibleArray,
2454                                  PureSat_Manager_t *pm,
2455                                  int from,
2456                                  int to)
2457{
2458
2459  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
2460  st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
2461                                                         MVFAIG_NETWORK_APPL_KEY);
2462  MvfAig_Function_t *mvfAig;
2463  bAigTimeFrame_t * tf = manager->timeframeWOI;
2464  mAigMvar_t lmVar;
2465  mAigBvar_t bVar;
2466  array_t *bVarList,*mVarList;
2467  int i,j,k,lmAigId,index,index1;
2468  char * name;
2469  Ntk_Node_t * latch;
2470  bAigEdge_t node,v, *li, *bli;
2471
2472  bVarList = mAigReadBinVarList(manager);
2473  mVarList = mAigReadMulVarList(manager);
2474
2475  /*Although some SV in tf 0 are not marked as visiblevar,
2476    //they actually visible since all SV of tf 0 are visible*/
2477  if(from<0)
2478    from=0;
2479  if(to>pm->Length+1)
2480    to=pm->Length+1;
2481
2482  /*clean VPGV mask*/
2483  li = tf->latchInputs[1];
2484  bli = tf->blatchInputs[1];
2485  for(j=0;j<tf->nLatches;j++)
2486    flags(li[j])&=ResetVPGVMask;
2487  for(j=0;j<tf->nbLatches;j++)
2488    flags(bli[j])&=ResetVPGVMask;
2489
2490  for(i=from;i<=to;i++){
2491    li = tf->latchInputs[i];
2492    bli = tf->blatchInputs[i];
2493    arrayForEachItem(char *,visibleArray,k,name){
2494      int retVal;
2495      latch = Ntk_NetworkFindNodeByName(network,name);
2496      st_lookup(node2MvfAigTable,latch,&mvfAig);
2497      for(j=0;j<mvfAig->num;j++){
2498        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
2499        if(v==bAig_Zero||v==bAig_One)
2500          continue;
2501        retVal = st_lookup(tf->li2index,(char*)v,&index);
2502        assert(retVal);
2503        if(li[index]==bAig_Zero||li[index]==bAig_One)
2504          continue;
2505        node = bAig_NonInvertedEdge(li[index]);
2506        manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
2507        /*marking PGV*/
2508        if(i==1){
2509          if(!st_lookup(pm->vertexTable,name,NIL(char*))){
2510            flags(node) |= VPGVMask;
2511
2512          }
2513        }
2514      }
2515
2516
2517      lmAigId = Ntk_NodeReadMAigId(latch);
2518      lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
2519      for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
2520        int retVal;
2521        bVar = array_fetch(mAigBvar_t,bVarList,index1);
2522        if(bVar.node==bAig_Zero||bVar.node==bAig_One)
2523          continue;
2524        retVal = st_lookup(tf->bli2index,(char*)bVar.node,&index);
2525        assert(retVal);
2526        if(bli[index]==bAig_Zero||bli[index]==bAig_One)
2527          continue;
2528        node = bAig_NonInvertedEdge(bli[index]);
2529        manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
2530        /*marking PGV*/
2531        if(i==1){
2532          if(!st_lookup(pm->vertexTable,name,NIL(char*)))
2533            flags(node) |= VPGVMask;
2534        }
2535      }
2536    }
2537  }
2538  return;
2539
2540}
2541
2542
2543/**Function********************************************************************
2544
2545  Synopsis    [Mark visible latch variables]
2546
2547  Description []
2548
2549  SideEffects []
2550
2551  SeeAlso     []
2552
2553******************************************************************************/
2554
2555void PuresatMarkVisibleVar(Ntk_Network_t *network,
2556                           array_t * visibleArray,
2557                           PureSat_Manager_t *pm,
2558                           int from,
2559                           int to)
2560{
2561
2562  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
2563  st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
2564                                                         MVFAIG_NETWORK_APPL_KEY);
2565  MvfAig_Function_t *mvfAig;
2566  bAigTimeFrame_t * tf = manager->timeframeWOI;
2567  mAigMvar_t lmVar;
2568  mAigBvar_t bVar;
2569  array_t *bVarList,*mVarList;
2570  int i,j,k,lmAigId,index,index1;
2571  char * name;
2572  Ntk_Node_t * latch;
2573  bAigEdge_t node,v, *li, *bli;
2574
2575  bVarList = mAigReadBinVarList(manager);
2576  mVarList = mAigReadMulVarList(manager);
2577
2578
2579  if(from<0)
2580    from=0;
2581  if(to>pm->Length+1)
2582    to=pm->Length+1;
2583
2584  for(i=from;i<=to;i++){
2585    li = tf->latchInputs[i];
2586    bli = tf->blatchInputs[i];
2587    arrayForEachItem(char *,visibleArray,k,name){
2588      latch = Ntk_NetworkFindNodeByName(network,name);
2589      st_lookup(node2MvfAigTable,latch,&mvfAig);
2590      /*multi val var*/
2591      for(j=0;j<mvfAig->num;j++){
2592        int retVal;
2593        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
2594        if(v==bAig_Zero||v==bAig_One)
2595          continue;
2596        retVal = st_lookup(tf->li2index,(char*)v,&index);
2597        assert(retVal);
2598        if(li[index]==bAig_Zero||li[index]==bAig_One)
2599          continue;
2600        node = bAig_NonInvertedEdge(li[index]);
2601        manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
2602      }
2603
2604      /*binary var*/
2605      lmAigId = Ntk_NodeReadMAigId(latch);
2606      lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
2607      for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
2608        int retVal;
2609        bVar = array_fetch(mAigBvar_t,bVarList,index1);
2610        if(bVar.node==bAig_Zero||bVar.node==bAig_One)
2611          continue;
2612        retVal = st_lookup(tf->bli2index,(char*)bVar.node,&index);
2613        assert(retVal);
2614        if(bli[index]==bAig_Zero||bli[index]==bAig_One)
2615          continue;
2616        node = bAig_NonInvertedEdge(bli[index]);
2617        manager->NodesArray[node+bAigFlags] |= VisibleVarMask;
2618      }
2619    }// arrayForEachItem(char *,visibleArray,k,name)
2620  }
2621
2622  return;
2623
2624}
2625
2626
2627/**Function********************************************************************
2628
2629  Synopsis    [Recursively mapping interpolant from a timeframe to another timeframe]
2630
2631  Description []
2632
2633  SideEffects []
2634
2635  SeeAlso     []
2636
2637******************************************************************************/
2638
2639bAigEdge_t PureSat_MapIPRecur(mAig_Manager_t *manager,
2640                         bAigEdge_t  node,
2641                         st_table * tmpTable)
2642{
2643  bAigEdge_t v,result,left,right;
2644  int isInverted;
2645
2646#if DBG
2647  assert(node!=bAig_NULL);
2648#endif
2649  if(node == bAig_One || node == bAig_Zero){
2650    return node;
2651  }
2652
2653  if(st_lookup(tmpTable,(char *)bAig_NonInvertedEdge(node),&v)){
2654    if(bAig_IsInverted(node))
2655      result = bAig_Not(v);
2656    else
2657      result = v;
2658
2659    return result;
2660  }
2661
2662  left = PureSat_MapIPRecur(manager,leftChild(node),tmpTable);
2663  right = PureSat_MapIPRecur(manager,rightChild(node),tmpTable);
2664
2665  v = PureSat_And(manager,left,right);
2666  isInverted = bAig_IsInverted(node);
2667  result = isInverted ? bAig_Not(v) : v;
2668  st_insert(tmpTable,(char *)bAig_NonInvertedEdge(node),(char *)v);
2669
2670  //fprintf(vis_stdout,"return %d->%d\n",node,result);
2671  return result;
2672}
2673
2674
2675
2676/**Function********************************************************************
2677
2678  Synopsis    [Maping interpolant from a timeframe to another timeframe]
2679
2680  Description []
2681
2682  SideEffects []
2683
2684  SeeAlso     []
2685
2686******************************************************************************/
2687
2688bAigEdge_t PureSat_MapIP(mAig_Manager_t *manager,
2689                         bAigEdge_t node,
2690                         int from,
2691                         int to)
2692{
2693  bAigTimeFrame_t *tf = manager->timeframeWOI;
2694  st_table *tmpTable = st_init_table(st_numcmp,st_numhash);
2695  bAigEdge_t * L1,*L0,result,v1,v0;
2696  int i;
2697
2698  if(node==bAig_One||node==bAig_Zero)
2699    return node;
2700
2701  L1 = tf->latchInputs[from];
2702  L0 = tf->latchInputs[to];
2703  for(i=0;i<tf->nLatches;i++){
2704   v1 = L1[i];
2705   v0 = L0[i];
2706   if(SATisInverted(v1)){
2707     v1 = SATnot(v1);
2708     v0 = SATnot(v0);
2709   }
2710   st_insert(tmpTable,(char*)v1,(char*)v0);
2711
2712  }
2713  L1 = tf->blatchInputs[from];
2714  L0 = tf->blatchInputs[to];
2715  for(i=0;i<tf->nbLatches;i++){
2716    v1 = L1[i];
2717    v0 = L0[i];
2718    if(SATisInverted(v1)){
2719      v1 = SATnot(v1);
2720      v0 = SATnot(v0);
2721    }
2722    st_insert(tmpTable,(char*)v1,(char*)v0);
2723
2724  }
2725
2726  manager->class_ = to;
2727  result = PureSat_MapIPRecur(manager,node,tmpTable);
2728
2729  st_free_table(tmpTable);
2730
2731  return result;
2732}
2733
2734
2735/**Function********************************************************************
2736
2737  Synopsis    [process dummy nodes]
2738
2739  Description [In UNSAT core, there may be dummy nodes, but in manager,
2740               they don't exist any more. This funct is to mark them]
2741
2742  SideEffects []
2743
2744  SeeAlso     []
2745
2746******************************************************************************/
2747
2748void PureSatProcessDummy(bAig_Manager_t *manager,
2749                         satManager_t *cm,
2750                         RTnode_t  RTnode)
2751{
2752  int i;
2753  bAigEdge_t *lp,node;
2754  RTManager_t *rm = cm->rm;
2755
2756  if(RT_flag(RTnode)&RT_VisitedMask){
2757    return;
2758  }
2759  RT_flag(RTnode) |= RT_VisitedMask;
2760
2761  if(RT_pivot(RTnode)==0){ /*leaf*/
2762#if DBG
2763    assert(RT_oriClsIdx(RTnode)==0);
2764#endif
2765    if(RT_oriClsIdx(RTnode))
2766      lp = (long*)SATfirstLit(RT_oriClsIdx(RTnode));
2767    else
2768
2769      lp = RT_formula(RTnode) + cm->rm->fArray;
2770    for(i=0;i<RT_fSize(RTnode);i++,lp++){
2771      assert(*lp>0);/* not processed yet*/
2772      if(RT_oriClsIdx(RTnode))/*is CNF*/
2773        node = SATgetNode(*lp);
2774      else /*is AIG*/
2775        node = *lp;
2776      node = SATnormalNode(node);
2777      if(node>=manager->nodesArraySize){
2778#if DBG
2779        assert(flags(node)&DummyMask);
2780#endif
2781        *lp = DUMMY;
2782      }
2783    }
2784  } /*leaf*/
2785
2786  /*not leaf*/
2787  else{
2788    if(RT_pivot(RTnode)>=manager->nodesArraySize){
2789      int class_ = bAig_Class(RT_pivot(RTnode));
2790      RT_pivot(RTnode) = DUMMY+class_;
2791    }
2792    PureSatProcessDummy(manager,cm,RT_left(RTnode));
2793    PureSatProcessDummy(manager,cm,RT_right(RTnode));
2794  }
2795
2796  return ;
2797
2798}
2799
2800
2801/**Function********************************************************************
2802
2803  Synopsis    [Find an aig node from its name]
2804
2805  Description []
2806
2807  SideEffects []
2808
2809  SeeAlso     []
2810
2811******************************************************************************/
2812
2813
2814bAigEdge_t
2815PureSat_FindNodeByName(
2816  bAig_Manager_t *manager,
2817  nameType_t     *name,
2818  int bound)
2819{
2820
2821  bAigEdge_t node;
2822
2823  if (!st_lookup(manager->SymbolTableArray[bound], name, &node)){
2824    node = bAig_NULL;
2825  }
2826
2827  return bAig_GetCanonical(manager, node);
2828}
2829
2830
2831/**Function********************************************************************
2832
2833  Synopsis    [Create Aig for a ltl formula]
2834
2835  Description []
2836
2837  SideEffects []
2838
2839  SeeAlso     []
2840
2841******************************************************************************/
2842
2843bAigEdge_t
2844PureSatCreatebAigOfPropFormula(
2845    Ntk_Network_t *network,
2846    bAig_Manager_t *manager,
2847    int bound,
2848    Ctlsp_Formula_t *ltl,
2849    int withInitialState)
2850{
2851  int index;
2852  bAigEdge_t result, left, right, *li;
2853  bAigTimeFrame_t *timeframe;
2854
2855  if (ltl == NIL(Ctlsp_Formula_t))      return bAig_NULL;
2856  if (ltl->type == Ctlsp_TRUE_c)        return bAig_One;
2857  if (ltl->type == Ctlsp_FALSE_c)       return bAig_Zero;
2858
2859  assert(Ctlsp_isPropositionalFormula(ltl));
2860
2861  if(withInitialState) timeframe = manager->timeframe;
2862  else                 timeframe = manager->timeframeWOI;
2863
2864  if (ltl->type == Ctlsp_ID_c){
2865      char *nodeNameString  = Ctlsp_FormulaReadVariableName(ltl);
2866      char *nodeValueString = Ctlsp_FormulaReadValueName(ltl);
2867      Ntk_Node_t *node      = Ntk_NetworkFindNodeByName(network, nodeNameString);
2868
2869      Var_Variable_t *nodeVar;
2870      int             nodeValue;
2871
2872      MvfAig_Function_t  *tmpMvfAig;
2873      st_table           *nodeToMvfAigTable; /* maps each node to its mvfAig */
2874
2875      if (node == NIL(Ntk_Node_t)) {
2876        char   *nameKey;
2877        char   tmpName[100];
2878
2879        sprintf(tmpName, "%s_%d", nodeNameString, bound);
2880        nameKey = util_strsav(tmpName);
2881
2882        result  = PureSat_FindNodeByName(manager, nameKey,bound);
2883        if(result == bAig_NULL){
2884           result = PureSat_CreateVarNode(manager, nameKey);
2885        } else {
2886
2887          FREE(nameKey);
2888        }
2889        return result;
2890      }
2891
2892      nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
2893      assert(nodeToMvfAigTable != NIL(st_table));
2894
2895      tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
2896      if (tmpMvfAig ==  NIL(MvfAig_Function_t)){
2897          tmpMvfAig = Bmc_NodeBuildMVF(network, node);
2898          array_free(tmpMvfAig);
2899          tmpMvfAig = Bmc_ReadMvfAig(node, nodeToMvfAigTable);
2900      }
2901
2902      nodeVar = Ntk_NodeReadVariable(node);
2903      if (Var_VariableTestIsSymbolic(nodeVar)) {
2904        nodeValue = Var_VariableReadIndexFromSymbolicValue(nodeVar, nodeValueString);
2905        if ( nodeValue == -1 ) {
2906          (void) fprintf(vis_stderr, "Value specified in RHS is not in domain of variable\n");
2907          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
2908          return bAig_NULL;
2909        }
2910      }
2911      else {
2912        int check;
2913         check = StringCheckIsInteger(nodeValueString, &nodeValue);
2914         if( check == 0 ) {
2915          (void) fprintf(vis_stderr,"Illegal value in the RHS\n");
2916          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
2917          return bAig_NULL;
2918         }
2919         if( check == 1 ) {
2920          (void) fprintf(vis_stderr,"Value in the RHS is out of range of int\n");
2921          (void) fprintf(vis_stderr,"%s = %s", nodeNameString, nodeValueString);
2922          return bAig_NULL;
2923         }
2924         if ( !(Var_VariableTestIsValueInRange(nodeVar, nodeValue))) {
2925          (void) fprintf(vis_stderr,"Value specified in RHS is not in domain of variable\n");
2926          (void) fprintf(vis_stderr,"%s = %s\n", nodeNameString, nodeValueString);
2927          return bAig_NULL;
2928
2929         }
2930      }
2931      result = MvfAig_FunctionReadComponent(tmpMvfAig, nodeValue);
2932      result = bAig_GetCanonical(manager, result);
2933      if(st_lookup(timeframe->li2index, (char *)result, &index)) {
2934        li = timeframe->latchInputs[bound];
2935        result = bAig_GetCanonical(manager, li[index]);
2936      }
2937      else if(st_lookup(timeframe->o2index, (char *)result, &index)) {
2938        li = timeframe->outputs[bound];
2939        result = bAig_GetCanonical(manager, li[index]);
2940
2941      }
2942      else if(st_lookup(timeframe->i2index, (char *)result, &index)) {
2943        li = timeframe->internals[bound];
2944        result = bAig_GetCanonical(manager, li[index]);
2945
2946      }
2947      return result;
2948  }
2949
2950  left = PureSatCreatebAigOfPropFormula(network, manager, bound, ltl->left, withInitialState);
2951  if (left == bAig_NULL){
2952    return bAig_NULL;
2953  }
2954  right = PureSatCreatebAigOfPropFormula(network, manager, bound, ltl->right, withInitialState);
2955  if (right == bAig_NULL && ltl->type ==Ctlsp_NOT_c ){
2956    return bAig_Not(left);
2957  }
2958  else if(right == bAig_NULL) {
2959    return bAig_NULL;
2960  }
2961
2962  switch(ltl->type) {
2963
2964    case Ctlsp_OR_c:
2965      result = PureSat_Or(manager, left, right);
2966      break;
2967    case Ctlsp_AND_c:
2968      result = PureSat_And(manager, left, right);
2969      break;
2970    case Ctlsp_THEN_c:
2971      result = PureSat_Then(manager, left, right);
2972      break;
2973    case Ctlsp_EQ_c:
2974      result = PureSat_Eq(manager, left, right);
2975      break;
2976    case Ctlsp_XOR_c:
2977      result = PureSat_Xor(manager, left, right);
2978      break;
2979    default:
2980      fail("Unexpected type");
2981  }
2982  return result;
2983} /* BmcCirCUsCreatebAigOfPropFormula */
2984
2985
2986
2987
2988/**Function********************************************************************
2989
2990  Synopsis    [Mark all node between from and to with obj mask]
2991
2992  Description []
2993
2994  SideEffects []
2995
2996  SeeAlso     []
2997
2998******************************************************************************/
2999
3000
3001
3002void PureSatMarkObj(bAig_Manager_t * manager,
3003                    long from,
3004                    long to)
3005{
3006  long v;
3007
3008  for(v=from;v<=to;v+=bAigNodeSize)
3009    flags(v)|=ObjMask;
3010}
3011
3012
3013
3014/**Function********************************************************************
3015
3016  Synopsis    [procedure of concretization]
3017
3018  Description []
3019
3020  SideEffects []
3021
3022  SeeAlso     []
3023
3024******************************************************************************/
3025
3026
3027boolean PureSat_ConcretTest(Ntk_Network_t *network,
3028                            PureSat_Manager_t *pm,
3029                            array_t *sufArray,
3030                            bAigEdge_t property,
3031                            array_t *previousResultArray,
3032                            int Con,
3033                            int satStat,
3034                            int inc)
3035{
3036  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
3037  int status,i,nodes_in_coi=0;
3038  satManager_t *cm;
3039  char *name;
3040  double t1,t2;
3041  satArray_t *saved;
3042  st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
3043  bAigEdge_t from,*lp;
3044
3045   arrayForEachItem(char *,sufArray,i,name){
3046    st_insert(SufAbsNameTable,name,(char*)0);
3047   }
3048
3049   manager->assertArray = sat_ArrayAlloc(1);
3050  sat_ArrayInsert(manager->assertArray,manager->InitState);
3051  cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
3052
3053  cm->option->coreGeneration = 0;
3054  cm->option->RT = 0;
3055  cm->option->AbRf = 1;
3056  if(inc){
3057    cm->option->incTraceObjective = 1;
3058    cm->savedConflictClauses = pm->savedConCls;
3059    pm->savedConCls = 0;
3060  }
3061  t1 = util_cpu_ctime();
3062  PureSat_CleanMask(manager,ResetVisibleVarMask);
3063  PuresatMarkVisibleVar(network,sufArray,pm,0,pm->Length+1);
3064  if(!Con){
3065    from = manager->nodesArraySize;
3066    PureSatSetCOI(network,pm,cm,SufAbsNameTable,0,pm->Length,pm->Length);
3067    PureSatKillPseudoGV(network,pm,SufAbsNameTable,1,pm->Length);
3068    if(inc){
3069      PureSatMarkObj(manager,from,manager->nodesArraySize-bAigNodeSize);
3070    }
3071    PureSat_ResetManager(manager,cm,0);
3072    PureSatProcessFanout(cm);
3073  }
3074  else{
3075    sat_MarkTransitiveFaninForNode(cm,property,CoiMask);
3076    sat_MarkTransitiveFaninForNode(cm,manager->InitState,CoiMask);
3077    cm->option->AbRf = 0;
3078  }
3079  t2 = util_cpu_ctime();
3080  pm->tPro += t2-t1;
3081  if(pm->verbosity>=2)
3082    fprintf(vis_stdout,"process time:%g,total:%g\n",
3083           (double)((t2-t1)/1000.0),pm->tPro/1000);
3084  if(pm->verbosity>=1){
3085    nodes_in_coi = PureSat_CountNodesInCoi(cm);
3086    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
3087  }
3088  st_free_table(SufAbsNameTable);
3089  manager->assertArray2 = cm->assertArray2;
3090  sat_Main(cm);
3091  if(satStat)
3092    sat_ReportStatistics(cm,cm->each);
3093  cm->option->AbRf = 1;
3094  manager->NodesArray = cm->nodesArray;
3095  t1 = util_cpu_ctime();
3096  if(!Con){
3097    PureSatRecoverFanout(cm,pm);
3098    PureSat_RestoreAigForDummyNode(manager,pm->oldPos);
3099    PureSat_CleanMask(manager,ResetVisited3Mask);
3100  }
3101  /*record conflict*/
3102  if(inc && cm->savedConflictClauses ){
3103    if(!Con){
3104      int num=0;
3105      saved = cm->savedConflictClauses;
3106      pm->savedConCls = sat_ArrayAlloc(1);
3107      for(i=0, lp=saved->space; i<saved->num; i++, lp++){
3108        sat_ArrayInsert(pm->savedConCls,*lp);
3109        if(*lp<0)
3110          num++;
3111      }
3112      assert(num%2==0);
3113      if(pm->verbosity>=2)
3114        fprintf(vis_stdout,"record %d ConCls for incremental concretization\n",num/2);
3115    }
3116    else
3117      pm->savedConCls = 0;
3118    sat_ArrayFree(cm->savedConflictClauses);
3119    cm->savedConflictClauses = 0;
3120  }
3121  t2 = util_cpu_ctime();
3122  pm->tPro += t2-t1;
3123  if(pm->verbosity>=2)
3124    fprintf(vis_stdout,"process time:%g,total:%g\n",
3125           (double)((t2-t1)/1000.0),pm->tPro/1000);
3126  sat_ArrayFree(manager->assertArray);
3127  status = cm->status;
3128  cm->option->coreGeneration = 1;
3129  PureSat_SatFreeManager(cm);
3130  if(status == SAT_SAT){
3131    if(pm->verbosity>=1)
3132      fprintf(vis_stdout,"CEX exist\n");
3133    return FALSE; /* cex exists*/
3134  }
3135  else{
3136    if(pm->verbosity>=1)
3137      fprintf(vis_stdout,"no CEX\n");
3138    return TRUE;   /* no cex*/
3139  }
3140
3141}
3142
3143
3144
3145/**Function********************************************************************
3146
3147  Synopsis    [Concretization procedure for unsat proof-based refinement minimization]
3148
3149  Description []
3150
3151  SideEffects []
3152
3153  SeeAlso     []
3154
3155******************************************************************************/
3156
3157
3158
3159boolean PureSat_ConcretTest_Core(Ntk_Network_t *network,
3160                                 PureSat_Manager_t *pm,
3161                                 array_t *sufArray,
3162                                 bAigEdge_t property,
3163                                 array_t *previousResultArray,
3164                                 st_table * junkTable)
3165{
3166  mAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
3167  int status,i,nodes_in_coi=0;
3168  satManager_t *cm;
3169  char *name;
3170  double t1,t2;
3171  st_table * SufAbsNameTable = st_init_table(strcmp,st_strhash);
3172  array_t * tmpRef1;
3173  st_table *refTable = st_init_table(strcmp,st_strhash);
3174
3175  arrayForEachItem(char *,sufArray,i,name){
3176    st_insert(SufAbsNameTable,name,(char*)0);
3177  }
3178
3179  manager->assertArray = sat_ArrayAlloc(1);
3180  sat_ArrayInsert(manager->assertArray,manager->InitState);
3181  cm = PureSat_SatManagerAlloc_WOCOI(manager,pm,property,previousResultArray);
3182  cm->option->coreGeneration = 1;
3183  cm->option->AbRf = 1;
3184  cm->option->IP = 1;
3185  t1 = util_cpu_ctime();
3186  PureSat_CleanMask(manager,ResetVisibleVarMask);
3187  PuresatMarkVisibleVarWithVPGV(network,sufArray,pm,0,pm->Length+1);
3188
3189    PureSatSetCOI(network,pm,cm,SufAbsNameTable,0,pm->Length,pm->Length);
3190    PureSatKillPseudoGV(network,pm,SufAbsNameTable,1,pm->Length);
3191    PureSat_ResetManager(manager,cm,0);
3192    PureSatProcessFanout(cm);
3193
3194  t2 = util_cpu_ctime();
3195  pm->tPro += t2-t1;
3196  if(pm->verbosity>=2)
3197    fprintf(vis_stdout,"process time:%g,total:%g\n",
3198           (double)((t2-t1)/1000.0),pm->tPro/1000);
3199  if(pm->verbosity>=1){
3200    nodes_in_coi = PureSat_CountNodesInCoi(cm);
3201    fprintf(vis_stdout,"There are %d node in COI\n",nodes_in_coi);
3202  }
3203  manager->assertArray2 = cm->assertArray2;
3204  sat_Main(cm);
3205  manager->NodesArray = cm->nodesArray;
3206  t1 = util_cpu_ctime();
3207    PureSatRecoverFanout(cm,pm);
3208    PureSat_RestoreAigForDummyNode(manager,pm->oldPos);
3209    PureSat_CleanMask(manager,ResetVisited3Mask);
3210    if(cm->status==SAT_UNSAT){
3211      PureSatProcessDummy(manager,cm,cm->rm->root);
3212      ResetRTree(cm->rm);
3213    }
3214  t2 = util_cpu_ctime();
3215  pm->tPro += t2-t1;
3216  if(pm->verbosity>=2)
3217    fprintf(vis_stdout,"process time:%g,total:%g\n",
3218           (double)((t2-t1)/1000.0),pm->tPro/1000);
3219
3220  if(cm->status==SAT_UNSAT){
3221    tmpRef1 = PureSat_GetSufAbsFromCore(network,cm,pm,property,SufAbsNameTable);
3222
3223    arrayForEachItem(char*,tmpRef1,i,name)
3224      st_insert(refTable,name,(char*)0);
3225
3226    arrayForEachItem(char*,sufArray,i,name){
3227      if(!st_lookup(refTable,name,NIL(char*))&&
3228         !st_lookup(pm->vertexTable,name,NIL(char*))){
3229        if(pm->verbosity>=2)
3230          fprintf(vis_stdout,"%s can be gotten rid of\n",name);
3231        st_insert(junkTable,name,(char*)0);
3232      }
3233    }
3234    array_free(tmpRef1);
3235  }
3236
3237  st_free_table(SufAbsNameTable);
3238  st_free_table(refTable);
3239  RT_Free(cm->rm);
3240  sat_ArrayFree(manager->assertArray);
3241  status = cm->status;
3242  cm->option->coreGeneration = 1;
3243  PureSat_SatFreeManager(cm);
3244  if(status == SAT_SAT){
3245    if(pm->verbosity>=1)
3246      fprintf(vis_stdout,"CEX exist\n");
3247    return FALSE; // cex exists
3248  }
3249  else{
3250    if(pm->verbosity>=1)
3251      fprintf(vis_stdout,"no CEX\n");
3252    return TRUE;   // no cex
3253  }
3254
3255}
3256
3257
3258/**Function********************************************************************
3259
3260  Synopsis    [Generate BFS ring for a network node]
3261
3262  Description []
3263
3264  SideEffects []
3265
3266  SeeAlso     []
3267
3268******************************************************************************/
3269
3270
3271void PureSatGenerateRingForNode(Ntk_Network_t *network,
3272                                PureSat_Manager_t *pm,
3273                                Ntk_Node_t * node1,
3274                                array_t * ringArray,
3275                                int *dfs)
3276{
3277  Ntk_Node_t *node;
3278  char *name;
3279  int i;
3280
3281  if(PureSatNodeReadColor(node1) == dfsBlack_c)
3282    return;
3283  PureSatNodeSetColor(node1,dfsBlack_c);
3284  if(Ntk_NodeTestIsLatch(node1)){
3285    name = Ntk_NodeReadName(node1);
3286    st_insert(pm->node2dfsTable,name,(char*)(long)(*dfs));
3287    array_insert_last(char *,ringArray,name);
3288    return;
3289  }
3290
3291  Ntk_NodeForEachFanin(node1,i,node){
3292    PureSatGenerateRingForNode(network,pm,node,ringArray,
3293                               dfs);
3294  }
3295  return;
3296}
3297
3298
3299/**Function********************************************************************
3300
3301  Synopsis    [Generate BFS ring for one array]
3302
3303  Description []
3304
3305  SideEffects []
3306
3307  SeeAlso     []
3308
3309******************************************************************************/
3310
3311array_t * PureSatGenerateRing(Ntk_Network_t *network,
3312                              PureSat_Manager_t *pm,
3313                              array_t * coreArray,
3314                              int * dfs)
3315{
3316  array_t * ringArray = array_alloc(char *,0);
3317  int i,j;
3318  char *name;
3319  Ntk_Node_t *node1,*node;
3320
3321  arrayForEachItem(char *,coreArray,i,name){
3322    node1 = Ntk_NetworkFindNodeByName(network,name);
3323    Ntk_NodeForEachFanin(node1,j,node){
3324      PureSatGenerateRingForNode(network,pm,node,
3325                                 ringArray,dfs);
3326    }
3327  }
3328  return ringArray;
3329}
3330
3331
3332/**Function********************************************************************
3333
3334  Synopsis    [Generate the ring information for the whole circuit]
3335
3336  Description []
3337
3338  SideEffects []
3339
3340  SeeAlso     []
3341
3342******************************************************************************/
3343
3344void PureSatGenerateDfs(Ntk_Network_t *network,
3345                        PureSat_Manager_t *pm,
3346                        array_t * vertexArray)
3347{
3348
3349  int dfs = 1,i,ct=0;
3350  char *name;
3351  Ntk_Node_t *node;
3352  array_t * ringArray = array_alloc(char *,0);
3353  array_t * coreArray;
3354  lsGen gen;
3355  st_generator * stgen;
3356
3357  Ntk_NetworkForEachNode( network, gen, node ) {
3358    PureSatNodeSetColor( node, dfsWhite_c );
3359  }
3360
3361  arrayForEachItem(char *,vertexArray,i,name){
3362    st_insert(pm->node2dfsTable,name,(char*)(long)dfs);
3363    node = Ntk_NetworkFindNodeByName(network,name);
3364    PureSatNodeSetColor(node,dfsBlack_c);
3365    ct++;
3366  }
3367
3368  coreArray = array_dup(vertexArray);
3369
3370  while(coreArray->num>0){
3371    dfs++;
3372    ringArray = PureSatGenerateRing(network,pm,coreArray,
3373                                    &dfs);
3374    arrayForEachItem(char*,ringArray,i,name){
3375      st_insert(pm->node2dfsTable,name,(char*)(long)dfs);
3376
3377      ct++;
3378    }
3379    array_free(coreArray);
3380    coreArray = ringArray;
3381  }
3382
3383  st_foreach_item(pm->CoiTable,stgen,&node,NIL(char*)){
3384    name = Ntk_NodeReadName(node);
3385    if(!st_lookup(pm->node2dfsTable,name,NIL(char*))){
3386      st_insert(pm->node2dfsTable,name,(char*)LARGEDFS);
3387      if(pm->verbosity>=2)
3388        fprintf(vis_stdout,"%s LARGEDFS is inserted into node2dfsTable\n",name);
3389    }
3390  }
3391
3392  return;
3393
3394}
3395
3396/**Function********************************************************************
3397
3398  Synopsis    [Sort latch candidate based on BFS ring and RC information]
3399
3400  Description []
3401
3402  SideEffects []
3403
3404  SeeAlso     []
3405
3406******************************************************************************/
3407
3408
3409array_t * PureSatComputeOrder_2(Ntk_Network_t *network,
3410                              PureSat_Manager_t *pm,
3411                              array_t * vertexArray,
3412                              array_t * invisibleArray,
3413                              int * sccArray,
3414                              int * NumInSecondLevel)
3415{
3416
3417  array_t * RCArray;
3418
3419  PureSatGenerateDfs(network,pm,vertexArray);
3420  RCArray = PureSatGenerateRCArray_2(network,pm,invisibleArray,
3421                                   NumInSecondLevel);
3422
3423  return RCArray;
3424}
3425
3426
3427
3428/**Function********************************************************************
3429
3430  Synopsis    [Some latches have the same aig node, add them all to
3431  abstractions once one is added. ]
3432
3433  Description []
3434
3435  SideEffects []
3436
3437  SeeAlso     []
3438
3439******************************************************************************/
3440
3441void PureSatAddIdenLatchToAbs(Ntk_Network_t *network,
3442                              PureSat_Manager_t *pm,
3443                              array_t *nameArray)
3444{
3445  int i;
3446  st_generator * stgen;
3447  st_table* table;
3448  char *name,*name1;
3449  st_table *table1 = st_init_table(st_ptrcmp,st_ptrhash);
3450  array_t * tmpArray = array_alloc(char*,0);
3451
3452  st_foreach_item(pm->vertexTable,stgen,&name,NIL(char*))
3453    st_insert(table1,name,(char*)0);
3454  arrayForEachItem(char*,nameArray,i,name)
3455    st_insert(table1,name,(char*)0);
3456
3457  arrayForEachItem(char*,nameArray,i,name){
3458
3459    if(st_lookup(pm->IdenLatchTable,name,&table)){
3460      st_foreach_item(table,stgen,&name1,NIL(char*)){
3461        if(!st_lookup(table1,name1,NIL(char*))){
3462          st_insert(table1,name1,(char*)0);
3463          array_insert_last(char*,tmpArray,name1);
3464        }
3465      }
3466    }
3467  }
3468
3469  arrayForEachItem(char*,tmpArray,i,name){
3470    array_insert_last(char*,nameArray,name);
3471    if(pm->verbosity>=2)
3472      fprintf(vis_stdout,"add %s to refineArray\n",name);
3473  }
3474
3475  array_free(tmpArray);
3476  st_free_table(table1);
3477}
3478
3479
3480/**Function********************************************************************
3481
3482  Synopsis    [Create initial abstraction from aig]
3483
3484  Description []
3485
3486  SideEffects []
3487
3488  SeeAlso     []
3489
3490******************************************************************************/
3491void
3492PureSatCreateInitAbsByAIG(bAig_Manager_t *manager,
3493                          PureSat_Manager_t *pm,
3494                          bAigEdge_t node,
3495                          st_table * tmpTable)
3496{
3497  bAigTimeFrame_t * tf = manager->timeframeWOI;
3498  char * name;
3499  st_table * table;
3500  st_generator * stgen;
3501
3502  if(node==bAig_NULL)
3503    return;
3504
3505  node = bAig_NonInvertedEdge(node);
3506
3507  if(flags(node)&VisitedMask)
3508    return;
3509
3510  flags(node) |= VisitedMask;
3511
3512
3513  if(flags(node)&StateBitMask){
3514    if(!st_lookup(tf->MultiLatchTable,(char*)node,&table)){
3515      int retVal = st_lookup(tf->idx2name,(char*)node,&name);
3516      assert(retVal);
3517      if(!st_lookup(tmpTable,name,NIL(char*))){
3518        st_insert(tmpTable,name,(char*)0);
3519
3520      }
3521    }
3522    else{
3523      st_foreach_item(table,stgen,&name,NIL(char*)){
3524        if(!st_lookup(tmpTable,name,NIL(char*))){
3525          st_insert(tmpTable,name,(char*)0);
3526
3527        }
3528      }
3529    }
3530  }
3531
3532  if(flags(node)&StateBitMask)
3533    return;
3534
3535  PureSatCreateInitAbsByAIG(manager,pm,leftChild(node),tmpTable);
3536  PureSatCreateInitAbsByAIG(manager,pm,rightChild(node),tmpTable);
3537}
3538
3539
3540/**Function********************************************************************
3541
3542  Synopsis    [Get support latches for one aig node]
3543
3544  Description []
3545
3546  SideEffects []
3547
3548  SeeAlso     []
3549
3550******************************************************************************/
3551
3552
3553void
3554PureSat_GetLatchForNode(bAig_Manager_t *manager,
3555                        PureSat_Manager_t *pm,
3556                        bAigEdge_t node,
3557                        array_t * nameArray,
3558                        st_table *tmpTable,
3559                        int cut)
3560{
3561  bAigTimeFrame_t * tf = manager->timeframeWOI;
3562  char * name;
3563  st_table * table;
3564  st_generator * stgen;
3565
3566  if(node==bAig_NULL)
3567    return;
3568
3569  node = bAig_NonInvertedEdge(node);
3570
3571  if(flags(node)&VisitedMask)
3572    return;
3573
3574  flags(node) |= VisitedMask;
3575
3576
3577  if(flags(node)&StateBitMask){
3578    if(!st_lookup(tf->MultiLatchTable,(char*)node,&table)){
3579      int retVal = st_lookup(tf->idx2name,(char*)node,&name);
3580      assert(retVal);
3581      if(!st_lookup(tmpTable,name,NIL(char*))){
3582        st_insert(tmpTable,name,(char*)0);
3583        array_insert_last(char *,nameArray,name);
3584        if(pm->verbosity>=2)
3585          fprintf(vis_stdout,"insert %s\n",name);
3586      }
3587    }
3588    else{
3589      st_foreach_item(table,stgen,&name,NIL(char*)){
3590        if(!st_lookup(tmpTable,name,NIL(char*))){
3591          st_insert(tmpTable,name,(char*)0);
3592          array_insert_last(char *,nameArray,name);
3593          if(pm->verbosity>=2)
3594            fprintf(vis_stdout,"insert %s\n",name);
3595        }
3596      }
3597    }
3598  }
3599
3600  if(cut==2){
3601    if(flags(node)&Visited2Mask)
3602      return;
3603  }
3604  else{
3605    if(cut==1){
3606      if(flags(node)&Visited3Mask)
3607        return;
3608    }
3609    else{
3610      fprintf(vis_stdout,"wrong cut\n");
3611      exit(0);
3612    }
3613  }
3614
3615  PureSat_GetLatchForNode(manager,pm,leftChild(node),nameArray,tmpTable,cut);
3616  PureSat_GetLatchForNode(manager,pm,rightChild(node),nameArray,tmpTable,cut);
3617}
3618
3619
3620/**Function********************************************************************
3621
3622  Synopsis    [Get COI reduction based on aig, not ntk]
3623
3624  Description []
3625
3626  SideEffects []
3627
3628  SeeAlso     []
3629
3630******************************************************************************/
3631
3632st_table * PureSatGetAigCoi(Ntk_Network_t *network,
3633                            PureSat_Manager_t *pm,
3634                            bAigEdge_t property)
3635{
3636  bAig_Manager_t *manager;
3637  st_table * node2MvfAigTable,*tmpTable;
3638  array_t * nameArray,*nameArray1;
3639  bAigTimeFrame_t *tf;
3640  char * name;
3641  Ntk_Node_t *latch;
3642  MvfAig_Function_t *mvfAig;
3643  mAigMvar_t lmVar;
3644  mAigBvar_t bVar;
3645  array_t *bVarList,*mVarList;
3646  int i,j,lmAigId;
3647  long index,index1;
3648  bAigEdge_t v, *li, *bli;
3649
3650  manager = Ntk_NetworkReadMAigManager(network);
3651  if (manager == NIL(mAig_Manager_t)) {
3652    (void) fprintf(vis_stdout,
3653                   "** bmc error: run build_partition_maigs command first\n");
3654    exit(0);;
3655  }
3656  node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
3657                                    MVFAIG_NETWORK_APPL_KEY);
3658  tf = manager->timeframeWOI;
3659
3660  bVarList = mAigReadBinVarList(manager);
3661  mVarList = mAigReadMulVarList(manager);
3662
3663  assert(manager->timeframeWOI->currentTimeframe>=2);
3664  PureSat_CleanMask(manager,ResetVisitedMask);
3665  PureSat_CleanMask(manager,ResetVisited2Mask);
3666  PureSat_CleanMask(manager,ResetVisited3Mask);
3667  li = tf->latchInputs[1];
3668  for(i=0;i<tf->nLatches;i++)
3669    flags(li[i])|=Visited3Mask;
3670  li = tf->blatchInputs[1];
3671  for(i=0;i<tf->nbLatches;i++)
3672    flags(li[i])|=Visited3Mask;
3673  li = tf->latchInputs[2];
3674  for(i=0;i<tf->nLatches;i++)
3675    flags(li[i])|=Visited2Mask;
3676  li = tf->blatchInputs[2];
3677  for(i=0;i<tf->nbLatches;i++)
3678    flags(li[i])|=Visited2Mask;
3679
3680  nameArray = array_alloc(char *,0);
3681  tmpTable = st_init_table(st_ptrcmp,st_ptrhash);
3682  PureSat_GetLatchForNode(manager,pm,property,nameArray,tmpTable,2);
3683  PureSat_CleanMask(manager,ResetVisitedMask);
3684
3685
3686  li = tf->latchInputs[2];
3687  bli = tf->blatchInputs[2];
3688  while(nameArray->num>0){
3689    nameArray1 = nameArray;
3690    nameArray = array_alloc(char *,0);
3691    arrayForEachItem(char*,nameArray1,i,name){
3692      latch = Ntk_NetworkFindNodeByName(network,name);
3693      st_lookup(node2MvfAigTable,latch,&mvfAig);
3694      for(j=0;j<mvfAig->num;j++){
3695        int retVal;
3696        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
3697        if(v==bAig_Zero||v==bAig_One)
3698          continue;
3699        retVal = st_lookup(tf->li2index,(char*)v,&index);
3700        assert(retVal);
3701        if(li[index]==bAig_Zero||li[index]==bAig_One)
3702          continue;
3703        PureSat_GetLatchForNode(manager,pm,li[index],nameArray,tmpTable,1);
3704      }
3705
3706
3707      lmAigId = Ntk_NodeReadMAigId(latch);
3708      lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
3709      for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
3710        int retVal;
3711        bVar = array_fetch(mAigBvar_t,bVarList,index1);
3712        if(bVar.node==bAig_Zero||bVar.node==bAig_One)
3713          continue;
3714        retVal = st_lookup(tf->bli2index,(char*)bVar.node,&index);
3715        assert(retVal);
3716        if(bli[index]==bAig_Zero||bli[index]==bAig_One)
3717          continue;
3718        PureSat_GetLatchForNode(manager,pm,bli[index],nameArray,tmpTable,1);
3719      }
3720    }
3721
3722    array_free(nameArray1);
3723  }
3724
3725  array_free(nameArray);
3726  PureSat_CleanMask(manager,ResetVisitedMask);
3727  PureSat_CleanMask(manager,ResetVisited2Mask);
3728  PureSat_CleanMask(manager,ResetVisited3Mask);
3729
3730  return tmpTable;
3731}
3732
3733
3734/**Function********************************************************************
3735
3736  Synopsis    [There are some latches whose DI is empty, put them
3737  into abstraction will not add any burden to model checker]
3738
3739  Description []
3740
3741  SideEffects []
3742
3743  SeeAlso     []
3744
3745******************************************************************************/
3746
3747
3748void PureSatPreProcLatch(Ntk_Network_t *network,
3749                         PureSat_Manager_t *pm)
3750{
3751  st_generator * stgen;
3752  bAig_Manager_t * manager = Ntk_NetworkReadMAigManager(network);
3753  st_table * node2MvfAigTable =(st_table *) Ntk_NetworkReadApplInfo(network,
3754                                                         MVFAIG_NETWORK_APPL_KEY);
3755  bAigTimeFrame_t * tf = manager->timeframeWOI;
3756  mAigMvar_t lmVar;
3757  mAigBvar_t bVar;
3758  array_t *bVarList,*mVarList;
3759  int j,lmAigId,id,index1;
3760  char * name;
3761  Ntk_Node_t * latch;
3762  bAigEdge_t v, **li, **bli;
3763  MvfAig_Function_t *mvfAig;
3764
3765  bVarList = mAigReadBinVarList(manager);
3766  mVarList = mAigReadMulVarList(manager);
3767  li = tf->latchInputs;
3768  bli = tf->blatchInputs;
3769
3770  st_foreach_item(pm->CoiTable,stgen,&latch,NIL(char*)){
3771    int checkbin=1;
3772    st_lookup(node2MvfAigTable,latch,&mvfAig);
3773    for(j=0;j<mvfAig->num;j++){
3774      int retVal;
3775      v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig,j));
3776      if(v==bAig_Zero||v==bAig_One)
3777        continue;
3778      retVal = st_lookup(tf->li2index,(char*)v,&id);
3779      assert(retVal);
3780      if(li[0][id]==li[1][id]&&li[1][id]==li[2][id]){
3781        name = Ntk_NodeReadName(latch);
3782        st_insert(pm->vertexTable,name,(char*)0);
3783        if(pm->verbosity>=2)
3784          fprintf(vis_stdout,"preproc: add %s to abs\n",name);
3785        checkbin = 0;
3786        break;
3787      }
3788    }
3789    if(checkbin){
3790      lmAigId = Ntk_NodeReadMAigId(latch);
3791      lmVar = array_fetch(mAigMvar_t, mVarList,lmAigId);
3792      for(j=0,index1=lmVar.bVars;j<lmVar.encodeLength;j++,index1++){
3793        int retVal;
3794        bVar = array_fetch(mAigBvar_t,bVarList,index1);
3795        if(bVar.node==bAig_Zero||bVar.node==bAig_One)
3796          continue;
3797        retVal = st_lookup(tf->bli2index,(char*)bVar.node,&id);
3798        assert(retVal);
3799        if(bli[0][id]==bli[1][id]&&bli[1][id]==bli[2][id]){
3800          name = Ntk_NodeReadName(latch);
3801          st_insert(pm->vertexTable,name,(char*)0);
3802          if(pm->verbosity>=2)
3803            fprintf(vis_stdout,"preproc BINARY: add %s to abs\n",name);
3804          break;
3805        }
3806      }
3807    }
3808  }
3809
3810}
3811
3812
3813/**Function********************************************************************
3814
3815  Synopsis    [Generate identical latch clusters]
3816
3817  Description []
3818
3819  SideEffects []
3820
3821  SeeAlso     []
3822
3823******************************************************************************/
3824
3825void PureSatGetIndenticalLatch(Ntk_Network_t *network,
3826                               PureSat_Manager_t *pm)
3827{
3828  bAig_Manager_t *manager = Ntk_NetworkReadMAigManager(network);
3829  bAigTimeFrame_t * tf = manager->timeframeWOI;
3830  bAigEdge_t *li=tf->latchInputs[2],*bli = tf->blatchInputs[2];
3831  int i;
3832  bAigEdge_t v;
3833  st_table *table;
3834  st_generator *stgen,*stgen1;
3835  char *name,*name1;
3836  st_table *table2,*table1=st_init_table(st_ptrcmp,st_ptrhash);
3837
3838  pm->IdenLatchTable = st_init_table(st_ptrcmp,st_ptrhash);
3839
3840  for(i=0;i<tf->nLatches;i++){
3841    v=bAig_NonInvertedEdge(li[i]);
3842    if(!st_lookup(table1,(char*)v,NIL(char*))){
3843      if(st_lookup(tf->MultiLatchTable,(char*)v,&table)){
3844        int init=0;
3845        st_foreach_item(table,stgen,&name,NIL(char*)){
3846          if(!st_lookup(pm->IdenLatchTable,name,&table2)){
3847            st_insert(pm->IdenLatchTable,name,table);
3848            if(pm->verbosity>=2)
3849              fprintf(vis_stdout,"%s and ",name);
3850            init = 1;
3851          }
3852          /*insert everything in table 2 into table
3853          name is already in another group, put everything of current group
3854          into that group*/
3855          else{
3856            st_foreach_item(table,stgen1,&name1,NIL(char*)){
3857              st_insert(table2,name1,(char*)0);
3858              st_insert(pm->IdenLatchTable,name1,table2);
3859              if(pm->verbosity>=2)
3860                fprintf(vis_stdout,"%s and ",name1);
3861            }
3862            if(pm->verbosity>=2)
3863              fprintf(vis_stdout,"are the same\n");
3864            break;
3865          }
3866        }
3867        if(init){
3868          if(pm->verbosity>=2)
3869            fprintf(vis_stdout,"are the same\n");
3870        }
3871      }
3872      st_insert(table1,(char*)v,(char*)0);
3873    }
3874  }
3875
3876
3877  for(i=0;i<tf->nbLatches;i++){
3878    v=bAig_NonInvertedEdge(bli[i]);
3879    if(!st_lookup(table1,(char*)v,NIL(char*))){
3880      if(st_lookup(tf->MultiLatchTable,(char*)v,&table)){
3881        int init=0;
3882        st_foreach_item(table,stgen,&name,NIL(char*)){
3883
3884          if(!st_lookup(pm->IdenLatchTable,name,table2)){
3885            st_insert(pm->IdenLatchTable,name,table);
3886            if(pm->verbosity>=2)
3887              fprintf(vis_stdout,"%s and ",name);
3888            init = 1;
3889          }
3890          /*insert everything in table 2 into table
3891          name is already in another group, put everything of current group
3892          into that group*/
3893          else{
3894            st_foreach_item(table,stgen1,&name1,NIL(char*)){
3895
3896              st_insert(table2,name1,(char*)0);
3897              st_insert(pm->IdenLatchTable,name1,table2);
3898              if(pm->verbosity>=2)
3899                fprintf(vis_stdout,"%s and ",name1);
3900            }
3901            if(pm->verbosity>=2)
3902              fprintf(vis_stdout,"are the same\n");
3903            break;
3904          }
3905        }
3906        if(init){
3907          if(pm->verbosity>=2)
3908            fprintf(vis_stdout,"are the same\n");
3909        }
3910      }
3911      st_insert(table1,(char*)v,(char*)0);
3912    }
3913  }
3914
3915  st_free_table(table1);
3916}
Note: See TracBrowser for help on using the repository browser.