[13] | 1 | /* |
---|
| 2 | * MDD Package |
---|
| 3 | * |
---|
| 4 | * $Id: mdd_dot.c,v 1.8 2009/01/30 03:38:54 fabio Exp $ |
---|
| 5 | * |
---|
| 6 | * Functions to convert mdds to graphviz's dot format for graphic display. |
---|
| 7 | * These functions are effectively no-ops unless the BDD package supports |
---|
| 8 | * the conversion of BDDs to the dot format. |
---|
| 9 | * |
---|
| 10 | * Author: Fabio Somenzi |
---|
| 11 | |
---|
| 12 | Copyright (c) 2009, Regents of the University of Colorado |
---|
| 13 | |
---|
| 14 | All rights reserved. |
---|
| 15 | |
---|
| 16 | Redistribution and use in source and binary forms, with or without |
---|
| 17 | modification, are permitted provided that the following conditions |
---|
| 18 | are met: |
---|
| 19 | |
---|
| 20 | Redistributions of source code must retain the above copyright |
---|
| 21 | notice, this list of conditions and the following disclaimer. |
---|
| 22 | |
---|
| 23 | Redistributions in binary form must reproduce the above copyright |
---|
| 24 | notice, this list of conditions and the following disclaimer in the |
---|
| 25 | documentation and/or other materials provided with the distribution. |
---|
| 26 | |
---|
| 27 | Neither the name of the University of Colorado nor the names of its |
---|
| 28 | contributors may be used to endorse or promote products derived from |
---|
| 29 | this software without specific prior written permission. |
---|
| 30 | |
---|
| 31 | THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS |
---|
| 32 | "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT |
---|
| 33 | LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS |
---|
| 34 | FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE |
---|
| 35 | COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, |
---|
| 36 | INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, |
---|
| 37 | BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; |
---|
| 38 | LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER |
---|
| 39 | CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT |
---|
| 40 | LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN |
---|
| 41 | ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE |
---|
| 42 | POSSIBILITY OF SUCH DAMAGE. |
---|
| 43 | |
---|
| 44 | * |
---|
| 45 | */ |
---|
| 46 | |
---|
| 47 | #include "mdd.h" |
---|
| 48 | |
---|
| 49 | /* Convert an array of mdds to dot format. |
---|
| 50 | * If name is the NULL pointer, "" is used. |
---|
| 51 | * If fp is the NULL pointer, stdout is used. |
---|
| 52 | */ |
---|
| 53 | void |
---|
| 54 | mdd_array_dump_dot( |
---|
| 55 | array_t *mdds /* of mdd_t *, mdds to be converted */, |
---|
| 56 | char *name /* for output names */, |
---|
| 57 | FILE *fp /* output file */ |
---|
| 58 | ) |
---|
| 59 | { |
---|
| 60 | mdd_manager *mgr; |
---|
| 61 | array_t *mvar_list; |
---|
| 62 | int i, n_mvar, k; |
---|
| 63 | int n_outputs = array_n(mdds); |
---|
| 64 | int n_inputs = 0; |
---|
| 65 | bdd_node **outputs = NULL; |
---|
| 66 | char **onames = NULL; |
---|
| 67 | char **inames = NULL; |
---|
| 68 | |
---|
| 69 | if (mdds == NIL(array_t) || n_outputs == 0) return; |
---|
| 70 | |
---|
| 71 | mgr = mdd_get_manager(array_fetch(mdd_t *, mdds, 0)); |
---|
| 72 | n_inputs = bdd_num_vars(mgr); |
---|
| 73 | mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 74 | n_mvar = array_n(mvar_list); |
---|
| 75 | /* Collect output nodes and names. */ |
---|
| 76 | outputs = ALLOC(bdd_node *, n_outputs); |
---|
| 77 | onames = ALLOC(char *, n_outputs); |
---|
| 78 | if (n_outputs == 1) { |
---|
| 79 | outputs[0] = array_fetch(mdd_t *, mdds, 0); |
---|
| 80 | onames[0] = strdup(name == NIL(char) ? "" : name); |
---|
| 81 | } else { |
---|
| 82 | for (i = 0; i < n_outputs; i++) { |
---|
| 83 | mdd_t *mdd = array_fetch(mdd_t *, mdds, i); |
---|
| 84 | outputs[i] = bdd_extract_node_as_is(mdd); |
---|
| 85 | if (name == NIL(char)) { |
---|
| 86 | onames[i] = ALLOC(char, integer_get_num_of_digits(i) + 1); |
---|
| 87 | sprintf(onames[i], "%d", i); |
---|
| 88 | } else { |
---|
| 89 | onames[i] = ALLOC(char, strlen(name) + |
---|
| 90 | integer_get_num_of_digits(i) + 2); |
---|
| 91 | sprintf(onames[i], "%s %d", name, i); |
---|
| 92 | } |
---|
| 93 | } |
---|
| 94 | } |
---|
| 95 | inames = ALLOC(char *, n_inputs); |
---|
| 96 | /* Set BDD variable names. */ |
---|
| 97 | k = 0; |
---|
| 98 | for (i = 0; i < n_mvar; i++) { |
---|
| 99 | int j; |
---|
| 100 | mvar_type mv = array_fetch(mvar_type, mvar_list, i); |
---|
| 101 | if (mv.encode_length == 1) { |
---|
| 102 | inames[k] = strdup(mv.name); |
---|
| 103 | k++; |
---|
| 104 | } else { |
---|
| 105 | for (j = 0; j < mv.encode_length; j++, k++) { |
---|
| 106 | inames[k] = ALLOC(char, strlen(mv.name) + |
---|
| 107 | integer_get_num_of_digits(j) + 2); |
---|
| 108 | sprintf(inames[k], "%s %d", mv.name, j); |
---|
| 109 | } |
---|
| 110 | } |
---|
| 111 | } |
---|
| 112 | /* Get the job done. */ |
---|
| 113 | bdd_dump_dot(mgr, n_outputs, outputs, inames, onames, |
---|
| 114 | fp == NIL(FILE) ? stdout: fp); |
---|
| 115 | /* Clean up */ |
---|
| 116 | FREE(outputs); |
---|
| 117 | for (i = 0; i < n_outputs; i++) { |
---|
| 118 | FREE(onames[i]); |
---|
| 119 | } |
---|
| 120 | FREE(onames); |
---|
| 121 | for (i = 0; i < n_inputs; i++) { |
---|
| 122 | FREE(inames[i]); |
---|
| 123 | } |
---|
| 124 | FREE(inames); |
---|
| 125 | |
---|
| 126 | } /* mdd_array_dump_dot */ |
---|
| 127 | |
---|
| 128 | |
---|
| 129 | /* Convert one mdd to dot format. */ |
---|
| 130 | void |
---|
| 131 | mdd_dump_dot( |
---|
| 132 | mdd_t *mdd /* mdd to be converted */, |
---|
| 133 | char *name /* for output names */, |
---|
| 134 | FILE *fp /* output file */ |
---|
| 135 | ) |
---|
| 136 | { |
---|
| 137 | array_t *arr = array_alloc(mdd_t *, 1); |
---|
| 138 | |
---|
| 139 | array_insert_last(mdd_t *, arr, mdd); |
---|
| 140 | mdd_array_dump_dot(arr, name, fp); |
---|
| 141 | array_free(arr); |
---|
| 142 | |
---|
| 143 | } /* mdd_dump_dot */ |
---|
| 144 | |
---|
| 145 | |
---|
| 146 | /* Print covers of an array of mdds. |
---|
| 147 | * If name is the NULL pointer, "" is used. |
---|
| 148 | */ |
---|
| 149 | void |
---|
| 150 | mdd_array_print_cover( |
---|
| 151 | array_t *mdds /* of mdd_t *, mdds to be printed */, |
---|
| 152 | char *name /* output name */, |
---|
| 153 | boolean disjoint /* print disjoint covers */ |
---|
| 154 | ) |
---|
| 155 | { |
---|
| 156 | mdd_manager *mgr; |
---|
| 157 | mdd_t *f; |
---|
| 158 | array_t *mvar_list; |
---|
| 159 | int i, n_mvar, n_bvar; |
---|
| 160 | int n_inputs = 0; |
---|
| 161 | char **inames = NULL; |
---|
| 162 | int height; |
---|
| 163 | |
---|
| 164 | if (mdds == NIL(array_t) || array_n(mdds) == 0) return; |
---|
| 165 | |
---|
| 166 | mgr = mdd_get_manager(array_fetch(mdd_t *, mdds, 0)); |
---|
| 167 | n_inputs = bdd_num_vars(mgr); |
---|
| 168 | mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 169 | n_mvar = array_n(mvar_list); |
---|
| 170 | n_bvar = array_n(mdd_ret_bvar_list(mgr)); |
---|
| 171 | height = name == NIL(char) ? 0 : strlen(name); |
---|
| 172 | inames = ALLOC(char *, n_inputs); |
---|
| 173 | for (i = 0; i < n_inputs; i++) inames[i] = NIL(char); |
---|
| 174 | /* Set BDD variable names. */ |
---|
| 175 | for (i = 0; i < n_mvar; i++) { |
---|
| 176 | mvar_type mv = array_fetch(mvar_type, mvar_list, i); |
---|
| 177 | if (mv.encode_length == 1) { |
---|
| 178 | int k = array_fetch(int, mv.bvars, 0); |
---|
| 179 | inames[k] = strdup(mv.name); |
---|
| 180 | height = MAX(height,strlen(inames[k])); |
---|
| 181 | } else { |
---|
| 182 | int j; |
---|
| 183 | for (j = 0; j < mv.encode_length; j++) { |
---|
| 184 | int k = array_fetch(int, mv.bvars, j); |
---|
| 185 | inames[k] = ALLOC(char, strlen(mv.name) + |
---|
| 186 | integer_get_num_of_digits(j) + 2); |
---|
| 187 | sprintf(inames[k], "%s %d", mv.name, j); |
---|
| 188 | height = MAX(height,strlen(inames[k])); |
---|
| 189 | } |
---|
| 190 | } |
---|
| 191 | } |
---|
| 192 | |
---|
| 193 | /* First print header and then BDDs. */ |
---|
| 194 | for (i = 0; i < height; i++) { |
---|
| 195 | int j; |
---|
| 196 | for (j = 0; j < n_inputs; j++) { |
---|
| 197 | if (inames[j] == NIL(char) || i >= strlen(inames[j])) { |
---|
| 198 | printf(" "); |
---|
| 199 | } else { |
---|
| 200 | printf("%c", inames[j][i]); |
---|
| 201 | } |
---|
| 202 | } |
---|
| 203 | if (disjoint) printf(" "); |
---|
| 204 | printf(" %c\n", name == NIL(char) || i >= strlen(name) ? ' ' : name[i]); |
---|
| 205 | } |
---|
| 206 | printf("\n"); |
---|
| 207 | arrayForEachItem(mdd_t *, mdds, i, f) { |
---|
| 208 | if (disjoint) { |
---|
| 209 | bdd_print_minterm(f); |
---|
| 210 | printf("\n"); |
---|
| 211 | } else { |
---|
| 212 | bdd_print_cover(f); |
---|
| 213 | } |
---|
| 214 | } |
---|
| 215 | /* Clean up. */ |
---|
| 216 | for (i = 0; i < n_inputs; i++) { |
---|
| 217 | if (inames[i] != NIL(char)) FREE(inames[i]); |
---|
| 218 | } |
---|
| 219 | FREE(inames); |
---|
| 220 | |
---|
| 221 | } /* mdd_array_print_cover */ |
---|
| 222 | |
---|
| 223 | |
---|
| 224 | /* Print a cover of an mdd. |
---|
| 225 | * If name is the NULL pointer, "" is used. |
---|
| 226 | */ |
---|
| 227 | void |
---|
| 228 | mdd_print_cover( |
---|
| 229 | mdd_t *f /* mdd to be printed */, |
---|
| 230 | char *name /* output name */, |
---|
| 231 | boolean disjoint /* print disjoint cover */ |
---|
| 232 | ) |
---|
| 233 | { |
---|
| 234 | array_t *arr = array_alloc(mdd_t *, 1); |
---|
| 235 | |
---|
| 236 | array_insert_last(mdd_t *, arr, f); |
---|
| 237 | mdd_array_print_cover(arr, name, disjoint); |
---|
| 238 | array_free(arr); |
---|
| 239 | |
---|
| 240 | } /* mdd_array_print_cover */ |
---|