Biddy  1.8.1
An academic Binary Decision Diagrams package
biddyOp.c
Go to the documentation of this file.
1 /***************************************************************************/
43 #include "biddyInt.h"
44 
45 /*----------------------------------------------------------------------------*/
46 /* Constant declarations */
47 /*----------------------------------------------------------------------------*/
48 
49 /*----------------------------------------------------------------------------*/
50 /* Variable declarations */
51 /*----------------------------------------------------------------------------*/
52 
53 /*----------------------------------------------------------------------------*/
54 /* Static function prototypes */
55 /*----------------------------------------------------------------------------*/
56 
57 static void exchangeEdges(Biddy_Edge *f, Biddy_Edge *g);
58 
59 static void complExchangeEdges(Biddy_Edge *f, Biddy_Edge *g);
60 
61 static Biddy_Edge createMinterm(Biddy_Manager MNG, Biddy_Edge support, long long unsigned int n, long long unsigned int x);
62 
63 static Biddy_Edge createFunction(Biddy_Manager MNG, Biddy_Edge support, long long unsigned int n, long long unsigned int m, long long unsigned int x);
64 
65 static inline unsigned int op3Hash(Biddy_Edge a, Biddy_Edge b, Biddy_Edge c, unsigned int size);
66 
67 static inline unsigned int keywordHash(Biddy_Edge a, unsigned int k, unsigned int size);
68 
69 static inline void addOp3Cache(Biddy_Manager MNG, BiddyOp3CacheTable cache, Biddy_Edge a, Biddy_Edge b, Biddy_Edge c, Biddy_Edge r, unsigned int index);
70 
71 static inline Biddy_Boolean findOp3Cache(Biddy_Manager MNG, BiddyOp3CacheTable cache, Biddy_Edge a, Biddy_Edge b, Biddy_Edge c, Biddy_Edge *r, unsigned int *index);
72 
73 static inline void addKeywordCache(Biddy_Manager MNG, BiddyKeywordCacheTable cache, Biddy_Edge a, unsigned int k, Biddy_Edge r, unsigned int index);
74 
75 static inline Biddy_Boolean findKeywordCache(Biddy_Manager MNG, BiddyKeywordCacheTable cache, Biddy_Edge a, unsigned int k, Biddy_Edge *r, unsigned int *index);
76 
77 /*----------------------------------------------------------------------------*/
78 /* Definition of exported functions */
79 /*----------------------------------------------------------------------------*/
80 
81 /***************************************************************************/
95 #ifdef __cplusplus
96 extern "C" {
97 #endif
98 
101 {
102  Biddy_Edge r;
103 
104  assert( f != NULL );
105 
106  if (!MNG) MNG = biddyAnonymousManager;
107  ZF_LOGI("Biddy_Not");
108 
109  assert( BiddyIsOK(f) == TRUE );
110 
111  r = biddyNull;
112 
113  if (biddyManagerType == BIDDYTYPEOBDD) {
114  /* IMPLEMENTED */
115  r = BiddyManagedNot(MNG,f);
116  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
117  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
118  /* IMPLEMENTED */
119  r = Biddy_Inv(f);
120  /* BiddyRefresh() */ /* not needed because the same node is returned */
121  } else if (biddyManagerType == BIDDYTYPEZBDD) {
122  /* IMPLEMENTED */
123  r = BiddyManagedNot(MNG,f);
124  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
125  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
126  /* IMPLEMENTED */
127  r = BiddyManagedNot(MNG,f);
128  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
129  } else if (biddyManagerType == BIDDYTYPETZBDD) {
130  /* IMPLEMENTED */
131  r = BiddyManagedNot(MNG,f);
132  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
133  } else if (biddyManagerType == BIDDYTYPETZBDDC)
134  {
135  fprintf(stderr,"Biddy_Not: this BDD type is not supported, yet!\n");
136  return biddyNull;
137  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
138  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
139  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
140  {
141  fprintf(stderr,"Biddy_Not: this BDD type is not supported, yet!\n");
142  return biddyNull;
143  } else {
144  fprintf(stderr,"Biddy_Not: Unsupported BDD type!\n");
145  return biddyNull;
146  }
147 
148  return r;
149 }
150 
151 #ifdef __cplusplus
152 }
153 #endif
154 
156 BiddyManagedNot(const Biddy_Manager MNG, const Biddy_Edge f)
157 {
158  Biddy_Edge r, T, E, Fv, Gv, Fneg_v, Gneg_v;
159  Biddy_Edge FF, GG, HH;
160  Biddy_Variable v, nt;
161  unsigned int cindex;
162 
163  assert( MNG != NULL );
164  assert( f != NULL );
165 
166  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
167  assert(
168  (biddyManagerType == BIDDYTYPEOBDD) ||
169  (biddyManagerType == BIDDYTYPEOBDDC) ||
170  (biddyManagerType == BIDDYTYPEZBDD) ||
171  (biddyManagerType == BIDDYTYPEZBDDC) ||
172  (biddyManagerType == BIDDYTYPETZBDD)
173  );
174 
175  r = biddyNull;
176 
177  /* LOOKING FOR SIMPLE CASE */
178 
179  if (f == biddyZero) {
180  return biddyOne;
181  }
182  if (f == biddyOne) {
183  return biddyZero;
184  }
185 
186  /* THIS IS NOT A SIMPLE CASE */
187 
188  FF = GG = HH = biddyNull;
189  Fneg_v = Fv = biddyNull;
190  Gneg_v = Gv = biddyNull;
191  v = 0;
192 
193  if (biddyManagerType == BIDDYTYPEOBDDC) {
194 
195  /* FOR OBDDC, CACHE TABLE IS NOT NEEDED */
196 
197  r = Biddy_Inv(f);
198 
199  }
200 
201  else if (biddyManagerType == BIDDYTYPEOBDD) {
202 
203  /* FOR OBDD, 'NOT' USES CACHE TABLE DIRECTLY */
204  /* THIS IS NOT ITE CACHE! */
205 
206  FF = f;
207  GG = biddyZero;
208  HH = biddyOne;
209 
210  /* IF RESULT IS NOT IN THE CACHE TABLE... */
211  cindex = 0;
212  if (!findOp3Cache(MNG,biddyOPCache,FF,GG,HH,&r,&cindex))
213  {
214 
215  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS */
216  v = BiddyV(f);
217  Fneg_v = BiddyE(f);
218  Fv = BiddyT(f);
219 
220  /* RECURSIVE CALLS */
221  if (Fneg_v == biddyZero) {
222  E = biddyOne;
223  } else if (Fneg_v == biddyOne) {
224  E = biddyZero;
225  } else {
226  E = BiddyManagedNot(MNG,Fneg_v);
227  }
228  if (Fv == biddyZero) {
229  T = biddyOne;
230  } else if (Fv == biddyOne) {
231  T = biddyZero;
232  } else {
233  T = BiddyManagedNot(MNG,Fv);
234  }
235 
236  r = BiddyManagedTaggedFoaNode(MNG,v,E,T,v,TRUE);
237  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
238 
239  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,r,cindex);
240 
241  } else {
242 
243  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
244  BiddyRefresh(r);
245 
246  }
247 
248  }
249 
250  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
251 
252  /* FOR ZBDD AND ZBDDC, RECURSIVE CALLS ARE VIA 'XOR' AND THUS ITS CACHE TABLE IS USED */
253 
254  v = BiddyV(biddyOne); /* biddyOne includes all variables */
255 
256  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS */
257  /* COMPLEMENTED EDGES MUST BE TRANSFERED */
258  if (BiddyV(f) == v) {
259  Fneg_v = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
260  Fv = BiddyT(f);
261  } else {
262  Fneg_v = f;
263  Fv = biddyZero;
264  }
265  Gneg_v = BiddyE(biddyOne); /* biddyOne does not have complement */
266  Gv = BiddyT(biddyOne);
267 
268  /* RECURSIVE CALLS */
269  if (Fneg_v == biddyZero) {
270  E = Gneg_v;
271  } else if (Gneg_v == biddyZero) {
272  E = Fneg_v;
273  } else {
274  E = BiddyManagedXor(MNG,Fneg_v,Gneg_v);
275  }
276  if (Fv == biddyZero) {
277  T = Gv;
278  } else if (Gv == biddyZero) {
279  T = Fv;
280  } else {
281  T = BiddyManagedXor(MNG,Fv,Gv);
282  }
283 
284  r = BiddyManagedTaggedFoaNode(MNG,v,E,T,v,TRUE);
285  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
286 
287  }
288 
289  else if (biddyManagerType == BIDDYTYPETZBDD) {
290 
291  /* FOR TZBDD, 'NOT' USES CACHE TABLE DIRECTLY */
292  /* THIS IS NOT ITE CACHE! */
293 
294  FF = f;
295  GG = biddyZero;
296  HH = biddyOne;
297 
298  /* IF RESULT IS NOT IN THE CACHE TABLE... */
299  cindex = 0;
300  if (!findOp3Cache(MNG,biddyOPCache,FF,GG,HH,&r,&cindex))
301  {
302 
303  v = BiddyV(f);
304  nt = Biddy_GetTag(f);
305  if (!v) {
306  r = biddyZero;
307  } else {
308  Fneg_v = BiddyE(f);
309  Fv = BiddyT(f);
310 
311  /* RECURSIVE CALLS */
312  if (Fneg_v == biddyZero) {
313  E = biddyOne;
314  } else if (Fneg_v == biddyOne) {
315  E = biddyZero;
316  } else {
317  E = BiddyManagedNot(MNG,Fneg_v);
318  }
319  if (Fv == biddyZero) {
320  T = biddyOne;
321  } else if (Fv == biddyOne) {
322  T = biddyZero;
323  } else {
324  T = BiddyManagedNot(MNG,Fv);
325  }
326 
327  r = BiddyManagedTaggedFoaNode(MNG,v,E,T,v,TRUE);
328  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
329  }
330 
331  while (v != nt) {
332  v = biddyVariableTable.table[v].prev;
333  r = BiddyManagedTaggedFoaNode(MNG,v,r,biddyOne,v,TRUE);
334  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
335  }
336 
337  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,r,cindex);
338 
339  } else {
340 
341  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
342  BiddyRefresh(r);
343 
344  }
345 
346  }
347 
348  return r;
349 }
350 
351 /***************************************************************************/
365 #ifdef __cplusplus
366 extern "C" {
367 #endif
368 
371 {
372  Biddy_Edge r;
373 
374  assert( f != NULL );
375  assert( g != NULL );
376  assert( h != NULL );
377 
378  if (!MNG) MNG = biddyAnonymousManager;
379  ZF_LOGI("Biddy_ITE");
380 
381  assert( BiddyIsOK(f) == TRUE );
382  assert( BiddyIsOK(g) == TRUE );
383  assert( BiddyIsOK(h) == TRUE );
384 
385  biddyNodeTable.funite++;
386 
387  r = biddyNull;
388 
389  if (biddyManagerType == BIDDYTYPEOBDD) {
390  /* IMPLEMENTED */
391  r = BiddyManagedITE(MNG,f,g,h);
392  BiddyRefresh(r); /* not always refreshed by BiddyManagedITE */
393  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
394  /* IMPLEMENTED */
395  r = BiddyManagedITE(MNG,f,g,h);
396  BiddyRefresh(r); /* not always refreshed by BiddyManagedITE */
397  } else if (biddyManagerType == BIDDYTYPEZBDD) {
398  /* IMPLEMENTED */
399  r = BiddyManagedITE(MNG,f,g,h);
400  BiddyRefresh(r); /* not always refreshed by BiddyManagedITE */
401  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
402  /* IMPLEMENTED */
403  r = BiddyManagedITE(MNG,f,g,h);
404  BiddyRefresh(r); /* not always refreshed by BiddyManagedITE */
405  } else if (biddyManagerType == BIDDYTYPETZBDD) {
406  /* IMPLEMENTED */
407  r = BiddyManagedITE(MNG,f,g,h);
408  BiddyRefresh(r); /* not always refreshed by BiddyManagedITE */
409  } else if (biddyManagerType == BIDDYTYPETZBDDC)
410  {
411  fprintf(stderr,"Biddy_ITE: this BDD type is not supported, yet!\n");
412  return biddyNull;
413  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
414  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
415  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
416  {
417  fprintf(stderr,"Biddy_ITE: this BDD type is not supported, yet!\n");
418  return biddyNull;
419  } else {
420  fprintf(stderr,"Biddy_ITE: Unsupported BDD type!\n");
421  return biddyNull;
422  }
423 
424  return r;
425 }
426 
427 #ifdef __cplusplus
428 }
429 #endif
430 
432 BiddyManagedITE(const Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Edge h)
433 {
434  Biddy_Edge r, T, E, Fv, Gv, Hv, Fneg_v, Gneg_v, Hneg_v;
435  Biddy_Edge FF, GG, HH;
436  Biddy_Boolean NN;
437  Biddy_Variable v,rtag;
438  unsigned cindex;
439 
440  static Biddy_Variable topF; /* CAN BE STATIC, WHAT IS BETTER? */
441  static Biddy_Variable topG; /* CAN BE STATIC, WHAT IS BETTER? */
442  static Biddy_Variable topH; /* CAN BE STATIC, WHAT IS BETTER? */
443  static Biddy_Variable tagF; /* CAN BE STATIC, WHAT IS BETTER? */
444  static Biddy_Variable tagG; /* CAN BE STATIC, WHAT IS BETTER? */
445  static Biddy_Variable tagH; /* CAN BE STATIC, WHAT IS BETTER? */
446 
447  /* DEBUGGING */
448  /*
449  static int mm = 0;
450  int nn;
451  nn = ++mm;
452  printf("BiddyManagedITE (%d) F\n",nn);
453  Biddy_Managed_PrintfBDD(MNG,f);
454  printf("\n");
455  printf("BiddyManagedITE (%d) G\n",nn);
456  Biddy_Managed_PrintfBDD(MNG,g);
457  printf("\n");
458  printf("BiddyManagedITE (%d) H\n",nn);
459  Biddy_Managed_PrintfBDD(MNG,h);
460  printf("\n");
461  mm = nn;
462  */
463 
464  assert( MNG != NULL );
465  assert( f != NULL );
466  assert( g != NULL );
467  assert( h != NULL );
468 
469  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
470  assert(
471  (biddyManagerType == BIDDYTYPEOBDD) ||
472  (biddyManagerType == BIDDYTYPEOBDDC) ||
473  (biddyManagerType == BIDDYTYPEZBDD) ||
474  (biddyManagerType == BIDDYTYPEZBDDC) ||
475  (biddyManagerType == BIDDYTYPETZBDD)
476  );
477 
478 #ifdef BIDDYEXTENDEDSTATS_YES
479  biddyNodeTable.iterecursive++;
480 #endif
481 
482  r = biddyNull;
483 
484  /* LOOKING FOR SIMPLE CASE */
485  /* using Not/Leq and returning biddyOne in a recursive call is wrong for ZBDD and ZBDDC, */
486  /* because top variable of the result may be lower (topmore) than top variables of the arguments */
487  /* (i.e. because the result depends on domain) */
488 
489  if (f == biddyOne) {
490  return g;
491  } else if (f == biddyZero) {
492  return h;
493  } else if (g == biddyOne) {
494  if (h == biddyOne) {
495  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
496  return biddyOne;
497  } else if (h == biddyZero) {
498  return f;
499  } else {
500  return BiddyManagedOr(MNG,f,h);
501  }
502  } else if (g == biddyZero) {
503  if (h == biddyOne) {
504  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
505  return BiddyManagedNot(MNG,f);
506  } else if (h == biddyZero) {
507  return biddyZero;
508  } else {
509  return BiddyManagedGt(MNG,h,f);
510  }
511  } else if (h == biddyOne) {
512  if ((biddyManagerType != BIDDYTYPEZBDDC) && (biddyManagerType != BIDDYTYPEZBDD)) {
513  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
514  /* FOR ZBDD AND ZBDDC ITE CANNOT BE RESOLVED BY LEQ, BECAUSE LEQ IS RESOLVED BY ITE */
515  return BiddyManagedLeq(MNG,f,g);
516  }
517  } else if (h == biddyZero) {
518  return BiddyManagedAnd(MNG,f,g);
519  } else if (g == h) {
520  return g;
521  } else if (f == g) {
522  return BiddyManagedOr(MNG,f,h);
523  } else if (f == h) {
524  return BiddyManagedAnd(MNG,f,g);
525  }
526 
527  if (biddyManagerType == BIDDYTYPEOBDDC) {
528  if (Biddy_IsEqvPointer(g,h)) {
529  return BiddyManagedXor(MNG,f,h);
530  } else if (Biddy_IsEqvPointer(f,g)) {
531  return BiddyManagedAnd(MNG,g,h);
532  } else if (Biddy_IsEqvPointer(f,h)) {
533  return BiddyManagedOr(MNG,g,h);
534  }
535  }
536 
537  /* THIS IS NOT A SIMPLE CASE */
538 
539  FF = GG = HH = biddyNull;
540  NN = FALSE;
541  Fneg_v = Fv = biddyNull;
542  Gneg_v = Gv = biddyNull;
543  Hneg_v = Hv = biddyNull;
544  rtag = 0;
545  v = 0;
546 
547  /* NORMALIZATION OF COMPLEMENTED EDGES */
548  /* APLICABLE ONLY TO OBDDC */
549  /* FF, GG, HH, and NN ARE USED FOR CACHE LOOKUP, ONLY */
550 
551  if (biddyManagerType == BIDDYTYPEOBDDC) {
552  if (Biddy_GetMark(f)) {
553  if (Biddy_GetMark(h)) {
554  NN = TRUE;
555  FF = Biddy_Inv(f);
556  GG = Biddy_Inv(h);
557  HH = Biddy_Inv(g);
558  } else {
559  FF = Biddy_Inv(f);
560  GG = h;
561  HH = g;
562  }
563  } else if (Biddy_GetMark(g)) {
564  NN = TRUE;
565  FF = f;
566  GG = Biddy_Inv(g);
567  HH = Biddy_Inv(h);
568  } else {
569  FF = f;
570  GG = g;
571  HH = h;
572  }
573  }
574 
575  else {
576 
577  /* IF NOT OBDDC THEN ITE CACHE IS NOT SHARED WITH OTHER OPERATIONS! */
578 
579  FF = f;
580  GG = g;
581  HH = h;
582  }
583 
584  /* IF RESULT IS NOT IN THE CACHE TABLE... */
585  cindex = 0;
586  if (!findOp3Cache(MNG,biddyOPCache,FF,GG,HH,&r,&cindex))
587  {
588 
589  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
590 
591  /* LOOKING FOR THE SMALLEST TOP VARIABLE */
592  topF = BiddyV(f);
593  topG = BiddyV(g);
594  topH = BiddyV(h);
595 
596  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
597  if (BiddyIsSmaller(topF,topG)) {
598  v = BiddyIsSmaller(topF,topH) ? topF : topH;
599  } else {
600  v = BiddyIsSmaller(topH,topG) ? topH : topG;
601  }
602 
603  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS */
604  if (topF == v) {
605  Fneg_v = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
606  Fv = Biddy_InvCond(BiddyT(f),Biddy_GetMark(f));
607  } else {
608  Fneg_v = Fv = f;
609  }
610  if (topG == v) {
611  Gneg_v = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
612  Gv = Biddy_InvCond(BiddyT(g),Biddy_GetMark(g));
613  } else {
614  Gneg_v = Gv = g;
615  }
616  if (topH == v) {
617  Hneg_v = Biddy_InvCond(BiddyE(h),Biddy_GetMark(h));
618  Hv = Biddy_InvCond(BiddyT(h),Biddy_GetMark(h));
619  } else {
620  Hneg_v = Hv = h;
621  }
622 
623  rtag = v;
624 
625  }
626 
627  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
628 
629  /* LOOKING FOR THE SMALLEST TOP VARIABLE */
630  topF = BiddyV(f);
631  topG = BiddyV(g);
632  topH = BiddyV(h);
633 
634  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
635  if (BiddyIsSmaller(topF,topG)) {
636  v = BiddyIsSmaller(topF,topH) ? topF : topH;
637  } else {
638  v = BiddyIsSmaller(topH,topG) ? topH : topG;
639  }
640 
641  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS */
642  if (topF == v) {
643  Fneg_v = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
644  Fv = BiddyT(f);
645  } else {
646  Fv = biddyZero;
647  Fneg_v = f;
648  }
649  if (topG == v) {
650  Gneg_v = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
651  Gv = BiddyT(g);
652  } else {
653  Gv = biddyZero;
654  Gneg_v = g;
655  }
656  if (topH == v) {
657  Hneg_v = Biddy_InvCond(BiddyE(h),Biddy_GetMark(h));
658  Hv = BiddyT(h);
659  } else {
660  Hv = biddyZero;
661  Hneg_v = h;
662  }
663 
664  rtag = v;
665 
666  }
667 
668  else if (biddyManagerType == BIDDYTYPETZBDD) {
669 
670  /* LOOKING FOR THE SMALLEST TAG AND THE SMALLEST TOP VARIABLE */
671  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
672  tagF = Biddy_GetTag(f);
673  tagG = Biddy_GetTag(g);
674  tagH = Biddy_GetTag(h);
675  topF = BiddyV(f);
676  topG = BiddyV(g);
677  topH = BiddyV(h);
678 
679  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
680  if (BiddyIsSmaller(tagF,tagG)) {
681  rtag = BiddyIsSmaller(tagF,tagH) ? tagF : tagH;
682  } else {
683  rtag = BiddyIsSmaller(tagH,tagG) ? tagH : tagG;
684  }
685  if (BiddyIsSmaller(topF,topG)) {
686  v = BiddyIsSmaller(topF,topH) ? topF : topH;
687  } else {
688  v = BiddyIsSmaller(topH,topG) ? topH : topG;
689  }
690 
691  if ((tagF != tagG) || (tagF != tagH)) v = rtag;
692 
693  if (tagF == rtag) {
694  if (topF == v) {
695  Fneg_v = BiddyE(f);
696  Fv = BiddyT(f);
697  } else {
698  Fneg_v = f;
699  Biddy_SetTag(Fneg_v,v);
700  Fneg_v = Biddy_Managed_IncTag(MNG,Fneg_v);
701  Fv = biddyZero;
702  }
703  } else {
704  Fneg_v = Fv = f;
705  }
706  if (tagG == rtag) {
707  if (topG == v) {
708  Gneg_v = BiddyE(g);
709  Gv = BiddyT(g);
710  } else {
711  Gneg_v = g;
712  Biddy_SetTag(Gneg_v,v);
713  Gneg_v = Biddy_Managed_IncTag(MNG,Gneg_v);
714  Gv = biddyZero;
715  }
716  } else {
717  Gneg_v = Gv = g;
718  }
719  if (tagH == rtag) {
720  if (topH == v) {
721  Hneg_v = BiddyE(h);
722  Hv = BiddyT(h);
723  } else {
724  Hneg_v = h;
725  Biddy_SetTag(Hneg_v,v);
726  Hneg_v = Biddy_Managed_IncTag(MNG,Hneg_v);
727  Hv = biddyZero;
728  }
729  } else {
730  Hneg_v = Hv = h;
731  }
732 
733  }
734 
735  /* RECURSIVE CALLS */
736  if (Fneg_v == biddyOne) {
737  E = Gneg_v;
738  } else if (Fneg_v == biddyZero) {
739  E = Hneg_v;
740  } else if (Gneg_v == Hneg_v) {
741  E = Gneg_v;
742  } else {
743  E = BiddyManagedITE(MNG,Fneg_v,Gneg_v,Hneg_v);
744  }
745  if (Fv == biddyOne) {
746  T = Gv;
747  } else if (Fv == biddyZero) {
748  T = Hv;
749  } else if (Gv == Hv) {
750  T = Gv;
751  } else {
752  T = BiddyManagedITE(MNG,Fv,Gv,Hv);
753  }
754 
755  r = BiddyManagedTaggedFoaNode(MNG,v,E,T,rtag,TRUE);
756  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
757 
758  /* CACHE EVERYTHING */
759  if (NN) {
760  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,Biddy_Inv(r),cindex);
761  } else {
762  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,r,cindex);
763  }
764 
765  /* DEBUGGING */
766  /*
767  printf("ITE has not used cache\n");
768  */
769 
770  } else {
771 
772  if (NN) {
773  Biddy_InvertMark(r);
774  }
775 
776  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
777  BiddyRefresh(r);
778 
779  }
780 
781  /* DEBUGGING */
782  /*
783  printf("BiddyManagedITE: (%d) result\n",nn);
784  Biddy_Managed_PrintfBDD(MNG,r);
785  */
786 
787  return r;
788 }
789 
790 /***************************************************************************/
807 #ifdef __cplusplus
808 extern "C" {
809 #endif
810 
813 {
814  Biddy_Edge r;
815 
816  assert( f != NULL );
817  assert( g != NULL );
818 
819  if (!MNG) MNG = biddyAnonymousManager;
820  ZF_LOGI("Biddy_And");
821 
822  assert( BiddyIsOK(f) == TRUE );
823  assert( BiddyIsOK(g) == TRUE );
824 
825  biddyNodeTable.funandor++;
826 
827  r = biddyNull;
828 
829  if (biddyManagerType == BIDDYTYPEOBDD) {
830  /* IMPLEMENTED */
831  r = BiddyManagedAnd(MNG,f,g);
832  BiddyRefresh(r); /* not always refreshed by BiddyManagedAnd */
833  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
834  /* IMPLEMENTED */
835  r = BiddyManagedAnd(MNG,f,g);
836  BiddyRefresh(r); /* not always refreshed by BiddyManagedAnd */
837  } else if (biddyManagerType == BIDDYTYPEZBDD) {
838  /* IMPLEMENTED */
839  r = BiddyManagedAnd(MNG,f,g);
840  BiddyRefresh(r); /* not always refreshed by BiddyManagedAnd */
841  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
842  /* IMPLEMENTED */
843  r = BiddyManagedAnd(MNG,f,g);
844  BiddyRefresh(r); /* not always refreshed by BiddyManagedAnd */
845  } else if (biddyManagerType == BIDDYTYPETZBDD) {
846  /* IMPLEMENTED */
847  r = BiddyManagedAnd(MNG,f,g);
848  BiddyRefresh(r); /* not always refreshed by BiddyManagedAnd */
849  } else if (biddyManagerType == BIDDYTYPETZBDDC)
850  {
851  fprintf(stderr,"Biddy_And: this BDD type is not supported, yet!\n");
852  return biddyNull;
853  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
854  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
855  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
856  {
857  fprintf(stderr,"Biddy_And: this BDD type is not supported, yet!\n");
858  return biddyNull;
859  } else {
860  fprintf(stderr,"Biddy_And: Unsupported BDD type!\n");
861  return biddyNull;
862  }
863 
864  return r;
865 }
866 
867 #ifdef __cplusplus
868 }
869 #endif
870 
872 BiddyManagedAnd(const Biddy_Manager MNG, const Biddy_Edge f, const Biddy_Edge g)
873 {
874  Biddy_Edge r, T, E, Fv, Gv, Fneg_v, Gneg_v;
875  Biddy_Edge FF, GG, HH;
876  Biddy_Boolean NN;
877  Biddy_Variable v,rtag;
878  unsigned int cindex;
879 
880  static Biddy_Variable topF; /* CAN BE STATIC, WHAT IS BETTER? */
881  static Biddy_Variable topG; /* CAN BE STATIC, WHAT IS BETTER? */
882  static Biddy_Variable tagF; /* CAN BE STATIC, WHAT IS BETTER? */
883  static Biddy_Variable tagG; /* CAN BE STATIC, WHAT IS BETTER? */
884 
885  assert( MNG != NULL );
886  assert( f != NULL );
887  assert( g != NULL );
888 
889  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
890  assert(
891  (biddyManagerType == BIDDYTYPEOBDD) ||
892  (biddyManagerType == BIDDYTYPEOBDDC) ||
893  (biddyManagerType == BIDDYTYPEZBDD) ||
894  (biddyManagerType == BIDDYTYPEZBDDC) ||
895  (biddyManagerType == BIDDYTYPETZBDD)
896  );
897 
898 #ifdef BIDDYEXTENDEDSTATS_YES
899  biddyNodeTable.andorrecursive++;
900 #endif
901 
902  /* LOOKING FOR SIMPLE CASE */
903  if (f == biddyZero) {
904  return biddyZero;
905  } else if (g == biddyZero) {
906  return biddyZero;
907  } else if (f == biddyOne) {
908  return g;
909  } else if (g == biddyOne) {
910  return f;
911  } else if (f == g) {
912  return f;
913  }
914 
915  if (biddyManagerType == BIDDYTYPEOBDDC) {
916  if (Biddy_IsEqvPointer(f,g)) {
917  return biddyZero;
918  }
919  }
920 
921  else if (biddyManagerType == BIDDYTYPETZBDD) {
922  if (BiddyR(f) == BiddyR(g)) {
923  if (BiddyIsSmaller(Biddy_GetTag(f),Biddy_GetTag(g))) {
924  return f;
925  } else {
926  return g;
927  }
928  }
929  }
930 
931  /* THIS IS NOT A SIMPLE CASE */
932 
933  FF = GG = HH = biddyNull;
934  NN = FALSE;
935  Fneg_v = Fv = biddyNull;
936  Gneg_v = Gv = biddyNull;
937  rtag = 0;
938  v = 0;
939 
940  /* NORMALIZATION OF COMPLEMENTED EDGES */
941  /* FF, GG, and HH ARE USED FOR CACHE LOOKUP, ONLY */
942  /* FF AND GG SHOULD NOT BE COMPLEMENTED */
943  /* ((uintptr_t) f) SHOULD BE GREATER THAN ((uintptr_t) g) */
944 
945  if (biddyManagerType == BIDDYTYPEOBDDC) {
946 
947  if (((uintptr_t) f) > ((uintptr_t) g)) {
948  if (Biddy_GetMark(f)) {
949  NN = TRUE;
950  FF = Biddy_Inv(f);
951  GG = biddyOne; /* Biddy_Inv(h) */
952  HH = Biddy_Inv(g);
953  } else {
954  if (Biddy_GetMark(g)) {
955  NN = TRUE;
956  FF = f;
957  GG = Biddy_Inv(g);
958  HH = biddyOne; /* Biddy_Inv(h) */
959  } else {
960  FF = f;
961  GG = g;
962  HH = biddyZero; /* h */
963  }
964  }
965  } else {
966  if (Biddy_GetMark(g)) {
967  NN = TRUE;
968  FF = Biddy_Inv(g);
969  GG = biddyOne; /* Biddy_Inv(h) */
970  HH = Biddy_Inv(f);
971  } else {
972  if (Biddy_GetMark(f)) {
973  NN = TRUE;
974  FF = g;
975  GG = Biddy_Inv(f);
976  HH = biddyOne; /* Biddy_Inv(h) */
977  } else {
978  FF = g;
979  GG = f;
980  HH = biddyZero; /* h */
981  }
982  }
983  }
984 
985  }
986 
987  else {
988 
989  /* THIS IS NOT ITE CACHE! */
990 
991  if (((uintptr_t) f) > ((uintptr_t) g)) {
992  FF = f;
993  GG = g;
994  HH = biddyZero;
995  } else {
996  FF = g;
997  GG = f;
998  HH = biddyZero;
999  }
1000 
1001  }
1002 
1003  /* IF RESULT IS NOT IN THE CACHE TABLE... */
1004  /* FOR ZBDDs, NOT EVERYTHING IS CACHED */
1005  cindex = 0;
1006  if ((((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) &&
1007  ((topF = BiddyV(f)) != (topG = BiddyV(g)))
1008  ) || !findOp3Cache(MNG,biddyOPCache,FF,GG,HH,&r,&cindex))
1009  {
1010 
1011  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1012 
1013  /* LOOKING FOR THE SMALLEST TOP VARIABLE */
1014  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
1015  topF = BiddyV(f);
1016  topG = BiddyV(g);
1017  v = BiddyIsSmaller(topF,topG) ? topF : topG;
1018 
1019  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS */
1020  /* COMPLEMENTED EDGES MUST BE TRANSFERED */
1021 
1022  if (topF == v) {
1023  Fneg_v = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
1024  Fv = Biddy_InvCond(BiddyT(f),Biddy_GetMark(f));
1025  } else {
1026  Fneg_v = Fv = f;
1027  }
1028 
1029  if (topG == v) {
1030  Gneg_v = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
1031  Gv = Biddy_InvCond(BiddyT(g),Biddy_GetMark(g));
1032  } else {
1033  Gneg_v = Gv = g;
1034  }
1035 
1036  rtag = v;
1037 
1038  }
1039 
1040  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
1041 
1042  /* LOOKING FOR THE SMALLEST TOP VARIABLE */
1043  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
1044  /* FOR ZBDD, topF AND topG HAVE BEEN ALREADY CALCULATED */
1045  /* topF = BiddyV(f); */ /* ALREADY CALCULATED */
1046  /* topG = BiddyV(g); */ /* ALREADY CALCULATED */
1047  v = BiddyIsSmaller(topF,topG) ? topF : topG;
1048 
1049  /* THIS CALL IS NOT INTRODUCING NEW NODES */
1050  /* COMPLEMENTED EDGES MUST BE TRANSFERED */
1051  /* IT SEEMS THAT CACHING THIS RESULTS IS NOT A GOOD IDEA */
1052  if (topF != topG) {
1053  if (topF == v) {
1054  r = BiddyManagedAnd(MNG,Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),g);
1055  return r;
1056  } else {
1057  r = BiddyManagedAnd(MNG,f,Biddy_InvCond(BiddyE(g),Biddy_GetMark(g)));
1058  return r;
1059  }
1060  }
1061 
1062  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS, topF == topG */
1063  /* COMPLEMENTED EDGES MUST BE TRANSFERED */
1064  Fneg_v = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
1065  Fv = BiddyT(f);
1066  Gneg_v = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
1067  Gv = BiddyT(g);
1068 
1069  rtag = v;
1070 
1071  }
1072 
1073  else if (biddyManagerType == BIDDYTYPETZBDD) {
1074 
1075  /* LOOKING FOR THE SMALLEST TAG AND SMALLEST TOP VARIABLE */
1076  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
1077  tagF = Biddy_GetTag(f);
1078  tagG = Biddy_GetTag(g);
1079  topF = BiddyV(f);
1080  topG = BiddyV(g);
1081  rtag = BiddyIsSmaller(tagF,tagG) ? tagF : tagG;
1082  v = BiddyIsSmaller(topF,topG) ? topF : topG;
1083 
1084  /* VARIANT 1 */
1085  /*
1086  if (BiddyIsSmaller(topF,tagG)) {
1087  Fneg_v = BiddyE(f);
1088  Fv = BiddyT(f);
1089  Gneg_v = Gv = g;
1090  } else if (BiddyIsSmaller(topG,tagF)) {
1091  Fneg_v = Fv = f;
1092  Gneg_v = BiddyE(g);
1093  Gv = BiddyT(g);
1094  } else {
1095  if (topF == v) {
1096  Fneg_v = BiddyE(f);
1097  Fv = BiddyT(f);
1098  } else {
1099  Fneg_v = f;
1100  Biddy_SetTag(Fneg_v,v);
1101  Fneg_v = Biddy_Managed_IncTag(MNG,Fneg_v);
1102  Fv = biddyZero;
1103  }
1104  if (topG == v) {
1105  Gneg_v = BiddyE(g);
1106  Gv = BiddyT(g);
1107  } else {
1108  Gneg_v = g;
1109  Biddy_SetTag(Gneg_v,v);
1110  Gneg_v = Biddy_Managed_IncTag(MNG,Gneg_v);
1111  Gv = biddyZero;
1112  }
1113  }
1114  */
1115 
1116  /* VARIANT 2 */
1117  /*
1118  if (topF == v) {
1119  Fneg_v = BiddyE(f);
1120  Fv = BiddyT(f);
1121  } else {
1122  if (BiddyIsSmaller(v,tagF)) {
1123  Fneg_v = Fv = f;
1124  } else {
1125  Fneg_v = f;
1126  Biddy_SetTag(Fneg_v,v);
1127  Fneg_v = Biddy_Managed_IncTag(MNG,Fneg_v);
1128  Fv = biddyZero;
1129  }
1130  }
1131  if (topG == v) {
1132  Gneg_v = BiddyE(g);
1133  Gv = BiddyT(g);
1134  } else {
1135  if (BiddyIsSmaller(v,tagG)) {
1136  Gneg_v = Gv = g;
1137  } else {
1138  Gneg_v = g;
1139  Biddy_SetTag(Gneg_v,v);
1140  Gneg_v = Biddy_Managed_IncTag(MNG,Gneg_v);
1141  Gv = biddyZero;
1142  }
1143  }
1144  */
1145 
1146  /* VARIANT 3 */
1147 
1148  if (BiddyIsSmaller(v,tagF)) {
1149  Fneg_v = Fv = f;
1150  } else if (v == topF) {
1151  Fneg_v = BiddyE(f);
1152  Fv = BiddyT(f);
1153  } else {
1154  Fneg_v = f;
1155  Biddy_SetTag(Fneg_v,v);
1156  Fneg_v = Biddy_Managed_IncTag(MNG,Fneg_v);
1157  Fv = biddyZero;
1158  }
1159  if (BiddyIsSmaller(v,tagG)) {
1160  Gneg_v = Gv = g;
1161  } else if (v == topG) {
1162  Gneg_v = BiddyE(g);
1163  Gv = BiddyT(g);
1164  } else {
1165  Gneg_v = g;
1166  Biddy_SetTag(Gneg_v,v);
1167  Gneg_v = Biddy_Managed_IncTag(MNG,Gneg_v);
1168  Gv = biddyZero;
1169  }
1170 
1171 
1172  }
1173 
1174  /* RECURSIVE CALLS */
1175  if (Fneg_v == biddyZero) {
1176  E = biddyZero;
1177  } else if (Gneg_v == biddyZero) {
1178  E = biddyZero;
1179  } else if (Fneg_v == biddyOne) {
1180  E = Gneg_v;
1181  } else if (Gneg_v == biddyOne) {
1182  E = Fneg_v;
1183  } else {
1184  E = BiddyManagedAnd(MNG,Fneg_v,Gneg_v);
1185  }
1186  if (Fv == biddyZero) {
1187  T = biddyZero;
1188  } else if (Gv == biddyZero) {
1189  T = biddyZero;
1190  } else if (Fv == biddyOne) {
1191  T = Gv;
1192  } else if (Gv == biddyOne) {
1193  T = Fv;
1194  } else {
1195  T = BiddyManagedAnd(MNG,Fv,Gv);
1196  }
1197 
1198  r = BiddyManagedTaggedFoaNode(MNG,v,E,T,rtag,TRUE);
1199  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
1200 
1201  if (NN) {
1202  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,Biddy_Inv(r),cindex);
1203  } else {
1204  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,r,cindex);
1205  }
1206 
1207  } else {
1208 
1209  if (NN) {
1210  Biddy_InvertMark(r);
1211  }
1212 
1213  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
1214  BiddyRefresh(r);
1215 
1216  }
1217 
1218  return r;
1219 
1220 }
1221 
1222 /***************************************************************************/
1238 #ifdef __cplusplus
1239 extern "C" {
1240 #endif
1241 
1242 Biddy_Edge
1244 {
1245  Biddy_Edge r;
1246 
1247  assert( f != NULL );
1248  assert( g != NULL );
1249 
1250  if (!MNG) MNG = biddyAnonymousManager;
1251  ZF_LOGI("Biddy_Or");
1252 
1253  assert( BiddyIsOK(f) == TRUE );
1254  assert( BiddyIsOK(g) == TRUE );
1255 
1256  biddyNodeTable.funandor++;
1257 
1258  r = biddyNull;
1259 
1260  if (biddyManagerType == BIDDYTYPEOBDD) {
1261  /* PROCEED BY CALCULATING NOT-AND */
1262  /*
1263  r = BiddyManagedNot(MNG,BiddyManagedAnd(MNG,BiddyManagedNot(MNG,f),BiddyManagedNot(MNG,g)));
1264  */
1265  /* PROCEED BY CALCULATING XOR-AND */
1266  /*
1267  r = BiddyManagedXor(MNG,BiddyManagedXor(MNG,f,g),BiddyManagedAnd(MNG,f,g));
1268  */
1269  /* IMPLEMENTED */
1270  r = BiddyManagedOr(MNG,f,g);
1271  BiddyRefresh(r); /* not always refreshed by BiddyManagedOr */
1272  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
1273  /* PROCEED BY CALCULATING NOT-AND */
1274  /*
1275  r = Biddy_Inv(BiddyManagedAnd(MNG,Biddy_Inv(f),Biddy_Inv(g)));
1276  */
1277  /* PROCEED BY CALCULATING XOR-AND */
1278  /*
1279  r = BiddyManagedXor(MNG,BiddyManagedXor(MNG,f,g),BiddyManagedAnd(MNG,f,g));
1280  */
1281  /* IMPLEMENTED */
1282  r = BiddyManagedOr(MNG,f,g);
1283  BiddyRefresh(r); /* not always refreshed by BiddyManagedOr */
1284  } else if (biddyManagerType == BIDDYTYPEZBDD) {
1285  /* PROCEED BY CALCULATING NOT-AND */
1286  /*
1287  r = BiddyManagedNot(MNG,BiddyManagedAnd(MNG,BiddyManagedNot(MNG,f),BiddyManagedNot(MNG,g)));
1288  */
1289  /* PROCEED BY CALCULATING XOR-AND */
1290  /*
1291  r = BiddyManagedXor(MNG,BiddyManagedXor(MNG,f,g),BiddyManagedAnd(MNG,f,g));
1292  */
1293  /* IMPLEMENTED */
1294  r = BiddyManagedOr(MNG,f,g);
1295  BiddyRefresh(r); /* not always refreshed by BiddyManagedOr */
1296  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
1297  /* PROCEED BY CALCULATING NOT-AND */
1298  /*
1299  r = BiddyManagedNot(MNG,BiddyManagedAnd(MNG,BiddyManagedNot(MNG,f),BiddyManagedNot(MNG,g)));
1300  */
1301  /* PROCEED BY CALCULATING XOR-AND */
1302  /*
1303  r = BiddyManagedXor(MNG,BiddyManagedXor(MNG,f,g),BiddyManagedAnd(MNG,f,g));
1304  */
1305  /* IMPLEMENTED */
1306  r = BiddyManagedOr(MNG,f,g);
1307  BiddyRefresh(r); /* not always refreshed by BiddyManagedOr */
1308  } else if (biddyManagerType == BIDDYTYPETZBDD) {
1309  /* PROCEED BY CALCULATING NOT-AND */
1310  /*
1311  r = BiddyManagedNot(MNG,BiddyManagedAnd(MNG,BiddyManagedNot(MNG,f),BiddyManagedNot(MNG,g)));
1312  */
1313  /* PROCEED BY CALCULATING XOR-AND */
1314  /*
1315  r = BiddyManagedXor(MNG,BiddyManagedXor(MNG,f,g),BiddyManagedAnd(MNG,f,g));
1316  */
1317  /* IMPLEMENTED */
1318  r = BiddyManagedOr(MNG,f,g);
1319  BiddyRefresh(r); /* not always refreshed by BiddyManagedOr */
1320  } else if (biddyManagerType == BIDDYTYPETZBDDC)
1321  {
1322  fprintf(stderr,"Biddy_Or: this BDD type is not supported, yet!\n");
1323  return biddyNull;
1324  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
1325  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
1326  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
1327  {
1328  fprintf(stderr,"Biddy_Or: this BDD type is not supported, yet!\n");
1329  return biddyNull;
1330  } else {
1331  fprintf(stderr,"Biddy_Or: Unsupported BDD type!\n");
1332  return biddyNull;
1333  }
1334 
1335  return r;
1336 }
1337 
1338 #ifdef __cplusplus
1339 }
1340 #endif
1341 
1342 Biddy_Edge
1343 BiddyManagedOr(const Biddy_Manager MNG, const Biddy_Edge f, const Biddy_Edge g)
1344 {
1345  Biddy_Edge r, T, E, Fv, Gv, Fneg_v, Gneg_v;
1346  Biddy_Edge FF, GG, HH;
1347  Biddy_Boolean NN;
1348  Biddy_Variable v,rtag;
1349  unsigned int cindex;
1350 
1351  static Biddy_Variable topF; /* CAN BE STATIC, WHAT IS BETTER? */
1352  static Biddy_Variable topG; /* CAN BE STATIC, WHAT IS BETTER? */
1353  static Biddy_Variable tagF; /* CAN BE STATIC, WHAT IS BETTER? */
1354  static Biddy_Variable tagG; /* CAN BE STATIC, WHAT IS BETTER? */
1355 
1356  assert( MNG != NULL );
1357  assert( f != NULL );
1358  assert( g != NULL );
1359 
1360  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
1361  assert(
1362  (biddyManagerType == BIDDYTYPEOBDD) ||
1363  (biddyManagerType == BIDDYTYPEOBDDC) ||
1364  (biddyManagerType == BIDDYTYPEZBDD) ||
1365  (biddyManagerType == BIDDYTYPEZBDDC) ||
1366  (biddyManagerType == BIDDYTYPETZBDD)
1367  );
1368 
1369 #ifdef BIDDYEXTENDEDSTATS_YES
1370  biddyNodeTable.andorrecursive++;
1371 #endif
1372 
1373  r = biddyNull;
1374 
1375  /* LOOKING FOR SIMPLE CASE */
1376  /* returning biddyOne in a recursive call is wrong for ZBDD and ZBDDC, */
1377  /* because top variable of the result may be lower (topmore) than top variables of the arguments */
1378  /* (i.e. because the result depends on domain) */
1379 
1380  if (f == biddyZero) {
1381  return g;
1382  } else if (g == biddyZero) {
1383  return f;
1384  } else if (f == biddyOne) {
1385  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
1386  return biddyOne;
1387  } else if (g == biddyOne) {
1388  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
1389  return biddyOne;
1390  } else if (f == g) {
1391  return f;
1392  }
1393 
1394  if (biddyManagerType == BIDDYTYPEOBDDC) {
1395  if (Biddy_IsEqvPointer(f,g)) {
1396  return biddyOne;
1397  }
1398  }
1399 
1400  if (biddyManagerType == BIDDYTYPETZBDD) {
1401  if (BiddyR(f) == BiddyR(g)) {
1402  if (BiddyIsSmaller(Biddy_GetTag(f),Biddy_GetTag(g))) {
1403  return g;
1404  } else {
1405  return f;
1406  }
1407  }
1408  }
1409 
1410  /* THIS IS NOT A SIMPLE CASE */
1411 
1412  FF = GG = HH = biddyNull;
1413  NN = FALSE;
1414  Fneg_v = Fv = biddyNull;
1415  Gneg_v = Gv = biddyNull;
1416  rtag = 0;
1417  v = 0;
1418 
1419  /* NORMALIZATION OF COMPLEMENTED EDGES */
1420  /* FF, GG, and HH ARE USED FOR CACHE LOOKUP, ONLY */
1421  /* FF AND GG SHOULD NOT BE COMPLEMENTED */
1422  /* ((uintptr_t) f) SHOULD BE GREATER THAN ((uintptr_t) g) */
1423 
1424  if (biddyManagerType == BIDDYTYPEOBDDC) {
1425 
1426  if (((uintptr_t) f) > ((uintptr_t) g)) {
1427  if (Biddy_GetMark(f)) {
1428  if (Biddy_GetMark(g)) {
1429  NN = TRUE;
1430  FF = Biddy_Inv(f);
1431  GG = Biddy_Inv(g);
1432  HH = biddyZero; /* Biddy_Inv(g) */
1433  } else {
1434  FF = Biddy_Inv(f);
1435  GG = g;
1436  HH = biddyOne; /* g */
1437  }
1438  } else {
1439  FF = f;
1440  GG = biddyOne;
1441  HH = g;
1442  }
1443  } else {
1444  if (Biddy_GetMark(g)) {
1445  if (Biddy_GetMark(f)) {
1446  NN = TRUE;
1447  FF = Biddy_Inv(g);
1448  GG = Biddy_Inv(f);
1449  HH = biddyZero; /* Biddy_Inv(g) */
1450  } else {
1451  FF = Biddy_Inv(g);
1452  GG = f;
1453  HH = biddyOne; /* g */
1454  }
1455  } else {
1456  FF = g;
1457  GG = biddyOne;
1458  HH = f;
1459  }
1460  }
1461  }
1462 
1463  else {
1464 
1465  /* THIS IS NOT ITE CACHE! */
1466 
1467  if (((uintptr_t) f) > ((uintptr_t) g)) {
1468  FF = biddyZero;
1469  GG = f;
1470  HH = g;
1471  } else {
1472  FF = biddyZero;
1473  GG = g;
1474  HH = f;
1475  }
1476 
1477  }
1478 
1479  /* IF RESULT IS NOT IN THE CACHE TABLE... */
1480  cindex = 0;
1481  if (!findOp3Cache(MNG,biddyOPCache,FF,GG,HH,&r,&cindex))
1482  {
1483 
1484  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
1485 
1486  /* LOOKING FOR THE SMALLEST TOP VARIABLE */
1487  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
1488  topF = BiddyV(f);
1489  topG = BiddyV(g);
1490  v = BiddyIsSmaller(topF,topG) ? topF : topG;
1491 
1492  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS */
1493  /* COMPLEMENTED EDGES MUST BE TRANSFERED */
1494  if (topF == v) {
1495  Fneg_v = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
1496  Fv = Biddy_InvCond(BiddyT(f),Biddy_GetMark(f));
1497  } else {
1498  Fneg_v = Fv = f;
1499  }
1500 
1501  if (topG == v) {
1502  Gneg_v = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
1503  Gv = Biddy_InvCond(BiddyT(g),Biddy_GetMark(g));
1504  } else {
1505  Gneg_v = Gv = g;
1506  }
1507 
1508  rtag = v;
1509 
1510  }
1511 
1512  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
1513 
1514  /* LOOKING FOR THE SMALLEST TOP VARIABLE */
1515  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
1516  topF = BiddyV(f);
1517  topG = BiddyV(g);
1518  v = BiddyIsSmaller(topF,topG) ? topF : topG;
1519 
1520  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS */
1521  /* COMPLEMENTED EDGES MUST BE TRANSFERED */
1522  if (topF == v) {
1523  Fneg_v = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
1524  Fv = BiddyT(f);
1525  } else {
1526  Fneg_v = f;
1527  Fv = biddyZero;
1528  }
1529  if (topG == v) {
1530  Gneg_v = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
1531  Gv = BiddyT(g);
1532  } else {
1533  Gneg_v = g;
1534  Gv = biddyZero;
1535  }
1536 
1537  rtag = v;
1538 
1539  }
1540 
1541  else if (biddyManagerType == BIDDYTYPETZBDD) {
1542 
1543  /* VARIANT 1 */
1544  /*
1545  tagF = Biddy_GetTag(f);
1546  tagG = Biddy_GetTag(g);
1547  if (tagF == tagG) {
1548  / * THE SAME TAG * /
1549  topF = BiddyV(f);
1550  topG = BiddyV(g);
1551  v = BiddyIsSmaller(topF,topG) ? topF : topG;
1552  rtag = tagF;
1553  w = v;
1554  if (topF == v) {
1555  Fneg_v = BiddyE(f);
1556  Fv = BiddyT(f);
1557  } else {
1558  Fneg_v = f;
1559  Biddy_SetTag(Fneg_v,v);
1560  Fneg_v = Biddy_Managed_IncTag(MNG,Fneg_v);
1561  Fv = biddyZero;
1562  }
1563  if (topG == v) {
1564  Gneg_v = BiddyE(g);
1565  Gv = BiddyT(g);
1566  } else {
1567  Gneg_v = g;
1568  Biddy_SetTag(Gneg_v,v);
1569  Gneg_v = Biddy_Managed_IncTag(MNG,Gneg_v);
1570  Gv = biddyZero;
1571  }
1572  } else {
1573  / * DIFFERENT TAG * /
1574  rtag = BiddyIsSmaller(tagF,tagG) ? tagF : tagG;
1575  w = rtag;
1576  if (tagF == rtag) {
1577  if (BiddyV(f) == rtag) {
1578  / * TAG AND TOP VARIABLE ARE EQUAL * /
1579  Fneg_v = BiddyE(f);
1580  Fv = BiddyT(f);
1581  } else {
1582  / * TAG AND TOP VARIABLE ARE NOT EQUAL * /
1583  Fneg_v = f;
1584  Biddy_SetTag(Fneg_v,rtag);
1585  Fneg_v = Biddy_Managed_IncTag(MNG,Fneg_v);
1586  Fv = biddyZero;
1587  }
1588  Gneg_v = Gv = g;
1589  } else {
1590  if (BiddyV(g) == rtag) {
1591  / * TAG AND TOP VARIABLE ARE EQUAL * /
1592  Gneg_v = BiddyE(g);
1593  Gv = BiddyT(g);
1594  } else {
1595  / * TAG AND TOP VARIABLE ARE NOT EQUAL * /
1596  Gneg_v = g;
1597  Biddy_SetTag(Gneg_v,rtag);
1598  Gneg_v = Biddy_Managed_IncTag(MNG,Gneg_v);
1599  Gv = biddyZero;
1600  }
1601  Fneg_v = Fv = f;
1602  }
1603  }
1604  */
1605 
1606  /* VARIANT 2 */
1607 
1608  tagF = Biddy_GetTag(f);
1609  tagG = Biddy_GetTag(g);
1610  topF = BiddyV(f);
1611  topG = BiddyV(g);
1612  rtag = BiddyIsSmaller(tagF,tagG) ? tagF : tagG;
1613  v = BiddyIsSmaller(topF,topG) ? topF : topG;
1614  if (tagF != tagG) v = rtag;
1615  if (tagF == rtag) {
1616  if (topF == v) {
1617  Fneg_v = BiddyE(f);
1618  Fv = BiddyT(f);
1619  } else {
1620  Fneg_v = f;
1621  Biddy_SetTag(Fneg_v,v);
1622  Fneg_v = Biddy_Managed_IncTag(MNG,Fneg_v);
1623  Fv = biddyZero;
1624  }
1625  } else {
1626  Fneg_v = Fv = f;
1627  }
1628  if (tagG == rtag) {
1629  if (topG == v) {
1630  Gneg_v = BiddyE(g);
1631  Gv = BiddyT(g);
1632  } else {
1633  Gneg_v = g;
1634  Biddy_SetTag(Gneg_v,v);
1635  Gneg_v = Biddy_Managed_IncTag(MNG,Gneg_v);
1636  Gv = biddyZero;
1637  }
1638  } else {
1639  Gneg_v = Gv = g;
1640  }
1641 
1642 
1643  }
1644 
1645  /* RECURSIVE CALLS */
1646  /* returning biddyOne in a recursive call is wrong for ZBDD and ZBDDC, */
1647  /* because top variable of the result may be lower (topmore) than top variables of the arguments */
1648  /* (i.e. because the result depends on domain) */
1649  if (Fneg_v == biddyZero) {
1650  E = Gneg_v;
1651  } else if (Gneg_v == biddyZero) {
1652  E = Fneg_v;
1653  } else if (Fneg_v == biddyOne) {
1654  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
1655  E = biddyOne;
1656  } else if (Gneg_v == biddyOne) {
1657  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
1658  E = biddyOne;
1659  } else {
1660  E = BiddyManagedOr(MNG,Fneg_v,Gneg_v);
1661  }
1662  if (Fv == biddyZero) {
1663  T = Gv;
1664  } else if (Gv == biddyZero) {
1665  T = Fv;
1666  } else if (Fv == biddyOne) {
1667  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
1668  T = biddyOne;
1669  } else if (Gv == biddyOne) {
1670  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
1671  T = biddyOne;
1672  } else {
1673  T = BiddyManagedOr(MNG,Fv,Gv);
1674  }
1675 
1676  r = BiddyManagedTaggedFoaNode(MNG,v,E,T,rtag,TRUE);
1677  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
1678 
1679  if (NN) {
1680  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,Biddy_Inv(r),cindex);
1681  } else {
1682  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,r,cindex);
1683  }
1684 
1685  } else {
1686 
1687  if (NN) {
1688  Biddy_InvertMark(r);
1689  }
1690 
1691  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
1692  BiddyRefresh(r);
1693 
1694  }
1695 
1696  return r;
1697 }
1698 
1699 /***************************************************************************/
1713 #ifdef __cplusplus
1714 extern "C" {
1715 #endif
1716 
1717 Biddy_Edge
1719 {
1720  Biddy_Edge r;
1721 
1722  assert( f != NULL );
1723  assert( g != NULL );
1724 
1725  if (!MNG) MNG = biddyAnonymousManager;
1726  ZF_LOGI("Biddy_Nand");
1727 
1728  assert( BiddyIsOK(f) == TRUE );
1729  assert( BiddyIsOK(g) == TRUE );
1730 
1731  r = biddyNull;
1732 
1733  if (biddyManagerType == BIDDYTYPEOBDD) {
1734  /* PROTOTYPED */
1735  r = BiddyManagedNot(MNG,BiddyManagedAnd(MNG,f,g));
1736  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
1737  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
1738  /* IMPLEMENTED */
1739  r = BiddyManagedNand(MNG,f,g);
1740  BiddyRefresh(r); /* not always refreshed by BiddyManagedNand */
1741  } else if (biddyManagerType == BIDDYTYPEZBDD) {
1742  /* PROTOTYPED */
1743  r = BiddyManagedNot(MNG,BiddyManagedAnd(MNG,f,g));
1744  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
1745  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
1746  /* PROTOTYPED */
1747  r = BiddyManagedNot(MNG,BiddyManagedAnd(MNG,f,g));
1748  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
1749  } else if (biddyManagerType == BIDDYTYPETZBDD) {
1750  /* PROTOTYPED */
1751  r = BiddyManagedNot(MNG,BiddyManagedAnd(MNG,f,g));
1752  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
1753  } else if (biddyManagerType == BIDDYTYPETZBDDC)
1754  {
1755  fprintf(stderr,"Biddy_Nand: this BDD type is not supported, yet!\n");
1756  return biddyNull;
1757  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
1758  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
1759  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
1760  {
1761  fprintf(stderr,"Biddy_Nand: this BDD type is not supported, yet!\n");
1762  return biddyNull;
1763  } else {
1764  fprintf(stderr,"Biddy_Nand: Unsupported BDD type!\n");
1765  return biddyNull;
1766  }
1767 
1768  return r;
1769 }
1770 
1771 #ifdef __cplusplus
1772 }
1773 #endif
1774 
1775 Biddy_Edge
1776 BiddyManagedNand(const Biddy_Manager MNG, const Biddy_Edge f,
1777  const Biddy_Edge g)
1778 {
1779  Biddy_Edge r;
1780 
1781  assert( MNG != NULL );
1782  assert( f != NULL );
1783  assert( g != NULL );
1784 
1785  /* IMPLEMENTED FOR OBDDC, ONLY */
1786  assert( biddyManagerType == BIDDYTYPEOBDDC );
1787 
1788  r = biddyNull;
1789 
1790  if (biddyManagerType == BIDDYTYPEOBDDC) {
1791  r = Biddy_Inv(BiddyManagedAnd(MNG,f,g));
1792  }
1793 
1794  return r;
1795 }
1796 
1797 /***************************************************************************/
1811 #ifdef __cplusplus
1812 extern "C" {
1813 #endif
1814 
1815 Biddy_Edge
1817 {
1818  Biddy_Edge r;
1819 
1820  assert( f != NULL );
1821  assert( g != NULL );
1822 
1823  if (!MNG) MNG = biddyAnonymousManager;
1824  ZF_LOGI("Biddy_Nor");
1825 
1826  assert( BiddyIsOK(f) == TRUE );
1827  assert( BiddyIsOK(g) == TRUE );
1828 
1829  r = biddyNull;
1830 
1831  if (biddyManagerType == BIDDYTYPEOBDD) {
1832  /* PROTOTYPED */
1833  r = BiddyManagedNot(MNG,BiddyManagedOr(MNG,f,g));
1834  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
1835  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
1836  /* IMPLEMENTED */
1837  r = BiddyManagedNor(MNG,f,g);
1838  BiddyRefresh(r); /* not always refreshed by BiddyManagedNor */
1839  } else if (biddyManagerType == BIDDYTYPEZBDD) {
1840  /* PROTOTYPED */
1841  r = BiddyManagedNot(MNG,BiddyManagedOr(MNG,f,g));
1842  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
1843  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
1844  /* PROTOTYPED */
1845  r = BiddyManagedNot(MNG,BiddyManagedOr(MNG,f,g));
1846  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
1847  } else if (biddyManagerType == BIDDYTYPETZBDD) {
1848  /* PROTOTYPED */
1849  r = BiddyManagedNot(MNG,BiddyManagedOr(MNG,f,g));
1850  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
1851  } else if (biddyManagerType == BIDDYTYPETZBDDC)
1852  {
1853  fprintf(stderr,"Biddy_Nor: this BDD type is not supported, yet!\n");
1854  return biddyNull;
1855  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
1856  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
1857  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
1858  {
1859  fprintf(stderr,"Biddy_Nor: this BDD type is not supported, yet!\n");
1860  return biddyNull;
1861  } else {
1862  fprintf(stderr,"Biddy_Nor: Unsupported BDD type!\n");
1863  return biddyNull;
1864  }
1865 
1866  return r;
1867 }
1868 
1869 #ifdef __cplusplus
1870 }
1871 #endif
1872 
1873 Biddy_Edge
1874 BiddyManagedNor(const Biddy_Manager MNG, const Biddy_Edge f,
1875  const Biddy_Edge g)
1876 {
1877  Biddy_Edge r;
1878 
1879  assert( MNG != NULL );
1880  assert( f != NULL );
1881  assert( g != NULL );
1882 
1883  /* IMPLEMENTED FOR OBDDC, ONLY */
1884  assert( biddyManagerType == BIDDYTYPEOBDDC );
1885 
1886  r = biddyNull;
1887 
1888  if (biddyManagerType == BIDDYTYPEOBDDC) {
1889  r = BiddyManagedAnd(MNG,Biddy_Inv(f),Biddy_Inv(g));
1890  }
1891 
1892  return r;
1893 }
1894 
1895 /***************************************************************************/
1908 #ifdef __cplusplus
1909 extern "C" {
1910 #endif
1911 
1912 Biddy_Edge
1914 {
1915  Biddy_Edge r;
1916 
1917  assert( f != NULL );
1918  assert( g != NULL );
1919 
1920  if (!MNG) MNG = biddyAnonymousManager;
1921  ZF_LOGI("Biddy_Xor");
1922 
1923  assert( BiddyIsOK(f) == TRUE );
1924  assert( BiddyIsOK(g) == TRUE );
1925 
1926  biddyNodeTable.funxor++;
1927 
1928  r = biddyNull;
1929 
1930  if (biddyManagerType == BIDDYTYPEOBDD) {
1931  /* IMPLEMENTED */
1932  r = BiddyManagedXor(MNG,f,g);
1933  BiddyRefresh(r); /* not always refreshed by BiddyManagedXor */
1934  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
1935  /* IMPLEMENTED */
1936  r = BiddyManagedXor(MNG,f,g);
1937  BiddyRefresh(r); /* not always refreshed by BiddyManagedXor */
1938  } else if (biddyManagerType == BIDDYTYPEZBDD) {
1939  /* IMPLEMENTED */
1940  r = BiddyManagedXor(MNG,f,g);
1941  BiddyRefresh(r); /* not always refreshed by BiddyManagedXor */
1942  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
1943  /* IMPLEMENTED */
1944  r = BiddyManagedXor(MNG,f,g);
1945  BiddyRefresh(r); /* not always refreshed by BiddyManagedXor */
1946  } else if (biddyManagerType == BIDDYTYPETZBDD) {
1947  /* IMPLEMENTED */
1948  r = BiddyManagedXor(MNG,f,g);
1949  BiddyRefresh(r); /* not always refreshed by BiddyManagedXor */
1950  } else if (biddyManagerType == BIDDYTYPETZBDDC)
1951  {
1952  fprintf(stderr,"Biddy_Xor: this BDD type is not supported, yet!\n");
1953  return biddyNull;
1954  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
1955  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
1956  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
1957  {
1958  fprintf(stderr,"Biddy_Xor: this BDD type is not supported, yet!\n");
1959  return biddyNull;
1960  } else {
1961  fprintf(stderr,"Biddy_Xor: Unsupported BDD type!\n");
1962  return biddyNull;
1963  }
1964 
1965  return r;
1966 }
1967 
1968 #ifdef __cplusplus
1969 }
1970 #endif
1971 
1972 Biddy_Edge
1973 BiddyManagedXor(const Biddy_Manager MNG, const Biddy_Edge f,
1974  const Biddy_Edge g)
1975 {
1976  Biddy_Edge r, T, E, Fv, Gv, Fneg_v, Gneg_v;
1977  Biddy_Edge FF, GG, HH;
1978  Biddy_Boolean NN;
1979  Biddy_Variable v,rtag;
1980  unsigned int cindex;
1981 
1982  static Biddy_Variable topF; /* CAN BE STATIC, WHAT IS BETTER? */
1983  static Biddy_Variable topG; /* CAN BE STATIC, WHAT IS BETTER? */
1984  static Biddy_Variable tagF; /* CAN BE STATIC, WHAT IS BETTER? */
1985  static Biddy_Variable tagG; /* CAN BE STATIC, WHAT IS BETTER? */
1986 
1987  assert( MNG != NULL );
1988  assert( f != NULL );
1989  assert( g != NULL );
1990 
1991  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
1992  assert(
1993  (biddyManagerType == BIDDYTYPEOBDD) ||
1994  (biddyManagerType == BIDDYTYPEOBDDC) ||
1995  (biddyManagerType == BIDDYTYPEZBDD) ||
1996  (biddyManagerType == BIDDYTYPEZBDDC) ||
1997  (biddyManagerType == BIDDYTYPETZBDD)
1998  );
1999 
2000 #ifdef BIDDYEXTENDEDSTATS_YES
2001  biddyNodeTable.xorrecursive++;
2002 #endif
2003 
2004  /* LOOKING FOR SIMPLE CASE */
2005  /* returning biddyOne in a recursive call is wrong for ZBDD and ZBDDC, */
2006  /* because top variable of the result may be lower (topmore) than top variables of the arguments */
2007  /* (i.e. because the result depends on domain) */
2008 
2009  if (f == biddyZero) {
2010  return g;
2011  } else if (g == biddyZero) {
2012  return f;
2013  } else if (f == biddyOne) {
2014  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
2015  return BiddyManagedNot(MNG,g);
2016  } else if (g == biddyOne) {
2017  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
2018  return BiddyManagedNot(MNG,f);
2019  } else if (f == g) {
2020  return biddyZero;
2021  }
2022 
2023  if (biddyManagerType == BIDDYTYPEOBDDC) {
2024  if (Biddy_IsEqvPointer(f,g)) {
2025  return biddyOne;
2026  }
2027  }
2028 
2029  /* THIS IS NOT A SIMPLE CASE */
2030 
2031  FF = GG = HH = biddyNull;
2032  NN = FALSE;
2033  Fneg_v = Fv = biddyNull;
2034  Gneg_v = Gv = biddyNull;
2035  rtag = 0;
2036  v = 0;
2037 
2038  /* NORMALIZATION OF COMPLEMENTED EDGES */
2039  /* FF, GG, and HH ARE USED FOR CACHE LOOKUP, ONLY */
2040  /* FF AND GG SHOULD NOT BE COMPLEMENTED */
2041  /* ((uintptr_t) f) SHOULD BE GREATER THAN ((uintptr_t) g) */
2042 
2043  if (biddyManagerType == BIDDYTYPEOBDDC) {
2044 
2045  if (((uintptr_t) f) > ((uintptr_t) g)) {
2046  if (Biddy_GetMark(f)) {
2047  if (Biddy_GetMark(g)) {
2048  FF = Biddy_Inv(f);
2049  GG = Biddy_Inv(g); /* h */
2050  HH = g;
2051  } else {
2052  NN = TRUE;
2053  FF = Biddy_Inv(f);
2054  GG = g;
2055  HH = Biddy_Inv(g); /* h */
2056  }
2057  } else {
2058  if (Biddy_GetMark(g)) {
2059  NN = TRUE;
2060  FF = f;
2061  GG = Biddy_Inv(g); /* h */
2062  HH = g;
2063  } else {
2064  FF = f;
2065  GG = g;
2066  HH = Biddy_Inv(g); /* h */
2067  }
2068  }
2069  } else {
2070  if (Biddy_GetMark(g)) {
2071  if (Biddy_GetMark(f)) {
2072  FF = Biddy_Inv(g);
2073  GG = Biddy_Inv(f); /* h */
2074  HH = f;
2075  } else {
2076  NN = TRUE;
2077  FF = Biddy_Inv(g);
2078  GG = f;
2079  HH = Biddy_Inv(f); /* h */
2080  }
2081  } else {
2082  if (Biddy_GetMark(f)) {
2083  NN = TRUE;
2084  FF = g;
2085  GG = Biddy_Inv(f); /* h */
2086  HH = f;
2087  } else {
2088  FF = g;
2089  GG = f;
2090  HH = Biddy_Inv(f); /* h */
2091  }
2092  }
2093  }
2094 
2095  }
2096 
2097  else {
2098 
2099  /* THIS IS NOT ITE CACHE! */
2100 
2101  if (((uintptr_t) f) > ((uintptr_t) g)) {
2102  FF = f;
2103  GG = biddyZero;
2104  HH = g;
2105  } else {
2106  FF = g;
2107  GG = biddyZero;
2108  HH = f;
2109  }
2110 
2111  }
2112 
2113  /* IF RESULT IS NOT IN THE CACHE TABLE... */
2114  cindex = 0;
2115  if (!findOp3Cache(MNG,biddyOPCache,FF,GG,HH,&r,&cindex))
2116  {
2117 
2118  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2119 
2120  /* LOOKING FOR THE SMALLEST TOP VARIABLE */
2121  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
2122  topF = BiddyV(f);
2123  topG = BiddyV(g);
2124  v = BiddyIsSmaller(topF,topG) ? topF : topG;
2125 
2126  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS */
2127  /* COMPLEMENTED EDGES MUST BE TRANSFERED */
2128  if (topF == v) {
2129  Fneg_v = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
2130  Fv = Biddy_InvCond(BiddyT(f),Biddy_GetMark(f));
2131  } else {
2132  Fneg_v = Fv = f;
2133  }
2134  if (topG == v) {
2135  Gneg_v = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
2136  Gv = Biddy_InvCond(BiddyT(g),Biddy_GetMark(g));
2137  } else {
2138  Gneg_v = Gv = g;
2139  }
2140 
2141  rtag = v;
2142 
2143  }
2144 
2145  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2146 
2147  /* LOOKING FOR THE SMALLEST TOP VARIABLE */
2148  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
2149  topF = BiddyV(f);
2150  topG = BiddyV(g);
2151  v = BiddyIsSmaller(topF,topG) ? topF : topG;
2152 
2153  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS */
2154  /* COMPLEMENTED EDGES MUST BE TRANSFERED */
2155  if (topF == v) {
2156  Fneg_v = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
2157  Fv = BiddyT(f);
2158  } else {
2159  Fneg_v = f;
2160  Fv = biddyZero;
2161  }
2162  if (topG == v) {
2163  Gneg_v = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
2164  Gv = BiddyT(g);
2165  } else {
2166  Gneg_v = g;
2167  Gv = biddyZero;
2168  }
2169 
2170  rtag = v;
2171 
2172  }
2173 
2174  else if (biddyManagerType == BIDDYTYPETZBDD) {
2175 
2176  /* VARIANT 1 */
2177  /*
2178  tagF = Biddy_GetTag(f);
2179  tagG = Biddy_GetTag(g);
2180  if (tagF == tagG) {
2181  / * THE SAME TAG * /
2182  topF = BiddyV(f);
2183  topG = BiddyV(g);
2184  v = BiddyIsSmaller(topF,topG) ? topF : topG;
2185  rtag = tagF;
2186  w = v;
2187  if (topF == v) {
2188  Fneg_v = BiddyE(f);
2189  Fv = BiddyT(f);
2190  } else {
2191  Fneg_v = f;
2192  Biddy_SetTag(Fneg_v,v);
2193  Fneg_v = Biddy_Managed_IncTag(MNG,Fneg_v);
2194  Fv = biddyZero;
2195  }
2196  if (topG == v) {
2197  Gneg_v = BiddyE(g);
2198  Gv = BiddyT(g);
2199  } else {
2200  Gneg_v = g;
2201  Biddy_SetTag(Gneg_v,v);
2202  Gneg_v = Biddy_Managed_IncTag(MNG,Gneg_v);
2203  Gv = biddyZero;
2204  }
2205  } else {
2206  / * DIFFERENT TAG * /
2207  rtag = BiddyIsSmaller(tagF,tagG) ? tagF : tagG;
2208  w = rtag;
2209  if (tagF == rtag) {
2210  if (BiddyV(f) == rtag) {
2211  / * TAG AND TOP VARIABLE ARE EQUAL * /
2212  Fneg_v = BiddyE(f);
2213  Fv = BiddyT(f);
2214  } else {
2215  / * TAG AND TOP VARIABLE ARE NOT EQUAL * /
2216  Fneg_v = f;
2217  Biddy_SetTag(Fneg_v,rtag);
2218  Fneg_v = Biddy_Managed_IncTag(MNG,Fneg_v);
2219  Fv = biddyZero;
2220  }
2221  Gneg_v = Gv = g;
2222  } else {
2223  if (BiddyV(g) == rtag) {
2224  / * TAG AND TOP VARIABLE ARE EQUAL * /
2225  Gneg_v = BiddyE(g);
2226  Gv = BiddyT(g);
2227  } else {
2228  / * TAG AND TOP VARIABLE ARE NOT EQUAL * /
2229  Gneg_v = g;
2230  Biddy_SetTag(Gneg_v,rtag);
2231  Gneg_v = Biddy_Managed_IncTag(MNG,Gneg_v);
2232  Gv = biddyZero;
2233  }
2234  Fneg_v = Fv = f;
2235  }
2236  }
2237  */
2238 
2239  /* VARIANT 2 */
2240 
2241  tagF = Biddy_GetTag(f);
2242  tagG = Biddy_GetTag(g);
2243  topF = BiddyV(f);
2244  topG = BiddyV(g);
2245  rtag = BiddyIsSmaller(tagF,tagG) ? tagF : tagG;
2246  v = BiddyIsSmaller(topF,topG) ? topF : topG;
2247  if (tagF != tagG) v = rtag;
2248  if (tagF == rtag) {
2249  if (topF == v) {
2250  Fneg_v = BiddyE(f);
2251  Fv = BiddyT(f);
2252  } else {
2253  Fneg_v = f;
2254  Biddy_SetTag(Fneg_v,v);
2255  Fneg_v = Biddy_Managed_IncTag(MNG,Fneg_v);
2256  Fv = biddyZero;
2257  }
2258  } else {
2259  Fneg_v = Fv = f;
2260  }
2261  if (tagG == rtag) {
2262  if (topG == v) {
2263  Gneg_v = BiddyE(g);
2264  Gv = BiddyT(g);
2265  } else {
2266  Gneg_v = g;
2267  Biddy_SetTag(Gneg_v,v);
2268  Gneg_v = Biddy_Managed_IncTag(MNG,Gneg_v);
2269  Gv = biddyZero;
2270  }
2271  } else {
2272  Gneg_v = Gv = g;
2273  }
2274 
2275 
2276  }
2277 
2278  /* RECURSIVE CALLS */
2279  /* returning biddyOne in a recursive call is wrong for ZBDD and ZBDDC, */
2280  /* because top variable of the result may be lower (topmore) than top variables of the arguments */
2281  /* (i.e. because the result depends on domain) */
2282  if (Fneg_v == biddyZero) {
2283  E = Gneg_v;
2284  } else if (Gneg_v == biddyZero) {
2285  E = Fneg_v;
2286  } else if (Fneg_v == biddyOne) {
2287  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
2288  E = BiddyManagedNot(MNG,Gneg_v);
2289  } else if (Gneg_v == biddyOne) {
2290  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
2291  E = BiddyManagedNot(MNG,Fneg_v);
2292  } else if (Fneg_v == Gneg_v) {
2293  E = biddyZero;
2294  } else {
2295  E = BiddyManagedXor(MNG,Fneg_v,Gneg_v);
2296  }
2297  if (Fv == biddyZero) {
2298  T = Gv;
2299  } else if (Gv == biddyZero) {
2300  T = Fv;
2301  } else if (Fv == biddyOne) {
2302  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
2303  T = BiddyManagedNot(MNG,Gv);
2304  } else if (Gv == biddyOne) {
2305  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
2306  T = BiddyManagedNot(MNG,Fv);
2307  } else if (Fv == Gv) {
2308  T = biddyZero;
2309  } else {
2310  T = BiddyManagedXor(MNG,Fv,Gv);
2311  }
2312 
2313  r = BiddyManagedTaggedFoaNode(MNG,v,E,T,rtag,TRUE);
2314  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
2315 
2316  if (NN) {
2317  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,Biddy_Inv(r),cindex);
2318  } else {
2319  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,r,cindex);
2320  }
2321 
2322  } else {
2323 
2324  if (NN) {
2325  Biddy_InvertMark(r);
2326  }
2327 
2328  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
2329  BiddyRefresh(r);
2330 
2331  }
2332 
2333  return r;
2334 }
2335 
2336 /***************************************************************************/
2349 #ifdef __cplusplus
2350 extern "C" {
2351 #endif
2352 
2353 Biddy_Edge
2355 {
2356  Biddy_Edge r;
2357 
2358  assert( f != NULL );
2359  assert( g != NULL );
2360 
2361  if (!MNG) MNG = biddyAnonymousManager;
2362  ZF_LOGI("Biddy_Xnor");
2363 
2364  assert( BiddyIsOK(f) == TRUE );
2365  assert( BiddyIsOK(g) == TRUE );
2366 
2367  r = biddyNull;
2368 
2369  if (biddyManagerType == BIDDYTYPEOBDD) {
2370  /* PROTOTYPED */
2371  r = BiddyManagedNot(MNG,BiddyManagedXor(MNG,f,g));
2372  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
2373  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
2374  /* IMPLEMENTED */
2375  r = BiddyManagedXnor(MNG,f,g);
2376  BiddyRefresh(r); /* not always refreshed by BiddyManagedXnor */
2377  } else if (biddyManagerType == BIDDYTYPEZBDD) {
2378  /* PROTOTYPED */
2379  r = BiddyManagedNot(MNG,BiddyManagedXor(MNG,f,g));
2380  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
2381  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
2382  /* PROTOTYPED */
2383  r = BiddyManagedNot(MNG,BiddyManagedXor(MNG,f,g));
2384  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
2385  } else if (biddyManagerType == BIDDYTYPETZBDD) {
2386  /* PROTOTYPED */
2387  r = BiddyManagedNot(MNG,BiddyManagedXor(MNG,f,g));
2388  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
2389  } else if (biddyManagerType == BIDDYTYPETZBDDC)
2390  {
2391  fprintf(stderr,"Biddy_Xnor: this BDD type is not supported, yet!\n");
2392  return biddyNull;
2393  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
2394  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
2395  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
2396  {
2397  fprintf(stderr,"Biddy_Xnor: this BDD type is not supported, yet!\n");
2398  return biddyNull;
2399  } else {
2400  fprintf(stderr,"Biddy_Xnor: Unsupported BDD type!\n");
2401  return biddyNull;
2402  }
2403 
2404  return r;
2405 }
2406 
2407 #ifdef __cplusplus
2408 }
2409 #endif
2410 
2411 Biddy_Edge
2412 BiddyManagedXnor(const Biddy_Manager MNG, const Biddy_Edge f,
2413  const Biddy_Edge g)
2414 {
2415  Biddy_Edge r;
2416 
2417  assert( MNG != NULL );
2418  assert( f != NULL );
2419  assert( g != NULL );
2420 
2421  r = biddyNull;
2422 
2423  /* IMPLEMENTED FOR OBDDC, ONLY */
2424  assert( biddyManagerType == BIDDYTYPEOBDDC );
2425 
2426  if (biddyManagerType == BIDDYTYPEOBDDC) {
2427  r = Biddy_Inv(BiddyManagedXor(MNG,f,g));
2428  }
2429 
2430  return r;
2431 }
2432 
2433 /***************************************************************************/
2447 #ifdef __cplusplus
2448 extern "C" {
2449 #endif
2450 
2451 Biddy_Edge
2453 {
2454  Biddy_Edge r;
2455 
2456  assert( f != NULL );
2457  assert( g != NULL );
2458 
2459  if (!MNG) MNG = biddyAnonymousManager;
2460  ZF_LOGI("Biddy_Leq");
2461 
2462  assert( BiddyIsOK(f) == TRUE );
2463  assert( BiddyIsOK(g) == TRUE );
2464 
2465  r = biddyNull;
2466 
2467  if (biddyManagerType == BIDDYTYPEOBDD) {
2468  /* IMPLEMENTED */
2469  r = BiddyManagedLeq(MNG,f,g);
2470  BiddyRefresh(r); /* not always refreshed by BiddyManagedLeq */
2471  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
2472  /* IMPLEMENTED */
2473  r = BiddyManagedLeq(MNG,f,g);
2474  BiddyRefresh(r); /* not always refreshed by BiddyManagedLeq */
2475  } else if (biddyManagerType == BIDDYTYPEZBDD) {
2476  /* IMPLEMENTED */
2477  r = BiddyManagedLeq(MNG,f,g);
2478  BiddyRefresh(r); /* not always refreshed by BiddyManagedLeq */
2479  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
2480  /* IMPLEMENTED */
2481  r = BiddyManagedLeq(MNG,f,g);
2482  BiddyRefresh(r); /* not always refreshed by BiddyManagedLeq */
2483  } else if (biddyManagerType == BIDDYTYPETZBDD) {
2484  /* IMPLEMENTED */
2485  r = BiddyManagedLeq(MNG,f,g);
2486  BiddyRefresh(r); /* not always refreshed by BiddyManagedLeq */
2487  } else if (biddyManagerType == BIDDYTYPETZBDDC)
2488  {
2489  fprintf(stderr,"Biddy_Leq: this BDD type is not supported, yet!\n");
2490  return biddyNull;
2491  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
2492  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
2493  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
2494  {
2495  fprintf(stderr,"Biddy_Leq: this BDD type is not supported, yet!\n");
2496  return biddyNull;
2497  } else {
2498  fprintf(stderr,"Biddy_Leq: Unsupported BDD type!\n");
2499  return biddyNull;
2500  }
2501 
2502  return r;
2503 }
2504 
2505 #ifdef __cplusplus
2506 }
2507 #endif
2508 
2509 Biddy_Edge
2510 BiddyManagedLeq(const Biddy_Manager MNG, const Biddy_Edge f, const Biddy_Edge g)
2511 {
2512  Biddy_Edge r, T, E, Fv, Gv, Fneg_v, Gneg_v;
2513  Biddy_Edge FF, GG, HH;
2514  Biddy_Variable v,rtag;
2515  unsigned int cindex;
2516 
2517  static Biddy_Variable topF; /* CAN BE STATIC, WHAT IS BETTER? */
2518  static Biddy_Variable topG; /* CAN BE STATIC, WHAT IS BETTER? */
2519  static Biddy_Variable tagF; /* CAN BE STATIC, WHAT IS BETTER? */
2520  static Biddy_Variable tagG; /* CAN BE STATIC, WHAT IS BETTER? */
2521 
2522  assert( MNG != NULL );
2523  assert( f != NULL );
2524  assert( g != NULL );
2525 
2526  r = biddyNull;
2527 
2528  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDDC */
2529  assert(
2530  (biddyManagerType == BIDDYTYPEOBDD) ||
2531  (biddyManagerType == BIDDYTYPEOBDDC) ||
2532  (biddyManagerType == BIDDYTYPEZBDD) ||
2533  (biddyManagerType == BIDDYTYPEZBDDC) ||
2534  (biddyManagerType == BIDDYTYPETZBDD)
2535  );
2536 
2537  if (biddyManagerType == BIDDYTYPEOBDDC) {
2538 
2539  /* FOR OBDDC, PROCEED BY CALCULATING NOT-AND */
2540 
2541  r = Biddy_Inv(BiddyManagedAnd(MNG,f,Biddy_Inv(g)));
2542  return r;
2543 
2544  }
2545 
2546  if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2547 
2548  /* FOR ZBDD AND ZBDDC, PROCEED BY CALCULATING ITE */
2549  /* THIS IS NOT DIRECT IMPLEMENTATION (AS FOR OBDD AND TZBDD), */
2550  /* BUT IT IS NOT SIGNIFICANTLY SLOWER */
2551 
2552  r = BiddyManagedITE(MNG,f,g,biddyOne);
2553  return r;
2554 
2555  }
2556 
2557  /* LOOKING FOR SIMPLE CASE */
2558  /* returning biddyOne in a RECURSIVE call is wrong for ZBDD and ZBDDC */
2559  /* using Not in a RECURSIVE call is wrong for ZBDD and ZBDDC */
2560  /* because top variable of biddyOne/result may be lower (topmore) than top variables of the arguments */
2561  /* (i.e. because biddyOne/result depends on domain) */
2562 
2563  /* ZBDD AND ZBDDC ARE ALREADY CALCULATED */
2564  if (f == biddyZero) {
2565  return biddyOne;
2566  } else if (g == biddyZero) {
2567  return BiddyManagedNot(MNG,f);
2568  } else if (f == biddyOne) {
2569  return g;
2570  } else if (g == biddyOne) {
2571  return biddyOne;
2572  } else if (f == g) {
2573  return biddyOne;
2574  }
2575 
2576  if (biddyManagerType == BIDDYTYPETZBDD) {
2577  if (BiddyR(f) == BiddyR(g)) {
2578  if (BiddyIsSmaller(Biddy_GetTag(f),Biddy_GetTag(g))) {
2579  return biddyOne;
2580  }
2581  }
2582  }
2583 
2584  /* THIS IS NOT A SIMPLE CASE */
2585 
2586  FF = GG = HH = biddyNull;
2587  Fneg_v = Fv = biddyNull;
2588  Gneg_v = Gv = biddyNull;
2589  rtag = 0;
2590  v = 0;
2591 
2592  if (biddyManagerType == BIDDYTYPEOBDDC) {
2593  /* ALREADY CALCULATED */
2594  }
2595 
2596  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2597  /* ALREADY CALCULATED */
2598  }
2599 
2600  else {
2601 
2602 #ifdef BIDDYEXTENDEDSTATS_YES
2603  biddyNodeTable.andorrecursive++;
2604 #endif
2605 
2606  /* FF, GG, and HH ARE USED FOR CACHE LOOKUP, ONLY */
2607  /* THIS IS NOT ITE CACHE! */
2608 
2609  FF = f;
2610  GG = f;
2611  HH = g;
2612 
2613  }
2614 
2615  /* IF RESULT IS NOT IN THE CACHE TABLE... */
2616  cindex = 0;
2617  if (!findOp3Cache(MNG,biddyOPCache,FF,GG,HH,&r,&cindex))
2618  {
2619 
2620  if (biddyManagerType == BIDDYTYPEOBDD) {
2621 
2622  /* LOOKING FOR THE SMALLEST TOP VARIABLE */
2623  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
2624  topF = BiddyV(f);
2625  topG = BiddyV(g);
2626  v = BiddyIsSmaller(topF,topG) ? topF : topG;
2627 
2628  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS */
2629  /* COMPLEMENTED EDGES MUST BE TRANSFERED */
2630  if (topF == v) {
2631  Fneg_v = BiddyE(f);
2632  Fv = BiddyT(f);
2633  } else {
2634  Fneg_v = Fv = f;
2635  }
2636 
2637  if (topG == v) {
2638  Gneg_v = BiddyE(g);
2639  Gv = BiddyT(g);
2640  } else {
2641  Gneg_v = Gv = g;
2642  }
2643 
2644  rtag = v;
2645 
2646  }
2647 
2648  else if (biddyManagerType == BIDDYTYPEOBDDC) {
2649  /* ALREADY CALCULATED */
2650  }
2651 
2652  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2653  /* ALREADY CALCULATED */
2654  }
2655 
2656  else if (biddyManagerType == BIDDYTYPETZBDD) {
2657 
2658  /* LOOKING FOR THE SMALLEST TAG AND SMALLEST TOP VARIABLE */
2659  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
2660  tagF = Biddy_GetTag(f);
2661  tagG = Biddy_GetTag(g);
2662  topF = BiddyV(f);
2663  topG = BiddyV(g);
2664  rtag = BiddyIsSmaller(tagF,tagG) ? tagF : tagG;
2665  v = BiddyIsSmaller(topF,topG) ? topF : topG;
2666 
2667  if (tagF != tagG) v = rtag;
2668  if (tagF == rtag) {
2669  if (topF == v) {
2670  Fneg_v = BiddyE(f);
2671  Fv = BiddyT(f);
2672  } else {
2673  Fneg_v = f;
2674  Biddy_SetTag(Fneg_v,v);
2675  Fneg_v = Biddy_Managed_IncTag(MNG,Fneg_v);
2676  Fv = biddyZero;
2677  }
2678  } else {
2679  Fneg_v = Fv = f;
2680  }
2681  if (tagG == rtag) {
2682  if (topG == v) {
2683  Gneg_v = BiddyE(g);
2684  Gv = BiddyT(g);
2685  } else {
2686  Gneg_v = g;
2687  Biddy_SetTag(Gneg_v,v);
2688  Gneg_v = Biddy_Managed_IncTag(MNG,Gneg_v);
2689  Gv = biddyZero;
2690  }
2691  } else {
2692  Gneg_v = Gv = g;
2693  }
2694 
2695  }
2696 
2697  /* RECURSIVE CALLS */
2698  /* returning biddyOne in a RECURSIVE call is wrong for ZBDD and ZBDDC */
2699  /* using Not in a RECURSIVE call is wrong for ZBDD and ZBDDC */
2700  /* because top variable of biddyOne/result may be lower (topmore) than top variables of the arguments */
2701  /* (i.e. because biddyOne/result depends on domain) */
2702 
2703  /* ZBDD AND ZBDDC ARE ALREADY CALCULATED */
2704  if (Fneg_v == biddyZero) {
2705  E = biddyOne;
2706  } else if (Gneg_v == biddyZero) {
2707  E = BiddyManagedNot(MNG,Fneg_v);
2708  } else if (Fneg_v == biddyOne) {
2709  E = Gneg_v;
2710  } else if (Gneg_v == biddyOne) {
2711  E = biddyOne;
2712  } else if (Fneg_v == Gneg_v) {
2713  E = biddyOne;
2714  } else {
2715  E = BiddyManagedLeq(MNG,Fneg_v,Gneg_v);
2716  }
2717  if (Fv == biddyZero) {
2718  T = biddyOne;
2719  } else if (Gv == biddyZero) {
2720  T = BiddyManagedNot(MNG,Fv);
2721  } else if (Fv == biddyOne) {
2722  T = Gv;
2723  } else if (Gv == biddyOne) {
2724  T = biddyOne;
2725  } else if (Fv == Gv) {
2726  T = biddyOne;
2727  } else {
2728  T = BiddyManagedLeq(MNG,Fv,Gv);
2729  }
2730 
2731  r = BiddyManagedTaggedFoaNode(MNG,v,E,T,rtag,TRUE);
2732  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
2733 
2734  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,r,cindex);
2735 
2736  } else {
2737 
2738  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
2739  BiddyRefresh(r);
2740 
2741  }
2742 
2743  return r;
2744 }
2745 
2746 /***************************************************************************/
2762 #ifdef __cplusplus
2763 extern "C" {
2764 #endif
2765 
2766 Biddy_Edge
2768 {
2769  Biddy_Edge r;
2770 
2771  assert( f != NULL );
2772  assert( g != NULL );
2773 
2774  if (!MNG) MNG = biddyAnonymousManager;
2775  ZF_LOGI("Biddy_Gt");
2776 
2777  assert( BiddyIsOK(f) == TRUE );
2778  assert( BiddyIsOK(g) == TRUE );
2779 
2780  r = biddyNull;
2781 
2782  if (biddyManagerType == BIDDYTYPEOBDD) {
2783  /* IMPLEMENTED */
2784  r = BiddyManagedGt(MNG,f,g);
2785  BiddyRefresh(r); /* not always refreshed by BiddyManagedGt */
2786  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
2787  /* IMPLEMENTED */
2788  r = BiddyManagedGt(MNG,f,g);
2789  BiddyRefresh(r); /* not always refreshed by BiddyManagedGt */
2790  } else if (biddyManagerType == BIDDYTYPEZBDD) {
2791  /* IMPLEMENTED */
2792  r = BiddyManagedGt(MNG,f,g);
2793  BiddyRefresh(r); /* not always refreshed by BiddyManagedGt */
2794  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
2795  /* IMPLEMENTED */
2796  r = BiddyManagedGt(MNG,f,g);
2797  BiddyRefresh(r); /* not always refreshed by BiddyManagedGt */
2798  } else if (biddyManagerType == BIDDYTYPETZBDD) {
2799  /* IMPLEMENTED */
2800  r = BiddyManagedGt(MNG,f,g);
2801  BiddyRefresh(r); /* not always refreshed by BiddyManagedGt */
2802  } else if (biddyManagerType == BIDDYTYPETZBDDC)
2803  {
2804  fprintf(stderr,"Biddy_Gt: this BDD type is not supported, yet!\n");
2805  return biddyNull;
2806  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
2807  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
2808  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
2809  {
2810  fprintf(stderr,"Biddy_Gt: this BDD type is not supported, yet!\n");
2811  return biddyNull;
2812  } else {
2813  fprintf(stderr,"Biddy_Gt: Unsupported BDD type!\n");
2814  return biddyNull;
2815  }
2816 
2817  return r;
2818 }
2819 
2820 #ifdef __cplusplus
2821 }
2822 #endif
2823 
2824 Biddy_Edge
2825 BiddyManagedGt(const Biddy_Manager MNG, const Biddy_Edge f, const Biddy_Edge g)
2826 {
2827  Biddy_Edge r, T, E, Fv, Gv, Fneg_v, Gneg_v;
2828  Biddy_Edge FF, GG, HH;
2829  Biddy_Variable v,rtag;
2830  unsigned int cindex;
2831 
2832  static Biddy_Variable topF; /* CAN BE STATIC, WHAT IS BETTER? */
2833  static Biddy_Variable topG; /* CAN BE STATIC, WHAT IS BETTER? */
2834  static Biddy_Variable tagF; /* CAN BE STATIC, WHAT IS BETTER? */
2835  static Biddy_Variable tagG; /* CAN BE STATIC, WHAT IS BETTER? */
2836 
2837  assert( MNG != NULL );
2838  assert( f != NULL );
2839  assert( g != NULL );
2840 
2841  r = biddyNull;
2842 
2843  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDDC */
2844  assert(
2845  (biddyManagerType == BIDDYTYPEOBDD) ||
2846  (biddyManagerType == BIDDYTYPEOBDDC) ||
2847  (biddyManagerType == BIDDYTYPEZBDD) ||
2848  (biddyManagerType == BIDDYTYPEZBDDC) ||
2849  (biddyManagerType == BIDDYTYPETZBDD)
2850  );
2851 
2852  if (biddyManagerType == BIDDYTYPEOBDDC) {
2853 
2854  /* FOR OBDDC, PROCEED BY CALCULATING NOT-AND */
2855 
2856  r = BiddyManagedAnd(MNG,f,Biddy_Inv(g));
2857  return r;
2858 
2859  }
2860 
2861  /* LOOKING FOR SIMPLE CASE */
2862  /* using BiddyManagedNot in a RECURSIVE call is wrong for ZBDD and ZBDDC */
2863  /* because top variable of the result may be lower (topmore) than top variables of the arguments */
2864  /* (i.e. because the result depends on domain) */
2865 
2866  if (f == biddyZero) {
2867  return biddyZero;
2868  } else if (g == biddyZero) {
2869  return f;
2870  } else if (f == biddyOne) {
2871  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
2872  return BiddyManagedNot(MNG,g);
2873  } else if (g == biddyOne) {
2874  return biddyZero;
2875  } else if (f == g) {
2876  return biddyZero;
2877  }
2878 
2879  if (biddyManagerType == BIDDYTYPETZBDD) {
2880  if (BiddyR(f) == BiddyR(g)) {
2881  if (BiddyIsSmaller(Biddy_GetTag(f),Biddy_GetTag(g))) {
2882  return biddyZero;
2883  }
2884  }
2885  }
2886 
2887  /* THIS IS NOT A SIMPLE CASE */
2888 
2889  FF = GG = HH = biddyNull;
2890  Fneg_v = Fv = biddyNull;
2891  Gneg_v = Gv = biddyNull;
2892  rtag = 0;
2893  v = 0;
2894 
2895  if (biddyManagerType == BIDDYTYPEOBDDC) {
2896  /* ALREADY CALCULATED */
2897  }
2898 
2899  else {
2900 
2901 #ifdef BIDDYEXTENDEDSTATS_YES
2902  biddyNodeTable.andorrecursive++;
2903 #endif
2904 
2905  /* FF, GG, and HH ARE USED FOR CACHE LOOKUP, ONLY */
2906  /* THIS IS NOT ITE CACHE! */
2907 
2908  FF = f;
2909  GG = g;
2910  HH = g;
2911 
2912  }
2913 
2914  /* IF RESULT IS NOT IN THE CACHE TABLE... */
2915  cindex = 0;
2916  if ((((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD))
2917  && BiddyIsSmaller(BiddyV(g),BiddyV(f))
2918  ) || !findOp3Cache(MNG,biddyOPCache,FF,GG,HH,&r,&cindex))
2919  {
2920 
2921  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
2922 
2923  /* FOR OBDDC THE RESULTS HAS BEEN ALREADY CALCULATED */
2924 
2925  /* LOOKING FOR THE SMALLEST TOP VARIABLE */
2926  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
2927  topF = BiddyV(f);
2928  topG = BiddyV(g);
2929  v = BiddyIsSmaller(topF,topG) ? topF : topG;
2930 
2931  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS */
2932  if (topF == v) {
2933  Fneg_v = BiddyE(f);
2934  Fv = BiddyT(f);
2935  } else {
2936  Fneg_v = Fv = f;
2937  }
2938 
2939  if (topG == v) {
2940  Gneg_v = BiddyE(g);
2941  Gv = BiddyT(g);
2942  } else {
2943  Gneg_v = Gv = g;
2944  }
2945 
2946  rtag = v;
2947 
2948  }
2949 
2950  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
2951 
2952  /* LOOKING FOR THE SMALLEST TOP VARIABLE */
2953  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
2954  topF = BiddyV(f);
2955  topG = BiddyV(g);
2956  v = BiddyIsSmaller(topF,topG) ? topF : topG;
2957 
2958  /* THIS CALL IS NOT INTRODUCING NEW NODES */
2959  /* COMPLEMENTED EDGES MUST BE TRANSFERED */
2960  /* IT SEEMS THAT CACHING THIS RESULTS IS NOT A GOOD IDEA */
2961  if (topF != v) {
2962  r = BiddyManagedGt(MNG,f,Biddy_InvCond(BiddyE(g),Biddy_GetMark(g)));
2963  return r;
2964  }
2965 
2966  /* DETERMINING PARAMETERS FOR RECURSIVE CALLS */
2967  /* IT IS ALREADY KNOWN THAT topF == v */
2968  /* COMPLEMENTED EDGES MUST BE TRANSFERED */
2969  Fneg_v = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
2970  Fv = BiddyT(f);
2971  if (topG == v) {
2972  Gneg_v = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
2973  Gv = BiddyT(g);
2974  } else {
2975  Gneg_v = g;
2976  Gv = biddyZero;
2977  }
2978 
2979  rtag = v;
2980 
2981  }
2982 
2983  else if (biddyManagerType == BIDDYTYPETZBDD) {
2984 
2985  /* LOOKING FOR THE SMALLEST TAG AND SMALLEST TOP VARIABLE */
2986  /* CONSTANT VARIABLE MUST HAVE MAX ORDER */
2987  tagF = Biddy_GetTag(f);
2988  tagG = Biddy_GetTag(g);
2989  topF = BiddyV(f);
2990  topG = BiddyV(g);
2991  rtag = BiddyIsSmaller(tagF,tagG) ? tagF : tagG;
2992  v = BiddyIsSmaller(topF,topG) ? topF : topG;
2993 
2994  if (BiddyIsSmaller(tagG,tagF)) v = rtag;
2995 
2996  if (BiddyIsSmaller(v,tagF)) {
2997  Fneg_v = Fv = f;
2998  } else if (BiddyIsSmaller(v,topF)) {
2999  Fneg_v = f;
3000  Biddy_SetTag(Fneg_v,v);
3001  Fneg_v = Biddy_Managed_IncTag(MNG,Fneg_v);
3002  Fv = biddyZero;
3003  } else {
3004  /* HERE topF == v */
3005  Fneg_v = BiddyE(f);
3006  Fv = BiddyT(f);
3007  }
3008  if (BiddyIsSmaller(v,tagG)) {
3009  Gneg_v = Gv = g;
3010  } else if (BiddyIsSmaller(v,topG)) {
3011  Gneg_v = g;
3012  Biddy_SetTag(Gneg_v,v);
3013  Gneg_v = Biddy_Managed_IncTag(MNG,Gneg_v);
3014  Gv = biddyZero;
3015  } else {
3016  /* HERE topG == v */
3017  Gneg_v = BiddyE(g);
3018  Gv = BiddyT(g);
3019  }
3020 
3021  }
3022 
3023  /* RECURSIVE CALLS */
3024  /* using BiddyManagedNot in a recursive call is wrong for ZBDD and ZBDDC, */
3025  /* because top variable of the result may be lower (topmore) than top variables of the arguments */
3026  /* (i.e. because the result depends on domain) */
3027 
3028  if (Fneg_v == biddyZero) {
3029  E = biddyZero;
3030  } else if (Gneg_v == biddyZero) {
3031  E = Fneg_v;
3032  } else if (Fneg_v == biddyOne) {
3033  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
3034  E = BiddyManagedNot(MNG,Gneg_v);
3035  } else if (Gneg_v == biddyOne) {
3036  E = biddyZero;
3037  } else if (Fneg_v == Gneg_v) {
3038  E = biddyZero;
3039  } else {
3040  E = BiddyManagedGt(MNG,Fneg_v,Gneg_v);
3041  }
3042  if (Fv == biddyZero) {
3043  T = biddyZero;
3044  } else if (Gv == biddyZero) {
3045  T = Fv;
3046  } else if (Fv == biddyOne) {
3047  /* FOR ZBDD AND ZBDDC THIS LINE IS NOT REACHABLE IN RECURSIVE CALLS */
3048  T = BiddyManagedNot(MNG,Gv);
3049  } else if (Gv == biddyOne) {
3050  T = biddyZero;
3051  } else if (Fv == Gv) {
3052  T = biddyZero;
3053  } else {
3054  T = BiddyManagedGt(MNG,Fv,Gv);
3055  }
3056 
3057  r = BiddyManagedTaggedFoaNode(MNG,v,E,T,rtag,TRUE);
3058  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3059 
3060  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,r,cindex);
3061 
3062  } else {
3063 
3064  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
3065  BiddyRefresh(r);
3066 
3067  }
3068 
3069  return r;
3070 }
3071 
3072 /***************************************************************************/
3084 #ifdef __cplusplus
3085 extern "C" {
3086 #endif
3087 
3090 {
3091  Biddy_Edge imp;
3092  Biddy_Boolean r;
3093 
3094  if (!MNG) MNG = biddyAnonymousManager;
3095  ZF_LOGI("Biddy_IsLeq");
3096 
3097  r = FALSE;
3098 
3099  if (biddyManagerType == BIDDYTYPEOBDD) {
3100  /* PROTOTYPED */
3101  imp = BiddyManagedLeq(MNG,f,g);
3102  r = (imp == biddyOne);
3103  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3104  /* PROTOTYPED */
3105  imp = BiddyManagedLeq(MNG,f,g);
3106  r = (imp == biddyOne);
3107  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3108  /* PROTOTYPED */
3109  imp = BiddyManagedLeq(MNG,f,g);
3110  r = (imp == biddyOne);
3111  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3112  /* PROTOTYPED */
3113  imp = BiddyManagedLeq(MNG,f,g);
3114  r = (imp == biddyOne);
3115  } else if (biddyManagerType == BIDDYTYPETZBDD) {
3116  /* PROTOTYPED */
3117  imp = BiddyManagedLeq(MNG,f,g);
3118  r = (imp == biddyOne);
3119  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3120  {
3121  fprintf(stderr,"Biddy_IsLeq: this BDD type is not supported, yet!\n");
3122  return FALSE;
3123  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
3124  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
3125  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
3126  {
3127  fprintf(stderr,"Biddy_IsLeq: this BDD type is not supported, yet!\n");
3128  return FALSE;
3129  } else {
3130  fprintf(stderr,"Biddy_IsLeq: Unsupported BDD type!\n");
3131  return FALSE;
3132  }
3133 
3134  return r;
3135 }
3136 
3137 #ifdef __cplusplus
3138 }
3139 #endif
3140 
3141 /***************************************************************************/
3156 #ifdef __cplusplus
3157 extern "C" {
3158 #endif
3159 
3160 Biddy_Edge
3162  Biddy_Boolean value)
3163 {
3164  Biddy_Edge r;
3165 
3166  assert( f != NULL );
3167 
3168  if (!MNG) MNG = biddyAnonymousManager;
3169  ZF_LOGI("Biddy_Restrict");
3170 
3171  assert( BiddyIsOK(f) == TRUE );
3172 
3173  r = biddyNull;
3174 
3175  if (biddyManagerType == BIDDYTYPEOBDD) {
3176  /* IMPLEMENTED */
3177  r = BiddyManagedRestrict(MNG,f,v,value);
3178  BiddyRefresh(r); /* not always refreshed by BiddyManagedRestrict */
3179  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3180  /* IMPLEMENTED */
3181  r = BiddyManagedRestrict(MNG,f,v,value);
3182  BiddyRefresh(r); /* not always refreshed by BiddyManagedRestrict */
3183  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3184  /* IMPLEMENTED */
3185  r = BiddyManagedRestrict(MNG,f,v,value);
3186  BiddyRefresh(r); /* not always refreshed by BiddyManagedRestrict */
3187  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3188  /* IMPLEMENTED */
3189  r = BiddyManagedRestrict(MNG,f,v,value);
3190  BiddyRefresh(r); /* not always refreshed by BiddyManagedRestrict */
3191  } else if (biddyManagerType == BIDDYTYPETZBDD) {
3192  /* IMPLEMENTED */
3193  r = BiddyManagedRestrict(MNG,f,v,value);
3194  BiddyRefresh(r); /* not always refreshed by BiddyManagedRestrict */
3195  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3196  {
3197  fprintf(stderr,"Biddy_Restrict: this BDD type is not supported, yet!\n");
3198  return biddyNull;
3199  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
3200  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
3201  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
3202  {
3203  fprintf(stderr,"Biddy_Restrict: this BDD type is not supported, yet!\n");
3204  return biddyNull;
3205  } else {
3206  fprintf(stderr,"Biddy_Restrict: Unsupported BDD type!\n");
3207  return biddyNull;
3208  }
3209 
3210  return r;
3211 }
3212 
3213 #ifdef __cplusplus
3214 }
3215 #endif
3216 
3217 Biddy_Edge
3218 BiddyManagedRestrict(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v,
3219  Biddy_Boolean value)
3220 {
3221  Biddy_Edge e, t, r;
3222  Biddy_Variable fv,tag;
3223  Biddy_Edge FF, GG, HH;
3224  unsigned int cindex;
3225 
3226  assert( MNG != NULL );
3227  assert( f != NULL );
3228 
3229  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
3230  assert(
3231  (biddyManagerType == BIDDYTYPEOBDD) ||
3232  (biddyManagerType == BIDDYTYPEOBDDC) ||
3233  (biddyManagerType == BIDDYTYPEZBDD) ||
3234  (biddyManagerType == BIDDYTYPEZBDDC) ||
3235  (biddyManagerType == BIDDYTYPETZBDD)
3236  );
3237 
3238  r = biddyNull;
3239 
3240  if (f == biddyZero) return biddyZero;
3241 
3242  FF = f;
3243  GG = value?biddyZero:biddyOne;
3244  HH = biddyVariableTable.table[v].variable;
3245 
3246  /* IF RESULT IS NOT IN THE CACHE TABLE... */
3247  /* Result is stored in cache only if recursive calls are needed */
3248  /* I am not sure if this is a good strategy! */
3249  cindex = 0;
3250  if (!findOp3Cache(MNG,biddyRCCache,FF,GG,HH,&r,&cindex))
3251  {
3252 
3253  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3254  if ((fv=BiddyV(f)) == v) {
3255  if (value) {
3256  r = Biddy_InvCond(BiddyT(f),Biddy_GetMark(f));
3257  } else {
3258  r = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
3259  }
3260  }
3261  else if (BiddyIsSmaller(v,fv)) {
3262  r = f;
3263  }
3264  else {
3265  e = BiddyManagedRestrict(MNG,BiddyE(f),v,value);
3266  t = BiddyManagedRestrict(MNG,BiddyT(f),v,value);
3267  r = Biddy_InvCond(BiddyManagedTaggedFoaNode(MNG,fv,e,t,fv,TRUE),Biddy_GetMark(f));
3268  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3269  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
3270  }
3271  }
3272 
3273  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3274  if ((fv=BiddyV(f)) == v) {
3275  if (value) {
3276  t = BiddyT(f);
3277  r = BiddyManagedTaggedFoaNode(MNG,v,t,t,v,TRUE);
3278  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3279  } else {
3280  e = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
3281  r = BiddyManagedTaggedFoaNode(MNG,v,e,e,v,TRUE);
3282  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3283  }
3284  }
3285  else if (BiddyIsSmaller(v,fv)) {
3286  if (value) {
3287  r = biddyZero;
3288  } else {
3289  r = BiddyManagedTaggedFoaNode(MNG,v,f,f,v,TRUE);
3290  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3291  }
3292  }
3293  else {
3294  e = BiddyManagedRestrict(MNG,Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),v,value);
3295  t = BiddyManagedRestrict(MNG,BiddyT(f),v,value);
3296  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,fv,TRUE);
3297  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3298  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
3299  }
3300  }
3301 
3302  else if (biddyManagerType == BIDDYTYPETZBDD) {
3303  tag = Biddy_GetTag(f);
3304  if (BiddyIsSmaller(v,tag)) {
3305  r = f;
3306  } else {
3307  fv = BiddyV(f);
3308  if (v == fv) {
3309  if (v == tag) {
3310  if (value) {
3311  r = BiddyT(f);
3312  } else {
3313  r = BiddyE(f);
3314  }
3315  } else {
3316  if (value) {
3317  t = BiddyT(f);
3318  r = BiddyManagedTaggedFoaNode(MNG,v,t,t,tag,TRUE);
3319  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3320  } else {
3321  e = BiddyE(f);
3322  r = BiddyManagedTaggedFoaNode(MNG,v,e,e,tag,TRUE);
3323  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3324  }
3325  }
3326  } else if (BiddyIsSmaller(v,fv)) {
3327  if (value) {
3328  r = biddyZero;
3329  } else {
3330  if (v == tag) {
3331  r = Biddy_Managed_IncTag(MNG,f);
3332  } else {
3333  r = f;
3334  Biddy_SetTag(r,v);
3335  r = Biddy_Managed_IncTag(MNG,r);
3336  r = BiddyManagedTaggedFoaNode(MNG,v,r,r,tag,TRUE);
3337  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3338  }
3339  }
3340  } else {
3341  e = BiddyManagedRestrict(MNG,BiddyE(f),v,value);
3342  t = BiddyManagedRestrict(MNG,BiddyT(f),v,value);
3343  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,tag,TRUE);
3344  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3345  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
3346  }
3347  }
3348  }
3349 
3350  } else {
3351 
3352  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
3353  BiddyRefresh(r);
3354 
3355  }
3356 
3357  return r;
3358 }
3359 
3360 /***************************************************************************/
3373 #ifdef __cplusplus
3374 extern "C" {
3375 #endif
3376 
3377 Biddy_Edge
3379  Biddy_Variable v)
3380 {
3381  Biddy_Edge r;
3382 
3383  assert( f != NULL );
3384  assert( g != NULL );
3385 
3386  if (!MNG) MNG = biddyAnonymousManager;
3387  ZF_LOGI("Biddy_Compose");
3388 
3389  assert( BiddyIsOK(f) == TRUE );
3390  assert( BiddyIsOK(g) == TRUE );
3391 
3392  r = biddyNull;
3393 
3394  if (biddyManagerType == BIDDYTYPEOBDD) {
3395  /* IMPLEMENTED */
3396  r = BiddyManagedCompose(MNG,f,g,v);
3397  BiddyRefresh(r); /* not always refreshed by BiddyManagedCompose */
3398  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3399  /* IMPLEMENTED */
3400  r = BiddyManagedCompose(MNG,f,g,v);
3401  BiddyRefresh(r); /* not always refreshed by BiddyManagedCompose */
3402  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3403  /* IMPLEMENTED */
3404  r = BiddyManagedCompose(MNG,f,g,v);
3405  BiddyRefresh(r); /* not always refreshed by BiddyManagedCompose */
3406  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3407  /* IMPLEMENTED */
3408  r = BiddyManagedCompose(MNG,f,g,v);
3409  BiddyRefresh(r); /* not always refreshed by BiddyManagedCompose */
3410  } else if (biddyManagerType == BIDDYTYPETZBDD) {
3411  /* IMPLEMENTED */
3412  r = BiddyManagedCompose(MNG,f,g,v);
3413  BiddyRefresh(r); /* not always refreshed by BiddyManagedCompose */
3414  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3415  {
3416  fprintf(stderr,"Biddy_Compose: this BDD type is not supported, yet!\n");
3417  return biddyNull;
3418  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
3419  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
3420  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
3421  {
3422  fprintf(stderr,"Biddy_Compose: this BDD type is not supported, yet!\n");
3423  return biddyNull;
3424  } else {
3425  fprintf(stderr,"Biddy_Compose: Unsupported BDD type!\n");
3426  return biddyNull;
3427  }
3428 
3429  return r;
3430 }
3431 
3432 #ifdef __cplusplus
3433 }
3434 #endif
3435 
3436 Biddy_Edge
3437 BiddyManagedCompose(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g,
3438  Biddy_Variable v)
3439 {
3440  Biddy_Edge e, t, r;
3441  Biddy_Variable fv,tag;
3442  Biddy_Edge FF, GG, HH;
3443  unsigned int cindex;
3444 
3445  assert( MNG != NULL );
3446  assert( f != NULL );
3447  assert( g != NULL );
3448 
3449  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
3450  assert(
3451  (biddyManagerType == BIDDYTYPEOBDD) ||
3452  (biddyManagerType == BIDDYTYPEOBDDC) ||
3453  (biddyManagerType == BIDDYTYPEZBDD) ||
3454  (biddyManagerType == BIDDYTYPEZBDDC) ||
3455  (biddyManagerType == BIDDYTYPETZBDD)
3456  );
3457 
3458  r = biddyNull;
3459 
3460  if (f == biddyZero) return f;
3461 
3462  FF = f;
3463  GG = g;
3464  HH = biddyVariableTable.table[v].variable;
3465 
3466  /* IF RESULT IS NOT IN THE CACHE TABLE... */
3467  /* TO DO: CHECK ONLY IF IT IS POSSIBLE TO EXIST IN THE CACHE */
3468  cindex = 0;
3469  if (!findOp3Cache(MNG,biddyRCCache,FF,GG,HH,&r,&cindex))
3470  {
3471 
3472  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3473  if ((fv=BiddyV(f)) == v) {
3474  r = Biddy_InvCond(BiddyManagedITE(MNG,g,BiddyT(f),BiddyE(f)),Biddy_GetMark(f));
3475  }
3476  else if (BiddyIsSmaller(v,fv)) {
3477  r = f;
3478  }
3479  else {
3480  e = BiddyManagedCompose(MNG,BiddyE(f),g,v);
3481  t = BiddyManagedCompose(MNG,BiddyT(f),g,v);
3482  /* VARIANT A: USE TRUE FOR THE FIRST CONDITION */
3483  /* VARIANT B: USE FALSE FOR THE FIRST CONDITION */
3484  if (TRUE && BiddyIsSmaller(fv,Biddy_GetTopVariable(e)) && BiddyIsSmaller(fv,Biddy_GetTopVariable(t))) {
3485  r = Biddy_InvCond(BiddyManagedTaggedFoaNode(MNG,fv,e,t,fv,TRUE),Biddy_GetMark(f));
3486  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3487  } else {
3488  r = Biddy_InvCond(BiddyManagedITE(MNG,biddyVariableTable.table[fv].variable,t,e),Biddy_GetMark(f));
3489  }
3490  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
3491  }
3492  }
3493 
3494  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3495  /* TO DO: Biddy_Replace USE DIFFERENT APPROACH */
3496  /* TO DO: check if that approach is applicable and more efficient */
3497  if ((fv=BiddyV(f)) == v) {
3498  e = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
3499  e = BiddyManagedTaggedFoaNode(MNG,v,e,e,v,TRUE);
3500  BiddyRefresh(e); /* FoaNode returns an obsolete node! */
3501  t = BiddyT(f);
3502  t = BiddyManagedTaggedFoaNode(MNG,v,t,t,v,TRUE);
3503  BiddyRefresh(t); /* FoaNode returns an obsolete node! */
3504  r = BiddyManagedITE(MNG,g,t,e);
3505  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
3506  }
3507  else if (BiddyIsSmaller(v,fv)) {
3508  r = BiddyManagedTaggedFoaNode(MNG,v,f,f,v,TRUE);
3509  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3510  r = BiddyManagedITE(MNG,g,biddyZero,r);
3511  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
3512  }
3513  else {
3514  e = BiddyManagedCompose(MNG,Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),g,v);
3515  t = BiddyManagedCompose(MNG,BiddyT(f),BiddyManagedChange(MNG,g,fv),v);
3516  t = BiddyManagedChange(MNG,t,fv);
3517  r = BiddyManagedXor(MNG,e,t);
3518  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
3519  }
3520  }
3521 
3522  else if (biddyManagerType == BIDDYTYPETZBDD) {
3523  /* TO DO: Biddy_Replace USE DIFFERENT APPROACH */
3524  /* TO DO: check if that approach is applicable and more efficient */
3525  tag = Biddy_GetTag(f);
3526  if (BiddyIsSmaller(v,tag)) {
3527  r = f;
3528  } else {
3529  if ((fv=BiddyV(f)) == v) {
3530  /* VARIANT 1 */
3531 
3532  if (v == tag) {
3533  e = BiddyE(f);
3534  t = BiddyT(f);
3535  } else {
3536  e = BiddyManagedTaggedFoaNode(MNG,v,BiddyE(f),BiddyE(f),tag,TRUE);
3537  BiddyRefresh(e); /* FoaNode returns an obsolete node! */
3538  t = BiddyManagedTaggedFoaNode(MNG,v,BiddyT(f),BiddyT(f),tag,TRUE);
3539  BiddyRefresh(t); /* FoaNode returns an obsolete node! */
3540  }
3541  r = BiddyManagedITE(MNG,g,t,e);
3542 
3543  /* VARIANT 2 - THIS COULD BE BETTER FOR SOME EXAMPLES */
3544  /*
3545  r = BiddyManagedTaggedFoaNode(MNG,v,biddyOne,biddyOne,tag,TRUE);
3546  BiddyRefresh(r);
3547  e = BiddyE(f);
3548  t = BiddyT(f);
3549  r = BiddyManagedAnd(MNG,r,BiddyManagedITE(MNG,g,t,e));
3550  */
3551  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
3552  }
3553  else if (BiddyIsSmaller(v,fv)) {
3554  r = BiddyManagedRestrict(MNG,f,v,FALSE);
3555  r = BiddyManagedITE(MNG,g,biddyZero,r);
3556  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
3557  } else {
3558  /* VARIANT 1 */
3559 
3560  r = BiddyManagedTaggedFoaNode(MNG,fv,biddyOne,biddyOne,tag,TRUE);
3561  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3562  e = BiddyManagedCompose(MNG,BiddyE(f),g,v);
3563  t = BiddyManagedCompose(MNG,BiddyT(f),g,v);
3564  r = BiddyManagedAnd(MNG,r,BiddyManagedITE(MNG,biddyVariableTable.table[fv].variable,t,e));
3565 
3566  /* VARIANT 2 - THIS SEEMS TO BE SLOWER */
3567  /*
3568  e = BiddyManagedTaggedFoaNode(MNG,fv,biddyOne,biddyZero,tag,TRUE);
3569  BiddyRefresh(e);
3570  t = BiddyManagedTaggedFoaNode(MNG,fv,biddyZero,biddyOne,tag,TRUE);
3571  BiddyRefresh(t);
3572  e = BiddyManagedAnd(MNG,e,BiddyManagedCompose(MNG,BiddyE(f),g,v));
3573  t = BiddyManagedAnd(MNG,t,BiddyManagedCompose(MNG,BiddyT(f),g,v));
3574  r = BiddyManagedXor(MNG,e,t);
3575  */
3576  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
3577  }
3578  }
3579  }
3580 
3581  } else {
3582 
3583  /* IF THE RESULT IS FROM CACHE TABLE, FRESH IT! */
3584  BiddyRefresh(r);
3585 
3586  }
3587 
3588  return r;
3589 }
3590 
3591 /***************************************************************************/
3605 #ifdef __cplusplus
3606 extern "C" {
3607 #endif
3608 
3609 Biddy_Edge
3611 {
3612  Biddy_Edge r;
3613 
3614  assert( f != NULL );
3615 
3616  if (!MNG) MNG = biddyAnonymousManager;
3617  ZF_LOGI("Biddy_E");
3618 
3619  assert( BiddyIsOK(f) == TRUE );
3620 
3621  r = biddyNull;
3622 
3623  if (biddyManagerType == BIDDYTYPEOBDD) {
3624  /* IMPLEMENTED */
3625  r = BiddyManagedE(MNG,f,v);
3626  BiddyRefresh(r); /* not always refreshed by BiddyManagedE */
3627  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3628  /* IMPLEMENTED */
3629  r = BiddyManagedE(MNG,f,v);
3630  BiddyRefresh(r); /* not always refreshed by BiddyManagedE */
3631  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3632  /* IMPLEMENTED */
3633  r = BiddyManagedE(MNG,f,v);
3634  BiddyRefresh(r); /* not always refreshed by BiddyManagedE */
3635  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3636  /* IMPLEMENTED */
3637  r = BiddyManagedE(MNG,f,v);
3638  BiddyRefresh(r); /* not always refreshed by BiddyManagedE */
3639  } else if (biddyManagerType == BIDDYTYPETZBDD) {
3640  /* IMPLEMENTED */
3641  r = BiddyManagedE(MNG,f,v);
3642  BiddyRefresh(r); /* not always refreshed by BiddyManagedE */
3643  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3644  {
3645  fprintf(stderr,"Biddy_E: this BDD type is not supported, yet!\n");
3646  return biddyNull;
3647  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
3648  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
3649  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
3650  {
3651  fprintf(stderr,"Biddy_E: this BDD type is not supported, yet!\n");
3652  return biddyNull;
3653  } else {
3654  fprintf(stderr,"Biddy_E: Unsupported BDD type!\n");
3655  return biddyNull;
3656  }
3657 
3658  return r;
3659 }
3660 
3661 #ifdef __cplusplus
3662 }
3663 #endif
3664 
3665 Biddy_Edge
3666 BiddyManagedE(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
3667 {
3668  Biddy_Edge h;
3669  Biddy_Edge e, t, r;
3670  Biddy_Variable fv,tag;
3671  unsigned int cindex;
3672 
3673  assert( MNG != NULL );
3674  assert( f != NULL );
3675 
3676  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
3677  assert(
3678  (biddyManagerType == BIDDYTYPEOBDD) ||
3679  (biddyManagerType == BIDDYTYPEOBDDC) ||
3680  (biddyManagerType == BIDDYTYPEZBDD) ||
3681  (biddyManagerType == BIDDYTYPEZBDDC) ||
3682  (biddyManagerType == BIDDYTYPETZBDD)
3683  );
3684 
3685  r = biddyNull;
3686 
3687  /* LOOKING FOR SIMPLE CASE */
3688  if (f == biddyZero) return f;
3689 
3690  h = biddyNull;
3691 
3692  /* h MUST BE COMPATIBLE WITH CUBE */
3693  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3694  h = biddyVariableTable.table[v].variable;
3695  }
3696  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3697  h = biddyVariableTable.table[v].element;
3698  }
3699  else if (biddyManagerType == BIDDYTYPETZBDD) {
3700  h = biddyVariableTable.table[v].variable;
3701  }
3702 
3703  /* IF RESULT IS NOT IN THE CACHE TABLE... */
3704  cindex = 0;
3705  if ((((uintptr_t) f) > ((uintptr_t) biddyOne)) ?
3706  !findOp3Cache(MNG,biddyEACache,biddyOne,f,h,&r,&cindex) :
3707  !findOp3Cache(MNG,biddyEACache,f,biddyOne,h,&r,&cindex))
3708  {
3709 
3710  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
3711  if ((fv=BiddyV(f)) == v) {
3712  r = BiddyManagedOr(MNG,
3713  Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),
3714  Biddy_InvCond(BiddyT(f),Biddy_GetMark(f)));
3715  }
3716  else if (BiddyIsSmaller(v,fv)) {
3717  r = f;
3718  }
3719  else {
3720  e = BiddyManagedE(MNG,Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),v);
3721  t = BiddyManagedE(MNG,Biddy_InvCond(BiddyT(f),Biddy_GetMark(f)),v);
3722  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,fv,TRUE);
3723  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3724  }
3725  }
3726 
3727  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
3728  if ((fv=BiddyV(f)) == v) {
3729  r = BiddyManagedOr(MNG,
3730  Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),
3731  BiddyT(f));
3732  r = BiddyManagedTaggedFoaNode(MNG,v,r,r,v,TRUE);
3733  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3734  }
3735  else if (BiddyIsSmaller(v,fv)) {
3736  r = BiddyManagedTaggedFoaNode(MNG,v,f,f,v,TRUE);
3737  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3738  }
3739  else {
3740  e = BiddyManagedE(MNG,Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),v);
3741  t = BiddyManagedE(MNG,BiddyT(f),v);
3742  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,fv,TRUE);
3743  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3744  }
3745  }
3746 
3747  else if (biddyManagerType == BIDDYTYPETZBDD) {
3748  tag = Biddy_GetTag(f);
3749  if (BiddyIsSmaller(v,tag)) {
3750  r = f;
3751  } else {
3752  fv = BiddyV(f);
3753  if (v == fv) {
3754  r = BiddyManagedOr(MNG,BiddyE(f),BiddyT(f));
3755  if (v != tag) {
3756  r = BiddyManagedTaggedFoaNode(MNG,v,r,r,tag,TRUE);
3757  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3758  }
3759  } else if (BiddyIsSmaller(v,fv)) {
3760  if (v == tag) {
3761  r = Biddy_Managed_IncTag(MNG,f);
3762  } else {
3763  r = f;
3764  Biddy_SetTag(r,v);
3765  r = Biddy_Managed_IncTag(MNG,r);
3766  r = BiddyManagedTaggedFoaNode(MNG,v,r,r,tag,TRUE);
3767  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3768  }
3769  } else {
3770  e = BiddyManagedE(MNG,BiddyE(f),v);
3771  t = BiddyManagedE(MNG,BiddyT(f),v);
3772  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,tag,TRUE);
3773  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
3774  }
3775  }
3776  }
3777 
3778  /* CACHE FOR Ex(v)(f*1), f*1 <=> 1*f */
3779  if (((uintptr_t) f) > ((uintptr_t) biddyOne)) {
3780  addOp3Cache(MNG,biddyEACache,biddyOne,f,h,r,cindex);
3781  } else {
3782  addOp3Cache(MNG,biddyEACache,f,biddyOne,h,r,cindex);
3783  }
3784 
3785  } else {
3786 
3787  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
3788  BiddyRefresh(r);
3789 
3790  }
3791 
3792  return r;
3793 }
3794 
3795 /***************************************************************************/
3810 #ifdef __cplusplus
3811 extern "C" {
3812 #endif
3813 
3814 Biddy_Edge
3816 {
3817  Biddy_Edge r;
3818 
3819  assert( f != NULL );
3820 
3821  if (!MNG) MNG = biddyAnonymousManager;
3822  ZF_LOGI("Biddy_A");
3823 
3824  assert( BiddyIsOK(f) == TRUE );
3825 
3826  r = biddyNull;
3827 
3828  if (biddyManagerType == BIDDYTYPEOBDD) {
3829  /* PROTOTYPED */
3830  r = BiddyManagedNot(MNG,BiddyManagedE(MNG,BiddyManagedNot(MNG,f),v));
3831  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
3832  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3833  /* IMPLEMENTED */
3834  r = BiddyManagedA(MNG,f,v);
3835  BiddyRefresh(r); /* not always refreshed by BiddyManagedA */
3836  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3837  /* PROTOTYPED */
3838  r = BiddyManagedNot(MNG,BiddyManagedE(MNG,BiddyManagedNot(MNG,f),v));
3839  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
3840  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
3841  /* PROTOTYPED */
3842  r = BiddyManagedNot(MNG,BiddyManagedE(MNG,BiddyManagedNot(MNG,f),v));
3843  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
3844  } else if (biddyManagerType == BIDDYTYPETZBDD) {
3845  /* PROTOTYPED */
3846  r = BiddyManagedNot(MNG,BiddyManagedE(MNG,BiddyManagedNot(MNG,f),v));
3847  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
3848  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3849  {
3850  fprintf(stderr,"Biddy_A: this BDD type is not supported, yet!\n");
3851  return biddyNull;
3852  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
3853  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
3854  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
3855  {
3856  fprintf(stderr,"Biddy_A: this BDD type is not supported, yet!\n");
3857  return biddyNull;
3858  } else {
3859  fprintf(stderr,"Biddy_A: Unsupported BDD type!\n");
3860  return biddyNull;
3861  }
3862 
3863  return r;
3864 }
3865 
3866 #ifdef __cplusplus
3867 }
3868 #endif
3869 
3870 Biddy_Edge
3871 BiddyManagedA(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
3872 {
3873  Biddy_Edge r;
3874 
3875  assert( MNG != NULL );
3876  assert( f != NULL );
3877 
3878  /* IMPLEMENTED FOR OBDDC, ONLY */
3879  assert( biddyManagerType == BIDDYTYPEOBDDC );
3880 
3881  /* LOOKING FOR SIMPLE CASE */
3882  if (Biddy_IsTerminal(f)) return f;
3883 
3884  /* PROCEED BY CALCULATING NOT (EX v NOT f) */
3885  r = Biddy_Inv(BiddyManagedE(MNG,Biddy_Inv(f),v));
3886 
3887  return r;
3888 }
3889 
3890 /***************************************************************************/
3905 #ifdef __cplusplus
3906 extern "C" {
3907 #endif
3908 
3911 {
3912  Biddy_Edge xa;
3913  Biddy_Boolean r;
3914 
3915  if (!MNG) MNG = biddyAnonymousManager;
3916  ZF_LOGI("Biddy_IsVariableDependent");
3917 
3918  r = FALSE;
3919 
3920  if (biddyManagerType == BIDDYTYPEOBDD) {
3921  /* PROTOTYPED */
3922  xa = BiddyManagedA(MNG,f,v);
3923  r = (xa == biddyZero);
3924  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3925  /* PROTOTYPED */
3926  xa = BiddyManagedA(MNG,f,v);
3927  r = (xa == biddyZero);
3928  } else if ((biddyManagerType == BIDDYTYPEZBDD) ||
3929  (biddyManagerType == BIDDYTYPEZBDDC) ||
3930  (biddyManagerType == BIDDYTYPETZBDD))
3931  {
3932  fprintf(stderr,"Biddy_IsVariableDependent: this BDD type is not supported, yet!\n");
3933  return FALSE;
3934  } else if (biddyManagerType == BIDDYTYPETZBDDC)
3935  {
3936  fprintf(stderr,"Biddy_IsVariableDependent: this BDD type is not supported, yet!\n");
3937  return FALSE;
3938  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
3939  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
3940  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
3941  {
3942  fprintf(stderr,"Biddy_IsVariableDependent: this BDD type is not supported, yet!\n");
3943  return FALSE;
3944  } else {
3945  fprintf(stderr,"Biddy_IsVariableDependent: Unsupported BDD type!\n");
3946  return FALSE;
3947  }
3948 
3949  return r;
3950 }
3951 
3952 #ifdef __cplusplus
3953 }
3954 #endif
3955 
3956 /***************************************************************************/
3968 #ifdef __cplusplus
3969 extern "C" {
3970 #endif
3971 
3972 Biddy_Edge
3974 {
3975  Biddy_Edge r;
3976 
3977  assert( f != NULL );
3978  assert( cube != NULL );
3979 
3980  if (!MNG) MNG = biddyAnonymousManager;
3981  ZF_LOGI("Biddy_ExistAbstract");
3982 
3983  assert( BiddyIsOK(f) == TRUE );
3984  assert( BiddyIsOK(cube) == TRUE );
3985 
3986  r = biddyNull;
3987 
3988  if (biddyManagerType == BIDDYTYPEOBDD) {
3989  /* IMPLEMENTED */
3990  r = BiddyManagedExistAbstract(MNG,f,cube);
3991  BiddyRefresh(r); /* not always refreshed by BiddyManagedExistAbstract */
3992  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
3993  /* IMPLEMENTED */
3994  r = BiddyManagedExistAbstract(MNG,f,cube);
3995  BiddyRefresh(r); /* not always refreshed by BiddyManagedExistAbstract */
3996  } else if (biddyManagerType == BIDDYTYPEZBDD) {
3997  /* IMPLEMENTED */
3998  r = BiddyManagedExistAbstract(MNG,f,cube);
3999  BiddyRefresh(r); /* not always refreshed by BiddyManagedExistAbstract */
4000  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
4001  /* IMPLEMENTED */
4002  r = BiddyManagedExistAbstract(MNG,f,cube);
4003  BiddyRefresh(r); /* not always refreshed by BiddyManagedExistAbstract */
4004  } else if (biddyManagerType == BIDDYTYPETZBDD) {
4005  /* IMPLEMENTED */
4006  r = BiddyManagedExistAbstract(MNG,f,cube);
4007  BiddyRefresh(r); /* not always refreshed by BiddyManagedExistAbstract */
4008  } else if (biddyManagerType == BIDDYTYPETZBDDC)
4009  {
4010  fprintf(stderr,"Biddy_ExistAbstract: this BDD type is not supported, yet!\n");
4011  return biddyNull;
4012  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
4013  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
4014  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
4015  {
4016  fprintf(stderr,"Biddy_ExistAbstract: this BDD type is not supported, yet!\n");
4017  return biddyNull;
4018  } else {
4019  fprintf(stderr,"Biddy_ExistAbstract: Unsupported BDD type!\n");
4020  return biddyNull;
4021  }
4022 
4023  return r;
4024 }
4025 
4026 #ifdef __cplusplus
4027 }
4028 #endif
4029 
4030 Biddy_Edge
4031 BiddyManagedExistAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge cube)
4032 {
4033  Biddy_Edge e, t, r;
4034  Biddy_Variable fv,cv,tag;
4035  unsigned int cindex;
4036 
4037  assert( MNG != NULL );
4038  assert( f != NULL );
4039  assert( cube != NULL );
4040 
4041  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
4042  assert(
4043  (biddyManagerType == BIDDYTYPEOBDD) ||
4044  (biddyManagerType == BIDDYTYPEOBDDC) ||
4045  (biddyManagerType == BIDDYTYPEZBDD) ||
4046  (biddyManagerType == BIDDYTYPEZBDDC) ||
4047  (biddyManagerType == BIDDYTYPETZBDD)
4048  );
4049 
4050  r = biddyNull;
4051 
4052  /* LOOKING FOR SIMPLE CASE */
4053  if (f == biddyZero) return f;
4054 
4055  /* IF RESULT IS NOT IN THE CACHE TABLE... */
4056  cindex = 0;
4057  if ((((uintptr_t) f) > ((uintptr_t) biddyOne)) ?
4058  !findOp3Cache(MNG,biddyEACache,biddyOne,f,cube,&r,&cindex) :
4059  !findOp3Cache(MNG,biddyEACache,f,biddyOne,cube,&r,&cindex))
4060  {
4061 
4062  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
4063  fv = BiddyV(f);
4064  cv = BiddyV(cube);
4065  while (!Biddy_IsTerminal(cube) && BiddyIsSmaller(cv,fv)) {
4066  cube = BiddyT(cube);
4067  cv = BiddyV(cube);
4068  }
4069  if (Biddy_IsTerminal(cube)) {
4070  return f;
4071  }
4072  if (cv == fv) {
4073  e = BiddyManagedExistAbstract(MNG,
4074  Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),BiddyT(cube));
4075  t = BiddyManagedExistAbstract(MNG,
4076  Biddy_InvCond(BiddyT(f),Biddy_GetMark(f)),BiddyT(cube));
4077  r = BiddyManagedOr(MNG,e,t);
4078  } else {
4079  e = BiddyManagedExistAbstract(MNG,
4080  Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),cube);
4081  t = BiddyManagedExistAbstract(MNG,
4082  Biddy_InvCond(BiddyT(f),Biddy_GetMark(f)),cube);
4083  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,fv,TRUE);
4084  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4085  }
4086  }
4087 
4088  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
4089  if (Biddy_IsTerminal(cube)) {
4090  return f;
4091  }
4092  cv = BiddyV(cube);
4093  fv = BiddyV(f);
4094  if (BiddyIsSmaller(cv,fv)) {
4095  r = BiddyManagedExistAbstract(MNG,f,BiddyT(cube));
4096  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,cv,TRUE);
4097  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4098  }
4099  else if (cv == fv) {
4100  e = BiddyManagedExistAbstract(MNG,
4101  Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),BiddyT(cube));
4102  t = BiddyManagedExistAbstract(MNG,BiddyT(f),BiddyT(cube));
4103  r = BiddyManagedOr(MNG,e,t);
4104  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,cv,TRUE);
4105  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4106  } else {
4107  e = BiddyManagedExistAbstract(MNG,
4108  Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),cube);
4109  t = BiddyManagedExistAbstract(MNG,BiddyT(f),cube);
4110  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,fv,TRUE);
4111  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4112  }
4113  }
4114 
4115  else if (biddyManagerType == BIDDYTYPETZBDD) {
4116  tag = Biddy_GetTag(f);
4117  cv = BiddyV(cube);
4118  while (!Biddy_IsTerminal(cube) && BiddyIsSmaller(cv,tag)) {
4119  cube = BiddyT(cube);
4120  cv = BiddyV(cube);
4121  }
4122  if (Biddy_IsTerminal(cube)) {
4123  return f;
4124  }
4125  fv = BiddyV(f);
4126 
4127  /* VARIANT 1 */
4128  /*
4129  if (cv == tag) {
4130  if (tag == fv) {
4131  e = BiddyManagedExistAbstract(MNG,BiddyE(f),BiddyT(cube));
4132  t = BiddyManagedExistAbstract(MNG,BiddyT(f),BiddyT(cube));
4133  r = BiddyManagedOr(MNG,e,t);
4134  } else {
4135  r = Biddy_Managed_IncTag(MNG,f);
4136  r = BiddyManagedExistAbstract(MNG,r,BiddyT(cube));
4137  }
4138  } else if (BiddyIsSmaller(cv,fv)) {
4139  r = f;
4140  Biddy_SetTag(r,cv);
4141  r = Biddy_Managed_IncTag(MNG,r);
4142  r = BiddyManagedExistAbstract(MNG,r,BiddyT(cube));
4143  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,tag,TRUE);
4144  BiddyRefresh(r); / * FoaNode returns an obsolete node! * /
4145  } else if (cv == fv) {
4146  e = BiddyManagedExistAbstract(MNG,BiddyE(f),BiddyT(cube));
4147  t = BiddyManagedExistAbstract(MNG,BiddyT(f),BiddyT(cube));
4148  r = BiddyManagedOr(MNG,e,t);
4149  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,tag,TRUE);
4150  BiddyRefresh(r); / * FoaNode returns an obsolete node! * /
4151  } else {
4152  e = BiddyManagedExistAbstract(MNG,BiddyE(f),cube);
4153  t = BiddyManagedExistAbstract(MNG,BiddyT(f),cube);
4154  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,tag,TRUE);
4155  BiddyRefresh(r); / * FoaNode returns an obsolete node! * /
4156  }
4157  */
4158 
4159  /* VARIANT 2 */
4160 
4161  if (cv == fv) {
4162  e = BiddyManagedExistAbstract(MNG,BiddyE(f),BiddyT(cube));
4163  t = BiddyManagedExistAbstract(MNG,BiddyT(f),BiddyT(cube));
4164  r = BiddyManagedOr(MNG,e,t);
4165  if (cv != tag) {
4166  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,tag,TRUE);
4167  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4168  }
4169  } else if (BiddyIsSmaller(cv,fv)) {
4170  if (cv == tag) {
4171  r = Biddy_Managed_IncTag(MNG,f);
4172  r = BiddyManagedExistAbstract(MNG,r,BiddyT(cube));
4173  } else {
4174  r = f;
4175  Biddy_SetTag(r,cv);
4176  r = Biddy_Managed_IncTag(MNG,r);
4177  r = BiddyManagedExistAbstract(MNG,r,BiddyT(cube));
4178  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,tag,TRUE);
4179  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4180  }
4181  } else {
4182  e = BiddyManagedExistAbstract(MNG,BiddyE(f),cube);
4183  t = BiddyManagedExistAbstract(MNG,BiddyT(f),cube);
4184  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,tag,TRUE);
4185  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4186  }
4187 
4188 
4189  }
4190 
4191  /* CACHE EVERYTHING */
4192  if (((uintptr_t) f) > ((uintptr_t) biddyOne)) {
4193  addOp3Cache(MNG,biddyEACache,biddyOne,f,cube,r,cindex);
4194  } else {
4195  addOp3Cache(MNG,biddyEACache,f,biddyOne,cube,r,cindex);
4196  }
4197 
4198  } else {
4199 
4200  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
4201  BiddyRefresh(r);
4202 
4203  }
4204 
4205  return r;
4206 }
4207 
4208 /***************************************************************************/
4221 #ifdef __cplusplus
4222 extern "C" {
4223 #endif
4224 
4225 Biddy_Edge
4227 {
4228  Biddy_Edge r;
4229 
4230  assert( f != NULL );
4231  assert( cube != NULL );
4232 
4233  if (!MNG) MNG = biddyAnonymousManager;
4234  ZF_LOGI("Biddy_UnivAbstract");
4235 
4236  assert( BiddyIsOK(f) == TRUE );
4237  assert( BiddyIsOK(cube) == TRUE );
4238 
4239  r = biddyNull;
4240 
4241  if (biddyManagerType == BIDDYTYPEOBDD) {
4242  /* PROTOTYPED */
4243  r = BiddyManagedNot(MNG,BiddyManagedExistAbstract(MNG,BiddyManagedNot(MNG,f),cube));
4244  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
4245  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
4246  /* IMPLEMENTED */
4247  r = BiddyManagedUnivAbstract(MNG,f,cube);
4248  BiddyRefresh(r); /* not always refreshed by BiddyManagedUnivAbstract */
4249  } else if (biddyManagerType == BIDDYTYPEZBDD) {
4250  /* PROTOTYPED */
4251  r = BiddyManagedNot(MNG,BiddyManagedExistAbstract(MNG,BiddyManagedNot(MNG,f),cube));
4252  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
4253  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
4254  /* PROTOTYPED */
4255  r = BiddyManagedNot(MNG,BiddyManagedExistAbstract(MNG,BiddyManagedNot(MNG,f),cube));
4256  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
4257  } else if (biddyManagerType == BIDDYTYPETZBDD) {
4258  /* PROTOTYPED */
4259  r = BiddyManagedNot(MNG,BiddyManagedExistAbstract(MNG,BiddyManagedNot(MNG,f),cube));
4260  BiddyRefresh(r); /* not always refreshed by BiddyManagedNot */
4261  } else if (biddyManagerType == BIDDYTYPETZBDDC)
4262  {
4263  fprintf(stderr,"Biddy_UnivAbstract: this BDD type is not supported, yet!\n");
4264  return biddyNull;
4265  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
4266  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
4267  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
4268  {
4269  fprintf(stderr,"Biddy_UnivAbstract: this BDD type is not supported, yet!\n");
4270  return biddyNull;
4271  } else {
4272  fprintf(stderr,"Biddy_UnivAbstract: Unsupported BDD type!\n");
4273  return biddyNull;
4274  }
4275 
4276  return r;
4277 }
4278 
4279 #ifdef __cplusplus
4280 }
4281 #endif
4282 
4283 Biddy_Edge
4284 BiddyManagedUnivAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge cube)
4285 {
4286  Biddy_Edge r;
4287 
4288  assert( MNG != NULL );
4289  assert( f != NULL );
4290  assert( cube != NULL );
4291 
4292  /* IMPLEMENTED FOR OBDDC, ONLY */
4293  assert( biddyManagerType == BIDDYTYPEOBDDC );
4294 
4295  /* LOOKING FOR SIMPLE CASE */
4296  if (Biddy_IsTerminal(f)) return f;
4297 
4298  /* PROCEED BY CALCULATING NOT (EX cube NOT f) */
4299  r = Biddy_Inv(BiddyManagedExistAbstract(MNG,Biddy_Inv(f),cube));
4300 
4301  return r;
4302 }
4303 
4304 /***************************************************************************/
4316 #ifdef __cplusplus
4317 extern "C" {
4318 #endif
4319 
4320 Biddy_Edge
4322  Biddy_Edge cube)
4323 {
4324  Biddy_Edge r;
4325 
4326  assert( f != NULL );
4327  assert( g != NULL );
4328  assert( cube != NULL );
4329 
4330  if (!MNG) MNG = biddyAnonymousManager;
4331  ZF_LOGI("Biddy_AndAbstract");
4332 
4333  assert( BiddyIsOK(f) == TRUE );
4334  assert( BiddyIsOK(g) == TRUE );
4335  assert( BiddyIsOK(cube) == TRUE );
4336 
4337  r = biddyNull;
4338 
4339  if (biddyManagerType == BIDDYTYPEOBDD) {
4340  /* IMPLEMENTED */
4341  r = BiddyManagedAndAbstract(MNG,f,g,cube);
4342  BiddyRefresh(r); /* not always refreshed by BiddyManagedAndAbstract */
4343  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
4344  /* IMPLEMENTED */
4345  r = BiddyManagedAndAbstract(MNG,f,g,cube);
4346  BiddyRefresh(r); /* not always refreshed by BiddyManagedAndAbstract */
4347  } else if (biddyManagerType == BIDDYTYPEZBDD) {
4348  /* IMPLEMENTED */
4349  r = BiddyManagedAndAbstract(MNG,f,g,cube);
4350  BiddyRefresh(r); /* not always refreshed by BiddyManagedAndAbstract */
4351  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
4352  /* IMPLEMENTED */
4353  r = BiddyManagedAndAbstract(MNG,f,g,cube);
4354  BiddyRefresh(r); /* not always refreshed by BiddyManagedAndAbstract */
4355  } else if (biddyManagerType == BIDDYTYPETZBDD) {
4356  /* IMPLEMENTED */
4357  r = BiddyManagedAndAbstract(MNG,f,g,cube);
4358  BiddyRefresh(r); /* not always refreshed by BiddyManagedAndAbstract */
4359  } else if (biddyManagerType == BIDDYTYPETZBDDC)
4360  {
4361  fprintf(stderr,"Biddy_AndAbstract: this BDD type is not supported, yet!\n");
4362  return biddyNull;
4363  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
4364  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
4365  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
4366  {
4367  fprintf(stderr,"Biddy_AndAbstract: this BDD type is not supported, yet!\n");
4368  return biddyNull;
4369  } else {
4370  fprintf(stderr,"Biddy_AndAbstract: Unsupported BDD type!\n");
4371  return biddyNull;
4372  }
4373 
4374  return r;
4375 }
4376 
4377 #ifdef __cplusplus
4378 }
4379 #endif
4380 
4381 Biddy_Edge
4382 BiddyManagedAndAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g,
4383  Biddy_Edge cube)
4384 {
4385  Biddy_Edge f0,f1,g0,g1;
4386  Biddy_Edge e, t, r;
4387  Biddy_Variable fv,gv,minv,cv;
4388  Biddy_Variable ftag,gtag,mintag;
4389  Biddy_Boolean cgt;
4390  unsigned int cindex;
4391 
4392  assert( MNG != NULL );
4393  assert( f != NULL );
4394  assert( g != NULL );
4395  assert( cube != NULL );
4396 
4397  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDDC */
4398  assert(
4399  (biddyManagerType == BIDDYTYPEOBDD) ||
4400  (biddyManagerType == BIDDYTYPEOBDDC) ||
4401  (biddyManagerType == BIDDYTYPEZBDD) ||
4402  (biddyManagerType == BIDDYTYPEZBDDC) ||
4403  (biddyManagerType == BIDDYTYPETZBDD)
4404  );
4405 
4406  r = biddyNull;
4407 
4408  /* LOOKING FOR SIMPLE CASE */
4409  if ((f == biddyZero) || (g == biddyZero)) {
4410  return biddyZero;
4411  } else if (Biddy_IsTerminal(cube)) {
4412  return BiddyManagedAnd(MNG,f,g);
4413  } else if (f == biddyOne) {
4414  return BiddyManagedExistAbstract(MNG,g,cube);
4415  } else if (g == biddyOne) {
4416  return BiddyManagedExistAbstract(MNG,f,cube);
4417  } else if (f == g) {
4418  return BiddyManagedExistAbstract(MNG,f,cube);
4419  }
4420 
4421  if (biddyManagerType == BIDDYTYPEOBDDC) {
4422  if (Biddy_IsEqvPointer(f,g)) {
4423  return biddyZero;
4424  }
4425  }
4426 
4427  else if (biddyManagerType == BIDDYTYPETZBDD) {
4428  if (BiddyR(f) == BiddyR(g)) {
4429  if (BiddyIsSmaller(Biddy_GetTag(f),Biddy_GetTag(g))) {
4430  return BiddyManagedExistAbstract(MNG,f,cube);
4431  } else {
4432  return BiddyManagedExistAbstract(MNG,g,cube);
4433  }
4434  }
4435  }
4436 
4437  /* NORMALIZATION */
4438  if (((uintptr_t) f) > ((uintptr_t) g)) {
4439  exchangeEdges(&f,&g);
4440  }
4441 
4442  /* IF RESULT IS NOT IN THE CACHE TABLE... */
4443  cindex = 0;
4444  if (!findOp3Cache(MNG,biddyEACache,f,g,cube,&r,&cindex))
4445  {
4446 
4447  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
4448  fv = BiddyV(f);
4449  gv = BiddyV(g);
4450  if (BiddyIsSmaller(fv,gv)) {
4451  f0 = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
4452  f1 = Biddy_InvCond(BiddyT(f),Biddy_GetMark(f));
4453  g0 = g;
4454  g1 = g;
4455  minv = fv;
4456  } else if (BiddyIsSmaller(gv,fv)) {
4457  f0 = f;
4458  f1 = f;
4459  g0 = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
4460  g1 = Biddy_InvCond(BiddyT(g),Biddy_GetMark(g));
4461  minv = gv;
4462  } else {
4463  f0 = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
4464  f1 = Biddy_InvCond(BiddyT(f),Biddy_GetMark(f));
4465  g0 = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
4466  g1 = Biddy_InvCond(BiddyT(g),Biddy_GetMark(g));
4467  minv = fv;
4468  }
4469  cv = BiddyV(cube);
4470  while (BiddyIsSmaller(cv,minv)) {
4471  cube = BiddyT(cube);
4472  cv = BiddyV(cube);
4473  }
4474  /* if (!cv) return BiddyManagedAnd(MNG,f,g); */ /* unnecessary */
4475  if (minv == cv) {
4476  /* Tricky optimizations are from: */
4477  /* B. Yang et al. A Performance Study of BDD-Based Model Checking. 1998. */
4478  /* http://fmv.jku.at/papers/YangEtAl-FMCAD98.pdf */
4479  e = BiddyManagedAndAbstract(MNG,f0,g0,BiddyT(cube));
4480  if (e == biddyOne) return biddyOne;
4481  if ((e == f1) || (e == g1)) {
4482  return e;
4483  /* r = e */ /* I AM NOT SURE IF THIS SHOULD BE CACHED */
4484  } else {
4485  if (e == Biddy_Inv(f1)) f1 = biddyOne; /* this is useful only for OBDDC, but not wrong for OBDD */
4486  if (e == Biddy_Inv(g1)) g1 = biddyOne; /* this is useful only for OBDDC, but not wrong for OBDD */
4487  t = BiddyManagedAndAbstract(MNG,f1,g1,BiddyT(cube));
4488  r = BiddyManagedOr(MNG,e,t);
4489  }
4490  } else {
4491  e = BiddyManagedAndAbstract(MNG,f0,g0,cube);
4492  t = BiddyManagedAndAbstract(MNG,f1,g1,cube);
4493  r = BiddyManagedTaggedFoaNode(MNG,minv,e,t,minv,TRUE);
4494  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4495  }
4496  }
4497 
4498  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
4499  fv = BiddyV(f);
4500  gv = BiddyV(g);
4501  minv = BiddyIsSmaller(fv,gv) ? fv : gv;
4502  if (fv != gv) {
4503  if (fv == minv) {
4504  if (Biddy_GetMark(f)) {
4505  /* return BiddyManagedAndAbstract(MNG,Biddy_Inv(BiddyE(f)),g,cube); */
4506  r = BiddyManagedAndAbstract(MNG,Biddy_Inv(BiddyE(f)),g,cube);
4507  } else {
4508  /* return BiddyManagedAndAbstract(MNG,BiddyE(f),g,cube); */
4509  r = BiddyManagedAndAbstract(MNG,BiddyE(f),g,cube);
4510  }
4511  } else {
4512  if (Biddy_GetMark(g)) {
4513  /* return BiddyManagedAndAbstract(MNG,f,Biddy_Inv(BiddyE(g)),cube); */
4514  r = BiddyManagedAndAbstract(MNG,f,Biddy_Inv(BiddyE(g)),cube);
4515  } else {
4516  /* return BiddyManagedAndAbstract(MNG,f,BiddyE(g),cube); */
4517  r = BiddyManagedAndAbstract(MNG,f,BiddyE(g),cube);
4518  }
4519  }
4520  } else {
4521  cv = BiddyV(cube);
4522  if (BiddyIsSmaller(cv,minv)) {
4523  r = BiddyManagedAndAbstract(MNG,f,g,BiddyT(cube));
4524  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,cv,TRUE);
4525  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4526  }
4527  else if (cv == minv) {
4528  f0 = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
4529  f1 = BiddyT(f);
4530  g0 = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
4531  g1 = BiddyT(g);
4532  e = BiddyManagedAndAbstract(MNG,f0,g0,BiddyT(cube));
4533  t = BiddyManagedAndAbstract(MNG,f1,g1,BiddyT(cube));
4534  r = BiddyManagedOr(MNG,e,t);
4535  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,cv,TRUE);
4536  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4537  } else {
4538  f0 = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
4539  f1 = BiddyT(f);
4540  g0 = Biddy_InvCond(BiddyE(g),Biddy_GetMark(g));
4541  g1 = BiddyT(g);
4542  e = BiddyManagedAndAbstract(MNG,f0,g0,cube);
4543  t = BiddyManagedAndAbstract(MNG,f1,g1,cube);
4544  r = BiddyManagedTaggedFoaNode(MNG,minv,e,t,minv,TRUE);
4545  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4546  }
4547  }
4548  }
4549 
4550  else if (biddyManagerType == BIDDYTYPETZBDD) {
4551  ftag = Biddy_GetTag(f);
4552  gtag = Biddy_GetTag(g);
4553  mintag = BiddyIsSmaller(ftag,gtag) ? ftag : gtag;
4554  cv = BiddyV(cube);
4555  while (BiddyIsSmaller(cv,mintag)) {
4556  cube = BiddyT(cube);
4557  cv = BiddyV(cube);
4558  }
4559  /* if (!cv) return BiddyManagedAnd(MNG,f,g); */ /* unnecessary */
4560 
4561  /* VARIANT 1 */
4562  /*
4563  fv = BiddyV(f);
4564  gv = BiddyV(g);
4565  minv = BiddyIsSmaller(fv,gv) ? fv : gv;
4566  if (BiddyIsSmaller(fv,gtag)) {
4567  f0 = BiddyE(f);
4568  f1 = BiddyT(f);
4569  g0 = g1 = g;
4570  } else if (BiddyIsSmaller(gv,ftag)) {
4571  f0 = f1 = f;
4572  g0 = BiddyE(g);
4573  g1 = BiddyT(g);
4574  } else {
4575  if (minv == fv) {
4576  f0 = BiddyE(f);
4577  f1 = BiddyT(f);
4578  } else {
4579  f0 = f;
4580  Biddy_SetTag(f0,minv);
4581  f0 = Biddy_Managed_IncTag(MNG,f0);
4582  f1 = biddyZero;
4583  }
4584  if (minv == gv) {
4585  g0 = BiddyE(g);
4586  g1 = BiddyT(g);
4587  } else {
4588  g0 = g;
4589  Biddy_SetTag(g0,minv);
4590  g0 = Biddy_Managed_IncTag(MNG,g0);
4591  g1 = biddyZero;
4592  }
4593  }
4594  if (BiddyIsSmaller(minv,cv)) {
4595  e = BiddyManagedAndAbstract(MNG,f0,g0,cube);
4596  t = BiddyManagedAndAbstract(MNG,f1,g1,cube);
4597  } else {
4598  e = BiddyManagedAndAbstract(MNG,f0,g0,BiddyT(cube));
4599  t = BiddyManagedAndAbstract(MNG,f1,g1,BiddyT(cube));
4600  }
4601  if (cv == mintag) {
4602  if (minv == mintag) {
4603  r = BiddyManagedOr(MNG,e,t);
4604  } else {
4605  r = BiddyManagedTaggedFoaNode(MNG,minv,e,t,mintag,TRUE);
4606  BiddyRefresh(r); / * FoaNode returns an obsolete node! * /
4607  if (r != biddyZero) r = Biddy_Managed_IncTag(MNG,r);
4608  }
4609  } else if (BiddyIsSmaller(cv,minv)) {
4610  r = BiddyManagedTaggedFoaNode(MNG,minv,e,t,cv,TRUE);
4611  r = Biddy_Managed_IncTag(MNG,r);
4612  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,mintag,TRUE);
4613  BiddyRefresh(r); / * FoaNode returns an obsolete node! * /
4614  } else if (cv == minv) {
4615  r = BiddyManagedOr(MNG,e,t);
4616  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,mintag,TRUE);
4617  BiddyRefresh(r); / * FoaNode returns an obsolete node! * /
4618  } else {
4619  r = BiddyManagedTaggedFoaNode(MNG,minv,e,t,mintag,TRUE);
4620  BiddyRefresh(r); / * FoaNode returns an obsolete node! * /
4621  }
4622  */
4623 
4624  /* VARIANT 2 */
4625  fv = BiddyV(f);
4626  gv = BiddyV(g);
4627  minv = BiddyIsSmaller(fv,gv) ? fv : gv;
4628  if (BiddyIsSmaller(minv,ftag)) {
4629  f0 = f1 = f;
4630  } else if (minv == fv) {
4631  f0 = BiddyE(f);
4632  f1 = BiddyT(f);
4633  } else {
4634  f0 = f;
4635  Biddy_SetTag(f0,minv);
4636  f0 = Biddy_Managed_IncTag(MNG,f0);
4637  f1 = biddyZero;
4638  }
4639  if (BiddyIsSmaller(minv,gtag)) {
4640  g0 = g1 = g;
4641  } else if (minv == gv) {
4642  g0 = BiddyE(g);
4643  g1 = BiddyT(g);
4644  } else {
4645  g0 = g;
4646  Biddy_SetTag(g0,minv);
4647  g0 = Biddy_Managed_IncTag(MNG,g0);
4648  g1 = biddyZero;
4649  }
4650  cgt = BiddyIsSmaller(minv,cv);
4651  if (f0 == biddyZero) {
4652  e = biddyZero;
4653  } else if (g0 == biddyZero) {
4654  e = biddyZero;
4655  } else {
4656  e = BiddyManagedAndAbstract(MNG,f0,g0,cgt?cube:BiddyT(cube));
4657  }
4658  if (f1 == biddyZero) {
4659  t = biddyZero;
4660  } else if (g1 == biddyZero) {
4661  t = biddyZero;
4662  } else {
4663  t = BiddyManagedAndAbstract(MNG,f1,g1,cgt?cube:BiddyT(cube));
4664  }
4665 
4666  /* VARIANT 2A */
4667  /*
4668  if (cv == mintag) {
4669  if (minv == mintag) {
4670  r = BiddyManagedOr(MNG,e,t);
4671  } else {
4672  r = BiddyManagedTaggedFoaNode(MNG,minv,e,t,mintag,TRUE);
4673  BiddyRefresh(r); / * FoaNode returns an obsolete node! * /
4674  if (r != biddyZero) r = Biddy_Managed_IncTag(MNG,r);
4675  }
4676  } else if (BiddyIsSmaller(cv,minv)) {
4677  r = BiddyManagedTaggedFoaNode(MNG,minv,e,t,cv,TRUE);
4678  BiddyRefresh(r); / * FoaNode returns an obsolete node! * /
4679  if (r != biddyZero) r = Biddy_Managed_IncTag(MNG,r);
4680  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,mintag,TRUE);
4681  BiddyRefresh(r); / * FoaNode returns an obsolete node! * /
4682  } else if (cv == minv) {
4683  r = BiddyManagedOr(MNG,e,t);
4684  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,mintag,TRUE);
4685  BiddyRefresh(r); / * FoaNode returns an obsolete node! * /
4686  } else {
4687  r = BiddyManagedTaggedFoaNode(MNG,minv,e,t,mintag,TRUE);
4688  BiddyRefresh(r); / * FoaNode returns an obsolete node! * /
4689  }
4690  */
4691 
4692  /* VARIANT 2B */
4693  if (BiddyIsSmaller(cv,minv)) {
4694  r = BiddyManagedTaggedFoaNode(MNG,minv,e,t,cv,TRUE);
4695  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4696  if (r != biddyZero) r = Biddy_Managed_IncTag(MNG,r);
4697  if (cv != mintag) {
4698  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,mintag,TRUE);
4699  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4700  }
4701  } else if (cv == minv) {
4702  r = BiddyManagedOr(MNG,e,t);
4703  if (cv != mintag) {
4704  r = BiddyManagedTaggedFoaNode(MNG,cv,r,r,mintag,TRUE);
4705  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4706  }
4707  } else {
4708  r = BiddyManagedTaggedFoaNode(MNG,minv,e,t,mintag,TRUE);
4709  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
4710  }
4711 
4712  }
4713 
4714  /* CACHE EVERYTHING */
4715  addOp3Cache(MNG,biddyEACache,f,g,cube,r,cindex);
4716 
4717  } else {
4718 
4719  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
4720  BiddyRefresh(r);
4721 
4722  }
4723 
4724  return r;
4725 }
4726 
4727 /***************************************************************************/
4742 /* SOME REFERENCES FOR Biddy_Constrain AND Biddy_Simplify */
4743 /* O. Coudert et al. Verification of synchronous sequential machines based on symbolic execution, 1989 */
4744 /* O. Coudert et al. A unified framework for the formal verification of sequential circuits, 1990 */
4745 /* B. Lin et al. Don't care minimization of multi-level sequential logic networks. 1990. */
4746 /* Thomas R. Shiple et al. Heuristic minimization of BDDs using don't cares, 1994 */
4747 /* Mark D. Aagaard. et al. Formal verification using parametric representations of Boolean constraints, 1999 */
4748 
4749 #ifdef __cplusplus
4750 extern "C" {
4751 #endif
4752 
4753 Biddy_Edge
4755 {
4756  Biddy_Edge r;
4757 
4758  assert( f != NULL );
4759  assert( c != NULL );
4760 
4761  if (!MNG) MNG = biddyAnonymousManager;
4762  ZF_LOGI("Biddy_Constrain");
4763 
4764  assert( BiddyIsOK(f) == TRUE );
4765  assert( BiddyIsOK(c) == TRUE );
4766 
4767  r = biddyNull;
4768 
4769  if (biddyManagerType == BIDDYTYPEOBDD) {
4770  /* IMPLEMENTED */
4771  r = BiddyManagedConstrain(MNG,f,c);
4772  BiddyRefresh(r); /* not always refreshed by BiddyManagedConstrain */
4773  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
4774  /* IMPLEMENTED */
4775  r = BiddyManagedConstrain(MNG,f,c);
4776  BiddyRefresh(r); /* not always refreshed by BiddyManagedConstrain */
4777  } else if ((biddyManagerType == BIDDYTYPEZBDD) ||
4778  (biddyManagerType == BIDDYTYPEZBDDC) ||
4779  (biddyManagerType == BIDDYTYPETZBDD))
4780  {
4781  fprintf(stderr,"Biddy_Constrain: this BDD type is not supported, yet!\n");
4782  return f;
4783  } else if (biddyManagerType == BIDDYTYPETZBDDC)
4784  {
4785  fprintf(stderr,"Biddy_Constrain: this BDD type is not supported, yet!\n");
4786  return biddyNull;
4787  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
4788  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
4789  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
4790  {
4791  fprintf(stderr,"Biddy_Constrain: this BDD type is not supported, yet!\n");
4792  return biddyNull;
4793  } else {
4794  fprintf(stderr,"Biddy_Constrain: Unsupported BDD type!\n");
4795  return biddyNull;
4796  }
4797 
4798  return r;
4799 }
4800 
4801 #ifdef __cplusplus
4802 }
4803 #endif
4804 
4805 Biddy_Edge
4806 BiddyManagedConstrain(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge c)
4807 {
4808  Biddy_Edge f0,f1,c0,c1;
4809  Biddy_Edge e, t, r;
4810  Biddy_Variable fv,cv,minv;
4811 
4812  assert( MNG != NULL );
4813  assert( f != NULL );
4814  assert( c != NULL );
4815 
4816  /* IMPLEMENTED FOR OBDD AND OBDDC */
4817  assert(
4818  (biddyManagerType == BIDDYTYPEOBDD) ||
4819  (biddyManagerType == BIDDYTYPEOBDDC)
4820  );
4821 
4822  r = biddyNull;
4823 
4824  /* LOOKING FOR SIMPLE CASE */
4825  if (c == biddyZero) {
4826  return biddyZero;
4827  } else if (c == biddyOne) {
4828  return f;
4829  } else if (Biddy_IsTerminal(f)) {
4830  return f;
4831  }
4832 
4833  fv = BiddyV(f);
4834  cv = BiddyV(c);
4835 
4836  if (BiddyIsSmaller(fv,cv)) {
4837  f0 = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
4838  f1 = Biddy_InvCond(BiddyT(f),Biddy_GetMark(f));
4839  c0 = c;
4840  c1 = c;
4841  minv = fv;
4842  } else if (BiddyIsSmaller(cv,fv)) {
4843  f0 = f;
4844  f1 = f;
4845  c0 = Biddy_InvCond(BiddyE(c),Biddy_GetMark(c));
4846  c1 = Biddy_InvCond(BiddyT(c),Biddy_GetMark(c));
4847  minv = cv;
4848  } else {
4849  f0 = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
4850  f1 = Biddy_InvCond(BiddyT(f),Biddy_GetMark(f));
4851  c0 = Biddy_InvCond(BiddyE(c),Biddy_GetMark(c));
4852  c1 = Biddy_InvCond(BiddyT(c),Biddy_GetMark(c));
4853  minv = cv;
4854  }
4855 
4856  if (c0 == biddyZero) return BiddyManagedConstrain(MNG,f1,c1);
4857  if (c1 == biddyZero) return BiddyManagedConstrain(MNG,f0,c0);
4858 
4859  e = BiddyManagedConstrain(MNG,f0,c0);
4860  t = BiddyManagedConstrain(MNG,f1,c1);
4861  r = BiddyManagedITE(MNG,biddyVariableTable.table[minv].variable,t,e);
4862 
4863  return r;
4864 }
4865 
4866 /***************************************************************************/
4882 #ifdef __cplusplus
4883 extern "C" {
4884 #endif
4885 
4886 Biddy_Edge
4888 {
4889  Biddy_Edge r;
4890 
4891  assert( f != NULL );
4892  assert( c != NULL );
4893 
4894  if (!MNG) MNG = biddyAnonymousManager;
4895  ZF_LOGI("Biddy_Simplify");
4896 
4897  assert( BiddyIsOK(f) == TRUE );
4898  assert( BiddyIsOK(c) == TRUE );
4899 
4900  r = biddyNull;
4901 
4902  if (biddyManagerType == BIDDYTYPEOBDD) {
4903  /* IMPLEMENTED */
4904  r = BiddyManagedSimplify(MNG,f,c);
4905  BiddyRefresh(r); /* not always refreshed by BiddyManagedSimplify */
4906  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
4907  /* IMPLEMENTED */
4908  r = BiddyManagedSimplify(MNG,f,c);
4909  BiddyRefresh(r); /* not always refreshed by BiddyManagedSimplify */
4910  } else if ((biddyManagerType == BIDDYTYPEZBDD) ||
4911  (biddyManagerType == BIDDYTYPEZBDDC) ||
4912  (biddyManagerType == BIDDYTYPETZBDD))
4913  {
4914  fprintf(stderr,"Biddy_Simplify: this BDD type is not supported, yet!\n");
4915  return f;
4916  } else if (biddyManagerType == BIDDYTYPETZBDDC)
4917  {
4918  fprintf(stderr,"Biddy_Simplify: this BDD type is not supported, yet!\n");
4919  return biddyNull;
4920  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
4921  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
4922  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
4923  {
4924  fprintf(stderr,"Biddy_Simplify: this BDD type is not supported, yet!\n");
4925  return biddyNull;
4926  } else {
4927  fprintf(stderr,"Biddy_Simplify: Unsupported BDD type!\n");
4928  return biddyNull;
4929  }
4930 
4931  return r;
4932 }
4933 
4934 #ifdef __cplusplus
4935 }
4936 #endif
4937 
4938 Biddy_Edge
4939 BiddyManagedSimplify(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge c)
4940 {
4941  Biddy_Edge f0,f1,c0,c1;
4942  Biddy_Edge e, t, r;
4943  Biddy_Variable fv,cv,minv;
4944 
4945  assert( MNG != NULL );
4946  assert( f != NULL );
4947  assert( c != NULL );
4948 
4949  /* IMPLEMENTED FOR OBDD AND OBDDC */
4950  assert(
4951  (biddyManagerType == BIDDYTYPEOBDD) ||
4952  (biddyManagerType == BIDDYTYPEOBDDC)
4953  );
4954 
4955  r = biddyNull;
4956 
4957  /* LOOKING FOR SIMPLE CASE */
4958  if (c == biddyZero) return biddyNull;
4959  if (c == biddyOne) {
4960  return f;
4961  } else if (Biddy_IsTerminal(f)) {
4962  return f;
4963  }
4964 
4965  /* THIS IS FROM 20-CS-626-001 */
4966  /* http://gauss.ececs.uc.edu/Courses/c626/lectures/BDD/bdd-desc.pdf */
4967  if (f == c) return biddyOne;
4968  if (biddyManagerType == BIDDYTYPEOBDDC) {
4969  if (Biddy_IsEqvPointer(f,c)) {
4970  return biddyZero;
4971  }
4972  }
4973 
4974  fv = BiddyV(f);
4975  cv = BiddyV(c);
4976 
4977  /* SPECIAL CASE: f/~a == f/a */
4978  if (BiddyIsSmaller(cv,fv)) {
4979  return BiddyManagedSimplify(MNG,f,BiddyManagedE(MNG,c,cv));
4980  }
4981 
4982  if (BiddyIsSmaller(fv,cv)) {
4983  f0 = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
4984  f1 = Biddy_InvCond(BiddyT(f),Biddy_GetMark(f));
4985  c0 = c;
4986  c1 = c;
4987  minv = fv;
4988  } else {
4989  f0 = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
4990  f1 = Biddy_InvCond(BiddyT(f),Biddy_GetMark(f));
4991  c0 = Biddy_InvCond(BiddyE(c),Biddy_GetMark(c));
4992  c1 = Biddy_InvCond(BiddyT(c),Biddy_GetMark(c));
4993  minv = cv;
4994  }
4995 
4996  if (c0 == biddyZero) return BiddyManagedSimplify(MNG,f1,c1);
4997  if (c1 == biddyZero) return BiddyManagedSimplify(MNG,f0,c0);
4998 
4999  e = BiddyManagedSimplify(MNG,f0,c0);
5000  t = BiddyManagedSimplify(MNG,f1,c1);
5001  r = BiddyManagedITE(MNG,biddyVariableTable.table[minv].variable,t,e);
5002 
5003  return r;
5004 }
5005 
5006 /***************************************************************************/
5022 #ifdef __cplusplus
5023 extern "C" {
5024 #endif
5025 
5026 Biddy_Edge
5028 {
5029  Biddy_Edge r;
5030 
5031  if (!MNG) MNG = biddyAnonymousManager;
5032  ZF_LOGI("Biddy_Support");
5033 
5034  assert( (f == NULL) || (BiddyIsOK(f) == TRUE) );
5035 
5036  r = biddyNull;
5037 
5038  if (biddyManagerType == BIDDYTYPEOBDD) {
5039  /* IMPLEMENTED */
5040  r = BiddyManagedSupport(MNG,f);
5041  BiddyRefresh(r); /* not always refreshed by BiddyManagedSupport */
5042  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
5043  /* IMPLEMENTED */
5044  r = BiddyManagedSupport(MNG,f);
5045  BiddyRefresh(r); /* not always refreshed by BiddyManagedSupport */
5046  } else if (biddyManagerType == BIDDYTYPEZBDD) {
5047  /* PROTOTYPED USING Restrict */
5048  /*
5049  Biddy_Variable v;
5050  r = biddyTerminal;
5051  for (v=1;v<biddyVariableTable.num;v++) {
5052  if (BiddyManagedRestrict(MNG,f,v,FALSE) != BiddyManagedRestrict(MNG,f,v,TRUE)) {
5053  r = BiddyManagedChange(MNG,r,v);
5054  }
5055  }
5056  */
5057  /* IMPLEMENTED */
5058  r = BiddyManagedSupport(MNG,f);
5059  BiddyRefresh(r); /* not always refreshed by BiddyManagedSupport */
5060  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
5061  /* PROTOTYPED USING Restrict */
5062  /*
5063  Biddy_Variable v;
5064  r = biddyTerminal;
5065  for (v=1;v<biddyVariableTable.num;v++) {
5066  if (BiddyManagedRestrict(MNG,f,v,FALSE) != BiddyManagedRestrict(MNG,f,v,TRUE)) {
5067  r = BiddyManagedChange(MNG,r,v);
5068  }
5069  }
5070  */
5071  /* IMPLEMENTED */
5072  r = BiddyManagedSupport(MNG,f);
5073  BiddyRefresh(r); /* not always refreshed by BiddyManagedSupport */
5074  } else if (biddyManagerType == BIDDYTYPETZBDD) {
5075  /* PROTOTYPED USING Restrict */
5076  /*
5077  Biddy_Variable v;
5078  r = biddyOne;
5079  for (v=1;v<biddyVariableTable.num;v++) {
5080  if (BiddyManagedRestrict(MNG,f,v,FALSE) != BiddyManagedRestrict(MNG,f,v,TRUE)) {
5081  r = BiddyManagedAnd(MNG,r,biddyVariableTable.table[v].variable);
5082  }
5083  }
5084  */
5085  /* IMPLEMENTED */
5086  r = BiddyManagedSupport(MNG,f);
5087  BiddyRefresh(r); /* not always refreshed by BiddyManagedSupport */
5088  } else if (biddyManagerType == BIDDYTYPETZBDDC)
5089  {
5090  fprintf(stderr,"Biddy_Support: this BDD type is not supported, yet!\n");
5091  return biddyNull;
5092  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
5093  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
5094  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
5095  {
5096  fprintf(stderr,"Biddy_Support: this BDD type is not supported, yet!\n");
5097  return biddyNull;
5098  } else {
5099  fprintf(stderr,"Biddy_Support: Unsupported BDD type!\n");
5100  return biddyNull;
5101  }
5102 
5103  return r;
5104 }
5105 
5106 #ifdef __cplusplus
5107 }
5108 #endif
5109 
5110 Biddy_Edge
5111 BiddyManagedSupport(Biddy_Manager MNG, Biddy_Edge f)
5112 {
5113  Biddy_Variable v;
5114  unsigned int n;
5115  Biddy_Edge s;
5116 
5117  assert( MNG != NULL );
5118 
5119  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDDC, and TZBDD */
5120  assert(
5121  (biddyManagerType == BIDDYTYPEOBDD) ||
5122  (biddyManagerType == BIDDYTYPEOBDDC) ||
5123  (biddyManagerType == BIDDYTYPEZBDD) ||
5124  (biddyManagerType == BIDDYTYPEZBDDC) ||
5125  (biddyManagerType == BIDDYTYPETZBDD)
5126  );
5127 
5128  if (Biddy_IsNull(f)) return biddyNull;
5129  if (Biddy_IsTerminal(f)) return biddyZero;
5130 
5131  /* MAKE VARIABLES UNSELECTED */
5132  /*
5133  for (v=1;v<biddyVariableTable.num;v++) {
5134  biddyVariableTable.table[v].selected = FALSE;
5135  }
5136  */
5137 
5138  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
5139  n = 1; /* NUMBER OF NODES NOT NEEDED, BUT NODES ARE COUNTED BY BiddyNodeVarNumber */
5140  Biddy_Managed_SelectNode(MNG,biddyTerminal); /* for OBDDs, this is needed for BiddyNodeVarNumber */
5141  BiddyNodeVarNumber(MNG,f,&n); /* DEPENDENT VARIABLES ARE MARKED, all nodes are selected */
5143  }
5144  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
5145  BiddyCreateLocalInfo(MNG,f); /* FOR ZBDDs, localinfo IS USED BY BiddyNodeVarNumber */
5146  n = 1; /* NUMBER OF NODES NOT NEEDED, BUT NODES ARE COUNTED BY BiddyNodeVarNumber */
5147  BiddyNodeVarNumber(MNG,f,&n); /* DEPENDENT VARIABLES ARE MARKED, selects all except terminal node */
5148  BiddyDeleteLocalInfo(MNG,f); /* FOR ZBDDs, localinfo IS USED BY BiddyNodeVarNumber */
5149  }
5150  else if (biddyManagerType == BIDDYTYPETZBDD) {
5151  n = 1; /* NUMBER OF NODES NOT NEEDED, BUT NODES ARE COUNTED BY BiddyNodeVarNumber */
5152  Biddy_Managed_SelectNode(MNG,biddyTerminal); /* for TZBDDs, this is needed for BiddyNodeVarNumber */
5153  BiddyNodeVarNumber(MNG,f,&n); /* DEPENDENT VARIABLES ARE MARKED, all nodes are selected */
5155  /* variables above the top variable which are equal or greater than the top tag are also dependent */
5156  v = Biddy_GetTag(f);
5157  while (BiddyIsSmaller(v,BiddyV(f))) {
5158  biddyVariableTable.table[v].selected = TRUE; /* select variable */
5159  v = biddyVariableTable.table[v].next;
5160  }
5161  }
5162 
5163  s = biddyNull;
5164  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
5165  s = biddyOne;
5166  for (v=1;v<biddyVariableTable.num;v++) {
5167  if (biddyVariableTable.table[v].selected == TRUE) {
5168  s = BiddyManagedAnd(MNG,s,biddyVariableTable.table[v].variable);
5169  biddyVariableTable.table[v].selected = FALSE;
5170  }
5171  }
5172  }
5173  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
5174  /* NOTE: for ZBDDs, variables above the top variable (which are always all dependent) */
5175  /* are not selected by BiddyNodeVarNumber! */
5176  s = biddyTerminal; /* this is base set */
5177  for (v=1;v<biddyVariableTable.num;v++) {
5178  if ((biddyVariableTable.table[v].selected == TRUE) || BiddyIsSmaller(v,BiddyV(f)))
5179  {
5180  s = BiddyManagedChange(MNG,s,v);
5181  biddyVariableTable.table[v].selected = FALSE;
5182  }
5183  }
5184  }
5185  else if (biddyManagerType == BIDDYTYPETZBDD) {
5186  s = biddyOne;
5187  for (v=1;v<biddyVariableTable.num;v++) {
5188  if (biddyVariableTable.table[v].selected == TRUE) {
5189  s = BiddyManagedAnd(MNG,s,biddyVariableTable.table[v].variable);
5190  biddyVariableTable.table[v].selected = FALSE;
5191  }
5192  }
5193  }
5194 
5195  return s;
5196 }
5197 
5198 /***************************************************************************/
5220 #ifdef __cplusplus
5221 extern "C" {
5222 #endif
5223 
5224 Biddy_Edge
5226  Biddy_String keyword)
5227 {
5228  Biddy_Edge r;
5229  unsigned int key;
5230  Biddy_Boolean OK;
5231  int cc;
5232  const Biddy_Boolean disableCache = FALSE;
5233  Biddy_Edge tmp, e, t;
5234  Biddy_Variable v;
5235 
5236  assert( f != NULL );
5237 
5238  if (!MNG) MNG = biddyAnonymousManager;
5239  ZF_LOGI("Biddy_Replace");
5240 
5241  assert( BiddyIsOK(f) == TRUE );
5242 
5243  if (f == biddyZero) return f;
5244  if (f == Biddy_Managed_GetConstantOne(MNG)) return f;
5245 
5246  r = biddyNull;
5247 
5248  /* find keyword in keywordList */
5249 
5250  /* VARIANT A: LINEAR SEARCH */
5251  key = 0;
5252  if (!disableCache && keyword) {
5253  OK = FALSE;
5254  if (biddyReplaceCache.keywordList) {
5255  for (key = 0; !OK && (key < biddyReplaceCache.keywordNum); key++) {
5256  cc = strcmp(keyword,biddyReplaceCache.keywordList[key]);
5257  if (cc == 0) {
5258  OK = TRUE;
5259  break;
5260  }
5261  if (cc < 0) break;
5262  }
5263  }
5264  }
5265 
5266  /* TO DO: BINARY SEARCH */
5267  /* NOT IMPORTANT BECAUSE NUMBER OF KEYWORDS IS VERY SMALL IN THE PRACTICE */
5268 
5269  if (disableCache || !keyword) {
5270  /* keyword not given */
5271  key = ++biddyReplaceCache.keyNum;
5272  } else {
5273  /* keyword given but not found - it will be added */
5274  if (!OK) {
5275  Biddy_String *tmp1;
5276  unsigned int *tmp2;
5277 
5278  biddyReplaceCache.keywordNum++;
5279  if (!(tmp1 = (Biddy_String *)
5280  realloc(biddyReplaceCache.keywordList,biddyReplaceCache.keywordNum*sizeof(Biddy_String))))
5281  {
5282  fprintf(stderr,"Biddy_Managed_ReplaceByKeyword: Out of memoy!\n");
5283  exit(1);
5284  }
5285  biddyReplaceCache.keywordList = tmp1;
5286  if (!(tmp2 = (unsigned int *)
5287  realloc(biddyReplaceCache.keyList,biddyReplaceCache.keywordNum*sizeof(unsigned int))))
5288  {
5289  fprintf(stderr,"Biddy_Managed_ReplaceByKeyword: Out of memoy!\n");
5290  exit(1);
5291  }
5292  biddyReplaceCache.keyList = tmp2;
5293 
5294  memmove(&biddyReplaceCache.keywordList[key+1],&biddyReplaceCache.keywordList[key],(biddyReplaceCache.keywordNum-key-1)*sizeof(Biddy_String));
5295  memmove(&biddyReplaceCache.keyList[key+1],&biddyReplaceCache.keyList[key],(biddyReplaceCache.keywordNum-key-1)*sizeof(unsigned int));
5296  /*
5297  for (i = biddyReplaceCache.keywordNum-1; i > key; i--) {
5298  biddyReplaceCache.keywordList[i] = biddyReplaceCache.keywordList[i-1];
5299  biddyReplaceCache.keyList[i] = biddyReplaceCache.keyList[i-1];
5300  }
5301  */
5302 
5303  biddyReplaceCache.keywordList[key] = strdup(keyword);
5304  biddyReplaceCache.keyList[key] = ++biddyReplaceCache.keyNum;
5305  }
5306  key = biddyReplaceCache.keyList[key];
5307  }
5308 
5309  /* DEBUGGING */
5310  /*
5311  fprintf(stderr,"ReplaceByKeyword: keyword = %s, key = %u\n",keyword,key);
5312  */
5313 
5314  if (biddyManagerType == BIDDYTYPEOBDD) {
5315  /* IMPLEMENTED */
5316  if (!disableCache && !key) BiddyReplaceGarbageDeleteAll(MNG); /* purge Replace cache */
5317  r = BiddyManagedReplaceByKeyword(MNG,f,0,key);
5318  BiddyRefresh(r); /* not always refreshed by BiddyManagedReplaceByKeyword */
5319  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
5320  /* IMPLEMENTED */
5321  if (!disableCache && !key) BiddyReplaceGarbageDeleteAll(MNG); /* purge Replace cache */
5322  r = BiddyManagedReplaceByKeyword(MNG,f,0,key);
5323  BiddyRefresh(r); /* not always refreshed by BiddyManagedReplaceByKeyword */
5324  } else if (biddyManagerType == BIDDYTYPEZBDD) {
5325  /* NOT COMPLETELY IMPLEMENTED, YET */
5326  /*
5327  if (!disableCache && !key) BiddyReplaceGarbageDeleteAll(MNG); / * purge Replace cache * /
5328  r = BiddyManagedReplaceByKeyword(MNG,f,Biddy_Managed_GetLowestVariable(MNG),key);
5329  BiddyRefresh(r); / * not always refreshed by BiddyManagedReplaceByKeyword * /
5330  */
5331  /* PROTOTYPED */
5332 
5333  r = f;
5334  for (v=1;v<biddyVariableTable.num;v++) {
5335  if ((tmp=biddyVariableTable.table[v].value) != biddyZero) {
5336  e = BiddyManagedRestrict(MNG,r,v,FALSE);
5337  t = BiddyManagedRestrict(MNG,r,v,TRUE);
5338  tmp = Biddy_Managed_GetVariableEdge(MNG,BiddyV(tmp));
5339  r = BiddyManagedXor(MNG,
5340  BiddyManagedAnd(MNG,tmp,t),
5341  BiddyManagedAnd(MNG,BiddyManagedNot(MNG,tmp),e));
5342  BiddyRefresh(r); /* not always refreshed by BiddyManagedXor */
5343  }
5344  }
5345 
5346  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
5347  /* NOT COMPLETELY IMPLEMENTED, YET */
5348  /*
5349  if (!disableCache && !key) BiddyReplaceGarbageDeleteAll(MNG); / * purge Replace cache * /
5350  r = BiddyManagedReplaceByKeyword(MNG,f,Biddy_Managed_GetLowestVariable(MNG),key);
5351  BiddyRefresh(r); / * not always refreshed by BiddyManagedReplaceByKeyword * /
5352  */
5353  /* PROTOTYPED */
5354 
5355  r = f;
5356  for (v=1;v<biddyVariableTable.num;v++) {
5357  if ((tmp=biddyVariableTable.table[v].value) != biddyZero) {
5358  e = BiddyManagedRestrict(MNG,r,v,FALSE);
5359  t = BiddyManagedRestrict(MNG,r,v,TRUE);
5360  tmp = Biddy_Managed_GetVariableEdge(MNG,BiddyV(tmp));
5361  r = BiddyManagedXor(MNG,
5362  BiddyManagedAnd(MNG,tmp,t),
5363  BiddyManagedAnd(MNG,BiddyManagedNot(MNG,tmp),e));
5364  BiddyRefresh(r); /* not always refreshed by BiddyManagedXor */
5365  }
5366  }
5367 
5368  } else if (biddyManagerType == BIDDYTYPETZBDD) {
5369  /* IMPLEMENTED */
5370  if (!disableCache && !key) BiddyReplaceGarbageDeleteAll(MNG); /* purge Replace cache */
5371  r = BiddyManagedReplaceByKeyword(MNG,f,0,key);
5372  BiddyRefresh(r); /* not always refreshed by BiddyManagedReplaceByKeyword */
5373  } else if (biddyManagerType == BIDDYTYPETZBDDC)
5374  {
5375  fprintf(stderr,"Biddy_ReplaceByKeyword: this BDD type is not supported, yet!\n");
5376  return biddyNull;
5377  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
5378  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
5379  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
5380  {
5381  fprintf(stderr,"Biddy_ReplaceByKeyword: this BDD type is not supported, yet!\n");
5382  return biddyNull;
5383  } else {
5384  fprintf(stderr,"Biddy_ReplaceByKeyword: Unsupported BDD type!\n");
5385  return biddyNull;
5386  }
5387 
5388  return r;
5389 }
5390 
5391 #ifdef __cplusplus
5392 }
5393 #endif
5394 
5395 Biddy_Edge
5396 BiddyManagedReplaceByKeyword(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable topv,
5397  const unsigned int key)
5398 {
5399  Biddy_Edge e,t,r;
5400  Biddy_Variable fv;
5401  Biddy_Edge FF;
5402  Biddy_Boolean NN;
5403  unsigned int cindex;
5404 
5405  /* topv is used for ZBDD and ZBDDC, only */
5406  assert( MNG != NULL );
5407  assert( f != NULL );
5408 
5409  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
5410  assert(
5411  (biddyManagerType == BIDDYTYPEOBDD) ||
5412  (biddyManagerType == BIDDYTYPEOBDDC) ||
5413  (biddyManagerType == BIDDYTYPEZBDD) ||
5414  (biddyManagerType == BIDDYTYPEZBDDC) ||
5415  (biddyManagerType == BIDDYTYPETZBDD)
5416  );
5417 
5418  if (f == biddyZero) return f;
5419  if (Biddy_IsTerminal(f) && !Biddy_GetTag(f) && !topv) return f;
5420 
5421  r = biddyNull;
5422 
5423  if (Biddy_GetMark(f)) {
5424  NN = TRUE;
5425  FF = Biddy_Inv(f);
5426  } else {
5427  NN = FALSE;
5428  FF = f;
5429  }
5430 
5431  /* IF RESULT IS NOT IN THE CACHE TABLE... */
5432  cindex = 0;
5433  if ((((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) && (BiddyV(f) != topv)
5434  ) || !findKeywordCache(MNG,biddyReplaceCache,FF,key,&r,&cindex))
5435  {
5436 
5437  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
5438 
5439  fv = BiddyV(f);
5440  if ((r=biddyVariableTable.table[fv].value) != biddyZero) {
5441 
5442  assert( r != NULL );
5443 
5444  fv = BiddyV(r);
5445 
5446  assert( fv != 0 );
5447 
5448  /* DEBUGGING */
5449  /*
5450  printf("OBDD/OBDDC REPLACE: %s(%u) -> %s(%u)\n",
5451  Biddy_Managed_GetVariableName(MNG,BiddyV(f)),
5452  BiddyV(f),
5453  Biddy_Managed_GetVariableName(MNG,fv),
5454  fv
5455  );
5456  */
5457 
5458  } else {
5459 
5460  /* DEBUGGING */
5461  /*
5462  printf("OBDD/OBDDC REPLACE NOT REQUESTED FOR %s(%u)\n",
5463  Biddy_Managed_GetVariableName(MNG,fv),
5464  fv
5465  );
5466  */
5467 
5468  }
5469 
5470  e = BiddyManagedReplaceByKeyword(MNG,Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),0,key);
5471  t = BiddyManagedReplaceByKeyword(MNG,Biddy_InvCond(BiddyT(f),Biddy_GetMark(f)),0,key);
5472 
5473  /* VARIANT A */
5474  /* THIS IS NOT SLOW BECAUSE CACHE TABLE FOR ITE RESOLVES A LOT OF CALLS */
5475 
5476  r = BiddyManagedITE(MNG,biddyVariableTable.table[fv].variable,t,e);
5477 
5478 
5479  /* VARIANT B */
5480  /* THIS IS NOT AS FAST AS WE WANT IT */
5481  /*
5482  if (BiddyIsSmaller(fv,BiddyV(e)) && BiddyIsSmaller(fv,BiddyV(t))) {
5483  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,fv,TRUE);
5484  BiddyRefresh(r);
5485  } else {
5486  r = BiddyManagedITE(MNG,biddyVariableTable.table[fv].variable,t,e);
5487  }
5488  */
5489 
5490  }
5491 
5492  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
5493 
5494  fv = topv;
5495  if ((r = biddyVariableTable.table[fv].value) != biddyZero) {
5496 
5497  assert(r != NULL);
5498 
5499  fv = BiddyV(r);
5500 
5501  assert(fv != 0);
5502 
5503  /* DEBUGGING */
5504 
5505  printf("ZBDD/ZBDDC REPLACE: %s(%u) -> %s(%u)\n",
5507  topv,
5509  fv
5510  );
5511 
5512 
5513  } else {
5514 
5515  /* DEBUGGING */
5516 
5517  printf("ZBDD/ZBDDC REPLACE NOT REQUESTED FOR %s(%u)\n",
5519  fv
5520  );
5521 
5522 
5523  }
5524 
5525  if (BiddyIsSmaller(topv, BiddyV(f))) {
5526  e = BiddyManagedTaggedFoaNode(MNG,topv,f,f,topv,TRUE);
5527  BiddyRefresh(e); /* FoaNode returns an obsolete node! */
5528  e = BiddyManagedReplaceByKeyword(MNG,e,Biddy_Managed_GetNextVariable(MNG,topv),key);
5529  r = BiddyManagedITE(MNG,biddyVariableTable.table[fv].variable,biddyZero,e);
5530 
5531  printf("ZBDD/ZBDDC IS SMALLER: TOP OF FV = %s(%u)\n", Biddy_Managed_GetVariableName(MNG, BiddyV(biddyVariableTable.table[fv].variable)), BiddyV(biddyVariableTable.table[fv].variable));
5532  Biddy_Managed_PrintfBDD(MNG, biddyVariableTable.table[fv].variable);
5533  printf("ZBDD/ZBDDC IS SMALLER: TOP OF biddyZero = %s(%u)\n", Biddy_Managed_GetVariableName(MNG, BiddyV(biddyZero)), BiddyV(biddyZero));
5534  Biddy_Managed_PrintfBDD(MNG, biddyZero);
5535  printf("ZBDD/ZBDDC IS SMALLER: TOP OF E = %s(%u)\n", Biddy_Managed_GetVariableName(MNG, BiddyV(e)), BiddyV(e));
5536  Biddy_Managed_PrintfBDD(MNG, e);
5537  printf("ZBDD/ZBDDC IS SMALLER: TOP RESULT = %s(%u)\n", Biddy_Managed_GetVariableName(MNG, BiddyV(r)), BiddyV(r));
5538  Biddy_Managed_PrintfBDD(MNG, r);
5539 
5540  } else if (BiddyIsSmaller(BiddyV(f),topv)) {
5541  /* TO DO: I CANNOT FIND THE SOLUTION FOR THIS! */
5542  } else {
5543  e = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
5544  e = BiddyManagedTaggedFoaNode(MNG,topv,e,e,topv,TRUE);
5545  BiddyRefresh(e); /* FoaNode returns an obsolete node! */
5546  e = BiddyManagedReplaceByKeyword(MNG,e,Biddy_Managed_GetNextVariable(MNG,topv),key);
5547  t = BiddyT(f);
5548  t = BiddyManagedTaggedFoaNode(MNG,topv,t,t,topv,TRUE);
5549  BiddyRefresh(t); /* FoaNode returns an obsolete node! */
5550  t = BiddyManagedReplaceByKeyword(MNG,t,Biddy_Managed_GetNextVariable(MNG,topv),key);
5551  r = BiddyManagedITE(MNG,biddyVariableTable.table[fv].variable,t,e);
5552 
5553  printf("ZBDD/ZBDDC NOT SMALLER: TOP RESULT = %s(%u)\n", Biddy_Managed_GetVariableName(MNG, BiddyV(r)), BiddyV(r));
5554 
5555  }
5556 
5557  }
5558 
5559  else if (biddyManagerType == BIDDYTYPETZBDD) {
5560 
5561  fv = Biddy_GetTag(f);
5562  if ((r=biddyVariableTable.table[fv].value) != biddyZero) {
5563 
5564  assert( r != NULL );
5565 
5566  fv = BiddyV(r);
5567 
5568  assert( fv != 0 );
5569 
5570  /* DEBUGGING */
5571  /*
5572  printf("TZBDD REPLACE: %s(%u) -> %s(%u)\n",
5573  Biddy_Managed_GetVariableName(MNG,Biddy_GetTag(f)),
5574  Biddy_GetTag(f),
5575  Biddy_Managed_GetVariableName(MNG,fv),
5576  fv
5577  );
5578  */
5579 
5580  } else {
5581 
5582  /* DEBUGGING */
5583  /*
5584  printf("TZBDD REPLACE NOT REQUESTED FOR %s(%u)\n",
5585  Biddy_Managed_GetVariableName(MNG,fv),
5586  fv
5587  );
5588  */
5589 
5590  }
5591 
5592  if (BiddyIsSmaller(Biddy_GetTag(f),BiddyV(f))) {
5593  e = BiddyManagedReplaceByKeyword(MNG,Biddy_Managed_IncTag(MNG,f),0,key);
5594  r = BiddyManagedITE(MNG,biddyVariableTable.table[fv].variable,biddyZero,e);
5595  } else {
5596  e = BiddyManagedReplaceByKeyword(MNG,BiddyE(f),0,key);
5597  t = BiddyManagedReplaceByKeyword(MNG,BiddyT(f),0,key);
5598  r = BiddyManagedITE(MNG,biddyVariableTable.table[fv].variable,t,e);
5599  }
5600 
5601  }
5602 
5603  if (NN) {
5604  addKeywordCache(MNG,biddyReplaceCache,FF,key,Biddy_Inv(r),cindex);
5605  } else {
5606  addKeywordCache(MNG,biddyReplaceCache,FF,key,r,cindex);
5607  }
5608 
5609  } else {
5610 
5611  if (NN) {
5612  Biddy_InvertMark(r);
5613  }
5614 
5615  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
5616  BiddyRefresh(r);
5617 
5618  }
5619 
5620  return r;
5621 }
5622 
5623 /***************************************************************************/
5636 #ifdef __cplusplus
5637 extern "C" {
5638 #endif
5639 
5640 Biddy_Edge
5642 {
5643  Biddy_Edge r;
5644 
5645  assert( f != NULL );
5646 
5647  if (!MNG) MNG = biddyAnonymousManager;
5648  ZF_LOGI("Biddy_Change");
5649 
5650  assert( BiddyIsOK(f) == TRUE );
5651 
5652  r = biddyNull;
5653 
5654  if (biddyManagerType == BIDDYTYPEOBDD) {
5655  /* IMPLEMENTED */
5656  r = BiddyManagedChange(MNG,f,v);
5657  BiddyRefresh(r); /* not always refreshed by BiddyManagedChange */
5658  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
5659  /* IMPLEMENTED */
5660  r = BiddyManagedChange(MNG,f,v);
5661  BiddyRefresh(r); /* not always refreshed by BiddyManagedChange */
5662  } else if (biddyManagerType == BIDDYTYPEZBDD) {
5663  /* IMPLEMENTED */
5664  r = BiddyManagedChange(MNG,f,v);
5665  BiddyRefresh(r); /* not always refreshed by BiddyManagedChange */
5666  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
5667  /* IMPLEMENTED */
5668  r = BiddyManagedChange(MNG,f,v);
5669  BiddyRefresh(r); /* not always refreshed by BiddyManagedChange */
5670  } else if (biddyManagerType == BIDDYTYPETZBDD) {
5671  /* IMPLEMENTED */
5672  r = BiddyManagedChange(MNG,f,v);
5673  BiddyRefresh(r); /* not always refreshed by BiddyManagedChange */
5674  } else if (biddyManagerType == BIDDYTYPETZBDDC)
5675  {
5676  fprintf(stderr,"Biddy_Change: this BDD type is not supported, yet!\n");
5677  return biddyNull;
5678  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
5679  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
5680  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
5681  {
5682  fprintf(stderr,"Biddy_Change: this BDD type is not supported, yet!\n");
5683  return biddyNull;
5684  } else {
5685  fprintf(stderr,"Biddy_Change: Unsupported BDD type!\n");
5686  return biddyNull;
5687  }
5688 
5689  return r;
5690 }
5691 
5692 #ifdef __cplusplus
5693 }
5694 #endif
5695 
5696 Biddy_Edge
5697 BiddyManagedChange(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
5698 {
5699  Biddy_Edge e,t,r;
5700  Biddy_Variable fv,tag;
5701  Biddy_Edge FF, GG, HH;
5702  unsigned int cindex;
5703 
5704  assert( MNG != NULL );
5705  assert( f != NULL );
5706 
5707  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
5708  assert(
5709  (biddyManagerType == BIDDYTYPEOBDD) ||
5710  (biddyManagerType == BIDDYTYPEOBDDC) ||
5711  (biddyManagerType == BIDDYTYPEZBDD) ||
5712  (biddyManagerType == BIDDYTYPEZBDDC) ||
5713  (biddyManagerType == BIDDYTYPETZBDD)
5714  );
5715 
5716  if (f == biddyZero) return biddyZero;
5717 
5718  r = biddyNull;
5719 
5720  FF = f;
5721  GG = biddyNull;
5722  HH = biddyVariableTable.table[v].variable;
5723 
5724  /* IF RESULT IS NOT IN THE CACHE TABLE... */
5725  /* TO DO: CHECK ONLY IF IT IS POSSIBLE TO EXIST IN THE CACHE */
5726  cindex = 0;
5727  if (!findOp3Cache(MNG,biddyRCCache,FF,GG,HH,&r,&cindex))
5728  {
5729 
5730  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
5731  fv = BiddyV(f);
5732  if (v == fv) {
5733  e = Biddy_InvCond(BiddyT(f),Biddy_GetMark(f));
5734  t = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
5735  r = BiddyManagedTaggedFoaNode(MNG,v,e,t,v,TRUE);
5736  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5737  } else if (BiddyIsSmaller(v,fv)) {
5738  r = f;
5739  } else {
5740  e = BiddyManagedChange(MNG,Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),v);
5741  t = BiddyManagedChange(MNG,Biddy_InvCond(BiddyT(f),Biddy_GetMark(f)),v);
5742  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,fv,TRUE);
5743  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5744  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
5745  }
5746  }
5747 
5748  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
5749  fv = BiddyV(f);
5750  if (v == fv) {
5751  e = BiddyT(f);
5752  t = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
5753  r = BiddyManagedTaggedFoaNode(MNG,v,e,t,v,TRUE);
5754  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5755  } else if (BiddyIsSmaller(v,fv)) {
5756  r = BiddyManagedTaggedFoaNode(MNG,v,biddyZero,f,v,TRUE);
5757  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5758  } else {
5759  e = BiddyManagedChange(MNG,Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),v);
5760  t = BiddyManagedChange(MNG,BiddyT(f),v);
5761  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,fv,TRUE);
5762  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5763  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
5764  }
5765  }
5766 
5767  else if (biddyManagerType == BIDDYTYPETZBDD) {
5768  tag = Biddy_GetTag(f);
5769  if (BiddyIsSmaller(v,tag)) {
5770  r = f;
5771  } else {
5772  fv = BiddyV(f);
5773  if (v == fv) {
5774  e = BiddyT(f);
5775  t = BiddyE(f);
5776  r = BiddyManagedTaggedFoaNode(MNG,v,e,t,tag,TRUE);
5777  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5778  } else if (BiddyIsSmaller(v,fv)) {
5779  r = f;
5780  Biddy_SetTag(r,v);
5781  r = Biddy_Managed_IncTag(MNG,r);
5782  r = BiddyManagedTaggedFoaNode(MNG,v,biddyZero,r,tag,TRUE);
5783  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5784  } else {
5785  e = BiddyManagedChange(MNG,BiddyE(f),v);
5786  t = BiddyManagedChange(MNG,BiddyT(f),v);
5787  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,tag,TRUE);
5788  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5789  addOp3Cache(MNG,biddyRCCache,FF,GG,HH,r,cindex);
5790  }
5791  }
5792  }
5793 
5794  } else {
5795 
5796  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
5797  BiddyRefresh(r);
5798 
5799  }
5800 
5801  return r;
5802 }
5803 
5804 /***************************************************************************/
5821 #ifdef __cplusplus
5822 extern "C" {
5823 #endif
5824 
5825 Biddy_Edge
5827  Biddy_Boolean value)
5828 {
5829  Biddy_Edge r;
5830 
5831  assert( f != NULL );
5832 
5833  if (!MNG) MNG = biddyAnonymousManager;
5834  ZF_LOGI("Biddy_Subset");
5835 
5836  assert( BiddyIsOK(f) == TRUE );
5837 
5838  r = biddyNull;
5839 
5840  if (biddyManagerType == BIDDYTYPEOBDD) {
5841  /* IMPLEMENTED */
5842  r = BiddyManagedSubset(MNG,f,v,value);
5843  BiddyRefresh(r); /* not always refreshed by BiddyManagedSubset */
5844  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
5845  /* IMPLEMENTED */
5846  r = BiddyManagedSubset(MNG,f,v,value);
5847  BiddyRefresh(r); /* not always refreshed by BiddyManagedSubset */
5848  } else if (biddyManagerType == BIDDYTYPEZBDD) {
5849  /* IMPLEMENTED */
5850  r = BiddyManagedSubset(MNG,f,v,value);
5851  BiddyRefresh(r); /* not always refreshed by BiddyManagedSubset */
5852  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
5853  /* IMPLEMENTED */
5854  r = BiddyManagedSubset(MNG,f,v,value);
5855  BiddyRefresh(r); /* not always refreshed by BiddyManagedSubset */
5856  } else if (biddyManagerType == BIDDYTYPETZBDD) {
5857  /* IMPLEMENTED */
5858  r = BiddyManagedSubset(MNG,f,v,value);
5859  BiddyRefresh(r); /* not always refreshed by BiddyManagedSubset */
5860  } else if (biddyManagerType == BIDDYTYPETZBDDC)
5861  {
5862  fprintf(stderr,"Biddy_Subset: this BDD type is not supported, yet!\n");
5863  return biddyNull;
5864  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
5865  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
5866  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
5867  {
5868  fprintf(stderr,"Biddy_Subset: this BDD type is not supported, yet!\n");
5869  return biddyNull;
5870  } else {
5871  fprintf(stderr,"Biddy_Subset: Unsupported BDD type!\n");
5872  return biddyNull;
5873  }
5874 
5875  return r;
5876 }
5877 
5878 #ifdef __cplusplus
5879 }
5880 #endif
5881 
5882 Biddy_Edge
5883 BiddyManagedSubset(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v,
5884  Biddy_Boolean value)
5885 {
5886  Biddy_Edge h;
5887  Biddy_Edge e, t, r;
5888  Biddy_Variable fv,tag,ntag;
5889  Biddy_Edge FF, GG, HH;
5890  unsigned int cindex;
5891 
5892  assert( MNG != NULL );
5893  assert( f != NULL );
5894 
5895  /* IMPLEMENTED FOR OBDD, OBDDC, ZBDD, ZBDDC, AND TZBDD */
5896  assert(
5897  (biddyManagerType == BIDDYTYPEOBDD) ||
5898  (biddyManagerType == BIDDYTYPEOBDDC) ||
5899  (biddyManagerType == BIDDYTYPEZBDD) ||
5900  (biddyManagerType == BIDDYTYPEZBDDC) ||
5901  (biddyManagerType == BIDDYTYPETZBDD)
5902  );
5903 
5904  if (f == biddyZero) return biddyZero;
5905 
5906  FF = biddyNull;
5907  GG = biddyNull;
5908  HH = biddyNull;
5909 
5910  h = biddyVariableTable.table[v].variable;
5911  if (!value) {
5912  h = BiddyManagedNot(MNG,h);
5913  }
5914 
5915  /* TO DO: CACHE TABLE FOR OBDDC COULD BE OPTIMIZED BY USING COMPLEMENTED EDGES */
5916  if (biddyManagerType == BIDDYTYPEOBDDC) {
5917  if (((uintptr_t) f) > ((uintptr_t) h)) {
5918  FF = f;
5919  GG = h;
5920  HH = biddyZero;
5921  } else {
5922  FF = h;
5923  GG = f;
5924  HH = biddyZero;
5925  }
5926  }
5927 
5928  else {
5929  if (((uintptr_t) f) > ((uintptr_t) h)) {
5930  FF = f;
5931  GG = h;
5932  HH = biddyZero;
5933  } else {
5934  FF = h;
5935  GG = f;
5936  HH = biddyZero;
5937  }
5938  }
5939 
5940  /* IF RESULT IS NOT IN THE CACHE TABLE... */
5941  /* TO DO: CHECK ONLY IF IT IS POSSIBLE TO EXIST IN THE CACHE */
5942  cindex = 0;
5943  if (!findOp3Cache(MNG,biddyOPCache,FF,GG,HH,&r,&cindex))
5944  {
5945  if ((biddyManagerType == BIDDYTYPEOBDDC) || (biddyManagerType == BIDDYTYPEOBDD)) {
5946  if ((fv=BiddyV(f)) == v) {
5947  if (value) {
5948  r = BiddyManagedTaggedFoaNode(MNG,v,biddyZero,Biddy_InvCond(BiddyT(f),Biddy_GetMark(f)),v,TRUE);
5949  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5950  } else {
5951  r = BiddyManagedTaggedFoaNode(MNG,v,Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),biddyZero,v,TRUE);
5952  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5953  }
5954  }
5955  else if (BiddyIsSmaller(v,fv)) {
5956  if (value) {
5957  r = BiddyManagedTaggedFoaNode(MNG,v,biddyZero,f,v,TRUE);
5958  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5959  } else {
5960  r = BiddyManagedTaggedFoaNode(MNG,v,f,biddyZero,v,TRUE);
5961  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5962  }
5963  } else {
5964  e = BiddyManagedSubset(MNG,Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),v,value);
5965  t = BiddyManagedSubset(MNG,Biddy_InvCond(BiddyT(f),Biddy_GetMark(f)),v,value);
5966  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,fv,TRUE);
5967  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5968  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,r,cindex);
5969  }
5970  }
5971 
5972  else if ((biddyManagerType == BIDDYTYPEZBDDC) || (biddyManagerType == BIDDYTYPEZBDD)) {
5973  if ((fv=BiddyV(f)) == v) {
5974  if (value) {
5975  r = BiddyManagedTaggedFoaNode(MNG,v,biddyZero,BiddyT(f),v,TRUE);
5976  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5977  } else {
5978  r = Biddy_InvCond(BiddyE(f),Biddy_GetMark(f));
5979  }
5980  }
5981  else if (BiddyIsSmaller(v,fv)) {
5982  if (value) {
5983  r = biddyZero;
5984  } else {
5985  r = f;
5986  }
5987  } else {
5988  e = BiddyManagedSubset(MNG,Biddy_InvCond(BiddyE(f),Biddy_GetMark(f)),v,value);
5989  t = BiddyManagedSubset(MNG,BiddyT(f),v,value);
5990  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,fv,TRUE);
5991  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
5992  addOp3Cache(MNG,biddyOPCache,FF,GG,HH,r,cindex);
5993  }
5994  }
5995 
5996  else if (biddyManagerType == BIDDYTYPETZBDD) {
5997  tag = Biddy_GetTag(f);
5998  if (BiddyIsSmaller(v,tag)) {
5999  if (value) {
6000  r = BiddyManagedTaggedFoaNode(MNG,v,biddyZero,f,v,TRUE);
6001  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
6002  } else {
6003  ntag = biddyVariableTable.table[v].next;
6004  if (tag == ntag) {
6005  r = f;
6006  Biddy_SetTag(r,v);
6007  } else {
6008  r = BiddyManagedTaggedFoaNode(MNG,ntag,f,f,v,TRUE);
6009  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
6010  }
6011  }
6012  } else {
6013  fv = BiddyV(f);
6014  if (v == fv) {
6015  if (value) {
6016  r = BiddyManagedTaggedFoaNode(MNG,v,biddyZero,BiddyT(f),tag,TRUE);
6017  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
6018  } else {
6019  ntag = biddyVariableTable.table[v].next;
6020  e = BiddyE(f);
6021  if (ntag == Biddy_GetTag(e)) {
6022  r = e;
6023  if (r != biddyZero) {
6024  Biddy_SetTag(r,tag);
6025  }
6026  } else {
6027  r = BiddyManagedTaggedFoaNode(MNG,ntag,e,e,tag,TRUE);
6028  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
6029  }
6030  }
6031  } else if (BiddyIsSmaller(v,fv)) {
6032  if (value) {
6033  r = biddyZero;
6034  } else {
6035  r = f;
6036  }
6037  } else {
6038  e = BiddyManagedSubset(MNG,BiddyE(f),v,value);
6039  t = BiddyManagedSubset(MNG,BiddyT(f),v,value);
6040  r = BiddyManagedTaggedFoaNode(MNG,fv,e,t,tag,TRUE);
6041  BiddyRefresh(r); /* FoaNode returns an obsolete node! */
6042  }
6043  }
6044  }
6045 
6046  } else {
6047 
6048  /* IF THE RESULT IS FROM CACHE TABLE, REFRESH IT! */
6049  BiddyRefresh(r);
6050 
6051  }
6052 
6053  return r;
6054 }
6055 
6056 /***************************************************************************/
6069 #ifdef __cplusplus
6070 extern "C" {
6071 #endif
6072 
6073 Biddy_Edge
6075  long long unsigned int x)
6076 {
6077  long long unsigned int n;
6078  Biddy_Edge tmp,result;
6079 
6080  if (!MNG) MNG = biddyAnonymousManager;
6081  ZF_LOGI("Biddy_CreateMinterm");
6082 
6083  if (biddyManagerType == BIDDYTYPEOBDD) {
6084  /* IMPLEMENTED */
6085  /* assert( printf("Biddy_CreateMinterm: OBDD\n") ); */
6086  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
6087  /* IMPLEMENTED */
6088  /* assert( printf("Biddy_CreateMinterm: OBDDC\n") ); */
6089  } else if (biddyManagerType == BIDDYTYPEZBDD) {
6090  /* IMPLEMENTED */
6091  /* assert( printf("Biddy_CreateMinterm: ZBDD\n") ); */
6092  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
6093  /* IMPLEMENTED */
6094  /* assert( printf("Biddy_CreateMinterm: ZBDDC\n") ); */
6095  } else if (biddyManagerType == BIDDYTYPETZBDD) {
6096  /* IMPLEMENTED */
6097  /* assert( printf("Biddy_CreateMinterm: TZBDD\n") ); */
6098  } else if (biddyManagerType == BIDDYTYPETZBDDC)
6099  {
6100  fprintf(stderr,"Biddy_CreateMinterm: this BDD type is not supported, yet!\n");
6101  return biddyNull;
6102  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
6103  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
6104  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6105  {
6106  fprintf(stderr,"Biddy_CreateMinterm: this BDD type is not supported, yet!\n");
6107  return biddyNull;
6108  } else {
6109  fprintf(stderr,"Biddy_CreateMinterm: Unsupported BDD type!\n");
6110  return biddyNull;
6111  }
6112 
6113  n = 1;
6114  tmp = support;
6115  while (!Biddy_IsTerminal(tmp)) {
6116 
6117  if (!(n<(2*n))) {
6118  /* support has to many variables */
6119  return biddyNull;
6120  }
6121 
6122  n = 2 * n;
6123  tmp = BiddyT(tmp);
6124  }
6125 
6126  result = createMinterm(MNG,support,n,x);
6127  BiddyRefresh(result); /* not refreshed by minterm */
6128 
6129  return result;
6130 }
6131 
6132 #ifdef __cplusplus
6133 }
6134 #endif
6135 
6136 /***************************************************************************/
6149 #ifdef __cplusplus
6150 extern "C" {
6151 #endif
6152 
6153 Biddy_Edge
6154 Biddy_Managed_CreateFunction(Biddy_Manager MNG, Biddy_Edge support, long long unsigned int x)
6155 {
6156  long long unsigned int n,m,q;
6157  Biddy_Edge tmp,result;
6158 
6159  if (!MNG) MNG = biddyAnonymousManager;
6160  ZF_LOGI("Biddy_CreateFunction");
6161 
6162  if (biddyManagerType == BIDDYTYPEOBDD) {
6163  /* IMPLEMENTED */
6164  /* assert( printf("Biddy_CreateFunction: OBDD\n") ); */
6165  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
6166  /* IMPLEMENTED */
6167  /* assert( printf("Biddy_CreateFunction: OBDDC\n") ); */
6168  } else if (biddyManagerType == BIDDYTYPEZBDD) {
6169  /* IMPLEMENTED */
6170  /* assert( printf("Biddy_CreateFunction: ZBDD\n") ); */
6171  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
6172  /* IMPLEMENTED */
6173  /* assert( printf("Biddy_CreateFunction: ZBDDC\n") ); */
6174  } else if (biddyManagerType == BIDDYTYPETZBDD) {
6175  /* IMPLEMENTED */
6176  /* assert( printf("Biddy_CreateFunction: TZBDD\n") ); */
6177  } else if (biddyManagerType == BIDDYTYPETZBDDC)
6178  {
6179  fprintf(stderr,"Biddy_CreateFunction: this BDD type is not supported, yet!\n");
6180  return biddyNull;
6181  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
6182  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
6183  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6184  {
6185  fprintf(stderr,"Biddy_CreateFunction: this BDD type is not supported, yet!\n");
6186  return biddyNull;
6187  } else {
6188  fprintf(stderr,"Biddy_CreateFunction: Unsupported BDD type!\n");
6189  return biddyNull;
6190  }
6191 
6192  n = 1;
6193  tmp = support;
6194  while (!Biddy_IsTerminal(tmp)) {
6195 
6196  if (!(n<(2*n))) {
6197  /* support has to many variables */
6198  return biddyNull;
6199  }
6200 
6201  n = 2 * n;
6202  tmp = BiddyT(tmp);
6203  }
6204 
6205  m = 1;
6206  q = n;
6207  while (q>0) {
6208 
6209  if (!(m<(2*m))) {
6210  /* support has to many variables */
6211  return biddyNull;
6212  }
6213 
6214  m = 2 * m;
6215  q--;
6216  }
6217 
6218  result = createFunction(MNG,support,n,m,x);
6219  BiddyRefresh(result); /* not refreshed by function */
6220 
6221  return result;
6222 }
6223 
6224 #ifdef __cplusplus
6225 }
6226 #endif
6227 
6228 /***************************************************************************/
6245 #ifdef __cplusplus
6246 extern "C" {
6247 #endif
6248 
6249 Biddy_Edge
6251 {
6252  long long unsigned int n,m,x;
6253  Biddy_Edge tmp,result;
6254  Biddy_Boolean opposite;
6255 
6256  if (!MNG) MNG = biddyAnonymousManager;
6257  ZF_LOGI("Biddy_RandomFunction");
6258 
6259  if (biddyManagerType == BIDDYTYPEOBDD) {
6260  /* IMPLEMENTED */
6261  /* assert( printf("Biddy_Random: OBDD\n") ); */
6262  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
6263  /* IMPLEMENTED */
6264  /* assert( printf("Biddy_Random: OBDDC\n") ); */
6265  } else if (biddyManagerType == BIDDYTYPEZBDD) {
6266  /* IMPLEMENTED */
6267  /* assert( printf("Biddy_Random: ZBDD\n") ); */
6268  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
6269  /* IMPLEMENTED */
6270  /* assert( printf("Biddy_Random: ZBDDC\n") ); */
6271  } else if (biddyManagerType == BIDDYTYPETZBDD) {
6272  /* IMPLEMENTED */
6273  /* assert( printf("Biddy_Random: TZBDD\n") ); */
6274  } else if (biddyManagerType == BIDDYTYPETZBDDC)
6275  {
6276  fprintf(stderr,"Biddy_Random: this BDD type is not supported, yet!\n");
6277  return biddyNull;
6278  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
6279  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
6280  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6281  {
6282  fprintf(stderr,"Biddy_Random: this BDD type is not supported, yet!\n");
6283  return biddyNull;
6284  } else {
6285  fprintf(stderr,"Biddy_Random: Unsupported BDD type!\n");
6286  return biddyNull;
6287  }
6288 
6289  if ((r < 0.0) || (r > 1.0)) {
6290  return biddyNull;
6291  }
6292 
6293  n = 1;
6294  tmp = support;
6295  while (!Biddy_IsTerminal(tmp)) {
6296 
6297  if (!(n<(2*n))) {
6298  /* support has to many variables */
6299  return biddyNull;
6300  }
6301 
6302  n = 2 * n;
6303  tmp = BiddyT(tmp);
6304  }
6305 
6306  opposite = FALSE;
6307  if (r > 0.5) {
6308  r = 1.0 - r;
6309  opposite = TRUE;
6310  }
6311 
6312  m = (long long unsigned int) (0.5 + n * r);
6313 
6314  if (m == 0) {
6315  if (opposite) {
6316  return biddyOne;
6317  } else {
6318  return biddyZero;
6319  }
6320  }
6321 
6322  result = biddyZero;
6323  while (m != 0) {
6324 
6325  /* DEBUGGING */
6326  /*
6327  printf("RANDOM: m=%llu\n",m);
6328  */
6329 
6330  /* GENERATE RANDOM NUMBER */
6331  x = rand();
6332 
6333  /* DEBUGGING */
6334  /*
6335  printf("RANDOM NUMBER: x=%llu, n=%llu, RAND_MAX=%llu\n",x,n,RAND_MAX);
6336  */
6337 
6338  x = (n*x)/RAND_MAX;
6339 
6340  /* DEBUGGING */
6341  /*
6342  printf("RANDOM NUMBER = %llu\n",x);
6343  */
6344 
6345  tmp = createMinterm(MNG,support,n,x);
6346  tmp = BiddyManagedOr(MNG,result,tmp);
6347  if (tmp != result) {
6348  result = tmp;
6349  m--;
6350  }
6351 
6352  }
6353 
6354  if (opposite) {
6355  result = BiddyManagedNot(MNG,result);
6356  }
6357 
6358  BiddyRefresh(result); /* not always refreshed by Or/Not */
6359 
6360  return result;
6361 }
6362 
6363 #ifdef __cplusplus
6364 }
6365 #endif
6366 
6367 /***************************************************************************/
6384 #ifdef __cplusplus
6385 extern "C" {
6386 #endif
6387 
6388 Biddy_Edge
6390 {
6391  long long unsigned int n,m,x,z;
6392  Biddy_Edge p,q,tmp,result;
6393  Biddy_Boolean opposite;
6394  Biddy_Variable one;
6395 
6396  if (!MNG) MNG = biddyAnonymousManager;
6397  ZF_LOGI("Biddy_RandomSet");
6398 
6399  if (biddyManagerType == BIDDYTYPEOBDD) {
6400  /* IMPLEMENTED */
6401  /* assert( printf("Biddy_RandomSet: OBDD\n") ); */
6402  } else if (biddyManagerType == BIDDYTYPEOBDDC) {
6403  /* IMPLEMENTED */
6404  /* assert( printf("Biddy_RandomSet: OBDDC\n") ); */
6405  } else if (biddyManagerType == BIDDYTYPEZBDD) {
6406  /* IMPLEMENTED */
6407  /* assert( printf("Biddy_RandomSet: ZBDD\n") ); */
6408  } else if (biddyManagerType == BIDDYTYPEZBDDC) {
6409  /* IMPLEMENTED */
6410  /* assert( printf("Biddy_RandomSet: ZBDDC\n") ); */
6411  } else if (biddyManagerType == BIDDYTYPETZBDD) {
6412  /* IMPLEMENTED */
6413  /* assert( printf("Biddy_RandomSet: TZBDD\n") ); */
6414  } else if (biddyManagerType == BIDDYTYPETZBDDC)
6415  {
6416  fprintf(stderr,"Biddy_RandomSet: this BDD type is not supported, yet!\n");
6417  return biddyNull;
6418  } else if ((biddyManagerType == BIDDYTYPEOFDDC) || (biddyManagerType == BIDDYTYPEOFDD) ||
6419  (biddyManagerType == BIDDYTYPEZFDDC) || (biddyManagerType == BIDDYTYPEZFDD) ||
6420  (biddyManagerType == BIDDYTYPETZFDDC) || (biddyManagerType == BIDDYTYPETZFDD))
6421  {
6422  fprintf(stderr,"Biddy_RandomSet: this BDD type is not supported, yet!\n");
6423  return biddyNull;
6424  } else {
6425  fprintf(stderr,"Biddy_RandomSet: Unsupported BDD type!\n");
6426  return biddyNull;
6427  }
6428 
6429  if ((r < 0.0) || (r > 1.0)) {
6430  return biddyNull;
6431  }
6432 
6433  n = 1;
6434  p = unit;
6435  while (!Biddy_IsTerminal(p)) {
6436 
6437  if (!(n<(2*n))) {
6438  /* unit has to many variables */
6439  return biddyNull;
6440  }
6441 
6442  n = 2 * n;
6443  p = BiddyT(p);
6444  }
6445 
6446  opposite = FALSE;
6447  if (r > 0.5) {
6448  r = 1.0 - r;
6449  opposite = TRUE;
6450  }
6451 
6452  m = (long long unsigned int) (0.5 + n * r);
6453 
6454  if (m == 0) {
6455  if (opposite) {
6456  return biddyOne;
6457  } else {
6458  return biddyZero;
6459  }
6460  }
6461 
6462  result = biddyZero;
6463  while (m != 0) {
6464 
6465  /* DEBUGGING */
6466  /*
6467  printf("RANDOM SET: m=%llu\n",m);
6468  */
6469 
6470  /* GENERATE RANDOM NUMBER */
6471  x = rand();
6472  x = (n*x)/RAND_MAX;
6473 
6474  /* DEBUGGING */
6475  /*
6476  printf("RANDOM NUMBER = %llu\n",x);
6477  */
6478 
6479  p = unit;
6480  z = n;
6481  q = Biddy_Managed_GetBaseSet(MNG);
6482  while (z != 1) {
6483  one = BiddyV(p);
6484  p = BiddyT(p);
6485  if (x <= ((z - 0.5) / 2)) {
6486  z = (long long unsigned int) (z + 0.5) / 2;
6487  } else {
6488  z = (long long unsigned int) (z + 0.5) / 2;
6489  x = x - z;
6490  q = BiddyManagedChange(MNG,q,one);
6491  }
6492  }
6493 
6494  tmp = BiddyManagedUnion(MNG,result,q);
6495  if (tmp != result) {
6496  result = tmp;
6497  m--;
6498  }
6499 
6500  }
6501 
6502  if (opposite) {
6503  result = BiddyManagedNot(MNG,result);
6504  }
6505 
6506  BiddyRefresh(result); /* not always refreshed by Union/Not */
6507 
6508  return result;
6509 }
6510 
6511 #ifdef __cplusplus
6512 }
6513 #endif
6514 
6515 /*----------------------------------------------------------------------------*/
6516 /* Definition of internal functions */
6517 /*----------------------------------------------------------------------------*/
6518 
6519 /*******************************************************************************
6520 \brief Function BiddyOPGarbage performs Garbage Collection for the OP cache.
6521 
6522 ### Description
6523 ### Side effects
6524 ### More info
6525 *******************************************************************************/
6526 
6527 void
6528 BiddyOPGarbage(Biddy_Manager MNG)
6529 {
6530  unsigned int j;
6531  BiddyOp3Cache *c;
6532 
6533  if (biddyOPCache.disabled) return;
6534  if (*biddyOPCache.notusedyet) return;
6535 
6536  for (j=0; j<=biddyOPCache.size; j++) {
6537  if (!Biddy_IsNull(biddyOPCache.table[j].result)) {
6538 
6539  if (*biddyOPCache.notusedyet) {
6540  printf("CUDNO!\n");
6541  exit(1);
6542  }
6543 
6544  c = &biddyOPCache.table[j];
6545  /* VARIANT A */
6546  /*
6547  if (((BiddyN(c->f)->expiry) && ((BiddyN(c->f)->expiry) < biddySystemAge)) ||
6548  ((BiddyN(c->g)->expiry) && ((BiddyN(c->g)->expiry) < biddySystemAge)) ||
6549  ((BiddyN(c->h)->expiry) && ((BiddyN(c->h)->expiry) < biddySystemAge)) ||
6550  ((BiddyN(c->result)->expiry) && ((BiddyN(c->result)->expiry) < biddySystemAge)))
6551  */
6552  /* VARIANT B */
6553  /*
6554  if (((BiddyN(c->result)->expiry) && ((BiddyN(c->result)->expiry) < biddySystemAge)) ||
6555  ((BiddyN(c->f)->expiry) && ((BiddyN(c->f)->expiry) < biddySystemAge)) ||
6556  ((BiddyN(c->g)->expiry) && ((BiddyN(c->g)->expiry) < biddySystemAge)) ||
6557  ((BiddyN(c->h)->expiry) && ((BiddyN(c->h)->expiry) < biddySystemAge)))
6558  */
6559  /* VARIANT C */
6560 
6561  if (((BiddyN(c->f)->expiry) && ((BiddyN(c->f)->expiry) < biddySystemAge)) ||
6562  ((BiddyN(c->result)->expiry) && ((BiddyN(c->result)->expiry) < biddySystemAge)) ||
6563  ((BiddyN(c->g)->expiry) && ((BiddyN(c->g)->expiry) < biddySystemAge)) ||
6564  ((BiddyN(c->h)->expiry) && ((BiddyN(c->h)->expiry) < biddySystemAge)))
6565 
6566  {
6567  c->result = biddyNull;
6568  }
6569  }
6570  }
6571 }
6572 
6573 /*******************************************************************************
6574 \brief Function BiddyOPGarbageNewVariable is used to clean the OP cache after
6575  the adding new variable.
6576 
6577 ### Description
6578  This function is needed for BDD types where adding new variable below
6579  the existing one changes the meaning of the existing formulae.
6580 ### Side effects
6581 ### More info
6582 *******************************************************************************/
6583 
6584 void
6585 BiddyOPGarbageNewVariable(Biddy_Manager MNG, Biddy_Variable v)
6586 {
6587  unsigned int j;
6588  BiddyOp3Cache *c;
6589 
6590  if (biddyOPCache.disabled) return;
6591  if (*biddyOPCache.notusedyet) return;
6592 
6593  for (j=0; j<=biddyOPCache.size; j++) {
6594  if (!Biddy_IsNull(biddyOPCache.table[j].result)) {
6595  c = &biddyOPCache.table[j];
6596  if ((BiddyIsSmaller(BiddyN(c->f)->v,v)) ||
6597  (BiddyIsSmaller(BiddyN(c->g)->v,v)) ||
6598  (BiddyIsSmaller(BiddyN(c->h)->v,v)) ||
6599  (BiddyIsSmaller(BiddyN(c->result)->v,v)))
6600  {
6601  c->result = biddyNull;
6602  }
6603  }
6604  }
6605 }
6606 
6607 /*******************************************************************************
6608 \brief Function BiddyOPGarbageDeleteAll deletes all entries in the OP cache.
6609 
6610 ### Description
6611 ### Side effects
6612 ### More info
6613 *******************************************************************************/
6614 
6615 void
6616 BiddyOPGarbageDeleteAll(Biddy_Manager MNG)
6617 {
6618  /*
6619  unsigned int j;
6620  BiddyOp3Cache *c;
6621  */
6622 
6623  if (biddyOPCache.disabled) return;
6624  if (*biddyOPCache.notusedyet) return;
6625 
6626 
6627  memset(biddyOPCache.table,0,(biddyOPCache.size+1)*sizeof(BiddyOp3Cache));
6628 
6629 
6630  /*
6631  bzero(biddyOPCache.table, (biddyOPCache.size+1) * sizeof(BiddyOp3Cache));
6632  */
6633 
6634  /*
6635  for (j=0; j<=biddyOPCache.size; j++) {
6636  if (!Biddy_IsNull(biddyOPCache.table[j].result)) {
6637  c = &biddyOPCache.table[j];
6638  c->result = biddyNull;
6639  }
6640  }
6641  */
6642 
6643  *biddyOPCache.notusedyet = TRUE;
6644 }
6645 
6646 /*******************************************************************************
6647 \brief Function BiddyEAGarbage performs Garbage Collection for the EA cache.
6648 
6649 ### Description
6650 ### Side effects
6651 ### More info
6652 *******************************************************************************/
6653 
6654 void
6655 BiddyEAGarbage(Biddy_Manager MNG)
6656 {
6657  unsigned int j;
6658  BiddyOp3Cache *c;
6659 
6660  if (biddyEACache.disabled) return;
6661  if (*biddyEACache.notusedyet) return;
6662 
6663  for (j=0; j<=biddyEACache.size; j++) {
6664  if (!Biddy_IsNull(biddyEACache.table[j].result)) {
6665  c = &biddyEACache.table[j];
6666  if (((BiddyN(c->f)->expiry) && ((BiddyN(c->f)->expiry) < biddySystemAge)) ||
6667  ((BiddyN(c->g)->expiry) && ((BiddyN(c->g)->expiry) < biddySystemAge)) ||
6668  ((BiddyN(c->h)->expiry) && ((BiddyN(c->h)->expiry) < biddySystemAge)) ||
6669  ((BiddyN(c->result)->expiry) && ((BiddyN(c->result)->expiry) < biddySystemAge)))
6670  {
6671  c->result = biddyNull;
6672  }
6673  }
6674  }
6675 }
6676 
6677 /*******************************************************************************
6678 \brief Function BiddyEAGarbageNewVariable is used to clean the EA cache after
6679  the adding new variable.
6680 
6681 ### Description
6682  This function is needed for BDD types where adding new variable below
6683  the existing one changes the meaning of the existing formulae.
6684 ### Side effects
6685 ### More info
6686 *******************************************************************************/
6687 
6688 void
6689 BiddyEAGarbageNewVariable(Biddy_Manager MNG, Biddy_Variable v)
6690 {
6691  unsigned int j;
6692  BiddyOp3Cache *c;
6693 
6694  if (biddyEACache.disabled) return;
6695  if (*biddyEACache.notusedyet) return;
6696 
6697  for (j=0; j<=biddyEACache.size; j++) {
6698  if (!Biddy_IsNull(biddyEACache.table[j].result)) {
6699  c = &biddyEACache.table[j];
6700  if ((BiddyIsSmaller(BiddyN(c->f)->v,v)) ||
6701  (BiddyIsSmaller(BiddyN(c->g)->v,v)) ||
6702  (BiddyIsSmaller(BiddyN(c->h)->v,v)) ||
6703  (BiddyIsSmaller(BiddyN(c->result)->v,v)))
6704  {
6705  c->result = biddyNull;
6706  }
6707  }
6708  }
6709 }
6710 
6711 /*******************************************************************************
6712 \brief Function BiddyEAGarbageDeleteAll deletes all entries in the EA cache.
6713 
6714 ### Description
6715 ### Side effects
6716 ### More info
6717 *******************************************************************************/
6718 
6719 void
6720 BiddyEAGarbageDeleteAll(Biddy_Manager MNG)
6721 {
6722  unsigned int j;
6723  BiddyOp3Cache *c;
6724 
6725  if (biddyEACache.disabled) return;
6726  if (*biddyEACache.notusedyet) return;
6727 
6728  for (j=0; j<=biddyEACache.size; j++) {
6729  c = &biddyEACache.table[j];
6730  c->result = biddyNull;
6731  }
6732  *biddyEACache.notusedyet = TRUE;
6733 }
6734 
6735 /*******************************************************************************
6736 \brief Function BiddyRCGarbage performs Garbage Collection for the RC cache.
6737 
6738 ### Description
6739 ### Side effects
6740 ### More info
6741 *******************************************************************************/
6742 
6743 void
6744 BiddyRCGarbage(Biddy_Manager MNG)
6745 {
6746  unsigned int j;
6747  BiddyOp3Cache *c;
6748 
6749  if (biddyRCCache.disabled) return;
6750  if (*biddyRCCache.notusedyet) return;
6751 
6752  for (j=0; j<=biddyRCCache.size; j++) {
6753  if (!Biddy_IsNull(biddyRCCache.table[j].result)) {
6754  c = &biddyRCCache.table[j];
6755  if (((BiddyN(c->f)->expiry) && ((BiddyN(c->f)->expiry) < biddySystemAge)) ||
6756  (c->g && (BiddyN(c->g)->expiry) && ((BiddyN(c->g)->expiry) < biddySystemAge)) ||
6757  ((BiddyN(c->h)->expiry) && ((BiddyN(c->h)->expiry) < biddySystemAge)) ||
6758  ((BiddyN(c->result)->expiry) && ((BiddyN(c->result)->expiry) < biddySystemAge)))
6759  {
6760  c->result = biddyNull;
6761  }
6762  }
6763  }
6764 }
6765 
6766 /*******************************************************************************
6767 \brief Function BiddyRCGarbageNewVariable is used to clean the RC cache after
6768  the adding new variable.
6769 
6770 ### Description
6771  This function is needed for BDD types where adding new variable below
6772  the existing one changes the meaning of the existing formulae.
6773 ### Side effects
6774 ### More info
6775 *******************************************************************************/
6776 
6777 void
6778 BiddyRCGarbageNewVariable(Biddy_Manager MNG, Biddy_Variable v)
6779 {
6780  unsigned int j;
6781  BiddyOp3Cache *c;
6782 
6783  if (biddyRCCache.disabled) return;
6784  if (*biddyRCCache.notusedyet) return;
6785 
6786  for (j=0; j<=biddyRCCache.size; j++) {
6787  if (!Biddy_IsNull(biddyRCCache.table[j].result)) {
6788  c = &biddyRCCache.table[j];
6789  if ((BiddyIsSmaller(BiddyN(c->f)->v,v)) ||
6790  (c->g && BiddyIsSmaller(BiddyN(c->g)->v,v)) ||
6791  (BiddyIsSmaller(BiddyN(c->h)->v,v)) ||
6792  (BiddyIsSmaller(BiddyN(c->result)->v,v)))
6793  {
6794  c->result = biddyNull;
6795  }
6796  }
6797  }
6798 }
6799 
6800 /*******************************************************************************
6801 \brief Function BiddyRCGarbageDeleteAll deletes all entries in the RC cache.
6802 
6803 ### Description
6804 ### Side effects
6805 ### More info
6806 *******************************************************************************/
6807 
6808 void
6809 BiddyRCGarbageDeleteAll(Biddy_Manager MNG)
6810 {
6811  unsigned int j;
6812  BiddyOp3Cache *c;
6813 
6814  if (biddyRCCache.disabled) return;
6815  if (*biddyRCCache.notusedyet) return;
6816 
6817  for (j=0; j<=biddyRCCache.size; j++) {
6818  c = &biddyRCCache.table[j];
6819  c->result = biddyNull;
6820  }
6821  *biddyRCCache.notusedyet = TRUE;
6822 }
6823 
6824 /*******************************************************************************
6825 \brief Function BiddyReplaceGarbage performs Garbage Collection for the Replace
6826  cache.
6827 
6828 ### Description
6829 ### Side effects
6830 ### More info
6831 *******************************************************************************/
6832 
6833 void
6834 BiddyReplaceGarbage(Biddy_Manager MNG)
6835 {
6836  unsigned int j;
6837  BiddyKeywordCache *c;
6838 
6839  if (biddyReplaceCache.disabled) return;
6840  if (*biddyReplaceCache.notusedyet) return;
6841 
6842  for (j=0; j<=biddyReplaceCache.size; j++) {
6843  if (!Biddy_IsNull(biddyReplaceCache.table[j].result)) {
6844  c = &biddyReplaceCache.table[j];
6845  if (((BiddyN(c->f)->expiry) && ((BiddyN(c->f)->expiry) < biddySystemAge)) ||
6846  ((BiddyN(c->result)->expiry) && ((BiddyN(c->result)->expiry) < biddySystemAge)))
6847  {
6848  c->result = biddyNull;
6849  }
6850  }
6851  }
6852 }
6853 
6854 /*******************************************************************************
6855 \brief Function BiddyReplaceGarbageNewVariable is used to clean the Replace
6856  cache after the adding new variable.
6857 
6858 ### Description
6859  This function is needed for BDD types where adding new variable below
6860  the existing one changes the meaning of the existing formulae.
6861 ### Side effects
6862 ### More info
6863 *******************************************************************************/
6864 
6865 void
6866 BiddyReplaceGarbageNewVariable(Biddy_Manager MNG, Biddy_Variable v)
6867 {
6868  unsigned int j;
6869  BiddyKeywordCache *c;
6870 
6871  if (biddyReplaceCache.disabled) return;
6872  if (*biddyReplaceCache.notusedyet) return;
6873 
6874  for (j=0; j<=biddyReplaceCache.size; j++) {
6875  if (!Biddy_IsNull(biddyReplaceCache.table[j].result)) {
6876  c = &biddyReplaceCache.table[j];
6877  if ((BiddyIsSmaller(BiddyN(c->f)->v,v)) ||
6878  (BiddyIsSmaller(BiddyN(c->result)->v,v)))
6879  {
6880  c->result = biddyNull;
6881  }
6882  }
6883  }
6884 }
6885 
6886 /*******************************************************************************
6887 \brief Function BiddyReplaceGarbageDeleteAll deletes all entries in the Replace
6888  cache.
6889 
6890 ### Description
6891 ### Side effects
6892 ### More info
6893 *******************************************************************************/
6894 
6895 void
6896 BiddyReplaceGarbageDeleteAll(Biddy_Manager MNG)
6897 {
6898  unsigned int j;
6899  BiddyKeywordCache *c;
6900 
6901  if (biddyReplaceCache.disabled) return;
6902  if (*biddyReplaceCache.notusedyet) return;
6903 
6904  for (j=0; j<=biddyReplaceCache.size; j++) {
6905  c = &biddyReplaceCache.table[j];
6906  c->result = biddyNull;
6907  }
6908  *biddyReplaceCache.notusedyet = TRUE;
6909 }
6910 
6911 /*----------------------------------------------------------------------------*/
6912 /* Definition of static functions */
6913 /*----------------------------------------------------------------------------*/
6914 
6915 /*******************************************************************************
6916 \brief Function exchangeEdges exchanges two functions.
6917 
6918 ### Description
6919 ### Side effects
6920 ### More info
6921 *******************************************************************************/
6922 
6923 static void
6924 exchangeEdges(Biddy_Edge *f, Biddy_Edge *g)
6925 {
6926  Biddy_Edge sup;
6927 
6928  sup = *f;
6929  *f = *g;
6930  *g = sup;
6931 }
6932 
6933 /*******************************************************************************
6934 \brief Function complExchangeEdges complements and exchanges two functions.
6935 
6936 ### Description
6937 ### Side effects
6938 ### More info
6939 *******************************************************************************/
6940 
6941 static void
6942 complExchangeEdges(Biddy_Edge *f, Biddy_Edge *g)
6943 {
6944  Biddy_Edge sup;
6945 
6946  sup = *f;
6947  *f = *g;
6948  *g = sup;
6949  Biddy_InvertMark((*f));
6950  Biddy_InvertMark((*g));
6951 }
6952 
6953 /*******************************************************************************
6954 \brief Function createMinterm generates one minterm.
6955 
6956 ### Description
6957 ### Side effects
6958 ### More info
6959 *******************************************************************************/
6960 
6961 static Biddy_Edge
6962 createMinterm(Biddy_Manager MNG, Biddy_Edge support, long long unsigned int n,
6963  long long unsigned int x)
6964 {
6965  Biddy_Edge one,q;
6966 
6967  /* DEBUGGING */
6968  /*
6969  printf("createMinterm: %llu/%llu\n",x,(n-1));
6970  */
6971 
6972  q = biddyOne;
6973  while (n != 1) {
6974 
6975  one = biddyVariableTable.table[BiddyV(support)].variable;
6976 
6977  assert( !Biddy_IsTerminal(one) );
6978 
6979  support = BiddyT(support);
6980  n = n / 2;
6981  if (x < n) {
6982  q = BiddyManagedITE(MNG,one,biddyZero,q);
6983  } else {
6984  x = x - n;
6985  q = BiddyManagedITE(MNG,one,q,biddyZero);
6986  }
6987  }
6988 
6989  return q;
6990 }
6991 
6992 /*******************************************************************************
6993 \brief Function createFunction generates one Boolean function.
6994 
6995 ### Description
6996 ### Side effects
6997 ### More info
6998 *******************************************************************************/
6999 
7000 static Biddy_Edge
7001 createFunction(Biddy_Manager MNG, Biddy_Edge support, long long unsigned int n,
7002  long long unsigned int m, long long unsigned int x)
7003 {
7004  Biddy_Edge mnt,q;
7005  long long unsigned int y;
7006 
7007  q = biddyZero;
7008  y = 0;
7009  while (m > 1) {
7010  m = m / 2;
7011  if (x >= m) {
7012  x = x - m;
7013  mnt = createMinterm(MNG,support,n,y);
7014  q = BiddyManagedOr(MNG,q,mnt);
7015  }
7016  y++;
7017  }
7018 
7019  return q;
7020 }
7021 
7022 /*******************************************************************************
7023 \brief Function op3Hash.
7024 
7025 ### Description
7026 ### Side effects
7027 ### More info
7028 *******************************************************************************/
7029 
7030 static inline unsigned int
7031 op3Hash(Biddy_Edge a, Biddy_Edge b, Biddy_Edge c, unsigned int size)
7032 {
7033 
7034  unsigned int hash;
7035 
7036  /* this is very simple but quite efficient */
7037  /*
7038  {
7039  uintptr_t k;
7040  k = ((uintptr_t) a >> 4) + ((uintptr_t) b >> 2) + ((uintptr_t) c >> 4);
7041  hash = k & size;
7042  return hash;
7043  }
7044  */
7045 
7046 #if UINTPTR_MAX == 0xffffffffffffffff
7047 
7048  /* this is experimentally determined */
7049  /* rndc1 = 12582917, rndc2 = 4256249, >> 1,1,2,8, calls: 33415082 */
7050  /* rndc1 = 1982250849, rndc2 = 423214982, >> 0,0,0,16, calls: 33382146 */
7051  /* rndc1 = 1327958971, rndc2=516963069, >> 1,2,0,19, calls: 33374477 */
7052 
7053  {
7054  uintptr_t k;
7055  k = ((((uintptr_t) b >> 1) + ((uintptr_t) c >> 2)) * 1327958971 + (uintptr_t) a) * 516963069;
7056  hash = (k >> 19) & size;
7057  return hash;
7058  }
7059 
7060 
7061  /* this is using ideas from MURMUR3, see https://code.google.com/p/smhasher/ */
7062  /*
7063  {
7064  uintptr_t k,k1,k2;
7065  k = (uintptr_t) a;
7066  k1 = (uintptr_t) b;
7067  k1 = (k1 << 31) | (k1 >> 33);
7068  k ^= k1;
7069  k2 = (uintptr_t) c;
7070  k2 = (k2 << 35) | (k2 >> 29);
7071  k ^= k2;
7072  k *= 0xff51afd7ed558ccdL;
7073  k ^= k >> 32;
7074  k *= 0xc4ceb9fe1a85ec53L;
7075  k ^= k >> 32;
7076  hash = k & size;
7077  return hash;
7078  }
7079  */
7080 
7081 #else
7082 
7083  /* MURMUR3 (A KIND OF) 32-bit HASH FUNCTION */
7084  /* https://code.google.com/p/smhasher/ */
7085  {
7086  uintptr_t k,k1,k2;
7087  k = (uintptr_t) a;
7088  k1 = (uintptr_t) b;
7089  k1 = (k1 << 15) | (k1 >> 17);
7090  k ^= k1;
7091  k2 = (uintptr_t) c;
7092  k2 = (k2 << 19) | (k2 >> 13);
7093  k ^= k2;
7094  k *= 0x85ebca6b;
7095  k ^= k >> 16;
7096  k *= 0xc2b2ae35;
7097  k ^= k >> 16;
7098  hash = k & size;
7099  return hash;
7100  }
7101 
7102 #endif
7103 
7104  return 0;
7105 }
7106 
7107 /*******************************************************************************
7108 \brief Function keywordHash.
7109 
7110 ### Description
7111 ### Side effects
7112 ### More info
7113 *******************************************************************************/
7114 
7115 static inline unsigned int
7116 keywordHash(Biddy_Edge a, unsigned int k, unsigned int size)
7117 {
7118 
7119  unsigned int hash;
7120 
7121  /* this is very simple */
7122 
7123  {
7124  uintptr_t key;
7125  key = (uintptr_t) a >> 3;
7126  hash = key & size;
7127  return hash;
7128  }
7129 
7130 
7131 #if UINTPTR_MAX == 0xffffffffffffffff
7132 
7133  /* this is experimentally determined */
7134  {
7135  uintptr_t key;
7136  key = ((uintptr_t) a >> 3) * 1327958971;
7137  hash = (key >> 19) & size;
7138  return hash;
7139  }
7140 
7141 #else
7142 
7143  /* this is experimentally determined */
7144  {
7145  uintptr_t key;
7146  key = ((uintptr_t) a >> 3) * 7958971;
7147  hash = (key >> 13) & size;
7148  return hash;
7149  }
7150 
7151 #endif
7152 
7153  return 0;
7154 }
7155 
7156 /*******************************************************************************
7157 \brief Function addOp3Cache adds a result to the cache table for
7158  three-arguments operations.
7159 
7160 ### Description
7161 ### Side effects
7162 ### More info
7163 *******************************************************************************/
7164 
7165 static inline void
7166 addOp3Cache(Biddy_Manager MNG, BiddyOp3CacheTable cache, Biddy_Edge a,
7167  Biddy_Edge b, Biddy_Edge c, Biddy_Edge r, unsigned int index)
7168 {
7169  BiddyOp3Cache *p;
7170 
7171  if (cache.disabled) return;
7172 
7173  p = &cache.table[index];
7174 
7175 #ifdef BIDDYEXTENDEDSTATS_YES
7176  if (!Biddy_IsNull(p->result)) {
7177  /* THE CELL IS NOT EMPTY, THUS THIS IS OVERWRITING */
7178  (*cache.overwrite)++;
7179  }
7180 #endif
7181 
7182 #ifdef BIDDYEXTENDEDSTATS_YES
7183  (*cache.insert)++;
7184 #endif
7185 
7186  p->f = a;
7187  p->g = b;
7188  p->h = c;
7189  p->result = r;
7190 
7191  if (*cache.notusedyet) *cache.notusedyet = FALSE;
7192 }
7193 
7194 /*******************************************************************************
7195 \brief Function findOp3Cache looks for the result in the cache table for
7196  three-arguments operations.
7197 
7198 ### Description
7199 ### Side effects
7200 ### More info
7201 *******************************************************************************/
7202 
7203 static inline Biddy_Boolean
7204 findOp3Cache(Biddy_Manager MNG, BiddyOp3CacheTable cache, Biddy_Edge a,
7205  Biddy_Edge b, Biddy_Edge c, Biddy_Edge *r, unsigned int *index)
7206 {
7207  Biddy_Boolean q;
7208  BiddyOp3Cache *p;
7209 
7210  if (cache.disabled) return FALSE;
7211 
7212  q = FALSE;
7213 
7214  *index = op3Hash(a,b,c,cache.size);
7215  p = &cache.table[*index];
7216 
7217  (*cache.search)++;
7218 
7219  if ((p->f == a) &&
7220  (p->g == b) &&
7221  (p->h == c) &&
7222  !Biddy_IsNull(p->result)
7223  )
7224  {
7225  (*cache.find)++;
7226  *r = p->result;
7227  q = TRUE;
7228  }
7229 
7230  /* DEBUGGING */
7231  /*
7232  if (q) printf("OP3CACHE RETURNED: %p\n",(void *) *r);
7233  */
7234 
7235  return q;
7236 }
7237 
7238 /*******************************************************************************
7239 \brief Function addKeywordCache adds a result to the cache table for
7240  one-arguments operation and labels the entry with a given keyword.
7241 
7242 ### Description
7243 ### Side effects
7244 ### More info
7245 *******************************************************************************/
7246 
7247 static inline void
7248 addKeywordCache(Biddy_Manager MNG, BiddyKeywordCacheTable cache,
7249  Biddy_Edge a, unsigned int k, Biddy_Edge r,
7250  unsigned int index)
7251 {
7252  BiddyKeywordCache *p;
7253 
7254  if (cache.disabled) return;
7255 
7256  p = &cache.table[index];
7257 
7258 #ifdef BIDDYEXTENDEDSTATS_YES
7259  if (!Biddy_IsNull(p->result)) {
7260  /* THE CELL IS NOT EMPTY, THUS THIS IS OVERWRITING */
7261  (*cache.overwrite)++;
7262  }
7263 #endif
7264 
7265 #ifdef BIDDYEXTENDEDSTATS_YES
7266  (*cache.insert)++;
7267 #endif
7268 
7269  p->f = a;
7270  p->keyword = k;
7271  p->result = r;
7272 
7273  *cache.notusedyet = FALSE;
7274 }
7275 
7276 /*******************************************************************************
7277 \brief Function findKeywordCache looks for the result in the cache table for
7278  one-argument operation which is labelled with a given keyword.
7279 
7280 ### Description
7281 ### Side effects
7282 ### More info
7283 *******************************************************************************/
7284 
7285 static inline Biddy_Boolean
7286 findKeywordCache(Biddy_Manager MNG, BiddyKeywordCacheTable cache,
7287  Biddy_Edge a, unsigned int k, Biddy_Edge *r,
7288  unsigned int *index)
7289 {
7290  Biddy_Boolean q;
7291  BiddyKeywordCache *p;
7292 
7293  if (cache.disabled) return FALSE;
7294 
7295  q = FALSE;
7296 
7297  *index = keywordHash(a,k,cache.size);
7298  p = &cache.table[*index];
7299 
7300  (*cache.search)++;
7301 
7302  if ((p->f == a) &&
7303  (p->keyword == k) &&
7304  !Biddy_IsNull(p->result)
7305  )
7306  {
7307  (*cache.find)++;
7308  *r = p->result;
7309  q = TRUE;
7310  }
7311 
7312  return q;
7313 }
Biddy_Edge Biddy_Managed_Or(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Or calculates Boolean function OR (disjunction).
Definition: biddyOp.c:1243
Biddy_Variable is used for indices in variable table.
EXTERN Biddy_Variable Biddy_Managed_GetNextVariable(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetNextVariable returns next variable in the global ordering (higher...
Definition: biddyMain.c:1872
Biddy_Edge Biddy_Managed_Not(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Not calculates Boolean function NOT.
Definition: biddyOp.c:100
EXTERN void Biddy_Managed_SelectNode(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_SelectNode selects the top node of the given function.
Definition: biddyMain.c:1379
Biddy_Edge Biddy_Managed_A(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
Function Biddy_Managed_A calculates an universal quantification of Boolean function.
Definition: biddyOp.c:3815
Biddy_Edge Biddy_Managed_Leq(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Leq calculates Boolean implication.
Definition: biddyOp.c:2452
EXTERN void Biddy_Managed_DeselectAll(Biddy_Manager MNG)
Function Biddy_Managed_DeselectAll deselects all nodes.
Definition: biddyMain.c:1515
Biddy_Edge Biddy_Managed_Gt(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Gt calculates the negation of Boolean implication.
Definition: biddyOp.c:2767
EXTERN Biddy_Edge Biddy_Managed_IncTag(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_IncTag returns edge with an incremented tag.
Definition: biddyMain.c:3162
Biddy_Edge Biddy_Managed_Simplify(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge c)
Function Biddy_Managed_Simplify calculates Coudert and Madre&#39;s restrict function. ...
Definition: biddyOp.c:4887
Biddy_Edge Biddy_Managed_Constrain(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge c)
Function Biddy_Managed_Constrain calculates Coudert and Madre&#39;s constrain function.
Definition: biddyOp.c:4754
Biddy_Edge is a marked edge (i.e. a marked pointer to BiddyNode).
#define Biddy_InvertMark(f)
Definition: biddy.h:177
EXTERN Biddy_String Biddy_Managed_GetVariableName(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableName returns the name of a variable.
Definition: biddyMain.c:1951
#define Biddy_GetMark(f)
Definition: biddy.h:168
Biddy_Edge Biddy_Managed_AndAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Edge cube)
Function Biddy_Managed_AndAbstract calculates the AND of two BDDs and simultaneously (existentially) ...
Definition: biddyOp.c:4321
#define Biddy_InvCond(f, c)
Definition: biddy.h:184
#define Biddy_Inv(f)
Definition: biddy.h:181
EXTERN Biddy_Edge Biddy_Managed_GetBaseSet(Biddy_Manager MNG)
Function Biddy_Managed_GetBaseSet returns set containing only a null combination, i...
Definition: biddyMain.c:1647
Biddy_Edge Biddy_Managed_ExistAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge cube)
Function Biddy_Managed_ExistAbstract existentially abstracts all the variables in cube from f...
Definition: biddyOp.c:3973
Biddy_Edge Biddy_Managed_CreateMinterm(Biddy_Manager MNG, Biddy_Edge support, long long unsigned int x)
Function Biddy_Managed_CreateMinterm generates one minterm.
Definition: biddyOp.c:6074
Biddy_String is used for strings.
Biddy_Edge Biddy_Managed_E(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
Function Biddy_Managed_E calculates an existential quantification of Boolean function.
Definition: biddyOp.c:3610
Biddy_Edge Biddy_Managed_Support(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Support calculates a product of all dependent variables (OBDDs and TZBDDs) or ...
Definition: biddyOp.c:5027
Biddy_Edge Biddy_Managed_RandomSet(Biddy_Manager MNG, Biddy_Edge unit, double r)
Function Biddy_Managed_RandomSet generates a random BDD.
Definition: biddyOp.c:6389
Biddy_Edge Biddy_Managed_Restrict(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v, Biddy_Boolean value)
Function Biddy_Managed_Restrict calculates a restriction of Boolean function.
Definition: biddyOp.c:3161
Biddy_Edge Biddy_Managed_CreateFunction(Biddy_Manager MNG, Biddy_Edge support, long long unsigned int x)
Function Biddy_Managed_CreateFunction generates one Boolean function.
Definition: biddyOp.c:6154
Biddy_Edge Biddy_Managed_Nand(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Nand calculates Boolean function NAND (Sheffer).
Definition: biddyOp.c:1718
Biddy_Boolean is used for boolean values.
Biddy_Edge Biddy_Managed_ITE(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Edge h)
Function Biddy_Managed_ITE calculates ITE operation of three Boolean functions.
Definition: biddyOp.c:370
Biddy_Edge Biddy_Managed_UnivAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge cube)
Function Biddy_Managed_UnivAbstract universally abstracts all the variables in cube from f...
Definition: biddyOp.c:4226
Biddy_Edge Biddy_Managed_Xnor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Xnor calculates Boolean function XNOR.
Definition: biddyOp.c:2354
#define Biddy_GetTag(f)
Definition: biddy.h:199
#define Biddy_IsNull(f)
Definition: biddy.h:150
#define Biddy_IsEqvPointer(f, g)
Definition: biddy.h:165
Biddy_Edge Biddy_Managed_Subset(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v, Biddy_Boolean value)
Function Biddy_Managed_Subset calculates a division of Boolean function with a literal.
Definition: biddyOp.c:5826
EXTERN void Biddy_Managed_PrintfBDD(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_PrintfBDD writes raw format using printf.
Definition: biddyInOut.c:1080
Biddy_Edge Biddy_Managed_Nor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Nor calculates Boolean function NOR (Peirce).
Definition: biddyOp.c:1816
EXTERN Biddy_Edge Biddy_Managed_GetConstantOne(Biddy_Manager MNG)
Function Biddy_Managed_GetConstantOne returns constant 1.
Definition: biddyMain.c:1621
Biddy_Edge Biddy_Managed_ReplaceByKeyword(Biddy_Manager MNG, Biddy_Edge f, Biddy_String keyword)
Function Biddy_Managed_ReplaceByKeyword calculates Boolean function with one or more variables replac...
Definition: biddyOp.c:5225
Biddy_Manager is used to specify manager.
EXTERN Biddy_Edge Biddy_Managed_GetVariableEdge(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableEdge returns variable&#39;s edge.
Definition: biddyMain.c:1901
#define Biddy_SetTag(f, t)
Definition: biddy.h:208
Biddy_Boolean Biddy_Managed_IsLeq(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_IsLeq returns TRUE iff function f is included in function g.
Definition: biddyOp.c:3089
#define Biddy_IsTerminal(f)
Definition: biddy.h:160
Biddy_Edge Biddy_Managed_And(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_And calculates Boolean function AND (conjunction).
Definition: biddyOp.c:812
Biddy_Edge Biddy_Managed_RandomFunction(Biddy_Manager MNG, Biddy_Edge support, double r)
Function Biddy_Managed_RandomFunction generates a random BDD.
Definition: biddyOp.c:6250
Biddy_Edge Biddy_Managed_Xor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Xor calculates Boolean function XOR.
Definition: biddyOp.c:1913
EXTERN Biddy_Variable Biddy_GetTopVariable(Biddy_Edge f)
Function Biddy_GetTopVariable returns the top variable.
Definition: biddyMain.c:1320
File biddyInt.h contains declaration of internal data structures.
Biddy_Boolean Biddy_Managed_IsVariableDependent(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
Function Biddy_Managed_IsVariableDependent returns TRUE iff variable is dependent on others in a func...
Definition: biddyOp.c:3910
Biddy_Edge Biddy_Managed_Change(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
Function Biddy_Managed_Change change the form of the given variable (positive literal becomes negativ...
Definition: biddyOp.c:5641
Biddy_Edge Biddy_Managed_Compose(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Variable v)
Function Biddy_Managed_Compose calculates a composition of two Boolean functions. ...
Definition: biddyOp.c:3378