Biddy  2.1.1
A multi-platform Binary Decision Diagrams package
biddy.h
Go to the documentation of this file.
1 /***************************************************************************/
44 #ifndef _BIDDY
45 #define _BIDDY
46 
47 #include <stdio.h>
48 #include <stdlib.h>
49 #include <stdint.h>
50 #include <stdarg.h>
51 #include <time.h>
52 
53 /* ON MS WINDOWS + MINGW THERE HAS TO BE DEFINED MINGW */
54 /* ON GNU/LINUX THERE HAS TO BE DEFINED UNIX */
55 /* ON MACOSX THERE HAS TO BE DEFINED MACOSX */
56 
57 #ifdef UNIX
58 # ifndef EXTERN
59 # define EXTERN extern
60 # endif
61 # ifndef DATAEXTERN
62 # define DATAEXTERN extern
63 # endif
64 #endif
65 
66 #ifdef MACOSX
67 # ifndef EXTERN
68 # define EXTERN extern
69 # endif
70 # ifndef DATAEXTERN
71 # define DATAEXTERN extern
72 # endif
73 #endif
74 
75 #if defined(MINGW) || defined(_MSC_VER)
76 # ifdef BUILD_BIDDY
77 # undef EXTERN
78 # define EXTERN __declspec (dllexport)
79 # undef DATAEXTERN
80 # define DATAEXTERN extern __declspec (dllexport)
81 # else
82 # ifdef USE_BIDDY
83 # undef EXTERN
84 # define EXTERN __declspec (dllimport)
85 # undef DATAEXTERN
86 # define DATAEXTERN __declspec (dllimport)
87 # else
88 # undef EXTERN
89 # define EXTERN extern
90 # undef DATAEXTERN
91 # define DATAEXTERN extern
92 # endif
93 # endif
94 #endif
95 
96 #ifndef EXTERN
97 # define EXTERN extern
98 #endif
99 #ifndef DATAEXTERN
100 # define DATAEXTERN extern
101 #endif
102 
103 #ifndef BIDDYVERSION
104 #define BIDDYVERSION "2.0.3"
105 #endif
106 
107 /*----------------------------------------------------------------------------*/
108 /* Constant definitions */
109 /*----------------------------------------------------------------------------*/
110 
111 #ifndef TRUE
112 # define TRUE (0 == 0)
113 #endif
114 #ifndef FALSE
115 # define FALSE !TRUE
116 #endif
117 
118 /* Supported BDD types */
119 
120 #define BIDDYTYPEOBDD 1
121 #define BIDDYTYPENAMEOBDD "ROBDD"
122 
123 #define BIDDYTYPEOBDDC 2
124 #define BIDDYTYPENAMEOBDDC "ROBDD WITH COMPLEMENTED EDGES"
125 
126 #define BIDDYTYPEZBDD 3
127 #define BIDDYTYPENAMEZBDD "ZBDD"
128 
129 #define BIDDYTYPEZBDDC 4
130 #define BIDDYTYPENAMEZBDDC "ZBDD WITH COMPLEMENTED EDGES"
131 
132 #define BIDDYTYPETZBDD 5
133 #define BIDDYTYPENAMETZBDD "TAGGED ZBDD"
134 
135 #define BIDDYTYPETZBDDC 6
136 #define BIDDYTYPENAMETZBDDC "TAGGED ZBDD WITH COMPLEMENTED EDGES"
137 
138 #define BIDDYTYPEOFDD 7
139 #define BIDDYTYPENAMEOFDD "ROFDD"
140 
141 #define BIDDYTYPEOFDDC 8
142 #define BIDDYTYPENAMEOFDDC "ROFDD WITH COMPLEMENTED EDGES"
143 
144 #define BIDDYTYPEZFDD 9
145 #define BIDDYTYPENAMEZFDD "ZFDD"
146 
147 #define BIDDYTYPEZFDDC 10
148 #define BIDDYTYPENAMEZFDDC "ZFDD WITH COMPLEMENTED EDGES"
149 
150 #define BIDDYTYPETZFDD 11
151 #define BIDDYTYPENAMETZFDD "TZFDD"
152 
153 #define BIDDYTYPETZFDDC 12
154 #define BIDDYTYPENAMETZFDDC "TZFDD WITH COMPLEMENTED EDGES"
155 
156 /* Supported system statistics types */
157 
158 /* unsigned int Biddy_Managed_SystemStat(Biddy_Manager MNG, unsigned int stat) */
159 #define BIDDYSTATVARIABLETABLENUM 1
160 #define BIDDYSTATFORMULATABLENUM 2
161 #define BIDDYSTATNODETABLESIZE 3
162 #define BIDDYSTATNODETABLEBLOCKNUMBER 4
163 #define BIDDYSTATNODETABLEGENERATED 5
164 #define BIDDYSTATNODETABLEMAX 6
165 #define BIDDYSTATNODETABLENUM 7
166 #define BIDDYSTATNODETABLERESIZENUMBER 8
167 #define BIDDYSTATNODETABLEGCNUMBER 9
168 #define BIDDYSTATNODETABLEGCTIME 10
169 #define BIDDYSTATNODETABLESWAPNUMBER 11
170 #define BIDDYSTATNODETABLESIFTINGNUMBER 12
171 #define BIDDYSTATNODETABLEDRTIME 13
172 #define BIDDYSTATNODETABLEITENUMBER 14
173 #define BIDDYSTATNODETABLEANDORNUMBER 15
174 #define BIDDYSTATNODETABLEXORNUMBER 16
175 
176 /* unsigned long long int Biddy_Managed_SystemLongStat(...) */
177 #define BIDDYLONGSTATNODETABLEFOANUMBER 101
178 #define BIDDYLONGSTATNODETABLEFINDNUMBER 102
179 #define BIDDYLONGSTATNODETABLECOMPARENUMBER 103
180 #define BIDDYLONGSTATNODETABLEADDNUMBER 104
181 #define BIDDYLONGSTATNODETABLEITERECURSIVENUMBER 105
182 #define BIDDYLONGSTATNODETABLEANDORRECURSIVENUMBER 106
183 #define BIDDYLONGSTATNODETABLEXORRECURSIVENUMBER 107
184 #define BIDDYLONGSTATOPCACHESEARCH 108
185 #define BIDDYLONGSTATOPCACHEFIND 109
186 #define BIDDYLONGSTATOPCACHEINSERT 110
187 #define BIDDYLONGSTATOPCACHEOVERWRITE 111
188 
189 /*----------------------------------------------------------------------------*/
190 /* Macro definitions */
191 /*----------------------------------------------------------------------------*/
192 
194 /* null edge is hardcoded since Biddy v1.4 */
195 #define Biddy_IsNull(f) (f == NULL)
196 
198 /* succesors should be the third and the fourth field in BiddyNode */
199 /* non-terminal nodes should not have null edges as successors */
200 /* for reduced (minimal) OBDD and OFDD this means that the represented function is 0 or 1 */
201 /* for TZBDD, true is returned also for tagged edges to terminal node! */
202 #if UINTPTR_MAX == 0xffffffffffffffff
203 #define Biddy_IsTerminal(f) ((((void**)((uintptr_t) f & 0x0000fffffffffffe))[2] == NULL) && (((void**)((uintptr_t) f & 0x0000fffffffffffe))[3] == NULL))
204 #else
205 #define Biddy_IsTerminal(f) ((((void**)((uintptr_t) f & ~((uintptr_t) 1)))[2] == NULL) && (((void**)((uintptr_t) f & ~((uintptr_t) 1)))[3] == NULL))
206 #endif
207 
209 /* for OBDDs and OFDDs this means that represented functions are equal or inverted */
210 #define Biddy_IsEqvPointer(f,g) (((uintptr_t) f & ~((uintptr_t) 1)) == ((uintptr_t) g & ~((uintptr_t) 1)))
211 
213 #define Biddy_GetMark(f) (((uintptr_t) f & (uintptr_t) 1) != 0)
214 
216 #define Biddy_SetMark(f) (f = (Biddy_Edge) ((uintptr_t) f | (uintptr_t) 1))
217 
219 #define Biddy_ClearMark(f) (f = (Biddy_Edge) ((uintptr_t) f & ~((uintptr_t) 1)))
220 
222 #define Biddy_InvertMark(f) (f = (Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1))
223 
225 /* for OBDD and OFDD this is the same as Biddy_Not */
226 #define Biddy_Inv(f) ((Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1))
227 
229 #define Biddy_InvCond(f,c) (c ? ((Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1)) : f)
230 
232 #define Biddy_Regular(f) ((Biddy_Edge) ((uintptr_t) f & ~((uintptr_t) 1)))
233 
235 #define Biddy_Complement(f) ((Biddy_Edge) ((uintptr_t) f | (uintptr_t) 1))
236 
238 /* use the extended version if there are more than 32768 variables */
239 /* this macro assumes 64-bit architecture */
240 #if UINTPTR_MAX == 0xffffffffffffffff
241 #define Biddy_GetTag(f) ((Biddy_Variable) ((uintptr_t) f >> 48))
242 /* #define Biddy_GetTag(f) ((Biddy_Variable) (((uintptr_t) f >> 48) & 0x000000000000ffff)) */
243 #else
244 #define Biddy_GetTag(f) ((Biddy_Variable) 0)
245 #endif
246 
248 /* CAREFULLY: you can create an invalid node! */
249 /* this macro assumes 64-bit architecture */
250 #if UINTPTR_MAX == 0xffffffffffffffff
251 #define Biddy_SetTag(f,t) (f = (Biddy_Edge) (((uintptr_t) f & 0x0000ffffffffffff) | ((uintptr_t) t << 48)))
252 #else
253 #define Biddy_SetTag(f,t) (f = (Biddy_Edge) 0)
254 #endif
255 
257 /* this macro assumes 64-bit architecture */
258 #if UINTPTR_MAX == 0xffffffffffffffff
259 #define Biddy_ClearTag(f) (f = (Biddy_Edge) ((uintptr_t) f & 0x0000ffffffffffff))
260 #else
261 #define Biddy_ClearTag(f) (f = (Biddy_Edge) 0)
262 #endif
263 
265 /* this macro assumes 64-bit architecture */
266 #if UINTPTR_MAX == 0xffffffffffffffff
267 #define Biddy_Untagged(f) ((Biddy_Edge) ((uintptr_t) f & 0x0000ffffffffffff))
268 #else
269 #define Biddy_Untagged(f) ((Biddy_Edge) 0)
270 #endif
271 
272 /*----------------------------------------------------------------------------*/
273 /* Type declarations */
274 /*----------------------------------------------------------------------------*/
275 
278 typedef char Biddy_Boolean;
279 
282 typedef char *Biddy_String;
283 
293 typedef void **Biddy_Manager;
294 
300 typedef void *Biddy_Cache;
301 
304 /* for tagged graphs this should not be larger than 16 bits = unsigned short int */
305 #ifdef PLAIN
306 typedef unsigned int Biddy_Variable;
307 #else
308 typedef unsigned short int Biddy_Variable;
309 #endif
310 
320 typedef void* Biddy_Edge;
321 
325 typedef void (*Biddy_GCFunction)(Biddy_Manager);
326 
331 
332 /*----------------------------------------------------------------------------*/
333 /* Structure declarations */
334 /*----------------------------------------------------------------------------*/
335 
336 /*----------------------------------------------------------------------------*/
337 /* Variable declarations */
338 /*----------------------------------------------------------------------------*/
339 
340 #ifdef __cplusplus
341 extern "C" {
342 #endif
343 
344 #ifdef __cplusplus
345 }
346 #endif
347 
348 /*----------------------------------------------------------------------------*/
349 /* Prototypes for functions exported from biddyMain.c */
350 /*----------------------------------------------------------------------------*/
351 
352 #ifdef __cplusplus
353 extern "C" {
354 #endif
355 
356 /* 1 */
358 EXTERN void Biddy_InitMNG(Biddy_Manager *mng, int bddtype);
359 #define Biddy_Init() Biddy_InitMNG(NULL,BIDDYTYPEOBDD)
360 #define Biddy_InitAnonymous(bddtype) Biddy_InitMNG(NULL,bddtype)
361 
362 /* 2 */
364 EXTERN void Biddy_ExitMNG(Biddy_Manager *mng);
365 #define Biddy_Exit() Biddy_ExitMNG(NULL)
366 
367 /* 3 */
368 EXTERN Biddy_String Biddy_About();
369 
370 /* 4 */
372 #define Biddy_GetManagerType() Biddy_Managed_GetManagerType(NULL)
374 
375 /* 5 */
377 #define Biddy_GetManagerName() Biddy_Managed_GetManagerName(NULL)
379 
380 /* 6 */
382 #define Biddy_SetManagerParameters(gcr,gcrF,gcrX,rr,rrF,rrX,st,cst) Biddy_Managed_SetManagerParameters(NULL,gcr,gcrF,gcrX,rr,rrF,rrX,st,cst)
383 EXTERN void Biddy_Managed_SetManagerParameters(Biddy_Manager MNG, float gcr, float gcrF, float gcrX, float rr, float rrF, float rrX, float st, float cst);
384 
385 /* 7 */
387 #define Biddy_Managed_GetThen(MNG,f) Biddy_GetThen(f)
389 
390 /* 8 */
392 #define Biddy_Managed_GetElse(MNG,f) Biddy_GetElse(f)
394 
395 /* 9 */
397 #define Biddy_Managed_GetTopVariable(MNG,f) Biddy_GetTopVariable(f)
399 
400 /* 10 */
402 #define Biddy_IsEqv(f1,MNG2,f2) Biddy_Managed_IsEqv(NULL,f1,MNG2,f2)
404 
405 /* 11 */
407 #define Biddy_SelectNode(f) Biddy_Managed_SelectNode(NULL,f)
409 
410 /* 12 */
412 #define Biddy_DeselectNode(f) Biddy_Managed_DeselectNode(NULL,f)
414 
415 /* 13 */
417 #define Biddy_IsSelected(f) Biddy_Managed_IsSelected(NULL,f)
419 
420 /* 14 */
422 #define Biddy_SelectFunction(f) Biddy_Managed_SelectFunction(NULL,f)
424 
425 /* 15 */
427 #define Biddy_DeselectAll() Biddy_Managed_DeselectAll(NULL)
429 
430 /* 16 */
432 #define Biddy_GetTerminal() Biddy_Managed_GetTerminal(NULL)
434 
435 /* 17 */
437 #define Biddy_GetConstantZero() Biddy_Managed_GetConstantZero(NULL)
439 #define Biddy_Managed_GetEmptySet(MNG) Biddy_Managed_GetConstantZero(MNG)
440 #define Biddy_GetEmptySet() Biddy_Managed_GetConstantZero(NULL)
441 
442 /* 18 */
444 #define Biddy_GetConstantOne() Biddy_Managed_GetConstantOne(NULL)
446 #define Biddy_Managed_GetUniversalSet(MNG) Biddy_Managed_GetConstantOne(MNG)
447 #define Biddy_GetUniversalSet() Biddy_Managed_GetConstantOne(NULL)
448 
449 /* 19 */
451 #define Biddy_GetBaseSet() Biddy_Managed_GetBaseSet(NULL)
453 
454 /* 20 */
456 #define Biddy_GetVariable(x) Biddy_Managed_GetVariable(NULL,x)
458 
459 /* 21 */
461 #define Biddy_GetLowestVariable() Biddy_Managed_GetLowestVariable(NULL)
463 
464 /* 22 */
466 #define Biddy_GetIthVariable(i) Biddy_Managed_GetIthVariable(NULL,i)
468 
469 /* 23 */
471 #define Biddy_GetPrevVariable(v) Biddy_Managed_GetPrevVariable(NULL,v)
473 
474 /* 24 */
476 #define Biddy_GetNextVariable(v) Biddy_Managed_GetNextVariable(NULL,v)
478 
479 /* 25 */
481 #define Biddy_GetVariableEdge(v) Biddy_Managed_GetVariableEdge(NULL,v)
483 
484 /* 26 */
486 #define Biddy_GetElementEdge(v) Biddy_Managed_GetElementEdge(NULL,v)
488 
489 /* 27 */
491 #define Biddy_GetVariableName(v) Biddy_Managed_GetVariableName(NULL,v)
493 
494 /* 28 */
496 #define Biddy_GetTopVariableEdge(f) Biddy_Managed_GetTopVariableEdge(NULL,f)
498 
499 /* 29 */
501 #define Biddy_GetTopVariableName(f) Biddy_Managed_GetTopVariableName(NULL,f)
503 
504 /* 30 */
506 #define Biddy_GetTopVariableChar(f) Biddy_Managed_GetTopVariableChar(NULL,f)
508 
509 /* 31 */
511 #define Biddy_ResetVariablesValue() Biddy_Managed_ResetVariablesValue(NULL)
513 
514 /* 32 */
516 #define Biddy_SetVariableValue(v,f) Biddy_Managed_SetVariableValue(NULL,v,f)
518 
519 /* 33 */
521 #define Biddy_GetVariableValue(v) Biddy_Managed_GetVariableValue(NULL,v)
523 
524 /* 34 */
526 #define Biddy_ClearVariablesData() Biddy_Managed_ClearVariablesData(NULL)
528 
529 /* 35 */
531 #define Biddy_SetVariableData(v,x) Biddy_Managed_SetVariableData(NULL,v,x)
532 EXTERN void Biddy_Managed_SetVariableData(Biddy_Manager MNG, Biddy_Variable v, void *x);
533 
534 /* 36 */
536 #define Biddy_GetVariableData(v) Biddy_Managed_GetVariableData(NULL,v)
538 
539 /* 37 */
541 #define Biddy_Eval(f) Biddy_Managed_Eval(NULL,f)
543 
544 /* 38 */
546 #define Biddy_EvalProbability(f) Biddy_Managed_EvalProbability(NULL,f)
548 
549 /* 39 */
551 #define Biddy_IsSmaller(fv,gv) Biddy_Managed_IsSmaller(NULL,fv,gv)
553 
554 /* 40 */
556 #define Biddy_IsLowest(v) Biddy_Managed_IsLowest(NULL,v)
558 
559 /* 41 */
561 #define Biddy_IsHighest(v) Biddy_Managed_IsHighest(NULL,v)
563 
564 /* 42 */
566 #define Biddy_FoaVariable(x,varelem) Biddy_Managed_FoaVariable(NULL,x,varelem)
568 
569 /* 43 */
571 #define Biddy_ChangeVariableName(v,x) Biddy_Managed_ChangeVariableName(NULL,v,x)
573 
574 /* 44 */
578 #define Biddy_AddVariableByName(x) Biddy_Managed_AddVariableByName(NULL,x)
580 #define Biddy_Managed_AddVariable(MNG) Biddy_Managed_AddVariableByName(MNG,NULL)
581 #define Biddy_AddVariable() Biddy_Managed_AddVariableByName(NULL,NULL)
582 #define Biddy_Managed_AddVariableEdge(MNG) Biddy_Managed_GetVariableEdge(MNG,Biddy_Managed_AddVariableByName(MNG,NULL))
583 #define Biddy_AddVariableEdge() Biddy_Managed_GetVariableEdge(NULL,Biddy_Managed_AddVariableByName(NULL,NULL))
584 
585 /* 45 */
589 #define Biddy_AddElementByName(x) Biddy_Managed_AddElementByName(NULL,x)
591 #define Biddy_Managed_AddElement(MNG) Biddy_Managed_AddElementByName(MNG,NULL)
592 #define Biddy_AddElement() Biddy_Managed_AddElementByName(NULL,NULL)
593 #define Biddy_Managed_AddElementEdge(MNG) Biddy_Managed_GetElementEdge(MNG,Biddy_Managed_AddElementByName(MNG,NULL))
594 #define Biddy_AddElementEdge() Biddy_Managed_GetElementEdge(NULL,Biddy_Managed_AddElementByName(NULL,NULL))
595 
596 /* 46 */
598 #define Biddy_AddVariableBelow(v) Biddy_Managed_AddVariableBelow(NULL,v)
600 
601 /* 47 */
603 #define Biddy_AddVariableAbove(v) Biddy_Managed_AddVariableAbove(NULL,v)
605 
606 /* 48 */
609 #define Biddy_TransferMark(f,mark,leftright) Biddy_Managed_TransferMark(NULL,f,mark,leftright)
611 
612 /* 49 */
614 #define Biddy_IncTag(f) Biddy_Managed_IncTag(NULL,f)
616 
617 /* 50 */
619 #define Biddy_TaggedFoaNode(v,pf,pt,ptag,garbageAllowed) Biddy_Managed_TaggedFoaNode(NULL,v,pf,pt,ptag,garbageAllowed)
621 #define Biddy_Managed_FoaNode(MNG,v,pf,pt,garbageAllowed) Biddy_Managed_TaggedFoaNode(MNG,v,pf,pt,v,garbageAllowed)
622 #define Biddy_FoaNode(v,pf,pt,garbageAllowed) Biddy_Managed_TaggedFoaNode(NULL,v,pf,pt,v,garbageAllowed)
623 
624 /* 51 */
626 #define Biddy_IsOK(f) Biddy_Managed_IsOK(NULL,f)
628 
629 /* 52 */
632 #define Biddy_GC(targetLT,targetGEQ,purge,total) Biddy_Managed_GC(NULL,targetLT,targetGEQ,purge,total)
633 EXTERN void Biddy_Managed_GC(Biddy_Manager MNG, Biddy_Variable targetLT, Biddy_Variable targetGEQ, Biddy_Boolean purge, Biddy_Boolean total);
634 #define Biddy_Managed_AutoGC(MNG) Biddy_Managed_GC(MNG,0,0,FALSE,FALSE)
635 #define Biddy_AutoGC() Biddy_Managed_GC(NULL,0,0,FALSE,FALSE)
636 #define Biddy_Managed_ForceGC(MNG) Biddy_Managed_GC(MNG,0,0,FALSE,TRUE)
637 #define Biddy_ForceGC() Biddy_Managed_GC(NULL,0,0,FALSE,TRUE)
638 
639 /* 53 */
641 #define Biddy_Clean() Biddy_Managed_Clean(NULL)
642 EXTERN void Biddy_Managed_Clean(Biddy_Manager MNG);
643 
644 /* 54 */
646 #define Biddy_Purge() Biddy_Managed_Purge(NULL)
647 EXTERN void Biddy_Managed_Purge(Biddy_Manager MNG);
648 
649 /* 55 */
651 #define Biddy_PurgeAndReorder(f,c) Biddy_Managed_PurgeAndReorder(NULL,f,c)
653 
654 /* 56 */
656 #define Biddy_Refresh(f) Biddy_Managed_Refresh(NULL,f)
658 
659 /* 57 */
661 #define Biddy_AddCache(gc) Biddy_Managed_AddCache(NULL,gc)
663 
664 /* 58 */
672 #define Biddy_AddFormula(x,f,c) Biddy_Managed_AddFormula(NULL,x,f,c)
673 EXTERN unsigned int Biddy_Managed_AddFormula(Biddy_Manager MNG, Biddy_String x, Biddy_Edge f, int c);
674 #define Biddy_Managed_AddTmpFormula(MNG,x,f) Biddy_Managed_AddFormula(MNG,x,f,-1)
675 #define Biddy_Managed_AddPersistentFormula(MNG,x,f) Biddy_Managed_AddFormula(MNG,x,f,0)
676 #define Biddy_Managed_KeepFormula(MNG,f) Biddy_Managed_AddFormula(MNG,NULL,f,1)
677 #define Biddy_Managed_KeepFormulaProlonged(MNG,f,c) Biddy_Managed_AddFormula(MNG,NULL,f,c)
678 #define Biddy_Managed_KeepFormulaUntilPurge(MNG,f) Biddy_Managed_AddFormula(MNG,NULL,f,0)
679 #define Biddy_AddTmpFormula(x,f) Biddy_Managed_AddFormula(NULL,x,f,-1)
680 #define Biddy_AddPersistentFormula(x,f) Biddy_Managed_AddFormula(NULL,x,f,0)
681 #define Biddy_KeepFormula(f) Biddy_Managed_AddFormula(NULL,NULL,f,1)
682 #define Biddy_KeepFormulaProlonged(f,c) Biddy_Managed_AddFormula(NULL,NULL,f,c)
683 #define Biddy_KeepFormulaUntilPurge(f) Biddy_Managed_AddFormula(NULL,NULL,f,0)
684 
685 /* 59 */
687 #define Biddy_FindFormula(x,idx,f) Biddy_Managed_FindFormula(NULL,x,idx,f)
688 EXTERN Biddy_Boolean Biddy_Managed_FindFormula(Biddy_Manager MNG, Biddy_String x, unsigned int *idx, Biddy_Edge *f);
689 
690 /* 60 */
692 #define Biddy_DeleteFormula(x) Biddy_Managed_DeleteFormula(NULL,x)
694 
695 /* 61 */
697 #define Biddy_DeleteIthFormula(x) Biddy_Managed_DeleteIthFormula(NULL,x)
699 
700 /* 62 */
702 #define Biddy_GetIthFormula(i) Biddy_Managed_GetIthFormula(NULL,i)
703 EXTERN Biddy_Edge Biddy_Managed_GetIthFormula(Biddy_Manager MNG, unsigned int i);
704 
705 /* 63 */
707 #define Biddy_GetIthFormulaName(i) Biddy_Managed_GetIthFormulaName(NULL,i)
709 
710 /* 64 */
712 #define Biddy_GetOrdering() Biddy_Managed_GetOrdering(NULL)
713 EXTERN Biddy_String Biddy_Managed_GetOrdering(Biddy_Manager MNG);
714 
715 /* 65 */
717 #define Biddy_SetOrdering(ordering) Biddy_Managed_SetOrdering(NULL,ordering)
718 EXTERN void Biddy_Managed_SetOrdering(Biddy_Manager MNG, Biddy_String ordering);
719 
720 /* 66 */
722 #define Biddy_SetAlphabeticOrdering() Biddy_Managed_SetAlphabeticOrdering(NULL)
724 
725 /* 67 */
727 #define Biddy_SwapWithHigher(v) Biddy_Managed_SwapWithHigher(NULL,v)
729 
730 /* 68 */
732 #define Biddy_SwapWithLower(v) Biddy_Managed_SwapWithLower(NULL,v)
734 
735 /* 69 */
737 #define Biddy_Sifting(f,c) Biddy_Managed_Sifting(NULL,f,c)
739 
740 /* 70 */
742 #define Biddy_MinimizeBDD(f) Biddy_Managed_MinimizeBDD(NULL,f)
744 
745 /* 71 */
747 #define Biddy_MaximizeBDD(f) Biddy_Managed_MaximizeBDD(NULL,f)
749 
750 /* 72 */
752 #define Biddy_Copy(MNG2,f) Biddy_Managed_Copy(NULL,MNG2,f)
753 #define Biddy_CopyFrom(MNG1,f) Biddy_Managed_Copy(MNG1,NULL,f)
755 
756 /* 73 */
759 #define Biddy_CopyFormulaTo(MNG2,x) Biddy_Managed_CopyFormula(NULL,MNG2,x)
760 #define Biddy_CopyFormulaFrom(MNG1,x) Biddy_Managed_CopyFormula(MNG1,NULL,x)
762 
763 /* 74 */
765 #define Biddy_ConstructBDD(numV,varlist,numN,nodelist) Biddy_Managed_ConstructBDD(NULL,numV,varlist,numV,nodelist)
766 EXTERN Biddy_Edge Biddy_Managed_ConstructBDD(Biddy_Manager MNG, int numV, Biddy_String varlist, int numN, Biddy_String nodelist);
767 
768 #ifdef __cplusplus
769 }
770 #endif
771 
772 /*----------------------------------------------------------------------------*/
773 /* Prototypes for functions exported from biddyOp.c */
774 /*----------------------------------------------------------------------------*/
775 
776 #ifdef __cplusplus
777 extern "C" {
778 #endif
779 
780 /* 75 */
783 #define Biddy_Not(f) Biddy_Managed_Not(NULL,f)
785 
786 /* 76 */
788 #define Biddy_ITE(f,g,h) Biddy_Managed_ITE(NULL,f,g,h)
790 
791 /* 77 */
794 #define Biddy_And(f,g) Biddy_Managed_And(NULL,f,g)
796 #define Biddy_Managed_Intersect(MNG,f,g) Biddy_Managed_And(MNG,f,g)
797 #define Biddy_Intersect(f,g) Biddy_Managed_And(NULL,f,g)
798 
799 /* 78 */
802 #define Biddy_Or(f,g) Biddy_Managed_Or(NULL,f,g)
804 #define Biddy_Managed_Union(MNG,f,g) Biddy_Managed_Or(MNG,f,g)
805 #define Biddy_Union(f,g) Biddy_Managed_Or(NULL,f,g)
806 
807 /* 79 */
809 #define Biddy_Nand(f,g) Biddy_Managed_Nand(NULL,f,g)
811 
812 /* 80 */
814 #define Biddy_Nor(f,g) Biddy_Managed_Nor(NULL,f,g)
816 
817 /* 81 */
819 #define Biddy_Xor(f,g) Biddy_Managed_Xor(NULL,f,g)
821 
822 /* 82 */
824 #define Biddy_Xnor(f,g) Biddy_Managed_Xnor(NULL,f,g)
826 
827 /* 83 */
829 #define Biddy_Leq(f,g) Biddy_Managed_Leq(NULL,f,g)
831 
832 /* 84 */
834 #define Biddy_Gt(f,g) Biddy_Managed_Gt(NULL,f,g)
836 #define Biddy_Managed_Diff(MNG,f,g) Biddy_Managed_Gt(MNG,f,g)
837 #define Biddy_Diff(f,g) Biddy_Managed_Gt(NULL,f,g)
838 
839 /* 85 */
841 #define Biddy_IsLeq(f,g) Biddy_Managed_IsLeq(NULL,f,g)
843 
844 /* 86 */
845 /* This is used to calculate cofactors f|{v=0} and f|{v=1}. */
847 #define Biddy_Restrict(f,v,value) Biddy_Managed_Restrict(NULL,f,v,value)
849 
850 /* 87 */
852 #define Biddy_Compose(f,g,v) Biddy_Managed_Compose(NULL,f,g,v)
854 
855 /* 88 */
857 #define Biddy_E(f,v) Biddy_Managed_E(NULL,f,v)
859 
860 /* 89 */
862 #define Biddy_A(f,v) Biddy_Managed_A(NULL,f,v)
864 
865 /* 90 */
867 #define Biddy_IsVariableDependent(f,v) Biddy_Managed_IsVariableDependent(NULL,f,v)
869 
870 /* 91 */
872 #define Biddy_ExistAbstract(f,cube) Biddy_Managed_ExistAbstract(NULL,f,cube)
874 
875 /* 92 */
877 #define Biddy_UnivAbstract(f,cube) Biddy_Managed_UnivAbstract(NULL,f,cube)
879 
880 /* 93 */
882 #define Biddy_AndAbstract(f,g,cube) Biddy_Managed_AndAbstract(NULL,f,g,cube)
884 
885 /* 94 */
887 #define Biddy_Constrain(f,c) Biddy_Managed_Constrain(NULL,f,c)
889 
890 /* 95 */
891 /* This is Coudert and Madre's restrict function */
893 #define Biddy_Simplify(f,c) Biddy_Managed_Simplify(NULL,f,c)
895 
896 /* 96 */
898 #define Biddy_Support(f) Biddy_Managed_Support(NULL,f)
900 
901 /* 97 */
905 #define Biddy_ReplaceByKeyword(f,keyword) Biddy_Managed_ReplaceByKeyword(NULL,f,keyword)
907 #define Biddy_Managed_Replace(MNG,f) Biddy_Managed_ReplaceByKeyword(MNG,f,NULL)
908 #define Biddy_Replace(f) Biddy_Managed_ReplaceByKeyword(NULL,f,NULL)
909 
910 /* 98 */
912 #define Biddy_Change(f,v) Biddy_Managed_Change(NULL,f,v)
914 
915 /* 99 */
916 /* This is used to calculate f*v and f*(-v) */
917 /* Using the provided macros, Biddy_Managed_Quotient and Biddy_Quotient are not implemented optimally */
919 #define Biddy_VarSubset(f,v,value) Biddy_Managed_VarSubset(NULL,f,v,value)
921 #define Biddy_Managed_Subset0(MNG,f,v) Biddy_Managed_VarSubset(MNG,f,v,FALSE)
922 #define Biddy_Subset0(f,v) Biddy_Managed_VarSubset(NULL,f,v,FALSE)
923 #define Biddy_Managed_Subset1(MNG,f,v) Biddy_Managed_VarSubset(MNG,f,v,TRUE)
924 #define Biddy_Subset1(f,v) Biddy_Managed_VarSubset(NULL,f,v,TRUE)
925 #define Biddy_Managed_Quotient(MNG,f,v) Biddy_Managed_Change(MNG,Biddy_Managed_VarSubset(MNG,f,v,TRUE),v)
926 #define Biddy_Quotient(f,v) Biddy_Change(Biddy_VarSubset(f,v,TRUE),v)
927 #define Biddy_Managed_Remainder(MNG,f,v) Biddy_Managed_VarSubset(MNG,f,v,FALSE)
928 #define Biddy_Remainder(f,v) Biddy_Managed_VarSubset(NULL,f,v,FALSE)
929 
930 /* 100 */
932 #define Biddy_ElementAbstract(f,v) Biddy_Managed_ElementAbstract(NULL,f,v)
934 
935 /* 101 */
937 #define Biddy_Product(f,g) Biddy_Managed_Product(NULL,f,g)
939 
940 /* 102 */
942 #define Biddy_SelectiveProduct(f,g,pncube) Biddy_Managed_SelectiveProduct(NULL,f,g,pncube)
944 
945 /* 103 */
946 /* This is restriction operation for combination sets. */
948 #define Biddy_Supset(f,g) Biddy_Managed_Supset(NULL,f,g)
950 
951 /* 104 */
952 /* This is permission operation for combination sets. */
954 #define Biddy_Subset(f,g) Biddy_Managed_Subset(NULL,f,g)
956 
957 /* 105 */
959 #define Biddy_Permitsym(f,n) Biddy_Managed_Permitsym(NULL,f,n)
960 EXTERN Biddy_Edge Biddy_Managed_Permitsym(Biddy_Manager MNG, Biddy_Edge f, unsigned int n);
961 
962 /* 106 */
964 #define Biddy_Stretch(f) Biddy_Managed_Stretch(NULL,f)
966 
967 /* 107 */
969 #define Biddy_CreateMinterm(support,x) Biddy_Managed_CreateMinterm(NULL,support,x)
970 EXTERN Biddy_Edge Biddy_Managed_CreateMinterm(Biddy_Manager MNG, Biddy_Edge support, long long unsigned int x);
971 
972 /* 108 */
974 #define Biddy_CreateFunction(support,x) Biddy_Managed_CreateFunction(NULL,support,x)
975 EXTERN Biddy_Edge Biddy_Managed_CreateFunction(Biddy_Manager MNG, Biddy_Edge support, long long unsigned int x);
976 
977 /* 109 */
979 #define Biddy_RandomFunction(support,ratio) Biddy_Managed_RandomFunction(NULL,support,ratio)
980 EXTERN Biddy_Edge Biddy_Managed_RandomFunction(Biddy_Manager MNG, Biddy_Edge support, double ratio);
981 
982 /* 110 */
984 #define Biddy_RandomSet(unit,ratio) Biddy_Managed_RandomSet(NULL,unit,ratio)
985 EXTERN Biddy_Edge Biddy_Managed_RandomSet(Biddy_Manager MNG, Biddy_Edge unit, double ratio);
986 
987 /* 111 */
989 #define Biddy_ExtractMinterm(f) Biddy_Managed_ExtractMinterm(NULL,f)
991 
992 #ifdef __cplusplus
993 }
994 #endif
995 
996 /* TO DO: unique */
997 /* Unique quantification of variables. */
998 /* Similar to existential quantification but uses XOR instead of OR. */
999 
1000 /*----------------------------------------------------------------------------*/
1001 /* Prototypes for functions exported from biddyStat.c */
1002 /*----------------------------------------------------------------------------*/
1003 
1004 #ifdef __cplusplus
1005 extern "C" {
1006 #endif
1007 
1008 /* 112 */
1010 #define Biddy_CountNodes(f) Biddy_Managed_CountNodes(NULL,f)
1011 EXTERN unsigned int Biddy_Managed_CountNodes(Biddy_Manager MNG, Biddy_Edge f);
1012 
1013 /* 113 */
1015 #define Biddy_Managed_MaxLevel(MNG,f) Biddy_MaxLevel(f)
1016 EXTERN unsigned int Biddy_MaxLevel(Biddy_Edge f);
1017 
1018 /* 114 */
1020 #define Biddy_Managed_AvgLevel(MNG,f) Biddy_AvgLevel(f)
1021 EXTERN float Biddy_AvgLevel(Biddy_Edge f);
1022 
1023 /* 115 */
1025 #define Biddy_SystemStat(stat) Biddy_Managed_SystemStat(NULL,stat)
1026 EXTERN unsigned int Biddy_Managed_SystemStat(Biddy_Manager MNG, unsigned int stat);
1027 #define Biddy_Managed_VariableTableNum(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATVARIABLETABLENUM)
1028 #define Biddy_Managed_FormulaTableNum(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATFORMULATABLENUM)
1029 #define Biddy_Managed_NodeTableSize(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLESIZE)
1030 #define Biddy_Managed_NodeTableBlockNumber(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLEBLOCKNUMBER)
1031 #define Biddy_Managed_NodeTableGenerated(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLEGENERATED)
1032 #define Biddy_Managed_NodeTableMax(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLEMAX)
1033 #define Biddy_Managed_NodeTableNum(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLENUM)
1034 #define Biddy_Managed_NodeTableResizeNumber(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLERESIZENUMBER)
1035 #define Biddy_Managed_NodeTableGCNumber(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLEGCNUMBER)
1036 #define Biddy_Managed_NodeTableGCTime(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLEGCTIME)
1037 #define Biddy_Managed_NodeTableSwapNumber(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLESWAPNUMBER)
1038 #define Biddy_Managed_NodeTableSiftingNumber(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLESIFTINGNUMBER)
1039 #define Biddy_Managed_NodeTableDRTime(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLEDRTIME)
1040 #define Biddy_Managed_NodeTableITENumber(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLEITENUMBER)
1041 #define Biddy_Managed_NodeTableANDORNumber(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLEANDORNUMBER)
1042 #define Biddy_Managed_NodeTableXORNumber(MNG) Biddy_Managed_SystemStat(MNG,BIDDYSTATNODETABLEXORNUMBER)
1043 #define Biddy_VariableTableNum() Biddy_Managed_SystemStat(NULL,BIDDYSTATVARIABLETABLENUM)
1044 #define Biddy_FormulaTableNum() Biddy_Managed_SystemStat(NULL,BIDDYSTATFORMULATABLENUM)
1045 #define Biddy_NodeTableSize() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLESIZE)
1046 #define Biddy_NodeTableBlockNumber() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLEBLOCKNUMBER)
1047 #define Biddy_NodeTableGenerated() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLEGENERATED)
1048 #define Biddy_NodeTableMax() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLEMAX)
1049 #define Biddy_NodeTableNum() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLENUM)
1050 #define Biddy_NodeTableResizeNumber() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLERESIZENUMBER)
1051 #define Biddy_NodeTableGCNumber() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLEGCNUMBER)
1052 #define Biddy_NodeTableGCTime() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLEGCTIME)
1053 #define Biddy_NodeTableSwapNumber() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLESWAPNUMBER)
1054 #define Biddy_NodeTableSiftingNumber() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLESIFTINGNUMBER)
1055 #define Biddy_NodeTableDRTime() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLEDRTIME)
1056 #define Biddy_NodeTableITENumber() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLEITENUMBER)
1057 #define Biddy_NodeTableANDORNumber() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLEANDORNUMBER)
1058 #define Biddy_NodeTableXORNumber() Biddy_Managed_SystemStat(NULL,BIDDYSTATNODETABLEXORNUMBER)
1059 
1060 /* 116 */
1062 #define Biddy_SystemLongStat(longstat) Biddy_Managed_SystemLongStat(NULL,longstat)
1063 EXTERN unsigned long long int Biddy_Managed_SystemLongStat(Biddy_Manager MNG, unsigned int longstat);
1064 #define Biddy_Managed_NodeTableFoaNumber(MNG) Biddy_Managed_SystemLongStat(MNG,BIDDYLONGSTATNODETABLEFOANUMBER)
1065 #define Biddy_Managed_NodeTableFindNumber(MNG) Biddy_Managed_SystemLongStat(MNG,BIDDYLONGSTATNODETABLEFINDNUMBER)
1066 #define Biddy_Managed_NodeTableCompareNumber(MNG) Biddy_Managed_SystemLongStat(MNG,BIDDYLONGSTATNODETABLECOMPARENUMBER)
1067 #define Biddy_Managed_NodeTableAddNumber(MNG) Biddy_Managed_SystemLongStat(MNG,BIDDYLONGSTATNODETABLEADDNUMBER)
1068 #define Biddy_Managed_NodeTableITERecursiveNumber(MNG) Biddy_Managed_SystemLongStat(MNG,BIDDYLONGSTATNODETABLEITERECURSIVENUMBER)
1069 #define Biddy_Managed_NodeTableANDORRecursiveNumber(MNG) Biddy_Managed_SystemLongStat(MNG,BIDDYLONGSTATNODETABLEANDORRECURSIVENUMBER)
1070 #define Biddy_Managed_NodeTableXORRecursiveNumber(MNG) Biddy_Managed_SystemLongStat(MNG,BIDDYLONGSTATNODETABLEXORRECURSIVENUMBER)
1071 #define Biddy_Managed_OPCacheSearch(MNG) Biddy_Managed_SystemLongStat(MNG,BIDDYLONGSTATOPCACHESEARCH)
1072 #define Biddy_Managed_OPCacheFind(MNG) Biddy_Managed_SystemLongStat(MNG,BIDDYLONGSTATOPCACHEFIND)
1073 #define Biddy_Managed_OPCacheInsert(MNG) Biddy_Managed_SystemLongStat(MNG,BIDDYLONGSTATOPCACHEINSERT)
1074 #define Biddy_Managed_OPCacheOverwrite(MNG) Biddy_Managed_SystemLongStat(MNG,BIDDYLONGSTATOPCACHEOVERWRITE)
1075 #define Biddy_NodeTableFoaNumber() Biddy_Managed_SystemLongStat(NULL,BIDDYLONGSTATNODETABLEFOANUMBER)
1076 #define Biddy_NodeTableFindNumber() Biddy_Managed_SystemLongStat(NULL,BIDDYLONGSTATNODETABLEFINDNUMBER)
1077 #define Biddy_NodeTableCompareNumber() Biddy_Managed_SystemLongStat(NULL,BIDDYLONGSTATNODETABLECOMPARENUMBER)
1078 #define Biddy_NodeTableAddNumber() Biddy_Managed_SystemLongStat(NULL,BIDDYLONGSTATNODETABLEADDNUMBER)
1079 #define Biddy_NodeTableITERecursiveNumber() Biddy_Managed_SystemLongStat(NULL,BIDDYLONGSTATNODETABLEITERECURSIVENUMBER)
1080 #define Biddy_NodeTableANDORRecursiveNumber() Biddy_Managed_SystemLongStat(NULL,BIDDYLONGSTATNODETABLEANDORRECURSIVENUMBER)
1081 #define Biddy_NodeTableXORRecursiveNumber() Biddy_Managed_SystemLongStat(NULL,BIDDYLONGSTATNODETABLEXORRECURSIVENUMBER)
1082 #define Biddy_OPCacheSearch() Biddy_Managed_SystemLongStat(NULL,BIDDYLONGSTATOPCACHESEARCH)
1083 #define Biddy_OPCacheFind() Biddy_Managed_SystemLongStat(NULL,BIDDYLONGSTATOPCACHEFIND)
1084 #define Biddy_OPCacheInsert() Biddy_Managed_SystemLongStat(NULL,BIDDYLONGSTATOPCACHEINSERT)
1085 #define Biddy_OPCacheOverwrite() Biddy_Managed_SystemLongStat(NULL,BIDDYLONGSTATOPCACHEOVERWRITE)
1086 
1087 /* 117 */
1089 #define Biddy_NodeTableNumVar(v) Biddy_Managed_NodeTableNumVar(NULL,v)
1090 EXTERN unsigned int Biddy_Managed_NodeTableNumVar(Biddy_Manager MNG, Biddy_Variable v);
1091 
1092 /* 118 */
1094 #define Biddy_NodeTableGCObsoleteNumber() Biddy_Managed_NodeTableGCObsoleteNumber(NULL)
1095 EXTERN unsigned long long int Biddy_Managed_NodeTableGCObsoleteNumber(Biddy_Manager MNG);
1096 
1097 /* 119 */
1099 #define Biddy_ListUsed() Biddy_Managed_ListUsed(NULL)
1100 EXTERN unsigned int Biddy_Managed_ListUsed(Biddy_Manager MNG);
1101 
1102 /* 120 */
1104 #define Biddy_ListMaxLength() Biddy_Managed_ListMaxLength(NULL)
1105 EXTERN unsigned int Biddy_Managed_ListMaxLength(Biddy_Manager MNG);
1106 
1107 /* 121 */
1109 #define Biddy_ListAvgLength() Biddy_Managed_ListAvgLength(NULL)
1110 EXTERN float Biddy_Managed_ListAvgLength(Biddy_Manager MNG);
1111 
1112 /* 122 */
1114 #define Biddy_CountNodesPlain(f) Biddy_Managed_CountNodesPlain(NULL,f)
1115 EXTERN unsigned int Biddy_Managed_CountNodesPlain(Biddy_Manager MNG, Biddy_Edge f);
1116 
1117 /* 123 */
1119 #define Biddy_DependentVariableNumber(f,select) Biddy_Managed_DependentVariableNumber(NULL,f,select)
1121 
1122 /* 124 */
1124 #define Biddy_CountComplementedEdges(f) Biddy_Managed_CountComplementedEdges(NULL,f)
1126 
1127 /* 125 */
1129 #define Biddy_CountPaths(f) Biddy_Managed_CountPaths(NULL,f)
1130 EXTERN unsigned long long int Biddy_Managed_CountPaths(Biddy_Manager MNG, Biddy_Edge f);
1131 
1132 /* 126 */
1134 #define Biddy_CountMinterms(f,nvars) Biddy_Managed_CountMinterms(NULL,f,nvars)
1135 EXTERN double Biddy_Managed_CountMinterms(Biddy_Manager MNG, Biddy_Edge f, int nvars);
1136 #define Biddy_Managed_CountCombinations(MNG,f) Biddy_Managed_CountMinterms(MNG,f,-1)
1137 #define Biddy_CountCombinations(f) Biddy_Managed_CountMinterms(NULL,f,-1)
1138 
1139 /* 127 */
1141 #define Biddy_DensityOfFunction(f,nvars) Biddy_Managed_DensityOfFunction(NULL,f,nvars)
1142 EXTERN double Biddy_Managed_DensityOfFunction(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars);
1143 
1144 /* 128 */
1146 #define Biddy_DensityOfBDD(f,nvars) Biddy_Managed_DensityOfBDD(NULL,f,nvars)
1147 EXTERN double Biddy_Managed_DensityOfBDD(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars);
1148 
1149 /* 129 */
1151 #define Biddy_MinNodes(f) Biddy_Managed_MinNodes(NULL,f)
1152 EXTERN unsigned int Biddy_Managed_MinNodes(Biddy_Manager MNG, Biddy_Edge f);
1153 
1154 /* 130 */
1156 #define Biddy_MaxNodes(f) Biddy_Managed_MaxNodes(NULL,f)
1157 EXTERN unsigned int Biddy_Managed_MaxNodes(Biddy_Manager MNG, Biddy_Edge f);
1158 
1159 /* 131 */
1161 #define Biddy_ReadMemoryInUse() Biddy_Managed_ReadMemoryInUse(NULL)
1162 EXTERN unsigned long long int Biddy_Managed_ReadMemoryInUse(Biddy_Manager MNG);
1163 
1164 /* 132 */
1166 #define Biddy_PrintInfo(f) Biddy_Managed_PrintInfo(NULL,f)
1167 EXTERN void Biddy_Managed_PrintInfo(Biddy_Manager MNG, FILE *f);
1168 
1169 #ifdef __cplusplus
1170 }
1171 #endif
1172 
1173 /*----------------------------------------------------------------------------*/
1174 /* Prototypes for functions exported from biddyInOut.c */
1175 /*----------------------------------------------------------------------------*/
1176 
1177 #ifdef __cplusplus
1178 extern "C" {
1179 #endif
1180 
1181 /* 133 */
1183 #define Biddy_Eval0(s) Biddy_Managed_Eval0(NULL,s)
1185 
1186 /* 134 */
1188 #define Biddy_Eval1x(s,lf) Biddy_Managed_Eval1x(NULL,s,lf)
1190 #define Biddy_Managed_Eval1(MNG,s) Biddy_Managed_Eval1x(MNG,s,NULL)
1191 #define Biddy_Eval1(s) Biddy_Managed_Eval1x(NULL,s,NULL)
1192 
1193 /* 135 */
1195 #define Biddy_Eval2(boolFunc) Biddy_Managed_Eval2(NULL,boolFunc)
1197 
1198 /* 136 */
1200 #define Biddy_ReadBddview(filename,name) Biddy_Managed_ReadBddview(NULL,filename,name)
1201 EXTERN Biddy_String Biddy_Managed_ReadBddview(Biddy_Manager MNG, const char filename[], Biddy_String name);
1202 
1203 /* 137 */
1205 #define Biddy_ReadVerilogFile(filename,prefix) Biddy_Managed_ReadVerilogFile(NULL,filename,prefix)
1206 EXTERN void Biddy_Managed_ReadVerilogFile(Biddy_Manager MNG, const char filename[], Biddy_String prefix);
1207 
1208 /* 138 */
1210 #define Biddy_PrintBDD(var,filename,f,label) Biddy_Managed_PrintBDD(NULL,var,filename,f,label)
1211 EXTERN void Biddy_Managed_PrintBDD(Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f, Biddy_String label);
1212 #define Biddy_Managed_PrintfBDD(MNG,f) Biddy_Managed_PrintBDD(MNG,NULL,"stdout",f,NULL)
1213 #define Biddy_Managed_SprintfBDD(MNG,var,f) Biddy_Managed_PrintBDD(MNG,var,"",f,NULL)
1214 #define Biddy_Managed_WriteBDD(MNG,filename,f,label) Biddy_Managed_PrintBDD(MNG,NULL,filename,f,label)
1215 #define Biddy_PrintfBDD(f) Biddy_Managed_PrintBDD(NULL,NULL,"stdout",f,NULL)
1216 #define Biddy_SprintfBDD(var,f) Biddy_Managed_PrintBDD(NULL,var,"",f,NULL)
1217 #define Biddy_WriteBDD(filename,f,label) Biddy_Managed_PrintBDD(NULL,NULL,filename,f,label)
1218 
1219 /* 139 */
1221 #define Biddy_PrintTable(var,filename,f) Biddy_Managed_PrintTable(NULL,var,filename,f)
1222 EXTERN void Biddy_Managed_PrintTable(Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f);
1223 #define Biddy_Managed_PrintfTable(MNG,f) Biddy_Managed_PrintTable(MNG,NULL,"stdout",f)
1224 #define Biddy_Managed_SprintfTable(MNG,var,f) Biddy_Managed_PrintTable(MNG,var,"",f)
1225 #define Biddy_Managed_WriteTable(MNG,filename,f) Biddy_Managed_PrintTable(MNG,NULL,filename,f)
1226 #define Biddy_PrintfTable(f) Biddy_Managed_PrintTable(NULL,NULL,"stdout",f)
1227 #define Biddy_SprintfTable(var,f) Biddy_Managed_PrintTable(NULL,var,"",f)
1228 #define Biddy_WriteTable(filename,f) Biddy_Managed_PrintTable(NULL,NULL,filename,f)
1229 
1230 /* 140 */
1232 #define Biddy_PrintSOP(var,filename,f) Biddy_Managed_PrintSOP(NULL,var,filename,f)
1233 EXTERN void Biddy_Managed_PrintSOP(Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f);
1234 #define Biddy_Managed_PrintfSOP(MNG,f) Biddy_Managed_PrintSOP(MNG,NULL,"stdout",f)
1235 #define Biddy_Managed_SprintfSOP(MNG,var,f) Biddy_Managed_PrintSOP(MNG,var,"",f)
1236 #define Biddy_Managed_WriteSOP(MNG,filename,f) Biddy_Managed_PrintSOP(MNG,NULL,filename,f)
1237 #define Biddy_PrintfSOP(f) Biddy_Managed_PrintSOP(NULL,NULL,"stdout",f)
1238 #define Biddy_SprintfSOP(var,f) Biddy_Managed_PrintSOP(NULL,var,"",f)
1239 #define Biddy_WriteSOP(filename,f) Biddy_Managed_PrintSOP(NULL,NULL,filename,f)
1240 
1241 /* 141 */
1243 #define Biddy_PrintMinterms(var,filename,f,negative) Biddy_Managed_PrintMinterms(NULL,var,filename,f,negative)
1244 EXTERN void Biddy_Managed_PrintMinterms(Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f, Biddy_Boolean negative);
1245 #define Biddy_Managed_PrintfMinterms(MNG,f,negative) Biddy_Managed_PrintMinterms(MNG,NULL,"stdout",f,negative)
1246 #define Biddy_Managed_SprintfMinterms(MNG,var,f,negative) Biddy_Managed_PrintMinterms(MNG,var,"",f,negative)
1247 #define Biddy_Managed_WriteMinterms(MNG,filename,f,negative) Biddy_Managed_PrintMinterms(MNG,NULL,filename,f,negative)
1248 #define Biddy_PrintfMinterms(f,negative) Biddy_Managed_PrintMinterms(NULL,NULL,"stdout",f,negative)
1249 #define Biddy_SprintfMinterms(var,f,negative) Biddy_Managed_PrintMinterms(NULL,var,"",f,negative)
1250 #define Biddy_WriteMinterms(filename,f,negative) Biddy_Managed_PrintMinterms(NULL,NULL,filename,f,negative)
1251 
1252 /* 142 */
1254 #define Biddy_WriteDot(filename,f,label,id,cudd) Biddy_Managed_WriteDot(NULL,filename,f,label,id,cudd)
1255 EXTERN unsigned int Biddy_Managed_WriteDot(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], int id, Biddy_Boolean cudd);
1256 
1257 /* 143 */
1259 #define Biddy_WriteBddview(filename,f,label,table) Biddy_Managed_WriteBddview(NULL,filename,f,label,table)
1260 EXTERN unsigned int Biddy_Managed_WriteBddview(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], void *xytable);
1261 
1262 #ifdef __cplusplus
1263 }
1264 #endif
1265 
1266 /* TO DO: CNF + DIMACS BENCHMARKS */
1267 /* http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html */
1268 /* http://www.dwheeler.com/essays/minisat-user-guide.html */
1269 /* http://www.miroslav-velev.com/sat_benchmarks.html */
1270 /* http://www.satcompetition.org/ */
1271 
1272 #endif /* _BIDDY */
Biddy_Managed_IsLeq
EXTERN 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:948
Biddy_Managed_Nor
EXTERN 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:553
Biddy_Managed_IncTag
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:2639
Biddy_Managed_MaxNodes
EXTERN unsigned int Biddy_Managed_MaxNodes(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_MaxNodes reports number of nodes in the worst ordering.
Definition: biddyStat.c:947
Biddy_Managed_GetVariable
EXTERN Biddy_Variable Biddy_Managed_GetVariable(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_GetVariable returns variable with the given name.
Definition: biddyMain.c:1377
Biddy_Managed_WriteDot
EXTERN unsigned int Biddy_Managed_WriteDot(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], int id, Biddy_Boolean cudd)
Function Biddy_Managed_WriteDot writes dot/graphviz format using fprintf.
Definition: biddyInOut.c:736
Biddy_Cache
Biddy_Cache is used to specify user's cache table.
Biddy_Managed_ListMaxLength
EXTERN unsigned int Biddy_Managed_ListMaxLength(Biddy_Manager MNG)
Function Biddy_Managed_ListMaxLength.
Definition: biddyStat.c:428
Biddy_Managed_Nand
EXTERN 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:474
Biddy_Managed_MaximizeBDD
EXTERN void Biddy_Managed_MaximizeBDD(Biddy_Manager MNG, Biddy_String name)
Function Biddy_Managed_MaximizeBDD reorders variables to maximize the node number of the given functi...
Definition: biddyMain.c:3782
Biddy_Managed_DependentVariableNumber
EXTERN unsigned int Biddy_Managed_DependentVariableNumber(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean select)
Function Biddy_Managed_DependentVariableNumber.
Definition: biddyStat.c:579
Biddy_Managed_GetIthFormulaName
EXTERN Biddy_String Biddy_Managed_GetIthFormulaName(Biddy_Manager MNG, unsigned int i)
Function Biddy_Managed_GetIthFormulaName returns name of the ith formula in a Formula table.
Definition: biddyMain.c:3350
Biddy_Managed_Copy
EXTERN Biddy_Edge Biddy_Managed_Copy(Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_Edge f)
Function Biddy_Managed_Copy copies a graph from one manager to another manager which can use the same...
Definition: biddyMain.c:3844
Biddy_Managed_Leq
EXTERN Biddy_Edge Biddy_Managed_Leq(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Leq calculates Boolean implication.
Definition: biddyOp.c:790
Biddy_Managed_RandomFunction
EXTERN Biddy_Edge Biddy_Managed_RandomFunction(Biddy_Manager MNG, Biddy_Edge support, double ratio)
Function Biddy_Managed_RandomFunction generates a random BDD.
Definition: biddyOp.c:3029
Biddy_Managed_CreateMinterm
EXTERN 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:2871
Biddy_Managed_CountComplementedEdges
EXTERN unsigned int Biddy_Managed_CountComplementedEdges(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountComplementedEdges count the number of complemented edges.
Definition: biddyStat.c:633
Biddy_Managed_Gt
EXTERN 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:871
Biddy_Managed_GetTopVariableChar
EXTERN char Biddy_Managed_GetTopVariableChar(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_GetTopVariableChar returns the first character in the name of top variable.
Definition: biddyMain.c:1862
Biddy_Managed_SwapWithHigher
EXTERN Biddy_Variable Biddy_Managed_SwapWithHigher(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_SwapWithHigher swaps two adjacent variables.
Definition: biddyMain.c:3555
Biddy_Managed_AndAbstract
EXTERN 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:1565
Biddy_Variable
Biddy_Variable is used for indices in variable table.
Biddy_Managed_Supset
EXTERN Biddy_Edge Biddy_Managed_Supset(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Supset calculates Coudert and Madre's operation SupSet.
Definition: biddyOp.c:2509
Biddy_Managed_CountMinterms
EXTERN double Biddy_Managed_CountMinterms(Biddy_Manager MNG, Biddy_Edge f, int nvars)
Function Biddy_Managed_CountMinterms.
Definition: biddyStat.c:745
Biddy_Managed_Purge
EXTERN void Biddy_Managed_Purge(Biddy_Manager MNG)
Function Biddy_Managed_Purge immediately removes all nodes which were not preserved or which are not ...
Definition: biddyMain.c:2915
Biddy_Managed_ReadMemoryInUse
EXTERN unsigned long long int Biddy_Managed_ReadMemoryInUse(Biddy_Manager MNG)
Function Biddy_Managed_ReadMemoryInUse reports memory consumption of main data strucutures in bytes (...
Definition: biddyStat.c:997
Biddy_Managed_GetPrevVariable
EXTERN Biddy_Variable Biddy_Managed_GetPrevVariable(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetPrevVariable returns previous variable in the global ordering (lower,...
Definition: biddyMain.c:1527
Biddy_String
Biddy_String is used for strings.
Biddy_Managed_FindFormula
EXTERN Biddy_Boolean Biddy_Managed_FindFormula(Biddy_Manager MNG, Biddy_String x, unsigned int *idx, Biddy_Edge *f)
Function Biddy_Managed_FindFormula find formula in Formula table.
Definition: biddyMain.c:3144
Biddy_Managed_CopyFormula
EXTERN void Biddy_Managed_CopyFormula(Biddy_Manager MNG1, Biddy_Manager MNG2, Biddy_String x)
Function Biddy_Managed_CopyFormula uses Biddy_Managed_Copy to copy a graph from one manager to anothe...
Definition: biddyMain.c:3921
Biddy_Managed_GetNextVariable
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:1575
Biddy_Managed_A
EXTERN 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:1264
Biddy_Managed_MinNodes
EXTERN unsigned int Biddy_Managed_MinNodes(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_MinNodes reports number of nodes in the optimal ordering.
Definition: biddyStat.c:896
Biddy_Managed_TaggedFoaNode
EXTERN Biddy_Edge Biddy_Managed_TaggedFoaNode(Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge pf, Biddy_Edge pt, Biddy_Variable ptag, Biddy_Boolean garbageAllowed)
Function Biddy_Managed_TaggedFoaNode finds or adds new node with the given variable and successors.
Definition: biddyMain.c:2711
Biddy_Managed_GetLowestVariable
EXTERN Biddy_Variable Biddy_Managed_GetLowestVariable(Biddy_Manager MNG)
Function Biddy_Managed_GetLowestVariable returns the lowest variable in the current ordering.
Definition: biddyMain.c:1426
Biddy_Managed_Refresh
EXTERN void Biddy_Managed_Refresh(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Refresh refreshes top node in a given function.
Definition: biddyMain.c:686
Biddy_Managed_CountNodes
EXTERN unsigned int Biddy_Managed_CountNodes(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountNodes.
Definition: biddyStat.c:90
Biddy_Managed_DeleteIthFormula
EXTERN Biddy_Boolean Biddy_Managed_DeleteIthFormula(Biddy_Manager MNG, unsigned int i)
Function Biddy_Managed_DeleteIthFormula deletes formula from the table.
Definition: biddyMain.c:3250
Biddy_Managed_IsOK
EXTERN Biddy_Boolean Biddy_Managed_IsOK(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_IsOK returns TRUE iff given node is not obsolete.
Definition: biddyMain.c:738
Biddy_InitMNG
EXTERN void Biddy_InitMNG(Biddy_Manager *mng, int bddtype)
Function Biddy_InitMNG initialize a manager.
Definition: biddyMain.c:188
Biddy_Managed_CreateFunction
EXTERN 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:2948
Biddy_LookupFunction
Biddy_LookupFunction is used in Biddy_Eval1x to specify user's function which will lookups in a user'...
Biddy_Managed_IsEqv
EXTERN Biddy_Boolean Biddy_Managed_IsEqv(Biddy_Manager MNG1, Biddy_Edge f1, Biddy_Manager MNG2, Biddy_Edge f2)
Function Biddy_Managed_IsEqv returns TRUE iff two BDDs are equal.
Definition: biddyMain.c:1064
Biddy_Managed_PrintInfo
EXTERN void Biddy_Managed_PrintInfo(Biddy_Manager MNG, FILE *f)
Function Biddy_Managed_PrintInfo prepares a file with stats.
Definition: biddyStat.c:1044
Biddy_Managed_GetVariableData
EXTERN void * Biddy_Managed_GetVariableData(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableData gets variable's data.
Definition: biddyMain.c:2152
Biddy_Edge
Biddy_Edge is a marked edge (i.e. a marked pointer to BiddyNode).
Biddy_Managed_ITE
EXTERN 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:184
Biddy_Managed_GetIthFormula
EXTERN Biddy_Edge Biddy_Managed_GetIthFormula(Biddy_Manager MNG, unsigned int i)
Function Biddy_Managed_GetIthFormula returns ith formula in a Formula table.
Definition: biddyMain.c:3300
Biddy_Managed_SetOrdering
EXTERN void Biddy_Managed_SetOrdering(Biddy_Manager MNG, Biddy_String ordering)
Function Biddy_Managed_SetOrdering use variable swapping to create the ordering given by string.
Definition: biddyMain.c:3451
Biddy_GetTopVariable
EXTERN Biddy_Variable Biddy_GetTopVariable(Biddy_Edge f)
Function Biddy_GetTopVariable returns the top variable.
Definition: biddyMain.c:337
Biddy_Managed_PrintTable
EXTERN void Biddy_Managed_PrintTable(Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f)
Function Biddy_Managed_PrintTable writes truth table.
Definition: biddyInOut.c:570
Biddy_Managed_SetManagerParameters
EXTERN void Biddy_Managed_SetManagerParameters(Biddy_Manager MNG, float gcr, float gcrF, float gcrX, float rr, float rrF, float rrX, float st, float cst)
Function Biddy_Managed_SetManagerParameters set modifiable parameters.
Definition: biddyMain.c:899
Biddy_Managed_MinimizeBDD
EXTERN void Biddy_Managed_MinimizeBDD(Biddy_Manager MNG, Biddy_String name)
Function Biddy_Managed_MinimizeBDD reorders variables to minimize the node number of the given formul...
Definition: biddyMain.c:3723
Biddy_Managed_GetConstantZero
EXTERN Biddy_Edge Biddy_Managed_GetConstantZero(Biddy_Manager MNG)
Function Biddy_Managed_GetConstantZero returns constant 0.
Definition: biddyMain.c:415
Biddy_Managed_AddVariableBelow
EXTERN Biddy_Edge Biddy_Managed_AddVariableBelow(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_AddVariableBelow adds variable.
Definition: biddyMain.c:2538
Biddy_Manager
Biddy_Manager is used to specify manager.
Biddy_Managed_SetVariableData
EXTERN void Biddy_Managed_SetVariableData(Biddy_Manager MNG, Biddy_Variable v, void *x)
Function Biddy_Managed_SetVariableData sets variable's data.
Definition: biddyMain.c:2104
Biddy_Managed_GetManagerName
EXTERN Biddy_String Biddy_Managed_GetManagerName(Biddy_Manager MNG)
Function Biddy_Managed_GetManagerName reports the name of the BDD type used in the manager.
Definition: biddyMain.c:834
Biddy_Managed_GetVariableValue
EXTERN Biddy_Edge Biddy_Managed_GetVariableValue(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableValue gets variable's value.
Definition: biddyMain.c:2007
Biddy_Managed_WriteBddview
EXTERN unsigned int Biddy_Managed_WriteBddview(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], void *xytable)
Function Biddy_Managed_WriteBDDView writes bddview format using fprintf.
Definition: biddyInOut.c:792
Biddy_Managed_Eval
EXTERN Biddy_Boolean Biddy_Managed_Eval(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Eval returns the value of a Boolean function for a given variable assignment.
Definition: biddyMain.c:2203
Biddy_Managed_GetBaseSet
EXTERN Biddy_Edge Biddy_Managed_GetBaseSet(Biddy_Manager MNG)
Function Biddy_Managed_GetBaseSet returns set containing only a null combination, i....
Definition: biddyMain.c:948
Biddy_Managed_PrintMinterms
EXTERN void Biddy_Managed_PrintMinterms(Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f, Biddy_Boolean negative)
Function Biddy_Managed_PrintMinterms writes minterms.
Definition: biddyInOut.c:680
Biddy_Boolean
Biddy_Boolean is used for boolean values.
Biddy_Managed_RandomSet
EXTERN Biddy_Edge Biddy_Managed_RandomSet(Biddy_Manager MNG, Biddy_Edge unit, double ratio)
Function Biddy_Managed_RandomSet generates a random BDD.
Definition: biddyOp.c:3111
Biddy_ExitMNG
EXTERN void Biddy_ExitMNG(Biddy_Manager *mng)
Function Biddy_ExitMNG deletes a manager.
Definition: biddyMain.c:213
Biddy_Managed_Eval1x
EXTERN Biddy_Edge Biddy_Managed_Eval1x(Biddy_Manager MNG, Biddy_String s, Biddy_LookupFunction lf)
Function Biddy_Managed_Eval1x evaluates prefix AND-OR-EXOR-NOT format.
Definition: biddyInOut.c:296
Biddy_Managed_Change
EXTERN 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:2056
Biddy_Managed_SwapWithLower
EXTERN Biddy_Variable Biddy_Managed_SwapWithLower(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_SwapWithLower swaps two adjacent variables.
Definition: biddyMain.c:3607
Biddy_Managed_GetTopVariableEdge
EXTERN Biddy_Edge Biddy_Managed_GetTopVariableEdge(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_GetTopVariableEdge returns variable's edge of top variable.
Definition: biddyMain.c:1766
Biddy_GetElse
EXTERN Biddy_Edge Biddy_GetElse(Biddy_Edge f)
Function Biddy_GetElse returns ELSE successor.
Definition: biddyMain.c:299
Biddy_Managed_NodeTableGCObsoleteNumber
EXTERN unsigned long long int Biddy_Managed_NodeTableGCObsoleteNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableGCObsoleteNumber.
Definition: biddyStat.c:334
Biddy_Managed_AddFormula
EXTERN unsigned int Biddy_Managed_AddFormula(Biddy_Manager MNG, Biddy_String x, Biddy_Edge f, int c)
Function Biddy_Managed_AddFormula adds formula to Formula table.
Definition: biddyMain.c:3093
Biddy_MaxLevel
EXTERN unsigned int Biddy_MaxLevel(Biddy_Edge f)
Function Biddy_MaxLevel.
Definition: biddyStat.c:137
Biddy_Managed_SelectFunction
EXTERN void Biddy_Managed_SelectFunction(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_SelectFunction recursively selects all nodes of a given function.
Definition: biddyMain.c:1280
Biddy_Managed_CountNodesPlain
EXTERN unsigned int Biddy_Managed_CountNodesPlain(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountNodesPlain.
Definition: biddyStat.c:524
Biddy_Managed_AddElementByName
EXTERN Biddy_Variable Biddy_Managed_AddElementByName(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_AddElementByName adds element.
Definition: biddyMain.c:2487
Biddy_Managed_ExtractMinterm
EXTERN Biddy_Edge Biddy_Managed_ExtractMinterm(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_ExtractMinterm.
Definition: biddyOp.c:3186
Biddy_Managed_GC
EXTERN void Biddy_Managed_GC(Biddy_Manager MNG, Biddy_Variable targetLT, Biddy_Variable targetGEQ, Biddy_Boolean purge, Biddy_Boolean total)
Function Biddy_Managed_GC performs garbage collection.
Definition: biddyMain.c:2804
Biddy_Managed_PrintSOP
EXTERN void Biddy_Managed_PrintSOP(Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f)
Function Biddy_Managed_PrintSOP writes (non-minimal) SOP.
Definition: biddyInOut.c:623
Biddy_Managed_ConstructBDD
EXTERN Biddy_Edge Biddy_Managed_ConstructBDD(Biddy_Manager MNG, int numV, Biddy_String varlist, int numN, Biddy_String nodelist)
Function Biddy_Managed_ConstructBDD constructs BDD from lists of nodes and edges.
Definition: biddyMain.c:4016
Biddy_Managed_Not
EXTERN Biddy_Edge Biddy_Managed_Not(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Not calculates Boolean function NOT.
Definition: biddyOp.c:103
Biddy_Managed_AddCache
EXTERN void Biddy_Managed_AddCache(Biddy_Manager MNG, Biddy_GCFunction gc)
Function Biddy_Managed_AddCache adds cache to the end of Cache list.
Definition: biddyMain.c:3020
Biddy_Managed_DeselectAll
EXTERN void Biddy_Managed_DeselectAll(Biddy_Manager MNG)
Function Biddy_Managed_DeselectAll deselects all nodes.
Definition: biddyMain.c:1328
Biddy_Managed_Sifting
EXTERN Biddy_Boolean Biddy_Managed_Sifting(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean converge)
Function Biddy_Managed_Sifting reorders variables to minimize node number using Rudell's sifting algo...
Definition: biddyMain.c:3663
Biddy_Managed_Support
EXTERN 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:1829
Biddy_Managed_Restrict
EXTERN 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:1023
Biddy_Managed_Clean
EXTERN void Biddy_Managed_Clean(Biddy_Manager MNG)
Function Biddy_Managed_Clean performs cleaning.
Definition: biddyMain.c:2859
Biddy_Managed_IsVariableDependent
EXTERN 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:1344
Biddy_Managed_ResetVariablesValue
EXTERN void Biddy_Managed_ResetVariablesValue(Biddy_Manager MNG)
Function Biddy_Managed_ResetVariablesValue sets all variable's value to biddyZero.
Definition: biddyMain.c:1911
Biddy_Managed_TransferMark
EXTERN Biddy_Edge Biddy_Managed_TransferMark(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean mark, Biddy_Boolean leftright)
Function Biddy_Managed_TransferMark returns edge with inverted complement bit iff the second paramete...
Definition: biddyMain.c:1015
Biddy_Managed_ElementAbstract
EXTERN Biddy_Edge Biddy_Managed_ElementAbstract(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v)
Function Biddy_Managed_ElementAbstract remove element from all combinations in the set.
Definition: biddyOp.c:2229
Biddy_Managed_SelectNode
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:1135
Biddy_Managed_DeleteFormula
EXTERN Biddy_Boolean Biddy_Managed_DeleteFormula(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_DeleteFormula delete formula from Formula table.
Definition: biddyMain.c:3197
Biddy_Managed_ListAvgLength
EXTERN float Biddy_Managed_ListAvgLength(Biddy_Manager MNG)
Function Biddy_Managed_ListAvgLength.
Definition: biddyStat.c:475
Biddy_Managed_AddVariableByName
EXTERN Biddy_Variable Biddy_Managed_AddVariableByName(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_AddVariableByName adds variable.
Definition: biddyMain.c:2434
Biddy_Managed_IsSmaller
EXTERN Biddy_Boolean Biddy_Managed_IsSmaller(Biddy_Manager MNG, Biddy_Variable fv, Biddy_Variable gv)
Function Biddy_Managed_IsSmaller returns TRUE if the first variable is smaller (= lower = previous = ...
Definition: biddyMain.c:518
Biddy_Managed_Constrain
EXTERN Biddy_Edge Biddy_Managed_Constrain(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge c)
Function Biddy_Managed_Constrain calculates Coudert and Madre's constrain function.
Definition: biddyOp.c:1662
Biddy_Managed_Compose
EXTERN 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:1102
Biddy_Managed_GetManagerType
EXTERN int Biddy_Managed_GetManagerType(Biddy_Manager MNG)
Function Biddy_Managed_GetManagerType reports BDD type used in the manager.
Definition: biddyMain.c:786
Biddy_Managed_GetIthVariable
EXTERN Biddy_Variable Biddy_Managed_GetIthVariable(Biddy_Manager MNG, Biddy_Variable i)
Function Biddy_Managed_GetIthVariable returns ith variable in the current global ordering.
Definition: biddyMain.c:1479
Biddy_Managed_ReplaceByKeyword
EXTERN 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:1944
Biddy_Managed_ClearVariablesData
EXTERN void Biddy_Managed_ClearVariablesData(Biddy_Manager MNG)
Function Biddy_Managed_ClearVariablesData free memory used for all variable's data.
Definition: biddyMain.c:2056
Biddy_Managed_FoaVariable
EXTERN Biddy_Variable Biddy_Managed_FoaVariable(Biddy_Manager MNG, Biddy_String x, Biddy_Boolean varelem)
Function Biddy_Managed_FoaVariable finds variable/element or adds new variable (i....
Definition: biddyMain.c:2329
Biddy_GetThen
EXTERN Biddy_Edge Biddy_GetThen(Biddy_Edge f)
Function Biddy_GetThen returns THEN successor.
Definition: biddyMain.c:260
Biddy_Managed_Product
EXTERN Biddy_Edge Biddy_Managed_Product(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Product calculates operation product defined over combination sets.
Definition: biddyOp.c:2308
Biddy_Managed_IsSelected
EXTERN Biddy_Boolean Biddy_Managed_IsSelected(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_IsSelected returns TRUE iff the top node of the given function is selected.
Definition: biddyMain.c:1231
Biddy_Managed_CountPaths
EXTERN unsigned long long int Biddy_Managed_CountPaths(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountPaths count the number of 1-paths.
Definition: biddyStat.c:681
Biddy_About
EXTERN Biddy_String Biddy_About()
Function Biddy_About reports version of Biddy package.
Definition: biddyMain.c:235
Biddy_Managed_Or
EXTERN 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:353
Biddy_Managed_Stretch
EXTERN Biddy_Edge Biddy_Managed_Stretch(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Stretch calculates minimal subset of the given set such that all elements in t...
Definition: biddyOp.c:2777
Biddy_Managed_VarSubset
EXTERN Biddy_Edge Biddy_Managed_VarSubset(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v, Biddy_Boolean value)
Function Biddy_Managed_VarSubset calculates a division of Boolean function with a literal.
Definition: biddyOp.c:2149
Biddy_Managed_ListUsed
EXTERN unsigned int Biddy_Managed_ListUsed(Biddy_Manager MNG)
Function Biddy_Managed_ListUsed.
Definition: biddyStat.c:381
Biddy_Managed_GetVariableEdge
EXTERN Biddy_Edge Biddy_Managed_GetVariableEdge(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableEdge returns variable's edge.
Definition: biddyMain.c:1622
Biddy_Managed_Xor
EXTERN 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:631
Biddy_Managed_Xnor
EXTERN 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:711
Biddy_GCFunction
Biddy_GCFunction is used in Biddy_AddCache to specify user's function which will performs garbage col...
Biddy_Managed_ReadVerilogFile
EXTERN void Biddy_Managed_ReadVerilogFile(Biddy_Manager MNG, const char filename[], Biddy_String prefix)
Function Biddy_Managed_ReadVerilogFile reads Verilog file and creates variables for all primary input...
Definition: biddyInOut.c:463
Biddy_Managed_ChangeVariableName
EXTERN void Biddy_Managed_ChangeVariableName(Biddy_Manager MNG, Biddy_Variable v, Biddy_String x)
Function Biddy_Managed_ChangeVariableName set new name to the given variable/element.
Definition: biddyMain.c:2381
Biddy_Managed_SystemStat
EXTERN unsigned int Biddy_Managed_SystemStat(Biddy_Manager MNG, unsigned int stat)
Function Biddy_Managed_SystemStat.
Definition: biddyStat.c:186
Biddy_Managed_PurgeAndReorder
EXTERN void Biddy_Managed_PurgeAndReorder(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean converge)
Function Biddy_Managed_PurgeAndReorder immediately removes non-preserved nodes and triggers reorderin...
Definition: biddyMain.c:2971
Biddy_Managed_IsLowest
EXTERN Biddy_Boolean Biddy_Managed_IsLowest(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_IsLowest returns TRUE if the variable is the lowest one (lowest == topmost).
Definition: biddyMain.c:567
Biddy_Managed_NodeTableNumVar
EXTERN unsigned int Biddy_Managed_NodeTableNumVar(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_NodeTableNumVar returns number of nodes with a given variable currently in nod...
Definition: biddyStat.c:283
Biddy_Managed_GetConstantOne
EXTERN Biddy_Edge Biddy_Managed_GetConstantOne(Biddy_Manager MNG)
Function Biddy_Managed_GetConstantOne returns constant 1.
Definition: biddyMain.c:469
Biddy_Managed_GetElementEdge
EXTERN Biddy_Edge Biddy_Managed_GetElementEdge(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetElementEdge returns element's edge.
Definition: biddyMain.c:1669
Biddy_Managed_IsHighest
EXTERN Biddy_Boolean Biddy_Managed_IsHighest(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_IsHighest returns TRUE if the variable is the highest one if terminal node is ...
Definition: biddyMain.c:626
Biddy_Managed_PrintBDD
EXTERN void Biddy_Managed_PrintBDD(Biddy_Manager MNG, Biddy_String *var, const char filename[], Biddy_Edge f, Biddy_String label)
Function Biddy_Managed_PrintBDD writes raw format.
Definition: biddyInOut.c:516
Biddy_Managed_And
EXTERN 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:270
Biddy_Managed_Simplify
EXTERN Biddy_Edge Biddy_Managed_Simplify(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge c)
Function Biddy_Managed_Simplify calculates (a slightly) modified Coudert and Madre's restrict functio...
Definition: biddyOp.c:1754
Biddy_Managed_E
EXTERN 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:1184
Biddy_Managed_Permitsym
EXTERN Biddy_Edge Biddy_Managed_Permitsym(Biddy_Manager MNG, Biddy_Edge f, unsigned int n)
Function Biddy_Managed_Permitsym return a subset of f where only combinations with up to n elements a...
Definition: biddyOp.c:2691
Biddy_Managed_GetTerminal
EXTERN Biddy_Edge Biddy_Managed_GetTerminal(Biddy_Manager MNG)
Function Biddy_Managed_GetTerminal returns unmarked and untagged edge pointing to terminal node 1.
Definition: biddyMain.c:363
Biddy_AvgLevel
EXTERN float Biddy_AvgLevel(Biddy_Edge f)
Function Biddy_AvgLevel.
Definition: biddyStat.c:163
Biddy_Managed_GetTopVariableName
EXTERN Biddy_String Biddy_Managed_GetTopVariableName(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_GetTopVariableName returns the name of top variable.
Definition: biddyMain.c:1814
Biddy_Managed_SetVariableValue
EXTERN void Biddy_Managed_SetVariableValue(Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge f)
Function Biddy_Managed_SetVariableValue sets variable's value.
Definition: biddyMain.c:1959
Biddy_Managed_SetAlphabeticOrdering
EXTERN void Biddy_Managed_SetAlphabeticOrdering(Biddy_Manager MNG)
Function Biddy_Managed_SetAlphabeticOrdering use variable swapping to create the alphabetic ordering.
Definition: biddyMain.c:3503
Biddy_Managed_Eval2
EXTERN Biddy_Edge Biddy_Managed_Eval2(Biddy_Manager MNG, Biddy_String boolFunc)
Function Biddy_Managed_Eval2 evaluates infix format.
Definition: biddyInOut.c:352
Biddy_Managed_SelectiveProduct
EXTERN Biddy_Edge Biddy_Managed_SelectiveProduct(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g, Biddy_Edge pncube)
Function Biddy_Managed_SelectiveProduct calculates operation selective product defined over combinati...
Definition: biddyOp.c:2413
Biddy_Managed_UnivAbstract
EXTERN 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:1488
Biddy_Managed_DeselectNode
EXTERN void Biddy_Managed_DeselectNode(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_DeselectNode deselects the top node of the given function.
Definition: biddyMain.c:1183
Biddy_Managed_ReadBddview
EXTERN Biddy_String Biddy_Managed_ReadBddview(Biddy_Manager MNG, const char filename[], Biddy_String name)
Function Biddy_Managed_ReadBddview reads bddview file and creates all Boolean functions specified by ...
Definition: biddyInOut.c:408
Biddy_Managed_Eval0
EXTERN Biddy_String Biddy_Managed_Eval0(Biddy_Manager MNG, Biddy_String s)
Function Biddy_Managed_Eval0 evaluates raw format.
Definition: biddyInOut.c:240
Biddy_Managed_GetVariableName
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:1716
Biddy_Managed_DensityOfBDD
EXTERN double Biddy_Managed_DensityOfBDD(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
Function Biddy_Managed_DensityOfBDD calculates the ratio of the number of on-set minterms to the numb...
Definition: biddyStat.c:845
Biddy_Managed_DensityOfFunction
EXTERN double Biddy_Managed_DensityOfFunction(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
Function Biddy_Managed_DensityOfFunction calculates the ratio of the number of on-set minterms to the...
Definition: biddyStat.c:795
Biddy_Managed_AddVariableAbove
EXTERN Biddy_Edge Biddy_Managed_AddVariableAbove(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_AddVariableAbove adds variable.
Definition: biddyMain.c:2589
Biddy_Managed_EvalProbability
EXTERN double Biddy_Managed_EvalProbability(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_EvalProbability evaluates BDD.
Definition: biddyMain.c:2254
Biddy_Managed_SystemLongStat
EXTERN unsigned long long int Biddy_Managed_SystemLongStat(Biddy_Manager MNG, unsigned int longstat)
Function Biddy_Managed_SystemLongStat.
Definition: biddyStat.c:235
Biddy_Managed_ExistAbstract
EXTERN 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:1410
Biddy_Managed_Subset
EXTERN Biddy_Edge Biddy_Managed_Subset(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Subset calculates Coudert and Madre's operation SubSet.
Definition: biddyOp.c:2603