[13] | 1 | #include "mdd.h" |
---|
| 2 | |
---|
| 3 | /* |
---|
| 4 | * MDD Package |
---|
| 5 | * |
---|
| 6 | * $Id: mdd_search.c,v 1.10 2002/08/27 16:30:26 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 | static void |
---|
| 19 | mdd_pr_cubes(mdd_manager *mgr) |
---|
| 20 | { |
---|
| 21 | int i, j; |
---|
| 22 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 23 | mvar_type mv; |
---|
| 24 | |
---|
| 25 | for (i=0; i<array_n(mvar_list); i++) { |
---|
| 26 | mv = array_fetch(mvar_type, mvar_list, i); |
---|
| 27 | (void) printf("\n%s = ", mv.name); |
---|
| 28 | for (j=0; j<mv.encode_length; j++) |
---|
| 29 | (void) printf("%d",mv.encoding[j]); |
---|
| 30 | } |
---|
| 31 | (void) printf("\n"); |
---|
| 32 | } |
---|
| 33 | |
---|
| 34 | static void |
---|
| 35 | mdd_pr_minterms(mdd_manager *mgr) |
---|
| 36 | { |
---|
| 37 | /* not implemented yet */ |
---|
| 38 | |
---|
| 39 | int i, j; |
---|
| 40 | mvar_type mv; |
---|
| 41 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 42 | |
---|
| 43 | for (i=0; i<array_n(mvar_list); i++) { |
---|
| 44 | mv = array_fetch(mvar_type, mvar_list, i); |
---|
| 45 | (void) printf("\n%s = ", mv.name); |
---|
| 46 | for (j=0; j<mv.encode_length; j++) |
---|
| 47 | (void) printf("%d",mv.encoding[j]); |
---|
| 48 | } |
---|
| 49 | (void) printf("\n"); |
---|
| 50 | } |
---|
| 51 | |
---|
| 52 | void |
---|
| 53 | mdd_search( |
---|
| 54 | mdd_manager *mgr, |
---|
| 55 | bdd_t *top, |
---|
| 56 | int phase, |
---|
| 57 | boolean minterms) |
---|
| 58 | { |
---|
| 59 | int is_complemented; |
---|
| 60 | bdd_t *child, *top_uncomp; |
---|
| 61 | |
---|
| 62 | if (mdd_is_tautology(top,1)) { |
---|
| 63 | if (phase == 1) { |
---|
| 64 | if (minterms == 1) mdd_pr_minterms(mgr); |
---|
| 65 | else mdd_pr_cubes(mgr); |
---|
| 66 | } |
---|
| 67 | return; |
---|
| 68 | } |
---|
| 69 | if (mdd_is_tautology(top,0)) { |
---|
| 70 | if (phase == 0) { |
---|
| 71 | if (minterms == 1) mdd_pr_minterms(mgr); |
---|
| 72 | else mdd_pr_cubes(mgr); |
---|
| 73 | } |
---|
| 74 | return; |
---|
| 75 | } |
---|
| 76 | |
---|
| 77 | (void)bdd_get_node(top,&is_complemented); |
---|
| 78 | |
---|
| 79 | if (is_complemented != 0) { |
---|
| 80 | phase = toggle(phase); |
---|
| 81 | } |
---|
| 82 | |
---|
| 83 | (void) mdd_mark(mgr, top, 1); |
---|
| 84 | |
---|
| 85 | if (is_complemented) top_uncomp = bdd_not(top); |
---|
| 86 | else top_uncomp = mdd_dup(top); |
---|
| 87 | |
---|
| 88 | child = bdd_then(top_uncomp); |
---|
| 89 | mdd_search(mgr, child, phase, minterms); |
---|
| 90 | mdd_free(child); |
---|
| 91 | |
---|
| 92 | |
---|
| 93 | child = bdd_else(top_uncomp); |
---|
| 94 | (void) mdd_mark(mgr, top, 0); |
---|
| 95 | mdd_search(mgr, child, phase, minterms); |
---|
| 96 | mdd_unmark(mgr, top); |
---|
| 97 | |
---|
| 98 | mdd_free(top_uncomp); |
---|
| 99 | mdd_free(child); |
---|
| 100 | return; |
---|
| 101 | } |
---|
| 102 | |
---|
| 103 | /*---------------------------------------------------------------------------*/ |
---|
| 104 | /* Static function prototypes */ |
---|
| 105 | /*---------------------------------------------------------------------------*/ |
---|
| 106 | |
---|
| 107 | |
---|