source: icGREP/icgrep-devel/cudd-2.5.1/sis/cuddBdd.h @ 4746

Last change on this file since 4746 was 4597, checked in by nmedfort, 4 years ago

Upload of the CUDD library.

File size: 12.7 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [cuddBdd.h]
4
5  PackageName [cudd]
6
7  Synopsis    [Defines interface for the CU package to work with the
8  ucb interface.]
9
10  Description []
11
12  Author      [Abelardo Pardo]
13
14  Copyright   [Copyright (c) 1994-1996 The Univ. of Colorado.
15  All rights reserved.
16
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.
21
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.
26
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.]
32
33  Revision    [$Id: cuddBdd.h,v 1.2 1996/07/30 20:42:04 bobbie Exp $]
34
35******************************************************************************/
36
37#ifndef _BDD
38#define _BDD
39
40/*---------------------------------------------------------------------------*/
41/* Nested includes                                                           */
42/*---------------------------------------------------------------------------*/
43
44#include "var_set.h"
45
46#ifdef __cplusplus
47extern "C" {
48#endif
49
50/*---------------------------------------------------------------------------*/
51/* Constant declarations                                                     */
52/*---------------------------------------------------------------------------*/
53
54
55/*---------------------------------------------------------------------------*/
56/* Stucture declarations                                                     */
57/*---------------------------------------------------------------------------*/
58
59#define boolean         int
60/*
61 *    foreach macro in the most misesque tradition
62 *    bdd_gen_free always returns 0
63 *
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.
69 */
70
71/*
72 *    foreach_bdd_cube(fn, gen, cube)
73 *    bdd_t *fn;
74 *    bdd_gen *gen;
75 *    array_t *cube;    - return
76 *
77 *    foreach_bdd_cube(fn, gen, cube) {
78 *        ...
79 *    }
80 */
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))
85
86/*
87 *    foreach_bdd_node(fn, gen, node)
88 *    bdd_t *fn;
89 *    bdd_gen *gen;
90 *    bdd_node *node;   - return
91 */
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))
96
97/*
98 * Default settings.
99 */
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
115
116
117/*---------------------------------------------------------------------------*/
118/* Type declarations                                                         */
119/*---------------------------------------------------------------------------*/
120
121typedef struct DdManager bdd_manager;           /* referenced via a pointer only */
122typedef unsigned int bdd_variableId;            /* the id of the variable in a bdd node */
123typedef struct DdNode bdd_node;                 /* referenced via a pointer only */
124typedef int bdd_literal;                        /* integers in the set { 0, 1, 2 } */
125
126/* This is to avoid problems with the mnemosyne library, which redefines
127** free.
128*/
129#ifdef MNEMOSYNE
130#undef free
131#endif
132
133typedef 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 */
137} bdd_t;       
138
139/*
140 * Initialization data structure.   Not supported in CMU package.
141 */
142typedef struct bdd_mgr_init {
143    struct {
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 */
147    } ITE_cache,
148      ITE_const_cache,
149      adhoc_cache;
150    struct {
151      boolean on;                     /* TRUE/FALSE: is the garbage collector on */
152    } garbage_collector;
153    struct {
154      void (*daemon)();               /* used for callback when memory limit exceeded */
155      unsigned int limit;             /* upper bound on memory allocated by the manager; in megabytes */
156    } memory;
157    struct {
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 */
160    } nodes;
161} bdd_mgr_init;
162
163/*
164 * Match types for BDD minimization.
165 */
166typedef enum {
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;
171
172/*
173 * Statistics and Other Queries
174 */
175typedef struct bdd_cache_stats {
176    unsigned int hits;
177    unsigned int misses;
178    unsigned int collisions;
179    unsigned int inserts;
180} bdd_cache_stats;
181
182typedef struct bdd_stats {
183    struct {
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 */
189    struct {
190        unsigned int calls;
191        struct {
192            unsigned int trivial;
193            unsigned int cached;
194            unsigned int full;
195        } returns;
196    } ITE_ops,
197      ITE_constant_ops,
198      adhoc_ops;
199    struct {
200        unsigned int total;
201    } blocks;           /* bdd_nodeBlock count */
202    struct {
203        unsigned int used;
204        unsigned int unused;
205        unsigned int total;
206        unsigned int peak;
207    } nodes;            /* bdd_node count */
208    struct {
209        unsigned int used;
210        unsigned int unused;
211        unsigned int total;
212        unsigned int blocks; 
213    } extptrs;          /* bdd_t count */
214    struct {
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 */
218    } gc;
219    struct {
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;
223        unsigned int nodes;
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;
229        unsigned int total;
230    } memory;           /* memory usage */
231} bdd_stats;
232
233/*
234 * Traversal of BDD Formulas
235 */
236
237typedef struct bdd_gen bdd_gen;
238
239/*
240 *    These are the hooks for stuff that uses bdd's
241 *
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.
245 */
246typedef struct bdd_external_hooks {
247    char *network;
248    char *mdd;
249    char *undef1;
250} bdd_external_hooks;
251
252/*
253 * Dynamic reordering.
254 */
255typedef enum {
256    BDD_REORDER_SIFT,
257    BDD_REORDER_WINDOW,
258    BDD_REORDER_NONE,
259    BDD_REORDER_SAME,
260    BDD_REORDER_RANDOM,
261    BDD_REORDER_RANDOM_PIVOT,
262    BDD_REORDER_SIFT_CONVERGE,
263    BDD_REORDER_SYMM_SIFT,
264    BDD_REORDER_SYMM_SIFT_CONV,
265    BDD_REORDER_WINDOW2,
266    BDD_REORDER_WINDOW3,
267    BDD_REORDER_WINDOW4,
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,
274    BDD_REORDER_GENETIC
275} bdd_reorder_type_t;
276
277
278/*---------------------------------------------------------------------------*/
279/* Variable declarations                                                     */
280/*---------------------------------------------------------------------------*/
281
282
283/*---------------------------------------------------------------------------*/
284/* Macro declarations                                                        */
285/*---------------------------------------------------------------------------*/
286
287/*
288 * BDD Manager Allocation And Destruction
289 */
290extern void bdd_end (bdd_manager *);
291extern void bdd_register_daemon (bdd_manager *, void (*daemon)());
292extern void bdd_set_mgr_init_dflts (bdd_mgr_init *);
293extern bdd_manager *bdd_start (int);
294extern bdd_manager *bdd_start_with_params (int, bdd_mgr_init *);
295
296/*
297 * BDD Variable Allocation
298 */
299extern bdd_t *bdd_create_variable (bdd_manager *);             
300extern bdd_t *bdd_get_variable (bdd_manager *, bdd_variableId); 
301
302/*
303 * BDD Formula Management
304 */
305extern bdd_t *bdd_dup (bdd_t *);
306extern void bdd_free (bdd_t *);
307
308/*
309 * Operations on BDD Formulas
310 */
311extern bdd_t *bdd_and (bdd_t *, bdd_t *, boolean, boolean);
312extern bdd_t *bdd_and_smooth (bdd_t *, bdd_t *, array_t *);
313extern bdd_t *bdd_between (bdd_t *, bdd_t *);
314extern bdd_t *bdd_cofactor (bdd_t *, bdd_t *);
315extern bdd_t *bdd_compose (bdd_t *, bdd_t *, bdd_t *);
316extern bdd_t *bdd_consensus (bdd_t *, array_t *);
317extern bdd_t *bdd_cproject (bdd_t *, array_t *);
318extern bdd_t *bdd_else (bdd_t *);
319extern bdd_t *bdd_ite (bdd_t *, bdd_t *, bdd_t *, boolean, boolean, boolean);
320extern bdd_t *bdd_minimize (bdd_t *, bdd_t *);
321extern bdd_t *bdd_minimize_with_params (bdd_t *, bdd_t *, bdd_min_match_type_t, boolean, boolean, boolean);
322extern bdd_t *bdd_not (bdd_t *);
323extern bdd_t *bdd_one (bdd_manager *);
324extern bdd_t *bdd_or (bdd_t *, bdd_t *, boolean, boolean);
325extern bdd_t *bdd_smooth (bdd_t *, array_t *);
326extern bdd_t *bdd_substitute (bdd_t *, array_t *, array_t *);
327extern bdd_t *bdd_then (bdd_t *);
328extern bdd_t *bdd_top_var (bdd_t *);
329extern bdd_t *bdd_xnor (bdd_t *, bdd_t *);
330extern bdd_t *bdd_xor (bdd_t *, bdd_t *);
331extern bdd_t *bdd_zero (bdd_manager *);
332
333/*
334 * Queries about BDD Formulas
335 */
336extern boolean bdd_equal (bdd_t *, bdd_t *);
337extern boolean bdd_is_cube (bdd_t *);
338extern boolean bdd_is_tautology (bdd_t *, boolean);
339extern boolean bdd_leq (bdd_t *, bdd_t *, boolean, boolean);
340
341extern double bdd_count_onset (bdd_t *, array_t *);
342extern bdd_manager *bdd_get_manager (bdd_t *);
343extern bdd_node *bdd_get_node (bdd_t *, boolean *);
344extern void bdd_get_stats (bdd_manager *, bdd_stats *);
345extern var_set_t *bdd_get_support (bdd_t *);
346extern array_t *bdd_get_varids (array_t *);
347extern unsigned int bdd_num_vars (bdd_manager *);
348extern void bdd_print (bdd_t *);
349extern void bdd_print_stats (bdd_stats, FILE *);
350extern int bdd_size (bdd_t *);
351extern bdd_variableId bdd_top_var_id (bdd_t *);
352extern bdd_t *bdd_create_variable_after (bdd_manager *, bdd_variableId);
353extern bdd_variableId bdd_get_id_from_level (bdd_manager *, long);
354extern long bdd_top_var_level (bdd_manager *, bdd_t *);
355
356extern int bdd_gen_free (bdd_gen *);
357
358/*
359 * These are NOT to be used directly; only indirectly in the macros.
360 */
361extern bdd_gen *bdd_first_cube (bdd_t *, array_t **);
362extern boolean bdd_next_cube (bdd_gen *, array_t **);
363extern bdd_gen *bdd_first_node (bdd_t *, bdd_node **);
364extern boolean bdd_next_node (bdd_gen *, bdd_node **);
365extern boolean bdd_is_gen_empty (bdd_gen *);
366
367/*
368 * Miscellaneous
369 */
370extern void bdd_set_gc_mode (bdd_manager *, boolean);
371
372extern bdd_external_hooks *bdd_get_external_hooks (bdd_manager *);
373
374extern void bdd_dynamic_reordering (bdd_manager *, bdd_reorder_type_t);
375
376extern int bdd_read_reordering_flag (bdd_manager *);
377
378#ifdef __cplusplus
379}
380#endif
381
382#endif /* _BDD */
Note: See TracBrowser for help on using the repository browser.