Biddy  1.7.3
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: 322 $]
17  Date [$Date: 2017-10-01 14:26:58 +0200 (ned, 01 okt 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_IsConstant 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 #if UINTPTR_MAX == 0xffffffffffffffff
157 #define Biddy_IsConstant(f) ((((void**)((uintptr_t) f & 0x0000fffffffffffe))[2] == NULL) && (((void**)((uintptr_t) f & 0x0000fffffffffffe))[3] == NULL))
158 #else
159 #define Biddy_IsConstant(f) ((((void**)((uintptr_t) f & ~((uintptr_t) 1)))[2] == NULL) && (((void**)((uintptr_t) f & ~((uintptr_t) 1)))[3] == NULL))
160 #endif
161 
162 /*! Biddy_IsTaggedConstant returns TRUE iff given edge points to the terminal node and it represents constant 0 or 1, since Biddy v1.7. */
163 /* succesors should be the third and the fourth field in BiddyNode */
164 /* non-terminal nodes should not have null edges as successors */
165 /* this macro assumes 64-bit architecture */
166 /* DO NOT USE THIS FOR RECURSION CONTROL: not all edges to terminal node are recognized */
167 /* use the extended version if there are more than 32768 variables */
168 #define Biddy_IsTaggedConstant(f) (((uintptr_t) f >> 48 == 0) && (((void**)((uintptr_t) f & ~((uintptr_t) 1)))[2] == NULL) && (((void**)((uintptr_t) f & ~((uintptr_t) 1)))[3] == NULL))
169 /* #define Biddy_IsTaggedConstant(f) (((((uintptr_t) f >> 48) & 0x000000000000ffff) == 0) && (((void**)((uintptr_t) f & ~((uintptr_t) 1)))[2] == NULL) && (((void**)((uintptr_t) f & ~((uintptr_t) 1)))[3] == NULL)) */
170 
171 /*! Biddy_IsEqvPointer returns TRUE iff given edges points to the same node. */
172 /* for OBDDs and OFDDs this means that represented functions are equal or inverted */
173 #define Biddy_IsEqvPointer(f,g) (((uintptr_t) f & ~((uintptr_t) 1)) == ((uintptr_t) g & ~((uintptr_t) 1)))
174 
175 /*! Biddy_GetMark returns TRUE iff given edge is complemented. */
176 #define Biddy_GetMark(f) (((uintptr_t) f & (uintptr_t) 1) != 0)
177 
178 /*! Biddy_SetMark makes given edge complemented. */
179 #define Biddy_SetMark(f) (f = (Biddy_Edge) ((uintptr_t) f | (uintptr_t) 1))
180 
181 /*! Biddy_ClearMark makes given edge not-complemented. */
182 #define Biddy_ClearMark(f) (f = (Biddy_Edge) ((uintptr_t) f & ~((uintptr_t) 1)))
183 
184 /*! Biddy_InvertMark changes complement bit of the given edge. */
185 #define Biddy_InvertMark(f) (f = (Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1))
186 
187 /*! Biddy_Inv returns edge with changed complement bit. */
188 /* for OBDD and OFDD this is the same as Biddy_Not */
189 #define Biddy_Inv(f) ((Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1))
190 
191 /*! Biddy_InvCond returns edge with conditinonaly changed complement bit. */
192 #define Biddy_InvCond(f,c) (c ? ((Biddy_Edge) ((uintptr_t) f ^ (uintptr_t) 1)) : f)
193 
194 /*! Biddy_Regular returns not-complemented version of edge, since Biddy v1.4. */
195 #define Biddy_Regular(f) ((Biddy_Edge) ((uintptr_t) f & ~((uintptr_t) 1)))
196 
197 /*! Biddy_Complement returns complemented version of edge, since Biddy v1.4. */
198 #define Biddy_Complement(f) ((Biddy_Edge) ((uintptr_t) f | (uintptr_t) 1))
199 
200 /*! Biddy_GetTag returns tag used for the given edge, since Biddy v1.7. */
201 /* this macro assumes 64-bit architecture */
202 /* use the extended version if there are more than 32768 variables */
203 #define Biddy_GetTag(f) ((Biddy_Variable) ((uintptr_t) f >> 48))
204 /* #define Biddy_GetTag(f) ((Biddy_Variable) (((uintptr_t) f >> 48) & 0x000000000000ffff)) */
205 
206 /*! Biddy_SetTag adds tag to the given edge, since Biddy v1.7. */
207 /* CAREFULLY: you can create an invalid node! */
208 /* this macro assumes 64-bit architecture */
209 #define Biddy_SetTag(f,t) (f = (Biddy_Edge) (((uintptr_t) f & 0x0000ffffffffffff) | ((uintptr_t) t << 48)))
210 
211 /*! Biddy_ClearTag removes tag from the given edge, since Biddy v1.7. */
212 /* this macro assumes 64-bit architecture */
213 #define Biddy_ClearTag(f) (f = (Biddy_Edge) ((uintptr_t) f & 0x0000ffffffffffff))
214 
215 /*----------------------------------------------------------------------------*/
216 /* Type declarations */
217 /*----------------------------------------------------------------------------*/
218 
219 /*! Biddy_Boolean is used for boolean values. */
220 typedef char Biddy_Boolean;
221 
222 /*! Biddy_String is used for strings. */
223 typedef char *Biddy_String;
224 
225 /*! Biddy_Manager is used to specify manager.
226  Manager is a pointer to BiddyManager. A manager includes Node Table,
227  Variable Table, Formulae Table, Ordering Table, three basic caches
228  (ITE Cache, EA Cache and RC Cache), list of user's caches, system
229  age and some other structures needed for memory management.
230  Internal structure of BiddyManager is not exported but
231  must be imitated to create user's managers */
232 typedef void **Biddy_Manager;
233 
234 /*! Biddy_Cache is used to specify user's cache table.
235  Caches for different operations are different and the user is
236  responsible for the correct internal structure. */
237 typedef void *Biddy_Cache;
238 
239 /*! Biddy_Variable is used for indices in variable table. */
240 /* for tagged graphs this should not be larger than 16 bits */
241 typedef unsigned short int Biddy_Variable;
242 
243 /*! Biddy_Edge is a marked edge (i.e. a marked pointer to BiddyNode).
244  Mark is encoded as the value of the last significant bit.
245  For TZBDDs and TZFDDs, edges are tagged. Tag is a 16 bit number
246  (unsigned short int) whish is stored in the highest part of
247  the pointer (this is safe because only 48 bits are used).
248  TZBDDs and TZFDDs are supported only on 64-bits architectures.
249  Internal structure of BiddyNode is not visible to the user. */
250 typedef void* Biddy_Edge;
251 
252 /*! Biddy_GCFunction is used in Biddy_AddCache to specify user's function
253  which will performs garbage collection. */
255 
256 /*! Biddy_LookupFunction is used in Biddy_Eval1x to specify user's function
257  which will lookups in a user's formula table. */
259 
260 /*----------------------------------------------------------------------------*/
261 /* Structure declarations */
262 /*----------------------------------------------------------------------------*/
263 
264 /*! Biddy_XY is used in Biddy_WriteBddview to pass node coordinates */
265 typedef struct {
266  int id;
267  Biddy_String label;
268  int x;
269  int y;
270  Biddy_Boolean isConstant;
271 } Biddy_XY;
272 
273 /*----------------------------------------------------------------------------*/
274 /* Variable declarations */
275 /*----------------------------------------------------------------------------*/
276 
277 #ifdef __cplusplus
278 extern "C" {
279 #endif
280 
281 #ifdef __cplusplus
282 }
283 #endif
284 
285 /*----------------------------------------------------------------------------*/
286 /* Prototypes for functions exported from biddyMain.c */
287 /*----------------------------------------------------------------------------*/
288 
289 #ifdef __cplusplus
290 extern "C" {
291 #endif
292 
293 /* 1 */
294 /*! Macros Biddy_Init and Biddy_InitAnonymous will initialize anonymous manager.*/
295 #define Biddy_Init() Biddy_InitMNG(NULL,BIDDYTYPEOBDDC)
296 #define Biddy_InitAnonymous(gddtype) Biddy_InitMNG(NULL,gddtype)
297 EXTERN void Biddy_InitMNG(Biddy_Manager *mng, int gddtype);
298 
299 /* 2 */
300 /*! Macro Biddy_Exit will delete anonymous manager. */
301 #define Biddy_Exit() Biddy_ExitMNG(NULL)
302 EXTERN void Biddy_ExitMNG(Biddy_Manager *mng);
303 
304 /* 3 */
305 EXTERN Biddy_String Biddy_About();
306 
307 /* 4 */
308 /*! Macro Biddy_GetManagerType is defined for use with anonymous manager. */
309 #define Biddy_GetManagerType() Biddy_Managed_GetManagerType(NULL)
311 
312 /* 5 */
313 /*! Macro Biddy_GetManagerName is defined for use with anonymous manager. */
314 #define Biddy_GetManagerName() Biddy_Managed_GetManagerName(NULL)
316 
317 /* 6 */
318 /*! Macro Biddy_SetManagerParameters is defined for use with anonymous manager. */
319 #define Biddy_SetManagerParameters(gcr,gcrF,gcrX,rr,rrF,rrX,st,fst,cst,fcst) Biddy_Managed_SetManagerParameters(NULL,gcr,gcrF,gcrX,rr,rrF,rrX,st,fst,cst,fcst)
320 EXTERN void Biddy_Managed_SetManagerParameters(Biddy_Manager MNG, float gcr, float gcrF, float gcrX, float rr, float rrF, float rrX, float st, float fst, float cst, float fcst);
321 
322 /* 7 */
323 /*! Macro Biddy_Managed_GetThen is defined for your convenience. */
324 #define Biddy_Managed_GetThen(MNG,f) Biddy_GetThen(f)
326 
327 /* 8 */
328 /*! Macro Biddy_Managed_GetElse is defined for your convenience. */
329 #define Biddy_Managed_GetElse(MNG,f) Biddy_GetElse(f)
331 
332 /* 9 */
333 /*! Macro Biddy_Managed_GetTopVariable is defined for your convenience. */
334 #define Biddy_Managed_GetTopVariable(MNG,f) Biddy_GetTopVariable(f)
336 
337 /* 10 */
338 /*! Macro Biddy_IsEqv is defined for use with anonymous manager. */
339 #define Biddy_IsEqv(f1,MNG2,f2) Biddy_Managed_IsEqv(NULL,f1,MNG2,f2)
341 
342 /* 11 */
343 /*! Macro Biddy_SelectNode is defined for use with anonymous manager. */
344 #define Biddy_SelectNode(f) Biddy_Managed_SelectNode(NULL,f)
346 
347 /* 12 */
348 /*! Macro Biddy_DeselectNode is defined for use with anonymous manager. */
349 #define Biddy_DeselectNode(f) Biddy_Managed_DeselectNode(NULL,f)
351 
352 /* 13 */
353 /*! Macro Biddy_IsSelected is defined for use with anonymous manager. */
354 #define Biddy_IsSelected(f) Biddy_Managed_IsSelected(NULL,f)
356 
357 /* 14 */
358 /*! Macro Biddy_SelectFunction is defined for use with anonymous manager. */
359 #define Biddy_SelectFunction(f) Biddy_Managed_SelectFunction(NULL,f)
361 
362 /* 15 */
363 /*! Macro Biddy_DeselectAll is defined for use with anonymous manager. */
364 #define Biddy_DeselectAll() Biddy_Managed_DeselectAll(NULL)
366 
367 /* 16 */
368 /*! Macro Biddy_GetTerminal is defined for use with anonymous manager. */
369 #define Biddy_GetTerminal() Biddy_Managed_GetTerminal(NULL)
371 
372 /* 17 */
373 /*! Macro Biddy_GetConstantZero is defined for use with anonymous manager. */
374 #define Biddy_GetConstantZero() Biddy_Managed_GetConstantZero(NULL)
376 #define Biddy_Managed_GetEmptySet(MNG) Biddy_Managed_GetConstantZero(MNG)
377 #define Biddy_GetEmptySet() Biddy_Managed_GetConstantZero(NULL)
378 
379 /* 18 */
380 /*! Macro Biddy_GetConstantOne is defined for use with anonymous manager. */
381 #define Biddy_GetConstantOne() Biddy_Managed_GetConstantOne(NULL)
383 #define Biddy_Managed_GetUniversalSet(MNG) Biddy_Managed_GetConstantOne(MNG)
384 #define Biddy_GetUniversalSet() Biddy_Managed_GetConstantOne(NULL)
385 
386 /* 19 */
387 /*! Macro Biddy_GetBaseSet is defined for use with anonymous manager. */
388 #define Biddy_GetBaseSet() Biddy_Managed_GetBaseSet(NULL)
390 
391 /* 20 */
392 /*! Macro Biddy_GetVariable is defined for use with anonymous manager. */
393 #define Biddy_GetVariable(x) Biddy_Managed_GetVariable(NULL,x)
395 
396 /* 21 */
397 /*! Macro Biddy_GetPrevVariable is defined for use with anonymous manager. */
398 #define Biddy_GetPrevVariable(v) Biddy_Managed_GetPrevVariable(NULL,v)
400 
401 /* 22 */
402 /*! Macro Biddy_GetNextVariable is defined for use with anonymous manager. */
403 #define Biddy_GetNextVariable(v) Biddy_Managed_GetNextVariable(NULL,v)
405 
406 /* 23 */
407 /*! Macro Biddy_GetVariableEdge is defined for use with anonymous manager. */
408 #define Biddy_GetVariableEdge(v) Biddy_Managed_GetVariableEdge(NULL,v)
410 
411 /* 24 */
412 /*! Macro Biddy_GetElementEdge is defined for use with anonymous manager. */
413 #define Biddy_GetElementEdge(v) Biddy_Managed_GetElementEdge(NULL,v)
415 
416 /* 25 */
417 /*! Macro Biddy_GetVariableName is defined for use with anonymous manager. */
418 #define Biddy_GetVariableName(v) Biddy_Managed_GetVariableName(NULL,v)
420 
421 /* 26 */
422 /*! Macro Biddy_GetTopVariableEdge is defined for use with anonymous manager. */
423 #define Biddy_GetTopVariableEdge(f) Biddy_Managed_GetTopVariableEdge(NULL,f)
425 
426 /* 27 */
427 /*! Macro Biddy_GetTopVariableName is defined for use with anonymous manager. */
428 #define Biddy_GetTopVariableName(f) Biddy_Managed_GetTopVariableName(NULL,f)
430 
431 /* 28 */
432 /*! Macro Biddy_GetTopVariableChar is defined for use with anonymous manager. */
433 #define Biddy_GetTopVariableChar(f) Biddy_Managed_GetTopVariableChar(NULL,f)
435 
436 /* 29 */
437 /*! Macro Biddy_ResetVariablesValue is defined for use with anonymous manager. */
438 #define Biddy_ResetVariablesValue() Biddy_Managed_ResetVariablesValue(NULL)
440 
441 /* 30 */
442 /*! Macro Biddy_SetVariableValue is defined for use with anonymous manager. */
443 #define Biddy_SetVariableValue(v,f) Biddy_Managed_SetVariableValue(NULL,v,f)
445 
446 /* 31 */
447 /*! Macro Biddy_IsSmaller is defined for use with anonymous manager. */
448 #define Biddy_IsSmaller(fv,gv) Biddy_Managed_IsSmaller(NULL,fv,gv)
450 
451 /* 32 */
452 /*! Macro Biddy_FoaVariable is defined for use with anonymous manager. */
453 #define Biddy_FoaVariable(x,varelem) Biddy_Managed_FoaVariable(NULL,x,varelem)
455 
456 /* 33 */
457 /*! Macro Biddy_ChangeVariableName is defined for use with anonymous manager. */
458 #define Biddy_ChangeVariableName(v,x) Biddy_Managed_ChangeVariableName(NULL,v,x)
460 
461 /* 34 */
462 /*! Macro Biddy_AddVariableByName is defined for use with anonymous manager. */
463 #define Biddy_AddVariableByName(x) Biddy_Managed_AddVariableByName(NULL,x)
465 #define Biddy_Managed_AddVariable(MNG) Biddy_Managed_AddVariableByName(MNG,NULL)
466 #define Biddy_AddVariable() Biddy_Managed_AddVariableByName(NULL,NULL)
467 
468 /* 35 */
469 /*! Macro Biddy_AddElementByName is defined for use with anonymous manager. */
470 #define Biddy_AddElementByName(x) Biddy_Managed_AddElementByName(NULL,x)
472 #define Biddy_Managed_AddElement(MNG) Biddy_Managed_AddElementByName(MNG,NULL)
473 #define Biddy_AddElement() Biddy_Managed_AddElementByName(NULL,NULL)
474 
475 /* 36 */
476 /*! Macro Biddy_AddVariableBelow is defined for use with anonymous manager. */
477 #define Biddy_AddVariableBelow(v) Biddy_Managed_AddVariableBelow(NULL,v)
479 
480 /* 37 */
481 /*! Macro Biddy_AddVariableAbove is defined for use with anonymous manager. */
482 #define Biddy_AddVariableAbove(v) Biddy_Managed_AddVariableAbove(NULL,v)
484 
485 /* 38 */
486 /*! Macro Biddy_TransferMark is defined for use with anonymous manager. */
487 /*! For OBDD, use macro Biddy_InvCond. */
488 #define Biddy_TransferMark(f,mark,leftright) Biddy_Managed_TransferMark(NULL,f,mark,leftright)
490 
491 /* 39 */
492 /*! Macro Biddy_IncTag is defined for use with anonymous manager. */
493 #define Biddy_IncTag(f) Biddy_Managed_IncTag(NULL,f)
495 
496 /* 40 */
497 /*! Macro Biddy_TaggedFoaNode is defined for use with anonymous manager. */
498 #define Biddy_TaggedFoaNode(v,pf,pt,ptag,garbageAllowed) Biddy_Managed_TaggedFoaNode(NULL,v,pf,pt,ptag,garbageAllowed)
500 #define Biddy_Managed_FoaNode(MNG,v,pf,pt,garbageAllowed) Biddy_Managed_TaggedFoaNode(MNG,v,pf,pt,v,garbageAllowed)
501 #define Biddy_FoaNode(v,pf,pt,garbageAllowed) Biddy_Managed_TaggedFoaNode(NULL,v,pf,pt,v,garbageAllowed)
502 
503 /* 41 */
504 /*! Macro Biddy_Not is defined for use with anonymous manager. */
505 /*! For OBDD and OFDD, use macro Biddy_Inv. */
506 #define Biddy_Not(f) Biddy_Managed_Not(NULL,f)
508 
509 /* 42 */
510 /*! Macro Biddy_ITE is defined for use with anonymous manager. */
511 #define Biddy_ITE(f,g,h) Biddy_Managed_ITE(NULL,f,g,h)
513 
514 /* 43 */
515 /*! Macro Biddy_And is defined for use with anonymous manager. */
516 /*! Macros Biddy_Managed_Intersect and Biddy_Intersect are defined for set manipulation. */
517 #define Biddy_And(f,g) Biddy_Managed_And(NULL,f,g)
519 #define Biddy_Managed_Intersect(MNG,f,g) Biddy_Managed_And(MNG,f,g)
520 #define Biddy_Intersect(f,g) Biddy_Managed_And(NULL,f,g)
521 
522 /* 44 */
523 /*! Macro Biddy_Or is defined for use with anonymous manager. */
524 /*! Macros Biddy_Managed_Union and Biddy_Union are defined for set manipulation. */
525 #define Biddy_Or(f,g) Biddy_Managed_Or(NULL,f,g)
527 #define Biddy_Managed_Union(MNG,f,g) Biddy_Managed_Or(MNG,f,g)
528 #define Biddy_Union(f,g) Biddy_Managed_Or(NULL,f,g)
529 
530 /* 45 */
531 /*! Macro Biddy_Nand is defined for use with anonymous manager. */
532 #define Biddy_Nand(f,g) Biddy_Managed_Nand(NULL,f,g)
534 
535 /* 46 */
536 /*! Macro Biddy_Nor is defined for use with anonymous manager. */
537 #define Biddy_Nor(f,g) Biddy_Managed_Nor(NULL,f,g)
539 
540 /* 47 */
541 /*! Macro Biddy_Xor is defined for use with anonymous manager. */
542 #define Biddy_Xor(f,g) Biddy_Managed_Xor(NULL,f,g)
544 
545 /* 48 */
546 /*! Macro Biddy_Xnor is defined for use with anonymous manager. */
547 #define Biddy_Xnor(f,g) Biddy_Managed_Xnor(NULL,f,g)
549 
550 /* 49 */
551 /*! Macro Biddy_Leq is defined for use with anonymous manager. */
552 #define Biddy_Leq(f,g) Biddy_Managed_Leq(NULL,f,g)
554 
555 /* 50 */
556 /*! Macro Biddy_Gt is defined for use with anonymous manager. */
557 #define Biddy_Gt(f,g) Biddy_Managed_Gt(NULL,f,g)
559 #define Biddy_Managed_Diff(MNG,f,g) Biddy_Managed_Gt(MNG,g,f)
560 #define Biddy_Diff(f,g) Biddy_Managed_Gt(NULL,g,f)
561 
562 /* 51 */
563 /*! Macro Biddy_IsLeq is defined for use with anonymous manager. */
564 #define Biddy_IsLeq(f,g) Biddy_Managed_IsLeq(NULL,f,g)
566 
567 /* 52 */
568 /* This is used to calculate cofactors f|{v=0} and f|{v=1}. */
569 /*! Macro Biddy_Restrict is defined for use with anonymous manager. */
570 #define Biddy_Restrict(f,v,value) Biddy_Managed_Restrict(NULL,f,v,value)
572 
573 /* 53 */
574 /*! Macro Biddy_Compose is defined for use with anonymous manager. */
575 #define Biddy_Compose(f,g,v) Biddy_Managed_Compose(NULL,f,g,v)
577 
578 /* 54 */
579 /*! Macro Biddy_E is defined for use with anonymous manager. */
580 #define Biddy_E(f,v) Biddy_Managed_E(NULL,f,v)
582 
583 /* 55 */
584 /*! Macro Biddy_A is defined for use with anonymous manager. */
585 #define Biddy_A(f,v) Biddy_Managed_A(NULL,f,v)
587 
588 /* 56 */
589 /*! Macro Biddy_IsVariableDependent is defined for use with anonymous manager. */
590 #define Biddy_IsVariableDependent(f,v) Biddy_Managed_IsVariableDependent(NULL,f,v)
592 
593 /* 57 */
594 /*! Macro Biddy_ExistAbstract is defined for use with anonymous manager. */
595 #define Biddy_ExistAbstract(f,cube) Biddy_Managed_ExistAbstract(NULL,f,cube)
597 
598 /* 58 */
599 /*! Macro Biddy_UnivAbstract is defined for use with anonymous manager. */
600 #define Biddy_UnivAbstract(f,cube) Biddy_Managed_UnivAbstract(NULL,f,cube)
602 
603 /* 59 */
604 /*! Macro Biddy_AndAbstract is defined for use with anonymous manager. */
605 #define Biddy_AndAbstract(f,g,cube) Biddy_Managed_AndAbstract(NULL,f,g,cube)
607 
608 /* 60 */
609 /*! Macro Biddy_Constrain is defined for use with anonymous manager. */
610 #define Biddy_Constrain(f,c) Biddy_Managed_Constrain(NULL,f,c)
612 
613 /* 61 */
614 /* This is Coudert and Madre's restrict function */
615 /*! Macro Biddy_Simplify is defined for use with anonymous manager. */
616 #define Biddy_Simplify(f,c) Biddy_Managed_Simplify(NULL,f,c)
618 
619 /* 62 */
620 /*! Macro Biddy_Support is defined for use with anonymous manager. */
621 #define Biddy_Support(f) Biddy_Managed_Support(NULL,f)
623 
624 /* 63 */
625 /*! Macro Biddy_ReplaceByKeyword is defined for use with anonymous manager. */
626 /*! Macros Biddy_Managed_Replace and Biddy_Replace are variants */
627 /*! with less effective cache table */
628 #define Biddy_ReplaceByKeyword(f,keyword) Biddy_Managed_ReplaceByKeyword(NULL,f,keyword)
630 #define Biddy_Managed_Replace(MNG,f) Biddy_Managed_ReplaceByKeyword(MNG,f,NULL)
631 #define Biddy_Replace(f) Biddy_Managed_ReplaceByKeyword(NULL,f,NULL)
632 
633 /* 64 */
634 /*! Macro Biddy_Change is defined for use with anonymous manager. */
635 #define Biddy_Change(f,v) Biddy_Managed_Change(NULL,f,v)
637 
638 /* 65 */
639 /* This is used to calculate f*v and f*(-v) */
640 /*! Macro Biddy_Subset is defined for use with anonymous manager. */
641 #define Biddy_Subset(f,v,value) Biddy_Managed_Subset(NULL,f,v,value)
643 #define Biddy_Managed_Subset0(MNG,f,v) Biddy_Managed_Subset(MNG,f,v,FALSE)
644 #define Biddy_Subset0(f,v) Biddy_Managed_Subset(NULL,f,v,FALSE)
645 #define Biddy_Managed_Subset1(MNG,f,v) Biddy_Managed_Subset(MNG,f,v,TRUE)
646 #define Biddy_Subset1(f,v) Biddy_Managed_Subset(NULL,f,v,TRUE)
647 
648 /* 66 */
649 /*! Macro Biddy_IsOK is defined for use with anonymous manager. */
650 #define Biddy_IsOK(f) Biddy_Managed_IsOK(NULL,f)
652 
653 /* 67 */
654 /*! Macro Biddy_GC is defined for use with anonymous manager. */
655 /*! Macros Biddy_Managed_FullGC and Biddy_FullGC are useful variants. */
656 #define Biddy_GC(target,purge,total) Biddy_Managed_GC(NULL,target,purge,total)
657 #define Biddy_Managed_AutoGC(MNG) Biddy_Managed_GC(MNG,0,FALSE,FALSE)
658 #define Biddy_AutoGC() Biddy_Managed_GC(NULL,0,FALSE,FALSE)
659 EXTERN void Biddy_Managed_GC(Biddy_Manager MNG, Biddy_Variable target, Biddy_Boolean purge, Biddy_Boolean total);
660 
661 /* 68 */
662 /*! Macro Biddy_Clean is defined for use with anonymous manager. */
663 #define Biddy_Clean() Biddy_Managed_Clean(NULL)
664 EXTERN void Biddy_Managed_Clean(Biddy_Manager MNG);
665 
666 /* 69 */
667 /*! Macro Biddy_Purge is defined for use with anonymous manager. */
668 #define Biddy_Purge() Biddy_Managed_Purge(NULL)
669 EXTERN void Biddy_Managed_Purge(Biddy_Manager MNG);
670 
671 /* 70 */
672 /*! Macro Biddy_PurgeAndReorder is defined for use with anonymous manager. */
673 #define Biddy_PurgeAndReorder(f,c) Biddy_Managed_PurgeAndReorder(NULL,f,c)
675 
676 /* 71 */
677 /*! Macro Biddy_Refresh is defined for use with anonymous manager. */
678 #define Biddy_Refresh(f) Biddy_Managed_Refresh(NULL,f)
680 
681 /* 72 */
682 /*! Macro Biddy_AddCache is defined for use with anonymous manager. */
683 #define Biddy_AddCache(gc) Biddy_Managed_AddCache(NULL,gc)
685 
686 /* 73 */
687 /*! Macro Biddy_AddFormula is defined for use with anonymous manager. */
688 /*! Macros Biddy_Managed_AddTmpFormula, Biddy_AddTmpFormula, */
689 /*! Biddy_Managed_AddPersistentFormula, and Biddy_AddPersistentFormula */
690 /*! are defined to simplify formulae management. */
691 #define Biddy_AddFormula(x,f,c) Biddy_Managed_AddFormula(NULL,x,f,c)
692 EXTERN unsigned int Biddy_Managed_AddFormula(Biddy_Manager MNG, Biddy_String x, Biddy_Edge f, int c);
693 #define Biddy_Managed_AddTmpFormula(mng,f,c) Biddy_Managed_AddFormula(mng,NULL,f,c)
694 #define Biddy_Managed_AddPersistentFormula(mng,x,f) Biddy_Managed_AddFormula(mng,x,f,0)
695 #define Biddy_AddTmpFormula(f,c) Biddy_Managed_AddFormula(NULL,NULL,f,c)
696 #define Biddy_AddPersistentFormula(x,f) Biddy_Managed_AddFormula(NULL,x,f,0)
697 
698 /* 74 */
699 /*! Macro Biddy_FindFormula is defined for use with anonymous manager. */
700 #define Biddy_FindFormula(x,idx,f) Biddy_Managed_FindFormula(NULL,x,idx,f)
701 EXTERN Biddy_Boolean Biddy_Managed_FindFormula(Biddy_Manager MNG, Biddy_String x, unsigned int *idx, Biddy_Edge *f);
702 
703 /* 75 */
704 /*! Macro Biddy_DeleteFormula is defined for use with anonymous manager. */
705 #define Biddy_DeleteFormula(x) Biddy_Managed_DeleteFormula(NULL,x)
707 
708 /* 76 */
709 /*! Macro Biddy_DeleteIthFormula is defined for use with anonymous manager. */
710 #define Biddy_DeleteIthFormula(x) Biddy_Managed_DeleteIthFormula(NULL,x)
712 
713 /* 77 */
714 /*! Macro Biddy_GetIthFormula is defined for use with anonymous manager. */
715 #define Biddy_GetIthFormula(i) Biddy_Managed_GetIthFormula(NULL,i)
716 EXTERN Biddy_Edge Biddy_Managed_GetIthFormula(Biddy_Manager MNG, unsigned int i);
717 
718 /* 78 */
719 /*! Macro Biddy_GetIthFormulaName is defined for use with anonymous manager. */
720 #define Biddy_GetIthFormulaName(i) Biddy_Managed_GetIthFormulaName(NULL,i)
722 
723 /* 79 */
724 /*! Macro Biddy_SwapWithHigher is defined for use with anonymous manager. */
725 #define Biddy_SwapWithHigher(v) Biddy_Managed_SwapWithHigher(NULL,v)
727 
728 /* 80 */
729 /*! Macro Biddy_SwapWithLower is defined for use with anonymous manager. */
730 #define Biddy_SwapWithLower(v) Biddy_Managed_SwapWithLower(NULL,v)
732 
733 /* 81 */
734 /*! Macro Biddy_Sifting is defined for use with anonymous manager. */
735 #define Biddy_Sifting(f,c) Biddy_Managed_Sifting(NULL,f,c)
737 
738 /* 82 */
739 /*! Macro Biddy_Copy is defined for use with anonymous manager. */
740 #define Biddy_Copy(MNG2,f) Biddy_Managed_Copy(NULL,MNG2,f)
742 
743 /* 83 */
744 /*! Macro Biddy_CopyFormula is defined for use with anonymous manager. */
745 #define Biddy_CopyFormula(MNG2,x) Biddy_Managed_CopyFormula(NULL,MNG2,x)
747 
748 /* 84 */
749 /*! Macro Biddy_Eval is defined for use with anonymous manager. */
750 #define Biddy_Eval(f) Biddy_Managed_Eval(NULL,f)
752 
753 /* 85 */
754 /*! Macro Biddy_Random is defined for use with anonymous manager. */
755 #define Biddy_Random(support,r) Biddy_Managed_Random(NULL,support,r)
756 EXTERN Biddy_Edge Biddy_Managed_Random(Biddy_Manager MNG, Biddy_Edge support, double r);
757 
758 /* 86 */
759 /*! Macro Biddy_RandomSet is defined for use with anonymous manager. */
760 #define Biddy_RandomSet(unit,r) Biddy_Managed_RandomSet(NULL,unit,r)
761 EXTERN Biddy_Edge Biddy_Managed_RandomSet(Biddy_Manager MNG, Biddy_Edge unit, double r);
762 
763 #ifdef __cplusplus
764 }
765 #endif
766 
767 /* TO DO: unique */
768 /* Unique quantification of variables. */
769 /* Similar to existential quantification but uses XOR instead of OR. */
770 
771 /*----------------------------------------------------------------------------*/
772 /* Prototypes for functions exported from biddyStat.c */
773 /*----------------------------------------------------------------------------*/
774 
775 #ifdef __cplusplus
776 extern "C" {
777 #endif
778 
779 /* 87 */
780 /*! Macro Biddy_NodeNumber(f) is defined for use with anonymous manager. */
781 #define Biddy_NodeNumber(f) Biddy_Managed_NodeNumber(NULL,f)
782 EXTERN unsigned int Biddy_Managed_NodeNumber(Biddy_Manager MNG, Biddy_Edge f);
783 
784 /* 88 */
785 /*! Macro Biddy_Managed_NodeMaxLevel(MNG,f) is defined for your convenience. */
786 #define Biddy_Managed_NodeMaxLevel(MNG,f) Biddy_NodeMaxLevel(f)
787 EXTERN unsigned int Biddy_NodeMaxLevel(Biddy_Edge f);
788 
789 /* 89 */
790 /*! Macro Biddy_Managed_NodeAvgLevel(MNG,f) is defined for your convenience. */
791 #define Biddy_Managed_NodeAvgLevel(MNG,f) Biddy_NodeAvgLevel(f)
792 EXTERN float Biddy_NodeAvgLevel(Biddy_Edge f);
793 
794 /* 90 */
795 /*! Macro Biddy_VariableTableNum is defined for use with anonymous manager. */
796 #define Biddy_VariableTableNum() Biddy_Managed_VariableTableNum(NULL)
798 
799 /* 91 */
800 /*! Macro Biddy_NodeTableSize is defined for use with anonymous manager. */
801 #define Biddy_NodeTableSize() Biddy_Managed_NodeTableSize(NULL)
802 EXTERN unsigned int Biddy_Managed_NodeTableSize(Biddy_Manager MNG);
803 
804 /* 92 */
805 /*! Macro Biddy_NodeTableBlockNumber is defined for use with anonymous manager. */
806 #define Biddy_NodeTableBlockNumber() Biddy_Managed_NodeTableBlockNumber(NULL)
807 EXTERN unsigned int Biddy_Managed_NodeTableBlockNumber(Biddy_Manager MNG);
808 
809 /* 93 */
810 /*! Macro Biddy_NodeTableGenerated is defined for use with anonymous manager. */
811 #define Biddy_NodeTableGenerated() Biddy_Managed_NodeTableGenerated(NULL)
812 EXTERN unsigned int Biddy_Managed_NodeTableGenerated(Biddy_Manager MNG);
813 
814 /* 94 */
815 /*! Macro Biddy_NodeTableMax is defined for use with anonymous manager. */
816 #define Biddy_NodeTableMax() Biddy_Managed_NodeTableMax(NULL)
817 EXTERN unsigned int Biddy_Managed_NodeTableMax(Biddy_Manager MNG);
818 
819 /* 95 */
820 /*! Macro Biddy_NodeTableNum is defined for use with anonymous manager. */
821 #define Biddy_NodeTableNum() Biddy_Managed_NodeTableNum(NULL)
822 EXTERN unsigned int Biddy_Managed_NodeTableNum(Biddy_Manager MNG);
823 
824 /* 96 */
825 /*! Macro Biddy_NodeTableNumVar is defined for use with anonymous manager. */
826 #define Biddy_NodeTableNumVar(v) Biddy_Managed_NodeTableNumVar(NULL,v)
828 
829 /* 97 */
830 /*! Macro Biddy_NodeTableResizeNumber is defined for use with anonymous manager. */
831 #define Biddy_NodeTableResizeNumber() Biddy_Managed_NodeTableResizeNumber(NULL)
832 EXTERN unsigned int Biddy_Managed_NodeTableResizeNumber(Biddy_Manager MNG);
833 
834 /* 98 */
835 /*! Macro Biddy_NodeTableFoaNumber is defined for use with anonymous manager. */
836 #define Biddy_NodeTableFoaNumber() Biddy_Managed_NodeTableFoaNumber(NULL)
837 EXTERN unsigned long long int Biddy_Managed_NodeTableFoaNumber(Biddy_Manager MNG);
838 
839 /* 99 */
840 /*! Macro Biddy_NodeTableFindNumber is defined for use with anonymous manager. */
841 #define Biddy_NodeTableFindNumber() Biddy_Managed_NodeTableFindNumber(NULL)
842 EXTERN unsigned long long int Biddy_Managed_NodeTableFindNumber(Biddy_Manager MNG);
843 
844 /* 100 */
845 /*! Macro Biddy_NodeTableCompareNumber is defined for use with anonymous manager. */
846 #define Biddy_NodeTableCompareNumber() Biddy_Managed_NodeTableCompareNumber(NULL)
847 EXTERN unsigned long long int Biddy_Managed_NodeTableCompareNumber(Biddy_Manager MNG);
848 
849 /* 101 */
850 /*! Macro Biddy_NodeTableAddNumber is defined for use with anonymous manager. */
851 #define Biddy_NodeTableAddNumber() Biddy_Managed_NodeTableAddNumber(NULL)
852 EXTERN unsigned long long int Biddy_Managed_NodeTableAddNumber(Biddy_Manager MNG);
853 
854 /* 102 */
855 /*! Macro Biddy_NodeTableGCNumber is defined for use with anonymous manager. */
856 #define Biddy_NodeTableGCNumber() Biddy_Managed_NodeTableGCNumber(NULL)
857 EXTERN unsigned int Biddy_Managed_NodeTableGCNumber(Biddy_Manager MNG);
858 
859 /* 103 */
860 /*! Macro Biddy_NodeTableGCTime is defined for use with anonymous manager. */
861 #define Biddy_NodeTableGCTime() Biddy_Managed_NodeTableGCTime(NULL)
862 EXTERN clock_t Biddy_Managed_NodeTableGCTime(Biddy_Manager MNG);
863 
864 /* 104 */
865 /*! Macro Biddy_NodeTableGCObsoleteNumber is defined for use with anonymous manager. */
866 #define Biddy_NodeTableGCObsoleteNumber() Biddy_Managed_NodeTableGCObsoleteNumber(NULL)
867 EXTERN unsigned long long int Biddy_Managed_NodeTableGCObsoleteNumber(Biddy_Manager MNG);
868 
869 /* 105 */
870 /*! Macro Biddy_NodeTableSwapNumber is defined for use with anonymous manager. */
871 #define Biddy_NodeTableSwapNumber() Biddy_Managed_NodeTableSwapNumber(NULL)
872 EXTERN unsigned int Biddy_Managed_NodeTableSwapNumber(Biddy_Manager MNG);
873 
874 /* 106 */
875 /*! Macro Biddy_NodeTableSiftingNumber is defined for use with anonymous manager. */
876 #define Biddy_NodeTableSiftingNumber() Biddy_Managed_NodeTableSiftingNumber(NULL)
877 EXTERN unsigned int Biddy_Managed_NodeTableSiftingNumber(Biddy_Manager MNG);
878 
879 /* 107 */
880 /*! Macro Biddy_NodeTableDRTime is defined for use with anonymous manager. */
881 #define Biddy_NodeTableDRTime() Biddy_Managed_NodeTableDRTime(NULL)
882 EXTERN clock_t Biddy_Managed_NodeTableDRTime(Biddy_Manager MNG);
883 
884 /* 108 */
885 /*! Macro Biddy_NodeTableITENumber is defined for use with anonymous manager. */
886 #define Biddy_NodeTableITENumber() Biddy_Managed_NodeTableITENumber(NULL)
887 EXTERN unsigned int Biddy_Managed_NodeTableITENumber(Biddy_Manager MNG);
888 
889 /* 109 */
890 /*! Macro Biddy_NodeTableITERecursiveNumber is defined for use with anonymous manager. */
891 #define Biddy_NodeTableITERecursiveNumber() Biddy_Managed_NodeTableITERecursiveNumber(NULL)
892 EXTERN unsigned long long int Biddy_Managed_NodeTableITERecursiveNumber(Biddy_Manager MNG);
893 
894 /* 110 */
895 /*! Macro Biddy_NodeTableANDORNumber is defined for use with anonymous manager. */
896 #define Biddy_NodeTableANDORNumber() Biddy_Managed_NodeTableANDORNumber(NULL)
897 EXTERN unsigned int Biddy_Managed_NodeTableANDORNumber(Biddy_Manager MNG);
898 
899 /* 111 */
900 /*! Macro Biddy_NodeTableANDORRecursiveNumber is defined for use with anonymous manager. */
901 #define Biddy_NodeTableANDORRecursiveNumber() Biddy_Managed_NodeTableANDORRecursiveNumber(NULL)
902 EXTERN unsigned long long int Biddy_Managed_NodeTableANDORRecursiveNumber(Biddy_Manager MNG);
903 
904 /* 112 */
905 /*! Macro Biddy_NodeTableXORNumber is defined for use with anonymous manager. */
906 #define Biddy_NodeTableXORNumber() Biddy_Managed_NodeTableXORNumber(NULL)
907 EXTERN unsigned int Biddy_Managed_NodeTableXORNumber(Biddy_Manager MNG);
908 
909 /* 113 */
910 /*! Macro Biddy_NodeTableXORRecursiveNumber is defined for use with anonymous manager. */
911 #define Biddy_NodeTableXORRecursiveNumber() Biddy_Managed_NodeTableXORRecursiveNumber(NULL)
912 EXTERN unsigned long long int Biddy_Managed_NodeTableXORRecursiveNumber(Biddy_Manager MNG);
913 
914 /* 114 */
915 /*! Macro Biddy_FormulaTableNum is defined for use with anonymous manager. */
916 #define Biddy_FormulaTableNum() Biddy_Managed_FormulaTableNum(NULL)
917 EXTERN unsigned int Biddy_Managed_FormulaTableNum(Biddy_Manager MNG);
918 
919 /* 115 */
920 /*! Macro Biddy_ListUsed is defined for use with anonymous manager. */
921 #define Biddy_ListUsed() Biddy_Managed_ListUsed(NULL)
922 EXTERN unsigned int Biddy_Managed_ListUsed(Biddy_Manager MNG);
923 
924 /* 116 */
925 /*! Macro Biddy_ListMaxLength is defined for use with anonymous manager. */
926 #define Biddy_ListMaxLength() Biddy_Managed_ListMaxLength(NULL)
927 EXTERN unsigned int Biddy_Managed_ListMaxLength(Biddy_Manager MNG);
928 
929 /* 117 */
930 /*! Macro Biddy_ListAvgLength is defined for use with anonymous manager. */
931 #define Biddy_ListAvgLength() Biddy_Managed_ListAvgLength(NULL)
933 
934 /* 118 */
935 /*! Macro Biddy_OPCacheSearch is defined for use with anonymous manager. */
936 #define Biddy_OPCacheSearch() Biddy_Managed_OPCacheSearch(NULL)
937 EXTERN unsigned long long int Biddy_Managed_OPCacheSearch(Biddy_Manager MNG);
938 
939 /* 119 */
940 /*! Macro Biddy_OPCacheFind is defined for use with anonymous manager. */
941 #define Biddy_OPCacheFind() Biddy_Managed_OPCacheFind(NULL)
942 EXTERN unsigned long long int Biddy_Managed_OPCacheFind(Biddy_Manager MNG);
943 
944 /* 120 */
945 /*! Macro Biddy_OPCacheInsert is defined for use with anonymous manager. */
946 #define Biddy_OPCacheInsert() Biddy_Managed_OPCacheInsert(NULL)
947 EXTERN unsigned long long int Biddy_Managed_OPCacheInsert(Biddy_Manager MNG);
948 
949 /* 121 */
950 /*! Macro Biddy_OPCacheOverwrite is defined for use with anonymous manager. */
951 #define Biddy_OPCacheOverwrite() Biddy_Managed_OPCacheOverwrite(NULL)
952 EXTERN unsigned long long int Biddy_Managed_OPCacheOverwrite(Biddy_Manager MNG);
953 
954 /* 122 */
955 /*! Macro Biddy_NodeNumberPlain is defined for use with anonymous manager. */
956 #define Biddy_NodeNumberPlain(f) Biddy_Managed_NodeNumberPlain(NULL,f)
957 EXTERN unsigned int Biddy_Managed_NodeNumberPlain(Biddy_Manager MNG, Biddy_Edge f);
958 
959 /* 123 */
960 /*! Macro Biddy_DependentVariableNumber is defined for use with anonymous manager. */
961 #define Biddy_DependentVariableNumber(f) Biddy_Managed_DependentVariableNumber(NULL,f)
963 
964 /* 124 */
965 /*! Macro Biddy_NodeVarNumber is defined for use with anonymous manager. */
966 #define Biddy_NodeVarNumber(f,n,v) Biddy_Managed_NodeVarNumber(NULL,f,n,v)
967 EXTERN void Biddy_Managed_NodeVarNumber(Biddy_Manager MNG, Biddy_Edge f, unsigned int *n, unsigned int *v);
968 
969 
970 /* 125 */
971 /*! Macro Biddy_CountComplemented is defined for use with anonymous manager. */
972 #define Biddy_CountComplemented(f) Biddy_Managed_CountComplemented(NULL,f)
973 EXTERN unsigned int Biddy_Managed_CountComplemented(Biddy_Manager MNG, Biddy_Edge f);
974 
975 /* 126 */
976 /*! Macro Biddy_CountPaths is defined for use with anonymous manager. */
977 #define Biddy_CountPaths(f) Biddy_Managed_CountPaths(NULL,f)
978 EXTERN unsigned long long int Biddy_Managed_CountPaths(Biddy_Manager MNG, Biddy_Edge f);
979 
980 /* 127 */
981 /*! Macro Biddy_CountMinterm is defined for use with anonymous manager. */
982 #define Biddy_CountMinterm(f,nvars) Biddy_Managed_CountMinterm(NULL,f,nvars)
983 EXTERN double Biddy_Managed_CountMinterm(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars);
984 #define Biddy_Managed_CountCombination(MNG,f,nvars) Biddy_Managed_CountMinterm(MNG,f,nvars)
985 #define Biddy_CountCombination(f) Biddy_Managed_CountMinterm(NULL,f,nvars)
986 
987 /* 128 */
988 /*! Macro Biddy_DensityFunction is defined for use with anonymous manager. */
989 #define Biddy_DensityFunction(f,nvars) Biddy_Managed_DensityFunction(NULL,f,nvars)
990 EXTERN double Biddy_Managed_DensityFunction(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars);
991 
992 /* 129 */
993 /*! Macro Biddy_DensityBDD is defined for use with anonymous manager. */
994 #define Biddy_DensityBDD(f,nvars) Biddy_Managed_DensityBDD(NULL,f,nvars)
995 EXTERN double Biddy_Managed_DensityBDD(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars);
996 
997 /* 130 */
998 /*! Macro Biddy_ReadMemoryInUse is defined for use with anonymous manager. */
999 #define Biddy_ReadMemoryInUse() Biddy_Managed_ReadMemoryInUse(NULL)
1000 EXTERN unsigned long long int Biddy_Managed_ReadMemoryInUse(Biddy_Manager MNG);
1001 
1002 /* 131 */
1003 /*! Macro Biddy_PrintInfo is defined for use with anonymous manager. */
1004 #define Biddy_PrintInfo(f) Biddy_Managed_PrintInfo(NULL,f)
1005 EXTERN void Biddy_Managed_PrintInfo(Biddy_Manager MNG, FILE *f);
1006 
1007 #ifdef __cplusplus
1008 }
1009 #endif
1010 
1011 /*----------------------------------------------------------------------------*/
1012 /* Prototypes for functions exported from biddyInOut.c */
1013 /*----------------------------------------------------------------------------*/
1014 
1015 #ifdef __cplusplus
1016 extern "C" {
1017 #endif
1018 
1019 /* 132 */
1020 /*! Macro Biddy_Eval0 is defined for use with anonymous manager. */
1021 #define Biddy_Eval0(s) Biddy_Managed_Eval0(NULL,s)
1023 
1024 /* 133 */
1025 /*! Macro Biddy_Eval1x is defined for use with anonymous manager. */
1026 #define Biddy_Eval1x(s,lf) Biddy_Managed_Eval1x(NULL,s,lf)
1028 #define Biddy_Managed_Eval1(MNG,s) Biddy_Managed_Eval1x(MNG,s,NULL)
1029 #define Biddy_Eval1(s) Biddy_Managed_Eval1x(NULL,s,NULL)
1030 
1031 /* 134 */
1032 /*! Macro Biddy_Eval2 is defined for use with anonymous manager. */
1033 #define Biddy_Eval2(boolFunc) Biddy_Managed_Eval2(NULL,boolFunc)
1035 
1036 /* 135 */
1037 /*! Macro Biddy_ReadVerilogFile is defined for use with anonymous manager. */
1038 #define Biddy_ReadVerilogFile(filename,prefix) Biddy_Managed_ReadVerilogFile(NULL,filename,prefix)
1039 EXTERN void Biddy_Managed_ReadVerilogFile(Biddy_Manager MNG, const char filename[], Biddy_String prefix);
1040 
1041 /* 136 */
1042 /*! Macro Biddy_PrintfBDD is defined for use with anonymous manager. */
1043 #define Biddy_PrintfBDD(f) Biddy_Managed_PrintfBDD(NULL,f)
1045 
1046 /* 137 */
1047 /*! Macro Biddy_WriteBDD is defined for use with anonymous manager. */
1048 #define Biddy_WriteBDD(filename,f,label) Biddy_Managed_WriteBDD(NULL,filename,f,label)
1049 EXTERN void Biddy_Managed_WriteBDD(Biddy_Manager MNG, const char filename[], Biddy_Edge f, Biddy_String label);
1050 
1051 /* 138 */
1052 /*! Macro Biddy_PrintfTable is defined for use with anonymous manager. */
1053 #define Biddy_PrintfTable(f) Biddy_Managed_PrintfTable(NULL,f)
1055 
1056 /* 139 */
1057 /*! Macro Biddy_WriteTable is defined for use with anonymous manager. */
1058 #define Biddy_WriteTable(filename,f) Biddy_Managed_WriteTable(NULL,filename,f)
1059 EXTERN void Biddy_Managed_WriteTable(Biddy_Manager MNG, const char filename[], Biddy_Edge f);
1060 
1061 /* 140 */
1062 /*! Macro Biddy_PrintfSOP is defined for use with anonymous manager. */
1063 #define Biddy_PrintfSOP(f) Biddy_Managed_PrintfSOP(NULL,f)
1065 
1066 /* 141 */
1067 /*! Macro Biddy_WriteSOP is defined for use with anonymous manager. */
1068 #define Biddy_WriteSOP(filename,f) Biddy_Managed_WriteSOP(NULL,filename,f)
1069 EXTERN void Biddy_Managed_WriteSOP(Biddy_Manager MNG, const char filename[], Biddy_Edge f);
1070 
1071 /* 142 */
1072 /*! Macro Biddy_WriteDot is defined for use with anonymous manager. */
1073 #define Biddy_WriteDot(filename,f,label,id,cudd) Biddy_Managed_WriteDot(NULL,filename,f,label,id,cudd);
1074 EXTERN unsigned int Biddy_Managed_WriteDot(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], int id, Biddy_Boolean cudd);
1075 
1076 /* 143 */
1077 /*! Macro Biddy_WriteBddview is defined for use with anonymous manager. */
1078 #define Biddy_WriteBddview(filename,f,label,table) Biddy_Managed_WriteBddview(NULL,filename,f,label,table);
1079 EXTERN unsigned int Biddy_Managed_WriteBddview(Biddy_Manager MNG, const char filename[], Biddy_Edge f, const char label[], Biddy_XY *table);
1080 
1081 #ifdef __cplusplus
1082 }
1083 #endif
1084 
1085 /* TO DO: CNF + DIMACS BENCHMARKS */
1086 /* http://people.sc.fsu.edu/~jburkardt/data/cnf/cnf.html */
1087 /* http://www.dwheeler.com/essays/minisat-user-guide.html */
1088 /* http://www.miroslav-velev.com/sat_benchmarks.html */
1089 /* http://www.satcompetition.org/ */
1090 
1091 #endif /* _BIDDY */
Biddy_Variable Biddy_Managed_SwapWithLower(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_SwapWithLower swaps two adjacent variables.
Definition: biddyMain.c:5817
unsigned long long int Biddy_Managed_OPCacheFind(Biddy_Manager MNG)
Function Biddy_Managed_OPCacheFind.
Definition: biddyStat.c:1097
int Biddy_Managed_GetManagerType(Biddy_Manager MNG)
Function Biddy_Managed_GetManagerType reports BDD type used in the manager.
Definition: biddyMain.c:938
Biddy_String Biddy_Managed_GetTopVariableName(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_GetTopVariableName returns the name of top variable.
Definition: biddyMain.c:1649
Biddy_Edge Biddy_Managed_And(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_And calculates Boolean function AND (conjunction).
Definition: biddyMain.c:2729
void Biddy_Managed_DeselectAll(Biddy_Manager MNG)
Function Biddy_Managed_DeselectAll deselects all nodes.
Definition: biddyMain.c:1285
Biddy_Edge Biddy_Managed_Eval2(Biddy_Manager MNG, Biddy_String boolFunc)
Function Biddy_Managed_Eval2 evaluates infix &|^~>< format.
Definition: biddyInOut.c:417
void Biddy_Managed_NodeVarNumber(Biddy_Manager MNG, Biddy_Edge f, unsigned int *n, unsigned int *v)
Function Biddy_Managed_NodeVarNumber.
Definition: biddyStat.c:1361
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: biddyMain.c:3722
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:1228
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:1509
Biddy_Boolean(* Biddy_LookupFunction)(Biddy_String, Biddy_Edge *)
Definition: biddy.h:258
void * Biddy_Edge
Definition: biddy.h:250
unsigned int Biddy_Managed_NodeTableGCNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableGCNumber.
Definition: biddyStat.c:560
unsigned long long int Biddy_Managed_NodeTableANDORRecursiveNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableANDORRecursiveNumber.
Definition: biddyStat.c:817
Biddy_Variable Biddy_Managed_GetVariable(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_GetVariable returns variable with the given name.
Definition: biddyMain.c:1440
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:1735
Biddy_Edge Biddy_Managed_AddVariableAbove(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_AddVariableAbove adds a numbered variable.
Definition: biddyMain.c:2056
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: biddyMain.c:3629
Biddy_Edge Biddy_Managed_Simplify(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge c)
Function Biddy_Managed_Simplify calculates Coudert and Madre&#39;s restrict function. ...
Definition: biddyMain.c:4315
unsigned int Biddy_Managed_NodeNumberPlain(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_NodeNumberPlain.
Definition: biddyStat.c:1185
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
Biddy_Edge Biddy_Managed_Random(Biddy_Manager MNG, Biddy_Edge support, double r)
Function Biddy_Managed_Random generates a random BDD.
Definition: biddyMain.c:6949
Biddy_Edge Biddy_Managed_GetBaseSet(Biddy_Manager MNG)
Function Biddy_Managed_GetBaseSet returns set containing only a null combination, i...
Definition: biddyMain.c:1405
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:5138
Biddy_Variable Biddy_Managed_VariableTableNum(Biddy_Manager MNG)
Function Biddy_Managed_VariableTableNum returns number of used variables.
Definition: biddyStat.c:223
Biddy_Edge Biddy_Managed_Support(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Support calculates a product of all dependent variables.
Definition: biddyMain.c:4408
Biddy_Edge Biddy_Managed_RandomSet(Biddy_Manager MNG, Biddy_Edge unit, double r)
Function Biddy_Managed_RandomSet generates a random BDD.
Definition: biddyMain.c:7061
clock_t Biddy_Managed_NodeTableDRTime(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableDRTime.
Definition: biddyStat.c:704
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:1515
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_Xnor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Xnor calculates Boolean function XNOR.
Definition: biddyMain.c:3322
clock_t Biddy_Managed_NodeTableGCTime(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableGCTime.
Definition: biddyStat.c:585
void Biddy_Managed_GC(Biddy_Manager MNG, Biddy_Variable target, Biddy_Boolean purge, Biddy_Boolean total)
Function Biddy_Managed_GC performs garbage collection.
Definition: biddyMain.c:4761
Biddy_Edge Biddy_GetThen(Biddy_Edge fun)
Function Biddy_GetThen returns THEN successor.
Definition: biddyMain.c:1018
Biddy_Boolean Biddy_Managed_FindFormula(Biddy_Manager MNG, Biddy_String x, Biddy_Edge *f)
Function Biddy_Managed_FindFormula find formula in Formula table.
Definition: biddyMain.c:5483
Biddy_Boolean Biddy_Managed_DeleteFormula(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_DeleteFormula delete formula from Formula table.
Definition: biddyMain.c:5584
unsigned long long int Biddy_Managed_NodeTableAddNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableAddNumber.
Definition: biddyStat.c:529
Biddy_Variable Biddy_GetTopVariable(Biddy_Edge fun)
Function Biddy_GetTopVariable returns the top variable.
Definition: biddyMain.c:1090
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. DescriptionThe functi...
Definition: biddyMain.c:6797
Biddy_String Biddy_About()
Function Biddy_About reports version of Biddy package.
Definition: biddyMain.c:916
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:1957
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:1761
Biddy_Variable Biddy_Managed_SwapWithHigher(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_SwapWithHigher swaps two adjacent variables.
Definition: biddyMain.c:5779
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:1114
double Biddy_Managed_DensityBDD(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
Function Biddy_Managed_DensityBDD calculates the ratio of the number of on-set minterms to the number...
Definition: biddyStat.c:1788
Biddy_Edge Biddy_Managed_Constrain(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge c)
Function Biddy_Managed_Constrain calculates Coudert and Madre&#39;s constrain function.
Definition: biddyMain.c:4222
float Biddy_NodeAvgLevel(Biddy_Edge f)
Function Biddy_NodeAvgLevel.
Definition: biddyStat.c:191
unsigned int Biddy_NodeMaxLevel(Biddy_Edge f)
Function Biddy_NodeMaxLevel.
Definition: biddyStat.c:163
void Biddy_ExitMNG(Biddy_Manager *mng)
Function Biddy_ExitMNG deletes a manager.
Definition: biddyMain.c:715
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: biddyMain.c:3872
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:5229
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: biddyMain.c:3418
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:5738
void Biddy_Managed_Clean(Biddy_Manager MNG)
Function Biddy_Managed_Clean performs cleaning.
Definition: biddyMain.c:5104
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: biddyMain.c:3467
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:5174
unsigned int Biddy_Managed_FormulaTableNum(Biddy_Manager MNG)
Function Biddy_Managed_FormulaTableNum returns number of known formulae.
Definition: biddyStat.c:908
unsigned int Biddy_Managed_NodeTableANDORNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableANDORNumber.
Definition: biddyStat.c:789
void ** Biddy_Manager
Definition: biddy.h:232
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:1149
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:6911
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:6872
unsigned long long int Biddy_Managed_NodeTableITERecursiveNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableITERecursiveNumber.
Definition: biddyStat.c:757
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: biddyMain.c:3903
Biddy_Edge Biddy_Managed_Leq(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Leq calculates Boolean implication.
Definition: biddyMain.c:3369
Biddy_Edge Biddy_Managed_Or(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Or calculates Boolean function OR (disjunction).
Definition: biddyMain.c:2945
void Biddy_Managed_Refresh(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Refresh refreshes top node in a given function.
Definition: biddyMain.c:5203
unsigned int Biddy_Managed_NodeTableSize(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableSize returns the size of node table.
Definition: biddyStat.c:248
Biddy_Edge Biddy_Managed_GetConstantZero(Biddy_Manager MNG)
Function Biddy_Managed_GetConstantZero returns constant 0.
Definition: biddyMain.c:1349
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: biddyMain.c:4546
float Biddy_Managed_ListAvgLength(Biddy_Manager MNG)
Function Biddy_Managed_ListAvgLength.
Definition: biddyStat.c:1030
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:1593
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:1175
unsigned int Biddy_Managed_NodeTableGenerated(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableGenerated.
Definition: biddyStat.c:303
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: biddyMain.c:4008
unsigned long long int Biddy_Managed_NodeTableFindNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableFindNumber.
Definition: biddyStat.c:465
void Biddy_Managed_PrintInfo(Biddy_Manager MNG, FILE *f)
Function Biddy_Managed_PrintInfo prepare a file with stats.
Definition: biddyStat.c:1935
Biddy_String Biddy_Managed_GetManagerName(Biddy_Manager MNG)
Function Biddy_Managed_GetManagerName reports the name of the BDD type used in the manager...
unsigned int Biddy_Managed_ListMaxLength(Biddy_Manager MNG)
Function Biddy_Managed_ListMaxLength.
Definition: biddyStat.c:966
unsigned short int Biddy_Variable
Definition: biddy.h:241
Biddy_Edge Biddy_Managed_Nor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Nor calculates Boolean function NOR (Peirce).
Definition: biddyMain.c:3048
void(* Biddy_GCFunction)(Biddy_Manager)
Definition: biddy.h:254
unsigned int Biddy_Managed_NodeNumber(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_NodeNumber.
Definition: biddyStat.c:85
void Biddy_InitMNG(Biddy_Manager *mng, int gddtype)
Function Biddy_InitMNG initialize a manager.
Definition: biddyMain.c:210
Biddy_Edge Biddy_Managed_Nand(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Nand calculates Boolean function NAND (Sheffer).
Definition: biddyMain.c:3000
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:614
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...
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:1621
void Biddy_Managed_PrintfSOP(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_PrintfSOP writes SOP using printf.
Definition: biddyInOut.c:918
void Biddy_Managed_ResetVariablesValue(Biddy_Manager MNG)
Function Biddy_Managed_ResetVariablesValue sets all variable&#39;s value to biddyZero.
Definition: biddyMain.c:1706
unsigned int Biddy_Managed_CountComplemented(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_CountComplemented count the number of complemented edges.
Definition: biddyStat.c:1446
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:1122
Biddy_Edge Biddy_Managed_Not(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_Not calculates Boolean function NOT.
Definition: biddyMain.c:2401
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:497
unsigned int Biddy_Managed_NodeTableXORNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableXORNumber.
Definition: biddyStat.c:848
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
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.
Biddy_Edge Biddy_Managed_AddVariableBelow(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_AddVariableBelow adds a numbered variable.
Definition: biddyMain.c:1989
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:1806
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:2119
unsigned long long int Biddy_Managed_NodeTableXORRecursiveNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableXORRecursiveNumber.
Definition: biddyStat.c:876
unsigned int Biddy_Managed_NodeTableMax(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableMax returns maximal (peek) number of nodes in node table...
Definition: biddyStat.c:329
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:5290
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:4721
Biddy_Edge Biddy_Managed_AddVariableByName(Biddy_Manager MNG, Biddy_String x)
Function Biddy_Managed_AddVariableByName adds variable.
Definition: biddyMain.c:1922
Biddy_Edge Biddy_Managed_GetElementEdge(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetElementEdge returns element&#39;s edge.
Definition: biddyMain.c:1569
unsigned int Biddy_Managed_ListUsed(Biddy_Manager MNG)
Function Biddy_Managed_ListUsed.
Definition: biddyStat.c:933
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:5707
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: biddyMain.c:3538
char Biddy_Boolean
Definition: biddy.h:220
unsigned long long int Biddy_Managed_NodeTableFoaNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableFoaNumber.
Definition: biddyStat.c:433
Biddy_Edge Biddy_Managed_Subset(Biddy_Manager MNG, Biddy_Edge f, Biddy_Variable v, Biddy_Boolean value)
Function Biddy_Managed_Subset calculates a division of Boolean function with a literal.
Definition: biddyMain.c:4615
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:1849
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:2185
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:1485
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:1201
unsigned int Biddy_Managed_DependentVariableNumber(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_DependentVariableNumber.
Definition: biddyStat.c:1250
double Biddy_Managed_CountMinterm(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
Function Biddy_Managed_CountMinterm.
Definition: biddyStat.c:1576
unsigned int Biddy_Managed_NodeTableITENumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableITENumber.
Definition: biddyStat.c:729
double Biddy_Managed_DensityFunction(Biddy_Manager MNG, Biddy_Edge f, unsigned int nvars)
Function Biddy_Managed_DensityFunction calculates the ratio of the number of on-set minterms to the n...
Definition: biddyStat.c:1719
unsigned long long int Biddy_Managed_OPCacheOverwrite(Biddy_Manager MNG)
Function Biddy_Managed_OPCacheOverwrite.
Definition: biddyStat.c:1153
unsigned int Biddy_Managed_NodeTableSwapNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableSwapNumber.
Definition: biddyStat.c:653
unsigned int Biddy_Managed_NodeTableResizeNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableResizeNumber.
Definition: biddyStat.c:407
Biddy_Edge Biddy_Managed_IncTag(Biddy_Manager MNG, Biddy_Edge f)
Function Biddy_Managed_IncTag returns edge with an incremented tag.
Definition: biddyMain.c:2147
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: biddyMain.c:3815
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: biddyMain.c:2435
Biddy_Edge Biddy_GetElse(Biddy_Edge fun)
Function Biddy_GetElse returns ELSE successor.
Definition: biddyMain.c:1054
Biddy_Boolean Biddy_Managed_DeleteIthFormula(Biddy_Manager MNG, unsigned int i)
Function Biddy_Managed_DeleteIthFormula deletes formula from the table.
Definition: biddyMain.c:5647
Biddy_Edge Biddy_Managed_GetVariableEdge(Biddy_Manager MNG, Biddy_Variable v)
Function Biddy_Managed_GetVariableEdge returns variable&#39;s edge.
Definition: biddyMain.c:1544
unsigned int Biddy_Managed_NodeTableSiftingNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableSiftingNumber.
Definition: biddyStat.c:679
Biddy_Edge Biddy_Managed_Xor(Biddy_Manager MNG, Biddy_Edge f, Biddy_Edge g)
Function Biddy_Managed_Xor calculates Boolean function XOR.
Definition: biddyMain.c:3096
unsigned int Biddy_Managed_NodeTableNum(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableNum returns number of all nodes currently in node table...
Definition: biddyStat.c:355
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:5854
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:1677
unsigned long long int Biddy_Managed_OPCacheSearch(Biddy_Manager MNG)
Function Biddy_Managed_OPCacheSearch.
Definition: biddyStat.c:1072
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
void Biddy_Managed_SetManagerParameters(Biddy_Manager MNG, float gcr, float gcrF, float gcrX, float rr, float rrF, float rrX, float st, float fst, float cst, float fcst)
Function Biddy_Managed_SetManagerParameters set modifiable parameters.
Definition: biddyMain.c:981
unsigned int Biddy_Managed_NodeTableBlockNumber(Biddy_Manager MNG)
Function Biddy_Managed_NodeTableBlockNumber.
Definition: biddyStat.c:278
Biddy_Edge Biddy_Managed_GetTerminal(Biddy_Manager MNG)
Function Biddy_Managed_GetTerminal returns unmarked edge pointing to the constant node 1...
Definition: biddyMain.c:1319
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:381
char * Biddy_String
Definition: biddy.h:223
Biddy_Edge Biddy_Managed_GetConstantOne(Biddy_Manager MNG)
Function Biddy_Managed_GetConstantOne returns constant 1.
Definition: biddyMain.c:1379
void * Biddy_Cache
Definition: biddy.h:237
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: biddyMain.c:4063