abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions | Variables
cuddZddIsop.c File Reference
#include "misc/util/util_hack.h"
#include "cuddInt.h"

Go to the source code of this file.

Functions

DdNode * Cudd_zddIsop (DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
 
DdNode * Cudd_bddIsop (DdManager *dd, DdNode *L, DdNode *U)
 
DdNode * Cudd_MakeBddFromZddCover (DdManager *dd, DdNode *node)
 
DdNode * cuddZddIsop (DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
 
DdNode * cuddBddIsop (DdManager *dd, DdNode *L, DdNode *U)
 
DdNode * cuddMakeBddFromZddCover (DdManager *dd, DdNode *node)
 

Variables

static
ABC_NAMESPACE_IMPL_START char
rcsid[] 		DD_UNUSED = "$Id: cuddZddIsop.c,v 1.20 2009/02/19 16:26:12 fabio Exp $"
 

Function Documentation

DdNode* Cudd_bddIsop ( DdManager *  dd,
DdNode *  L,
DdNode *  U 
)

Function********************************************************************

Synopsis [Computes a BDD in the interval between L and U with a simple sum-of-produuct cover.]

Description [Computes a BDD in the interval between L and U with a simple sum-of-produuct cover. This procedure is similar to Cudd_zddIsop, but it does not return the ZDD for the cover. Returns a pointer to the BDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_zddIsop]

Definition at line 174 of file cuddZddIsop.c.

178 {
179  DdNode *res;
180 
181  do {
182  dd->reordered = 0;
183  res = cuddBddIsop(dd, L, U);
184  } while (dd->reordered == 1);
185  return(res);
186 
187 } /* end of Cudd_bddIsop */
DdNode
Definition: cudd.h:278
DdManager::reordered
int reordered
Definition: cuddInt.h:409
cuddBddIsop
DdNode * cuddBddIsop(DdManager *dd, DdNode *L, DdNode *U)
Definition: cuddZddIsop.c:575
DdNode* Cudd_MakeBddFromZddCover ( DdManager *  dd,
DdNode *  node 
)

Function********************************************************************

Synopsis [Converts a ZDD cover to a BDD graph.]

Description [Converts a ZDD cover to a BDD graph. If successful, it returns a BDD node, otherwise it returns NULL.]

SideEffects []

SeeAlso [cuddMakeBddFromZddCover]

Definition at line 203 of file cuddZddIsop.c.

206 {
207  DdNode *res;
208 
209  do {
210  dd->reordered = 0;
211  res = cuddMakeBddFromZddCover(dd, node);
212  } while (dd->reordered == 1);
213  return(res);
214 } /* end of Cudd_MakeBddFromZddCover */
DdNode
Definition: cudd.h:278
cuddMakeBddFromZddCover
DdNode * cuddMakeBddFromZddCover(DdManager *dd, DdNode *node)
Definition: cuddZddIsop.c:800
DdManager::reordered
int reordered
Definition: cuddInt.h:409
DdNode* Cudd_zddIsop ( DdManager *  dd,
DdNode *  L,
DdNode *  U,
DdNode **  zdd_I 
)

AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [Computes an ISOP in ZDD form from BDDs.]

Description [Computes an irredundant sum of products (ISOP) in ZDD form from BDDs. The two BDDs L and U represent the lower bound and the upper bound, respectively, of the function. The ISOP uses two ZDD variables for each BDD variable: One for the positive literal, and one for the negative literal. These two variables should be adjacent in the ZDD order. The two ZDD variables corresponding to BDD variable i should have indices 2i and 2i+1. The result of this procedure depends on the variable order. If successful, Cudd_zddIsop returns the BDD for the function chosen from the interval. The ZDD representing the irredundant cover is returned as a side effect in zdd_I. In case of failure, NULL is returned.]

SideEffects [zdd_I holds the pointer to the ZDD for the ISOP on successful return.]

SeeAlso [Cudd_bddIsop Cudd_zddVarsFromBddVars]

Definition at line 136 of file cuddZddIsop.c.

141 {
142  DdNode *res;
143  int autoDynZ;
144 
145  autoDynZ = dd->autoDynZ;
146  dd->autoDynZ = 0;
147 
148  do {
149  dd->reordered = 0;
150  res = cuddZddIsop(dd, L, U, zdd_I);
151  } while (dd->reordered == 1);
152  dd->autoDynZ = autoDynZ;
153  return(res);
154 
155 } /* end of Cudd_zddIsop */
DdNode
Definition: cudd.h:278
cuddZddIsop
DdNode * cuddZddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Definition: cuddZddIsop.c:234
DdManager::reordered
int reordered
Definition: cuddInt.h:409
DdManager::autoDynZ
int autoDynZ
Definition: cuddInt.h:417
DdNode* cuddBddIsop ( DdManager *  dd,
DdNode *  L,
DdNode *  U 
)

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_bddIsop.]

Description []

SideEffects [None]

SeeAlso [Cudd_bddIsop]

Definition at line 575 of file cuddZddIsop.c.

579 {
580  DdNode *one = DD_ONE(dd);
581  DdNode *zero = Cudd_Not(one);
582  int v, top_l, top_u;
583  DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
584  DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
585  DdNode *Isub0, *Isub1, *Id;
586  DdNode *x;
587  DdNode *term0, *term1, *sum;
588  DdNode *Lv, *Uv, *Lnv, *Unv;
589  DdNode *r;
590  int index;
591 
592  statLine(dd);
593  if (L == zero)
594  return(zero);
595  if (U == one)
596  return(one);
597 
598  /* Check cache */
599  r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
600  if (r)
601  return(r);
602 
603  top_l = dd->perm[Cudd_Regular(L)->index];
604  top_u = dd->perm[Cudd_Regular(U)->index];
605  v = ddMin(top_l, top_u);
606 
607  /* Compute cofactors */
608  if (top_l == v) {
609  index = Cudd_Regular(L)->index;
610  Lv = Cudd_T(L);
611  Lnv = Cudd_E(L);
612  if (Cudd_IsComplement(L)) {
613  Lv = Cudd_Not(Lv);
614  Lnv = Cudd_Not(Lnv);
615  }
616  }
617  else {
618  index = Cudd_Regular(U)->index;
619  Lv = Lnv = L;
620  }
621 
622  if (top_u == v) {
623  Uv = Cudd_T(U);
624  Unv = Cudd_E(U);
625  if (Cudd_IsComplement(U)) {
626  Uv = Cudd_Not(Uv);
627  Unv = Cudd_Not(Unv);
628  }
629  }
630  else {
631  Uv = Unv = U;
632  }
633 
634  Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
635  if (Lsub0 == NULL)
636  return(NULL);
637  Cudd_Ref(Lsub0);
638  Usub0 = Unv;
639  Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
640  if (Lsub1 == NULL) {
641  Cudd_RecursiveDeref(dd, Lsub0);
642  return(NULL);
643  }
644  Cudd_Ref(Lsub1);
645  Usub1 = Uv;
646 
647  Isub0 = cuddBddIsop(dd, Lsub0, Usub0);
648  if (Isub0 == NULL) {
649  Cudd_RecursiveDeref(dd, Lsub0);
650  Cudd_RecursiveDeref(dd, Lsub1);
651  return(NULL);
652  }
653  Cudd_Ref(Isub0);
654  Isub1 = cuddBddIsop(dd, Lsub1, Usub1);
655  if (Isub1 == NULL) {
656  Cudd_RecursiveDeref(dd, Lsub0);
657  Cudd_RecursiveDeref(dd, Lsub1);
658  Cudd_RecursiveDeref(dd, Isub0);
659  return(NULL);
660  }
661  Cudd_Ref(Isub1);
662  Cudd_RecursiveDeref(dd, Lsub0);
663  Cudd_RecursiveDeref(dd, Lsub1);
664 
665  Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
666  if (Lsuper0 == NULL) {
667  Cudd_RecursiveDeref(dd, Isub0);
668  Cudd_RecursiveDeref(dd, Isub1);
669  return(NULL);
670  }
671  Cudd_Ref(Lsuper0);
672  Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
673  if (Lsuper1 == NULL) {
674  Cudd_RecursiveDeref(dd, Isub0);
675  Cudd_RecursiveDeref(dd, Isub1);
676  Cudd_RecursiveDeref(dd, Lsuper0);
677  return(NULL);
678  }
679  Cudd_Ref(Lsuper1);
680  Usuper0 = Unv;
681  Usuper1 = Uv;
682 
683  /* Ld = Lsuper0 + Lsuper1 */
684  Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
685  Ld = Cudd_NotCond(Ld, Ld != NULL);
686  if (Ld == NULL) {
687  Cudd_RecursiveDeref(dd, Isub0);
688  Cudd_RecursiveDeref(dd, Isub1);
689  Cudd_RecursiveDeref(dd, Lsuper0);
690  Cudd_RecursiveDeref(dd, Lsuper1);
691  return(NULL);
692  }
693  Cudd_Ref(Ld);
694  Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
695  if (Ud == NULL) {
696  Cudd_RecursiveDeref(dd, Isub0);
697  Cudd_RecursiveDeref(dd, Isub1);
698  Cudd_RecursiveDeref(dd, Lsuper0);
699  Cudd_RecursiveDeref(dd, Lsuper1);
700  Cudd_RecursiveDeref(dd, Ld);
701  return(NULL);
702  }
703  Cudd_Ref(Ud);
704  Cudd_RecursiveDeref(dd, Lsuper0);
705  Cudd_RecursiveDeref(dd, Lsuper1);
706 
707  Id = cuddBddIsop(dd, Ld, Ud);
708  if (Id == NULL) {
709  Cudd_RecursiveDeref(dd, Isub0);
710  Cudd_RecursiveDeref(dd, Isub1);
711  Cudd_RecursiveDeref(dd, Ld);
712  Cudd_RecursiveDeref(dd, Ud);
713  return(NULL);
714  }
715  Cudd_Ref(Id);
716  Cudd_RecursiveDeref(dd, Ld);
717  Cudd_RecursiveDeref(dd, Ud);
718 
719  x = cuddUniqueInter(dd, index, one, zero);
720  if (x == NULL) {
721  Cudd_RecursiveDeref(dd, Isub0);
722  Cudd_RecursiveDeref(dd, Isub1);
723  Cudd_RecursiveDeref(dd, Id);
724  return(NULL);
725  }
726  Cudd_Ref(x);
727  term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
728  if (term0 == NULL) {
729  Cudd_RecursiveDeref(dd, Isub0);
730  Cudd_RecursiveDeref(dd, Isub1);
731  Cudd_RecursiveDeref(dd, Id);
732  Cudd_RecursiveDeref(dd, x);
733  return(NULL);
734  }
735  Cudd_Ref(term0);
736  Cudd_RecursiveDeref(dd, Isub0);
737  term1 = cuddBddAndRecur(dd, x, Isub1);
738  if (term1 == NULL) {
739  Cudd_RecursiveDeref(dd, Isub1);
740  Cudd_RecursiveDeref(dd, Id);
741  Cudd_RecursiveDeref(dd, x);
742  Cudd_RecursiveDeref(dd, term0);
743  return(NULL);
744  }
745  Cudd_Ref(term1);
746  Cudd_RecursiveDeref(dd, x);
747  Cudd_RecursiveDeref(dd, Isub1);
748  /* sum = term0 + term1 */
749  sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
750  sum = Cudd_NotCond(sum, sum != NULL);
751  if (sum == NULL) {
752  Cudd_RecursiveDeref(dd, Id);
753  Cudd_RecursiveDeref(dd, term0);
754  Cudd_RecursiveDeref(dd, term1);
755  return(NULL);
756  }
757  Cudd_Ref(sum);
758  Cudd_RecursiveDeref(dd, term0);
759  Cudd_RecursiveDeref(dd, term1);
760  /* r = sum + Id */
761  r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
762  r = Cudd_NotCond(r, r != NULL);
763  if (r == NULL) {
764  Cudd_RecursiveDeref(dd, Id);
765  Cudd_RecursiveDeref(dd, sum);
766  return(NULL);
767  }
768  Cudd_Ref(r);
769  Cudd_RecursiveDeref(dd, sum);
770  Cudd_RecursiveDeref(dd, Id);
771 
772  cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
773 
774  Cudd_Deref(r);
775  return(r);
776 
777 } /* end of cuddBddIsop */
Cudd_T
#define Cudd_T(node)
Definition: cudd.h:440
Cudd_E
#define Cudd_E(node)
Definition: cudd.h:455
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
cuddCacheInsert2
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Definition: cuddCache.c:277
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
cuddCacheLookup2
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:502
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
one
static DdNode * one
Definition: cuddDecomp.c:112
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:818
cuddBddIsop
DdNode * cuddBddIsop(DdManager *dd, DdNode *L, DdNode *U)
Definition: cuddZddIsop.c:575
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
cuddBddAndRecur
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:886
DdManager::perm
int * perm
Definition: cuddInt.h:386
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
zero
static DdNode * zero
Definition: cuddApa.c:100
DdNode* cuddMakeBddFromZddCover ( DdManager *  dd,
DdNode *  node 
)

Function********************************************************************

Synopsis [Converts a ZDD cover to a BDD graph.]

Description [Converts a ZDD cover to a BDD graph. If successful, it returns a BDD node, otherwise it returns NULL. It is a recursive algorithm as the following. First computes 3 cofactors of a ZDD cover; f1, f0 and fd. Second, compute BDDs(b1, b0 and bd) of f1, f0 and fd. Third, compute T=b1+bd and E=b0+bd. Fourth, compute ITE(v,T,E) where v is the variable which has the index of the top node of the ZDD cover. In this case, since the index of v can be larger than either one of T or one of E, cuddUniqueInterIVO is called, here IVO stands for independent variable ordering.]

SideEffects []

SeeAlso [Cudd_MakeBddFromZddCover]

Definition at line 800 of file cuddZddIsop.c.

803 {
804  DdNode *neW;
805  int v;
806  DdNode *f1, *f0, *fd;
807  DdNode *b1, *b0, *bd;
808  DdNode *T, *E;
809 
810  statLine(dd);
811  if (node == dd->one)
812  return(dd->one);
813  if (node == dd->zero)
814  return(Cudd_Not(dd->one));
815 
816  /* Check cache */
817  neW = cuddCacheLookup1(dd, cuddMakeBddFromZddCover, node);
818  if (neW)
819  return(neW);
820 
821  v = Cudd_Regular(node)->index; /* either yi or zi */
822  if (cuddZddGetCofactors3(dd, node, v, &f1, &f0, &fd)) return(NULL);
823  Cudd_Ref(f1);
824  Cudd_Ref(f0);
825  Cudd_Ref(fd);
826 
827  b1 = cuddMakeBddFromZddCover(dd, f1);
828  if (!b1) {
829  Cudd_RecursiveDerefZdd(dd, f1);
830  Cudd_RecursiveDerefZdd(dd, f0);
831  Cudd_RecursiveDerefZdd(dd, fd);
832  return(NULL);
833  }
834  Cudd_Ref(b1);
835  b0 = cuddMakeBddFromZddCover(dd, f0);
836  if (!b0) {
837  Cudd_RecursiveDerefZdd(dd, f1);
838  Cudd_RecursiveDerefZdd(dd, f0);
839  Cudd_RecursiveDerefZdd(dd, fd);
840  Cudd_RecursiveDeref(dd, b1);
841  return(NULL);
842  }
843  Cudd_Ref(b0);
844  Cudd_RecursiveDerefZdd(dd, f1);
845  Cudd_RecursiveDerefZdd(dd, f0);
846  if (fd != dd->zero) {
847  bd = cuddMakeBddFromZddCover(dd, fd);
848  if (!bd) {
849  Cudd_RecursiveDerefZdd(dd, fd);
850  Cudd_RecursiveDeref(dd, b1);
851  Cudd_RecursiveDeref(dd, b0);
852  return(NULL);
853  }
854  Cudd_Ref(bd);
855  Cudd_RecursiveDerefZdd(dd, fd);
856 
857  T = cuddBddAndRecur(dd, Cudd_Not(b1), Cudd_Not(bd));
858  if (!T) {
859  Cudd_RecursiveDeref(dd, b1);
860  Cudd_RecursiveDeref(dd, b0);
861  Cudd_RecursiveDeref(dd, bd);
862  return(NULL);
863  }
864  T = Cudd_NotCond(T, T != NULL);
865  Cudd_Ref(T);
866  Cudd_RecursiveDeref(dd, b1);
867  E = cuddBddAndRecur(dd, Cudd_Not(b0), Cudd_Not(bd));
868  if (!E) {
869  Cudd_RecursiveDeref(dd, b0);
870  Cudd_RecursiveDeref(dd, bd);
871  Cudd_RecursiveDeref(dd, T);
872  return(NULL);
873  }
874  E = Cudd_NotCond(E, E != NULL);
875  Cudd_Ref(E);
876  Cudd_RecursiveDeref(dd, b0);
877  Cudd_RecursiveDeref(dd, bd);
878  }
879  else {
880  Cudd_RecursiveDerefZdd(dd, fd);
881  T = b1;
882  E = b0;
883  }
884 
885  if (Cudd_IsComplement(T)) {
886  neW = cuddUniqueInterIVO(dd, v / 2, Cudd_Not(T), Cudd_Not(E));
887  if (!neW) {
888  Cudd_RecursiveDeref(dd, T);
889  Cudd_RecursiveDeref(dd, E);
890  return(NULL);
891  }
892  neW = Cudd_Not(neW);
893  }
894  else {
895  neW = cuddUniqueInterIVO(dd, v / 2, T, E);
896  if (!neW) {
897  Cudd_RecursiveDeref(dd, T);
898  Cudd_RecursiveDeref(dd, E);
899  return(NULL);
900  }
901  }
902  Cudd_Ref(neW);
903  Cudd_RecursiveDeref(dd, T);
904  Cudd_RecursiveDeref(dd, E);
905 
906  cuddCacheInsert1(dd, cuddMakeBddFromZddCover, node, neW);
907  Cudd_Deref(neW);
908  return(neW);
909 
910 } /* end of cuddMakeBddFromZddCover */
Cudd_RecursiveDerefZdd
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
b1
#define b1
Definition: extraBdd.h:76
DdManager::zero
DdNode * zero
Definition: cuddInt.h:346
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
cuddMakeBddFromZddCover
DdNode * cuddMakeBddFromZddCover(DdManager *dd, DdNode *node)
Definition: cuddZddIsop.c:800
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
cuddCacheLookup1
DdNode * cuddCacheLookup1(DdManager *table, DD_CTFP1 op, DdNode *f)
Definition: cuddCache.c:556
cuddUniqueInterIVO
DdNode * cuddUniqueInterIVO(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1304
cuddZddGetCofactors3
int cuddZddGetCofactors3(DdManager *dd, DdNode *f, int v, DdNode **f1, DdNode **f0, DdNode **fd)
Definition: cuddZddFuncs.c:1360
b0
#define b0
Definition: extraBdd.h:75
DdManager::one
DdNode * one
Definition: cuddInt.h:345
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
cuddBddAndRecur
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:886
cuddCacheInsert1
void cuddCacheInsert1(DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data)
Definition: cuddCache.c:323
DdNode* cuddZddIsop ( DdManager *  dd,
DdNode *  L,
DdNode *  U,
DdNode **  zdd_I 
)

Function********************************************************************

Synopsis [Performs the recursive step of Cudd_zddIsop.]

Description []

SideEffects [None]

SeeAlso [Cudd_zddIsop]

Definition at line 234 of file cuddZddIsop.c.

239 {
240  DdNode *one = DD_ONE(dd);
241  DdNode *zero = Cudd_Not(one);
242  DdNode *zdd_one = DD_ONE(dd);
243  DdNode *zdd_zero = DD_ZERO(dd);
244  int v, top_l, top_u;
245  DdNode *Lsub0, *Usub0, *Lsub1, *Usub1, *Ld, *Ud;
246  DdNode *Lsuper0, *Usuper0, *Lsuper1, *Usuper1;
247  DdNode *Isub0, *Isub1, *Id;
248  DdNode *zdd_Isub0, *zdd_Isub1, *zdd_Id;
249  DdNode *x;
250  DdNode *term0, *term1, *sum;
251  DdNode *Lv, *Uv, *Lnv, *Unv;
252  DdNode *r, *y, *z;
253  int index;
254  DD_CTFP cacheOp;
255 
256  statLine(dd);
257  if (L == zero) {
258  *zdd_I = zdd_zero;
259  return(zero);
260  }
261  if (U == one) {
262  *zdd_I = zdd_one;
263  return(one);
264  }
265 
266  if (U == zero || L == one) {
267  printf("*** ERROR : illegal condition for ISOP (U < L).\n");
268  exit(1);
269  }
270 
271  /* Check the cache. We store two results for each recursive call.
272  ** One is the BDD, and the other is the ZDD. Both are needed.
273  ** Hence we need a double hit in the cache to terminate the
274  ** recursion. Clearly, collisions may evict only one of the two
275  ** results. */
276  cacheOp = (DD_CTFP) cuddZddIsop;
277  r = cuddCacheLookup2(dd, cuddBddIsop, L, U);
278  if (r) {
279  *zdd_I = cuddCacheLookup2Zdd(dd, cacheOp, L, U);
280  if (*zdd_I)
281  return(r);
282  else {
283  /* The BDD result may have been dead. In that case
284  ** cuddCacheLookup2 would have called cuddReclaim,
285  ** whose effects we now have to undo. */
286  cuddRef(r);
287  Cudd_RecursiveDeref(dd, r);
288  }
289  }
290 
291  top_l = dd->perm[Cudd_Regular(L)->index];
292  top_u = dd->perm[Cudd_Regular(U)->index];
293  v = ddMin(top_l, top_u);
294 
295  /* Compute cofactors. */
296  if (top_l == v) {
297  index = Cudd_Regular(L)->index;
298  Lv = Cudd_T(L);
299  Lnv = Cudd_E(L);
300  if (Cudd_IsComplement(L)) {
301  Lv = Cudd_Not(Lv);
302  Lnv = Cudd_Not(Lnv);
303  }
304  }
305  else {
306  index = Cudd_Regular(U)->index;
307  Lv = Lnv = L;
308  }
309 
310  if (top_u == v) {
311  Uv = Cudd_T(U);
312  Unv = Cudd_E(U);
313  if (Cudd_IsComplement(U)) {
314  Uv = Cudd_Not(Uv);
315  Unv = Cudd_Not(Unv);
316  }
317  }
318  else {
319  Uv = Unv = U;
320  }
321 
322  Lsub0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Uv));
323  if (Lsub0 == NULL)
324  return(NULL);
325  Cudd_Ref(Lsub0);
326  Usub0 = Unv;
327  Lsub1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Unv));
328  if (Lsub1 == NULL) {
329  Cudd_RecursiveDeref(dd, Lsub0);
330  return(NULL);
331  }
332  Cudd_Ref(Lsub1);
333  Usub1 = Uv;
334 
335  Isub0 = cuddZddIsop(dd, Lsub0, Usub0, &zdd_Isub0);
336  if (Isub0 == NULL) {
337  Cudd_RecursiveDeref(dd, Lsub0);
338  Cudd_RecursiveDeref(dd, Lsub1);
339  return(NULL);
340  }
341  /*
342  if ((!cuddIsConstant(Cudd_Regular(Isub0))) &&
343  (Cudd_Regular(Isub0)->index != zdd_Isub0->index / 2 ||
344  dd->permZ[index * 2] > dd->permZ[zdd_Isub0->index])) {
345  printf("*** ERROR : illegal permutation in ZDD. ***\n");
346  }
347  */
348  Cudd_Ref(Isub0);
349  Cudd_Ref(zdd_Isub0);
350  Isub1 = cuddZddIsop(dd, Lsub1, Usub1, &zdd_Isub1);
351  if (Isub1 == NULL) {
352  Cudd_RecursiveDeref(dd, Lsub0);
353  Cudd_RecursiveDeref(dd, Lsub1);
354  Cudd_RecursiveDeref(dd, Isub0);
355  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
356  return(NULL);
357  }
358  /*
359  if ((!cuddIsConstant(Cudd_Regular(Isub1))) &&
360  (Cudd_Regular(Isub1)->index != zdd_Isub1->index / 2 ||
361  dd->permZ[index * 2] > dd->permZ[zdd_Isub1->index])) {
362  printf("*** ERROR : illegal permutation in ZDD. ***\n");
363  }
364  */
365  Cudd_Ref(Isub1);
366  Cudd_Ref(zdd_Isub1);
367  Cudd_RecursiveDeref(dd, Lsub0);
368  Cudd_RecursiveDeref(dd, Lsub1);
369 
370  Lsuper0 = cuddBddAndRecur(dd, Lnv, Cudd_Not(Isub0));
371  if (Lsuper0 == NULL) {
372  Cudd_RecursiveDeref(dd, Isub0);
373  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
374  Cudd_RecursiveDeref(dd, Isub1);
375  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
376  return(NULL);
377  }
378  Cudd_Ref(Lsuper0);
379  Lsuper1 = cuddBddAndRecur(dd, Lv, Cudd_Not(Isub1));
380  if (Lsuper1 == NULL) {
381  Cudd_RecursiveDeref(dd, Isub0);
382  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
383  Cudd_RecursiveDeref(dd, Isub1);
384  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
385  Cudd_RecursiveDeref(dd, Lsuper0);
386  return(NULL);
387  }
388  Cudd_Ref(Lsuper1);
389  Usuper0 = Unv;
390  Usuper1 = Uv;
391 
392  /* Ld = Lsuper0 + Lsuper1 */
393  Ld = cuddBddAndRecur(dd, Cudd_Not(Lsuper0), Cudd_Not(Lsuper1));
394  if (Ld == NULL) {
395  Cudd_RecursiveDeref(dd, Isub0);
396  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
397  Cudd_RecursiveDeref(dd, Isub1);
398  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
399  Cudd_RecursiveDeref(dd, Lsuper0);
400  Cudd_RecursiveDeref(dd, Lsuper1);
401  return(NULL);
402  }
403  Ld = Cudd_Not(Ld);
404  Cudd_Ref(Ld);
405  /* Ud = Usuper0 * Usuper1 */
406  Ud = cuddBddAndRecur(dd, Usuper0, Usuper1);
407  if (Ud == NULL) {
408  Cudd_RecursiveDeref(dd, Isub0);
409  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
410  Cudd_RecursiveDeref(dd, Isub1);
411  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
412  Cudd_RecursiveDeref(dd, Lsuper0);
413  Cudd_RecursiveDeref(dd, Lsuper1);
414  Cudd_RecursiveDeref(dd, Ld);
415  return(NULL);
416  }
417  Cudd_Ref(Ud);
418  Cudd_RecursiveDeref(dd, Lsuper0);
419  Cudd_RecursiveDeref(dd, Lsuper1);
420 
421  Id = cuddZddIsop(dd, Ld, Ud, &zdd_Id);
422  if (Id == NULL) {
423  Cudd_RecursiveDeref(dd, Isub0);
424  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
425  Cudd_RecursiveDeref(dd, Isub1);
426  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
427  Cudd_RecursiveDeref(dd, Ld);
428  Cudd_RecursiveDeref(dd, Ud);
429  return(NULL);
430  }
431  /*
432  if ((!cuddIsConstant(Cudd_Regular(Id))) &&
433  (Cudd_Regular(Id)->index != zdd_Id->index / 2 ||
434  dd->permZ[index * 2] > dd->permZ[zdd_Id->index])) {
435  printf("*** ERROR : illegal permutation in ZDD. ***\n");
436  }
437  */
438  Cudd_Ref(Id);
439  Cudd_Ref(zdd_Id);
440  Cudd_RecursiveDeref(dd, Ld);
441  Cudd_RecursiveDeref(dd, Ud);
442 
443  x = cuddUniqueInter(dd, index, one, zero);
444  if (x == NULL) {
445  Cudd_RecursiveDeref(dd, Isub0);
446  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
447  Cudd_RecursiveDeref(dd, Isub1);
448  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
449  Cudd_RecursiveDeref(dd, Id);
450  Cudd_RecursiveDerefZdd(dd, zdd_Id);
451  return(NULL);
452  }
453  Cudd_Ref(x);
454  /* term0 = x * Isub0 */
455  term0 = cuddBddAndRecur(dd, Cudd_Not(x), Isub0);
456  if (term0 == NULL) {
457  Cudd_RecursiveDeref(dd, Isub0);
458  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
459  Cudd_RecursiveDeref(dd, Isub1);
460  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
461  Cudd_RecursiveDeref(dd, Id);
462  Cudd_RecursiveDerefZdd(dd, zdd_Id);
463  Cudd_RecursiveDeref(dd, x);
464  return(NULL);
465  }
466  Cudd_Ref(term0);
467  Cudd_RecursiveDeref(dd, Isub0);
468  /* term1 = x * Isub1 */
469  term1 = cuddBddAndRecur(dd, x, Isub1);
470  if (term1 == NULL) {
471  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
472  Cudd_RecursiveDeref(dd, Isub1);
473  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
474  Cudd_RecursiveDeref(dd, Id);
475  Cudd_RecursiveDerefZdd(dd, zdd_Id);
476  Cudd_RecursiveDeref(dd, x);
477  Cudd_RecursiveDeref(dd, term0);
478  return(NULL);
479  }
480  Cudd_Ref(term1);
481  Cudd_RecursiveDeref(dd, x);
482  Cudd_RecursiveDeref(dd, Isub1);
483  /* sum = term0 + term1 */
484  sum = cuddBddAndRecur(dd, Cudd_Not(term0), Cudd_Not(term1));
485  if (sum == NULL) {
486  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
487  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
488  Cudd_RecursiveDeref(dd, Id);
489  Cudd_RecursiveDerefZdd(dd, zdd_Id);
490  Cudd_RecursiveDeref(dd, term0);
491  Cudd_RecursiveDeref(dd, term1);
492  return(NULL);
493  }
494  sum = Cudd_Not(sum);
495  Cudd_Ref(sum);
496  Cudd_RecursiveDeref(dd, term0);
497  Cudd_RecursiveDeref(dd, term1);
498  /* r = sum + Id */
499  r = cuddBddAndRecur(dd, Cudd_Not(sum), Cudd_Not(Id));
500  r = Cudd_NotCond(r, r != NULL);
501  if (r == NULL) {
502  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
503  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
504  Cudd_RecursiveDeref(dd, Id);
505  Cudd_RecursiveDerefZdd(dd, zdd_Id);
506  Cudd_RecursiveDeref(dd, sum);
507  return(NULL);
508  }
509  Cudd_Ref(r);
510  Cudd_RecursiveDeref(dd, sum);
511  Cudd_RecursiveDeref(dd, Id);
512 
513  if (zdd_Isub0 != zdd_zero) {
514  z = cuddZddGetNodeIVO(dd, index * 2 + 1, zdd_Isub0, zdd_Id);
515  if (z == NULL) {
516  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
517  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
518  Cudd_RecursiveDerefZdd(dd, zdd_Id);
519  Cudd_RecursiveDeref(dd, r);
520  return(NULL);
521  }
522  }
523  else {
524  z = zdd_Id;
525  }
526  Cudd_Ref(z);
527  if (zdd_Isub1 != zdd_zero) {
528  y = cuddZddGetNodeIVO(dd, index * 2, zdd_Isub1, z);
529  if (y == NULL) {
530  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
531  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
532  Cudd_RecursiveDerefZdd(dd, zdd_Id);
533  Cudd_RecursiveDeref(dd, r);
534  Cudd_RecursiveDerefZdd(dd, z);
535  return(NULL);
536  }
537  }
538  else
539  y = z;
540  Cudd_Ref(y);
541 
542  Cudd_RecursiveDerefZdd(dd, zdd_Isub0);
543  Cudd_RecursiveDerefZdd(dd, zdd_Isub1);
544  Cudd_RecursiveDerefZdd(dd, zdd_Id);
545  Cudd_RecursiveDerefZdd(dd, z);
546 
547  cuddCacheInsert2(dd, cuddBddIsop, L, U, r);
548  cuddCacheInsert2(dd, cacheOp, L, U, y);
549 
550  Cudd_Deref(r);
551  Cudd_Deref(y);
552  *zdd_I = y;
553  /*
554  if (Cudd_Regular(r)->index != y->index / 2) {
555  printf("*** ERROR : mismatch in indices between BDD and ZDD. ***\n");
556  }
557  */
558  return(r);
559 
560 } /* end of cuddZddIsop */
cuddZddGetNodeIVO
DdNode * cuddZddGetNodeIVO(DdManager *dd, int index, DdNode *g, DdNode *h)
Definition: cuddTable.c:1074
cuddCacheLookup2Zdd
DdNode * cuddCacheLookup2Zdd(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:610
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
exit
VOID_HACK exit()
Cudd_RecursiveDerefZdd
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
Cudd_T
#define Cudd_T(node)
Definition: cudd.h:440
Cudd_E
#define Cudd_E(node)
Definition: cudd.h:455
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
cuddCacheInsert2
void cuddCacheInsert2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g, DdNode *data)
Definition: cuddCache.c:277
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
DD_CTFP
DdNode *(* DD_CTFP)(DdManager *, DdNode *, DdNode *)
Definition: cudd.h:321
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
cuddZddIsop
DdNode * cuddZddIsop(DdManager *dd, DdNode *L, DdNode *U, DdNode **zdd_I)
Definition: cuddZddIsop.c:234
cuddCacheLookup2
DdNode * cuddCacheLookup2(DdManager *table, DD_CTFP op, DdNode *f, DdNode *g)
Definition: cuddCache.c:502
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
one
static DdNode * one
Definition: cuddDecomp.c:112
ddMin
#define ddMin(x, y)
Definition: cuddInt.h:818
cuddBddIsop
DdNode * cuddBddIsop(DdManager *dd, DdNode *L, DdNode *U)
Definition: cuddZddIsop.c:575
Cudd_NotCond
#define Cudd_NotCond(node, c)
Definition: cudd.h:383
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
cuddBddAndRecur
DdNode * cuddBddAndRecur(DdManager *manager, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:886
DdManager::perm
int * perm
Definition: cuddInt.h:386
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
zero
static DdNode * zero
Definition: cuddApa.c:100
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927

Variable Documentation

ABC_NAMESPACE_IMPL_START char rcsid [] DD_UNUSED = "$Id: cuddZddIsop.c,v 1.20 2009/02/19 16:26:12 fabio Exp $"
static

CFile***********************************************************************

FileName [cuddZddIsop.c]

PackageName [cudd]

Synopsis [Functions to find irredundant SOP covers as ZDDs from BDDs.]

Description [External procedures included in this module:

Internal procedures included in this module:

Static procedures included in this module:

]

SeeAlso []

Author [In-Ho Moon]

Copyright [Copyright (c) 1995-2004, Regents of the University of Colorado

All rights reserved.

Redistribution and use in source and binary forms, with or without modification, are permitted provided that the following conditions are met:

Redistributions of source code must retain the above copyright notice, this list of conditions and the following disclaimer.

Redistributions in binary form must reproduce the above copyright notice, this list of conditions and the following disclaimer in the documentation and/or other materials provided with the distribution.

Neither the name of the University of Colorado nor the names of its contributors may be used to endorse or promote products derived from this software without specific prior written permission.

THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.]

Definition at line 91 of file cuddZddIsop.c.