src/mdd/mdd_intv.c File Reference

#include "mdd.h"

Include dependency graph for mdd_intv.c:

Functions
mdd_t *	build_leq_c (mdd_manager *mgr, int mvar_id, int c)
mdd_t *	build_lt_c (mdd_manager *mgr, int mvar_id, int c)
mdd_t *	build_geq_c (mdd_manager *mgr, int mvar_id, int c)
mdd_t *	build_gt_c (mdd_manager *mgr, int mvar_id, int c)
mdd_t *	mdd_interval (mdd_manager *mgr, int mvar_id, int low, int high)

Function Documentation

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

Definition at line 80 of file mdd_intv.c.

00084 {
00085 /*
00086   mdd_t *A, *one, *zero;
00087         array_t *bvar_list = mdd_ret_bvar_list(mgr),
00088                 *mvar_list = mdd_ret_mvar_list(mgr);
00089         mvar_type a_mv;
00090         int i;
00091         bvar_type bit_i;
00092         mdd_t *temp_A;
00093 
00094         one = mdd_one(mgr);
00095         zero = mdd_zero(mgr);
00096 
00097         a_mv = array_fetch( mvar_type, mvar_list, mvar_id);
00098 
00099         if ( a_mv.values <= c ) { 
00100                 mdd_free( one );
00101                 return zero;
00102         }
00103 
00104 
00105         A = mdd_one(mgr);
00106 
00107         for(i=1; i <= a_mv.encode_length; i++){
00108                 bit_i = mdd_ret_bvar(&a_mv, (a_mv.encode_length - i), bvar_list );
00109                 temp_A = A;
00110                 if ( getbit(c,i-1) == 0 ) {
00111                         A = mdd_ite(bit_i.node, one, temp_A, 1, 1, 1);
00112                 }
00113                 else {
00114                         A = mdd_ite(bit_i.node, temp_A, zero, 1, 1, 1);
00115                      }
00116                 bdd_free(temp_A);       
00117         }
00118 
00119         mdd_free(one);
00120         mdd_free(zero);
00121                 
00122         return A;
00123     */
00124     return mdd_geq_c(mgr, mvar_id, c);
00125 }

mdd_t* build_gt_c	(	mdd_manager *	mgr,
		int	mvar_id,
		int	c
	)

Definition at line 129 of file mdd_intv.c.

00133 {
00134         return build_geq_c(mgr, mvar_id, c+1);
00135 }

mdd_t* build_leq_c	(	mdd_manager *	mgr,
		int	mvar_id,
		int	c
	)

Definition at line 20 of file mdd_intv.c.

00024 {
00025         return build_lt_c(mgr, mvar_id, c+1);
00026 }

mdd_t* build_lt_c	(	mdd_manager *	mgr,
		int	mvar_id,
		int	c
	)

Definition at line 29 of file mdd_intv.c.

00033 {
00034 /*      mdd_t *A, *one, *zero;
00035         array_t *mvar_list = mdd_ret_mvar_list(mgr);
00036         array_t *bvar_list = mdd_ret_bvar_list(mgr);
00037         mvar_type a_mv;
00038         int i;
00039         bvar_type bit_i;
00040         mdd_t *temp_A;
00041 
00042         one = mdd_one(mgr);
00043         zero = mdd_zero(mgr);
00044 
00045         a_mv = array_fetch( mvar_type, mvar_list, mvar_id);
00046 
00047 
00048         if ( a_mv.values <= c ) {
00049                 mdd_free(zero);
00050                 return one;
00051         }
00052 
00053         A = mdd_zero(mgr);
00054 
00055         for(i=1; i <= a_mv.encode_length; i++){
00056                 bit_i = mdd_ret_bvar(&a_mv, (a_mv.encode_length - i), bvar_list);
00057                 temp_A = A;
00058                 if ( getbit(c,i-1) == 0 ) {
00059                         A = mdd_ite(bit_i.node, zero, temp_A, 1, 1, 1);
00060                 }
00061                 else {
00062                         A = mdd_ite(bit_i.node, temp_A, one, 1, 1, 1);
00063                 }
00064                 bdd_free(temp_A);
00065         }
00066 
00067         mdd_free(one);
00068         mdd_free(zero);
00069                 
00070         return A;
00071     */
00072 
00073 /* Temporary fix until the routines are rewritten taking care of don't cares. */    
00074 
00075     return mdd_lt_c(mgr, mvar_id, c);
00076 }

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

Definition at line 139 of file mdd_intv.c.

00144 {
00145         mdd_t *HIGH_MDD, *LOW_MDD, *result;
00146 
00147 
00148     LOW_MDD = build_geq_c(mgr,mvar_id,low);
00149         HIGH_MDD = build_leq_c(mgr,mvar_id,high);
00150 
00151         result = mdd_and(HIGH_MDD, LOW_MDD, 1, 1);
00152 
00153         mdd_free(LOW_MDD);
00154         mdd_free(HIGH_MDD);
00155 
00156         return result;
00157 }

src/mdd/mdd_intv.c File Reference

Functions

Function Documentation