1 /**CFile***********************************************************************
7 Synopsis [Functions for the solution of satisfiability related
10 Description [External procedures included in this file:
13 <li> Cudd_ShortestPath()
14 <li> Cudd_LargestCube()
15 <li> Cudd_ShortestLength()
16 <li> Cudd_Decreasing()
17 <li> Cudd_Increasing()
19 <li> Cudd_bddLeqUnless()
20 <li> Cudd_EqualSupNorm()
21 <li> Cudd_bddMakePrime()
23 Internal procedures included in this module:
25 <li> cuddBddMakePrime()
27 Static procedures included in this module:
36 Author [Seh-Woong Jeong, Fabio Somenzi]
38 Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado
42 Redistribution and use in source and binary forms, with or without
43 modification, are permitted provided that the following conditions
46 Redistributions of source code must retain the above copyright
47 notice, this list of conditions and the following disclaimer.
49 Redistributions in binary form must reproduce the above copyright
50 notice, this list of conditions and the following disclaimer in the
51 documentation and/or other materials provided with the distribution.
53 Neither the name of the University of Colorado nor the names of its
54 contributors may be used to endorse or promote products derived from
55 this software without specific prior written permission.
57 THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
58 "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
59 LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS
60 FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE
61 COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT,
62 INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING,
63 BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
64 LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
65 CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT
66 LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN
67 ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
68 POSSIBILITY OF SUCH DAMAGE.]
70 ******************************************************************************/
75 /*---------------------------------------------------------------------------*/
76 /* Constant declarations */
77 /*---------------------------------------------------------------------------*/
79 #define DD_BIGGY 1000000
81 /*---------------------------------------------------------------------------*/
82 /* Stucture declarations */
83 /*---------------------------------------------------------------------------*/
85 /*---------------------------------------------------------------------------*/
86 /* Type declarations */
87 /*---------------------------------------------------------------------------*/
89 typedef struct cuddPathPair
{
94 /*---------------------------------------------------------------------------*/
95 /* Variable declarations */
96 /*---------------------------------------------------------------------------*/
99 static char rcsid
[] DD_UNUSED
= "$Id: cuddSat.c,v 1.36 2009/03/08 02:49:02 fabio Exp $";
102 static DdNode
*one
, *zero
;
104 /*---------------------------------------------------------------------------*/
105 /* Macro declarations */
106 /*---------------------------------------------------------------------------*/
108 #define WEIGHT(weight, col) ((weight) == NULL ? 1 : weight[col])
114 /**AutomaticStart*************************************************************/
116 /*---------------------------------------------------------------------------*/
117 /* Static function prototypes */
118 /*---------------------------------------------------------------------------*/
120 static enum st_retval
freePathPair (char *key
, char *value
, char *arg
);
121 static cuddPathPair
getShortest (DdNode
*root
, int *cost
, int *support
, st_table
*visited
);
122 static DdNode
* getPath (DdManager
*manager
, st_table
*visited
, DdNode
*f
, int *weight
, int cost
);
123 static cuddPathPair
getLargest (DdNode
*root
, st_table
*visited
);
124 static DdNode
* getCube (DdManager
*manager
, st_table
*visited
, DdNode
*f
, int cost
);
126 /**AutomaticEnd***************************************************************/
132 /*---------------------------------------------------------------------------*/
133 /* Definition of exported functions */
134 /*---------------------------------------------------------------------------*/
137 /**Function********************************************************************
139 Synopsis [Returns the value of a DD for a given variable assignment.]
141 Description [Finds the value of a DD for a given variable
142 assignment. The variable assignment is passed in an array of int's,
143 that should specify a zero or a one for each variable in the support
144 of the function. Returns a pointer to a constant node. No new nodes
149 SeeAlso [Cudd_bddLeq Cudd_addEvalConst]
151 ******************************************************************************/
161 comple
= Cudd_IsComplement(f
);
162 ptr
= Cudd_Regular(f
);
164 while (!cuddIsConstant(ptr
)) {
165 if (inputs
[ptr
->index
] == 1) {
168 comple
^= Cudd_IsComplement(cuddE(ptr
));
169 ptr
= Cudd_Regular(cuddE(ptr
));
172 return(Cudd_NotCond(ptr
,comple
));
174 } /* end of Cudd_Eval */
177 /**Function********************************************************************
179 Synopsis [Finds a shortest path in a DD.]
181 Description [Finds a shortest path in a DD. f is the DD we want to
182 get the shortest path for; weight\[i\] is the weight of the THEN arc
183 coming from the node whose index is i. If weight is NULL, then unit
184 weights are assumed for all THEN arcs. All ELSE arcs have 0 weight.
185 If non-NULL, both weight and support should point to arrays with at
186 least as many entries as there are variables in the manager.
187 Returns the shortest path as the BDD of a cube.]
189 SideEffects [support contains on return the true support of f.
190 If support is NULL on entry, then Cudd_ShortestPath does not compute
191 the true support info. length contains the length of the path.]
193 SeeAlso [Cudd_ShortestLength Cudd_LargestCube]
195 ******************************************************************************/
207 cuddPathPair
*rootPair
;
208 int complement
, cost
;
211 one
= DD_ONE(manager
);
212 zero
= DD_ZERO(manager
);
214 /* Initialize support. Support does not depend on variable order.
215 ** Hence, it does not need to be reinitialized if reordering occurs.
218 for (i
= 0; i
< manager
->size
; i
++) {
223 if (f
== Cudd_Not(one
) || f
== zero
) {
225 return(Cudd_Not(one
));
227 /* From this point on, a path exists. */
230 manager
->reordered
= 0;
232 /* Initialize visited table. */
233 visited
= st_init_table(st_ptrcmp
, st_ptrhash
);
235 /* Now get the length of the shortest path(s) from f to 1. */
236 (void) getShortest(f
, weight
, support
, visited
);
238 complement
= Cudd_IsComplement(f
);
242 if (!st_lookup(visited
, F
, &rootPair
)) return(NULL
);
245 cost
= rootPair
->neg
;
247 cost
= rootPair
->pos
;
250 /* Recover an actual shortest path. */
251 sol
= getPath(manager
,visited
,f
,weight
,cost
);
253 st_foreach(visited
, freePathPair
, NULL
);
254 st_free_table(visited
);
256 } while (manager
->reordered
== 1);
261 } /* end of Cudd_ShortestPath */
264 /**Function********************************************************************
266 Synopsis [Finds a largest cube in a DD.]
268 Description [Finds a largest cube in a DD. f is the DD we want to
269 get the largest cube for. The problem is translated into the one of
270 finding a shortest path in f, when both THEN and ELSE arcs are assumed to
271 have unit length. This yields a largest cube in the disjoint cover
272 corresponding to the DD. Therefore, it is not necessarily the largest
273 implicant of f. Returns the largest cube as a BDD.]
275 SideEffects [The number of literals of the cube is returned in length.]
277 SeeAlso [Cudd_ShortestPath]
279 ******************************************************************************/
289 cuddPathPair
*rootPair
;
290 int complement
, cost
;
292 one
= DD_ONE(manager
);
293 zero
= DD_ZERO(manager
);
295 if (f
== Cudd_Not(one
) || f
== zero
) {
297 return(Cudd_Not(one
));
299 /* From this point on, a path exists. */
302 manager
->reordered
= 0;
304 /* Initialize visited table. */
305 visited
= st_init_table(st_ptrcmp
, st_ptrhash
);
307 /* Now get the length of the shortest path(s) from f to 1. */
308 (void) getLargest(f
, visited
);
310 complement
= Cudd_IsComplement(f
);
314 if (!st_lookup(visited
, F
, &rootPair
)) return(NULL
);
317 cost
= rootPair
->neg
;
319 cost
= rootPair
->pos
;
322 /* Recover an actual shortest path. */
323 sol
= getCube(manager
,visited
,f
,cost
);
325 st_foreach(visited
, freePathPair
, NULL
);
326 st_free_table(visited
);
328 } while (manager
->reordered
== 1);
333 } /* end of Cudd_LargestCube */
336 /**Function********************************************************************
338 Synopsis [Find the length of the shortest path(s) in a DD.]
340 Description [Find the length of the shortest path(s) in a DD. f is
341 the DD we want to get the shortest path for; weight\[i\] is the
342 weight of the THEN edge coming from the node whose index is i. All
343 ELSE edges have 0 weight. Returns the length of the shortest
344 path(s) if such a path is found; a large number if the function is
345 identically 0, and CUDD_OUT_OF_MEM in case of failure.]
349 SeeAlso [Cudd_ShortestPath]
351 ******************************************************************************/
360 cuddPathPair
*my_pair
;
361 int complement
, cost
;
363 one
= DD_ONE(manager
);
364 zero
= DD_ZERO(manager
);
366 if (f
== Cudd_Not(one
) || f
== zero
) {
370 /* From this point on, a path exists. */
371 /* Initialize visited table and support. */
372 visited
= st_init_table(st_ptrcmp
, st_ptrhash
);
374 /* Now get the length of the shortest path(s) from f to 1. */
375 (void) getShortest(f
, weight
, NULL
, visited
);
377 complement
= Cudd_IsComplement(f
);
381 if (!st_lookup(visited
, F
, &my_pair
)) return(CUDD_OUT_OF_MEM
);
389 st_foreach(visited
, freePathPair
, NULL
);
390 st_free_table(visited
);
394 } /* end of Cudd_ShortestLength */
397 /**Function********************************************************************
399 Synopsis [Determines whether a BDD is negative unate in a
402 Description [Determines whether the function represented by BDD f is
403 negative unate (monotonic decreasing) in variable i. Returns the
404 constant one is f is unate and the (logical) constant zero if it is not.
405 This function does not generate any new nodes.]
409 SeeAlso [Cudd_Increasing]
411 ******************************************************************************/
418 unsigned int topf
, level
;
419 DdNode
*F
, *fv
, *fvn
, *res
;
424 assert(0 <= i
&& i
< dd
->size
);
428 topf
= cuddI(dd
,F
->index
);
430 /* Check terminal case. If topf > i, f does not depend on var.
431 ** Therefore, f is unate in i.
433 level
= (unsigned) dd
->perm
[i
];
438 /* From now on, f is not constant. */
441 cacheOp
= (DD_CTFP
) Cudd_Decreasing
;
442 res
= cuddCacheLookup2(dd
,cacheOp
,f
,dd
->vars
[i
]);
447 /* Compute cofactors. */
448 fv
= cuddT(F
); fvn
= cuddE(F
);
454 if (topf
== (unsigned) level
) {
455 /* Special case: if fv is regular, fv(1,...,1) = 1;
456 ** If in addition fvn is complemented, fvn(1,...,1) = 0.
457 ** But then f(1,1,...,1) > f(0,1,...,1). Hence f is not
458 ** monotonic decreasing in i.
460 if (!Cudd_IsComplement(fv
) && Cudd_IsComplement(fvn
)) {
461 return(Cudd_Not(DD_ONE(dd
)));
463 res
= Cudd_bddLeq(dd
,fv
,fvn
) ? DD_ONE(dd
) : Cudd_Not(DD_ONE(dd
));
465 res
= Cudd_Decreasing(dd
,fv
,i
);
466 if (res
== DD_ONE(dd
)) {
467 res
= Cudd_Decreasing(dd
,fvn
,i
);
471 cuddCacheInsert2(dd
,cacheOp
,f
,dd
->vars
[i
],res
);
474 } /* end of Cudd_Decreasing */
477 /**Function********************************************************************
479 Synopsis [Determines whether a BDD is positive unate in a
482 Description [Determines whether the function represented by BDD f is
483 positive unate (monotonic increasing) in variable i. It is based on
484 Cudd_Decreasing and the fact that f is monotonic increasing in i if
485 and only if its complement is monotonic decreasing in i.]
489 SeeAlso [Cudd_Decreasing]
491 ******************************************************************************/
498 return(Cudd_Decreasing(dd
,Cudd_Not(f
),i
));
500 } /* end of Cudd_Increasing */
503 /**Function********************************************************************
505 Synopsis [Tells whether F and G are identical wherever D is 0.]
507 Description [Tells whether F and G are identical wherever D is 0. F
508 and G are either two ADDs or two BDDs. D is either a 0-1 ADD or a
509 BDD. The function returns 1 if F and G are equivalent, and 0
510 otherwise. No new nodes are created.]
514 SeeAlso [Cudd_bddLeqUnless]
516 ******************************************************************************/
524 DdNode
*tmp
, *One
, *Gr
, *Dr
;
525 DdNode
*Fv
, *Fvn
, *Gv
, *Gvn
, *Dv
, *Dvn
;
527 unsigned int flevel
, glevel
, dlevel
, top
;
532 /* Check terminal cases. */
533 if (D
== One
|| F
== G
) return(1);
534 if (D
== Cudd_Not(One
) || D
== DD_ZERO(dd
) || F
== Cudd_Not(G
)) return(0);
536 /* From now on, D is non-constant. */
538 /* Normalize call to increase cache efficiency. */
544 if (Cudd_IsComplement(F
)) {
549 /* From now on, F is regular. */
552 tmp
= cuddCacheLookup(dd
,DD_EQUIV_DC_TAG
,F
,G
,D
);
553 if (tmp
!= NULL
) return(tmp
== One
);
555 /* Find splitting variable. */
556 flevel
= cuddI(dd
,F
->index
);
557 Gr
= Cudd_Regular(G
);
558 glevel
= cuddI(dd
,Gr
->index
);
559 top
= ddMin(flevel
,glevel
);
560 Dr
= Cudd_Regular(D
);
561 dlevel
= dd
->perm
[Dr
->index
];
562 top
= ddMin(top
,dlevel
);
564 /* Compute cofactors. */
592 /* Solve recursively. */
593 res
= Cudd_EquivDC(dd
,Fv
,Gv
,Dv
);
595 res
= Cudd_EquivDC(dd
,Fvn
,Gvn
,Dvn
);
597 cuddCacheInsert(dd
,DD_EQUIV_DC_TAG
,F
,G
,D
,(res
) ? One
: Cudd_Not(One
));
601 } /* end of Cudd_EquivDC */
604 /**Function********************************************************************
606 Synopsis [Tells whether f is less than of equal to G unless D is 1.]
608 Description [Tells whether f is less than of equal to G unless D is
609 1. f, g, and D are BDDs. The function returns 1 if f is less than
610 of equal to G, and 0 otherwise. No new nodes are created.]
614 SeeAlso [Cudd_EquivDC Cudd_bddLeq Cudd_bddIteConstant]
616 ******************************************************************************/
624 DdNode
*tmp
, *One
, *F
, *G
;
625 DdNode
*Ft
, *Fe
, *Gt
, *Ge
, *Dt
, *De
;
627 unsigned int flevel
, glevel
, dlevel
, top
;
633 /* Check terminal cases. */
634 if (f
== g
|| g
== One
|| f
== Cudd_Not(One
) || D
== One
||
635 D
== f
|| D
== Cudd_Not(g
)) return(1);
636 /* Check for two-operand cases. */
637 if (D
== Cudd_Not(One
) || D
== g
|| D
== Cudd_Not(f
))
638 return(Cudd_bddLeq(dd
,f
,g
));
639 if (g
== Cudd_Not(One
) || g
== Cudd_Not(f
)) return(Cudd_bddLeq(dd
,f
,D
));
640 if (f
== One
) return(Cudd_bddLeq(dd
,Cudd_Not(g
),D
));
642 /* From now on, f, g, and D are non-constant, distinct, and
643 ** non-complementary. */
645 /* Normalize call to increase cache efficiency. We rely on the
646 ** fact that f <= g unless D is equivalent to not(g) <= not(f)
647 ** unless D and to f <= D unless g. We make sure that D is
648 ** regular, and that at most one of f and g is complemented. We also
649 ** ensure that when two operands can be swapped, the one with the
650 ** lowest address comes first. */
652 if (Cudd_IsComplement(D
)) {
653 if (Cudd_IsComplement(g
)) {
654 /* Special case: if f is regular and g is complemented,
655 ** f(1,...,1) = 1 > 0 = g(1,...,1). If D(1,...,1) = 0, return 0.
657 if (!Cudd_IsComplement(f
)) return(0);
658 /* !g <= D unless !f or !D <= g unless !f */
668 if (Cudd_IsComplement(f
)) {
669 /* !D <= !f unless g or !D <= g unless !f */
679 /* f <= D unless g or !D <= !f unless g */
691 if (Cudd_IsComplement(g
)) {
692 if (Cudd_IsComplement(f
)) {
693 /* !g <= !f unless D or !g <= D unless !f */
703 /* f <= g unless D or !g <= !f unless D */
711 /* f <= g unless D or f <= D unless g */
720 /* From now on, D is regular. */
723 tmp
= cuddCacheLookup(dd
,DD_BDD_LEQ_UNLESS_TAG
,f
,g
,D
);
724 if (tmp
!= NULL
) return(tmp
== One
);
726 /* Find splitting variable. */
728 flevel
= dd
->perm
[F
->index
];
730 glevel
= dd
->perm
[G
->index
];
731 top
= ddMin(flevel
,glevel
);
732 dlevel
= dd
->perm
[D
->index
];
733 top
= ddMin(top
,dlevel
);
735 /* Compute cofactors. */
763 /* Solve recursively. */
764 res
= Cudd_bddLeqUnless(dd
,Ft
,Gt
,Dt
);
766 res
= Cudd_bddLeqUnless(dd
,Fe
,Ge
,De
);
768 cuddCacheInsert(dd
,DD_BDD_LEQ_UNLESS_TAG
,f
,g
,D
,Cudd_NotCond(One
,!res
));
772 } /* end of Cudd_bddLeqUnless */
775 /**Function********************************************************************
777 Synopsis [Compares two ADDs for equality within tolerance.]
779 Description [Compares two ADDs for equality within tolerance. Two
780 ADDs are reported to be equal if the maximum difference between them
781 (the sup norm of their difference) is less than or equal to the
782 tolerance parameter. Returns 1 if the two ADDs are equal (within
783 tolerance); 0 otherwise. If parameter <code>pr</code> is positive
784 the first failure is reported to the standard output.]
790 ******************************************************************************/
793 DdManager
* dd
/* manager */,
794 DdNode
* f
/* first ADD */,
795 DdNode
* g
/* second ADD */,
796 CUDD_VALUE_TYPE tolerance
/* maximum allowed difference */,
797 int pr
/* verbosity level */)
799 DdNode
*fv
, *fvn
, *gv
, *gvn
, *r
;
800 unsigned int topf
, topg
;
803 /* Check terminal cases. */
804 if (f
== g
) return(1);
805 if (Cudd_IsConstant(f
) && Cudd_IsConstant(g
)) {
806 if (ddEqualVal(cuddV(f
),cuddV(g
),tolerance
)) {
810 (void) fprintf(dd
->out
,"Offending nodes:\n");
811 (void) fprintf(dd
->out
,
812 "f: address = %p\t value = %40.30f\n",
813 (void *) f
, cuddV(f
));
814 (void) fprintf(dd
->out
,
815 "g: address = %p\t value = %40.30f\n",
816 (void *) g
, cuddV(g
));
822 /* We only insert the result in the cache if the comparison is
823 ** successful. Therefore, if we hit we return 1. */
824 r
= cuddCacheLookup2(dd
,(DD_CTFP
)Cudd_EqualSupNorm
,f
,g
);
829 /* Compute the cofactors and solve the recursive subproblems. */
830 topf
= cuddI(dd
,f
->index
);
831 topg
= cuddI(dd
,g
->index
);
833 if (topf
<= topg
) {fv
= cuddT(f
); fvn
= cuddE(f
);} else {fv
= fvn
= f
;}
834 if (topg
<= topf
) {gv
= cuddT(g
); gvn
= cuddE(g
);} else {gv
= gvn
= g
;}
836 if (!Cudd_EqualSupNorm(dd
,fv
,gv
,tolerance
,pr
)) return(0);
837 if (!Cudd_EqualSupNorm(dd
,fvn
,gvn
,tolerance
,pr
)) return(0);
839 cuddCacheInsert2(dd
,(DD_CTFP
)Cudd_EqualSupNorm
,f
,g
,DD_ONE(dd
));
843 } /* end of Cudd_EqualSupNorm */
846 /**Function********************************************************************
848 Synopsis [Expands cube to a prime implicant of f.]
850 Description [Expands cube to a prime implicant of f. Returns the prime
851 if successful; NULL otherwise. In particular, NULL is returned if cube
852 is not a real cube or is not an implicant of f.]
858 ******************************************************************************/
861 DdManager
*dd
/* manager */,
862 DdNode
*cube
/* cube to be expanded */,
863 DdNode
*f
/* function of which the cube is to be made a prime */)
867 if (!Cudd_bddLeq(dd
,cube
,f
)) return(NULL
);
871 res
= cuddBddMakePrime(dd
,cube
,f
);
872 } while (dd
->reordered
== 1);
875 } /* end of Cudd_bddMakePrime */
878 /*---------------------------------------------------------------------------*/
879 /* Definition of internal functions */
880 /*---------------------------------------------------------------------------*/
883 /**Function********************************************************************
885 Synopsis [Performs the recursive step of Cudd_bddMakePrime.]
887 Description [Performs the recursive step of Cudd_bddMakePrime.
888 Returns the prime if successful; NULL otherwise.]
894 ******************************************************************************/
897 DdManager
*dd
/* manager */,
898 DdNode
*cube
/* cube to be expanded */,
899 DdNode
*f
/* function of which the cube is to be made a prime */)
904 DdNode
*zero
= Cudd_Not(DD_ONE(dd
));
908 while (!Cudd_IsConstant(scan
)) {
909 DdNode
*reg
= Cudd_Regular(scan
);
910 DdNode
*var
= dd
->vars
[reg
->index
];
911 DdNode
*expanded
= Cudd_bddExistAbstract(dd
,res
,var
);
912 if (expanded
== NULL
) {
916 if (Cudd_bddLeq(dd
,expanded
,f
)) {
917 Cudd_RecursiveDeref(dd
,res
);
920 Cudd_RecursiveDeref(dd
,expanded
);
922 cuddGetBranches(scan
,&t
,&e
);
925 } else if (e
== zero
) {
928 Cudd_RecursiveDeref(dd
,res
);
929 return(NULL
); /* cube is not a cube */
933 if (scan
== DD_ONE(dd
)) {
937 Cudd_RecursiveDeref(dd
,res
);
941 } /* end of cuddBddMakePrime */
944 /*---------------------------------------------------------------------------*/
945 /* Definition of static functions */
946 /*---------------------------------------------------------------------------*/
949 /**Function********************************************************************
951 Synopsis [Frees the entries of the visited symbol table.]
953 Description [Frees the entries of the visited symbol table. Returns
958 ******************************************************************************/
959 static enum st_retval
967 pair
= (cuddPathPair
*) value
;
971 } /* end of freePathPair */
974 /**Function********************************************************************
976 Synopsis [Finds the length of the shortest path(s) in a DD.]
978 Description [Finds the length of the shortest path(s) in a DD.
979 Uses a local symbol table to store the lengths for each
980 node. Only the lengths for the regular nodes are entered in the table,
981 because those for the complement nodes are simply obtained by swapping
983 Returns a pair of lengths: the length of the shortest path to 1;
984 and the length of the shortest path to 0. This is done so as to take
985 complement arcs into account.]
987 SideEffects [Accumulates the support of the DD in support.]
991 ******************************************************************************/
999 cuddPathPair
*my_pair
, res_pair
, pair_T
, pair_E
;
1000 DdNode
*my_root
, *T
, *E
;
1003 my_root
= Cudd_Regular(root
);
1005 if (st_lookup(visited
, my_root
, &my_pair
)) {
1006 if (Cudd_IsComplement(root
)) {
1007 res_pair
.pos
= my_pair
->neg
;
1008 res_pair
.neg
= my_pair
->pos
;
1010 res_pair
.pos
= my_pair
->pos
;
1011 res_pair
.neg
= my_pair
->neg
;
1016 /* In the case of a BDD the following test is equivalent to
1017 ** testing whether the BDD is the constant 1. This formulation,
1018 ** however, works for ADDs as well, by assuming the usual
1019 ** dichotomy of 0 and != 0.
1021 if (cuddIsConstant(my_root
)) {
1022 if (my_root
!= zero
) {
1024 res_pair
.neg
= DD_BIGGY
;
1026 res_pair
.pos
= DD_BIGGY
;
1033 pair_T
= getShortest(T
, cost
, support
, visited
);
1034 pair_E
= getShortest(E
, cost
, support
, visited
);
1035 weight
= WEIGHT(cost
, my_root
->index
);
1036 res_pair
.pos
= ddMin(pair_T
.pos
+weight
, pair_E
.pos
);
1037 res_pair
.neg
= ddMin(pair_T
.neg
+weight
, pair_E
.neg
);
1039 /* Update support. */
1040 if (support
!= NULL
) {
1041 support
[my_root
->index
] = 1;
1045 my_pair
= ALLOC(cuddPathPair
, 1);
1046 if (my_pair
== NULL
) {
1047 if (Cudd_IsComplement(root
)) {
1048 int tmp
= res_pair
.pos
;
1049 res_pair
.pos
= res_pair
.neg
;
1054 my_pair
->pos
= res_pair
.pos
;
1055 my_pair
->neg
= res_pair
.neg
;
1057 st_insert(visited
, (char *)my_root
, (char *)my_pair
);
1058 if (Cudd_IsComplement(root
)) {
1059 res_pair
.pos
= my_pair
->neg
;
1060 res_pair
.neg
= my_pair
->pos
;
1062 res_pair
.pos
= my_pair
->pos
;
1063 res_pair
.neg
= my_pair
->neg
;
1067 } /* end of getShortest */
1070 /**Function********************************************************************
1072 Synopsis [Build a BDD for a shortest path of f.]
1074 Description [Build a BDD for a shortest path of f.
1075 Given the minimum length from the root, and the minimum
1076 lengths for each node (in visited), apply triangulation at each node.
1077 Of the two children of each node on a shortest path, at least one is
1078 on a shortest path. In case of ties the procedure chooses the THEN
1080 Returns a pointer to the cube BDD representing the path if
1081 successful; NULL otherwise.]
1087 ******************************************************************************/
1090 DdManager
* manager
,
1097 DdNode
*my_dd
, *T
, *E
;
1098 cuddPathPair
*T_pair
, *E_pair
;
1102 my_dd
= Cudd_Regular(f
);
1103 complement
= Cudd_IsComplement(f
);
1108 while (!cuddIsConstant(my_dd
)) {
1109 Tcost
= cost
- WEIGHT(weight
, my_dd
->index
);
1115 if (complement
) {T
= Cudd_Not(T
); E
= Cudd_Not(E
);}
1117 st_lookup(visited
, Cudd_Regular(T
), &T_pair
);
1118 if ((Cudd_IsComplement(T
) && T_pair
->neg
== Tcost
) ||
1119 (!Cudd_IsComplement(T
) && T_pair
->pos
== Tcost
)) {
1120 tmp
= cuddBddAndRecur(manager
,manager
->vars
[my_dd
->index
],sol
);
1122 Cudd_RecursiveDeref(manager
,sol
);
1126 Cudd_RecursiveDeref(manager
,sol
);
1129 complement
= Cudd_IsComplement(T
);
1130 my_dd
= Cudd_Regular(T
);
1134 st_lookup(visited
, Cudd_Regular(E
), &E_pair
);
1135 if ((Cudd_IsComplement(E
) && E_pair
->neg
== Ecost
) ||
1136 (!Cudd_IsComplement(E
) && E_pair
->pos
== Ecost
)) {
1137 tmp
= cuddBddAndRecur(manager
,Cudd_Not(manager
->vars
[my_dd
->index
]),sol
);
1139 Cudd_RecursiveDeref(manager
,sol
);
1143 Cudd_RecursiveDeref(manager
,sol
);
1145 complement
= Cudd_IsComplement(E
);
1146 my_dd
= Cudd_Regular(E
);
1150 (void) fprintf(manager
->err
,"We shouldn't be here!!\n");
1151 manager
->errorCode
= CUDD_INTERNAL_ERROR
;
1158 } /* end of getPath */
1161 /**Function********************************************************************
1163 Synopsis [Finds the size of the largest cube(s) in a DD.]
1165 Description [Finds the size of the largest cube(s) in a DD.
1166 This problem is translated into finding the shortest paths from a node
1167 when both THEN and ELSE arcs have unit lengths.
1168 Uses a local symbol table to store the lengths for each
1169 node. Only the lengths for the regular nodes are entered in the table,
1170 because those for the complement nodes are simply obtained by swapping
1172 Returns a pair of lengths: the length of the shortest path to 1;
1173 and the length of the shortest path to 0. This is done so as to take
1174 complement arcs into account.]
1180 ******************************************************************************/
1186 cuddPathPair
*my_pair
, res_pair
, pair_T
, pair_E
;
1187 DdNode
*my_root
, *T
, *E
;
1189 my_root
= Cudd_Regular(root
);
1191 if (st_lookup(visited
, my_root
, &my_pair
)) {
1192 if (Cudd_IsComplement(root
)) {
1193 res_pair
.pos
= my_pair
->neg
;
1194 res_pair
.neg
= my_pair
->pos
;
1196 res_pair
.pos
= my_pair
->pos
;
1197 res_pair
.neg
= my_pair
->neg
;
1202 /* In the case of a BDD the following test is equivalent to
1203 ** testing whether the BDD is the constant 1. This formulation,
1204 ** however, works for ADDs as well, by assuming the usual
1205 ** dichotomy of 0 and != 0.
1207 if (cuddIsConstant(my_root
)) {
1208 if (my_root
!= zero
) {
1210 res_pair
.neg
= DD_BIGGY
;
1212 res_pair
.pos
= DD_BIGGY
;
1219 pair_T
= getLargest(T
, visited
);
1220 pair_E
= getLargest(E
, visited
);
1221 res_pair
.pos
= ddMin(pair_T
.pos
, pair_E
.pos
) + 1;
1222 res_pair
.neg
= ddMin(pair_T
.neg
, pair_E
.neg
) + 1;
1225 my_pair
= ALLOC(cuddPathPair
, 1);
1226 if (my_pair
== NULL
) { /* simply do not cache this result */
1227 if (Cudd_IsComplement(root
)) {
1228 int tmp
= res_pair
.pos
;
1229 res_pair
.pos
= res_pair
.neg
;
1234 my_pair
->pos
= res_pair
.pos
;
1235 my_pair
->neg
= res_pair
.neg
;
1237 /* Caching may fail without affecting correctness. */
1238 st_insert(visited
, (char *)my_root
, (char *)my_pair
);
1239 if (Cudd_IsComplement(root
)) {
1240 res_pair
.pos
= my_pair
->neg
;
1241 res_pair
.neg
= my_pair
->pos
;
1243 res_pair
.pos
= my_pair
->pos
;
1244 res_pair
.neg
= my_pair
->neg
;
1248 } /* end of getLargest */
1251 /**Function********************************************************************
1253 Synopsis [Build a BDD for a largest cube of f.]
1255 Description [Build a BDD for a largest cube of f.
1256 Given the minimum length from the root, and the minimum
1257 lengths for each node (in visited), apply triangulation at each node.
1258 Of the two children of each node on a shortest path, at least one is
1259 on a shortest path. In case of ties the procedure chooses the THEN
1261 Returns a pointer to the cube BDD representing the path if
1262 successful; NULL otherwise.]
1268 ******************************************************************************/
1271 DdManager
* manager
,
1277 DdNode
*my_dd
, *T
, *E
;
1278 cuddPathPair
*T_pair
, *E_pair
;
1282 my_dd
= Cudd_Regular(f
);
1283 complement
= Cudd_IsComplement(f
);
1288 while (!cuddIsConstant(my_dd
)) {
1295 if (complement
) {T
= Cudd_Not(T
); E
= Cudd_Not(E
);}
1297 if (!st_lookup(visited
, Cudd_Regular(T
), &T_pair
)) return(NULL
);
1298 if ((Cudd_IsComplement(T
) && T_pair
->neg
== Tcost
) ||
1299 (!Cudd_IsComplement(T
) && T_pair
->pos
== Tcost
)) {
1300 tmp
= cuddBddAndRecur(manager
,manager
->vars
[my_dd
->index
],sol
);
1302 Cudd_RecursiveDeref(manager
,sol
);
1306 Cudd_RecursiveDeref(manager
,sol
);
1309 complement
= Cudd_IsComplement(T
);
1310 my_dd
= Cudd_Regular(T
);
1314 if (!st_lookup(visited
, Cudd_Regular(E
), &E_pair
)) return(NULL
);
1315 if ((Cudd_IsComplement(E
) && E_pair
->neg
== Ecost
) ||
1316 (!Cudd_IsComplement(E
) && E_pair
->pos
== Ecost
)) {
1317 tmp
= cuddBddAndRecur(manager
,Cudd_Not(manager
->vars
[my_dd
->index
]),sol
);
1319 Cudd_RecursiveDeref(manager
,sol
);
1323 Cudd_RecursiveDeref(manager
,sol
);
1325 complement
= Cudd_IsComplement(E
);
1326 my_dd
= Cudd_Regular(E
);
1330 (void) fprintf(manager
->err
,"We shouldn't be here!\n");
1331 manager
->errorCode
= CUDD_INTERNAL_ERROR
;
1338 } /* end of getCube */