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 | |
---|