1 /**CFile***********************************************************************
2
3 FileName [cuddLiteral.c]
4
5 PackageName [cudd]
6
7 Synopsis [Functions for manipulation of literal sets represented by
8 BDDs.]
9
10 Description [External procedures included in this file:
11 <ul>
12 <li> Cudd_bddLiteralSetIntersection()
13 </ul>
14 Internal procedures included in this file:
15 <ul>
16 <li> cuddBddLiteralSetIntersectionRecur()
17 </ul>]
18
19 Author [Fabio Somenzi]
20
21 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
22
23 All rights reserved.
24
25 Redistribution and use in source and binary forms, with or without
26 modification, are permitted provided that the following conditions
27 are met:
28
29 Redistributions of source code must retain the above copyright
30 notice, this list of conditions and the following disclaimer.
31
32 Redistributions in binary form must reproduce the above copyright
33 notice, this list of conditions and the following disclaimer in the
34 documentation and/or other materials provided with the distribution.
35
36 Neither the name of the University of Colorado nor the names of its
37 contributors may be used to endorse or promote products derived from
38 this software without specific prior written permission.
39
40 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
41 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
42 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
43 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
44 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
45 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
46 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
47 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
48 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
49 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
50 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
51 POSSIBILITY OF SUCH DAMAGE.]
52
53 ******************************************************************************/
54
55 #include "misc/util/util_hack.h"
56 #include "cuddInt.h"
57
58 ABC_NAMESPACE_IMPL_START
59
60
61
62
63 /*---------------------------------------------------------------------------*/
64 /* Constant declarations */
65 /*---------------------------------------------------------------------------*/
66
67 /*---------------------------------------------------------------------------*/
68 /* Stucture declarations */
69 /*---------------------------------------------------------------------------*/
70
71 /*---------------------------------------------------------------------------*/
72 /* Type declarations */
73 /*---------------------------------------------------------------------------*/
74
75 /*---------------------------------------------------------------------------*/
76 /* Variable declarations */
77 /*---------------------------------------------------------------------------*/
78
79 #ifndef lint
80 static char rcsid[] DD_UNUSED = "$Id: cuddLiteral.c,v 1.8 2004/08/13 18:04:50 fabio Exp $";
81 #endif
82
83 /*---------------------------------------------------------------------------*/
84 /* Macro declarations */
85 /*---------------------------------------------------------------------------*/
86
87 /**AutomaticStart*************************************************************/
88
89 /*---------------------------------------------------------------------------*/
90 /* Static function prototypes */
91 /*---------------------------------------------------------------------------*/
92
93
94 /**AutomaticEnd***************************************************************/
95
96
97 /*---------------------------------------------------------------------------*/
98 /* Definition of exported functions */
99 /*---------------------------------------------------------------------------*/
100
101
102 /**Function********************************************************************
103
104 Synopsis [Computes the intesection of two sets of literals
105 represented as BDDs.]
106
107 Description [Computes the intesection of two sets of literals
108 represented as BDDs. Each set is represented as a cube of the
109 literals in the set. The empty set is represented by the constant 1.
110 No variable can be simultaneously present in both phases in a set.
111 Returns a pointer to the BDD representing the intersected sets, if
112 successful; NULL otherwise.]
113
114 SideEffects [None]
115
116 ******************************************************************************/
117 DdNode *
Cudd_bddLiteralSetIntersection(DdManager * dd,DdNode * f,DdNode * g)118 Cudd_bddLiteralSetIntersection(
119 DdManager * dd,
120 DdNode * f,
121 DdNode * g)
122 {
123 DdNode *res;
124
125 do {
126 dd->reordered = 0;
127 res = cuddBddLiteralSetIntersectionRecur(dd,f,g);
128 } while (dd->reordered == 1);
129 return(res);
130
131 } /* end of Cudd_bddLiteralSetIntersection */
132
133
134 /*---------------------------------------------------------------------------*/
135 /* Definition of internal functions */
136 /*---------------------------------------------------------------------------*/
137
138
139 /**Function********************************************************************
140
141 Synopsis [Performs the recursive step of
142 Cudd_bddLiteralSetIntersection.]
143
144 Description [Performs the recursive step of
145 Cudd_bddLiteralSetIntersection. Scans the cubes for common variables,
146 and checks whether they agree in phase. Returns a pointer to the
147 resulting cube if successful; NULL otherwise.]
148
149 SideEffects [None]
150
151 ******************************************************************************/
152 DdNode *
cuddBddLiteralSetIntersectionRecur(DdManager * dd,DdNode * f,DdNode * g)153 cuddBddLiteralSetIntersectionRecur(
154 DdManager * dd,
155 DdNode * f,
156 DdNode * g)
157 {
158 DdNode *res, *tmp;
159 DdNode *F, *G;
160 DdNode *fc, *gc;
161 DdNode *one;
162 DdNode *zero;
163 unsigned int topf, topg, comple;
164 int phasef, phaseg;
165
166 statLine(dd);
167 if (f == g) return(f);
168
169 F = Cudd_Regular(f);
170 G = Cudd_Regular(g);
171 one = DD_ONE(dd);
172
173 /* Here f != g. If F == G, then f and g are complementary.
174 ** Since they are two cubes, this case only occurs when f == v,
175 ** g == v', and v is a variable or its complement.
176 */
177 if (F == G) return(one);
178
179 zero = Cudd_Not(one);
180 topf = cuddI(dd,F->index);
181 topg = cuddI(dd,G->index);
182 /* Look for a variable common to both cubes. If there are none, this
183 ** loop will stop when the constant node is reached in both cubes.
184 */
185 while (topf != topg) {
186 if (topf < topg) { /* move down on f */
187 comple = f != F;
188 f = cuddT(F);
189 if (comple) f = Cudd_Not(f);
190 if (f == zero) {
191 f = cuddE(F);
192 if (comple) f = Cudd_Not(f);
193 }
194 F = Cudd_Regular(f);
195 topf = cuddI(dd,F->index);
196 } else if (topg < topf) {
197 comple = g != G;
198 g = cuddT(G);
199 if (comple) g = Cudd_Not(g);
200 if (g == zero) {
201 g = cuddE(G);
202 if (comple) g = Cudd_Not(g);
203 }
204 G = Cudd_Regular(g);
205 topg = cuddI(dd,G->index);
206 }
207 }
208
209 /* At this point, f == one <=> g == 1. It suffices to test one of them. */
210 if (f == one) return(one);
211
212 res = cuddCacheLookup2(dd,Cudd_bddLiteralSetIntersection,f,g);
213 if (res != NULL) {
214 return(res);
215 }
216
217 /* Here f and g are both non constant and have the same top variable. */
218 comple = f != F;
219 fc = cuddT(F);
220 phasef = 1;
221 if (comple) fc = Cudd_Not(fc);
222 if (fc == zero) {
223 fc = cuddE(F);
224 phasef = 0;
225 if (comple) fc = Cudd_Not(fc);
226 }
227 comple = g != G;
228 gc = cuddT(G);
229 phaseg = 1;
230 if (comple) gc = Cudd_Not(gc);
231 if (gc == zero) {
232 gc = cuddE(G);
233 phaseg = 0;
234 if (comple) gc = Cudd_Not(gc);
235 }
236
237 tmp = cuddBddLiteralSetIntersectionRecur(dd,fc,gc);
238 if (tmp == NULL) {
239 return(NULL);
240 }
241
242 if (phasef != phaseg) {
243 res = tmp;
244 } else {
245 cuddRef(tmp);
246 if (phasef == 0) {
247 res = cuddBddAndRecur(dd,Cudd_Not(dd->vars[F->index]),tmp);
248 } else {
249 res = cuddBddAndRecur(dd,dd->vars[F->index],tmp);
250 }
251 if (res == NULL) {
252 Cudd_RecursiveDeref(dd,tmp);
253 return(NULL);
254 }
255 cuddDeref(tmp); /* Just cuddDeref, because it is included in result */
256 }
257
258 cuddCacheInsert2(dd,Cudd_bddLiteralSetIntersection,f,g,res);
259
260 return(res);
261
262 } /* end of cuddBddLiteralSetIntersectionRecur */
263
264
265 /*---------------------------------------------------------------------------*/
266 /* Definition of static functions */
267 /*---------------------------------------------------------------------------*/
268
269
270 ABC_NAMESPACE_IMPL_END
271
272
273