1 /**CHeaderFile*****************************************************************
7 Synopsis [Defines interface for the CU package to work with the
12 Author [Abelardo Pardo]
14 Copyright [Copyright (c) 1994-1996 The Univ. of Colorado.
17 Permission is hereby granted, without written agreement and without license
18 or royalty fees, to use, copy, modify, and distribute this software and its
19 documentation for any purpose, provided that the above copyright notice and
20 the following two paragraphs appear in all copies of this software.
22 IN NO EVENT SHALL THE UNIVERSITY OF COLORADO BE LIABLE TO ANY PARTY FOR
23 DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
24 OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
25 COLORADO HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
27 THE UNIVERSITY OF COLORADO SPECIFICALLY DISCLAIMS ANY WARRANTIES,
28 INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
29 FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN
30 "AS IS" BASIS, AND THE UNIVERSITY OF COLORADO HAS NO OBLIGATION TO PROVIDE
31 MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
33 Revision [$Id: cuddBdd.h,v 1.2 1996/07/30 20:42:04 bobbie Exp $]
35 ******************************************************************************/
40 /*---------------------------------------------------------------------------*/
42 /*---------------------------------------------------------------------------*/
50 /*---------------------------------------------------------------------------*/
51 /* Constant declarations */
52 /*---------------------------------------------------------------------------*/
55 /*---------------------------------------------------------------------------*/
56 /* Stucture declarations */
57 /*---------------------------------------------------------------------------*/
61 * foreach macro in the most misesque tradition
62 * bdd_gen_free always returns 0
64 * CAUTION: in the context of the port to the CUDD package, it is assumed that
65 * dynamic reordering will not occur while there are open generators. It is
66 * the user's responsibility to make sure dynamic reordering doesn't occur.
67 * As long as new nodes are not created during generation, and you don't
68 * explicitly call dynamic reordering, you should be okay.
72 * foreach_bdd_cube(fn, gen, cube)
75 * array_t *cube; - return
77 * foreach_bdd_cube(fn, gen, cube) {
81 #define foreach_bdd_cube(fn, gen, cube)\
82 for((gen) = bdd_first_cube(fn, &cube);\
83 bdd_is_gen_empty(gen) ? bdd_gen_free(gen) : TRUE;\
84 (void) bdd_next_cube(gen, &cube))
87 * foreach_bdd_node(fn, gen, node)
90 * bdd_node *node; - return
92 #define foreach_bdd_node(fn, gen, node)\
93 for((gen) = bdd_first_node(fn, &node);\
94 bdd_is_gen_empty(gen) ? bdd_gen_free(gen) : TRUE;\
95 (void) bdd_next_node(gen, &node))
100 #define BDD_NO_LIMIT ((1<<30)-2)
101 #define BDD_DFLT_ITE_ON TRUE
102 #define BDD_DFLT_ITE_RESIZE_AT 75
103 #define BDD_DFLT_ITE_MAX_SIZE 1000000
104 #define BDD_DFLT_ITE_CONST_ON TRUE
105 #define BDD_DFLT_ITE_CONST_RESIZE_AT 75
106 #define BDD_DFLT_ITE_CONST_MAX_SIZE 1000000
107 #define BDD_DFLT_ADHOC_ON TRUE
108 #define BDD_DFLT_ADHOC_RESIZE_AT 0
109 #define BDD_DFLT_ADHOC_MAX_SIZE 10000000
110 #define BDD_DFLT_GARB_COLLECT_ON TRUE
111 #define BDD_DFLT_DAEMON NIL(void)
112 #define BDD_DFLT_MEMORY_LIMIT BDD_NO_LIMIT
113 #define BDD_DFLT_NODE_RATIO 2.0
114 #define BDD_DFLT_INIT_BLOCKS 10
117 /*---------------------------------------------------------------------------*/
118 /* Type declarations */
119 /*---------------------------------------------------------------------------*/
121 typedef struct DdManager bdd_manager
; /* referenced via a pointer only */
122 typedef unsigned int bdd_variableId
; /* the id of the variable in a bdd node */
123 typedef struct DdNode bdd_node
; /* referenced via a pointer only */
124 typedef int bdd_literal
; /* integers in the set { 0, 1, 2 } */
126 /* This is to avoid problems with the mnemosyne library, which redefines
133 typedef struct bdd_t
{
134 boolean free
; /* TRUE if this is free, FALSE otherwise ... */
135 bdd_node
*node
; /* ptr to the top node of the function */
136 bdd_manager
*mgr
; /* the manager */
140 * Initialization data structure. Not supported in CMU package.
142 typedef struct bdd_mgr_init
{
144 boolean on
; /* TRUE/FALSE: is the cache on */
145 unsigned int resize_at
; /* percentage at which to resize (e.g. 85% is 85); doesn't apply to adhoc */
146 unsigned int max_size
; /* max allowable number of buckets; for adhoc, max allowable number of entries */
151 boolean on
; /* TRUE/FALSE: is the garbage collector on */
154 void (*daemon
)(); /* used for callback when memory limit exceeded */
155 unsigned int limit
; /* upper bound on memory allocated by the manager; in megabytes */
158 float ratio
; /* allocate new bdd_nodes to achieve ratio of used to unused nodes */
159 unsigned int init_blocks
; /* number of bdd_nodeBlocks initially allocated */
164 * Match types for BDD minimization.
167 BDD_MIN_TSM
, /* two-side match */
168 BDD_MIN_OSM
, /* one-side match */
169 BDD_MIN_OSDM
/* one-side DC match */
170 } bdd_min_match_type_t
;
173 * Statistics and Other Queries
175 typedef struct bdd_cache_stats
{
178 unsigned int collisions
;
179 unsigned int inserts
;
182 typedef struct bdd_stats
{
184 bdd_cache_stats hashtable
; /* the unique table; collisions and inserts fields not used */
185 bdd_cache_stats itetable
;
186 bdd_cache_stats consttable
;
187 bdd_cache_stats adhoc
;
188 } cache
; /* various cache statistics */
192 unsigned int trivial
;
201 } blocks
; /* bdd_nodeBlock count */
207 } nodes
; /* bdd_node count */
213 } extptrs
; /* bdd_t count */
215 unsigned int times
; /* the number of times the garbage-collector has run */
216 unsigned int nodes_collected
; /* cumulative number of nodes collected over life of manager */
217 long runtime
; /* cumulative CPU time spent garbage collecting */
220 int first_sbrk
; /* value of sbrk at start of manager; used to analyze memory usage */
221 int last_sbrk
; /* value of last sbrk (see "man sbrk") fetched; used to analyze memory usage */
222 unsigned int manager
;
224 unsigned int hashtable
;
225 unsigned int ext_ptrs
;
226 unsigned int ITE_cache
;
227 unsigned int ITE_const_cache
;
228 unsigned int adhoc_cache
;
230 } memory
; /* memory usage */
234 * Traversal of BDD Formulas
237 typedef struct bdd_gen bdd_gen
;
240 * These are the hooks for stuff that uses bdd's
242 * There are three hooks, and users may use them in whatever
243 * way they wish; these hooks are guaranteed to never be used
244 * by the bdd package.
246 typedef struct bdd_external_hooks
{
250 } bdd_external_hooks
;
253 * Dynamic reordering.
261 BDD_REORDER_RANDOM_PIVOT
,
262 BDD_REORDER_SIFT_CONVERGE
,
263 BDD_REORDER_SYMM_SIFT
,
264 BDD_REORDER_SYMM_SIFT_CONV
,
268 BDD_REORDER_WINDOW2_CONV
,
269 BDD_REORDER_WINDOW3_CONV
,
270 BDD_REORDER_WINDOW4_CONV
,
271 BDD_REORDER_GROUP_SIFT
,
272 BDD_REORDER_GROUP_SIFT_CONV
,
273 BDD_REORDER_ANNEALING
,
275 } bdd_reorder_type_t
;
278 /*---------------------------------------------------------------------------*/
279 /* Variable declarations */
280 /*---------------------------------------------------------------------------*/
283 /*---------------------------------------------------------------------------*/
284 /* Macro declarations */
285 /*---------------------------------------------------------------------------*/
288 * BDD Manager Allocation And Destruction
290 extern void bdd_end (bdd_manager
*);
291 extern void bdd_register_daemon (bdd_manager
*, void (*daemon
)());
292 extern void bdd_set_mgr_init_dflts (bdd_mgr_init
*);
293 extern bdd_manager
*bdd_start (int);
294 extern bdd_manager
*bdd_start_with_params (int, bdd_mgr_init
*);
297 * BDD Variable Allocation
299 extern bdd_t
*bdd_create_variable (bdd_manager
*);
300 extern bdd_t
*bdd_get_variable (bdd_manager
*, bdd_variableId
);
303 * BDD Formula Management
305 extern bdd_t
*bdd_dup (bdd_t
*);
306 extern void bdd_free (bdd_t
*);
309 * Operations on BDD Formulas
311 extern bdd_t
*bdd_and (bdd_t
*, bdd_t
*, boolean
, boolean
);
312 extern bdd_t
*bdd_and_smooth (bdd_t
*, bdd_t
*, array_t
*);
313 extern bdd_t
*bdd_between (bdd_t
*, bdd_t
*);
314 extern bdd_t
*bdd_cofactor (bdd_t
*, bdd_t
*);
315 extern bdd_t
*bdd_compose (bdd_t
*, bdd_t
*, bdd_t
*);
316 extern bdd_t
*bdd_consensus (bdd_t
*, array_t
*);
317 extern bdd_t
*bdd_cproject (bdd_t
*, array_t
*);
318 extern bdd_t
*bdd_else (bdd_t
*);
319 extern bdd_t
*bdd_ite (bdd_t
*, bdd_t
*, bdd_t
*, boolean
, boolean
, boolean
);
320 extern bdd_t
*bdd_minimize (bdd_t
*, bdd_t
*);
321 extern bdd_t
*bdd_minimize_with_params (bdd_t
*, bdd_t
*, bdd_min_match_type_t
, boolean
, boolean
, boolean
);
322 extern bdd_t
*bdd_not (bdd_t
*);
323 extern bdd_t
*bdd_one (bdd_manager
*);
324 extern bdd_t
*bdd_or (bdd_t
*, bdd_t
*, boolean
, boolean
);
325 extern bdd_t
*bdd_smooth (bdd_t
*, array_t
*);
326 extern bdd_t
*bdd_substitute (bdd_t
*, array_t
*, array_t
*);
327 extern bdd_t
*bdd_then (bdd_t
*);
328 extern bdd_t
*bdd_top_var (bdd_t
*);
329 extern bdd_t
*bdd_xnor (bdd_t
*, bdd_t
*);
330 extern bdd_t
*bdd_xor (bdd_t
*, bdd_t
*);
331 extern bdd_t
*bdd_zero (bdd_manager
*);
334 * Queries about BDD Formulas
336 extern boolean
bdd_equal (bdd_t
*, bdd_t
*);
337 extern boolean
bdd_is_cube (bdd_t
*);
338 extern boolean
bdd_is_tautology (bdd_t
*, boolean
);
339 extern boolean
bdd_leq (bdd_t
*, bdd_t
*, boolean
, boolean
);
341 extern double bdd_count_onset (bdd_t
*, array_t
*);
342 extern bdd_manager
*bdd_get_manager (bdd_t
*);
343 extern bdd_node
*bdd_get_node (bdd_t
*, boolean
*);
344 extern void bdd_get_stats (bdd_manager
*, bdd_stats
*);
345 extern var_set_t
*bdd_get_support (bdd_t
*);
346 extern array_t
*bdd_get_varids (array_t
*);
347 extern unsigned int bdd_num_vars (bdd_manager
*);
348 extern void bdd_print (bdd_t
*);
349 extern void bdd_print_stats (bdd_stats
, FILE *);
350 extern int bdd_size (bdd_t
*);
351 extern bdd_variableId
bdd_top_var_id (bdd_t
*);
352 extern bdd_t
*bdd_create_variable_after (bdd_manager
*, bdd_variableId
);
353 extern bdd_variableId
bdd_get_id_from_level (bdd_manager
*, long);
354 extern long bdd_top_var_level (bdd_manager
*, bdd_t
*);
356 extern int bdd_gen_free (bdd_gen
*);
359 * These are NOT to be used directly; only indirectly in the macros.
361 extern bdd_gen
*bdd_first_cube (bdd_t
*, array_t
**);
362 extern boolean
bdd_next_cube (bdd_gen
*, array_t
**);
363 extern bdd_gen
*bdd_first_node (bdd_t
*, bdd_node
**);
364 extern boolean
bdd_next_node (bdd_gen
*, bdd_node
**);
365 extern boolean
bdd_is_gen_empty (bdd_gen
*);
370 extern void bdd_set_gc_mode (bdd_manager
*, boolean
);
372 extern bdd_external_hooks
*bdd_get_external_hooks (bdd_manager
*);
374 extern void bdd_dynamic_reordering (bdd_manager
*, bdd_reorder_type_t
);
376 extern int bdd_read_reordering_flag (bdd_manager
*);