Biddy  1.8.1
An academic Binary Decision Diagrams package
biddyMain.c
Go to the documentation of this file.
1 /***************************************************************************/
44 #include "biddyInt.h"
45 
46 #ifdef UNIX
47 #include <unistd.h> /* used for sysconf(), UNIX only */
48 #include <sys/resource.h> /* used for setrlimit(), UNIX only */
49 #endif
50 
51 #ifdef UNIXXX
52 #include <malloc.h> /* experimental */
53 #endif
54 
55 /*----------------------------------------------------------------------------*/
56 /* Constant declarations */
57 /*----------------------------------------------------------------------------*/
58 
59 /* ALL SIZES ARE unsigned int */
60 /* Size of node and cache tables must be 2^N-1 */
61 /* e.g. 2^16-1 = 65535, 2^20-1 = 1048575, 2^24-1 = 16777215 */
62 
63 /* If BDD node is 24B (e.g. 32-bit GNU/Linux systems) */
64 /* 256 nodes is 6 kB */
65 /* 65536 nodes is 1.5 MB */
66 /* 262144 nodes is 6 MB */
67 /* 524288 nodes is 12 MB */
68 /* 1048576 nodes is 24.0 MB */
69 /* 2097152 nodes is 48.0 MB */
70 /* 4194304 nodes is 96.0 MB */
71 /* 8388608 nodes is 192.0 MB */
72 /* 16777216 nodes is 384.0 MB */
73 
74 /* If BDD node is 48B (e.g. 64-bit GNU/Linux systems), then: */
75 /* 256 nodes is 12 kB */
76 /* 65536 nodes is 3.0 MB */
77 /* 262144 nodes is 12 MB */
78 /* 524288 nodes is 24 MB */
79 /* 1048576 nodes is 48.0 MB */
80 /* 2097152 nodes is 96.0 MB */
81 /* 4194304 nodes is 192.0 MB */
82 /* 8388608 nodes is 384.0 MB */
83 /* 16777216 nodes is 768.0 MB */
84 
85 #define TINY_SIZE 1023
86 #define SMALL_SIZE 65535
87 #define MEDIUM_SIZE 262143
88 #define LARGE_SIZE 1048575
89 #define XLARGE_SIZE 2097151
90 #define XXLARGE_SIZE 4194303
91 #define XXXLARGE_SIZE 8388607
92 #define HUGE_SIZE 16777215
93 
94 /*----------------------------------------------------------------------------*/
95 /* Variable declarations */
96 /*----------------------------------------------------------------------------*/
97 
98 /* EXPORTED VARIABLES */
99 
100 #ifdef __cplusplus
101 extern "C" {
102 #endif
103 
104 #ifdef __cplusplus
105 }
106 #endif
107 
108 /* INTERNAL VARIABLES */
109 
110 Biddy_Manager biddyAnonymousManager /* anonymous manager */
111  = NULL;
112 
113 BiddyLocalInfo *biddyLocalInfo /* local info table */
114  = NULL;
115 
116 /* Biddy_Edge debug_edge = NULL; */ /* debugging, only */
117 /* Biddy_Boolean biddySiftingActive = FALSE; */ /* debugging, only */
118 
119 /*----------------------------------------------------------------------------*/
120 /* Static function prototypes */
121 /*----------------------------------------------------------------------------*/
122 
123 static Biddy_Boolean isEqv(Biddy_Manager MNG1, Biddy_Edge f1, Biddy_Manager MNG2, Biddy_Edge f2);
124 static BiddyLocalInfo * createLocalInfo(Biddy_Manager MNG, Biddy_Edge f, BiddyLocalInfo *c);
125 static void deleteLocalInfo(Biddy_Manager MNG, Biddy_Edge f);
126 static inline unsigned int nodeTableHash(Biddy_Variable v, Biddy_Edge pf, Biddy_Edge pt, unsigned int size);
127 static inline void addNodeTable(Biddy_Manager MNG, unsigned int hash, BiddyNode *node, BiddyNode *sup1);
128 static inline BiddyNode *findNodeTable(Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge pf, Biddy_Edge pt, BiddyNode **thesup);
129 static Biddy_Edge addVariableElement(Biddy_Manager MNG, Biddy_String x);
130 static void evalProbability(Biddy_Manager MNG, Biddy_Edge f, double *c1, double *c0, Biddy_Boolean *leftmost);
131 static Biddy_Boolean checkFunctionOrdering(Biddy_Manager MNG, Biddy_Edge f);
132 static Biddy_Variable getGlobalOrdering(Biddy_Manager MNG, Biddy_Variable v);
133 static Biddy_Variable swapWithHigher(Biddy_Manager MNG, Biddy_Variable v, Biddy_Boolean *active);
134 static Biddy_Variable swapWithLower(Biddy_Manager MNG, Biddy_Variable v, Biddy_Boolean *active);
135 static void swapVariables(Biddy_Manager MNG, Biddy_Variable low, Biddy_Variable high, Biddy_Boolean *active);
136 static void oneSwap(Biddy_Manager MNG, BiddyNode *sup, Biddy_Variable low, Biddy_Variable high, Biddy_Edge *u0, Biddy_Edge *u1);
137 static void oneSwapEdge(Biddy_Manager MNG, Biddy_Edge sup, Biddy_Variable low, Biddy_Variable high, Biddy_Edge *u, Biddy_Boolean *active);
138 static void nullOrdering(BiddyOrderingTable table);
139 static void alphabeticOrdering(Biddy_Manager MNG, BiddyOrderingTable table);
140 static void nodeNumberOrdering(Biddy_Manager MNG, Biddy_Edge f, unsigned int *i, BiddyOrderingTable ordering);
141 static void reorderVariables(Biddy_Manager MNG, int numV, BiddyVariableOrder *tableV, int numN, BiddyNodeList *tableN, int id);
142 static void constructBDD(Biddy_Manager MNG, int numN, BiddyNodeList *tableN, int id);
143 static void warshall(BiddyOrderingTable table, Biddy_Variable varnum);
144 static void writeBDD(Biddy_Manager MNG, Biddy_Edge f);
145 static void writeORDER(Biddy_Manager MNG);
146 static void debugNode(Biddy_Manager MNG, BiddyNode *node);
147 static void debugEdge(Biddy_Manager MNG, Biddy_Edge edge);
148 static void debugORDERING(Biddy_Manager MNG, BiddyOrderingTable table, Biddy_Variable varnum);
149 
150 /*----------------------------------------------------------------------------*/
151 /* Definition of exported functions */
152 /*----------------------------------------------------------------------------*/
153 
154 /***************************************************************************/
172 #ifdef __cplusplus
173 extern "C" {
174 #endif
175 
176 void
177 Biddy_InitMNG(Biddy_Manager *mng, int bddtype)
178 {
179  unsigned int i,j;
180  Biddy_Manager MNG;
181 
182 #ifdef UNIX
183  struct rlimit rl;
184 #endif
185 
186 #ifdef UNIX
187  /* printf("The page size for this system is %ld bytes.\n", sysconf(_SC_PAGESIZE)); */
188  rl.rlim_max = rl.rlim_cur = RLIM_INFINITY;
189  if (setrlimit(RLIMIT_STACK, &rl)) {
190  fprintf(stderr,"ERROR: setrlimit\n");
191  perror("setrlimit");
192  exit(1);
193  }
194 #endif
195 
196 #ifdef UNIXXX
197  mallopt(M_MMAP_MAX,0);
198  mallopt(M_TRIM_THRESHOLD,-1);
199 #endif
200 
201  /* RANDOM NUMBERS GENERATOR */
202  srand((unsigned int) time(NULL));
203 
204  if (!mng) {
205  if (!(biddyAnonymousManager = (Biddy_Manager) malloc(sizeof(BiddyManager)))) {
206  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
207  exit(1);
208  }
209  MNG = biddyAnonymousManager;
210  } else {
211  if (!(*mng = (Biddy_Manager) malloc(sizeof(BiddyManager)))) {
212  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
213  exit(1);
214  }
215  MNG = *mng;
216  }
217 
218  /* DEBUGGING */
219  /*
220  printf("DEBUG (Biddy_InitMNG): Biddy_InitMNG STARTED\n");
221  printf("DEBUG (Biddy_InitMNG): mng = %p\n",mng);
222  printf("DEBUG (Biddy_InitMNG): bddtype = %d\n",bddtype);
223  printf("DEBUG (Biddy_InitMNG): MNG = %p\n",MNG);
224  */
225 
226  /* CREATION OF MANAGER'S STRUCTURES - VALUES ARE NOT INITIALIZED HERE */
227  MNG[0] = NULL; /* biddyManagerName */
228  if (!(MNG[1] = (short int *) malloc(sizeof(short int)))) {
229  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
230  exit(1);
231  }
232  biddyManagerType = 0;
233  MNG[2] = NULL; /* biddyTerminal */
234  MNG[3] = NULL; /* biddyZero */
235  MNG[4] = NULL; /* biddyOne */
236  if (!(MNG[5] = (BiddyNodeTable *) malloc(sizeof(BiddyNodeTable)))) {
237  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
238  exit(1);
239  }
240  biddyNodeTable.table = NULL;
241  biddyNodeTable.blocktable = NULL;
242  biddyNodeTable.initsize = 0;
243  biddyNodeTable.size = 0;
244  biddyNodeTable.limitsize = 0;
245  biddyNodeTable.blocknumber = 0;
246  biddyNodeTable.initblocksize = 0;
247  biddyNodeTable.blocksize = 0;
248  biddyNodeTable.limitblocksize = 0;
249  biddyNodeTable.generated = 0;
250  biddyNodeTable.max = 0;
251  biddyNodeTable.num = 0;
252  biddyNodeTable.garbage = 0;
253  biddyNodeTable.swap = 0;
254  biddyNodeTable.sifting = 0;
255  biddyNodeTable.nodetableresize = 0;
256  biddyNodeTable.funite = 0;
257  biddyNodeTable.funandor = 0;
258  biddyNodeTable.funxor = 0;
259  biddyNodeTable.gctime = 0;
260  biddyNodeTable.drtime = 0;
261  biddyNodeTable.gcratio = 0.0;
262  biddyNodeTable.gcratioF = 0.0;
263  biddyNodeTable.gcratioX = 0.0;
264  biddyNodeTable.resizeratio = 0.0;
265  biddyNodeTable.resizeratioF = 0.0;
266  biddyNodeTable.resizeratioX = 0.0;
267  biddyNodeTable.siftingtreshold = 0.0;
268  biddyNodeTable.convergesiftingtreshold = 0.0;
269 #ifdef BIDDYEXTENDEDSTATS_YES
270  biddyNodeTable.foa = 0;
271  biddyNodeTable.find = 0;
272  biddyNodeTable.compare = 0;
273  biddyNodeTable.add = 0;
274  biddyNodeTable.iterecursive = 0;
275  biddyNodeTable.andorrecursive = 0;
276  biddyNodeTable.xorrecursive = 0;
277  biddyNodeTable.gcobsolete = NULL;
278 #endif
279  if (!(MNG[6] = (BiddyVariableTable *) malloc(sizeof(BiddyVariableTable)))) {
280  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
281  exit(1);
282  }
283  biddyVariableTable.table = NULL;
284  biddyVariableTable.lookup = NULL;
285  biddyVariableTable.size = 0;
286  biddyVariableTable.num = 0;
287  biddyVariableTable.numnum = 0;
288  if (!(MNG[7] = (BiddyFormulaTable *) malloc(sizeof(BiddyFormulaTable)))) {
289  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
290  exit(1);
291  }
292  biddyFormulaTable.table = NULL;
293  biddyFormulaTable.size = 0;
294  biddyFormulaTable.numOrdered = 0;
295  biddyFormulaTable.deletedName = NULL;
296  if (!(MNG[8] = (BiddyOp3CacheTable *) malloc(sizeof(BiddyOp3CacheTable)))) {
297  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
298  exit(1);
299  }
300  biddyOPCache.table = NULL;
301  biddyOPCache.size = 0;
302  biddyOPCache.disabled = FALSE;
303  if (!(biddyOPCache.notusedyet = (Biddy_Boolean *) malloc(sizeof(Biddy_Boolean)))) {
304  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
305  exit(1);
306  }
307  *(biddyOPCache.notusedyet) = FALSE;
308  if (!(biddyOPCache.search = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
309  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
310  exit(1);
311  }
312  if (!(biddyOPCache.find = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
313  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
314  exit(1);
315  }
316 #ifdef BIDDYEXTENDEDSTATS_YES
317  if (!(biddyOPCache.insert = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
318  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
319  exit(1);
320  }
321  if (!(biddyOPCache.overwrite = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
322  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
323  exit(1);
324  }
325 #endif
326  *(biddyOPCache.search) = 0;
327  *(biddyOPCache.find) = 0;
328 #ifdef BIDDYEXTENDEDSTATS_YES
329  *(biddyOPCache.insert) = 0;
330  *(biddyOPCache.overwrite) = 0;
331 #endif
332  if (!(MNG[9] = (BiddyOp3CacheTable *) malloc(sizeof(BiddyOp3CacheTable)))) {
333  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
334  exit(1);
335  }
336  biddyEACache.table = NULL;
337  biddyEACache.size = 0;
338  biddyEACache.disabled = FALSE;
339  if (!(biddyEACache.notusedyet = (Biddy_Boolean *) malloc(sizeof(Biddy_Boolean)))) {
340  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
341  exit(1);
342  }
343  *(biddyEACache.notusedyet) = FALSE;
344  if (!(biddyEACache.search = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
345  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
346  exit(1);
347  }
348  if (!(biddyEACache.find = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
349  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
350  exit(1);
351  }
352 #ifdef BIDDYEXTENDEDSTATS_YES
353  if (!(biddyEACache.insert = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
354  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
355  exit(1);
356  }
357  if (!(biddyEACache.overwrite = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
358  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
359  exit(1);
360  }
361 #endif
362  *(biddyEACache.search) = 0;
363  *(biddyEACache.find) = 0;
364 #ifdef BIDDYEXTENDEDSTATS_YES
365  *(biddyEACache.insert) = 0;
366  *(biddyEACache.overwrite) = 0;
367 #endif
368  if (!(MNG[10] = (BiddyOp3CacheTable *) malloc(sizeof(BiddyOp3CacheTable)))) {
369  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
370  exit(1);
371  }
372  biddyRCCache.table = NULL;
373  biddyRCCache.size = 0;
374  biddyRCCache.disabled = FALSE;
375  if (!(biddyRCCache.notusedyet = (Biddy_Boolean *) malloc(sizeof(Biddy_Boolean)))) {
376  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
377  exit(1);
378  }
379  *(biddyRCCache.notusedyet) = FALSE;
380  if (!(biddyRCCache.search = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
381  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
382  exit(1);
383  }
384  if (!(biddyRCCache.find = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
385  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
386  exit(1);
387  }
388 #ifdef BIDDYEXTENDEDSTATS_YES
389  if (!(biddyRCCache.insert = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
390  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
391  exit(1);
392  }
393  if (!(biddyRCCache.overwrite = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
394  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
395  exit(1);
396  }
397 #endif
398  *(biddyRCCache.search) = 0;
399  *(biddyRCCache.find) = 0;
400 #ifdef BIDDYEXTENDEDSTATS_YES
401  *(biddyRCCache.insert) = 0;
402  *(biddyRCCache.overwrite) = 0;
403 #endif
404  if (!(MNG[11] = (BiddyKeywordCacheTable *) malloc(sizeof(BiddyKeywordCacheTable)))) {
405  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
406  exit(1);
407  }
408  biddyReplaceCache.table = NULL;
409  biddyReplaceCache.size = 0;
410  biddyReplaceCache.keywordList = NULL;
411  biddyReplaceCache.keyList = NULL;
412  biddyReplaceCache.keyNum = 0;
413  biddyReplaceCache.keywordNum = 0;
414  biddyReplaceCache.disabled = FALSE;
415  if (!(biddyReplaceCache.notusedyet = (Biddy_Boolean *) malloc(sizeof(Biddy_Boolean)))) {
416  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
417  exit(1);
418  }
419  *(biddyReplaceCache.notusedyet) = FALSE;
420  if (!(biddyReplaceCache.search = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
421  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
422  exit(1);
423  }
424  if (!(biddyReplaceCache.find = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
425  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
426  exit(1);
427  }
428 #ifdef BIDDYEXTENDEDSTATS_YES
429  if (!(biddyReplaceCache.insert = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
430  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
431  exit(1);
432  }
433  if (!(biddyReplaceCache.overwrite = (unsigned long long int *) malloc(sizeof(unsigned long long int)))) {
434  fprintf(stderr, "Biddy_InitMNG: Out of memoy!\n");
435  exit(1);
436  }
437 #endif
438  *(biddyReplaceCache.search) = 0;
439  *(biddyReplaceCache.find) = 0;
440 #ifdef BIDDYEXTENDEDSTATS_YES
441  *(biddyReplaceCache.insert) = 0;
442  *(biddyReplaceCache.overwrite) = 0;
443 #endif
444  if (!(MNG[12] = (BiddyCacheList* *) malloc(sizeof(BiddyCacheList*)))) {
445  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
446  exit(1);
447  }
448  biddyCacheList = NULL;
449  if (!(MNG[13] = (BiddyNode* *) malloc(sizeof(BiddyNode*)))) {
450  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
451  exit(1);
452  }
453  biddyFreeNodes = NULL;
454  if (!(MNG[14] = (BiddyOrderingTable *) malloc(sizeof(BiddyOrderingTable)))) {
455  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
456  exit(1);
457  }
458  if (!(MNG[15] = (unsigned int *) malloc(sizeof(unsigned int)))) {
459  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
460  exit(1);
461  }
462  biddySystemAge = 0;
463  if (!(MNG[16] = (unsigned short int *) malloc(sizeof(unsigned short int)))) {
464  fprintf(stderr,"Biddy_InitMNG: Out of memoy!\n");
465  exit(1);
466  }
467  biddySelect = 0;
468 
469  /* INITIALIZATION OF MANAGER'S STRUCTURES - VALUES ARE NOW INITIALIZED */
470  if (bddtype == BIDDYTYPEOBDD) {
471  MNG[0] = strdup(BIDDYTYPENAMEOBDD); /* biddyManagerName */
472  } else if (bddtype == BIDDYTYPEOBDDC) {
473  MNG[0] = strdup(BIDDYTYPENAMEOBDDC); /* biddyManagerName */
474  } else if (bddtype == BIDDYTYPEZBDD) {
475  MNG[0] = strdup(BIDDYTYPENAMEZBDD); /* biddyManagerName */
476  } else if (bddtype == BIDDYTYPEZBDDC) {
477  MNG[0] = strdup(BIDDYTYPENAMEZBDDC); /* biddyManagerName */
478  } else if (bddtype == BIDDYTYPETZBDD) {
479 #if UINTPTR_MAX == 0xffffffffffffffff
480 #else
481  fprintf(stderr,"Biddy_InitMNG: TZBDDs are supported on 64-bit architecture, only!\n");
482  exit(1);
483 #endif
484  MNG[0] = strdup(BIDDYTYPENAMETZBDD); /* biddyManagerName */
485  } else if (bddtype == BIDDYTYPETZBDDC) {
486 #if UINTPTR_MAX == 0xffffffffffffffff
487 #else
488  fprintf(stderr,"Biddy_InitMNG: TZBDDs are supported on 64-bit architecture, only!\n");
489  exit(1);
490 #endif
491  MNG[0] = strdup(BIDDYTYPENAMETZBDDC); /* biddyManagerName */
492  fprintf(stderr,"Biddy_InitMNG: %s is not supported, yet!\n",BIDDYTYPENAMETZBDDC);
493  exit(1);
494  } else if (bddtype == BIDDYTYPEOFDD) {
495  MNG[0] = strdup(BIDDYTYPENAMEOFDD); /* biddyManagerName */
496  fprintf(stderr,"Biddy_InitMNG: %s is not supported, yet!\n",BIDDYTYPENAMEOFDD);
497  exit(1);
498  } else if (bddtype == BIDDYTYPEOFDDC) {
499  MNG[0] = strdup(BIDDYTYPENAMEOFDDC); /* biddyManagerName */
500  fprintf(stderr,"Biddy_InitMNG: %s is not supported, yet!\n",BIDDYTYPENAMEOFDDC);
501  exit(1);
502  } else if (bddtype == BIDDYTYPEZFDD) {
503  MNG[0] = strdup(BIDDYTYPENAMEZFDD); /* biddyManagerName */
504  fprintf(stderr,"Biddy_InitMNG: %s is not supported, yet!\n",BIDDYTYPENAMEZFDD);
505  exit(1);
506  } else if (bddtype == BIDDYTYPEZFDDC) {
507  MNG[0] = strdup(BIDDYTYPENAMEZFDDC); /* biddyManagerName */
508  fprintf(stderr,"Biddy_InitMNG: %s is not supported, yet!\n",BIDDYTYPENAMEZFDDC);
509  exit(1);
510  } else if (bddtype == BIDDYTYPETZFDD) {
511 #if UINTPTR_MAX == 0xffffffffffffffff
512 #else
513  fprintf(stderr,"Biddy_InitMNG: TZFDDs are supported on 64-bit architecture, only!\n");
514  exit(1);
515 #endif
516  MNG[0] = strdup(BIDDYTYPENAMETZFDD); /* biddyManagerName */
517  fprintf(stderr,"Biddy_InitMNG: %s is not supported, yet!\n",BIDDYTYPENAMETZFDD);
518  exit(1);
519  } else if (bddtype == BIDDYTYPETZFDDC) {
520 #if UINTPTR_MAX == 0xffffffffffffffff
521 #else
522  fprintf(stderr,"Biddy_InitMNG: TZFDDs are supported on 64-bit architecture, only!\n");
523  exit(1);
524 #endif
525  MNG[0] = strdup(BIDDYTYPENAMETZFDDC); /* biddyManagerName */
526  fprintf(stderr,"Biddy_InitMNG: %s is not supported, yet!\n",BIDDYTYPENAMETZFDDC);
527  exit(1);
528  } else {
529  fprintf(stderr,"Biddy_InitMNG: Unsupported BDD type!\n");
530  exit(1);
531  }
532 
533  biddyManagerType = bddtype;
534 
535  /* THESE ARE DEFAULT SIZES */
536  biddyVariableTable.size = BIDDYVARMAX;
537  biddyNodeTable.initblocksize = MEDIUM_SIZE; /* 12.0 MB on 64-bit */
538  biddyNodeTable.limitblocksize = XLARGE_SIZE; /* 96.0 MB on 64-bit */
539  biddyNodeTable.initsize = SMALL_SIZE;
540  biddyNodeTable.limitsize = HUGE_SIZE;
541  biddyOPCache.size = MEDIUM_SIZE;
542  biddyEACache.size = SMALL_SIZE;
543  biddyRCCache.size = SMALL_SIZE;
544  biddyReplaceCache.size = SMALL_SIZE;
545 
546  /* USED FOR LARGER PROBLEMS, E.G. DICTIONARY EXAMPLE */
547  /*
548  biddyOPCache.size = LARGE_SIZE;
549  */
550 
551  /* TESTING */
552  /*
553  biddyOPCache.size = LARGE_SIZE;
554  biddyEACache.size = MEDIUM_SIZE;
555  biddyRCCache.size = MEDIUM_SIZE;
556  biddyReplaceCache.size = MEDIUM_SIZE;
557  */
558 
559  /* these values are experimentally determined */
560  /* gcr=1.67, gcrF=1.20, gcrX=0.91, rr=0.01, rrF=1.45, rrX=0.98 */ /* used in v1.7.1 */
561  /* gcr=1.32, gcrF=0.99, gcrX=1.10, rr=0.01, rrF=0.89, rrX=0.91 */ /* used in v1.7.2 */
562  biddyNodeTable.gcratio = (float) 1.32; /* do not delete nodes if the effect is to small, gcratio */
563  biddyNodeTable.gcratioF = (float) 0.99; /* do not delete nodes if the effect is to small, gcratio */
564  biddyNodeTable.gcratioX = (float) 1.10; /* do not delete nodes if the effect is to small, gcratio */
565  biddyNodeTable.resizeratio = (float) 0.01; /* resize Node table if there are to many nodes */
566  biddyNodeTable.resizeratioF = (float) 0.89; /* resize Node table if there are to many nodes */
567  biddyNodeTable.resizeratioX = (float) 0.91; /* resize Node table if there are to many nodes */
568 
569  /* these values are experimentally determined */
570  biddyNodeTable.siftingtreshold = (float) 0.95; /* stop sifting if the size of the system grows to much */
571  biddyNodeTable.convergesiftingtreshold = (float) 1.01; /* stop one step of converging sifting if the size of the system grows to much */
572 
573  /* CREATE AND INITIALIZE NODE TABLE */
574  /* THE ACTUAL SIZE OF NODE TABLE IS biddyNodeTable.size+2 */
575  /* BECAUSE OF USED TRICKS, HASH FUNCTION MUST NEVER RETURN ZERO! */
576  /* USEFUL INDICES ARE FROM [1] TO [biddyNodeTable.size+1] */
577  biddyNodeTable.size = biddyNodeTable.initsize;
578  if (!(biddyNodeTable.table = (BiddyNode **)
579  calloc((biddyNodeTable.size+2),sizeof(BiddyNode *)))) {
580  fprintf(stderr,"Biddy_InitMNG (node table): Out of memoy!\n");
581  exit(1);
582  }
583  /* for (i=0;i<=biddyNodeTable.size+1;i++) biddyNodeTable.table[i] = NULL; */
584 
585  /* CREATE AND INITIALIZE VARIABLE TABLE */
586  /* VARIABLE "1" HAS INDEX [0] */
587  /* VARIABLES ARE ORDERED BY INDEX IN THE VARIABLE TABLE */
588  /* IN THE BDD, SMALLER (PREV) VARIABLES ARE ABOVE THE GREATER (NEXT) ONES */
589  /* VARIABLE "1" MUST ALWAYS HAVE MAX GLOBAL ORDER (IT IS BOTTOMMOST) */
590  /* THIS PART OF CODE DETERMINES DEFAULT ORDERING FOR NEW VARIABLES: */
591  /* ORDER FOR OBDDs AND OFDDs: [1] < [2] < ... < [size-1] < [0] */
592  /* ORDER FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: [size-1] < [size-2] < ... < [1] < [0] */
593  /* FOR OBDDs AND OFDDs: the topmost variable always has prev=biddyVariableTable.size */
594  /* FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: the topmost variable always has prev=biddyVariableTable.num */
595  biddyVariableTable.table = (BiddyVariable *)
596  malloc(biddyVariableTable.size * sizeof(BiddyVariable));
597  nullOrdering(biddyOrderingTable);
598  biddyVariableTable.table[0].name = strdup("1");
599  biddyVariableTable.table[0].num = 1;
600  biddyVariableTable.table[0].firstNode = NULL;
601  biddyVariableTable.table[0].lastNode = NULL;
602  biddyVariableTable.table[0].variable = biddyNull;
603  biddyVariableTable.table[0].element = biddyNull;
604  biddyVariableTable.table[0].selected = FALSE;
605  biddyVariableTable.table[0].data = NULL;
606  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
607  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
608  {
609  biddyVariableTable.table[0].prev = biddyVariableTable.size;
610  biddyVariableTable.table[0].next = 0; /* fixed */
611  }
612  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
613  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
614  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
615  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
616  {
617  biddyVariableTable.table[0].prev = 1;
618  biddyVariableTable.table[0].next = 0; /* fixed */
619  }
620  for (i=1; i<biddyVariableTable.size; i++) {
621  biddyVariableTable.table[i].name = NULL;
622  biddyVariableTable.table[i].num = 0;
623  biddyVariableTable.table[i].firstNode = NULL;
624  biddyVariableTable.table[i].lastNode = NULL;
625  biddyVariableTable.table[i].variable = biddyNull;
626  biddyVariableTable.table[i].element = biddyNull;
627  biddyVariableTable.table[i].selected = FALSE;
628  biddyVariableTable.table[i].data = NULL;
629  SET_ORDER(biddyOrderingTable,i,0);
630  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
631  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
632  {
633  biddyVariableTable.table[i].prev = i-1;
634  biddyVariableTable.table[i].next = i+1;
635  for (j=i+1; j<biddyVariableTable.size; j++) {
636  SET_ORDER(biddyOrderingTable,i,j);
637  }
638  }
639  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
640  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
641  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
642  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
643  {
644  biddyVariableTable.table[i].prev = i+1;
645  biddyVariableTable.table[i].next = i-1;
646  for (j=1; j<i; j++) {
647  SET_ORDER(biddyOrderingTable,i,j);
648  }
649  }
650  }
651  biddyVariableTable.num = 1; /* ONLY VARIABLE '1' IS CREATED */
652  biddyVariableTable.numnum = 1; /* VARIABLE '1' IS A NUMBERED VARIABLE */
653 
654  /* LOOKUP TABLE FOR FASTER SEARCHING OF VARIABLES */
655  /* CURRENTLY, THIS IS NOT USED */
656  /*
657  biddyVariableTable.lookup = (BiddyLookupVariable *)
658  malloc(biddyVariableTable.size * sizeof(BiddyLookupVariable));
659  biddyVariableTable.lookup[0].name = strdup("1");
660  biddyVariableTable.lookup[0].v = 0;
661  */
662 
663  /* DEBUGGING */
664  /*
665  writeORDER(MNG);
666  */
667 
668  /* DEBUGGING */
669  /*
670  warshall(biddyOrderingTable,Biddy_Managed_VariableTableNum(MNG));
671  writeORDER(MNG);
672  */
673 
674  /* INITIALIZATION OF MEMORY MANAGEMENT */
675  /* ALLOCATE FIRST CHUNK OF NODES */
676  biddyNodeTable.blocksize = biddyNodeTable.initblocksize;
677  if (!(biddyFreeNodes = (BiddyNode *)
678  malloc((biddyNodeTable.blocksize) * sizeof(BiddyNode)))) {
679  fprintf(stderr,"Biddy_InitMNG (nodes): Out of memoy!\n");
680  exit(1);
681  }
682  if (!(biddyNodeTable.blocktable = (BiddyNode **)malloc(sizeof(BiddyNode *)))) {
683  fprintf(stderr, "Biddy_InitMNG (blocktable): Out of memoy!\n");
684  exit(1);
685  }
686  biddyNodeTable.blocktable[0] = biddyFreeNodes;
687  biddyNodeTable.table[0] = biddyFreeNodes;
688  biddyFreeNodes = &biddyFreeNodes[1];
689  for (i=0; i<biddyNodeTable.blocksize-2; i++) {
690  biddyFreeNodes[i].list = (void *) &biddyFreeNodes[i+1];
691  }
692  biddyFreeNodes[biddyNodeTable.blocksize-2].list = NULL;
693  biddyNodeTable.generated = biddyNodeTable.blocksize;
694  biddyNodeTable.blocknumber = 1;
695 
696  /* MAKE TERMINAL NODE "1" */
697  /* TERMINAL NODE IS "1" FOR ALL BDD TYPES AND IT IS AT INDEX [0] */
698  biddyNodeTable.table[0]->prev = NULL;
699  biddyNodeTable.table[0]->next = NULL;
700  biddyNodeTable.table[0]->list = NULL;
701  biddyNodeTable.table[0]->f = biddyNull;
702  biddyNodeTable.table[0]->t = biddyNull;
703  biddyNodeTable.table[0]->v = 0; /* terminal node is the only one with v = 0 */
704  biddyNodeTable.table[0]->expiry = 0; /* terminal node is fortified */
705  biddyNodeTable.table[0]->select = 0; /* initialy it is not selected */
706 
707  /* MAKE TERMINAL EDGE AND EDGES REPRESENTING CONSTANTS */
708  /* FOR THE EMPTY DOMAIN, biddyZero AND biddyOne ARE THE SAME FOR ALL BDD TYPES */
709  /* biddyZero IS COMPLEMENTED FOR ALL BDD TYPES, INCLUDING OBDD, ZBDD, AND TZBDD */
710  MNG[2] = (void *) biddyNodeTable.table[0]; /* biddyTerminal */
711  MNG[3] = Biddy_Complement(biddyTerminal); /* biddyZero */
712  MNG[4] = biddyTerminal; /* biddyOne */
713 
714  /* DEBUGGING */
715  /*
716  printf("DEBUG (Biddy_InitMNG): biddyOne = %p\n",biddyOne);
717  printf("DEBUG (Biddy_InitMNG): biddyZero = %p\n",biddyZero);
718  */
719 
720  /* INITIALIZATION OF VARIABLE'S VALUES */
721  biddyVariableTable.table[0].value = biddyZero;
722  for (i=1; i<biddyVariableTable.size; i++) {
723 #pragma warning(suppress: 6386)
724  biddyVariableTable.table[i].value = biddyZero;
725  }
726 
727  /* INITIALIZATION OF NODE SELECTION */
728  biddySelect = 1;
729 
730  /* INITIALIZATION OF GARBAGE COLLECTION */
731  /* MINIMAL VALUE FOR biddySystemAge IS 2 (SEE IMPLEMENTATION OF SIFTING) */
732  biddySystemAge = 2;
733 
734  /* INITIALIZE FORMULA TABLE */
735  /* first formula is 0, it is always a single terminal node */
736  /* second formula is 1, it could be a large graph, e.g. for ZBDD */
737  biddyFormulaTable.deletedName = strdup("BIDDY_DELETED_FORMULA");
738  biddyFormulaTable.size = 2;
739  biddyFormulaTable.numOrdered = 2;
740  if (!(biddyFormulaTable.table = (BiddyFormula *)
741  malloc(biddyFormulaTable.size*sizeof(BiddyFormula))))
742  {
743  fprintf(stderr,"Biddy_InitMNG (formula table): Out of memoy!\n");
744  exit(1);
745  }
746  biddyFormulaTable.table[0].name = strdup("0");
747  biddyFormulaTable.table[0].f = biddyZero;
748  biddyFormulaTable.table[0].expiry = 0;
749  biddyFormulaTable.table[0].deleted = FALSE;
750  biddyFormulaTable.table[1].name = strdup("1");
751  biddyFormulaTable.table[1].f = biddyOne;
752  biddyFormulaTable.table[1].expiry = biddySystemAge;
753  biddyFormulaTable.table[1].deleted = FALSE;
754 
755  /* INITIALIZATION OF NODE TABLE */
756  biddyNodeTable.max = 1;
757  biddyNodeTable.num = 1;
758  biddyNodeTable.garbage = 0;
759  biddyNodeTable.swap = 0;
760  biddyNodeTable.sifting = 0;
761  biddyNodeTable.nodetableresize = 0;
762  biddyNodeTable.funite = 0;
763  biddyNodeTable.funandor = 0;
764  biddyNodeTable.funxor = 0;
765  biddyNodeTable.gctime = 0;
766  biddyNodeTable.drtime = 0;
767 #ifdef BIDDYEXTENDEDSTATS_YES
768  biddyNodeTable.foa = 0;
769  biddyNodeTable.find = 0;
770  biddyNodeTable.compare = 0;
771  biddyNodeTable.add = 0;
772  biddyNodeTable.iterecursive = 0;
773  biddyNodeTable.andorrecursive = 0;
774  biddyNodeTable.xorrecursive = 0;
775  biddyNodeTable.gcobsolete = NULL;
776 #endif
777 
778  /* INITIALIZATION OF CACHE LIST */
779  biddyCacheList = NULL;
780 
781  /* INITIALIZATION OF DEFAULT OPERATION CACHE - USED FOR ITE AND OTHER BOOLEAN OPERATIONS */
782  biddyOPCache.disabled = FALSE;
783  *(biddyOPCache.notusedyet) = TRUE;
784  *(biddyOPCache.search) = *(biddyOPCache.find) = 0;
785 #ifdef BIDDYEXTENDEDSTATS_YES
786  *(biddyOPCache.insert) = *(biddyOPCache.overwrite) = 0;
787 #endif
788  if (!(biddyOPCache.table = (BiddyOp3Cache *)
789  calloc((biddyOPCache.size+1),sizeof(BiddyOp3Cache)))) {
790  fprintf(stderr,"Biddy_InitMNG (OP cache): Out of memoy!\n");
791  exit(1);
792  }
793  /* for (i=0;i<=biddyOPCache.size;i++) biddyOPCache.table[i].result = biddyNull; */
794  Biddy_Managed_AddCache(MNG,BiddyOPGarbage);
795 
796  /* INITIALIZATION OF DEFAULT EA CACHE - USED FOR QUANTIFICATIONS */
797  biddyEACache.disabled = FALSE;
798  *(biddyEACache.notusedyet) = TRUE;
799  *(biddyEACache.search) = *(biddyEACache.find) = 0;
800 #ifdef BIDDYEXTENDEDSTATS_YES
801  *(biddyEACache.insert) = *(biddyEACache.overwrite) = 0;
802 #endif
803  if (!(biddyEACache.table = (BiddyOp3Cache *)
804  calloc((biddyEACache.size+1),sizeof(BiddyOp3Cache)))) {
805  fprintf(stderr,"Biddy_InitMNG (EA cache): Out of memoy!\n");
806  exit(1);
807  }
808  /* for (i=0;i<=biddyEACache.size;i++) biddyEACache.table[i].result = biddyNull; */
809  Biddy_Managed_AddCache(MNG,BiddyEAGarbage);
810 
811  /* INITIALIZATION OF DEFAULT RC CACHE - USED FOR RESTRICT AND COMPOSE */
812  biddyRCCache.disabled = FALSE;
813  *(biddyRCCache.notusedyet) = TRUE;
814  *(biddyRCCache.search) = *(biddyRCCache.find) = 0;
815 #ifdef BIDDYEXTENDEDSTATS_YES
816  *(biddyRCCache.insert) = *(biddyRCCache.overwrite) = 0;
817 #endif
818  if (!(biddyRCCache.table = (BiddyOp3Cache *)
819  calloc((biddyRCCache.size+1),sizeof(BiddyOp3Cache)))) {
820  fprintf(stderr,"Biddy_InitMNG (RC cache): Out of memoy!\n");
821  exit(1);
822  }
823  /* for (i=0;i<=biddyRCCache.size;i++) biddyRCCache.table[i].result = biddyNull; */
824  Biddy_Managed_AddCache(MNG,BiddyRCGarbage);
825 
826  /* INITIALIZATION OF DEFAULT REPLACE CACHE - USED FOR REPLACE */
827  biddyReplaceCache.keywordList = NULL;
828  biddyReplaceCache.keyList = NULL;
829  biddyReplaceCache.keyNum = 0;
830  biddyReplaceCache.keywordNum = 0;
831  biddyReplaceCache.disabled = FALSE;
832  *(biddyReplaceCache.notusedyet) = TRUE;
833  *(biddyReplaceCache.search) = *(biddyReplaceCache.find) = 0;
834 #ifdef BIDDYEXTENDEDSTATS_YES
835  *(biddyReplaceCache.insert) = *(biddyReplaceCache.overwrite) = 0;
836 #endif
837  if (!(biddyReplaceCache.table = (BiddyKeywordCache *)
838  calloc((biddyReplaceCache.size+1),sizeof(BiddyKeywordCache)))) {
839  fprintf(stderr,"Biddy_InitMNG (Replace cache): Out of memoy!\n");
840  exit(1);
841  }
842  /* for (i=0;i<=biddyReplaceCache.size;i++) biddyReplaceCache.table[i].result = biddyNull; */
843  Biddy_Managed_AddCache(MNG,BiddyReplaceGarbage);
844 
845  /* DEBUGGING */
846  /*
847  BiddySystemReport(MNG);
848  */
849 
850  /* DEBUGGING WITH GDB AND DDD */
851  /* USE "up" TO CHANGE CONTEXT */
852  /* use "print sizeof(BiddyNode)" */
853  /* use "print sizeof(((BiddyNode *) biddyOne).f)" */
854  /* use "graph display *((BiddyNode *) biddyOne)" */
855  /* use "print ((BiddyNode *) biddyOne)" */
856  /* use "print ((BiddyNode *) (((uintptr_t) f) & (~((uintptr_t) 1))))->v */
857  /* use "print ((BiddyNode *) ((BiddyNode *) (((uintptr_t) f) & (~((uintptr_t) 1))))->f)->v" */
858  /* use "print ((BiddyNode *) ((BiddyNode *) (((uintptr_t) f) & (~((uintptr_t) 1))))->t)->v" */
859  /* use "print biddyVariableTable.table[0].name" */
860 
861 }
862 
863 #ifdef __cplusplus
864 }
865 #endif
866 
867 /***************************************************************************/
878 #ifdef __cplusplus
879 extern "C" {
880 #endif
881 
882 void
884 {
885  unsigned int i;
886  BiddyCacheList *sup1, *sup2;
887  Biddy_Manager MNG;
888 
889  if (!mng) {
890  MNG = biddyAnonymousManager;
891  } else {
892  MNG = *mng;
893  }
894 
895  /* REPORT ABOUT THE SYSTEM */
896  /* CHECKING THE CORRECTNESS AND THE EFFICIENCY OF MEMORY MANAGEMENT */
897 
898  /*
899 #ifdef BIDDYEXTENDEDSTATS_YES
900  BiddySystemReport(MNG);
901  printf("Number of ITE calls: %u (internal direct and recursive calls: %llu)\n",biddyNodeTable.funite,biddyNodeTable.iterecursive);
902  printf("Number of AND and OR calls: %u (internal direct and recursive calls: %llu)\n",biddyNodeTable.funandor,biddyNodeTable.andorrecursive);
903  printf("Number of XOR calls: %u (internal direct and recursive calls: %llu)\n",biddyNodeTable.funxor,biddyNodeTable.xorrecursive);
904 #ifdef MINGW
905  printf("Memory in use: %I64u bytes\n",Biddy_Managed_ReadMemoryInUse(MNG));
906 #else
907  printf("Memory in use: %llu bytes\n",Biddy_Managed_ReadMemoryInUse(MNG));
908 #endif
909  printf("Garbage collections so far: %u (node table resizing so far: %u)\n",biddyNodeTable.garbage,biddyNodeTable.nodetableresize);
910  printf("Total time for garbage collections so far: %.3fs\n",biddyNodeTable.gctime / (1.0 * CLOCKS_PER_SEC));
911  printf("Used buckets in node table: %u (%.2f%%)\n",
912  Biddy_Managed_ListUsed(MNG),
913  (100.0*Biddy_Managed_ListUsed(MNG)/(biddyNodeTable.size+1)));
914  printf("Peak number of live BDD nodes: %u\n",biddyNodeTable.max);
915  printf("Number of live BDD nodes: %u\n",biddyNodeTable.num);
916  printf("Number of compared nodes: %llu (%.2f per findNodeTable call)\n",
917  biddyNodeTable.compare,
918  biddyNodeTable.find ?
919  (1.0*biddyNodeTable.compare/biddyNodeTable.find):0);
920 #endif
921  */
922 
923  /*
924  printf("Delete name and type...\n");
925  */
926  free(biddyManagerName); /* MNG[0] is not derefenced by macro */
927 
928  /*
929  printf("Delete BDD type ...\n");
930  */
931  free((short int*)(MNG[1]));
932 
933  MNG[2] = NULL; /* biddyTerminal */
934  MNG[3] = NULL; /* biddyZero */
935  MNG[4] = NULL; /* biddyOne */
936 
937  /*
938  printf("Delete nodes, block table, and node table...\n");
939  */
940  if ((BiddyNodeTable*)(MNG[5])) {
941  for (i = 0; i < biddyNodeTable.blocknumber; i++) {
942  free(biddyNodeTable.blocktable[i]);
943  }
944  free(biddyNodeTable.blocktable);
945  free(biddyNodeTable.table);
946 #ifdef BIDDYEXTENDEDSTATS_YES
947  free(biddyNodeTable.gcobsolete);
948 #endif
949 #pragma warning(suppress: 6001)
950  free((BiddyNodeTable*)(MNG[5]));
951  }
952 
953  /* TO DO: REMOVE VARIABLE NAMES! */
954  /*
955  printf("Delete variable table...\n");
956  */
957  if ((BiddyVariableTable*)(MNG[6])) {
958  free(biddyVariableTable.table);
959  free(biddyVariableTable.lookup);
960 #pragma warning(suppress: 6001)
961  free((BiddyVariableTable*)(MNG[6]));
962  }
963 
964  /* TO DO: REMOVE FORMULAE NAMES! */
965  /*
966  printf("Delete formula table...\n");
967  */
968  if ((BiddyFormulaTable*)(MNG[7])) {
969  free(biddyFormulaTable.table);
970  free(biddyFormulaTable.deletedName);
971 #pragma warning(suppress: 6001)
972  free((BiddyFormulaTable*)(MNG[7]));
973  }
974 
975  /*
976  printf("Delete OP cache...\n");
977  */
978  if ((BiddyOp3CacheTable*)(MNG[8])) {
979  free(biddyOPCache.table);
980  free(biddyOPCache.notusedyet);
981  free(biddyOPCache.search);
982  free(biddyOPCache.find);
983 #ifdef BIDDYEXTENDEDSTATS_YES
984  free(biddyOPCache.insert);
985  free(biddyOPCache.overwrite);
986 #endif
987 #pragma warning(suppress: 6001)
988  free((BiddyOp3CacheTable*)(MNG[8]));
989  }
990 
991  /*
992  printf("Delete EA cache...\n");
993  */
994  if ((BiddyOp3CacheTable*)(MNG[9])) {
995  free(biddyEACache.table);
996  free(biddyEACache.notusedyet);
997  free(biddyEACache.search);
998  free(biddyEACache.find);
999 #ifdef BIDDYEXTENDEDSTATS_YES
1000  free(biddyEACache.insert);
1001  free(biddyEACache.overwrite);
1002 #endif
1003 #pragma warning(suppress: 6001)
1004  free((BiddyOp3CacheTable*)(MNG[9]));
1005  }
1006 
1007  /*
1008  printf("Delete RC cache...\n");
1009  */
1010  if ((BiddyOp3CacheTable*)(MNG[10])) {
1011  free(biddyRCCache.table);
1012  free(biddyRCCache.notusedyet);
1013  free(biddyRCCache.search);
1014  free(biddyRCCache.find);
1015 #ifdef BIDDYEXTENDEDSTATS_YES
1016  free(biddyRCCache.insert);
1017  free(biddyRCCache.overwrite);
1018 #endif
1019 #pragma warning(suppress: 6001)
1020  free((BiddyOp3CacheTable*)(MNG[10]));
1021  }
1022 
1023  /*
1024  printf("Delete Replace cache...\n");
1025  */
1026  if ((BiddyKeywordCacheTable*)(MNG[11])) {
1027  for (i = 0; i < biddyReplaceCache.keywordNum; i++) {
1028  free(biddyReplaceCache.keywordList[i]);
1029  }
1030  free(biddyReplaceCache.keywordList);
1031  free(biddyReplaceCache.keyList);
1032  free(biddyReplaceCache.table);
1033  free(biddyReplaceCache.notusedyet);
1034  free(biddyReplaceCache.search);
1035  free(biddyReplaceCache.find);
1036 #ifdef BIDDYEXTENDEDSTATS_YES
1037  free(biddyReplaceCache.insert);
1038  free(biddyReplaceCache.overwrite);
1039 #endif
1040 #pragma warning(suppress: 6001)
1041  free((BiddyKeywordCacheTable*)(MNG[11]));
1042  }
1043 
1044  /*
1045  printf("Delete cache list...\n");
1046  */
1047  if ((BiddyCacheList**)(MNG[12])) {
1048 #pragma warning(suppress: 6001)
1049  sup1 = biddyCacheList;
1050  while (sup1) {
1051  sup2 = sup1->next;
1052  free(sup1);
1053  sup1 = sup2;
1054  }
1055 #pragma warning(suppress: 6001)
1056  free((BiddyCacheList**)(MNG[12]));
1057  }
1058 
1059  /*
1060  printf("Delete pointer biddyFreeNodes...\n");
1061  */
1062 #pragma warning(suppress: 6001)
1063  free((BiddyNode**)(MNG[13]));
1064 
1065  /*
1066  printf("Delete Ordering table...\n");
1067  */
1068 #pragma warning(suppress: 6001)
1069  free((BiddyOrderingTable*)(MNG[14]));
1070 
1071  /*
1072  printf("Delete age...\n");
1073  */
1074  free((unsigned int*)(MNG[15]));
1075 
1076  /*
1077  printf("Delete selector...\n");
1078  */
1079  free((unsigned short int*)(MNG[16]));
1080 
1081  /*
1082  printf("And finally, delete manager...\n");
1083  */
1084  free((BiddyManager*)MNG);
1085 
1086  /* USER SHOULD DELETE HIS OWN CACHES */
1087 }
1088 
1089 #ifdef __cplusplus
1090 }
1091 #endif
1092 
1093 /***************************************************************************/
1101 #ifdef __cplusplus
1102 extern "C" {
1103 #endif
1104 
1107  return strdup(BIDDYVERSION);
1108 }
1109 
1110 #ifdef __cplusplus
1111 }
1112 #endif
1113 
1114 /***************************************************************************/
1124 #ifdef __cplusplus
1125 extern "C" {
1126 #endif
1127 
1128 int
1130 {
1131  if (!MNG) MNG = biddyAnonymousManager;
1132 
1133  return biddyManagerType;
1134 }
1135 
1136 #ifdef __cplusplus
1137 }
1138 #endif
1139 
1140 /***************************************************************************/
1150 #ifdef __cplusplus
1151 extern "C" {
1152 #endif
1153 
1156 {
1157  if (!MNG) MNG = biddyAnonymousManager;
1158 
1159  return biddyManagerName;
1160 }
1161 
1162 #ifdef __cplusplus
1163 }
1164 #endif
1165 
1166 /***************************************************************************/
1193 #ifdef __cplusplus
1194 extern "C" {
1195 #endif
1196 
1197 void
1199  float gcrX, float rr, float rrF, float rrX, float st, float cst)
1200 {
1201  if (!MNG) MNG = biddyAnonymousManager;
1202 
1203  if (gcr > 0.0) biddyNodeTable.gcratio = gcr;
1204  if (gcrF > 0.0) biddyNodeTable.gcratioF = gcrF;
1205  if (gcrX > 0.0) biddyNodeTable.gcratioX = gcrX;
1206  if (rr > 0.0) biddyNodeTable.resizeratio = rr;
1207  if (rrF > 0.0) biddyNodeTable.resizeratioF = rrF;
1208  if (rrX > 0.0) biddyNodeTable.resizeratioX = rrX;
1209  if (st > 0.0) biddyNodeTable.siftingtreshold = st;
1210  if (cst > 0.0) biddyNodeTable.convergesiftingtreshold = cst;
1211 
1212  /* PROFILING */
1213  /*
1214  fprintf(stderr,"gcr=%.2f, ",biddyNodeTable.gcratio);
1215  fprintf(stderr,"gcrF=%.2f, ",biddyNodeTable.gcratioF);
1216  fprintf(stderr,"gcrX=%.2f, ",biddyNodeTable.gcratioX);
1217  fprintf(stderr,"rr=%.2f, ",biddyNodeTable.resizeratio);
1218  fprintf(stderr,"rrF=%.2f, ",biddyNodeTable.resizeratioF);
1219  fprintf(stderr,"rrX=%.2f, ",biddyNodeTable.resizeratioX);
1220  */
1221 }
1222 
1223 #ifdef __cplusplus
1224 }
1225 #endif
1226 
1227 /***************************************************************************/
1238 #ifdef __cplusplus
1239 extern "C" {
1240 #endif
1241 
1242 Biddy_Edge
1244 {
1245  Biddy_Edge r;
1246 
1247  if (Biddy_IsTerminal(fun)) return fun;
1248 
1249  r = BiddyT(fun);
1250 
1251  /* EXTERNAL FUNCTIONS MUST RETURN NON-OBSOLETE NODE */
1252  if ((BiddyN(r)->expiry) &&
1253  ((BiddyN(r)->expiry<BiddyN(fun)->expiry) || !(BiddyN(fun)->expiry))
1254  )
1255  {
1256  BiddyN(r)->expiry = BiddyN(fun)->expiry;
1257  }
1258 
1259  return r;
1260 }
1261 
1262 #ifdef __cplusplus
1263 }
1264 #endif
1265 
1266 /***************************************************************************/
1277 #ifdef __cplusplus
1278 extern "C" {
1279 #endif
1280 
1281 Biddy_Edge
1283 {
1284  Biddy_Edge r;
1285 
1286  if (Biddy_IsTerminal(fun)) return fun;
1287 
1288  r = BiddyE(fun);
1289 
1290  /* EXTERNAL FUNCTIONS MUST RETURN NON-OBSOLETE NODE */
1291  if ((BiddyN(r)->expiry) &&
1292  ((BiddyN(r)->expiry<BiddyN(fun)->expiry) || !(BiddyN(fun)->expiry))
1293  )
1294  {
1295  BiddyN(r)->expiry = BiddyN(fun)->expiry;
1296  }
1297 
1298  return r;
1299 }
1300 
1301 #ifdef __cplusplus
1302 }
1303 #endif
1304 
1305 /***************************************************************************/
1315 #ifdef __cplusplus
1316 extern "C" {
1317 #endif
1318 
1321 {
1322  return BiddyV(fun);
1323 }
1324 
1325 #ifdef __cplusplus
1326 }
1327 #endif
1328 
1329 /***************************************************************************/
1339 #ifdef __cplusplus
1340 extern "C" {
1341 #endif
1342 
1345  Biddy_Edge f2)
1346 {
1347  Biddy_Boolean r;
1348  if (!MNG1) MNG1 = biddyAnonymousManager;
1349 
1350  assert( biddyManagerType1 == biddyManagerType2 );
1351 
1352  if (MNG1 == MNG2) return (f1 == f2);
1353 
1354  r = isEqv(MNG1,f1,MNG2,f2);
1356 
1357  return r;
1358 }
1359 
1360 #ifdef __cplusplus
1361 }
1362 #endif
1363 
1364 /***************************************************************************/
1374 #ifdef __cplusplus
1375 extern "C" {
1376 #endif
1377 
1378 void
1380 {
1381  if (!MNG) MNG = biddyAnonymousManager;
1382 
1383  ((BiddyNode *) BiddyP(f))->select = biddySelect;
1384 }
1385 
1386 #ifdef __cplusplus
1387 }
1388 #endif
1389 
1390 /***************************************************************************/
1400 #ifdef __cplusplus
1401 extern "C" {
1402 #endif
1403 
1404 void
1406 {
1407  if (!MNG) MNG = biddyAnonymousManager;
1408 
1409  ((BiddyNode *) BiddyP(f))->select = 0;
1410 }
1411 
1412 #ifdef __cplusplus
1413 }
1414 #endif
1415 
1416 /***************************************************************************/
1426 #ifdef __cplusplus
1427 extern "C" {
1428 #endif
1429 
1432 {
1433  if (!MNG) MNG = biddyAnonymousManager;
1434 
1435  return (((BiddyNode *) BiddyP(f))->select == biddySelect);
1436 }
1437 
1438 #ifdef __cplusplus
1439 }
1440 #endif
1441 
1442 /***************************************************************************/
1453 #ifdef __cplusplus
1454 extern "C" {
1455 #endif
1456 
1457 void
1459 {
1460  if (!MNG) MNG = biddyAnonymousManager;
1461 
1462  /* VARIANT 1 - ITERATIVE */
1463  /*
1464  BiddyNode **stack;
1465  BiddyNode **SP;
1466  BiddyNode *p;
1467  if ((p=(BiddyNode *) BiddyP(f))->select != biddySelect) {
1468  SP = stack = (BiddyNode **)
1469  malloc(biddyNodeTable.num * sizeof(BiddyNode *));
1470  *(SP++) = p;
1471  while (SP != stack) {
1472  p = (*(--SP));
1473  p->select = biddySelect;
1474  if (((BiddyNode *) BiddyP(p->f))->select != biddySelect) {
1475  *(SP++) = (BiddyNode *) BiddyP(p->f);
1476  }
1477  if (((BiddyNode *) p->t)->select != biddySelect) {
1478  *(SP++) = (BiddyNode *) p->t;
1479  }
1480  }
1481  free(stack);
1482  }
1483  */
1484 
1485  /* VARIANT 2 - RECURSIVE */
1486 
1487  if (((BiddyNode *)BiddyP(f))->select != biddySelect) {
1488  ((BiddyNode *)BiddyP(f))->select = biddySelect;
1489  Biddy_Managed_SelectFunction(MNG, BiddyE(f));
1490  Biddy_Managed_SelectFunction(MNG, BiddyT(f));
1491  }
1492 
1493 
1494 }
1495 
1496 #ifdef __cplusplus
1497 }
1498 #endif
1499 
1500 /***************************************************************************/
1510 #ifdef __cplusplus
1511 extern "C" {
1512 #endif
1513 
1514 void
1516 {
1517  if (!MNG) MNG = biddyAnonymousManager;
1518 
1519  if (++biddySelect == 0) {
1520  /* biddySelect is back to start - explicite deselection is required */
1521  Biddy_Variable v;
1522  BiddyNode *sup;
1523  biddyNodeTable.table[0]->select = 0;
1524  for (v=1; v<biddyVariableTable.num; v++) {
1525  biddyVariableTable.table[v].lastNode->list = NULL;
1526  sup = biddyVariableTable.table[v].firstNode;
1527  assert( sup != NULL );
1528  while (sup) {
1529  assert(sup->v == v) ;
1530  sup->select = 0;
1531  sup = (BiddyNode *) sup->list;
1532  }
1533  }
1534  biddySelect = 1;
1535  }
1536 }
1537 
1538 #ifdef __cplusplus
1539 }
1540 #endif
1541 
1542 /***************************************************************************/
1554 #ifdef __cplusplus
1555 extern "C" {
1556 #endif
1557 
1558 Biddy_Edge
1560 {
1561  if (!MNG) MNG = biddyAnonymousManager;
1562 
1563  return biddyTerminal;
1564 }
1565 
1566 #ifdef __cplusplus
1567 }
1568 #endif
1569 
1570 /***************************************************************************/
1584 #ifdef __cplusplus
1585 extern "C" {
1586 #endif
1587 
1588 Biddy_Edge
1590 {
1591  if (!MNG) MNG = biddyAnonymousManager;
1592 
1593  return biddyZero;
1594 }
1595 
1596 #ifdef __cplusplus
1597 }
1598 #endif
1599 
1600 /***************************************************************************/
1616 #ifdef __cplusplus
1617 extern "C" {
1618 #endif
1619 
1620 Biddy_Edge
1622 {
1623  if (!MNG) MNG = biddyAnonymousManager;
1624 
1625  return biddyOne;
1626 }
1627 
1628 #ifdef __cplusplus
1629 }
1630 #endif
1631 
1632 /***************************************************************************/
1642 #ifdef __cplusplus
1643 extern "C" {
1644 #endif
1645 
1646 Biddy_Edge
1648 {
1649  Biddy_Edge r;
1650  Biddy_Variable v,top;
1651 
1652  if (!MNG) MNG = biddyAnonymousManager;
1653 
1654  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1655  /* IMPLEMENTED */
1656  r = biddyOne;
1657  for (v=1;v<biddyVariableTable.num;v++) {
1658  r = BiddyManagedITE(MNG,biddyVariableTable.table[v].variable,biddyZero,r);
1659  }
1660  BiddyRefresh(r); /* not always refreshed by ITE */
1661 
1662  } else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
1663  /* IMPLEMENTED */
1664 
1665  r = biddyTerminal;
1666 
1667  } else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
1668  /* IMPLEMENTED */
1669 
1670  /* find topmost variable */
1671  top = 0;
1672  for (v = 1; v < biddyVariableTable.num; v++) {
1673  top = biddyVariableTable.table[top].prev;
1674  }
1675  r = biddyTerminal;
1676  Biddy_SetTag(r,top);
1677 
1678  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
1679  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
1680  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
1681  {
1682  fprintf(stderr,"Biddy_GetBaseSet: this BDD type is not supported, yet!\n");
1683  return biddyNull;
1684  } else {
1685  fprintf(stderr,"Biddy_GetBaseSet: Unsupported BDD type!\n");
1686  return biddyNull;
1687  }
1688 
1689  return r;
1690 }
1691 
1692 #ifdef __cplusplus
1693 }
1694 #endif
1695 
1696 /***************************************************************************/
1707 #ifdef __cplusplus
1708 extern "C" {
1709 #endif
1710 
1713 {
1714  Biddy_Variable v;
1715  Biddy_Boolean find;
1716 
1717  if (!MNG) MNG = biddyAnonymousManager;
1718 
1719  /* VARIABLE TABLE IS NEVER EMPTY. AT LEAST, THERE IS ELEMENT '1' AT INDEX [0] */
1720 
1721  /* SEARCH FOR THE VARIABLE IN THE ORIGINAL TABLE */
1722 
1723  v = 0;
1724  find = FALSE;
1725  while (!find && v<biddyVariableTable.num) {
1726  if ((x[0] == biddyVariableTable.table[v].name[0]) &&
1727  (!strcmp(x,biddyVariableTable.table[v].name)))
1728  {
1729  find = TRUE;
1730  } else {
1731  v++;
1732  }
1733  }
1734 
1735 
1736  /* TO DO: SEARCH FOR THE VARIABLE IN THE LOOKUP TABLE INSTEAD IN THE ORIGINAL TABLE */
1737 
1738  /* IF find THEN v IS THE INDEX OF THE CORRECT ELEMENT! */
1739  if (!find) {
1740  v = 0;
1741  }
1742 
1743  return v;
1744 }
1745 
1746 #ifdef __cplusplus
1747 }
1748 #endif
1749 
1750 /***************************************************************************/
1761 #ifdef __cplusplus
1762 extern "C" {
1763 #endif
1764 
1767 {
1768  Biddy_Variable v,k;
1769 
1770  if (!MNG) MNG = biddyAnonymousManager;
1771 
1772  v = 0;
1773  for (k = 1; k < biddyVariableTable.num; k++) {
1774  v = biddyVariableTable.table[v].prev;
1775  }
1776 
1777  return v;
1778 }
1779 
1780 #ifdef __cplusplus
1781 }
1782 #endif
1783 
1784 /***************************************************************************/
1799 #ifdef __cplusplus
1800 extern "C" {
1801 #endif
1802 
1805 {
1806  Biddy_Variable v;
1807 
1808  if (!MNG) MNG = biddyAnonymousManager;
1809 
1810  if ((i == 0) || (i > biddyVariableTable.num)) {
1811  return 0;
1812  } else {
1813  v = 0;
1814  while (i < biddyVariableTable.num) {
1815  v = Biddy_Managed_GetPrevVariable(MNG,v);
1816  i++;
1817  }
1818  }
1819 
1820  return v;
1821 }
1822 
1823 #ifdef __cplusplus
1824 }
1825 #endif
1826 
1827 /***************************************************************************/
1837 #ifdef __cplusplus
1838 extern "C" {
1839 #endif
1840 
1843 {
1844  if (!MNG) MNG = biddyAnonymousManager;
1845 
1846  if (v >= biddyVariableTable.num) {
1847  return 0;
1848  } else {
1849  return biddyVariableTable.table[v].prev;
1850  }
1851 }
1852 
1853 #ifdef __cplusplus
1854 }
1855 #endif
1856 
1857 /***************************************************************************/
1867 #ifdef __cplusplus
1868 extern "C" {
1869 #endif
1870 
1873 {
1874  if (!MNG) MNG = biddyAnonymousManager;
1875 
1876  if (v >= biddyVariableTable.num) {
1877  return 0;
1878  } else {
1879  return biddyVariableTable.table[v].next;
1880  }
1881 }
1882 
1883 #ifdef __cplusplus
1884 }
1885 #endif
1886 
1887 /***************************************************************************/
1896 #ifdef __cplusplus
1897 extern "C" {
1898 #endif
1899 
1900 Biddy_Edge
1902 {
1903  if (!MNG) MNG = biddyAnonymousManager;
1904 
1905  return biddyVariableTable.table[v].variable;
1906 }
1907 
1908 #ifdef __cplusplus
1909 }
1910 #endif
1911 
1912 /***************************************************************************/
1921 #ifdef __cplusplus
1922 extern "C" {
1923 #endif
1924 
1925 Biddy_Edge
1927 {
1928  if (!MNG) MNG = biddyAnonymousManager;
1929 
1930  return biddyVariableTable.table[v].element;
1931 }
1932 
1933 #ifdef __cplusplus
1934 }
1935 #endif
1936 
1937 /***************************************************************************/
1946 #ifdef __cplusplus
1947 extern "C" {
1948 #endif
1949 
1952 {
1953  if (!MNG) MNG = biddyAnonymousManager;
1954 
1955  return biddyVariableTable.table[v].name;
1956 }
1957 
1958 #ifdef __cplusplus
1959 }
1960 #endif
1961 
1962 /***************************************************************************/
1974 #ifdef __cplusplus
1975 extern "C" {
1976 #endif
1977 
1978 Biddy_Edge
1980 {
1981  if (!MNG) MNG = biddyAnonymousManager;
1982 
1983  assert( f != NULL );
1984 
1985  return biddyVariableTable.table[BiddyV(f)].variable;
1986 }
1987 
1988 #ifdef __cplusplus
1989 }
1990 #endif
1991 
1992 /***************************************************************************/
2002 #ifdef __cplusplus
2003 extern "C" {
2004 #endif
2005 
2008 {
2009  if (!MNG) MNG = biddyAnonymousManager;
2010 
2011  assert( f != NULL );
2012 
2013  return biddyVariableTable.table[BiddyV(f)].name;
2014 }
2015 
2016 #ifdef __cplusplus
2017 }
2018 #endif
2019 
2020 /***************************************************************************/
2030 #ifdef __cplusplus
2031 extern "C" {
2032 #endif
2033 
2034 char
2036 {
2037  if (!MNG) MNG = biddyAnonymousManager;
2038 
2039  assert( f != NULL );
2040 
2041  return biddyVariableTable.table[BiddyV(f)].name[0];
2042 }
2043 
2044 #ifdef __cplusplus
2045 }
2046 #endif
2047 
2048 /***************************************************************************/
2059 #ifdef __cplusplus
2060 extern "C" {
2061 #endif
2062 
2063 void
2065 {
2066  Biddy_Variable v;
2067 
2068  if (!MNG) MNG = biddyAnonymousManager;
2069 
2070  for (v=0; v<biddyVariableTable.num; v++) {
2071  biddyVariableTable.table[v].value = biddyZero;
2072  }
2073 }
2074 
2075 #ifdef __cplusplus
2076 }
2077 #endif
2078 
2079 /***************************************************************************/
2089 #ifdef __cplusplus
2090 extern "C" {
2091 #endif
2092 
2093 void
2095 {
2096  if (!MNG) MNG = biddyAnonymousManager;
2097 
2098  biddyVariableTable.table[v].value = f;
2099 }
2100 
2101 #ifdef __cplusplus
2102 }
2103 #endif
2104 
2105 /***************************************************************************/
2115 #ifdef __cplusplus
2116 extern "C" {
2117 #endif
2118 
2119 Biddy_Edge
2121 {
2122  if (!MNG) MNG = biddyAnonymousManager;
2123 
2124  return biddyVariableTable.table[v].value;
2125 }
2126 
2127 #ifdef __cplusplus
2128 }
2129 #endif
2130 
2131 /***************************************************************************/
2142 #ifdef __cplusplus
2143 extern "C" {
2144 #endif
2145 
2146 void
2148 {
2149  Biddy_Variable v;
2150 
2151  if (!MNG) MNG = biddyAnonymousManager;
2152 
2153  for (v=0; v<biddyVariableTable.num; v++) {
2154  if (biddyVariableTable.table[v].data) {
2155  free(biddyVariableTable.table[v].data);
2156  biddyVariableTable.table[v].data = NULL;
2157  }
2158  }
2159 }
2160 
2161 #ifdef __cplusplus
2162 }
2163 #endif
2164 
2165 /***************************************************************************/
2175 #ifdef __cplusplus
2176 extern "C" {
2177 #endif
2178 
2179 void
2181 {
2182  if (!MNG) MNG = biddyAnonymousManager;
2183 
2184  biddyVariableTable.table[v].data = x;
2185 }
2186 
2187 #ifdef __cplusplus
2188 }
2189 #endif
2190 
2191 /***************************************************************************/
2201 #ifdef __cplusplus
2202 extern "C" {
2203 #endif
2204 
2205 void *
2207 {
2208  if (!MNG) MNG = biddyAnonymousManager;
2209 
2210  return biddyVariableTable.table[v].data;
2211 }
2212 
2213 #ifdef __cplusplus
2214 }
2215 #endif
2216 
2217 /***************************************************************************/
2229 #ifdef __cplusplus
2230 extern "C" {
2231 #endif
2232 
2235 {
2236  Biddy_Boolean r;
2237  Biddy_Variable fv,ftop;
2238 
2239  assert( f != NULL );
2240 
2241  if (!MNG) MNG = biddyAnonymousManager;
2242 
2243  if (f == biddyNull) return FALSE;
2244 
2245  ftop = 0;
2246  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2247  /* IMPLEMENTED */
2248  ftop = BiddyV(f);
2249  } else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2250  /* IMPLEMENTED */
2251  /* determine the topmost variable (for ZBDDs, it has prev=biddyVariableTable.num) */
2252  ftop = BiddyV(f);
2253  while (biddyVariableTable.table[ftop].prev != biddyVariableTable.num) {
2254  ftop = biddyVariableTable.table[ftop].prev;
2255  }
2256  } else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
2257  /* IMPLEMENTED */
2258  ftop = Biddy_GetTag(f);
2259  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
2260  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
2261  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
2262  {
2263  fprintf(stderr,"Biddy_Eval: this BDD type is not supported, yet!\n");
2264  return FALSE;
2265  } else {
2266  fprintf(stderr,"Biddy_Eval: Unsupported BDD type!\n");
2267  return FALSE;
2268  }
2269 
2270  r = !(Biddy_GetMark(f));
2271  while (ftop != 0) {
2272 
2273  fv = BiddyV(f);
2274  assert( biddyVariableTable.table[fv].value != NULL );
2275 
2276  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2277 
2278  if (biddyVariableTable.table[fv].value == biddyZero) {
2279  f = BiddyE(f);
2280  /* for OBDDC, 'else' successor can be marked */
2281  if (Biddy_GetMark(f)) r = !r;
2282  } else {
2283  f = BiddyT(f);
2284  /* for OBDD, biddyZero is a marked edge to 'then' successor! */
2285  if (Biddy_GetMark(f)) r = !r;
2286  }
2287  ftop = BiddyV(f);
2288 
2289  } else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2290 
2291  while (ftop != fv) {
2292  assert( biddyVariableTable.table[ftop].value != NULL );
2293  if (biddyVariableTable.table[ftop].value == biddyZero) {
2294  ftop = Biddy_Managed_GetNextVariable(MNG,ftop);
2295  } else {
2296  r = FALSE;
2297  ftop = fv = 0;
2298  }
2299  }
2300  if (fv != 0) {
2301  if (biddyVariableTable.table[fv].value == biddyZero) {
2302  f = BiddyE(f);
2303  /* for ZBDDs, 'else' successor is never marked */
2304  } else {
2305  f = BiddyT(f);
2306  /* for ZBDDC, mark is transfered only to the left successor */
2307  r = TRUE;
2308  /* for ZBDDC, 'then' successor can be marked */
2309  if (Biddy_GetMark(f)) r = !r;
2310  }
2311  ftop = Biddy_Managed_GetNextVariable(MNG,fv);
2312  }
2313 
2314  } else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
2315 
2316  while (ftop != fv) {
2317  assert( biddyVariableTable.table[ftop].value != NULL );
2318  if (biddyVariableTable.table[ftop].value == biddyZero) {
2319  ftop = Biddy_Managed_GetNextVariable(MNG,ftop);
2320  } else {
2321  r = FALSE;
2322  ftop = fv = 0;
2323  }
2324  }
2325  if (fv != 0) {
2326  if (biddyVariableTable.table[fv].value == biddyZero) {
2327  f = BiddyE(f);
2328  /* for TZBDD, marks are not transfered but used only to denote 0 */
2329  if (Biddy_GetMark(f)) r = FALSE;
2330  } else {
2331  f = BiddyT(f);
2332  /* for TZBDD, marks are not transfered but used only to denote 0 */
2333  if (Biddy_GetMark(f)) r = FALSE;
2334  }
2335  ftop = Biddy_GetTag(f);
2336  }
2337  }
2338  }
2339 
2340  return r;
2341 }
2342 
2343 #ifdef __cplusplus
2344 }
2345 #endif
2346 
2347 /***************************************************************************/
2361 #ifdef __cplusplus
2362 extern "C" {
2363 #endif
2364 
2365 double
2367 {
2368  double r1,r0;
2369  Biddy_Boolean rf;
2370 
2371  if (!MNG) MNG = biddyAnonymousManager;
2372 
2373  if (biddyManagerType == BIDDYTYPEOBDD) {
2374  /* IMPLEMENTED */
2375  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
2376  /* IMPLEMENTED */
2377  } else if (biddyManagerType == BIDDYTYPEZBDD) {
2378  /* IMPLEMENTED */
2379  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
2380  /* IMPLEMENTED */
2381  } else if (biddyManagerType == BIDDYTYPETZBDD) {
2382  /* IMPLEMENTED */
2383  } else if (biddyManagerType == BIDDYTYPETZBDDC)
2384  {
2385  fprintf(stderr,"Biddy_EvalProbability: this BDD type is not supported, yet!\n");
2386  return 0;
2387  } else if ((biddyManagerType == BIDDYTYPEOFDD) || (biddyManagerType == BIDDYTYPEOFDDC) ||
2388  (biddyManagerType == BIDDYTYPEZFDD) || (biddyManagerType == BIDDYTYPEZFDDC) ||
2389  (biddyManagerType == BIDDYTYPETZFDD) || (biddyManagerType == BIDDYTYPETZFDDC))
2390  {
2391  fprintf(stderr,"Biddy_EvalProbability: this BDD type is not supported, yet!\n");
2392  return 0;
2393  } else {
2394  fprintf(stderr,"Biddy_EvalProbability: Unsupported BDD type!\n");
2395  return 0;
2396  }
2397 
2398  if (Biddy_IsNull(f)) return 0;
2399  if (f == biddyZero) return 0;
2400  if (Biddy_IsTerminal(f)) return 1;
2401 
2402  BiddyCreateLocalInfo(MNG,f);
2403  evalProbability(MNG,f,&r1,&r0,&rf); /* all nodes except terminal node are selected */
2404  BiddyDeleteLocalInfo(MNG,f);
2405 
2406  return r1;
2407 }
2408 
2409 #ifdef __cplusplus
2410 }
2411 #endif
2412 
2413 /***************************************************************************/
2424 #ifdef __cplusplus
2425 extern "C" {
2426 #endif
2427 
2430 {
2431  if (!MNG) MNG = biddyAnonymousManager;
2432 
2433  return GET_ORDER(biddyOrderingTable,fv,gv);
2434 }
2435 
2436 #ifdef __cplusplus
2437 }
2438 #endif
2439 
2440 /***************************************************************************/
2451 #ifdef __cplusplus
2452 extern "C" {
2453 #endif
2454 
2457 {
2458  /* lowest (topmost) variable has global ordering 1 */
2459  /* global ordering is the number of zeros in corresponding line of orderingTable */
2460 
2461  if (!MNG) MNG = biddyAnonymousManager;
2462 
2463  /* FOR OBDDs AND OFDDs: the lowest (topmost) variable always has prev=biddyVariableTable.size */
2464  /* FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: the topmost variable always has prev=biddyVariableTable.num */
2465 
2466  if (v >= biddyVariableTable.num) {
2467  return FALSE;
2468  } else {
2469  return (biddyVariableTable.table[v].prev >= biddyVariableTable.num);
2470  }
2471 }
2472 
2473 #ifdef __cplusplus
2474 }
2475 #endif
2476 
2477 /***************************************************************************/
2488 #ifdef __cplusplus
2489 extern "C" {
2490 #endif
2491 
2494 {
2495  /* bottommost variable is '1' and has global ordering numUsedVariables */
2496  /* global ordering is the number of zeros in corresponding line of orderingTable */
2497 
2498  if (!MNG) MNG = biddyAnonymousManager;
2499 
2500  /* ALWAYS: the bottommost variable has next=0 */
2501 
2502  if ((biddyVariableTable.num == 1) && (v == 0)) return TRUE;
2503  if ((v == 0) || (v >= biddyVariableTable.num)) {
2504  return FALSE;
2505  } else {
2506  return (biddyVariableTable.table[v].next == 0);
2507  }
2508 }
2509 
2510 #ifdef __cplusplus
2511 }
2512 #endif
2513 
2514 /***************************************************************************/
2546 #ifdef __cplusplus
2547 extern "C" {
2548 #endif
2549 
2552  Biddy_Boolean varelem)
2553 {
2554  unsigned int i;
2555  Biddy_Variable v,w;
2556  int cc;
2557  Biddy_Boolean isNumbered,find;
2558  Biddy_Edge result;
2559 
2560  if (!MNG) MNG = biddyAnonymousManager;
2561 
2562  v = 0;
2563  isNumbered = FALSE;
2564  if (!x) {
2565 
2566  biddyVariableTable.numnum++;
2567  if (!(x = (Biddy_String)malloc(15))) {
2568  fprintf(stderr, "Biddy_Managed_FoaVariable: Out of memoy!\n");
2569  exit(1);
2570  }
2571  sprintf(x,"%u",biddyVariableTable.numnum);
2572  v = biddyVariableTable.num;
2573  find = FALSE;
2574  isNumbered = TRUE;
2575 
2576  } else {
2577 
2578  /* SEARCH FOR THE EXISTING VARIABLE/ELEMENT/FORMULA WITH THE GIVEN NAME */
2579  /* VARIABLE TABLE IS NEVER EMPTY. AT LEAST, THERE IS ELEMENT '1' AT INDEX [0] */
2580  v = 0;
2581  find = FALSE;
2582  while (!find && v<biddyVariableTable.num) {
2583  if (!strcmp(x,biddyVariableTable.table[v].name)) {
2584  find = TRUE;
2585  } else {
2586  v++;
2587  }
2588  }
2589 
2590  /* SEARCH FOR THE VARIABLE/ELEMENT IN THE LOOKUP TABLE INSTEAD IN THE ORIGINAL TABLE */
2591 
2592  }
2593 
2594  /* IF find THEN v IS THE INDEX OF THE CORRECT VARIABLE/ELEMENT! */
2595  if (!find) {
2596 
2597  /* SEARCH FOR THE EXISTING FORMULA WITH THE SAME NAME */
2598  /* FORMULAE IN FORMULA TABLE ARE ORDERED BY NAME */
2599  /* TO DO: USE THE SAME METHOD AS IN FindFormula */
2600  for (i = 0; !find && (i < biddyFormulaTable.numOrdered); i++) {
2601  if (biddyFormulaTable.table[i].name) {
2602  cc = strcmp(x,biddyFormulaTable.table[i].name);
2603  if ((cc == 0) && !biddyFormulaTable.table[i].deleted) {
2604  find = TRUE;
2605  break;
2606  }
2607  if (cc < 0) break;
2608  } else {
2609  fprintf(stderr,"Biddy_Managed_FoaVariable: Problem with the formula table!\n");
2610  exit(1);
2611  }
2612  }
2613 
2614  if (find) {
2615  printf("WARNING (Biddy_Managed_FoaVariable): new variable/element %s has the same name as an existing formula!\n",x);
2616  }
2617 
2618  /* addVariableElement creates variable, prolongs results, and returns variable edge */
2619  result = addVariableElement(MNG,x);
2620 
2621  assert ( v == biddyVariableTable.num-1 );
2622 
2623  /* *** ADAPTING CACHE TABLES *** */
2624 
2625  /* FOR OBDDs AND OFDDs, CACHE DOES NOT NEED TO BE ADAPTED */
2626 
2627  /* FOR ZBDDs AND ZFDDs, CACHE DOES NOT NEED TO BE ADAPTED */
2628 
2629  /* FOR TZBDDs AND TZFDDs, ALL RESULTS IN CACHE WHERE TOP VARIABLE IS ABOVE THE NEW VARIABLE MAY BE WRONG! */
2630  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
2631  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
2632  {
2633  /* DEBUGGING */
2634  /*
2635  printf("Biddy_Managed_FoaVariable: variable \"%s\"(%u) added, cleaning cache tables\n",x,v);
2636  */
2637 
2638  /* VARIANT 1: DELETE ONLY INVALID RESULTS */
2639  /*
2640  BiddyOPGarbageNewVariable(MNG,v);
2641  BiddyEAGarbageNewVariable(MNG,v);
2642  BiddyRCGarbageNewVariable(MNG,v);
2643  BiddyReplaceGarbageNewVariable(MNG,v);
2644  */
2645 
2646  /* VARIANT 2: SIMPLY DELETE ALL RESULTS */
2647 
2648  BiddyOPGarbageDeleteAll(MNG);
2649  BiddyEAGarbageDeleteAll(MNG);
2650  BiddyRCGarbageDeleteAll(MNG);
2651  BiddyReplaceGarbageDeleteAll(MNG);
2652 
2653  }
2654 
2655  /* *** ADAPTING FORMULAE *** */
2656 
2657  /* FOR OBDDs AND OFDDs, FORMULAE MUST BE ADAPTED IF THEY REPRESENT COMBINATION SETS */
2658  /* biddyZero AND biddyOne ALWAYS REPRESENT A BOOLEAN FORMULA! */
2659  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
2660  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
2661  {
2662  if (!varelem) {
2663  /* NOT IMPLEMENTED, YET */
2664  }
2665  }
2666 
2667  /* FOR ZBDDs AND ZFDDs, FORMULAE MUST BE ADAPTED IF THEY REPRESENT BOOLEAN FUNCTIONS */
2668  /* biddyZero AND biddyOne ALWAYS REPRESENT A BOOLEAN FORMULA! */
2669  /* first formula is 0, it is always a single terminal node */
2670  /* second formula is 1, it could be a large graph, e.g. for ZBDD */
2671  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
2672  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD))
2673  {
2674 
2675  if (varelem) {
2676 
2677  for (i = 1; i < biddyFormulaTable.size; i++) {
2678  if (!biddyFormulaTable.table[i].deleted && (biddyFormulaTable.table[i].f != result)) {
2679  if (BiddyIsSmaller(BiddyV(biddyFormulaTable.table[i].f),v)) {
2680  /* NOT IMPLEMENTED, YET */
2681  printf("Biddy_Managed_FoaVariable: For ZBDDs, adding new variable below the existing ones is not supported, yet!\n");
2682  return 0;
2683  }
2684  }
2685  }
2686 
2687  for (i = 1; i < biddyFormulaTable.size; i++) {
2688  if (!biddyFormulaTable.table[i].deleted && (biddyFormulaTable.table[i].f != result)) {
2689 
2690  /* DEBUGGING */
2691  /*
2692  printf("Biddy_FoaVariable: updating formula %s\n",biddyFormulaTable.table[i].name);
2693  */
2694 
2695  biddyFormulaTable.table[i].f =
2696  BiddyManagedTaggedFoaNode(MNG,v,biddyFormulaTable.table[i].f,
2697  biddyFormulaTable.table[i].f,v,TRUE); /* FoaNode returns an obsolete node! */
2698  BiddyRefresh(biddyFormulaTable.table[i].f);
2699 
2700  }
2701  }
2702 
2703  /* MNG[3] = biddyFormulaTable.table[0].f; */ /* biddyZero does not need to be updated */
2704  MNG[4] = biddyFormulaTable.table[1].f; /* biddyOne must be updated, e.g. for ZBDD */
2705 
2706  } else {
2707 
2708  for (i = 0; i < 2; i++) {
2709  biddyFormulaTable.table[i].f =
2710  BiddyManagedTaggedFoaNode(MNG,v,biddyFormulaTable.table[i].f,
2711  biddyFormulaTable.table[i].f,v,TRUE); /* FoaNode returns an obsolete node! */
2712  BiddyRefresh(biddyFormulaTable.table[i].f);
2713  }
2714 
2715  MNG[3] = biddyFormulaTable.table[0].f; /* biddyZero must be updated */
2716  MNG[4] = biddyFormulaTable.table[1].f; /* biddyOne must be updated */
2717 
2718  }
2719  }
2720 
2721  /* FOR TZBDDs AND TZFDDs, FORMULAE MUST BE ADAPTED REGARDLESS OF WHAT THEY REPRESENT */
2722  /* biddyZero AND biddyOne ALWAYS REPRESENT A BOOLEAN FORMULA! */
2723  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
2724  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
2725  {
2726 
2727  if (varelem) {
2728  /* FOR BOOLEAN FUNCTIONS, ALL FORMULAE WHERE TOP TAG IS ABOVE THE NEW VARIABLE MUST BE ADAPTED */
2729  if (biddyNodeTable.num > 1) {
2730  for (i = 1; i < biddyFormulaTable.size; i++) {
2731  if (!biddyFormulaTable.table[i].deleted && (biddyFormulaTable.table[i].f != result)) {
2732  if (BiddyIsSmaller(Biddy_GetTag(biddyFormulaTable.table[i].f),v)) {
2733  printf("Biddy_Managed_FoaVariable: For TZBDDs, adding new variable below the existing ones is not supported, yet!\n");
2734  return 0;
2735  }
2736  }
2737  }
2738  }
2739 
2740  } else {
2741  /* FOR COMBINATION SETS, ... */
2742  /* NOT IMPLEMENTED, YET */
2743  }
2744 
2745  }
2746 
2747  /* *** ADAPTING VARIABLES AND ELEMENTS *** */
2748 
2749  /* FOR OBDDs AND OFDDs, NEW VARIABLE IS ADDED BELOW ALL THE EXISTING ONES */
2750  /* FOR OBDDs AND OFDDs, ALL ELEMENTS MUST BE ADAPTED */
2751  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
2752  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
2753  {
2754  /* NOT IMPLEMENTED, YET */
2755  }
2756 
2757  /* FOR ZBDDs AND ZFDDs, NEW VARIABLE IS ADDED ABOVE ALL THE EXISTING ONES */
2758  /* FOR ZBDDs AND ZFDDs, ALL VARIABLES MUST BE ADAPTED */
2759  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
2760  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD))
2761  {
2762  for (w = 1; w < biddyVariableTable.num-1; w++) {
2763 
2764  /* DEBUGGING */
2765  /*
2766  printf("Biddy_FoaVariable: updating variable %s (w=%u)\n",Biddy_Managed_GetVariableName(MNG,w),w);
2767  printf("top node before updating: %s\n",Biddy_Managed_GetTopVariableName(MNG,biddyVariableTable.table[w].variable));
2768  */
2769 
2770  biddyVariableTable.table[w].variable =
2771  BiddyManagedTaggedFoaNode(MNG,v,biddyVariableTable.table[w].variable,
2772  biddyVariableTable.table[w].variable,v,TRUE); /* FoaNode returns an obsolete node! */
2773  BiddyRefresh(biddyVariableTable.table[w].variable);
2774 
2775  /* DEBUGGING */
2776  /*
2777  printf("top node of variable after updating: %s\n",Biddy_Managed_GetTopVariableName(MNG,biddyVariableTable.table[w].variable));
2778  */
2779  }
2780  }
2781 
2782  /* FOR TZBDDs AND TZFDDs, NEW VARIABLE IS ADDED ABOVE ALL THE EXISTING ONES */
2783  /* FOR TZBDDs AND TZFDDs, ELEMENTS MUST BE ADAPTED IF NEW VARIABLE IS ADDED ABOVE ALL THE EXISTING VARIABLES */
2784  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
2785  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
2786  {
2787  for (w = 1; w < biddyVariableTable.num-1; w++) {
2788  Biddy_SetTag(biddyVariableTable.table[w].element,v);
2789  }
2790  }
2791 
2792  /* FOR TZBDDs AND TZFDDs, ELEMENT MUST BE ADAPTED IF NEW VARIABLE IS ADDED IMMEDIATELLY BELLOW IT */
2793  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
2794  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
2795  {
2796  /* NOT NEEDED */
2797  }
2798 
2799  } else {
2800 
2801  /* assert( printf("WARNING (Biddy_Managed_FoaVariable): variable %s already exists\n",x) ); */
2802 
2803  }
2804 
2805  if (isNumbered) {
2806  free(x);
2807  }
2808 
2809  /* RETURN VARIABLE, WHICH HAS BEEN LOOKED FOR */
2810  return v;
2811 }
2812 
2813 #ifdef __cplusplus
2814 }
2815 #endif
2816 
2817 /***************************************************************************/
2830 #ifdef __cplusplus
2831 extern "C" {
2832 #endif
2833 
2834 void
2836 {
2837  if (!MNG) MNG = biddyAnonymousManager;
2838 
2839  if (v == 0) return; /* constant variable cannot be renamed */
2840  if (v >= biddyVariableTable.num) return; /* unexisting varible */
2841 
2842  free(biddyVariableTable.table[v].name);
2843  biddyVariableTable.table[v].name = strdup(x);
2844 }
2845 
2846 #ifdef __cplusplus
2847 }
2848 #endif
2849 
2850 /***************************************************************************/
2866 #ifdef __cplusplus
2867 extern "C" {
2868 #endif
2869 
2872 {
2873  if (!MNG) MNG = biddyAnonymousManager;
2874 
2875  return Biddy_Managed_FoaVariable(MNG,x,TRUE);
2876 }
2877 
2878 #ifdef __cplusplus
2879 }
2880 #endif
2881 
2882 /***************************************************************************/
2898 #ifdef __cplusplus
2899 extern "C" {
2900 #endif
2901 
2904 {
2905  if (!MNG) MNG = biddyAnonymousManager;
2906 
2907  return Biddy_Managed_FoaVariable(MNG,x,FALSE);
2908 }
2909 
2910 #ifdef __cplusplus
2911 }
2912 #endif
2913 
2914 /***************************************************************************/
2927 #ifdef __cplusplus
2928 extern "C" {
2929 #endif
2930 
2931 Biddy_Edge
2933 {
2934  Biddy_Edge f;
2935  Biddy_Variable x;
2936  Biddy_Variable i;
2937 
2938  if (!MNG) MNG = biddyAnonymousManager;
2939 
2940  assert( v > 0 );
2941  assert( v < biddyVariableTable.num );
2942 
2943  if (v == 0) {
2944  fprintf(stderr,"WARNING: variable cannot be added below constant variable\n");
2945  return biddyNull;
2946  }
2947 
2948  if (v >= biddyVariableTable.num ) {
2949  fprintf(stderr,"WARNING: variable cannot be added below the non-existing node\n");
2950  return biddyNull;
2951  }
2952 
2954  x = biddyVariableTable.num - 1;
2955 
2956  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
2957  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
2958  {
2959  if (v == biddyVariableTable.table[0].prev) return f; /* variable shifting is not needed */
2960  biddyVariableTable.table[0].prev = biddyVariableTable.table[x].prev;
2961  biddyVariableTable.table[biddyVariableTable.table[x].prev].next = 0;
2962  biddyVariableTable.table[biddyVariableTable.table[v].next].prev = x;
2963  biddyVariableTable.table[x].next = biddyVariableTable.table[v].next;
2964  biddyVariableTable.table[x].prev = v;
2965  biddyVariableTable.table[v].next = x;
2966  }
2967  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
2968  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
2969  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
2970  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
2971  {
2972  /* NOT IMPLEMENTED, YET */
2973  fprintf(stderr,"Biddy_AddVariableBelow:: this BDD type is not supported, yet!\n");
2974  return biddyNull;
2975  } else {
2976  fprintf(stderr,"Biddy_AddVariableBelow: Unsupported BDD type!\n");
2977  return biddyNull;
2978  }
2979 
2980  for (i=0; i<biddyVariableTable.size; i++) {
2981  if (GET_ORDER(biddyOrderingTable,v,i)) {
2982  SET_ORDER(biddyOrderingTable,x,i);
2983  CLEAR_ORDER(biddyOrderingTable,i,x);
2984  } else {
2985  SET_ORDER(biddyOrderingTable,i,x);
2986  CLEAR_ORDER(biddyOrderingTable,x,i);
2987  }
2988  }
2989 
2990  return f;
2991 }
2992 
2993 #ifdef __cplusplus
2994 }
2995 #endif
2996 
2997 /***************************************************************************/
3010 #ifdef __cplusplus
3011 extern "C" {
3012 #endif
3013 
3014 Biddy_Edge
3016 {
3017  Biddy_Edge f;
3018  Biddy_Variable x;
3019  Biddy_Variable i;
3020 
3021  if (!MNG) MNG = biddyAnonymousManager;
3022 
3023  assert( v < biddyVariableTable.num );
3024 
3025  if (v >= biddyVariableTable.num ) {
3026  fprintf(stderr,"WARNING: variable cannot be added above the non-existing node\n");
3027  return biddyNull;
3028  }
3029 
3031  x = biddyVariableTable.num - 1;
3032 
3033  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
3034  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
3035  {
3036  if (v == 0) return f; /* variable shifting is not needed */
3037  biddyVariableTable.table[0].prev = biddyVariableTable.table[x].prev;
3038  biddyVariableTable.table[biddyVariableTable.table[x].prev].next = 0;
3039  if (biddyVariableTable.table[v].prev != biddyVariableTable.size) {
3040  biddyVariableTable.table[biddyVariableTable.table[v].prev].next = x;
3041  }
3042  biddyVariableTable.table[x].prev = biddyVariableTable.table[v].prev;
3043  biddyVariableTable.table[x].next = v;
3044  biddyVariableTable.table[v].prev = x;
3045  }
3046  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
3047  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
3048  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
3049  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
3050  {
3051  /* NOT IMPLEMENTED, YET */
3052  fprintf(stderr,"Biddy_AddVariableAbove: this BDD type is not supported, yet!\n");
3053  return biddyNull;
3054  } else {
3055  fprintf(stderr,"Biddy_AddVariableAbove: Unsupported BDD type!\n");
3056  return biddyNull;
3057  }
3058 
3059  for (i=0; i<biddyVariableTable.size; i++) {
3060  if (GET_ORDER(biddyOrderingTable,i,v)) {
3061  SET_ORDER(biddyOrderingTable,i,x);
3062  CLEAR_ORDER(biddyOrderingTable,x,i);
3063  } else {
3064  SET_ORDER(biddyOrderingTable,x,i);
3065  CLEAR_ORDER(biddyOrderingTable,i,x);
3066  }
3067  }
3068 
3069  return f;
3070 }
3071 
3072 #ifdef __cplusplus
3073 }
3074 #endif
3075 
3076 /***************************************************************************/
3091 #ifdef __cplusplus
3092 extern "C" {
3093 #endif
3094 
3095 Biddy_Edge
3097  Biddy_Boolean leftright)
3098 {
3099  if (!MNG) MNG = biddyAnonymousManager;
3100 
3101  assert (
3102  (biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
3103  (biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
3104  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
3105  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
3106  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
3107  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD)
3108  );
3109 
3110  if (biddyManagerType == BIDDYTYPEOBDDC) {
3111  /* IMPLEMENTED */
3112  if (Biddy_GetMark(f) != mark) Biddy_SetMark(f); else Biddy_ClearMark(f);
3113  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3114  /* IMPLEMENTED */
3115  if (leftright) {
3116  if (Biddy_GetMark(f) != mark) Biddy_SetMark(f); else Biddy_ClearMark(f);
3117  }
3118  } else if (biddyManagerType == BIDDYTYPETZBDDC) {
3119  /* NOT IMPLEMENTED, YET */
3120  fprintf(stderr,"Biddy_TransferMark: this BDD type is not supported, yet!\n");
3121  return biddyNull;
3122  } else if ((biddyManagerType == BIDDYTYPEOFDDC) ||
3123  (biddyManagerType == BIDDYTYPEZFDDC) ||
3124  (biddyManagerType == BIDDYTYPETZFDDC))
3125  {
3126  fprintf(stderr,"Biddy_TransferMark: this BDD type is not supported, yet!\n");
3127  return biddyNull;
3128  } else if ((biddyManagerType == BIDDYTYPEOBDD) ||
3129  (biddyManagerType == BIDDYTYPEZBDD) ||
3130  (biddyManagerType == BIDDYTYPETZBDD) ||
3131  (biddyManagerType == BIDDYTYPEOFDD) ||
3132  (biddyManagerType == BIDDYTYPEZFDD) ||
3133  (biddyManagerType == BIDDYTYPETZFDD))
3134  {
3135  /* NOTHING TO TRANSFER */
3136  }
3137 
3138  return f;
3139 }
3140 
3141 #ifdef __cplusplus
3142 }
3143 #endif
3144 
3145 /***************************************************************************/
3157 #ifdef __cplusplus
3158 extern "C" {
3159 #endif
3160 
3161 Biddy_Edge
3163 {
3164  Biddy_Variable tag,var;
3165 
3166  if (!MNG) MNG = biddyAnonymousManager;
3167 
3168  assert(
3169  (biddyManagerType == BIDDYTYPETZBDD) ||
3170  (biddyManagerType == BIDDYTYPETZBDDC) ||
3171  (biddyManagerType == BIDDYTYPETZFDD) ||
3172  (biddyManagerType == BIDDYTYPETZFDDC)
3173  );
3174 
3175  tag = Biddy_GetTag(f);
3176  var = BiddyV(f);
3177 
3178  assert( BiddyIsSmaller(tag,var) );
3179 
3180  tag = biddyVariableTable.table[tag].next;
3181 
3182  if (biddyManagerType == BIDDYTYPETZBDD) {
3183 
3184  /* WE HAVE TO CHECK IF MINIMIZATION RULE 3 CAN BE APPLIED */
3185  if (var && (var == tag) && (BiddyE(f) == BiddyT(f))) {
3186  f = BiddyE(f);
3187  } else {
3188  Biddy_SetTag(f,tag);
3189  }
3190 
3191  assert ( (Biddy_GetTag(f) == BiddyV(f)) || BiddyIsSmaller(Biddy_GetTag(f),BiddyV(f)) );
3192 
3193  } else if (biddyManagerType == BIDDYTYPETZBDDC) {
3194  /* NOT IMPLEMENTED, YET */
3195  fprintf(stderr,"Biddy_IncTag: this BDD type is not supported, yet!\n");
3196  return biddyNull;
3197  } else if ((biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD)) {
3198  /* NOT IMPLEMENTED, YET */
3199  fprintf(stderr,"Biddy_IncTag: this BDD type is not supported, yet!\n");
3200  return biddyNull;
3201  }
3202 
3203  return f;
3204 }
3205 
3206 #ifdef __cplusplus
3207 }
3208 #endif
3209 
3210 /***************************************************************************/
3239 #ifdef __cplusplus
3240 extern "C" {
3241 #endif
3242 
3243 Biddy_Edge
3245  Biddy_Edge pt, Biddy_Variable ptag,
3246  Biddy_Boolean garbageAllowed)
3247 {
3248  Biddy_Edge r;
3249 
3250  if (!MNG) MNG = biddyAnonymousManager;
3251 
3252  assert( (pf == NULL) || (BiddyIsOK(pf) == TRUE) );
3253  assert( (pt == NULL) || (BiddyIsOK(pt) == TRUE) );
3254 
3255  if (biddyManagerType == BIDDYTYPEOBDD) {
3256  /* IMPLEMENTED */
3257  r = BiddyManagedTaggedFoaNode(MNG,v,pf,pt,ptag,garbageAllowed);
3258  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3259  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3260  /* IMPLEMENTED */
3261  r = BiddyManagedTaggedFoaNode(MNG,v,pf,pt,ptag,garbageAllowed);
3262  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3263  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3264  /* IMPLEMENTED */
3265  r = BiddyManagedTaggedFoaNode(MNG,v,pf,pt,ptag,garbageAllowed);
3266  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3267  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3268  /* IMPLEMENTED */
3269  r = BiddyManagedTaggedFoaNode(MNG,v,pf,pt,ptag,garbageAllowed);
3270  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3271  } else if (biddyManagerType == BIDDYTYPETZBDD) {
3272  /* IMPLEMENTED */
3273  r = BiddyManagedTaggedFoaNode(MNG,v,pf,pt,ptag,garbageAllowed);
3274  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3275  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3276  {
3277  fprintf(stderr,"Biddy_TaggedFoaNode: this BDD type is not supported, yet!\n");
3278  return biddyNull;
3279  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
3280  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
3281  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
3282  {
3283  fprintf(stderr,"Biddy_TaggedFoaNode: this BDD type is not supported, yet!\n");
3284  return biddyNull;
3285  } else {
3286  fprintf(stderr,"Biddy_TaggedFoaNode: Unsupported BDD type!\n");
3287  return biddyNull;
3288  }
3289 
3290  return r;
3291 }
3292 
3293 #ifdef __cplusplus
3294 }
3295 #endif
3296 
3297 Biddy_Edge
3298 BiddyManagedTaggedFoaNode(Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge pf,
3299  Biddy_Edge pt, Biddy_Variable ptag,
3300  Biddy_Boolean garbageAllowed)
3301 {
3302  unsigned int hash;
3303  Biddy_Edge edge;
3304  BiddyNode *sup, *sup1;
3305  Biddy_Boolean complementedResult;
3306  unsigned int i;
3307  BiddyNode ** tmp;
3308  Biddy_Boolean addNodeSpecial;
3309  Biddy_Variable tag;
3310 
3311  static BiddyNode *newFreeNodes;
3312 
3313  /* DEBUGGING */
3314  /*
3315  printf("BiddyManagedTaggedFoaNode: %p, %d\n",MNG,Biddy_Managed_GetManagerType(MNG));
3316  */
3317 
3318  assert( MNG != NULL );
3319 
3320  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
3321  assert(
3322  (biddyManagerType == BIDDYTYPEOBDD) ||
3323  (biddyManagerType == BIDDYTYPEOBDDC) ||
3324  (biddyManagerType == BIDDYTYPEZBDD) ||
3325  (biddyManagerType == BIDDYTYPEZBDDC) ||
3326  (biddyManagerType == BIDDYTYPETZBDD)
3327  );
3328 
3329  assert( v != 0 );
3330 
3331  /* CURRENTLY, SPECIAL CASE 2 IS ONLY INTENDED FOR USE WITH TAGGED BDDs */
3332  /* TO DO: USE SPECIAL CASE 2 FOR ALL BDD TYPES TO IMPROVE GRAPH COPYING/CONSTRUCTING */
3333  assert( (biddyManagerType == BIDDYTYPETZBDD) ||
3334  (biddyManagerType == BIDDYTYPETZBDDC) ||
3335  (ptag != 0) );
3336 
3337 #ifdef BIDDYEXTENDEDSTATS_YES
3338  biddyNodeTable.foa++;
3339 #endif
3340 
3341  /* DEBUGGING */
3342  /*
3343  printf("FOANODE: v=%u, pf = %p, pt = %p, tag = %u, biddyNull = %p\n",v,pf,pt,biddyNull,NULL);
3344  */
3345 
3346  /* DISABLE GC */
3347  /*
3348  garbageAllowed = FALSE;
3349  */
3350 
3351  addNodeSpecial = FALSE;
3352  complementedResult = FALSE;
3353 
3354  /* SPECIAL CASE1: pf == pt == NULL */
3355 
3356  if (!pf) {
3357  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3358  pf = biddyZero;
3359  pt = biddyTerminal;
3360  }
3361  else if (biddyManagerType == BIDDYTYPEZBDD) {
3362  pf = biddyZero;
3363  pt = biddyTerminal;
3364  }
3365  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3366  pf = biddyTerminal;
3367  pt = biddyTerminal;
3368  complementedResult = TRUE;
3369  }
3370  else if (biddyManagerType == BIDDYTYPETZBDD) {
3371  pf = biddyZero;
3372  pt = biddyTerminal;
3373  }
3374  else if (biddyManagerType == BIDDYTYPETZBDDC) {
3375  pf = biddyTerminal;
3376  pt = biddyTerminal;
3377  complementedResult = TRUE;
3378  }
3379  ptag = v;
3380  addNodeSpecial = TRUE;
3381  } else {
3382  assert( BiddyIsSmaller(v,BiddyV(pf)) );
3383  assert( BiddyIsSmaller(v,BiddyV(pt)) );
3384  }
3385 
3386  /* DEBUGGING */
3387  /*
3388  printf("FOANODE (%d)",Biddy_Managed_GetManagerType(MNG));
3389  if (addNodeSpecial) {
3390  printf("(addNodeSpecial==TRUE)");
3391  }
3392  printf(": v = <%s>%s, pf = <%s>%s, pt = <%s>%s\n",
3393  biddyVariableTable.table[ptag].name,
3394  biddyVariableTable.table[v].name,
3395  biddyVariableTable.table[Biddy_GetTag(pf)].name,
3396  Biddy_GetMark(pf)?"0":Biddy_Managed_GetTopVariableName(MNG,pf),
3397  biddyVariableTable.table[Biddy_GetTag(pt)].name,
3398  Biddy_GetMark(pt)?"0":Biddy_Managed_GetTopVariableName(MNG,pt));
3399  */
3400 
3401  /* SPECIAL CASE 2: ptag == 0 */
3402 
3403  if (!addNodeSpecial && ptag) {
3404 
3405  /* SIMPLE CASES */
3406 
3407  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3408  if (pf == pt) {
3409  return pf;
3410  }
3411  }
3412 
3413  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3414  if (pt == biddyZero) {
3415  return pf;
3416  }
3417  }
3418 
3419  else if (biddyManagerType == BIDDYTYPETZBDD) {
3420  if (BiddyR(pt) == biddyZero) {
3421  if (BiddyR(pf) == biddyZero) {
3422  return biddyZero;
3423  }
3424  tag = Biddy_GetTag(pf);
3425  v = biddyVariableTable.table[v].next;
3426  if (tag == v) {
3427  return Biddy_SetTag(pf,ptag);
3428  } else {
3429  return BiddyManagedTaggedFoaNode(MNG,v,pf,pf,ptag,garbageAllowed);
3430  }
3431  }
3432  if (pf == pt) {
3433  if (ptag == v) {
3434  return pf;
3435  }
3436  }
3437  }
3438 
3439  /* NORMALIZATION OF COMPLEMENTED EDGES */
3440 
3441  if (biddyManagerType == BIDDYTYPEOBDDC) {
3442  if (Biddy_GetMark(pt)) {
3443  Biddy_InvertMark(pf);
3444  Biddy_ClearMark(pt);
3445  complementedResult = TRUE;
3446  } else {
3447  complementedResult = FALSE;
3448  }
3449  }
3450 
3451  else if (biddyManagerType == BIDDYTYPEZBDDC) {
3452  if (Biddy_GetMark(pf)) {
3453  Biddy_ClearMark(pf);
3454  complementedResult = TRUE;
3455  } else {
3456  complementedResult = FALSE;
3457  }
3458  }
3459 
3460  else if (biddyManagerType == BIDDYTYPETZBDD) {
3461  /* COMPLEMENTED EDGES ARE NOT USED */
3462  }
3463 
3464  }
3465 
3466  /* SOME NODES ARE NOT HASHED IN THE USUAL WAY */
3467  /* FOR THEM, THE RESULTING EDGE IS STORED ONLY AS PART OF BiddyVariable */
3468  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
3469  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
3470  {
3471  if ((pf == biddyZero) && (pt == biddyTerminal) && !addNodeSpecial) {
3472  if (complementedResult) {
3473  return Biddy_Inv(biddyVariableTable.table[v].variable);
3474  } else {
3475  return biddyVariableTable.table[v].variable;
3476  }
3477  }
3478  }
3479  if ((biddyManagerType == BIDDYTYPEZBDD) || (biddyManagerType == BIDDYTYPEZFDD))
3480  {
3481  if ((pf == biddyZero) && (pt == biddyTerminal) && !addNodeSpecial) {
3482  return biddyVariableTable.table[v].element;
3483  }
3484  }
3485  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZFDDC))
3486  {
3487  if ((pf == biddyTerminal) && (pt == biddyTerminal) && !addNodeSpecial) {
3488  if (complementedResult) {
3489  return biddyVariableTable.table[v].element;
3490  }
3491  else {
3492  return Biddy_Inv(biddyVariableTable.table[v].element);
3493  }
3494  }
3495  }
3496  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
3497  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
3498  {
3499  if ((pf == biddyZero) && (pt == biddyTerminal) && !addNodeSpecial) {
3500  edge = biddyVariableTable.table[v].variable;
3501  Biddy_SetTag(edge,ptag);
3502  return edge;
3503  }
3504  }
3505 
3506  /* FIND OR ADD - THERE IS A HASH TABLE WITH CHAINING */
3507  /* THE CREATED NODE WILL ALWAYS BE THE FIRST NODE IN THE CHAIN */
3508  /* BECAUSE OF USED TRICKS, HASH FUNCTION MUST NEVER RETURN ZERO! */
3509  /* VARIABLES/ELEMENTS (v,0,1) ARE NOT HASHED IN THE USUAL WAY */
3510 
3511  if (addNodeSpecial) {
3512  sup = sup1 = NULL;
3513  hash = 0;
3514  } else {
3515  hash = nodeTableHash(v,pf,pt,biddyNodeTable.size);
3516  sup = biddyNodeTable.table[hash];
3517  sup1 = findNodeTable(MNG,v,pf,pt,&sup);
3518  }
3519 
3520  if ((!sup) || (v != sup->v)) {
3521 
3522  /* NEW NODE MUST BE ADDED */
3523 
3524  /* IF ALL GENERATED NODES ARE USED THEN TRY GARBAGE COLLECTION */
3525  if (garbageAllowed && !biddyFreeNodes) {
3526 
3527  /* PROFILING */
3528  /*
3529  fprintf(stderr,"AutoGC IN: biddyNodeTable.num = %u, biddyNodeTable.generated = %u\n",biddyNodeTable.num,biddyNodeTable.generated);
3530  */
3531 
3532  Biddy_Managed_AutoGC(MNG);
3533 
3534  /* PROFILING */
3535  /*
3536  fprintf(stderr,"AutoGC OUT: biddyNodeTable.num = %u, biddyNodeTable.generated = %u, free = %u (%.2f)\n",
3537  biddyNodeTable.num,biddyNodeTable.generated,biddyNodeTable.generated-biddyNodeTable.num,100.0*biddyNodeTable.num/biddyNodeTable.generated);
3538  */
3539 
3540  /* the table may be resized, thus the element must be rehashed */
3541  hash = nodeTableHash(v, pf, pt, biddyNodeTable.size);
3542  sup = biddyNodeTable.table[hash];
3543  sup1 = findNodeTable(MNG, v, pf, pt, &sup);
3544 
3545  }
3546 
3547  /* IF NO FREE NODES ARE FOUND THEN CREATE NEW BLOCK OF NODES */
3548  if (!biddyFreeNodes) {
3549 
3550  /* the size of a memory block is increased until the limit is reached */
3551  if (biddyNodeTable.blocksize < biddyNodeTable.limitblocksize)
3552  {
3553  biddyNodeTable.blocksize = biddyNodeTable.resizeratio * biddyNodeTable.size;
3554  if (biddyNodeTable.blocksize < biddyNodeTable.initblocksize)
3555  biddyNodeTable.blocksize = biddyNodeTable.initblocksize;
3556  if (biddyNodeTable.blocksize > biddyNodeTable.limitblocksize)
3557  biddyNodeTable.blocksize = biddyNodeTable.limitblocksize;
3558 
3559  /* PROFILING */
3560  /*
3561  printf(">");
3562  */
3563  }
3564 
3565  /* PROFILING */
3566  /*
3567  else {
3568  printf("=");
3569  }
3570  */
3571 
3572  if (!(newFreeNodes = (BiddyNode *)
3573  malloc((biddyNodeTable.blocksize) * sizeof(BiddyNode))))
3574  {
3575  fprintf(stderr, "\nBIDDY (BiddyManagedTaggedFoaNode): Out of memory error!\n");
3576  fprintf(stderr, "Currently, there exist %d nodes.\n", biddyNodeTable.num);
3577  exit(1);
3578  }
3579 
3580  biddyNodeTable.blocknumber++;
3581  if (!(tmp = (BiddyNode **)realloc(biddyNodeTable.blocktable,
3582  biddyNodeTable.blocknumber * sizeof(BiddyNode *))))
3583  {
3584  fprintf(stderr, "\nBIDDY (BiddyManagedTaggedFoaNode): Out of memory error!\n");
3585  fprintf(stderr, "Currently, there exist %d nodes.\n", biddyNodeTable.num);
3586  exit(1);
3587  }
3588  biddyNodeTable.blocktable = tmp;
3589  biddyNodeTable.blocktable[biddyNodeTable.blocknumber - 1] = newFreeNodes;
3590  biddyNodeTable.generated = biddyNodeTable.generated + biddyNodeTable.blocksize;
3591 
3592  newFreeNodes[biddyNodeTable.blocksize - 1].list = biddyFreeNodes;
3593  biddyFreeNodes = newFreeNodes;
3594  for (i = 0; i < biddyNodeTable.blocksize - 1; i++) {
3595  newFreeNodes = (BiddyNode*)(newFreeNodes->list = &newFreeNodes[1]);
3596  }
3597 
3598  /* PROFILING */
3599  /*
3600  fprintf(stderr,"FOANODE NEW BLOCK: biddyNodeTable.num = %u, biddyNodeTable.generated = %u, free = %u (%.2f)\n",
3601  biddyNodeTable.num,biddyNodeTable.generated,biddyNodeTable.generated-biddyNodeTable.num,100.0*biddyNodeTable.num/biddyNodeTable.generated);
3602  */
3603 
3604  }
3605 
3606  /* ADDING NEW NODE */
3607  (biddyNodeTable.num)++;
3608  if (biddyNodeTable.num > biddyNodeTable.max) biddyNodeTable.max = biddyNodeTable.num;
3609  (biddyVariableTable.table[v].num)++;
3610 
3611  sup = biddyFreeNodes;
3612  biddyFreeNodes = (BiddyNode *)sup->list;
3613 
3614  /* DEBUGGING */
3615  /*
3616  printf("FOANODE after the normalization: (%s,%s,%s)\n",
3617  Biddy_Managed_GetVariableName(MNG,v),
3618  Biddy_Managed_GetVariableName(MNG,BiddyV(pf)),
3619  Biddy_Managed_GetVariableName(MNG,BiddyV(pt))
3620  );
3621  */
3622 
3623  assert(BiddyIsSmaller(v,BiddyV(pf)));
3624  assert(BiddyIsSmaller(v,BiddyV(pt)));
3625 
3626  sup->f = pf; /* BE CAREFULL !!!! */
3627  sup->t = pt; /* you can create node with an arbitrary (wrong!) ordering */
3628  if (addNodeSpecial) {
3629  sup->expiry = biddySystemAge; /* variable/element node is refreshed! */
3630  } else {
3631  sup->expiry = 1; /* other nodes are not refreshed! */
3632  }
3633  sup->select = 0;
3634  sup->v = v;
3635 
3636  /* add new node to Node table */
3637  /* nodes (v,0,1) are not stored in Node table */
3638  if (!addNodeSpecial) {
3639  addNodeTable(MNG, hash, sup, sup1);
3640  }
3641 
3642  /* add new node to the list */
3643  /* all nodes are added to list, also variables/elements which are not added to Node table */
3644  /* lastNode->list IS NOT FIXED! */
3645  /* YOU MUST NEVER ASSUME THAT lastNode->list = NULL */
3646  biddyVariableTable.table[v].lastNode->list = (void *)sup;
3647  biddyVariableTable.table[v].lastNode = sup;
3648 
3649  }
3650 
3651  edge = sup;
3652 
3653  if (complementedResult) {
3654  Biddy_SetMark(edge);
3655  }
3656 
3657  if ((biddyManagerType == BIDDYTYPETZBDD) && ptag) {
3658  Biddy_SetTag(edge,ptag);
3659  }
3660 
3661  /* (Biddy v1.5) To enable efficient memory management (e.g. sifting) */
3662  /* the function started with the returned node is not recursively refreshed! */
3663 
3664  /* DEBUGGING */
3665  /*
3666  printf("FOANODE COMPLETE ");
3667  if (addNodeSpecial) printf("(addNodeSpecial==TRUE) ");
3668  debugEdge(MNG,edge);
3669  printf("\n");
3670  */
3671 
3672  /* DEBUGGING */
3673  /*
3674  if (!((biddyManagerType != BIDDYTYPETZBDD) || (Biddy_GetTag(edge) == BiddyV(edge)) || BiddyIsSmaller(Biddy_GetTag(edge),BiddyV(edge))))
3675  {
3676  printf("FOANODE ERROR");
3677  if (addNodeSpecial) printf(" (addNodeSpecial==TRUE)");
3678  printf("!\n");
3679  writeORDER(MNG);
3680  debugEdge(MNG,edge);
3681  printf("\n");
3682  }
3683  */
3684 
3685  assert( BiddyIsSmaller(BiddyV(edge),BiddyV(BiddyE(edge))) );
3686  assert( BiddyIsSmaller(BiddyV(edge),BiddyV(BiddyT(edge))) );
3687  assert( (biddyManagerType != BIDDYTYPETZBDD) || !ptag || (Biddy_GetTag(edge) == BiddyV(edge)) || BiddyIsSmaller(Biddy_GetTag(edge),BiddyV(edge)) );
3688  assert( (biddyManagerType != BIDDYTYPETZBDD) || !ptag || (Biddy_GetTag(BiddyE(edge)) == BiddyV(BiddyE(edge))) || BiddyIsSmaller(Biddy_GetTag(BiddyE(edge)),BiddyV(BiddyE(edge))) );
3689  assert( (biddyManagerType != BIDDYTYPETZBDD) || !ptag || (Biddy_GetTag(BiddyT(edge)) == BiddyV(BiddyT(edge))) || BiddyIsSmaller(Biddy_GetTag(BiddyT(edge)),BiddyV(BiddyT(edge))) );
3690 
3691  return edge;
3692 }
3693 
3694 /***************************************************************************/
3706 #ifdef __cplusplus
3707 extern "C" {
3708 #endif
3709 
3712 {
3713  if (!MNG) MNG = biddyAnonymousManager;
3714 
3715  return (!(BiddyN(f)->expiry) || ((BiddyN(f)->expiry) >= biddySystemAge));
3716 }
3717 
3718 #ifdef __cplusplus
3719 }
3720 #endif
3721 
3722 /***************************************************************************/
3757 #ifdef __cplusplus
3758 extern "C" {
3759 #endif
3760 
3761 void
3763  Biddy_Variable targetGEQ,Biddy_Boolean purge,
3764  Biddy_Boolean total)
3765 {
3766  unsigned int i,j;
3767  BiddyFormula *tmp;
3768  BiddyNode *tmpnode1,*tmpnode2;
3769  BiddyNode *sup;
3770  BiddyCacheList *c;
3771  Biddy_Boolean cacheOK;
3772  Biddy_Boolean resizeRequired;
3773  Biddy_Boolean gcUseful;
3774  Biddy_Variable v;
3775  unsigned int hash;
3776  clock_t starttime;
3777 
3778  if (!MNG) MNG = biddyAnonymousManager;
3779  ZF_LOGI("Biddy_Garbage");
3780 
3781  /* DEBUGGING */
3782  /*
3783  {
3784  static int n = 0;
3785  fprintf(stdout,"\nGarbage (%d), targetLT=%u, targetGEQ=%u, systemAge=%u, there are %u BDD nodes, NodeTableSize=%u\n",
3786  ++n,targetLT,targetGEQ,biddySystemAge,biddyNodeTable.num,biddyNodeTable.size);
3787  }
3788  */
3789 
3790  assert( (targetLT == 0) || (targetGEQ != 0) );
3791 
3792  /* GC calls used during sifting are not counted */
3793  if (targetLT == 0) {
3794  biddyNodeTable.garbage++;
3795  }
3796 
3797 #ifdef BIDDYEXTENDEDSTATS_YES
3798  if (!(biddyNodeTable.gcobsolete = (unsigned long long int *) realloc(biddyNodeTable.gcobsolete,
3799  biddyNodeTable.garbage * sizeof(unsigned long long int))))
3800  {
3801  fprintf(stderr,"Biddy_Managed_GC: Out of memoy!\n");
3802  exit(1);
3803  }
3804  biddyNodeTable.gcobsolete[biddyNodeTable.garbage-1] = 0;
3805 #endif
3806 
3807  /* DEBUGGING - REPORT ALL NODES WITH A SPECIFIC VARIABLE */
3808  /*
3809  {
3810  BiddyNode *sup;
3811  biddyVariableTable.table[3].lastNode->list = NULL;
3812  sup = biddyVariableTable.table[3].firstNode;
3813  while (sup) {
3814  debugNode(MNG,sup);
3815  sup = (BiddyNode *) sup->list;
3816  }
3817  printf("\n");
3818  }
3819  */
3820 
3821  starttime = clock();
3822 
3823  /* REMOVE ALL FORMULAE WHICH ARE NOT PRESERVED ANYMORE */
3824  /* The first two formulae ("0" and "1") are never removed. */
3825  /* Iff parameter purge is true then all formulae without name are removed. */
3826  /* Iff parameter purge is true then all deleted formulae (even if fortified/preserved) are removed. */
3827 
3828  if (targetLT == 0) {
3829  i = 2;
3830  biddyFormulaTable.numOrdered = 2;
3831  } else {
3832  /* if (targetLT != 0) then there should not obsolete formulae */
3833  i = biddyFormulaTable.size;
3834  }
3835  for (j = i; j < biddyFormulaTable.size; j++) {
3836 
3837  /* DEBUGGING */
3838  /*
3839  printf("[FORM:%s@%u]",biddyFormulaTable.table[j].name,biddyFormulaTable.table[j].expiry);
3840  */
3841 
3842  if (purge && !biddyFormulaTable.table[j].name) {
3843  biddyFormulaTable.table[j].deleted = TRUE;
3844  }
3845 
3846  if ((!purge || !biddyFormulaTable.table[j].deleted)
3847  &&
3848  (!biddyFormulaTable.table[j].expiry || biddyFormulaTable.table[j].expiry >= biddySystemAge))
3849  {
3850 
3851  /* THIS FORMULA IS OK */
3852  if (i != j) {
3853  biddyFormulaTable.table[i] = biddyFormulaTable.table[j];
3854  }
3855  if (biddyFormulaTable.table[i].name) biddyFormulaTable.numOrdered++;
3856  i++;
3857 
3858  } else {
3859 
3860  /* THIS FORMULA IS BAD */
3861 
3862  /* DEBUGGING */
3863  /*
3864  fprintf(stderr,"Biddy_Managed_GC: Formula %s will be deleted!\n",biddyFormulaTable.table[j].name);
3865  if (biddyFormulaTable.table[j].deleted) fprintf(stderr,"Biddy_Managed_GC: Formula has DELETED flag!\n");
3866  if (biddyFormulaTable.table[j].expiry && biddyFormulaTable.table[j].expiry < biddySystemAge)
3867  fprintf(stderr,"Biddy_Managed_GC: Formula is obsolete!\n");
3868  */
3869 
3870  if (biddyFormulaTable.table[j].name) free(biddyFormulaTable.table[j].name);
3871 
3872  }
3873  }
3874 
3875  /* UPDATE FORMULA TABLE */
3876  if (i != biddyFormulaTable.size) {
3877  biddyFormulaTable.size = i;
3878  if (!(tmp = (BiddyFormula *)
3879  realloc(biddyFormulaTable.table,biddyFormulaTable.size*sizeof(BiddyFormula))))
3880  {
3881  fprintf(stderr,"Biddy_Managed_GC: Out of memoy!\n");
3882  exit(1);
3883  }
3884  biddyFormulaTable.table = tmp;
3885  }
3886 
3887  /* if parameter purge is true then nodes which are not part of any non-obsolete */
3888  /* non-deleted formulae are removed even if they are fresh or fortified */
3889  /* (this should not be used during the automatic garbage collection!) */
3890 
3891  if ((targetLT == 0) && purge) {
3892  for (v=1; v<biddyVariableTable.num; v++) {
3893  biddyVariableTable.table[v].lastNode->list = NULL;
3894  sup = biddyVariableTable.table[v].firstNode;
3895  while (sup) {
3896  sup->expiry = 1;
3897  sup = (BiddyNode *) sup->list;
3898  }
3899  }
3900  }
3901 
3902  /* RESTORE expiry VALUE FOR TOP NODE OF ALL CONSTANTS, VARIABLES, ELEMENTS, AND EXTERNAL FORMULAE */
3903  /* THIS IS NEEDED EVEN IF PURGE == FALSE (E.G. SIFTING) */
3904  /* first formula is 0, it is always a single terminal node */
3905  /* second formula is 1, it could be a large graph, e.g. for ZBDD */
3906  BiddyRefresh(biddyZero);
3907  BiddyRefresh(biddyOne);
3908  for (v = 1; v < biddyVariableTable.num; v++) {
3909  BiddyRefresh(biddyVariableTable.table[v].variable);
3910  BiddyRefresh(biddyVariableTable.table[v].element);
3911  }
3912  for (j = 1; j < biddyFormulaTable.size; j++) {
3913  if (!Biddy_IsNull(biddyFormulaTable.table[j].f) &&
3914  !Biddy_IsTerminal(biddyFormulaTable.table[j].f))
3915  {
3916  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
3917  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
3918  {
3919  if ((BiddyE(biddyFormulaTable.table[j].f) == biddyZero) && (BiddyT(biddyFormulaTable.table[j].f) == biddyTerminal)) {
3920  /* variable/element already refreshed */
3921  } else {
3922  BiddyProlongOne(biddyFormulaTable.table[j].f,biddyFormulaTable.table[j].expiry);
3923  }
3924  }
3925  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
3926  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD))
3927  {
3928  if ((BiddyE(biddyFormulaTable.table[j].f) == biddyTerminal) && (BiddyT(biddyFormulaTable.table[j].f) == biddyTerminal)) {
3929  /* variable/element already refreshed */
3930  } else {
3931  BiddyProlongOne(biddyFormulaTable.table[j].f,biddyFormulaTable.table[j].expiry);
3932  }
3933  }
3934  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
3935  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
3936  {
3937  if ((BiddyE(biddyFormulaTable.table[j].f) == biddyZero) && (BiddyT(biddyFormulaTable.table[j].f) == biddyTerminal)) {
3938  /* variable/element already refreshed */
3939  } else {
3940  BiddyProlongOne(biddyFormulaTable.table[j].f,biddyFormulaTable.table[j].expiry);
3941  }
3942  }
3943  }
3944  }
3945 
3946  /* REFRESH OBSOLETE NODES WHICH SHOULD NOT BE OBSOLETE */
3947  /* ALSO, COUNT HOW MANY OBSOLETE NODES PER VARIABLE EXIST */
3948  for (v=1; v<biddyVariableTable.num; v++) {
3949  biddyVariableTable.table[v].lastNode->list = NULL;
3950  biddyVariableTable.table[v].numobsolete = 0;
3951  }
3952  for (v=1; v<biddyVariableTable.num; v++) {
3953  /* if (targetLT != 0) then nodes equal or higher (bottom-more) than targetLT */
3954  /* and smaller (top-more) than targetGEQ will not be prolonged */
3955  if (v == targetLT) {
3956  /* there is always at least one node in the list */
3957  sup = biddyVariableTable.table[v].firstNode;
3958  assert( sup != NULL );
3959  while (sup) {
3960  assert(sup->v == v) ;
3961  if ((sup->expiry) && (sup->expiry < biddySystemAge)) {
3962  (biddyVariableTable.table[v].numobsolete)++;
3963  }
3964  sup = (BiddyNode *) sup->list;
3965  }
3966  }
3967  else if ((targetLT == 0) || (BiddyIsSmaller(v,targetLT))) {
3968  /* (targetLT == 0) used in the above 'if' for the evaluation speed, only */
3969  /* there is always at least one node in the list */
3970  sup = biddyVariableTable.table[v].firstNode;
3971  assert( sup != NULL );
3972  assert( sup->v == v );
3973  /* successors of the first node in the list does not need to be prolonged */
3974  sup = (BiddyNode *) sup->list;
3975  while (sup) {
3976  assert( sup->v == v );
3977  if (!(sup->expiry) || (sup->expiry >= biddySystemAge)) {
3978  assert( !Biddy_IsNull(BiddyE(sup)) );
3979  assert( !Biddy_IsNull(BiddyT(sup)) );
3980  BiddyProlongRecursively(MNG,BiddyE(sup),sup->expiry,targetLT);
3981  BiddyProlongRecursively(MNG,BiddyT(sup),sup->expiry,targetLT);
3982  } else {
3983  (biddyVariableTable.table[v].numobsolete)++;
3984  }
3985  sup = (BiddyNode *) sup->list;
3986  }
3987  }
3988  }
3989 
3990  /* CHECK IF THE RESIZING OF NODE TABLE IS NECESSARY */
3991  i = biddyNodeTable.num; /* we will count how many nodes are non-obsolete */
3992  resizeRequired = FALSE;
3993  for (v=1; v<biddyVariableTable.num; v++) {
3994 
3995  /* there should be at least one non-obsolete node for each variable */
3996  assert ( biddyVariableTable.table[v].numobsolete < biddyVariableTable.table[v].num );
3997 
3998  i = i - biddyVariableTable.table[v].numobsolete;
3999  }
4000  resizeRequired = (
4001  (biddyNodeTable.size < biddyNodeTable.limitsize) &&
4002  (i > biddyNodeTable.resizeratio * biddyNodeTable.size)
4003  );
4004 
4005  /* IF (targetLT != 0) THEN NODE TABLE RESIZING IS DISABLED */
4006  if (targetLT != 0) resizeRequired = FALSE;
4007 
4008  /* CHECK IF THE DELETION OF NODES IS USEFUL - how many nodes will be deleted */
4009  gcUseful = ((biddyNodeTable.num - i) > (biddyNodeTable.gcratio * biddyNodeTable.blocksize));
4010  if (gcUseful) resizeRequired = FALSE;
4011 
4012  /* IF total AND THERE IS SOMETHING TO DELETE THEN gcUseful must be TRUE */
4013  if (total && (i < biddyNodeTable.num)) gcUseful = TRUE;
4014 
4015  /* DEBUGGING */
4016  /*
4017  printf("GC CHECK: %u obsolete nodes ",biddyNodeTable.num - i);
4018  if (gcUseful) printf("(GC useful) "); else printf("(GC NOT useful) ");
4019  if (resizeRequired) printf("(Resize required)"); else printf("Resize NOT required)");
4020  printf("\n");
4021  */
4022 
4023  /* REMOVE ALL OBSOLETE NODES */
4024  /* RESIZE NODE TABLE IF IT SEEMS TO BE TO SMALL */
4025  cacheOK = TRUE;
4026  if (gcUseful || resizeRequired) {
4027 
4028 #ifdef BIDDYEXTENDEDSTATS_YES
4029  biddyNodeTable.gcobsolete[biddyNodeTable.garbage-1] = (biddyNodeTable.num - i);
4030 #endif
4031 
4032  if (resizeRequired) {
4033 
4034  /* DEBUGGING */
4035  /*
4036  printf("Biddy_Managed_GC: resizeRequired == TRUE\n");
4037  */
4038 
4039  /* REMOVE OLD NODE TABLE */
4040  free(biddyNodeTable.table);
4041  biddyNodeTable.nodetableresize++;
4042 
4043  /* DETERMINE NEW SIZE OF THE NODE TABLE */
4044  while (resizeRequired) {
4045  biddyNodeTable.size = 2 * biddyNodeTable.size + 1;
4046  /* ADAPT PARAMETERS */
4047  #pragma warning(suppress: 4244)
4048  biddyNodeTable.gcratio = (1.0 - biddyNodeTable.gcratioX) + (biddyNodeTable.gcratio / biddyNodeTable.gcratioF);
4049  #pragma warning(suppress: 4244)
4050  biddyNodeTable.resizeratio = (1.0 - biddyNodeTable.resizeratioX) + (biddyNodeTable.resizeratio * biddyNodeTable.resizeratioF);
4051  if (biddyNodeTable.gcratio < 0.0) biddyNodeTable.gcratio = 0.0;
4052  if (biddyNodeTable.resizeratio < 0.0) biddyNodeTable.resizeratio = 0.0;
4053  resizeRequired = (
4054  (biddyNodeTable.size < biddyNodeTable.limitsize) &&
4055  (i > biddyNodeTable.resizeratio * biddyNodeTable.size)
4056  );
4057  }
4058  resizeRequired = TRUE; /* reset variable resizeRequired */
4059 
4060  /* CREATE NEW NODE TABLE */
4061  if (!(biddyNodeTable.table = (BiddyNode **)
4062  calloc((biddyNodeTable.size+2),sizeof(BiddyNode *)))) {
4063  fprintf(stderr,"Biddy_Managed_GC: Out of memoy!\n");
4064  exit(1);
4065  }
4066  biddyNodeTable.table[0] = (BiddyNode *) biddyTerminal;
4067 
4068  /* PROFILING */
4069  /*
4070  printf("(size=%u)(gcr=%.2f)(rr=%.2f)",biddyNodeTable.size,biddyNodeTable.gcratio,biddyNodeTable.resizeratio);
4071  */
4072 
4073  }
4074 
4075  /* PROFILING */
4076  /*
4077  else {
4078  printf("+");
4079  }
4080  */
4081 
4082  /* BECAUSE OF REHASHING (NODES ARE STORED IN NODE TABLE IN 'ORDERED' LISTS) */
4083  /* IT IS REQUIRED TO VISIT NODES STARTING WITH THE LAST VARIABLE! */
4084  /* LAST VARIABLE IS NOT THE SAME AS THE SMALLEST/LARGEST IN THE VARIABLE ORDERING! */
4085  for (v=biddyVariableTable.num-1; v>0; v--) {
4086 
4087  /* DEBUGGING - !!! PRINTF THE NUMBER OF OBSOLETE NODES PER VARIABLE !!! */
4088  /*
4089  printf("GC VARIABLE %u (NODES: %u, OBSOLETE NODES: %u)\n",v,biddyVariableTable.table[v].num,biddyVariableTable.table[v].numobsolete);
4090  */
4091 
4092  /* if (v >= targetLT) or (v < targetGEQ) then no action is required because */
4093  /* there should be no obsolete nodes with (v >= targetLT) or (v < targetGEQ) */
4094  /* please note, that resize is not allowed if (targetLT != 0) */
4095  /* (targetLT != 0) is used in the next 'if' for evaluation speed, only */
4096  if ((targetLT != 0) && (!BiddyIsSmaller(v,targetLT) || BiddyIsSmaller(v,targetGEQ))) continue;
4097 
4098  /* IF RESIZE THEN ALL NODES EXCEPT THE FIRST ONE MUST BE VISITED */
4099  if (resizeRequired) {
4100  biddyVariableTable.table[v].numobsolete = biddyVariableTable.table[v].num - 1;
4101  }
4102 
4103  /* BE CAREFULLY WITH TYPE BiddyNode !!!! */
4104  /* FIELDS 'prev' AND 'next' HAVE TO BE THE FIRST AND THE SECOND! */
4105  /* THIS COMPUTATION USE SOME TRICKS! */
4106 
4107  if (biddyVariableTable.table[v].numobsolete) {
4108 
4109  /* UPDATING NODE TABLE */
4110  /* there is always at least one node in the list and the first node is never obsolete */
4111  tmpnode1 = biddyVariableTable.table[v].firstNode;
4112  assert( BiddyIsOK(tmpnode1) );
4113 
4114  biddyVariableTable.table[v].lastNode->list = NULL;
4115 
4116  /* the first node in the list is variable/element */
4117  /* and because it is not stored in Node table it does not need rehashing */
4118  tmpnode2 = (BiddyNode *) tmpnode1->list;
4119 
4120  while (biddyVariableTable.table[v].numobsolete) {
4121 
4122  /* DEBUGGING */
4123  /*
4124  printf(" GC WHILE OBSOLETE NODES = %u\n",biddyVariableTable.table[v].numobsolete);
4125  */
4126 
4127  assert( tmpnode2 != NULL) ;
4128  assert( tmpnode2->v == v ) ;
4129 
4130  if (!(tmpnode2->expiry) || (tmpnode2->expiry >= biddySystemAge)) {
4131  /* fortified, fresh or prolonged node */
4132  tmpnode1 = tmpnode2;
4133 
4134  /* if resize is required then this node must be rehashed and stored into new Node table */
4135  if (resizeRequired) {
4136  hash = nodeTableHash(v,tmpnode2->f,tmpnode2->t,biddyNodeTable.size);
4137  addNodeTable(MNG,hash,tmpnode2,NULL); /* add node to hash table */
4138  (biddyVariableTable.table[v].numobsolete)--; /* if resize is required then all nodes are counted with this counter */
4139  }
4140 
4141  } else {
4142 
4143  /* if targetLT is used then */
4144  /* there should not exist obsolete nodes with variable equal or higher than targetLT */
4145  /* and variable smaller than targetGEQ */
4146  /* in fact, nodes with obsolete 'expiry' may exist but only because */
4147  /* they have not been prolonged - they must not be removed! */
4148  assert( (targetLT == 0) || (BiddyIsSmaller(v,targetLT) && !BiddyIsSmaller(v,targetGEQ)) ) ;
4149 
4150  /* DEBUGGING */
4151  /*
4152  printf("REMOVE %p\n",(void *)tmpnode2);
4153  */
4154 
4155  /* obsolete node */
4156  cacheOK = FALSE;
4157  (biddyNodeTable.num)--;
4158  (biddyVariableTable.table[v].num)--;
4159  (biddyVariableTable.table[v].numobsolete)--;
4160  /* if resize is not required then remove from Node table */
4161  if (!resizeRequired) {
4162  tmpnode2->prev->next = tmpnode2->next;
4163  if (tmpnode2->next) {
4164  tmpnode2->next->prev = tmpnode2->prev;
4165  }
4166  }
4167  /* update list of live nodes */
4168  tmpnode1->list = (BiddyNode *) tmpnode2->list;
4169  /* insert obsolete node to the list of free nodes */
4170  tmpnode2->list = (void *) biddyFreeNodes;
4171  biddyFreeNodes = tmpnode2;
4172  }
4173 
4174  tmpnode2 = (BiddyNode *) tmpnode1->list;
4175  }
4176  if (!tmpnode1->list) {
4177  biddyVariableTable.table[v].lastNode = tmpnode1;
4178  }
4179  }
4180 
4181  }
4182  }
4183 
4184  /* DEBUGGING */
4185  /*
4186  else {
4187  printf("#");
4188  }
4189  */
4190 
4191  /* Updating cache tables - only if needed */
4192  if (!cacheOK) {
4193  c = biddyCacheList;
4194  while (c) {
4195  c->gc(MNG);
4196  c = c->next;
4197  }
4198  }
4199 
4200  /* DEBUGGING */
4201  /*
4202  printf("GC FINISHED: systemAge = %u, there are %u BDD nodes, NodeTableSize = %u\n",
4203  biddySystemAge,biddyNodeTable.num,biddyNodeTable.size);
4204  */
4205 
4206  /* DEBUGGING */
4207  /*
4208  if (purge) {
4209  for (v=1; v<biddyVariableTable.num; v++) {
4210  biddyVariableTable.table[v].lastNode->list = NULL;
4211  sup = biddyVariableTable.table[v].firstNode;
4212  while (sup) {
4213  if ((sup->expiry) && (sup->expiry < biddySystemAge)) {
4214  printf("Biddy_Managed_GC:: INVALID OBSOLETE NODE!\n");
4215  exit(1);
4216  }
4217  sup = (BiddyNode *) sup->list;
4218  }
4219  }
4220  }
4221  */
4222 
4223  /* GC calls used during sifting are not counted */
4224  if (targetLT == 0) {
4225  biddyNodeTable.gctime += clock() - starttime;
4226  }
4227 }
4228 
4229 #ifdef __cplusplus
4230 }
4231 #endif
4232 
4233 /***************************************************************************/
4247 #ifdef __cplusplus
4248 extern "C" {
4249 #endif
4250 
4251 void
4253 {
4254  Biddy_Variable v;
4255 
4256  if (!MNG) MNG = biddyAnonymousManager;
4257 
4258  /* DISCARD ALL NODES WHICH ARE NOT PRESERVED */
4259  /* implemented by simple increasing of biddySystemAge */
4260  BiddyIncSystemAge(MNG);
4261 
4262  /* to ensure that parameters in external functions are never obsolete, */
4263  /* constant functions must be explicitly refreshed, here */
4264  BiddyRefresh(biddyZero);
4265  BiddyRefresh(biddyOne);
4266 
4267  /* to ensure that parameters in external functions are never obsolete, */
4268  /* all variables and elements must be explicitly refreshed, here */
4269  for (v = 1; v < biddyVariableTable.num; v++) {
4270  BiddyRefresh(biddyVariableTable.table[v].variable);
4271  BiddyRefresh(biddyVariableTable.table[v].element);
4272  }
4273 
4274 }
4275 
4276 #ifdef __cplusplus
4277 }
4278 #endif
4279 
4280 /***************************************************************************/
4298 #ifdef __cplusplus
4299 extern "C" {
4300 #endif
4301 
4302 void
4304 {
4305  Biddy_Variable v;
4306 
4307  if (!MNG) MNG = biddyAnonymousManager;
4308 
4309  BiddyIncSystemAge(MNG);
4310  Biddy_Managed_GC(MNG,0,0,TRUE,TRUE); /* purge = TRUE, total = TRUE */
4311  BiddyDecSystemAge(MNG);
4312 
4313  /* constant functions must be explicitly repaired, here */
4314  BiddyDefresh(biddyZero);
4315  BiddyDefresh(biddyOne);
4316 
4317  /* all variables and elements must be explicitly repaired, here */
4318  for (v = 1; v < biddyVariableTable.num; v++) {
4319  BiddyDefresh(biddyVariableTable.table[v].variable);
4320  BiddyDefresh(biddyVariableTable.table[v].element);
4321  }
4322 }
4323 
4324 #ifdef __cplusplus
4325 }
4326 #endif
4327 
4328 /***************************************************************************/
4346 #ifdef __cplusplus
4347 extern "C" {
4348 #endif
4349 
4350 void
4352  Biddy_Boolean converge)
4353 {
4354  if (!MNG) MNG = biddyAnonymousManager;
4355 
4356  Biddy_Managed_Purge(MNG);
4357  Biddy_Managed_Sifting(MNG,f,converge);
4358 }
4359 
4360 #ifdef __cplusplus
4361 }
4362 #endif
4363 
4364 /***************************************************************************/
4375 #ifdef __cplusplus
4376 extern "C" {
4377 #endif
4378 
4379 void
4381 {
4382  if (!MNG) MNG = biddyAnonymousManager;
4383 
4384  BiddyRefresh(f);
4385 }
4386 
4387 #ifdef __cplusplus
4388 }
4389 #endif
4390 
4391 /***************************************************************************/
4401 #ifdef __cplusplus
4402 extern "C" {
4403 #endif
4404 
4405 void
4407 {
4408  BiddyCacheList *sup;
4409 
4410  if (!MNG) MNG = biddyAnonymousManager;
4411 
4412  if (!biddyCacheList) {
4413 
4414  if (!(biddyCacheList = (BiddyCacheList *) malloc(sizeof(BiddyCacheList)))) {
4415  fprintf(stdout,"Biddy_Managed_AddCache: Out of memoy!\n");
4416  exit(1);
4417  }
4418 
4419  biddyCacheList->gc = gc;
4420  biddyCacheList->next = NULL;
4421  } else {
4422  sup = biddyCacheList;
4423  while (sup->next) sup = sup->next;
4424 
4425  if (!(sup->next = (BiddyCacheList *) malloc(sizeof(BiddyCacheList)))) {
4426  fprintf(stdout,"Biddy_Managed_AddCache: Out of memoy!\n");
4427  exit(1);
4428  }
4429 
4430  sup = sup->next;
4431  sup->gc = gc;
4432  sup->next = NULL;
4433  }
4434 }
4435 
4436 #ifdef __cplusplus
4437 }
4438 #endif
4439 
4440 /***************************************************************************/
4475 #ifdef __cplusplus
4476 extern "C" {
4477 #endif
4478 
4479 unsigned int
4481 {
4482  unsigned int i;
4483  Biddy_Boolean OK;
4484  BiddyFormula *tmp;
4485  Biddy_Edge old;
4486 
4487  if (!MNG) MNG = biddyAnonymousManager;
4488 
4489  /* DEBUGGING */
4490  /*
4491  if (x) {
4492  printf("Biddy_Managed_AddFormula: Formula %s\n",x);
4493  } else {
4494  printf("Biddy_Managed_AddFormula: Anonymous formula with top variable %s\n",Biddy_Managed_GetTopVariableName(MNG,f));
4495  }
4496  */
4497 
4498  /*
4499  if (f && !BiddyIsOK(f)) {
4500  fprintf(stdout,"ERROR (Biddy_Managed_AddFormula): Bad f\n");
4501  free((void *)1);
4502  exit(1);
4503  }
4504  */
4505 
4506  if (c == -1) {
4507  c = biddySystemAge;
4508  }
4509  else if (c) {
4510  if ((c+biddySystemAge) < biddySystemAge) {
4511  BiddyCompactSystemAge(MNG);
4512  }
4513  c += biddySystemAge;
4514  }
4515 
4516  /* if formula does not have a name and is NULL or constant function, */
4517  /* then it will not be added, such BDD is already fortified, redundancy not needed */
4518  if (!x && (Biddy_IsNull(f) || (f == biddyZero) || (f == biddyOne))) {
4519  return 0;
4520  }
4521 
4522  /* if formula does not have a name and it is the same as a basic variable/element, */
4523  /* then it will not be added, such BDD is already fortified, redundancy not needed */
4524  if (!x && !Biddy_IsNull(f)) {
4525  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
4526  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
4527  {
4528  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
4529  return 0;
4530  }
4531  }
4532  if ((biddyManagerType == BIDDYTYPEZBDD) || (biddyManagerType == BIDDYTYPEZFDD))
4533  {
4534  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
4535  return 0;
4536  }
4537  }
4538  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZFDDC))
4539  {
4540  if ((BiddyE(f) == biddyTerminal) && (BiddyT(f) == biddyTerminal)) {
4541  return 0;
4542  }
4543  }
4544  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
4545  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
4546  {
4547  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
4548  return 0;
4549  }
4550  }
4551  }
4552 
4553  /* SEARCH IN THE FORMULA TABLE */
4554  if (!x) {
4555  OK = FALSE;
4556  i = biddyFormulaTable.size; /* tmp formulae are added on the end of the table */
4557  } else {
4558  OK = Biddy_Managed_FindFormula(MNG,x,&i,&old);
4559  }
4560 
4561  /* DEBUGGING */
4562  /*
4563  printf("Biddy_Managed_AddFormula: biddyFormulaTable.size = %u, findFormula returned %u\n",biddyFormulaTable.size,i);
4564  */
4565 
4566  /* the first two formulae ("0" and "1") must not be changed */
4567  if (OK && (i<2))
4568  {
4569  printf("WARNING (Biddy_Managed_AddFormula): formula %s not added because it has the same name as the existing constant!\n",x);
4570  return i;
4571  }
4572 
4573  /* element found */
4574  if (OK) {
4575 
4576  /* need to change persistent formula - new formula will be created */
4577  if (!biddyFormulaTable.table[i].expiry) {
4578  if (!biddyFormulaTable.table[i].deleted) {
4579  biddyFormulaTable.table[i].deleted = TRUE;
4580  i++;
4581  OK = FALSE;
4582  } else {
4583  fprintf(stderr,"Biddy_Managed_AddFormula: Problem with deleted persistent function!\n");
4584  exit(1);
4585  }
4586  }
4587 
4588  /* need to change preserved formula - new formula will be created */
4589  else if (biddyFormulaTable.table[i].expiry > biddySystemAge) {
4590  if (!biddyFormulaTable.table[i].deleted) {
4591  biddyFormulaTable.table[i].deleted = TRUE;
4592  i++;
4593  OK = FALSE;
4594  } else {
4595  fprintf(stderr,"Biddy_Managed_AddFormula: Problem with deleted preserved function!\n");
4596  exit(1);
4597  }
4598  }
4599 
4600  }
4601 
4602  /* element can be reused */
4603  if (OK) {
4604 
4605  /* DEBUGGING */
4606  /*
4607  printf("Biddy_Managed_AddFormula: Formula %s OVERWRITTEN!\n",x);
4608  */
4609 
4610  biddyFormulaTable.table[i].f = f;
4611  biddyFormulaTable.table[i].expiry = (unsigned int) c;
4612  biddyFormulaTable.table[i].deleted = FALSE;
4613  if (!Biddy_IsNull(f)) {
4614  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
4615  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
4616  {
4617  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
4618  /* this is variable, not changed */
4619  } else {
4620  BiddyProlongOne(f,(unsigned int) c);
4621  }
4622  }
4623  if ((biddyManagerType == BIDDYTYPEZBDD) || (biddyManagerType == BIDDYTYPEZFDD))
4624  {
4625  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
4626  /* this is element, not changed */
4627  } else {
4628  BiddyProlongOne(f,(unsigned int) c);
4629  }
4630  }
4631  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZFDDC))
4632  {
4633  if ((BiddyE(f) == biddyTerminal) && (BiddyT(f) == biddyTerminal)) {
4634  /* this is element, not changed */
4635  }
4636  else {
4637  BiddyProlongOne(f, (unsigned int)c);
4638  }
4639  }
4640  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
4641  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
4642  {
4643  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
4644  /* this is variable/element, not changed */
4645  } else {
4646  BiddyProlongOne(f,(unsigned int) c);
4647  }
4648  }
4649  }
4650  return i;
4651  }
4652 
4653  /* formula must be added, indices of the first two formulae must not be changed */
4654  if (i < 2) {
4655  fprintf(stderr,"Biddy_Managed_AddFormula: Name of the formula must be after \"1\"!\n");
4656  exit(1);
4657  }
4658 
4659  biddyFormulaTable.size++;
4660  if (!(tmp = (BiddyFormula *)
4661  realloc(biddyFormulaTable.table,biddyFormulaTable.size*sizeof(BiddyFormula))))
4662  {
4663  fprintf(stderr,"Biddy_Managed_AddFormula: Out of memoy!\n");
4664  exit(1);
4665  }
4666  biddyFormulaTable.table = tmp;
4667 
4668  /* DEBUGGING */
4669  /*
4670  printf("Biddy_Managed_AddFormula: biddyFormulaTable.size = %u, i = %u\n",biddyFormulaTable.size,i);
4671  */
4672 
4673  memmove(&biddyFormulaTable.table[i+1],&biddyFormulaTable.table[i],(biddyFormulaTable.size-i-1)*sizeof(BiddyFormula));
4674  /*
4675  for (j = biddyFormulaTable.size-1; j > i; j--) {
4676  biddyFormulaTable.table[j] = biddyFormulaTable.table[j-1];
4677  }
4678  */
4679 
4680  if (x) {
4681  biddyFormulaTable.table[i].name = strdup(x);
4682  biddyFormulaTable.numOrdered++;
4683  } else {
4684  biddyFormulaTable.table[i].name = NULL;
4685  }
4686  biddyFormulaTable.table[i].f = f;
4687  biddyFormulaTable.table[i].expiry = (unsigned int) c;
4688  biddyFormulaTable.table[i].deleted = FALSE;
4689  if (!Biddy_IsNull(f)) {
4690  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD) ||
4691  (biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD))
4692  {
4693  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
4694  /* this is variable, not changed */
4695  } else {
4696  BiddyProlongOne(f,(unsigned int) c);
4697  }
4698  }
4699  if ((biddyManagerType == BIDDYTYPEZBDD) || (biddyManagerType == BIDDYTYPEZFDD))
4700  {
4701  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
4702  /* this is element, not changed */
4703  } else {
4704  BiddyProlongOne(f,(unsigned int) c);
4705  }
4706  }
4707  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZFDDC))
4708  {
4709  if ((BiddyE(f) == biddyTerminal) && (BiddyT(f) == biddyTerminal)) {
4710  /* this is element, not changed */
4711  }
4712  else {
4713  BiddyProlongOne(f, (unsigned int)c);
4714  }
4715  }
4716  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD) ||
4717  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
4718  {
4719  if ((BiddyE(f) == biddyZero) && (BiddyT(f) == biddyTerminal)) {
4720  /* this is variable/element, not changed */
4721  } else {
4722  BiddyProlongOne(f,(unsigned int) c);
4723  }
4724  }
4725  }
4726 
4727  /* DEBUGGING */
4728  /*
4729  printf("Biddy_Managed_AddFormula: i=%d/%d, x=%s, f=%p\n",i,biddyFormulaTable.size-1,x,f);
4730  */
4731 
4732  if (!x) i = 0; /* if formula does not have a name return 0 */
4733 
4734  return i;
4735 }
4736 
4737 #ifdef __cplusplus
4738 }
4739 #endif
4740 
4741 /***************************************************************************/
4754 #ifdef __cplusplus
4755 extern "C" {
4756 #endif
4757 
4760  unsigned int *idx, Biddy_Edge *f)
4761 {
4762  unsigned int i,min,max;
4763  Biddy_Variable v;
4764  Biddy_Boolean OK;
4765  int cc;
4766 
4767  if (!MNG) MNG = biddyAnonymousManager;
4768 
4769  *idx = 0;
4770  *f = biddyNull;
4771  if (!x) return FALSE;
4772 
4773  assert ( biddyFormulaTable.table );
4774 
4775  if (!strcmp(x,biddyFormulaTable.table[0].name)) { /* [0] = biddyZero */
4776  *idx = 0;
4777  *f = biddyZero;
4778  return TRUE;
4779  }
4780 
4781  if (!strcmp(x,biddyFormulaTable.table[1].name)) { /* [1] = biddyOne */
4782  *idx = 1;
4783  *f = biddyOne;
4784  return TRUE;
4785  }
4786 
4787  /* VARIABLES ARE CONSIDERED TO BE FORMULAE, [0] = constant variable 1 */
4788  v = 1;
4789  OK = FALSE;
4790  while (!OK && v<biddyVariableTable.num) {
4791  if (!strcmp(x,biddyVariableTable.table[v].name)) {
4792  OK = TRUE;
4793  } else {
4794  v++;
4795  }
4796  }
4797  if (OK) {
4798  *f = biddyVariableTable.table[v].variable;
4799  return TRUE;
4800  }
4801 
4802  /* THERE ARE ONLY TWO FORMULAE, I.E. 0 AND 1 */
4803  if (biddyFormulaTable.numOrdered == 2) {
4804  *idx = 2;
4805  return FALSE;
4806  }
4807 
4808  /* VARIANT A: LINEAR SEARCH */
4809  /*
4810  OK = FALSE;
4811  for (i = 2; !OK && (i < biddyFormulaTable.numOrdered); i++) {
4812  if (biddyFormulaTable.table[i].name) {
4813  cc = strcmp(x,biddyFormulaTable.table[i].name);
4814  if ((cc == 0) && !biddyFormulaTable.table[i].deleted) {
4815  OK = TRUE;
4816  break;
4817  }
4818  if (cc < 0) break;
4819  } else {
4820  fprintf(stderr,"Biddy_Managed_FindFormula: Problem with the formula table!\n");
4821  exit(1);
4822  }
4823  }
4824  j = i;
4825  */
4826 
4827  /* VARIANT B: BINARY SEARCH */
4828  min = 2;
4829  max = biddyFormulaTable.numOrdered - 1;
4830 
4831  assert ( max <= biddyFormulaTable.size );
4832 
4833  /* DEBUGGING */
4834  /*
4835  fprintf(stderr,"biddyFormulaTable.size = %u, search for %s, min = %u (%s), max = %u (%s)\n",
4836  biddyFormulaTable.size,x,min,biddyFormulaTable.table[min].name,max,biddyFormulaTable.table[max].name);
4837  */
4838 
4839  cc = strcmp(x,biddyFormulaTable.table[min].name);
4840  if ((cc == 0) && !biddyFormulaTable.table[min].deleted) {
4841  i = min;
4842  OK = TRUE;
4843  } else if (cc < 0) {
4844  i = min;
4845  OK = FALSE;
4846  } else {
4847  cc = strcmp(x,biddyFormulaTable.table[max].name);
4848  if ((cc == 0) && !biddyFormulaTable.table[max].deleted) {
4849  i = max;
4850  OK = TRUE;
4851  } else if (cc > 0) {
4852  i = max+1;
4853  OK = FALSE;
4854  } else {
4855  i = (min + max) / 2;
4856  while (i != min) {
4857  cc = strcmp(x,biddyFormulaTable.table[i].name);
4858  if ((cc == 0) && !biddyFormulaTable.table[i].deleted) {
4859  min = max = i;
4860  OK = TRUE;
4861  } else if (cc < 0) {
4862  max = i;
4863  } else {
4864  min = i;
4865  }
4866  i = (min + max) / 2;
4867  }
4868  if (!OK) i++;
4869  }
4870  }
4871 
4872  /* DEBUGGING */
4873  /*
4874  if (i != j) {
4875  fprintf(stderr,"ERROR, i=%u, j=%u\n",i,j);
4876  for (i = 2; !OK && (i < biddyFormulaTable.numOrdered); i++) {
4877  fprintf(stderr,"%i. %s\n",i,biddyFormulaTable.table[i].name);
4878  }
4879  exit(1);
4880  }
4881  */
4882 
4883  if (OK) {
4884 
4885  /* element found */
4886  *idx = i;
4887  *f = biddyFormulaTable.table[i].f;
4888 
4889  /* DEBUGGING */
4890  /*
4891  printf("\nBiddy_FindFormula: i=%d, x=%s, f=%p\n",i,x,*f);
4892  */
4893 
4894  } else {
4895 
4896  /* element not found */
4897  *idx = i;
4898 
4899  /* DEBUGGING */
4900  /*
4901  printf("\nBiddy_FindFormula: <%s> NOT FOUND!\n",x);
4902  */
4903 
4904  }
4905 
4906  assert ( *idx <= biddyFormulaTable.size );
4907 
4908  return OK;
4909 }
4910 
4911 #ifdef __cplusplus
4912 }
4913 #endif
4914 
4915 /***************************************************************************/
4928 #ifdef __cplusplus
4929 extern "C" {
4930 #endif
4931 
4934 {
4935  unsigned int i;
4936  Biddy_Boolean OK;
4937  int cc;
4938 
4939  if (!MNG) MNG = biddyAnonymousManager;
4940 
4941  if (!x) {
4942  printf("WARNING (Biddy_Managed_DeleteFormula): empty name!\n");
4943  return FALSE;
4944  }
4945 
4946  OK = FALSE;
4947 
4948  if (!biddyFormulaTable.table) {
4949  i = 0;
4950  } else {
4951  for (i = 0; !OK && (i < biddyFormulaTable.numOrdered); i++) {
4952  if (biddyFormulaTable.table[i].name) {
4953  cc = strcmp(x,biddyFormulaTable.table[i].name);
4954  if ((cc == 0) && !biddyFormulaTable.table[i].deleted) {
4955  OK = TRUE;
4956  break;
4957  }
4958  if (cc < 0) break;
4959  } else {
4960  fprintf(stderr,"Biddy_Managed_DeleteFormula: Problem with the formula table!\n");
4961  exit(1);
4962  }
4963  }
4964  }
4965 
4966  if (OK) {
4967  OK = Biddy_Managed_DeleteIthFormula(MNG,i);
4968  }
4969 
4970  return OK;
4971 }
4972 
4973 #ifdef __cplusplus
4974 }
4975 #endif
4976 
4977 
4978 /***************************************************************************/
4992 #ifdef __cplusplus
4993 extern "C" {
4994 #endif
4995 
4998 {
4999  Biddy_Boolean OK;
5000 
5001  if (!MNG) MNG = biddyAnonymousManager;
5002 
5003  /* the first two formulae ("0" and "1") must not be deleted */
5004  if (i<2) {
5005  OK = FALSE;
5006  } else {
5007  OK = TRUE;
5008  }
5009 
5010  if (OK) {
5011  /* formulae representing variables must not be deleted */
5012  if (Biddy_IsNull(biddyFormulaTable.table[i].f) ||
5013  !biddyFormulaTable.table[i].name ||
5014  strcmp(biddyFormulaTable.table[i].name,
5015  Biddy_Managed_GetTopVariableName(MNG,biddyFormulaTable.table[i].f)))
5016  {
5017 
5018  /* DEBUGGING */
5019  /*
5020  if (biddyFormulaTable.table[i].name) {
5021  fprintf(stderr,"Biddy_Managed_DeleteIthFormula: Deleted %s\n",biddyFormulaTable.table[i].name);
5022  exit(1);
5023  }
5024  */
5025 
5026  /* this can be removed */
5027  biddyFormulaTable.table[i].deleted = TRUE;
5028  } else {
5029  OK = FALSE;
5030  }
5031  }
5032 
5033  return OK;
5034 }
5035 
5036 #ifdef __cplusplus
5037 }
5038 #endif
5039 
5040 /***************************************************************************/
5052 #ifdef __cplusplus
5053 extern "C" {
5054 #endif
5055 
5056 Biddy_Edge
5058 {
5059  if (!MNG) MNG = biddyAnonymousManager;
5060 
5061  if (!biddyFormulaTable.table) return biddyNull;
5062  if (i >= biddyFormulaTable.size) return biddyNull;
5063 
5064  return biddyFormulaTable.table[i].f;
5065 }
5066 
5067 #ifdef __cplusplus
5068 }
5069 #endif
5070 
5071 /***************************************************************************/
5083 #ifdef __cplusplus
5084 extern "C" {
5085 #endif
5086 
5089 {
5090  Biddy_String name;
5091 
5092  if (!MNG) MNG = biddyAnonymousManager;
5093 
5094  if (!biddyFormulaTable.table) return NULL;
5095  if (i >= biddyFormulaTable.size) return NULL;
5096 
5097  if (biddyFormulaTable.table[i].deleted) {
5098  name = biddyFormulaTable.deletedName;
5099  } else {
5100  name = biddyFormulaTable.table[i].name;
5101  }
5102 
5103  return name;
5104 }
5105 
5106 #ifdef __cplusplus
5107 }
5108 #endif
5109 
5110 /***************************************************************************/
5124 #ifdef __cplusplus
5125 extern "C" {
5126 #endif
5127 
5128 void
5130 {
5131  BiddyOrderingTable table;
5132 
5133  if (!MNG) MNG = biddyAnonymousManager;
5134 
5135  alphabeticOrdering(MNG,table);
5136  BiddySetOrdering(MNG,table);
5137 }
5138 
5139 #ifdef __cplusplus
5140 }
5141 #endif
5142 
5143 /***************************************************************************/
5157 #ifdef __cplusplus
5158 extern "C" {
5159 #endif
5160 
5163 {
5164  Biddy_Boolean active;
5165  Biddy_Variable vhigh;
5166 
5167  if (!MNG) MNG = biddyAnonymousManager;
5168 
5169  /* OBSOLETE NODES ARE REMOVED BEFORE SWAPPING */
5170  Biddy_Managed_AutoGC(MNG);
5171 
5172  if (biddyManagerType == BIDDYTYPEOBDD) {
5173  /* IMPLEMENTED */
5174  vhigh = swapWithHigher(MNG,v,&active);
5175  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
5176  /* IMPLEMENTED */
5177  vhigh = swapWithHigher(MNG,v,&active);
5178  } else if (biddyManagerType == BIDDYTYPEZBDD) {
5179  /* IMPLEMENTED */
5180  vhigh = swapWithHigher(MNG,v,&active);
5181  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
5182  /* IMPLEMENTED */
5183  vhigh = swapWithHigher(MNG,v,&active);
5184  } else if (biddyManagerType == BIDDYTYPETZBDD) {
5185  /* IMPLEMENTED */
5186  vhigh = swapWithHigher(MNG,v,&active);
5187  } else if (biddyManagerType == BIDDYTYPETZBDDC)
5188  {
5189  fprintf(stderr,"Biddy_SwapWithHigher: this BDD type is not supported, yet!\n");
5190  return 0;
5191  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
5192  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
5193  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
5194  {
5195  fprintf(stderr,"Biddy_SwapWithHigher: this BDD type is not supported, yet!\n");
5196  return 0;
5197  } else {
5198  fprintf(stderr,"Biddy_SwapWithHigher: Unsupported BDD type!\n");
5199  return 0;
5200  }
5201 
5202  return vhigh;
5203 }
5204 
5205 #ifdef __cplusplus
5206 }
5207 #endif
5208 
5209 /***************************************************************************/
5223 #ifdef __cplusplus
5224 extern "C" {
5225 #endif
5226 
5229 {
5230  Biddy_Boolean active;
5231  Biddy_Variable vlow;
5232 
5233  if (!MNG) MNG = biddyAnonymousManager;
5234 
5235  /* OBSOLETE NODES ARE REMOVED BEFORE SWAPPING */
5236  Biddy_Managed_AutoGC(MNG);
5237 
5238  if (biddyManagerType == BIDDYTYPEOBDD) {
5239  /* IMPLEMENTED */
5240  vlow = swapWithLower(MNG,v,&active);
5241  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
5242  /* IMPLEMENTED */
5243  vlow = swapWithLower(MNG,v,&active);
5244  } else if (biddyManagerType == BIDDYTYPEZBDD) {
5245  /* IMPLEMENTED */
5246  vlow = swapWithLower(MNG,v,&active);
5247  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
5248  /* IMPLEMENTED */
5249  vlow = swapWithLower(MNG,v,&active);
5250  } else if (biddyManagerType == BIDDYTYPETZBDD) {
5251  /* IMPLEMENTED */
5252  vlow = swapWithLower(MNG,v,&active);
5253  } else if (biddyManagerType == BIDDYTYPETZBDDC)
5254  {
5255  fprintf(stderr,"Biddy_SwapWithLower: this BDD type is not supported, yet!\n");
5256  return 0;
5257  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
5258  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
5259  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
5260  {
5261  fprintf(stderr,"Biddy_SwapWithLower: this BDD type is not supported, yet!\n");
5262  return 0;
5263  } else {
5264  fprintf(stderr,"Biddy_SwapWithLower: Unsupported BDD type!\n");
5265  return 0;
5266  }
5267 
5268  return vlow;
5269 }
5270 
5271 #ifdef __cplusplus
5272 }
5273 #endif
5274 
5275 /***************************************************************************/
5293 #ifdef __cplusplus
5294 extern "C" {
5295 #endif
5296 
5299 {
5300  Biddy_Boolean status;
5301  clock_t starttime;
5302 
5303  assert( (f == NULL) || (BiddyIsOK(f) == TRUE) );
5304 
5305  /* biddySiftingActive = TRUE; */
5306 
5307  if (!MNG) MNG = biddyAnonymousManager;
5308  ZF_LOGI("Biddy_Sifting");
5309 
5310  if (biddyManagerType == BIDDYTYPEOBDD) {
5311  /* IMPLEMENTED */
5312  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
5313  /* IMPLEMENTED */
5314  } else if (biddyManagerType == BIDDYTYPEZBDD) {
5315  /* IMPLEMENTED */
5316  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
5317  /* IMPLEMENTED */
5318  } else if (biddyManagerType == BIDDYTYPETZBDD) {
5319  /* IMPLEMENTED */
5320  } else if (biddyManagerType == BIDDYTYPETZBDDC)
5321  {
5322  fprintf(stderr,"Biddy_Sifting: this BDD type is not supported, yet!\n");
5323  return FALSE;
5324  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
5325  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
5326  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
5327  {
5328  fprintf(stderr,"Biddy_Sifting: this BDD type is not supported, yet!\n");
5329  return FALSE;
5330  } else {
5331  fprintf(stderr,"Biddy_Sifting: Unsupported BDD type!\n");
5332  return FALSE;
5333  }
5334 
5335  /* DEBUGGING */
5336  /*
5337  printf("SIFTING START: num sifting: %u\n",Biddy_Managed_NodeTableSiftingNumber(MNG));
5338  */
5339 
5340  /* DEBUGGING */
5341  /*
5342  {
5343  Biddy_Variable n;
5344  printf("========================================\n");
5345  printf("SIFTING START: num sifting: %u\n",Biddy_Managed_NodeTableSiftingNumber(MNG));
5346  printf("SIFTING START: num swapping: %u\n",Biddy_Managed_NodeTableSwapNumber(MNG));
5347  printf("SIFTING START: num garbage collection: %u\n",Biddy_Managed_NodeTableGCNumber(MNG));
5348  if (f) {
5349  BiddyFormula formula;
5350  printf("MINIMIZING NODE NUMBER FOR THE GIVEN FUNCTION\n");
5351  for (n=0;n<biddyFormulaTable.size;n++) {
5352  formula = biddyFormulaTable.table[n];
5353  if (formula.f == f) {
5354  if (formula.name) {
5355  printf("Formula name: %s\n",formula.name);
5356  } else {
5357  printf("Formula name: NULL\n");
5358  }
5359  }
5360  }
5361  printf("Initial number of dependent variables: %u\n",Biddy_Managed_DependentVariableNumber(MNG,f,FALSE));
5362  printf("Initial number of minterms: %.0f\n",Biddy_Managed_CountMinterms(MNG,f,0));
5363  printf("Initial number of nodes: %u\n",Biddy_Managed_CountNodes(MNG,f));
5364  printf("Top edge: %p\n",(void *) f);
5365  printf("Top variable: %s\n",Biddy_Managed_GetTopVariableName(MNG,f));
5366  printf("Expiry value of top node: %d\n",((BiddyNode *) BiddyP(f))->expiry);
5367  }
5368  printf("SIFTING: initial order\n");
5369  writeORDER(MNG);
5370  BiddySystemReport(MNG);
5371  for (n = 1; n < biddyFormulaTable.size; n++) {
5372  if (!Biddy_IsNull(biddyFormulaTable.table[n].f) &&
5373  !Biddy_IsTerminal(biddyFormulaTable.table[n].f))
5374  {
5375  assert( BiddyIsOK(biddyFormulaTable.table[n].f) );
5376  }
5377  }
5378  printf("========================================\n");
5379  }
5380  */
5381 
5382  biddyNodeTable.sifting++;
5383  starttime = clock();
5384 
5385  /* DELETE ALL CACHE TABLES AND DISABLE THEM */
5386  /* TO DO: user cache tables are not considered, yet */
5387  BiddyOPGarbageDeleteAll(MNG);
5388  BiddyEAGarbageDeleteAll(MNG);
5389  BiddyRCGarbageDeleteAll(MNG);
5390  BiddyReplaceGarbageDeleteAll(MNG);
5391  biddyOPCache.disabled = TRUE;
5392  biddyEACache.disabled = TRUE;
5393  biddyRCCache.disabled = TRUE;
5394  biddyReplaceCache.disabled = TRUE;
5395 
5396  if (!f) {
5397  /* MINIMIZING NODE NUMBER FOR THE WHOLE SYSTEM */
5398  /* WE REMOVE OBSOLETE NODES BECAUSE THEY SHOULD NOT BE CONSIDERED */
5399  /* WE DO NOT WANT TO USE PURGE HERE BECAUSE IT LIMITS THE USABILITY OF SIFTING */
5400  Biddy_Managed_ForceGC(MNG);
5401  status = BiddyGlobalSifting(MNG,converge);
5402  } else {
5403  /* MINIMIZING NODE NUMBER FOR THE GIVEN FUNCTION */
5404  status = BiddySiftingOnFunction(MNG,f,converge);
5405  }
5406 
5407  /* ENABLE ALL CACHE TABLES */
5408  /* TO DO: user caches are not considered, yet */
5409  biddyOPCache.disabled = FALSE;
5410  biddyEACache.disabled = FALSE;
5411  biddyRCCache.disabled = FALSE;
5412  biddyReplaceCache.disabled = FALSE;
5413 
5414  biddyNodeTable.drtime += clock() - starttime;
5415 
5416  /* DEBUGGING */
5417  /*
5418  {
5419  Biddy_Variable n;
5420  printf("========================================\n");
5421  printf("SIFTING FINISH: num sifting: %u\n",Biddy_Managed_NodeTableSiftingNumber(MNG));
5422  printf("SIFTING FINISH: num swapping: %u\n",Biddy_Managed_NodeTableSwapNumber(MNG));
5423  printf("SIFTING FINISH: num garbage collection: %u\n",Biddy_Managed_NodeTableGCNumber(MNG));
5424  if (f) {
5425  printf("Final number of dependent variables: %u\n",Biddy_Managed_DependentVariableNumber(MNG,f,FALSE));
5426  printf("Final number of minterms: %.0f\n",Biddy_Managed_CountMinterms(MNG,f,0));
5427  printf("Final number of nodes: %u\n",Biddy_Managed_CountNodes(MNG,f));
5428  printf("Top edge: %p\n",(void *) f);
5429  printf("Top variable: %s\n",Biddy_Managed_GetTopVariableName(MNG,f));
5430  printf("Expiry value of top node: %d\n",((BiddyNode *) BiddyP(f))->expiry);
5431  }
5432  printf("SIFTING: final order\n");
5433  writeORDER(MNG);
5434  BiddySystemReport(MNG);
5435  for (n = 1; n < biddyFormulaTable.size; n++) {
5436  if (!Biddy_IsNull(biddyFormulaTable.table[n].f) &&
5437  !Biddy_IsTerminal(biddyFormulaTable.table[n].f))
5438  {
5439  assert( BiddyIsOK(biddyFormulaTable.table[n].f) );
5440  }
5441  }
5442  printf("========================================\n");
5443  }
5444  */
5445 
5446  /* biddySiftingActive = FALSE; */
5447 
5448  return status; /* sifting has been performed */
5449 }
5450 
5451 #ifdef __cplusplus
5452 }
5453 #endif
5454 
5455 /***************************************************************************/
5476 #ifdef __cplusplus
5477 extern "C" {
5478 #endif
5479 
5480 void
5482 {
5483  Biddy_Edge f;
5484  unsigned int idx;
5485  unsigned int n,MIN;
5486  BiddyOrderingTable finalOrdering;
5487  Biddy_Boolean first;
5488 
5489  /* DEBUGGING */
5490  /*
5491  if (Biddy_Managed_FindFormula(MNG,name,&idx,&f)) {
5492  printf("MINIMIZE FOR %s STARTED\n",name);
5493  n = Biddy_Managed_CountNodes(MNG,f);
5494  printf("START: n=%u\n",n);
5495  } else {
5496  printf("MINIMIZE: FORMULA %s NOT FOUND\n",name);
5497  }
5498  */
5499 
5500  BiddySjtInit(MNG);
5501 
5502  MIN = 0;
5503  first = TRUE;
5504  do {
5505  Biddy_Managed_FindFormula(MNG,name,&idx,&f);
5506 
5507  /* use this to minimize the number of internal nodes */
5508  /*
5509  n = 0;
5510  Biddy_Managed_SelectNode(MNG,biddyTerminal);
5511  BiddyNodeNumber(MNG,f,&n);
5512  Biddy_Managed_DeselectAll(MNG);
5513  */
5514 
5515  /* use this to minimize the number of all nodes */
5516 
5517  n = Biddy_Managed_CountNodes(MNG,f);
5518 
5519 
5520  /* DEBUGGING */
5521  /*
5522  printf("MINIMIZATION STEP: n=%u\n",n);
5523  */
5524 
5525  if (first || (n < MIN)) {
5526  MIN = n;
5527  memcpy(finalOrdering,biddyOrderingTable,sizeof(BiddyOrderingTable));
5528  }
5529 
5530  first = FALSE;
5531 
5532  } while(BiddySjtStep(MNG));
5533 
5534  BiddySjtExit(MNG);
5535 
5536  BiddySetOrdering(MNG,finalOrdering);
5537 
5538  /* DEBUGGING */
5539  /*
5540  Biddy_Managed_FindFormula(MNG,name,&idx,&f);
5541  n = Biddy_Managed_CountNodes(MNG,f);
5542  printf("FINAL: n=%u\n",n);
5543  */
5544 }
5545 
5546 #ifdef __cplusplus
5547 }
5548 #endif
5549 
5550 /***************************************************************************/
5571 #ifdef __cplusplus
5572 extern "C" {
5573 #endif
5574 
5575 void
5577 {
5578  Biddy_Edge f;
5579  unsigned int idx;
5580  unsigned int n,MAX;
5581  BiddyOrderingTable finalOrdering;
5582 
5583  /* DEBUGGING */
5584  /*
5585  if (Biddy_Managed_FindFormula(MNG,name,&idx,&f)) {
5586  printf("MAXIMIZE FOR %s STARTED\n",name);
5587  n = Biddy_Managed_CountNodes(MNG,f);
5588  printf("START: n=%u\n",n);
5589  } else {
5590  printf("MAXIMIZE: FORMULA %s NOT FOUND\n",name);
5591  }
5592  */
5593 
5594  BiddySjtInit(MNG);
5595  MAX = 0;
5596  do {
5597  Biddy_Managed_FindFormula(MNG,name,&idx,&f);
5598 
5599  /* use this to maximize the number of internal nodes */
5600  /*
5601  n = 0;
5602  Biddy_Managed_SelectNode(MNG,biddyTerminal);
5603  BiddyNodeNumber(MNG,f,&n);
5604  Biddy_Managed_DeselectAll(MNG);
5605  */
5606 
5607  /* use this to maximize the number of all nodes */
5608 
5609  n = Biddy_Managed_CountNodes(MNG,f);
5610 
5611 
5612  /* DEBUGGING */
5613  /*
5614  printf("MAXIMIZATION STEP: n=%u\n",n);
5615  */
5616 
5617  if (!MAX || (n > MAX)) {
5618  MAX = n;
5619  memcpy(finalOrdering,biddyOrderingTable,sizeof(BiddyOrderingTable));
5620  }
5621  } while(BiddySjtStep(MNG));
5622 
5623  BiddySjtExit(MNG);
5624 
5625  BiddySetOrdering(MNG,finalOrdering);
5626 
5627  /* DEBUGGING */
5628  /*
5629  Biddy_Managed_FindFormula(MNG,name,&idx,&f);
5630  n = Biddy_Managed_CountNodes(MNG,f);
5631  printf("FINAL: n=%u\n",n);
5632  */
5633 }
5634 
5635 #ifdef __cplusplus
5636 }
5637 #endif
5638 
5639 /***************************************************************************/
5662 #ifdef __cplusplus
5663 extern "C" {
5664 #endif
5665 
5666 Biddy_Edge
5668 {
5669  Biddy_Edge r;
5670  Biddy_Variable v1,v2,k;
5671  Biddy_Variable top,prevvar;
5672  Biddy_String vname,topname;
5673  Biddy_Boolean simplecopy;
5674 
5675  if (!MNG1) MNG1 = biddyAnonymousManager;
5676  ZF_LOGI("Biddy_Copy");
5677 
5678  if (MNG1 == MNG2) {
5679  return f;
5680  }
5681 
5682  /* CHECK IF THE TARGET MNG IS EMPTY */
5683  simplecopy = FALSE;
5684  if (biddyVariableTable2.num == 1) {
5685  simplecopy = TRUE;
5686  }
5687 
5688  /* COPY THE DOMAIN */
5689  /* the ordering of the new variable is determined in Biddy_InitMNG */
5690  /* FOR OBDDs AND OFDDs: new variable is added below (bottommore) all others */
5691  /* FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: new variable is added above (topmore) all others */
5692  /* FINAL ORDER FOR OBDDs AND OFDDs: [1] < [2] < ... < [size-1] < [0] */
5693  /* FINAL ORDER FOR ZBDDs, ZFDDs, TZBDDs, AND TZFDDs: [size-1] < [size-2] < ... < [1] < [0] */
5694  if ((biddyManagerType2 == BIDDYTYPEOBDDC) || (biddyManagerType2 == BIDDYTYPEOBDD) ||
5695  (biddyManagerType2 == BIDDYTYPEOFDDC) || (biddyManagerType2 == BIDDYTYPEOFDD))
5696  {
5697  v1 = Biddy_Managed_GetLowestVariable(MNG1); /* lowest = topmost */
5698  for (k = 1; k < biddyVariableTable1.num; k++) {
5699  vname = Biddy_Managed_GetVariableName(MNG1,v1);
5700  v2 = Biddy_Managed_AddVariableByName(MNG2,vname);
5702  v1 = biddyVariableTable1.table[v1].next;
5703  }
5704  }
5705 
5706  else if ((biddyManagerType2 == BIDDYTYPEZBDDC) || (biddyManagerType2 == BIDDYTYPEZBDD) ||
5707  (biddyManagerType2 == BIDDYTYPEZFDDC) || (biddyManagerType2 == BIDDYTYPEZFDD) ||
5708  (biddyManagerType2 == BIDDYTYPETZBDDC) || (biddyManagerType2 == BIDDYTYPETZBDD) ||
5709  (biddyManagerType2 == BIDDYTYPETZFDDC) || (biddyManagerType2 == BIDDYTYPETZFDD))
5710  {
5711  v1 = 0;
5712  for (k = 1; k < biddyVariableTable1.num; k++) {
5713  v1 = biddyVariableTable1.table[v1].prev;
5714  vname = Biddy_Managed_GetVariableName(MNG1,v1);
5715  v2 = Biddy_Managed_AddVariableByName(MNG2,vname);
5717  }
5718  }
5719 
5720  else {
5721  fprintf(stderr,"Biddy_Managed_Copy: Unsupported BDD type for MNG2!\n");
5722  }
5723 
5724  /* DEBUGGING - PRINT BOTH DOMAINS */
5725  /*
5726  printf("Biddy_Copy: SOURCE DOMAIN FOR %s\n",Biddy_Managed_GetManagerName(MNG1));
5727  v1 = 0;
5728  for (k = 1; k < biddyVariableTable1.num; k++) {
5729  vname = Biddy_Managed_GetVariableName(MNG1,k);
5730  printf("(%u)%s,",k,vname);
5731  v1 = biddyVariableTable1.table[v1].prev;
5732  }
5733  printf("\n");
5734  for (k = 1; k < biddyVariableTable1.num; k++) {
5735  vname = Biddy_Managed_GetVariableName(MNG1,v1);
5736  printf("%s,",vname);
5737  v1 = biddyVariableTable1.table[v1].next;
5738  }
5739  printf("\n");
5740  printf("Biddy_Copy: TARGET DOMAIN FOR %s\n",Biddy_Managed_GetManagerName(MNG2));
5741  v1 = 0;
5742  for (k = 1; k < biddyVariableTable2.num; k++) {
5743  vname = Biddy_Managed_GetVariableName(MNG2,k);
5744  printf("(%u)%s,",k,vname);
5745  v1 = biddyVariableTable2.table[v1].prev;
5746  }
5747  printf("\n");
5748  for (k = 1; k < biddyVariableTable2.num; k++) {
5749  vname = Biddy_Managed_GetVariableName(MNG2,v1);
5750  printf("%s,",vname);
5751  v1 = biddyVariableTable2.table[v1].next;
5752  }
5753  printf("\n");
5754  if (simplecopy) printf("Biddy_Copy: SIMPLE COPY!\n");
5755  if (f == biddyZero1) printf("Biddy_Copy: DOMAIN COPIED AND FINISHED!\n");
5756  */
5757 
5758  if (f == biddyZero1) return biddyZero2; /* domain has been already copied */
5759 
5760  r = biddyNull;
5761 
5762  if (simplecopy) {
5763 
5764  if (biddyManagerType1 == biddyManagerType2) {
5765 
5766  /* MANAGERS ARE OF THE SAME TYPE AND THE TARGET MANAGER IS EMPTY */
5767  r = BiddyCopy(MNG1,MNG2,f);
5768 
5769  } else {
5770 
5771  /* MANAGERS ARE OF DIFFERENT TYPE BUT TARGET MNG IS EMPTY */
5772  /* WE USE DIRECT CONVERSION BECAUSE IT IS MORE EFFICIENT */
5773  r = BiddyConvertDirect(MNG1,MNG2,f);
5774 
5775  if (((biddyManagerType1 == BIDDYTYPEOBDDC) || (biddyManagerType1 == BIDDYTYPEOBDD))
5776  &&
5777  ((biddyManagerType2 == BIDDYTYPEOBDDC) || (biddyManagerType2 == BIDDYTYPEOBDD)))
5778  {
5779  /* RESULT IS ALREADY CORRECT */
5780  }
5781 
5782  else if (((biddyManagerType1 == BIDDYTYPEOBDDC) || (biddyManagerType1 == BIDDYTYPEOBDD))
5783  &&
5784  ((biddyManagerType2 == BIDDYTYPEZBDDC) || (biddyManagerType2 == BIDDYTYPEZBDD)))
5785  {
5786  /* BiddyConvertDirect does not create the topmost variables which are not present in OBDD */
5787  /* MNG2 was empty on the beginning and the domain have been correctly copied */
5788  /* thus, we can assume that MNG1 and MNG2 have the same ordering */
5789  /* NOTE: this implementation allows that MNG2 contains extra variables */
5790  /* NOTE: this implementation allows that the same variable has different indices in MNG1 and MNG2 */
5791 
5792  /* determine the topmost variable in the domain of MNG2 (for ZBDDs, it has prev=biddyVariableTable.num) */
5793  top = BiddyV(r); /* not always the best start, but it is correct */
5794  while (biddyVariableTable2.table[top].prev != biddyVariableTable2.num) {
5795  top = biddyVariableTable2.table[top].prev;
5796  }
5797  /* determine topmost variable of f in MNG2 considered by BiddyConvertDirect (by checking the topmost variable of f in MNG1) */
5798  topname = Biddy_Managed_GetTopVariableName(MNG1,f);
5799  prevvar = Biddy_Managed_GetVariable(MNG2,topname);
5800  /* add all missing variables to f in MNG2 which are missing in MNG2 */
5801  while (prevvar != top) {
5802  prevvar = biddyVariableTable2.table[prevvar].prev;
5803  r = BiddyManagedTaggedFoaNode(MNG2,prevvar,r,r,prevvar,TRUE);
5804  BiddyProlongOne(r,biddySystemAge2); /* FoaNode returns an obsolete node! */
5805  }
5806  }
5807 
5808  else if (((biddyManagerType1 == BIDDYTYPEOBDDC) || (biddyManagerType1 == BIDDYTYPEOBDD))
5809  &&
5810  ((biddyManagerType2 == BIDDYTYPETZBDDC) || (biddyManagerType2 == BIDDYTYPETZBDD)))
5811  {
5812  /* RESULT IS ALREADY CORRECT */
5813  }
5814 
5815  else if (((biddyManagerType1 == BIDDYTYPEZBDDC) || (biddyManagerType1 == BIDDYTYPEZBDD))
5816  &&
5817  ((biddyManagerType2 == BIDDYTYPEZBDDC) || (biddyManagerType2 == BIDDYTYPEZBDD)))
5818  {
5819  /* IF MNG1 AND MNG2 CONTAINS EXACTLY THE SAME VARIABLES THEN THE RESULT IS ALREADY CORRECT */
5820  /* TO DO: */
5821  /* extend for the case where MNG2 contains extra variables and */
5822  /* the same variable may have different indices in MNG1 and MNG2 */
5823  }
5824 
5825  else if (((biddyManagerType1 == BIDDYTYPEZBDDC) || (biddyManagerType1 == BIDDYTYPEZBDD))
5826  &&
5827  ((biddyManagerType2 == BIDDYTYPEOBDDC) || (biddyManagerType2 == BIDDYTYPEOBDD)))
5828  {
5829  /* BiddyConvertDirect does not create the topmost variables which are not present in ZBDD */
5830  /* MNG2 was empty on the beginning and the domain have been correctly copied */
5831  /* thus, we can assume that MNG1 and MNG2 have the same ordering */
5832  /* NOTE: this implementation allows that MNG2 contains extra variables */
5833  /* NOTE: this implementation allows that the same variable has different indices in MNG1 and MNG2 */
5834 
5835  /* determine the topmost variable in the domain of MNG1 (for ZBDDs, it has prev=biddyVariableTable.num) */
5836  top = BiddyV(f);
5837  while (biddyVariableTable1.table[top].prev != biddyVariableTable1.num) {
5838  top = biddyVariableTable1.table[top].prev;
5839  }
5840  /* determine topmost variable of f in MNG1 considered by BiddyConvertDirect (by checking the topmost variable of f in MNG1) */
5841  prevvar = BiddyV(f);
5842  /* add all variables to f in MNG2 which are missing in MNG1 */
5843  while (prevvar != top) {
5844  prevvar = biddyVariableTable1.table[prevvar].prev;
5845  topname = Biddy_Managed_GetVariableName(MNG1,prevvar);
5846  v2 = Biddy_Managed_GetVariable(MNG2,topname);
5847  r = BiddyManagedTaggedFoaNode(MNG2,v2,r,biddyZero2,v2,TRUE);
5848  BiddyProlongOne(r,biddySystemAge2); /* FoaNode returns an obsolete node! */
5849  }
5850  }
5851 
5852  else if (((biddyManagerType1 == BIDDYTYPEZBDDC) || (biddyManagerType1 == BIDDYTYPEZBDD))
5853  &&
5854  ((biddyManagerType2 == BIDDYTYPETZBDDC) || (biddyManagerType2 == BIDDYTYPETZBDD)))
5855  {
5856  /* BiddyConvertDirect does not create the topmost variables which are not present in ZBDD */
5857  /* MNG2 was empty on the beginning and the domain have been correctly copied */
5858  /* thus, we can assume that MNG1 and MNG2 have the same ordering */
5859  /* this implementation is correct only if MNG1 and MNG2 contain exactly the same variables */
5860  /* TO DO: */
5861  /* extend for the case where MNG2 contains extra variables and */
5862  /* the same variable may have different indices in MNG1 and MNG2 */
5863 
5864  /* determine the topmost variable in the domain of MNG1 (for ZBDDs, it has prev=biddyVariableTable.num) */
5865  top = BiddyV(f);
5866  while (biddyVariableTable1.table[top].prev != biddyVariableTable1.num) {
5867  top = biddyVariableTable1.table[top].prev;
5868  }
5869  /* determine topmost variable of f in MNG1 considered by BiddyConvertDirect (by checking the topmost variable of f in MNG1) */
5870  prevvar = BiddyV(f);
5871  /* add all variables to f in MNG2 which are missing in MNG1 */
5872  if (prevvar != top) {
5873  topname = Biddy_Managed_GetVariableName(MNG1,top);
5874  v2 = Biddy_Managed_GetVariable(MNG2,topname);
5875  Biddy_SetTag(r,v2);
5876  }
5877  }
5878 
5879  else if (((biddyManagerType1 == BIDDYTYPETZBDDC) || (biddyManagerType1 == BIDDYTYPETZBDD))
5880  &&
5881  ((biddyManagerType2 == BIDDYTYPEOBDDC) || (biddyManagerType2 == BIDDYTYPEOBDD)))
5882  {
5883  /* RESULT IS ALREADY CORRECT */
5884  }
5885 
5886  else if (((biddyManagerType1 == BIDDYTYPETZBDDC) || (biddyManagerType1 == BIDDYTYPETZBDD))
5887  &&
5888  ((biddyManagerType2 == BIDDYTYPEZBDDC) || (biddyManagerType2 == BIDDYTYPEZBDD)))
5889  {
5890  /* BiddyConvertDirect does not create the topmost variables which are not present in TZBDD */
5891  /* MNG2 was empty on the beginning and the domain have been correctly copied */
5892  /* thus, we can assume that MNG1 and MNG2 have the same ordering */
5893  /* NOTE: this implementation allows that MNG2 contains extra variables */
5894  /* NOTE: this implementation allows that the same variable has different indices in MNG1 and MNG2 */
5895 
5896  /* determine the topmost variable in the domain of MNG2 (for ZBDDs, it has prev=biddyVariableTable.num) */
5897  top = BiddyV(r); /* not always the best start, but it is correct */
5898  while (biddyVariableTable2.table[top].prev != biddyVariableTable2.num) {
5899  top = biddyVariableTable2.table[top].prev;
5900  }
5901  /* determine topmost variable of f in MNG2 considered by BiddyConvertDirect (by checking the topmost tag of f in MNG1) */
5902  topname = Biddy_Managed_GetVariableName(MNG1,Biddy_GetTag(f));
5903  prevvar = Biddy_Managed_GetVariable(MNG2,topname);
5904  /* add all missing variables to f in MNG2 which are missing in MNG2 */
5905  while (prevvar != top) {
5906  prevvar = biddyVariableTable2.table[prevvar].prev;
5907  r = BiddyManagedTaggedFoaNode(MNG2,prevvar,r,r,prevvar,TRUE);
5908  BiddyProlongOne(r,biddySystemAge2); /* FoaNode returns an obsolete node! */
5909  }
5910  }
5911 
5912  else if (((biddyManagerType1 == BIDDYTYPETZBDDC) || (biddyManagerType1 == BIDDYTYPETZBDD))
5913  &&
5914  ((biddyManagerType2 == BIDDYTYPETZBDDC) || (biddyManagerType2 == BIDDYTYPETZBDD)))
5915  {
5916  /* IF MNG1 AND MNG2 CONTAINS EXACTLY THE SAME VARIABLES THEN THE RESULT IS ALREADY CORRECT */
5917  /* TO DO: */
5918  /* extend for the case where MNG2 contains extra variables and */
5919  /* the same variable may have different indices in MNG1 and MNG2 */
5920  }
5921 
5922  else {
5923  fprintf(stderr,"Biddy_Managed_Copy: Unsupported BDD type combination for MNG1 or MNG2!\n");
5924  assert ( FALSE );
5925  }
5926 
5927  }
5928 
5929  } else {
5930 
5931  if ((biddyManagerType1 == BIDDYTYPEOBDDC) || (biddyManagerType1 == BIDDYTYPEOBDD)) {
5932  r = BiddyCopyOBDD(MNG1,MNG2,f);
5933  BiddyProlongOne(r,biddySystemAge2); /* not always refreshed by BiddyCopy */
5934  }
5935  else if ((biddyManagerType1 == BIDDYTYPEZBDDC) || (biddyManagerType1 == BIDDYTYPEZBDD)) {
5936  r = BiddyCopyZBDD(MNG1,MNG2,f);
5937  BiddyProlongOne(r,biddySystemAge2); /* not always refreshed by BiddyCopy */
5938  }
5939  else if ((biddyManagerType1 == BIDDYTYPETZBDDC) || (biddyManagerType1 == BIDDYTYPETZBDD)) {
5940  r = BiddyCopyTZBDD(MNG1,MNG2,f);
5941  BiddyProlongOne(r,biddySystemAge2); /* not always refreshed by BiddyCopy */
5942  }
5943  else {
5944  fprintf(stderr,"Biddy_Managed_Copy: Unsupported BDD type for MNG1!\n");
5945  }
5946 
5947  }
5948 
5949  return r;
5950 }
5951 
5952 #ifdef __cplusplus
5953 }
5954 #endif
5955 
5956 /***************************************************************************/
5970 #ifdef __cplusplus
5971 extern "C" {
5972 #endif
5973 
5974 void
5976 {
5977  unsigned int i;
5978  Biddy_Boolean OK;
5979  Biddy_Edge src,dst;
5980 
5981  if (!x) return;
5982 
5983  if (!MNG1) MNG1 = biddyAnonymousManager;
5984 
5985  /* DEBUGGING */
5986  /*
5987  printf("Biddy_Managed_CopyFormula STARTED: %s\n",x);
5988  */
5989 
5990  OK = Biddy_Managed_FindFormula(MNG1,x,&i,&src);
5991 
5992  if (OK) {
5993  OK = Biddy_Managed_FindFormula(MNG2,x,&i,&dst);
5994  if (OK) {
5995  printf("WARNING (Biddy_Managed_CopyFormula): formula overwritten!\n");
5996  }
5997  if (src == biddyZero1) {
5998  dst = biddyZero2;
5999  } else {
6000  dst = Biddy_Managed_Copy(MNG1,MNG2,src);
6001  }
6002  Biddy_Managed_AddFormula(MNG2,x,dst,-1);
6003  }
6004 
6005  /* DEBUGGING */
6006  /*
6007  printf("Biddy_Managed_CopyFormula FINISHED: %s\n",x);
6008  */
6009 }
6010 
6011 #ifdef __cplusplus
6012 }
6013 #endif
6014 
6039 #ifdef __cplusplus
6040 extern "C" {
6041 #endif
6042 
6043 Biddy_Edge
6044 Biddy_Managed_ConstructBDD(Biddy_Manager MNG, int numV, Biddy_String varlist, int numN,
6045  Biddy_String nodelist)
6046 {
6047  BiddyVariableOrder *tableV;
6048  BiddyNodeList *tableN;
6049  Biddy_Boolean usetags;
6050  Biddy_Edge r;
6051  Biddy_String word;
6052  int i; /* must be signed because of used for loop */
6053 
6054  if (!MNG) MNG = biddyAnonymousManager;
6055 
6056  /* DEBUGGING */
6057  /*
6058  printf("Biddy_ConstructBDD\n");
6059  printf("%d variables\n",numV);
6060  printf("%s\n",varlist);
6061  printf("%d nodes\n",numN);
6062  printf("%s\n",nodelist);
6063  */
6064 
6065  tableV = (BiddyVariableOrder *) malloc(numV * sizeof(BiddyVariableOrder));
6066  if (!tableV) return biddyNull;
6067  tableN = (BiddyNodeList *) malloc(numN * sizeof(BiddyNodeList));
6068  if (!tableN) return biddyNull;
6069 
6070  /* VARIABLES */
6071  if (numV) {
6072  word = strtok(varlist," "); /* parsing list of variables */
6073  tableV[0].name = strdup(word);
6074  tableV[0].order = 0;
6075  for (i=1; i<numV; i++) {
6076  word = strtok(NULL," ");
6077  tableV[i].name = strdup(word);
6078  tableV[i].order = 0;
6079  }
6080  }
6081 
6082  /* DEBUGGING */
6083  /*
6084  printf("VARIABLES %d:\n",numV);
6085  for (i=0; i<numV; i++) {
6086  printf("%s\n",tableV[i].name);
6087  }
6088  */
6089 
6090  usetags = FALSE;
6091  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD))
6092  {
6093  for (i=0; i<numV; i++) {
6094  Biddy_Managed_AddVariableByName(MNG,tableV[i].name);
6095  }
6096  }
6097  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD))
6098  {
6099  for (i=numV-1; i>=0; i--) {
6100  Biddy_Managed_AddVariableByName(MNG,tableV[i].name);
6101  }
6102  }
6103  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
6104  {
6105  usetags = TRUE;
6106  for (i=numV-1; i>=0; i--) {
6107  Biddy_Managed_AddVariableByName(MNG,tableV[i].name);
6108  }
6109  }
6110  else {
6111  fprintf(stderr,"Biddy_ConstructBDD: Unknown BDD type!\n");
6112  return biddyNull;
6113  }
6114 
6115  /* NODES AND EDGES */
6116  word = strtok(nodelist," "); /* ignored */
6117  for (i=0; i<numN; i++) {
6118  word = strtok(NULL," "); /* node id */
6119  tableN[i].id = atoi(word);
6120  word = strtok(NULL," "); /* node name */
6121  tableN[i].name = strdup(word);
6122  word = strtok(NULL," "); /* node type */
6123  tableN[i].type = atoi(word);
6124  word = strtok(NULL," "); /* node left successor */
6125  tableN[i].l = atoi(word);
6126  if (usetags) {
6127  word = strtok(NULL," "); /* left successor's tag */
6128  if (tableN[i].l != -1) {
6129  tableN[i].ltag = Biddy_Managed_GetVariable(MNG,word);
6130  } else {
6131  tableN[i].ltag = 0;
6132  }
6133  } else {
6134  tableN[i].ltag = 0;
6135  }
6136  word = strtok(NULL," "); /* node right successor */
6137  tableN[i].r = atoi(word);
6138  if (usetags) {
6139  word = strtok(NULL," "); /* right successor's tag */
6140  if (tableN[i].r != -1) {
6141  tableN[i].rtag = Biddy_Managed_GetVariable(MNG,word);
6142  } else {
6143  tableN[i].rtag = 0;
6144  }
6145  } else {
6146  tableN[i].rtag = 0;
6147  }
6148  }
6149 
6150  r = BiddyConstructBDD(MNG,numN,tableN);
6151 
6152  for (i=0; i<numV; ++i) {
6153  free(tableV[i].name);
6154  }
6155  for (i=0; i<numN; ++i) {
6156  free(tableN[i].name);
6157  }
6158 
6159  free(tableV);
6160  free(tableN);
6161 
6162  return r;
6163 }
6164 
6165 #ifdef __cplusplus
6166 }
6167 #endif
6168 
6169 /*----------------------------------------------------------------------------*/
6170 /* Definition of internal functions */
6171 /*----------------------------------------------------------------------------*/
6172 
6173 /***************************************************************************/
6183 void
6184 BiddyIncSystemAge(Biddy_Manager MNG)
6185 {
6186  if (++biddySystemAge <= 0) {
6187  biddySystemAge--;
6188  BiddyCompactSystemAge(MNG);
6189  biddySystemAge++;
6190  }
6191 }
6192 
6193 /***************************************************************************/
6202 void
6203 BiddyDecSystemAge(Biddy_Manager MNG)
6204 {
6205  if (--biddySystemAge < 1) {
6206  printf("ERROR (BiddyDecSystemAge): biddySystemAge is wrong");
6207  exit(1);
6208  }
6209 }
6210 
6211 /***************************************************************************/
6221 void
6222 BiddyCompactSystemAge(Biddy_Manager MNG)
6223 {
6224  Biddy_Variable v;
6225  BiddyNode *sup;
6226  unsigned int i;
6227 
6228  /* DEBUGGING */
6229 
6230  printf("NOTE FROM BIDDY: BiddyCompactSystemAge\n");
6231 
6232 
6233  /* CHANGE expiry VALUE OF ALL NODES */
6234  for (v=1; v<biddyVariableTable.num; v++) {
6235  sup = biddyVariableTable.table[v].firstNode;
6236  if (sup->expiry) {
6237  if (sup->expiry < biddySystemAge) {
6238  sup->expiry = 1;
6239  } else {
6240  sup->expiry = 2+sup->expiry-biddySystemAge;
6241  }
6242  }
6243  sup = (BiddyNode *) sup->list;
6244  }
6245 
6246  /* CHANGE expiry VALUE OF ALL FORMULAE */
6247  for (i = 2; i < biddyFormulaTable.size; i++) {
6248  if (biddyFormulaTable.table[i].expiry) {
6249  if (biddyFormulaTable.table[i].expiry) {
6250  biddyFormulaTable.table[i].expiry = biddyFormulaTable.table[i].expiry;
6251  } else {
6252  biddyFormulaTable.table[i].expiry = 2+biddyFormulaTable.table[i].expiry-biddySystemAge;
6253  }
6254  }
6255  }
6256 
6257  biddySystemAge = 2;
6258 }
6259 
6260 /***************************************************************************/
6273 void
6274 BiddyProlongRecursively(Biddy_Manager MNG, Biddy_Edge f, unsigned int c,
6275  Biddy_Variable target)
6276 {
6277  if ((target != 0) && !BiddyIsSmaller(BiddyV(f),target)) return;
6278  if (((BiddyNode *) BiddyP(f))->expiry &&
6279  (((BiddyNode *) BiddyP(f))->expiry < biddySystemAge))
6280  {
6281  BiddyProlongOne(f,c);
6282  if (biddyVariableTable.table[BiddyV(f)].numobsolete != 0) {
6283  (biddyVariableTable.table[BiddyV(f)].numobsolete)--;
6284  }
6285  BiddyProlongRecursively(MNG,BiddyE(f),c,target);
6286  BiddyProlongRecursively(MNG,BiddyT(f),c,target);
6287  }
6288 }
6289 
6290 /*******************************************************************************
6291 \brief Function BiddyCreateLocalInfo creates local info table for the given
6292  function.
6293 
6294 ### Description
6295  Only one local info table may exists! It is not allowed to add new BDD
6296  nodes if local info table exists. It is not allowed to start GC if local
6297  info table exists. The last element and only the last element in the table
6298  has back = NULL. Function returns number of noticeable variables.
6299  For OBDD, noticeable variables are all variables existing in the graph.
6300  For ZBDD, all variables are noticeable variables.
6301  For TZBDD, noticeable variables are all variables equal or below a top
6302  variable (considering the tag).
6303 ### Side effects
6304  Local info for terminal node is not created!
6305 ### More info
6306 *******************************************************************************/
6307 
6309 BiddyCreateLocalInfo(Biddy_Manager MNG, Biddy_Edge f)
6310 {
6311  unsigned int num;
6312  BiddyLocalInfo *c;
6313  Biddy_Variable i,var;
6314 
6315  if (Biddy_IsNull(f)) return 0;
6316  if (Biddy_IsTerminal(f)) return 0;
6317 
6318  assert( !Biddy_Managed_IsSelected(MNG,f) );
6319 
6320  num = 0; /* TERMINAL NODE IS NOT COUNTED HERE */
6321 
6322  for (i=1;i<biddyVariableTable.num;i++) {
6323  biddyVariableTable.table[i].selected = FALSE;
6324  }
6325 
6326  /* DETERMINE NUMBER OF NODES */
6327  Biddy_Managed_SelectNode(MNG,biddyTerminal);
6328  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
6329  BiddyNodeVarNumber(MNG,f,&num); /* NOW, ALL NODES ARE SELECTED, NOTICEABLE VARS COUNTED */
6330  }
6331  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
6332  BiddyNodeNumber(MNG,f,&num); /* NOW, ALL NODES ARE SELECTED, NOTICEABLE VARS DOES NOT NEED TO BE COUNTED */
6333  }
6334  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
6335  BiddyNodeNumber(MNG,f,&num); /* NOW, ALL NODES ARE SELECTED, NOTICEABLE VARS DOES NOT NEED TO BE COUNTED */
6336  }
6337  else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
6338  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
6339  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6340  {
6341  fprintf(stderr,"BiddyCreateLocalInfo: this BDD type is not supported, yet!\n");
6342  return 0;
6343  }
6344  else {
6345  fprintf(stderr,"BiddyCreateLocalInfo: Unsupported BDD type!\n");
6346  return 0;
6347  }
6348 
6349  Biddy_Managed_DeselectNode(MNG,biddyTerminal); /* REQUIRED FOR createLocalInfo */
6350 
6351  /* DETERMINE NUMBER OF NOTICEABLE VARIABLES */
6352  var = 0;
6353  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
6354  for (i=1;i<biddyVariableTable.num;i++) {
6355  if (biddyVariableTable.table[i].selected == TRUE) {
6356  var++;
6357  biddyVariableTable.table[i].selected = FALSE; /* deselect variable */
6358  }
6359  }
6360  }
6361  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
6362  var = biddyVariableTable.num-1;
6363  }
6364  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
6365  for (i=1;i<biddyVariableTable.num;i++) {
6366  if ((Biddy_GetTag(f) == i) || BiddyIsSmaller(Biddy_GetTag(f),i)) {
6367  var++;
6368  }
6369  }
6370  }
6371  else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
6372  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
6373  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6374  {
6375  fprintf(stderr,"BiddyCreateLocalInfo: this BDD type is not supported, yet!\n");
6376  return 0;
6377  }
6378  else {
6379  fprintf(stderr,"BiddyCreateLocalInfo: Unsupported BDD type!\n");
6380  return 0;
6381  }
6382 
6383  /* calloc is used here because we want initialization to zero */
6384  if (!(biddyLocalInfo = (BiddyLocalInfo *)
6385  calloc((num+1),sizeof(BiddyLocalInfo)))) {
6386  fprintf(stderr,"BiddyCreateLocalInfo: Out of memoy!\n");
6387  exit(1);
6388  }
6389  c = createLocalInfo(MNG,f,biddyLocalInfo);
6390  if (!c) {
6391  fprintf(stderr,"ERROR: createLocalInfo returns NULL\n");
6392  exit(1);
6393  }
6394  biddyLocalInfo[num].back = NULL;
6395 
6396  return var;
6397 }
6398 
6399 /*******************************************************************************
6400 \brief Function BiddyDeleteLocalInfo deletes local info table for the given
6401  function.
6402 
6403 ### Description
6404  Only one local info table may exists! After deleting local info table,
6405  Biddy is ready for any operation.
6406 ### Side effects
6407  All nodes except terminal node must be selected.
6408  Local info for terminal node should not be created!
6409 ### More info
6410 *******************************************************************************/
6411 
6412 void
6413 BiddyDeleteLocalInfo(Biddy_Manager MNG, Biddy_Edge f)
6414 {
6415  if (Biddy_IsNull(f)) return;
6416  if (Biddy_IsTerminal(f)) return;
6417  if (!Biddy_Managed_IsSelected(MNG,f)) {
6418  fprintf(stderr,"ERROR: BiddyDeleteLocalInfo got unselected node\n");
6419  exit(1);
6420  }
6421  deleteLocalInfo(MNG,f); /* this will deselect all nodes */
6422  free(biddyLocalInfo);
6423  biddyLocalInfo = NULL;
6424 }
6425 
6426 /*******************************************************************************
6427 \brief Function BiddyGetSeqByNode returns seq number of a given node.
6428 
6429 ### Description
6430 ### Side effects
6431  Local info must be created before using this function.
6432  This should not be called for terminal node because terminal node does
6433  not have local info!
6434 ### More info
6435 *******************************************************************************/
6436 
6437 unsigned int
6438 BiddyGetSeqByNode(Biddy_Edge root, Biddy_Edge f)
6439 {
6440  unsigned int n;
6441 
6442  n = (unsigned int)
6443  (((uintptr_t)(((BiddyNode *)BiddyP(f))->list)) -
6444  ((uintptr_t)(((BiddyNode *)BiddyP(root))->list))
6445  ) / sizeof(BiddyLocalInfo);
6446 
6447  return n;
6448 }
6449 
6450 /*******************************************************************************
6451 \brief Function BiddyGetNodeBySeq returns node with a given seq number.
6452 
6453 ### Description
6454 ### Side effects
6455  Local info must be created before using this function.
6456  Function fails if node with a given seq number does not exist.
6457 ### More info
6458 *******************************************************************************/
6459 
6460 Biddy_Edge
6461 BiddyGetNodeBySeq(Biddy_Edge root, unsigned int n)
6462 {
6463  return (Biddy_Edge)(((BiddyLocalInfo *)
6464  (((BiddyNode *)BiddyP(root))->list))[n].back);
6465 }
6466 
6467 /*******************************************************************************
6468 \brief Function BiddySetEnumerator is used in enumerateNodes.
6469 
6470 ### Description
6471 ### Side effects
6472  Local info must be created before using this function.
6473  This should not be called for terminal node because terminal node does
6474  not have local info!
6475 ### More info
6476 *******************************************************************************/
6477 
6478 void
6479 BiddySetEnumerator(Biddy_Edge f, unsigned int n)
6480 {
6481  ((BiddyLocalInfo *)(((BiddyNode *)BiddyP(f))->list))->data.enumerator = n;
6482 }
6483 
6484 /*******************************************************************************
6485 \brief Function BiddyGetEnumerator is used in enumerateNodes.
6486 
6487 ### Description
6488 ### Side effects
6489  Local info must be created before using this function.
6490  This should not be called for terminal node because terminal node does
6491  not have local info!
6492 ### More info
6493 *******************************************************************************/
6494 
6495 unsigned int
6496 BiddyGetEnumerator(Biddy_Edge f)
6497 {
6498  return ((BiddyLocalInfo *)(((BiddyNode *)BiddyP(f))->list))->data.enumerator;
6499 }
6500 
6501 /*******************************************************************************
6502 \brief Function BiddySetCopy is used in BiddyCopy.
6503 
6504 ### Description
6505 ### Side effects
6506  Local info must be created before using this function.
6507  This should not be called for terminal node because terminal node does
6508  not have local info!
6509 ### More info
6510 *******************************************************************************/
6511 
6512 void
6513 BiddySetCopy(Biddy_Edge f, BiddyNode *n)
6514 {
6515  ((BiddyLocalInfo *)(((BiddyNode *)BiddyP(f))->list))->data.copy = n;
6516 }
6517 
6518 /*******************************************************************************
6519 \brief Function BiddyGetCopy is used in BiddyCopy.
6520 
6521 ### Description
6522 ### Side effects
6523  Local info must be created before using this function.
6524  This should not be called for terminal node because terminal node does
6525  not have local info!
6526 ### More info
6527 *******************************************************************************/
6528 
6529 BiddyNode *
6530 BiddyGetCopy(Biddy_Edge f)
6531 {
6532  return ((BiddyLocalInfo *)(((BiddyNode *)BiddyP(f))->list))->data.copy;
6533 }
6534 
6535 /*******************************************************************************
6536 \brief Function BiddySetPath1Count is used in pathCount().
6537 
6538 ### Description
6539 ### Side effects
6540  Local info must be created before using this function.
6541  This should not be called for terminal node because terminal node does
6542  not have local info!
6543 ### More info
6544 *******************************************************************************/
6545 
6546 void
6547 BiddySetPath1Count(Biddy_Edge f, unsigned long long int value)
6548 {
6549  ((BiddyLocalInfo *)(((BiddyNode *) BiddyP(f))->list))->data.path1Count = value;
6550 }
6551 
6552 /*******************************************************************************
6553 \brief Function BiddyGetPath1Count is used in pathCount().
6554 
6555 ### Description
6556 ### Side effects
6557  Local info must be created before using this function.
6558  This should not be called for terminal node because terminal node does
6559  not have local info!
6560 ### More info
6561 *******************************************************************************/
6562 
6563 unsigned long long int
6564 BiddyGetPath1Count(Biddy_Edge f)
6565 {
6566  return ((BiddyLocalInfo *)(((BiddyNode *) BiddyP(f))->list))->data.path1Count;
6567 }
6568 
6569 /*******************************************************************************
6570 \brief Function BiddySetPath0Count is used in pathCount().
6571 
6572 ### Description
6573 ### Side effects
6574  Local info must be created before using this function.
6575  This should not be called for terminal node because terminal node does
6576  not have local info!
6577 ### More info
6578 *******************************************************************************/
6579 
6580 void
6581 BiddySetPath0Count(Biddy_Edge f, unsigned long long int value)
6582 {
6583  ((BiddyLocalInfo *)(((BiddyNode *) BiddyP(f))->list))->datax.path0Count = value;
6584 }
6585 
6586 /*******************************************************************************
6587 \brief Function BiddyGetPath0Count is used in pathCount().
6588 
6589 ### Description
6590 ### Side effects
6591  Local info must be created before using this function.
6592  This should not be called for terminal node because terminal node does
6593  not have local info!
6594 ### More info
6595 *******************************************************************************/
6596 
6597 unsigned long long int
6598 BiddyGetPath0Count(Biddy_Edge f)
6599 {
6600  return ((BiddyLocalInfo *)(((BiddyNode *) BiddyP(f))->list))->datax.path0Count;
6601 }
6602 
6603 /*******************************************************************************
6604 \brief Function BiddySetPath1ProbabilitySum is used in pathProbabilitySum().
6605 
6606 ### Description
6607 ### Side effects
6608  Local info must be created before using this function.
6609  This should not be called for terminal node because terminal node does
6610  not have local info!
6611 ### More info
6612 *******************************************************************************/
6613 
6614 void
6615 BiddySetPath1ProbabilitySum(Biddy_Edge f, double value)
6616 {
6617  ((BiddyLocalInfo *)(((BiddyNode *) BiddyP(f))->list))->data.path1Probability = value;
6618 }
6619 
6620 /*******************************************************************************
6621 \brief Function BiddyGetPath1ProbabilitySum is used in pathProbabilitySum().
6622 
6623 ### Description
6624 ### Side effects
6625  Local info must be created before using this function.
6626  This should not be called for terminal node because terminal node does
6627  not have local info!
6628 ### More info
6629 *******************************************************************************/
6630 
6631 double
6632 BiddyGetPath1ProbabilitySum(Biddy_Edge f)
6633 {
6634  return ((BiddyLocalInfo *)(((BiddyNode *) BiddyP(f))->list))->data.path1Probability;
6635 }
6636 
6637 /*******************************************************************************
6638 \brief Function BiddySetPath0ProbabilitySum is used in pathProbabilitySum().
6639 
6640 ### Description
6641 ### Side effects
6642  Local info must be created before using this function.
6643  This should not be called for terminal node because terminal node does
6644  not have local info!
6645 ### More info
6646 *******************************************************************************/
6647 
6648 void
6649 BiddySetPath0ProbabilitySum(Biddy_Edge f, double value)
6650 {
6651  ((BiddyLocalInfo *)(((BiddyNode *) BiddyP(f))->list))->datax.path0Probability = value;
6652 }
6653 
6654 /*******************************************************************************
6655 \brief Function BiddyGetPath0ProbabilitySum is used in pathProbabilitySum().
6656 
6657 ### Description
6658 ### Side effects
6659  Local info must be created before using this function.
6660  This should not be called for terminal node because terminal node does
6661  not have local info!
6662 ### More info
6663 *******************************************************************************/
6664 
6665 double
6666 BiddyGetPath0ProbabilitySum(Biddy_Edge f)
6667 {
6668  return ((BiddyLocalInfo *)(((BiddyNode *) BiddyP(f))->list))->datax.path0Probability;
6669 }
6670 
6671 /*******************************************************************************
6672 \brief Function BiddySetLeftmost is used in pathCount().
6673 
6674 ### Description
6675 ### Side effects
6676  Local info must be created before using this function.
6677  This should not be called for terminal node because terminal node does
6678  not have local info!
6679 ### More info
6680 *******************************************************************************/
6681 
6682 void
6683 BiddySetLeftmost(Biddy_Edge f, Biddy_Boolean value)
6684 {
6685  ((BiddyLocalInfo *)(((BiddyNode *) BiddyP(f))->list))->datax.leftmost = value;
6686 }
6687 
6688 /*******************************************************************************
6689 \brief Function BiddyGetLeftmost is used in pathCount().
6690 
6691 ### Description
6692 ### Side effects
6693  Local info must be created before using this function.
6694  This should not be called for terminal node because terminal node does
6695  not have local info!
6696 ### More info
6697 *******************************************************************************/
6698 
6700 BiddyGetLeftmost(Biddy_Edge f)
6701 {
6702  return ((BiddyLocalInfo *)(((BiddyNode *) BiddyP(f))->list))->datax.leftmost;
6703 }
6704 
6705 /*******************************************************************************
6706 \brief Function BiddySetMintermCount is used in mintermCount().
6707 
6708 ### Description
6709 ### Side effects
6710  Local info must be created before using this function.
6711  We are using GNU Multiple Precision Arithmetic Library (GMP).
6712  This should not be called for terminal node because terminal node does
6713  not have local info!
6714 ### More info
6715 *******************************************************************************/
6716 
6717 void
6718 BiddySetMintermCount(Biddy_Edge f, mpz_t value)
6719 {
6720  mpz_init(((BiddyLocalInfo *)
6721  (((BiddyNode *) BiddyP(f))->list))->data.mintermCount);
6722  mpz_set(((BiddyLocalInfo *)
6723  (((BiddyNode *) BiddyP(f))->list))->data.mintermCount,value);
6724 }
6725 
6726 /*******************************************************************************
6727 \brief Function BiddyGetMintermCount is used in mintermCount().
6728 
6729 ### Description
6730 ### Side effects
6731  Local info must be created before using this function.
6732  We are using GNU Multiple Precision Arithmetic Library (GMP).
6733  This should not be called for terminal node because terminal node does
6734  not have local info!
6735 ### More info
6736 *******************************************************************************/
6737 
6738 void
6739 BiddyGetMintermCount(Biddy_Edge f, mpz_t result)
6740 {
6741  mpz_set(result,((BiddyLocalInfo *)
6742  (((BiddyNode *) BiddyP(f))->list))->data.mintermCount);
6743 }
6744 
6745 /*******************************************************************************
6746 \brief Function BiddySelectNP is used in nodePlainNumber().
6747 
6748 ### Description
6749 ### Side effects
6750  Local info must be created before using this function.
6751  This should not be called for terminal node because terminal node does
6752  not have local info!
6753 ### More info
6754 *******************************************************************************/
6755 
6756 void
6757 BiddySelectNP(Biddy_Edge f)
6758 {
6759  if (Biddy_GetMark(f)) {
6760  (((BiddyLocalInfo *)
6761  (((BiddyNode *) BiddyP(f))->list))->data.npSelected) |= (unsigned int) 2;
6762  } else {
6763  (((BiddyLocalInfo *)
6764  (((BiddyNode *) BiddyP(f))->list))->data.npSelected) |= (unsigned int) 1;
6765  }
6766 }
6767 
6768 /*******************************************************************************
6769 \brief Function BiddyIsSelectedNP is used in nodePlainNumber().
6770 
6771 ### Description
6772 ### Side effects
6773  Local info must be created before using this function.
6774  This should not be called for terminal node because terminal node does
6775  not have local info!
6776 ### More info
6777 *******************************************************************************/
6778 
6780 BiddyIsSelectedNP(Biddy_Edge f)
6781 {
6782  Biddy_Boolean r;
6783 
6784  if (Biddy_GetMark(f)) {
6785  r = ((((BiddyLocalInfo *)
6786  (((BiddyNode *) BiddyP(f))->list))->data.npSelected
6787  ) & (unsigned int) 2
6788  ) != 0;
6789  } else {
6790  r = ((((BiddyLocalInfo *)
6791  (((BiddyNode *) BiddyP(f))->list))->data.npSelected
6792  ) & (unsigned int) 1
6793  ) != 0;
6794  }
6795 
6796  return r;
6797 }
6798 
6799 /***************************************************************************/
6817 BiddyGlobalSifting(Biddy_Manager MNG, Biddy_Boolean converge)
6818 {
6819  unsigned int num,min,min2,vnum,vv,totalbest;
6820  unsigned int best1,best2;
6821  Biddy_Variable v,vmax,k,n,minvar,maxvar;
6822  Biddy_Boolean highfirst,stop,finish,active,goback;
6823  unsigned int varTable[BIDDYVARMAX];
6824  float treshold;
6825 
6826  /* DEBUGGING */
6827  /*
6828  printf("SIFTING START: numNodes=%u, systemAge=%u\n",Biddy_Managed_NodeTableNum(MNG),biddySystemAge);
6829  BiddySystemReport(MNG);
6830  */
6831 
6832  /* determine current number of nodes in the global system */
6833  num = Biddy_Managed_NodeTableNum(MNG);
6834 
6835  /* determine minvar (lowest == topmost) and maxvar (highest == bottommost) */
6836  minvar = Biddy_Managed_GetLowestVariable(MNG);
6837  maxvar = 0;
6838 
6839  /* DEBUGGING - CHECKING THE SOUNDNESS OF THE ACTIVE ORDERING */
6840  /*
6841  {
6842  Biddy_Variable k,minvarOrder,maxvarOrder;
6843  minvarOrder = maxvarOrder = Biddy_Managed_VariableTableNum(MNG);
6844  for (k=0; k<Biddy_Managed_VariableTableNum(MNG); k++) {
6845  if (GET_ORDER(biddyOrderingTable,minvar,k)) minvarOrder--;
6846  if (GET_ORDER(biddyOrderingTable,maxvar,k)) maxvarOrder--;
6847  }
6848  if (minvarOrder != 1) {
6849  fprintf(stdout,"ERROR (BiddyGlobalSifting): minvarOrder %u is wrong\n",minvarOrder);
6850  exit(1);
6851  }
6852  if (maxvarOrder != Biddy_Managed_VariableTableNum(MNG)) {
6853  fprintf(stdout,"ERROR (BiddyGlobalSifting): maxvarOrder %u is wrong\n",maxvarOrder);
6854  exit(1);
6855  }
6856  }
6857  */
6858 
6859  /* SIFTING ALGORITHM */
6860  /* EXAMINE EVERY VARIABLE ONCE! */
6861 
6862  /* WE ARE STARTING WITH A CURRENT NUMBER OF NODES */
6863  if (converge) {
6864  treshold = biddyNodeTable.convergesiftingtreshold;
6865  } else {
6866  treshold = biddyNodeTable.siftingtreshold;
6867  }
6868  min = num;
6869 
6870  totalbest = min+1;
6871  while (min < totalbest) {
6872  totalbest = min;
6873 
6874  /* INIT varTable */
6875  /* varTable is used in the following way: */
6876  /* varTable[i] == 1 iff variable has not been sifted, yet */
6877  /* varTable[i] == 2 iff variable has already been sifted */
6878 
6879  varTable[0] = 2; /* variable '1' is not swapped */
6880  for (k=1; k<biddyVariableTable.num; k++) {
6881  varTable[k] = 1;
6882  }
6883 
6884  /* CHOOSE THE VARIABLE THAT WILL BE SIFTED FIRST */
6885  /* 1. it has not been sifted, yet */
6886  /* 2. it has max number of nodes */
6887 
6888  finish = (varTable[minvar] == 2); /* maybe, we are sifting constant variable '1' */
6889  v = 0;
6890  if (!finish) {
6891  /* VARIANT 1 */
6892  /* choose a variable that has the max number of nodes */
6893  vmax = 1;
6894  vnum = biddyVariableTable.table[1].num;
6895  v = 2;
6896  while (v < biddyVariableTable.num) {
6897  if ((vv=biddyVariableTable.table[v].num) > vnum) {
6898  vmax = v;
6899  vnum = vv;
6900  }
6901  v++;
6902  }
6903  v = vmax;
6904  /* VARIANT 2 */
6905  /* simply choose the smallest (topmost) variable */
6906  /*
6907  v = minvar;
6908  */
6909  }
6910 
6911  while (!finish) {
6912  varTable[v] = 2;
6913 
6914  /* DETERMINE FIRST DIRECTION */
6915  if (v == minvar) { /* TOPMOST VARIABLE */
6916  stop = TRUE; /* skip first direction */
6917  highfirst = FALSE; /* swapWithHigher will be used in second direction */
6918  } else if (v == maxvar) { /* BOTTOMMOST VARIABLE */
6919  stop = TRUE; /* skip first direction */
6920  highfirst = TRUE; /* swapWithLower will be used in second direction */
6921  } else {
6922  stop = FALSE;
6923 
6924  /* VARIANT A: start with shorter direction, thus calculate v's global ordering */
6925 
6926  n = getGlobalOrdering(MNG,v);
6927  if (n > (1+biddyVariableTable.num)/2) highfirst = TRUE; else highfirst = FALSE;
6928 
6929 
6930  /* VARIANT B: start with highfirst = TRUE */
6931  /*
6932  highfirst = TRUE;
6933  */
6934  }
6935 
6936  /* PROFILING */
6937  /*
6938  {
6939  Biddy_Variable varOrder;
6940  varOrder = getGlobalOrdering(MNG,v);
6941  printf("SIFTING LOOP START WITH variable \"%s\" (v=%u): startOrder=%u, min=%u, numNodes=%u, systemAge=%u, ",
6942  Biddy_Managed_GetVariableName(MNG,v),v,varOrder,min,Biddy_Managed_NodeTableNum(MNG),biddySystemAge);
6943  if (highfirst) printf("HIGHFIRST\n"); else printf("LOWFIRST\n");
6944  }
6945  */
6946 
6947  /* DEBUGGING */
6948  /*
6949  for (k=0; k<Biddy_Managed_VariableTableNum(MNG); k++) {
6950  printf("[\"%s\"@%u]",biddyVariableTable.table[k].name,biddyVariableTable.table[k].num);
6951  }
6952  printf("\n");
6953  */
6954 
6955  /* DEBUGGING */
6956  /*
6957  printf("SIFTING: FIRST DIRECTION\n");
6958  */
6959 
6960  /* ONE DIRECTION */
6961  n = 0;
6962  best1 = 0;
6963  while (!stop && (highfirst ?
6964  (k=swapWithHigher(MNG,v,&active)) :
6965  (k=swapWithLower(MNG,v,&active))))
6966  {
6967 
6968  n++; /* number of steps performed*/
6969 
6970  /* DEBUGGING */
6971  /*
6972  printf("SIFTING: ");
6973  if (highfirst) {
6974  printf("%u swaped with higher %u",v,k);
6975  } else {
6976  printf("%u swaped with lower %u",v,k);
6977  }
6978  if (active) printf(" (ACTIVE)");
6979  printf("\n");
6980  */
6981 
6982  if (highfirst) {
6983  if (v == minvar) {
6984  minvar = k; /* update minvar */
6985  }
6986  if (k == maxvar) {
6987  maxvar = v; /* update maxvar */
6988  stop = TRUE;
6989  }
6990  } else {
6991  if (k == minvar) {
6992  minvar = v; /* update minvar */
6993  stop = TRUE;
6994  }
6995  if (v == maxvar) {
6996  maxvar = k; /* update maxvar */
6997  }
6998  }
6999 
7000  /* NUMBER OF NODES CAN CHANGE ONLY IF v AND k HAVE BEEN ACTIVELY SWAPPED */
7001  /* FOR OBDDs AND ZBDDs, ONLY NODES WITH (v == smaller(k,v)) CAN BE OBSOLETE */
7002  /* FOR TZBDs, ALL NODES CAN BE OBSOLETE ?? */
7003  if (active) {
7004 
7005  /* DETERMINE THE NUMBER OF USEFUL NODES */
7006  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
7007  /* Biddy_Managed_GC(MNG,0,0,FALSE,TRUE); */ /* try this if there are strange problems */
7008  Biddy_Managed_GC(MNG,
7009  BiddyIsSmaller(k,v)?v:k,
7010  BiddyIsSmaller(k,v)?k:v,
7011  FALSE,TRUE);
7012  num = biddyNodeTable.num;
7013  }
7014  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
7015  /* Biddy_Managed_GC(MNG,0,0,FALSE,TRUE); */ /* try this if there are strange problems */
7016  Biddy_Managed_GC(MNG,
7017  BiddyIsSmaller(k,v)?v:k,
7018  BiddyIsSmaller(k,v)?k:v,
7019  FALSE,TRUE);
7020  num = biddyNodeTable.num;
7021  }
7022  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
7023  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
7024  num = biddyNodeTable.num;
7025  }
7026  else {
7027  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
7028  num = biddyNodeTable.num;
7029  }
7030 
7031  /* DEBUGGING */
7032  /*
7033  printf("SIFTING: first direction, step=%u, min=%u, num=%u\n",n,min,num);
7034  */
7035 
7036  if (num < min) { /* first direction should use strict less */
7037  min = num;
7038  best1 = n;
7039  }
7040 
7041  if (num > (treshold * min)) {
7042  stop = TRUE;
7043  }
7044 
7045  /* THIS IS EXPERIMENTAL !!! */
7046  /* IN THE FIRST DIRECTION, PERFORM LIMIT NUMBER OF STEPS */
7047  /* THIS COULD RESULT IN SHORT TIME AND NOT VERY BAD SIZE */
7048  /*
7049  if (n >= 1) {
7050  stop = TRUE;
7051  }
7052  */
7053 
7054  }
7055  } /* while (!stop ...) */
7056 
7057  /* PROFILING */
7058  /*
7059  {
7060  Biddy_Variable varOrder;
7061  varOrder = getGlobalOrdering(MNG,v);
7062  printf("SIFTING BEFORE GO-BACK: variable: \"%s\" (v=%u), currentOrder=%u, min=%u, numNodes=%u\n",
7063  Biddy_Managed_GetVariableName(MNG,v),v,varOrder,min,Biddy_Managed_NodeTableNum(MNG));
7064  }
7065  */
7066 
7067  /* DEBUGGING */
7068  /*
7069  for (k=0; k<Biddy_Managed_VariableTableNum(MNG); k++) {
7070  printf("[\"%s\"@%u]",biddyVariableTable.table[k].name,biddyVariableTable.table[k].num);
7071  }
7072  printf("\n");
7073  */
7074 
7075  /* DEBUGGING */
7076  /*
7077  printf("SIFTING: GO-BACK!\n");
7078  */
7079 
7080  /* GO BACK */
7081  goback = (n > 0);
7082  if (goback) vmax = biddyVariableTable.table[v].next; /* save the initial position of v */
7083  while (n) {
7084  if (highfirst) {
7085  k = swapWithLower(MNG,v,&active);
7086 
7087  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
7088  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
7089  }
7090 
7091  if (v == maxvar) {
7092  maxvar = k;
7093  }
7094  if (k == minvar) {
7095  minvar = v;
7096  }
7097  } else {
7098  k = swapWithHigher(MNG,v,&active);
7099 
7100  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
7101  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
7102  }
7103 
7104  if (v == minvar) {
7105  minvar = k;
7106  }
7107  if (k == maxvar) {
7108  maxvar = v;
7109  }
7110  }
7111  n--;
7112  }
7113 
7114  /* PROFILING */
7115  /*
7116  {
7117  Biddy_Variable varOrder;
7118  varOrder = getGlobalOrdering(MNG,v);
7119  printf("SIFTING AFTER GO BACK: variable: \"%s\" (v=%u), currentOrder=%u, min=%u, numNodes=%u\n",
7120  Biddy_Managed_GetVariableName(MNG,v),v,varOrder,min,Biddy_Managed_NodeTableNum(MNG));
7121  }
7122  */
7123 
7124  /* IF GO-BACK WAS MOVING VARIABLE UP (highfirst == TRUE) */
7125  /* OBDD, ZBDD: ONLY OBSOLETE NODES WITH (var == v) EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
7126  /* TZBDD: OBSOLETE NODES WITH ANY var EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) ?? */
7127 
7128  /* IF GO-BACK WAS MOVING VARIABLE DOWN (highfirst == FALSE) */
7129  /* OBDD, ZBDD: OBSOLETE NODES WITH (vmax <= var < v) EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
7130  /* TZBDD: OBSOLETE NODES WITH ANY var EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) ?? */
7131 
7132  /* this garbage collection is required here to remove all obsolete nodes */
7133  /* next GC call may use parameter target and may not remove old obsolete nodes! */
7134  if (goback) {
7135 
7136  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
7137  /* Biddy_Managed_GC(MNG,0,0,FALSE,TRUE); */ /* try this if there are strange problems */
7138  if (highfirst) {
7139  Biddy_Managed_GC(MNG,k,v,FALSE,TRUE);
7140  } else {
7141  Biddy_Managed_GC(MNG,v,vmax,FALSE,TRUE);
7142  }
7143  }
7144  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
7145  /* Biddy_Managed_GC(MNG,0,0,FALSE,TRUE); */ /* try this if there are strange problems */
7146  if (highfirst) {
7147  Biddy_Managed_GC(MNG,k,v,FALSE,TRUE);
7148  } else {
7149  Biddy_Managed_GC(MNG,v,vmax,FALSE,TRUE);
7150  }
7151  }
7152  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
7153  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
7154  }
7155  else {
7156  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
7157  }
7158 
7159  }
7160 
7161  /* PROFILING */
7162  /*
7163  {
7164  Biddy_Variable varOrder;
7165  varOrder = getGlobalOrdering(MNG,v);
7166  printf("SIFTING AFTER FIRST DIRECTION: variable: \"%s\" (v=%u), currentOrder=%u, min=%u, numNodes=%u\n",
7167  Biddy_Managed_GetVariableName(MNG,v),v,varOrder,min,Biddy_Managed_NodeTableNum(MNG));
7168  }
7169  */
7170 
7171  /* DEBUGGING */
7172  /*
7173  for (k=0; k<Biddy_Managed_VariableTableNum(MNG); k++) {
7174  printf("[\"%s\"@%u]",biddyVariableTable.table[k].name,biddyVariableTable.table[k].num);
7175  }
7176  printf("\n");
7177  */
7178 
7179  /* DEBUGGING */
7180  /*
7181  printf("SIFTING: SECOND DIRECTION\n");
7182  */
7183 
7184  /* OPPOSITE DIRECTION */
7185 
7186  n = 0;
7187  best2 = 0;
7188  stop = FALSE;
7189  min2 = biddyNodeTable.num; /* recalculate node number after go-back */
7190 
7191  if (converge) {
7192 
7193  /* VARIANT C1: min from the first direction is not used within second direction */
7194  /* no code is needed in this variant */
7195 
7196  /* VARIANT C2: min from the first direction is used within second direction */
7197  /*
7198  min2 = min;
7199  */
7200 
7201  /* VARIANT C3: if there is min in the first direction do not check second direction */
7202  /*
7203  if (best1) {
7204  stop = TRUE;
7205  }
7206  */
7207 
7208  } else {
7209 
7210  /* VARIANT NC1: min from the first direction is not used within second direction */
7211  /* no code is needed in this variant */
7212 
7213  /* VARIANT NC2: min from the first direction is used within second direction */
7214  /*
7215  min2 = min;
7216  */
7217 
7218  /* VARIANT NC3: if there is min in the first direction do not check second direction */
7219  /* THIS SEEMS TO BE BAD FOR REGULAR SIFTING */
7220 
7221  }
7222 
7223  while (!stop && (highfirst ?
7224  (k=swapWithLower(MNG,v,&active)) :
7225  (k=swapWithHigher(MNG,v,&active))))
7226  {
7227 
7228  n++;
7229 
7230  /* DEBUGGING */
7231  /*
7232  printf("SIFTING: ");
7233  if (highfirst) {
7234  printf("%u swaped with lower %u",v,k);
7235  } else {
7236  printf("%u swaped with higher %u",v,k);
7237  }
7238  if (active) printf(" (ACTIVE)");
7239  printf("\n");
7240  */
7241 
7242  if (highfirst) {
7243  if (k == minvar) {
7244  minvar = v; /* update minvar */
7245  stop = TRUE;
7246  }
7247  if (v == maxvar) {
7248  maxvar = k; /* update maxvar */
7249  }
7250  } else {
7251  if (v == minvar) {
7252  minvar = k; /* update minvar */
7253  }
7254  if (k == maxvar) {
7255  maxvar = v; /* update maxvar */
7256  stop = TRUE;
7257  }
7258  }
7259 
7260  /* NUMBER OF NODES CAN CHANGE ONLY IF v AND k HAVE BEEN ACTIVELY SWAPPED */
7261  /* FOR OBDDs AND ZBDDs, ONLY NODES WITH (v == smaller(k,v)) CAN BE OBSOLETE */
7262  /* FOR TZBDs, ALL NODES CAN BE OBSOLETE ?? */
7263  if (active) {
7264 
7265  /* DETERMINE THE NUMBER OF USEFUL NODES */
7266  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
7267  /* Biddy_Managed_GC(MNG,0,0,FALSE,TRUE); */ /* try this if there are strange problems */
7268  Biddy_Managed_GC(MNG,
7269  BiddyIsSmaller(k,v)?v:k,
7270  BiddyIsSmaller(k,v)?k:v,
7271  FALSE,TRUE);
7272  num = biddyNodeTable.num;
7273  }
7274  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
7275  /* Biddy_Managed_GC(MNG,0,0,FALSE,TRUE); */ /* try this if there are strange problems */
7276  Biddy_Managed_GC(MNG,
7277  BiddyIsSmaller(k,v)?v:k,
7278  BiddyIsSmaller(k,v)?k:v,
7279  FALSE,TRUE);
7280  num = biddyNodeTable.num;
7281  }
7282  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
7283  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
7284  num = biddyNodeTable.num;
7285  }
7286  else {
7287  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
7288  num = biddyNodeTable.num;
7289  }
7290 
7291  /* DEBUGGING */
7292  /*
7293  printf("SIFTING: second direction, step=%u, min2=%u, num=%u\n",n,min2,num);
7294  */
7295 
7296  if (num <= min2) { /* second direction should use less or equal */
7297  min2 = num;
7298  best2 = n;
7299  }
7300 
7301  if (num > (treshold * min2)) {
7302  stop = TRUE;
7303  }
7304 
7305  }
7306  } /* while (!stop ...) */
7307 
7308  if (min2 <= min) { /* second direction should use less or equal */
7309  min = min2;
7310  } else {
7311  best2 = 0;
7312  }
7313 
7314  /* IF best2==0 THEN MINIMUM WAS REACHED IN THE FIRST WHILE */
7315  /* YOU HAVE TO GO-BACK AND THEN MAKE ADDITIONAL best1 BACK STEPS */
7316  /* IF best2!=0 THEN MINIMUM WAS REACHED IN THE SECOND WHILE */
7317  /* YOU HAVE TO GO-BACK UNTIL n == best2 */
7318 
7319  goback = ((!best2 && (n+best1 > 0)) || (best2 && (n != best2)));
7320  if (goback) vmax = biddyVariableTable.table[v].next; /* save the initial position of v */
7321  if (!best2) {
7322  while (n) {
7323  if (highfirst) {
7324  k = swapWithHigher(MNG,v,&active);
7325  if (v == minvar) {
7326  minvar = k;
7327  }
7328  if (k == maxvar) {
7329  maxvar = v;
7330  }
7331  } else {
7332  k = swapWithLower(MNG,v,&active);
7333  if (v == maxvar) {
7334  maxvar = k;
7335  }
7336  if (k == minvar) {
7337  minvar = v;
7338  }
7339  }
7340  n--;
7341  }
7342  while (n!=best1) {
7343  if (highfirst) {
7344  k = swapWithHigher(MNG,v,&active);
7345  if (v == minvar) {
7346  minvar = k;
7347  }
7348  if (k == maxvar) {
7349  maxvar = v;
7350  }
7351  } else {
7352  k = swapWithLower(MNG,v,&active);
7353  if (v == maxvar) {
7354  maxvar = k;
7355  }
7356  if (k == minvar) {
7357  minvar = v;
7358  }
7359  }
7360  n++;
7361  }
7362  } else {
7363  while (n!=best2) {
7364  if (highfirst) {
7365  k = swapWithHigher(MNG,v,&active);
7366  if (v == minvar) {
7367  minvar = k;
7368  }
7369  if (k == maxvar) {
7370  maxvar = v;
7371  }
7372  } else {
7373  k = swapWithLower(MNG,v,&active);
7374  if (v == maxvar) {
7375  maxvar = k;
7376  }
7377  if (k == minvar) {
7378  minvar = v;
7379  }
7380  }
7381  n--;
7382  }
7383  }
7384 
7385  /* IF SECOND GO-BACK WAS MOVING VARIABLE UP (highfirst == FALSE) */
7386  /* OBDD, ZBDD: ONLY OBSOLETE NODES WITH (var == v) EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
7387  /* TZBDD: OBSOLETE NODES WITH var >= v EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
7388 
7389  /* IF SECOND GO-BACK WAS MOVING VARIABLE DOWN (highfirst == TRUE) */
7390  /* OBDD, ZBDD: OBSOLETE NODES WITH (vmax <= var < v) EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
7391  /* TZBDD: OBSOLETE NODES WITH ANY var EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) ?? */
7392 
7393  /* this garbage collection is required here to remove all obsolete nodes */
7394  /* next GC call may use parameter target and may not remove old obsolete nodes! */
7395  if (goback) {
7396 
7397  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
7398  /* Biddy_Managed_GC(MNG,0,0,FALSE,TRUE); */ /* try this if there are strange problems */
7399  if (highfirst) {
7400  Biddy_Managed_GC(MNG,v,vmax,FALSE,TRUE);
7401  } else {
7402  Biddy_Managed_GC(MNG,k,v,FALSE,TRUE);
7403  }
7404  }
7405  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
7406  /* Biddy_Managed_GC(MNG,0,0,FALSE,TRUE); */ /* try this if there are strange problems */
7407  if (highfirst) {
7408  Biddy_Managed_GC(MNG,v,vmax,FALSE,TRUE);
7409  } else {
7410  Biddy_Managed_GC(MNG,k,v,FALSE,TRUE);
7411  }
7412  }
7413  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
7414  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
7415  }
7416  else {
7417  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
7418  }
7419 
7420  }
7421 
7422  /* CHOOSE NEXT VARIABLE OR FINISH */
7423 
7424  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
7425  assert( min == biddyNodeTable.num );
7426  num = min;
7427  }
7428  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
7429  assert( min == biddyNodeTable.num );
7430  num = min;
7431  }
7432  else if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
7433  assert( min == biddyNodeTable.num );
7434  num = min;
7435  }
7436  else {
7437  num = Biddy_Managed_NodeTableNum(MNG);
7438  }
7439 
7440  /* PROFILING */
7441  /*
7442  {
7443  Biddy_Variable varOrder;
7444  varOrder = getGlobalOrdering(MNG,v);
7445  printf("SIFTING LOOP FINISH WITH variable \"%s\" (v=%u): finalOrder=%u, best1=%u, best2=%u, min=%u, num=%u, numNodes=%u\n",
7446  Biddy_Managed_GetVariableName(MNG,v),v,varOrder,best1,best2,min,num,Biddy_Managed_NodeTableNum(MNG));
7447  }
7448  */
7449 
7450  /* DEBUGGING */
7451  /*
7452  for (k=0; k<Biddy_Managed_VariableTableNum(MNG); k++) {
7453  printf("[\"%s\"@%u]",biddyVariableTable.table[k].name,biddyVariableTable.table[k].num);
7454  }
7455  printf("\n");
7456  */
7457 
7458  finish = TRUE;
7459  /* choose a variable that has not been sifted, yet, and has the max number of nodes */
7460  vmax = 0;
7461  vnum = 0;
7462  v = 1;
7463  while (v < biddyVariableTable.num) {
7464  if ((varTable[v] == 1) && ((vv=biddyVariableTable.table[v].num) > vnum)) {
7465  vmax = v;
7466  vnum = vv;
7467  finish = FALSE;
7468  }
7469  v++;
7470  }
7471  v = vmax;
7472 
7473  /* FOR NON-CONVERGING SIFTING, EVERY NEXT VARIABLE HAS A LITTLE BIT GREATER TRESHOLD */
7474  if (!converge) {
7475  if (treshold < 1.25 * biddyNodeTable.siftingtreshold) {
7476  treshold = treshold + 1 / ((float)3.14 * biddyVariableTable.num);
7477  }
7478  }
7479 
7480  /* PROFILING */
7481  /*
7482  printf("TRESHOLD = %.3f\n",treshold);
7483  */
7484 
7485  } /* while (!finish) */
7486 
7487  /* THIS CODE DISABLES FURTHER CALLS IN THE CASE OF NOT-CONVERGING SIFTING */
7488  /* IN THE CASE OF CONVERGING SIFTING, TRESHOLD IS ADAPTED IN EVERY STEP */
7489  if (!converge) {
7490  totalbest = min;
7491  } else {
7492  treshold = treshold * biddyNodeTable.convergesiftingtreshold;
7493  }
7494 
7495  } /* while (min < totalbest) */
7496 
7497  /* END OF SIFTING ALGORITHM */
7498 
7499  /* DEBUGGING */
7500  /*
7501  printf("SIFTING FINISH: numNodes=%u, systemAge=%u\n",Biddy_Managed_NodeTableNum(MNG),biddySystemAge);
7502  BiddySystemReport(MNG);
7503  */
7504 
7505  return TRUE; /* sifting has been performed */
7506 }
7507 
7508 /***************************************************************************/
7520 BiddySiftingOnFunction(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean converge)
7521 {
7522  Biddy_Manager MNG2;
7523  Biddy_Edge fnew;
7524  Biddy_Variable v;
7525  Biddy_Boolean status;
7526 
7527  /* PROFILING */
7528  /*
7529  clock_t elapsedtime;
7530  BiddyOrderingTable initialOrdering;
7531  memcpy(initialOrdering,biddyOrderingTable,sizeof(BiddyOrderingTable));
7532  elapsedtime = clock();
7533  */
7534 
7535  /* DEBUGGING */
7536  /*
7537  printf("SIFTING ON FUNCTION: Initial number of nodes for f = %u\n",Biddy_Managed_CountNodes(MNG,f));
7538  printf("INITIAL ORDERING:\n");
7539  writeORDER(MNG);
7540  */
7541 
7543 
7544  /* FOR MNG2, DISABLE ALL CACHE TABLES - COPY AND SIFTING IS FASTER WITHOUT THEM */
7545  /* TO DO: user cache tables are not considered, yet */
7546  biddyOPCache2.disabled = TRUE;
7547  biddyEACache2.disabled = TRUE;
7548  biddyRCCache2.disabled = TRUE;
7549  biddyReplaceCache2.disabled = TRUE;
7550 
7551  fnew = Biddy_Managed_Copy(MNG,MNG2,f);
7552  Biddy_Managed_AddPersistentFormula(MNG2,(Biddy_String) "_BIDDY_SIFTING_ON_FUNCTION",fnew); /* sifting uses purge */
7553 
7554  /* PROFILING */
7555  /*
7556  printf("COPY TIME = %.2f\n",(clock()-elapsedtime)/(1.0*CLOCKS_PER_SEC));
7557  */
7558 
7559  /* DEBUGGING */
7560  /*
7561  printf("SIFTING ON FUNCTION: Initial number of nodes for fnew = %u\n",Biddy_Managed_CountNodes(MNG2,fnew));
7562  printf("INITIAL ORDERING FOR fnew:\n");
7563  writeORDER(MNG);
7564  */
7565 
7566  status = BiddyGlobalSifting(MNG2,converge);
7567 
7568  /* PROFILING */
7569  /*
7570  printf("GLOBAL SIFTING TIME = %.2f\n",(clock()-elapsedtime)/(1.0*CLOCKS_PER_SEC));
7571  */
7572 
7573  /* DEBUGGING */
7574  /*
7575  printf("SIFTING ON FUNCTION: Resulting number of nodes for fnew = %u\n",Biddy_Managed_CountNodes(MNG2,fnew));
7576  printf("RESULTING ORDERING FOR fnew:\n");
7577  writeORDER(MNG2);
7578  */
7579 
7580  /* ADAPT FINAL ORDERING TO THE INITIAL MANAGER */
7581  for (v = 1; v < biddyVariableTable.num; v++) {
7582  Biddy_Variable *data = (Biddy_Variable *) malloc(sizeof(Biddy_Variable));
7583  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD))
7584  {
7585  *data = getGlobalOrdering(MNG,v);
7586  }
7587  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
7588  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
7589  {
7590  /* for ZBDD and TZBDD variables are added in the reverse ordering */
7591  *data = biddyVariableTable.num - getGlobalOrdering(MNG,v);
7592  }
7593  else {
7594  exit(1);
7595  }
7596  Biddy_Managed_SetVariableData(MNG,v,(void *) data);
7597  }
7598  BiddySetOrderingByData(MNG,biddyOrderingTable2);
7600 
7601  /* PROFILING */
7602  /*
7603  printf("ADAPTING TIME = %.2f\n",(clock()-elapsedtime)/(1.0*CLOCKS_PER_SEC));
7604  */
7605 
7606  /* DEBUGGING */
7607  /*
7608  printf("SIFTING ON FUNCTION: Resulting number of nodes for f = %u\n",Biddy_Managed_CountNodes(MNG,f));
7609  printf("RESULTING ORDERING:\n");
7610  writeORDER(MNG);
7611  */
7612 
7613  Biddy_ExitMNG(&MNG2);
7614 
7615  /* PROFILING */
7616  /*
7617  BiddySetOrdering(MNG,initialOrdering);
7618  elapsedtime = clock();
7619  BiddySiftingOnFunctionDirect(MNG,f,converge);
7620  printf("LOCAL SIFTING TIME = %.2f\n",(clock()-elapsedtime)/(1.0*CLOCKS_PER_SEC));
7621  printf("SIFTING ON FUNCTION: Resulting number of nodes for f = %u\n",Biddy_Managed_CountNodes(MNG,f));
7622  */
7623 
7624  return status;
7625 }
7626 
7627 /***************************************************************************/
7640 BiddySiftingOnFunctionDirect(Biddy_Manager MNG, Biddy_Edge f,
7641  Biddy_Boolean converge)
7642 {
7643  unsigned int num,min,min2,vnum,vv,totalbest;
7644  unsigned int best1,best2;
7645  Biddy_Variable v,vmax,k,n,minvar,maxvar;
7646  Biddy_Boolean highfirst,stop,finish,active;
7647  unsigned int varTable[BIDDYVARMAX];
7648  float treshold;
7649 
7650  Biddy_Variable minvarOrder,maxvarOrder;
7651  BiddyOrderingTable *fOrdering;
7652 
7653  assert( (f != NULL) && (BiddyIsOK(f) == TRUE) );
7654 
7655  if (f && (((BiddyNode *) BiddyP(f))->expiry == biddySystemAge)) {
7656  fprintf(stdout,"ERROR (BiddySiftingOnFunction): Sifting on fresh function is wrong!\n");
7657  return FALSE;
7658  }
7659 
7660  /* garbage collection is not needed here */
7661  /* however, using GC before sifting on function seems to be a good idea */
7662  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
7663 
7664  /* determine node number and variable ordering for the specific function */
7665  /* fOrdering is the same ordering as biddyOrderingTable, but it */
7666  /* also contains information about which variables are neighbours in f */
7667  /* function nodeNumberOrdering also counts the number of each variable in f */
7668  if (!(fOrdering = (BiddyOrderingTable *) malloc(sizeof(BiddyOrderingTable)))) {
7669  fprintf(stderr,"ERROR (BiddySiftingOnFunction): Out of memoy!\n");
7670  exit(1);
7671  }
7672  for (k=1; k<Biddy_Managed_VariableTableNum(MNG); k++) {
7673  biddyVariableTable.table[k].numone = 0;
7674  }
7675  nullOrdering(*fOrdering);
7676  num = 1;
7677  nodeNumberOrdering(MNG,f,&num,*fOrdering);
7679 
7680  /* determine minvar (lowest == topmost) and maxvar (highest == bottommost) for function f */
7681  minvar = maxvar = BiddyV(f);
7682  stop = FALSE;
7683  while (!stop) {
7684  stop = TRUE;
7685  for (k=1; k<Biddy_Managed_VariableTableNum(MNG); k++) {
7686  if (GET_ORDER(*fOrdering,maxvar,k)) {
7687  maxvar = k;
7688  stop = FALSE;
7689  break;
7690  }
7691  }
7692  }
7693 
7694  /* determine minvar's and maxvar's global ordering */
7695  /* in this global ordering, highest (topmost) variable has ordering 1 */
7696  /* and smallest (bottommost) variable '1' has ordering numUsedVariables */
7697  minvarOrder = maxvarOrder = Biddy_Managed_VariableTableNum(MNG);
7698  for (k=0; k<Biddy_Managed_VariableTableNum(MNG); k++) {
7699  if (GET_ORDER(biddyOrderingTable,minvar,k)) minvarOrder--;
7700  if (GET_ORDER(biddyOrderingTable,maxvar,k)) maxvarOrder--;
7701  }
7702 
7703  /* DEBUGGING */
7704  /*
7705  printf("========================================\n");
7706  printf("minvar: %s (id=%u, order=%u), maxvar: %s (id=%u, order=%u)\n",
7707  Biddy_Managed_GetVariableName(MNG,minvar),minvar,minvarOrder,
7708  Biddy_Managed_GetVariableName(MNG,maxvar),maxvar,maxvarOrder);
7709  printf("========================================\n");
7710  */
7711 
7712  /* SIFTING ALGORITHM */
7713  /* EXAMINE EVERY VARIABLE ONCE! */
7714 
7715  /* WE ARE STARTING WITH A CURRENT NUMBER OF NODES */
7716  if (converge) {
7717  treshold = biddyNodeTable.convergesiftingtreshold;
7718  } else {
7719  treshold = biddyNodeTable.siftingtreshold;
7720  }
7721  min = num;
7722 
7723  totalbest = min+1;
7724  while (min < totalbest) {
7725  totalbest = min;
7726 
7727  /* INIT varTable */
7728  /* varTable is used in the following way: */
7729  /* varTable[i] == 0 iff variable is not in f */
7730  /* varTable[i] == 1 iff variable is in f and has not been sifted, yet */
7731  /* varTable[i] == 2 iff variable is in f and has already been sifted */
7732 
7733  varTable[0] = 2; /* variable '1' is not swapped */
7734  for (k=1; k<Biddy_Managed_VariableTableNum(MNG); k++) {
7735  if (biddyVariableTable.table[k].numone == 0) {
7736  varTable[k] = 0;
7737  } else {
7738  varTable[k] = 1;
7739  }
7740  }
7741 
7742  /* FOR ZBDD WITHOUT COMPLEMENTED EDGES */
7743  /* do not swap variables which are not dependent in any function */
7744  /*
7745  if (biddyManagerType == BIDDYTYPEZBDD) {
7746  for (k=1; k<biddyVariableTable.num; k++) {
7747  BiddyNode *sup;
7748  Biddy_Boolean end,redundant;
7749  end = FALSE;
7750  redundant = TRUE;
7751  sup = biddyVariableTable.table[k].firstNode;
7752  do {
7753  if (sup->f != sup->t) {
7754  redundant = FALSE;
7755  end = TRUE;
7756  }
7757  end = end || (sup == biddyVariableTable.table[k].lastNode);
7758  if (!end) sup = (BiddyNode *) sup->list;
7759  } while (!end);
7760  if (redundant) varTable[k] == 2;
7761  }
7762  }
7763  */
7764 
7765  /* CHOOSE THE VARIABLE THAT WILL BE SIFTED FIRST */
7766  /* 1. it has not been sifted, yet */
7767  /* 2. it has max number of nodes */
7768 
7769  finish = (varTable[minvar] == 2); /* maybe, we are sifting constant variable '1' */
7770  v = 0;
7771  if (!finish) {
7772  /* VARIANT 1 */
7773  /* choose a variable that has the max number of nodes */
7774  vmax = 1;
7775  vnum = biddyVariableTable.table[1].numone;
7776  v = 2;
7777  while (v < Biddy_Managed_VariableTableNum(MNG)) {
7778  if ((vv=biddyVariableTable.table[v].numone) > vnum) {
7779  vmax = v;
7780  vnum = vv;
7781  }
7782  v++;
7783  }
7784  v = vmax;
7785  /* VARIANT 2 */
7786  /* simply choose the smallest (topmost) variable */
7787  /*
7788  v = minvar;
7789  */
7790  }
7791 
7792  while (!finish) {
7793  varTable[v] = 2;
7794 
7795  /* DETERMINE FIRST DIRECTION */
7796  if (v == minvar) { /* TOPMOST VARIABLE */
7797  stop = TRUE; /* skip first direction */
7798  highfirst = FALSE; /* swapWithHigher will be used in second direction */
7799  } else if (v == maxvar) { /* BOTTOMMOST VARIABLE */
7800  stop = TRUE; /* skip first direction */
7801  highfirst = TRUE; /* swapWithLower will be used in second direction */
7802  } else {
7803  stop = FALSE;
7804 
7805  /* VARIANT A: start with shorter direction, thus calculate v's global ordering */
7806 
7807  n = getGlobalOrdering(MNG,v);
7808  if (n > (minvarOrder+maxvarOrder)/2) highfirst = TRUE; else highfirst = FALSE;
7809 
7810 
7811  /* VARIANT B: start with highfirst = TRUE */
7812  /*
7813  highfirst = TRUE;
7814  */
7815  }
7816 
7817  /* PROFILING */
7818  /*
7819  {
7820  Biddy_Variable varOrder;
7821  varOrder = getGlobalOrdering(MNG,v);
7822  printf("SIFTING START: variable: \"%s\" (v=%u), startOrder=%u, min=%u, numNodes=%u, systemAge=%u, ",
7823  Biddy_Managed_GetVariableName(MNG,v),v,varOrder,min,Biddy_Managed_NodeTableNum(MNG),biddySystemAge);
7824  if (highfirst) printf("HIGHFIRST\n"); else printf("LOWFIRST\n");
7825  }
7826  */
7827 
7828  /* DEBUGGING */
7829  /*
7830  for (k=0; k<Biddy_Managed_VariableTableNum(MNG); k++) {
7831  printf("[\"%s\"@%u]",biddyVariableTable.table[k].name,biddyVariableTable.table[k].num);
7832  }
7833  printf("\n");
7834  */
7835 
7836  /* DEBUGGING */
7837  /*
7838  printf("SIFTING: FIRST DIRECTION\n");
7839  */
7840 
7841  /* ONE DIRECTION */
7842  n = 0;
7843  best1 = 0;
7844  while (!stop && (highfirst ?
7845  (k=swapWithHigher(MNG,v,&active)) :
7846  (k=swapWithLower(MNG,v,&active))))
7847  {
7848 
7849  n++; /* number of steps performed*/
7850 
7851  /* DEBUGGING */
7852  /*
7853  printf("SIFTING: ");
7854  if (highfirst) {
7855  printf("%u swaped with higher %u",v,k);
7856  } else {
7857  printf("%u swaped with lower %u",v,k);
7858  }
7859  if (active) printf(" (ACTIVE)");
7860  printf("\n");
7861  */
7862 
7863  if (active) {
7864  /* IF v AND k HAVE BEEN SWAPPED */
7865 
7866  if (highfirst) {
7867  if (v == minvar) {
7868  minvar = k; /* update minvar */
7869  /* minvarOrder is the same */
7870  }
7871  if (k == maxvar) {
7872  maxvar = v; /* update maxvar */
7873  /* maxvarOrder is the same */
7874  stop = TRUE;
7875  }
7876  } else {
7877  if (k == minvar) {
7878  minvar = v; /* update minvar */
7879  /* minvarOrder is the same */
7880  stop = TRUE;
7881  }
7882  if (v == maxvar) {
7883  maxvar = k; /* update maxvar */
7884  /* maxvarOrder is the same */
7885  }
7886  }
7887 
7888  } else {
7889  /* IF v AND k HAVE NOT BEEN SWAPPED */
7890  /* THEY ARE NOT NEIGHBOURS BUT THEY MAY BE BOTH IN f !! */
7891 
7892  if (highfirst) {
7893  if (v == minvar) {
7894  /* if k is in f then minvar = k else minvarOrder++ */
7895  if (varTable[k]) {
7896  minvar = k;
7897  } else {
7898  minvarOrder++;
7899  }
7900  }
7901  if (k == maxvar) {
7902  /* if v is in f then maxvar = v else maxvarOrder-- */
7903  if (varTable[v]) {
7904  maxvar = v;
7905  } else {
7906  maxvarOrder--;
7907  }
7908  stop = TRUE;
7909  }
7910  } else {
7911  if (k == minvar) {
7912  /* if v is in f then minvar = v else minvarOrder++ */
7913  if (varTable[v]) {
7914  minvar = v;
7915  } else {
7916  minvarOrder++;
7917  }
7918  stop = TRUE;
7919  }
7920  if (v == maxvar) {
7921  /* if k is in f then maxvar = k else maxvarOrder-- */
7922  if (varTable[k]) {
7923  maxvar = k;
7924  } else {
7925  maxvarOrder--;
7926  }
7927  }
7928  }
7929 
7930  }
7931 
7932  /* NUMBER OF NODES CAN CHANGE ONLY IF v AND k HAVE BEEN ACTIVELY SWAPPED */
7933  if (active) {
7934 
7935  /* update node number and variable ordering for the specific function */
7936  /* both is neccessary for the algorithm */
7937  /* *fOrdering is the same ordering as biddyOrderingTable, but it */
7938  /* also contains information about which variables are neighbours */
7939  /* garbage collection is not neccessary here! */
7940  for (vmax=1; vmax<Biddy_Managed_VariableTableNum(MNG); vmax++) {
7941  biddyVariableTable.table[vmax].numone = 0;
7942  }
7943  nullOrdering(*fOrdering);
7944  num = 1;
7945  nodeNumberOrdering(MNG,f,&num,*fOrdering);
7947 
7948  /* DEBUGGING */
7949  /*
7950  printf("SIFTING: first direction, step=%u, min=%u, num=%u\n",n,min,num);
7951  */
7952 
7953  if (num < min) { /* first direction should use strict less */
7954  min = num;
7955  best1 = n;
7956  }
7957 
7958  if (num > (treshold * min)) {
7959  stop = TRUE;
7960  }
7961 
7962  /* THIS IS EXPERIMENTAL !!! */
7963  /* IN THE FIRST DIRECTION, PERFORM LIMIT NUMBER OF STEPS */
7964  /* THIS COULD RESULT IN SHORT TIME AND NOT VERY BAD SIZE */
7965  /*
7966  if (n >= 1) {
7967  stop = TRUE;
7968  }
7969  */
7970 
7971  }
7972  } /* while (!stop ...) */
7973 
7974  /* PROFILING */
7975  /*
7976  {
7977  Biddy_Variable varOrder;
7978  varOrder = getGlobalOrdering(MNG,v);
7979  printf("SIFTING BEFORE GO-BACK: variable: \"%s\" (v=%u), currentOrder=%u, min=%u, numNodes=%u\n",
7980  Biddy_Managed_GetVariableName(MNG,v),v,varOrder,min,Biddy_Managed_NodeTableNum(MNG));
7981  }
7982  */
7983 
7984  /* DEBUGGING */
7985  /*
7986  for (k=0; k<Biddy_Managed_VariableTableNum(MNG); k++) {
7987  printf("[\"%s\"@%u]",biddyVariableTable.table[k].name,biddyVariableTable.table[k].num);
7988  }
7989  printf("\n");
7990  */
7991 
7992  /* DEBUGGING */
7993  /*
7994  printf("SIFTING: GO-BACK!\n");
7995  */
7996 
7997  /* GO BACK */
7998  while (n) {
7999  if (highfirst) {
8000  k = swapWithLower(MNG,v,&active);
8001 
8002  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
8003  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
8004  }
8005 
8006  if (v == maxvar) {
8007  /* if k is in f then maxvar = k else maxvarOrder-- */
8008  if (varTable[k]) {
8009  maxvar = k;
8010  } else {
8011  maxvarOrder--;
8012  }
8013  }
8014  if (k == minvar) {
8015  /* if v is in f then minvar = v else minvarOrder++ */
8016  if (varTable[v]) {
8017  minvar = v;
8018  } else {
8019  minvarOrder++;
8020  }
8021  }
8022  } else {
8023  k = swapWithHigher(MNG,v,&active);
8024 
8025  if ((biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD)) {
8026  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
8027  }
8028 
8029  if (v == minvar) {
8030  /* if k is in f then minvar = k else minvarOrder++ */
8031  if (varTable[k]) {
8032  minvar = k;
8033  } else {
8034  minvarOrder++;
8035  }
8036  }
8037  if (k == maxvar) {
8038  /* if v is in f then maxvar = v else maxvarOrder-- */
8039  if (varTable[v]) {
8040  maxvar = v;
8041  } else {
8042  maxvarOrder--;
8043  }
8044  }
8045  }
8046  n--;
8047  }
8048 
8049  /* IF GO-BACK WAS MOVING VARIABLE UP (highfirst == TRUE) */
8050  /* OBDD, ZBDD: ONLY OBSOLETE NODES WITH var == v EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
8051  /* TZBDD: OBSOLETE NODES WITH var >= v EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
8052 
8053  /* IF GO-BACK WAS MOVING VARIABLE DOWN (highfirst == FALSE) */
8054  /* OBDD, ZBDD: OBSOLETE NODES WITH var < v EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
8055  /* TZBDD: OBSOLETE NODES WITH var < v EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
8056 
8057  /* garbage collection is not needed here */
8058  /* however, it seems to be a good idea */
8059  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
8060 
8061  /* update variable ordering for the specific function */
8062  /* to update which variables are neighbours */
8063  for (vmax=1; vmax<Biddy_Managed_VariableTableNum(MNG); vmax++) {
8064  biddyVariableTable.table[vmax].numone = 0;
8065  }
8066  nullOrdering(*fOrdering);
8067  num = 1;
8068  nodeNumberOrdering(MNG,f,&num,*fOrdering);
8070 
8071  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD) ||
8072  (biddyManagerType == BIDDYTYPETZBDDC) || (biddyManagerType == BIDDYTYPETZBDD))
8073  {
8074  fOrdering = &biddyOrderingTable;
8075  }
8076 
8077  /* PROFILING */
8078  /*
8079  {
8080  Biddy_Variable varOrder;
8081  varOrder = getGlobalOrdering(MNG,v);
8082  printf("SIFTING AFTER FIRST DIRECTION: variable: \"%s\" (v=%u), currentOrder=%u, min=%u, numNodes=%u\n",
8083  Biddy_Managed_GetVariableName(MNG,v),v,varOrder,min,Biddy_Managed_NodeTableNum(MNG));
8084  }
8085  */
8086 
8087  /* DEBUGGING */
8088  /*
8089  for (k=0; k<Biddy_Managed_VariableTableNum(MNG); k++) {
8090  printf("[\"%s\"@%u]",biddyVariableTable.table[k].name,biddyVariableTable.table[k].num);
8091  }
8092  printf("\n");
8093  */
8094 
8095  /* DEBUGGING */
8096  /*
8097  printf("SIFTING: SECOND DIRECTION\n");
8098  */
8099 
8100  /* OPPOSITE DIRECTION */
8101 
8102  n = 0;
8103  best2 = 0;
8104  stop = FALSE;
8105  min2 = Biddy_Managed_NodeTableNum(MNG); /* recalculate node number after go-back */
8106 
8107  if (converge) {
8108 
8109  /* VARIANT C1: min from the first direction is not used within second direction */
8110  /* no code is needed in this variant */
8111 
8112  /* VARIANT C2: min from the first direction is used within second direction */
8113  /*
8114  min2 = min;
8115  */
8116 
8117  /* VARIANT C3: if there is min in the first direction do not check second direction */
8118  /*
8119  if (best1) {
8120  stop = TRUE;
8121  }
8122  */
8123 
8124  } else {
8125 
8126  /* VARIANT NC1: min from the first direction is not used within second direction */
8127  /* no code is needed in this variant */
8128 
8129  /* VARIANT NC2: min from the first direction is used within second direction */
8130  /*
8131  min2 = min;
8132  */
8133 
8134  /* VARIANT NC3: if there is min in the first direction do not check second direction */
8135  /* THIS SEEMS TO BE BAD FOR REGULAR SIFTING */
8136 
8137  }
8138 
8139  while (!stop && (highfirst ?
8140  (k=swapWithLower(MNG,v,&active)) :
8141  (k=swapWithHigher(MNG,v,&active))))
8142  {
8143 
8144  n++;
8145 
8146  /* DEBUGGING */
8147  /*
8148  printf("SIFTING: ");
8149  if (highfirst) {
8150  printf("%u swaped with lower %u",v,k);
8151  } else {
8152  printf("%u swaped with higher %u",v,k);
8153  }
8154  if (active) printf(" (ACTIVE)");
8155  printf("\n");
8156  */
8157 
8158  if (active) {
8159  /* IF v AND k HAVE BEEN SWAPPED */
8160 
8161  if (highfirst) {
8162  if (k == minvar) {
8163  minvar = v; /* update minvar */
8164  stop = TRUE;
8165  }
8166  if (v == maxvar) {
8167  maxvar = k; /* update maxvar */
8168  /* maxvarOrder is the same */
8169  }
8170  } else {
8171  if (v == minvar) {
8172  minvar = k; /* update minvar */
8173  /* minvarOrder is the same */
8174  }
8175  if (k == maxvar) {
8176  maxvar = v; /* update maxvar */
8177  stop = TRUE;
8178  }
8179  }
8180 
8181  } else {
8182  /* IF v AND k HAVE NOT BEEN SWAPPED */
8183  /* THEY ARE NOT NEIGHBOURS BUT THEY MAY BE BOTH IN f !! */
8184 
8185  if (highfirst) {
8186  if (k == minvar) {
8187  /* if v is in f then minvar = v else minvarOrder++ */
8188  if (varTable[v]) {
8189  minvar = v;
8190  } else {
8191  minvarOrder++;
8192  }
8193  stop = TRUE;
8194  }
8195  if (v == maxvar) {
8196  /* if k is in f then maxvar = k else maxvarOrder-- */
8197  if (varTable[k]) {
8198  maxvar = k;
8199  } else {
8200  maxvarOrder--;
8201  }
8202  }
8203  } else {
8204  if (v == minvar) {
8205  /* if k is in f then minvar = k else minvarOrder++ */
8206  if (varTable[k]) {
8207  minvar = k;
8208  } else {
8209  minvarOrder++;
8210  }
8211  }
8212  if (k == maxvar) {
8213  /* if v is in f then maxvar = v else maxvarOrder-- */
8214  if (varTable[v]) {
8215  maxvar = v;
8216  } else {
8217  maxvarOrder--;
8218  }
8219  stop = TRUE;
8220  }
8221  }
8222 
8223  }
8224 
8225  /* NUMBER OF NODES CAN CHANGE ONLY IF v AND k HAVE BEEN ACTIVELY SWAPPED */
8226  if (active) {
8227 
8228  /* update node number and variable ordering for the specific function */
8229  /* both is neccessary for the algorithm */
8230  /* *fOrdering is the same ordering as biddyOrderingTable, but it */
8231  /* also contains information about which variables are neighbours */
8232  /* garbage collection is not neccessary here! */
8233  for (vmax=1; vmax<Biddy_Managed_VariableTableNum(MNG); vmax++) {
8234  biddyVariableTable.table[vmax].numone = 0;
8235  }
8236  nullOrdering(*fOrdering);
8237  num = 1;
8238  nodeNumberOrdering(MNG,f,&num,*fOrdering);
8240 
8241  /* DEBUGGING */
8242  /*
8243  printf("SIFTING: second direction, step=%u, min2=%u, num=%u\n",n,min2,num);
8244  */
8245 
8246  if (num <= min2) { /* second direction should use less or equal */
8247  min2 = num;
8248  best2 = n;
8249  }
8250 
8251  if (num > (treshold * min2)) {
8252  stop = TRUE;
8253  }
8254 
8255  }
8256  } /* while (!stop ...) */
8257 
8258  if (min2 <= min) { /* second direction should use less or equal */
8259  min = min2;
8260  } else {
8261  best2 = 0;
8262  }
8263 
8264  /* IF best2==0 THEN MINIMUM WAS REACHED IN THE FIRST WHILE */
8265  /* YOU HAVE TO GO-BACK AND THEN MAKE ADDITIONAL best1 BACK STEPS */
8266  /* IF best2!=0 THEN MINIMUM WAS REACHED IN THE SECOND WHILE */
8267  /* YOU HAVE TO GO-BACK UNTIL n == best2 */
8268 
8269  if (!best2) {
8270  while (n) {
8271  if (highfirst) {
8272  k = swapWithHigher(MNG,v,&active);
8273  if (v == minvar) {
8274  /* if k is in f then minvar = k else minvarOrder++ */
8275  if (varTable[k]) {
8276  minvar = k;
8277  } else {
8278  minvarOrder++;
8279  }
8280  }
8281  if (k == maxvar) {
8282  /* if v is in f then maxvar = v else maxvarOrder-- */
8283  if (varTable[v]) {
8284  maxvar = v;
8285  } else {
8286  maxvarOrder--;
8287  }
8288  }
8289  } else {
8290  k = swapWithLower(MNG,v,&active);
8291  if (v == maxvar) {
8292  /* if k is in f then maxvar = k else maxvarOrder-- */
8293  if (varTable[k]) {
8294  maxvar = k;
8295  } else {
8296  maxvarOrder--;
8297  }
8298  }
8299  if (k == minvar) {
8300  /* if v is in f then minvar = v else minvarOrder++ */
8301  if (varTable[v]) {
8302  minvar = v;
8303  } else {
8304  minvarOrder++;
8305  }
8306  }
8307  }
8308  n--;
8309  }
8310  while (n!=best1) {
8311  if (highfirst) {
8312  k = swapWithHigher(MNG,v,&active);
8313  if (v == minvar) {
8314  /* if k is in f then minvar = k else minvarOrder++ */
8315  if (varTable[k]) {
8316  minvar = k;
8317  } else {
8318  minvarOrder++;
8319  }
8320  }
8321  if (k == maxvar) {
8322  /* if v is in f then maxvar = v else maxvarOrder-- */
8323  if (varTable[v]) {
8324  maxvar = v;
8325  } else {
8326  maxvarOrder--;
8327  }
8328  }
8329  } else {
8330  k = swapWithLower(MNG,v,&active);
8331  if (v == maxvar) {
8332  /* if k is in f then maxvar = k else maxvarOrder-- */
8333  if (varTable[k]) {
8334  maxvar = k;
8335  } else {
8336  maxvarOrder--;
8337  }
8338  }
8339  if (k == minvar) {
8340  /* if v is in f then minvar = v else minvarOrder++ */
8341  if (varTable[v]) {
8342  minvar = v;
8343  } else {
8344  minvarOrder++;
8345  }
8346  }
8347  }
8348  n++;
8349  }
8350  } else {
8351  while (n!=best2) {
8352  if (highfirst) {
8353  k = swapWithHigher(MNG,v,&active);
8354  if (v == minvar) {
8355  /* if k is in f then minvar = k else minvarOrder++ */
8356  if (varTable[k]) {
8357  minvar = k;
8358  } else {
8359  minvarOrder++;
8360  }
8361  }
8362  if (k == maxvar) {
8363  /* if v is in f then maxvar = v else maxvarOrder-- */
8364  if (varTable[v]) {
8365  maxvar = v;
8366  } else {
8367  maxvarOrder--;
8368  }
8369  }
8370  } else {
8371  k = swapWithLower(MNG,v,&active);
8372  if (v == maxvar) {
8373  /* if k is in f then maxvar = k else maxvarOrder-- */
8374  if (varTable[k]) {
8375  maxvar = k;
8376  } else {
8377  maxvarOrder--;
8378  }
8379  }
8380  if (k == minvar) {
8381  /* if v is in f then minvar = v else minvarOrder++ */
8382  if (varTable[v]) {
8383  minvar = v;
8384  } else {
8385  minvarOrder++;
8386  }
8387  }
8388  }
8389  n--;
8390  }
8391  }
8392 
8393  /* IF SECOND GO-BACK WAS MOVING VARIABLE UP (highfirst == FALSE) */
8394  /* OBDD, ZBDD: ONLY OBSOLETE NODES WITH var == v EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
8395  /* TZBDD: OBSOLETE NODES WITH var >= v EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
8396 
8397  /* IF SECOND GO-BACK WAS MOVING VARIABLE DOWN (highfirst == TRUE) */
8398  /* OBDD, ZBDD: OBSOLETE NODES WITH var < v EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
8399  /* TZBDD: OBSOLETE NODES WITH var < v EXIST IN THE SYSTEM (NO GC WAS CALLED FOR GO-BACK) */
8400 
8401  /* garbage collection is not needed here */
8402  /* however, it seems to be a good idea */
8403  Biddy_Managed_GC(MNG,0,0,FALSE,TRUE);
8404 
8405  /* CHOOSE NEXT VARIABLE OR FINISH */
8406  /* VARIABLES NOT IN f WILL BE SKIPPED */
8407  /* ou have to update variable ordering for the function to update which variables are neighbours */
8408 
8409  for (vmax=1; vmax<Biddy_Managed_VariableTableNum(MNG); vmax++) {
8410  biddyVariableTable.table[vmax].numone = 0;
8411  }
8412  nullOrdering(*fOrdering);
8413  num = 1;
8414  nodeNumberOrdering(MNG,f,&num,*fOrdering);
8416 
8417  /* PROFILING */
8418  /*
8419  {
8420  Biddy_Variable varOrder;
8421  varOrder = getGlobalOrdering(MNG,v);
8422  printf("SIFTING FINAL: variable: \"%s\" (v=%u), finalOrder=%u, best1=%u, best2=%u, min=%u, num=%u, numNodes=%u\n",
8423  Biddy_Managed_GetVariableName(MNG,v),v,varOrder,best1,best2,min,num,Biddy_Managed_NodeTableNum(MNG));
8424  }
8425  */
8426 
8427  /* DEBUGGING */
8428  /*
8429  for (k=0; k<Biddy_Managed_VariableTableNum(MNG); k++) {
8430  printf("[\"%s\"@%u]",biddyVariableTable.table[k].name,biddyVariableTable.table[k].num);
8431  }
8432  printf("\n");
8433  */
8434 
8435  finish = TRUE;
8436  /* choose a variable that has not been sifted, yet, and has the max number of nodes */
8437  vmax = 0;
8438  vnum = 0;
8439  v = 1;
8440  while (v < Biddy_Managed_VariableTableNum(MNG)) {
8441  if ((varTable[v] == 1) && ((vv=biddyVariableTable.table[v].numone) > vnum)) {
8442  vmax = v;
8443  vnum = vv;
8444  finish = FALSE;
8445  }
8446  v++;
8447  }
8448  v = vmax;
8449 
8450  /* FOR NON-CONVERGING SIFTING, EVERY NEXT VARIABLE HAS A LITTLE BIT GREATER TRESHOLD */
8451  if (!converge) {
8452  if (treshold < 1.25 * biddyNodeTable.siftingtreshold) {
8453  treshold = treshold + 1 / ((float)3.14 * Biddy_Managed_VariableTableNum(MNG));
8454  }
8455  }
8456 
8457  /* PROFILING */
8458  /*
8459  printf("TRESHOLD = %.3f\n",treshold);
8460  */
8461 
8462  } /* while (!finish) */
8463 
8464  /* THIS CODE DISABLES FURTHER CALLS IN THE CASE OF NOT-CONVERGING SIFTING */
8465  /* IN THE CASE OF CONVERGING SIFTING, TRESHOLD IS ADAPTED IN EVERY STEP */
8466  if (!converge) {
8467  totalbest = min;
8468  } else {
8469  treshold = treshold * biddyNodeTable.convergesiftingtreshold;
8470  }
8471 
8472  } /* while (min < totalbest) */
8473 
8474  /* END OF SIFTING ALGORITHM */
8475 
8476  free(fOrdering);
8477 
8478  return TRUE; /* sifting has been performed */
8479 }
8480 
8481 /*******************************************************************************
8482 \brief Initialization of Steinhaus–Johnson–Trotter algorithm.
8483 
8484 ### Description
8485  Create data needed for Steinhaus–Johnson–Trotter algorithm.
8486 ### Side effects
8487 ### More info
8488 *******************************************************************************/
8489 
8490 void
8491 BiddySjtInit(Biddy_Manager MNG)
8492 {
8493  unsigned int i;
8494  Biddy_Variable v;
8495 
8496  struct userdata {
8497  unsigned int value;
8498  Biddy_Boolean direction;
8499  } *ud;
8500 
8501  /* OBSOLETE NODES ARE REMOVED TO MAKE SWAPPING FASTER */
8502  Biddy_Managed_AutoGC(MNG);
8503 
8505  i = 0;
8506  do {
8507  ud = (struct userdata *) malloc(sizeof(struct userdata));
8508  ud->value = i;
8509  ud->direction = FALSE; /* FALSE = left = toTop = toLowest, TRUE = right = toBottom = toHighest */
8510  Biddy_Managed_SetVariableData(MNG,v,(void *) ud);
8511  v = biddyVariableTable.table[v].next;
8512  i++;
8513  } while (v != 0);
8514 }
8515 
8516 /*******************************************************************************
8517 \brief Remove data needed for Steinhaus–Johnson–Trotter algorithm.
8518 
8519 ### Description
8520 ### Side effects
8521 ### More info
8522 *******************************************************************************/
8523 
8524 void
8525 BiddySjtExit(Biddy_Manager MNG)
8526 {
8528 }
8529 
8530 /*******************************************************************************
8531 \brief One step of Steinhaus–Johnson–Trotter algorithm.
8532 
8533 ### Description
8534  Returns TRUE if a step was made, otherwise it returns FALSE.
8535 ### Side effects
8536 ### More info
8537 *******************************************************************************/
8538 
8540 BiddySjtStep(Biddy_Manager MNG)
8541 {
8542  Biddy_Variable v,mm;
8543  unsigned int mmvalue;
8544  Biddy_Boolean STOP;
8545