glu-2.2: src/cmuBdd/bdduser.h Source File

00001 /* BDD user-visible definitions */
00002 
00003 
00004 #if !defined(_BDDUSERH)
00005 #define _BDDUSERH
00006 
00007 
00008 #include <stdio.h>
00009 #include <memuser.h>
00010 
00011 
00012 #define ARGS(args) args
00013 
00014 
00015 /* Types */
00016 
00017 typedef struct bdd_ *bdd;
00018 typedef struct bdd_manager_ *cmu_bdd_manager;
00019 typedef struct block_ *block;
00020 
00021 
00022 /* Return values for cmu_bdd_type */
00023 
00024 #define BDD_TYPE_NONTERMINAL 0
00025 #define BDD_TYPE_ZERO 1
00026 #define BDD_TYPE_ONE 2
00027 #define BDD_TYPE_POSVAR 3
00028 #define BDD_TYPE_NEGVAR 4
00029 #define BDD_TYPE_OVERFLOW 5
00030 #define BDD_TYPE_CONSTANT 6
00031 
00032 
00033 /* Error codes for cmu_bdd_undump_bdd */
00034 
00035 #define BDD_UNDUMP_FORMAT 1
00036 #define BDD_UNDUMP_OVERFLOW 2
00037 #define BDD_UNDUMP_IOERROR 3
00038 #define BDD_UNDUMP_EOF 4
00039 
00040 
00041 /* Basic BDD routine declarations */
00042 
00043 extern bdd cmu_bdd_one ARGS((cmu_bdd_manager));
00044 extern bdd cmu_bdd_zero ARGS((cmu_bdd_manager));
00045 extern bdd cmu_bdd_new_var_first ARGS((cmu_bdd_manager));
00046 extern bdd cmu_bdd_new_var_last ARGS((cmu_bdd_manager));
00047 extern bdd cmu_bdd_new_var_before ARGS((cmu_bdd_manager, bdd));
00048 extern bdd cmu_bdd_new_var_after ARGS((cmu_bdd_manager, bdd));
00049 extern bdd cmu_bdd_var_with_index ARGS((cmu_bdd_manager, long));
00050 extern bdd cmu_bdd_var_with_id ARGS((cmu_bdd_manager, long));
00051 extern bdd cmu_bdd_ite ARGS((cmu_bdd_manager, bdd, bdd, bdd));
00052 extern bdd cmu_bdd_and ARGS((cmu_bdd_manager, bdd, bdd));
00053 extern bdd cmu_bdd_nand ARGS((cmu_bdd_manager, bdd, bdd));
00054 extern bdd cmu_bdd_or ARGS((cmu_bdd_manager, bdd, bdd));
00055 extern bdd cmu_bdd_nor ARGS((cmu_bdd_manager, bdd, bdd));
00056 extern bdd cmu_bdd_xor ARGS((cmu_bdd_manager, bdd, bdd));
00057 extern bdd cmu_bdd_xnor ARGS((cmu_bdd_manager, bdd, bdd));
00058 extern bdd cmu_bdd_identity ARGS((cmu_bdd_manager, bdd));
00059 extern bdd cmu_bdd_not ARGS((cmu_bdd_manager, bdd));
00060 extern bdd cmu_bdd_if ARGS((cmu_bdd_manager, bdd));
00061 extern long cmu_bdd_if_index ARGS((cmu_bdd_manager, bdd));
00062 extern long cmu_bdd_if_id ARGS((cmu_bdd_manager, bdd));
00063 extern bdd cmu_bdd_then ARGS((cmu_bdd_manager, bdd));
00064 extern bdd cmu_bdd_else ARGS((cmu_bdd_manager, bdd));
00065 extern bdd cmu_bdd_intersects ARGS((cmu_bdd_manager, bdd, bdd));
00066 extern bdd cmu_bdd_implies ARGS((cmu_bdd_manager, bdd, bdd));
00067 extern int cmu_bdd_type ARGS((cmu_bdd_manager, bdd));
00068 extern void cmu_bdd_unfree ARGS((cmu_bdd_manager, bdd));
00069 extern void cmu_bdd_free ARGS((cmu_bdd_manager, bdd));
00070 extern long cmu_bdd_vars ARGS((cmu_bdd_manager));
00071 extern long cmu_bdd_total_size ARGS((cmu_bdd_manager));
00072 extern int cmu_bdd_cache_ratio ARGS((cmu_bdd_manager, int));
00073 extern long cmu_bdd_node_limit ARGS((cmu_bdd_manager, long));
00074 extern int cmu_bdd_overflow ARGS((cmu_bdd_manager));
00075 extern void cmu_bdd_overflow_closure ARGS((cmu_bdd_manager, void (*) ARGS((cmu_bdd_manager, pointer)), pointer));
00076 extern void cmu_bdd_abort_closure ARGS((cmu_bdd_manager, void (*) ARGS((cmu_bdd_manager, pointer)), pointer));
00077 extern void cmu_bdd_stats ARGS((cmu_bdd_manager, FILE *));
00078 extern cmu_bdd_manager cmu_bdd_init ARGS((void));
00079 extern void cmu_bdd_quit ARGS((cmu_bdd_manager));
00080 
00081 
00082 /* Variable association routine declarations */
00083 
00084 extern int cmu_bdd_new_assoc ARGS((cmu_bdd_manager, bdd *, int));
00085 extern void cmu_bdd_free_assoc ARGS((cmu_bdd_manager, int));
00086 extern void cmu_bdd_temp_assoc ARGS((cmu_bdd_manager, bdd *, int));
00087 extern void cmu_bdd_augment_temp_assoc ARGS((cmu_bdd_manager, bdd *, int));
00088 extern int cmu_bdd_assoc ARGS((cmu_bdd_manager, int));
00089 
00090 
00091 /* Comparison routine declarations */
00092 
00093 extern int cmu_bdd_compare ARGS((cmu_bdd_manager, bdd, bdd, bdd));
00094 
00095 
00096 /* Composition routine declarations */
00097 
00098 extern bdd cmu_bdd_compose ARGS((cmu_bdd_manager, bdd, bdd, bdd));
00099 extern bdd cmu_bdd_substitute ARGS((cmu_bdd_manager, bdd));
00100 
00101 
00102 /* Variable exchange routine declarations */
00103 
00104 extern bdd cmu_bdd_swap_vars ARGS((cmu_bdd_manager, bdd, bdd, bdd));
00105 
00106 
00107 /* Quantification routine declarations */
00108 
00109 extern bdd cmu_bdd_exists ARGS((cmu_bdd_manager, bdd));
00110 extern bdd cmu_bdd_forall ARGS((cmu_bdd_manager, bdd));
00111 
00112 
00113 /* Reduce routine declarations */
00114 
00115 extern bdd cmu_bdd_reduce ARGS((cmu_bdd_manager, bdd, bdd));
00116 extern bdd cmu_bdd_cofactor ARGS((cmu_bdd_manager, bdd, bdd));
00117 
00118 
00119 /* Relational product routine declarations */
00120 
00121 extern bdd cmu_bdd_rel_prod ARGS((cmu_bdd_manager, bdd, bdd));
00122 
00123 
00124 /* Satisfying valuation routine declarations */
00125 
00126 extern bdd cmu_bdd_satisfy ARGS((cmu_bdd_manager, bdd));
00127 extern bdd cmu_bdd_satisfy_support ARGS((cmu_bdd_manager, bdd));
00128 extern double cmu_bdd_satisfying_fraction ARGS((cmu_bdd_manager, bdd));
00129 
00130 
00131 /* Generic apply routine declarations */
00132 
00133 extern bdd bdd_apply2 ARGS((cmu_bdd_manager, bdd (*) ARGS((cmu_bdd_manager, bdd *, bdd *, pointer)), bdd, bdd, pointer));
00134 extern bdd bdd_apply1 ARGS((cmu_bdd_manager, bdd (*) ARGS((cmu_bdd_manager, bdd *, pointer)), bdd, pointer));
00135 
00136 
00137 /* Size and profile routine declarations */
00138 
00139 extern long cmu_bdd_size ARGS((cmu_bdd_manager, bdd, int));
00140 extern long cmu_bdd_size_multiple ARGS((cmu_bdd_manager, bdd *, int));
00141 extern void cmu_bdd_profile ARGS((cmu_bdd_manager, bdd, long *, int));
00142 extern void cmu_bdd_profile_multiple ARGS((cmu_bdd_manager, bdd *, long *, int));
00143 extern void cmu_bdd_function_profile ARGS((cmu_bdd_manager, bdd, long *));
00144 extern void cmu_bdd_function_profile_multiple ARGS((cmu_bdd_manager, bdd *, long *));
00145 
00146 
00147 /* Print routine declarations */
00148 
00149 #define bdd_naming_fn_none ((char *(*)(cmu_bdd_manager, bdd, pointer))0)
00150 #define bdd_terminal_id_fn_none ((char *(*)(cmu_bdd_manager, INT_PTR, INT_PTR, pointer))0)
00151 
00152 extern void cmu_bdd_print_bdd ARGS((cmu_bdd_manager,
00153                                 bdd,
00154                                 char *(*) ARGS((cmu_bdd_manager, bdd, pointer)),
00155                                 char *(*) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, pointer)),
00156                                 pointer,
00157                                 FILE *));
00158 extern void cmu_bdd_print_profile_aux ARGS((cmu_bdd_manager,
00159                                         long *,
00160                                         char *(*) ARGS((cmu_bdd_manager, bdd, pointer)),
00161                                         pointer,
00162                                         int,
00163                                         FILE *));
00164 extern void cmu_bdd_print_profile ARGS((cmu_bdd_manager,
00165                                     bdd,
00166                                     char *(*) ARGS((cmu_bdd_manager, bdd, pointer)),
00167                                     pointer,
00168                                     int,
00169                                     FILE *));
00170 extern void cmu_bdd_print_profile_multiple ARGS((cmu_bdd_manager,
00171                                              bdd *,
00172                                              char *(*) ARGS((cmu_bdd_manager, bdd, pointer)),
00173                                              pointer,
00174                                              int,
00175                                              FILE *));
00176 extern void cmu_bdd_print_function_profile ARGS((cmu_bdd_manager,
00177                                              bdd,
00178                                              char *(*) ARGS((cmu_bdd_manager, bdd, pointer)),
00179                                              pointer,
00180                                              int,
00181                                              FILE *));
00182 extern void cmu_bdd_print_function_profile_multiple ARGS((cmu_bdd_manager,
00183                                                       bdd *,
00184                                                       char *(*) ARGS((cmu_bdd_manager, bdd, pointer)),
00185                                                       pointer,
00186                                                       int,
00187                                                       FILE *));
00188 
00189 
00190 /* Dump/undump routine declarations */
00191 
00192 extern int cmu_bdd_dump_bdd ARGS((cmu_bdd_manager, bdd, bdd *, FILE *));
00193 extern bdd cmu_bdd_undump_bdd ARGS((cmu_bdd_manager, bdd *, FILE *, int *));
00194 
00195 
00196 /* Support routine declarations */
00197 
00198 extern int cmu_bdd_depends_on ARGS((cmu_bdd_manager, bdd, bdd));
00199 extern void cmu_bdd_support ARGS((cmu_bdd_manager, bdd, bdd *));
00200 
00201 
00202 /* Unique table routine declarations */
00203 
00204 extern void cmu_bdd_gc ARGS((cmu_bdd_manager));
00205 extern void cmu_bdd_clear_refs ARGS((cmu_bdd_manager));
00206 
00207 
00208 /* Dynamic reordering routines */
00209 
00210 #define cmu_bdd_reorder_none ((void (*)(cmu_bdd_manager))0)
00211 
00212 extern void cmu_bdd_reorder_stable_window3 ARGS((cmu_bdd_manager));
00213 extern void cmu_bdd_reorder_sift ARGS((cmu_bdd_manager));
00214 extern void cmu_bdd_reorder_hybrid ARGS((cmu_bdd_manager));
00215 extern void cmu_bdd_var_block_reorderable ARGS((cmu_bdd_manager, block, int));
00216 extern void cmu_bdd_dynamic_reordering ARGS((cmu_bdd_manager, void (*) ARGS((cmu_bdd_manager))));
00217 extern void cmu_bdd_reorder ARGS((cmu_bdd_manager));
00218 
00219 extern bdd cmu_bdd_project ARGS((cmu_bdd_manager, bdd));
00220 
00221 /* Variable block routines */
00222 
00223 extern block cmu_bdd_new_var_block ARGS((cmu_bdd_manager, bdd, long));
00224 
00225 
00226 /* Multi-terminal BDD routine declarations */
00227 
00228 extern void mtbdd_transform_closure ARGS((cmu_bdd_manager,
00229                                           int (*) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, pointer)),
00230                                           void (*) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, INT_PTR *, INT_PTR *, pointer)),
00231                                           pointer));
00232 extern void mtcmu_bdd_one_data ARGS((cmu_bdd_manager, INT_PTR, INT_PTR));
00233 extern void cmu_mtbdd_free_terminal_closure ARGS((cmu_bdd_manager,
00234                                               void (*) ARGS((cmu_bdd_manager, INT_PTR, INT_PTR, pointer)),
00235                                               pointer));
00236 extern bdd cmu_mtbdd_get_terminal ARGS((cmu_bdd_manager, INT_PTR, INT_PTR));
00237 extern void cmu_mtbdd_terminal_value ARGS((cmu_bdd_manager, bdd, INT_PTR *, INT_PTR *));
00238 extern bdd mtcmu_bdd_ite ARGS((cmu_bdd_manager, bdd, bdd, bdd));
00239 extern bdd cmu_mtbdd_equal ARGS((cmu_bdd_manager, bdd, bdd));
00240 extern bdd mtcmu_bdd_substitute ARGS((cmu_bdd_manager, bdd));
00241 #define mtbdd_transform(bddm, f) (cmu_bdd_not(bddm, f))
00242 
00243 
00244 #undef ARGS
00245 
00246 #endif