[8] | 1 | #include "mdd.h" |
---|
| 2 | |
---|
| 3 | /* |
---|
| 4 | * MDD Package |
---|
| 5 | * |
---|
| 6 | * $Id: mdd_cofactor.c,v 1.9 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_traverse( |
---|
| 20 | mdd_manager *mgr, |
---|
| 21 | bdd_t *top, |
---|
| 22 | boolean *mvar_present) |
---|
| 23 | { |
---|
| 24 | bvar_type bv; |
---|
| 25 | array_t *bvar_list = mdd_ret_bvar_list(mgr); |
---|
| 26 | int is_complemented; |
---|
| 27 | bdd_t *uncomp_top, *child, *temp_child; |
---|
| 28 | |
---|
| 29 | if (bdd_is_tautology(top,1)) { |
---|
| 30 | return; |
---|
| 31 | } |
---|
| 32 | if (bdd_is_tautology(top,0)) { |
---|
| 33 | return; |
---|
| 34 | } |
---|
| 35 | |
---|
| 36 | (void)bdd_get_node(top,&is_complemented); |
---|
| 37 | |
---|
| 38 | bv = array_fetch(bvar_type, bvar_list, bdd_top_var_id(top)); |
---|
| 39 | mvar_present[bv.mvar_id] = 1; |
---|
| 40 | |
---|
| 41 | if (is_complemented) uncomp_top = bdd_not(top); |
---|
| 42 | else uncomp_top = mdd_dup(top); |
---|
| 43 | |
---|
| 44 | child = bdd_then(uncomp_top); |
---|
| 45 | (void) bdd_get_node(child,&is_complemented); |
---|
| 46 | if (is_complemented) { |
---|
| 47 | temp_child = child; |
---|
| 48 | child = bdd_not(temp_child); |
---|
| 49 | mdd_free(temp_child); |
---|
| 50 | } |
---|
| 51 | |
---|
| 52 | mdd_traverse(mgr, child , mvar_present); |
---|
| 53 | mdd_free(child); |
---|
| 54 | |
---|
| 55 | child = bdd_else(uncomp_top); |
---|
| 56 | (void) bdd_get_node(child,&is_complemented); |
---|
| 57 | if (is_complemented) { |
---|
| 58 | temp_child = child; |
---|
| 59 | child = bdd_not(temp_child); |
---|
| 60 | mdd_free(temp_child); |
---|
| 61 | } |
---|
| 62 | |
---|
| 63 | mdd_traverse(mgr, child, mvar_present); |
---|
| 64 | |
---|
| 65 | |
---|
| 66 | mdd_free(child); |
---|
| 67 | mdd_free(uncomp_top); |
---|
| 68 | return; |
---|
| 69 | } |
---|
| 70 | |
---|
| 71 | |
---|
| 72 | static array_t * |
---|
| 73 | mvars_extract( |
---|
| 74 | mdd_manager *mgr, |
---|
| 75 | mdd_t *fn) |
---|
| 76 | { |
---|
| 77 | int i, no_mvar; |
---|
| 78 | boolean *mvar_present; |
---|
| 79 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
| 80 | array_t *mvars; |
---|
| 81 | |
---|
| 82 | |
---|
| 83 | mvars = array_alloc(int, 0); |
---|
| 84 | no_mvar = array_n(mvar_list); |
---|
| 85 | mvar_present = ALLOC(boolean, no_mvar); |
---|
| 86 | for (i=0; i<no_mvar; i++) mvar_present[i] = 0; |
---|
| 87 | mdd_traverse(mgr, fn, mvar_present); |
---|
| 88 | for (i=0; i<no_mvar; i++) |
---|
| 89 | if (mvar_present[i] == 1) array_insert_last(int, mvars, i); |
---|
| 90 | FREE(mvar_present); |
---|
| 91 | return mvars; |
---|
| 92 | } |
---|
| 93 | |
---|
| 94 | mdd_t * |
---|
| 95 | mdd_cofactor( |
---|
| 96 | mdd_manager *mgr, |
---|
| 97 | mdd_t *fn, |
---|
| 98 | mdd_t *cube) |
---|
| 99 | { |
---|
| 100 | array_t *mvars; |
---|
| 101 | mdd_t *top; |
---|
| 102 | |
---|
| 103 | mvars = mvars_extract(mgr, cube); |
---|
| 104 | top = mdd_and_smooth(mgr, fn, cube, mvars); |
---|
| 105 | array_free(mvars); |
---|
| 106 | return top; |
---|
| 107 | } |
---|
| 108 | |
---|
| 109 | |
---|
| 110 | |
---|
| 111 | /*---------------------------------------------------------------------------*/ |
---|
| 112 | /* Static function prototypes */ |
---|
| 113 | /*---------------------------------------------------------------------------*/ |
---|
| 114 | |
---|
| 115 | |
---|