1 /**CFile***********************************************************************
3 FileName [cuddLiteral.c]
7 Synopsis [Functions for manipulation of literal sets represented by
10 Description [External procedures included in this file:
12 <li> Cudd_bddLiteralSetIntersection()
14 Internal procedures included in this file:
16 <li> cuddBddLiteralSetIntersectionRecur()
19 Author [Fabio Somenzi]
21 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
25 Redistribution and use in source and binary forms, with or without
26 modification, are permitted provided that the following conditions
29 Redistributions of source code must retain the above copyright
30 notice, this list of conditions and the following disclaimer.
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.
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.
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.]
53 ******************************************************************************/
59 /*---------------------------------------------------------------------------*/
60 /* Constant declarations */
61 /*---------------------------------------------------------------------------*/
63 /*---------------------------------------------------------------------------*/
64 /* Stucture declarations */
65 /*---------------------------------------------------------------------------*/
67 /*---------------------------------------------------------------------------*/
68 /* Type declarations */
69 /*---------------------------------------------------------------------------*/
71 /*---------------------------------------------------------------------------*/
72 /* Variable declarations */
73 /*---------------------------------------------------------------------------*/
76 static char rcsid
[] DD_UNUSED
= "$Id: cuddLiteral.c,v 1.8 2004/08/13 18:04:50 fabio Exp $";
79 /*---------------------------------------------------------------------------*/
80 /* Macro declarations */
81 /*---------------------------------------------------------------------------*/
83 /**AutomaticStart*************************************************************/
85 /*---------------------------------------------------------------------------*/
86 /* Static function prototypes */
87 /*---------------------------------------------------------------------------*/
90 /**AutomaticEnd***************************************************************/
93 /*---------------------------------------------------------------------------*/
94 /* Definition of exported functions */
95 /*---------------------------------------------------------------------------*/
98 /**Function********************************************************************
100 Synopsis [Computes the intesection of two sets of literals
101 represented as BDDs.]
103 Description [Computes the intesection of two sets of literals
104 represented as BDDs. Each set is represented as a cube of the
105 literals in the set. The empty set is represented by the constant 1.
106 No variable can be simultaneously present in both phases in a set.
107 Returns a pointer to the BDD representing the intersected sets, if
108 successful; NULL otherwise.]
112 ******************************************************************************/
114 Cudd_bddLiteralSetIntersection(
123 res
= cuddBddLiteralSetIntersectionRecur(dd
,f
,g
);
124 } while (dd
->reordered
== 1);
127 } /* end of Cudd_bddLiteralSetIntersection */
130 /*---------------------------------------------------------------------------*/
131 /* Definition of internal functions */
132 /*---------------------------------------------------------------------------*/
135 /**Function********************************************************************
137 Synopsis [Performs the recursive step of
138 Cudd_bddLiteralSetIntersection.]
140 Description [Performs the recursive step of
141 Cudd_bddLiteralSetIntersection. Scans the cubes for common variables,
142 and checks whether they agree in phase. Returns a pointer to the
143 resulting cube if successful; NULL otherwise.]
147 ******************************************************************************/
149 cuddBddLiteralSetIntersectionRecur(
159 unsigned int topf
, topg
, comple
;
163 if (f
== g
) return(f
);
169 /* Here f != g. If F == G, then f and g are complementary.
170 ** Since they are two cubes, this case only occurs when f == v,
171 ** g == v', and v is a variable or its complement.
173 if (F
== G
) return(one
);
175 zero
= Cudd_Not(one
);
176 topf
= cuddI(dd
,F
->index
);
177 topg
= cuddI(dd
,G
->index
);
178 /* Look for a variable common to both cubes. If there are none, this
179 ** loop will stop when the constant node is reached in both cubes.
181 while (topf
!= topg
) {
182 if (topf
< topg
) { /* move down on f */
185 if (comple
) f
= Cudd_Not(f
);
188 if (comple
) f
= Cudd_Not(f
);
191 topf
= cuddI(dd
,F
->index
);
192 } else if (topg
< topf
) {
195 if (comple
) g
= Cudd_Not(g
);
198 if (comple
) g
= Cudd_Not(g
);
201 topg
= cuddI(dd
,G
->index
);
205 /* At this point, f == one <=> g == 1. It suffices to test one of them. */
206 if (f
== one
) return(one
);
208 res
= cuddCacheLookup2(dd
,Cudd_bddLiteralSetIntersection
,f
,g
);
213 /* Here f and g are both non constant and have the same top variable. */
217 if (comple
) fc
= Cudd_Not(fc
);
221 if (comple
) fc
= Cudd_Not(fc
);
226 if (comple
) gc
= Cudd_Not(gc
);
230 if (comple
) gc
= Cudd_Not(gc
);
233 tmp
= cuddBddLiteralSetIntersectionRecur(dd
,fc
,gc
);
238 if (phasef
!= phaseg
) {
243 res
= cuddBddAndRecur(dd
,Cudd_Not(dd
->vars
[F
->index
]),tmp
);
245 res
= cuddBddAndRecur(dd
,dd
->vars
[F
->index
],tmp
);
248 Cudd_RecursiveDeref(dd
,tmp
);
251 cuddDeref(tmp
); /* Just cuddDeref, because it is included in result */
254 cuddCacheInsert2(dd
,Cudd_bddLiteralSetIntersection
,f
,g
,res
);
258 } /* end of cuddBddLiteralSetIntersectionRecur */
261 /*---------------------------------------------------------------------------*/
262 /* Definition of static functions */
263 /*---------------------------------------------------------------------------*/