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

Go to the source code of this file.

Functions

static DdNode * zddPortFromBddStep (DdManager *dd, DdNode *B, int expected)
 
static DdNode * zddPortToBddStep (DdManager *dd, DdNode *f, int depth)
 
DdNode * Cudd_zddPortFromBdd (DdManager *dd, DdNode *B)
 
DdNode * Cudd_zddPortToBdd (DdManager *dd, DdNode *f)
 

Variables

static
ABC_NAMESPACE_IMPL_START char
rcsid[] 		DD_UNUSED = "$Id: cuddZddPort.c,v 1.13 2004/08/13 18:04:53 fabio Exp $"
 

Function Documentation

DdNode* Cudd_zddPortFromBdd ( DdManager *  dd,
DdNode *  B 
)

AutomaticEnd Function********************************************************************

Synopsis [Converts a BDD into a ZDD.]

Description [Converts a BDD into a ZDD. This function assumes that there is a one-to-one correspondence between the BDD variables and the ZDD variables, and that the variable order is the same for both types of variables. These conditions are established if the ZDD variables are created by one call to Cudd_zddVarsFromBddVars with multiplicity =

  1. Returns a pointer to the resulting ZDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_zddVarsFromBddVars]

Definition at line 131 of file cuddZddPort.c.

134 {
135  DdNode *res;
136 
137  do {
138  dd->reordered = 0;
139  res = zddPortFromBddStep(dd,B,0);
140  } while (dd->reordered == 1);
141 
142  return(res);
143 
144 } /* end of Cudd_zddPortFromBdd */
zddPortFromBddStep
static DdNode * zddPortFromBddStep(DdManager *dd, DdNode *B, int expected)
Definition: cuddZddPort.c:197
DdNode
Definition: cudd.h:278
DdManager::reordered
int reordered
Definition: cuddInt.h:409
DdNode* Cudd_zddPortToBdd ( DdManager *  dd,
DdNode *  f 
)

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

Synopsis [Converts a ZDD into a BDD.]

Description [Converts a ZDD into a BDD. Returns a pointer to the resulting ZDD if successful; NULL otherwise.]

SideEffects [None]

SeeAlso [Cudd_zddPortFromBdd]

Definition at line 160 of file cuddZddPort.c.

163 {
164  DdNode *res;
165 
166  do {
167  dd->reordered = 0;
168  res = zddPortToBddStep(dd,f,0);
169  } while (dd->reordered == 1);
170 
171  return(res);
172 
173 } /* end of Cudd_zddPortToBdd */
DdNode
Definition: cudd.h:278
zddPortToBddStep
static DdNode * zddPortToBddStep(DdManager *dd, DdNode *f, int depth)
Definition: cuddZddPort.c:305
DdManager::reordered
int reordered
Definition: cuddInt.h:409
static DdNode * zddPortFromBddStep ( DdManager *  dd,
DdNode *  B,
int  expected 
)
static

AutomaticStart

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

Synopsis [Performs the recursive step of Cudd_zddPortFromBdd.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 197 of file cuddZddPort.c.

201 {
202  DdNode *res, *prevZdd, *t, *e;
203  DdNode *Breg, *Bt, *Be;
204  int id, level;
205 
206  statLine(dd);
207  /* Terminal cases. */
208  if (B == Cudd_Not(DD_ONE(dd)))
209  return(DD_ZERO(dd));
210  if (B == DD_ONE(dd)) {
211  if (expected >= dd->sizeZ) {
212  return(DD_ONE(dd));
213  } else {
214  return(dd->univ[expected]);
215  }
216  }
217 
218  Breg = Cudd_Regular(B);
219 
220  /* Computed table look-up. */
221  res = cuddCacheLookup1Zdd(dd,Cudd_zddPortFromBdd,B);
222  if (res != NULL) {
223  level = cuddI(dd,Breg->index);
224  /* Adding DC vars. */
225  if (expected < level) {
226  /* Add suppressed variables. */
227  cuddRef(res);
228  for (level--; level >= expected; level--) {
229  prevZdd = res;
230  id = dd->invperm[level];
231  res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
232  if (res == NULL) {
233  Cudd_RecursiveDerefZdd(dd, prevZdd);
234  return(NULL);
235  }
236  cuddRef(res);
237  Cudd_RecursiveDerefZdd(dd, prevZdd);
238  }
239  cuddDeref(res);
240  }
241  return(res);
242  } /* end of cache look-up */
243 
244  if (Cudd_IsComplement(B)) {
245  Bt = Cudd_Not(cuddT(Breg));
246  Be = Cudd_Not(cuddE(Breg));
247  } else {
248  Bt = cuddT(Breg);
249  Be = cuddE(Breg);
250  }
251 
252  id = Breg->index;
253  level = cuddI(dd,id);
254  t = zddPortFromBddStep(dd, Bt, level+1);
255  if (t == NULL) return(NULL);
256  cuddRef(t);
257  e = zddPortFromBddStep(dd, Be, level+1);
258  if (e == NULL) {
259  Cudd_RecursiveDerefZdd(dd, t);
260  return(NULL);
261  }
262  cuddRef(e);
263  res = cuddZddGetNode(dd, id, t, e);
264  if (res == NULL) {
265  Cudd_RecursiveDerefZdd(dd, t);
266  Cudd_RecursiveDerefZdd(dd, e);
267  return(NULL);
268  }
269  cuddRef(res);
270  Cudd_RecursiveDerefZdd(dd, t);
271  Cudd_RecursiveDerefZdd(dd, e);
272 
273  cuddCacheInsert1(dd,Cudd_zddPortFromBdd,B,res);
274 
275  for (level--; level >= expected; level--) {
276  prevZdd = res;
277  id = dd->invperm[level];
278  res = cuddZddGetNode(dd, id, prevZdd, prevZdd);
279  if (res == NULL) {
280  Cudd_RecursiveDerefZdd(dd, prevZdd);
281  return(NULL);
282  }
283  cuddRef(res);
284  Cudd_RecursiveDerefZdd(dd, prevZdd);
285  }
286 
287  cuddDeref(res);
288  return(res);
289 
290 } /* end of zddPortFromBddStep */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
Cudd_RecursiveDerefZdd
void Cudd_RecursiveDerefZdd(DdManager *table, DdNode *n)
Definition: cuddRef.c:385
zddPortFromBddStep
static DdNode * zddPortFromBddStep(DdManager *dd, DdNode *B, int expected)
Definition: cuddZddPort.c:197
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
DdNode
Definition: cudd.h:278
cuddZddGetNode
DdNode * cuddZddGetNode(DdManager *zdd, int id, DdNode *T, DdNode *E)
Definition: cuddTable.c:1041
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Cudd_Regular
#define Cudd_Regular(node)
Definition: cudd.h:397
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
Cudd_zddPortFromBdd
DdNode * Cudd_zddPortFromBdd(DdManager *dd, DdNode *B)
Definition: cuddZddPort.c:131
Cudd_IsComplement
#define Cudd_IsComplement(node)
Definition: cudd.h:425
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
cuddI
#define cuddI(dd, index)
Definition: cuddInt.h:686
DdManager::sizeZ
int sizeZ
Definition: cuddInt.h:362
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
DdManager::invperm
int * invperm
Definition: cuddInt.h:388
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
cuddCacheLookup1Zdd
DdNode * cuddCacheLookup1Zdd(DdManager *table, DD_CTFP1 op, DdNode *f)
Definition: cuddCache.c:664
cuddCacheInsert1
void cuddCacheInsert1(DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data)
Definition: cuddCache.c:323
DdManager::univ
DdNode ** univ
Definition: cuddInt.h:392
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
static DdNode * zddPortToBddStep ( DdManager *  dd,
DdNode *  f,
int  depth 
)
static

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

Synopsis [Performs the recursive step of Cudd_zddPortToBdd.]

Description []

SideEffects [None]

SeeAlso []

Definition at line 305 of file cuddZddPort.c.

309 {
310  DdNode *one, *zero, *T, *E, *res, *var;
311  unsigned int index;
312  unsigned int level;
313 
314  statLine(dd);
315  one = DD_ONE(dd);
316  zero = DD_ZERO(dd);
317  if (f == zero) return(Cudd_Not(one));
318 
319  if (depth == dd->sizeZ) return(one);
320 
321  index = dd->invpermZ[depth];
322  level = cuddIZ(dd,f->index);
323  var = cuddUniqueInter(dd,index,one,Cudd_Not(one));
324  if (var == NULL) return(NULL);
325  cuddRef(var);
326 
327  if (level > (unsigned) depth) {
328  E = zddPortToBddStep(dd,f,depth+1);
329  if (E == NULL) {
330  Cudd_RecursiveDeref(dd,var);
331  return(NULL);
332  }
333  cuddRef(E);
334  res = cuddBddIteRecur(dd,var,Cudd_Not(one),E);
335  if (res == NULL) {
336  Cudd_RecursiveDeref(dd,var);
337  Cudd_RecursiveDeref(dd,E);
338  return(NULL);
339  }
340  cuddRef(res);
341  Cudd_RecursiveDeref(dd,var);
342  Cudd_RecursiveDeref(dd,E);
343  cuddDeref(res);
344  return(res);
345  }
346 
347  res = cuddCacheLookup1(dd,Cudd_zddPortToBdd,f);
348  if (res != NULL) {
349  Cudd_RecursiveDeref(dd,var);
350  return(res);
351  }
352 
353  T = zddPortToBddStep(dd,cuddT(f),depth+1);
354  if (T == NULL) {
355  Cudd_RecursiveDeref(dd,var);
356  return(NULL);
357  }
358  cuddRef(T);
359  E = zddPortToBddStep(dd,cuddE(f),depth+1);
360  if (E == NULL) {
361  Cudd_RecursiveDeref(dd,var);
362  Cudd_RecursiveDeref(dd,T);
363  return(NULL);
364  }
365  cuddRef(E);
366 
367  res = cuddBddIteRecur(dd,var,T,E);
368  if (res == NULL) {
369  Cudd_RecursiveDeref(dd,var);
370  Cudd_RecursiveDeref(dd,T);
371  Cudd_RecursiveDeref(dd,E);
372  return(NULL);
373  }
374  cuddRef(res);
375  Cudd_RecursiveDeref(dd,var);
376  Cudd_RecursiveDeref(dd,T);
377  Cudd_RecursiveDeref(dd,E);
378  cuddDeref(res);
379 
380  cuddCacheInsert1(dd,Cudd_zddPortToBdd,f,res);
381 
382  return(res);
383 
384 } /* end of zddPortToBddStep */
cuddRef
#define cuddRef(n)
Definition: cuddInt.h:584
cuddDeref
#define cuddDeref(n)
Definition: cuddInt.h:604
cuddIZ
#define cuddIZ(dd, index)
Definition: cuddInt.h:704
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
DdManager::invpermZ
int * invpermZ
Definition: cuddInt.h:389
Minisat::var
int var(Lit p)
Definition: SolverTypes.h:62
zddPortToBddStep
static DdNode * zddPortToBddStep(DdManager *dd, DdNode *f, int depth)
Definition: cuddZddPort.c:305
statLine
#define statLine(dd)
Definition: cuddInt.h:1037
cuddCacheLookup1
DdNode * cuddCacheLookup1(DdManager *table, DD_CTFP1 op, DdNode *f)
Definition: cuddCache.c:556
one
static DdNode * one
Definition: cuddDecomp.c:112
cuddT
#define cuddT(node)
Definition: cuddInt.h:636
DdManager::sizeZ
int sizeZ
Definition: cuddInt.h:362
DdNode::index
DdHalfWord index
Definition: cudd.h:279
cuddE
#define cuddE(node)
Definition: cuddInt.h:652
DD_ONE
#define DD_ONE(dd)
Definition: cuddInt.h:911
cuddUniqueInter
DdNode * cuddUniqueInter(DdManager *unique, int index, DdNode *T, DdNode *E)
Definition: cuddTable.c:1128
zero
static DdNode * zero
Definition: cuddApa.c:100
cuddCacheInsert1
void cuddCacheInsert1(DdManager *table, DD_CTFP1 op, DdNode *f, DdNode *data)
Definition: cuddCache.c:323
Cudd_zddPortToBdd
DdNode * Cudd_zddPortToBdd(DdManager *dd, DdNode *f)
Definition: cuddZddPort.c:160
DD_ZERO
#define DD_ZERO(dd)
Definition: cuddInt.h:927
cuddBddIteRecur
DdNode * cuddBddIteRecur(DdManager *dd, DdNode *f, DdNode *g, DdNode *h)
Definition: cuddBddIte.c:633

Variable Documentation

ABC_NAMESPACE_IMPL_START char rcsid [] DD_UNUSED = "$Id: cuddZddPort.c,v 1.13 2004/08/13 18:04:53 fabio Exp $"
static

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

FileName [cuddZddPort.c]

PackageName [cudd]

Synopsis [Functions that translate BDDs to ZDDs.]

Description [External procedures included in this module:

Internal procedures included in this module:

Static procedures included in this module:

]

SeeAlso []

Author [Hyong-kyoon Shin, 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 89 of file cuddZddPort.c.