1 | #include "mdd.h" |
---|
2 | |
---|
3 | /* |
---|
4 | * MDD Package |
---|
5 | * |
---|
6 | * $Id: mdd_andsmoot.c,v 1.12 2002/08/27 00:55:23 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 | mdd_t * |
---|
19 | mdd_and_smooth( |
---|
20 | mdd_manager *mgr, |
---|
21 | mdd_t *f, |
---|
22 | mdd_t *g, |
---|
23 | array_t *mvars) |
---|
24 | { |
---|
25 | int i, j, mv_no; |
---|
26 | mvar_type mv; |
---|
27 | mdd_t *top; |
---|
28 | bdd_t *temp; |
---|
29 | |
---|
30 | array_t *bdd_vars = array_alloc(bdd_t *, 0); |
---|
31 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
32 | |
---|
33 | |
---|
34 | if ( mvars == NIL( array_t ) ) { |
---|
35 | printf("\nWARNING: Empty Array of Smoothing Variables\n"); |
---|
36 | array_free(bdd_vars); |
---|
37 | return ( bdd_and(f, g, 1, 1) ) ; |
---|
38 | } |
---|
39 | else if ( array_n(mvars) == 0) { |
---|
40 | printf("\nWARNING: Empty Array of Smoothing Variables\n"); |
---|
41 | array_free(bdd_vars); |
---|
42 | return ( bdd_and(f, g, 1, 1) ) ; |
---|
43 | } |
---|
44 | |
---|
45 | for (i=0; i<array_n(mvars); i++) { |
---|
46 | mv_no = array_fetch(int, mvars, i); |
---|
47 | mv = array_fetch(mvar_type, mvar_list, mv_no); |
---|
48 | if (mv.status == MDD_BUNDLED) { |
---|
49 | (void) fprintf(stderr, |
---|
50 | "\nmdd_andsmooth: bundled variable %s used\n",mv.name); |
---|
51 | fail(""); |
---|
52 | } |
---|
53 | |
---|
54 | for (j = 0; j < mv.encode_length; j++) { |
---|
55 | temp = bdd_get_variable(mgr, mdd_ret_bvar_id(&mv,j) ); |
---|
56 | array_insert_last(bdd_t *, bdd_vars, temp); |
---|
57 | } |
---|
58 | } |
---|
59 | |
---|
60 | assert( array_n(bdd_vars) != 0 ); |
---|
61 | top = bdd_and_smooth(f, g, bdd_vars); |
---|
62 | |
---|
63 | for (i = 0; i < array_n(bdd_vars); i++) { |
---|
64 | temp = array_fetch(bdd_t *, bdd_vars, i); |
---|
65 | bdd_free(temp); |
---|
66 | } |
---|
67 | array_free(bdd_vars); |
---|
68 | |
---|
69 | return top; |
---|
70 | } |
---|
71 | |
---|
72 | |
---|
73 | mdd_t * |
---|
74 | mdd_and_smooth_with_limit( |
---|
75 | mdd_manager *mgr, |
---|
76 | mdd_t *f, |
---|
77 | mdd_t *g, |
---|
78 | array_t *mvars, |
---|
79 | unsigned int limit) |
---|
80 | { |
---|
81 | int i, j, mv_no; |
---|
82 | mvar_type mv; |
---|
83 | mdd_t *top; |
---|
84 | bdd_t *temp; |
---|
85 | |
---|
86 | array_t *bdd_vars = array_alloc(bdd_t *, 0); |
---|
87 | array_t *mvar_list = mdd_ret_mvar_list(mgr); |
---|
88 | |
---|
89 | |
---|
90 | if ( mvars == NIL( array_t ) ) { |
---|
91 | printf("\nWARNING: Empty Array of Smoothing Variables\n"); |
---|
92 | array_free(bdd_vars); |
---|
93 | return ( bdd_and_with_limit(f, g, 1, 1, limit) ) ; |
---|
94 | } |
---|
95 | else if ( array_n(mvars) == 0) { |
---|
96 | printf("\nWARNING: Empty Array of Smoothing Variables\n"); |
---|
97 | array_free(bdd_vars); |
---|
98 | return ( bdd_and_with_limit(f, g, 1, 1, limit) ) ; |
---|
99 | } |
---|
100 | |
---|
101 | for (i=0; i<array_n(mvars); i++) { |
---|
102 | mv_no = array_fetch(int, mvars, i); |
---|
103 | mv = array_fetch(mvar_type, mvar_list, mv_no); |
---|
104 | if (mv.status == MDD_BUNDLED) { |
---|
105 | (void) fprintf(stderr, |
---|
106 | "\nmdd_andsmooth: bundled variable %s used\n",mv.name); |
---|
107 | fail(""); |
---|
108 | } |
---|
109 | |
---|
110 | for (j = 0; j < mv.encode_length; j++) { |
---|
111 | temp = bdd_get_variable(mgr, mdd_ret_bvar_id(&mv,j) ); |
---|
112 | array_insert_last(bdd_t *, bdd_vars, temp); |
---|
113 | } |
---|
114 | } |
---|
115 | |
---|
116 | assert( array_n(bdd_vars) != 0 ); |
---|
117 | top = bdd_and_smooth_with_limit(f, g, bdd_vars, limit); |
---|
118 | |
---|
119 | for (i = 0; i < array_n(bdd_vars); i++) { |
---|
120 | temp = array_fetch(bdd_t *, bdd_vars, i); |
---|
121 | bdd_free(temp); |
---|
122 | } |
---|
123 | array_free(bdd_vars); |
---|
124 | |
---|
125 | return top; |
---|
126 | } |
---|
127 | |
---|
128 | /*---------------------------------------------------------------------------*/ |
---|
129 | /* Static function prototypes */ |
---|
130 | /*---------------------------------------------------------------------------*/ |
---|
131 | |
---|
132 | |
---|