[8] | 1 | #include "mdd.h" |
---|
| 2 | |
---|
| 3 | /* |
---|
| 4 | * MDD Package |
---|
| 5 | * |
---|
| 6 | * $Id: mdd_intv.c,v 1.9 2002/08/24 21:48:15 fabio Exp $ |
---|
| 7 | * |
---|
| 8 | * Author: Timothy Kam |
---|
| 9 | * |
---|
| 10 | * Copyright 1992 by the Regents of the University of California. |
---|
| 11 | * |
---|
| 12 | * All rights reserved. Permission to use, copy, modify and distribute |
---|
| 13 | * this software is hereby granted, provided that the above copyright |
---|
| 14 | * notice and this permission notice appear in all copies. This software |
---|
| 15 | * is made available as is, with no warranties. |
---|
| 16 | */ |
---|
| 17 | |
---|
| 18 | /* var <= c */ |
---|
| 19 | mdd_t * |
---|
| 20 | build_leq_c( |
---|
| 21 | mdd_manager *mgr, |
---|
| 22 | int mvar_id, |
---|
| 23 | int c) |
---|
| 24 | { |
---|
| 25 | return build_lt_c(mgr, mvar_id, c+1); |
---|
| 26 | } |
---|
| 27 | |
---|
| 28 | mdd_t * |
---|
| 29 | build_lt_c( |
---|
| 30 | mdd_manager *mgr, |
---|
| 31 | int mvar_id, |
---|
| 32 | int c) |
---|
| 33 | { |
---|
| 34 | /* mdd_t *A, *one, *zero; |
---|
| 35 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 36 | array_t *bvar_list = mdd_ret_bvar_list(mgr); |
---|
| 37 | mvar_type a_mv; |
---|
| 38 | int i; |
---|
| 39 | bvar_type bit_i; |
---|
| 40 | mdd_t *temp_A; |
---|
| 41 | |
---|
| 42 | one = mdd_one(mgr); |
---|
| 43 | zero = mdd_zero(mgr); |
---|
| 44 | |
---|
| 45 | a_mv = array_fetch( mvar_type, mvar_list, mvar_id); |
---|
| 46 | |
---|
| 47 | |
---|
| 48 | if ( a_mv.values <= c ) { |
---|
| 49 | mdd_free(zero); |
---|
| 50 | return one; |
---|
| 51 | } |
---|
| 52 | |
---|
| 53 | A = mdd_zero(mgr); |
---|
| 54 | |
---|
| 55 | for(i=1; i <= a_mv.encode_length; i++){ |
---|
| 56 | bit_i = mdd_ret_bvar(&a_mv, (a_mv.encode_length - i), bvar_list); |
---|
| 57 | temp_A = A; |
---|
| 58 | if ( getbit(c,i-1) == 0 ) { |
---|
| 59 | A = mdd_ite(bit_i.node, zero, temp_A, 1, 1, 1); |
---|
| 60 | } |
---|
| 61 | else { |
---|
| 62 | A = mdd_ite(bit_i.node, temp_A, one, 1, 1, 1); |
---|
| 63 | } |
---|
| 64 | bdd_free(temp_A); |
---|
| 65 | } |
---|
| 66 | |
---|
| 67 | mdd_free(one); |
---|
| 68 | mdd_free(zero); |
---|
| 69 | |
---|
| 70 | return A; |
---|
| 71 | */ |
---|
| 72 | |
---|
| 73 | /* Temporary fix until the routines are rewritten taking care of don't cares. */ |
---|
| 74 | |
---|
| 75 | return mdd_lt_c(mgr, mvar_id, c); |
---|
| 76 | } |
---|
| 77 | |
---|
| 78 | |
---|
| 79 | mdd_t * |
---|
| 80 | build_geq_c( |
---|
| 81 | mdd_manager *mgr, |
---|
| 82 | int mvar_id, |
---|
| 83 | int c) |
---|
| 84 | { |
---|
| 85 | /* |
---|
| 86 | mdd_t *A, *one, *zero; |
---|
| 87 | array_t *bvar_list = mdd_ret_bvar_list(mgr), |
---|
| 88 | *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 89 | mvar_type a_mv; |
---|
| 90 | int i; |
---|
| 91 | bvar_type bit_i; |
---|
| 92 | mdd_t *temp_A; |
---|
| 93 | |
---|
| 94 | one = mdd_one(mgr); |
---|
| 95 | zero = mdd_zero(mgr); |
---|
| 96 | |
---|
| 97 | a_mv = array_fetch( mvar_type, mvar_list, mvar_id); |
---|
| 98 | |
---|
| 99 | if ( a_mv.values <= c ) { |
---|
| 100 | mdd_free( one ); |
---|
| 101 | return zero; |
---|
| 102 | } |
---|
| 103 | |
---|
| 104 | |
---|
| 105 | A = mdd_one(mgr); |
---|
| 106 | |
---|
| 107 | for(i=1; i <= a_mv.encode_length; i++){ |
---|
| 108 | bit_i = mdd_ret_bvar(&a_mv, (a_mv.encode_length - i), bvar_list ); |
---|
| 109 | temp_A = A; |
---|
| 110 | if ( getbit(c,i-1) == 0 ) { |
---|
| 111 | A = mdd_ite(bit_i.node, one, temp_A, 1, 1, 1); |
---|
| 112 | } |
---|
| 113 | else { |
---|
| 114 | A = mdd_ite(bit_i.node, temp_A, zero, 1, 1, 1); |
---|
| 115 | } |
---|
| 116 | bdd_free(temp_A); |
---|
| 117 | } |
---|
| 118 | |
---|
| 119 | mdd_free(one); |
---|
| 120 | mdd_free(zero); |
---|
| 121 | |
---|
| 122 | return A; |
---|
| 123 | */ |
---|
| 124 | return mdd_geq_c(mgr, mvar_id, c); |
---|
| 125 | } |
---|
| 126 | |
---|
| 127 | |
---|
| 128 | mdd_t * |
---|
| 129 | build_gt_c( |
---|
| 130 | mdd_manager *mgr, |
---|
| 131 | int mvar_id, |
---|
| 132 | int c) |
---|
| 133 | { |
---|
| 134 | return build_geq_c(mgr, mvar_id, c+1); |
---|
| 135 | } |
---|
| 136 | |
---|
| 137 | /* low <= var <= high */ |
---|
| 138 | mdd_t * |
---|
| 139 | mdd_interval( |
---|
| 140 | mdd_manager *mgr, |
---|
| 141 | int mvar_id, |
---|
| 142 | int low, |
---|
| 143 | int high) |
---|
| 144 | { |
---|
| 145 | mdd_t *HIGH_MDD, *LOW_MDD, *result; |
---|
| 146 | |
---|
| 147 | |
---|
| 148 | LOW_MDD = build_geq_c(mgr,mvar_id,low); |
---|
| 149 | HIGH_MDD = build_leq_c(mgr,mvar_id,high); |
---|
| 150 | |
---|
| 151 | result = mdd_and(HIGH_MDD, LOW_MDD, 1, 1); |
---|
| 152 | |
---|
| 153 | mdd_free(LOW_MDD); |
---|
| 154 | mdd_free(HIGH_MDD); |
---|
| 155 | |
---|
| 156 | return result; |
---|
| 157 | } |
---|
| 158 | |
---|
| 159 | /*---------------------------------------------------------------------------*/ |
---|
| 160 | /* Static function prototypes */ |
---|
| 161 | /*---------------------------------------------------------------------------*/ |
---|
| 162 | |
---|