Biddy  1.8.1
An academic Binary Decision Diagrams package
biddyInt.h
Go to the documentation of this file.
1 /***************************************************************************/
43 #ifndef _BIDDYINT
44 #define _BIDDYINT
45 
46 #include "biddy.h"
47 #include <assert.h>
48 #include <string.h>
49 #include <ctype.h>
50 #include <gmp.h>
51 
52 /* sleep() is not included in modern version of MINGW */
53 /* #define sleep(sec) (Sleep ((sec) * 1000), 0) */
54 
55 #ifdef MINGW
56 #define sleep(sec) 0
57 #endif
58 
59 /* this is from */
60 /* http://stackoverflow.com/questions/3694723/error-c3861-strcasecmp-identifier-not-found-in-visual-studio-2008 */
61 /* not #if defined(_WIN32) || defined(_WIN64) because we have strncasecmp in mingw */
62 #ifdef _MSC_VER
63 #define strncasecmp _strnicmp
64 #define strcasecmp _stricmp
65 #endif
66 
67 /* extended stats (YES or NO) */
68 /* if YES then you have to use -lm for linking */
69 #define BIDDYEXTENDEDSTATS_NO
70 
71 /* event log (YES or NO) */
72 #define BIDDYEVENTLOG_NO
73 #ifdef BIDDYEVENTLOG_YES
74 #define ZF_LOGI(x) {static unsigned int biddystat = 0;printf(x);printf("#%u,%.2f\n",++biddystat,clock()/(1.0*CLOCKS_PER_SEC));}
75 #else
76 #define ZF_LOGI(x)
77 #endif
78 
79 /* use this to use CUDD style for edges: */
80 /* solid line: regular THEN arcs */
81 /* bold line: complemented THEN arcs */
82 /* dashed line: regular ELSE arcs */
83 /* dotted line: complemented ELSE arcs */
84 /* without LEGACY_DOT, an experimental style for edges is used */
85 /* this setting is NOT USED for CUDD-like generation of dot files */
86 #define LEGACY_DOT
87 
88 /*----------------------------------------------------------------------------*/
89 /* Constant declarations */
90 /*----------------------------------------------------------------------------*/
91 
92 /* UINTPTR and UINTPTRSIZE are used for BiddyOrdering */
93 #define UINTPTR uintptr_t
94 #define UINTPTRSIZE (8*sizeof(UINTPTR))
95 
96 /* max number of variables - this is hardcoded for better performance */
97 /* for optimal space reservation use VARMAX = 32*N */
98 /* variable "1" is one of these variables */
99 /* for TZBDDs and TZFDDs, the limit is 65536 variables on 64-bit architecture */
100 /* if there are more than 32768 variables then some macros in biddy.h must be changed */
101 /* BIDDY IS NOT EFFICIENT WITH MANY VARIABLES! */
102 /* #define BIDDYVARMAX 1024 */
103 /* #define BIDDYVARMAX 2048 */
104 /* #define BIDDYVARMAX 4096 */
105 #define BIDDYVARMAX 6144
106 /* #define BIDDYVARMAX 8192 */
107 
108 /* the following constants are used in Biddy_ReadVerilogFile */
109 #define LINESIZE 999 /* maximum length of each input line read */
110 #define BUFSIZE 99999 /* maximum length of a buffer */
111 #define INOUTNUM 999 /* maximum number of inputs and outputs */
112 #define REGNUM 9999 /* maximum number of registers */
113 #define TOKENNUM 9999 /* maximum number of tokens */
114 #define GATENUM 9999 /* maximum number of gates */
115 #define LINENUM 99999 /* maximum number of lines */
116 #define WIRENUM 99999 /* maximum number of wires */
117 
118 /*----------------------------------------------------------------------------*/
119 /* Macro definitions */
120 /*----------------------------------------------------------------------------*/
121 
122 /* Null edge, this is hardcoded since Biddy v1.4 */
123 #define biddyNull ((Biddy_Edge)NULL)
124 
125 /* BiddyP returns the pointer used with the given edge (without tag and complement bit), since Biddy v1.7. */
126 #if UINTPTR_MAX == 0xffffffffffffffff
127 #define BiddyP(fun) ((void *)((uintptr_t) fun & 0x0000fffffffffffe))
128 #else
129 #define BiddyP(fun) ((void *)((uintptr_t) fun & ~((uintptr_t) 1)))
130 #endif
131 
132 /* BiddyR returns not-tagged version of edge, since Biddy v1.7. */
133 /* tagged edges assumes 64-bit architecture */
134 #if UINTPTR_MAX == 0xffffffffffffffff
135 #define BiddyR(fun) ((void *)((uintptr_t) fun & 0x0000ffffffffffff))
136 #else
137 #define BiddyR(fun) (fun)
138 #endif
139 
140 /* BiddyN returns the node pointed by the given edge, since Biddy v1.7. */
141 #if UINTPTR_MAX == 0xffffffffffffffff
142 #define BiddyN(fun) ((BiddyNode*)((uintptr_t) fun & 0x0000fffffffffffe))
143 #else
144 #define BiddyN(fun) ((BiddyNode*)((uintptr_t) fun & ~((uintptr_t) 1)))
145 #endif
146 
147 /* BiddyT returns THEN successor, since Biddy v1.4 */
148 
149 #define BiddyT(fun) (BiddyN(fun)->t)
150 
151 /* BiddyE returns ELSE successor, since Biddy v1.4 */
152 
153 #define BiddyE(fun) (BiddyN(fun)->f)
154 
155 /* BiddyV returns top variable, since Biddy v1.6 */
156 
157 #define BiddyV(fun) (BiddyN(fun)->v)
158 
159 /* orderingtable[X,Y]==1 iff variabe X is smaller than variable Y */
160 /* IN THE BDD, SMALLER VARIABLES ARE ABOVE THE GREATER ONES */
161 /* GET_ORDER check if variabe X is smaller (topmore) than variable Y */
162 /* SET_ORDER set variabe X to be smaller (topmore) than variable Y */
163 /* CLEAR_ORDER set variabe X not to be smaller (topmore) than variable Y */
164 /* SET_ORDER and CLEAR_ORDER should be used simultaneously */
165 #define GET_ORDER(orderingtable,X,Y) ((orderingtable)[X][Y/UINTPTRSIZE]&(((UINTPTR) 1)<<(Y%UINTPTRSIZE)))!=0
166 #define SET_ORDER(orderingtable,X,Y) (orderingtable)[X][Y/UINTPTRSIZE] |= (((UINTPTR) 1)<<(Y%UINTPTRSIZE))
167 #define CLEAR_ORDER(orderingtable,X,Y) (orderingtable)[X][Y/UINTPTRSIZE] &= (~(((UINTPTR) 1)<<(Y%UINTPTRSIZE)))
168 
169 /* The name of manager MNG, since Biddy v1.4. */
170 #define biddyManagerName ((Biddy_String)(MNG[0]))
171 #define biddyManagerName1 ((Biddy_String)(MNG1[0]))
172 #define biddyManagerName2 ((Biddy_String)(MNG2[0]))
173 
174 /* Type of manager MNG, since Biddy v1.7 this is used for BDD type */
175 #define biddyManagerType (*((short int*)(MNG[1])))
176 #define biddyManagerType1 (*((short int*)(MNG1[1])))
177 #define biddyManagerType2 (*((short int*)(MNG2[1])))
178 
179 /* Terminal node in manager MNG, since Biddy v1.7. */
180 #define biddyTerminal ((void *)(MNG[2]))
181 #define biddyTerminal1 ((void *)(MNG1[2]))
182 #define biddyTerminal2 ((void *)(MNG2[2]))
183 
184 /* Constant 0 in manager MNG, since Biddy v1.4. */
185 #define biddyZero ((Biddy_Edge)(MNG[3]))
186 #define biddyZero1 ((Biddy_Edge)(MNG1[3]))
187 #define biddyZero2 ((Biddy_Edge)(MNG2[3]))
188 
189 /* Constant 1 in manager MNG, since Biddy v1.4. */
190 #define biddyOne ((Biddy_Edge)(MNG[4]))
191 #define biddyOne1 ((Biddy_Edge)(MNG1[4]))
192 #define biddyOne2 ((Biddy_Edge)(MNG2[4]))
193 
194 /* Node table in manager MNG, since Biddy v1.4. */
195 /* this is typecasted to (BiddyNodeTable*) and dereferenced */
196 /* gdb -g: p *((BiddyNodeTable*)(MNG[5])) */
197 /* gdb -g: p ((BiddyNodeTable*)(MNG[5])).table[i] */
198 /* gdb -g3: p biddyNodeTable */
199 /* gdb -g3: p biddyNodeTable.table[i] */
200 #define biddyNodeTable (*((BiddyNodeTable*)(MNG[5])))
201 #define biddyNodeTable1 (*((BiddyNodeTable*)(MNG1[5])))
202 #define biddyNodeTable2 (*((BiddyNodeTable*)(MNG2[5])))
203 
204 /* Variable table in manager MNG, since Biddy v1.4. */
205 /* this is typecasted to (BiddyVariableTable*) and dereferenced */
206 /* gdb -g: p *((BiddyVariableTable*)(MNG[6])) */
207 /* gdb -g: p ((BiddyVariableTable*)(MNG[6])).table[i] */
208 /* gdb -g3: p biddyVariableTable */
209 /* gdb -g3: p biddyVariableTable.table[i] */
210 #define biddyVariableTable (*((BiddyVariableTable*)(MNG[6])))
211 #define biddyVariableTable1 (*((BiddyVariableTable*)(MNG1[6])))
212 #define biddyVariableTable2 (*((BiddyVariableTable*)(MNG2[6])))
213 
214 /* Formula table in manager MNG, since Biddy v1.4. */
215 /* this is typecasted to (BiddyFormulaTable*) and dereferenced */
216 #define biddyFormulaTable (*((BiddyFormulaTable*)(MNG[7])))
217 #define biddyFormulaTable1 (*((BiddyFormulaTable*)(MNG1[7])))
218 #define biddyFormulaTable2 (*((BiddyFormulaTable*)(MNG2[7])))
219 
220 /* OP Cache in manager MNG, since Biddy v1.4. */
221 /* this is typecasted to (BiddyOp3CacheTable*) and dereferenced */
222 #define biddyOPCache (*((BiddyOp3CacheTable*)(MNG[8])))
223 #define biddyOPCache1 (*((BiddyOp3CacheTable*)(MNG1[8])))
224 #define biddyOPCache2 (*((BiddyOp3CacheTable*)(MNG2[8])))
225 
226 /* EA Cache in manager MNG, since Biddy v1.4. */
227 /* this is typecasted to (BiddyOp3CacheTable*) and dereferenced */
228 #define biddyEACache (*((BiddyOp3CacheTable*)(MNG[9])))
229 #define biddyEACache1 (*((BiddyOp3CacheTable*)(MNG1[9])))
230 #define biddyEACache2 (*((BiddyOp3CacheTable*)(MNG2[9])))
231 
232 /* RC Cache in manager MNG, since Biddy v1.4. */
233 /* this is typecasted to (BiddyOp3CacheTable*) and dereferenced */
234 #define biddyRCCache (*((BiddyOp3CacheTable*)(MNG[10])))
235 #define biddyRCCache1 (*((BiddyOp3CacheTable*)(MNG1[10])))
236 #define biddyRCCache2 (*((BiddyOp3CacheTable*)(MNG2[10])))
237 
238 /* Replace Cache in manager MNG, since Biddy v1.7. */
239 /* this is typecasted to (BiddyKeywordCacheTable*) and dereferenced */
240 #define biddyReplaceCache (*((BiddyKeywordCacheTable*)(MNG[11])))
241 #define biddyReplaceCache1 (*((BiddyKeywordCacheTable*)(MNG1[11])))
242 #define biddyReplaceCache2 (*((BiddyKeywordCacheTable*)(MNG2[11])))
243 
244 /* Cache list in manager MNG, since Biddy v1.4. */
245 /* this is typecasted to (BiddyCacheList**) and dereferenced */
246 #define biddyCacheList (*((BiddyCacheList**)(MNG[12])))
247 #define biddyCacheList1 (*((BiddyCacheList**)(MNG1[12])))
248 #define biddyCacheList2 (*((BiddyCacheList**)(MNG2[12])))
249 
250 /* List of free nodes in manager MNG, since Biddy v1.4. */
251 /* this is typecasted to (BiddyNode**) and dereferenced */
252 #define biddyFreeNodes (*((BiddyNode**)(MNG[13])))
253 #define biddyFreeNodes1 (*((BiddyNode**)(MNG1[13])))
254 #define biddyFreeNodes2 (*((BiddyNode**)(MNG2[13])))
255 
256 /* Variable ordering in manager MNG, since Biddy v1.4. */
257 /* this is typecasted to (BiddyOrderingTable*) and dereferenced */
258 #define biddyOrderingTable (*((BiddyOrderingTable*)(MNG[14])))
259 #define biddyOrderingTable1 (*((BiddyOrderingTable*)(MNG1[14])))
260 #define biddyOrderingTable2 (*((BiddyOrderingTable*)(MNG2[14])))
261 
262 /* System age in manager MNG, since Biddy v1.4. */
263 /* this is typecasted to (int*) and dereferenced */
264 #define biddySystemAge (*((unsigned int*)(MNG[15])))
265 #define biddySystemAge1 (*((unsigned int*)(MNG1[15])))
266 #define biddySystemAge2 (*((unsigned int*)(MNG2[15])))
267 
268 /* Node selector in manager MNG, since Biddy v1.6 */
269 /* this is typecasted to (int*) and dereferenced */
270 #define biddySelect (*((unsigned short int*)(MNG[16])))
271 #define biddySelect1 (*((unsigned short int*)(MNG1[16])))
272 #define biddySelect2 (*((unsigned short int*)(MNG2[16])))
273 
274 /* BiddyProlongOne prolonges top node of the given function, since Biddy v1.6 */
275 #define BiddyProlongOne(f,c) if((!(c))||(BiddyN(f)->expiry&&(BiddyN(f)->expiry<(c))))BiddyN(f)->expiry=(c)
276 
277 /* BiddyRefresh prolonges top node of the given function, manager MNG is assumed, since Biddy v1.7 */
278 #define BiddyRefresh(f) if(BiddyN(f)->expiry&&(BiddyN(f)->expiry<(biddySystemAge)))BiddyN(f)->expiry=(biddySystemAge)
279 #define BiddyDefresh(f) if(BiddyN(f)->expiry&&(BiddyN(f)->expiry>(biddySystemAge)))BiddyN(f)->expiry=(biddySystemAge)
280 
281 /* BiddyIsSmaller returns TRUE if the first variable is smaller (= lower = previous = above = topmore), manager MNG is assumed, since Biddy v1.7 */
282 #define BiddyIsSmaller(fv,gv) GET_ORDER(biddyOrderingTable,fv,gv)
283 
284 /* BiddyIsLowest returns TRUE if the variable is the lowest one (lowest = topmost), manager MNG is assumed, since Biddy v1.7 */
285 #define BiddyIsLowest(v) (biddyVariableTable.table[v].prev >= biddyVariableTable.num)
286 
287 /* BiddyIsHighest returns TRUE if the variable is the highest one ignoring the terminal node (highest = bottommost), manager MNG is assumed, since Biddy v1.7 */
288 #define BiddyIsHighest(v) (biddyVariableTable.table[v].next == 0)
289 
290 /* BiddyIsOK is intended for debugging, only, manager MNG is assumed, since Biddy v1.7 */
291 #define BiddyIsOK(f) (!(BiddyN(f)->expiry) || ((BiddyN(f)->expiry) >= biddySystemAge))
292 /* #define BiddyIsOK(f) ((!(BiddyN(f)->expiry) || ((BiddyN(f)->expiry) >= biddySystemAge)) && checkFunctionOrdering(MNG,f)) */
293 
294 /*----------------------------------------------------------------------------*/
295 /* Type declarations */
296 /*----------------------------------------------------------------------------*/
297 
298 /*----------------------------------------------------------------------------*/
299 /* Structure declarations */
300 /*----------------------------------------------------------------------------*/
301 
302 /* NODE TABLE (UNIQUE TABLE) = a fixed-size hash table with chaining */
303 /* TYPE Biddy_Variable IS DEFINED IN biddy.h */
304 /* IF Biddy_Variable IS unsigned short int (2B) THEN: */
305 /* THE SIZE OF BiddyNode on 32-bit systems is 28 Bytes */
306 /* THE SIZE OF BiddyNode on 64-bit systems is 48 Bytes */
307 typedef struct BiddyNode {
308  struct BiddyNode *prev, *next; /* !!!MUST BE FIRST AND SECOND */
309  Biddy_Edge f, t; /* f = left = else, t = right = then, !!!MUST BE THIRD AND FOURTH */
310  void *list; /* list of nodes (various purposes) */
311  unsigned int expiry; /* expiry value */
312  unsigned short int select; /* used to select node */
313  Biddy_Variable v; /* index in variable table */
314 } BiddyNode;
315 
316 typedef struct {
317  BiddyNode **table;
318  BiddyNode **blocktable; /* table of allocated memory blocks */
319  unsigned int initsize; /* initial size of Node table */
320  unsigned int size; /* current size of Node table */
321  unsigned int limitsize; /* limit for the size of Node table */
322  unsigned int blocknumber; /* number of allocated memory blocks */
323  unsigned int initblocksize; /* the size of the first block of nodes */
324  unsigned int blocksize; /* the size of the last block of nodes */
325  unsigned int limitblocksize; /* limit for the size of the block of nodes */
326  unsigned int generated; /* total number of generated nodes */
327  unsigned int max; /* maximal (peek) number of nodes in node table */
328  unsigned int num; /* number of nodes currently in node table */
329  unsigned int garbage; /* number of garbage collections */
330  unsigned int swap; /* number of performed variable swapping */
331  unsigned int sifting; /* number of performed dynamic reordering */
332  unsigned int nodetableresize; /* number of performed node table resizing */
333  unsigned int funite; /* number of calls of function Biddy_ITE */
334  unsigned int funandor; /* number of calls of function Biddy_And and Biddy_Or */
335  unsigned int funxor; /* number of calls of function Xor */
336  clock_t gctime; /* total time spent for garbage collections */
337  clock_t drtime; /* total time spent for dynamic reordering */
338  float gcratio; /* do not delete nodes if the effect is to small */
339  float gcratioF; /* do not delete nodes if the effect is to small */
340  float gcratioX; /* do not delete nodes if the effect is to small */
341  float resizeratio; /* resize Node table if there are to many nodes */
342  float resizeratioF; /* resize Node table if there are to many nodes */
343  float resizeratioX; /* resize Node table if there are to many nodes */
344  float siftingtreshold; /* stop sifting if the size of the system grows to much */
345  float convergesiftingtreshold; /* stop one step of converging sifting if the size of the system grows to much */
346 
347 #ifdef BIDDYEXTENDEDSTATS_YES
348  unsigned long long int foa; /* number of calls to Biddy_FoaNode */
349  unsigned long long int find; /* number of calls to findNodeTable */
350  unsigned long long int compare; /* num of compared nodes in findNodeTable */
351  unsigned long long int add; /* number of calls to addNodeTable (node table insertions) */
352  unsigned long long int iterecursive; /* number of calls to BiddyITE (direct and recursive) */
353  unsigned long long int andorrecursive; /* number of calls to BiddyAnd and BiddyOr (direct and recursive) */
354  unsigned long long int xorrecursive; /* number of calls to BiddyXor (direct and recursive) */
355  unsigned long long int *gcobsolete; /* number of obsolete nodes removed by GC */
356 #endif
357 } BiddyNodeTable;
358 
359 /* VARIABLE TABLE (SYMBOL TREE) = dynamicaly allocated table */
360 /* variable "1" has id == 0 */
361 /* size of variable table must be compatible with Biddy_Variable */
362 /* value is used for evaluation and also for renaming variables */
363 /* counting variables is also used in BiddyCreateLocalInfo */
364 /* lastNode->list IS NOT DEFINED! */
365 /* YOU MUST NEVER ASSUME THAT lastNode->list = NULL */
366 typedef struct {
367  Biddy_String name; /* name of variable */
368  unsigned int num; /* number of nodes with this variable */
369  unsigned int numone; /* used to count number of nodes with this variable in one function */
370  unsigned int numobsolete; /* used to count number of obsolete nodes with this variable */
371  BiddyNode *firstNode;
372  BiddyNode *lastNode;
373  Biddy_Variable prev; /* previous variable in the global ordering (lower, topmore) */
374  Biddy_Variable next; /* next variable in the global ordering (higher, bottommore) */
375  Biddy_Edge variable; /* bdd representing a single positive variable */
376  Biddy_Edge element; /* bdd representing a set with a single element, i.e. {{x}} */
377  Biddy_Edge value; /* value: biddyZero = 0, biddyOne = 1, reused in some algorithms */
378  Biddy_Boolean selected; /* used to count variables */
379  void *data; /* can be used to associate various user data with every variable */
380 } BiddyVariable;
381 
382 typedef struct {
383  Biddy_String name; /* name of variable */
384  Biddy_Variable v; /* variable corresponding to the name */
385 } BiddyLookupVariable;
386 
387 typedef struct {
388  BiddyVariable *table;
389  BiddyLookupVariable *lookup;
390  Biddy_Variable size; /* size = Biddy_VARMAX */
391  Biddy_Variable num; /* number of all variables, inc. 1 */
392  Biddy_Variable numnum; /* number of numbered variables, inc. 1 */
393 } BiddyVariableTable;
394 
395 /* ORDERING TABLE = TWO-DIMENSIONAL MATRIX OF BITS */
396 /* ordering table is used to define variable ordering. */
397 /* constant variable 1 has max order */
398 /* USABLE ONLY AS AN IRREFLEXIVE TRANSITIVE RELATION */
399 /* MATRIX'S DIMENSION IN BITS = (VARMAX) x (VARMAX) */
400 /* orderingtable[X,Y]==1 iff variabe X is smaller than variable Y */
401 /* IN THE BDD, SMALLER VARIABLES ARE ABOVE THE GREATER ONES */
402 typedef UINTPTR BiddyOrderingTable[BIDDYVARMAX][1+(BIDDYVARMAX-1)/UINTPTRSIZE];
403 
404 /* FORMULA TABLE (FORMULAE TREE) = dynamicaly allocated table */
405 /* expiry = 0, deleted = FALSE -> permanently preserved formula */
406 /* expiry = 0, deleted = TRUE -> deleted permanently preserved formula */
407 /* expiry >= biddySystemAge, deleted = FALSE -> preserved formula */
408 /* expiry >= biddySystemAge, deleted = TRUE -> deleted depreserved formula */
409 typedef struct {
410  Biddy_Edge f;
411  Biddy_String name;
412  unsigned int expiry;
413  Biddy_Boolean deleted;
414 } BiddyFormula;
415 
416 typedef struct {
417  BiddyFormula *table;
418  unsigned int size;
419  unsigned int numOrdered; /* formulae with name are ordered */
420  Biddy_String deletedName; /* used to report deleted formulae */
421 } BiddyFormulaTable;
422 
423 /* CACHE LIST = unidirectional list */
424 typedef struct BiddyCacheList {
425  struct BiddyCacheList *next;
426  Biddy_GCFunction gc;
427 } BiddyCacheList;
428 
429 /* OP1 Cache = a fixed-size cache table for one-argument operations */
430 typedef struct {
431  Biddy_Edge result; /* biddy_null = not valid record! */
432  Biddy_Edge f;
433 } BiddyOp1Cache;
434 
435 typedef struct {
436  BiddyOp1Cache *table;
437  unsigned int size;
438  Biddy_Boolean disabled;
439  Biddy_Boolean notusedyet;
440  unsigned long long int *search;
441  unsigned long long int *find;
442 #ifdef BIDDYEXTENDEDSTATS_YES
443  unsigned long long int *insert;
444  unsigned long long int *overwrite;
445 #endif
446 } BiddyOp1CacheTable;
447 
448 /* OP2 Cache = a fixed-size cache table for two-arguments operations */
449 typedef struct {
450  Biddy_Edge result; /* biddy_null = not valid record! */
451  Biddy_Edge f,g;
452 } BiddyOp2Cache;
453 
454 typedef struct {
455  BiddyOp2Cache *table;
456  unsigned int size;
457  Biddy_Boolean disabled;
458  Biddy_Boolean notusedyet;
459  unsigned long long int *search;
460  unsigned long long int *find;
461 #ifdef BIDDYEXTENDEDSTATS_YES
462  unsigned long long int *insert;
463  unsigned long long int *overwrite;
464 #endif
465 } BiddyOp2CacheTable;
466 
467 /* OP3 Cache = a fixed-size cache table for three-arguments operations */
468 typedef struct {
469  Biddy_Edge result; /* biddy_null = not valid record! */
470  Biddy_Edge f,g,h;
471 } BiddyOp3Cache;
472 
473 typedef struct {
474  BiddyOp3Cache *table;
475  unsigned int size;
476  Biddy_Boolean disabled;
477  Biddy_Boolean *notusedyet;
478  unsigned long long int *search;
479  unsigned long long int *find;
480 #ifdef BIDDYEXTENDEDSTATS_YES
481  unsigned long long int *insert;
482  unsigned long long int *overwrite;
483 #endif
484 } BiddyOp3CacheTable;
485 
486 /* EA Cache = a fixed-size cache table intended for Biddy_E and Biddy_A */
487 /* Since Biddy v1.5, EA Cache is BiddyOp3Cache where variable is represented by h */
488 
489 /* RC Cache = a fixed-size cache table intended for Biddy_Restrict and Biddy_Compose */
490 /* Since Biddy v1.5, RC Cache is BiddyOp3Cache where variable is represented by h */
491 
492 /* Keyword Cache = a fixed-size cache table for one-argument operations */
493 /* Since Biddy v1.7, KeywordCache is used for Biddy_ReplaceByKeyword */
494 /* TO DO: use it also for other functions, e.g. copyBDD */
495 typedef struct {
496  Biddy_Edge result; /* biddy_null = not valid record! */
497  Biddy_Edge f;
498  unsigned int keyword;
499 } BiddyKeywordCache;
500 
501 typedef struct {
502  BiddyKeywordCache *table;
503  Biddy_String *keywordList;
504  unsigned int *keyList;
505  unsigned int keywordNum;
506  unsigned int keyNum;
507  unsigned int size;
508  Biddy_Boolean disabled;
509  Biddy_Boolean *notusedyet;
510  unsigned long long int *search;
511  unsigned long long int *find;
512 #ifdef BIDDYEXTENDEDSTATS_YES
513  unsigned long long int *insert;
514  unsigned long long int *overwrite;
515 #endif
516 } BiddyKeywordCacheTable;
517 
518 /* Manager = configuration of a BDD system, since Biddy v1.4 */
519 /* All fields in BiddyManager must be pointers or arrays */
520 /* Anonymous manager (i.e. anonymous namespace) is created by Biddy_Init */
521 /* BDD systems managed by different managers are completely independent */
522 /* (different node table, different caches, different system age etc.) */
523 /* User can create its own manager and use it instead of anonymous manager */
524 /* All managers are of type void** but internally they have the structure */
525 /* given here (see function Biddy_Init for details). */
526 /* NOTE: names of elements given here are not used in the program! */
527 typedef struct {
528  void *name; /* this is typecasted to Biddy_String */
529  void *type; /* this is typecasted to (short int*) */
530  void *terminalEdge; /* this is typecasted to (void *) */
531  void *constantZero; /* this is typecasted to Biddy_Edge */
532  void *constantOne; /* this is typecasted to Biddy_Edge */
533  void *nodeTable; /* this is typecasted to (BiddyNodeTable*) */
534  void *variableTable; /* this is typecasted to (BiddyVariableTable*) */
535  void *formulaTable; /* this is typecasted to (BiddyFormulaTable*) */
536  void *OPcache; /* this is typecasted to (BiddyOp3CacheTable*) */
537  void *EAcache; /* this is typecasted to (BiddyOp3CacheTable*) */
538  void *RCcache; /* this is typecasted to (BiddyOp3CacheTable*) */
539  void *REPLACEcache; /* this is typecasted to (BiddyKeywordCacheTable*) */
540  void *cacheList; /* this is typecasted to (BiddyCacheList*) */
541  void *freeNodes; /* this is typecasted to (BiddyNode*) */
542  void *ordering; /* this is typecasted to (BiddyOrderingTable*) */
543  void *age; /* this is typecasted to (unsigned int*) */
544  void *selector; /* this is typecasted to (unsigned short int*) */
545 } BiddyManager;
546 
547 /* LocalInfo = a table for additional info about nodes, since Biddy v1.4 */
548 /* Created only if needed and deleted before normal operations */
549 /* It reuses pointer which is normally used for garbage collection! */
550 /* Only one element of the union can be used! */
551 typedef struct {
552  BiddyNode *back; /* reference to node */
553  BiddyNode *org; /* original pointer, used when deleting local cache */
554  union {
555  unsigned int enumerator; /* used in enumerateNodes */
556  BiddyNode *copy; /* used in BiddyCopy */
557  unsigned int npSelected; /* used in nodePlainNumber and nodeVarNumber */
558  /* NOTE: positiveSelected iff (data.npSelected & 1 != 0) */
559  /* NOTE: negativeSelected iff (data.npSelected & 2 != 0) */
560  unsigned long long int path1Count; /* used in pathCount */
561  double path1Probability; /* used in pathProbabilitySum */
562  mpz_t mintermCount; /* used in mintermCount, represented using GMP library */
563  } data;
564  union {
565  Biddy_Boolean leftmost; /* used in pathCount and pathProbabilitySum for ZBDDs, only */
566  unsigned long long int path0Count; /* used in pathCount for OBDDs, only */
567  double path0Probability; /* used in pathProbabilitySum for OBDDs, only */
568  } datax;
569 } BiddyLocalInfo;
570 
571 /* BiddyVariableOrder is used in Biddy_ConstructBDD, since Biddy v1.8 */
572 typedef struct {
573  Biddy_String name;
574  int order;
575 } BiddyVariableOrder;
576 
577 /* BiddyNodeList is used in Biddy_ConstructBDD, since Biddy v1.8 */
578 typedef struct {
579  Biddy_String name;
580  int id;
581  int type;
582  int l,r;
583  Biddy_Variable ltag,rtag;
584  Biddy_Edge f;
585  Biddy_Boolean created;
586 } BiddyNodeList;
587 
588 /* BiddyXY is used in Biddy_WriteBDDView, since Biddy v1.8 */
589 /* this is used to pass node coordinates */
590 typedef struct {
591  int id;
592  Biddy_String label;
593  int x;
594  int y;
595  Biddy_Boolean isConstant;
596 } BiddyXY;
597 
598 /* BiddyBTreeNode and BiddyBTreeContainer are used in Biddy_Eval2, since Biddy v1.8 */
599 typedef struct {
600  int parent;
601  int left;
602  int right;
603  int index;
604  unsigned char op;
605  Biddy_String name;
606 } BiddyBTreeNode;
607 
608 typedef struct {
609  BiddyBTreeNode *tnode;
610  int availableNode;
611 } BiddyBTreeContainer;
612 
613 /* BiddyVarList is used in in Biddy_PrintfSOP and Biddy_WriteSOP, since Biddy v1.8 */
614 typedef struct BiddyVarList {
615  struct BiddyVarList *next;
616  Biddy_Variable v;
617  Biddy_Boolean negative;
618 } BiddyVarList;
619 
620 /* BiddyVerilogLine, BiddyVerilogNode, BiddyVerilogWire, BiddyVerilogModule, and */
621 /* BiddyVerilogCircuit are used in Biddy_ReadVerilogFile, since Biddy v1.8 */
622 
623 typedef struct { /* table of lines is used to store acceptable lines */
624  Biddy_String keyword;
625  Biddy_String line;
626 } BiddyVerilogLine;
627 
628 typedef struct { /* table of nodes is used to store names of all symbols */
629  Biddy_String type; /* input, output, wire, gate, extern */
630  Biddy_String name; /* node name */
631 } BiddyVerilogNode;
632 
633 typedef struct { /* wires are primary inputs and gates */
634  int id; /* input/gate ID number */
635  Biddy_String type; /* type of a signal driving this wire, "I" for primary input, "W" for internal wire */
636  unsigned int inputcount; /* number of input/gate inputs */
637  int inputs[INOUTNUM]; /* array of inputs */
638  unsigned int outputcount; /* number of input/gate outputs - currently not used */
639  int outputs[INOUTNUM]; /* array of outputs - currently not used */
640  int fanout; /* how many times this wire is used as an input to some gate or another wire */
641  int ttl; /* tmp nuber used to guide GC during the creation of BDD */
642  Biddy_Edge bdd; /* BDD associated with the wire/gate */
643 } BiddyVerilogWire;
644 
645 typedef struct {
646  char *name; /* name of the module */
647  Biddy_Boolean outputFirst; /* TRUE iff "nand NAND2_1 (N1, N2, N3);" defines N1 = NAND(N2,N3) */
648  unsigned int inputcount, outputcount; /* count of primary inputs and primary outputs. */
649  unsigned int wirecount, regcount, gatecount; /* count of wires ,regs, gates */
650  Biddy_String inputs[INOUTNUM], outputs[INOUTNUM]; /* name list of primary inputs and primary outputs in the netlist */
651  Biddy_String wires[WIRENUM]; /* name list of wires in the netlist */
652  Biddy_String regs[REGNUM]; /* name list of regs in the netlist */
653  Biddy_String gates[GATENUM]; /* name list of gates in the netlist */
654 } BiddyVerilogModule;
655 
656 typedef struct {
657  Biddy_String name; /* name of the circuit */
658  unsigned int inputcount, outputcount; /* number of primary inputs and primary outputs */
659  unsigned int nodecount, wirecount; /* number of nodes and wires */
660  Biddy_String inputs[INOUTNUM], outputs[INOUTNUM]; /* name list of primary inputs and primary outputs in the netlist */
661  BiddyVerilogWire **wires; /* array of all wires */
662  BiddyVerilogNode **nodes; /* array of nodes */
663 } BiddyVerilogCircuit;
664 
665 /*----------------------------------------------------------------------------*/
666 /* Variable declarations */
667 /*----------------------------------------------------------------------------*/
668 
669 extern Biddy_Manager biddyAnonymousManager; /* anonymous manager */
670 
671 extern BiddyLocalInfo *biddyLocalInfo; /* reference to Local Info */
672 
673 /*----------------------------------------------------------------------------*/
674 /* Prototypes for internal functions defined in biddyMain.c */
675 /*----------------------------------------------------------------------------*/
676 
677 #define BiddyManagedFoaNode(MNG,v,pf,pt,garbageAllowed) BiddyManagedTaggedFoaNode(MNG,v,pf,pt,v,garbageAllowed)
678 extern Biddy_Edge BiddyManagedTaggedFoaNode(Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge pf, Biddy_Edge pt, Biddy_Variable ptag, Biddy_Boolean garbageAllowed);
679 
680 extern void BiddyIncSystemAge(Biddy_Manager MNG);
681 extern void BiddyDecSystemAge(Biddy_Manager MNG);
682 void BiddyCompactSystemAge(Biddy_Manager MNG);
683 extern void BiddyProlongRecursively(Biddy_Manager MNG, Biddy_Edge f, unsigned int c, Biddy_Variable target);
684 
685 extern Biddy_Variable BiddyCreateLocalInfo(Biddy_Manager MNG, Biddy_Edge f);
686 extern void BiddyDeleteLocalInfo(Biddy_Manager MNG, Biddy_Edge f);
687 extern unsigned int BiddyGetSeqByNode(Biddy_Edge root, Biddy_Edge f);
688 extern Biddy_Edge BiddyGetNodeBySeq(Biddy_Edge root, unsigned int n);
689 extern void BiddySetEnumerator(Biddy_Edge f, unsigned int n);
690 extern unsigned int BiddyGetEnumerator(Biddy_Edge f);
691 extern void BiddySetCopy(Biddy_Edge f, BiddyNode *n);
692 extern BiddyNode * BiddyGetCopy(Biddy_Edge f);
693 extern void BiddySetPath1Count(Biddy_Edge f, unsigned long long int value);
694 extern unsigned long long int BiddyGetPath1Count(Biddy_Edge f);
695 extern void BiddySetPath0Count(Biddy_Edge f, unsigned long long int value);
696 extern unsigned long long int BiddyGetPath0Count(Biddy_Edge f);
697 extern void BiddySetPath1ProbabilitySum(Biddy_Edge f, double value);
698 extern double BiddyGetPath1ProbabilitySum(Biddy_Edge f);
699 extern void BiddySetPath0ProbabilitySum(Biddy_Edge f, double value);
700 extern double BiddyGetPath0ProbabilitySum(Biddy_Edge f);
701 extern void BiddySetLeftmost(Biddy_Edge f, Biddy_Boolean value);
702 extern Biddy_Boolean BiddyGetLeftmost(Biddy_Edge f);
703 extern void BiddySetMintermCount(Biddy_Edge f, mpz_t value);
704 extern void BiddyGetMintermCount(Biddy_Edge f, mpz_t result);
705 extern void BiddySelectNP(Biddy_Edge f);
706 extern Biddy_Boolean BiddyIsSelectedNP(Biddy_Edge f);
707 
708 extern Biddy_Boolean BiddyGlobalSifting(Biddy_Manager MNG, Biddy_Boolean converge);
709 extern Biddy_Boolean BiddySiftingOnFunction(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean converge);
710 extern Biddy_Boolean BiddySiftingOnFunctionDirect(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean converge);
711 extern void BiddySjtInit(Biddy_Manager MNG);
712 extern void BiddySjtExit(Biddy_Manager MNG);
713 extern Biddy_Boolean BiddySjtStep(Biddy_Manager MNG);
714 extern void BiddySetOrdering(Biddy_Manager MNG, BiddyOrderingTable ordering);
715 extern void BiddySetOrderingByData(Biddy_Manager MNG, BiddyOrderingTable ordering);
716 
717 extern Biddy_Edge BiddyCopy(Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_Edge f);
718 extern Biddy_Edge BiddyCopyOBDD(Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_Edge f);
719 extern Biddy_Edge BiddyCopyZBDD(Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_Edge f);
720 extern Biddy_Edge BiddyCopyTZBDD(Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_Edge f);
721 extern Biddy_Edge BiddyConvertDirect(Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_Edge f);
722 Biddy_Edge BiddyConstructBDD(Biddy_Manager MNG, int numN, BiddyNodeList *tableN);
723 
724 extern void BiddyOPGarbage(Biddy_Manager MNG);
725 extern void BiddyOPGarbageNewVariable(Biddy_Manager MNG, Biddy_Variable v);
726 extern void BiddyOPGarbageDeleteAll(Biddy_Manager MNG);
727 extern void BiddyEAGarbage(Biddy_Manager MNG);
728 extern void BiddyEAGarbageNewVariable(Biddy_Manager MNG, Biddy_Variable v);
729 extern void BiddyEAGarbageDeleteAll(Biddy_Manager MNG);
730 extern void BiddyRCGarbage(Biddy_Manager MNG);
731 extern void BiddyRCGarbageNewVariable(Biddy_Manager MNG, Biddy_Variable v);
732 extern void BiddyRCGarbageDeleteAll(Biddy_Manager MNG);
733 extern void BiddyReplaceGarbage(Biddy_Manager MNG);
734 extern void BiddyReplaceGarbageNewVariable(Biddy_Manager MNG, Biddy_Variable v);
735 extern void BiddyReplaceGarbageDeleteAll(Biddy_Manager MNG);
736 
737 extern void BiddySystemReport(Biddy_Manager MNG);
738 extern void BiddyFunctionReport(Biddy_Manager MNG, Biddy_Edge f);
739 extern void BiddyDebugNode(Biddy_Manager MNG, BiddyNode *node);
740 extern void BiddyDebugEdge(Biddy_Manager MNG, Biddy_Edge edge);
741 
742 /*----------------------------------------------------------------------------*/
743 /* Prototypes for internal functions defined in biddyOp.c */
744 /*----------------------------------------------------------------------------*/
745 
746 extern Biddy_Edge BiddyManagedNot(const Biddy_Manager MNG, const Biddy_Edge f);
747 extern Biddy_Edge BiddyManagedITE(const Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Edge h);
748 extern Biddy_Edge BiddyManagedAnd(const Biddy_Manager MNG, const Biddy_Edge f, const Biddy_Edge g);
749 extern Biddy_Edge BiddyManagedOr(const Biddy_Manager MNG, const Biddy_Edge f, const Biddy_Edge g);
750 extern Biddy_Edge BiddyManagedNand(const Biddy_Manager MNG, const Biddy_Edge f, const Biddy_Edge g);
751 extern Biddy_Edge BiddyManagedNor(const Biddy_Manager MNG, const Biddy_Edge f, const Biddy_Edge g);
752 extern Biddy_Edge BiddyManagedXor(const Biddy_Manager MNG, const Biddy_Edge f, const Biddy_Edge g);
753 extern Biddy_Edge BiddyManagedXnor(const Biddy_Manager MNG, const Biddy_Edge f, const Biddy_Edge g);
754 extern Biddy_Edge BiddyManagedLeq(const Biddy_Manager MNG, const Biddy_Edge f, const Biddy_Edge g);
755 extern Biddy_Edge BiddyManagedGt(const Biddy_Manager MNG, const Biddy_Edge f, const Biddy_Edge g);
756 
757 extern Biddy_Edge BiddyManagedRestrict(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v, Biddy_Boolean value);
758 extern Biddy_Edge BiddyManagedCompose(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Variable v);
759 extern Biddy_Edge BiddyManagedE(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v);
760 extern Biddy_Edge BiddyManagedA(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v);
761 extern Biddy_Edge BiddyManagedExistAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge cube);
762 extern Biddy_Edge BiddyManagedUnivAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge cube);
763 extern Biddy_Edge BiddyManagedAndAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Edge cube);
764 extern Biddy_Edge BiddyManagedConstrain(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge c);
765 extern Biddy_Edge BiddyManagedSimplify(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge c);
766 extern Biddy_Edge BiddyManagedSupport(Biddy_Manager MNG, Biddy_Edge f);
767 extern Biddy_Edge BiddyManagedReplaceByKeyword(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable topv, const unsigned int key);
768 extern Biddy_Edge BiddyManagedChange(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v);
769 extern Biddy_Edge BiddyManagedSubset(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v, Biddy_Boolean value);
770 
771 #define BiddyManagedUnion(MNG,f,g) BiddyManagedOr(MNG,f,g)
772 #define BiddyManagedIntersect(MNG,f,g) BiddyManagedAnd(MNG,f,g)
773 #define BiddyManagedDiff(MNG,f,g) BiddyManagedGt(MNG,g,f)
774 
775 /*----------------------------------------------------------------------------*/
776 /* Prototypes for internal functions defined in biddyStat.c */
777 /*----------------------------------------------------------------------------*/
778 
779 extern void BiddyNodeNumber(Biddy_Manager MNG, Biddy_Edge f, unsigned int *n);
780 extern void BiddyComplementedEdgeNumber(Biddy_Manager MNG, Biddy_Edge f, unsigned int *n);
781 extern void BiddyNodeVarNumber(Biddy_Manager MNG, Biddy_Edge f, unsigned int *n);
782 
783 /*----------------------------------------------------------------------------*/
784 /* Prototypes for internal functions defined in biddyInOut.c */
785 /*----------------------------------------------------------------------------*/
786 
787 #endif /* _BIDDYINT */
Biddy_Variable is used for indices in variable table.
Biddy_Edge is a marked edge (i.e. a marked pointer to BiddyNode).
Biddy_String is used for strings.
Biddy_GCFunction is used in Biddy_AddCache to specify user&#39;s function which will performs garbage col...
Biddy_Boolean is used for boolean values.
File biddy.h contains declaration of all external data structures.
Biddy_Manager is used to specify manager.