src/cmuPort/cmuPort.c File Reference

#include "cmuPortInt.h"
#include "epd.h"
Include dependency graph for cmuPort.c:

Go to the source code of this file.

Functions

bdd_t * bdd_construct_bdd_t (bdd_manager *manager, bdd_node *func)
bdd_package_type_t bdd_get_package_name (void)
void bdd_end (bdd_manager *manager)
bdd_manager * bdd_start (int nvariables)
bdd_t * bdd_create_variable (bdd_manager *manager)
bdd_t * bdd_create_variable_after (bdd_manager *manager, bdd_variableId after_id)
bdd_t * bdd_get_variable (bdd_manager *manager, bdd_variableId variable_ID)
bdd_t * bdd_dup (bdd_t *f)
void bdd_free (bdd_t *f)
bdd_t * bdd_and (bdd_t *f, bdd_t *g, boolean f_phase, boolean g_phase)
bdd_t * bdd_and_with_limit (bdd_t *f, bdd_t *g, boolean f_phase, boolean g_phase, unsigned int limit)
bdd_t * bdd_and_array (bdd_t *f, array_t *g_array, boolean f_phase, boolean g_phase)
bdd_t * bdd_multiway_and (bdd_manager *manager, array_t *bddArray)
bdd_t * bdd_multiway_or (bdd_manager *manager, array_t *bddArray)
bdd_t * bdd_multiway_xor (bdd_manager *manager, array_t *bddArray)
array_t * bdd_pairwise_or (bdd_manager *manager, array_t *bddArray1, array_t *bddArray2)
array_t * bdd_pairwise_and (bdd_manager *manager, array_t *bddArray1, array_t *bddArray2)
array_t * bdd_pairwise_xor (bdd_manager *manager, array_t *bddArray1, array_t *bddArray2)
bdd_t * bdd_and_smooth (bdd_t *f, bdd_t *g, array_t *smoothing_vars)
bdd_t * bdd_and_smooth_with_limit (bdd_t *f, bdd_t *g, array_t *smoothing_vars, unsigned int limit)
bdd_t * bdd_between (bdd_t *f_min, bdd_t *f_max)
bdd_t * bdd_cofactor (bdd_t *f, bdd_t *g)
bdd_t * bdd_cofactor_array (bdd_t *f, array_t *bddArray)
bdd_t * bdd_compose (bdd_t *f, bdd_t *v, bdd_t *g)
bdd_t * bdd_consensus (bdd_t *f, array_t *quantifying_vars)
bdd_t * bdd_cproject (bdd_t *f, array_t *quantifying_vars)
bdd_t * bdd_else (bdd_t *f)
bdd_t * bdd_ite (bdd_t *i, bdd_t *t, bdd_t *e, boolean i_phase, boolean t_phase, boolean e_phase)
bdd_t * bdd_minimize (bdd_t *f, bdd_t *c)
bdd_t * bdd_minimize_array (bdd_t *f, array_t *bddArray)
bdd_t * bdd_not (bdd_t *f)
bdd_t * bdd_one (bdd_manager *manager)
bdd_t * bdd_or (bdd_t *f, bdd_t *g, boolean f_phase, boolean g_phase)
bdd_t * bdd_smooth (bdd_t *f, array_t *smoothing_vars)
bdd_t * bdd_substitute (bdd_t *f, array_t *old_array, array_t *new_array)
array_t * bdd_substitute_array (array_t *f_array, array_t *old_array, array_t *new_array)
void * bdd_pointer (bdd_t *f)
bdd_t * bdd_then (bdd_t *f)
bdd_t * bdd_top_var (bdd_t *f)
bdd_t * bdd_xnor (bdd_t *f, bdd_t *g)
bdd_t * bdd_xor (bdd_t *f, bdd_t *g)
bdd_t * bdd_zero (bdd_manager *manager)
boolean bdd_equal (bdd_t *f, bdd_t *g)
boolean bdd_equal_mod_care_set (bdd_t *f, bdd_t *g, bdd_t *CareSet)
bdd_t * bdd_intersects (bdd_t *f, bdd_t *g)
bdd_t * bdd_closest_cube (bdd_t *f, bdd_t *g, int *dist)
boolean bdd_is_tautology (bdd_t *f, boolean phase)
boolean bdd_leq (bdd_t *f, bdd_t *g, boolean f_phase, boolean g_phase)
boolean bdd_lequal_mod_care_set (bdd_t *f, bdd_t *g, boolean f_phase, boolean g_phase, bdd_t *careSet)
boolean bdd_leq_array (bdd_t *f, array_t *g_array, boolean f_phase, boolean g_phase)
double bdd_count_onset (bdd_t *f, array_t *var_array)
int bdd_epd_count_onset (bdd_t *f, array_t *var_array, EpDouble *epd)
int bdd_get_free (bdd_t *f)
bdd_manager * bdd_get_manager (bdd_t *f)
bdd_node * bdd_get_node (bdd_t *f, boolean *is_complemented)
var_set_t * bdd_get_support (bdd_t *f)
int bdd_is_support_var (bdd_t *f, bdd_t *var)
int bdd_is_support_var_id (bdd_t *f, int index)
array_t * bdd_get_varids (array_t *var_array)
unsigned int bdd_num_vars (bdd_manager *manager)
void bdd_print (bdd_t *f)
void bdd_print_stats (bdd_manager *manager, FILE *file)
int bdd_set_parameters (bdd_manager *mgr, avl_tree *valueTable, FILE *file)
int bdd_size (bdd_t *f)
int bdd_node_size (bdd_node *f)
long bdd_size_multiple (array_t *bdd_array)
bdd_variableId bdd_top_var_id (bdd_t *f)
bdd_external_hooks * bdd_get_external_hooks (bdd_manager *manager)
void bdd_set_gc_mode (bdd_manager *manager, boolean no_gc)
void bdd_dynamic_reordering (bdd_manager *manager, bdd_reorder_type_t algorithm_type, bdd_reorder_verbosity_t verbosity)
void bdd_dynamic_reordering_zdd (bdd_manager *manager, bdd_reorder_type_t algorithm_type, bdd_reorder_verbosity_t verbosity)
void bdd_reorder (bdd_manager *manager)
bdd_variableId bdd_get_id_from_level (bdd_manager *manager, long level)
long bdd_top_var_level (bdd_manager *manager, bdd_t *fn)
boolean bdd_is_cube (bdd_t *f)
bdd_block * bdd_new_var_block (bdd_t *f, long length)
bdd_t * bdd_var_with_index (bdd_manager *manager, int index)
bdd_t * bdd_compact (bdd_t *f, bdd_t *g)
bdd_t * bdd_squeeze (bdd_t *f, bdd_t *g)
double bdd_correlation (bdd_t *f, bdd_t *g)
int bdd_reordering_status (bdd_manager *mgr, bdd_reorder_type_t *method)
bdd_t * bdd_compute_cube (bdd_manager *mgr, array_t *vars)
bdd_t * bdd_compute_cube_with_phase (bdd_manager *mgr, array_t *vars, array_t *phase)
bdd_t * bdd_clipping_and_smooth (bdd_t *f, bdd_t *g, array_t *smoothing_vars, int maxDepth, int over)
bdd_t * bdd_approx_hb (bdd_t *f, bdd_approx_dir_t approxDir, int numVars, int threshold)
bdd_t * bdd_approx_sp (bdd_t *f, bdd_approx_dir_t approxDir, int numVars, int threshold, int hardlimit)
bdd_t * bdd_approx_ua (bdd_t *f, bdd_approx_dir_t approxDir, int numVars, int threshold, int safe, double quality)
bdd_t * bdd_approx_remap_ua (bdd_t *f, bdd_approx_dir_t approxDir, int numVars, int threshold, double quality)
bdd_t * bdd_approx_biased_rua (bdd_t *f, bdd_approx_dir_t approxDir, bdd_t *bias, int numVars, int threshold, double quality, double quality1)
bdd_t * bdd_approx_compress (bdd_t *f, bdd_approx_dir_t approxDir, int numVars, int threshold)
int bdd_gen_decomp (bdd_t *f, bdd_partition_type_t partType, bdd_t ***conjArray)
int bdd_var_decomp (bdd_t *f, bdd_partition_type_t partType, bdd_t ***conjArray)
int bdd_approx_decomp (bdd_t *f, bdd_partition_type_t partType, bdd_t ***conjArray)
int bdd_iter_decomp (bdd_t *f, bdd_partition_type_t partType, bdd_t ***conjArray)
bdd_t * bdd_solve_eqn (bdd_t *f, array_t *g, array_t *unknowns)
int bdd_add_hook (bdd_manager *mgr, int(*procedure)(bdd_manager *, char *, void *), bdd_hook_type_t whichHook)
int bdd_remove_hook (bdd_manager *mgr, int(*procedure)(bdd_manager *, char *, void *), bdd_hook_type_t whichHook)
int bdd_enable_reordering_reporting (bdd_manager *mgr)
int bdd_disable_reordering_reporting (bdd_manager *mgr)
bdd_reorder_verbosity_t bdd_reordering_reporting (bdd_manager *mgr)
int bdd_print_apa_minterm (FILE *fp, bdd_t *f, int nvars, int precision)
int bdd_apa_compare_ratios (int nvars, bdd_t *f1, bdd_t *f2, int f1Num, int f2Num)
int bdd_read_node_count (bdd_manager *mgr)
int bdd_reordering_zdd_status (bdd_manager *mgr, bdd_reorder_type_t *method)
bdd_node * bdd_bdd_to_add (bdd_manager *mgr, bdd_node *fn)
bdd_node * bdd_add_permute (bdd_manager *mgr, bdd_node *fn, int *permut)
bdd_node * bdd_bdd_permute (bdd_manager *mgr, bdd_node *fn, int *permut)
void bdd_ref (bdd_node *fn)
void bdd_recursive_deref (bdd_manager *mgr, bdd_node *f)
bdd_node * bdd_add_exist_abstract (bdd_manager *mgr, bdd_node *fn, bdd_node *vars)
bdd_node * bdd_add_apply (bdd_manager *mgr, bdd_node *(*operation)(bdd_manager *, bdd_node **, bdd_node **), bdd_node *fn1, bdd_node *fn2)
bdd_node * bdd_add_nonsim_compose (bdd_manager *mgr, bdd_node *fn, bdd_node **vector)
bdd_node * bdd_add_residue (bdd_manager *mgr, int n, int m, int options, int top)
bdd_node * bdd_add_vector_compose (bdd_manager *mgr, bdd_node *fn, bdd_node **vector)
bdd_node * bdd_add_times (bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2)
int bdd_check_zero_ref (bdd_manager *mgr)
void bdd_dynamic_reordering_disable (bdd_manager *mgr)
void bdd_dynamic_reordering_zdd_disable (bdd_manager *mgr)
bdd_node * bdd_add_xnor (bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2)
int bdd_shuffle_heap (bdd_manager *mgr, int *permut)
bdd_node * bdd_add_compose (bdd_manager *mgr, bdd_node *fn1, bdd_node *fn2, int var)
bdd_node * bdd_add_ith_var (bdd_manager *mgr, int i)
int bdd_get_level_from_id (bdd_manager *mgr, int id)
bdd_node * bdd_bdd_exist_abstract (bdd_manager *mgr, bdd_node *fn, bdd_node *cube)
int bdd_equal_sup_norm (bdd_manager *mgr, bdd_node *fn, bdd_node *gn, BDD_VALUE_TYPE tolerance, int pr)
bdd_node * bdd_read_logic_zero (bdd_manager *mgr)
bdd_node * bdd_bdd_ith_var (bdd_manager *mgr, int i)
bdd_node * bdd_add_divide (bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2)
bdd_node * bdd_bdd_constrain (bdd_manager *mgr, bdd_node *f, bdd_node *c)
bdd_node * bdd_bdd_restrict (bdd_manager *mgr, bdd_node *f, bdd_node *c)
bdd_node * bdd_add_hamming (bdd_manager *mgr, bdd_node **xVars, bdd_node **yVars, int nVars)
bdd_node * bdd_add_ite (bdd_manager *mgr, bdd_node *f, bdd_node *g, bdd_node *h)
bdd_node * bdd_add_find_max (bdd_manager *mgr, bdd_node *f)
int bdd_bdd_pick_one_cube (bdd_manager *mgr, bdd_node *node, char *string)
bdd_node * bdd_add_swap_variables (bdd_manager *mgr, bdd_node *f, bdd_node **x, bdd_node **y, int n)
bdd_node * bdd_bdd_swap_variables (bdd_manager *mgr, bdd_node *f, bdd_node **x, bdd_node **y, int n)
bdd_node * bdd_bdd_or (bdd_manager *mgr, bdd_node *f, bdd_node *g)
bdd_node * bdd_bdd_compute_cube (bdd_manager *mgr, bdd_node **vars, int *phase, int n)
bdd_node * bdd_indices_to_cube (bdd_manager *mgr, int *idArray, int n)
bdd_node * bdd_bdd_and (bdd_manager *mgr, bdd_node *f, bdd_node *g)
bdd_node * bdd_add_matrix_multiply (bdd_manager *mgr, bdd_node *A, bdd_node *B, bdd_node **z, int nz)
bdd_node * bdd_add_compute_cube (bdd_manager *mgr, bdd_node **vars, int *phase, int n)
bdd_node * bdd_add_const (bdd_manager *mgr, BDD_VALUE_TYPE c)
double bdd_count_minterm (bdd_manager *mgr, bdd_node *f, int n)
bdd_node * bdd_add_bdd_threshold (bdd_manager *mgr, bdd_node *f, BDD_VALUE_TYPE value)
bdd_node * bdd_add_bdd_strict_threshold (bdd_manager *mgr, bdd_node *f, BDD_VALUE_TYPE value)
BDD_VALUE_TYPE bdd_read_epsilon (bdd_manager *mgr)
bdd_node * bdd_read_one (bdd_manager *mgr)
bdd_node * bdd_bdd_pick_one_minterm (bdd_manager *mgr, bdd_node *f, bdd_node **vars, int n)
bdd_t * bdd_pick_one_minterm (bdd_t *f, array_t *varsArray)
array_t * bdd_bdd_pick_arbitrary_minterms (bdd_t *f, array_t *varsArray, int n, int k)
bdd_node * bdd_read_zero (bdd_manager *mgr)
bdd_node * bdd_bdd_new_var (bdd_manager *mgr)
bdd_node * bdd_bdd_and_abstract (bdd_manager *mgr, bdd_node *f, bdd_node *g, bdd_node *cube)
void bdd_deref (bdd_node *f)
bdd_node * bdd_add_plus (bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2)
int bdd_read_reorderings (bdd_manager *mgr)
int bdd_read_next_reordering (bdd_manager *mgr)
void bdd_set_next_reordering (bdd_manager *mgr, int next)
bdd_node * bdd_bdd_xnor (bdd_manager *mgr, bdd_node *f, bdd_node *g)
bdd_node * bdd_bdd_vector_compose (bdd_manager *mgr, bdd_node *f, bdd_node **vector)
bdd_node * bdd_extract_node_as_is (bdd_t *fn)
bdd_node * bdd_zdd_get_node (bdd_manager *mgr, int id, bdd_node *g, bdd_node *h)
bdd_node * bdd_zdd_product (bdd_manager *mgr, bdd_node *f, bdd_node *g)
bdd_node * bdd_zdd_product_recur (bdd_manager *mgr, bdd_node *f, bdd_node *g)
bdd_node * bdd_zdd_union (bdd_manager *mgr, bdd_node *f, bdd_node *g)
bdd_node * bdd_zdd_weak_div (bdd_manager *mgr, bdd_node *f, bdd_node *g)
bdd_node * bdd_zdd_weak_div_recur (bdd_manager *mgr, bdd_node *f, bdd_node *g)
bdd_node * bdd_zdd_isop_recur (bdd_manager *mgr, bdd_node *L, bdd_node *U, bdd_node **zdd_I)
bdd_node * bdd_zdd_isop (bdd_manager *mgr, bdd_node *L, bdd_node *U, bdd_node **zdd_I)
int bdd_zdd_get_cofactors3 (bdd_manager *mgr, bdd_node *f, int v, bdd_node **f1, bdd_node **f0, bdd_node **fd)
bdd_node * bdd_bdd_and_recur (bdd_manager *mgr, bdd_node *f, bdd_node *g)
bdd_node * bdd_unique_inter (bdd_manager *mgr, int v, bdd_node *f, bdd_node *g)
bdd_node * bdd_unique_inter_ivo (bdd_manager *mgr, int v, bdd_node *f, bdd_node *g)
bdd_node * bdd_zdd_diff (bdd_manager *mgr, bdd_node *f, bdd_node *g)
bdd_node * bdd_zdd_diff_recur (bdd_manager *mgr, bdd_node *f, bdd_node *g)
int bdd_num_zdd_vars (bdd_manager *mgr)
bdd_node * bdd_regular (bdd_node *f)
int bdd_is_constant (bdd_node *f)
int bdd_is_complement (bdd_node *f)
bdd_node * bdd_bdd_T (bdd_node *f)
bdd_node * bdd_bdd_E (bdd_node *f)
bdd_node * bdd_not_bdd_node (bdd_node *f)
void bdd_recursive_deref_zdd (bdd_manager *mgr, bdd_node *f)
int bdd_zdd_count (bdd_manager *mgr, bdd_node *f)
int bdd_read_zdd_level (bdd_manager *mgr, int index)
int bdd_zdd_vars_from_bdd_vars (bdd_manager *mgr, int multiplicity)
void bdd_zdd_realign_enable (bdd_manager *mgr)
void bdd_zdd_realign_disable (bdd_manager *mgr)
int bdd_zdd_realignment_enabled (bdd_manager *mgr)
void bdd_realign_enable (bdd_manager *mgr)
void bdd_realign_disable (bdd_manager *mgr)
int bdd_realignment_enabled (bdd_manager *mgr)
int bdd_node_read_index (bdd_node *f)
bdd_node * bdd_read_next (bdd_node *f)
void bdd_set_next (bdd_node *f, bdd_node *g)
int bdd_read_reordered_field (bdd_manager *mgr)
void bdd_set_reordered_field (bdd_manager *mgr, int n)
bdd_node * bdd_add_apply_recur (bdd_manager *mgr, bdd_node *(*operation)(bdd_manager *, bdd_node **, bdd_node **), bdd_node *fn1, bdd_node *fn2)
BDD_VALUE_TYPE bdd_add_value (bdd_node *f)
int bdd_print_minterm (bdd_t *f)
int bdd_print_cover (bdd_t *f)
bdd_t * bdd_xor_smooth (bdd_t *f, bdd_t *g, array_t *smoothing_vars)
bdd_node * bdd_read_plus_infinity (bdd_manager *mgr)
bdd_node * bdd_priority_select (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 **))
void bdd_set_background (bdd_manager *mgr, bdd_node *f)
bdd_node * bdd_read_background (bdd_manager *mgr)
bdd_node * bdd_bdd_cofactor (bdd_manager *mgr, bdd_node *f, bdd_node *g)
bdd_node * bdd_bdd_ite (bdd_manager *mgr, bdd_node *f, bdd_node *g, bdd_node *h)
bdd_node * bdd_add_minus (bdd_manager *mgr, bdd_node **fn1, bdd_node **fn2)
bdd_node * bdd_dxygtdxz (bdd_manager *mgr, int N, bdd_node **x, bdd_node **y, bdd_node **z)
bdd_node * bdd_bdd_univ_abstract (bdd_manager *mgr, bdd_node *fn, bdd_node *vars)
bdd_node * bdd_bdd_cprojection (bdd_manager *mgr, bdd_node *R, bdd_node *Y)
bdd_node * bdd_xeqy (bdd_manager *mgr, int N, bdd_node **x, bdd_node **y)
bdd_node * bdd_add_roundoff (bdd_manager *mgr, bdd_node *f, int N)
bdd_node * bdd_xgty (bdd_manager *mgr, int N, bdd_node **x, bdd_node **y)
bdd_node * bdd_add_cmpl (bdd_manager *mgr, bdd_node *f)
bdd_node * bdd_split_set (bdd_manager *mgr, bdd_node *f, bdd_node **x, int n, double m)
int bdd_debug_check (bdd_manager *mgr)
bdd_node * bdd_bdd_xor (bdd_manager *mgr, bdd_node *f, bdd_node *g)
void bdd_dump_blif (bdd_manager *mgr, int nBdds, bdd_node **bdds, char **inames, char **onames, char *model, FILE *fp)
void bdd_dump_blif_body (bdd_manager *mgr, int nBdds, bdd_node **bdds, char **inames, char **onames, FILE *fp)
void bdd_dump_dot (bdd_manager *mgr, int nBdds, bdd_node **bdds, char **inames, char **onames, FILE *fp)
bdd_node * bdd_make_bdd_from_zdd_cover (bdd_manager *mgr, bdd_node *node)
bdd_node * bdd_zdd_complement (bdd_manager *mgr, bdd_node *node)
bdd_node * bdd_bdd_vector_support (bdd_manager *mgr, bdd_node **F, int n)
int bdd_bdd_vector_support_size (bdd_manager *mgr, bdd_node **F, int n)
int bdd_bdd_support_size (bdd_manager *mgr, bdd_node *F)
bdd_node * bdd_bdd_support (bdd_manager *mgr, bdd_node *F)
bdd_node * bdd_add_general_vector_compose (bdd_manager *mgr, bdd_node *f, bdd_node **vectorOn, bdd_node **vectorOff)
int bdd_bdd_leq (bdd_manager *mgr, bdd_node *f, bdd_node *g)
bdd_node * bdd_bdd_boolean_diff (bdd_manager *mgr, bdd_node *f, int x)
int bdd_ptrcmp (bdd_t *f, bdd_t *g)
int bdd_ptrhash (bdd_t *f, int size)
bdd_t * bdd_subset_with_mask_vars (bdd_t *f, array_t *varsArray, array_t *maskVarsArray)
bdd_t * bdd_and_smooth_with_cube (bdd_t *f, bdd_t *g, bdd_t *cube)
bdd_t * bdd_smooth_with_cube (bdd_t *f, bdd_t *cube)
bdd_t * bdd_substitute_with_permut (bdd_t *f, int *permut)
array_t * bdd_substitute_array_with_permut (array_t *f_array, int *permut)
bdd_t * bdd_vector_compose (bdd_t *f, array_t *varArray, array_t *funcArray)
double * bdd_cof_minterm (bdd_t *f)
int bdd_var_is_dependent (bdd_t *f, bdd_t *var)
array_t * bdd_find_essential (bdd_t *f)
bdd_t * bdd_find_essential_cube (bdd_t *f)
int bdd_estimate_cofactor (bdd_t *f, bdd_t *var, int phase)
long bdd_read_peak_memory (bdd_manager *mgr)
int bdd_read_peak_live_node (bdd_manager *mgr)
int bdd_set_pi_var (bdd_manager *mgr, int index)
int bdd_set_ps_var (bdd_manager *mgr, int index)
int bdd_set_ns_var (bdd_manager *mgr, int index)
int bdd_is_pi_var (bdd_manager *mgr, int index)
int bdd_is_ps_var (bdd_manager *mgr, int index)
int bdd_is_ns_var (bdd_manager *mgr, int index)
int bdd_set_pair_index (bdd_manager *mgr, int index, int pairIndex)
int bdd_read_pair_index (bdd_manager *mgr, int index)
int bdd_set_var_to_be_grouped (bdd_manager *mgr, int index)
int bdd_set_var_hard_group (bdd_manager *mgr, int index)
int bdd_reset_var_to_be_grouped (bdd_manager *mgr, int index)
int bdd_is_var_to_be_grouped (bdd_manager *mgr, int index)
int bdd_is_var_hard_group (bdd_manager *mgr, int index)
int bdd_is_var_to_be_ungrouped (bdd_manager *mgr, int index)
int bdd_set_var_to_be_ungrouped (bdd_manager *mgr, int index)
int bdd_bind_var (bdd_manager *mgr, int index)
int bdd_unbind_var (bdd_manager *mgr, int index)
int bdd_is_lazy_sift (bdd_manager *mgr)
void bdd_discard_all_var_groups (bdd_manager *mgr)

Function Documentation

bdd_node* bdd_add_apply ( bdd_manager *  mgr,
bdd_node *(*)(bdd_manager *, bdd_node **, bdd_node **)  operation,
bdd_node *  fn1,
bdd_node *  fn2 
)

Definition at line 1609 of file cmuPort.c.

01614 {
01615   return NIL(bdd_node);
01616 }

bdd_node* bdd_add_apply_recur ( bdd_manager *  mgr,
bdd_node *(*)(bdd_manager *, bdd_node **, bdd_node **)  operation,
bdd_node *  fn1,
bdd_node *  fn2 
)

Definition at line 2357 of file cmuPort.c.

02362 {
02363     return NIL(bdd_node);
02364 }

bdd_node* bdd_add_bdd_strict_threshold ( bdd_manager *  mgr,
bdd_node *  f,
BDD_VALUE_TYPE  value 
)

Definition at line 1951 of file cmuPort.c.

01955 {
01956     return NIL(bdd_node);
01957 }

bdd_node* bdd_add_bdd_threshold ( bdd_manager *  mgr,
bdd_node *  f,
BDD_VALUE_TYPE  value 
)

Definition at line 1941 of file cmuPort.c.

01945 {
01946     return NIL(bdd_node);
01947 }

bdd_node* bdd_add_cmpl ( bdd_manager *  mgr,
bdd_node *  f 
)

Definition at line 2537 of file cmuPort.c.

02540 {
02541   return NIL(bdd_node);
02542 
02543 } /* end of bdd_add_cmpl */

bdd_node* bdd_add_compose ( bdd_manager *  mgr,
bdd_node *  fn1,
bdd_node *  fn2,
int  var 
)

Definition at line 1701 of file cmuPort.c.

01706 {
01707   return NIL(bdd_node);
01708 }

bdd_node* bdd_add_compute_cube ( bdd_manager *  mgr,
bdd_node **  vars,
int *  phase,
int  n 
)

Definition at line 1911 of file cmuPort.c.

01916 {
01917     return NIL(bdd_node);
01918 }

bdd_node* bdd_add_const ( bdd_manager *  mgr,
BDD_VALUE_TYPE  c 
)

Definition at line 1922 of file cmuPort.c.

01925 {
01926     return NIL(bdd_node);
01927 }

bdd_node* bdd_add_divide ( bdd_manager *  mgr,
bdd_node **  fn1,
bdd_node **  fn2 
)

Definition at line 1766 of file cmuPort.c.

01770 {
01771   return NIL(bdd_node);
01772 }

bdd_node* bdd_add_exist_abstract ( bdd_manager *  mgr,
bdd_node *  fn,
bdd_node *  vars 
)

Definition at line 1599 of file cmuPort.c.

01603 {
01604   return NIL(bdd_node);
01605 }

bdd_node* bdd_add_find_max ( bdd_manager *  mgr,
bdd_node *  f 
)

Definition at line 1817 of file cmuPort.c.

01820 {
01821     return NIL(bdd_node);
01822 }

bdd_node* bdd_add_general_vector_compose ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node **  vectorOn,
bdd_node **  vectorOff 
)

Definition at line 2658 of file cmuPort.c.

02663 {
02664   return NIL(bdd_node);
02665 }

bdd_node* bdd_add_hamming ( bdd_manager *  mgr,
bdd_node **  xVars,
bdd_node **  yVars,
int  nVars 
)

Definition at line 1795 of file cmuPort.c.

01800 {
01801     return NIL(bdd_node);
01802 }

int bdd_add_hook ( bdd_manager *  mgr,
int(*)(bdd_manager *, char *, void *)  procedure,
bdd_hook_type_t  whichHook 
)

Definition at line 1486 of file cmuPort.c.

01490 {
01491   return 0;
01492 }

bdd_node* bdd_add_ite ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g,
bdd_node *  h 
)

Definition at line 1806 of file cmuPort.c.

01811 {
01812     return NIL(bdd_node);
01813 }

bdd_node* bdd_add_ith_var ( bdd_manager *  mgr,
int  i 
)

Definition at line 1712 of file cmuPort.c.

01715 {
01716   return NIL(bdd_node);
01717 }

bdd_node* bdd_add_matrix_multiply ( bdd_manager *  mgr,
bdd_node *  A,
bdd_node *  B,
bdd_node **  z,
int  nz 
)

Definition at line 1899 of file cmuPort.c.

01905 {
01906     return NIL(bdd_node);
01907 }

bdd_node* bdd_add_minus ( bdd_manager *  mgr,
bdd_node **  fn1,
bdd_node **  fn2 
)

Definition at line 2460 of file cmuPort.c.

02464 {
02465     return NIL(bdd_node);
02466 
02467 } /* end of bdd_add_plus */

bdd_node* bdd_add_nonsim_compose ( bdd_manager *  mgr,
bdd_node *  fn,
bdd_node **  vector 
)

Definition at line 1620 of file cmuPort.c.

01624 {
01625   return NIL(bdd_node);
01626 }

bdd_node* bdd_add_permute ( bdd_manager *  mgr,
bdd_node *  fn,
int *  permut 
)

Definition at line 1567 of file cmuPort.c.

01571 {
01572   return NIL(bdd_node);
01573 }

bdd_node* bdd_add_plus ( bdd_manager *  mgr,
bdd_node **  fn1,
bdd_node **  fn2 
)

Definition at line 2032 of file cmuPort.c.

02036 {
02037   return NIL(bdd_node);
02038 }

bdd_node* bdd_add_residue ( bdd_manager *  mgr,
int  n,
int  m,
int  options,
int  top 
)

Definition at line 1630 of file cmuPort.c.

01636 {
01637   return NIL(bdd_node);
01638 }

bdd_node* bdd_add_roundoff ( bdd_manager *  mgr,
bdd_node *  f,
int  N 
)

Definition at line 2516 of file cmuPort.c.

02520 {
02521   return NIL(bdd_node);
02522 
02523 } /* end of bdd_add_roundoff */

bdd_node* bdd_add_swap_variables ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node **  x,
bdd_node **  y,
int  n 
)

Definition at line 1836 of file cmuPort.c.

01842 {
01843     return NIL(bdd_node);
01844 }

bdd_node* bdd_add_times ( bdd_manager *  mgr,
bdd_node **  fn1,
bdd_node **  fn2 
)

Definition at line 1652 of file cmuPort.c.

01656 {
01657   return NIL(bdd_node);
01658 }

BDD_VALUE_TYPE bdd_add_value ( bdd_node *  f  ) 

Definition at line 2367 of file cmuPort.c.

02368 {
02369     return 0.0; 
02370 }

bdd_node* bdd_add_vector_compose ( bdd_manager *  mgr,
bdd_node *  fn,
bdd_node **  vector 
)

Definition at line 1642 of file cmuPort.c.

01646 {
01647   return NIL(bdd_node);
01648 }

bdd_node* bdd_add_xnor ( bdd_manager *  mgr,
bdd_node **  fn1,
bdd_node **  fn2 
)

Definition at line 1682 of file cmuPort.c.

01686 {
01687   return NIL(bdd_node);
01688 }

bdd_t* bdd_and ( bdd_t *  f,
bdd_t *  g,
boolean  f_phase,
boolean  g_phase 
)

Definition at line 250 of file cmuPort.c.

00255 {
00256   struct bdd_ *temp1, *temp2;
00257   bdd_t *result;
00258   struct bdd_manager_ *mgr;
00259   
00260   mgr = f->mgr;
00261   temp1 = ( (f_phase == TRUE) ? cmu_bdd_identity(mgr, f->node) : cmu_bdd_not(mgr, f->node));
00262   temp2 = ( (g_phase == TRUE) ? cmu_bdd_identity(mgr, g->node) : cmu_bdd_not(mgr, g->node));
00263   result = bdd_construct_bdd_t(mgr, cmu_bdd_and(mgr, temp1, temp2));
00264   cmu_bdd_free(mgr, temp1);
00265   cmu_bdd_free(mgr, temp2);
00266   return result;
00267 }

bdd_t* bdd_and_array ( bdd_t *  f,
array_t *  g_array,
boolean  f_phase,
boolean  g_phase 
)

Definition at line 282 of file cmuPort.c.

00287 {
00288   struct bdd_ *temp1, *temp2, *result;
00289   bdd_t *g;
00290   struct bdd_manager_ *mgr;
00291   int i;
00292 
00293   mgr = f->mgr;
00294   result = ((f_phase == TRUE) ? cmu_bdd_identity(mgr, f->node) :
00295             cmu_bdd_not(mgr, f->node)); 
00296 
00297   for (i = 0; i < array_n(g_array); i++) {
00298     g = array_fetch(bdd_t *, g_array, i);
00299     temp1 = result;
00300     temp2 = ((g_phase == TRUE) ? cmu_bdd_identity(mgr, g->node) :
00301              cmu_bdd_not(mgr, g->node));
00302     result = cmu_bdd_and(mgr, temp1, temp2);
00303     cmu_bdd_free(mgr, temp1);
00304     cmu_bdd_free(mgr, temp2);
00305     if (result == NULL)
00306       return(NULL);
00307   }
00308 
00309   return(bdd_construct_bdd_t(mgr, result));
00310 }

bdd_t* bdd_and_smooth ( bdd_t *  f,
bdd_t *  g,
array_t *  smoothing_vars 
)

Definition at line 436 of file cmuPort.c.

00440 {
00441   int num_vars, i;
00442   bdd_t *fn, *result;
00443   struct bdd_ **assoc;
00444   struct bdd_manager_ *mgr;
00445   
00446   num_vars = array_n(smoothing_vars);
00447   if (num_vars <= 0) {
00448         cmu_bdd_fatal("bdd_and_smooth: no smoothing variables");
00449   }
00450   
00451   assoc = ALLOC(struct bdd_ *, num_vars+1);
00452   
00453   for (i = 0; i < num_vars; i++) {
00454         fn = array_fetch(bdd_t *, smoothing_vars, i);
00455         assoc[i] = fn->node;
00456   }
00457   assoc[num_vars] = (struct bdd_ *) 0;
00458   
00459   mgr = f->mgr;
00460   cmu_bdd_temp_assoc(mgr, assoc, 0);
00461   (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current association */
00462   
00463   result = bdd_construct_bdd_t(mgr, cmu_bdd_rel_prod(mgr, f->node, g->node));
00464   FREE(assoc);
00465   return result;
00466 }

bdd_t* bdd_and_smooth_with_cube ( bdd_t *  f,
bdd_t *  g,
bdd_t *  cube 
)

Definition at line 2728 of file cmuPort.c.

02732 {
02733   return NIL(bdd_t);
02734 }

bdd_t* bdd_and_smooth_with_limit ( bdd_t *  f,
bdd_t *  g,
array_t *  smoothing_vars,
unsigned int  limit 
)

Definition at line 469 of file cmuPort.c.

00474 {
00475   /* Unsupported: fall back to standard and_smooth */
00476   return bdd_and_smooth(f, g, smoothing_vars);
00477 }

bdd_t* bdd_and_with_limit ( bdd_t *  f,
bdd_t *  g,
boolean  f_phase,
boolean  g_phase,
unsigned int  limit 
)

Definition at line 270 of file cmuPort.c.

00276 {
00277   /* Unsupported: fall back on standard AND. */
00278   return bdd_and(f, g, f_phase, g_phase);
00279 }

int bdd_apa_compare_ratios ( int  nvars,
bdd_t *  f1,
bdd_t *  f2,
int  f1Num,
int  f2Num 
)

Definition at line 1532 of file cmuPort.c.

01538 {
01539   return 0;
01540 }

bdd_t* bdd_approx_biased_rua ( bdd_t *  f,
bdd_approx_dir_t  approxDir,
bdd_t *  bias,
int  numVars,
int  threshold,
double  quality,
double  quality1 
)

Definition at line 1418 of file cmuPort.c.

01426 {
01427   return NIL(bdd_t);
01428 }

bdd_t* bdd_approx_compress ( bdd_t *  f,
bdd_approx_dir_t  approxDir,
int  numVars,
int  threshold 
)

Definition at line 1431 of file cmuPort.c.

01436 {
01437   return NIL(bdd_t);
01438 }

int bdd_approx_decomp ( bdd_t *  f,
bdd_partition_type_t  partType,
bdd_t ***  conjArray 
)

Definition at line 1459 of file cmuPort.c.

01463 {
01464   return 0;
01465 }

bdd_t* bdd_approx_hb ( bdd_t *  f,
bdd_approx_dir_t  approxDir,
int  numVars,
int  threshold 
)

Definition at line 1374 of file cmuPort.c.

01379 {
01380   return NIL(bdd_t);
01381 }

bdd_t* bdd_approx_remap_ua ( bdd_t *  f,
bdd_approx_dir_t  approxDir,
int  numVars,
int  threshold,
double  quality 
)

Definition at line 1407 of file cmuPort.c.

01413 {
01414   return NIL(bdd_t);
01415 }

bdd_t* bdd_approx_sp ( bdd_t *  f,
bdd_approx_dir_t  approxDir,
int  numVars,
int  threshold,
int  hardlimit 
)

Definition at line 1384 of file cmuPort.c.

01390 {
01391   return NIL(bdd_t);
01392 }

bdd_t* bdd_approx_ua ( bdd_t *  f,
bdd_approx_dir_t  approxDir,
int  numVars,
int  threshold,
int  safe,
double  quality 
)

Definition at line 1395 of file cmuPort.c.

01402 {
01403   return NIL(bdd_t);
01404 }

bdd_node* bdd_bdd_and ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 1889 of file cmuPort.c.

01893 {
01894     return NIL(bdd_node);
01895 }

bdd_node* bdd_bdd_and_abstract ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g,
bdd_node *  cube 
)

Definition at line 2017 of file cmuPort.c.

02022 {
02023     return NIL(bdd_node);
02024 }

bdd_node* bdd_bdd_and_recur ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2175 of file cmuPort.c.

02179 {
02180      return NIL(bdd_node);
02181 }

bdd_node* bdd_bdd_boolean_diff ( bdd_manager *  mgr,
bdd_node *  f,
int  x 
)

Definition at line 2677 of file cmuPort.c.

02681 {
02682   return NIL(bdd_node);
02683 }

bdd_node* bdd_bdd_cofactor ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2437 of file cmuPort.c.

02441 {
02442     return NIL(bdd_node);
02443 
02444 } /* end of bdd_bdd_cofactor */

bdd_node* bdd_bdd_compute_cube ( bdd_manager *  mgr,
bdd_node **  vars,
int *  phase,
int  n 
)

Definition at line 1869 of file cmuPort.c.

01874 {
01875     return NIL(bdd_node);
01876 }

bdd_node* bdd_bdd_constrain ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  c 
)

Definition at line 1776 of file cmuPort.c.

01780 {
01781     return NIL(bdd_node);
01782 }

bdd_node* bdd_bdd_cprojection ( bdd_manager *  mgr,
bdd_node *  R,
bdd_node *  Y 
)

Definition at line 2495 of file cmuPort.c.

02499 {
02500     return NIL(bdd_node);
02501 
02502 } /* end of bdd_bdd_cprojection */

bdd_node* bdd_bdd_E ( bdd_node *  f  ) 

Definition at line 2253 of file cmuPort.c.

02254 {
02255     return NIL(bdd_node);
02256 }

bdd_node* bdd_bdd_exist_abstract ( bdd_manager *  mgr,
bdd_node *  fn,
bdd_node *  cube 
)

Definition at line 1730 of file cmuPort.c.

01734 {
01735   return NIL(bdd_node);
01736 }

bdd_node* bdd_bdd_ite ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g,
bdd_node *  h 
)

Definition at line 2448 of file cmuPort.c.

02453 {
02454     return NIL(bdd_node);
02455 
02456 } /* end of bdd_bdd_ite */

bdd_node* bdd_bdd_ith_var ( bdd_manager *  mgr,
int  i 
)

Definition at line 1759 of file cmuPort.c.

01760 {
01761     return NIL(bdd_node);
01762 }

int bdd_bdd_leq ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2668 of file cmuPort.c.

02672 {
02673   return -1;
02674 }

bdd_node* bdd_bdd_new_var ( bdd_manager *  mgr  ) 

Definition at line 2010 of file cmuPort.c.

02011 {
02012     return NIL(bdd_node);
02013 }

bdd_node* bdd_bdd_or ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 1859 of file cmuPort.c.

01863 {
01864     return NIL(bdd_node);
01865 }

bdd_node* bdd_bdd_permute ( bdd_manager *  mgr,
bdd_node *  fn,
int *  permut 
)

Definition at line 1576 of file cmuPort.c.

01580 {
01581   return NIL(bdd_node);
01582 }

array_t* bdd_bdd_pick_arbitrary_minterms ( bdd_t *  f,
array_t *  varsArray,
int  n,
int  k 
)

Definition at line 1993 of file cmuPort.c.

01998 {
01999     return NIL(array_t);
02000 }

int bdd_bdd_pick_one_cube ( bdd_manager *  mgr,
bdd_node *  node,
char *  string 
)

Definition at line 1826 of file cmuPort.c.

01830 {
01831     return 0;
01832 }

bdd_node* bdd_bdd_pick_one_minterm ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node **  vars,
int  n 
)

Definition at line 1973 of file cmuPort.c.

01978 {
01979     return NIL(bdd_node);
01980 }

bdd_node* bdd_bdd_restrict ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  c 
)

Definition at line 1785 of file cmuPort.c.

01789 {
01790     return NIL(bdd_node);
01791 }

bdd_node* bdd_bdd_support ( bdd_manager *  mgr,
bdd_node *  F 
)

Definition at line 2650 of file cmuPort.c.

02653 {
02654   return NIL(bdd_node);
02655 }

int bdd_bdd_support_size ( bdd_manager *  mgr,
bdd_node *  F 
)

Definition at line 2642 of file cmuPort.c.

02645 {
02646   return -1;
02647 }

bdd_node* bdd_bdd_swap_variables ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node **  x,
bdd_node **  y,
int  n 
)

Definition at line 1847 of file cmuPort.c.

01853 {
01854     return NIL(bdd_node);
01855 }

bdd_node* bdd_bdd_T ( bdd_node *  f  ) 

Definition at line 2247 of file cmuPort.c.

02248 {
02249     return NIL(bdd_node);
02250 }

bdd_node* bdd_bdd_to_add ( bdd_manager *  mgr,
bdd_node *  fn 
)

Definition at line 1559 of file cmuPort.c.

01562 {
01563   return NIL(bdd_node);
01564 }

bdd_node* bdd_bdd_univ_abstract ( bdd_manager *  mgr,
bdd_node *  fn,
bdd_node *  vars 
)

Definition at line 2484 of file cmuPort.c.

02488 {
02489     return NIL(bdd_node);
02490 
02491 } /* end of bdd_bdd_univ_abstract */

bdd_node* bdd_bdd_vector_compose ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node **  vector 
)

Definition at line 2069 of file cmuPort.c.

02073 {
02074     return NIL(bdd_node);
02075 }

bdd_node* bdd_bdd_vector_support ( bdd_manager *  mgr,
bdd_node **  F,
int  n 
)

Definition at line 2624 of file cmuPort.c.

02628 {
02629   return NIL(bdd_node);
02630 }

int bdd_bdd_vector_support_size ( bdd_manager *  mgr,
bdd_node **  F,
int  n 
)

Definition at line 2633 of file cmuPort.c.

02637 {
02638   return -1;
02639 }

bdd_node* bdd_bdd_xnor ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2060 of file cmuPort.c.

02064 {
02065     return NIL(bdd_node);
02066 }

bdd_node* bdd_bdd_xor ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2566 of file cmuPort.c.

02570 {
02571     return NIL(bdd_node);
02572 }

bdd_t* bdd_between ( bdd_t *  f_min,
bdd_t *  f_max 
)

Definition at line 480 of file cmuPort.c.

00481 {
00482   bdd_t *temp, *ret;
00483   long size1, size2, size3; 
00484   temp = bdd_or(f_min, f_max, 1, 0);
00485   ret = bdd_minimize(f_min, temp);
00486   bdd_free(temp);
00487   size1 = bdd_size(f_min);
00488   size2 = bdd_size(f_max);
00489   size3 = bdd_size(ret);
00490   if (size3 < size1) {
00491         if (size3 < size2){
00492       return ret;
00493     }
00494     else {
00495       bdd_free(ret);
00496       return bdd_dup(f_max);
00497     }
00498   }
00499   else {
00500     bdd_free(ret);
00501     if (size1 < size2){
00502       return bdd_dup(f_min);
00503     }
00504     else {
00505       return bdd_dup(f_max);
00506     }
00507   }
00508 }

int bdd_bind_var ( bdd_manager *  mgr,
int  index 
)

Definition at line 2920 of file cmuPort.c.

02921 {
02922     return(0);
02923 }

int bdd_check_zero_ref ( bdd_manager *  mgr  ) 

Definition at line 1662 of file cmuPort.c.

01663 {
01664   return 0;
01665 }

bdd_t* bdd_clipping_and_smooth ( bdd_t *  f,
bdd_t *  g,
array_t *  smoothing_vars,
int  maxDepth,
int  over 
)

Definition at line 1363 of file cmuPort.c.

01369 {
01370   return NIL(bdd_t);
01371 }

bdd_t* bdd_closest_cube ( bdd_t *  f,
bdd_t *  g,
int *  dist 
)

Definition at line 885 of file cmuPort.c.

00886 {
00887     return (NULL);
00888 }

double* bdd_cof_minterm ( bdd_t *  f  ) 

Definition at line 2788 of file cmuPort.c.

02789 {
02790   return(NIL(double));
02791 }

bdd_t* bdd_cofactor ( bdd_t *  f,
bdd_t *  g 
)

Definition at line 511 of file cmuPort.c.

00512 {
00513   return bdd_construct_bdd_t(f->mgr, cmu_bdd_cofactor(f->mgr, f->node, g->node));
00514 }

bdd_t* bdd_cofactor_array ( bdd_t *  f,
array_t *  bddArray 
)

Definition at line 517 of file cmuPort.c.

00518 {
00519   bdd_t *operand;
00520   struct bdd_ *result, *temp;
00521   int i;
00522 
00523   result = cmu_bdd_identity(f->mgr, f->node);
00524 
00525   for (i = 0; i < array_n(bddArray); i++) {
00526     operand = array_fetch(bdd_t *, bddArray, i);
00527     temp = cmu_bdd_cofactor(f->mgr, result, operand->node);
00528     if (temp == NULL) {
00529       cmu_bdd_free(f->mgr, result);
00530       return(NULL);
00531     }
00532     cmu_bdd_free(f->mgr, result);
00533     result = temp;
00534   }
00535 
00536   return(bdd_construct_bdd_t(f->mgr, result));
00537 }

bdd_t* bdd_compact ( bdd_t *  f,
bdd_t *  g 
)

Definition at line 1304 of file cmuPort.c.

01305 {
01306     return (NULL);
01307 }

bdd_t* bdd_compose ( bdd_t *  f,
bdd_t *  v,
bdd_t *  g 
)

Definition at line 540 of file cmuPort.c.

00544 {
00545   return bdd_construct_bdd_t(f->mgr, cmu_bdd_compose(f->mgr, f->node, v->node, g->node));
00546 }

bdd_t* bdd_compute_cube ( bdd_manager *  mgr,
array_t *  vars 
)

Function********************************************************************

Synopsis [Dummy functions defined in bdd.h]

SideEffects []

Definition at line 1346 of file cmuPort.c.

01349 {
01350   return NIL(bdd_t);
01351 }

bdd_t* bdd_compute_cube_with_phase ( bdd_manager *  mgr,
array_t *  vars,
array_t *  phase 
)

Definition at line 1354 of file cmuPort.c.

01358 {
01359   return NIL(bdd_t);
01360 }

bdd_t* bdd_consensus ( bdd_t *  f,
array_t *  quantifying_vars 
)

Definition at line 549 of file cmuPort.c.

00552 {
00553   int num_vars, i;
00554   bdd_t *fn, *result;
00555   struct bdd_ **assoc;
00556   struct bdd_manager_ *mgr;
00557   
00558   num_vars = array_n(quantifying_vars);
00559   if (num_vars <= 0) {
00560         cmu_bdd_fatal("bdd_consensus: no quantifying variables");
00561   }
00562   
00563   assoc = ALLOC(struct bdd_ *, num_vars+1);
00564   
00565   for (i = 0; i < num_vars; i++) {
00566         fn = array_fetch(bdd_t *, quantifying_vars, i);
00567         assoc[i] = fn->node;
00568   }
00569   assoc[num_vars] = (struct bdd_ *) 0;
00570   
00571   mgr = f->mgr;
00572   cmu_bdd_temp_assoc(mgr, assoc, 0);
00573   (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current association */
00574   
00575   result = bdd_construct_bdd_t(mgr, cmu_bdd_forall(mgr, f->node));
00576   FREE(assoc);
00577   return result;
00578 }

bdd_t* bdd_construct_bdd_t ( bdd_manager *  manager,
bdd_node *  func 
)

CFile***********************************************************************

FileName [cmuPort.c]

PackageName [cmu_port]

Synopsis [Port routines for CMU package.]

Description [optional]

SeeAlso [optional]

Author [Thomas R. Shiple. Some changes by Rajeev K. Ranjan.]

Copyright [Copyright (c) 1994-1996 The Regents of the Univ. of California. All rights reserved.

Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.

IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE SOFTWARE PROVIDED HEREUNDER IS ON AN "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]

Revision [

Id
cmuPort.c,v 1.80 2009/04/11 16:13:17 fabio Exp

]AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Builds the bdd_t structure.]

Description [Builds the bdd_t structure from manager and node. Assumes that the reference count of the node has already been increased.]

SideEffects []

Definition at line 93 of file cmuPort.c.

00094 {
00095     bdd_t *result;
00096     cmu_bdd_manager mgr = (cmu_bdd_manager)manager;
00097     bdd fn = (bdd)func;
00098 
00099     if (fn == (struct bdd_ *) 0) {
00100         cmu_bdd_fatal("bdd_construct_bdd_t: possible memory overflow");
00101     }
00102 
00103     result = ALLOC(bdd_t, 1);
00104     result->mgr = mgr;
00105     result->node = fn;
00106     result->free = FALSE;
00107     return result;
00108 }

double bdd_correlation ( bdd_t *  f,
bdd_t *  g 
)

Definition at line 1317 of file cmuPort.c.

01318 {
01319     return (0.0);
01320 }

double bdd_count_minterm ( bdd_manager *  mgr,
bdd_node *  f,
int  n 
)

Definition at line 1931 of file cmuPort.c.

01935 {
01936     return 0;
01937 }

double bdd_count_onset ( bdd_t *  f,
array_t *  var_array 
)

Definition at line 972 of file cmuPort.c.

00975 {
00976     int num_vars;
00977     double fraction;
00978 
00979     num_vars = array_n(var_array);
00980     fraction = cmu_bdd_satisfying_fraction(f->mgr, f->node); /* cannot give support vars */
00981     return (fraction * pow((double) 2, (double) num_vars));
00982 }

bdd_t* bdd_cproject ( bdd_t *  f,
array_t *  quantifying_vars 
)

Definition at line 582 of file cmuPort.c.

00585 {
00586   int num_vars, i;
00587   bdd_t *fn, *result;
00588   struct bdd_ **assoc;
00589   struct bdd_manager_ *mgr;
00590   
00591   if (f == NIL(bdd_t)) fail ("bdd_cproject: invalid BDD");
00592   
00593   num_vars = array_n(quantifying_vars);
00594   if (num_vars <= 0) {
00595     printf("Warning: bdd_cproject: no projection variables\n");
00596     result = bdd_dup(f);
00597   }
00598   else {
00599     assoc = ALLOC(struct bdd_ *, num_vars+1);
00600     for (i = 0; i < num_vars; i++) {
00601       fn = array_fetch(bdd_t *, quantifying_vars, i);
00602       assoc[i] = fn->node;
00603     }
00604     assoc[num_vars] = (struct bdd_ *) 0;
00605     mgr = f->mgr;
00606     cmu_bdd_temp_assoc(mgr, assoc, 0);
00607     (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current a
00608                                        ssociation */
00609     
00610     result = bdd_construct_bdd_t(mgr, cmu_bdd_project(mgr, f->node));
00611     FREE(assoc);
00612   }
00613   return result;
00614 }

bdd_t* bdd_create_variable ( bdd_manager *  manager  ) 

Definition at line 171 of file cmuPort.c.

00172 {
00173   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00174   return bdd_construct_bdd_t(mgr, cmu_bdd_new_var_last(mgr));
00175 }

bdd_t* bdd_create_variable_after ( bdd_manager *  manager,
bdd_variableId  after_id 
)

Definition at line 178 of file cmuPort.c.

00179 {
00180   struct bdd_ *after_var;
00181   bdd_t         *result;
00182   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00183 
00184   after_var = cmu_bdd_var_with_id(mgr, (long)after_id + 1);
00185   
00186   result =  bdd_construct_bdd_t(mgr, cmu_bdd_new_var_after(mgr, after_var));
00187   
00188   /* No need to free after_var, since single variable BDDs are never garbage collected */
00189   
00190   return result;
00191 }

int bdd_debug_check ( bdd_manager *  mgr  ) 

Definition at line 2559 of file cmuPort.c.

02560 {
02561     return (-1);
02562 
02563 } /* end of bdd_debug_check */

void bdd_deref ( bdd_node *  f  ) 

Definition at line 2027 of file cmuPort.c.

02028 {
02029 }

int bdd_disable_reordering_reporting ( bdd_manager *  mgr  ) 

Definition at line 1510 of file cmuPort.c.

01511 {
01512   return 0;
01513 }

void bdd_discard_all_var_groups ( bdd_manager *  mgr  ) 

Definition at line 2938 of file cmuPort.c.

02939 {
02940     return;
02941 }

void bdd_dump_blif ( bdd_manager *  mgr,
int  nBdds,
bdd_node **  bdds,
char **  inames,
char **  onames,
char *  model,
FILE *  fp 
)

Definition at line 2575 of file cmuPort.c.

02583 {
02584   return;
02585 }

void bdd_dump_blif_body ( bdd_manager *  mgr,
int  nBdds,
bdd_node **  bdds,
char **  inames,
char **  onames,
FILE *  fp 
)

Definition at line 2588 of file cmuPort.c.

02595 {
02596   return;
02597 }

void bdd_dump_dot ( bdd_manager *  mgr,
int  nBdds,
bdd_node **  bdds,
char **  inames,
char **  onames,
FILE *  fp 
)

Definition at line 2600 of file cmuPort.c.

02607 {
02608   return;
02609 }

bdd_t* bdd_dup ( bdd_t *  f  ) 

Definition at line 217 of file cmuPort.c.

00218 {
00219   return bdd_construct_bdd_t(f->mgr, cmu_bdd_identity(f->mgr, f->node));
00220 }

bdd_node* bdd_dxygtdxz ( bdd_manager *  mgr,
int  N,
bdd_node **  x,
bdd_node **  y,
bdd_node **  z 
)

Definition at line 2471 of file cmuPort.c.

02477 {
02478     return NIL(bdd_node);
02479 
02480 } /* end of bdd_dxygtdxz */

void bdd_dynamic_reordering ( bdd_manager *  manager,
bdd_reorder_type_t  algorithm_type,
bdd_reorder_verbosity_t  verbosity 
)

Definition at line 1209 of file cmuPort.c.

01211 {
01212   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01213     switch(algorithm_type) {
01214     case BDD_REORDER_SIFT:
01215         cmu_bdd_dynamic_reordering(mgr, cmu_bdd_reorder_sift);
01216         break;
01217     case BDD_REORDER_WINDOW:
01218         cmu_bdd_dynamic_reordering(mgr, cmu_bdd_reorder_stable_window3);
01219         break;
01220     case BDD_REORDER_NONE:
01221         cmu_bdd_dynamic_reordering(mgr, cmu_bdd_reorder_none);
01222         break;
01223     default:
01224       fprintf(stderr,"CMU: bdd_dynamic_reordering: unknown algorithm type\n");
01225       fprintf(stderr,"Using SIFT method instead\n");
01226       cmu_bdd_dynamic_reordering(mgr, cmu_bdd_reorder_sift);
01227     }
01228 }

void bdd_dynamic_reordering_disable ( bdd_manager *  mgr  ) 

Definition at line 1669 of file cmuPort.c.

01670 {
01671   return;
01672 }

void bdd_dynamic_reordering_zdd ( bdd_manager *  manager,
bdd_reorder_type_t  algorithm_type,
bdd_reorder_verbosity_t  verbosity 
)

Definition at line 1231 of file cmuPort.c.

01233 {
01234     return;
01235 }

void bdd_dynamic_reordering_zdd_disable ( bdd_manager *  mgr  ) 

Definition at line 1675 of file cmuPort.c.

01676 {
01677   return;
01678 }

bdd_t* bdd_else ( bdd_t *  f  ) 

Definition at line 618 of file cmuPort.c.

00619 {
00620   return bdd_construct_bdd_t(f->mgr, cmu_bdd_else(f->mgr, f->node));
00621 }

int bdd_enable_reordering_reporting ( bdd_manager *  mgr  ) 

Definition at line 1504 of file cmuPort.c.

01505 {
01506   return 0;
01507 }

void bdd_end ( bdd_manager *  manager  ) 

Definition at line 129 of file cmuPort.c.

00130 {
00131     bdd_external_hooks *hooks;
00132     cmu_bdd_manager mgr = (cmu_bdd_manager)manager;
00133     hooks = (bdd_external_hooks *) mgr->hooks;
00134     FREE(hooks); 
00135     cmu_bdd_quit(mgr);
00136 }

int bdd_epd_count_onset ( bdd_t *  f,
array_t *  var_array,
EpDouble *  epd 
)

Function********************************************************************

Synopsis [Counts the number of minterms in the on set.]

SideEffects []

Definition at line 992 of file cmuPort.c.

00996 {
00997   double nMinterms;
00998 
00999   nMinterms = bdd_count_onset(f, var_array);
01000   EpdConvert(nMinterms, epd);
01001   return 0;
01002 } /* end of bdd_epd_count_onset */

boolean bdd_equal ( bdd_t *  f,
bdd_t *  g 
)

Definition at line 856 of file cmuPort.c.

00857 {
00858     return (f->node == g->node);
00859 }

boolean bdd_equal_mod_care_set ( bdd_t *  f,
bdd_t *  g,
bdd_t *  CareSet 
)

Definition at line 862 of file cmuPort.c.

00863 {
00864   bdd_t *diffBdd;
00865   boolean result;
00866 
00867   if (bdd_equal(f, g))
00868     return 1;
00869 
00870   diffBdd = bdd_xor(f, g);
00871 
00872   result = bdd_leq(diffBdd, CareSet, 1, 0);
00873   bdd_free(diffBdd);
00874 
00875   return(result);
00876 }

int bdd_equal_sup_norm ( bdd_manager *  mgr,
bdd_node *  fn,
bdd_node *  gn,
BDD_VALUE_TYPE  tolerance,
int  pr 
)

Definition at line 1740 of file cmuPort.c.

01746 {
01747   return 0;
01748 }

int bdd_estimate_cofactor ( bdd_t *  f,
bdd_t *  var,
int  phase 
)

Definition at line 2812 of file cmuPort.c.

02813 {
02814   return(0);
02815 }

bdd_node* bdd_extract_node_as_is ( bdd_t *  fn  ) 

Definition at line 2078 of file cmuPort.c.

02079 {
02080   return NIL(bdd_node);
02081 }

array_t* bdd_find_essential ( bdd_t *  f  ) 

Definition at line 2800 of file cmuPort.c.

02801 {
02802   return(NIL(array_t));
02803 }

bdd_t* bdd_find_essential_cube ( bdd_t *  f  ) 

Definition at line 2806 of file cmuPort.c.

02807 {
02808   return(NIL(bdd_t));
02809 }

void bdd_free ( bdd_t *  f  ) 

Definition at line 223 of file cmuPort.c.

00224 {
00225   if (f == NIL(bdd_t)) {
00226         fail("bdd_free: trying to free a NIL bdd_t");                   
00227   }
00228   
00229   if (f->free == TRUE) {
00230         fail("bdd_free: trying to free a freed bdd_t");                 
00231   }     
00232   
00233   cmu_bdd_free(f->mgr, f->node);
00234   
00235   /*
00236    * In case the user tries to free this bdd_t again, set the free field to TRUE, 
00237      * and NIL out the other fields.  Then free the bdd_t structure itself.
00238      */
00239   f->free = TRUE;
00240   f->node = NIL(struct bdd_);
00241   f->mgr = NIL(struct bdd_manager_);
00242   FREE(f);  
00243 }

int bdd_gen_decomp ( bdd_t *  f,
bdd_partition_type_t  partType,
bdd_t ***  conjArray 
)

Definition at line 1441 of file cmuPort.c.

01445 {
01446   return 0;
01447 }

bdd_external_hooks* bdd_get_external_hooks ( bdd_manager *  manager  ) 

Definition at line 1195 of file cmuPort.c.

01196 {
01197   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01198   return ((bdd_external_hooks *) mgr->hooks);
01199 }

int bdd_get_free ( bdd_t *  f  ) 

Definition at line 1005 of file cmuPort.c.

01006 {
01007     return (f->free);
01008 }

bdd_variableId bdd_get_id_from_level ( bdd_manager *  manager,
long  level 
)

Definition at line 1245 of file cmuPort.c.

01246 {
01247   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01248   struct bdd_ *fn;
01249 
01250   fn = cmu_bdd_var_with_index(mgr, level);
01251   
01252   if (fn == (struct bdd_ *) 0) {
01253     /* variable should always be found, since they are created at bdd_start */
01254     cmu_bdd_fatal("bdd_get_id_from_level: assumption violated");
01255   }
01256   
01257   return ((bdd_variableId)(cmu_bdd_if_id(mgr, fn) - 1 ));
01258   
01259 }

int bdd_get_level_from_id ( bdd_manager *  mgr,
int  id 
)

Definition at line 1721 of file cmuPort.c.

01724 {
01725   return 0;
01726 }

bdd_manager* bdd_get_manager ( bdd_t *  f  ) 

Definition at line 1011 of file cmuPort.c.

01012 {
01013     return (bdd_manager *) (f->mgr);
01014 }

bdd_node* bdd_get_node ( bdd_t *  f,
boolean *  is_complemented 
)

Definition at line 1017 of file cmuPort.c.

01020 {
01021     *is_complemented = (boolean) TAG0(f->node);  /* using bddint.h */
01022     return ((bdd_node *) BDD_POINTER(f->node));  /* using bddint.h */
01023 }

bdd_package_type_t bdd_get_package_name ( void   ) 

Function******************************************************************** Synopsis [required]

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 120 of file cmuPort.c.

00121 {
00122   return CMU;
00123 }

var_set_t* bdd_get_support ( bdd_t *  f  ) 

Definition at line 1026 of file cmuPort.c.

01027 {
01028     struct bdd_ **support, *var;
01029     struct bdd_manager_ *mgr;
01030     long num_vars;
01031     var_set_t *result;
01032     int id, i;
01033 
01034     mgr = f->mgr;
01035     num_vars = cmu_bdd_vars(mgr);
01036 
01037     result = var_set_new((int) num_vars);
01038     support = (struct bdd_ **) mem_get_block((num_vars+1) * sizeof(struct bdd_ *));
01039     (void) cmu_bdd_support(mgr, f->node, support);
01040 
01041     for (i = 0; i < num_vars; ++i) {  /* can never have more than num_var non-zero entries in array */
01042         var = support[i]; 
01043         if (var == (struct bdd_ *) 0) {
01044             break;  /* have reach end of null-terminated array */
01045         }
01046         id = (int) (cmu_bdd_if_id(mgr, var) - 1);  /* a variable is never garbage collected, so no need to free */
01047         var_set_set_elt(result, id);
01048     }
01049 
01050     mem_free_block((pointer)support);
01051 
01052     return result;
01053 }

bdd_t* bdd_get_variable ( bdd_manager *  manager,
bdd_variableId  variable_ID 
)

Definition at line 196 of file cmuPort.c.

00197 {
00198   struct bdd_ *fn;
00199   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00200   fn = cmu_bdd_var_with_id(mgr, (long) (variable_ID + 1));
00201 
00202   if (fn == (struct bdd_ *) 0) {
00203     int i;
00204     for (i=cmu_bdd_vars(mgr); i < variable_ID + 1; i++) {
00205       fn = cmu_bdd_new_var_last(mgr);
00206     }
00207   }
00208   
00209   return bdd_construct_bdd_t(mgr, fn);
00210 }

array_t* bdd_get_varids ( array_t *  var_array  ) 

Definition at line 1093 of file cmuPort.c.

01094 {
01095   int i;
01096   bdd_t *var;
01097   array_t *result;
01098  
01099   result = array_alloc(bdd_variableId, 0);
01100   for (i = 0; i < array_n(var_array); i++) {
01101     var = array_fetch(bdd_t *, var_array, i);
01102     array_insert_last(bdd_variableId, result, bdd_top_var_id(var));
01103   }
01104   return result;
01105 }

bdd_node* bdd_indices_to_cube ( bdd_manager *  mgr,
int *  idArray,
int  n 
)

Definition at line 1880 of file cmuPort.c.

01884 {
01885     return NIL(bdd_node);
01886 }

bdd_t* bdd_intersects ( bdd_t *  f,
bdd_t *  g 
)

Definition at line 879 of file cmuPort.c.

00880 {
00881     return bdd_construct_bdd_t(f->mgr, cmu_bdd_intersects(f->mgr, f->node, g->node));
00882 }

int bdd_is_complement ( bdd_node *  f  ) 

Definition at line 2241 of file cmuPort.c.

02242 {
02243     return 0;
02244 }

int bdd_is_constant ( bdd_node *  f  ) 

Definition at line 2235 of file cmuPort.c.

02236 {
02237     return 0;
02238 }

boolean bdd_is_cube ( bdd_t *  f  ) 

Definition at line 1272 of file cmuPort.c.

01273 {
01274   struct bdd_manager_ *manager;
01275 
01276   if (f == NIL(bdd_t)) {
01277         fail("bdd_is_cube: invalid BDD");
01278   }
01279   if(  f->free ) fail ("Freed Bdd passed to bdd_is_cube");
01280   manager = f->mgr;
01281   return ((boolean)cmu_bdd_is_cube(manager, f->node));
01282 }

int bdd_is_lazy_sift ( bdd_manager *  mgr  ) 

Definition at line 2932 of file cmuPort.c.

02933 {
02934     return(0);
02935 }

int bdd_is_ns_var ( bdd_manager *  mgr,
int  index 
)

Definition at line 2860 of file cmuPort.c.

02861 {
02862     return(0);
02863 }

int bdd_is_pi_var ( bdd_manager *  mgr,
int  index 
)

Definition at line 2848 of file cmuPort.c.

02849 {
02850     return(0);
02851 }

int bdd_is_ps_var ( bdd_manager *  mgr,
int  index 
)

Definition at line 2854 of file cmuPort.c.

02855 {
02856     return(0);
02857 }

int bdd_is_support_var ( bdd_t *  f,
bdd_t *  var 
)

Definition at line 1056 of file cmuPort.c.

01057 {
01058     return(bdd_is_support_var_id(f, bdd_top_var_id(var)));
01059 }

int bdd_is_support_var_id ( bdd_t *  f,
int  index 
)

Definition at line 1062 of file cmuPort.c.

01063 {
01064     struct bdd_ **support, *var;
01065     struct bdd_manager_ *mgr;
01066     long num_vars;
01067     int id, i;
01068 
01069     mgr = f->mgr;
01070     num_vars = cmu_bdd_vars(mgr);
01071 
01072     support = (struct bdd_ **) mem_get_block((num_vars+1) * sizeof(struct bdd_ *));
01073     (void) cmu_bdd_support(mgr, f->node, support);
01074 
01075     for (i = 0; i < num_vars; ++i) {  /* can never have more than num_var non-zero entries in array */
01076         var = support[i]; 
01077         if (var == (struct bdd_ *) 0) {
01078             break;  /* have reach end of null-terminated array */
01079         }
01080         id = (int) (cmu_bdd_if_id(mgr, var) - 1);  /* a variable is never garbage collected, so no need to free */
01081         if (id == index) {
01082             mem_free_block((pointer)support);
01083             return 1;
01084         }
01085     }
01086 
01087     mem_free_block((pointer)support);
01088 
01089     return 0;
01090 }

boolean bdd_is_tautology ( bdd_t *  f,
boolean  phase 
)

Definition at line 891 of file cmuPort.c.

00892 {
00893     return ((phase == TRUE) ? (f->node == cmu_bdd_one(f->mgr)) : (f->node == cmu_bdd_zero(f->mgr)));
00894 }

int bdd_is_var_hard_group ( bdd_manager *  mgr,
int  index 
)

Definition at line 2902 of file cmuPort.c.

02903 {
02904     return(0);
02905 }

int bdd_is_var_to_be_grouped ( bdd_manager *  mgr,
int  index 
)

Definition at line 2896 of file cmuPort.c.

02897 {
02898     return(0);
02899 }

int bdd_is_var_to_be_ungrouped ( bdd_manager *  mgr,
int  index 
)

Definition at line 2908 of file cmuPort.c.

02909 {
02910     return(0);
02911 }

bdd_t* bdd_ite ( bdd_t *  i,
bdd_t *  t,
bdd_t *  e,
boolean  i_phase,
boolean  t_phase,
boolean  e_phase 
)

Definition at line 625 of file cmuPort.c.

00632 {
00633   struct bdd_ *temp1, *temp2, *temp3;
00634   bdd_t *result;
00635   struct bdd_manager_ *mgr;
00636   
00637   mgr = i->mgr;
00638   temp1 = ( (i_phase == TRUE) ? cmu_bdd_identity(mgr, i->node) : cmu_bdd_not(mgr, i->node));
00639   temp2 = ( (t_phase == TRUE) ? cmu_bdd_identity(mgr, t->node) : cmu_bdd_not(mgr, t->node));
00640   temp3 = ( (e_phase == TRUE) ? cmu_bdd_identity(mgr, e->node) : cmu_bdd_not(mgr, e->node));
00641   result = bdd_construct_bdd_t(mgr, cmu_bdd_ite(mgr, temp1, temp2, temp3));
00642   cmu_bdd_free(mgr, temp1);
00643   cmu_bdd_free(mgr, temp2);
00644   cmu_bdd_free(mgr, temp3);
00645   return result;
00646 }

int bdd_iter_decomp ( bdd_t *  f,
bdd_partition_type_t  partType,
bdd_t ***  conjArray 
)

Definition at line 1468 of file cmuPort.c.

01472 {
01473   return 0;
01474 }

boolean bdd_leq ( bdd_t *  f,
bdd_t *  g,
boolean  f_phase,
boolean  g_phase 
)

Definition at line 897 of file cmuPort.c.

00902 {
00903     struct bdd_ *temp1, *temp2, *implies_fn;
00904     struct bdd_manager_ *mgr;
00905     boolean result_value;
00906 
00907     mgr = f->mgr;
00908     temp1 = ( (f_phase == TRUE) ? cmu_bdd_identity(mgr, f->node) : cmu_bdd_not(mgr, f->node));
00909     temp2 = ( (g_phase == TRUE) ? cmu_bdd_identity(mgr, g->node) : cmu_bdd_not(mgr, g->node));
00910     implies_fn = cmu_bdd_implies(mgr, temp1, temp2); /* returns a minterm of temp1*!temp2 */
00911     result_value = (implies_fn == cmu_bdd_zero(mgr));
00912     cmu_bdd_free(mgr, temp1);
00913     cmu_bdd_free(mgr, temp2);
00914     cmu_bdd_free(mgr, implies_fn);
00915     return result_value;
00916 }

boolean bdd_leq_array ( bdd_t *  f,
array_t *  g_array,
boolean  f_phase,
boolean  g_phase 
)

Definition at line 941 of file cmuPort.c.

00946 {
00947   int   i;
00948   bdd_t *g;
00949   boolean result;
00950 
00951   arrayForEachItem(bdd_t *, g_array, i, g) {
00952     result = bdd_leq(f, g, f_phase, g_phase);
00953     if (g_phase) {
00954       if (!result)
00955         return(0);
00956     } else {
00957       if (result)
00958         return(1);
00959     }
00960   }
00961   if (g_phase)
00962     return(1);
00963   else
00964     return(0);
00965 }

boolean bdd_lequal_mod_care_set ( bdd_t *  f,
bdd_t *  g,
boolean  f_phase,
boolean  g_phase,
bdd_t *  careSet 
)

Definition at line 919 of file cmuPort.c.

00925 {
00926   bdd_t *temp;
00927   boolean result;
00928 
00929   if (bdd_leq(f, g, f_phase, g_phase))
00930     return 1;
00931 
00932   temp = bdd_and(f, careSet, f_phase, 1);
00933 
00934   result = bdd_leq(temp, g, 1, g_phase);
00935   bdd_free(temp);
00936 
00937   return(result);
00938 }

bdd_node* bdd_make_bdd_from_zdd_cover ( bdd_manager *  mgr,
bdd_node *  node 
)

Definition at line 2612 of file cmuPort.c.

02613 {
02614     return(NIL(bdd_node));
02615 }

bdd_t* bdd_minimize ( bdd_t *  f,
bdd_t *  c 
)

Definition at line 649 of file cmuPort.c.

00650 {
00651   bdd_t *result = bdd_construct_bdd_t(f->mgr, cmu_bdd_reduce(f->mgr,
00652                                                              f->node,
00653                                                              c->node)); 
00654   if (bdd_size(result) < bdd_size(f)){
00655     return result;
00656   }
00657   else{
00658     bdd_free(result);
00659     return bdd_dup(f);
00660   }
00661 }

bdd_t* bdd_minimize_array ( bdd_t *  f,
array_t *  bddArray 
)

Definition at line 664 of file cmuPort.c.

00665 {
00666   bdd_t *operand;
00667   struct bdd_ *result, *temp;
00668   bdd_t *final;
00669   int i;
00670 
00671   result = cmu_bdd_identity(f->mgr, f->node);
00672   for (i = 0; i < array_n(bddArray); i++) {
00673     operand = array_fetch(bdd_t *, bddArray, i);
00674     temp = cmu_bdd_reduce(f->mgr, result, operand->node);
00675     if (temp == NULL) {
00676       cmu_bdd_free(f->mgr, result);
00677       return(NULL);
00678     }
00679     cmu_bdd_free(f->mgr, result);
00680     result = temp;
00681   }
00682 
00683   final = bdd_construct_bdd_t(f->mgr, result);
00684 
00685   if (bdd_size(final) < bdd_size(f)){
00686     return final;
00687   }
00688   else{
00689     bdd_free(final);
00690     return bdd_dup(f);
00691   }
00692 }

bdd_t* bdd_multiway_and ( bdd_manager *  manager,
array_t *  bddArray 
)

Definition at line 313 of file cmuPort.c.

00314 {
00315   int i;
00316   bdd temp, result;
00317   bdd_t *operand;
00318   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00319   result = cmu_bdd_one(mgr);
00320   for (i=0; i<array_n(bddArray); i++){
00321     operand = array_fetch(bdd_t *, bddArray, i);
00322     temp = cmu_bdd_and(mgr, result, operand->node);
00323     cmu_bdd_free(mgr, result);
00324     result = temp;
00325   }
00326   return bdd_construct_bdd_t(mgr, result);
00327 }

bdd_t* bdd_multiway_or ( bdd_manager *  manager,
array_t *  bddArray 
)

Definition at line 330 of file cmuPort.c.

00331 {
00332   int i;
00333   bdd temp, result;
00334   bdd_t *operand;
00335   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00336   result = cmu_bdd_zero(mgr);
00337   for (i=0; i<array_n(bddArray); i++){
00338     operand = array_fetch(bdd_t *, bddArray, i);
00339     temp = cmu_bdd_or(mgr, result, operand->node);
00340     cmu_bdd_free(mgr, result);
00341     result = temp;
00342   }
00343   return bdd_construct_bdd_t(mgr, result);
00344 }

bdd_t* bdd_multiway_xor ( bdd_manager *  manager,
array_t *  bddArray 
)

Definition at line 347 of file cmuPort.c.

00348 {
00349   int i;
00350   bdd temp, result;
00351   bdd_t *operand;
00352   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00353   result = cmu_bdd_zero(mgr);
00354   for (i=0; i<array_n(bddArray); i++){
00355     operand = array_fetch(bdd_t *, bddArray, i);
00356     temp = cmu_bdd_xor(mgr, result, operand->node);
00357     cmu_bdd_free(mgr, result);
00358     result = temp;
00359   }
00360   return bdd_construct_bdd_t(mgr, result);
00361 }

bdd_block* bdd_new_var_block ( bdd_t *  f,
long  length 
)

Function********************************************************************

Synopsis []

Description [optional]

SideEffects [required]

SeeAlso [optional]

Definition at line 1285 of file cmuPort.c.

01286 {
01287   struct bdd_manager_ *manager;
01288   if (f == NIL(bdd_t)) {
01289         fail("bdd_new_var_block: invalid BDD");
01290   }
01291   manager = f->mgr;
01292   return (bdd_block *)cmu_bdd_new_var_block(manager, f->node, length);
01293 }

int bdd_node_read_index ( bdd_node *  f  ) 

Definition at line 2325 of file cmuPort.c.

02326 {
02327     return -1;
02328 }

int bdd_node_size ( bdd_node *  f  ) 

Definition at line 1151 of file cmuPort.c.

01152 {
01153   return(0);
01154 }

bdd_t* bdd_not ( bdd_t *  f  ) 

Definition at line 696 of file cmuPort.c.

00697 {
00698   return bdd_construct_bdd_t(f->mgr, cmu_bdd_not(f->mgr, f->node));
00699 }

bdd_node* bdd_not_bdd_node ( bdd_node *  f  ) 

Definition at line 2259 of file cmuPort.c.

02260 {
02261     return NIL(bdd_node);
02262 }

unsigned int bdd_num_vars ( bdd_manager *  manager  ) 

Definition at line 1108 of file cmuPort.c.

01109 {
01110   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01111   return (cmu_bdd_vars(mgr));
01112 }

int bdd_num_zdd_vars ( bdd_manager *  mgr  ) 

Definition at line 2223 of file cmuPort.c.

02224 {
02225     return -1;
02226 }

bdd_t* bdd_one ( bdd_manager *  manager  ) 

Definition at line 702 of file cmuPort.c.

00703 {
00704   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00705   return bdd_construct_bdd_t(mgr, cmu_bdd_one(mgr));
00706 }

bdd_t* bdd_or ( bdd_t *  f,
bdd_t *  g,
boolean  f_phase,
boolean  g_phase 
)

Definition at line 709 of file cmuPort.c.

00714 {
00715   struct bdd_ *temp1, *temp2;
00716   bdd_t *result;
00717   struct bdd_manager_ *mgr;
00718   
00719   mgr = f->mgr;
00720   temp1 = ( (f_phase == TRUE) ? cmu_bdd_identity(mgr, f->node) : cmu_bdd_not(mgr, f->node));
00721   temp2 = ( (g_phase == TRUE) ? cmu_bdd_identity(mgr, g->node) : cmu_bdd_not(mgr, g->node));
00722   result = bdd_construct_bdd_t(mgr, cmu_bdd_or(mgr, temp1, temp2));
00723   cmu_bdd_free(mgr, temp1);
00724   cmu_bdd_free(mgr, temp2);
00725   return result;
00726 }

array_t* bdd_pairwise_and ( bdd_manager *  manager,
array_t *  bddArray1,
array_t *  bddArray2 
)

Definition at line 388 of file cmuPort.c.

00390 {
00391   int i;
00392   bdd_t *operand1, *operand2;
00393   array_t *resultArray;
00394   bdd result;
00395   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00396   if (array_n(bddArray1) != array_n(bddArray2)){
00397     fprintf(stderr, "bdd_pairwise_and: Arrays of different lengths.\n");
00398     return NIL(array_t);
00399   }
00400   resultArray = array_alloc(bdd_t *, 0);
00401   for (i=0; i<array_n(bddArray1); i++){
00402     operand1 = array_fetch(bdd_t *, bddArray1, i);
00403     operand2 = array_fetch(bdd_t *, bddArray2, i);
00404     result = cmu_bdd_and(mgr, operand1->node, operand2->node);
00405     array_insert_last(bdd_t*, resultArray,
00406                       bdd_construct_bdd_t(mgr, result)); 
00407   }
00408   return resultArray;
00409 }

array_t* bdd_pairwise_or ( bdd_manager *  manager,
array_t *  bddArray1,
array_t *  bddArray2 
)

Definition at line 364 of file cmuPort.c.

00366 {
00367   int i;
00368   bdd_t *operand1, *operand2;
00369   array_t *resultArray;
00370   bdd result;
00371   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00372   if (array_n(bddArray1) != array_n(bddArray2)){
00373     fprintf(stderr, "bdd_pairwise_or: Arrays of different lengths.\n");
00374     return NIL(array_t);
00375   }
00376   resultArray = array_alloc(bdd_t *, 0);
00377   for (i=0; i<array_n(bddArray1); i++){
00378     operand1 = array_fetch(bdd_t *, bddArray1, i);
00379     operand2 = array_fetch(bdd_t *, bddArray2, i);
00380     result = cmu_bdd_or(mgr, operand1->node, operand2->node);
00381     array_insert_last(bdd_t*, resultArray,
00382                       bdd_construct_bdd_t(mgr, result)); 
00383   }
00384   return resultArray;
00385 }

array_t* bdd_pairwise_xor ( bdd_manager *  manager,
array_t *  bddArray1,
array_t *  bddArray2 
)

Definition at line 412 of file cmuPort.c.

00414 {
00415   int i;
00416   bdd_t *operand1, *operand2;
00417   array_t *resultArray;
00418   bdd result;
00419   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00420   if (array_n(bddArray1) != array_n(bddArray2)){
00421     fprintf(stderr, "bdd_pairwise_xor: Arrays of different lengths.\n");
00422     return NIL(array_t);
00423   }
00424   resultArray = array_alloc(bdd_t *, 0);
00425   for (i=0; i<array_n(bddArray1); i++){
00426     operand1 = array_fetch(bdd_t *, bddArray1, i);
00427     operand2 = array_fetch(bdd_t *, bddArray2, i);
00428     result = cmu_bdd_xor(mgr, operand1->node, operand2->node);
00429     array_insert_last(bdd_t*, resultArray,
00430                       bdd_construct_bdd_t(mgr, result)); 
00431   }
00432   return resultArray;
00433 }

bdd_t* bdd_pick_one_minterm ( bdd_t *  f,
array_t *  varsArray 
)

Definition at line 1984 of file cmuPort.c.

01987 {
01988     return NIL(bdd_t);
01989 }

void* bdd_pointer ( bdd_t *  f  ) 

Definition at line 815 of file cmuPort.c.

00816 {
00817     return((void *)f->node);
00818 }

void bdd_print ( bdd_t *  f  ) 

Definition at line 1115 of file cmuPort.c.

01116 {
01117     cmu_bdd_print_bdd(f->mgr, f->node, bdd_naming_fn_none, bdd_terminal_id_fn_none, (pointer) 0, stdout);
01118 }

int bdd_print_apa_minterm ( FILE *  fp,
bdd_t *  f,
int  nvars,
int  precision 
)

Definition at line 1522 of file cmuPort.c.

01527 {
01528   return 0;
01529 }

int bdd_print_cover ( bdd_t *  f  ) 

Definition at line 2379 of file cmuPort.c.

02380 {
02381   return 0;
02382 }

int bdd_print_minterm ( bdd_t *  f  ) 

Definition at line 2373 of file cmuPort.c.

02374 {
02375   return 0;
02376 }

void bdd_print_stats ( bdd_manager *  manager,
FILE *  file 
)

Definition at line 1121 of file cmuPort.c.

01122 {
01123   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01124   cmu_bdd_stats(mgr, file);
01125 }

bdd_node* bdd_priority_select ( bdd_manager *  mgr,
bdd_node *  R,
bdd_node **  x,
bdd_node **  y,
bdd_node **  z,
bdd_node *  Pi,
int  n,
bdd_node *(*)(bdd_manager *, int, bdd_node **, bdd_node **, bdd_node **)  Pifunc 
)

Definition at line 2403 of file cmuPort.c.

02412 {
02413     return NIL(bdd_node);
02414 
02415 } /* end of bdd_priority_select */

int bdd_ptrcmp ( bdd_t *  f,
bdd_t *  g 
)

Function********************************************************************

Synopsis [Compares two bdds are same.]

SideEffects []

Definition at line 2693 of file cmuPort.c.

02694 {
02695   if (f->node == g->node)
02696     return(0);
02697   else
02698     return(1);
02699 }

int bdd_ptrhash ( bdd_t *  f,
int  size 
)

Function********************************************************************

Synopsis [Returns the hash value of a bdd.]

SideEffects []

Definition at line 2710 of file cmuPort.c.

02711 {
02712   int hash;
02713 
02714   hash = (int)((unsigned long)f->node >> 2) % size;
02715   return(hash);
02716 }

bdd_node* bdd_read_background ( bdd_manager *  mgr  ) 

Definition at line 2429 of file cmuPort.c.

02430 {
02431   return NIL(bdd_node);
02432 
02433 } /* end of bdd_read_background */

BDD_VALUE_TYPE bdd_read_epsilon ( bdd_manager *  mgr  ) 

Definition at line 1960 of file cmuPort.c.

01961 {
01962     return 0;
01963 }

bdd_node* bdd_read_logic_zero ( bdd_manager *  mgr  ) 

Definition at line 1752 of file cmuPort.c.

01753 {
01754     return NIL(bdd_node);
01755 }

bdd_node* bdd_read_next ( bdd_node *  f  ) 

Definition at line 2331 of file cmuPort.c.

02332 {
02333     return NIL(bdd_node);
02334 }

int bdd_read_next_reordering ( bdd_manager *  mgr  ) 

Definition at line 2048 of file cmuPort.c.

02049 {
02050     return 0;
02051 }

int bdd_read_node_count ( bdd_manager *  mgr  ) 

Definition at line 1543 of file cmuPort.c.

01544 {
01545   return 0;
01546 }

bdd_node* bdd_read_one ( bdd_manager *  mgr  ) 

Definition at line 1966 of file cmuPort.c.

01967 {
01968     return NIL(bdd_node);
01969 }

int bdd_read_pair_index ( bdd_manager *  mgr,
int  index 
)

Definition at line 2872 of file cmuPort.c.

02873 {
02874     return(0);
02875 }

int bdd_read_peak_live_node ( bdd_manager *  mgr  ) 

Definition at line 2824 of file cmuPort.c.

02825 {
02826   return(0);
02827 }

long bdd_read_peak_memory ( bdd_manager *  mgr  ) 

Definition at line 2818 of file cmuPort.c.

02819 {
02820   return(0);
02821 }

bdd_node* bdd_read_plus_infinity ( bdd_manager *  mgr  ) 

Definition at line 2395 of file cmuPort.c.

02396 {
02397     return NIL(bdd_node);
02398 
02399 } /* end of bdd_read_plus_infinity */

int bdd_read_reordered_field ( bdd_manager *  mgr  ) 

Definition at line 2345 of file cmuPort.c.

02346 {
02347     return -1;
02348 }

int bdd_read_reorderings ( bdd_manager *  mgr  ) 

Definition at line 2042 of file cmuPort.c.

02043 {
02044     return 0;
02045 }

int bdd_read_zdd_level ( bdd_manager *  mgr,
int  index 
)

Definition at line 2277 of file cmuPort.c.

02278 {
02279     return -1;
02280 }

bdd_node* bdd_read_zero ( bdd_manager *  mgr  ) 

Definition at line 2003 of file cmuPort.c.

02004 {
02005     return NIL(bdd_node);
02006 }

void bdd_realign_disable ( bdd_manager *  mgr  ) 

Definition at line 2313 of file cmuPort.c.

02314 {
02315     return;
02316 }

void bdd_realign_enable ( bdd_manager *  mgr  ) 

Definition at line 2307 of file cmuPort.c.

02308 {
02309     return;
02310 }

int bdd_realignment_enabled ( bdd_manager *  mgr  ) 

Definition at line 2319 of file cmuPort.c.

02320 {
02321     return 0;
02322 }

void bdd_recursive_deref ( bdd_manager *  mgr,
bdd_node *  f 
)

Definition at line 1592 of file cmuPort.c.

01593 {
01594   return;
01595 }

void bdd_recursive_deref_zdd ( bdd_manager *  mgr,
bdd_node *  f 
)

Definition at line 2265 of file cmuPort.c.

02266 {
02267     return;
02268 }

void bdd_ref ( bdd_node *  fn  ) 

Definition at line 1585 of file cmuPort.c.

01586 {
01587   return ;
01588 }

bdd_node* bdd_regular ( bdd_node *  f  ) 

Definition at line 2229 of file cmuPort.c.

02230 {
02231     return NIL(bdd_node);
02232 }

int bdd_remove_hook ( bdd_manager *  mgr,
int(*)(bdd_manager *, char *, void *)  procedure,
bdd_hook_type_t  whichHook 
)

Definition at line 1495 of file cmuPort.c.

01499 {
01500   return 0;
01501 }

void bdd_reorder ( bdd_manager *  manager  ) 

Definition at line 1238 of file cmuPort.c.

01239 {
01240   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01241   cmu_bdd_reorder(mgr);
01242 }

bdd_reorder_verbosity_t bdd_reordering_reporting ( bdd_manager *  mgr  ) 

Definition at line 1516 of file cmuPort.c.

01517 {
01518   return BDD_REORDER_VERBOSITY_DEFAULT;
01519 }

int bdd_reordering_status ( bdd_manager *  mgr,
bdd_reorder_type_t *  method 
)

Function********************************************************************

Synopsis [Dummy functions defined in bdd.h]

SideEffects []

Definition at line 1330 of file cmuPort.c.

01333 {
01334   return 0;
01335 }

int bdd_reordering_zdd_status ( bdd_manager *  mgr,
bdd_reorder_type_t *  method 
)

Definition at line 1550 of file cmuPort.c.

01553 {
01554   return 0;
01555 }

int bdd_reset_var_to_be_grouped ( bdd_manager *  mgr,
int  index 
)

Definition at line 2890 of file cmuPort.c.

02891 {
02892     return(0);
02893 }

void bdd_set_background ( bdd_manager *  mgr,
bdd_node *  f 
)

Definition at line 2419 of file cmuPort.c.

02422 {
02423     return;
02424  
02425 } /* end of bdd_set_background */

void bdd_set_gc_mode ( bdd_manager *  manager,
boolean  no_gc 
)

Definition at line 1203 of file cmuPort.c.

01204 {
01205   cmu_bdd_warning("bdd_set_gc_mode: translated to no-op in CMU package");
01206 }

void bdd_set_next ( bdd_node *  f,
bdd_node *  g 
)

Definition at line 2338 of file cmuPort.c.

02339 {
02340     return;
02341 }

void bdd_set_next_reordering ( bdd_manager *  mgr,
int  next 
)

Definition at line 2054 of file cmuPort.c.

02055 {
02056 }

int bdd_set_ns_var ( bdd_manager *  mgr,
int  index 
)

Definition at line 2842 of file cmuPort.c.

02843 {
02844     return(0);
02845 }

int bdd_set_pair_index ( bdd_manager *  mgr,
int  index,
int  pairIndex 
)

Definition at line 2866 of file cmuPort.c.

02867 {
02868     return(0);
02869 }

int bdd_set_parameters ( bdd_manager *  mgr,
avl_tree *  valueTable,
FILE *  file 
)

Function********************************************************************

Synopsis [Sets the internal parameters of the package to the given values.]

SideEffects []

Definition at line 1135 of file cmuPort.c.

01139 {
01140   (void) fprintf(file, "Functionality not supported yet in the CMU package\n");
01141   return 1;
01142 } /* End of bdd_set_parameters */

int bdd_set_pi_var ( bdd_manager *  mgr,
int  index 
)

Definition at line 2830 of file cmuPort.c.

02831 {
02832     return(0);
02833 }

int bdd_set_ps_var ( bdd_manager *  mgr,
int  index 
)

Definition at line 2836 of file cmuPort.c.

02837 {
02838     return(0);
02839 }

void bdd_set_reordered_field ( bdd_manager *  mgr,
int  n 
)

Definition at line 2351 of file cmuPort.c.

02352 {
02353     return;
02354 }

int bdd_set_var_hard_group ( bdd_manager *  mgr,
int  index 
)

Definition at line 2884 of file cmuPort.c.

02885 {
02886     return(0);
02887 }

int bdd_set_var_to_be_grouped ( bdd_manager *  mgr,
int  index 
)

Definition at line 2878 of file cmuPort.c.

02879 {
02880     return(0);
02881 }

int bdd_set_var_to_be_ungrouped ( bdd_manager *  mgr,
int  index 
)

Definition at line 2914 of file cmuPort.c.

02915 {
02916     return(0);
02917 }

int bdd_shuffle_heap ( bdd_manager *  mgr,
int *  permut 
)

Definition at line 1692 of file cmuPort.c.

01695 {
01696   return 0;
01697 }

int bdd_size ( bdd_t *  f  ) 

Definition at line 1145 of file cmuPort.c.

01146 {
01147     return ((int) cmu_bdd_size(f->mgr, f->node, 1));
01148 }

long bdd_size_multiple ( array_t *  bdd_array  ) 

Definition at line 1157 of file cmuPort.c.

01158 {
01159     long result;
01160     struct bdd_ **vector_bdd;
01161     bdd_t *f;
01162     int i;
01163     struct bdd_manager_ *mgr;
01164 
01165     if ((bdd_array == NIL(array_t)) || (array_n(bdd_array) == 0))
01166         return 0;
01167 
01168     f = array_fetch(bdd_t*, bdd_array, 0);
01169     mgr = f->mgr;
01170 
01171     vector_bdd = (struct bdd_ **)
01172                         malloc((array_n(bdd_array)+1)*sizeof(struct bdd_ *));
01173 
01174     for(i=0; i<array_n(bdd_array);i++){
01175         f = array_fetch(bdd_t*, bdd_array, i);
01176         vector_bdd[i] = f->node;
01177     }
01178     vector_bdd[array_n(bdd_array)] = 0;
01179     result =  cmu_bdd_size_multiple(mgr, vector_bdd,1);
01180     FREE(vector_bdd);
01181     return result;
01182 }

bdd_t* bdd_smooth ( bdd_t *  f,
array_t *  smoothing_vars 
)

Definition at line 729 of file cmuPort.c.

00732 {
00733   int num_vars, i;
00734   bdd_t *fn, *result;
00735   struct bdd_ **assoc;
00736   struct bdd_manager_ *mgr;
00737   
00738   num_vars = array_n(smoothing_vars);
00739   if (num_vars <= 0) {
00740         cmu_bdd_fatal("bdd_smooth: no smoothing variables");
00741   }
00742   
00743   assoc = ALLOC(struct bdd_ *, num_vars+1);
00744   
00745   for (i = 0; i < num_vars; i++) {
00746         fn = array_fetch(bdd_t *, smoothing_vars, i);
00747         assoc[i] = fn->node;
00748   }
00749   assoc[num_vars] = (struct bdd_ *) 0;
00750   
00751   mgr = f->mgr;
00752   cmu_bdd_temp_assoc(mgr, assoc, 0);
00753   (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current association */
00754   
00755   result = bdd_construct_bdd_t(mgr, cmu_bdd_exists(mgr, f->node));
00756   FREE(assoc);
00757   return result;
00758 }

bdd_t* bdd_smooth_with_cube ( bdd_t *  f,
bdd_t *  cube 
)

Definition at line 2737 of file cmuPort.c.

02738 {
02739   int i;
02740   bdd_t *var, *res;
02741   array_t *smoothingVars;
02742   var_set_t *supportVarSet;
02743 
02744   smoothingVars = array_alloc(bdd_t *, 0);
02745   supportVarSet = bdd_get_support(f);
02746   for (i = 0; i < supportVarSet->n_elts; i++) {
02747     if (var_set_get_elt(supportVarSet, i) == 1) {
02748       var = bdd_var_with_index(f->mgr, i);
02749       array_insert_last(bdd_t *, smoothingVars, var);
02750     }
02751   }
02752   var_set_free(supportVarSet);
02753 
02754   res = bdd_smooth(f, smoothingVars);
02755 
02756   for (i = 0; i < array_n(smoothingVars); i++) {
02757     var = array_fetch(bdd_t *, smoothingVars, i);
02758     bdd_free(var);
02759   }
02760   array_free(smoothingVars);
02761   return res;
02762 }

bdd_t* bdd_solve_eqn ( bdd_t *  f,
array_t *  g,
array_t *  unknowns 
)

Definition at line 1477 of file cmuPort.c.

01481 {
01482   return NIL(bdd_t);
01483 }

bdd_node* bdd_split_set ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node **  x,
int  n,
double  m 
)

Definition at line 2546 of file cmuPort.c.

02552 {
02553   return NIL(bdd_node);
02554 
02555 } /* end of bdd_split_set */

bdd_t* bdd_squeeze ( bdd_t *  f,
bdd_t *  g 
)

Definition at line 1311 of file cmuPort.c.

01312 {
01313     return (NULL);
01314 }

bdd_manager* bdd_start ( int  nvariables  ) 

Definition at line 140 of file cmuPort.c.

00141 {
00142     struct bdd_manager_ *mgr;
00143     int i;
00144     bdd_external_hooks *hooks;
00145    
00146     mgr = cmu_bdd_init();    /*no args*/
00147 
00148     /*
00149      * Calls to UCB bdd_get_variable are translated into cmu_bdd_var_with_id calls.  However,
00150      * cmu_bdd_var_with_id assumes that single variable BDDs have already been created for 
00151      * all the variables that we wish to access.  Thus, following, we explicitly create n
00152      * variables.  We do not care about the return value of cmu_bdd_new_var_last; in the 
00153      * CMU package, the single variable BDDs are NEVER garbage collected.
00154      */
00155     for (i = 0; i < nvariables; i++) {
00156         (void) cmu_bdd_new_var_last(mgr);
00157     }
00158 
00159     hooks = ALLOC(bdd_external_hooks, 1);
00160     hooks->mdd = hooks->network = hooks->undef1 = (char *) 0;
00161     mgr->hooks = (char *) hooks;  /* new field added to CMU manager */
00162 
00163     return (bdd_manager *) mgr;
00164 }

bdd_t* bdd_subset_with_mask_vars ( bdd_t *  f,
array_t *  varsArray,
array_t *  maskVarsArray 
)

Definition at line 2719 of file cmuPort.c.

02723 {
02724   return NIL(bdd_t);
02725 }

bdd_t* bdd_substitute ( bdd_t *  f,
array_t *  old_array,
array_t *  new_array 
)

Definition at line 761 of file cmuPort.c.

00765 {
00766     int num_old_vars, num_new_vars, i;
00767     bdd_t *fn_old, *fn_new, *result;
00768     struct bdd_ **assoc;
00769     struct bdd_manager_ *mgr;
00770 
00771     num_old_vars = array_n(old_array);
00772     num_new_vars = array_n(new_array);
00773     if (num_old_vars != num_new_vars) {
00774         cmu_bdd_fatal("bdd_substitute: mismatch of number of new and old variables");
00775     }
00776 
00777     assoc = ALLOC(struct bdd_ *, 2*(num_old_vars+1));
00778 
00779     for (i = 0; i < num_old_vars; i++) {
00780         fn_old = array_fetch(bdd_t *, old_array, i);
00781         fn_new = array_fetch(bdd_t *, new_array, i);
00782         assoc[2*i]   = fn_old->node;
00783         assoc[2*i+1] = fn_new->node;
00784     }
00785     assoc[2*num_old_vars]   = (struct bdd_ *) 0;
00786     assoc[2*num_old_vars+1] = (struct bdd_ *) 0;  /* not sure if we need this second 0 */
00787 
00788     mgr = f->mgr;
00789     cmu_bdd_temp_assoc(mgr, assoc, 1);
00790     (void) cmu_bdd_assoc(mgr, -1);  /* set the temp association as the current association */
00791 
00792     result = bdd_construct_bdd_t(mgr, cmu_bdd_substitute(mgr, f->node));
00793     FREE(assoc);
00794     return result;
00795 }

array_t* bdd_substitute_array ( array_t *  f_array,
array_t *  old_array,
array_t *  new_array 
)

Definition at line 798 of file cmuPort.c.

00802 {
00803   int   i;
00804   bdd_t *f, *new_;
00805   array_t *substitute_array = array_alloc(bdd_t *, 0);
00806 
00807   arrayForEachItem(bdd_t *, f_array, i, f) {
00808     new_ = bdd_substitute(f, old_array, new_array);
00809     array_insert_last(bdd_t *, substitute_array, new_);
00810   }
00811   return(substitute_array);
00812 }

array_t* bdd_substitute_array_with_permut ( array_t *  f_array,
int *  permut 
)

Definition at line 2771 of file cmuPort.c.

02774 {
02775   return NIL(array_t);
02776 }

bdd_t* bdd_substitute_with_permut ( bdd_t *  f,
int *  permut 
)

Definition at line 2765 of file cmuPort.c.

02766 {
02767   return NIL(bdd_t);
02768 }

bdd_t* bdd_then ( bdd_t *  f  ) 

Definition at line 821 of file cmuPort.c.

00822 {
00823     return bdd_construct_bdd_t(f->mgr, cmu_bdd_then(f->mgr, f->node));
00824 }

bdd_t* bdd_top_var ( bdd_t *  f  ) 

Definition at line 827 of file cmuPort.c.

00828 {
00829     return bdd_construct_bdd_t(f->mgr, cmu_bdd_if(f->mgr, f->node));
00830 }

bdd_variableId bdd_top_var_id ( bdd_t *  f  ) 

Definition at line 1185 of file cmuPort.c.

01186 {
01187     return ((bdd_variableId) (cmu_bdd_if_id(f->mgr, f->node) - 1));
01188 }

long bdd_top_var_level ( bdd_manager *  manager,
bdd_t *  fn 
)

Definition at line 1262 of file cmuPort.c.

01263 {
01264   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
01265   return cmu_bdd_if_index(mgr, fn->node);
01266 }

int bdd_unbind_var ( bdd_manager *  mgr,
int  index 
)

Definition at line 2926 of file cmuPort.c.

02927 {
02928     return(0);
02929 }

bdd_node* bdd_unique_inter ( bdd_manager *  mgr,
int  v,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2184 of file cmuPort.c.

02189 {
02190      return NIL(bdd_node);
02191 }

bdd_node* bdd_unique_inter_ivo ( bdd_manager *  mgr,
int  v,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2194 of file cmuPort.c.

02199 {
02200      return NIL(bdd_node);
02201 }

int bdd_var_decomp ( bdd_t *  f,
bdd_partition_type_t  partType,
bdd_t ***  conjArray 
)

Definition at line 1450 of file cmuPort.c.

01454 {
01455   return 0;
01456 }

int bdd_var_is_dependent ( bdd_t *  f,
bdd_t *  var 
)

Definition at line 2794 of file cmuPort.c.

02795 {
02796   return(0);
02797 }

bdd_t* bdd_var_with_index ( bdd_manager *  manager,
int  index 
)

Definition at line 1296 of file cmuPort.c.

01297 {
01298   return bdd_construct_bdd_t(manager, 
01299                             cmu_bdd_var_with_index((cmu_bdd_manager) manager,
01300                                                    index));
01301 }

bdd_t* bdd_vector_compose ( bdd_t *  f,
array_t *  varArray,
array_t *  funcArray 
)

Definition at line 2779 of file cmuPort.c.

02783 {
02784   return NIL(bdd_t);
02785 }

bdd_node* bdd_xeqy ( bdd_manager *  mgr,
int  N,
bdd_node **  x,
bdd_node **  y 
)

Definition at line 2505 of file cmuPort.c.

02510 {
02511   return NIL(bdd_node);
02512 
02513 } /* end of bdd_xeqy */

bdd_node* bdd_xgty ( bdd_manager *  mgr,
int  N,
bdd_node **  x,
bdd_node **  y 
)

Definition at line 2526 of file cmuPort.c.

02531 {
02532   return NIL(bdd_node);
02533 
02534 } /* end of bdd_xgty */

bdd_t* bdd_xnor ( bdd_t *  f,
bdd_t *  g 
)

Definition at line 833 of file cmuPort.c.

00834 {
00835     return bdd_construct_bdd_t(f->mgr, cmu_bdd_xnor(f->mgr, f->node, g->node));
00836 }

bdd_t* bdd_xor ( bdd_t *  f,
bdd_t *  g 
)

Definition at line 839 of file cmuPort.c.

00840 {
00841     return bdd_construct_bdd_t(f->mgr, cmu_bdd_xor(f->mgr, f->node, g->node));
00842 }

bdd_t* bdd_xor_smooth ( bdd_t *  f,
bdd_t *  g,
array_t *  smoothing_vars 
)

Definition at line 2385 of file cmuPort.c.

02389 {
02390     return NIL(bdd_t);
02391 }

bdd_node* bdd_zdd_complement ( bdd_manager *  mgr,
bdd_node *  node 
)

Definition at line 2618 of file cmuPort.c.

02619 {
02620     return(NIL(bdd_node));
02621 }

int bdd_zdd_count ( bdd_manager *  mgr,
bdd_node *  f 
)

Definition at line 2271 of file cmuPort.c.

02272 {
02273     return 0;
02274 }

bdd_node* bdd_zdd_diff ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2205 of file cmuPort.c.

02209 {
02210     return NIL(bdd_node);
02211 }

bdd_node* bdd_zdd_diff_recur ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2214 of file cmuPort.c.

02218 {
02219     return NIL(bdd_node);
02220 }

int bdd_zdd_get_cofactors3 ( bdd_manager *  mgr,
bdd_node *  f,
int  v,
bdd_node **  f1,
bdd_node **  f0,
bdd_node **  fd 
)

Definition at line 2163 of file cmuPort.c.

02170 {
02171     return 0;
02172 }

bdd_node* bdd_zdd_get_node ( bdd_manager *  mgr,
int  id,
bdd_node *  g,
bdd_node *  h 
)

Definition at line 2085 of file cmuPort.c.

02090 {
02091     return NIL(bdd_node);
02092 }

bdd_node* bdd_zdd_isop ( bdd_manager *  mgr,
bdd_node *  L,
bdd_node *  U,
bdd_node **  zdd_I 
)

Definition at line 2153 of file cmuPort.c.

02158 {
02159     return NIL(bdd_node);
02160 }

bdd_node* bdd_zdd_isop_recur ( bdd_manager *  mgr,
bdd_node *  L,
bdd_node *  U,
bdd_node **  zdd_I 
)

Definition at line 2142 of file cmuPort.c.

02147 {
02148     return NIL(bdd_node);
02149 }

bdd_node* bdd_zdd_product ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2095 of file cmuPort.c.

02099 {
02100     return NIL(bdd_node);
02101 }

bdd_node* bdd_zdd_product_recur ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2104 of file cmuPort.c.

02108 {
02109     return NIL(bdd_node);
02110 }

void bdd_zdd_realign_disable ( bdd_manager *  mgr  ) 

Definition at line 2295 of file cmuPort.c.

02296 {
02297     return;
02298 }

void bdd_zdd_realign_enable ( bdd_manager *  mgr  ) 

Definition at line 2289 of file cmuPort.c.

02290 {
02291     return;
02292 }

int bdd_zdd_realignment_enabled ( bdd_manager *  mgr  ) 

Definition at line 2301 of file cmuPort.c.

02302 {
02303     return 0;
02304 }

bdd_node* bdd_zdd_union ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2114 of file cmuPort.c.

02118 {
02119   return NIL(bdd_node);
02120 }

int bdd_zdd_vars_from_bdd_vars ( bdd_manager *  mgr,
int  multiplicity 
)

Definition at line 2283 of file cmuPort.c.

02284 {
02285    return 0;
02286 }

bdd_node* bdd_zdd_weak_div ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2124 of file cmuPort.c.

02128 {
02129     return NIL(bdd_node);
02130 }

bdd_node* bdd_zdd_weak_div_recur ( bdd_manager *  mgr,
bdd_node *  f,
bdd_node *  g 
)

Definition at line 2133 of file cmuPort.c.

02137 {
02138     return NIL(bdd_node);
02139 }

bdd_t* bdd_zero ( bdd_manager *  manager  ) 

Definition at line 845 of file cmuPort.c.

00846 {
00847   cmu_bdd_manager mgr = (cmu_bdd_manager) manager;
00848   return bdd_construct_bdd_t(mgr, cmu_bdd_zero(mgr));
00849 }

Generated on Tue Jan 12 13:57:16 2010 for glu-2.2 by  doxygen 1.6.1