[13] | 1 | #include "mdd.h" |
---|
| 2 | |
---|
| 3 | /* |
---|
| 4 | * MDD Package |
---|
| 5 | * |
---|
| 6 | * $Id: mdd_support.c,v 1.12 2002/08/24 21:48:15 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 | array_t * |
---|
| 19 | mdd_get_support(mdd_manager *mdd_mgr, mdd_t *f) |
---|
| 20 | { |
---|
| 21 | array_t *full_list, *support_list; |
---|
| 22 | array_t *mvar_list = mdd_ret_mvar_list(mdd_mgr); |
---|
| 23 | array_t *bvar_list = mdd_ret_bvar_list(mdd_mgr); |
---|
| 24 | var_set_t *vset; |
---|
| 25 | int i, list_length; |
---|
| 26 | bvar_type bv; |
---|
| 27 | boolean present; |
---|
| 28 | |
---|
| 29 | |
---|
| 30 | /* initialize full list of mvar id's */ |
---|
| 31 | list_length = array_n(mvar_list); |
---|
| 32 | full_list = array_alloc(boolean, list_length); |
---|
| 33 | for (i = 0; i < array_n(mvar_list); i++) { |
---|
| 34 | array_insert(boolean, full_list, i, 0); |
---|
| 35 | } |
---|
| 36 | |
---|
| 37 | vset = bdd_get_support(f); |
---|
| 38 | for (i = 0; i < array_n(bvar_list); i++) { |
---|
| 39 | if (var_set_get_elt(vset, i) == 1) { |
---|
| 40 | bv = array_fetch(bvar_type, bvar_list, i); |
---|
| 41 | (void) array_insert(boolean, full_list, bv.mvar_id, 1); |
---|
| 42 | } |
---|
| 43 | } |
---|
| 44 | |
---|
| 45 | support_list = array_alloc(int, 0); |
---|
| 46 | for (i = 0; i < array_n(mvar_list); i++) { |
---|
| 47 | present = array_fetch(boolean, full_list, i); |
---|
| 48 | if (present) array_insert_last(int, support_list, i); |
---|
| 49 | } |
---|
| 50 | |
---|
| 51 | (void) array_free(full_list); |
---|
| 52 | (void) var_set_free(vset); |
---|
| 53 | |
---|
| 54 | return support_list; |
---|
| 55 | } |
---|
| 56 | |
---|
| 57 | array_t * |
---|
| 58 | mdd_get_bdd_support_ids(mdd_manager *mdd_mgr, mdd_t *f) |
---|
| 59 | { |
---|
| 60 | array_t *bdd_support_list; |
---|
| 61 | array_t *bvar_list = mdd_ret_bvar_list(mdd_mgr); |
---|
| 62 | var_set_t *vset; |
---|
| 63 | int i; |
---|
| 64 | |
---|
| 65 | bdd_support_list = array_alloc(int, 0); |
---|
| 66 | |
---|
| 67 | vset = bdd_get_support(f); |
---|
| 68 | for (i = 0; i < array_n(bvar_list); i++) { |
---|
| 69 | if (var_set_get_elt(vset, i) == 1) { |
---|
| 70 | array_insert_last(int, bdd_support_list, i); |
---|
| 71 | } |
---|
| 72 | } |
---|
| 73 | |
---|
| 74 | (void) var_set_free(vset); |
---|
| 75 | return bdd_support_list; |
---|
| 76 | } |
---|
| 77 | |
---|
| 78 | array_t * |
---|
| 79 | mdd_get_bdd_support_vars(mdd_manager *mdd_mgr, mdd_t *f) |
---|
| 80 | { |
---|
| 81 | array_t *bdd_support_list; |
---|
| 82 | array_t *bvar_list = mdd_ret_bvar_list(mdd_mgr); |
---|
| 83 | var_set_t *vset; |
---|
| 84 | mdd_t *var; |
---|
| 85 | int i; |
---|
| 86 | |
---|
| 87 | bdd_support_list = array_alloc(mdd_t *, 0); |
---|
| 88 | |
---|
| 89 | vset = bdd_get_support(f); |
---|
| 90 | for (i = 0; i < array_n(bvar_list); i++) { |
---|
| 91 | if (var_set_get_elt(vset, i) == 1) { |
---|
| 92 | var = bdd_var_with_index(mdd_mgr, i); |
---|
| 93 | array_insert_last(mdd_t *, bdd_support_list, var); |
---|
| 94 | } |
---|
| 95 | } |
---|
| 96 | |
---|
| 97 | (void) var_set_free(vset); |
---|
| 98 | return bdd_support_list; |
---|
| 99 | } |
---|
| 100 | |
---|
| 101 | /*---------------------------------------------------------------------------*/ |
---|
| 102 | /* Static function prototypes */ |
---|
| 103 | /*---------------------------------------------------------------------------*/ |
---|
| 104 | |
---|