00001 #include "mdd.h" 00002 00003 /* 00004 * MDD Package 00005 * 00006 * $Id: mdd_intv.c,v 1.9 2002/08/24 21:48:15 fabio Exp $ 00007 * 00008 * Author: Timothy Kam 00009 * 00010 * Copyright 1992 by the Regents of the University of California. 00011 * 00012 * All rights reserved. Permission to use, copy, modify and distribute 00013 * this software is hereby granted, provided that the above copyright 00014 * notice and this permission notice appear in all copies. This software 00015 * is made available as is, with no warranties. 00016 */ 00017 00018 /* var <= c */ 00019 mdd_t * 00020 build_leq_c( 00021 mdd_manager *mgr, 00022 int mvar_id, 00023 int c) 00024 { 00025 return build_lt_c(mgr, mvar_id, c+1); 00026 } 00027 00028 mdd_t * 00029 build_lt_c( 00030 mdd_manager *mgr, 00031 int mvar_id, 00032 int 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 } 00077 00078 00079 mdd_t * 00080 build_geq_c( 00081 mdd_manager *mgr, 00082 int mvar_id, 00083 int 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 } 00126 00127 00128 mdd_t * 00129 build_gt_c( 00130 mdd_manager *mgr, 00131 int mvar_id, 00132 int c) 00133 { 00134 return build_geq_c(mgr, mvar_id, c+1); 00135 } 00136 00137 /* low <= var <= high */ 00138 mdd_t * 00139 mdd_interval( 00140 mdd_manager *mgr, 00141 int mvar_id, 00142 int low, 00143 int high) 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 } 00158 00159 /*---------------------------------------------------------------------------*/ 00160 /* Static function prototypes */ 00161 /*---------------------------------------------------------------------------*/ 00162
1.6.1