Biddy  1.7.4
An academic Binary Decision Diagrams package
biddy.h
Go to the documentation of this file.
1 /***************************************************************************//*!
2 \file biddy.h
3 \brief File biddy.h contains declaration of all external data structures.
4 
5 ### Description
6 
7  PackageName [Biddy]
8  Synopsis [Biddy provides data structures and algorithms for the
9  representation and manipulation of Boolean functions with
10  ROBDDs, 0-sup-BDDs, and TZBDDs. A hash table is used for quick
11  search of nodes. Complement edges decreases the number of
12  nodes. An automatic garbage collection with a system age is
13  implemented. Variable swapping and sifting are implemented.]
14 
15  FileName [biddy.h]
16  Revision [$Revision: 365 $]
17  Date [$Date: 2017-12-18 13:01:40 +0100 (pon, 18 dec 2017) $]
18  Authors [Robert Meolic (robert.meolic@um.si),
19  Ales Casar (ales@homemade.net)]
20 
21 ### Copyright
22 
23 Copyright (C) 2006, 2017 UM FERI, Koroska cesta 46, SI-2000 Maribor, Slovenia
24 
25 Biddy is free software; you can redistribute it and/or modify it under the terms
26 of the GNU General Public License as published by the Free Software Foundation;
27 either version 2 of the License, or (at your option) any later version.
28 
29 Biddy is distributed in the hope that it will be useful, but WITHOUT ANY
30 WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A
31 PARTICULAR PURPOSE. See the GNU General Public License for more details.
32 
33 You should have received a copy of the GNU General Public License along with
34 this program; if not, write to the Free Software Foundation, Inc., 51 Franklin
35 Street, Fifth Floor, Boston, MA 02110-1301 USA.
36 
37 ### More info
38 
39 See also: biddyInt.h
40 
41 *******************************************************************************/
42 
43 #ifndef _BIDDY
44 #define _BIDDY
45 
46 #include <stdio.h>
47 #include <stdlib.h>
48 #include <stdint.h>
49 #include <stdarg.h>
50 #include <time.h>
51 
52 /* ON MS WINDOWS + MINGW THERE HAS TO BE DEFINED MINGW */
53 /* ON GNU/LINUX THERE HAS TO BE DEFINED UNIX */
54 /* ON MACOSX THERE HAS TO BE DEFINED MACOSX */
55 
56 #ifdef UNIX
57 # ifndef EXTERN
58 # define EXTERN extern
59 # endif
60 # ifndef DATAEXTERN
61 # define DATAEXTERN extern
62 # endif
63 #endif
64 
65 #ifdef MACOSX
66 # ifndef EXTERN
67 # define EXTERN extern
68 # endif
69 # ifndef DATAEXTERN
70 # define DATAEXTERN extern
71 # endif
72 #endif
73 
74 #if defined(MINGW) || defined(_MSC_VER)
75 # ifdef BUILD_BIDDY
76 # undef EXTERN
77 # define EXTERN __declspec (dllexport)
78 # undef DATAEXTERN
79 # define DATAEXTERN extern __declspec (dllexport)
80 # else
81 # ifdef USE_BIDDY
82 # undef EXTERN
83 # define EXTERN __declspec (dllimport)
84 # undef DATAEXTERN
85 # define DATAEXTERN __declspec (dllimport)
86 # else
87 # undef EXTERN
88 # define EXTERN extern
89 # undef DATAEXTERN
90 # define DATAEXTERN extern
91 # endif
92 # endif
93 #endif
94 
95 /*----------------------------------------------------------------------------*/
96 /* Constant definitions */
97 /*----------------------------------------------------------------------------*/
98 
99 #ifndef TRUE
100 # define TRUE (0 == 0)
101 #endif
102 #ifndef FALSE
103 # define FALSE !TRUE
104 #endif
105 
106 /* Supported BDD types */
107 
108 #define BIDDYTYPEOBDD 1
109 #define BIDDYTYPENAMEOBDD "ROBDD"
110 
111 #define BIDDYTYPEOBDDC 2
112 #define BIDDYTYPENAMEOBDDC "ROBDD WITH COMPLEMENTED EDGES"
113 
114 #define BIDDYTYPEZBDD 3
115 #define BIDDYTYPENAMEZBDD "ZBDD"
116 
117 #define BIDDYTYPEZBDDC 4
118 #define BIDDYTYPENAMEZBDDC "ZBDD WITH COMPLEMENTED EDGES"
119 
120 #define BIDDYTYPETZBDD 5
121 #define BIDDYTYPENAMETZBDD "TAGGED ZBDD"
122 
123 #define BIDDYTYPETZBDDC 6
124 #define BIDDYTYPENAMETZBDDC "TAGGED ZBDD WITH COMPLEMENTED EDGES"
125 
126 #define BIDDYTYPEOFDD 7
127 #define BIDDYTYPENAMEOFDD "ROFDD"
128 
129 #define BIDDYTYPEOFDDC 8
130 #define BIDDYTYPENAMEOFDDC "ROFDD WITH COMPLEMENTED EDGES"
131 
132 #define BIDDYTYPEZFDD 9
133 #define BIDDYTYPENAMEZFDD "ZFDD"
134 
135 #define BIDDYTYPEZFDDC 10
136 #define BIDDYTYPENAMEZFDDC "ZFDD WITH COMPLEMENTED EDGES"
137 
138 #define BIDDYTYPETZFDD 11
139 #define BIDDYTYPENAMETZFDD "TZFDD"
140 
141 #define BIDDYTYPETZFDDC 12
142 #define BIDDYTYPENAMETZFDDC "TZFDD WITH COMPLEMENTED EDGES"
143 
144 /*----------------------------------------------------------------------------*/
145 /* Macro definitions */
146 /*----------------------------------------------------------------------------*/
147 
148 /*! Biddy_IsNull returns TRUE iff given BDD is a null edge. */
149 /* null edge is hardcoded since Biddy v1.4 */
150 #define Biddy_IsNull(f) (f == NULL)
151 
152 /*! Biddy_IsTerminal returns TRUE iff given edge points to the terminal node. */
153 /* succesors should be the third and the fourth field in BiddyNode */
154 /* non-terminal nodes should not have null edges as successors */
155 /* for reduced (minimal) OBDD and OFDD this means that the represented function is 0 or 1 */
156 /* for TZBDD, true is returned also for tagged edges to terminal node! */
157 #if UINTPTR_MAX == 0xffffffffffffffff
158 #define Biddy_IsTerminal(f) ((((void**)((uintptr_t) f & 0x0000fffffffffffe))[2] == NULL) && (((void**)((uintptr_t) f & 0x0000fffffffffffe))[3] == NULL))
159 #else
160 #define Biddy_IsTerminal(f) ((((void**)((uintptr_t) f & ~((uintptr_t) 1)))[2] == NULL) && (((void**)((uintptr_t) f & ~((uintptr_t) 1)))[3] == NULL))
161 #endif
162 
163 /*! Biddy_IsEqvPointer returns TRUE iff given edges points to the same node. */
164 /* for OBDDs and OFDDs this means that represented functions are equal or inverted */
165 #define Biddy_IsEqvPointer(f,g) (((uintptr_t) f & ~((uintptr_t) 1)) == ((uintptr_t) g & ~((uintptr_t) 1)))
166 
167 /*! Biddy_GetMark returns TRUE iff given edge is complemented. */
168 #define Biddy_GetMark(f) (((uintptr_t) f & (uintptr_t) 1) != 0)
169 
170 /*! Biddy_SetMark makes given edge complemented. */
171 #define Biddy_SetMark(f) (f = (Biddy_Edge) ((uintptr_t) f | (uintptr_t) 1))
172 
173 /*! Biddy_ClearMark makes given edge not-complemented. */
174 #define Biddy_ClearMark(f) (f = (Biddy_Edge) ((uintptr_t) f & ~((uintptr_t) 1)))
175 
176 /*! Biddy_InvertMark changes complement bit of the given edge. */
177 #define Biddy_InvertMark(f) (f = (Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1))
178 
179 /*! Biddy_Inv returns edge with changed complement bit. */
180 /* for OBDD and OFDD this is the same as Biddy_Not */
181 #define Biddy_Inv(f) ((Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1))
182 
183 /*! Biddy_InvCond returns edge with conditinonaly changed complement bit. */
184 #define Biddy_InvCond(f,c) (c ? ((Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1)) : f)
185 
186 /*! Biddy_Regular returns not-complemented version of edge, since Biddy v1.4. */
187 #define Biddy_Regular(f) ((Biddy_Edge) ((uintptr_t) f & ~((uintptr_t) 1)))
188 
189 /*! Biddy_Complement returns complemented version of edge, since Biddy v1.4. */
190 #define Biddy_Complement(f) ((Biddy_Edge) ((uintptr_t) f | (uintptr_t) 1))
191 
192 /*! Biddy_GetTag returns tag used for the given edge, since Biddy v1.7. */
193 /* use the extended version if there are more than 32768 variables */
194 /* this macro assumes 64-bit architecture */
195 #if UINTPTR_MAX == 0xffffffffffffffff
196 #define Biddy_GetTag(f) ((Biddy_Variable) ((uintptr_t) f >> 48))
197 /* #define Biddy_GetTag(f) ((Biddy_Variable) (((uintptr_t) f >> 48) & 0x000000000000ffff)) */
198 #else
199 #define Biddy_GetTag(f) 0
200 #endif
201 
202 /*! Biddy_SetTag adds tag to the given edge, since Biddy v1.7. */
203 /* CAREFULLY: you can create an invalid node! */
204 /* this macro assumes 64-bit architecture */
205 #if UINTPTR_MAX == 0xffffffffffffffff
206 #define Biddy_SetTag(f,t) (f = (Biddy_Edge) (((uintptr_t) f & 0x0000ffffffffffff) | ((uintptr_t) t << 48)))
207 #else
208 #define Biddy_SetTag(f,t) 0
209 #endif
210 
211 /*! Biddy_ClearTag removes tag from the given edge, since Biddy v1.7. */
212 /* this macro assumes 64-bit architecture */
213 #if UINTPTR_MAX == 0xffffffffffffffff
214 #define Biddy_ClearTag(f) (f = (Biddy_Edge) ((uintptr_t) f & 0x0000ffffffffffff))
215 #else
216 #define Biddy_ClearTag(f) 0
217 #endif
218 
219 /*! Biddy_Untagged returns untagged version of edge, since Biddy v1.7. */
220 /* this macro assumes 64-bit architecture */
221 #if UINTPTR_MAX == 0xffffffffffffffff
222 #define Biddy_Untagged(f) ((Biddy_Edge) ((uintptr_t) f & 0x0000ffffffffffff))
223 #else
224 #define Biddy_Untagged(f) 0
225 #endif
226 
227 /*----------------------------------------------------------------------------*/
228 /* Type declarations */
229 /*----------------------------------------------------------------------------*/
230 
231 /*! Biddy_Boolean is used for boolean values. */
232 typedef char Biddy_Boolean;
233 
234 /*! Biddy_String is used for strings. */
235 typedef char *Biddy_String;
236 
237 /*! Biddy_Manager is used to specify manager.
238  Manager is a pointer to BiddyManager. A manager includes Node Table,
239  Variable Table, Formulae Table, Ordering Table, three basic caches
240  (ITE Cache, EA Cache and RC Cache), list of user's caches, system
241  age and some other structures needed for memory management.
242  Internal structure of BiddyManager is not exported but
243  must be imitated to create user's managers */
244 typedef void **Biddy_Manager;
245 
246 /*! Biddy_Cache is used to specify user's cache table.
247  Caches for different operations are different and the user is
248  responsible for the correct internal structure. */
249 typedef void *Biddy_Cache;
250 
251 /*! Biddy_Variable is used for indices in variable table. */
252 /* for tagged graphs this should not be larger than 16 bits */
253 typedef unsigned short int Biddy_Variable;
254 
255 /*! Biddy_Edge is a marked edge (i.e. a marked pointer to BiddyNode).
256  Mark is encoded as the value of the last significant bit.
257  For TZBDDs and TZFDDs, edges are tagged. Tag is a 16 bit number
258  (unsigned short int) whish is stored in the highest part of
259  the pointer (this is safe because only 48 bits are used).
260  TZBDDs and TZFDDs are supported only on 64-bits architectures.
261  Internal structure of BiddyNode is not visible to the user. */
262 typedef void* Biddy_Edge;
263 
264 /*! Biddy_GCFunction is used in Biddy_AddCache to specify user's function
265  which will performs garbage collection. */
267 
268 /*! Biddy_LookupFunction is used in Biddy_Eval1x to specify user's function
269  which will lookups in a user's formula table. */
271 
272 /*----------------------------------------------------------------------------*/
273 /* Structure declarations */
274 /*----------------------------------------------------------------------------*/
275 
276 /*! Biddy_XY is used in Biddy_WriteBddview to pass node coordinates */
277 typedef struct {
278  int id;
279  Biddy_String label;
280  int x;
281  int y;
282  Biddy_Boolean isConstant;
283 } Biddy_XY;
284 
285 /*----------------------------------------------------------------------------*/
286 /* Variable declarations */
287 /*----------------------------------------------------------------------------*/
288 
289 #ifdef __cplusplus
290 extern "C" {
291 #endif
292 
293 #ifdef __cplusplus
294 }
295 #endif
296 
297 /*----------------------------------------------------------------------------*/
298 /* Prototypes for functions exported from biddyMain.c */
299 /*----------------------------------------------------------------------------*/
300 
301 #ifdef __cplusplus
302 extern "C" {
303 #endif
304 
305 /* 1 */
306 /*! Macros Biddy_Init and Biddy_InitAnonymous will initialize anonymous manager.*/
307 #define Biddy_Init() Biddy_InitMNG(NULL,BIDDYTYPEOBDDC)
308 #define Biddy_InitAnonymous(gddtype) Biddy_InitMNG(NULL,gddtype)
309 EXTERN void Biddy_InitMNG(Biddy_Manager *mng, int gddtype);
310 
311 /* 2 */
312 /*! Macro Biddy_Exit will delete anonymous manager. */
313 #define Biddy_Exit() Biddy_ExitMNG(NULL)
314 EXTERN void Biddy_ExitMNG(Biddy_Manager *mng);
315 
316 /* 3 */
317 EXTERN Biddy_String Biddy_About();
318 
319 /* 4 */
320 /*! Macro Biddy_GetManagerType is defined for use with anonymous manager. */
321 #define Biddy_GetManagerType() Biddy_Managed_GetManagerType(NULL)
323 
324 /* 5 */
325 /*! Macro Biddy_GetManagerName is defined for use with anonymous manager. */
326 #define Biddy_GetManagerName() Biddy_Managed_GetManagerName(NULL)
328 
329 /* 6 */
330 /*! Macro Biddy_SetManagerParameters is defined for use with anonymous manager. */
331 #define Biddy_SetManagerParameters(gcr,gcrF,gcrX,rr,rrF,rrX,st,cst) Biddy_Managed_SetManagerParameters(NULL,gcr,gcrF,gcrX,rr,rrF,rrX,st,cst)
332 EXTERN void Biddy_Managed_SetManagerParameters(Biddy_Manager MNG, float gcr, float gcrF, float gcrX, float rr, float rrF, float rrX, float st, float cst);
333 
334 /* 7 */
335 /*! Macro Biddy_Managed_GetThen is defined for your convenience. */
336 #define Biddy_Managed_GetThen(MNG,f) Biddy_GetThen(f)
338 
339 /* 8 */
340 /*! Macro Biddy_Managed_GetElse is defined for your convenience. */
341 #define Biddy_Managed_GetElse(MNG,f) Biddy_GetElse(f)
343 
344 /* 9 */
345 /*! Macro Biddy_Managed_GetTopVariable is defined for your convenience. */
346 #define Biddy_Managed_GetTopVariable(MNG,f) Biddy_GetTopVariable(f)
348 
349 /* 10 */
350 /*! Macro Biddy_IsEqv is defined for use with anonymous manager. */
351 #define Biddy_IsEqv(f1,MNG2,f2) Biddy_Managed_IsEqv(NULL,f1,MNG2,f2)
353 
354 /* 11 */
355 /*! Macro Biddy_SelectNode is defined for use with anonymous manager. */
356 #define Biddy_SelectNode(f) Biddy_Managed_SelectNode(NULL,f)
358 
359 /* 12 */
360 /*! Macro Biddy_DeselectNode is defined for use with anonymous manager. */
361 #define Biddy_DeselectNode(f) Biddy_Managed_DeselectNode(NULL,f)
363 
364 /* 13 */
365 /*! Macro Biddy_IsSelected is defined for use with anonymous manager. */
366 #define Biddy_IsSelected(f) Biddy_Managed_IsSelected(NULL,f)
368 
369 /* 14 */
370 /*! Macro Biddy_SelectFunction is defined for use with anonymous manager. */
371 #define Biddy_SelectFunction(f) Biddy_Managed_SelectFunction(NULL,f)
373 
374 /* 15 */
375 /*! Macro Biddy_DeselectAll is defined for use with anonymous manager. */
376 #define Biddy_DeselectAll() Biddy_Managed_DeselectAll(NULL)
378 
379 /* 16 */
380 /*! Macro Biddy_GetTerminal is defined for use with anonymous manager. */
381 #define Biddy_GetTerminal() Biddy_Managed_GetTerminal(NULL)
383 
384 /* 17 */
385 /*! Macro Biddy_GetConstantZero is defined for use with anonymous manager. */
386 #define Biddy_GetConstantZero() Biddy_Managed_GetConstantZero(NULL)
388 #define Biddy_Managed_GetEmptySet(MNG) Biddy_Managed_GetConstantZero(MNG)
389 #define Biddy_GetEmptySet() Biddy_Managed_GetConstantZero(NULL)
390 
391 /* 18 */
392 /*! Macro Biddy_GetConstantOne is defined for use with anonymous manager. */
393 #define Biddy_GetConstantOne() Biddy_Managed_GetConstantOne(NULL)
395 #define Biddy_Managed_GetUniversalSet(MNG) Biddy_Managed_GetConstantOne(MNG)
396 #define Biddy_GetUniversalSet() Biddy_Managed_GetConstantOne(NULL)
397 
398 /* 19 */
399 /*! Macro Biddy_GetBaseSet is defined for use with anonymous manager. */
400 #define Biddy_GetBaseSet() Biddy_Managed_GetBaseSet(NULL)
402 
403 /* 20 */
404 /*! Macro Biddy_GetVariable is defined for use with anonymous manager. */
405 #define Biddy_GetVariable(x) Biddy_Managed_GetVariable(NULL,x)
407 
408 /* 21 */
409 /*! Macro Biddy_GetLowestVariable is defined for use with anonymous manager. */
410 #define Biddy_GetLowestVariable() Biddy_Managed_GetLowestVariable(NULL)
412 
413 /* 22 */
414 /*! Macro Biddy_GetIthVariable is defined for use with anonymous manager. */
415 #define Biddy_GetIthVariable(i) Biddy_Managed_GetIthVariable(NULL,i)
417 
418 /* 23 */
419 /*! Macro Biddy_GetPrevVariable is defined for use with anonymous manager. */
420 #define Biddy_GetPrevVariable(v) Biddy_Managed_GetPrevVariable(NULL,v)
422 
423 /* 24 */
424 /*! Macro Biddy_GetNextVariable is defined for use with anonymous manager. */
425 #define Biddy_GetNextVariable(v) Biddy_Managed_GetNextVariable(NULL,v)
427 
428 /* 25 */
429 /*! Macro Biddy_GetVariableEdge is defined for use with anonymous manager. */
430 #define Biddy_GetVariableEdge(v) Biddy_Managed_GetVariableEdge(NULL,v)
432 
433 /* 26 */
434 /*! Macro Biddy_GetElementEdge is defined for use with anonymous manager. */
435 #define Biddy_GetElementEdge(v) Biddy_Managed_GetElementEdge(NULL,v)
437 
438 /* 27 */
439 /*! Macro Biddy_GetVariableName is defined for use with anonymous manager. */
440 #define Biddy_GetVariableName(v) Biddy_Managed_GetVariableName(NULL,v)
442 
443 /* 28 */
444 /*! Macro Biddy_GetTopVariableEdge is defined for use with anonymous manager. */
445 #define Biddy_GetTopVariableEdge(f) Biddy_Managed_GetTopVariableEdge(NULL,f)
447 
448 /* 29 */
449 /*! Macro Biddy_GetTopVariableName is defined for use with anonymous manager. */
450 #define Biddy_GetTopVariableName(f) Biddy_Managed_GetTopVariableName(NULL,f)
452 
453 /* 30 */
454 /*! Macro Biddy_GetTopVariableChar is defined for use with anonymous manager. */
455 #define Biddy_GetTopVariableChar(f) Biddy_Managed_GetTopVariableChar(NULL,f)
457 
458 /* 31 */
459 /*! Macro Biddy_ResetVariablesValue is defined for use with anonymous manager. */
460 #define Biddy_ResetVariablesValue() Biddy_Managed_ResetVariablesValue(NULL)
462 
463 /* 32 */
464 /*! Macro Biddy_SetVariableValue is defined for use with anonymous manager. */
465 #define Biddy_SetVariableValue(v,f) Biddy_Managed_SetVariableValue(NULL,v,f)
467 
468 /* 33 */
469 /*! Macro Biddy_GetVariableValue is defined for use with anonymous manager. */
470 #define Biddy_GetVariableValue(v) Biddy_Managed_GetVariableValue(NULL,v)
472 
473 /* 34 */
474 /*! Macro Biddy_ClearVariablesData is defined for use with anonymous manager. */
475 #define Biddy_ClearVariablesData() Biddy_Managed_ClearVariablesData(NULL)
477 
478 /* 35 */
479 /*! Macro Biddy_SetVariableData is defined for use with anonymous manager. */
480 #define Biddy_SetVariableData(v,x) Biddy_Managed_SetVariableData(NULL,v,x)
481 EXTERN void Biddy_Managed_SetVariableData(Biddy_Manager MNG, Biddy_Variable v, void *x);
482 
483 /* 36 */
484 /*! Macro Biddy_GetVariableData is defined for use with anonymous manager. */
485 #define Biddy_GetVariableData(v) Biddy_Managed_GetVariableData(NULL,v)
487 
488 /* 37 */
489 /*! Macro Biddy_IsSmaller is defined for use with anonymous manager. */
490 #define Biddy_IsSmaller(fv,gv) Biddy_Managed_IsSmaller(NULL,fv,gv)
492 
493 /* 38 */
494 /*! Macro Biddy_IsLowest is defined for use with anonymous manager. */
495 #define Biddy_IsLowest(v) Biddy_Managed_IsLowest(NULL,v)
497 
498 /* 39 */
499 /*! Macro Biddy_IsHighest is defined for use with anonymous manager. */
500 #define Biddy_IsHighest(v) Biddy_Managed_IsHighest(NULL,v)
502 
503 /* 40 */
504 /*! Macro Biddy_FoaVariable is defined for use with anonymous manager. */
505 #define Biddy_FoaVariable(x,varelem) Biddy_Managed_FoaVariable(NULL,x,varelem)
507 
508 /* 41 */
509 /*! Macro Biddy_ChangeVariableName is defined for use with anonymous manager. */
510 #define Biddy_ChangeVariableName(v,x) Biddy_Managed_ChangeVariableName(NULL,v,x)
512 
513 /* 42 */
514 /*! Macro Biddy_AddVariableByName is defined for use with anonymous manager. */
515 #define Biddy_AddVariableByName(x) Biddy_Managed_AddVariableByName(NULL,x)
517 #define Biddy_Managed_AddVariable(MNG) Biddy_Managed_AddVariableByName(MNG,NULL)
518 #define Biddy_AddVariable() Biddy_Managed_AddVariableByName(NULL,NULL)
519 
520 /* 43 */
521 /*! Macro Biddy_AddElementByName is defined for use with anonymous manager. */
522 #define Biddy_AddElementByName(x) Biddy_Managed_AddElementByName(NULL,x)
524 #define Biddy_Managed_AddElement(MNG) Biddy_Managed_AddElementByName(MNG,NULL)
525 #define Biddy_AddElement() Biddy_Managed_AddElementByName(NULL,NULL)
526 
527 /* 44 */
528 /*! Macro Biddy_AddVariableBelow is defined for use with anonymous manager. */
529 #define Biddy_AddVariableBelow(v) Biddy_Managed_AddVariableBelow(NULL,v)
531 
532 /* 45 */
533 /*! Macro Biddy_AddVariableAbove is defined for use with anonymous manager. */
534 #define Biddy_AddVariableAbove(v) Biddy_Managed_AddVariableAbove(NULL,v)
536 
537 /* 46 */
538 /*! Macro Biddy_TransferMark is defined for use with anonymous manager. */
539 /*! For OBDD, use macro Biddy_InvCond. */
540 #define Biddy_TransferMark(f,mark,leftright) Biddy_Managed_TransferMark(NULL,f,mark,leftright)
542 
543 /* 47 */
544 /*! Macro Biddy_IncTag is defined for use with anonymous manager. */
545 #define Biddy_IncTag(f) Biddy_Managed_IncTag(NULL,f)
547 
548 /* 48 */
549 /*! Macro Biddy_TaggedFoaNode is defined for use with anonymous manager. */
550 #define Biddy_TaggedFoaNode(v,pf,pt,ptag,garbageAllowed) Biddy_Managed_TaggedFoaNode(NULL,v,pf,pt,ptag,garbageAllowed)
552 #define Biddy_Managed_FoaNode(MNG,v,pf,pt,garbageAllowed) Biddy_Managed_TaggedFoaNode(MNG,v,pf,pt,v,garbageAllowed)
553 #define Biddy_FoaNode(v,pf,pt,garbageAllowed) Biddy_Managed_TaggedFoaNode(NULL,v,pf,pt,v,garbageAllowed)
554 
555 /* 49 */
556 /*! Macro Biddy_IsOK is defined for use with anonymous manager. */
557 #define Biddy_IsOK(f) Biddy_Managed_IsOK(NULL,f)
559 
560 /* 50 */
561 /*! Macro Biddy_GC is defined for use with anonymous manager. */
562 /*! Macros Biddy_Managed_FullGC and Biddy_FullGC are useful variants. */
563 #define Biddy_GC(targetLT,targetGEQ,purge,total) Biddy_Managed_GC(NULL,targetLT,targetGEQ,purge,total)
564 #define Biddy_Managed_AutoGC(MNG) Biddy_Managed_GC(MNG,0,0,FALSE,FALSE)
565 #define Biddy_AutoGC() Biddy_Managed_GC(NULL,0,0,FALSE,FALSE)
566 EXTERN void Biddy_Managed_GC(Biddy_Manager MNG, Biddy_Variable targetLT, Biddy_Variable targetGEQ, Biddy_Boolean purge, Biddy_Boolean total);
567 
568 /* 51 */
569 /*! Macro Biddy_Clean is defined for use with anonymous manager. */
570 #define Biddy_Clean() Biddy_Managed_Clean(NULL)
571 EXTERN void Biddy_Managed_Clean(Biddy_Manager MNG);
572 
573 /* 52 */
574 /*! Macro Biddy_Purge is defined for use with anonymous manager. */
575 #define Biddy_Purge() Biddy_Managed_Purge(NULL)
576 EXTERN void Biddy_Managed_Purge(Biddy_Manager MNG);
577 
578 /* 53 */
579 /*! Macro Biddy_PurgeAndReorder is defined for use with anonymous manager. */
580 #define Biddy_PurgeAndReorder(f,c) Biddy_Managed_PurgeAndReorder(NULL,f,c)
582 
583 /* 54 */
584 /*! Macro Biddy_Refresh is defined for use with anonymous manager. */
585 #define Biddy_Refresh(f) Biddy_Managed_Refresh(NULL,f)
587 
588 /* 55 */
589 /*! Macro Biddy_AddCache is defined for use with anonymous manager. */
590 #define Biddy_AddCache(gc) Biddy_Managed_AddCache(NULL,gc)
592 
593 /* 56 */
594 /*! Macro Biddy_AddFormula is defined for use with anonymous manager. */
595 /*! Macros Biddy_Managed_AddTmpFormula, Biddy_AddTmpFormula, */
596 /*! Biddy_Managed_AddPreservedFormula, Biddy_AddPreservedFormula, */
597 /*! Biddy_Managed_AddPersistentFormula, Biddy_AddPersistentFormula, */
598 /*! Biddy_Managed_KeepFormula, Biddy_KeepFormula, */
599 /*! Biddy_Managed_KeepFormulaUntilDelete, and Biddy_KeepFormulaUntilDelete */
600 /*! are defined to simplify formulae management. */
601 #define Biddy_AddFormula(x,f,c) Biddy_Managed_AddFormula(NULL,x,f,c)
602 EXTERN unsigned int Biddy_Managed_AddFormula(Biddy_Manager MNG, Biddy_String x, Biddy_Edge f, int c);
603 #define Biddy_Managed_AddTmpFormula(mng,x,f) Biddy_Managed_AddFormula(mng,x,f,-1)
604 #define Biddy_Managed_AddPersistentFormula(mng,x,f) Biddy_Managed_AddFormula(mng,x,f,0)
605 #define Biddy_Managed_KeepFormula(mng,f) Biddy_Managed_AddFormula(mng,NULL,f,1)
606 #define Biddy_Managed_KeepFormulaUntilPurge(mng,f) Biddy_Managed_AddFormula(mng,NULL,f,0)
607 #define Biddy_Managed_KeepFormulaProlonged(mng,f,c) Biddy_Managed_AddFormula(mng,NULL,f,c)
608 #define Biddy_AddTmpFormula(x,f) Biddy_Managed_AddFormula(NULL,x,f,-1)
609 #define Biddy_AddPersistentFormula(x,f) Biddy_Managed_AddFormula(NULL,x,f,0)
610 #define Biddy_KeepFormula(f) Biddy_Managed_AddFormula(NULL,NULL,f,1)
611 #define Biddy_KeepFormulaUntilPurge(f) Biddy_Managed_AddFormula(NULL,NULL,f,0)
612 #define Biddy_KeepFormulaProlonged(f,c) Biddy_Managed_AddFormula(NULL,NULL,f,c)
613 
614 /* 57 */
615 /*! Macro Biddy_FindFormula is defined for use with anonymous manager. */
616 #define Biddy_FindFormula(x,idx,f) Biddy_Managed_FindFormula(NULL,x,idx,f)
617 EXTERN Biddy_Boolean Biddy_Managed_FindFormula(Biddy_Manager MNG, Biddy_String x, unsigned int *idx, Biddy_Edge *f);
618 
619 /* 58 */
620 /*! Macro Biddy_DeleteFormula is defined for use with anonymous manager. */
621 #define Biddy_DeleteFormula(x) Biddy_Managed_DeleteFormula(NULL,x)
623 
624 /* 59 */
625 /*! Macro Biddy_DeleteIthFormula is defined for use with anonymous manager. */
626 #define Biddy_DeleteIthFormula(x) Biddy_Managed_DeleteIthFormula(NULL,x)
628 
629 /* 60 */
630 /*! Macro Biddy_GetIthFormula is defined for use with anonymous manager. */
631 #define Biddy_GetIthFormula(i) Biddy_Managed_GetIthFormula(NULL,i)
632 EXTERN Biddy_Edge Biddy_Managed_GetIthFormula(Biddy_Manager MNG, unsigned int i);
633 
634 /* 61 */
635 /*! Macro Biddy_GetIthFormulaName is defined for use with anonymous manager. */
636 #define Biddy_GetIthFormulaName(i) Biddy_Managed_GetIthFormulaName(NULL,i)
638 
639 /* 62 */
640 /*! Macro Biddy_SwapWithHigher is defined for use with anonymous manager. */
641 #define Biddy_SwapWithHigher(v) Biddy_Managed_SwapWithHigher(NULL,v)
643 
644 /* 63 */
645 /*! Macro Biddy_SwapWithLower is defined for use with anonymous manager. */
646 #define Biddy_SwapWithLower(v) Biddy_Managed_SwapWithLower(NULL,v)
648 
649 /* 64 */
650 /*! Macro Biddy_Sifting is defined for use with anonymous manager. */
651 #define Biddy_Sifting(f,c) Biddy_Managed_Sifting(NULL,f,c)
653 
654 /* 65 */
655 /*! Macro Biddy_MinimizeBDD is defined for use with anonymous manager. */
656 #define Biddy_MinimizeBDD(f) Biddy_Managed_MinimizeBDD(NULL,f)
658 
659 /* 66 */
660 /*! Macro Biddy_MaximizeBDD is defined for use with anonymous manager. */
661 #define Biddy_MaximizeBDD(f) Biddy_Managed_MaximizeBDD(NULL,f)
663 
664 /* 67 */
665 /*! Macro Biddy_Copy is defined for use with anonymous manager. */
666 #define Biddy_Copy(MNG2,f) Biddy_Managed_Copy(NULL,MNG2,f)
668 
669 /* 68 */
670 /*! Macro Biddy_CopyFormula is defined for use with anonymous manager. */
671 #define Biddy_CopyFormula(MNG2,x) Biddy_Managed_CopyFormula(NULL,MNG2,x)
673 
674 /* 69 */
675 /*! Macro Biddy_Eval is defined for use with anonymous manager. */
676 #define Biddy_Eval(f) Biddy_Managed_Eval(NULL,f)
678 
679 #ifdef __cplusplus
680 }
681 #endif
682 
683 /*----------------------------------------------------------------------------*/
684 /* Prototypes for functions exported from biddyOp.c */
685 /*----------------------------------------------------------------------------*/
686 
687 #ifdef __cplusplus
688 extern "C" {
689 #endif
690 
691 /* 70 */
692 /*! Macro Biddy_Not is defined for use with anonymous manager. */
693 /*! For OBDD and OFDD, use macro Biddy_Inv. */
694 #define Biddy_Not(f) Biddy_Managed_Not(NULL,f)
696 
697 /* 71 */
698 /*! Macro Biddy_ITE is defined for use with anonymous manager. */
699 #define Biddy_ITE(f,g,h) Biddy_Managed_ITE(NULL,f,g,h)
701 
702 /* 72 */
703 /*! Macro Biddy_And is defined for use with anonymous manager. */
704 /*! Macros Biddy_Managed_Intersect and Biddy_Intersect are defined for set manipulation. */
705 #define Biddy_And(f,g) Biddy_Managed_And(NULL,f,g)
707 #define Biddy_Managed_Intersect(MNG,f,g) Biddy_Managed_And(MNG,f,g)
708 #define Biddy_Intersect(f,g) Biddy_Managed_And(NULL,f,g)
709 
710 /* 73 */
711 /*! Macro Biddy_Or is defined for use with anonymous manager. */
712 /*! Macros Biddy_Managed_Union and Biddy_Union are defined for set manipulation. */
713 #define Biddy_Or(f,g) Biddy_Managed_Or(NULL,f,g)
715 #define Biddy_Managed_Union(MNG,f,g) Biddy_Managed_Or(MNG,f,g)
716 #define Biddy_Union(f,g) Biddy_Managed_Or(NULL,f,g)
717 
718 /* 74 */
719 /*! Macro Biddy_Nand is defined for use with anonymous manager. */
720 #define Biddy_Nand(f,g) Biddy_Managed_Nand(NULL,f,g)
722 
723 /* 75 */
724 /*! Macro Biddy_Nor is defined for use with anonymous manager. */
725 #define Biddy_Nor(f,g) Biddy_Managed_Nor(NULL,f,g)
727 
728 /* 76 */
729 /*! Macro Biddy_Xor is defined for use with anonymous manager. */
730 #define Biddy_Xor(f,g) Biddy_Managed_Xor(NULL,f,g)
732 
733 /* 77 */
734 /*! Macro Biddy_Xnor is defined for use with anonymous manager. */
735 #define Biddy_Xnor(f,g) Biddy_Managed_Xnor(NULL,f,g)
737 
738 /* 78 */
739 /*! Macro Biddy_Leq is defined for use with anonymous manager. */
740 #define Biddy_Leq(f,g) Biddy_Managed_Leq(NULL,f,g)
742 
743 /* 79 */
744 /*! Macro Biddy_Gt is defined for use with anonymous manager. */
745 #define Biddy_Gt(f,g) Biddy_Managed_Gt(NULL,f,g)
747 #define Biddy_Managed_Diff(MNG,f,g) Biddy_Managed_Gt(MNG,g,f)
748 #define Biddy_Diff(f,g) Biddy_Managed_Gt(NULL,g,f)
749 
750 /* 80 */
751 /*! Macro Biddy_IsLeq is defined for use with anonymous manager. */
752 #define Biddy_IsLeq(f,g) Biddy_Managed_IsLeq(NULL,f,g)
754 
755 /* 81 */
756 /* This is used to calculate cofactors f|{v=0} and f|{v=1}. */
757 /*! Macro Biddy_Restrict is defined for use with anonymous manager. */
758 #define Biddy_Restrict(f,v,value) Biddy_Managed_Restrict(NULL,f,v,value)
760 
761 /* 82 */
762 /*! Macro Biddy_Compose is defined for use with anonymous manager. */
763 #define Biddy_Compose(f,g,v) Biddy_Managed_Compose(NULL,f,g,v)
765 
766 /* 83 */
767 /*! Macro Biddy_E is defined for use with anonymous manager. */
768 #define Biddy_E(f,v) Biddy_Managed_E(NULL,f,v)
770 
771 /* 84 */
772 /*! Macro Biddy_A is defined for use with anonymous manager. */
773 #define Biddy_A(f,v) Biddy_Managed_A(NULL,f,v)
775 
776 /* 85 */
777 /*! Macro Biddy_IsVariableDependent is defined for use with anonymous manager. */
778 #define Biddy_IsVariableDependent(f,v) Biddy_Managed_IsVariableDependent(NULL,f,v)
780 
781 /* 86 */
782 /*! Macro Biddy_ExistAbstract is defined for use with anonymous manager. */
783 #define Biddy_ExistAbstract(f,cube) Biddy_Managed_ExistAbstract(NULL,f,cube)
785 
786 /* 87 */
787 /*! Macro Biddy_UnivAbstract is defined for use with anonymous manager. */
788 #define Biddy_UnivAbstract(f,cube) Biddy_Managed_UnivAbstract(NULL,f,cube)
790 
791 /* 88 */
792 /*! Macro Biddy_AndAbstract is defined for use with anonymous manager. */
793 #define Biddy_AndAbstract(f,g,cube) Biddy_Managed_AndAbstract(NULL,f,g,cube)
795 
796 /* 89 */
797 /*! Macro Biddy_Constrain is defined for use with anonymous manager. */
798 #define Biddy_Constrain(f,c) Biddy_Managed_Constrain(NULL,f,c)
800 
801 /* 90 */
802 /* This is Coudert and Madre's restrict function */
803 /*! Macro Biddy_Simplify is defined for use with anonymous manager. */
804 #define Biddy_Simplify(f,c) Biddy_Managed_Simplify(NULL,f,c)
806 
807 /* 91 */
808 /*! Macro Biddy_Support is defined for use with anonymous manager. */
809 #define Biddy_Support(f) Biddy_Managed_Support(NULL,f)
811 
812 /* 92 */
813 /*! Macro Biddy_ReplaceByKeyword is defined for use with anonymous manager. */
814 /*! Macros Biddy_Managed_Replace and Biddy_Replace are variants */
815 /*! with less effective cache table */
816 #define Biddy_ReplaceByKeyword(f,keyword) Biddy_Managed_ReplaceByKeyword(NULL,f,keyword)
818 #define Biddy_Managed_Replace(MNG,f) Biddy_Managed_ReplaceByKeyword(MNG,f,NULL)
819 #define Biddy_Replace(f) Biddy_Managed_ReplaceByKeyword(NULL,f,NULL)
820 
821 /* 93 */
822 /*! Macro Biddy_Change is defined for use with anonymous manager. */
823 #define Biddy_Change(f,v) Biddy_Managed_Change(NULL,f,v)
825 
826 /* 94 */
827 /* This is used to calculate f*v and f*(-v) */
828 /*! Macro Biddy_Subset is defined for use with anonymous manager. */
829 #define Biddy_Subset(f,v,value) Biddy_Managed_Subset(NULL,f,v,value)
831 #define Biddy_Managed_Subset0(MNG,f,v) Biddy_Managed_Subset(MNG,f,v,FALSE)
832 #define Biddy_Subset0(f,v) Biddy_Managed_Subset(NULL,f,v,FALSE)
833 #define Biddy_Managed_Subset1(MNG,f,v) Biddy_Managed_Subset(MNG,f,v,TRUE)
834 #define Biddy_Subset1(f,v) Biddy_Managed_Subset(NULL,f,v,TRUE)
835 
836 /* 95 */
837 /*! Macro Biddy_CreateMinterm is defined for use with anonymous manager. */
838 #define Biddy_CreateMinterm(support,x) Biddy_Managed_CreateMinterm(NULL,support,x)
839 EXTERN Biddy_Edge Biddy_Managed_CreateMinterm(Biddy_Manager MNG, Biddy_Edge support, long long unsigned int x);
840 
841 /* 96 */
842 /*! Macro Biddy_CreateFunction is defined for use with anonymous manager. */
843 #define Biddy_CreateFunction(support,x) Biddy_Managed_CreateFunction(NULL,support,x)
844 EXTERN Biddy_Edge Biddy_Managed_CreateFunction(Biddy_Manager MNG, Biddy_Edge support, long long unsigned int x);
845 
846 /* 97 */
847 /*! Macro Biddy_RandomFunction is defined for use with anonymous manager. */
848 #define Biddy_RandomFunction(support,r) Biddy_Managed_RandomFunction(NULL,support,r)
849 EXTERN Biddy_Edge Biddy_Managed_RandomFunction(Biddy_Manager MNG, Biddy_Edge support, double r);
850 
851 /* 98 */
852 /*! Macro Biddy_RandomSet is defined for use with anonymous manager. */
853 #define Biddy_RandomSet(unit,r) Biddy_Managed_RandomSet(NULL,unit,r)
854 EXTERN Biddy_Edge Biddy_Managed_RandomSet(Biddy_Manager MNG, Biddy_Edge unit, double r);
855 
856 #ifdef __cplusplus
857 }
858 #endif
859 
860 /* TO DO: unique */
861 /* Unique quantification of variables. */
862 /* Similar to existential quantification but uses XOR instead of OR. */
863 
864 /*----------------------------------------------------------------------------*/
865 /* Prototypes for functions exported from biddyStat.c */
866 /*----------------------------------------------------------------------------*/
867 
868 #ifdef __cplusplus
869 extern "C" {
870 #endif
871 
872 /* 99 */
873 /*! Macro Biddy_CountNodes(f) is defined for use with anonymous manager. */
874 #define Biddy_CountNodes(f) Biddy_Managed_CountNodes(NULL,f)
875 EXTERN unsigned int Biddy_Managed_CountNodes(Biddy_Manager MNG, Biddy_Edge f);
876 
877 /* 100 */
878 /*! Macro Biddy_Managed_MaxLevel(MNG,f) is defined for your convenience. */
879 #define Biddy_Managed_MaxLevel(MNG,f) Biddy_MaxLevel(f)
880 EXTERN unsigned int Biddy_MaxLevel(Biddy_Edge f);
881 
882 /* 101 */
883 /*! Macro Biddy_Managed_AvgLevel(MNG,f) is defined for your convenience. */
884 #define Biddy_Managed_AvgLevel(MNG,f) Biddy_AvgLevel(f)
885 EXTERN float Biddy_AvgLevel(Biddy_Edge f);
886 
887 /* 102 */
888 /*! Macro Biddy_VariableTableNum is defined for use with anonymous manager. */
889 #define Biddy_VariableTableNum() Biddy_Managed_VariableTableNum(NULL)
891 
892 /* 103 */
893 /*! Macro Biddy_NodeTableSize is defined for use with anonymous manager. */
894 #define Biddy_NodeTableSize() Biddy_Managed_NodeTableSize(NULL)
895 EXTERN unsigned int Biddy_Managed_NodeTableSize(Biddy_Manager MNG);
896 
897 /* 104 */
898 /*! Macro Biddy_NodeTableBlockNumber is defined for use with anonymous manager. */
899 #define Biddy_NodeTableBlockNumber() Biddy_Managed_NodeTableBlockNumber(NULL)
900 EXTERN unsigned int Biddy_Managed_NodeTableBlockNumber(Biddy_Manager MNG);
901 
902 /* 105 */
903 /*! Macro Biddy_NodeTableGenerated is defined for use with anonymous manager. */
904 #define Biddy_NodeTableGenerated() Biddy_Managed_NodeTableGenerated(NULL)
905 EXTERN unsigned int Biddy_Managed_NodeTableGenerated(Biddy_Manager MNG);
906 
907 /* 106 */
908 /*! Macro Biddy_NodeTableMax is defined for use with anonymous manager. */
909 #define Biddy_NodeTableMax() Biddy_Managed_NodeTableMax(NULL)
910 EXTERN unsigned int Biddy_Managed_NodeTableMax(Biddy_Manager MNG);
911 
912 /* 107 */
913 /*! Macro Biddy_NodeTableNum is defined for use with anonymous manager. */
914 #define Biddy_NodeTableNum() Biddy_Managed_NodeTableNum(NULL)
915 EXTERN unsigned int Biddy_Managed_NodeTableNum(Biddy_Manager MNG);
916 
917 /* 108 */
918 /*! Macro Biddy_NodeTableNumVar is defined for use with anonymous manager. */
919 #define Biddy_NodeTableNumVar(v) Biddy_Managed_NodeTableNumVar(NULL,v)
921 
922 /* 109 */
923 /*! Macro Biddy_NodeTableResizeNumber is defined for use with anonymous manager. */
924 #define Biddy_NodeTableResizeNumber() Biddy_Managed_NodeTableResizeNumber(NULL)
925 EXTERN unsigned int Biddy_Managed_NodeTableResizeNumber(Biddy_Manager MNG);
926 
927 /* 110 */
928 /*! Macro Biddy_NodeTableFoaNumber is defined for use with anonymous manager. */
929 #define Biddy_NodeTableFoaNumber() Biddy_Managed_NodeTableFoaNumber(NULL)
930 EXTERN unsigned long long int Biddy_Managed_NodeTableFoaNumber(Biddy_Manager MNG);
931 
932 /* 111 */
933 /*! Macro Biddy_NodeTableFindNumber is defined for use with anonymous manager. */
934 #define Biddy_NodeTableFindNumber() Biddy_Managed_NodeTableFindNumber(NULL)
935 EXTERN unsigned long long int Biddy_Managed_NodeTableFindNumber(Biddy_Manager MNG);
936 
937 /* 112 */
938 /*! Macro Biddy_NodeTableCompareNumber is defined for use with anonymous manager. */
939 #define Biddy_NodeTableCompareNumber() Biddy_Managed_NodeTableCompareNumber(NULL)
940 EXTERN unsigned long long int Biddy_Managed_NodeTableCompareNumber(Biddy_Manager MNG);
941 
942 /* 113 */
943 /*! Macro Biddy_NodeTableAddNumber is defined for use with anonymous manager. */
944 #define Biddy_NodeTableAddNumber() Biddy_Managed_NodeTableAddNumber(NULL)
945 EXTERN unsigned long long int Biddy_Managed_NodeTableAddNumber(Biddy_Manager MNG);
946 
947 /* 114 */
948 /*! Macro Biddy_NodeTableGCNumber is defined for use with anonymous manager. */
949 #define Biddy_NodeTableGCNumber() Biddy_Managed_NodeTableGCNumber(NULL)
950 EXTERN unsigned int Biddy_Managed_NodeTableGCNumber(Biddy_Manager MNG);
951 
952 /* 115 */
953 /*! Macro Biddy_NodeTableGCTime is defined for use with anonymous manager. */
954 #define Biddy_NodeTableGCTime() Biddy_Managed_NodeTableGCTime(NULL)
955 EXTERN unsigned int Biddy_Managed_NodeTableGCTime(Biddy_Manager MNG);
956 
957 /* 116 */
958 /*! Macro Biddy_NodeTableGCObsoleteNumber is defined for use with anonymous manager. */
959 #define Biddy_NodeTableGCObsoleteNumber() Biddy_Managed_NodeTableGCObsoleteNumber(NULL)
960 EXTERN unsigned long long int Biddy_Managed_NodeTableGCObsoleteNumber(Biddy_Manager MNG);
961 
962 /* 117 */
963 /*! Macro Biddy_NodeTableSwapNumber is defined for use with anonymous manager. */
964 #define Biddy_NodeTableSwapNumber() Biddy_Managed_NodeTableSwapNumber(NULL)
965 EXTERN unsigned int Biddy_Managed_NodeTableSwapNumber(Biddy_Manager MNG);
966 
967 /* 118 */
968 /*! Macro Biddy_NodeTableSiftingNumber is defined for use with anonymous manager. */
969 #define Biddy_NodeTableSiftingNumber() Biddy_Managed_NodeTableSiftingNumber(NULL)
970 EXTERN unsigned int Biddy_Managed_NodeTableSiftingNumber(Biddy_Manager MNG);
971 
972 /* 119 */
973 /*! Macro Biddy_NodeTableDRTime is defined for use with anonymous manager. */
974 #define Biddy_NodeTableDRTime() Biddy_Managed_NodeTableDRTime(NULL)
975 EXTERN unsigned int Biddy_Managed_NodeTableDRTime(Biddy_Manager MNG);
976 
977 /* 120 */
978 /*! Macro Biddy_NodeTableITENumber is defined for use with anonymous manager. */
979 #define Biddy_NodeTableITENumber() Biddy_Managed_NodeTableITENumber(NULL)
980 EXTERN unsigned int Biddy_Managed_NodeTableITENumber(Biddy_Manager MNG);
981 
982 /* 121 */
983 /*! Macro Biddy_NodeTableITERecursiveNumber is defined for use with anonymous manager. */
984 #define Biddy_NodeTableITERecursiveNumber() Biddy_Managed_NodeTableITERecursiveNumber(NULL)
985 EXTERN unsigned long long int Biddy_Managed_NodeTableITERecursiveNumber(Biddy_Manager MNG);
986 
987 /* 122 */
988 /*! Macro Biddy_NodeTableANDORNumber is defined for use with anonymous manager. */
989 #define Biddy_NodeTableANDORNumber() Biddy_Managed_NodeTableANDORNumber(NULL)
990 EXTERN unsigned int Biddy_Managed_NodeTableANDORNumber(Biddy_Manager MNG);
991 
992 /* 123 */
993 /*! Macro Biddy_NodeTableANDORRecursiveNumber is defined for use with anonymous manager. */
994 #define Biddy_NodeTableANDORRecursiveNumber() Biddy_Managed_NodeTableANDORRecursiveNumber(NULL)
995 EXTERN unsigned long long int Biddy_Managed_NodeTableANDORRecursiveNumber(Biddy_Manager MNG);
996 
997 /* 124 */
998 /*! Macro Biddy_NodeTableXORNumber is defined for use with anonymous manager. */
999 #define Biddy_NodeTableXORNumber() Biddy_Managed_NodeTableXORNumber(NULL)
1000 EXTERN unsigned int Biddy_Managed_NodeTableXORNumber(Biddy_Manager MNG);
1001 
1002 /* 125 */
1003 /*! Macro Biddy_NodeTableXORRecursiveNumber is defined for use with anonymous manager. */
1004 #define Biddy_NodeTableXORRecursiveNumber() Biddy_Managed_NodeTableXORRecursiveNumber(NULL)
1005 EXTERN unsigned long long int Biddy_Managed_NodeTableXORRecursiveNumber(Biddy_Manager MNG);
1006 
1007 /* 126 */
1008 /*! Macro Biddy_FormulaTableNum is defined for use with anonymous manager. */
1009 #define Biddy_FormulaTableNum() Biddy_Managed_FormulaTableNum(NULL)
1010 EXTERN unsigned int Biddy_Managed_FormulaTableNum(Biddy_Manager MNG);
1011 
1012 /* 127 */
1013 /*! Macro Biddy_ListUsed is defined for use with anonymous manager. */
1014 #define Biddy_ListUsed() Biddy_Managed_ListUsed(NULL)
1015 EXTERN unsigned int Biddy_Managed_ListUsed(Biddy_Manager MNG);
1016 
1017 /* 128 */
1018 /*! Macro Biddy_ListMaxLength is defined for use with anonymous manager. */
1019 #define Biddy_ListMaxLength() Biddy_Managed_ListMaxLength(NULL)
1020 EXTERN unsigned int Biddy_Managed_ListMaxLength(Biddy_Manager MNG);
1021 
1022 /* 129 */
1023 /*! Macro Biddy_ListAvgLength is defined for use with anonymous manager. */
1024 #define Biddy_ListAvgLength() Biddy_Managed_ListAvgLength(NULL)
1025 EXTERN float Biddy_Managed_ListAvgLength(Biddy_Manager MNG);
1026 
1027 /* 130 */
1028 /*! Macro Biddy_OPCacheSearch is defined for use with anonymous manager. */
1029 #define Biddy_OPCacheSearch() Biddy_Managed_OPCacheSearch(NULL)
1030 EXTERN unsigned long long int Biddy_Managed_OPCacheSearch(Biddy_Manager MNG);
1031 
1032 /* 131 */
1033 /*! Macro Biddy_OPCacheFind is defined for use with anonymous manager. */
1034 #define Biddy_OPCacheFind() Biddy_Managed_OPCacheFind(NULL)
1035 EXTERN unsigned long long int Biddy_Managed_OPCacheFind(Biddy_Manager MNG);
1036 
1037 /* 132 */
1038 /*! Macro Biddy_OPCacheInsert is defined for use with anonymous manager. */
1039 #define Biddy_OPCacheInsert() Biddy_Managed_OPCacheInsert(NULL)
1040 EXTERN unsigned long long int Biddy_Managed_OPCacheInsert(Biddy_Manager MNG);
1041 
1042 /* 133 */
1043 /*! Macro Biddy_OPCacheOverwrite is defined for use with anonymous manager. */
1044 #define Biddy_OPCacheOverwrite() Biddy_Managed_OPCacheOverwrite(NULL)
1045 EXTERN unsigned long long int Biddy_Managed_OPCacheOverwrite(Biddy_Manager MNG);
1046 
1047 /* 134 */
1048 /*! Macro Biddy_CountNodesPlain is defined for use with anonymous manager. */
1049 #define Biddy_CountNodesPlain(f) Biddy_Managed_CountNodesPlain(NULL,f)
1050 EXTERN unsigned int Biddy_Managed_CountNodesPlain(Biddy_Manager MNG, Biddy_Edge f);
1051 
1052 /* 135 */
1053 /*! Macro Biddy_DependentVariableNumber is defined for use with anonymous manager. */
1054 #define Biddy_DependentVariableNumber(f) Biddy_Managed_DependentVariableNumber(NULL,f)
1056 
1057 /* 136 */
1058 /*! Macro Biddy_CountComplementedEdges is defined for use with anonymous manager. */
1059 #define Biddy_CountComplementedEdges(f) Biddy_Managed_CountComplementedEdges(NULL,f)
1061 
1062 /* 137 */
1063 /*! Macro Biddy_CountPaths is defined for use with anonymous manager. */
1064 #define Biddy_CountPaths(f) Biddy_Managed_CountPaths(NULL,f)
1065 EXTERN unsigned long long int Biddy_Managed_CountPaths(Biddy_Manager MNG, Biddy_Edge f);
1066 
1067 /* 138 */
1068 /*! Macro Biddy_CountMinterms is defined for use with anonymous manager. */
1069 #define Biddy_CountMinterms(f,nvars) Biddy_Managed_CountMinterms(NULL,f,nvars)
1070 EXTERN double Biddy_Managed_CountMinterms(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars);
1071 #define Biddy_Managed_CountCombinations(MNG,f,nvars) Biddy_Managed_CountMinterms(MNG,f,nvars)
1072 #define Biddy_CountCombinations(f) Biddy_Managed_CountMinterms(NULL,f,nvars)
1073 
1074 /* 139 */
1075 /*! Macro Biddy_DensityOfFunction is defined for use with anonymous manager. */
1076 #define Biddy_DensityOfFunction(f,nvars) Biddy_Managed_DensityOfFunction(NULL,f,nvars)
1077 EXTERN double Biddy_Managed_DensityOfFunction(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars);
1078 
1079 /* 140 */
1080 /*! Macro Biddy_DensityOfBDD is defined for use with anonymous manager. */
1081 #define Biddy_DensityOfBDD(f,nvars) Biddy_Managed_DensityOfBDD(NULL,f,nvars)
1082 EXTERN double Biddy_Managed_DensityOfBDD(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars);
1083 
1084 /* 141 */
1085 /*! Macro Biddy_ReadMemoryInUse is defined for use with anonymous manager. */
1086 #define Biddy_ReadMemoryInUse() Biddy_Managed_ReadMemoryInUse(NULL)
1087 EXTERN unsigned long long int Biddy_Managed_ReadMemoryInUse(Biddy_Manager MNG);
1088 
1089 /* 142 */
1090 /*! Macro Biddy_PrintInfo is defined for use with anonymous manager. */
1091 #define Biddy_PrintInfo(f) Biddy_Managed_PrintInfo(NULL,f)
1092 EXTERN void Biddy_Managed_PrintInfo(Biddy_Manager MNG, FILE *f);
1093 
1094 #ifdef __cplusplus
1095 }
1096 #endif
1097 
1098 /*----------------------------------------------------------------------------*/
1099 /* Prototypes for functions exported from biddyInOut.c */
1100 /*----------------------------------------------------------------------------*/
1101 
1102 #ifdef __cplusplus
1103 extern "C" {
1104 #endif
1105 
1106 /* 143 */
1107 /*! Macro Biddy_Eval0 is defined for use with anonymous manager. */
1108 #define Biddy_Eval0(s) Biddy_Managed_Eval0(NULL,s)
1110 
1111 /* 144 */
1112 /*! Macro Biddy_Eval1x is defined for use with anonymous manager. */
1113 #define Biddy_Eval1x(s,lf) Biddy_Managed_Eval1x(NULL,s,lf)
1115 #define Biddy_Managed_Eval1(MNG,s) Biddy_Managed_Eval1x(MNG,s,NULL)
1116 #define Biddy_Eval1(s) Biddy_Managed_Eval1x(NULL,s,NULL)
1117 
1118 /* 145 */
1119 /*! Macro Biddy_Eval2 is defined for use with anonymous manager. */
1120 #define Biddy_Eval2(boolFunc) Biddy_Managed_Eval2(NULL,boolFunc)
1122 
1123 /* 146 */
1124 /*! Macro Biddy_ReadVerilogFile is defined for use with anonymous manager. */
1125 #define Biddy_ReadVerilogFile(filename,prefix) Biddy_Managed_ReadVerilogFile(NULL,filename,prefix)
1126 EXTERN void Biddy_Managed_ReadVerilogFile(Biddy_Manager MNG, const char filename[], Biddy_String prefix);
1127 
1128 /* 147 */
1129 /*! Macro Biddy_PrintfBDD is defined for use with anonymous manager. */
1130 #define Biddy_PrintfBDD(f) Biddy_Managed_PrintfBDD(NULL,f)
1132 
1133 /* 148 */
1134 /*! Macro Biddy_WriteBDD is defined for use with anonymous manager. */
1135 #define Biddy_WriteBDD(filename,f,label) Biddy_Managed_WriteBDD(NULL,filename,f,label)
1136 EXTERN void Biddy_Managed_WriteBDD(Biddy_Manager MNG, const char filename[], Biddy_Edge f, Biddy_String label);
1137 
1138 /* 149 */
1139 /*! Macro Biddy_PrintfTable is defined for use with anonymous manager. */
1140 #define Biddy_PrintfTable(f) Biddy_Managed_PrintfTable(NULL,f)
1142 
1143 /* 150 */
1144 /*! Macro Biddy_WriteTable is defined for use with anonymous manager. */
1145 #define Biddy_WriteTable(filename,f) Biddy_Managed_WriteTable(NULL,filename,f)
1146 EXTERN void Biddy_Managed_WriteTable(Biddy_Manager MNG, const char filename[], Biddy_Edge f);
1147 
1148 /* 151 */
1149 /*! Macro Biddy_PrintfSOP is defined for use with anonymous manager. */
1150 #define Biddy_PrintfSOP(f) Biddy_Managed_PrintfSOP(NULL,f)
1152 
1153 /* 152 */
1154 /*! Macro Biddy_WriteSOP is defined for use with anonymous manager. */
1155 #define Biddy_WriteSOP(filename,f) Biddy_Managed_WriteSOP(NULL,filename,f)
1156 EXTERN void Biddy_Managed_WriteSOP(Biddy_Manager MNG, const char filename[], Biddy_Edge f);
1157 
1158 /* 153 */
1159 /*! Macro Biddy_WriteDot is defined for use with anonymous manager. */
1160 #define Biddy_WriteDot(filename,f,label,id,cudd) Biddy_Managed_WriteDot(NULL,filename,f,label,id,cudd);
1161 EXTERN unsigned int Biddy_Managed_WriteDot(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], int id, Biddy_Boolean cudd);
1162 
1163 /* 154 */
1164 /*! Macro Biddy_WriteBddview is defined for use with anonymous manager. */
1165 #define Biddy_WriteBddview(filename,f,label,table) Biddy_Managed_WriteBddview(NULL,filename,f,label,table);
1166 EXTERN unsigned int Biddy_Managed_WriteBddview(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], Biddy_XY *table);
1167 
1168 #ifdef __cplusplus
1169 }
1170 #endif
1171 
1172 /* TO DO: CNF + DIMACS BENCHMARKS */
1173 /* http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html */
1174 /* http://www.dwheeler.com/essays/minisat-user-guide.html */
1175 /* http://www.miroslav-velev.com/sat_benchmarks.html */
1176 /* http://www.satcompetition.org/ */
1177 
1178 #endif /* _BIDDY */
Biddy_Variable Biddy_Managed_SwapWithLower(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_SwapWithLower swaps two adjacent variables.
Definition: biddyMain.c:4875
unsigned long long int Biddy_Managed_OPCacheFind(Biddy_Manager MNG)
Function Biddy_Managed_OPCacheFind.
Definition: biddyStat.c:1102
int Biddy_Managed_GetManagerType(Biddy_Manager MNG)
Function Biddy_Managed_GetManagerType reports BDD type used in the manager.
Definition: biddyMain.c:1100
Biddy_String Biddy_Managed_GetTopVariableName(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_GetTopVariableName returns the name of top variable.
Definition: biddyMain.c:1970
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:3468
void Biddy_Managed_DeselectAll(Biddy_Manager MNG)
Function Biddy_Managed_DeselectAll deselects all nodes.
Definition: biddyMain.c:1480
Biddy_Edge Biddy_Managed_Eval2(Biddy_Manager MNG, Biddy_String boolFunc)
Function Biddy_Managed_Eval2 evaluates infix &|^~>< format.
Definition: biddyInOut.c:417
unsigned int Biddy_MaxLevel(Biddy_Edge f)
Function Biddy_MaxLevel.
Definition: biddyStat.c:164
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. ...
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:1423
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:1452
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) ...
Biddy_Boolean(* Biddy_LookupFunction)(Biddy_String, Biddy_Edge *)
Definition: biddy.h:270
void * Biddy_Edge
Definition: biddy.h:262
unsigned int Biddy_Managed_NodeTableGCNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableGCNumber.
Definition: biddyStat.c:565
unsigned long long int Biddy_Managed_NodeTableANDORRecursiveNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableANDORRecursiveNumber.
Definition: biddyStat.c:822
Biddy_Variable Biddy_Managed_GetVariable(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_GetVariable returns variable with the given name.
Definition: biddyMain.c:1677
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:2586
void Biddy_Managed_SetVariableValue(Biddy_Manager MNG, Biddy_Variable v, Biddy_Edge f)
Function Biddy_Managed_SetVariableValue sets variable&#39;s value.
Definition: biddyMain.c:2057
Biddy_Edge Biddy_Managed_AddVariableAbove(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_AddVariableAbove adds variable.
Definition: biddyMain.c:2772
void Biddy_Managed_WriteSOP(Biddy_Manager MNG, const char filename[], Biddy_Edge f)
Function Biddy_Managed_WriteSOP writes SOP using fprintf.
Definition: biddyInOut.c:996
void * Biddy_Managed_GetVariableData(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableData gets variable&#39;s data.
Definition: biddyMain.c:2169
double Biddy_Managed_CountMinterms(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
Function Biddy_Managed_CountMinterms.
Definition: biddyStat.c:1520
Biddy_Edge Biddy_Managed_GetBaseSet(Biddy_Manager MNG)
Function Biddy_Managed_GetBaseSet returns set containing only a null combination, i...
Definition: biddyMain.c:1612
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:4008
Biddy_Variable Biddy_Managed_VariableTableNum(Biddy_Manager MNG)
Function Biddy_Managed_VariableTableNum returns number of used variables.
Definition: biddyStat.c:228
Biddy_Edge Biddy_Managed_Or(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Or calculates Boolean function OR (disjunction).
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:1835
void Biddy_Managed_PrintfBDD(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_PrintfBDD writes raw format using printf.
Definition: biddyInOut.c:711
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:5804
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:1169
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:5222
Biddy_Edge Biddy_GetThen(Biddy_Edge fun)
Function Biddy_GetThen returns THEN successor.
Definition: biddyMain.c:1213
Biddy_Boolean Biddy_Managed_DeleteFormula(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_DeleteFormula delete formula from Formula table.
Definition: biddyMain.c:4615
unsigned long long int Biddy_Managed_NodeTableAddNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableAddNumber.
Definition: biddyStat.c:534
Biddy_Variable Biddy_GetTopVariable(Biddy_Edge fun)
Function Biddy_GetTopVariable returns the top variable.
Definition: biddyMain.c:1285
void Biddy_Managed_WriteBDD(Biddy_Manager MNG, const char filename[], Biddy_Edge f, Biddy_String label)
Function Biddy_Managed_WriteBDD writes raw format using fprintf.
Definition: biddyInOut.c:741
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:5312
Biddy_Edge Biddy_Managed_Leq(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Leq calculates Boolean implication.
Biddy_String Biddy_About()
Function Biddy_About reports version of Biddy package.
Definition: biddyMain.c:1077
void Biddy_Managed_WriteTable(Biddy_Manager MNG, const char filename[], Biddy_Edge f)
Function Biddy_Managed_WriteTable writes truth table using fprintf.
Definition: biddyInOut.c:896
Biddy_Edge Biddy_Managed_AddElementByName(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_AddElementByName adds element.
Definition: biddyMain.c:2657
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:2196
Biddy_Variable Biddy_Managed_SwapWithHigher(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_SwapWithHigher swaps two adjacent variables.
Definition: biddyMain.c:4811
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:1309
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.
Biddy_Edge Biddy_Managed_Gt(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Gt calculates the negation of Boolean implication.
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.
Biddy_Variable Biddy_Managed_GetLowestVariable(Biddy_Manager MNG)
Function Biddy_Managed_GetLowestVariable returns the lowest variable in the current ordering...
Definition: biddyMain.c:1729
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:2260
void Biddy_ExitMNG(Biddy_Manager *mng)
Function Biddy_ExitMNG deletes a manager.
Definition: biddyMain.c:854
Biddy_Edge Biddy_Managed_Support(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Support calculates a product of all dependent variables.
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:4111
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.
Biddy_Edge Biddy_Managed_Nor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Nor calculates Boolean function NOR (Peirce).
unsigned int Biddy_Managed_NodeTableGCTime(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableGCTime.
Definition: biddyStat.c:590
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:4770
void Biddy_Managed_Clean(Biddy_Manager MNG)
Function Biddy_Managed_Clean performs cleaning.
Definition: biddyMain.c:3958
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:4056
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.
unsigned int Biddy_Managed_FormulaTableNum(Biddy_Manager MNG)
Function Biddy_Managed_FormulaTableNum returns number of known formulae.
Definition: biddyStat.c:913
unsigned int Biddy_Managed_NodeTableANDORNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableANDORNumber.
Definition: biddyStat.c:794
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. ...
void ** Biddy_Manager
Definition: biddy.h:244
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:1344
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:5666
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:5613
unsigned long long int Biddy_Managed_NodeTableITERecursiveNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableITERecursiveNumber.
Definition: biddyStat.c:762
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...
void Biddy_Managed_ClearVariablesData(Biddy_Manager MNG)
Function Biddy_Managed_ClearVariablesData free memory used for all variable&#39;s data.
Definition: biddyMain.c:2110
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...
void Biddy_Managed_Refresh(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Refresh refreshes top node in a given function.
Definition: biddyMain.c:4085
unsigned int Biddy_Managed_CountComplementedEdges(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountComplementedEdges count the number of complemented edges.
Definition: biddyStat.c:1389
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:1735
unsigned int Biddy_Managed_NodeTableSize(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableSize returns the size of node table.
Definition: biddyStat.c:253
Biddy_Edge Biddy_Managed_GetConstantZero(Biddy_Manager MNG)
Function Biddy_Managed_GetConstantZero returns constant 0.
Definition: biddyMain.c:1554
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:5120
float Biddy_Managed_ListAvgLength(Biddy_Manager MNG)
Function Biddy_Managed_ListAvgLength.
Definition: biddyStat.c:1035
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:1111
Biddy_String Biddy_Managed_GetVariableName(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableName returns the name of a variable.
Definition: biddyMain.c:1914
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:1370
unsigned int Biddy_Managed_NodeTableGenerated(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableGenerated.
Definition: biddyStat.c:308
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:1126
unsigned long long int Biddy_Managed_NodeTableFindNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableFindNumber.
Definition: biddyStat.c:470
float Biddy_AvgLevel(Biddy_Edge f)
Function Biddy_AvgLevel.
Definition: biddyStat.c:196
void Biddy_Managed_PrintInfo(Biddy_Manager MNG, FILE *f)
Function Biddy_Managed_PrintInfo prepare a file with stats.
Definition: biddyStat.c:1914
unsigned int Biddy_Managed_ListMaxLength(Biddy_Manager MNG)
Function Biddy_Managed_ListMaxLength.
Definition: biddyStat.c:971
unsigned short int Biddy_Variable
Definition: biddy.h:253
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:4441
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.
void(* Biddy_GCFunction)(Biddy_Manager)
Definition: biddy.h:266
void Biddy_InitMNG(Biddy_Manager *mng, int gddtype)
Function Biddy_InitMNG initialize a manager.
Definition: biddyMain.c:178
unsigned int Biddy_Managed_NodeTableDRTime(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableDRTime.
Definition: biddyStat.c:709
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:318
unsigned long long int Biddy_Managed_NodeTableGCObsoleteNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableGCObsoleteNumber.
Definition: biddyStat.c:619
Biddy_Edge Biddy_Managed_Xor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Xor calculates Boolean function XOR.
Biddy_Edge Biddy_Managed_GetTopVariableEdge(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_GetTopVariableEdge returns variable&#39;s edge of top variable.
Definition: biddyMain.c:1942
void Biddy_Managed_PrintfSOP(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_PrintfSOP writes SOP using printf.
Definition: biddyInOut.c:918
Biddy_Edge Biddy_Managed_GetVariableValue(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableValue gets variable&#39;s value.
Definition: biddyMain.c:2083
void Biddy_Managed_ResetVariablesValue(Biddy_Manager MNG)
Function Biddy_Managed_ResetVariablesValue sets all variable&#39;s value to biddyZero.
Definition: biddyMain.c:2027
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:1663
Biddy_Edge Biddy_Managed_RandomSet(Biddy_Manager MNG, Biddy_Edge unit, double r)
Function Biddy_Managed_RandomSet generates a random BDD.
Biddy_String Biddy_Managed_Eval0(Biddy_Manager MNG, Biddy_String s)
Function Biddy_Managed_Eval0 evaluates raw format.
Definition: biddyInOut.c:241
unsigned long long int Biddy_Managed_OPCacheInsert(Biddy_Manager MNG)
Function Biddy_Managed_OPCacheInsert.
Definition: biddyStat.c:1127
void Biddy_Managed_PrintfTable(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_PrintfTable writes truth table using printf.
Definition: biddyInOut.c:788
unsigned long long int Biddy_Managed_NodeTableCompareNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableCompareNumber.
Definition: biddyStat.c:502
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:2223
unsigned int Biddy_Managed_NodeTableXORNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableXORNumber.
Definition: biddyStat.c:853
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.
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:610
Biddy_Edge Biddy_Managed_AddVariableBelow(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_AddVariableBelow adds variable.
Definition: biddyMain.c:2689
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.e. Boolean function f = x) and new element (i.e. it creates set {{x}}).
Definition: biddyMain.c:2318
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:2853
unsigned long long int Biddy_Managed_NodeTableXORRecursiveNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableXORRecursiveNumber.
Definition: biddyStat.c:881
Biddy_Edge Biddy_Managed_Not(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Not calculates Boolean function NOT.
unsigned int Biddy_Managed_NodeTableMax(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableMax returns maximal (peek) number of nodes in node table...
Definition: biddyStat.c:334
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:4185
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:3419
Biddy_Edge Biddy_Managed_AddVariableByName(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_AddVariableByName adds variable.
Definition: biddyMain.c:2622
Biddy_Edge Biddy_Managed_GetElementEdge(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetElementEdge returns element&#39;s edge.
Definition: biddyMain.c:1889
Biddy_Edge Biddy_Managed_RandomFunction(Biddy_Manager MNG, Biddy_Edge support, double r)
Function Biddy_Managed_RandomFunction generates a random BDD.
Definition: biddyOp.c:5976
unsigned int Biddy_Managed_ListUsed(Biddy_Manager MNG)
Function Biddy_Managed_ListUsed.
Definition: biddyStat.c:938
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:5127
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:4739
char Biddy_Boolean
Definition: biddy.h:232
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:1767
unsigned long long int Biddy_Managed_NodeTableFoaNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableFoaNumber.
Definition: biddyStat.c:438
unsigned long long int Biddy_Managed_ReadMemoryInUse(Biddy_Manager MNG)
Function Biddy_Managed_ReadMemoryInUse report memory consumption of main data strucutures (nodes...
Definition: biddyStat.c:1828
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:2997
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:1805
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:1396
unsigned int Biddy_Managed_DependentVariableNumber(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_DependentVariableNumber.
Definition: biddyStat.c:1275
Biddy_Edge Biddy_Managed_Xnor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Xnor calculates Boolean function XNOR.
unsigned int Biddy_Managed_NodeTableITENumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableITENumber.
Definition: biddyStat.c:734
Biddy_Edge Biddy_Managed_And(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_And calculates Boolean function AND (conjunction).
unsigned long long int Biddy_Managed_OPCacheOverwrite(Biddy_Manager MNG)
Function Biddy_Managed_OPCacheOverwrite.
Definition: biddyStat.c:1158
unsigned int Biddy_Managed_NodeTableSwapNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableSwapNumber.
Definition: biddyStat.c:658
unsigned int Biddy_Managed_NodeTableResizeNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableResizeNumber.
Definition: biddyStat.c:412
Biddy_Edge Biddy_Managed_IncTag(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_IncTag returns edge with an incremented tag.
Definition: biddyMain.c:2919
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...
Biddy_Edge Biddy_GetElse(Biddy_Edge fun)
Function Biddy_GetElse returns ELSE successor.
Definition: biddyMain.c:1249
unsigned int Biddy_Managed_CountNodes(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountNodes.
Definition: biddyStat.c:85
Biddy_Boolean Biddy_Managed_DeleteIthFormula(Biddy_Manager MNG, unsigned int i)
Function Biddy_Managed_DeleteIthFormula deletes formula from the table.
Definition: biddyMain.c:4679
Biddy_Edge Biddy_Managed_GetVariableEdge(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableEdge returns variable&#39;s edge.
Definition: biddyMain.c:1864
unsigned int Biddy_Managed_CountNodesPlain(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountNodesPlain.
Definition: biddyStat.c:1191
unsigned int Biddy_Managed_NodeTableSiftingNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableSiftingNumber.
Definition: biddyStat.c:684
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.
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...
unsigned int Biddy_Managed_NodeTableNum(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableNum returns number of all nodes currently in node table...
Definition: biddyStat.c:360
Biddy_Boolean Biddy_Managed_Sifting(Biddy_Manager MNG, Biddy_Edge f, Biddy_Boolean converge)
Function Biddy_Managed_Sifting reorders variables to minimize node number for the whole system (if f ...
Definition: biddyMain.c:4943
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:1998
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:5882
unsigned long long int Biddy_Managed_OPCacheSearch(Biddy_Manager MNG)
Function Biddy_Managed_OPCacheSearch.
Definition: biddyStat.c:1077
unsigned int Biddy_Managed_WriteBddview(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], Biddy_XY *table)
Function Biddy_Managed_WriteBDDView writes bddview format using fprintf.
Definition: biddyInOut.c:1330
unsigned int Biddy_Managed_NodeTableBlockNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableBlockNumber.
Definition: biddyStat.c:283
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:1524
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:386
Biddy_Edge Biddy_Managed_Nand(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Nand calculates Boolean function NAND (Sheffer).
void Biddy_Managed_SetVariableData(Biddy_Manager MNG, Biddy_Variable v, void *x)
Function Biddy_Managed_SetVariableData sets variable&#39;s data.
Definition: biddyMain.c:2143
char * Biddy_String
Definition: biddy.h:235
Biddy_Edge Biddy_Managed_GetConstantOne(Biddy_Manager MNG)
Function Biddy_Managed_GetConstantOne returns constant 1.
Definition: biddyMain.c:1586
void * Biddy_Cache
Definition: biddy.h:249