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