source: vis_dev/glu-2.1/src/bdd/bdd.h @ 6

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

Ajout de glus pour dev VIS mod
File size: 27.5 KB
Line 
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.78 2004/02/06 22:21:55 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_shortest_path ARGS((bdd_t *f, int *weight, int *support, int *length));
304
305EXTERN bdd_t *bdd_compute_cube ARGS((bdd_manager *mgr, array_t *vars));
306EXTERN bdd_t *bdd_compute_cube_with_phase ARGS((bdd_manager *mgr, array_t *vars, array_t *phase));
307EXTERN bdd_node *bdd_add_compose ARGS((bdd_manager *mgr, bdd_node *fn1, bdd_node *fn2, int var));
308EXTERN bdd_node *bdd_add_xnor ARGS((bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2 ));
309EXTERN bdd_node *bdd_add_times ARGS((bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2));
310EXTERN bdd_node *bdd_add_vector_compose ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node **vector));
311EXTERN bdd_node *bdd_add_residue ARGS((bdd_manager *mgr, int n, int m, int options, int top));
312EXTERN bdd_node *bdd_add_nonsim_compose ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node **vector));
313EXTERN bdd_node *bdd_add_apply ARGS((bdd_manager *mgr, bdd_node *(*operation)(bdd_manager *, bdd_node **, bdd_node **), bdd_node *fn1, bdd_node *fn2));
314EXTERN bdd_node *bdd_add_exist_abstract ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node *vars));
315EXTERN void bdd_recursive_deref ARGS((bdd_manager *mgr, bdd_node *f));
316EXTERN void bdd_ref ARGS((bdd_node *fn));
317EXTERN bdd_node *bdd_bdd_to_add ARGS((bdd_manager *mgr, bdd_node *fn));
318EXTERN bdd_node *bdd_add_permute ARGS((bdd_manager *mgr, bdd_node *fn, int *permut));
319EXTERN bdd_node *bdd_bdd_permute ARGS((bdd_manager *mgr, bdd_node *fn, int *permut));
320EXTERN bdd_node * bdd_bdd_exist_abstract ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node *cube));
321/* Added by Balakrishna Kumthekar. There are potential duplicates. */
322
323EXTERN int  bdd_equal_sup_norm  ARGS((bdd_manager *mgr, bdd_node *fn, bdd_node *gn, BDD_VALUE_TYPE tolerance, int pr));
324EXTERN bdd_node * bdd_read_logic_zero ARGS((bdd_manager *mgr));
325EXTERN bdd_node * bdd_bdd_ith_var ARGS((bdd_manager *mgr, int i));
326EXTERN bdd_node * bdd_add_divide ARGS((bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2));
327EXTERN bdd_node * bdd_bdd_constrain ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *c));
328EXTERN bdd_node * bdd_bdd_restrict ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *c));
329EXTERN bdd_node * bdd_add_hamming ARGS((bdd_manager *mgr, bdd_node **xVars, bdd_node **yVars, int nVars));
330EXTERN bdd_node * bdd_add_ite ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g, bdd_node *h));
331EXTERN bdd_node * bdd_add_find_max ARGS((bdd_manager *mgr, bdd_node *f));
332EXTERN int bdd_bdd_pick_one_cube ARGS((bdd_manager *mgr, bdd_node *node, char *string));
333EXTERN bdd_node * bdd_add_swap_variables ARGS((bdd_manager *mgr, bdd_node *f, bdd_node **x, bdd_node **y, int n));
334EXTERN bdd_node * bdd_bdd_or ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
335EXTERN bdd_node * bdd_bdd_compute_cube ARGS((bdd_manager *mgr, bdd_node **vars, int *phase, int n));
336EXTERN bdd_node * bdd_indices_to_cube ARGS((bdd_manager *mgr, int *idArray, int n));
337EXTERN bdd_node * bdd_bdd_and ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
338EXTERN bdd_node * bdd_add_matrix_multiply ARGS((bdd_manager *mgr, bdd_node *A, bdd_node *B, bdd_node **z, int nz));
339EXTERN bdd_node * bdd_add_compute_cube ARGS((bdd_manager *mgr, bdd_node **vars, int *phase, int n));
340EXTERN bdd_node * bdd_add_const ARGS((bdd_manager *mgr, BDD_VALUE_TYPE c));
341EXTERN bdd_node * bdd_bdd_swap_variables ARGS((bdd_manager *mgr, bdd_node *f, bdd_node **x, bdd_node **y, int n));
342EXTERN double bdd_count_minterm ARGS((bdd_manager *mgr, bdd_node *f, int n));
343EXTERN bdd_node * bdd_add_bdd_threshold ARGS((bdd_manager *mgr, bdd_node *f, BDD_VALUE_TYPE value));
344EXTERN bdd_node * bdd_add_bdd_strict_threshold ARGS((bdd_manager *mgr,bdd_node *f,BDD_VALUE_TYPE value));
345EXTERN BDD_VALUE_TYPE bdd_read_epsilon ARGS((bdd_manager *mgr)); 
346EXTERN bdd_node * bdd_read_one ARGS((bdd_manager *mgr));
347EXTERN bdd_node * bdd_bdd_pick_one_minterm ARGS((bdd_manager *mgr, bdd_node *f, bdd_node **vars, int n));
348EXTERN bdd_t * bdd_pick_one_minterm ARGS((bdd_t *f, array_t *varsArray));
349EXTERN array_t * bdd_bdd_pick_arbitrary_minterms ARGS((bdd_t *f, array_t *varsArray, int n, int k));
350EXTERN bdd_t * bdd_subset_with_mask_vars ARGS((bdd_t *f, array_t *varsArray, array_t *maskVarsArray));
351EXTERN bdd_node * bdd_read_zero ARGS((bdd_manager *mgr));
352EXTERN bdd_node * bdd_bdd_new_var ARGS((bdd_manager *mgr));
353EXTERN bdd_node * bdd_bdd_and_abstract ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g, bdd_node *cube));
354
355EXTERN int bdd_test_unate ARGS((bdd_t *f, int varId, int phase));
356EXTERN array_t * bdd_find_essential ARGS((bdd_t *));
357EXTERN bdd_t * bdd_find_essential_cube ARGS((bdd_t *));
358EXTERN void bdd_deref ARGS((bdd_node *f));
359EXTERN bdd_node * bdd_add_plus ARGS((bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2));
360EXTERN int bdd_read_reorderings ARGS((bdd_manager *mgr));
361EXTERN int bdd_read_next_reordering ARGS((bdd_manager *mgr));
362EXTERN void bdd_set_next_reordering ARGS((bdd_manager *mgr, int next));
363EXTERN bdd_node * bdd_bdd_xnor ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
364EXTERN bdd_node * bdd_bdd_xor ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
365EXTERN bdd_node * bdd_bdd_vector_compose ARGS((bdd_manager *mgr, bdd_node *f, bdd_node **vector));
366
367EXTERN bdd_node * bdd_zdd_get_node ARGS((bdd_manager *mgr, int id, bdd_node *g, bdd_node *h));
368EXTERN bdd_node * bdd_zdd_product ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
369EXTERN bdd_node * bdd_zdd_product_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
370EXTERN bdd_node * bdd_zdd_union ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
371EXTERN bdd_node * bdd_zdd_union_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
372EXTERN bdd_node * bdd_zdd_weak_div ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
373EXTERN bdd_node * bdd_zdd_weak_div_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
374EXTERN bdd_node * bdd_zdd_isop_recur ARGS((bdd_manager *mgr, bdd_node *L, bdd_node *U, bdd_node **zdd_I));
375EXTERN bdd_node * bdd_zdd_isop ARGS((bdd_manager *mgr, bdd_node *L, bdd_node *U, bdd_node **zdd_I));
376EXTERN int bdd_zdd_get_cofactors3 ARGS((bdd_manager *mgr, bdd_node *f, int v, bdd_node **f1, bdd_node **f0, bdd_node **fd));
377EXTERN bdd_node * bdd_bdd_and_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
378EXTERN bdd_node * bdd_unique_inter ARGS((bdd_manager *mgr, int v, bdd_node *f, bdd_node *g));
379EXTERN bdd_node * bdd_unique_inter_ivo ARGS((bdd_manager *mgr, int v, bdd_node *f, bdd_node *g));
380EXTERN bdd_node * bdd_zdd_diff ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
381EXTERN bdd_node * bdd_zdd_diff_recur ARGS((bdd_manager *mgr, bdd_node *f, bdd_node *g));
382EXTERN int bdd_num_zdd_vars ARGS((bdd_manager *mgr));
383EXTERN bdd_node * bdd_regular ARGS((bdd_node *f));
384EXTERN int bdd_is_constant ARGS((bdd_node *f));
385EXTERN int bdd_is_complement ARGS((bdd_node *f));
386EXTERN bdd_node * bdd_bdd_T ARGS((bdd_node *f));
387EXTERN bdd_node * bdd_bdd_E ARGS((bdd_node *f));
388EXTERN bdd_node * bdd_not_bdd_node ARGS((bdd_node *f));
389EXTERN void bdd_recursive_deref_zdd ARGS((bdd_manager *mgr, bdd_node *f));
390EXTERN int bdd_zdd_count ARGS((bdd_manager *mgr, bdd_node *f));
391EXTERN int bdd_read_zdd_level ARGS((bdd_manager *mgr, int index));
392EXTERN int bdd_zdd_vars_from_bdd_vars ARGS((bdd_manager *mgr, int multiplicity));
393EXTERN void bdd_zdd_realign_enable ARGS((bdd_manager *mgr));
394EXTERN void bdd_zdd_realign_disable ARGS((bdd_manager *mgr));
395EXTERN int bdd_zdd_realignment_enabled ARGS((bdd_manager *mgr));
396EXTERN void bdd_realign_enable ARGS((bdd_manager *mgr));
397EXTERN void bdd_realign_disable ARGS((bdd_manager *mgr));
398EXTERN int bdd_realignment_enabled ARGS((bdd_manager *mgr));
399EXTERN int bdd_node_read_index ARGS((bdd_node *f));
400EXTERN bdd_node * bdd_read_next ARGS((bdd_node *f));
401/* This function should not be used by an external user. This will not be a
402 * part of any future releases.
403 */
404EXTERN void bdd_set_next ARGS((bdd_node *f, bdd_node *g));
405EXTERN 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));
406EXTERN BDD_VALUE_TYPE bdd_add_value ARGS((bdd_node *f));
407
408EXTERN bdd_node * bdd_read_plus_infinity ARGS((bdd_manager *mgr));
409EXTERN 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 **)));
410EXTERN void bdd_set_background ARGS((bdd_manager *mgr,bdd_node *f));
411EXTERN bdd_node * bdd_read_background ARGS((bdd_manager *mgr));
412EXTERN bdd_node * bdd_bdd_cofactor ARGS((bdd_manager *mgr,bdd_node *f,bdd_node *g));
413EXTERN bdd_node * bdd_bdd_ite ARGS((bdd_manager *mgr,bdd_node *f,bdd_node *g,bdd_node *h));
414EXTERN bdd_node * bdd_add_minus ARGS((bdd_manager *mgr,bdd_node **fn1,bdd_node **fn2));
415EXTERN bdd_node * bdd_dxygtdxz ARGS((bdd_manager *mgr,int N,bdd_node **x, bdd_node **y, bdd_node **z));
416EXTERN bdd_node * bdd_bdd_univ_abstract ARGS((bdd_manager *mgr,bdd_node *fn,bdd_node *vars));
417EXTERN bdd_node * bdd_bdd_cprojection ARGS((bdd_manager *mgr,bdd_node *R,bdd_node *Y));
418EXTERN double *bdd_cof_minterm ARGS((bdd_t *));
419EXTERN int bdd_var_is_dependent ARGS((bdd_t *, bdd_t *));
420EXTERN int bdd_debug_check ARGS((bdd_manager *mgr));
421EXTERN bdd_node * bdd_xeqy ARGS((bdd_manager *mgr, int N, bdd_node **x, bdd_node **y));
422EXTERN bdd_node * bdd_add_roundoff ARGS((bdd_manager *mgr, bdd_node *f, int N));
423EXTERN bdd_node * bdd_xgty ARGS((bdd_manager *mgr, int N, bdd_node **x, bdd_node **y));
424EXTERN bdd_node * bdd_add_cmpl ARGS((bdd_manager *mgr, bdd_node *f));
425EXTERN bdd_node * bdd_split_set ARGS((bdd_manager *mgr, bdd_node *f, bdd_node ** x, int n, double m));
426
427/*
428 * Queries about BDD Formulas
429 */
430EXTERN boolean bdd_equal ARGS((bdd_t *, bdd_t *));
431EXTERN boolean bdd_equal_mod_care_set ARGS((bdd_t *, bdd_t *, bdd_t *));
432EXTERN boolean bdd_equal_mod_care_set_array ARGS((bdd_t *, bdd_t *, array_t *));
433EXTERN bdd_t *bdd_intersects ARGS((bdd_t *, bdd_t *));
434EXTERN bdd_t *bdd_closest_cube ARGS((bdd_t *, bdd_t *, int *));
435EXTERN boolean bdd_is_tautology ARGS((bdd_t *, boolean));
436EXTERN boolean bdd_leq ARGS((bdd_t *, bdd_t *, boolean, boolean));
437EXTERN boolean bdd_lequal_mod_care_set ARGS((bdd_t *, bdd_t *, boolean, boolean, bdd_t *));
438EXTERN boolean bdd_lequal_mod_care_set_array ARGS((bdd_t *, bdd_t *, boolean, boolean, array_t *));
439EXTERN boolean bdd_leq_array ARGS((bdd_t *, array_t *, boolean, boolean));
440EXTERN double bdd_count_onset ARGS((bdd_t *, array_t *));
441EXTERN int bdd_epd_count_onset ARGS((bdd_t *, array_t *, EpDouble *epd));
442EXTERN int bdd_print_apa_minterm ARGS((FILE *, bdd_t *, int, int));
443EXTERN int bdd_apa_compare_ratios ARGS((int, bdd_t *, bdd_t *, int, int));
444
445EXTERN double bdd_correlation ARGS((bdd_t *, bdd_t *));
446EXTERN int bdd_get_free ARGS((bdd_t *));
447EXTERN bdd_manager *bdd_get_manager ARGS((bdd_t *));
448EXTERN bdd_node *bdd_get_node ARGS((bdd_t *, boolean *));
449EXTERN bdd_node *bdd_extract_node_as_is ARGS((bdd_t *));
450EXTERN var_set_t *bdd_get_support ARGS((bdd_t *));
451EXTERN int bdd_is_support_var ARGS((bdd_t *, bdd_t *));
452EXTERN int bdd_is_support_var_id ARGS((bdd_t *, int));
453EXTERN array_t *bdd_get_varids ARGS((array_t *));
454EXTERN unsigned int bdd_num_vars ARGS((bdd_manager *));
455EXTERN int bdd_read_node_count ARGS((bdd_manager *mgr));
456EXTERN void bdd_print ARGS((bdd_t *));
457EXTERN int bdd_print_minterm ARGS((bdd_t *));
458EXTERN void bdd_print_stats ARGS((bdd_manager *, FILE *));
459EXTERN int bdd_set_parameters ARGS((bdd_manager *, avl_tree *valueTable, FILE *));
460EXTERN int bdd_size ARGS((bdd_t *));
461EXTERN int bdd_node_size ARGS((bdd_node *));
462EXTERN long bdd_size_multiple ARGS((array_t *));
463EXTERN boolean bdd_is_cube ARGS((bdd_t*));
464EXTERN bdd_block * bdd_new_var_block(bdd_t *f, long length);
465EXTERN long bdd_top_var_level ARGS((bdd_manager *manager, bdd_t *fn));
466EXTERN bdd_variableId bdd_get_id_from_level ARGS((bdd_manager *, long));
467EXTERN bdd_variableId bdd_top_var_id ARGS((bdd_t *));
468EXTERN int bdd_get_level_from_id ARGS((bdd_manager *mgr, int id));
469EXTERN int bdd_check_zero_ref ARGS((bdd_manager *mgr));
470EXTERN int bdd_estimate_cofactor ARGS((bdd_t *, bdd_t *, int ));
471/* Reordering related stuff */
472EXTERN void bdd_dynamic_reordering ARGS((bdd_manager *, bdd_reorder_type_t, bdd_reorder_verbosity_t));
473EXTERN void bdd_dynamic_reordering_zdd ARGS((bdd_manager *, bdd_reorder_type_t, bdd_reorder_verbosity_t));
474EXTERN int bdd_reordering_status ARGS((bdd_manager *mgr, bdd_reorder_type_t *method));
475EXTERN int bdd_reordering_zdd_status ARGS((bdd_manager *mgr, bdd_reorder_type_t *method));
476EXTERN void bdd_reorder ARGS((bdd_manager *));
477EXTERN int bdd_shuffle_heap ARGS((bdd_manager *mgr, int *permut));
478EXTERN void bdd_dynamic_reordering_disable ARGS((bdd_manager *mgr));
479EXTERN void bdd_dynamic_reordering_zdd_disable ARGS((bdd_manager *mgr));
480EXTERN int bdd_read_reordered_field ARGS((bdd_manager *mgr));
481EXTERN int bdd_add_hook ARGS((bdd_manager *, int (*procedure)(bdd_manager *, char *, void *), bdd_hook_type_t ));
482EXTERN int bdd_remove_hook ARGS((bdd_manager *, int (*procedure)(bdd_manager *, char *, void *), bdd_hook_type_t ));
483EXTERN int bdd_enable_reordering_reporting ARGS((bdd_manager *));
484EXTERN int bdd_disable_reordering_reporting ARGS((bdd_manager *));
485EXTERN bdd_reorder_verbosity_t bdd_reordering_reporting ARGS((bdd_manager *));
486/* This function should not be used by an external user. It will
487 * not be a part of any future release.
488 */
489EXTERN void bdd_set_reordered_field ARGS((bdd_manager *mgr, int n));
490EXTERN bdd_node *bdd_bdd_vector_support ARGS((bdd_manager *mgr,bdd_node **F,int n));
491EXTERN int bdd_bdd_vector_support_size ARGS((bdd_manager *mgr,bdd_node **F, int n));
492EXTERN int bdd_bdd_support_size ARGS((bdd_manager *mgr,bdd_node *F));
493EXTERN bdd_node *bdd_bdd_support ARGS((bdd_manager *mgr,bdd_node *F));
494EXTERN bdd_node *bdd_add_general_vector_compose ARGS((bdd_manager *mgr,bdd_node *f,bdd_node **vectorOn,bdd_node **vectorOff));
495EXTERN int bdd_bdd_leq ARGS((bdd_manager *mgr,bdd_node *f,bdd_node *g));
496EXTERN bdd_node *bdd_bdd_boolean_diff ARGS((bdd_manager *mgr,bdd_node *f,int x));
497
498/*
499** Generator related functions.
500** These are NOT to be used directly; only indirectly in the macros.
501*/
502EXTERN bdd_gen_status bdd_gen_read_status ARGS((bdd_gen *gen));
503EXTERN bdd_gen *bdd_first_cube ARGS((bdd_t *, array_t **));
504EXTERN boolean bdd_next_cube ARGS((bdd_gen *, array_t **));
505EXTERN bdd_gen *bdd_first_disjoint_cube ARGS((bdd_t *, array_t **));
506EXTERN boolean bdd_next_disjoint_cube ARGS((bdd_gen *, array_t **));
507EXTERN bdd_gen *bdd_first_node ARGS((bdd_t *, bdd_node **));
508EXTERN boolean bdd_next_node ARGS((bdd_gen *, bdd_node **));
509EXTERN int bdd_gen_free ARGS((bdd_gen *));
510
511/*
512 * Miscellaneous
513 */
514EXTERN void bdd_set_gc_mode ARGS((bdd_manager *, boolean));
515EXTERN bdd_external_hooks *bdd_get_external_hooks ARGS((bdd_manager *));
516EXTERN bdd_t *bdd_construct_bdd_t ARGS((bdd_manager *mgr, bdd_node * fn));
517EXTERN void bdd_dump_blif ARGS((bdd_manager *mgr, int nBdds, bdd_node **bdds, char **inames, char **onames, char *model, FILE *fp));
518EXTERN void bdd_dump_blif_body ARGS((bdd_manager *mgr, int nBdds, bdd_node **bdds, char **inames, char **onames, FILE *fp));
519EXTERN void bdd_dump_dot ARGS((bdd_manager *mgr, int nBdds, bdd_node **bdds, char **inames, char **onames, FILE *fp));
520EXTERN bdd_node *bdd_make_bdd_from_zdd_cover ARGS((bdd_manager *mgr, bdd_node *node));
521EXTERN bdd_node *bdd_zdd_complement ARGS((bdd_manager *mgr, bdd_node *node));
522EXTERN int bdd_ptrcmp ARGS((bdd_t *f, bdd_t *g));
523EXTERN int bdd_ptrhash ARGS((bdd_t *f,int size));
524EXTERN long bdd_read_peak_memory ARGS (( bdd_manager *mgr));
525EXTERN int bdd_read_peak_live_node ARGS (( bdd_manager *mgr));
526EXTERN int bdd_set_pi_var ARGS((bdd_manager *mgr, int index));
527EXTERN int bdd_set_ps_var ARGS((bdd_manager *mgr, int index));
528EXTERN int bdd_set_ns_var ARGS((bdd_manager *mgr, int index));
529EXTERN int bdd_is_pi_var ARGS((bdd_manager *mgr, int index));
530EXTERN int bdd_is_ps_var ARGS((bdd_manager *mgr, int index));
531EXTERN int bdd_is_ns_var ARGS((bdd_manager *mgr, int index));
532EXTERN int bdd_set_pair_index ARGS((bdd_manager *mgr, int index, int pairIndex));
533EXTERN int bdd_read_pair_index ARGS((bdd_manager *mgr, int index));
534EXTERN int bdd_set_var_to_be_grouped ARGS((bdd_manager *mgr, int index));
535EXTERN int bdd_set_var_hard_group ARGS((bdd_manager *mgr, int index));
536EXTERN int bdd_reset_var_to_be_grouped ARGS((bdd_manager *mgr, int index));
537EXTERN int bdd_is_var_to_be_grouped ARGS((bdd_manager *mgr, int index));
538EXTERN int bdd_is_var_hard_group ARGS((bdd_manager *mgr, int index));
539EXTERN int bdd_is_var_to_be_ungrouped ARGS((bdd_manager *mgr, int index));
540EXTERN int bdd_set_var_to_be_ungrouped ARGS((bdd_manager *mgr, int index));
541EXTERN int bdd_bind_var ARGS((bdd_manager *mgr, int index));
542EXTERN int bdd_unbind_var ARGS((bdd_manager *mgr, int index));
543EXTERN int bdd_is_lazy_sift ARGS((bdd_manager *mgr));
544EXTERN void bdd_discard_all_var_groups ARGS((bdd_manager *mgr));
545#endif
546
Note: See TracBrowser for help on using the repository browser.