source: vis_dev/glu-2.3/src/cmuBdd/bdd.3 @ 84

Last change on this file since 84 was 13, checked in by cecile, 13 years ago

library glu 2.3

File size: 56.3 KB
Line 
1.\" BDD library man page
2.TH BDD 3 "11 June 1993"
3.SH NAME
4bdd \- a binary decision diagram (BDD) package
5.SH SYNOPSIS
6.B #include <bdduser.h>
7.SH DESCRIPTION
8The
9.B libbdd
10library provides a set of routines for manipulating binary decision
11diagrams (BDDs).  Some support is also provided for multi-terminal
12BDDs (MTBDDs).  Programs designed to be used with the library should
13use the
14.B -lbdd -lmem
15options to
16.B cc
17when linking.
18.SH "LIST OF FUNCTIONS"
19.nf
20.ta 3in
21\fIName\fP      \fIFunction\fP
22bdd_init        Initialize the library
23bdd_quit        Finish using the library
24bdd_new_var_first       Create a variable first in the order
25bdd_new_var_last        Create a variable last in the order
26bdd_new_var_before      Create a variable before an existing one
27bdd_new_var_after       Create a variable after an existing one
28bdd_var_with_index      Obtain an existing variable
29bdd_var_with_id Obtain an existing variable
30bdd_one Constant TRUE
31bdd_zero        Constant FALSE
32bdd_and Logical AND
33bdd_nand        Logical NAND
34bdd_or  Logical OR
35bdd_nor Logical NOR
36bdd_xor Logical XOR
37bdd_xnor        Logical XNOR
38bdd_identity    Logical identity
39bdd_not Logical NOT
40bdd_ite Logical IF-THEN-ELSE
41bdd_if  Get the variable of the top node in a BDD
42bdd_then        Get the THEN branch of the top node in a BDD
43bdd_else        Get the ELSE branch of the top node in a BDD
44bdd_if_index    Get the index of the top variable in a BDD
45bdd_if_id       Get a unique ID number for the top variable
46bdd_intersects  Check intersection
47bdd_implies     Check boolean implication
48bdd_new_assoc   Make a new variable association
49bdd_free_assoc  Free a variable association
50bdd_temp_assoc  Set the temporary variable association
51bdd_augment_temp_assoc  Set the temporary variable association
52bdd_assoc       Set the current variable association
53bdd_exists      Existential quantification
54bdd_forall      Universal quantification
55bdd_rel_prod    Relational product
56bdd_compose     Substitute for a variable
57bdd_substitute  Substitute for a set of variables
58bdd_reduce      Simplify given a constraint
59bdd_cofactor    Generalized cofactor
60bdd_depends_on  Determine if a BDD depends on a variable
61bdd_support     Find the support of a BDD
62bdd_satisfy     Find a satisfying assignment
63bdd_satisfy_support     Find a satisfying assignment
64bdd_satisfying_fraction Fraction of valuations satisfying a BDD
65bdd_swap_vars   Swap two variables in a BDD
66bdd_apply2      Generic apply routine
67bdd_apply1      Generic apply routine
68bdd_size        Number of nodes in a BDD
69bdd_size_multiple       Number of nodes in multiple BDDs
70bdd_profile     Node profile of a BDD
71bdd_profile_multiple    Node profile of multiple BDDs
72bdd_function_profile    Function profile of a BDD
73bdd_function_profile_multiple   Function profile of multiple BDDs
74bdd_print_bdd   Print a BDD in human-readable form
75bdd_print_profile       Print a node profile of a BDD
76bdd_print_profile_multiple      Print a profile of multiple BDDs
77bdd_print_function_profile      Print a function profile of a BDD
78bdd_dump_bdd    Write a BDD to a file
79bdd_undump_bdd  Load a BDD from a file
80bdd_type        Classify a BDD
81bdd_free        Decrease the reference count of a BDD
82bdd_unfree      Increase the reference count of a BDD
83bdd_clear_refs  Set all BDD reference counts to zero
84bdd_gc  Garbage collect unused BDD nodes
85bdd_total_size  Total number of BDD nodes in use
86bdd_vars        Total number of variables in existence
87bdd_cache_ratio Get/set operation result cache size
88bdd_node_limit  Get/set the number of BDD nodes allowed
89bdd_overflow    Get/clear overflow flag
90bdd_overflow_closure    Set a closure to invoke on overflow
91bdd_abort_closure       Used to abort operations in progress
92bdd_stats       Print statistics
93bdd_dynamic_reordering  Specify dynamic reordering technique
94bdd_reorder     Invoke dynamic reordering
95bdd_new_var_block       Create variable block
96bdd_var_block_reorderable       Set block reorderability
97mtbdd_free_terminal_closure     Called when freeing an MTBDD terminal
98mtbdd_get_terminal      Get an MTBDD terminal node
99mtbdd_terminal_value    Get the value of an MTBDD terminal node
100mtbdd_ite       IF-THEN-ELSE operation for MTBDDs
101mtbdd_equal     Equality operation for MTBDDs
102mtbdd_transform Applies the current transform to an MTBDD
103mtbdd_transform_closure Called to set the MTBDD transform
104mtbdd_one_data  Sets the MTBDD data value for TRUE
105.fi
106.SH "BASIC CONCEPTS"
107For a general overview of BDDs, see the original article by Bryant
108[1].
109
110Almost all of the BDD library routines require a BDD manager as one of
111their arguments.  A BDD manager is a structure which holds various
112variables used by the BDD routines.  The type
113.B bdd_manager
114is a pointer to this structure.  BDDs themselves are also represented
115internally as structures.  The type
116.B bdd
117is a pointer to one of these structures.
118
119There is a global ordering on the boolean variables which may appear
120in a BDD.  The variable at the root of a BDD is earlier in the
121ordering than all other variables in the BDD.  Each variable has an
122index which represents its position in the ordering;
123.I v1
124appears before
125.I v2
126in the ordering if and only if the index for
127.I v1
128is less than the ordering for \fIv2\fR.  Each variable is also
129assigned a unique ID number that is invariant.  Since variables can be
130created at any position within the order, this is not true for the
131index.  Also, the library supports dynamic variable reordering.  With
132dynamic variable reordering, variables may be shuffled around in the
133middle of an operation in order to reduce the number of BDD nodes in
134use.
135
136Some routines such as
137.B bdd_substitute
138require a mapping from variables to BDDs to operate.  This mapping is
139supplied in the form of a variable association which is a set of
140pairs.  The first element of each pair is the variable, and the second
141element is the BDD that the variable is associated with.  Multiple
142associations may exist at any one time.  Other routines such as
143.B bdd_exists
144require sets of variables.  Sets of variables are represented by
145variable associations where only the fact that a variable is
146associated with some BDD is significant.  There is one association,
147called the temporary variable association, which is special in two
148ways.  First, this association always exists.  Second, results are not
149cached across calls when this association is used.  The temporary
150association is intended for when an association will not be reused.
151The advantage of using it is that setting the temporary association
152does not require scanning the result cache to flush out-of-date
153results.
154
155The results returned by the library represent canonical forms and may
156be checked for equivalence using the standard C comparison operators.
157For example:
158
159.nf
160{
161  bdd_manager bddm;
162  bdd f;
163  ...
164  if (f == bdd_one(bddm))  /* Tautology check */
165    ...
166}
167.fi
168
169For checking for relations such as boolean implication, use
170.B bdd_intersects
171and \fBbdd_implies\fR.
172
173Multi-terminal BDDs are like BDDs, except an MTBDD may have more than
174just the constants TRUE and FALSE at the leaves.  Passing an MTBDD to
175a routine expecting a BDD will give undefined results, except where
176noted below.  MTBDDs are built up using
177.B mtbdd_get_terminal
178and \fBmtbdd_ite\fR.
179.SH "STORAGE MANAGEMENT"
180Each BDD node has an associated reference count which records the
181number of references to the BDD (internal and external).  Whenever a
182BDD is returned from a function, the reference count for its top node
183is incremented.  (If the BDD did not exist before, the reference count
184will be 1.)  Each time a garbage collection occurs, either internally
185or because of a call to \fBbdd_gc\fR, all nodes which are not
186referenced are reclaimed.  The reference count of a BDD may be
187decremented by calling \fBbdd_free\fR.  This should be done whenever
188possible for maximum space efficiency.  You may also specify a limit
189for the total number of BDD nodes using \fBbdd_node_limit\fR.  If it
190is not possible to complete an operation without exceeding this limit,
191the operation is aborted and (by default) a null pointer is returned.
192Whenever this happens, the reference counts of all nodes are restored
193to what they were before the operation.  If a null pointer is passed
194to a routine, the routine simply returns null.  Thus, it is not
195necessary to check for overflows after each operation.  There is also
196an internal flag that indicates whether any operation has caused an
197overflow.  It may be read and reset by \fBbdd_overflow\fR.
198Optionally, a user-defined closure may be invoked when an overflow
199occurs; see \fBbdd_overflow_closure\fR.  Also see \fBbdd_free\fR,
200\fBbdd_unfree\fR, \fBbdd_clear_refs\fR, \fBbdd_node_limit\fR and
201\fBbdd_gc\fR.  The library also includes high-performance replacements
202for
203.B malloc
204and \fBfree\fR.  See the discussion at the end of the section on
205adding new routines.
206.SH "DETAILED DESCRIPTION"
207.B bdd_manager
208.br
209.B bdd_init()
210.in +4
211Creates and initializes a new BDD manager.  Multiple BDD managers may
212exist at any time.
213.LP
214.B void
215.br
216.B bdd_quit(bddm)
217.br
218.B bdd_manager bddm;
219.in +4
220Deallocates the BDD manager given by
221.B bddm
222and all the storage associated with it.
223.LP
224.B bdd
225.br
226.B bdd_new_var_first(bddm)
227.br
228.B bdd_manager bddm;
229.in +4
230Creates a new variable at the start of the BDD variable ordering and
231returns the BDD for it.
232.LP
233.B bdd
234.br
235.B bdd_new_var_last(bddm)
236.br
237.B bdd_manager bddm;
238.in +4
239Creates a new variable at the end of the BDD variable ordering and
240returns the BDD for it.
241.LP
242.B bdd
243.br
244.B bdd_new_var_before(bddm, var)
245.br
246.B bdd_manager bddm;
247.br
248.B bdd var;
249.in +4
250Creates a new variable which is before
251.B var
252in the BDD variable ordering and returns the BDD for the new variable.
253.LP
254.B bdd
255.br
256.B bdd_new_var_after(bddm, var)
257.br
258.B bdd_manager bddm;
259.br
260.B bdd var;
261.in +4
262Creates a new variable which is after
263.B var
264in the BDD variable ordering and returns the BDD for the new variable.
265.LP
266.B bdd
267.br
268.B bdd_var_with_index(bddm, i)
269.br
270.B bdd_manager bddm;
271.br
272.B long i;
273.in +4
274If a variable with index
275.B i
276has been created, returns the BDD for the variable.  If no such
277variable exists, returns null.  See also \fBbdd_if_index\fR.
278.LP
279.B bdd
280.br
281.B bdd_var_with_id(bddm, i)
282.br
283.B bdd_manager bddm;
284.br
285.B long i;
286.in +4
287If a variable with ID
288.B i
289has been created, returns the BDD for the variable.  If no such
290variable has been created, returns null.  See also \fBbdd_if_id\fR.
291.LP
292.B bdd
293.br
294.B bdd_one(bddm)
295.br
296.B bdd_manager bddm;
297.in +4
298Returns the BDD for the constant TRUE.
299.LP
300.B bdd
301.br
302.B bdd_zero(bddm)
303.br
304.B bdd_manager bddm;
305.in +4
306Returns the BDD for the constant FALSE.
307.LP
308.B bdd
309.br
310.B bdd_and(bddm, f, g)
311.br
312.B bdd_manager bddm;
313.br
314.B bdd f, g;
315.in +4
316Returns the BDD for the logical AND of
317.B f
318and \fBg\fR.
319.LP
320.B bdd
321.br
322.B bdd_nand(bddm, f, g)
323.br
324.B bdd_manager bddm;
325.br
326.B bdd f, g;
327.in +4
328Returns the BDD for the logical NAND of
329.B f
330and \fBg\fR.
331.LP
332.B bdd
333.br
334.B bdd_or(bddm, f, g)
335.br
336.B bdd_manager bddm;
337.br
338.B bdd f, g;
339.in +4
340Returns the BDD for the logical OR of
341.B f
342and \fBg\fR.
343.LP
344.B bdd
345.br
346.B bdd_nor(bddm, f, g)
347.br
348.B bdd_manager bddm;
349.br
350.B bdd f, g;
351.in +4
352Returns the BDD for the logical NOR of
353.B f
354and \fBg\fR.
355.LP
356.B bdd
357.br
358.B bdd_xor(bddm, f, g)
359.br
360.B bdd_manager bddm;
361.br
362.B bdd f, g;
363.in +4
364Returns the BDD for the logical XOR of
365.B f
366and \fBg\fR.
367.LP
368.B bdd
369.br
370.B bdd_xnor(bddm, f, g)
371.br
372.B bdd_manager bddm;
373.br
374.B bdd f, g;
375.in +4
376Returns the BDD for the logical XNOR of
377.B f
378and \fBg\fR.
379.LP
380.B bdd
381.br
382.B bdd_identity(bddm, f)
383.br
384.B bdd_manager bddm;
385.br
386.B bdd f;
387.in +4
388Returns the BDD for \fBf\fR.  The only real effect of this function is
389to increase the reference count of \fBf\fR.  Also works with MTBDDs.
390.LP
391.B bdd
392.br
393.B bdd_not(bddm, f)
394.br
395.B bdd_manager bddm;
396.br
397.B bdd f;
398.in +4
399Returns the BDD for the logical NOT of \fBf\fR.
400.LP
401.B bdd
402.br
403.B bdd_ite(bddm, f, g, h)
404.br
405.B bdd_manager bddm;
406.br
407.B bdd f, g, h;
408.in +4
409Returns the BDD for the logical operation IF
410.B f
411THEN
412.B g
413ELSE \fBh\fR.
414.LP
415.B bdd
416.br
417.B bdd_if(bddm, f)
418.br
419.B bdd_manager bddm;
420.br
421.B bdd f;
422.in +4
423Returns the BDD for the variable which labels the root of the BDD
424given by \fBf\fR.  Also works with MTBDDs.  The result is undefined if
425.B f
426is one of the constants TRUE or FALSE or an MTBDD terminal node.
427.LP
428.B bdd
429.br
430.B bdd_then(bddm, f)
431.br
432.B bdd_manager bddm;
433.br
434.B bdd f;
435.in +4
436Returns the BDD for the THEN branch of the root of the BDD given by
437\fBf\fR.  Also works with MTBDDs.  The result is undefined if
438.B f
439is one of the constants TRUE or FALSE or an MTBDD terminal node.
440.LP
441.B bdd
442.br
443.B bdd_else(bddm, f)
444.br
445.B bdd_manager bddm;
446.br
447.B bdd f;
448.in +4
449Returns the BDD for the ELSE branch of the root of the BDD given by
450\fBf\fR.  Also works with MTBDDs.  The result is undefined if
451.B f
452is one of the constants TRUE or FALSE or an MTBDD terminal node.
453.LP
454.B long
455.br
456.B bdd_if_index(bddm, f)
457.br
458.B bdd_manager bddm;
459.br
460.B bdd f;
461.in +4
462Returns the index of the variable which labels the root of the BDD
463given by \fBf\fR.  Also works with MTBDDs.  The result is undefined if
464.B f
465is one of the constants TRUE or FALSE or an MTBDD terminal node.  The
466variable at the start of variable ordering has index 0, the next has
467index 1, etc.  Note that creating new variables may change the index
468of existing variables.  Dynamic reordering may also change the index
469of variables.
470.LP
471.B long
472.br
473.B bdd_if_id(bddm, f)
474.br
475.B bdd_manager bddm;
476.br
477.B bdd f;
478.in +4
479Returns a unique ID number for the variable which labels the root of
480the BDD given by \fBf\fR.  Also works with MTBDDs.  The result is
481undefined if
482.B f
483is one of the constants TRUE or FALSE or an MTBDD terminal node.  The
484ID for a variable is fixed at the time the variable is created and
485never changes after that.
486.LP
487.B bdd
488.br
489.B bdd_intersects(bddm, f, g)
490.br
491.B bdd_manager bddm;
492.br
493.B bdd f, g;
494.in +4
495Computes a BDD that implies the conjunction of
496.B f
497and \fBg\fR.  If the conjunction is not FALSE, then the BDD returned
498will not be FALSE.  Also, the function tries to construct as few new
499nodes as possible.  This routine is intended for cases where you need
500to test for a FALSE conjunction, and, when it the conjunction is not
501FALSE, to obtain just one valuation satisfying both
502.B f
503and \fBg\fR.  A non-FALSE result from
504.B bdd_intersects
505can be passed directly to a routine like \fBbdd_satisfy_support\fR.
506.LP
507.B bdd
508.br
509.B bdd_implies(bddm, f, g)
510.br
511.B bdd_manager bddm;
512.br
513.B bdd f, g;
514.in +4
515This is equivalent to calling
516.B bdd_intersects
517with
518.B f
519and NOT \fBg\fR.
520.LP
521.B int
522.br
523.B bdd_new_assoc(bddm, assoc, pairs)
524.br
525.B bdd_manager bddm;
526.br
527.B bdd *assoc;
528.br
529.B int pairs;
530.in +4
531Creates or finds a variable association.  The association is specified
532by
533.B assoc
534and should be a null-terminated array of BDDs.  If
535.B pairs
536is 0, the array is assumed to be an array of variables.  In this case,
537each variable is paired with the BDD for TRUE.  Such an association
538may essentially be viewed as specifying a set of variables for use
539with routines such as \fBbdd_exists\fR.  If
540.B pairs
541is nonzero, then the even numbered array elements should be variables
542and the odd numbered elements should be the BDDs which they are mapped
543to.  In both cases, the return value is an integer identifier for this
544association.  Note: if the given association is equivalent to one
545which already exists, the same identifier is used for both, and the
546reference count of the association is increased by one.
547.LP
548.B void
549.br
550.B bdd_free_assoc(bddm, id)
551.br
552.B bdd_manager bddm;
553.br
554.B int id;
555.in +4
556Decrements the reference count of the variable association with
557identifier \fBid\fR, and frees it if the reference count becomes zero.
558.LP
559.B void
560.br
561.B bdd_temp_assoc(bddm, assoc, pairs)
562.br
563.B bdd_manager bddm;
564.br
565.B bdd *assoc;
566.br
567.B int pairs;
568.in +4
569Sets the temporary variable association.  The arguments
570.B assoc
571and
572.B pairs
573are as in \fBbdd_new_assoc\fR.
574.LP
575.B void
576.br
577.B bdd_augment_temp_assoc(bddm, assoc, pairs)
578.br
579.B bdd_manager bddm;
580.br
581.B bdd *assoc;
582.br
583.B int pairs;
584.in +4
585Add to the temporary variable association.  The arguments
586.B assoc
587and
588.B pairs
589are as in \fBbdd_new_assoc\fR.  Any existing associations are
590overwritten.  This is mainly used when doing things like substituting
591for all variables in a BDD.  It isn't necessary to clear out the
592temporary association in such cases, so you can save a little time by
593using this routine.
594.LP
595.B int
596.br
597.B bdd_assoc(bddm, id)
598.br
599.B bdd_manager bddm;
600.br
601.B int id;
602.in +4
603Sets the current variable association to the one identified by
604\fBid\fR.  The identifier for the old current association is returned.
605The temporary variable association has identifier -1.
606.LP
607.B bdd
608.br
609.B bdd_exists(bddm, f)
610.br
611.B bdd_manager bddm;
612.br
613.B bdd f;
614.in +4
615Returns the BDD for
616.B f
617with all the variables that are paired with something in the current
618variable association existentially quantified out.
619.LP
620.B bdd
621.br
622.B bdd_forall(bddm, f)
623.br
624.B bdd_manager bddm;
625.br
626.B bdd f;
627.in +4
628Returns the BDD for
629.B f
630with all the variables that are paired with something in the current
631variable association universally quantified out.
632.LP
633.B bdd
634.br
635.B bdd_rel_prod(bddm, f, g)
636.br
637.B bdd_manager bddm;
638.br
639.B bdd f, g;
640.in +4
641Returns the BDD for the logical AND of
642.B f
643and
644.B g
645with all the variables that are paired with something in the current
646variable association existentially quantified out.  If
647.B f
648and
649.B g
650are viewed as boolean relations, this operation corresponds to
651relational product.  This routine is generally much more efficient
652than doing the operations separately.
653.LP
654.B bdd
655.br
656.B bdd_compose(bddm, f, g, h)
657.br
658.B bdd_manager bddm;
659.br
660.B bdd f, g, h;
661.in +4
662Returns the BDD for the substitution of
663.B h
664for the variable
665.B g
666in \fBf\fR.  When
667.B h
668does not depend on \fBg\fR, the operation may be viewed as composition
669of boolean functions.  If
670.B h
671does depend on \fBg\fR, it corresponds to instantaneous substitution
672in a boolean formula.
673.LP
674.B bdd
675.br
676.B bdd_substitute(bddm, f)
677.br
678.B bdd_manager bddm;
679.br
680.B bdd f;
681.in +4
682Returns the BDD for
683.B f
684under a substitution defined by the current variable association.
685Each variable is replaced by its associated BDD.  The substitution is
686effectively simultaneous.
687.LP
688.B bdd
689.br
690.B bdd_reduce(bddm, f, g)
691.br
692.B bdd_manager bddm;
693.br
694.B bdd f, g;
695.in +4
696Returns a BDD which agrees with
697.B f
698for all valuations which satisfy \fBg\fR.  The result is usually
699smaller in terms of number of BDD nodes than \fBf\fR.  This operation
700is typically used in state space searches to simplify the
701representation for the set of states which will be expanded at each
702step.
703.LP
704.B bdd
705.br
706.B bdd_cofactor(bddm, f, g)
707.br
708.B bdd_manager bddm;
709.br
710.B bdd f, g;
711.in +4
712Returns a BDD for the generalized cofactor of
713.B f
714by \fBg\fR.  The BDD indicated by
715.B g
716should not be the constant FALSE.  For some properties of this
717operation, see Touati
718.I et al.
719[2].
720.LP
721.B int
722.br
723.B bdd_depends_on(bddm, f, g)
724.br
725.B bdd_manager bddm;
726.br
727.B bdd f;
728.br
729.B bdd g;
730.in +4
731Returns 1 if the BDD or MTBDD
732.B f
733depends on the variable given by the BDD \fBg\fR, and returns 0
734otherwise.
735.LP
736.B void
737.br
738.B bdd_support(bddm, f, support)
739.br
740.B bdd_manager bddm;
741.br
742.B bdd f;
743.br
744.B bdd *support;
745.in +4
746Stores the support of
747.B f
748as a null-terminated sequence of variables in \fBsupport\fR.  Works
749for MTBDDs also.
750.LP
751.B bdd
752.br
753.B bdd_satisfy(bddm, f)
754.br
755.B bdd_manager bddm;
756.br
757.B bdd f;
758.in +4
759Returns a BDD which is not false, implies \fBf\fR, and has at most one
760BDD node at each level.  The BDD indicated by
761.B f
762should not be the constant FALSE.
763.LP
764.B bdd
765.br
766.B bdd_satisfy_support(bddm, f)
767.br
768.B bdd_manager bddm;
769.br
770.B bdd f;
771.in +4
772Returns a BDD which is not false, implies \fBf\fR, has at most one
773BDD node at each level, and has a node labeled with each variable
774which is paired with something in the current variable association.
775If
776.B f
777is the constant FALSE, the result is undefined.
778.LP
779.B double
780.br
781.B bdd_satisfying_fraction(bddm, f)
782.br
783.B bdd_manager bddm;
784.br
785.B bdd f;
786.in +4
787Returns the fraction of valuations which satisfy \fBf\fR.  If
788.B f
789is a function of
790.I n
791variables, then 2 to the power
792.I n
793times this fraction is the number of valuations which satisfy \fBf\fR.
794.LP
795.B bdd
796.br
797.B bdd_swap_vars(bddm, f, g, h)
798.br
799.B bdd_manager bddm;
800.br
801.B bdd f;
802.br
803.B bdd g;
804.br
805.B bdd h;
806.in +4
807Returns the BDD for
808.B f
809with
810.B g
811substituted for
812.B h
813and
814.B h
815substituted for \fBg\fR.  The substitution is effectively
816simultaneous.
817.LP
818.B bdd
819.br
820.B bdd_apply2(bddm, terminal_fn, f, g, env)
821.br
822.B bdd_manager bddm;
823.br
824.B bdd (*terminal_fn)();
825.br
826.B bdd f;
827.br
828.B bdd g;
829.br
830.B pointer env;
831.in +4
832This is a generic two-argument operation.  The behavior of the
833operation on terminal values is given by \fBterminal_fn\fR.  It should
834take as arguments: the BDD manager, pointers to two BDDs (the
835arguments for the call), and the pointer given by \fBenv\fR.  If the
836value of the call can be determined immediately from the arguments, it
837should return that value.  Otherwise, it should return a null pointer.
838In this case, it may also use the BDD pointers that it received to
839alter the arguments to the call.  A typical use for this ability is to
840put the arguments in a canonical order for commutative operations.
841The function should not alter the reference counts of either the
842arguments or the returned value.  Also, the returned value (if
843non-null) has its temporary reference count incremented once
844automatically.  If your function always returns one of the arguments
845or TRUE or FALSE, this is the right thing and you don't have to worry
846about it.  If you want to call other routines to determine the return
847value, you should read the section on adding new routines below.
848Works with MTBDDs.
849.LP
850.B bdd
851.br
852.B bdd_apply1(bddm, terminal_fn, f, env)
853.br
854.B bdd_manager bddm;
855.br
856.B bdd (*terminal_fn)();
857.br
858.B bdd f;
859.br
860.B pointer env;
861.in +4
862This is a generic one-argument operation.  It is basically like
863\fBbdd_apply2\fR, except that
864.B terminal_fn
865takes a single BDD pointer argument instead of the pair of pointers in
866the two-argument case.  Works with MTBDDs.
867.LP
868.B long
869.br
870.B bdd_size(bddm, f, negout)
871.br
872.B bdd_manager bddm;
873.br
874.B bdd f;
875.br
876.B int negout;
877.in +4
878Returns the number of nodes in \fBf\fR.  The parameter
879.B negout
880is a flag indicating whether negative output pointers should be
881considered.  The library uses this type of pointer flag internally,
882so if the flag is nonzero, the actual number of nodes used is
883returned.  If the flag is zero, the return value is the number of
884nodes which would be needed to represent
885.B f
886using a basic BDD.  Works for MTBDDs too.
887.LP
888.B long
889.br
890.B bdd_size_multiple(bddm, fs, negout)
891.br
892.B bdd_manager bddm;
893.br
894.B bdd *fs;
895.br
896.B int negout;
897.in +4
898Returns the number of nodes in the set of BDDs or MTBDDs given by
899\fBfs\fR, which should be a null-terminated array.  Nodes which are
900shared among the BDDs are only counted once.  The parameter
901.B negout
902is as in \fBbdd_size\fR.
903.LP
904.B void
905.br
906.B bdd_profile(bddm, f, level_counts, negout)
907.br
908.B bdd_manager bddm;
909.br
910.B bdd f;
911.br
912.B long *level_counts;
913.br
914.B int negout;
915.in +4
916Returns the ``node profile'' of \fBf\fR, i.e., the number of nodes at
917each level in \fBf\fR.  The parameter
918.B level_counts
919should be an array of longs of size one plus the number of variables
920in existence (see \fBbdd_vars\fR).  On return, this array holds the
921profile; the \fIi\fRth entry is the number of nodes labeled with the
922variable of index \fIi\fR.  The last entry corresponds to the nodes
923for TRUE and FALSE.  The parameter
924.B negout
925is as in \fBbdd_size\fR.  Works for MTBDDs too; in this case, the
926last entry corresponds to the MTBDD terminal nodes.
927.LP
928.B void
929.br
930.B bdd_profile_multiple(bddm, fs, level_counts, negout)
931.br
932.B bdd_manager bddm;
933.br
934.B bdd* fs;
935.br
936.B long *level_counts;
937.br
938.B int negout;
939.in +4
940Returns the ``node profile'' of the set of BDDs or MTBDDs given by
941\fBfs\fR, which should be a null-terminated array.  The parameters
942\fBlevel_counts\fR and
943.B negout
944are as in \fBbdd_profile\fR.
945.LP
946.B void
947.br
948.B bdd_function_profile(bddm, f, func_counts)
949.br
950.B bdd_manager bddm;
951.br
952.B bdd f;
953.br
954.B long *func_counts;
955.in +4
956Returns the ``function profile'' of \fBf\fR, i.e., the number of
957functions at or below each level in \fBf\fR.  The parameter
958.B func_counts
959should be an array of longs of size one plus the number of variables
960in existence (see \fBbdd_vars\fR).  On return, this array holds the
961profile.  The \fIi\fRth entry corresponds to the number of functions
962which can be obtained by restricting those variables of index less
963than \fIi\fR, provided that
964.B f
965has at least one node labeled with the variable of index \fIi\fR.  If
966.B f
967has no nodes labeled with the variable of index \fIi\fR, then the
968\fIi\fRth entry of the profile is 0.  Works for MTBDDs also.
969.LP
970.B void
971.br
972.B bdd_function_profile_multiple(bddm, fs, func_counts)
973.br
974.B bdd_manager bddm;
975.br
976.B bdd *fs;
977.br
978.B long *func_counts;
979.in +4
980Returns the ``function profile'' of the set of BDDs or MTBDDs given by
981\fBfs\fR, which should be a null-terminated array.  The parameter
982.B func_counts
983is as in \fBbdd_function_profile\fR.
984.LP
985.B void
986.br
987.B bdd_print_bdd(bddm, f, naming_fn, terminal_id_fn, env, fp)
988.br
989.B bdd_manager bddm;
990.br
991.B bdd f;
992.br
993.B char *(*naming_fn)();
994.br
995.B char *(*terminal_id_fn)();
996.br
997.B pointer env;
998.br
999.B FILE *fp;
1000.in +4
1001Prints a human-readable representation of the BDD or MTBDD
1002.B f
1003to the file given by \fBfp\fR.  The
1004.B naming_fn
1005should be a pointer to a function taking a \fBbdd_manager\fR, a
1006.B bdd
1007and the pointer given by \fBenv\fR.  This function should return
1008either a null pointer or a string that is the name of the supplied
1009variable.  If it returns a null pointer, a default name is generated
1010based on the index of the variable.  It is also legal for
1011.B naming_fn
1012to be null; in this case, default names are generated for all variables.
1013The macro
1014.B bdd_naming_fn_none
1015is a null pointer of suitable type.
1016.B terminal_id_fn
1017should be a pointer to a function taking a
1018.B bdd_manager
1019and two longs, plus the pointer given by \fBenv\fR.  It should
1020return either a null pointer or a string representing the MTBDD
1021terminal represented by the given value.  If it returns a null
1022pointer, or if
1023.B terminal_id_fn
1024is null, then default names are generated for the terminals.
1025The macro
1026.B bdd_terminal_id_fn_none
1027is a null pointer of suitable type.
1028.LP
1029.B void
1030.br
1031.B bdd_print_profile(bddm, f, naming_fn, env, width, fp)
1032.br
1033.B bdd_manager bddm;
1034.br
1035.B bdd f;
1036.br
1037.B char *(*naming_fn)();
1038.br
1039.B pointer env;
1040.br
1041.B int width;
1042.br
1043.B FILE *fp;
1044.in +4
1045Prints a node profile of a BDD in histogram form.  The argument
1046.B naming_fn
1047should be as described in \fBbdd_print_bdd\fR.  The width of the
1048output stream is specified by \fBwidth\fR.  This is used to determine
1049how to scale the histogram.
1050.LP
1051.B void
1052.br
1053.B bdd_print_profile_multiple(bddm, fs, naming_fn, env, width, fp)
1054.br
1055.B bdd_manager bddm;
1056.br
1057.B bdd *fs;
1058.br
1059.B char *(*naming_fn)();
1060.br
1061.B pointer env;
1062.br
1063.B int width;
1064.br
1065.B FILE *fp;
1066.in +4
1067Prints a node profile of a set of BDDs, which should be given as a
1068null-terminated array.  The other arguments are as in
1069\fBbdd_print_profile\fR.
1070.LP
1071.B void
1072.br
1073.B bdd_print_function_profile(bddm, f, naming_fn, env, width, fp)
1074.br
1075.B bdd_manager bddm;
1076.br
1077.B bdd f;
1078.br
1079.B char *(*naming_fn)();
1080.br
1081.B pointer env;
1082.br
1083.B int width;
1084.br
1085.B FILE *fp;
1086.in +4
1087Prints a function profile of a BDD in histogram form.  The arguments
1088are the same as those to \fBbdd_print_profile\fR.
1089.LP
1090.B int
1091.br
1092.B bdd_dump_bdd(bddm, f, vars, fp)
1093.br
1094.B bdd_manager bddm;
1095.br
1096.B bdd f;
1097.br
1098.B bdd *vars;
1099.br
1100.B FILE *fp;
1101.in +4
1102Writes an encoded description of the BDD or MTBDD
1103.B f
1104to the file given by \fBfp\fR.  The argument
1105.B vars
1106should be a null-terminated array of variables that include the
1107support of \fBf\fR.  These variables need not be in order of
1108increasing index.  The function returns a nonzero value if
1109.B f
1110was written to the file successfully.
1111.LP
1112.B bdd
1113.br
1114.B bdd_undump_bdd(bddm, vars, fp, error)
1115.br
1116.B bdd_manager bddm;
1117.br
1118.B bdd *vars;
1119.br
1120.B FILE *fp;
1121.br
1122.B int *error;
1123.in +4
1124Loads an encoded description of a BDD or MTBDD from the file given by
1125\fBfp\fR.  The argument
1126.B vars
1127should be a null-terminated array of variables that will become the
1128support of the BDD.  As in \fBbdd_dump_bdd\fR, these need not be in
1129order of increasing index.  If the same array of variables is used in
1130dumping and undumping, the BDD returned will be equal to the one that
1131was dumped.  More generally, if the array
1132.B v1
1133is used when dumping, and the array
1134.B v2
1135is used when undumping, the BDD returned will be equal to the original
1136BDD with the \fIi\fRth variable in
1137.B v2
1138substituted for the \fIi\fRth variable in
1139.B v1
1140for all \fIi\fR.  Null is returned if the operation fails for some
1141reason (node limit reached, I/O error, invalid file format, etc.).
1142In this case, an error code is stored in \fBerror\fR.  The code will
1143be one of the following.
1144.nf
1145.ta 3in
1146\fIValue\fR     \fIMeaning\fR
1147BDD_UNDUMP_FORMAT       Invalid file format
1148BDD_UNDUMP_OVERFLOW     Node limit exceeded
1149BDD_UNDUMP_IOERROR      File I/O error
1150BDD_UNDUMP_EOF  Unexpected EOF
1151.fi
1152.LP
1153.B int
1154.br
1155.B bdd_type(bddm, f)
1156.br
1157.B bdd_manager bddm;
1158.br
1159.B bdd f;
1160.in +4
1161Returns an integer classifying the BDD or MTBDD \fBf\fR.  The possible
1162return values and their meanings are as follows.
1163.nf
1164.ta 3in
1165\fIValue\fR     \fIMeaning\fR
1166BDD_TYPE_OVERFLOW       \fBf\fR is a null pointer
1167BDD_TYPE_ZERO   \fBf\fR is the constant FALSE
1168BDD_TYPE_ONE    \fBf\fR is the constant TRUE
1169BDD_TYPE_CONSTANT       \fBf\fR is an MTBDD constant
1170BDD_TYPE_POSVAR \fBf\fR is a variable
1171BDD_TYPE_NEGVAR \fBf\fR is the negation of a variable
1172BDD_TYPE_NONTERMINAL    \fBf\fR is not one of the above
1173.fi
1174.LP
1175.B void
1176.br
1177.B bdd_free(bddm, f)
1178.br
1179.B bdd_manager bddm;
1180.br
1181.B bdd f;
1182.in +4
1183Decreases the reference count of
1184.B f
1185by one.  When the reference count of a BDD or MTBDD node reaches 0,
1186the node and any of its children that are not otherwise referenced may
1187eventually be garbage collected and reused.  Intermediate results and
1188unused BDDs and MTBDDs should be freed whenever possible.  For
1189example:
1190
1191.nf
1192bdd
1193f_or_g_and_h(bddm, f, g, h)
1194     bdd_manager bddm;
1195     bdd f, g, h;
1196{
1197  bdd temp, result;
1198  temp=bdd_and(bddm, g, h);
1199  result=bdd_or(bddm, f, temp);
1200  bdd_free(bddm, temp);    /* Free intermediate */
1201  return (result);
1202}
1203.fi
1204.LP
1205.B void
1206.br
1207.B bdd_unfree(bddm, f)
1208.br
1209.B bdd_manager bddm;
1210.br
1211.B bdd f;
1212.in +4
1213Increases the reference count of
1214.B f
1215by one.  This is usually used in conjunction with
1216\fBbdd_clear_refs\fR.  Works with MTBDDs.
1217.LP
1218.B void
1219.br
1220.B bdd_clear_refs(bddm)
1221.br
1222.B bdd_manager bddm;
1223.in +4
1224Sets the reference counts of all BDD and MTBDD nodes (except for the
1225node for TRUE/FALSE) to 0.  Calling this routine and then immediately
1226calling
1227.B bdd_unfree
1228on a set of BDDs has the effect of disposing of all BDDs except those
1229in the set.
1230.LP
1231.B void
1232.br
1233.B bdd_gc(bddm)
1234.br
1235.B bdd_manager bddm;
1236.in +4
1237Forces a BDD garbage collection; all nodes not reachable from a node
1238with a nonzero reference count are disposed of.  (Garbage collections
1239also occur internally at various times.)
1240.LP
1241.B long
1242.br
1243.B bdd_total_size(bddm)
1244.br
1245.B bdd_manager bddm;
1246.in +4
1247Returns the number of BDD and MTBDD nodes in existence (including
1248those which are eligible for garbage collection).
1249.LP
1250.B long
1251.br
1252.B bdd_vars(bddm)
1253.br
1254.B bdd_manager bddm;
1255.in +4
1256Returns the number of variables in existence.
1257.LP
1258.B int
1259.br
1260.B bdd_cache_ratio(bddm, ratio)
1261.br
1262.B bdd_manager bddm;
1263.br
1264.B int ratio;
1265.in +4
1266Sets the BDD operation cache size ratio to
1267.B ratio
1268and returns the old cache size ratio.  The number of cache entries is
1269constrained to be (roughly) less than the cache size ratio divided by
127016 times the number of BDD nodes in existence.  The default size ratio
1271is 4, which gives about 1 cache entry per 4 BDD nodes.  The amount of
1272memory required per node will be about 17+(\fBratio\fR/16)*20 bytes on
1273a machine with 32-bit words.
1274.LP
1275.B void
1276.br
1277.B bdd_node_limit(bddm, limit)
1278.br
1279.B bdd_manager bddm;
1280.br
1281.B long limit;
1282.in +4
1283Sets the number of allowed BDD nodes to
1284.B limit
1285and returns the old limit.  A value of 0 specifies no limit.  If in
1286the course of an operation, the number of nodes reaches the limit, an
1287internal garbage collection takes place.  If this does not free enough
1288nodes to continue, the operation is aborted and a null value is
1289returned.  When dynamic reordering is used to shift around large
1290variable block, this limit may be exceeded during reordering.
1291.LP
1292.B int
1293.br
1294.B bdd_overflow(bddm)
1295.br
1296.B bdd_manager bddm;
1297.in +4
1298Returns 1 if any operation has caused an overflow in the number of
1299nodes, and 0 otherwise.  Calling this routine clears the internal
1300overflow flag, so subsequent calls will return 0 until the next
1301overflow occurs.
1302.LP
1303.B void
1304.br
1305.B bdd_overflow_closure(bddm, overflow_fn, overflow_env)
1306.br
1307.B bdd_manager bddm;
1308.br
1309.B void (*overflow_fn)();
1310.br
1311.B pointer overflow_env;
1312.in +4
1313Sets the closure to invoke when an overflow occurs.  The function
1314given by
1315.B overflow_fn
1316will be invoked as the last stage in the cleanup after the overflow.
1317The function is passed the BDD manager and the pointer given by
1318\fBoverflow_env\fR.  Typically, the function will jump to a
1319user-provided error recovery routine.
1320.LP
1321.B void
1322.br
1323.B bdd_abort_closure(bddm, abort_fn, abort_env)
1324.br
1325.B bdd_manager bddm;
1326.br
1327.B void (*abort_fn)();
1328.br
1329.B pointer abort_env;
1330.in +4
1331Sets a closure to invoke when the next node creation is attempted.
1332All temporary results will be cleaned up just before the function
1333given by
1334.B abort_fn
1335is called.  The function is passed the BDD manager and the pointer
1336given by \fBabort_env\fR.  Typically, the function will jump to a
1337user-provided error recovery routine.  This functionality is intended
1338to be used to cleanly interrupt BDD operations.  Typically,
1339.B bdd_abort_closure
1340will be called within a signal handler.
1341.LP
1342.B void
1343.br
1344.B bdd_stats(bddm, fp)
1345.br
1346.B bdd_manager bddm;
1347.br
1348.B FILE *fp;
1349.in +4
1350Prints some statistics to the file given by \fBfp\fR.
1351.LP
1352.B void
1353.br
1354.B bdd_dynamic_reordering(bddm, reorder_fn)
1355.br
1356.B bdd_manager bddm;
1357.br
1358.B void (*reorder_fn)();
1359.in +4
1360Selects the method for dynamic reordering.  When dynamic reordering is
1361being used, the library may attempt to rearrange the BDD variable
1362ordering in the midst of an operation so as to reduce the number of
1363nodes in use.  There are currently two available reordering methods.
1364The first, \fBbdd_reorder_stable_window3\fR, permutes the variables
1365within windows of three adjacent variables so as to minimize the
1366overall BDD size.  This process is repeated until no more reduction in
1367size occurs.  The second method, \fBbdd_reorder_sift\fR, moves each
1368variable throughout the order to find an optimal position for that
1369variable (assuming all other variables are fixed).  This generally
1370achieves greater size reductions than the window-based method, but is
1371slower.  The
1372.B reorder_fn
1373may also be
1374.B bdd_reorder_none
1375(an appropriately cast null pointer), in which case dynamic reordering
1376is turned off.  Also see the discussion on variable blocks in
1377\fBbdd_new_var_block\fR.
1378.LP
1379.B void
1380.br
1381.B bdd_reorder(bddm)
1382.br
1383.B bdd_manager bddm;
1384.in +4
1385Invoke the current dynamic reordering method.
1386.LP
1387.B block
1388.br
1389.B bdd_new_var_block(bddm, v, n)
1390.br
1391.B bdd_manager bddm;
1392.br
1393.B bdd v;
1394.br
1395.B long n;
1396.in +4
1397Groups the variable
1398.B v
1399and the \fBn\fR-1 variables after it in the ordering into a single
1400block for purposes of dynamic reordering.  The purpose of blocks is to
1401provide control over the possible orders that dynamic reordering will
1402consider.  In general, the variable blocks form a hierarchy.  For
1403example, a block consisting of the variables with indexes 0 through 3
1404might be made up of two sub-blocks, one for the variables with index 0
1405and 1, and one for the variables with index 2 and 3.  When dynamic
1406reordering is invoked, it is actually applied to each block within the
1407hierarchy.  Reordering a block involves shuffling around the
1408sub-blocks within it.  Thus, dynamic reordering actually moves groups
1409of variables rather than single variables.  If you know that a group
1410of variables should be together in the ordering, you should collect
1411them together into a block.  As an example, in BDD-based sequential
1412verification algorithms, the variables representing the current state
1413and next state of a state-holding element should generally be adjacent
1414in a good ordering.  By grouping these variables into a block, we can
1415ensure that only orderings with this property are considered.  After a
1416block has been reordered, each sub-block within it is recursively
1417reordered as well.  You can also specify that certain blocks should
1418not be reordered (see
1419.B bdd_var_block_reorderable
1420below).
1421.LP
1422.B void
1423.br
1424.B bdd_var_block_reorderable(bddm, b, reorderable)
1425.br
1426.B bdd_manager bddm;
1427.br
1428.B block b;
1429.br
1430.B int reorderable;
1431.in +4
1432If
1433.B reorderable
1434is non-zero, turns on reordering for the given block, otherwise turns
1435it off.  By default, blocks are not reorderable.  As an example,
1436suppose we are building the BDDs representing a circuit with distinct
1437control and data path.  In such a case, we typically want to have the
1438control variables at the top of the ordering.  For the data path, we
1439probably want to have the variables for each bit slice grouped
1440together, and we want the bit slices to be ordered from
1441most-significant to least-significant.  However, we want to allow
1442reordering within the control part and within each slice.  To do this,
1443we create the variables in the following order: control variables
1444first, down to LSB slice variables.  Then we create separate variable
1445blocks for the control part and for each slice.  We then turn on
1446reordering for these blocks.  Next, we create a block containing all
1447of the variables, and we leave reordering off for this block.  When
1448dynamic reordering is invoked, it will rearrange the control variables
1449and the variables within each slice, but will not move the control
1450variables or the slices in relation to each other.
1451.LP
1452.B void
1453.br
1454.B bdd_free_terminal_closure(bddm, free_terminal_fn, free_terminal_env)
1455.br
1456.B bdd_manager bddm;
1457.br
1458.B void (*free_terminal_fn)();
1459.br
1460.B pointer free_terminal_env;
1461.in +4
1462Sets a closure to invoke when freeing an MTBDD terminal node.  The
1463function receives the BDD manager, two longs representing the value of
1464the terminal, and the pointer given by \fBfree_terminal_env\fR.  If
1465you using the terminal value to hold pointers to other data
1466structures, you can set up this routine to free those structures.
1467.LP
1468.B bdd
1469.br
1470.B mtbdd_get_terminal(bddm, value1, value2)
1471.br
1472.B bdd_manager bddm;
1473.br
1474.B long value1;
1475.br
1476.B long value2;
1477.in +4
1478Creates an MTBDD terminal node corresponding to the value given by
1479.B value1
1480and \fBvalue2\fR.  If a terminal node with the value already exists,
1481its reference count is increased.  See also
1482\fBbdd_free_terminal_closure\fR.
1483.LP
1484.B void
1485.br
1486.B mtbdd_terminal_value(bddm, f, value1, value2)
1487.br
1488.B bdd_manager bddm;
1489.br
1490.B bdd f;
1491.br
1492.B long *value1;
1493.br
1494.B long *value2;
1495.in +4
1496.B f
1497should be an MTBDD terminal node.  The value of the node is stored in
1498.B value1
1499and \fBvalue2\fR.
1500.LP
1501.B bdd
1502.br
1503.B mtbdd_ite(bddm, f, g, h)
1504.br
1505.B bdd_manager bddm;
1506.br
1507.B bdd f;
1508.br
1509.B bdd g;
1510.br
1511.B bdd h;
1512.in +4
1513.B f
1514should be a BDD and
1515.B g
1516and
1517.B h
1518should be MTBDDs.  Returns the MTBDD for the operation IF
1519.B f
1520THEN
1521.B g
1522ELSE \fBh\fR.
1523.LP
1524.B bdd
1525.br
1526.B mtbdd_substitute(bddm, f)
1527.br
1528.B bdd_manager bddm;
1529.br
1530.B bdd f;
1531.in +4
1532Does the analog of
1533.B bdd_substitute
1534for the MTBDD \fBf\fR.  The elements in the variable association must
1535be BDDs.
1536.LP
1537.B bdd
1538.br
1539.B mtbdd_equal(bddm, f, g)
1540.br
1541.B bdd_manager bddm;
1542.br
1543.B bdd f;
1544.br
1545.B bdd g;
1546.in +4
1547Returns the BDD which is true for those valuations on which the MTBDDs
1548.B f
1549and
1550.B g
1551are equal.  That is, this is the analog of a logical XNOR for MTBDDs.
1552.LP
1553.B bdd
1554.br
1555.B mtbdd_transform(bddm, f)
1556.br
1557.B bdd_manager bddm;
1558.br
1559.B bdd f;
1560.in +4
1561Conceptually applies the user-defined transform to all terminals of
1562the specified MTBDD.  (This is actually done by just flipping the
1563pointer flag, so this routine is really a macro for \fBbdd_not\fR.)
1564See \fBmtbdd_transform_closure\fR.
1565.LP
1566.B void
1567.br
1568.B mtbdd_transform_closure(bddm, canonical_fn, transform_fn, env)
1569.br
1570.B bdd_manager bddm;
1571.br
1572.B int (*canonical_fn)();
1573.br
1574.B void (*transform_fn)();
1575.br
1576.B pointer env;
1577.in +4
1578Sets the MTBDD terminal transformation closure.  Currently in the
1579library, the pointer representing a boolean function and the pointer
1580representing the negation of that function are identical except for
1581the low-order bit.  Complementing a function is done by simply
1582toggling that bit.  The MTBDD terminal transformation allows this
1583mechanism to be extended to MTBDDs.  Whenever a terminal is created,
1584.B canonical_fn
1585will be called.  It is passed the BDD manager, two longs representing
1586the terminal being created, and the pointer given by \fBenv\fR.  The
1587function should return zero if the value is already canonical, and a
1588non-zero result if it needs to be transformed.  If the value needs to
1589be transformed, then
1590.B transform_fn
1591will be called, with the BDD manager, two longs representing the value
1592to be transformed, pointers to two longs to hold the result, and the
1593pointer given by \fBenv\fR.  The actual terminal node that is created
1594will contain the transformed value.  The original terminal requested
1595will be represented by a pointer to this node, with the low-order bit
1596of the pointer set.  Also see \fBmtbdd_one_data\fR.  If you are going
1597to call this function, you should do it before creating any MTBDD
1598terminals.
1599.LP
1600.B void
1601.br
1602.B mtbdd_one_data(bddm, value1, value2)
1603.br
1604.B bdd_manager bddm;
1605.br
1606.B long value1;
1607.br
1608.B long value2;
1609.in +4
1610If you are planning to use MTBDDs that contain TRUE and FALSE as well
1611as other values, you may need to use this function to set the MTBDD
1612value for the node representing TRUE.  In this case, also keep in mind
1613that the when the transformation function is applied to this value, it
1614should yield the value that you want for FALSE.  Also, the value for
1615TRUE should be regarding as canonical, i.e., TRUE must be represented
1616by a pointer with the low-order bit cleared.  As an example, suppose
1617that we are planning to use MTBDDs to represent spectral transforms of
1618boolean functions [4].  In this case, the MTBDD terminal values will
1619conceptually be integers.  Further, it is convenient for TRUE to be
1620represented by the value -1, and FALSE to be represented by +1.  We
1621will represent terminal values using two longs, with the first long
1622representing the most-significant part of the integer.  We will also
1623assume a 2's complement representation, so TRUE should be represented
1624by the data values -1 and -1.  Since the value for FALSE is the
1625negation of that for TRUE, we will have our transform function
1626represent integer negation.  Also, since we want the value for TRUE to
1627be canonical, we will regard nonnegative values as canonical.  Thus,
1628we define
1629
1630.nf
1631int
1632canonical_fn(bddm, value1, value2, env)
1633     bdd_manager bddm;
1634     long value1;
1635     long value2;
1636     pointer env;
1637{
1638  return (value1 > 0 || (!value1 && value2 > 0));
1639}
1640
1641void
1642transform_fn(bddm, value1, value2, result1, result2, env)
1643     bdd_manager bddm;
1644     long value1;
1645     long value2;
1646     long *result1;
1647     long *result2;
1648     pointer env;
1649{
1650  if (!value2)
1651    /* Will be a carry when taking 2's complement of value2.  Thus, */
1652    /* take 2's complement of high part. */
1653    value1= -value1;
1654  else
1655    {
1656      value2= -value2;
1657      value1= ~value1;
1658    }
1659  *result1=value1;
1660  *result2=value2;
1661}
1662.fi
1663
1664We then call
1665.B mtbdd_transform_closure
1666to register these functions, and use
1667
1668.nf
1669bdd_one_data(bddm, -1l, -1l);
1670.fi
1671
1672to set the value for TRUE to -1.  (The default canonical checking and
1673transformation functions and the default MTBDD values for TRUE and
1674FALSE are actually as given in this example.)  If you are going to
1675call \fBbdd_one_data\fR, you should do it before creating any MTBDD
1676terminals.
1677.SH "ADDING NEW ROUTINES"
1678If you want to add new routines to the library, you would be
1679well-advised to look at some of the existing ones to get a feel for
1680how they operate.  Good ones include \fBbdd_ite\fR (the basic logical
1681operation) and \fBbdd_exists\fR (a routine using variable
1682associations).  Some basic points are explained below.  To get the
1683declarations of the internal library data structures and routines, you
1684should
1685.B #include <bddint.h>
1686instead of using \fBbdduser.h\fR.  You will probably want to study
1687this file to become familiar with the data structures.
1688
1689Pointers to BDD nodes and cache entries are tagged using the low three
1690bits of the pointer.  Because of this, all structures must be aligned
1691on eight byte boundaries.  The storage allocation routines guarantee
1692this alignment.  The tag field of a tagged pointer is extracted with
1693the
1694.B TAG
1695macro.  The
1696.B POINTER
1697macro masks off the tag to get the actual pointer.  If the pointer is
1698a pointer to a BDD node, you can use
1699.B BDD_POINTER
1700instead; this just casts the result to a
1701.B bdd
1702after masking off the tag.  The tag can be set using \fBSET_TAG\fR, and
1703individual tag bits can be manipulated with \fBTAG0\fR,
1704.B FLIP_TAG0
1705and \fBSET_TAG0\fR for tag bit 0, and the analogous macros for tag
1706bits 1 and 2.  More commonly, slightly higher level macros are used
1707for manipulating tags.  For BDD nodes, there is only one tag bit that
1708is actually used.  When it is set, it indicates the pointer should be
1709interpreted as representing the complement of the node that it points
1710to.  (Or for MTBDDs, that it should be interpreted as transformed
1711using the user-definable transformation function).  There are macros
1712for testing, clearing, and flipping the negation flag.
1713
1714Before using the macros below on a pointer \fBf\fR, you need to use
1715\fBBDD_SETUP(f)\fR.  This actually declares a new variable to hold the
1716masked pointer \fBBDD_POINTER(f)\fR.  Hence, it needs to be placed at
1717some point where a variable declaration could legally go.  If you
1718change \fBf\fR, you can reset this internal variable using
1719\fBBDD_RESET\fR.
1720
1721BDD pointers are generally manipulated using the following macros.
1722Below, ``node'' refers to the node referenced by the pointer.
1723.LP
1724.B BDD_IS_CONST
1725.in +4
1726Tests if the node represents the constant TRUE or FALSE or an MTBDD
1727terminal node.
1728.LP
1729.B BDD_INDEX
1730.in +4
1731Returns the index of the node, or
1732.B BDD_MAX_INDEX
1733if given a constant node.
1734.LP
1735.B BDD_INDEXINDEX
1736.in +4
1737Returns the index index of a node.  This field is the value returned
1738by \fBbdd_if_id\fR and is invariant; when you create a new variable,
1739the index of old nodes may change, but the index index stays the same.
1740When you call \fBbdd_find\fR, you pass the desired index index of the
1741new node, not the index.
1742.LP
1743.B BDD_NOT
1744.in +4
1745Flips the negation flag on a pointer.
1746.LP
1747.B BDD_THEN, BDD_ELSE
1748.in +4
1749Return the THEN and ELSE pointers of a node, taking proper account of
1750pointer flags.  These are used for doing Shannon expansions on a node.
1751.LP
1752.B BDD_TOP_VAR2
1753Takes a \fBbdd_manager\fR, a variable that can hold an index index,
1754and two \fBbdd\fRs.  Sets the index index variable to the index index
1755of the variable with the lowest index among the variables at the roots
1756of the BDDs.  This index index can then be used with...
1757.LP
1758.B BDD_COFACTOR
1759Takes an index index, a BDD, and two variables of type \fBbdd\fR, and
1760sets the two variables either to the original BDD or to the cofactors
1761of the original BDD with respect to its top variable, depending on
1762whether the index index of the first BDD matches that specified.  You
1763can do a Shannon expansion on the top variable of two BDDs by using
1764.B BDD_TOP_VAR2
1765to get the index index of the highest variable and then using
1766.B BDD_COFACTOR
1767to take the appropriate cofactors.
1768.LP
1769.B BDD_MARK
1770.in +4
1771Accesses the mark field of a node.  This expands to a l-value, so you
1772can set the mark with this as well.  (But see BDD_TEMP_REFS below.)
1773.LP
1774.B BDD_ONE, BDD_ZERO
1775.in +4
1776Take a BDD manager and give back the BDDs for TRUE and FALSE.
1777.LP
1778.B BDD_REFS
1779.in +4
1780Accesses the reference count field of a node.
1781.LP
1782.B BDD_INCREFS, BDD_DECREFS
1783.in +4
1784Increment and decrement the reference count.
1785.LP
1786.B BDD_TEMP_REFS
1787.in +4
1788Accesses the temporary reference count field of a node.  The temporary
1789reference count and the mark actually share storage, so you can't use
1790both at once!  That is, unless you are very clever, you can't write a
1791routine that builds temporary nodes and uses the marks.
1792.LP
1793.B BDD_TEMP_INCREFS, BDD_TEMP_DECREFS
1794.in +4
1795Increment and decrement the temporary reference count.
1796.LP
1797
1798New BDD nodes are created using \fBbdd_find\fR.  This routine takes a
1799BDD manager, an index index, and two subBDDs as arguments.  New MTBDD
1800terminals can be created with \fBbdd_find_terminal\fR.  The result
1801cache is manipulated using the
1802.B bdd_lookup_in_cache
1803and
1804.B bdd_insert_in_cache
1805routines.  There are different versions of these routines depending on
1806exactly what is being cached.  The basic ones are
1807\fBbdd_lookup_in_cache31\fR and \fBbdd_insert_in_cache31\fR.
1808The first of these takes a cache entry type (CACHE_TYPE_ITE,
1809CACHE_TYPE_TWO, etc.), three arguments of unspecified type (passed as
1810longs), and a pointer to an unspecified type of result (a pointer to a
1811long).  It returns a nonzero result if the lookup succeeds.  The
1812corresponding insert routine is similar except that the result is
1813passed in as a long, and nothing is returned.  There are similar
1814functions that are for routines that take two arguments and return two
1815results (or a single double-word result), or for routines that take
1816one argument and return three results.  There are also macros such as
1817\fBbdd_lookup_in_cache2\fR that are wrappers for things like
1818two-argument functions, etc.  In general, some action must be taken
1819when results are returned from the cache, when entries are purged from
1820the cache, when entries are garbage collected, and when a variable
1821association ID is reclaimed.  For the built-in cache entry types,
1822these actions are done automatically.  For example, when a BDD is
1823returned from an entry with CACHE_TYPE_TWO, the temporary reference
1824count of the BDD is incremented.  Some of the entry types are
1825available for customization.  The actions to take for these entry
1826types are specified by calling \fBbdd_cache_functions\fR.  This
1827function takes a BDD manager, an integer between 1 and 3 specifying
1828the number of arguments you want to cache on, and four function
1829pointers.  When returning a result, purging an entry, garbage
1830collecting, or reclaiming an association ID, these functions are
1831called.  The first three functions are passed the BDD manager and the
1832entry.  (The tag bits will have already been masked off the entry
1833pointer.)  The last receives these plus the association ID being freed
1834(cast to a pointer).  The garbage collection function should return a
1835nonzero result if the entry should be garbage collected.  If the entry
1836contains some BDD nodes, they should be tested with \fBBDD_IS_USED\fR.
1837The function called when an association ID is reclaimed should return
1838a nonzero result if the entry should be flushed from the cache.  This
1839function and the purge function and return functions may be null,
1840specifying that no action need be taken.  \fBbdd_cache_functions\fR
1841returns an integer that represents a tag to use with the cache
1842insertion and lookup routines, or -1 if there are no more free tags
1843available.  The routine \fBbdd_free_cache_tag\fR makes a tag available
1844again.
1845
1846Routines that build new BDD nodes must take into account the
1847possibility of running into the node limit.  The package is set up to
1848make this easy if you use the following strategy.  Organize your
1849routine as a top-level (user-callable) procedure and an internal
1850procedure for performing the actual computation.  The top-level
1851procedure should check its arguments before calling the internal
1852routine.  The
1853.B bdd_check_arguments
1854function can be used to test for null arguments (indicating a prior
1855overflow) or arguments with a zero reference count (indicating a bug).
1856It should also use the
1857.B FIREWALL
1858macro to set up an overflow trap.  The internal routine should use
1859temporary reference counts to keep track of the nodes it is using.
1860When a node is returned from the internal routine, increment its
1861temporary reference count once.  (You don't have to do this for the
1862constants or for variables, since they can't be garbage collected.)
1863When you pass a node to \fBbdd_find\fR, its temporary reference count
1864is decremented once automatically, and its reference count is
1865incremented.  Also, the result of \fBbdd_find\fR has its temporary
1866reference count incremented once automatically.  Hence, if you your
1867routine has the standard organization (Shannon's expansion followed by
1868\fBbdd_find\fR on the subresults), you usually don't have to worry
1869about incrementing or decrementing the reference counts yourself.  If
1870you don't use a subresult, or if you want a subresult to stick around
1871after calling \fBbdd_find\fR, you'll have to do the appropriate
1872twiddling.  When the internal routine finally returns, you should have
1873a BDD with a single temporary reference count.  Use
1874.B RETURN_BDD
1875to convert this temporary reference count to an external one and
1876return the result to the user.  If you follow this strategy, you won't
1877have to deal with overflow; when the node limit is reached,
1878\fBbdd_find\fR will try garbage collecting, and if that doesn't work,
1879will call the overflow trap set up by \fBFIREWALL\fR.  The overflow
1880trap handler will automatically zero all temporary reference counts
1881and return a null pointer to the user.  Note: if you want to call
1882other routines, such as the IF-THEN-ELSE routine, within your internal
1883procedure, you should call the internal procedure for the routine.
1884That way, the overflow handler will give control back to the user
1885if the routine you are calling causes an overflow.
1886
1887A typical routine looks like:
1888
1889.nf
1890bdd
1891foo_step(bddm, f, g)
1892     bdd_manager bddm;
1893     bdd f, g;
1894{
1895  bdd_indexindex_type top_indexindex;
1896  bdd f1, f2;
1897  bdd g1, g2;
1898  bdd temp1, temp2;
1899  bdd result;
1900 
1901  BDD_SETUP(f);
1902  BDD_SETUP(g);
1903  if (<terminal case>)
1904    {
1905      BDD_TEMP_INCREFS(f);
1906      return (f);
1907    }
1908  if (bdd_lookup_in_cache2(bddm, <op>, f, g, &result))
1909    return (result);
1910  BDD_TOP_VAR2(top_indexindex, bddm, f, g);
1911  BDD_COFACTOR(top_indexindex, f, f1, f2);
1912  BDD_COFACTOR(top_indexindex, g, g1, g2);
1913  temp1=foo_step(bddm, f1, g1);
1914  temp2=foo_step(bddm, f2, g2);
1915  result=bdd_find(bddm, top_indexindex, temp1, temp2);
1916  bdd_insert_in_cache2(bddm, <op>, f, g, result);
1917  return (result);
1918}
1919
1920bdd
1921foo(bddm, f, g)
1922     bdd_manager bddm;
1923     bdd f, g;
1924{
1925  if (bdd_check_arguments(2, f, g))
1926    {
1927      FIREWALL(bddm);
1928      RETURN_BDD(foo_step(bddm, f, g));
1929    }
1930  return ((bdd)0);
1931}
1932.fi
1933
1934In the case of dynamic variable reordering, the same abort mechanism
1935is used.  After reordering, all reference counts are reset to their
1936original values and the operation is retried.  This is handled
1937automatically by the FIREWALL macro.  (The operation is aborted since
1938after reordering, the implicit ordering represented in the C
1939subroutine call stack may be different from the new variable order.
1940Reordering occurs before freeing the temporaries, since we want to
1941minimize the aggregate size of the operands plus the result that is
1942being constructed.)
1943
1944Storage can be allocated through a number of mechanisms.  The routines
1945\fBmem_get_block\fR, \fBmem_free_block\fR, and \fBmem_resize_block\fR
1946are generally used for large single items.  For smaller uniformly
1947sized items, you probably should use a record manager.
1948.B mem_new_rec_mgr
1949will return a record manager that handles blocks of a given size.
1950Use
1951.B mem_new_rec
1952and
1953.B mem_free_rec
1954to obtain and free individual records.  Finally,
1955.B mem_free_rec_mgr
1956will dispose of the record manager and all of its associated records.
1957These routines are documented in more detail in the storage management
1958library man page.  If your structures are at most 64 bytes in size,
1959you can use the macros
1960.B BDD_NEW_REC
1961and \fBBDD_FREE_REC\fR.  These obtain records from the internal BDD
1962record managers.
1963.SH "PORTABILITY NOTES"
1964Since pointer tagging is heavily used, you'll have major problems if
1965you can't cast back and forth between pointers and longs without
1966losing something.  The low-level storage management routines are
1967fairly UNIX specific; they call
1968.B sbrk
1969directly.  If you don't have something similar, you may have to
1970rewrite them.  The storage management routines also need to be able to
1971move and clear blocks of memory whose size is given by a long.  You
1972may have to fiddle with these, especially if you have a machine where
1973int and long are different.  If you encounter portability problems,
1974let me know; maybe the next release will be able to accommodate your
1975machine.
1976.SH "SEE ALSO"
1977mem(3)
1978.SH BUGS
1979Surely you're joking.
1980.SH REFERENCES
1981[1] R. E. Bryant.  Graph Based Algorithms for Boolean Function
1982Manipulation.  \fIIEEE Transactions on Computers\fR, C-35(8):677-691,
1983August 1986.
1984.LP
1985[2] H. J. Touati, H. Savoj, B. Lin, R. K. Brayton, and A.
1986Sangiovanni-Vincentelli.  Implicit State Enumeration of Finite State
1987Machines using BDD's.  In \fIProceedings of the 1990 IEEE
1988International Conference on Computer-Aided Design\fR, November, 1990.
1989.LP
1990[3] K. S. Brace, R. L. Rudell, and R. E. Bryant.  Efficient
1991Implementation of a BDD Package.  In \fIProceedings of the 27th
1992ACM/IEEE Design Automation Conference\fR, June, 1990.
1993.LP
1994[4] E. M. Clarke, K. L. McMillan, X. Zhao, M. Fujita, and J. C.-Y.
1995Yang.  Spectral Transforms for Large Boolean Functions with
1996Applications to Technology Mapping.  In \fIProceedings of the 30th
1997ACM/IEEE Design Automation Conference\fR, June, 1993.
1998.SH AUTHOR
1999David E. Long
2000.br
2001long@research.att.com
Note: See TracBrowser for help on using the repository browser.