source: vis_dev/cusp-1.1/src/aig/aig.h

Last change on this file was 12, checked in by cecile, 13 years ago

cusp added
File size: 19.8 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [Aig.h]
4
5  PackageName [Aig]
6
7  Synopsis    [Binary AND/INVERTER graph]
8
9  Description [External functions and data strucures of the binary AND/INVERTER graph package]
10
11  SeeAlso     [AigInt.h]
12
13  Author      [Mohammad Awedh]
14
15  Copyright [This file was created at the University of Colorado at
16  Boulder.  The University of Colorado at Boulder makes no warranty
17  about the suitability of this software for any purpose.  It is
18  presented on an AS IS basis.]
19
20  Revision    [$Id: aig.h,v 1.1.1.1 2008-11-14 20:40:11 hhkim Exp $]
21
22
23******************************************************************************/
24
25#ifndef _AIG
26#define _AIG
27
28#ifdef __cplusplus
29extern "C" {
30#endif
31
32#include <stdio.h>
33#include <string.h>
34#include <stdlib.h>
35#include "st.h"
36#include "util.h"
37#include "array.h"
38
39
40/*---------------------------------------------------------------------------*/
41/* Constant declarations                                                     */
42/*---------------------------------------------------------------------------*/
43
44#ifndef TRUE
45#define TRUE 1
46#endif
47
48#ifndef FALSE
49#define FALSE 0
50#endif
51
52#define AigInvertBit      0x1                        /* This bit is set to indicate inverted edge*/
53
54#define AigArrayMaxSize   (1 << 27)  /* Maximum size of the node array */
55
56#define ZERO_NODE_INDEX    0                          /* Reserve this index for constant Zero node*/
57#define Aig_Zero          (ZERO_NODE_INDEX)          /* Constatnt Zero node */
58#define Aig_One           (Aig_Not(Aig_Zero))      /* Constatnt One node  */
59
60#define Aig_NULL          2
61/* Bing */
62#define AigNodeSize       8                          /* Array is used to implement the Aig graph.
63                                                         Each node occupies AigNodeSize array elements. */
64#define AigFirstNodeIndex   AigNodeSize             /* The first node index. */
65
66#define Aig_HashTableSize 481931
67
68#define  AigValue     0   /* Index of the decision level. */ 
69#define  AigFlags     1   /* Index of flag for this node.*/
70#define  AigLeft      2   /* Index of the left child */ 
71#define  AigRight     3   /* Index of the right child */ 
72#define  AigNFanout   4   /* Index of number of fanout.*/
73#define  AigFanout    5   /* Index of fanout pointer for this node.*/
74#define  AigCanonical 6   /* Index of canonical node for this node.*/
75#define  AigNext      7   /* Index of dummy for this node.*/
76
77/* Bing */
78#define  AigClass     8
79
80/**
81 * If AIG nodes are identified as equivalent node, then they are merged
82 * into one of them. This mask bit is used identified the representative
83 * of those equivalent nodes.
84 **/
85#define CanonicalBitMask       0x00020000
86#define ResetCanonicalBitMask  ~0x00020000L
87
88/*---------------------------------------------------------------------------*/
89/* Type declarations                                                         */
90/*---------------------------------------------------------------------------*/
91
92typedef char                     nameType_t;
93typedef long                     AigEdge_t;
94typedef struct AigManagerStruct Aig_Manager_t;
95typedef struct AigTimeFrameStruct       AigTimeFrame_t;
96
97/*---------------------------------------------------------------------------*/
98/* Structure declarations                                                    */
99/*---------------------------------------------------------------------------*/
100
101/**Struct**********************************************************************
102
103  Synopsis    [And/Inverter graph manager.]
104
105  Description []
106
107******************************************************************************/
108struct AigManagerStruct {
109  AigEdge_t *NodesArray;       /* contains pointers to nodes of type
110                                   Aig_Node_t */
111  long        nodesArraySize;    /* contains the current number of nodes */
112  long        maxNodesArraySize; /* Nodes Array maximum size */
113
114  AigEdge_t *HashTable;        /* Hash table */
115  st_table   *SymbolTable;      /* Symbol table to store variables and their
116                                   indices */
117  char       **nameList;        /* This table contains the name of each node.
118                                   nodeID is used to access the node's name. */
119  array_t    *mVarList;         /* List of mVarId of each variable */ 
120  array_t    *bVarList;         /* List of bVardId (Aig_t) of the binary value
121                                   encoding for multi-valued variables. */
122  int        allocatedFlags;
123  st_table   *id2aig;
124
125  struct AigTimeFrameStruct *timeframe;
126  struct AigTimeFrameStruct *timeframeWOI;
127  char *dummy;
128 
129  /* Bing: for interpolation */
130  AigEdge_t **  HashTableArray;
131  st_table **    SymbolTableArray;
132  int NumOfTable;
133
134  int cls; /* one is C1, 2 is C2 or for multiCut it is the timeframe; */
135  AigEdge_t  InitState, IPState;
136  int IP,test2LevelMini;
137};
138
139/**Struct**********************************************************************
140
141  Synopsis    [A struct to save unrolled system]
142
143******************************************************************************/
144struct AigTimeFrameStruct {
145    int nInputs;                 /* the number of inputs */
146    int nOutputs;                /* the number of outputs */
147    int nLatches;                /* the number of latchs */
148    int nInternals;              /* the numebr of internal nodes */
149    int currentTimeframe;        /* the number of unrolled timeframe */
150    AigEdge_t **inputs;         /* the array to save input of each unrolled timeframe */
151    AigEdge_t **outputs;        /* the array to save output of each unrolled timeframe */
152    AigEdge_t **latchInputs;    /* the array to save latch input of each unrolled timeframe */
153    AigEdge_t **internals;      /* the array to save internal node of each unrolled timeframe */
154                                 /* we need this array to build property */
155                                 /* based on internal node, there might be */
156                                 /* the way to improve this. */
157    AigEdge_t *oriLatchInputs;  /* the array to save latch input of original system */
158    AigEdge_t *oribLatchInputs; /* the array to save latch input of original system */
159    AigEdge_t *oriInputs;       /* the array to save input of original system */
160    AigEdge_t *oribInputs;      /* the array to save input of original system */
161    st_table *li2index;          /* It maps the latch input aig to index which can identify i'th latch input through latchInputs[i][index] */
162    st_table *o2index;           /* It maps the output aig to index which can identify i'th latch input through outputs[i][index] */
163    st_table *i2index;           /* It maps the input aig to index which can identify i'th latch input through inputs[i][index] */
164    st_table *pi2index;          /* It maps the input aig to index which can identify i'th latch input through inputs[i][index] */
165    array_t *latchArr;
166    array_t *inputArr;
167    array_t *outputArr;
168    array_t *iindexArray;
169    array_t *assertedArray;
170    int nbInputs;                /* the number of input bits */
171    int nbLatches;               /* the number of latche bits */
172    AigEdge_t **binputs;        /* the array to save input bit of each unrolled timeframe */
173    AigEdge_t **blatchInputs;   /* the array to save latch input bit of each unrolled timeframe */
174    st_table *bli2index;         /* It maps the latch input bit of aig to index which can identify i'th latch input through blatchInputs[i][index] */
175    st_table *bpi2index;         /* It maps the input bit of aig to index which can identify i'th latch input through binputs[i][index] */
176
177    /* Bing */
178    st_table *libli2eq;
179    st_table *idx2name;
180    st_table *MultiLatchTable;   /* stores var corresponding to multiple latches */
181};
182
183/**Struct**********************************************************************
184
185  Synopsis    [A struct to save transition relation of AIG ]
186
187******************************************************************************/
188typedef struct AigTransitionStruct      AigTransition_t;
189struct AigTransitionStruct {
190    Aig_Manager_t    *manager;
191    int nInputs;           
192    int nLatches;         
193    AigEdge_t objective;
194    AigEdge_t *inputs;         
195    AigEdge_t *cstates;   
196    AigEdge_t *nstates;
197    AigEdge_t *initials;
198    AigEdge_t *n2c;
199    AigEdge_t *c2n;
200    AigEdge_t *cobj;
201    int csize;
202    int istates;
203    AigEdge_t *tstates;   
204    AigEdge_t *coiStates;  /* to identified the next states variables in froniter set **/ 
205
206    int *vinputs;     /** to save the value of primary inputs **/ 
207    int *vtstates;    /** to save the value of tstates variable during lifting **/
208    int objValue;
209    int latestBlockingClause;
210    int iteration;
211    int avgLits;
212    int sum;
213    int period;
214    int interval;
215    int nBlocked;
216
217    int method;
218    int interface;
219    int inclusionInitial;
220    int constrain;
221    int verbose;
222    int reductionUsingUnsat;
223    int disableLifting;
224};
225
226
227/*---------------------------------------------------------------------------*/
228/* Variable declarations                                                     */
229/*---------------------------------------------------------------------------*/
230
231/*---------------------------------------------------------------------------*/
232/* Macro declarations                                                        */
233/*---------------------------------------------------------------------------*/
234
235/**Macro***********************************************************************
236
237  Synopsis     [Performs the 'Not' Logical operator]
238
239  Description  [This macro inverts the edge going to a node which corresponds
240                to NOT operator]
241
242  SideEffects [none]
243
244  SeeAlso      []
245
246******************************************************************************/
247/* Bing */
248#define Aig_Class(node) (\
249 bm->NodesArray[Aig_NonInvertedEdge(node)+AigClass]\
250)
251
252#define Aig_Not(node) (                         \
253        (AigEdge_t) ((node) ^ (AigInvertBit))  \
254)
255
256/**Macro***********************************************************************
257
258  Synopsis     [Returns the non inverted edge.]
259
260  Description  [This macro returns the non inverted edge.  It clears the least
261  significant bit of the edge if it is set.]
262
263  SideEffects  [none]
264
265  SeeAlso      []
266
267******************************************************************************/
268#define Aig_NonInvertedEdge(edge) ( \
269        (edge) & ~(AigInvertBit)    \
270)
271
272/**Macro***********************************************************************
273
274  Synopsis     [Returns true if the edge is inverted.]
275
276  Description  []
277
278  SideEffects [none]
279
280  SeeAlso      []
281
282******************************************************************************/
283#define Aig_IsInverted(edge) (   \
284        (edge) & (AigInvertBit)  \
285)
286
287/**Macro***********************************************************************
288
289  Synopsis    [Return right child of aig node]
290
291  Description []
292
293  SideEffects [none]
294
295  SeeAlso     []
296
297******************************************************************************/
298#define rightChild(node)(\
299(bm->NodesArray[Aig_NonInvertedEdge(node)+AigRight])\
300)
301
302/**Macro***********************************************************************
303
304  Synopsis    [Return left child of aig node]
305
306  Description []
307
308  SideEffects [none]
309
310  SeeAlso     []
311
312******************************************************************************/
313#define leftChild(node)(\
314(bm->NodesArray[Aig_NonInvertedEdge(node)+AigLeft])\
315)
316
317/**Macro***********************************************************************
318
319  Synopsis    []
320
321  Description []
322
323  SideEffects [none]
324
325  SeeAlso     []
326
327******************************************************************************/
328#define fanout(node)(\
329bm->NodesArray[Aig_NonInvertedEdge(node)+AigFanout]\
330)
331
332/**Macro***********************************************************************
333
334  Synopsis    []
335
336  Description []
337
338  SideEffects [none]
339
340  SeeAlso     []
341
342******************************************************************************/
343#define nFanout(node)(\
344bm->NodesArray[Aig_NonInvertedEdge(node)+AigNFanout]\
345)
346
347/**Macro***********************************************************************
348
349  Synopsis    []
350
351  Description []
352
353  SideEffects [none]
354
355  SeeAlso     []
356
357******************************************************************************/
358#define flags(node)(\
359bm->NodesArray[Aig_NonInvertedEdge(node)+AigFlags]\
360)
361
362/**Macro***********************************************************************
363
364  Synopsis    []
365
366  Description []
367
368  SideEffects [none]
369
370  SeeAlso     []
371
372******************************************************************************/
373#define canonical(node)(\
374bm->NodesArray[Aig_NonInvertedEdge(node)+AigCanonical]\
375)
376
377
378/**Macro***********************************************************************
379
380  Synopsis    [return next of aig]
381
382  Description [This is used to build hash table for structural hashing]
383
384  SideEffects [none]
385
386  SeeAlso     []
387
388******************************************************************************/
389#define aig_next(node)(\
390bm->NodesArray[Aig_NonInvertedEdge(node)+AigNext]\
391)
392
393/**Macro***********************************************************************
394
395  Synopsis    [return value of aig node]
396
397  Description []
398
399  SideEffects [none]
400
401  SeeAlso     []
402
403******************************************************************************/
404#define aig_value(node)(\
405(bm->NodesArray[Aig_NonInvertedEdge(node)+AigValue])\
406)
407
408/**Macro***********************************************************************
409
410  Synopsis    [The node ID]
411
412  Description [Node ID is a unique number for each node and can be found by
413              dividing the edge going to this node by AigNodeSize.]
414
415  SideEffects [none]
416
417  SeeAlso     []
418
419******************************************************************************/
420/*#define AigNodeID(edge)(\
421Aig_NonInvertedEdge(edge)>>3 \
422)*/
423
424
425/* Bing */
426#define AigNodeID(edge)(\
427Aig_NonInvertedEdge(edge)/AigNodeSize \
428)
429
430/**Macro***********************************************************************
431
432  Synopsis    [Hash function for the hash table.]
433
434  Description []
435
436  SideEffects [none]
437
438  SeeAlso     []
439
440******************************************************************************/
441#if 1
442#if 1
443#define HashTableFunction(left, right) \
444( (AigEdge_t) \
445((( (AigEdge_t) (left)) << 3) + \
446(( (AigEdge_t) (right)) << 3)) % Aig_HashTableSize \
447)
448#else
449#define HashTableFunction(left, right) \
450((AigEdge_t) \
451((((((AigEdge_t) (left)) + (((AigEdge_t) (left)) << 5)) ^ \
452(((AigEdge_t) (right)) + (((AigEdge_t) (right)) << 5)) + left ) % Aig_HashTableSize \
453)))
454#endif
455#else
456#define HashTableFunction(left, right) \
457( (AigEdge_t) \
458((( (AigEdge_t) (left)) + (( (AigEdge_t) (left)) << 5)) ^ \
459(( (AigEdge_t) (right)) + (( (AigEdge_t) (right)) << 5)) + \
460left ) % Aig_HashTableSize \
461) 
462#endif
463
464
465/**Macro***********************************************************************
466
467  Synopsis    [Traverse fanout of AIG ]
468
469  Description []
470
471  SideEffects [none]
472
473  SeeAlso     []
474
475******************************************************************************/
476#define AigEdgeForEachFanout(                             \
477        manager,     /* Aig_Manager_t */                  \
478        v,           /* AigEdge_t */                      \
479        cur,         /* AigEdge_t for fanout */           \
480        ii,                                                \
481        iii,                                               \
482        pfan                                               \
483)                                                          \
484for(ii=0, iii=nFanout(v), pfan=(AigEdge_t *)fanout(v);         \
485    (ii<iii) && (cur = pfan[ii]);                           \
486    ii++)
487
488
489/**Macro***********************************************************************
490
491  Synopsis    [Is AIG node is variable node]
492
493  Description []
494
495  SideEffects [none]
496
497  SeeAlso     []
498
499******************************************************************************/
500#define AigIsVar(manager, v)                              \
501    (leftChild(v) == 2 ? 1 : 0)
502
503
504/**Macro***********************************************************************
505
506  Synopsis    [Check whether two nodes are same or not]
507
508  Description []
509
510  SideEffects [none]
511
512  SeeAlso     []
513
514******************************************************************************/
515#define AigCompareNode(l, r)                              \
516    ((l==r) ? 1 : ((l+1 == r) ? 1 : ((l==r+1) ? 1 : 0)))
517
518
519/**Macro***********************************************************************
520
521  Synopsis    [Swap AIG nodes ]
522
523  Description []
524
525  SideEffects [none]
526
527  SeeAlso     []
528
529******************************************************************************/
530#define AigSwap(l, r)                                     \
531{                                                          \
532    AigEdge_t __tmp;                                      \
533      __tmp = l; l = r; r = __tmp;                         \
534}
535
536
537
538
539/**AutomaticStart*************************************************************/
540
541/*---------------------------------------------------------------------------*/
542/* Function prototypes                                                       */
543/*---------------------------------------------------------------------------*/
544
545EXTERN void Aig_Init(void);
546EXTERN void Aig_End(void);
547EXTERN Aig_Manager_t * Aig_initAig(int maxSize);
548EXTERN void Aig_quit(Aig_Manager_t *bm);
549EXTERN void Aig_NodePrint(Aig_Manager_t *bm, AigEdge_t node);
550EXTERN nameType_t * Aig_NodeReadName(Aig_Manager_t *bm, AigEdge_t node);
551EXTERN void Aig_NodeSetName(Aig_Manager_t *bm, AigEdge_t node, nameType_t *name);
552EXTERN int Aig_NodeReadIndexOfRightChild(Aig_Manager_t *bm, AigEdge_t nodeIndex);
553EXTERN AigEdge_t Aig_NodeReadIndexOfLeftChild(Aig_Manager_t *bm, AigEdge_t nodeIndex);
554EXTERN AigEdge_t Aig_GetCanonical(Aig_Manager_t *bm, AigEdge_t nodeIndex);
555EXTERN int Aig_Merge(Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2);
556EXTERN void Aig_PrintNode(Aig_Manager_t *bm, AigEdge_t i);
557EXTERN AigEdge_t Aig_And(Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2);
558EXTERN AigEdge_t Aig_And2(Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2);
559EXTERN AigEdge_t Aig_AndsInBFSManner(Aig_Manager_t *bm, array_t * nodeIndexArray);
560EXTERN AigEdge_t Aig_Or(Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2);
561EXTERN AigEdge_t Aig_OrsInBFSManner(Aig_Manager_t *bm, array_t * nodeIndexArray);
562EXTERN AigEdge_t Aig_Xor(Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2);
563EXTERN AigEdge_t Aig_Eq(Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2);
564EXTERN AigEdge_t Aig_Then(Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2);
565EXTERN AigEdge_t Aig_Nand(Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2);
566EXTERN AigEdge_t Aig_Ite(Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2, AigEdge_t nodeIndex3);
567EXTERN AigEdge_t Aig_Inequality(Aig_Manager_t *bm, int  N, int nx, int ny, int c, AigEdge_t *x, AigEdge_t *y);
568EXTERN AigEdge_t Aig_Equality(Aig_Manager_t *bm, int N, int nx, int ny, int c, AigEdge_t *x, AigEdge_t *y);
569EXTERN AigEdge_t Aig_Disequality(Aig_Manager_t *bm, int  N, int c, AigEdge_t *x, AigEdge_t *y);
570EXTERN AigEdge_t Aig_Bound(Aig_Manager_t *bm, int  N, int lb, int ub, AigEdge_t *x);
571EXTERN AigEdge_t Aig_CreateNode(Aig_Manager_t *bm, AigEdge_t nodeIndex1, AigEdge_t nodeIndex2);
572EXTERN AigEdge_t Aig_FindNodeByName(Aig_Manager_t *bm, nameType_t *name);
573EXTERN AigEdge_t Aig_CreateVarNode(Aig_Manager_t *bm, nameType_t *name);
574EXTERN int Aig_isVarNode(Aig_Manager_t *bm, AigEdge_t node);
575EXTERN int Aig_PrintDot(FILE *fp, Aig_Manager_t *bm);
576EXTERN int Aig_PrintAIG(Aig_Manager_t *bm, AigEdge_t object, char *fileName);
577EXTERN AigEdge_t Aig_And4(Aig_Manager_t *bm, AigEdge_t l, AigEdge_t r);
578EXTERN AigEdge_t Aig_And3(Aig_Manager_t *bm, AigEdge_t l, AigEdge_t r);
579EXTERN void Aig_SetMaskTransitiveFanin(Aig_Manager_t *bm, int v, unsigned int mask);
580EXTERN void Aig_ResetMaskTransitiveFanin(Aig_Manager_t *bm, int v, unsigned int mask, unsigned int resetMask);
581EXTERN int Aig_GetValueOfNode(Aig_Manager_t *bm, AigEdge_t v);
582
583/**AutomaticEnd***************************************************************/
584#ifdef __cplusplus
585}
586#endif
587#endif /* _AIG */
Note: See TracBrowser for help on using the repository browser.