src/mdd/mdd.h File Reference

#include "util.h"
#include "array.h"
#include "st.h"
#include "var_set.h"
#include "bdd.h"

Include dependency graph for mdd.h:

This graph shows which files directly or indirectly include this file:

Data Structures
struct	mvar_type
struct	bvar_type
struct	mdd_hook_type
struct	mdd_gen
Defines
#define	str_len 10
#define	MONITOR 0
#define	MDD_VERBOSE 0
#define	SOLUTION 0
#define	BDD_SIZE 1
#define	USE_ITE 1
#define	BYPASS 1
#define	INTERLEAVE 0
#define	mdd_and bdd_and
#define	mdd_and_with_limit bdd_and_with_limit
#define	mdd_and_array bdd_and_array
#define	mdd_cofactor_minterm bdd_cofactor
#define	mdd_constant bdd_constant
#define	mdd_dup bdd_dup
#define	mdd_equal bdd_equal
#define	mdd_equal_mod_care_set bdd_equal_mod_care_set
#define	mdd_closest_cube bdd_closest_cube
#define	mdd_free bdd_free
#define	mdd_get_manager bdd_get_manager
#define	mdd_is_tautology bdd_is_tautology
#define	mdd_ite bdd_ite
#define	mdd_lequal bdd_leq
#define	mdd_lequal_mod_care_set bdd_lequal_mod_care_set
#define	mdd_lequal_array bdd_leq_array
#define	mdd_multiway_and bdd_multiway_and
#define	mdd_multiway_or bdd_multiway_or
#define	mdd_multiway_xor bdd_multiway_xor
#define	mdd_not bdd_not
#define	mdd_one bdd_one
#define	mdd_or bdd_or
#define	mdd_size bdd_size
#define	mdd_size_multiple bdd_size_multiple
#define	mdd_top_var_id bdd_top_var_id
#define	mdd_xor bdd_xor
#define	mdd_xnor bdd_xnor
#define	mdd_zero bdd_zero
#define	mdd_EMPTY bdd_EMPTY
#define	mdd_first_solution mdd_first_cube
#define	mdd_next_solution mdd_next_cube
#define	mdd_eq_c(m, a, b) mdd_func1c(m,a,b,eq2)
#define	mdd_geq_c(m, a, b) mdd_func1c(m,a,b,geq2)
#define	mdd_gt_c(m, a, b) mdd_func1c(m,a,b,gt2)
#define	mdd_leq_c(m, a, b) mdd_func1c(m,a,b,leq2)
#define	mdd_lt_c(m, a, b) mdd_func1c(m,a,b,lt2)
#define	mdd_neq_c(m, a, b) mdd_func1c(m,a,b,neq2)
#define	mdd_eq(m, a, b) mdd_func2(m,a,b,eq2)
#define	mdd_geq(m, a, b) mdd_func2(m,a,b,geq2)
#define	mdd_gt(m, a, b) mdd_func2(m,a,b,gt2)
#define	mdd_leq(m, a, b) mdd_func2(m,a,b,leq2)
#define	mdd_lt(m, a, b) mdd_func2(m,a,b,lt2)
#define	mdd_neq(m, a, b) mdd_func2(m,a,b,neq2)
#define	mdd_unary_minus(m, a, b) mdd_func2(m,a,b,unary_minus2)
#define	mdd_eq_plus(m, a, b, c) mdd_func3(m,a,b,c,eq_plus3)
#define	mdd_geq_plus(m, a, b, c) mdd_func3(m,a,b,c,geq_plus3)
#define	mdd_gt_plus(m, a, b, c) mdd_func3(m,a,b,c,gt_plus3)
#define	mdd_leq_plus(m, a, b, c) mdd_func3(m,a,b,c,leq_plus3)
#define	mdd_lt_plus(m, a, b, c) mdd_func3(m,a,b,c,lt_plus3)
#define	mdd_neq_plus(m, a, b, c) mdd_func3(m,a,b,c,neq_plus3)
#define	mdd_eq_minus(m, a, b, c) mdd_func3(m,a,b,c,eq_minus3)
#define	mdd_geq_minus(m, a, b, c) mdd_func3(m,a,b,c,geq_minus3)
#define	mdd_gt_minus(m, a, b, c) mdd_func3(m,a,b,c,gt_minus3)
#define	mdd_leq_minus(m, a, b, c) mdd_func3(m,a,b,c,leq_minus3)
#define	mdd_lt_minus(m, a, b, c) mdd_func3(m,a,b,c,lt_minus3)
#define	mdd_neq_minus(m, a, b, c) mdd_func3(m,a,b,c,neq_minus3)
#define	mdd_eq_plus_c(m, a, b, c) mdd_func2c(m,a,b,c,eq_plus3)
#define	mdd_geq_plus_c(m, a, b, c) mdd_func2c(m,a,b,c,geq_plus3)
#define	mdd_gt_plus_c(m, a, b, c) mdd_func2c(m,a,b,c,gt_plus3)
#define	mdd_leq_plus_c(m, a, b, c) mdd_func2c(m,a,b,c,leq_plus3)
#define	mdd_lt_plus_c(m, a, b, c) mdd_func2c(m,a,b,c,lt_plus3)
#define	mdd_neq_plus_c(m, a, b, c) mdd_func2c(m,a,b,c,neq_plus3)
#define	mdd_eq_plus_c_mod(m, a, b, c) mdd_func2c_mod(m,a,b,c,eq_plus3mod)
#define	mdd_geq_plus_c_mod(m, a, b, c) mdd_func2c_mod(m,a,b,c,geq_plus3mod)
#define	mdd_gt_plus_c_mod(m, a, b, c) mdd_func2c_mod(m,a,b,c,gt_plus3mod)
#define	mdd_leq_plus_c_mod(m, a, b, c) mdd_func2c_mod(m,a,b,c,leq_plus3mod)
#define	mdd_lt_plus_c_mod(m, a, b, c) mdd_func2c_mod(m,a,b,c,lt_plus3mod)
#define	mdd_neq_plus_c_mod(m, a, b, c) mdd_func2c_mod(m,a,b,c,neq_plus3mod)
#define	mdd_eq_minus_c_mod(m, a, b, c) mdd_func2c_mod(m,a,b,c,eq_minus3mod)
#define	mdd_geq_minus_c_mod(m, a, b, c) mdd_func2c_mod(m,a,b,c,geq_minus3mod)
#define	mdd_gt_minus_c_mod(m, a, b, c) mdd_func2c_mod(m,a,b,c,gt_minus3mod)
#define	mdd_leq_minus_c_mod(m, a, b, c) mdd_func2c_mod(m,a,b,c,leq_minus3mod)
#define	mdd_lt_minus_c_mod(m, a, b, c) mdd_func2c_mod(m,a,b,c,lt_minus3mod)
#define	mdd_neq_minus_c_mod(m, a, b, c) mdd_func2c_mod(m,a,b,c,neq_minus3mod)
#define	mdd_eq_s(m, a, b) mdd_ineq_template_s(m,a,b,0,0,1)
#define	mdd_geq_s(m, a, b) mdd_ineq_template_s(m,a,b,0,1,1)
#define	mdd_gt_s(m, a, b) mdd_ineq_template_s(m,a,b,0,1,0)
#define	mdd_neq_s(m, a, b) mdd_ineq_template_s(m,a,b,1,1,0)
#define	mdd_leq_s(m, a, b) mdd_ineq_template_s(m,a,b,1,0,1)
#define	mdd_lt_s(m, a, b) mdd_ineq_template_s(m,a,b,1,0,0)
#define	mdd_eq_g(m, a, b) mdd_func2(m,a,b,eq2)
#define	mdd_geq_g(m, a, b) mdd_func2(m,a,b,geq2)
#define	mdd_gt_g(m, a, b) mdd_func2(m,a,b,gt2)
#define	mdd_leq_g(m, a, b) mdd_func2(m,a,b,leq2)
#define	mdd_lt_g(m, a, b) mdd_func2(m,a,b,lt2)
#define	mdd_neq_g(m, a, b) mdd_func2(m,a,b,neq2)
#define	mdd_init_name(v, n, s) mdd_init(v,n,s)
#define	MDD_NOT(node) ((bdd_node *) ((int) (node) ^ 01))
#define	MDD_REGULAR(node) ((bdd_node *) ((int) (node) & ~01))
#define	MDD_IS_COMPLEMENT(node) ((int) (node) & 01)
#define	MDD_ONE(bdd) (bdd)->one
#define	MDD_ZERO(bdd) (MDD_NOT(MDD_ONE(bdd)))
#define	MAX(a, b) (a) > (b) ? (a) : (b)
#define	MIN(a, b) (a) < (b) ? (a) : (b)
#define	foreach_mdd_minterm(fn, gen, minterm, var_list)
Typedefs
typedef bdd_t	mdd_t
typedef bdd_manager	mdd_manager
typedef struct mvar_type	mvar_type
typedef struct bvar_type	bvar_type
typedef struct mdd_hook_type	mdd_hook_type
typedef struct mdd_gen	mdd_gen
Enumerations
enum	mvar_status { MDD_ACTIVE, MDD_BUNDLED }
Functions
EXTERN mdd_manager *mdd_init	ARGS ((array_t mvar_values, array_t mvar_names, array_t *mvar_strides))
EXTERN mdd_manager *mdd_init_empty	ARGS ((void))
EXTERN unsigned int mdd_create_variables	ARGS ((mdd_manager mgr, array_t mvar_values, array_t mvar_names, array_t mvar_strides))
EXTERN unsigned int mdd_create_variables_after	ARGS ((mdd_manager , int, array_t , array_t , array_t ))
EXTERN unsigned int mdd_create_variables_interleaved	ARGS ((mdd_manager , int, int, array_t ))
EXTERN void mdd_quit	ARGS ((mdd_manager *mgr))
EXTERN void mdd_var_expunge_bdd_variable	ARGS ((mdd_manager *mgr, int bddId, int val))
EXTERN mdd_t *mdd_case	ARGS ((mdd_manager mgr, int mvar, array_t child_list))
EXTERN mdd_t *mdd_consensus	ARGS ((mdd_manager mgr, mdd_t fn, array_t *mvars))
EXTERN mdd_t *mdd_encode	ARGS ((mdd_manager mgr, array_t child_list, mvar_type *mv_ptr, int index))
EXTERN mdd_t *mdd_literal	ARGS ((mdd_manager mgr, int mddid, array_t values))
EXTERN void mdd_search	ARGS ((mdd_manager mgr, bdd_t top, int phase, boolean minterms))
EXTERN mdd_t *mdd_cofactor	ARGS ((mdd_manager mgr, mdd_t fn, mdd_t *cube))
EXTERN mdd_t *mdd_and_smooth	ARGS ((mdd_manager mgr, mdd_t f, mdd_t g, array_t mvars))
EXTERN mdd_t *mdd_and_smooth_with_limit	ARGS ((mdd_manager mgr, mdd_t f, mdd_t g, array_t mvars, unsigned int limit))
EXTERN mdd_t *mdd_substitute	ARGS ((mdd_manager mgr, mdd_t fn, array_t old_mvars, array_t new_mvars))
EXTERN array_t *mdd_substitute_array	ARGS ((mdd_manager mgr, array_t fn_array, array_t old_mvars, array_t new_mvars))
EXTERN array_t *mdd_get_support	ARGS ((mdd_manager mdd_mgr, mdd_t f))
EXTERN mdd_t *mdd_interval	ARGS ((mdd_manager *mgr, int mvar_id, int low, int high))
EXTERN double mdd_count_onset	ARGS ((mdd_manager mddMgr, mdd_t aMdd, array_t *mddIdArr))
EXTERN int mdd_epd_count_onset	ARGS ((mdd_manager mddMgr, mdd_t aMdd, array_t mddIdArr, EpDouble epd))
EXTERN array_t *mdd_ret_bvars_of_mvar	ARGS ((mvar_type *mvar_ptr))
EXTERN mdd_t *mdd_cproject	ARGS ((mdd_manager mgr, mdd_t T, array_t *mvars))
EXTERN mdd_t *mdd_mod	ARGS ((mdd_manager *mgr, int a_mvar_id, int b_mvar_id, int M))
EXTERN mdd_t *mdd_ineq_template_s	ARGS ((mdd_manager *mgr, int mvar1, int mvar2, int zero_then_val, int one_else_val, int bottom_val))
EXTERN mdd_t *mdd_add_s	ARGS ((mdd_manager *mgr, int sum_id, int mvar_id1, int mvar_id2))
EXTERN mdd_gen *mdd_first_minterm	ARGS ((mdd_t f, array_t minterm_p, array_t var_list))
EXTERN boolean mdd_next_minterm	ARGS ((mdd_gen mgen, array_t *minterm_p))
EXTERN void mdd_print_array	ARGS ((array_t *array))
EXTERN int mdd_gen_free	ARGS ((mdd_gen *mgen))
EXTERN mdd_t *mdd_func1c	ARGS ((mdd_manager mgr, int mvar1, int mvar2, boolean(func1c)(int, int)))
EXTERN mdd_t *mdd_func2	ARGS ((mdd_manager mgr, int mvar1, int mvar2, boolean(func2)(int, int)))
EXTERN boolean eq2	ARGS ((int x, int y))
EXTERN mdd_t *mdd_func2c	ARGS ((mdd_manager mgr, int mvar1, int mvar2, int constant, boolean(func3)(int, int, int)))
EXTERN mdd_t *mdd_func2c_mod	ARGS ((mdd_manager mgr, int mvar1, int mvar2, int constant, boolean(func4)(int, int, int, int)))
EXTERN mdd_t *mdd_func3	ARGS ((mdd_manager mgr, int mvar1, int mvar2, int mvar3, boolean(func3)(int, int, int)))
EXTERN boolean eq_plus3	ARGS ((int x, int y, int z))
EXTERN array_t *mdd_id_to_bdd_id_array	ARGS ((mdd_manager *mddManager, int mddId))
EXTERN array_t *mdd_id_array_to_bdd_array	ARGS ((mdd_manager mddManager, array_t mddIdArray))
EXTERN int mdd_get_number_of_bdd_support	ARGS ((mdd_manager mddManager, mdd_t f))
EXTERN array_t *mdd_fn_array_to_bdd_rel_array	ARGS ((mdd_manager mddManager, int mddId, array_t mddFnArray))
EXTERN array_t *mdd_pick_arbitrary_minterms	ARGS ((mdd_manager mgr, mdd_t f, array_t *mddIdArr, int n))
EXTERN mdd_t *mdd_subset_with_mask_vars	ARGS ((mdd_manager mgr, mdd_t f, array_t mddIdArr, array_t maskIdArr))
EXTERN mvar_type mdd_get_var_by_id	ARGS ((mdd_manager *mddMgr, int id))
EXTERN void mdd_print_support	ARGS ((mdd_t *f))
EXTERN void mdd_print_support_to_file	ARGS ((FILE fout, char format, mdd_t *f))
EXTERN int mdd_check_support	ARGS ((mdd_manager mddMgr, mdd_t mdd, array_t *supportIdArray))
EXTERN int mdd_equal_mod_care_set_array	ARGS ((mdd_t aSet, mdd_t bSet, array_t *CareSetArray))
EXTERN int mdd_lequal_mod_care_set_array	ARGS ((mdd_t aSet, mdd_t bSet, boolean aPhase, boolean bPhase, array_t *CareSetArray))
EXTERN boolean eq_plus3mod	ARGS ((int x, int y, int z, int range))
EXTERN void mdd_array_dump_dot	ARGS ((array_t mdds, char name, FILE *fp))
EXTERN void mdd_dump_dot	ARGS ((mdd_t mdd, char name, FILE *fp))
EXTERN void mdd_array_print_cover	ARGS ((array_t mdds, char name, boolean disjoint))
EXTERN void mdd_print_cover	ARGS ((mdd_t f, char name, boolean disjoint))
EXTERN int toggle	ARGS ((int x))
EXTERN int no_bit_encode	ARGS ((int n))
EXTERN void print_strides	ARGS ((array_t *mvar_strides))
EXTERN void print_bdd_list_id	ARGS ((array_t *bdd_list))
EXTERN void print_bdd	ARGS ((bdd_manager mgr, bdd_t top))
EXTERN mvar_type find_mvar_id	ARGS ((mdd_manager *mgr, unsigned short id))
EXTERN void mdd_mark	ARGS ((mdd_manager mgr, bdd_t top, int phase))
EXTERN void mdd_unmark	ARGS ((mdd_manager mgr, bdd_t top))
EXTERN mvar_type find_mvar	ARGS ((mdd_manager mgr, char name))
EXTERN void mdd_set_mvar_list	ARGS ((mdd_manager mgr, array_t mvar_list))
EXTERN void mdd_set_bvar_list	ARGS ((mdd_manager mgr, array_t bvar_list))
EXTERN mdd_t *build_lt_c	ARGS ((mdd_manager *mgr, int mvar_id, int c))
EXTERN int getbit	ARGS ((int number, int position))
EXTERN int integer_get_num_of_digits	ARGS ((int value))
EXTERN int mdd_ret_bvar_id	ARGS ((mvar_type *mvar_ptr, int i))
EXTERN bvar_type mdd_ret_bvar	ARGS ((mvar_type mvar_ptr, int i, array_t bvar_list))
EXTERN void mdd_array_free	ARGS ((array_t *mddArray))
EXTERN void mdd_array_array_free	ARGS ((array_t *arrayBddArray))
EXTERN boolean mdd_array_equal	ARGS ((array_t array1, array_t array2))
EXTERN mdd_t *mdd_range_mdd	ARGS ((mdd_manager mgr, array_t support))
EXTERN int mdd_bundle_variables	ARGS ((mdd_manager mgr, array_t bundle_vars, char mdd_var_name, int mdd_id))
EXTERN mdd_t *mdd_unary_minus_s	ARGS ((mdd_manager *mgr, int mvar1, int mvar2))
EXTERN array_t *mvar2bdds	ARGS ((mdd_manager mgr, array_t mvars))
Variables
mdd_hook_type	mdd_hook

Define Documentation

#define BDD_SIZE 1

Definition at line 23 of file mdd.h.

#define BYPASS 1

Definition at line 25 of file mdd.h.

#define foreach_mdd_minterm	(	fn,
		gen,
		minterm,
		var_list	)

Value:

for((gen) = mdd_first_minterm(fn, &minterm, var_list);\
      ((gen)->status != bdd_EMPTY) ? TRUE: mdd_gen_free(gen);\
      (void) mdd_next_minterm(gen, &minterm))

Definition at line 198 of file mdd.h.

#define INTERLEAVE 0

Definition at line 27 of file mdd.h.

#define MAX	(	a,
		b		)	(a) > (b) ? (a) : (b)

Definition at line 144 of file mdd.h.

#define mdd_and bdd_and

Definition at line 29 of file mdd.h.

#define mdd_and_array bdd_and_array

Definition at line 31 of file mdd.h.

#define mdd_and_with_limit bdd_and_with_limit

Definition at line 30 of file mdd.h.

#define mdd_closest_cube bdd_closest_cube

Definition at line 40 of file mdd.h.

#define mdd_cofactor_minterm bdd_cofactor

Definition at line 32 of file mdd.h.

#define mdd_constant bdd_constant

Definition at line 33 of file mdd.h.

#define mdd_dup bdd_dup

Definition at line 34 of file mdd.h.

#define mdd_EMPTY bdd_EMPTY

Definition at line 63 of file mdd.h.

#define mdd_eq	(	m,
		a,
		b	)	mdd_func2(m,a,b,eq2)

Definition at line 75 of file mdd.h.

#define mdd_eq_c	(	m,
		a,
		b	)	mdd_func1c(m,a,b,eq2)

Definition at line 68 of file mdd.h.

#define mdd_eq_g	(	m,
		a,
		b	)	mdd_func2(m,a,b,eq2)

Definition at line 127 of file mdd.h.

#define mdd_eq_minus	(	m,
		a,
		b,
		c	)	mdd_func3(m,a,b,c,eq_minus3)

Definition at line 90 of file mdd.h.

#define mdd_eq_minus_c_mod	(	m,
		a,
		b,
		c	)	mdd_func2c_mod(m,a,b,c,eq_minus3mod)

Definition at line 112 of file mdd.h.

#define mdd_eq_plus	(	m,
		a,
		b,
		c	)	mdd_func3(m,a,b,c,eq_plus3)

Definition at line 83 of file mdd.h.

#define mdd_eq_plus_c	(	m,
		a,
		b,
		c	)	mdd_func2c(m,a,b,c,eq_plus3)

Definition at line 97 of file mdd.h.

#define mdd_eq_plus_c_mod	(	m,
		a,
		b,
		c	)	mdd_func2c_mod(m,a,b,c,eq_plus3mod)

Definition at line 105 of file mdd.h.

#define mdd_eq_s	(	m,
		a,
		b	)	mdd_ineq_template_s(m,a,b,0,0,1)

Definition at line 119 of file mdd.h.

#define mdd_equal bdd_equal

Definition at line 38 of file mdd.h.

#define mdd_equal_mod_care_set bdd_equal_mod_care_set

Definition at line 39 of file mdd.h.

#define mdd_first_solution mdd_first_cube

Definition at line 65 of file mdd.h.

#define mdd_free bdd_free

Definition at line 41 of file mdd.h.

#define mdd_geq	(	m,
		a,
		b	)	mdd_func2(m,a,b,geq2)

Definition at line 76 of file mdd.h.

#define mdd_geq_c	(	m,
		a,
		b	)	mdd_func1c(m,a,b,geq2)

Definition at line 69 of file mdd.h.

#define mdd_geq_g	(	m,
		a,
		b	)	mdd_func2(m,a,b,geq2)

Definition at line 128 of file mdd.h.

#define mdd_geq_minus	(	m,
		a,
		b,
		c	)	mdd_func3(m,a,b,c,geq_minus3)

Definition at line 91 of file mdd.h.

#define mdd_geq_minus_c_mod	(	m,
		a,
		b,
		c	)	mdd_func2c_mod(m,a,b,c,geq_minus3mod)

Definition at line 113 of file mdd.h.

#define mdd_geq_plus	(	m,
		a,
		b,
		c	)	mdd_func3(m,a,b,c,geq_plus3)

Definition at line 84 of file mdd.h.

#define mdd_geq_plus_c	(	m,
		a,
		b,
		c	)	mdd_func2c(m,a,b,c,geq_plus3)

Definition at line 98 of file mdd.h.

#define mdd_geq_plus_c_mod	(	m,
		a,
		b,
		c	)	mdd_func2c_mod(m,a,b,c,geq_plus3mod)

Definition at line 106 of file mdd.h.

#define mdd_geq_s	(	m,
		a,
		b	)	mdd_ineq_template_s(m,a,b,0,1,1)

Definition at line 120 of file mdd.h.

#define mdd_get_manager bdd_get_manager

Definition at line 42 of file mdd.h.

#define mdd_gt	(	m,
		a,
		b	)	mdd_func2(m,a,b,gt2)

Definition at line 77 of file mdd.h.

#define mdd_gt_c	(	m,
		a,
		b	)	mdd_func1c(m,a,b,gt2)

Definition at line 70 of file mdd.h.

#define mdd_gt_g	(	m,
		a,
		b	)	mdd_func2(m,a,b,gt2)

Definition at line 129 of file mdd.h.

#define mdd_gt_minus	(	m,
		a,
		b,
		c	)	mdd_func3(m,a,b,c,gt_minus3)

Definition at line 92 of file mdd.h.

#define mdd_gt_minus_c_mod	(	m,
		a,
		b,
		c	)	mdd_func2c_mod(m,a,b,c,gt_minus3mod)

Definition at line 114 of file mdd.h.

#define mdd_gt_plus	(	m,
		a,
		b,
		c	)	mdd_func3(m,a,b,c,gt_plus3)

Definition at line 85 of file mdd.h.

#define mdd_gt_plus_c	(	m,
		a,
		b,
		c	)	mdd_func2c(m,a,b,c,gt_plus3)

Definition at line 99 of file mdd.h.

#define mdd_gt_plus_c_mod	(	m,
		a,
		b,
		c	)	mdd_func2c_mod(m,a,b,c,gt_plus3mod)

Definition at line 107 of file mdd.h.

#define mdd_gt_s	(	m,
		a,
		b	)	mdd_ineq_template_s(m,a,b,0,1,0)

Definition at line 121 of file mdd.h.

#define mdd_init_name	(	v,
		n,
		s	)	mdd_init(v,n,s)

Definition at line 133 of file mdd.h.

#define MDD_IS_COMPLEMENT ( node ) ((int) (node) & 01)

Definition at line 138 of file mdd.h.

#define mdd_is_tautology bdd_is_tautology

Definition at line 43 of file mdd.h.

#define mdd_ite bdd_ite

Definition at line 44 of file mdd.h.

#define mdd_leq	(	m,
		a,
		b	)	mdd_func2(m,a,b,leq2)

Definition at line 78 of file mdd.h.

#define mdd_leq_c	(	m,
		a,
		b	)	mdd_func1c(m,a,b,leq2)

Definition at line 71 of file mdd.h.

#define mdd_leq_g	(	m,
		a,
		b	)	mdd_func2(m,a,b,leq2)

Definition at line 130 of file mdd.h.

#define mdd_leq_minus	(	m,
		a,
		b,
		c	)	mdd_func3(m,a,b,c,leq_minus3)

Definition at line 93 of file mdd.h.

#define mdd_leq_minus_c_mod	(	m,
		a,
		b,
		c	)	mdd_func2c_mod(m,a,b,c,leq_minus3mod)

Definition at line 115 of file mdd.h.

#define mdd_leq_plus	(	m,
		a,
		b,
		c	)	mdd_func3(m,a,b,c,leq_plus3)

Definition at line 86 of file mdd.h.

#define mdd_leq_plus_c	(	m,
		a,
		b,
		c	)	mdd_func2c(m,a,b,c,leq_plus3)

Definition at line 100 of file mdd.h.

#define mdd_leq_plus_c_mod	(	m,
		a,
		b,
		c	)	mdd_func2c_mod(m,a,b,c,leq_plus3mod)

Definition at line 108 of file mdd.h.

#define mdd_leq_s	(	m,
		a,
		b	)	mdd_ineq_template_s(m,a,b,1,0,1)

Definition at line 123 of file mdd.h.

#define mdd_lequal bdd_leq

Definition at line 48 of file mdd.h.

#define mdd_lequal_array bdd_leq_array

Definition at line 50 of file mdd.h.

#define mdd_lequal_mod_care_set bdd_lequal_mod_care_set

Definition at line 49 of file mdd.h.

#define mdd_lt	(	m,
		a,
		b	)	mdd_func2(m,a,b,lt2)

Definition at line 79 of file mdd.h.

#define mdd_lt_c	(	m,
		a,
		b	)	mdd_func1c(m,a,b,lt2)

Definition at line 72 of file mdd.h.

#define mdd_lt_g	(	m,
		a,
		b	)	mdd_func2(m,a,b,lt2)

Definition at line 131 of file mdd.h.

#define mdd_lt_minus	(	m,
		a,
		b,
		c	)	mdd_func3(m,a,b,c,lt_minus3)

Definition at line 94 of file mdd.h.

#define mdd_lt_minus_c_mod	(	m,
		a,
		b,
		c	)	mdd_func2c_mod(m,a,b,c,lt_minus3mod)

Definition at line 116 of file mdd.h.

#define mdd_lt_plus	(	m,
		a,
		b,
		c	)	mdd_func3(m,a,b,c,lt_plus3)

Definition at line 87 of file mdd.h.

#define mdd_lt_plus_c	(	m,
		a,
		b,
		c	)	mdd_func2c(m,a,b,c,lt_plus3)

Definition at line 101 of file mdd.h.

#define mdd_lt_plus_c_mod	(	m,
		a,
		b,
		c	)	mdd_func2c_mod(m,a,b,c,lt_plus3mod)

Definition at line 109 of file mdd.h.

#define mdd_lt_s	(	m,
		a,
		b	)	mdd_ineq_template_s(m,a,b,1,0,0)

Definition at line 124 of file mdd.h.

#define mdd_multiway_and bdd_multiway_and

Definition at line 51 of file mdd.h.

#define mdd_multiway_or bdd_multiway_or

Definition at line 52 of file mdd.h.

#define mdd_multiway_xor bdd_multiway_xor

Definition at line 53 of file mdd.h.

#define mdd_neq	(	m,
		a,
		b	)	mdd_func2(m,a,b,neq2)

Definition at line 80 of file mdd.h.

#define mdd_neq_c	(	m,
		a,
		b	)	mdd_func1c(m,a,b,neq2)

Definition at line 73 of file mdd.h.

#define mdd_neq_g	(	m,
		a,
		b	)	mdd_func2(m,a,b,neq2)

Definition at line 132 of file mdd.h.

#define mdd_neq_minus	(	m,
		a,
		b,
		c	)	mdd_func3(m,a,b,c,neq_minus3)

Definition at line 95 of file mdd.h.

#define mdd_neq_minus_c_mod	(	m,
		a,
		b,
		c	)	mdd_func2c_mod(m,a,b,c,neq_minus3mod)

Definition at line 117 of file mdd.h.

#define mdd_neq_plus	(	m,
		a,
		b,
		c	)	mdd_func3(m,a,b,c,neq_plus3)

Definition at line 88 of file mdd.h.

#define mdd_neq_plus_c	(	m,
		a,
		b,
		c	)	mdd_func2c(m,a,b,c,neq_plus3)

Definition at line 102 of file mdd.h.

#define mdd_neq_plus_c_mod	(	m,
		a,
		b,
		c	)	mdd_func2c_mod(m,a,b,c,neq_plus3mod)

Definition at line 110 of file mdd.h.

#define mdd_neq_s	(	m,
		a,
		b	)	mdd_ineq_template_s(m,a,b,1,1,0)

Definition at line 122 of file mdd.h.

#define mdd_next_solution mdd_next_cube

Definition at line 66 of file mdd.h.

#define MDD_NOT ( node ) ((bdd_node *) ((int) (node) ^ 01))

Definition at line 136 of file mdd.h.

#define mdd_not bdd_not

Definition at line 54 of file mdd.h.

#define MDD_ONE ( bdd ) (bdd)->one

Definition at line 140 of file mdd.h.

#define mdd_one bdd_one

Definition at line 55 of file mdd.h.

#define mdd_or bdd_or

Definition at line 56 of file mdd.h.

#define MDD_REGULAR ( node ) ((bdd_node *) ((int) (node) & ~01))

Definition at line 137 of file mdd.h.

#define mdd_size bdd_size

Definition at line 57 of file mdd.h.

#define mdd_size_multiple bdd_size_multiple

Definition at line 58 of file mdd.h.

#define mdd_top_var_id bdd_top_var_id

Definition at line 59 of file mdd.h.

#define mdd_unary_minus	(	m,
		a,
		b	)	mdd_func2(m,a,b,unary_minus2)

Definition at line 81 of file mdd.h.

#define MDD_VERBOSE 0

Definition at line 21 of file mdd.h.

#define mdd_xnor bdd_xnor

Definition at line 61 of file mdd.h.

#define mdd_xor bdd_xor

Definition at line 60 of file mdd.h.

#define MDD_ZERO ( bdd ) (MDD_NOT(MDD_ONE(bdd)))

Definition at line 141 of file mdd.h.

#define mdd_zero bdd_zero

Definition at line 62 of file mdd.h.

#define MIN	(	a,
		b		)	(a) < (b) ? (a) : (b)

Definition at line 148 of file mdd.h.

#define MONITOR 0

Definition at line 20 of file mdd.h.

#define SOLUTION 0

Definition at line 22 of file mdd.h.

#define str_len 10

Definition at line 19 of file mdd.h.

#define USE_ITE 1

Definition at line 24 of file mdd.h.

Typedef Documentation

typedef struct bvar_type bvar_type

Definition at line 177 of file mdd.h.

typedef struct mdd_gen mdd_gen

Definition at line 196 of file mdd.h.

typedef struct mdd_hook_type mdd_hook_type

Definition at line 184 of file mdd.h.

typedef bdd_manager mdd_manager

Definition at line 152 of file mdd.h.

typedef bdd_t mdd_t

Definition at line 151 of file mdd.h.

typedef struct mvar_type mvar_type

Definition at line 171 of file mdd.h.

Enumeration Type Documentation

enum mvar_status

Enumerator:

MDD_ACTIVE
MDD_BUNDLED

Definition at line 154 of file mdd.h.

00154              {
00155         MDD_ACTIVE,
00156         MDD_BUNDLED
00157 } mvar_status;

Function Documentation

EXTERN array_t* mvar2bdds ARGS ( (mdd_manager *mgr, array_t *mvars) )

EXTERN mdd_t* mdd_unary_minus_s ARGS ( (mdd_manager *mgr, int mvar1, int mvar2) )

EXTERN int mdd_bundle_variables ARGS ( (mdd_manager *mgr, array_t *bundle_vars, char *mdd_var_name, int *mdd_id) )

EXTERN mdd_t* mdd_range_mdd ARGS ( (mdd_manager *mgr, array_t *support) )

EXTERN boolean mdd_array_equal ARGS ( (array_t *array1, array_t *array2) )

EXTERN void mdd_array_array_free ARGS ( (array_t *arrayBddArray) )

EXTERN array_t *mdd_array_duplicate ARGS ( (array_t *mddArray) )

EXTERN bvar_type mdd_ret_bvar ARGS ( (mvar_type *mvar_ptr, int i, array_t *bvar_list) )

EXTERN int mdd_ret_bvar_id ARGS ( (mvar_type *mvar_ptr, int i) )

EXTERN int integer_get_num_of_digits ARGS ( (int value) )

EXTERN int getbit ARGS ( (int number, int position) )

EXTERN mdd_t *build_geq_c ARGS ( (mdd_manager *mgr, int mvar_id, int c) )

EXTERN void mdd_set_bvar_list ARGS ( (mdd_manager *mgr, array_t *bvar_list) )

EXTERN void mdd_set_mvar_list ARGS ( (mdd_manager *mgr, array_t *mvar_list) )

EXTERN mvar_type find_mvar ARGS ( (mdd_manager *mgr, char *name) )

EXTERN void mdd_unmark ARGS ( (mdd_manager *mgr, bdd_t *top) )

EXTERN void mdd_mark ARGS ( (mdd_manager *mgr, bdd_t *top, int phase) )

EXTERN mvar_type find_mvar_id ARGS ( (mdd_manager *mgr, unsigned short id) )

EXTERN void print_bdd ARGS ( (bdd_manager *mgr, bdd_t *top) )

EXTERN void print_bdd_list_id ARGS ( (array_t *bdd_list) )

EXTERN void print_strides ARGS ( (array_t *mvar_strides) )

EXTERN int no_bit_encode ARGS ( (int n) )

EXTERN int toggle ARGS ( (int x) )

EXTERN void mdd_print_cover ARGS ( (mdd_t *f, char *name, boolean disjoint) )

EXTERN void mdd_array_print_cover ARGS ( (array_t *mdds, char *name, boolean disjoint) )

EXTERN void mdd_dump_dot ARGS ( (mdd_t *mdd, char *name, FILE *fp) )

EXTERN void mdd_array_dump_dot ARGS ( (array_t *mdds, char *name, FILE *fp) )

EXTERN boolean neq_minus3mod ARGS ( (int x, int y, int z, int range) )

EXTERN int mdd_lequal_mod_care_set_array ARGS ( (mdd_t *aSet, mdd_t *bSet, boolean aPhase, boolean bPhase, array_t *CareSetArray) )

EXTERN int mdd_equal_mod_care_set_array ARGS ( (mdd_t *aSet, mdd_t *bSet, array_t *CareSetArray) )

EXTERN int mdd_check_support ARGS ( (mdd_manager *mddMgr, mdd_t *mdd, array_t *supportIdArray) )

EXTERN void mdd_print_support_to_file ARGS ( (FILE *fout, char *format, mdd_t *f) )

EXTERN int mdd_read_mdd_id ARGS ( (mdd_t *f) )

EXTERN mvar_type mdd_get_var_by_id ARGS ( (mdd_manager *mddMgr, int id) )

EXTERN mdd_t* mdd_subset_with_mask_vars ARGS ( (mdd_manager *mgr, mdd_t *f, array_t *mddIdArr, array_t *maskIdArr) )

EXTERN array_t* mdd_pick_arbitrary_minterms ARGS ( (mdd_manager *mgr, mdd_t *f, array_t *mddIdArr, int n) )

EXTERN array_t *mdd_fn_array_to_bdd_fn_array ARGS ( (mdd_manager *mddManager, int mddId, array_t *mddFnArray) )

EXTERN int mdd_get_number_of_bdd_support ARGS ( (mdd_manager *mddManager, mdd_t *f) )

EXTERN int mdd_get_number_of_bdd_vars ARGS ( (mdd_manager *mddManager, array_t *mddIdArray) )

EXTERN array_t *mdd_id_to_bdd_array ARGS ( (mdd_manager *mddManager, int mddId) )

EXTERN boolean neq_minus3 ARGS ( (int x, int y, int z) )

EXTERN mdd_t* mdd_func3 ARGS ( (mdd_manager *mgr, int mvar1, int mvar2, int mvar3, boolean(*func3)(int, int, int)) )

EXTERN mdd_t* mdd_func2c_mod ARGS ( (mdd_manager *mgr, int mvar1, int mvar2, int constant, boolean(*func4)(int, int, int, int)) )

EXTERN mdd_t* mdd_func2c ARGS ( (mdd_manager *mgr, int mvar1, int mvar2, int constant, boolean(*func3)(int, int, int)) )

EXTERN boolean unary_minus2 ARGS ( (int x, int y) )

EXTERN mdd_t* mdd_func2 ARGS ( (mdd_manager *mgr, int mvar1, int mvar2, boolean(*func2)(int, int)) )

EXTERN mdd_t* mdd_func1c ARGS ( (mdd_manager *mgr, int mvar1, int mvar2, boolean(*func1c)(int, int)) )

EXTERN int mdd_gen_free ARGS ( (mdd_gen *mgen) )

EXTERN void mdd_print_array ARGS ( (array_t *array) )

EXTERN boolean mdd_next_minterm ARGS ( (mdd_gen *mgen, array_t **minterm_p) )

EXTERN mdd_gen* mdd_first_minterm ARGS ( (mdd_t *f, array_t **minterm_p, array_t *var_list) )

EXTERN mdd_t* mdd_add_s ARGS ( (mdd_manager *mgr, int sum_id, int mvar_id1, int mvar_id2) )

EXTERN mdd_t* mdd_ineq_template_s ARGS ( (mdd_manager *mgr, int mvar1, int mvar2, int zero_then_val, int one_else_val, int bottom_val) )

EXTERN mdd_t* mdd_mod ARGS ( (mdd_manager *mgr, int a_mvar_id, int b_mvar_id, int M) )

EXTERN mdd_t* mdd_cproject ARGS ( (mdd_manager *mgr, mdd_t *T, array_t *mvars) )

EXTERN array_t* mdd_ret_bvars_of_mvar ARGS ( (mvar_type *mvar_ptr) )

EXTERN int mdd_epd_count_onset ARGS ( (mdd_manager *mddMgr, mdd_t *aMdd, array_t *mddIdArr, EpDouble *epd) )

EXTERN mdd_t *mdd_onset_bdd ARGS ( (mdd_manager *mddMgr, mdd_t *aMdd, array_t *mddIdArr) )

EXTERN mdd_t* mdd_interval ARGS ( (mdd_manager *mgr, int mvar_id, int low, int high) )

EXTERN array_t *mdd_get_bdd_support_vars ARGS ( (mdd_manager *mdd_mgr, mdd_t *f) )

EXTERN array_t* mdd_substitute_array ARGS ( (mdd_manager *mgr, array_t *fn_array, array_t *old_mvars, array_t *new_mvars) )

EXTERN mdd_t* mdd_substitute ARGS ( (mdd_manager *mgr, mdd_t *fn, array_t *old_mvars, array_t *new_mvars) )

EXTERN mdd_t* mdd_and_smooth_with_limit ARGS ( (mdd_manager *mgr, mdd_t *f, mdd_t *g, array_t *mvars, unsigned int limit) )

EXTERN mdd_t* mdd_and_smooth ARGS ( (mdd_manager *mgr, mdd_t *f, mdd_t *g, array_t *mvars) )

EXTERN mdd_t* mdd_cofactor ARGS ( (mdd_manager *mgr, mdd_t *fn, mdd_t *cube) )

EXTERN void mdd_search ARGS ( (mdd_manager *mgr, bdd_t *top, int phase, boolean minterms) )

EXTERN mdd_t* mdd_literal ARGS ( (mdd_manager *mgr, int mddid, array_t *values) )

EXTERN mdd_t* mdd_encode ARGS ( (mdd_manager *mgr, array_t *child_list, mvar_type *mv_ptr, int index) )

EXTERN mdd_t *mdd_smooth ARGS ( (mdd_manager *mgr, mdd_t *fn, array_t *mvars) )

EXTERN mdd_t* mdd_case ARGS ( (mdd_manager *mgr, int mvar, array_t *child_list) )

EXTERN void mdd_var_expunge_bdd_variable ARGS ( (mdd_manager *mgr, int bddId, int val) )

EXTERN array_t *mdd_ret_bvar_list ARGS ( (mdd_manager *mgr) )

EXTERN unsigned int mdd_create_variables_interleaved ARGS ( (mdd_manager *, int, int, array_t *) )

EXTERN unsigned int mdd_create_variables_after ARGS ( (mdd_manager *, int, array_t *, array_t *, array_t *) )

EXTERN unsigned int mdd_create_variables ARGS ( (mdd_manager *mgr, array_t *mvar_values, array_t *mvar_names, array_t *mvar_strides) )

EXTERN mdd_manager* mdd_init_empty ARGS ( (void) )

EXTERN mdd_manager* mdd_init ARGS ( (array_t *mvar_values, array_t *mvar_names, array_t *mvar_strides) )

Variable Documentation

mdd_hook_type mdd_hook

src/mdd/mdd.h File Reference

Data Structures

Defines

Typedefs

Enumerations

Functions

Variables

Define Documentation

Typedef Documentation

Enumeration Type Documentation

Function Documentation

Variable Documentation