cudd_sys/
cudd.rs

1use crate::{
2    DdApaDigit, DdApaNumber, DdConstApaNumber, DdGen, DdManager, DdNode, DdTlcInfo, EpDouble,
3    MtrNode,
4};
5use libc::{FILE, c_char, c_double, c_int, c_long, c_uint, c_ulong, c_void, size_t};
6use std::ops::Not;
7use std::ptr::null_mut;
8
9/// Type of the value of a terminal node.
10pub type CUDD_VALUE_TYPE = c_double;
11
12/// Type of the hook function.
13pub type DD_HOOK_FUNCTION = extern "C" fn(*mut DdManager, *const c_char, *mut c_void) -> c_int;
14
15/// Type of the priority function.
16pub type DD_PRIORITY_FUNCTION = extern "C" fn(
17    *mut DdManager,
18    c_int,
19    *mut *mut DdNode,
20    *mut *mut DdNode,
21    *mut *mut DdNode,
22) -> *mut DdNode;
23
24/// Type of the apply operator function.
25pub type DD_APPLY_OPERATOR =
26    extern "C" fn(*mut DdManager, *mut *mut DdNode, *mut *mut DdNode) -> *mut DdNode;
27
28/// Type of the monadic apply operator function.
29pub type DD_MONADIC_APPLY_OPERATOR = extern "C" fn(*mut DdManager, *mut DdNode) -> *mut DdNode;
30
31/// Type of the out-of-memory function.
32pub type DD_OUT_OF_MEMORY_FUNCTION = extern "C" fn(size_t) -> c_void;
33
34/// Type of the termination handler function.
35pub type DD_TERMINATION_HANDLER = extern "C" fn(*const c_void) -> c_int;
36
37/// Type of the time-out handler function.
38pub type DD_TIME_OUT_HANDLER = extern "C" fn(*mut DdManager, *mut c_void) -> c_void;
39
40/// An integer representation of a Boolean `true` constant. (This is not a DD construct!)
41pub const CUDD_TRUE: c_uint = 1;
42/// An integer representation of a Boolean `false` constant. (This is not a DD construct!)
43pub const CUDD_FALSE: c_uint = 0;
44
45/// An special return value indicating an out-of-memory error.
46pub const CUDD_OUT_OF_MEM: c_int = -1;
47
48/// Recommended default size of the unique node table.
49pub const CUDD_UNIQUE_SLOTS: c_uint = 1 << 8;
50/// Recommended default size of the operation cache table.
51pub const CUDD_CACHE_SLOTS: c_uint = 1 << 18;
52
53/// Default option for `Cudd_addResidue`: specifies that the least-significant-bit is on top,
54/// and the number is interpreted as unsigned.
55pub const CUDD_RESIDUE_DEFAULT: c_int = 0;
56
57/// Used with `Cudd_addResidue`: add (logical or) this flag to the default options to specify that
58/// the most-significant-bit is on top.
59pub const CUDD_RESIDUE_MSB: c_int = 1;
60
61/// Used with `Cudd_addResidue`: add (logical or) this flag to the default options to specify that
62/// the number should be interpreted as a signed two's complement.
63pub const CUDD_RESIDUE_TC: c_int = 2;
64
65/// Types of variable reordering algorithms.
66#[repr(C)]
67pub enum Cudd_ReorderingType {
68    CUDD_REORDER_SAME,
69    CUDD_REORDER_NONE,
70    CUDD_REORDER_RANDOM,
71    CUDD_REORDER_RANDOM_PIVOT,
72    CUDD_REORDER_SIFT,
73    CUDD_REORDER_SIFT_CONVERGE,
74    CUDD_REORDER_SYMM_SIFT,
75    CUDD_REORDER_SYMM_SIFT_CONV,
76    CUDD_REORDER_WINDOW2,
77    CUDD_REORDER_WINDOW3,
78    CUDD_REORDER_WINDOW4,
79    CUDD_REORDER_WINDOW2_CONV,
80    CUDD_REORDER_WINDOW3_CONV,
81    CUDD_REORDER_WINDOW4_CONV,
82    CUDD_REORDER_GROUP_SIFT,
83    CUDD_REORDER_GROUP_SIFT_CONV,
84    CUDD_REORDER_ANNEALING,
85    CUDD_REORDER_GENETIC,
86    CUDD_REORDER_LINEAR,
87    CUDD_REORDER_LINEAR_CONVERGE,
88    CUDD_REORDER_LAZY_SIFT,
89    CUDD_REORDER_EXACT,
90}
91
92/// Type of aggregation method algorithm.
93#[repr(C)]
94pub enum Cudd_AggregationType {
95    CUDD_NO_CHECK,
96    CUDD_GROUP_CHECK,
97    CUDD_GROUP_CHECK2,
98    CUDD_GROUP_CHECK3,
99    CUDD_GROUP_CHECK4,
100    CUDD_GROUP_CHECK5,
101    CUDD_GROUP_CHECK6,
102    CUDD_GROUP_CHECK7,
103    CUDD_GROUP_CHECK8,
104    CUDD_GROUP_CHECK9,
105}
106
107/// Type of a hook.
108#[repr(C)]
109pub enum Cudd_HookType {
110    CUDD_PRE_GC_HOOK,
111    CUDD_POST_GC_HOOK,
112    CUDD_PRE_REORDERING_HOOK,
113    CUDD_POST_REORDERING_HOOK,
114}
115
116// Type of an error code.
117#[repr(C)]
118pub enum Cudd_ErrorType {
119    CUDD_NO_ERROR,
120    CUDD_MEMORY_OUT,
121    CUDD_TOO_MANY_NODES,
122    CUDD_MAX_MEM_EXCEEDED,
123    CUDD_TIMEOUT_EXPIRED,
124    CUDD_TERMINATION,
125    CUDD_INVALID_ARG,
126    CUDD_INTERNAL_ERROR,
127}
128
129/// Type of grouping used during lazy sifting.
130#[repr(C)]
131pub enum Cudd_LazyGroupType {
132    CUDD_LAZY_NONE,
133    CUDD_LAZY_SOFT_GROUP,
134    CUDD_LAZY_HARD_GROUP,
135    CUDD_LAZY_UNGROUP,
136}
137
138/// Type of variable used during lazy sifting.
139#[repr(C)]
140pub enum Cudd_VariableType {
141    CUDD_VAR_PRIMARY_INPUT,
142    CUDD_VAR_PRESENT_STATE,
143    CUDD_VAR_NEXT_STATE,
144}
145
146/// Complements a DD node by flipping the complement attribute of
147/// the pointer (the least significant bit).
148///
149/// # Safety
150///
151/// This function should only be called on a valid `DdNode` pointer.
152#[inline]
153pub unsafe fn Cudd_Not(node: *mut DdNode) -> *mut DdNode {
154    ((node as usize) ^ 1) as *mut DdNode
155}
156
157/// Complements a DD node by flipping the complement attribute
158/// of the pointer if a condition is satisfied. The `condition`
159/// argument must be always either `1` or `0`.
160///
161/// # Safety
162///
163/// This function should only be called on a valid `DdNode` pointer.
164#[inline]
165pub unsafe fn Cudd_NotCond(node: *mut DdNode, condition: c_int) -> *mut DdNode {
166    ((node as usize) ^ (condition as usize)) as *mut DdNode
167}
168
169/// Computes the regular version of a node pointer (i.e. without the complement
170/// bit set, regardless of its previous value).
171///
172/// # Safety
173///
174/// This function should only be called on a valid `DdNode` pointer.
175#[inline]
176pub unsafe fn Cudd_Regular(node: *mut DdNode) -> *mut DdNode {
177    ((node as usize) & (1_usize).not()) as *mut DdNode
178}
179
180/// Computes the complemented version of a node pointer (i.e. with a complement
181/// bit set, regardless of its previous value).
182///
183/// # Safety
184///
185/// This function should only be called on a valid `DdNode` pointer.
186#[inline]
187pub unsafe fn Cudd_Complement(node: *mut DdNode) -> *mut DdNode {
188    ((node as usize) | 1) as *mut DdNode
189}
190
191/// Returns 1 if a pointer is complemented.
192///
193/// # Safety
194///
195/// This function should only be called on a valid `DdNode` pointer.
196#[inline]
197pub unsafe fn Cudd_IsComplement(node: *mut DdNode) -> c_int {
198    ((node as usize) & 1) as c_int
199}
200
201/// Returns the current position in the order of variable
202/// index. This macro is obsolete and is kept for compatibility. New
203/// applications should use `Cudd_ReadPerm` instead.
204///
205/// # Safety
206///
207/// Follows the same invariants as `Cudd_ReadPerm`.
208#[inline]
209pub unsafe fn Cudd_ReadIndex(dd: *mut DdManager, index: c_int) -> c_int {
210    unsafe { Cudd_ReadPerm(dd, index) }
211}
212
213/// Iterates over the cubes of a decision diagram f. The length of the cube is the number
214/// of variables in the CUDD manager when the iteration is started.
215///
216/// See `Cudd_FirstCube` for more info.
217///
218/// # Safety
219///
220/// The cube is freed at the end of Cudd_ForeachCube and hence is not available
221/// outside of the loop.
222///
223/// CAUTION: It is assumed that dynamic reordering will not occur while
224/// there are open generators. It is the user's responsibility to make sure
225/// that dynamic reordering does not occur. As long as new nodes are not created
226/// during generation, and dynamic reordering is not called explicitly,
227/// dynamic reordering will not occur. Alternatively, it is sufficient to
228/// disable dynamic reordering. It is a mistake to dispose of a diagram
229/// on which generation is ongoing.
230#[inline]
231pub unsafe fn Cudd_ForeachCube<F: FnMut(*mut c_int, CUDD_VALUE_TYPE)>(
232    manager: *mut DdManager,
233    f: *mut DdNode,
234    mut action: F,
235) {
236    let mut cube = null_mut();
237    let mut value = 0.0;
238    unsafe {
239        let generator = Cudd_FirstCube(manager, f, &mut cube, &mut value);
240        while Cudd_IsGenEmpty(generator) != 1 {
241            action(cube, value);
242            Cudd_NextCube(generator, &mut cube, &mut value);
243        }
244        Cudd_GenFree(generator);
245    }
246}
247
248/// Iterates over the primes of a Boolean function producing
249/// a prime (but not necessarily irredundant) cover.
250/// For more information, see `Cudd_FirstPrime`.
251///
252/// # Safety
253///
254/// The Boolean function is described by an upper bound and a lower bound.  If
255/// the function is completely specified, the two bounds coincide.
256/// Cudd_ForeachPrime allocates and frees the generator.  Therefore the
257/// application should not try to do that.  Also, the cube is freed at the
258/// end of Cudd_ForeachPrime and hence is not available outside of the loop.<p>
259/// CAUTION: It is a mistake to change a diagram on which generation is ongoing.
260#[inline]
261pub unsafe fn Cudd_ForeachPrime<F: FnMut(*mut c_int)>(
262    manager: *mut DdManager,
263    l: *mut DdNode,
264    u: *mut DdNode,
265    mut action: F,
266) {
267    let mut cube = null_mut();
268    unsafe {
269        let generator = Cudd_FirstPrime(manager, l, u, &mut cube);
270        while Cudd_IsGenEmpty(generator) != 1 {
271            action(cube);
272            Cudd_NextPrime(generator, &mut cube);
273        }
274        Cudd_GenFree(generator);
275    }
276}
277
278/// Iterates over the nodes of a decision diagram `f`. See also `Cudd_FirstNode`.
279///
280/// # Safety
281///
282/// The nodes are returned in a seemingly random order.
283///
284/// CAUTION: It is assumed that dynamic reordering will not occur while
285/// there are open generators. It is the user's responsibility to make sure
286/// that dynamic reordering does not occur. As long as new nodes are not created
287/// during generation, and dynamic reordering is not called explicitly,
288/// dynamic reordering will not occur. Alternatively, it is sufficient to
289/// disable dynamic reordering. It is a mistake to dispose of a diagram
290/// on which generation is ongoing.
291#[inline]
292pub unsafe fn Cudd_ForeachNode<F: FnMut(*mut DdNode)>(
293    manager: *mut DdManager,
294    f: *mut DdNode,
295    mut action: F,
296) {
297    let mut node = null_mut();
298    unsafe {
299        let generator = Cudd_FirstNode(manager, f, &mut node);
300        while Cudd_IsGenEmpty(generator) != 1 {
301            action(node);
302            Cudd_NextNode(generator, &mut node);
303        }
304        Cudd_GenFree(generator);
305    }
306}
307
308/// Iterates over the paths of a ZDD `f`.
309///
310/// # Safety
311///
312/// The path is freed at the end of Cudd_zddForeachPath and hence is not available outside
313/// of the loop.
314///
315/// CAUTION: It is assumed that dynamic reordering will not occur while
316/// there are open generators.  It is the user's responsibility to make sure
317/// that dynamic reordering does not occur.  As long as new nodes are not created
318/// during generation, and dynamic reordering is not called explicitly,
319/// dynamic reordering will not occur.  Alternatively, it is sufficient to
320/// disable dynamic reordering.  It is a mistake to dispose of a diagram
321/// on which generation is ongoing.
322#[inline]
323pub unsafe fn Cudd_zddForeachPath<F: FnMut(*mut c_int)>(
324    manager: *mut DdManager,
325    f: *mut DdNode,
326    mut action: F,
327) {
328    let mut path = null_mut();
329    unsafe {
330        let generator = Cudd_zddFirstPath(manager, f, &mut path);
331        while Cudd_IsGenEmpty(generator) != 1 {
332            action(path);
333            Cudd_zddNextPath(generator, &mut path);
334        }
335        Cudd_GenFree(generator);
336    }
337}
338
339unsafe extern "C" {
340    pub fn Cudd_addNewVar(dd: *mut DdManager) -> *mut DdNode;
341    pub fn Cudd_addNewVarAtLevel(dd: *mut DdManager, level: c_int) -> *mut DdNode;
342    pub fn Cudd_bddNewVar(dd: *mut DdManager) -> *mut DdNode;
343    pub fn Cudd_bddNewVarAtLevel(dd: *mut DdManager, level: c_int) -> *mut DdNode;
344    pub fn Cudd_bddIsVar(dd: *mut DdManager, f: *mut DdNode) -> c_int;
345    pub fn Cudd_addIthVar(dd: *mut DdManager, i: c_int) -> *mut DdNode;
346    pub fn Cudd_bddIthVar(dd: *mut DdManager, i: c_int) -> *mut DdNode;
347    pub fn Cudd_zddIthVar(dd: *mut DdManager, i: c_int) -> *mut DdNode;
348    pub fn Cudd_zddVarsFromBddVars(dd: *mut DdManager, multiplicity: c_int) -> c_int;
349    pub fn Cudd_ReadMaxIndex() -> c_uint;
350    pub fn Cudd_addConst(dd: *mut DdManager, c: CUDD_VALUE_TYPE) -> *mut DdNode;
351    pub fn Cudd_IsConstant(node: *mut DdNode) -> c_int;
352    pub fn Cudd_IsNonConstant(f: *mut DdNode) -> c_int;
353    pub fn Cudd_T(node: *mut DdNode) -> *mut DdNode;
354    pub fn Cudd_E(node: *mut DdNode) -> *mut DdNode;
355    pub fn Cudd_V(node: *mut DdNode) -> CUDD_VALUE_TYPE;
356    pub fn Cudd_ReadStartTime(unique: *mut DdManager) -> c_ulong;
357    pub fn Cudd_ReadElapsedTime(unique: *mut DdManager) -> c_ulong;
358    pub fn Cudd_SetStartTime(unique: *mut DdManager, st: c_ulong) -> c_void;
359    pub fn Cudd_ResetStartTime(unique: *mut DdManager) -> c_void;
360    pub fn Cudd_ReadTimeLimit(unique: *mut DdManager) -> c_ulong;
361    pub fn Cudd_SetTimeLimit(unique: *mut DdManager, tl: c_ulong) -> c_ulong;
362    pub fn Cudd_UpdateTimeLimit(unique: *mut DdManager) -> c_void;
363    pub fn Cudd_IncreaseTimeLimit(unique: *mut DdManager, increase: c_ulong) -> c_void;
364    pub fn Cudd_UnsetTimeLimit(unique: *mut DdManager) -> c_void;
365    pub fn Cudd_TimeLimited(unique: *mut DdManager) -> c_int;
366    pub fn Cudd_RegisterTerminationCallback(
367        unique: *mut DdManager,
368        callback: DD_TERMINATION_HANDLER,
369        callback_arg: *mut c_void,
370    ) -> c_void;
371    pub fn Cudd_UnregisterTerminationCallback(unique: *mut DdManager) -> c_void;
372    pub fn Cudd_RegisterOutOfMemoryCallback(
373        unique: *mut DdManager,
374        callback: Option<DD_OUT_OF_MEMORY_FUNCTION>,
375    ) -> Option<DD_OUT_OF_MEMORY_FUNCTION>;
376    pub fn Cudd_UnregisterOutOfMemoryCallback(unique: *mut DdManager) -> c_void;
377    pub fn Cudd_RegisterTimeoutHandler(
378        unique: *mut DdManager,
379        handler: Option<DD_TIME_OUT_HANDLER>,
380        arg: *mut c_void,
381    ) -> c_void;
382    pub fn Cudd_ReadTimeoutHandler(
383        unique: *mut DdManager,
384        argp: *mut *mut c_void,
385    ) -> Option<DD_TIME_OUT_HANDLER>;
386    pub fn Cudd_AutodynEnable(unique: *mut DdManager, method: Cudd_ReorderingType) -> c_void;
387    pub fn Cudd_AutodynDisable(unique: *mut DdManager) -> c_void;
388    pub fn Cudd_ReorderingStatus(unique: *mut DdManager, method: *mut Cudd_ReorderingType)
389    -> c_int;
390    pub fn Cudd_AutodynEnableZdd(unique: *mut DdManager, method: Cudd_ReorderingType) -> c_void;
391    pub fn Cudd_AutodynDisableZdd(unique: *mut DdManager) -> c_void;
392    pub fn Cudd_ReorderingStatusZdd(
393        unique: *mut DdManager,
394        method: *mut Cudd_ReorderingType,
395    ) -> c_int;
396    pub fn Cudd_zddRealignmentEnabled(unique: *mut DdManager) -> c_int;
397    pub fn Cudd_zddRealignEnable(unique: *mut DdManager) -> c_void;
398    pub fn Cudd_zddRealignDisable(unique: *mut DdManager) -> c_void;
399    pub fn Cudd_bddRealignmentEnabled(unique: *mut DdManager) -> c_int;
400    pub fn Cudd_bddRealignEnable(unique: *mut DdManager) -> c_void;
401    pub fn Cudd_bddRealignDisable(unique: *mut DdManager) -> c_void;
402    pub fn Cudd_ReadOne(dd: *mut DdManager) -> *mut DdNode;
403    pub fn Cudd_ReadZddOne(dd: *mut DdManager, i: c_int) -> *mut DdNode;
404    pub fn Cudd_ReadZero(dd: *mut DdManager) -> *mut DdNode;
405    pub fn Cudd_ReadLogicZero(dd: *mut DdManager) -> *mut DdNode;
406    pub fn Cudd_ReadPlusInfinity(dd: *mut DdManager) -> *mut DdNode;
407    pub fn Cudd_ReadMinusInfinity(dd: *mut DdManager) -> *mut DdNode;
408    pub fn Cudd_ReadBackground(dd: *mut DdManager) -> *mut DdNode;
409    pub fn Cudd_SetBackground(dd: *mut DdManager, bck: *mut DdNode) -> c_void;
410    pub fn Cudd_ReadCacheSlots(dd: *mut DdManager) -> c_uint;
411    pub fn Cudd_ReadCacheUsedSlots(dd: *mut DdManager) -> c_double;
412    pub fn Cudd_ReadCacheLookUps(dd: *mut DdManager) -> c_double;
413    pub fn Cudd_ReadCacheHits(dd: *mut DdManager) -> c_double;
414    pub fn Cudd_ReadRecursiveCalls(dd: *mut DdManager) -> c_double;
415    pub fn Cudd_ReadMinHit(dd: *mut DdManager) -> c_uint;
416    pub fn Cudd_SetMinHit(dd: *mut DdManager, hr: c_uint) -> c_void;
417    pub fn Cudd_ReadLooseUpTo(dd: *mut DdManager) -> c_uint;
418    pub fn Cudd_SetLooseUpTo(dd: *mut DdManager, lut: c_uint) -> c_void;
419    pub fn Cudd_ReadMaxCache(dd: *mut DdManager) -> c_uint;
420    pub fn Cudd_ReadMaxCacheHard(dd: *mut DdManager) -> c_uint;
421    pub fn Cudd_SetMaxCacheHard(dd: *mut DdManager, mc: c_uint) -> c_void;
422    pub fn Cudd_ReadSize(dd: *mut DdManager) -> c_int;
423    pub fn Cudd_ReadZddSize(dd: *mut DdManager) -> c_int;
424    pub fn Cudd_ReadSlots(dd: *mut DdManager) -> c_uint;
425    pub fn Cudd_ReadUsedSlots(dd: *mut DdManager) -> c_double;
426    pub fn Cudd_ExpectedUsedSlots(dd: *mut DdManager) -> c_double;
427    pub fn Cudd_ReadKeys(dd: *mut DdManager) -> c_uint;
428    pub fn Cudd_ReadDead(dd: *mut DdManager) -> c_uint;
429    pub fn Cudd_ReadMinDead(dd: *mut DdManager) -> c_uint;
430    pub fn Cudd_ReadReorderings(dd: *mut DdManager) -> c_uint;
431    pub fn Cudd_ReadMaxReorderings(dd: *mut DdManager) -> c_uint;
432    pub fn Cudd_SetMaxReorderings(dd: *mut DdManager, mr: c_uint) -> c_void;
433    pub fn Cudd_ReadReorderingTime(dd: *mut DdManager) -> c_long;
434    pub fn Cudd_ReadGarbageCollections(dd: *mut DdManager) -> c_int;
435    pub fn Cudd_ReadGarbageCollectionTime(dd: *mut DdManager) -> c_long;
436    pub fn Cudd_ReadNodesFreed(dd: *mut DdManager) -> c_double;
437    pub fn Cudd_ReadNodesDropped(dd: *mut DdManager) -> c_double;
438    pub fn Cudd_ReadUniqueLookUps(dd: *mut DdManager) -> c_double;
439    pub fn Cudd_ReadUniqueLinks(dd: *mut DdManager) -> c_double;
440    pub fn Cudd_ReadSiftMaxVar(dd: *mut DdManager) -> c_int;
441    pub fn Cudd_SetSiftMaxVar(dd: *mut DdManager, smv: c_int) -> c_void;
442    pub fn Cudd_ReadSiftMaxSwap(dd: *mut DdManager) -> c_int;
443    pub fn Cudd_SetSiftMaxSwap(dd: *mut DdManager, sms: c_int) -> c_void;
444    pub fn Cudd_ReadMaxGrowth(dd: *mut DdManager) -> c_double;
445    pub fn Cudd_SetMaxGrowth(dd: *mut DdManager, mg: c_double) -> c_void;
446    pub fn Cudd_ReadMaxGrowthAlternate(dd: *mut DdManager) -> c_double;
447    pub fn Cudd_SetMaxGrowthAlternate(dd: *mut DdManager, mg: c_double) -> c_void;
448    pub fn Cudd_ReadReorderingCycle(dd: *mut DdManager) -> c_int;
449    pub fn Cudd_SetReorderingCycle(dd: *mut DdManager, cycle: c_int) -> c_void;
450    pub fn Cudd_NodeReadIndex(dd: *mut DdNode) -> c_uint;
451    pub fn Cudd_ReadPerm(dd: *mut DdManager, i: c_int) -> c_int;
452    pub fn Cudd_ReadPermZdd(dd: *mut DdManager, i: c_int) -> c_int;
453    pub fn Cudd_ReadInvPerm(dd: *mut DdManager, i: c_int) -> c_int;
454    pub fn Cudd_ReadInvPermZdd(dd: *mut DdManager, i: c_int) -> c_int;
455    pub fn Cudd_ReadVars(dd: *mut DdManager, i: c_int) -> *mut DdNode;
456    pub fn Cudd_ReadEpsilon(dd: *mut DdManager) -> CUDD_VALUE_TYPE;
457    pub fn Cudd_SetEpsilon(dd: *mut DdManager, ep: CUDD_VALUE_TYPE) -> c_void;
458    pub fn Cudd_ReadGroupcheck(dd: *mut DdManager) -> Cudd_AggregationType;
459    pub fn Cudd_SetGroupcheck(dd: *mut DdManager, gc: Cudd_AggregationType) -> c_void;
460    pub fn Cudd_GarbageCollectionEnabled(dd: *mut DdManager) -> c_int;
461    pub fn Cudd_EnableGarbageCollection(dd: *mut DdManager) -> c_void;
462    pub fn Cudd_DisableGarbageCollection(dd: *mut DdManager) -> c_void;
463    pub fn Cudd_DeadAreCounted(dd: *mut DdManager) -> c_int;
464    pub fn Cudd_TurnOnCountDead(dd: *mut DdManager) -> c_void;
465    pub fn Cudd_TurnOffCountDead(dd: *mut DdManager) -> c_void;
466    pub fn Cudd_ReadRecomb(dd: *mut DdManager) -> c_int;
467    pub fn Cudd_SetRecomb(dd: *mut DdManager, recomb: c_int) -> c_void;
468    pub fn Cudd_ReadSymmviolation(dd: *mut DdManager) -> c_int;
469    pub fn Cudd_SetSymmviolation(dd: *mut DdManager, symmviolation: c_int) -> c_void;
470    pub fn Cudd_ReadArcviolation(dd: *mut DdManager) -> c_int;
471    pub fn Cudd_SetArcviolation(dd: *mut DdManager, arcviolation: c_int) -> c_void;
472    pub fn Cudd_ReadPopulationSize(dd: *mut DdManager) -> c_int;
473    pub fn Cudd_SetPopulationSize(dd: *mut DdManager, populationSize: c_int) -> c_void;
474    pub fn Cudd_ReadNumberXovers(dd: *mut DdManager) -> c_int;
475    pub fn Cudd_SetNumberXovers(dd: *mut DdManager, numberXovers: c_int) -> c_void;
476    pub fn Cudd_ReadOrderRandomization(dd: *mut DdManager) -> c_uint;
477    pub fn Cudd_SetOrderRandomization(dd: *mut DdManager, factor: c_uint) -> c_void;
478    pub fn Cudd_ReadMemoryInUse(dd: *mut DdManager) -> size_t;
479    pub fn Cudd_PrintInfo(dd: *mut DdManager, fp: *mut FILE) -> c_int;
480    pub fn Cudd_ReadPeakNodeCount(dd: *mut DdManager) -> c_long;
481    pub fn Cudd_ReadPeakLiveNodeCount(dd: *mut DdManager) -> c_int;
482    pub fn Cudd_ReadNodeCount(dd: *mut DdManager) -> c_long;
483    pub fn Cudd_zddReadNodeCount(dd: *mut DdManager) -> c_long;
484    pub fn Cudd_AddHook(dd: *mut DdManager, f: DD_HOOK_FUNCTION, hook_type: Cudd_HookType)
485    -> c_int;
486    pub fn Cudd_RemoveHook(
487        dd: *mut DdManager,
488        f: DD_HOOK_FUNCTION,
489        hook_type: Cudd_HookType,
490    ) -> c_int;
491    pub fn Cudd_IsInHook(
492        dd: *mut DdManager,
493        f: DD_HOOK_FUNCTION,
494        hook_type: Cudd_HookType,
495    ) -> c_int;
496    pub fn Cudd_StdPreReordHook(dd: *mut DdManager, str: *const c_char, data: *mut c_void)
497    -> c_int;
498    pub fn Cudd_StdPostReordHook(
499        dd: *mut DdManager,
500        str: *const c_char,
501        data: *mut c_void,
502    ) -> c_int;
503    pub fn Cudd_EnableReorderingReporting(dd: *mut DdManager) -> c_int;
504    pub fn Cudd_DisableReorderingReporting(dd: *mut DdManager) -> c_int;
505    pub fn Cudd_ReorderingReporting(dd: *mut DdManager) -> c_int;
506    pub fn Cudd_PrintGroupedOrder(
507        dd: *mut DdManager,
508        str: *const c_char,
509        data: *mut c_void,
510    ) -> c_int;
511    pub fn Cudd_EnableOrderingMonitoring(dd: *mut DdManager) -> c_int;
512    pub fn Cudd_DisableOrderingMonitoring(dd: *mut DdManager) -> c_int;
513    pub fn Cudd_OrderingMonitoring(dd: *mut DdManager) -> c_int;
514    pub fn Cudd_SetApplicationHook(dd: *mut DdManager, value: *mut c_void) -> c_void;
515    pub fn Cudd_ReadApplicationHook(dd: *mut DdManager) -> *mut c_void;
516    pub fn Cudd_ReadErrorCode(dd: *mut DdManager) -> Cudd_ErrorType;
517    pub fn Cudd_ClearErrorCode(dd: *mut DdManager) -> c_void;
518    pub fn Cudd_InstallOutOfMemoryHandler(
519        newHandler: DD_OUT_OF_MEMORY_FUNCTION,
520    ) -> DD_OUT_OF_MEMORY_FUNCTION;
521    pub fn Cudd_ReadStdout(dd: *mut DdManager) -> *mut FILE;
522    pub fn Cudd_SetStdout(dd: *mut DdManager, fp: *mut FILE) -> c_void;
523    pub fn Cudd_ReadStderr(dd: *mut DdManager) -> *mut FILE;
524    pub fn Cudd_SetStderr(dd: *mut DdManager, fp: *mut FILE) -> c_void;
525    pub fn Cudd_ReadNextReordering(dd: *mut DdManager) -> c_uint;
526    pub fn Cudd_SetNextReordering(dd: *mut DdManager, next: c_uint) -> c_void;
527    pub fn Cudd_ReadSwapSteps(dd: *mut DdManager) -> c_double;
528    pub fn Cudd_ReadMaxLive(dd: *mut DdManager) -> c_uint;
529    pub fn Cudd_SetMaxLive(dd: *mut DdManager, maxLive: c_uint) -> c_void;
530    pub fn Cudd_ReadMaxMemory(dd: *mut DdManager) -> size_t;
531    pub fn Cudd_SetMaxMemory(dd: *mut DdManager, maxMemory: size_t) -> size_t;
532    pub fn Cudd_bddBindVar(dd: *mut DdManager, index: c_int) -> c_int;
533    pub fn Cudd_bddUnbindVar(dd: *mut DdManager, index: c_int) -> c_int;
534    pub fn Cudd_bddVarIsBound(dd: *mut DdManager, index: c_int) -> c_int;
535    pub fn Cudd_addExistAbstract(
536        manager: *mut DdManager,
537        f: *mut DdNode,
538        cube: *mut DdNode,
539    ) -> *mut DdNode;
540    pub fn Cudd_addUnivAbstract(
541        manager: *mut DdManager,
542        f: *mut DdNode,
543        cube: *mut DdNode,
544    ) -> *mut DdNode;
545    pub fn Cudd_addOrAbstract(
546        manager: *mut DdManager,
547        f: *mut DdNode,
548        cube: *mut DdNode,
549    ) -> *mut DdNode;
550    pub fn Cudd_addApply(
551        dd: *mut DdManager,
552        op: DD_APPLY_OPERATOR,
553        f: *mut DdNode,
554        g: *mut DdNode,
555    ) -> *mut DdNode;
556    pub fn Cudd_addPlus(
557        dd: *mut DdManager,
558        f: *mut *mut DdNode,
559        g: *mut *mut DdNode,
560    ) -> *mut DdNode;
561    pub fn Cudd_addTimes(
562        dd: *mut DdManager,
563        f: *mut *mut DdNode,
564        g: *mut *mut DdNode,
565    ) -> *mut DdNode;
566    pub fn Cudd_addThreshold(
567        dd: *mut DdManager,
568        f: *mut *mut DdNode,
569        g: *mut *mut DdNode,
570    ) -> *mut DdNode;
571    pub fn Cudd_addSetNZ(
572        dd: *mut DdManager,
573        f: *mut *mut DdNode,
574        g: *mut *mut DdNode,
575    ) -> *mut DdNode;
576    pub fn Cudd_addDivide(
577        dd: *mut DdManager,
578        f: *mut *mut DdNode,
579        g: *mut *mut DdNode,
580    ) -> *mut DdNode;
581    pub fn Cudd_addMinus(
582        dd: *mut DdManager,
583        f: *mut *mut DdNode,
584        g: *mut *mut DdNode,
585    ) -> *mut DdNode;
586    pub fn Cudd_addMinimum(
587        dd: *mut DdManager,
588        f: *mut *mut DdNode,
589        g: *mut *mut DdNode,
590    ) -> *mut DdNode;
591    pub fn Cudd_addMaximum(
592        dd: *mut DdManager,
593        f: *mut *mut DdNode,
594        g: *mut *mut DdNode,
595    ) -> *mut DdNode;
596    pub fn Cudd_addOneZeroMaximum(
597        dd: *mut DdManager,
598        f: *mut *mut DdNode,
599        g: *mut *mut DdNode,
600    ) -> *mut DdNode;
601    pub fn Cudd_addDiff(
602        dd: *mut DdManager,
603        f: *mut *mut DdNode,
604        g: *mut *mut DdNode,
605    ) -> *mut DdNode;
606    pub fn Cudd_addAgreement(
607        dd: *mut DdManager,
608        f: *mut *mut DdNode,
609        g: *mut *mut DdNode,
610    ) -> *mut DdNode;
611    pub fn Cudd_addOr(dd: *mut DdManager, f: *mut *mut DdNode, g: *mut *mut DdNode) -> *mut DdNode;
612    pub fn Cudd_addNand(
613        dd: *mut DdManager,
614        f: *mut *mut DdNode,
615        g: *mut *mut DdNode,
616    ) -> *mut DdNode;
617    pub fn Cudd_addNor(dd: *mut DdManager, f: *mut *mut DdNode, g: *mut *mut DdNode)
618    -> *mut DdNode;
619    pub fn Cudd_addXor(dd: *mut DdManager, f: *mut *mut DdNode, g: *mut *mut DdNode)
620    -> *mut DdNode;
621    pub fn Cudd_addXnor(
622        dd: *mut DdManager,
623        f: *mut *mut DdNode,
624        g: *mut *mut DdNode,
625    ) -> *mut DdNode;
626    pub fn Cudd_addMonadicApply(
627        dd: *mut DdManager,
628        op: DD_MONADIC_APPLY_OPERATOR,
629        f: *mut DdNode,
630    ) -> *mut DdNode;
631    pub fn Cudd_addLog(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode;
632    pub fn Cudd_addFindMax(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode;
633    pub fn Cudd_addFindMin(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode;
634    pub fn Cudd_addIthBit(dd: *mut DdManager, f: *mut DdNode, bit: c_int) -> *mut DdNode;
635    pub fn Cudd_addScalarInverse(
636        dd: *mut DdManager,
637        f: *mut DdNode,
638        epsilon: *mut DdNode,
639    ) -> *mut DdNode;
640    pub fn Cudd_addIte(
641        dd: *mut DdManager,
642        f: *mut DdNode,
643        g: *mut DdNode,
644        h: *mut DdNode,
645    ) -> *mut DdNode;
646    pub fn Cudd_addIteConstant(
647        dd: *mut DdManager,
648        f: *mut DdNode,
649        g: *mut DdNode,
650        h: *mut DdNode,
651    ) -> *mut DdNode;
652    pub fn Cudd_addEvalConst(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
653    pub fn Cudd_addLeq(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> c_int;
654    pub fn Cudd_addCmpl(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode;
655    pub fn Cudd_addNegate(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode;
656    pub fn Cudd_addRoundOff(dd: *mut DdManager, f: *mut DdNode, N: c_int) -> *mut DdNode;
657    pub fn Cudd_addWalsh(
658        dd: *mut DdManager,
659        x: *mut *mut DdNode,
660        y: *mut *mut DdNode,
661        n: c_int,
662    ) -> *mut DdNode;
663    pub fn Cudd_addResidue(
664        dd: *mut DdManager,
665        n: c_int,
666        m: c_int,
667        options: c_int,
668        top: c_int,
669    ) -> *mut DdNode;
670    pub fn Cudd_bddAndAbstract(
671        manager: *mut DdManager,
672        f: *mut DdNode,
673        g: *mut DdNode,
674        cube: *mut DdNode,
675    ) -> *mut DdNode;
676    pub fn Cudd_bddAndAbstractLimit(
677        manager: *mut DdManager,
678        f: *mut DdNode,
679        g: *mut DdNode,
680        cube: *mut DdNode,
681        limit: c_uint,
682    ) -> *mut DdNode;
683    pub fn Cudd_ApaNumberOfDigits(binaryDigits: c_int) -> c_int;
684    pub fn Cudd_NewApaNumber(digits: c_int) -> DdApaNumber;
685    pub fn Cudd_FreeApaNumber(number: DdApaNumber) -> c_void;
686    pub fn Cudd_ApaCopy(digits: c_int, source: DdConstApaNumber, dest: DdApaNumber) -> c_void;
687    pub fn Cudd_ApaAdd(
688        digits: c_int,
689        a: DdConstApaNumber,
690        b: DdConstApaNumber,
691        sum: DdApaNumber,
692    ) -> DdApaDigit;
693    pub fn Cudd_ApaSubtract(
694        digits: c_int,
695        a: DdConstApaNumber,
696        b: DdConstApaNumber,
697        diff: DdApaNumber,
698    ) -> DdApaDigit;
699    pub fn Cudd_ApaShortDivision(
700        digits: c_int,
701        dividend: DdConstApaNumber,
702        divisor: DdApaDigit,
703        quotient: DdApaNumber,
704    ) -> DdApaDigit;
705    pub fn Cudd_ApaIntDivision(
706        digits: c_int,
707        dividend: DdConstApaNumber,
708        divisor: c_uint,
709        quotient: DdApaNumber,
710    ) -> c_uint;
711    pub fn Cudd_ApaShiftRight(
712        digits: c_int,
713        input: DdApaDigit,
714        a: DdConstApaNumber,
715        b: DdApaNumber,
716    ) -> c_void;
717    pub fn Cudd_ApaSetToLiteral(digits: c_int, number: DdApaNumber, literal: DdApaDigit) -> c_void;
718    pub fn Cudd_ApaPowerOfTwo(digits: c_int, number: DdApaNumber, power: c_int) -> c_void;
719    pub fn Cudd_ApaCompare(
720        digitsFirst: c_int,
721        first: DdConstApaNumber,
722        digitsSecond: c_int,
723        second: DdConstApaNumber,
724    ) -> c_int;
725    pub fn Cudd_ApaCompareRatios(
726        digitsFirst: c_int,
727        firstNum: DdConstApaNumber,
728        firstDen: c_uint,
729        digitsSecond: c_int,
730        secondNum: DdConstApaNumber,
731        secondDen: c_uint,
732    ) -> c_int;
733    pub fn Cudd_ApaPrintHex(fp: *mut FILE, digits: c_int, number: DdConstApaNumber) -> c_int;
734    pub fn Cudd_ApaPrintDecimal(fp: *mut FILE, digits: c_int, number: DdConstApaNumber) -> c_int;
735    pub fn Cudd_ApaStringDecimal(digits: c_int, number: DdConstApaNumber) -> *mut c_char;
736    pub fn Cudd_ApaPrintExponential(
737        fp: *mut FILE,
738        digits: c_int,
739        number: DdConstApaNumber,
740        precision: c_int,
741    ) -> c_int;
742    pub fn Cudd_ApaCountMinterm(
743        manager: *const DdManager,
744        node: *mut DdNode,
745        nvars: c_int,
746        digits: *mut c_int,
747    ) -> DdApaNumber;
748    pub fn Cudd_ApaPrintMinterm(
749        fp: *mut FILE,
750        dd: *const DdManager,
751        node: *mut DdNode,
752        nvars: c_int,
753    ) -> c_int;
754    pub fn Cudd_ApaPrintMintermExp(
755        fp: *mut FILE,
756        dd: *const DdManager,
757        node: *mut DdNode,
758        nvars: c_int,
759        precision: c_int,
760    ) -> c_int;
761    pub fn Cudd_ApaPrintDensity(
762        fp: *mut FILE,
763        dd: *mut DdManager,
764        node: *mut DdNode,
765        nvars: c_int,
766    ) -> c_int;
767    pub fn Cudd_UnderApprox(
768        dd: *mut DdManager,
769        f: *mut DdNode,
770        numVars: c_int,
771        threshold: c_int,
772        safe: c_int,
773        quality: c_double,
774    ) -> *mut DdNode;
775    pub fn Cudd_OverApprox(
776        dd: *mut DdManager,
777        f: *mut DdNode,
778        numVars: c_int,
779        threshold: c_int,
780        safe: c_int,
781        quality: c_double,
782    ) -> *mut DdNode;
783    pub fn Cudd_RemapUnderApprox(
784        dd: *mut DdManager,
785        f: *mut DdNode,
786        numVars: c_int,
787        threshold: c_int,
788        quality: c_double,
789    ) -> *mut DdNode;
790    pub fn Cudd_RemapOverApprox(
791        dd: *mut DdManager,
792        f: *mut DdNode,
793        numVars: c_int,
794        threshold: c_int,
795        quality: c_double,
796    ) -> *mut DdNode;
797    pub fn Cudd_BiasedUnderApprox(
798        dd: *mut DdManager,
799        f: *mut DdNode,
800        b: *mut DdNode,
801        numVars: c_int,
802        threshold: c_int,
803        quality1: c_double,
804        quality0: c_double,
805    ) -> *mut DdNode;
806    pub fn Cudd_BiasedOverApprox(
807        dd: *mut DdManager,
808        f: *mut DdNode,
809        b: *mut DdNode,
810        numVars: c_int,
811        threshold: c_int,
812        quality1: c_double,
813        quality0: c_double,
814    ) -> *mut DdNode;
815    pub fn Cudd_bddExistAbstract(
816        manager: *mut DdManager,
817        f: *mut DdNode,
818        cube: *mut DdNode,
819    ) -> *mut DdNode;
820    pub fn Cudd_bddExistAbstractLimit(
821        manager: *mut DdManager,
822        f: *mut DdNode,
823        cube: *mut DdNode,
824        limit: c_uint,
825    ) -> *mut DdNode;
826    pub fn Cudd_bddXorExistAbstract(
827        manager: *mut DdManager,
828        f: *mut DdNode,
829        g: *mut DdNode,
830        cube: *mut DdNode,
831    ) -> *mut DdNode;
832    pub fn Cudd_bddUnivAbstract(
833        manager: *mut DdManager,
834        f: *mut DdNode,
835        cube: *mut DdNode,
836    ) -> *mut DdNode;
837    pub fn Cudd_bddBooleanDiff(manager: *mut DdManager, f: *mut DdNode, x: c_int) -> *mut DdNode;
838    pub fn Cudd_bddVarIsDependent(dd: *mut DdManager, f: *mut DdNode, var: *mut DdNode) -> c_int;
839    pub fn Cudd_bddCorrelation(manager: *mut DdManager, f: *mut DdNode, g: *mut DdNode)
840    -> c_double;
841    pub fn Cudd_bddCorrelationWeights(
842        manager: *mut DdManager,
843        f: *mut DdNode,
844        g: *mut DdNode,
845        prob: *mut c_double,
846    ) -> c_double;
847    pub fn Cudd_bddIte(
848        dd: *mut DdManager,
849        f: *mut DdNode,
850        g: *mut DdNode,
851        h: *mut DdNode,
852    ) -> *mut DdNode;
853    pub fn Cudd_bddIteLimit(
854        dd: *mut DdManager,
855        f: *mut DdNode,
856        g: *mut DdNode,
857        h: *mut DdNode,
858        limit: c_uint,
859    ) -> *mut DdNode;
860    pub fn Cudd_bddIteConstant(
861        dd: *mut DdManager,
862        f: *mut DdNode,
863        g: *mut DdNode,
864        h: *mut DdNode,
865    ) -> *mut DdNode;
866    pub fn Cudd_bddIntersect(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
867    pub fn Cudd_bddAnd(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
868    pub fn Cudd_bddAndLimit(
869        dd: *mut DdManager,
870        f: *mut DdNode,
871        g: *mut DdNode,
872        limit: c_uint,
873    ) -> *mut DdNode;
874    pub fn Cudd_bddOr(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
875    pub fn Cudd_bddOrLimit(
876        dd: *mut DdManager,
877        f: *mut DdNode,
878        g: *mut DdNode,
879        limit: c_uint,
880    ) -> *mut DdNode;
881    pub fn Cudd_bddNand(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
882    pub fn Cudd_bddNor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
883    pub fn Cudd_bddXor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
884    pub fn Cudd_bddXnor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
885    pub fn Cudd_bddXnorLimit(
886        dd: *mut DdManager,
887        f: *mut DdNode,
888        g: *mut DdNode,
889        limit: c_uint,
890    ) -> *mut DdNode;
891    pub fn Cudd_bddLeq(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> c_int;
892    pub fn Cudd_addBddThreshold(
893        dd: *mut DdManager,
894        f: *mut DdNode,
895        value: CUDD_VALUE_TYPE,
896    ) -> *mut DdNode;
897    pub fn Cudd_addBddStrictThreshold(
898        dd: *mut DdManager,
899        f: *mut DdNode,
900        value: CUDD_VALUE_TYPE,
901    ) -> *mut DdNode;
902    pub fn Cudd_addBddInterval(
903        dd: *mut DdManager,
904        f: *mut DdNode,
905        lower: CUDD_VALUE_TYPE,
906        upper: CUDD_VALUE_TYPE,
907    ) -> *mut DdNode;
908    pub fn Cudd_addBddIthBit(dd: *mut DdManager, f: *mut DdNode, bit: c_int) -> *mut DdNode;
909    pub fn Cudd_BddToAdd(dd: *mut DdManager, B: *mut DdNode) -> *mut DdNode;
910    pub fn Cudd_addBddPattern(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode;
911    pub fn Cudd_bddTransfer(
912        ddSource: *mut DdManager,
913        ddDestination: *mut DdManager,
914        f: *mut DdNode,
915    ) -> *mut DdNode;
916    pub fn Cudd_DebugCheck(table: *mut DdManager) -> c_int;
917    pub fn Cudd_CheckKeys(table: *mut DdManager) -> c_int;
918    pub fn Cudd_bddClippingAnd(
919        dd: *mut DdManager,
920        f: *mut DdNode,
921        g: *mut DdNode,
922        maxDepth: c_int,
923        direction: c_int,
924    ) -> *mut DdNode;
925    pub fn Cudd_bddClippingAndAbstract(
926        dd: *mut DdManager,
927        f: *mut DdNode,
928        g: *mut DdNode,
929        cube: *mut DdNode,
930        maxDepth: c_int,
931        direction: c_int,
932    ) -> *mut DdNode;
933    pub fn Cudd_Cofactor(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
934    pub fn Cudd_CheckCube(dd: *mut DdManager, g: *mut DdNode) -> c_int;
935    pub fn Cudd_VarsAreSymmetric(
936        dd: *mut DdManager,
937        f: *mut DdNode,
938        index1: c_int,
939        index2: c_int,
940    ) -> c_int;
941    pub fn Cudd_bddCompose(
942        dd: *mut DdManager,
943        f: *mut DdNode,
944        g: *mut DdNode,
945        v: c_int,
946    ) -> *mut DdNode;
947    pub fn Cudd_addCompose(
948        dd: *mut DdManager,
949        f: *mut DdNode,
950        g: *mut DdNode,
951        v: c_int,
952    ) -> *mut DdNode;
953    pub fn Cudd_addPermute(
954        manager: *mut DdManager,
955        node: *mut DdNode,
956        permut: *mut c_int,
957    ) -> *mut DdNode;
958    pub fn Cudd_addSwapVariables(
959        dd: *mut DdManager,
960        f: *mut DdNode,
961        x: *mut *mut DdNode,
962        y: *mut *mut DdNode,
963        n: c_int,
964    ) -> *mut DdNode;
965    pub fn Cudd_bddPermute(
966        manager: *mut DdManager,
967        node: *mut DdNode,
968        permut: *mut c_int,
969    ) -> *mut DdNode;
970    pub fn Cudd_bddVarMap(manager: *mut DdManager, f: *mut DdNode) -> *mut DdNode;
971    pub fn Cudd_SetVarMap(
972        manager: *mut DdManager,
973        x: *mut *mut DdNode,
974        y: *mut *mut DdNode,
975        n: c_int,
976    ) -> c_int;
977    pub fn Cudd_bddSwapVariables(
978        dd: *mut DdManager,
979        f: *mut DdNode,
980        x: *mut *mut DdNode,
981        y: *mut *mut DdNode,
982        n: c_int,
983    ) -> *mut DdNode;
984    pub fn Cudd_bddAdjPermuteX(
985        dd: *mut DdManager,
986        B: *mut DdNode,
987        x: *mut *mut DdNode,
988        n: c_int,
989    ) -> *mut DdNode;
990    pub fn Cudd_addVectorCompose(
991        dd: *mut DdManager,
992        f: *mut DdNode,
993        vector: *mut *mut DdNode,
994    ) -> *mut DdNode;
995    pub fn Cudd_addGeneralVectorCompose(
996        dd: *mut DdManager,
997        f: *mut DdNode,
998        vectorOn: *mut *mut DdNode,
999        vectorOff: *mut *mut DdNode,
1000    ) -> *mut DdNode;
1001    pub fn Cudd_addNonSimCompose(
1002        dd: *mut DdManager,
1003        f: *mut DdNode,
1004        vector: *mut *mut DdNode,
1005    ) -> *mut DdNode;
1006    pub fn Cudd_bddVectorCompose(
1007        dd: *mut DdManager,
1008        f: *mut DdNode,
1009        vector: *mut *mut DdNode,
1010    ) -> *mut DdNode;
1011    pub fn Cudd_bddApproxConjDecomp(
1012        dd: *mut DdManager,
1013        f: *mut DdNode,
1014        conjuncts: *mut *mut *mut DdNode,
1015    ) -> c_int;
1016    pub fn Cudd_bddApproxDisjDecomp(
1017        dd: *mut DdManager,
1018        f: *mut DdNode,
1019        disjuncts: *mut *mut *mut DdNode,
1020    ) -> c_int;
1021    pub fn Cudd_bddIterConjDecomp(
1022        dd: *mut DdManager,
1023        f: *mut DdNode,
1024        conjuncts: *mut *mut *mut DdNode,
1025    ) -> c_int;
1026    pub fn Cudd_bddIterDisjDecomp(
1027        dd: *mut DdManager,
1028        f: *mut DdNode,
1029        disjuncts: *mut *mut *mut DdNode,
1030    ) -> c_int;
1031    pub fn Cudd_bddGenConjDecomp(
1032        dd: *mut DdManager,
1033        f: *mut DdNode,
1034        conjuncts: *mut *mut *mut DdNode,
1035    ) -> c_int;
1036    pub fn Cudd_bddGenDisjDecomp(
1037        dd: *mut DdManager,
1038        f: *mut DdNode,
1039        disjuncts: *mut *mut *mut DdNode,
1040    ) -> c_int;
1041    pub fn Cudd_bddVarConjDecomp(
1042        dd: *mut DdManager,
1043        f: *mut DdNode,
1044        conjuncts: *mut *mut *mut DdNode,
1045    ) -> c_int;
1046    pub fn Cudd_bddVarDisjDecomp(
1047        dd: *mut DdManager,
1048        f: *mut DdNode,
1049        disjuncts: *mut *mut *mut DdNode,
1050    ) -> c_int;
1051    pub fn Cudd_FindEssential(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode;
1052    pub fn Cudd_bddIsVarEssential(
1053        manager: *mut DdManager,
1054        f: *mut DdNode,
1055        id: c_int,
1056        phase: c_int,
1057    ) -> c_int;
1058    pub fn Cudd_FindTwoLiteralClauses(dd: *mut DdManager, f: *mut DdNode) -> *mut DdTlcInfo;
1059    pub fn Cudd_PrintTwoLiteralClauses(
1060        dd: *mut DdManager,
1061        f: *mut DdNode,
1062        names: *mut *mut c_char,
1063        fp: *mut FILE,
1064    ) -> c_int;
1065    pub fn Cudd_ReadIthClause(
1066        tlc: *mut DdTlcInfo,
1067        i: c_int,
1068        var1: *mut c_uint,
1069        var2: *mut c_uint,
1070        phase1: *mut c_int,
1071        phase2: *mut c_int,
1072    ) -> c_int;
1073    pub fn Cudd_tlcInfoFree(t: *mut DdTlcInfo) -> c_void;
1074    pub fn Cudd_DumpBlif(
1075        dd: *mut DdManager,
1076        n: c_int,
1077        f: *mut *mut DdNode,
1078        inames: *const *const c_char,
1079        onames: *const *const c_char,
1080        mname: *mut c_char,
1081        fp: *mut FILE,
1082        mv: c_int,
1083    ) -> c_int;
1084    pub fn Cudd_DumpBlifBody(
1085        dd: *mut DdManager,
1086        n: c_int,
1087        f: *mut *mut DdNode,
1088        inames: *const *const c_char,
1089        onames: *const *const c_char,
1090        fp: *mut FILE,
1091        mv: c_int,
1092    ) -> c_int;
1093    pub fn Cudd_DumpDot(
1094        dd: *mut DdManager,
1095        n: c_int,
1096        f: *mut *mut DdNode,
1097        inames: *const *const c_char,
1098        onames: *const *const c_char,
1099        fp: *mut FILE,
1100    ) -> c_int;
1101    pub fn Cudd_DumpDaVinci(
1102        dd: *mut DdManager,
1103        n: c_int,
1104        f: *mut *mut DdNode,
1105        inames: *const *const c_char,
1106        onames: *const *const c_char,
1107        fp: *mut FILE,
1108    ) -> c_int;
1109    pub fn Cudd_DumpDDcal(
1110        dd: *mut DdManager,
1111        n: c_int,
1112        f: *mut *mut DdNode,
1113        inames: *const *const c_char,
1114        onames: *const *const c_char,
1115        fp: *mut FILE,
1116    ) -> c_int;
1117    pub fn Cudd_DumpFactoredForm(
1118        dd: *mut DdManager,
1119        n: c_int,
1120        f: *mut *mut DdNode,
1121        inames: *const *const c_char,
1122        onames: *const *const c_char,
1123        fp: *mut FILE,
1124    ) -> c_int;
1125    pub fn Cudd_FactoredFormString(
1126        dd: *mut DdManager,
1127        f: *mut DdNode,
1128        inames: *const *const c_char,
1129    ) -> *mut c_char;
1130    pub fn Cudd_bddConstrain(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode;
1131    pub fn Cudd_bddRestrict(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode;
1132    pub fn Cudd_bddNPAnd(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode;
1133    pub fn Cudd_addConstrain(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode;
1134    pub fn Cudd_bddConstrainDecomp(dd: *mut DdManager, f: *mut DdNode) -> *mut *mut DdNode;
1135    pub fn Cudd_addRestrict(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode;
1136    pub fn Cudd_bddCharToVect(dd: *mut DdManager, f: *mut DdNode) -> *mut *mut DdNode;
1137    pub fn Cudd_bddLICompaction(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode;
1138    pub fn Cudd_bddSqueeze(dd: *mut DdManager, l: *mut DdNode, u: *mut DdNode) -> *mut DdNode;
1139    pub fn Cudd_bddInterpolate(dd: *mut DdManager, l: *mut DdNode, u: *mut DdNode) -> *mut DdNode;
1140    pub fn Cudd_bddMinimize(dd: *mut DdManager, f: *mut DdNode, c: *mut DdNode) -> *mut DdNode;
1141    pub fn Cudd_SubsetCompress(
1142        dd: *mut DdManager,
1143        f: *mut DdNode,
1144        nvars: c_int,
1145        threshold: c_int,
1146    ) -> *mut DdNode;
1147    pub fn Cudd_SupersetCompress(
1148        dd: *mut DdManager,
1149        f: *mut DdNode,
1150        nvars: c_int,
1151        threshold: c_int,
1152    ) -> *mut DdNode;
1153    pub fn Cudd_addHarwell(
1154        fp: *mut FILE,
1155        dd: *mut DdManager,
1156        E: *mut *mut DdNode,
1157        x: *mut *mut *mut DdNode,
1158        y: *mut *mut *mut DdNode,
1159        xn: *mut *mut *mut DdNode,
1160        yn_: *mut *mut *mut DdNode,
1161        nx: *mut c_int,
1162        ny: *mut c_int,
1163        m: *mut c_int,
1164        n: *mut c_int,
1165        bx: c_int,
1166        sx: c_int,
1167        by: c_int,
1168        sy: c_int,
1169        pr: c_int,
1170    ) -> c_int;
1171    pub fn Cudd_Init(
1172        numVars: c_uint,
1173        numVarsZ: c_uint,
1174        numSlots: c_uint,
1175        cacheSize: c_uint,
1176        maxMemory: size_t,
1177    ) -> *mut DdManager;
1178    pub fn Cudd_Quit(unique: *mut DdManager) -> c_void;
1179    pub fn Cudd_PrintLinear(table: *mut DdManager) -> c_int;
1180    pub fn Cudd_ReadLinear(table: *mut DdManager, x: c_int, y: c_int) -> c_int;
1181    pub fn Cudd_bddLiteralSetIntersection(
1182        dd: *mut DdManager,
1183        f: *mut DdNode,
1184        g: *mut DdNode,
1185    ) -> *mut DdNode;
1186    pub fn Cudd_addMatrixMultiply(
1187        dd: *mut DdManager,
1188        A: *mut DdNode,
1189        B: *mut DdNode,
1190        z: *mut *mut DdNode,
1191        nz: c_int,
1192    ) -> *mut DdNode;
1193    pub fn Cudd_addTimesPlus(
1194        dd: *mut DdManager,
1195        A: *mut DdNode,
1196        B: *mut DdNode,
1197        z: *mut *mut DdNode,
1198        nz: c_int,
1199    ) -> *mut DdNode;
1200    pub fn Cudd_addTriangle(
1201        dd: *mut DdManager,
1202        f: *mut DdNode,
1203        g: *mut DdNode,
1204        z: *mut *mut DdNode,
1205        nz: c_int,
1206    ) -> *mut DdNode;
1207    pub fn Cudd_addOuterSum(
1208        dd: *mut DdManager,
1209        M: *mut DdNode,
1210        r: *mut DdNode,
1211        c: *mut DdNode,
1212    ) -> *mut DdNode;
1213    pub fn Cudd_PrioritySelect(
1214        dd: *mut DdManager,
1215        R: *mut DdNode,
1216        x: *mut *mut DdNode,
1217        y: *mut *mut DdNode,
1218        z: *mut *mut DdNode,
1219        Pi: *mut DdNode,
1220        n: c_int,
1221        PiFunc: DD_PRIORITY_FUNCTION,
1222    ) -> *mut DdNode;
1223    pub fn Cudd_Xgty(
1224        dd: *mut DdManager,
1225        N: c_int,
1226        z: *mut *mut DdNode,
1227        x: *mut *mut DdNode,
1228        y: *mut *mut DdNode,
1229    ) -> *mut DdNode;
1230    pub fn Cudd_Xeqy(
1231        dd: *mut DdManager,
1232        N: c_int,
1233        x: *mut *mut DdNode,
1234        y: *mut *mut DdNode,
1235    ) -> *mut DdNode;
1236    pub fn Cudd_addXeqy(
1237        dd: *mut DdManager,
1238        N: c_int,
1239        x: *mut *mut DdNode,
1240        y: *mut *mut DdNode,
1241    ) -> *mut DdNode;
1242    pub fn Cudd_Dxygtdxz(
1243        dd: *mut DdManager,
1244        N: c_int,
1245        x: *mut *mut DdNode,
1246        y: *mut *mut DdNode,
1247        z: *mut *mut DdNode,
1248    ) -> *mut DdNode;
1249    pub fn Cudd_Dxygtdyz(
1250        dd: *mut DdManager,
1251        N: c_int,
1252        x: *mut *mut DdNode,
1253        y: *mut *mut DdNode,
1254        z: *mut *mut DdNode,
1255    ) -> *mut DdNode;
1256    pub fn Cudd_Inequality(
1257        dd: *mut DdManager,
1258        N: c_int,
1259        c: c_int,
1260        x: *mut *mut DdNode,
1261        y: *mut *mut DdNode,
1262    ) -> *mut DdNode;
1263    pub fn Cudd_Disequality(
1264        dd: *mut DdManager,
1265        N: c_int,
1266        c: c_int,
1267        x: *mut *mut DdNode,
1268        y: *mut *mut DdNode,
1269    ) -> *mut DdNode;
1270    pub fn Cudd_bddInterval(
1271        dd: *mut DdManager,
1272        N: c_int,
1273        x: *mut *mut DdNode,
1274        lowerB: c_uint,
1275        upperB: c_uint,
1276    ) -> *mut DdNode;
1277    pub fn Cudd_CProjection(dd: *mut DdManager, R: *mut DdNode, Y: *mut DdNode) -> *mut DdNode;
1278    pub fn Cudd_addHamming(
1279        dd: *mut DdManager,
1280        xVars: *mut *mut DdNode,
1281        yVars: *mut *mut DdNode,
1282        nVars: c_int,
1283    ) -> *mut DdNode;
1284    pub fn Cudd_MinHammingDist(
1285        dd: *mut DdManager,
1286        f: *mut DdNode,
1287        minterm: *mut c_int,
1288        upperBound: c_int,
1289    ) -> c_int;
1290    pub fn Cudd_bddClosestCube(
1291        dd: *mut DdManager,
1292        f: *mut DdNode,
1293        g: *mut DdNode,
1294        distance: *mut c_int,
1295    ) -> *mut DdNode;
1296    pub fn Cudd_addRead(
1297        fp: *mut FILE,
1298        dd: *mut DdManager,
1299        E: *mut *mut DdNode,
1300        x: *mut *mut *mut DdNode,
1301        y: *mut *mut *mut DdNode,
1302        xn: *mut *mut *mut DdNode,
1303        yn_: *mut *mut *mut DdNode,
1304        nx: *mut c_int,
1305        ny: *mut c_int,
1306        m: *mut c_int,
1307        n: *mut c_int,
1308        bx: c_int,
1309        sx: c_int,
1310        by: c_int,
1311        sy: c_int,
1312    ) -> c_int;
1313    pub fn Cudd_bddRead(
1314        fp: *mut FILE,
1315        dd: *mut DdManager,
1316        E: *mut *mut DdNode,
1317        x: *mut *mut *mut DdNode,
1318        y: *mut *mut *mut DdNode,
1319        nx: *mut c_int,
1320        ny: *mut c_int,
1321        m: *mut c_int,
1322        n: *mut c_int,
1323        bx: c_int,
1324        sx: c_int,
1325        by: c_int,
1326        sy: c_int,
1327    ) -> c_int;
1328    pub fn Cudd_Ref(n: *mut DdNode) -> c_void;
1329    pub fn Cudd_RecursiveDeref(table: *mut DdManager, n: *mut DdNode) -> c_void;
1330    pub fn Cudd_IterDerefBdd(table: *mut DdManager, n: *mut DdNode) -> c_void;
1331    pub fn Cudd_DelayedDerefBdd(table: *mut DdManager, n: *mut DdNode) -> c_void;
1332    pub fn Cudd_RecursiveDerefZdd(table: *mut DdManager, n: *mut DdNode) -> c_void;
1333    pub fn Cudd_Deref(node: *mut DdNode) -> c_void;
1334    pub fn Cudd_CheckZeroRef(manager: *mut DdManager) -> c_int;
1335    pub fn Cudd_ReduceHeap(
1336        table: *mut DdManager,
1337        heuristic: Cudd_ReorderingType,
1338        minsize: c_int,
1339    ) -> c_int;
1340    pub fn Cudd_ShuffleHeap(table: *mut DdManager, permutation: *mut c_int) -> c_int;
1341    pub fn Cudd_Eval(dd: *mut DdManager, f: *mut DdNode, inputs: *mut c_int) -> *mut DdNode;
1342    pub fn Cudd_ShortestPath(
1343        manager: *mut DdManager,
1344        f: *mut DdNode,
1345        weight: *mut c_int,
1346        support: *mut c_int,
1347        length: *mut c_int,
1348    ) -> *mut DdNode;
1349    pub fn Cudd_LargestCube(
1350        manager: *mut DdManager,
1351        f: *mut DdNode,
1352        length: *mut c_int,
1353    ) -> *mut DdNode;
1354    pub fn Cudd_ShortestLength(
1355        manager: *mut DdManager,
1356        f: *mut DdNode,
1357        weight: *mut c_int,
1358    ) -> c_int;
1359    pub fn Cudd_Decreasing(dd: *mut DdManager, f: *mut DdNode, i: c_int) -> *mut DdNode;
1360    pub fn Cudd_Increasing(dd: *mut DdManager, f: *mut DdNode, i: c_int) -> *mut DdNode;
1361    pub fn Cudd_EquivDC(
1362        dd: *mut DdManager,
1363        F: *mut DdNode,
1364        G: *mut DdNode,
1365        D: *mut DdNode,
1366    ) -> c_int;
1367    pub fn Cudd_bddLeqUnless(
1368        dd: *mut DdManager,
1369        f: *mut DdNode,
1370        g: *mut DdNode,
1371        D: *mut DdNode,
1372    ) -> c_int;
1373    pub fn Cudd_EqualSupNorm(
1374        dd: *mut DdManager,
1375        f: *mut DdNode,
1376        g: *mut DdNode,
1377        tolerance: CUDD_VALUE_TYPE,
1378        pr: c_int,
1379    ) -> c_int;
1380    pub fn Cudd_bddMakePrime(dd: *mut DdManager, cube: *mut DdNode, f: *mut DdNode) -> *mut DdNode;
1381    pub fn Cudd_bddMaximallyExpand(
1382        dd: *mut DdManager,
1383        lb: *mut DdNode,
1384        ub: *mut DdNode,
1385        f: *mut DdNode,
1386    ) -> *mut DdNode;
1387    pub fn Cudd_bddLargestPrimeUnate(
1388        dd: *mut DdManager,
1389        f: *mut DdNode,
1390        phaseBdd: *mut DdNode,
1391    ) -> *mut DdNode;
1392    pub fn Cudd_CofMinterm(dd: *mut DdManager, node: *mut DdNode) -> *mut c_double;
1393    pub fn Cudd_SolveEqn(
1394        bdd: *mut DdManager,
1395        F: *mut DdNode,
1396        Y: *mut DdNode,
1397        G: *mut *mut DdNode,
1398        yIndex: *mut *mut c_int,
1399        n: c_int,
1400    ) -> *mut DdNode;
1401    pub fn Cudd_VerifySol(
1402        bdd: *mut DdManager,
1403        F: *mut DdNode,
1404        G: *mut *mut DdNode,
1405        yIndex: *mut c_int,
1406        n: c_int,
1407    ) -> *mut DdNode;
1408    pub fn Cudd_SplitSet(
1409        manager: *mut DdManager,
1410        S: *mut DdNode,
1411        xVars: *mut *mut DdNode,
1412        n: c_int,
1413        m: c_double,
1414    ) -> *mut DdNode;
1415    pub fn Cudd_SubsetHeavyBranch(
1416        dd: *mut DdManager,
1417        f: *mut DdNode,
1418        numVars: c_int,
1419        threshold: c_int,
1420    ) -> *mut DdNode;
1421    pub fn Cudd_SupersetHeavyBranch(
1422        dd: *mut DdManager,
1423        f: *mut DdNode,
1424        numVars: c_int,
1425        threshold: c_int,
1426    ) -> *mut DdNode;
1427    pub fn Cudd_SubsetShortPaths(
1428        dd: *mut DdManager,
1429        f: *mut DdNode,
1430        numVars: c_int,
1431        threshold: c_int,
1432        hardlimit: c_int,
1433    ) -> *mut DdNode;
1434    pub fn Cudd_SupersetShortPaths(
1435        dd: *mut DdManager,
1436        f: *mut DdNode,
1437        numVars: c_int,
1438        threshold: c_int,
1439        hardlimit: c_int,
1440    ) -> *mut DdNode;
1441    pub fn Cudd_SymmProfile(table: *mut DdManager, lower: c_int, upper: c_int) -> c_void;
1442    pub fn Cudd_Prime(p: c_uint) -> c_uint;
1443    pub fn Cudd_Reserve(manager: *mut DdManager, amount: c_int) -> c_int;
1444    pub fn Cudd_PrintMinterm(manager: *mut DdManager, node: *mut DdNode) -> c_int;
1445    pub fn Cudd_bddPrintCover(dd: *mut DdManager, l: *mut DdNode, u: *mut DdNode) -> c_int;
1446    pub fn Cudd_PrintDebug(dd: *mut DdManager, f: *mut DdNode, n: c_int, pr: c_int) -> c_int;
1447    pub fn Cudd_PrintSummary(dd: *mut DdManager, f: *mut DdNode, n: c_int, mode: c_int) -> c_int;
1448    pub fn Cudd_DagSize(node: *mut DdNode) -> c_int;
1449    pub fn Cudd_EstimateCofactor(
1450        dd: *mut DdManager,
1451        node: *mut DdNode,
1452        i: c_int,
1453        phase: c_int,
1454    ) -> c_int;
1455    pub fn Cudd_EstimateCofactorSimple(node: *mut DdNode, i: c_int) -> c_int;
1456    pub fn Cudd_SharingSize(nodeArray: *mut *mut DdNode, n: c_int) -> c_int;
1457    pub fn Cudd_CountMinterm(manager: *mut DdManager, node: *mut DdNode, nvars: c_int) -> c_double;
1458    pub fn Cudd_EpdCountMinterm(
1459        manager: *const DdManager,
1460        node: *mut DdNode,
1461        nvars: c_int,
1462        epd: *mut EpDouble,
1463    ) -> c_int;
1464    /*
1465    Type f128 cannot be safely represented in Rust at the moment, and 128-bit bytes don't have
1466    a stable ABI format anyway.
1467
1468    pub fn Cudd_LdblCountMinterm(
1469        manager: *const DdManager,
1470        node: *mut DdNode,
1471        nvars: c_int,
1472    ) -> f128;
1473    */
1474    pub fn Cudd_EpdPrintMinterm(dd: *const DdManager, node: *mut DdNode, nvars: c_int) -> c_int;
1475    pub fn Cudd_CountPath(node: *mut DdNode) -> c_double;
1476    pub fn Cudd_CountPathsToNonZero(node: *mut DdNode) -> c_double;
1477    pub fn Cudd_SupportIndices(
1478        dd: *mut DdManager,
1479        f: *mut DdNode,
1480        indices: *mut *mut c_int,
1481    ) -> c_int;
1482    pub fn Cudd_Support(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode;
1483    pub fn Cudd_SupportIndex(dd: *mut DdManager, f: *mut DdNode) -> *mut c_int;
1484    pub fn Cudd_SupportSize(dd: *mut DdManager, f: *mut DdNode) -> c_int;
1485    pub fn Cudd_VectorSupportIndices(
1486        dd: *mut DdManager,
1487        F: *mut *mut DdNode,
1488        n: c_int,
1489        indices: *mut *mut c_int,
1490    ) -> c_int;
1491    pub fn Cudd_VectorSupport(dd: *mut DdManager, F: *mut *mut DdNode, n: c_int) -> *mut DdNode;
1492    pub fn Cudd_VectorSupportIndex(dd: *mut DdManager, F: *mut *mut DdNode, n: c_int)
1493    -> *mut c_int;
1494    pub fn Cudd_VectorSupportSize(dd: *mut DdManager, F: *mut *mut DdNode, n: c_int) -> c_int;
1495    pub fn Cudd_ClassifySupport(
1496        dd: *mut DdManager,
1497        f: *mut DdNode,
1498        g: *mut DdNode,
1499        common: *mut *mut DdNode,
1500        onlyF: *mut *mut DdNode,
1501        onlyG: *mut *mut DdNode,
1502    ) -> c_int;
1503    pub fn Cudd_CountLeaves(node: *mut DdNode) -> c_int;
1504    pub fn Cudd_bddPickOneCube(
1505        ddm: *mut DdManager,
1506        node: *mut DdNode,
1507        string: *mut c_char,
1508    ) -> c_int;
1509    pub fn Cudd_bddPickOneMinterm(
1510        dd: *mut DdManager,
1511        f: *mut DdNode,
1512        vars: *mut *mut DdNode,
1513        n: c_int,
1514    ) -> *mut DdNode;
1515    pub fn Cudd_bddPickArbitraryMinterms(
1516        dd: *mut DdManager,
1517        f: *mut DdNode,
1518        vars: *mut *mut DdNode,
1519        n: c_int,
1520        k: c_int,
1521    ) -> *mut *mut DdNode;
1522    pub fn Cudd_SubsetWithMaskVars(
1523        dd: *mut DdManager,
1524        f: *mut DdNode,
1525        vars: *mut *mut DdNode,
1526        nvars: c_int,
1527        maskVars: *mut *mut DdNode,
1528        mvars: c_int,
1529    ) -> *mut DdNode;
1530    pub fn Cudd_FirstCube(
1531        dd: *mut DdManager,
1532        f: *mut DdNode,
1533        cube: *mut *mut c_int,
1534        value: *mut CUDD_VALUE_TYPE,
1535    ) -> *mut DdGen;
1536    pub fn Cudd_NextCube(
1537        r#gen: *mut DdGen,
1538        cube: *mut *mut c_int,
1539        value: *mut CUDD_VALUE_TYPE,
1540    ) -> c_int;
1541    pub fn Cudd_FirstPrime(
1542        dd: *mut DdManager,
1543        l: *mut DdNode,
1544        u: *mut DdNode,
1545        cube: *mut *mut c_int,
1546    ) -> *mut DdGen;
1547    pub fn Cudd_NextPrime(r#gen: *mut DdGen, cube: *mut *mut c_int) -> c_int;
1548    pub fn Cudd_bddComputeCube(
1549        dd: *mut DdManager,
1550        vars: *mut *mut DdNode,
1551        phase: *mut c_int,
1552        n: c_int,
1553    ) -> *mut DdNode;
1554    pub fn Cudd_addComputeCube(
1555        dd: *mut DdManager,
1556        vars: *mut *mut DdNode,
1557        phase: *mut c_int,
1558        n: c_int,
1559    ) -> *mut DdNode;
1560    pub fn Cudd_CubeArrayToBdd(dd: *mut DdManager, array: *mut c_int) -> *mut DdNode;
1561    pub fn Cudd_BddToCubeArray(dd: *mut DdManager, cube: *mut DdNode, array: *mut c_int) -> c_int;
1562    pub fn Cudd_FirstNode(dd: *mut DdManager, f: *mut DdNode, node: *mut *mut DdNode)
1563    -> *mut DdGen;
1564    pub fn Cudd_NextNode(r#gen: *mut DdGen, node: *mut *mut DdNode) -> c_int;
1565    pub fn Cudd_GenFree(r#gen: *mut DdGen) -> c_int;
1566    pub fn Cudd_IsGenEmpty(r#gen: *mut DdGen) -> c_int;
1567    pub fn Cudd_IndicesToCube(dd: *mut DdManager, array: *mut c_int, n: c_int) -> *mut DdNode;
1568    pub fn Cudd_PrintVersion(fp: *mut FILE) -> c_void;
1569    pub fn Cudd_AverageDistance(dd: *mut DdManager) -> c_double;
1570    pub fn Cudd_Random(dd: *mut DdManager) -> i32;
1571    pub fn Cudd_Srandom(dd: *mut DdManager, seed: i32) -> c_void;
1572    pub fn Cudd_Density(dd: *mut DdManager, f: *mut DdNode, nvars: c_int) -> c_double;
1573    pub fn Cudd_OutOfMem(size: size_t) -> c_void;
1574    pub fn Cudd_OutOfMemSilent(size: size_t) -> c_void;
1575    pub fn Cudd_zddCount(zdd: *mut DdManager, P: *mut DdNode) -> c_int;
1576    pub fn Cudd_zddCountDouble(zdd: *mut DdManager, P: *mut DdNode) -> c_double;
1577    pub fn Cudd_zddProduct(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
1578    pub fn Cudd_zddUnateProduct(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
1579    pub fn Cudd_zddWeakDiv(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
1580    pub fn Cudd_zddDivide(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
1581    pub fn Cudd_zddWeakDivF(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
1582    pub fn Cudd_zddDivideF(dd: *mut DdManager, f: *mut DdNode, g: *mut DdNode) -> *mut DdNode;
1583    pub fn Cudd_zddComplement(dd: *mut DdManager, node: *mut DdNode) -> *mut DdNode;
1584    pub fn Cudd_zddIsop(
1585        dd: *mut DdManager,
1586        L: *mut DdNode,
1587        U: *mut DdNode,
1588        zdd_I: *mut *mut DdNode,
1589    ) -> *mut DdNode;
1590    pub fn Cudd_bddIsop(dd: *mut DdManager, L: *mut DdNode, U: *mut DdNode) -> *mut DdNode;
1591    pub fn Cudd_MakeBddFromZddCover(dd: *mut DdManager, node: *mut DdNode) -> *mut DdNode;
1592    pub fn Cudd_zddDagSize(p_node: *mut DdNode) -> c_int;
1593    pub fn Cudd_zddCountMinterm(zdd: *mut DdManager, node: *mut DdNode, path: c_int) -> c_double;
1594    pub fn Cudd_zddPrintSubtable(table: *mut DdManager) -> c_void;
1595    pub fn Cudd_zddPortFromBdd(dd: *mut DdManager, B: *mut DdNode) -> *mut DdNode;
1596    pub fn Cudd_zddPortToBdd(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode;
1597    pub fn Cudd_zddReduceHeap(
1598        table: *mut DdManager,
1599        heuristic: Cudd_ReorderingType,
1600        minsize: c_int,
1601    ) -> c_int;
1602    pub fn Cudd_zddShuffleHeap(table: *mut DdManager, permutation: *mut c_int) -> c_int;
1603    pub fn Cudd_zddIte(
1604        dd: *mut DdManager,
1605        f: *mut DdNode,
1606        g: *mut DdNode,
1607        h: *mut DdNode,
1608    ) -> *mut DdNode;
1609    pub fn Cudd_zddUnion(dd: *mut DdManager, P: *mut DdNode, Q: *mut DdNode) -> *mut DdNode;
1610    pub fn Cudd_zddIntersect(dd: *mut DdManager, P: *mut DdNode, Q: *mut DdNode) -> *mut DdNode;
1611    pub fn Cudd_zddDiff(dd: *mut DdManager, P: *mut DdNode, Q: *mut DdNode) -> *mut DdNode;
1612    pub fn Cudd_zddDiffConst(zdd: *mut DdManager, P: *mut DdNode, Q: *mut DdNode) -> *mut DdNode;
1613    pub fn Cudd_zddSubset1(dd: *mut DdManager, P: *mut DdNode, var: c_int) -> *mut DdNode;
1614    pub fn Cudd_zddSubset0(dd: *mut DdManager, P: *mut DdNode, var: c_int) -> *mut DdNode;
1615    pub fn Cudd_zddChange(dd: *mut DdManager, P: *mut DdNode, var: c_int) -> *mut DdNode;
1616    pub fn Cudd_zddSymmProfile(table: *mut DdManager, lower: c_int, upper: c_int) -> c_void;
1617    pub fn Cudd_zddPrintMinterm(zdd: *mut DdManager, node: *mut DdNode) -> c_int;
1618    pub fn Cudd_zddPrintCover(zdd: *mut DdManager, node: *mut DdNode) -> c_int;
1619    pub fn Cudd_zddPrintDebug(zdd: *mut DdManager, f: *mut DdNode, n: c_int, pr: c_int) -> c_int;
1620    pub fn Cudd_zddFirstPath(
1621        zdd: *mut DdManager,
1622        f: *mut DdNode,
1623        path: *mut *mut c_int,
1624    ) -> *mut DdGen;
1625    pub fn Cudd_zddNextPath(r#gen: *mut DdGen, path: *mut *mut c_int) -> c_int;
1626    pub fn Cudd_zddCoverPathToString(
1627        zdd: *mut DdManager,
1628        path: *mut c_int,
1629        str: *mut c_char,
1630    ) -> *mut c_char;
1631    pub fn Cudd_zddSupport(dd: *mut DdManager, f: *mut DdNode) -> *mut DdNode;
1632    pub fn Cudd_zddDumpDot(
1633        dd: *mut DdManager,
1634        n: c_int,
1635        f: *mut *mut DdNode,
1636        inames: *const *const c_char,
1637        onames: *const *const c_char,
1638        fp: *mut FILE,
1639    ) -> c_int;
1640    pub fn Cudd_bddSetPiVar(dd: *mut DdManager, index: c_int) -> c_int;
1641    pub fn Cudd_bddSetPsVar(dd: *mut DdManager, index: c_int) -> c_int;
1642    pub fn Cudd_bddSetNsVar(dd: *mut DdManager, index: c_int) -> c_int;
1643    pub fn Cudd_bddIsPiVar(dd: *mut DdManager, index: c_int) -> c_int;
1644    pub fn Cudd_bddIsPsVar(dd: *mut DdManager, index: c_int) -> c_int;
1645    pub fn Cudd_bddIsNsVar(dd: *mut DdManager, index: c_int) -> c_int;
1646    pub fn Cudd_bddSetPairIndex(dd: *mut DdManager, index: c_int, pairIndex: c_int) -> c_int;
1647    pub fn Cudd_bddReadPairIndex(dd: *mut DdManager, index: c_int) -> c_int;
1648    pub fn Cudd_bddSetVarToBeGrouped(dd: *mut DdManager, index: c_int) -> c_int;
1649    pub fn Cudd_bddSetVarHardGroup(dd: *mut DdManager, index: c_int) -> c_int;
1650    pub fn Cudd_bddResetVarToBeGrouped(dd: *mut DdManager, index: c_int) -> c_int;
1651    pub fn Cudd_bddIsVarToBeGrouped(dd: *mut DdManager, index: c_int) -> c_int;
1652    pub fn Cudd_bddSetVarToBeUngrouped(dd: *mut DdManager, index: c_int) -> c_int;
1653    pub fn Cudd_bddIsVarToBeUngrouped(dd: *mut DdManager, index: c_int) -> c_int;
1654    pub fn Cudd_bddIsVarHardGroup(dd: *mut DdManager, index: c_int) -> c_int;
1655    pub fn Cudd_ReadTree(dd: *mut DdManager) -> *mut MtrNode;
1656    pub fn Cudd_SetTree(dd: *mut DdManager, tree: *mut MtrNode) -> c_void;
1657    pub fn Cudd_FreeTree(dd: *mut DdManager) -> c_void;
1658    pub fn Cudd_ReadZddTree(dd: *mut DdManager) -> *mut MtrNode;
1659    pub fn Cudd_SetZddTree(dd: *mut DdManager, tree: *mut MtrNode) -> c_void;
1660    pub fn Cudd_FreeZddTree(dd: *mut DdManager) -> c_void;
1661    pub fn Cudd_MakeTreeNode(
1662        dd: *mut DdManager,
1663        low: c_uint,
1664        size: c_uint,
1665        mtr_type: c_uint,
1666    ) -> *mut MtrNode;
1667    pub fn Cudd_MakeZddTreeNode(
1668        dd: *mut DdManager,
1669        low: c_uint,
1670        size: c_uint,
1671        mtr_type: c_uint,
1672    ) -> *mut MtrNode;
1673}
cudd_sys/cudd.rs

cudd_sys/
cudd.rs
