glu-2.2: src/bdd/bdd.h Source File

00001 /******************************************************************************
00002 
00003   PackageName [bdd]
00004 
00005   Synopsis    [Package-independent BDD interface functions.]
00006 
00007   Description []
00008 
00009   SeeAlso     []
00010 
00011   Author      [Thomas R. Shiple. Modified by Rajeev K. Ranjan.]
00012 
00013   Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
00014   All rights reserved.
00015 
00016   Permission is hereby granted, without written agreement and without license
00017   or royalty fees, to use, copy, modify, and distribute this software and its
00018   documentation for any purpose, provided that the above copyright notice and
00019   the following two paragraphs appear in all copies of this software.
00020 
00021   IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
00022   DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
00023   OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
00024   CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
00025 
00026   THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
00027   INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
00028   FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
00029   "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
00030   MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
00031 
00032   Revision    [$Id: bdd.h,v 1.79 2007/02/10 01:09:52 fabio Exp $]
00033 
00034 ******************************************************************************/
00035 
00036 #ifndef _BDD_H
00037 #define _BDD_H
00038 #include "util.h"  
00039 #include "array.h"
00040 #include "st.h"
00041 #include "var_set.h"
00042 #include "avl.h"
00043 #ifndef EPD_MAX_BIN
00044 #include "epd.h"
00045 #endif
00046 
00047 /*---------------------------------------------------------------------------*/
00048 /* Constant declarations                                                     */
00049 /*---------------------------------------------------------------------------*/
00050 
00051 
00052 /*---------------------------------------------------------------------------*/
00053 /* Type declarations                                                         */
00054 /*---------------------------------------------------------------------------*/
00055 typedef int boolean;
00056 typedef void bdd_manager;
00057 typedef unsigned int bdd_variableId; /* the id of the variable in a bdd node */
00058 typedef void bdd_mgr_init; /* Typecasting to void to avoid error messages */
00059 typedef int bdd_literal;                /* integers in the set { 0, 1, 2 } */
00060 typedef struct bdd_t bdd_t;
00061 typedef void bdd_node;
00062 typedef void bdd_gen;
00063 typedef struct bdd_external_hooks_struct bdd_external_hooks;
00064 typedef void bdd_block;
00065 typedef double BDD_VALUE_TYPE;
00066 
00067 /*---------------------------------------------------------------------------*/
00068 /* Enumerated type declarations                                              */
00069 /*---------------------------------------------------------------------------*/
00070 
00071 /*
00072  * Dynamic reordering.
00073  */
00074 typedef enum {
00075   BDD_REORDER_SIFT,
00076   BDD_REORDER_WINDOW,
00077   BDD_REORDER_SAME,
00078   BDD_REORDER_RANDOM,
00079   BDD_REORDER_RANDOM_PIVOT,
00080   BDD_REORDER_SIFT_CONVERGE,
00081   BDD_REORDER_SYMM_SIFT,
00082   BDD_REORDER_SYMM_SIFT_CONV,
00083   BDD_REORDER_LINEAR,
00084   BDD_REORDER_LINEAR_CONVERGE,
00085   BDD_REORDER_EXACT,
00086   BDD_REORDER_WINDOW2,
00087   BDD_REORDER_WINDOW3,
00088   BDD_REORDER_WINDOW4,
00089   BDD_REORDER_WINDOW2_CONV,
00090   BDD_REORDER_WINDOW3_CONV,
00091   BDD_REORDER_WINDOW4_CONV,
00092   BDD_REORDER_GROUP_SIFT,
00093   BDD_REORDER_GROUP_SIFT_CONV,
00094   BDD_REORDER_ANNEALING,
00095   BDD_REORDER_GENETIC,
00096   BDD_REORDER_LAZY_SIFT,
00097   BDD_REORDER_NONE
00098 } bdd_reorder_type_t;
00099 
00100 typedef enum {
00101   CMU,
00102   CAL,
00103   CUDD
00104 } bdd_package_type_t;
00105 
00106 typedef enum {
00107     bdd_EMPTY,
00108     bdd_NONEMPTY
00109 } bdd_gen_status;
00110 
00111 typedef enum {
00112     BDD_PRE_GC_HOOK,
00113     BDD_POST_GC_HOOK,
00114     BDD_PRE_REORDERING_HOOK,
00115     BDD_POST_REORDERING_HOOK
00116 } bdd_hook_type_t;
00117 
00118 typedef enum {
00119     BDD_OVER_APPROX,
00120     BDD_UNDER_APPROX
00121 } bdd_approx_dir_t;
00122 
00123 typedef enum {
00124     BDD_CONJUNCTS,
00125     BDD_DISJUNCTS
00126 } bdd_partition_type_t;
00127 
00128 typedef enum {
00129   BDD_REORDER_VERBOSITY_DEFAULT,
00130   BDD_REORDER_NO_VERBOSITY,
00131   BDD_REORDER_VERBOSITY
00132 }bdd_reorder_verbosity_t;
00133 
00134 typedef enum {
00135   BDD_APPROX_HB,
00136   BDD_APPROX_SP,
00137   BDD_APPROX_COMP,
00138   BDD_APPROX_UA,
00139   BDD_APPROX_RUA,
00140   BDD_APPROX_BIASED_RUA
00141 } bdd_approx_type_t;
00142 
00143 
00144 /*---------------------------------------------------------------------------*/
00145 /* Structure declarations                                                    */
00146 /*---------------------------------------------------------------------------*/
00147 struct bdd_external_hooks_struct {
00148     char *network;
00149     char *mdd;
00150     char *undef1;
00151 };
00152 
00153 
00154 /*---------------------------------------------------------------------------*/
00155 /* Variable declarations                                                     */
00156 /*---------------------------------------------------------------------------*/
00157 
00158 
00159 /*---------------------------------------------------------------------------*/
00160 /* Macro declarations                                                        */
00161 /*---------------------------------------------------------------------------*/
00162 /*
00163 ** It is assumed that dynamic reordering will not occur while there are open
00164 ** generators.  It is the user's responsibility to make sure dynamic
00165 ** reordering doesn't occur. As long as new nodes are not created during
00166 ** generation, and you don't explicitly call dynamic reordering, you should be
00167 ** okay. 
00168 */
00169 
00170 /*
00171  *    foreach_bdd_cube(fn, gen, cube)
00172  *    bdd_t *fn;
00173  *    bdd_gen *gen;
00174  *    array_t *cube;    - return
00175  *
00176  *    foreach_bdd_cube(fn, gen, cube) {
00177  *        ...
00178  *    }
00179  */
00180 #define foreach_bdd_cube(fn, gen, cube)\
00181   for((gen) = bdd_first_cube(fn, &cube);\
00182       (bdd_gen_read_status(gen) != bdd_EMPTY) ? TRUE: bdd_gen_free(gen);\
00183       (void) bdd_next_cube(gen, &cube))
00184 
00185 /*
00186  *    foreach_bdd_disjoint_cube(fn, gen, cube)
00187  *    bdd_t *fn;
00188  *    bdd_gen *gen;
00189  *    array_t *cube;    - return
00190  *
00191  *    foreach_bdd_disjoint_cube(fn, gen, cube) {
00192  *        ...
00193  *    }
00194  */
00195 #define foreach_bdd_disjoint_cube(fn, gen, cube)\
00196   for((gen) = bdd_first_disjoint_cube(fn, &cube);\
00197       (bdd_gen_read_status(gen) != bdd_EMPTY) ? TRUE: bdd_gen_free(gen);\
00198       (void) bdd_next_disjoint_cube(gen, &cube))
00199 
00200 /*
00201  *    foreach_bdd_node(fn, gen, node)
00202  *    bdd_t *fn;
00203  *    bdd_gen *gen;
00204  *    bdd_node *node;   - return
00205  */
00206 #define foreach_bdd_node(fn, gen, node)\
00207   for((gen) = bdd_first_node(fn, &node);\
00208       (bdd_gen_read_status(gen) != bdd_EMPTY) ? TRUE: bdd_gen_free(gen);\
00209       (void) bdd_next_node(gen, &node))
00210 
00211 
00214 /*---------------------------------------------------------------------------*/
00215 /* Function prototypes                                                       */
00216 /*---------------------------------------------------------------------------*/
00217 
00218 
00221 EXTERN bdd_package_type_t bdd_get_package_name ARGS((void));
00222 
00223 /*
00224  * BDD Manager Allocation And Destruction
00225  */
00226 EXTERN bdd_manager *bdd_start ARGS((int));
00227 EXTERN void bdd_end ARGS((bdd_manager *));
00228 
00229 /*
00230  * BDD variable management
00231  */
00232 EXTERN bdd_t *bdd_create_variable ARGS((bdd_manager *));                
00233 EXTERN bdd_t *bdd_create_variable_after ARGS((bdd_manager *, bdd_variableId));
00234 EXTERN bdd_t *bdd_get_variable ARGS((bdd_manager *, bdd_variableId));   
00235 EXTERN bdd_t *bdd_create_variable_after ARGS((bdd_manager *, bdd_variableId));
00236 EXTERN bdd_t * bdd_var_with_index ARGS((bdd_manager *manager, int index));
00237 EXTERN bdd_node *bdd_add_ith_var ARGS((bdd_manager *mgr, int i));
00238 
00239 
00240 /*
00241  * BDD Formula Management
00242  */
00243 EXTERN bdd_t *bdd_dup ARGS((bdd_t *));
00244 EXTERN void bdd_free ARGS((bdd_t *));
00245 
00246 /* 
00247  * Operations on BDD Formulas
00248  */
00249 EXTERN bdd_t *bdd_and ARGS((bdd_t *, bdd_t *, boolean, boolean));
00250 EXTERN bdd_t *bdd_and_with_limit ARGS((bdd_t *, bdd_t *, boolean, boolean, unsigned int));
00251 EXTERN bdd_t *bdd_and_array ARGS((bdd_t *, array_t *, boolean, boolean));
00252 EXTERN bdd_t *bdd_and_smooth ARGS((bdd_t *, bdd_t *, array_t *));
00253 EXTERN bdd_t *bdd_and_smooth_with_limit ARGS((bdd_t *, bdd_t *, array_t *, unsigned int));
00254 EXTERN bdd_t *bdd_and_smooth_with_cube ARGS((bdd_t *, bdd_t *, bdd_t *));
00255 EXTERN bdd_t *bdd_clipping_and_smooth ARGS((bdd_t *, bdd_t *, array_t *, int , int ));
00256 EXTERN bdd_t *bdd_xor_smooth ARGS((bdd_t *, bdd_t *, array_t *));
00257 EXTERN bdd_t *bdd_between ARGS((bdd_t *, bdd_t *));
00258 EXTERN bdd_t *bdd_cofactor ARGS((bdd_t *, bdd_t *));
00259 EXTERN bdd_t *bdd_cofactor_array ARGS((bdd_t *, array_t *));
00260 EXTERN bdd_t *bdd_var_cofactor ARGS((bdd_t *, bdd_t *));
00261 EXTERN bdd_t *bdd_compose ARGS((bdd_t *, bdd_t *, bdd_t *));
00262 EXTERN bdd_t *bdd_vector_compose ARGS((bdd_t *, array_t *, array_t *));
00263 EXTERN bdd_t *bdd_consensus ARGS((bdd_t *, array_t *));
00264 EXTERN bdd_t *bdd_consensus_with_cube ARGS((bdd_t *, bdd_t *));
00265 EXTERN bdd_t *bdd_cproject ARGS((bdd_t *, array_t *));
00266 EXTERN bdd_t *bdd_else ARGS((bdd_t *));
00267 EXTERN bdd_t *bdd_ite ARGS((bdd_t *, bdd_t *, bdd_t *, boolean, boolean, boolean));
00268 EXTERN bdd_t *bdd_minimize ARGS((bdd_t *, bdd_t *));
00269 EXTERN bdd_t *bdd_minimize_array ARGS((bdd_t *, array_t *));
00270 EXTERN bdd_t *bdd_compact ARGS((bdd_t *, bdd_t *));
00271 EXTERN bdd_t *bdd_squeeze ARGS((bdd_t *, bdd_t *));
00272 EXTERN bdd_t *bdd_not ARGS((bdd_t *));
00273 EXTERN bdd_t *bdd_one ARGS((bdd_manager *));
00274 EXTERN bdd_t *bdd_or ARGS((bdd_t *, bdd_t *, boolean, boolean));
00275 EXTERN bdd_t *bdd_smooth ARGS((bdd_t *, array_t *));
00276 EXTERN bdd_t *bdd_smooth_with_cube ARGS((bdd_t *, bdd_t *));
00277 EXTERN bdd_t *bdd_substitute ARGS((bdd_t *, array_t *, array_t *));
00278 EXTERN bdd_t *bdd_substitute_with_permut ARGS((bdd_t *, int *));
00279 EXTERN array_t *bdd_substitute_array ARGS((array_t *, array_t *, array_t *));
00280 EXTERN array_t *bdd_substitute_array_with_permut ARGS((array_t *, int *));
00281 EXTERN void *bdd_pointer ARGS((bdd_t *));
00282 EXTERN bdd_t *bdd_then ARGS((bdd_t *));
00283 EXTERN bdd_t *bdd_top_var ARGS((bdd_t *));
00284 EXTERN bdd_t *bdd_xnor ARGS((bdd_t *, bdd_t *));
00285 EXTERN bdd_t *bdd_xor ARGS((bdd_t *, bdd_t *));
00286 EXTERN bdd_t *bdd_zero ARGS((bdd_manager *));
00287 EXTERN bdd_t *bdd_multiway_and ARGS((bdd_manager *, array_t *));
00288 EXTERN bdd_t *bdd_multiway_or ARGS((bdd_manager *, array_t *));
00289 EXTERN bdd_t *bdd_multiway_xor ARGS((bdd_manager *, array_t *));
00290 EXTERN array_t * bdd_pairwise_or ARGS((bdd_manager *manager, array_t *bddArray1, array_t *bddArray2));
00291 EXTERN array_t * bdd_pairwise_and ARGS((bdd_manager *manager, array_t *bddArray1, array_t *bddArray2));
00292 EXTERN array_t * bdd_pairwise_xor ARGS((bdd_manager *manager, array_t *bddArray1, array_t *bddArray2));
00293 EXTERN bdd_t *bdd_approx_hb ARGS((bdd_t *, bdd_approx_dir_t , int , int ));
00294 EXTERN bdd_t *bdd_approx_sp ARGS((bdd_t *, bdd_approx_dir_t , int , int , int ));
00295 EXTERN bdd_t *bdd_approx_ua ARGS((bdd_t *, bdd_approx_dir_t , int , int , int , double ));
00296 EXTERN bdd_t *bdd_approx_remap_ua ARGS((bdd_t *, bdd_approx_dir_t , int , int , double ));
00297 EXTERN bdd_t *bdd_approx_biased_rua ARGS((bdd_t *, bdd_approx_dir_t , bdd_t *, int , int , double, double ));
00298 EXTERN bdd_t *bdd_approx_compress ARGS((bdd_t *, bdd_approx_dir_t , int , int ));
00299 EXTERN int bdd_var_decomp ARGS((bdd_t *, bdd_partition_type_t , bdd_t ***));
00300 EXTERN int bdd_gen_decomp ARGS((bdd_t *, bdd_partition_type_t , bdd_t ***));
00301 EXTERN int bdd_approx_decomp ARGS((bdd_t *, bdd_partition_type_t , bdd_t ***));
00302 EXTERN int bdd_iter_decomp ARGS((bdd_t *, bdd_partition_type_t , bdd_t ***));
00303 EXTERN bdd_t *bdd_solve_eqn ARGS((bdd_t *f, array_t *g, array_t *unknowns));
00304 EXTERN bdd_t *bdd_shortest_path ARGS((bdd_t *f, int *weight, int *support, int *length));
00305 
00306 EXTERN bdd_t *bdd_compute_cube ARGS((bdd_manager *mgr, array_t *vars));
00307 EXTERN bdd_t *bdd_compute_cube_with_phase ARGS((bdd_manager *mgr, array_t *vars, array_t *phase));
00308 EXTERN bdd_node *bdd_add_compose ARGS((bdd_manager *mgr, bdd_node *fn1, bdd_node *fn2, int var));
00309 EXTERN bdd_node *bdd_add_xnor ARGS((bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2 ));
00310 EXTERN bdd_node *bdd_add_times ARGS((bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2));
00311 EXTERN bdd_node *bdd_add_vector_compose ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node **vector));
00312 EXTERN bdd_node *bdd_add_residue ARGS((bdd_manager *mgr, int n, int m, int options, int top));
00313 EXTERN bdd_node *bdd_add_nonsim_compose ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node **vector));
00314 EXTERN bdd_node *bdd_add_apply ARGS((bdd_manager *mgr, bdd_node *(*operation)(bdd_manager *, bdd_node **, bdd_node **), bdd_node *fn1, bdd_node *fn2));
00315 EXTERN bdd_node *bdd_add_exist_abstract ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node *vars));
00316 EXTERN void bdd_recursive_deref ARGS((bdd_manager *mgr, bdd_node *f));
00317 EXTERN void bdd_ref ARGS((bdd_node *fn));
00318 EXTERN bdd_node *bdd_bdd_to_add ARGS((bdd_manager *mgr, bdd_node *fn));
00319 EXTERN bdd_node *bdd_add_permute ARGS((bdd_manager *mgr, bdd_node *fn, int *permut));
00320 EXTERN bdd_node *bdd_bdd_permute ARGS((bdd_manager *mgr, bdd_node *fn, int *permut));
00321 EXTERN bdd_node * bdd_bdd_exist_abstract ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node *cube));
00322 /* Added by Balakrishna Kumthekar. There are potential duplicates. */
00323 
00324 EXTERN int  bdd_equal_sup_norm  ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node *gn, BDD_VALUE_TYPE tolerance, int pr));
00325 EXTERN bdd_node * bdd_read_logic_zero ARGS((bdd_manager *mgr));
00326 EXTERN bdd_node * bdd_bdd_ith_var ARGS((bdd_manager *mgr, int i));
00327 EXTERN bdd_node * bdd_add_divide ARGS((bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2));
00328 EXTERN bdd_node * bdd_bdd_constrain ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *c));
00329 EXTERN bdd_node * bdd_bdd_restrict ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *c));
00330 EXTERN bdd_node * bdd_add_hamming ARGS((bdd_manager *mgr, bdd_node **xVars, bdd_node **yVars, int nVars));
00331 EXTERN bdd_node * bdd_add_ite ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g, bdd_node *h));
00332 EXTERN bdd_node * bdd_add_find_max ARGS((bdd_manager *mgr, bdd_node *f));
00333 EXTERN int bdd_bdd_pick_one_cube ARGS((bdd_manager *mgr, bdd_node *node, char *string));
00334 EXTERN bdd_node * bdd_add_swap_variables ARGS((bdd_manager *mgr, bdd_node *f, bdd_node **x, bdd_node **y, int n));
00335 EXTERN bdd_node * bdd_bdd_or ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00336 EXTERN bdd_node * bdd_bdd_compute_cube ARGS((bdd_manager *mgr, bdd_node **vars, int *phase, int n));
00337 EXTERN bdd_node * bdd_indices_to_cube ARGS((bdd_manager *mgr, int *idArray, int n));
00338 EXTERN bdd_node * bdd_bdd_and ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00339 EXTERN bdd_node * bdd_add_matrix_multiply ARGS((bdd_manager *mgr, bdd_node *A, bdd_node *B, bdd_node **z, int nz));
00340 EXTERN bdd_node * bdd_add_compute_cube ARGS((bdd_manager *mgr, bdd_node **vars, int *phase, int n));
00341 EXTERN bdd_node * bdd_add_const ARGS((bdd_manager *mgr, BDD_VALUE_TYPE c));
00342 EXTERN bdd_node * bdd_bdd_swap_variables ARGS((bdd_manager *mgr, bdd_node *f, bdd_node **x, bdd_node **y, int n));
00343 EXTERN double bdd_count_minterm ARGS((bdd_manager *mgr, bdd_node *f, int n));
00344 EXTERN bdd_node * bdd_add_bdd_threshold ARGS((bdd_manager *mgr, bdd_node *f, BDD_VALUE_TYPE value));
00345 EXTERN bdd_node * bdd_add_bdd_strict_threshold ARGS((bdd_manager *mgr,bdd_node *f,BDD_VALUE_TYPE value));
00346 EXTERN BDD_VALUE_TYPE bdd_read_epsilon ARGS((bdd_manager *mgr)); 
00347 EXTERN bdd_node * bdd_read_one ARGS((bdd_manager *mgr));
00348 EXTERN bdd_node * bdd_bdd_pick_one_minterm ARGS((bdd_manager *mgr, bdd_node *f, bdd_node **vars, int n));
00349 EXTERN bdd_t * bdd_pick_one_minterm ARGS((bdd_t *f, array_t *varsArray));
00350 EXTERN array_t * bdd_bdd_pick_arbitrary_minterms ARGS((bdd_t *f, array_t *varsArray, int n, int k));
00351 EXTERN bdd_t * bdd_subset_with_mask_vars ARGS((bdd_t *f, array_t *varsArray, array_t *maskVarsArray));
00352 EXTERN bdd_node * bdd_read_zero ARGS((bdd_manager *mgr));
00353 EXTERN bdd_node * bdd_bdd_new_var ARGS((bdd_manager *mgr));
00354 EXTERN bdd_node * bdd_bdd_and_abstract ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g, bdd_node *cube));
00355 
00356 EXTERN int bdd_test_unate ARGS((bdd_t *f, int varId, int phase));
00357 EXTERN array_t * bdd_find_essential ARGS((bdd_t *));
00358 EXTERN bdd_t * bdd_find_essential_cube ARGS((bdd_t *));
00359 EXTERN void bdd_deref ARGS((bdd_node *f));
00360 EXTERN bdd_node * bdd_add_plus ARGS((bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2));
00361 EXTERN int bdd_read_reorderings ARGS((bdd_manager *mgr));
00362 EXTERN int bdd_read_next_reordering ARGS((bdd_manager *mgr));
00363 EXTERN void bdd_set_next_reordering ARGS((bdd_manager *mgr, int next));
00364 EXTERN bdd_node * bdd_bdd_xnor ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00365 EXTERN bdd_node * bdd_bdd_xor ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00366 EXTERN bdd_node * bdd_bdd_vector_compose ARGS((bdd_manager *mgr, bdd_node *f, bdd_node **vector));
00367 
00368 EXTERN bdd_node * bdd_zdd_get_node ARGS((bdd_manager *mgr, int id, bdd_node *g, bdd_node *h));
00369 EXTERN bdd_node * bdd_zdd_product ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00370 EXTERN bdd_node * bdd_zdd_product_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00371 EXTERN bdd_node * bdd_zdd_union ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00372 EXTERN bdd_node * bdd_zdd_union_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00373 EXTERN bdd_node * bdd_zdd_weak_div ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00374 EXTERN bdd_node * bdd_zdd_weak_div_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00375 EXTERN bdd_node * bdd_zdd_isop_recur ARGS((bdd_manager *mgr, bdd_node *L, bdd_node *U, bdd_node **zdd_I));
00376 EXTERN bdd_node * bdd_zdd_isop ARGS((bdd_manager *mgr, bdd_node *L, bdd_node *U, bdd_node **zdd_I));
00377 EXTERN int bdd_zdd_get_cofactors3 ARGS((bdd_manager *mgr, bdd_node *f, int v, bdd_node **f1, bdd_node **f0, bdd_node **fd));
00378 EXTERN bdd_node * bdd_bdd_and_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00379 EXTERN bdd_node * bdd_unique_inter ARGS((bdd_manager *mgr, int v, bdd_node *f, bdd_node *g));
00380 EXTERN bdd_node * bdd_unique_inter_ivo ARGS((bdd_manager *mgr, int v, bdd_node *f, bdd_node *g));
00381 EXTERN bdd_node * bdd_zdd_diff ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00382 EXTERN bdd_node * bdd_zdd_diff_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
00383 EXTERN int bdd_num_zdd_vars ARGS((bdd_manager *mgr));
00384 EXTERN bdd_node * bdd_regular ARGS((bdd_node *f));
00385 EXTERN int bdd_is_constant ARGS((bdd_node *f));
00386 EXTERN int bdd_is_complement ARGS((bdd_node *f));
00387 EXTERN bdd_node * bdd_bdd_T ARGS((bdd_node *f));
00388 EXTERN bdd_node * bdd_bdd_E ARGS((bdd_node *f));
00389 EXTERN bdd_node * bdd_not_bdd_node ARGS((bdd_node *f));
00390 EXTERN void bdd_recursive_deref_zdd ARGS((bdd_manager *mgr, bdd_node *f));
00391 EXTERN int bdd_zdd_count ARGS((bdd_manager *mgr, bdd_node *f));
00392 EXTERN int bdd_read_zdd_level ARGS((bdd_manager *mgr, int index));
00393 EXTERN int bdd_zdd_vars_from_bdd_vars ARGS((bdd_manager *mgr, int multiplicity));
00394 EXTERN void bdd_zdd_realign_enable ARGS((bdd_manager *mgr));
00395 EXTERN void bdd_zdd_realign_disable ARGS((bdd_manager *mgr));
00396 EXTERN int bdd_zdd_realignment_enabled ARGS((bdd_manager *mgr));
00397 EXTERN void bdd_realign_enable ARGS((bdd_manager *mgr));
00398 EXTERN void bdd_realign_disable ARGS((bdd_manager *mgr));
00399 EXTERN int bdd_realignment_enabled ARGS((bdd_manager *mgr));
00400 EXTERN int bdd_node_read_index ARGS((bdd_node *f));
00401 EXTERN bdd_node * bdd_read_next ARGS((bdd_node *f));
00402 /* This function should not be used by an external user. This will not be a
00403  * part of any future releases.
00404  */
00405 EXTERN void bdd_set_next ARGS((bdd_node *f, bdd_node *g));
00406 EXTERN bdd_node * bdd_add_apply_recur ARGS((bdd_manager *mgr, bdd_node *(*operation)(bdd_manager *, bdd_node **, bdd_node **), bdd_node *fn1, bdd_node *fn2));
00407 EXTERN BDD_VALUE_TYPE bdd_add_value ARGS((bdd_node *f));
00408 
00409 EXTERN bdd_node * bdd_read_plus_infinity ARGS((bdd_manager *mgr));
00410 EXTERN bdd_node * bdd_priority_select ARGS((bdd_manager *mgr,bdd_node *R,bdd_node **x,bdd_node **y,bdd_node **z,bdd_node *Pi,int n, bdd_node *(*Pifunc)(bdd_manager *, int, bdd_node **, bdd_node **, bdd_node **)));
00411 EXTERN void bdd_set_background ARGS((bdd_manager *mgr,bdd_node *f));
00412 EXTERN bdd_node * bdd_read_background ARGS((bdd_manager *mgr));
00413 EXTERN bdd_node * bdd_bdd_cofactor ARGS((bdd_manager *mgr,bdd_node *f,bdd_node *g));
00414 EXTERN bdd_node * bdd_bdd_ite ARGS((bdd_manager *mgr,bdd_node *f,bdd_node *g,bdd_node *h));
00415 EXTERN bdd_node * bdd_add_minus ARGS((bdd_manager *mgr,bdd_node **fn1,bdd_node **fn2));
00416 EXTERN bdd_node * bdd_dxygtdxz ARGS((bdd_manager *mgr,int N,bdd_node **x, bdd_node **y, bdd_node **z));
00417 EXTERN bdd_node * bdd_bdd_univ_abstract ARGS((bdd_manager *mgr,bdd_node *fn,bdd_node *vars));
00418 EXTERN bdd_node * bdd_bdd_cprojection ARGS((bdd_manager *mgr,bdd_node *R,bdd_node *Y));
00419 EXTERN double *bdd_cof_minterm ARGS((bdd_t *));
00420 EXTERN int bdd_var_is_dependent ARGS((bdd_t *, bdd_t *));
00421 EXTERN int bdd_debug_check ARGS((bdd_manager *mgr));
00422 EXTERN bdd_node * bdd_xeqy ARGS((bdd_manager *mgr, int N, bdd_node **x, bdd_node **y));
00423 EXTERN bdd_node * bdd_add_roundoff ARGS((bdd_manager *mgr, bdd_node *f, int N));
00424 EXTERN bdd_node * bdd_xgty ARGS((bdd_manager *mgr, int N, bdd_node **x, bdd_node **y));
00425 EXTERN bdd_node * bdd_add_cmpl ARGS((bdd_manager *mgr, bdd_node *f));
00426 EXTERN bdd_node * bdd_split_set ARGS((bdd_manager *mgr, bdd_node *f, bdd_node ** x, int n, double m));
00427 
00428 /*
00429  * Queries about BDD Formulas
00430  */
00431 EXTERN boolean bdd_equal ARGS((bdd_t *, bdd_t *));
00432 EXTERN boolean bdd_equal_mod_care_set ARGS((bdd_t *, bdd_t *, bdd_t *));
00433 EXTERN boolean bdd_equal_mod_care_set_array ARGS((bdd_t *, bdd_t *, array_t *));
00434 EXTERN bdd_t *bdd_intersects ARGS((bdd_t *, bdd_t *));
00435 EXTERN bdd_t *bdd_closest_cube ARGS((bdd_t *, bdd_t *, int *));
00436 EXTERN boolean bdd_is_tautology ARGS((bdd_t *, boolean));
00437 EXTERN boolean bdd_leq ARGS((bdd_t *, bdd_t *, boolean, boolean));
00438 EXTERN boolean bdd_lequal_mod_care_set ARGS((bdd_t *, bdd_t *, boolean, boolean, bdd_t *));
00439 EXTERN boolean bdd_lequal_mod_care_set_array ARGS((bdd_t *, bdd_t *, boolean, boolean, array_t *));
00440 EXTERN boolean bdd_leq_array ARGS((bdd_t *, array_t *, boolean, boolean));
00441 EXTERN double bdd_count_onset ARGS((bdd_t *, array_t *));
00442 EXTERN int bdd_epd_count_onset ARGS((bdd_t *, array_t *, EpDouble *epd));
00443 EXTERN int bdd_print_apa_minterm ARGS((FILE *, bdd_t *, int, int));
00444 EXTERN int bdd_apa_compare_ratios ARGS((int, bdd_t *, bdd_t *, int, int));
00445 
00446 EXTERN double bdd_correlation ARGS((bdd_t *, bdd_t *));
00447 EXTERN int bdd_get_free ARGS((bdd_t *));
00448 EXTERN bdd_manager *bdd_get_manager ARGS((bdd_t *));
00449 EXTERN bdd_node *bdd_get_node ARGS((bdd_t *, boolean *));
00450 EXTERN bdd_node *bdd_extract_node_as_is ARGS((bdd_t *));
00451 EXTERN var_set_t *bdd_get_support ARGS((bdd_t *));
00452 EXTERN int bdd_is_support_var ARGS((bdd_t *, bdd_t *));
00453 EXTERN int bdd_is_support_var_id ARGS((bdd_t *, int));
00454 EXTERN array_t *bdd_get_varids ARGS((array_t *));
00455 EXTERN unsigned int bdd_num_vars ARGS((bdd_manager *));
00456 EXTERN int bdd_read_node_count ARGS((bdd_manager *mgr));
00457 EXTERN void bdd_print ARGS((bdd_t *));
00458 EXTERN int bdd_print_minterm ARGS((bdd_t *));
00459 EXTERN int bdd_print_cover ARGS((bdd_t *));
00460 EXTERN void bdd_print_stats ARGS((bdd_manager *, FILE *));
00461 EXTERN int bdd_set_parameters ARGS((bdd_manager *, avl_tree *valueTable, FILE *));
00462 EXTERN int bdd_size ARGS((bdd_t *));
00463 EXTERN int bdd_node_size ARGS((bdd_node *));
00464 EXTERN long bdd_size_multiple ARGS((array_t *));
00465 EXTERN boolean bdd_is_cube ARGS((bdd_t*));
00466 EXTERN bdd_block * bdd_new_var_block(bdd_t *f, long length);
00467 EXTERN long bdd_top_var_level ARGS((bdd_manager *manager, bdd_t *fn));
00468 EXTERN bdd_variableId bdd_get_id_from_level ARGS((bdd_manager *, long));
00469 EXTERN bdd_variableId bdd_top_var_id ARGS((bdd_t *));
00470 EXTERN int bdd_get_level_from_id ARGS((bdd_manager *mgr, int id));
00471 EXTERN int bdd_check_zero_ref ARGS((bdd_manager *mgr));
00472 EXTERN int bdd_estimate_cofactor ARGS((bdd_t *, bdd_t *, int ));
00473 /* Reordering related stuff */
00474 EXTERN void bdd_dynamic_reordering ARGS((bdd_manager *, bdd_reorder_type_t, bdd_reorder_verbosity_t));
00475 EXTERN void bdd_dynamic_reordering_zdd ARGS((bdd_manager *, bdd_reorder_type_t, bdd_reorder_verbosity_t));
00476 EXTERN int bdd_reordering_status ARGS((bdd_manager *mgr, bdd_reorder_type_t *method));
00477 EXTERN int bdd_reordering_zdd_status ARGS((bdd_manager *mgr, bdd_reorder_type_t *method));
00478 EXTERN void bdd_reorder ARGS((bdd_manager *));
00479 EXTERN int bdd_shuffle_heap ARGS((bdd_manager *mgr, int *permut));
00480 EXTERN void bdd_dynamic_reordering_disable ARGS((bdd_manager *mgr));
00481 EXTERN void bdd_dynamic_reordering_zdd_disable ARGS((bdd_manager *mgr));
00482 EXTERN int bdd_read_reordered_field ARGS((bdd_manager *mgr));
00483 EXTERN int bdd_add_hook ARGS((bdd_manager *, int (*procedure)(bdd_manager *, char *, void *), bdd_hook_type_t ));
00484 EXTERN int bdd_remove_hook ARGS((bdd_manager *, int (*procedure)(bdd_manager *, char *, void *), bdd_hook_type_t ));
00485 EXTERN int bdd_enable_reordering_reporting ARGS((bdd_manager *));
00486 EXTERN int bdd_disable_reordering_reporting ARGS((bdd_manager *));
00487 EXTERN bdd_reorder_verbosity_t bdd_reordering_reporting ARGS((bdd_manager *));
00488 /* This function should not be used by an external user. It will
00489  * not be a part of any future release.
00490  */
00491 EXTERN void bdd_set_reordered_field ARGS((bdd_manager *mgr, int n));
00492 EXTERN bdd_node *bdd_bdd_vector_support ARGS((bdd_manager *mgr,bdd_node **F,int n));
00493 EXTERN int bdd_bdd_vector_support_size ARGS((bdd_manager *mgr,bdd_node **F, int n));
00494 EXTERN int bdd_bdd_support_size ARGS((bdd_manager *mgr,bdd_node *F));
00495 EXTERN bdd_node *bdd_bdd_support ARGS((bdd_manager *mgr,bdd_node *F));
00496 EXTERN bdd_node *bdd_add_general_vector_compose ARGS((bdd_manager *mgr,bdd_node *f,bdd_node **vectorOn,bdd_node **vectorOff));
00497 EXTERN int bdd_bdd_leq ARGS((bdd_manager *mgr,bdd_node *f,bdd_node *g));
00498 EXTERN bdd_node *bdd_bdd_boolean_diff ARGS((bdd_manager *mgr,bdd_node *f,int x));
00499 
00500 /*
00501 ** Generator related functions.
00502 ** These are NOT to be used directly; only indirectly in the macros.
00503 */
00504 EXTERN bdd_gen_status bdd_gen_read_status ARGS((bdd_gen *gen));
00505 EXTERN bdd_gen *bdd_first_cube ARGS((bdd_t *, array_t **));
00506 EXTERN boolean bdd_next_cube ARGS((bdd_gen *, array_t **));
00507 EXTERN bdd_gen *bdd_first_disjoint_cube ARGS((bdd_t *, array_t **));
00508 EXTERN boolean bdd_next_disjoint_cube ARGS((bdd_gen *, array_t **));
00509 EXTERN bdd_gen *bdd_first_node ARGS((bdd_t *, bdd_node **));
00510 EXTERN boolean bdd_next_node ARGS((bdd_gen *, bdd_node **));
00511 EXTERN int bdd_gen_free ARGS((bdd_gen *));
00512 
00513 /* 
00514  * Miscellaneous
00515  */
00516 EXTERN void bdd_set_gc_mode ARGS((bdd_manager *, boolean));
00517 EXTERN bdd_external_hooks *bdd_get_external_hooks ARGS((bdd_manager *));
00518 EXTERN bdd_t *bdd_construct_bdd_t ARGS((bdd_manager *mgr, bdd_node * fn));
00519 EXTERN void bdd_dump_blif ARGS((bdd_manager *mgr, int nBdds, bdd_node **bdds, char **inames, char **onames, char *model, FILE *fp));
00520 EXTERN void bdd_dump_blif_body ARGS((bdd_manager *mgr, int nBdds, bdd_node **bdds, char **inames, char **onames, FILE *fp));
00521 EXTERN void bdd_dump_dot ARGS((bdd_manager *mgr, int nBdds, bdd_node **bdds, char **inames, char **onames, FILE *fp));
00522 EXTERN bdd_node *bdd_make_bdd_from_zdd_cover ARGS((bdd_manager *mgr, bdd_node *node));
00523 EXTERN bdd_node *bdd_zdd_complement ARGS((bdd_manager *mgr, bdd_node *node));
00524 EXTERN int bdd_ptrcmp ARGS((bdd_t *f, bdd_t *g));
00525 EXTERN int bdd_ptrhash ARGS((bdd_t *f,int size));
00526 EXTERN long bdd_read_peak_memory ARGS (( bdd_manager *mgr));
00527 EXTERN int bdd_read_peak_live_node ARGS (( bdd_manager *mgr));
00528 EXTERN int bdd_set_pi_var ARGS((bdd_manager *mgr, int index));
00529 EXTERN int bdd_set_ps_var ARGS((bdd_manager *mgr, int index));
00530 EXTERN int bdd_set_ns_var ARGS((bdd_manager *mgr, int index));
00531 EXTERN int bdd_is_pi_var ARGS((bdd_manager *mgr, int index));
00532 EXTERN int bdd_is_ps_var ARGS((bdd_manager *mgr, int index));
00533 EXTERN int bdd_is_ns_var ARGS((bdd_manager *mgr, int index));
00534 EXTERN int bdd_set_pair_index ARGS((bdd_manager *mgr, int index, int pairIndex));
00535 EXTERN int bdd_read_pair_index ARGS((bdd_manager *mgr, int index));
00536 EXTERN int bdd_set_var_to_be_grouped ARGS((bdd_manager *mgr, int index));
00537 EXTERN int bdd_set_var_hard_group ARGS((bdd_manager *mgr, int index));
00538 EXTERN int bdd_reset_var_to_be_grouped ARGS((bdd_manager *mgr, int index));
00539 EXTERN int bdd_is_var_to_be_grouped ARGS((bdd_manager *mgr, int index));
00540 EXTERN int bdd_is_var_hard_group ARGS((bdd_manager *mgr, int index));
00541 EXTERN int bdd_is_var_to_be_ungrouped ARGS((bdd_manager *mgr, int index));
00542 EXTERN int bdd_set_var_to_be_ungrouped ARGS((bdd_manager *mgr, int index));
00543 EXTERN int bdd_bind_var ARGS((bdd_manager *mgr, int index));
00544 EXTERN int bdd_unbind_var ARGS((bdd_manager *mgr, int index));
00545 EXTERN int bdd_is_lazy_sift ARGS((bdd_manager *mgr));
00546 EXTERN void bdd_discard_all_var_groups ARGS((bdd_manager *mgr));
00547 #endif 
00548