distr/sis/cuddBdd.h

   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
  47 extern "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
 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 } */
 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
 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 */
 137 } bdd_t;
 138
 139 /*
 140  * Initialization data structure.   Not supported in CMU package.
 141  */
 142 typedef 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  */
 166 typedef 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  */
 175 typedef 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
 182 typedef 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
 237 typedef 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  */
 246 typedef struct bdd_external_hooks {
 247     char *network;
 248     char *mdd;
 249     char *undef1;
 250 } bdd_external_hooks;
 251
 252 /*
 253  * Dynamic reordering.
 254  */
 255 typedef 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  */
 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 *);
 295
 296 /*
 297  * BDD Variable Allocation
 298  */
 299 extern bdd_t *bdd_create_variable (bdd_manager *);
 300 extern bdd_t *bdd_get_variable (bdd_manager *, bdd_variableId);
 301
 302 /*
 303  * BDD Formula Management
 304  */
 305 extern bdd_t *bdd_dup (bdd_t *);
 306 extern void bdd_free (bdd_t *);
 307
 308 /*
 309  * Operations on BDD Formulas
 310  */
 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 *);
 332
 333 /*
 334  * Queries about BDD Formulas
 335  */
 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);
 340
 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 *);
 355
 356 extern int bdd_gen_free (bdd_gen *);
 357
 358 /*
 359  * These are NOT to be used directly; only indirectly in the macros.
 360  */
 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 *);
 366
 367 /*
 368  * Miscellaneous
 369  */
 370 extern void bdd_set_gc_mode (bdd_manager *, boolean);
 371
 372 extern bdd_external_hooks *bdd_get_external_hooks (bdd_manager *);
 373
 374 extern void bdd_dynamic_reordering (bdd_manager *, bdd_reorder_type_t);
 375
 376 extern int bdd_read_reordering_flag (bdd_manager *);
 377
 378 #ifdef __cplusplus
 379 }
 380 #endif
 381
 382 #endif /* _BDD */