source: vis_dev/vis-2.3/src/puresat/puresatAig.c @ 101

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

vis2.3
File size: 24.4 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [puresatAig.c]
4
5  PackageName [puresat]
6
7  Synopsis    [Abstraction refinement for large scale invariant checking.]
8
9  Description [This file contains the functions to check invariant properties
10  by the PureSAT abstraction refinement algorithm, which is entirely based on
11  SAT solver, the input of which could be either CNF or AIG. It has several
12  parts:
13
14  * Localization-reduction base Abstraction
15  * K-induction or interpolation to prove the truth of a property
16  * Bounded Model Checking to find bugs
17  * Incremental concretization based methods to verify abstract bugs
18  * Incremental SAT solver to improve efficiency
19  * UNSAT proof based method to obtain refinement
20  * AROSAT to bring in only necessary latches into unsat proofs
21  * Bridge abstraction to get compact coarse refinement
22  * Refinement minization to guarrantee minimal refinements
23  * Unsat proof-based refinement minimization to eliminate multiple candidate
24    by on SAT test
25  * Refinement prediction to decrease the number of refinement iterations
26  * Dynamic switching to redistribute computional resources to improve
27    efficiency
28
29  For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05
30  paper of Li et al., "A satisfiability-based appraoch to abstraction
31  refinement in model checking", " Abstraction in symbolic model checking
32  using satisfiability as the only decision procedure", "Efficient computation
33  of small abstraction refinements", and "Efficient abstraction refinement in
34  interpolation-based unbounded model checking"]
35
36  Author      [Bing Li]
37
38  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
39  All rights reserved.
40
41  Permission is hereby granted, without written agreement and without
42  license or royalty fees, to use, copy, modify, and distribute this
43  software and its documentation for any purpose, provided that the
44  above copyright notice and the following two paragraphs appear in
45  all copies of this software.]
46
47******************************************************************************/
48#include "maigInt.h"
49#include "baig.h"
50#include "ntk.h"
51#include "puresatInt.h"
52/*---------------------------------------------------------------------------*/
53/* Constant declarations                                                     */
54/*---------------------------------------------------------------------------*/
55
56/*---------------------------------------------------------------------------*/
57/* Type declarations                                                         */
58/*---------------------------------------------------------------------------*/
59
60
61/*---------------------------------------------------------------------------*/
62/* Structure declarations                                                    */
63/*---------------------------------------------------------------------------*/
64
65
66/*---------------------------------------------------------------------------*/
67/* Variable declarations                                                     */
68/*---------------------------------------------------------------------------*/
69
70/*---------------------------------------------------------------------------*/
71/* Macro declarations                                                        */
72/*---------------------------------------------------------------------------*/
73
74/**AutomaticStart*************************************************************/
75
76/*---------------------------------------------------------------------------*/
77/* Static function prototypes                                                */
78/*---------------------------------------------------------------------------*/
79
80
81/**AutomaticEnd***************************************************************/
82
83/*---------------------------------------------------------------------------*/
84/* Definition of exported functions                                          */
85/*---------------------------------------------------------------------------*/
86
87
88/*---------------------------------------------------------------------------*/
89/* Definition of internal functions                                          */
90/*---------------------------------------------------------------------------*/
91
92/**Function********************************************************************
93
94  Synopsis    [For AIG recovery--unconnect output for nodes eliminated]
95
96  Description [For AIG recovery--unconnect output for nodes eliminated]
97
98  SideEffects []
99
100  SeeAlso     []
101
102******************************************************************************/
103
104void
105PureSat_unconnectOutput(
106   bAig_Manager_t *manager,
107   bAigEdge_t from,
108   bAigEdge_t to)
109{
110   bAigEdge_t cur, *pfan, *newfan;
111   int i, nfan,find=0;
112
113  from = bAig_NonInvertedEdge(from);
114  to = bAig_NonInvertedEdge(to);
115
116  pfan = (bAigEdge_t *)fanout(from);
117  nfan = nFanout(from);
118  newfan = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*(nfan));
119  for(i=0; i<nfan; i++) {
120    cur = pfan[i];
121    cur = cur >> 1;
122    cur = bAig_NonInvertedEdge(cur);
123    if(cur == to) {
124      find = 1;
125      memcpy(newfan, pfan, sizeof(bAigEdge_t)*i);
126      memcpy(&(newfan[i]), &(pfan[i+1]), sizeof(bAigEdge_t)*(nfan-i-1));
127      newfan[nfan-1] = 0;
128
129      fanout(from) = (bAigEdge_t)newfan;
130
131
132      free(pfan);
133      nFanout(from) = nfan-1;
134      break;
135    }
136  }
137  assert(find);
138}
139
140
141/**Function********************************************************************
142
143  Synopsis    [for AIG generation---create connection between new and
144              old aig nodes]
145
146  Description []
147
148  SideEffects []
149
150  SeeAlso     []
151
152******************************************************************************/
153
154void
155PureSat_connectOutput(
156   bAig_Manager_t *manager,
157   bAigEdge_t from,
158   bAigEdge_t to,
159   int inputIndex)
160{
161  bAigEdge_t *pfan;
162  bAigEdge_t nfan;
163
164  to = bAig_NonInvertedEdge(to);
165  pfan = (bAigEdge_t *)fanout(from);
166  nfan = nFanout(from);
167  if(nfan == 0) pfan = malloc((sizeof(bAigEdge_t)*2));
168  else          pfan = realloc(pfan, sizeof(bAigEdge_t)*(nfan+2));
169  to += bAig_IsInverted(from);
170  to = to << 1;
171  to += inputIndex;
172  pfan[nfan++] = to;
173  pfan[nfan] = 0;
174  fanout(from) = (bAigEdge_t)pfan;
175  nFanout(from) = nfan;
176}
177
178
179/**Function********************************************************************
180
181  Synopsis    [Check whether a node has been created or not]
182
183  Description []
184
185  SideEffects []
186
187  SeeAlso     []
188
189******************************************************************************/
190
191bAigEdge_t
192PureSat_HashTableLookup(
193  bAig_Manager_t *manager,
194  bAigEdge_t  node1,
195  bAigEdge_t  node2)
196{
197  bAigEdge_t key = HashTableFunction(node1, node2);
198  bAigEdge_t node;
199
200  node = manager->HashTableArray[manager->class_][key];
201  if  (node == bAig_NULL) {
202    return bAig_NULL;
203  }
204  else{
205    while ( (rightChild(bAig_NonInvertedEdge(node)) != node2) ||
206            (leftChild(bAig_NonInvertedEdge(node))  != node1)) {
207
208      if (next(bAig_NonInvertedEdge(node)) == bAig_NULL){
209        return(bAig_NULL);
210      }
211      node = next(bAig_NonInvertedEdge(node)); /* Get the next Node */
212    } /* While loop */
213    return(node);
214
215  } /* If Then Else */
216
217} /* End of HashTableLookup() */
218
219
220/**Function********************************************************************
221
222  Synopsis    [Add one new node to hash table]
223
224  Description []
225
226  SideEffects []
227
228  SeeAlso     []
229
230******************************************************************************/
231
232int
233PureSat_HashTableAdd(
234  bAig_Manager_t   *manager,
235  bAigEdge_t  nodeIndexParent,
236  bAigEdge_t  nodeIndex1,
237  bAigEdge_t  nodeIndex2)
238{
239  bAigEdge_t key = HashTableFunction(nodeIndex1, nodeIndex2);
240  bAigEdge_t nodeIndex;
241  bAigEdge_t node;
242
243  nodeIndex = manager->HashTableArray[manager->class_][key];
244  if  (nodeIndex == bAig_NULL) {
245    manager->HashTableArray[manager->class_][key] = nodeIndexParent;
246    return TRUE;
247  }
248  else{
249    node = nodeIndex;
250    nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));  /* Get the Node */
251    while (nodeIndex != bAig_NULL) {
252      node = nodeIndex;
253      nodeIndex = next(bAig_NonInvertedEdge(nodeIndex));
254    }
255    next(bAig_NonInvertedEdge(node)) = nodeIndexParent;
256    return TRUE;
257  }
258
259}
260
261
262
263/**Function********************************************************************
264
265  Synopsis    [Create a node for AND operation]
266
267  Description []
268
269  SideEffects []
270
271  SeeAlso     []
272
273******************************************************************************/
274
275bAigEdge_t
276PureSat_CreateAndNode(
277   bAig_Manager_t  *manager,
278   bAigEdge_t node1,
279   bAigEdge_t node2)
280{
281
282  bAigEdge_t varIndex;
283  char       *name = NIL(char);
284  char       *node1Str = util_inttostr(node1);
285  char       *node2Str = util_inttostr(node2);
286  long class_ = manager->class_;
287
288  name = util_strcat4("Nd", node1Str,"_", node2Str);
289  while (st_lookup(manager->SymbolTableArray[class_], name, &varIndex)){
290    fprintf(vis_stdout, "Find redundant node at %ld %ld\n", node1, node2);
291    name = util_strcat3(name, node1Str, node2Str);
292  }
293  FREE(node1Str);
294  FREE(node2Str);
295  varIndex = bAig_CreateNode(manager, node1, node2);
296  if (varIndex == bAig_NULL){
297    FREE(name);
298    return (varIndex);
299  }
300  /* Insert the varaible in the Symbol Table */
301  st_insert(manager->SymbolTableArray[class_], name, (char*) (long) varIndex);
302  manager->nameList[bAigNodeID(varIndex)] = name;
303
304  return(varIndex);
305
306}
307
308
309/**Function********************************************************************
310
311  Synopsis    [And function for 2 aig nodes]
312
313  Description []
314
315  SideEffects []
316
317  SeeAlso     []
318
319******************************************************************************/
320
321bAigEdge_t
322PureSat_And2(
323   bAig_Manager_t *manager,
324   bAigEdge_t nodeIndex1,
325   bAigEdge_t nodeIndex2)
326{
327  bAigEdge_t newNodeIndex;
328
329    newNodeIndex = PureSat_CreateAndNode(manager, nodeIndex1, nodeIndex2) ;
330
331    PureSat_HashTableAdd(manager, newNodeIndex, nodeIndex1, nodeIndex2);
332    PureSat_connectOutput(manager, nodeIndex1, newNodeIndex, 0);
333    PureSat_connectOutput(manager, nodeIndex2, newNodeIndex, 1);
334
335  return newNodeIndex;
336
337}
338
339
340/**Function********************************************************************
341
342  Synopsis    [And function for 3 aig nodes]
343
344  Description []
345
346  SideEffects []
347
348  SeeAlso     []
349
350******************************************************************************/
351
352bAigEdge_t
353PureSat_And3(
354           bAig_Manager_t *manager,
355           bAigEdge_t l,
356           bAigEdge_t r)
357{
358  int caseIndex, caseSig;
359  bAigEdge_t rl, rr;
360
361  rl = leftChild(r);
362  rr = rightChild(r);
363
364  caseIndex = 0; /* (a)(b c) */
365  if(bAigCompareNode(l, rl)) {
366    caseIndex = 1; /* (a)(a b) */
367  }
368  else if(bAigCompareNode(l, rr)) {
369    caseIndex = 2; /* (a)(b a) */
370  }
371
372  caseSig = 0;
373  if(bAig_IsInverted(l))  caseSig += 8;
374  if(bAig_IsInverted(rl)) caseSig += 4;
375  if(bAig_IsInverted(rr)) caseSig += 2;
376  if(bAig_IsInverted(r))  caseSig += 1;
377  if(caseIndex == 0) {
378    return(PureSat_And2(manager, l, r));
379  }
380  else if(caseIndex == 1) {
381    switch(caseSig) {
382        case 2 :
383        case 0 :
384        case 14 :
385        case 12 :
386      return(r);
387        case 10 :
388        case 8 :
389        case 6 :
390        case 4 :
391      return(bAig_Zero);
392        case 3 :
393        case 1 :
394        case 15 :
395        case 13 :
396      return(PureSat_And(manager, rl, bAig_Not(rr)));
397        case 11 :
398        case 9 :
399        case 7 :
400        case 5 :
401      return(l);
402    }
403  }
404  else if(caseIndex == 2) {
405    switch(caseSig) {
406        case 4 :
407        case 0 :
408        case 14 :
409        case 10 :
410      return(r);
411        case 12 :
412        case 8 :
413        case 6 :
414        case 2 :
415      return(bAig_Zero);
416        case 5 :
417        case 1 :
418        case 15 :
419        case 11 :
420      return(PureSat_And(manager, bAig_Not(rl), rr));
421        case 13 :
422        case 9 :
423        case 7 :
424        case 3 :
425      return(l);
426    }
427  }
428  return(0);
429}
430
431
432/**Function********************************************************************
433
434  Synopsis    [And function for 4 aig nodes]
435
436  Description []
437
438  SideEffects []
439
440  SeeAlso     []
441
442******************************************************************************/
443
444bAigEdge_t
445PureSat_And4(
446           bAig_Manager_t *manager,
447           bAigEdge_t l,
448           bAigEdge_t r)
449{
450  int caseIndex, caseSig;
451  bAigEdge_t ll, lr, rl, rr;
452  bAigEdge_t t1, t2;
453
454  ll = leftChild(l);
455  lr = rightChild(l);
456  rl = leftChild(r);
457  rr = rightChild(r);
458
459  if(bAigCompareNode(l, rl) ||
460     bAigCompareNode(l, rr)) {
461    return(PureSat_And3(manager, l, r));
462  }
463  else if(bAigCompareNode(r, ll) ||
464     bAigCompareNode(r, lr)) {
465    return(PureSat_And3(manager, r, l));
466  }
467
468  if(ll > lr+1) bAigSwap(ll, lr);
469  if(rl > rr+1) bAigSwap(rl, rr);
470
471  caseIndex = 0; /* (a b)(c d) */
472  if(bAigCompareNode(ll, rl)) {
473    if(bAigCompareNode(lr, rr)) {
474      caseIndex = 4; /* (a b) (a b) */
475    }
476    else {
477      caseIndex = 1; /* (a b) (a c) */
478      if(lr > rr+1) {
479        bAigSwap(ll, rl);
480        bAigSwap(lr, rr);
481        bAigSwap(l, r);
482      }
483    }
484  }
485  else if(bAigCompareNode(lr, rl)) {
486    caseIndex = 2; /* (b a)(a c) */
487  }
488  else if(bAigCompareNode(lr, rr)) {
489    caseIndex = 3; /* (b a)(c a) */
490    if(ll > rl+1) {
491      bAigSwap(ll, rl);
492      bAigSwap(lr, rr);
493      bAigSwap(l, r);
494    }
495  }
496  else if(bAigCompareNode(ll, rr)) {
497    /* (a b)(c a)  */
498    bAigSwap(ll, rl);
499    bAigSwap(lr, rr);
500    bAigSwap(l, r);
501    caseIndex = 2; /* (c a )(a b) because of c < b */
502  }
503
504  caseSig = 0;
505  if(bAig_IsInverted(ll)) caseSig += 32;
506  if(bAig_IsInverted(lr)) caseSig += 16;
507  if(bAig_IsInverted(l))  caseSig += 8;
508  if(bAig_IsInverted(rl)) caseSig += 4;
509  if(bAig_IsInverted(rr)) caseSig += 2;
510  if(bAig_IsInverted(r))  caseSig += 1;
511
512  if(caseIndex == 0) {
513    return(PureSat_And2(manager, l, r));
514  }
515  else if(caseIndex == 1) {
516    switch(caseSig) {
517        case 19 :
518        case 17 :
519        case 3 :
520        case 1 :
521        case 55 :
522        case 53 :
523        case 39 :
524        case 37 :
525      t1 = PureSat_And(manager, lr, bAig_Not(rr));
526      t2 = PureSat_And(manager, ll, t1);
527      return(t2);
528        case 18 :
529        case 16 :
530        case 2 :
531        case 0 :
532        case 54 :
533        case 52 :
534        case 38 :
535        case 36 :
536      t1 = PureSat_And(manager, lr, rr);
537      t2 = PureSat_And(manager, ll, t1);
538      return(t2);
539        case 26 :
540        case 24 :
541        case 10 :
542        case 8 :
543        case 62 :
544        case 60 :
545        case 46 :
546        case 44 :
547      t1 = PureSat_And(manager, bAig_Not(lr), rr);
548      t2 = PureSat_And(manager, ll, t1);
549      return(t2);
550        case 61 :
551        case 27 :
552        case 25 :
553        case 11 :
554        case 63 :
555        case 47 :
556        case 9 :
557        case 45 :
558      t1 = PureSat_And(manager, bAig_Not(lr), bAig_Not(rr));
559      t2 = PureSat_Or(manager, bAig_Not(ll), t1);
560      return(t2);
561        case 23 :
562        case 21 :
563        case 7 :
564        case 5 :
565        case 51 :
566        case 49 :
567        case 35 :
568        case 33 :
569      return(l);
570        case 30 :
571        case 28 :
572        case 14 :
573        case 12 :
574        case 58 :
575        case 56 :
576        case 42 :
577        case 40 :
578      return(r);
579        case 22 :
580        case 20 :
581        case 6 :
582        case 4 :
583        case 50 :
584        case 48 :
585        case 34 :
586        case 32 :
587      return(bAig_Zero);
588        case 31 :
589        case 29 :
590        case 15 :
591        case 13 :
592        case 59 :
593        case 57 :
594        case 43 :
595        case 41 :
596      t1 = PureSat_And2(manager, l, r);
597      return(t1);
598    }
599  }
600  else if(caseIndex == 2) {
601    switch(caseSig) {
602        case 35 :
603        case 33 :
604        case 3 :
605        case 1 :
606        case 55 :
607        case 53 :
608        case 23 :
609        case 21 :
610      t1 = PureSat_And(manager, lr, bAig_Not(rr));
611      t2 = PureSat_And(manager, ll, t1);
612      return(t2);
613        case 34 :
614        case 32 :
615        case 2 :
616        case 0 :
617        case 54 :
618        case 52 :
619        case 22 :
620        case 20 :
621      t1 = PureSat_And(manager, lr, rr);
622      t2 = PureSat_And(manager, ll, t1);
623      return(t2);
624        case 42 :
625        case 40 :
626        case 10 :
627        case 8 :
628        case 62 :
629        case 60 :
630        case 30 :
631        case 28 :
632      t1 = PureSat_And(manager, lr, rr);
633      t2 = PureSat_And(manager, bAig_Not(ll), t1);
634      return(t2);
635        case 43 :
636        case 41 :
637        case 11 :
638        case 9 :
639        case 63 :
640        case 61 :
641        case 31 :
642        case 29 :
643      t1 = PureSat_And(manager, bAig_Not(ll), bAig_Not(rr));
644      t2 = PureSat_Or(manager, bAig_Not(lr), t1);
645      return(t2);
646        case 39 :
647        case 37 :
648        case 7 :
649        case 5 :
650        case 51 :
651        case 49 :
652        case 19 :
653        case 17 :
654      return(l);
655        case 46 :
656        case 44 :
657        case 14 :
658        case 12 :
659        case 58 :
660        case 56 :
661        case 26 :
662        case 24 :
663      return(r);
664        case 38 :
665        case 36 :
666        case 6 :
667        case 4 :
668        case 50 :
669        case 48 :
670        case 18 :
671        case 16 :
672      return(bAig_Zero);
673        case 45 :
674        case 15 :
675        case 13 :
676        case 59 :
677        case 57 :
678        case 47 :
679        case 27 :
680        case 25 :
681      t1 = PureSat_And2(manager, l, r);
682      return(t1);
683    }
684  }
685  else if(caseIndex == 3) {
686    switch(caseSig) {
687        case 37 :
688        case 33 :
689        case 5 :
690        case 1 :
691        case 55 :
692        case 51 :
693        case 23 :
694        case 19 :
695      t1 = PureSat_And(manager, bAig_Not(rl), lr);
696      t2 = PureSat_And(manager, ll, t1);
697      return(t2);
698        case 36 :
699        case 32 :
700        case 4 :
701        case 0 :
702        case 54 :
703        case 50 :
704        case 22 :
705        case 18 :
706      t1 = PureSat_And(manager, rl, lr);
707      t2 = PureSat_And(manager, ll, t1);
708      return(t2);
709        case 44 :
710        case 40 :
711        case 12 :
712        case 8 :
713        case 62 :
714        case 58 :
715        case 30 :
716        case 26 :
717      t1 = PureSat_And(manager, rl, lr);
718      t2 = PureSat_And(manager, bAig_Not(ll), t1);
719      return(t2);
720        case 45 :
721        case 41 :
722        case 13 :
723        case 9 :
724        case 63 :
725        case 59 :
726        case 31 :
727        case 27 :
728      t1 = PureSat_And(manager, bAig_Not(ll), bAig_Not(rl));
729      t2 = PureSat_Or(manager, bAig_Not(lr), t1);
730      return(t2);
731        case 39 :
732        case 35 :
733        case 7 :
734        case 3 :
735        case 53 :
736        case 49 :
737        case 21 :
738        case 17 :
739      return(l);
740        case 46 :
741        case 42 :
742        case 14 :
743        case 10 :
744        case 60 :
745        case 56 :
746        case 28 :
747        case 24 :
748      return(r);
749        case 38 :
750        case 34 :
751        case 6 :
752        case 2 :
753        case 52 :
754        case 48 :
755        case 20 :
756        case 16 :
757      return(bAig_Zero);
758        case 47 :
759        case 43 :
760        case 15 :
761        case 11 :
762        case 61 :
763        case 57 :
764        case 29 :
765        case 25 :
766      t1 = PureSat_And2(manager, l, r);
767      return(t1);
768    }
769  }
770  else if(caseIndex == 4) {
771    switch(caseSig) {
772        case 22 :
773        case 20 :
774        case 6 :
775        case 4 :
776        case 50 :
777        case 48 :
778        case 34 :
779        case 32 :
780        case 2 :
781        case 16 :
782        case 52 :
783        case 1 :
784        case 8 :
785        case 19 :
786        case 26 :
787        case 37 :
788        case 44 :
789        case 38 :
790        case 55 :
791        case 62 :
792      return(bAig_Zero);
793        case 0 :
794        case 18 :
795        case 36 :
796        case 54 :
797        case 9 :
798        case 27 :
799        case 45 :
800        case 63 :
801        case 5 :
802        case 23 :
803        case 33 :
804        case 51 :
805        case 3 :
806        case 17 :
807        case 49 :
808        case 7 :
809        case 35 :
810        case 21 :
811        case 39 :
812        case 53 :
813      return(l);
814        case 40 :
815        case 58 :
816        case 12 :
817        case 30 :
818        case 24 :
819        case 10 :
820        case 14 :
821        case 56 :
822        case 28 :
823        case 42 :
824        case 60 :
825        case 46 :
826      return(r);
827        case 11 :
828        case 47 :
829        case 25 :
830        case 61 :
831      return(bAig_Not(ll));
832        case 41 :
833        case 59 :
834        case 13 :
835        case 31 :
836      return(bAig_Not(lr));
837        case 15 :
838      t1 = PureSat_And(manager, ll, bAig_Not(lr));
839      t2 = PureSat_And(manager, bAig_Not(ll), lr);
840      return(bAig_Not(PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
841        case 57 :
842      t1 = PureSat_And(manager, rl, bAig_Not(rr));
843      t2 = PureSat_And(manager, bAig_Not(rl), rr);
844      return(bAig_Not(PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
845        case 29 :
846      t1 = PureSat_And(manager, ll, lr);
847      t2 = PureSat_And(manager, bAig_Not(ll), bAig_Not(lr));
848      return((PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
849        case 43 :
850      t1 = PureSat_And(manager, rl, rr);
851      t2 = PureSat_And(manager, bAig_Not(rl), bAig_Not(rr));
852      return((PureSat_And2(manager, bAig_Not(t1), bAig_Not(t2))));
853    }
854  }
855  return(0);
856}
857
858
859
860/**Function********************************************************************
861
862  Synopsis    [test whether two level minimization can be enabled--iff the two
863               nodes are in the same timeframe]
864
865  Description [output, l,r,ll,lr,rl,rr must be in the same class to pass the test]
866
867  SideEffects []
868
869  SeeAlso     []
870
871******************************************************************************/
872
873
874int PureSat_Test2LevelMini(bAig_Manager_t *manager,
875                           bAigEdge_t l,
876                           bAigEdge_t r)
877{
878  int class_ = bAig_Class(l);
879  bAigEdge_t ll,lr,rl,rr;
880
881  if(!manager->test2LevelMini)
882    return 0;
883
884  if(class_!= bAig_Class(r) || class_ != manager->class_)
885    return 0;
886
887  ll = leftChild(l);
888  if(ll!=bAig_NULL && class_!=bAig_Class(ll))
889    return 0;
890  lr = rightChild(l);
891  if(lr!=bAig_NULL && class_!=bAig_Class(lr))
892    return 0;
893  rl = leftChild(r);
894  if(rl!=bAig_NULL && class_!=bAig_Class(rl))
895    return 0;
896  rr = rightChild(r);
897  if(rr!=bAig_NULL && class_!=bAig_Class(rr))
898    return 0;
899
900  return 1;
901}
902
903/**Function********************************************************************
904
905  Synopsis [And function for two AIG nodes. The difference with
906            bAigCreateAndNode is that here two level minimization
907            is only allowed with the same timeframe, otherwise the
908            global variable for interpolation generation may not be
909            latch variables]
910
911  Description []
912
913  SideEffects []
914
915  SeeAlso     []
916
917******************************************************************************/
918
919bAigEdge_t
920PureSat_And(
921   bAig_Manager_t *manager,
922   bAigEdge_t nodeIndex1,
923   bAigEdge_t nodeIndex2)
924{
925
926  bAigEdge_t newNodeIndex;
927
928  nodeIndex1 = bAig_GetCanonical(manager, nodeIndex1);
929  nodeIndex2 = bAig_GetCanonical(manager, nodeIndex2);
930
931  newNodeIndex = nodeIndex1;     /* The left node has the smallest index */
932  if (bAig_NonInvertedEdge(nodeIndex1) > bAig_NonInvertedEdge(nodeIndex2)){
933    nodeIndex1 = nodeIndex2;
934    nodeIndex2 = newNodeIndex;
935  }
936
937  if ( nodeIndex2 == bAig_Zero ) {
938    return bAig_Zero;
939  }
940  if ( nodeIndex1 == bAig_Zero ) {
941    return bAig_Zero;
942  }
943  if ( nodeIndex2 == bAig_One ) {
944    return nodeIndex1;
945  }
946  if ( nodeIndex1 == bAig_One ) {
947    return nodeIndex2;
948  }
949  if ( nodeIndex1 == nodeIndex2 ) {
950    return nodeIndex1;
951  }
952  if ( nodeIndex1 == bAig_Not(nodeIndex2) ) {
953    return bAig_Zero;
954  }
955
956  /* Look for the new node in the Hash table */
957  newNodeIndex = PureSat_HashTableLookup(manager, nodeIndex1, nodeIndex2);
958
959
960  if (newNodeIndex == bAig_NULL){
961    if(!PureSat_Test2LevelMini(manager,nodeIndex1,nodeIndex2)){
962      newNodeIndex = PureSat_And2(manager, nodeIndex1, nodeIndex2);
963      return newNodeIndex;
964    }
965
966    if(bAigIsVar(manager, nodeIndex1) && bAigIsVar(manager, nodeIndex2))
967      newNodeIndex = PureSat_And2(manager, nodeIndex1, nodeIndex2);
968    else if(bAigIsVar(manager, nodeIndex1))
969      newNodeIndex = PureSat_And3(manager, nodeIndex1, nodeIndex2);
970    else if(bAigIsVar(manager, nodeIndex2))
971      newNodeIndex = PureSat_And3(manager, nodeIndex2, nodeIndex1);
972    else {
973      newNodeIndex = PureSat_And4(manager, nodeIndex1, nodeIndex2);
974    }
975  }
976
977  return newNodeIndex;
978
979}
980
981
982/**Function********************************************************************
983
984  Synopsis    [OR operation for two aig nodes]
985
986  Description []
987
988  SideEffects []
989
990  SeeAlso     []
991
992******************************************************************************/
993
994bAigEdge_t
995PureSat_Or(
996   bAig_Manager_t *manager,
997   bAigEdge_t nodeIndex1,
998   bAigEdge_t nodeIndex2)
999{
1000  return ( bAig_Not(PureSat_And(manager,  bAig_Not(nodeIndex1),  bAig_Not(nodeIndex2))));
1001}
1002
1003
1004/**Function********************************************************************
1005
1006  Synopsis    [XOR operation for two aig nodes]
1007
1008  Description []
1009
1010  SideEffects []
1011
1012  SeeAlso     []
1013
1014******************************************************************************/
1015
1016bAigEdge_t
1017PureSat_Xor(
1018   bAig_Manager_t *manager,
1019   bAigEdge_t nodeIndex1,
1020   bAigEdge_t nodeIndex2)
1021{
1022 return PureSat_Or(manager,
1023            PureSat_And(manager, nodeIndex1, bAig_Not(nodeIndex2)),
1024            PureSat_And(manager, bAig_Not(nodeIndex1),nodeIndex2)
1025        );
1026}
1027
1028
1029/**Function********************************************************************
1030
1031  Synopsis    [EQ operation for two aig nodes]
1032
1033  Description []
1034
1035  SideEffects []
1036
1037  SeeAlso     []
1038
1039******************************************************************************/
1040
1041bAigEdge_t
1042PureSat_Eq(
1043   bAig_Manager_t *manager,
1044   bAigEdge_t nodeIndex1,
1045   bAigEdge_t nodeIndex2)
1046{
1047 return bAig_Not(
1048            PureSat_Xor(manager, nodeIndex1, nodeIndex2)
1049            );
1050}
1051
1052
1053/**Function********************************************************************
1054
1055  Synopsis    [THEN operation for two aig nodes]
1056
1057  Description []
1058
1059  SideEffects []
1060
1061  SeeAlso     []
1062
1063******************************************************************************/
1064
1065bAigEdge_t
1066PureSat_Then(
1067   bAig_Manager_t *manager,
1068   bAigEdge_t nodeIndex1,
1069   bAigEdge_t nodeIndex2)
1070{
1071 return PureSat_Or(manager,
1072                bAig_Not(nodeIndex1),
1073                nodeIndex2);
1074}
1075
1076
1077
1078/**Function********************************************************************
1079
1080  Synopsis    [Create variable AIG nodes]
1081
1082  Description []
1083
1084  SideEffects []
1085
1086  SeeAlso     []
1087
1088******************************************************************************/
1089
1090
1091bAigEdge_t
1092PureSat_CreateVarNode(
1093   bAig_Manager_t  *manager,
1094   nameType_t      *name)
1095{
1096
1097  bAigEdge_t varIndex;
1098  int class_ = manager->class_;
1099
1100
1101  if (!st_lookup(manager->SymbolTableArray[class_], name, &varIndex)){
1102    varIndex = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
1103    if (varIndex == bAig_NULL){
1104      return (varIndex);
1105    }
1106    /* Insert the varaible in the Symbol Table */
1107    st_insert(manager->SymbolTableArray[class_],
1108              name, (char*) (long) varIndex);
1109    manager->nameList[bAigNodeID(varIndex)] = name;
1110    return(varIndex);
1111  }
1112  else {
1113    return (varIndex);
1114  }
1115}
Note: See TracBrowser for help on using the repository browser.