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