source: vis_dev/glu-2.3/src/bdd/bdd.h @ 36

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

library glu 2.3
File size: 27.7 KB
RevLine 
[13]1/******************************************************************************
2
3  PackageName [bdd]
4
5  Synopsis    [Package-independent BDD interface functions.]
6
7  Description []
8
9  SeeAlso     []
10
11  Author      [Thomas R. Shiple. Modified by Rajeev K. Ranjan.]
12
13  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
14  All rights reserved.
15
16  Permission is hereby granted, without written agreement and without license
17  or royalty fees, to use, copy, modify, and distribute this software and its
18  documentation for any purpose, provided that the above copyright notice and
19  the following two paragraphs appear in all copies of this software.
20
21  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
22  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
23  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
24  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
25
26  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
27  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
28  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
29  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
30  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
31
32  Revision    [$Id: bdd.h,v 1.79 2007/02/10 01:09:52 fabio Exp $]
33
34******************************************************************************/
35
36#ifndef _BDD_H
37#define _BDD_H
38#include "util.h" 
39#include "array.h"
40#include "st.h"
41#include "var_set.h"
42#include "avl.h"
43#ifndef EPD_MAX_BIN
44#include "epd.h"
45#endif
46
47/*---------------------------------------------------------------------------*/
48/* Constant declarations                                                     */
49/*---------------------------------------------------------------------------*/
50
51
52/*---------------------------------------------------------------------------*/
53/* Type declarations                                                         */
54/*---------------------------------------------------------------------------*/
55typedef int boolean;
56typedef void bdd_manager;
57typedef unsigned int bdd_variableId; /* the id of the variable in a bdd node */
58typedef void bdd_mgr_init; /* Typecasting to void to avoid error messages */
59typedef int bdd_literal;                /* integers in the set { 0, 1, 2 } */
60typedef struct bdd_t bdd_t;
61typedef void bdd_node;
62typedef void bdd_gen;
63typedef struct bdd_external_hooks_struct bdd_external_hooks;
64typedef void bdd_block;
65typedef double BDD_VALUE_TYPE;
66
67/*---------------------------------------------------------------------------*/
68/* Enumerated type declarations                                              */
69/*---------------------------------------------------------------------------*/
70
71/*
72 * Dynamic reordering.
73 */
74typedef enum {
75  BDD_REORDER_SIFT,
76  BDD_REORDER_WINDOW,
77  BDD_REORDER_SAME,
78  BDD_REORDER_RANDOM,
79  BDD_REORDER_RANDOM_PIVOT,
80  BDD_REORDER_SIFT_CONVERGE,
81  BDD_REORDER_SYMM_SIFT,
82  BDD_REORDER_SYMM_SIFT_CONV,
83  BDD_REORDER_LINEAR,
84  BDD_REORDER_LINEAR_CONVERGE,
85  BDD_REORDER_EXACT,
86  BDD_REORDER_WINDOW2,
87  BDD_REORDER_WINDOW3,
88  BDD_REORDER_WINDOW4,
89  BDD_REORDER_WINDOW2_CONV,
90  BDD_REORDER_WINDOW3_CONV,
91  BDD_REORDER_WINDOW4_CONV,
92  BDD_REORDER_GROUP_SIFT,
93  BDD_REORDER_GROUP_SIFT_CONV,
94  BDD_REORDER_ANNEALING,
95  BDD_REORDER_GENETIC,
96  BDD_REORDER_LAZY_SIFT,
97  BDD_REORDER_NONE
98} bdd_reorder_type_t;
99
100typedef enum {
101  CMU,
102  CAL,
103  CUDD
104} bdd_package_type_t;
105
106typedef enum {
107    bdd_EMPTY,
108    bdd_NONEMPTY
109} bdd_gen_status;
110
111typedef enum {
112    BDD_PRE_GC_HOOK,
113    BDD_POST_GC_HOOK,
114    BDD_PRE_REORDERING_HOOK,
115    BDD_POST_REORDERING_HOOK
116} bdd_hook_type_t;
117
118typedef enum {
119    BDD_OVER_APPROX,
120    BDD_UNDER_APPROX
121} bdd_approx_dir_t;
122
123typedef enum {
124    BDD_CONJUNCTS,
125    BDD_DISJUNCTS
126} bdd_partition_type_t;
127
128typedef enum {
129  BDD_REORDER_VERBOSITY_DEFAULT,
130  BDD_REORDER_NO_VERBOSITY,
131  BDD_REORDER_VERBOSITY
132}bdd_reorder_verbosity_t;
133
134typedef enum {
135  BDD_APPROX_HB,
136  BDD_APPROX_SP,
137  BDD_APPROX_COMP,
138  BDD_APPROX_UA,
139  BDD_APPROX_RUA,
140  BDD_APPROX_BIASED_RUA
141} bdd_approx_type_t;
142
143
144/*---------------------------------------------------------------------------*/
145/* Structure declarations                                                    */
146/*---------------------------------------------------------------------------*/
147struct bdd_external_hooks_struct {
148    char *network;
149    char *mdd;
150    char *undef1;
151};
152
153
154/*---------------------------------------------------------------------------*/
155/* Variable declarations                                                     */
156/*---------------------------------------------------------------------------*/
157
158
159/*---------------------------------------------------------------------------*/
160/* Macro declarations                                                        */
161/*---------------------------------------------------------------------------*/
162/*
163** It is assumed that dynamic reordering will not occur while there are open
164** generators.  It is the user's responsibility to make sure dynamic
165** reordering doesn't occur. As long as new nodes are not created during
166** generation, and you don't explicitly call dynamic reordering, you should be
167** okay.
168*/
169
170/*
171 *    foreach_bdd_cube(fn, gen, cube)
172 *    bdd_t *fn;
173 *    bdd_gen *gen;
174 *    array_t *cube;    - return
175 *
176 *    foreach_bdd_cube(fn, gen, cube) {
177 *        ...
178 *    }
179 */
180#define foreach_bdd_cube(fn, gen, cube)\
181  for((gen) = bdd_first_cube(fn, &cube);\
182      (bdd_gen_read_status(gen) != bdd_EMPTY) ? TRUE: bdd_gen_free(gen);\
183      (void) bdd_next_cube(gen, &cube))
184
185/*
186 *    foreach_bdd_disjoint_cube(fn, gen, cube)
187 *    bdd_t *fn;
188 *    bdd_gen *gen;
189 *    array_t *cube;    - return
190 *
191 *    foreach_bdd_disjoint_cube(fn, gen, cube) {
192 *        ...
193 *    }
194 */
195#define foreach_bdd_disjoint_cube(fn, gen, cube)\
196  for((gen) = bdd_first_disjoint_cube(fn, &cube);\
197      (bdd_gen_read_status(gen) != bdd_EMPTY) ? TRUE: bdd_gen_free(gen);\
198      (void) bdd_next_disjoint_cube(gen, &cube))
199
200/*
201 *    foreach_bdd_node(fn, gen, node)
202 *    bdd_t *fn;
203 *    bdd_gen *gen;
204 *    bdd_node *node;   - return
205 */
206#define foreach_bdd_node(fn, gen, node)\
207  for((gen) = bdd_first_node(fn, &node);\
208      (bdd_gen_read_status(gen) != bdd_EMPTY) ? TRUE: bdd_gen_free(gen);\
209      (void) bdd_next_node(gen, &node))
210
211
212/**AutomaticStart*************************************************************/
213
214/*---------------------------------------------------------------------------*/
215/* Function prototypes                                                       */
216/*---------------------------------------------------------------------------*/
217
218
219/**AutomaticEnd***************************************************************/
220
221EXTERN bdd_package_type_t bdd_get_package_name ARGS((void));
222
223/*
224 * BDD Manager Allocation And Destruction
225 */
226EXTERN bdd_manager *bdd_start ARGS((int));
227EXTERN void bdd_end ARGS((bdd_manager *));
228
229/*
230 * BDD variable management
231 */
232EXTERN bdd_t *bdd_create_variable ARGS((bdd_manager *));               
233EXTERN bdd_t *bdd_create_variable_after ARGS((bdd_manager *, bdd_variableId));
234EXTERN bdd_t *bdd_get_variable ARGS((bdd_manager *, bdd_variableId));   
235EXTERN bdd_t *bdd_create_variable_after ARGS((bdd_manager *, bdd_variableId));
236EXTERN bdd_t * bdd_var_with_index ARGS((bdd_manager *manager, int index));
237EXTERN bdd_node *bdd_add_ith_var ARGS((bdd_manager *mgr, int i));
238
239
240/*
241 * BDD Formula Management
242 */
243EXTERN bdd_t *bdd_dup ARGS((bdd_t *));
244EXTERN void bdd_free ARGS((bdd_t *));
245
246/*
247 * Operations on BDD Formulas
248 */
249EXTERN bdd_t *bdd_and ARGS((bdd_t *, bdd_t *, boolean, boolean));
250EXTERN bdd_t *bdd_and_with_limit ARGS((bdd_t *, bdd_t *, boolean, boolean, unsigned int));
251EXTERN bdd_t *bdd_and_array ARGS((bdd_t *, array_t *, boolean, boolean));
252EXTERN bdd_t *bdd_and_smooth ARGS((bdd_t *, bdd_t *, array_t *));
253EXTERN bdd_t *bdd_and_smooth_with_limit ARGS((bdd_t *, bdd_t *, array_t *, unsigned int));
254EXTERN bdd_t *bdd_and_smooth_with_cube ARGS((bdd_t *, bdd_t *, bdd_t *));
255EXTERN bdd_t *bdd_clipping_and_smooth ARGS((bdd_t *, bdd_t *, array_t *, int , int ));
256EXTERN bdd_t *bdd_xor_smooth ARGS((bdd_t *, bdd_t *, array_t *));
257EXTERN bdd_t *bdd_between ARGS((bdd_t *, bdd_t *));
258EXTERN bdd_t *bdd_cofactor ARGS((bdd_t *, bdd_t *));
259EXTERN bdd_t *bdd_cofactor_array ARGS((bdd_t *, array_t *));
260EXTERN bdd_t *bdd_var_cofactor ARGS((bdd_t *, bdd_t *));
261EXTERN bdd_t *bdd_compose ARGS((bdd_t *, bdd_t *, bdd_t *));
262EXTERN bdd_t *bdd_vector_compose ARGS((bdd_t *, array_t *, array_t *));
263EXTERN bdd_t *bdd_consensus ARGS((bdd_t *, array_t *));
264EXTERN bdd_t *bdd_consensus_with_cube ARGS((bdd_t *, bdd_t *));
265EXTERN bdd_t *bdd_cproject ARGS((bdd_t *, array_t *));
266EXTERN bdd_t *bdd_else ARGS((bdd_t *));
267EXTERN bdd_t *bdd_ite ARGS((bdd_t *, bdd_t *, bdd_t *, boolean, boolean, boolean));
268EXTERN bdd_t *bdd_minimize ARGS((bdd_t *, bdd_t *));
269EXTERN bdd_t *bdd_minimize_array ARGS((bdd_t *, array_t *));
270EXTERN bdd_t *bdd_compact ARGS((bdd_t *, bdd_t *));
271EXTERN bdd_t *bdd_squeeze ARGS((bdd_t *, bdd_t *));
272EXTERN bdd_t *bdd_not ARGS((bdd_t *));
273EXTERN bdd_t *bdd_one ARGS((bdd_manager *));
274EXTERN bdd_t *bdd_or ARGS((bdd_t *, bdd_t *, boolean, boolean));
275EXTERN bdd_t *bdd_smooth ARGS((bdd_t *, array_t *));
276EXTERN bdd_t *bdd_smooth_with_cube ARGS((bdd_t *, bdd_t *));
277EXTERN bdd_t *bdd_substitute ARGS((bdd_t *, array_t *, array_t *));
278EXTERN bdd_t *bdd_substitute_with_permut ARGS((bdd_t *, int *));
279EXTERN array_t *bdd_substitute_array ARGS((array_t *, array_t *, array_t *));
280EXTERN array_t *bdd_substitute_array_with_permut ARGS((array_t *, int *));
281EXTERN void *bdd_pointer ARGS((bdd_t *));
282EXTERN bdd_t *bdd_then ARGS((bdd_t *));
283EXTERN bdd_t *bdd_top_var ARGS((bdd_t *));
284EXTERN bdd_t *bdd_xnor ARGS((bdd_t *, bdd_t *));
285EXTERN bdd_t *bdd_xor ARGS((bdd_t *, bdd_t *));
286EXTERN bdd_t *bdd_zero ARGS((bdd_manager *));
287EXTERN bdd_t *bdd_multiway_and ARGS((bdd_manager *, array_t *));
288EXTERN bdd_t *bdd_multiway_or ARGS((bdd_manager *, array_t *));
289EXTERN bdd_t *bdd_multiway_xor ARGS((bdd_manager *, array_t *));
290EXTERN array_t * bdd_pairwise_or ARGS((bdd_manager *manager, array_t *bddArray1, array_t *bddArray2));
291EXTERN array_t * bdd_pairwise_and ARGS((bdd_manager *manager, array_t *bddArray1, array_t *bddArray2));
292EXTERN array_t * bdd_pairwise_xor ARGS((bdd_manager *manager, array_t *bddArray1, array_t *bddArray2));
293EXTERN bdd_t *bdd_approx_hb ARGS((bdd_t *, bdd_approx_dir_t , int , int ));
294EXTERN bdd_t *bdd_approx_sp ARGS((bdd_t *, bdd_approx_dir_t , int , int , int ));
295EXTERN bdd_t *bdd_approx_ua ARGS((bdd_t *, bdd_approx_dir_t , int , int , int , double ));
296EXTERN bdd_t *bdd_approx_remap_ua ARGS((bdd_t *, bdd_approx_dir_t , int , int , double ));
297EXTERN bdd_t *bdd_approx_biased_rua ARGS((bdd_t *, bdd_approx_dir_t , bdd_t *, int , int , double, double ));
298EXTERN bdd_t *bdd_approx_compress ARGS((bdd_t *, bdd_approx_dir_t , int , int ));
299EXTERN int bdd_var_decomp ARGS((bdd_t *, bdd_partition_type_t , bdd_t ***));
300EXTERN int bdd_gen_decomp ARGS((bdd_t *, bdd_partition_type_t , bdd_t ***));
301EXTERN int bdd_approx_decomp ARGS((bdd_t *, bdd_partition_type_t , bdd_t ***));
302EXTERN int bdd_iter_decomp ARGS((bdd_t *, bdd_partition_type_t , bdd_t ***));
303EXTERN bdd_t *bdd_solve_eqn ARGS((bdd_t *f, array_t *g, array_t *unknowns));
304EXTERN bdd_t *bdd_shortest_path ARGS((bdd_t *f, int *weight, int *support, int *length));
305
306EXTERN bdd_t *bdd_compute_cube ARGS((bdd_manager *mgr, array_t *vars));
307EXTERN bdd_t *bdd_compute_cube_with_phase ARGS((bdd_manager *mgr, array_t *vars, array_t *phase));
308EXTERN bdd_node *bdd_add_compose ARGS((bdd_manager *mgr, bdd_node *fn1, bdd_node *fn2, int var));
309EXTERN bdd_node *bdd_add_xnor ARGS((bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2 ));
310EXTERN bdd_node *bdd_add_times ARGS((bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2));
311EXTERN bdd_node *bdd_add_vector_compose ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node **vector));
312EXTERN bdd_node *bdd_add_residue ARGS((bdd_manager *mgr, int n, int m, int options, int top));
313EXTERN bdd_node *bdd_add_nonsim_compose ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node **vector));
314EXTERN bdd_node *bdd_add_apply ARGS((bdd_manager *mgr, bdd_node *(*operation)(bdd_manager *, bdd_node **, bdd_node **), bdd_node *fn1, bdd_node *fn2));
315EXTERN bdd_node *bdd_add_exist_abstract ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node *vars));
316EXTERN void bdd_recursive_deref ARGS((bdd_manager *mgr, bdd_node *f));
317EXTERN void bdd_ref ARGS((bdd_node *fn));
318EXTERN bdd_node *bdd_bdd_to_add ARGS((bdd_manager *mgr, bdd_node *fn));
319EXTERN bdd_node *bdd_add_permute ARGS((bdd_manager *mgr, bdd_node *fn, int *permut));
320EXTERN bdd_node *bdd_bdd_permute ARGS((bdd_manager *mgr, bdd_node *fn, int *permut));
321EXTERN bdd_node * bdd_bdd_exist_abstract ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node *cube));
322/* Added by Balakrishna Kumthekar. There are potential duplicates. */
323
324EXTERN int  bdd_equal_sup_norm  ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node *gn, BDD_VALUE_TYPE tolerance, int pr));
325EXTERN bdd_node * bdd_read_logic_zero ARGS((bdd_manager *mgr));
326EXTERN bdd_node * bdd_bdd_ith_var ARGS((bdd_manager *mgr, int i));
327EXTERN bdd_node * bdd_add_divide ARGS((bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2));
328EXTERN bdd_node * bdd_bdd_constrain ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *c));
329EXTERN bdd_node * bdd_bdd_restrict ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *c));
330EXTERN bdd_node * bdd_add_hamming ARGS((bdd_manager *mgr, bdd_node **xVars, bdd_node **yVars, int nVars));
331EXTERN bdd_node * bdd_add_ite ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g, bdd_node *h));
332EXTERN bdd_node * bdd_add_find_max ARGS((bdd_manager *mgr, bdd_node *f));
333EXTERN int bdd_bdd_pick_one_cube ARGS((bdd_manager *mgr, bdd_node *node, char *string));
334EXTERN bdd_node * bdd_add_swap_variables ARGS((bdd_manager *mgr, bdd_node *f, bdd_node **x, bdd_node **y, int n));
335EXTERN bdd_node * bdd_bdd_or ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
336EXTERN bdd_node * bdd_bdd_compute_cube ARGS((bdd_manager *mgr, bdd_node **vars, int *phase, int n));
337EXTERN bdd_node * bdd_indices_to_cube ARGS((bdd_manager *mgr, int *idArray, int n));
338EXTERN bdd_node * bdd_bdd_and ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
339EXTERN bdd_node * bdd_add_matrix_multiply ARGS((bdd_manager *mgr, bdd_node *A, bdd_node *B, bdd_node **z, int nz));
340EXTERN bdd_node * bdd_add_compute_cube ARGS((bdd_manager *mgr, bdd_node **vars, int *phase, int n));
341EXTERN bdd_node * bdd_add_const ARGS((bdd_manager *mgr, BDD_VALUE_TYPE c));
342EXTERN bdd_node * bdd_bdd_swap_variables ARGS((bdd_manager *mgr, bdd_node *f, bdd_node **x, bdd_node **y, int n));
343EXTERN double bdd_count_minterm ARGS((bdd_manager *mgr, bdd_node *f, int n));
344EXTERN bdd_node * bdd_add_bdd_threshold ARGS((bdd_manager *mgr, bdd_node *f, BDD_VALUE_TYPE value));
345EXTERN bdd_node * bdd_add_bdd_strict_threshold ARGS((bdd_manager *mgr,bdd_node *f,BDD_VALUE_TYPE value));
346EXTERN BDD_VALUE_TYPE bdd_read_epsilon ARGS((bdd_manager *mgr)); 
347EXTERN bdd_node * bdd_read_one ARGS((bdd_manager *mgr));
348EXTERN bdd_node * bdd_bdd_pick_one_minterm ARGS((bdd_manager *mgr, bdd_node *f, bdd_node **vars, int n));
349EXTERN bdd_t * bdd_pick_one_minterm ARGS((bdd_t *f, array_t *varsArray));
350EXTERN array_t * bdd_bdd_pick_arbitrary_minterms ARGS((bdd_t *f, array_t *varsArray, int n, int k));
351EXTERN bdd_t * bdd_subset_with_mask_vars ARGS((bdd_t *f, array_t *varsArray, array_t *maskVarsArray));
352EXTERN bdd_node * bdd_read_zero ARGS((bdd_manager *mgr));
353EXTERN bdd_node * bdd_bdd_new_var ARGS((bdd_manager *mgr));
354EXTERN bdd_node * bdd_bdd_and_abstract ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g, bdd_node *cube));
355
356EXTERN int bdd_test_unate ARGS((bdd_t *f, int varId, int phase));
357EXTERN array_t * bdd_find_essential ARGS((bdd_t *));
358EXTERN bdd_t * bdd_find_essential_cube ARGS((bdd_t *));
359EXTERN void bdd_deref ARGS((bdd_node *f));
360EXTERN bdd_node * bdd_add_plus ARGS((bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2));
361EXTERN int bdd_read_reorderings ARGS((bdd_manager *mgr));
362EXTERN int bdd_read_next_reordering ARGS((bdd_manager *mgr));
363EXTERN void bdd_set_next_reordering ARGS((bdd_manager *mgr, int next));
364EXTERN bdd_node * bdd_bdd_xnor ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
365EXTERN bdd_node * bdd_bdd_xor ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
366EXTERN bdd_node * bdd_bdd_vector_compose ARGS((bdd_manager *mgr, bdd_node *f, bdd_node **vector));
367
368EXTERN bdd_node * bdd_zdd_get_node ARGS((bdd_manager *mgr, int id, bdd_node *g, bdd_node *h));
369EXTERN bdd_node * bdd_zdd_product ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
370EXTERN bdd_node * bdd_zdd_product_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
371EXTERN bdd_node * bdd_zdd_union ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
372EXTERN bdd_node * bdd_zdd_union_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
373EXTERN bdd_node * bdd_zdd_weak_div ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
374EXTERN bdd_node * bdd_zdd_weak_div_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
375EXTERN bdd_node * bdd_zdd_isop_recur ARGS((bdd_manager *mgr, bdd_node *L, bdd_node *U, bdd_node **zdd_I));
376EXTERN bdd_node * bdd_zdd_isop ARGS((bdd_manager *mgr, bdd_node *L, bdd_node *U, bdd_node **zdd_I));
377EXTERN int bdd_zdd_get_cofactors3 ARGS((bdd_manager *mgr, bdd_node *f, int v, bdd_node **f1, bdd_node **f0, bdd_node **fd));
378EXTERN bdd_node * bdd_bdd_and_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
379EXTERN bdd_node * bdd_unique_inter ARGS((bdd_manager *mgr, int v, bdd_node *f, bdd_node *g));
380EXTERN bdd_node * bdd_unique_inter_ivo ARGS((bdd_manager *mgr, int v, bdd_node *f, bdd_node *g));
381EXTERN bdd_node * bdd_zdd_diff ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
382EXTERN bdd_node * bdd_zdd_diff_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
383EXTERN int bdd_num_zdd_vars ARGS((bdd_manager *mgr));
384EXTERN bdd_node * bdd_regular ARGS((bdd_node *f));
385EXTERN int bdd_is_constant ARGS((bdd_node *f));
386EXTERN int bdd_is_complement ARGS((bdd_node *f));
387EXTERN bdd_node * bdd_bdd_T ARGS((bdd_node *f));
388EXTERN bdd_node * bdd_bdd_E ARGS((bdd_node *f));
389EXTERN bdd_node * bdd_not_bdd_node ARGS((bdd_node *f));
390EXTERN void bdd_recursive_deref_zdd ARGS((bdd_manager *mgr, bdd_node *f));
391EXTERN int bdd_zdd_count ARGS((bdd_manager *mgr, bdd_node *f));
392EXTERN int bdd_read_zdd_level ARGS((bdd_manager *mgr, int index));
393EXTERN int bdd_zdd_vars_from_bdd_vars ARGS((bdd_manager *mgr, int multiplicity));
394EXTERN void bdd_zdd_realign_enable ARGS((bdd_manager *mgr));
395EXTERN void bdd_zdd_realign_disable ARGS((bdd_manager *mgr));
396EXTERN int bdd_zdd_realignment_enabled ARGS((bdd_manager *mgr));
397EXTERN void bdd_realign_enable ARGS((bdd_manager *mgr));
398EXTERN void bdd_realign_disable ARGS((bdd_manager *mgr));
399EXTERN int bdd_realignment_enabled ARGS((bdd_manager *mgr));
400EXTERN int bdd_node_read_index ARGS((bdd_node *f));
401EXTERN bdd_node * bdd_read_next ARGS((bdd_node *f));
402/* This function should not be used by an external user. This will not be a
403 * part of any future releases.
404 */
405EXTERN void bdd_set_next ARGS((bdd_node *f, bdd_node *g));
406EXTERN 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));
407EXTERN BDD_VALUE_TYPE bdd_add_value ARGS((bdd_node *f));
408
409EXTERN bdd_node * bdd_read_plus_infinity ARGS((bdd_manager *mgr));
410EXTERN 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 **)));
411EXTERN void bdd_set_background ARGS((bdd_manager *mgr,bdd_node *f));
412EXTERN bdd_node * bdd_read_background ARGS((bdd_manager *mgr));
413EXTERN bdd_node * bdd_bdd_cofactor ARGS((bdd_manager *mgr,bdd_node *f,bdd_node *g));
414EXTERN bdd_node * bdd_bdd_ite ARGS((bdd_manager *mgr,bdd_node *f,bdd_node *g,bdd_node *h));
415EXTERN bdd_node * bdd_add_minus ARGS((bdd_manager *mgr,bdd_node **fn1,bdd_node **fn2));
416EXTERN bdd_node * bdd_dxygtdxz ARGS((bdd_manager *mgr,int N,bdd_node **x, bdd_node **y, bdd_node **z));
417EXTERN bdd_node * bdd_bdd_univ_abstract ARGS((bdd_manager *mgr,bdd_node *fn,bdd_node *vars));
418EXTERN bdd_node * bdd_bdd_cprojection ARGS((bdd_manager *mgr,bdd_node *R,bdd_node *Y));
419EXTERN double *bdd_cof_minterm ARGS((bdd_t *));
420EXTERN int bdd_var_is_dependent ARGS((bdd_t *, bdd_t *));
421EXTERN int bdd_debug_check ARGS((bdd_manager *mgr));
422EXTERN bdd_node * bdd_xeqy ARGS((bdd_manager *mgr, int N, bdd_node **x, bdd_node **y));
423EXTERN bdd_node * bdd_add_roundoff ARGS((bdd_manager *mgr, bdd_node *f, int N));
424EXTERN bdd_node * bdd_xgty ARGS((bdd_manager *mgr, int N, bdd_node **x, bdd_node **y));
425EXTERN bdd_node * bdd_add_cmpl ARGS((bdd_manager *mgr, bdd_node *f));
426EXTERN bdd_node * bdd_split_set ARGS((bdd_manager *mgr, bdd_node *f, bdd_node ** x, int n, double m));
427
428/*
429 * Queries about BDD Formulas
430 */
431EXTERN boolean bdd_equal ARGS((bdd_t *, bdd_t *));
432EXTERN boolean bdd_equal_mod_care_set ARGS((bdd_t *, bdd_t *, bdd_t *));
433EXTERN boolean bdd_equal_mod_care_set_array ARGS((bdd_t *, bdd_t *, array_t *));
434EXTERN bdd_t *bdd_intersects ARGS((bdd_t *, bdd_t *));
435EXTERN bdd_t *bdd_closest_cube ARGS((bdd_t *, bdd_t *, int *));
436EXTERN boolean bdd_is_tautology ARGS((bdd_t *, boolean));
437EXTERN boolean bdd_leq ARGS((bdd_t *, bdd_t *, boolean, boolean));
438EXTERN boolean bdd_lequal_mod_care_set ARGS((bdd_t *, bdd_t *, boolean, boolean, bdd_t *));
439EXTERN boolean bdd_lequal_mod_care_set_array ARGS((bdd_t *, bdd_t *, boolean, boolean, array_t *));
440EXTERN boolean bdd_leq_array ARGS((bdd_t *, array_t *, boolean, boolean));
441EXTERN double bdd_count_onset ARGS((bdd_t *, array_t *));
442EXTERN int bdd_epd_count_onset ARGS((bdd_t *, array_t *, EpDouble *epd));
443EXTERN int bdd_print_apa_minterm ARGS((FILE *, bdd_t *, int, int));
444EXTERN int bdd_apa_compare_ratios ARGS((int, bdd_t *, bdd_t *, int, int));
445
446EXTERN double bdd_correlation ARGS((bdd_t *, bdd_t *));
447EXTERN int bdd_get_free ARGS((bdd_t *));
448EXTERN bdd_manager *bdd_get_manager ARGS((bdd_t *));
449EXTERN bdd_node *bdd_get_node ARGS((bdd_t *, boolean *));
450EXTERN bdd_node *bdd_extract_node_as_is ARGS((bdd_t *));
451EXTERN var_set_t *bdd_get_support ARGS((bdd_t *));
452EXTERN int bdd_is_support_var ARGS((bdd_t *, bdd_t *));
453EXTERN int bdd_is_support_var_id ARGS((bdd_t *, int));
454EXTERN array_t *bdd_get_varids ARGS((array_t *));
455EXTERN unsigned int bdd_num_vars ARGS((bdd_manager *));
456EXTERN int bdd_read_node_count ARGS((bdd_manager *mgr));
457EXTERN void bdd_print ARGS((bdd_t *));
458EXTERN int bdd_print_minterm ARGS((bdd_t *));
459EXTERN int bdd_print_cover ARGS((bdd_t *));
460EXTERN void bdd_print_stats ARGS((bdd_manager *, FILE *));
461EXTERN int bdd_set_parameters ARGS((bdd_manager *, avl_tree *valueTable, FILE *));
462EXTERN int bdd_size ARGS((bdd_t *));
463EXTERN int bdd_node_size ARGS((bdd_node *));
464EXTERN long bdd_size_multiple ARGS((array_t *));
465EXTERN boolean bdd_is_cube ARGS((bdd_t*));
466EXTERN bdd_block * bdd_new_var_block(bdd_t *f, long length);
467EXTERN long bdd_top_var_level ARGS((bdd_manager *manager, bdd_t *fn));
468EXTERN bdd_variableId bdd_get_id_from_level ARGS((bdd_manager *, long));
469EXTERN bdd_variableId bdd_top_var_id ARGS((bdd_t *));
470EXTERN int bdd_get_level_from_id ARGS((bdd_manager *mgr, int id));
471EXTERN int bdd_check_zero_ref ARGS((bdd_manager *mgr));
472EXTERN int bdd_estimate_cofactor ARGS((bdd_t *, bdd_t *, int ));
473/* Reordering related stuff */
474EXTERN void bdd_dynamic_reordering ARGS((bdd_manager *, bdd_reorder_type_t, bdd_reorder_verbosity_t));
475EXTERN void bdd_dynamic_reordering_zdd ARGS((bdd_manager *, bdd_reorder_type_t, bdd_reorder_verbosity_t));
476EXTERN int bdd_reordering_status ARGS((bdd_manager *mgr, bdd_reorder_type_t *method));
477EXTERN int bdd_reordering_zdd_status ARGS((bdd_manager *mgr, bdd_reorder_type_t *method));
478EXTERN void bdd_reorder ARGS((bdd_manager *));
479EXTERN int bdd_shuffle_heap ARGS((bdd_manager *mgr, int *permut));
480EXTERN void bdd_dynamic_reordering_disable ARGS((bdd_manager *mgr));
481EXTERN void bdd_dynamic_reordering_zdd_disable ARGS((bdd_manager *mgr));
482EXTERN int bdd_read_reordered_field ARGS((bdd_manager *mgr));
483EXTERN int bdd_add_hook ARGS((bdd_manager *, int (*procedure)(bdd_manager *, char *, void *), bdd_hook_type_t ));
484EXTERN int bdd_remove_hook ARGS((bdd_manager *, int (*procedure)(bdd_manager *, char *, void *), bdd_hook_type_t ));
485EXTERN int bdd_enable_reordering_reporting ARGS((bdd_manager *));
486EXTERN int bdd_disable_reordering_reporting ARGS((bdd_manager *));
487EXTERN bdd_reorder_verbosity_t bdd_reordering_reporting ARGS((bdd_manager *));
488/* This function should not be used by an external user. It will
489 * not be a part of any future release.
490 */
491EXTERN void bdd_set_reordered_field ARGS((bdd_manager *mgr, int n));
492EXTERN bdd_node *bdd_bdd_vector_support ARGS((bdd_manager *mgr,bdd_node **F,int n));
493EXTERN int bdd_bdd_vector_support_size ARGS((bdd_manager *mgr,bdd_node **F, int n));
494EXTERN int bdd_bdd_support_size ARGS((bdd_manager *mgr,bdd_node *F));
495EXTERN bdd_node *bdd_bdd_support ARGS((bdd_manager *mgr,bdd_node *F));
496EXTERN bdd_node *bdd_add_general_vector_compose ARGS((bdd_manager *mgr,bdd_node *f,bdd_node **vectorOn,bdd_node **vectorOff));
497EXTERN int bdd_bdd_leq ARGS((bdd_manager *mgr,bdd_node *f,bdd_node *g));
498EXTERN bdd_node *bdd_bdd_boolean_diff ARGS((bdd_manager *mgr,bdd_node *f,int x));
499
500/*
501** Generator related functions.
502** These are NOT to be used directly; only indirectly in the macros.
503*/
504EXTERN bdd_gen_status bdd_gen_read_status ARGS((bdd_gen *gen));
505EXTERN bdd_gen *bdd_first_cube ARGS((bdd_t *, array_t **));
506EXTERN boolean bdd_next_cube ARGS((bdd_gen *, array_t **));
507EXTERN bdd_gen *bdd_first_disjoint_cube ARGS((bdd_t *, array_t **));
508EXTERN boolean bdd_next_disjoint_cube ARGS((bdd_gen *, array_t **));
509EXTERN bdd_gen *bdd_first_node ARGS((bdd_t *, bdd_node **));
510EXTERN boolean bdd_next_node ARGS((bdd_gen *, bdd_node **));
511EXTERN int bdd_gen_free ARGS((bdd_gen *));
512
513/*
514 * Miscellaneous
515 */
516EXTERN void bdd_set_gc_mode ARGS((bdd_manager *, boolean));
517EXTERN bdd_external_hooks *bdd_get_external_hooks ARGS((bdd_manager *));
518EXTERN bdd_t *bdd_construct_bdd_t ARGS((bdd_manager *mgr, bdd_node * fn));
519EXTERN void bdd_dump_blif ARGS((bdd_manager *mgr, int nBdds, bdd_node **bdds, char **inames, char **onames, char *model, FILE *fp));
520EXTERN void bdd_dump_blif_body ARGS((bdd_manager *mgr, int nBdds, bdd_node **bdds, char **inames, char **onames, FILE *fp));
521EXTERN void bdd_dump_dot ARGS((bdd_manager *mgr, int nBdds, bdd_node **bdds, char **inames, char **onames, FILE *fp));
522EXTERN bdd_node *bdd_make_bdd_from_zdd_cover ARGS((bdd_manager *mgr, bdd_node *node));
523EXTERN bdd_node *bdd_zdd_complement ARGS((bdd_manager *mgr, bdd_node *node));
524EXTERN int bdd_ptrcmp ARGS((bdd_t *f, bdd_t *g));
525EXTERN int bdd_ptrhash ARGS((bdd_t *f,int size));
526EXTERN long bdd_read_peak_memory ARGS (( bdd_manager *mgr));
527EXTERN int bdd_read_peak_live_node ARGS (( bdd_manager *mgr));
528EXTERN int bdd_set_pi_var ARGS((bdd_manager *mgr, int index));
529EXTERN int bdd_set_ps_var ARGS((bdd_manager *mgr, int index));
530EXTERN int bdd_set_ns_var ARGS((bdd_manager *mgr, int index));
531EXTERN int bdd_is_pi_var ARGS((bdd_manager *mgr, int index));
532EXTERN int bdd_is_ps_var ARGS((bdd_manager *mgr, int index));
533EXTERN int bdd_is_ns_var ARGS((bdd_manager *mgr, int index));
534EXTERN int bdd_set_pair_index ARGS((bdd_manager *mgr, int index, int pairIndex));
535EXTERN int bdd_read_pair_index ARGS((bdd_manager *mgr, int index));
536EXTERN int bdd_set_var_to_be_grouped ARGS((bdd_manager *mgr, int index));
537EXTERN int bdd_set_var_hard_group ARGS((bdd_manager *mgr, int index));
538EXTERN int bdd_reset_var_to_be_grouped ARGS((bdd_manager *mgr, int index));
539EXTERN int bdd_is_var_to_be_grouped ARGS((bdd_manager *mgr, int index));
540EXTERN int bdd_is_var_hard_group ARGS((bdd_manager *mgr, int index));
541EXTERN int bdd_is_var_to_be_ungrouped ARGS((bdd_manager *mgr, int index));
542EXTERN int bdd_set_var_to_be_ungrouped ARGS((bdd_manager *mgr, int index));
543EXTERN int bdd_bind_var ARGS((bdd_manager *mgr, int index));
544EXTERN int bdd_unbind_var ARGS((bdd_manager *mgr, int index));
545EXTERN int bdd_is_lazy_sift ARGS((bdd_manager *mgr));
546EXTERN void bdd_discard_all_var_groups ARGS((bdd_manager *mgr));
547#endif
548
Note: See TracBrowser for help on using the repository browser.