[13] | 1 | #include "mdd.h" |
---|
| 2 | |
---|
| 3 | /* |
---|
| 4 | * MDD Package |
---|
| 5 | * |
---|
| 6 | * $Id: mdd_case.c,v 1.10 2002/08/24 20:44:27 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 | mdd_t * |
---|
| 19 | mdd_case( |
---|
| 20 | mdd_manager *mgr, |
---|
| 21 | int mvar, |
---|
| 22 | array_t *child_list) |
---|
| 23 | { |
---|
| 24 | mvar_type mv; |
---|
| 25 | mdd_t *mnode; |
---|
| 26 | mdd_t *tmp; |
---|
| 27 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 28 | |
---|
| 29 | mv = array_fetch(mvar_type, mvar_list, mvar); |
---|
| 30 | |
---|
| 31 | if (mv.values != array_n(child_list)) |
---|
| 32 | fail("mdd_case: mvar.values different from length of child_list\n"); |
---|
| 33 | |
---|
| 34 | if (mv.status == MDD_BUNDLED) { |
---|
| 35 | (void) fprintf(stderr, |
---|
| 36 | "\nmdd_andsmooth: bundled variable %s used\n",mv.name); |
---|
| 37 | fail(""); |
---|
| 38 | } |
---|
| 39 | |
---|
| 40 | if (mv.values == 1) { |
---|
| 41 | tmp = array_fetch(mdd_t *, child_list, 0); |
---|
| 42 | mnode = mdd_dup(tmp); |
---|
| 43 | } |
---|
| 44 | else { |
---|
| 45 | mnode = mdd_encode(mgr, child_list, &mv, mv.encode_length-1); |
---|
| 46 | } |
---|
| 47 | return mnode; |
---|
| 48 | } |
---|
| 49 | |
---|
| 50 | |
---|
| 51 | mdd_t * |
---|
| 52 | mdd_encode( |
---|
| 53 | mdd_manager *mgr, |
---|
| 54 | array_t *child_list, |
---|
| 55 | mvar_type *mv_ptr, |
---|
| 56 | int index) |
---|
| 57 | { |
---|
| 58 | array_t *new_child_list; |
---|
| 59 | int i; |
---|
| 60 | int child_count = 0; |
---|
| 61 | int q = array_n(child_list); |
---|
| 62 | bvar_type bv; |
---|
| 63 | mdd_t *f, *g, *h, *t; |
---|
| 64 | mdd_t *one, *zero; |
---|
| 65 | array_t *bvar_list; |
---|
| 66 | |
---|
| 67 | if (q == 1) { |
---|
| 68 | f = array_fetch(mdd_t *, child_list, 0); |
---|
| 69 | h = mdd_dup(f); |
---|
| 70 | if (!mdd_is_tautology(f,1) && !mdd_is_tautology(f,0)) mdd_free(f); |
---|
| 71 | return h; |
---|
| 72 | } |
---|
| 73 | one = mdd_one(mgr); |
---|
| 74 | zero = mdd_zero(mgr); |
---|
| 75 | bvar_list = mdd_ret_bvar_list(mgr); |
---|
| 76 | |
---|
| 77 | new_child_list = array_alloc(mdd_t *, 0); |
---|
| 78 | |
---|
| 79 | bv = mdd_ret_bvar(mv_ptr, index, bvar_list); |
---|
| 80 | |
---|
| 81 | for (i=0; i<(q/2); i++) { |
---|
| 82 | |
---|
| 83 | f = mdd_dup(bv.node); |
---|
| 84 | h = array_fetch(mdd_t *, child_list, child_count++); |
---|
| 85 | g = array_fetch(mdd_t *, child_list, child_count++); |
---|
| 86 | #if USE_ITE |
---|
| 87 | #if BYPASS |
---|
| 88 | /* bypasses cases */ |
---|
| 89 | /* 1 = ite(F,1,1) */ |
---|
| 90 | /* 0 = ite(F,0,0) */ |
---|
| 91 | /* F = ite(F,1,0) */ |
---|
| 92 | /* !F = ite(F,0,1) */ |
---|
| 93 | /* G = ite(F,G,G) */ |
---|
| 94 | if (mdd_is_tautology(g,0) && mdd_is_tautology(h,0)) { |
---|
| 95 | array_insert_last(mdd_t *, new_child_list, zero); |
---|
| 96 | } |
---|
| 97 | else if (mdd_is_tautology(g,0) && mdd_is_tautology(h,1)) { |
---|
| 98 | t = mdd_not(f); |
---|
| 99 | array_insert_last(mdd_t *, new_child_list, t); |
---|
| 100 | } |
---|
| 101 | else if (mdd_is_tautology(g,1) && mdd_is_tautology(h,1)) { |
---|
| 102 | array_insert_last(mdd_t *, new_child_list, one); |
---|
| 103 | } |
---|
| 104 | else if (mdd_is_tautology(g,1) && mdd_is_tautology(h,0)) { |
---|
| 105 | t = mdd_dup(f); |
---|
| 106 | array_insert_last(mdd_t *, new_child_list, t); |
---|
| 107 | } |
---|
| 108 | else if (mdd_equal(f,g)) { |
---|
| 109 | t = mdd_dup(f); |
---|
| 110 | array_insert_last(mdd_t *, new_child_list, t); |
---|
| 111 | } |
---|
| 112 | else { |
---|
| 113 | t = mdd_ite(f, g, h, 1, 1, 1); |
---|
| 114 | array_insert_last(mdd_t *, new_child_list, t); |
---|
| 115 | } |
---|
| 116 | if (!mdd_is_tautology(g,1) && !mdd_is_tautology(g,0)) mdd_free(g); |
---|
| 117 | if (!mdd_is_tautology(h,1) && !mdd_is_tautology(h,0)) mdd_free(h); |
---|
| 118 | #else |
---|
| 119 | t = mdd_ite(f, g, h, 1, 1, 1); |
---|
| 120 | if (!mdd_is_tautology(g,1) && !mdd_is_tautology(g,0)) mdd_free(g); |
---|
| 121 | if (!mdd_is_tautology(h,1) && !mdd_is_tautology(h,0)) mdd_free(h); |
---|
| 122 | array_insert_last(mdd_t *, new_child_list, t); |
---|
| 123 | #endif |
---|
| 124 | #else |
---|
| 125 | a1 = mdd_and(f,g,1,1); |
---|
| 126 | if (!mdd_is_tautology(g,1) && !mdd_is_tautology(g,0)) mdd_free(g); |
---|
| 127 | a2 = mdd_and(f,h,0,1); |
---|
| 128 | if (!mdd_is_tautology(h,1) && !mdd_is_tautology(h,0)) mdd_free(h); |
---|
| 129 | t = mdd_or(a1,a2,1,1); |
---|
| 130 | /* t = mdd_or(mdd_and(f,g,1,1), mdd_and(f,h,0,1), 1, 1); */ |
---|
| 131 | if (!mdd_is_tautology(a1,1) && !mdd_is_tautology(a1,0)) mdd_free(a1); |
---|
| 132 | if (!mdd_is_tautology(a2,1) && !mdd_is_tautology(a2,0)) mdd_free(a2); |
---|
| 133 | array_insert_last(mdd_t *, new_child_list, t); |
---|
| 134 | #endif |
---|
| 135 | |
---|
| 136 | mdd_free(f); |
---|
| 137 | } |
---|
| 138 | |
---|
| 139 | if (q & 1) { /* if q is odd */ |
---|
| 140 | t = array_fetch(mdd_t *, child_list, child_count); |
---|
| 141 | array_insert_last(mdd_t *, new_child_list, t); |
---|
| 142 | } |
---|
| 143 | f = mdd_encode(mgr, new_child_list, mv_ptr, index - 1); |
---|
| 144 | array_free(new_child_list); |
---|
| 145 | mdd_free(one); |
---|
| 146 | mdd_free(zero); |
---|
| 147 | return f; |
---|
| 148 | } |
---|
| 149 | |
---|
| 150 | |
---|
| 151 | /*---------------------------------------------------------------------------*/ |
---|
| 152 | /* Static function prototypes */ |
---|
| 153 | /*---------------------------------------------------------------------------*/ |
---|
| 154 | |
---|
| 155 | |
---|