summaryrefslogtreecommitdiffstats
path: root/src/misc
diff options
context:
space:
mode:
Diffstat (limited to 'src/misc')
-rw-r--r--src/misc/extra/extra.h2
-rw-r--r--src/misc/extra/extraBddMisc.c141
-rw-r--r--src/misc/hash/hashFlt.h5
-rw-r--r--src/misc/hash/hashPtr.h12
4 files changed, 152 insertions, 8 deletions
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 96ff6072..33303fac 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -196,6 +196,8 @@ extern DdNode * Extra_bddCreateExor( DdManager * dd, int nVars );
extern DdNode * Extra_zddPrimes( DdManager * dd, DdNode * F );
extern void Extra_bddPermuteArray( DdManager * dd, DdNode ** bNodesIn, DdNode ** bNodesOut, int nNodes, int *permut );
extern DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars );
+extern DdNode * Extra_bddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
+extern DdNode * extraBddChangePolarity( DdManager * dd, DdNode * bFunc, DdNode * bVars );
#ifndef ABC_PRB
#define ABC_PRB(dd,f) printf("%s = ", #f); Extra_bddPrint(dd,f); printf("\n")
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index cdded9b8..69309a4d 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -1013,6 +1013,32 @@ DdNode * Extra_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars )
return bRes;
}
+/**Function********************************************************************
+
+ Synopsis [Changes the polarity of vars listed in the cube.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+DdNode * Extra_bddChangePolarity(
+ DdManager * dd, /* the DD manager */
+ DdNode * bFunc,
+ DdNode * bVars)
+{
+ DdNode *res;
+ do {
+ dd->reordered = 0;
+ res = extraBddChangePolarity( dd, bFunc, bVars );
+ } while (dd->reordered == 1);
+ return(res);
+
+} /* end of Extra_bddChangePolarity */
+
+
/*---------------------------------------------------------------------------*/
/* Definition of internal functions */
/*---------------------------------------------------------------------------*/
@@ -1659,6 +1685,121 @@ cuddBddPermuteRecur( DdManager * manager /* DD manager */ ,
} /* end of cuddBddPermuteRecur */
+/**Function********************************************************************
+
+ Synopsis [Performs the reordering-sensitive step of Extra_bddChangePolarity().]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+DdNode * extraBddChangePolarity(
+ DdManager * dd, /* the DD manager */
+ DdNode * bFunc,
+ DdNode * bVars)
+{
+ DdNode * bRes;
+
+ if ( bVars == b1 )
+ return bFunc;
+ if ( Cudd_IsConstant(bFunc) )
+ return bFunc;
+
+ if ( bRes = cuddCacheLookup2(dd, extraBddChangePolarity, bFunc, bVars) )
+ return bRes;
+ else
+ {
+ DdNode * bFR = Cudd_Regular(bFunc);
+ int LevelF = dd->perm[bFR->index];
+ int LevelV = dd->perm[bVars->index];
+
+ if ( LevelV < LevelF )
+ bRes = extraBddChangePolarity( dd, bFunc, cuddT(bVars) );
+ else // if ( LevelF <= LevelV )
+ {
+ DdNode * bRes0, * bRes1;
+ DdNode * bF0, * bF1;
+ DdNode * bVarsNext;
+
+ // cofactor the functions
+ if ( bFR != bFunc ) // bFunc is complemented
+ {
+ bF0 = Cudd_Not( cuddE(bFR) );
+ bF1 = Cudd_Not( cuddT(bFR) );
+ }
+ else
+ {
+ bF0 = cuddE(bFR);
+ bF1 = cuddT(bFR);
+ }
+
+ if ( LevelF == LevelV )
+ bVarsNext = cuddT(bVars);
+ else
+ bVarsNext = bVars;
+
+ bRes0 = extraBddChangePolarity( dd, bF0, bVarsNext );
+ if ( bRes0 == NULL )
+ return NULL;
+ cuddRef( bRes0 );
+
+ bRes1 = extraBddChangePolarity( dd, bF1, bVarsNext );
+ if ( bRes1 == NULL )
+ {
+ Cudd_RecursiveDeref( dd, bRes0 );
+ return NULL;
+ }
+ cuddRef( bRes1 );
+
+ if ( LevelF == LevelV )
+ { // swap the cofactors
+ DdNode * bTemp;
+ bTemp = bRes0;
+ bRes0 = bRes1;
+ bRes1 = bTemp;
+ }
+
+ /* only aRes0 and aRes1 are referenced at this point */
+
+ /* consider the case when Res0 and Res1 are the same node */
+ if ( bRes0 == bRes1 )
+ bRes = bRes1;
+ /* consider the case when Res1 is complemented */
+ else if ( Cudd_IsComplement(bRes1) )
+ {
+ bRes = cuddUniqueInter(dd, bFR->index, Cudd_Not(bRes1), Cudd_Not(bRes0));
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref(dd,bRes0);
+ Cudd_RecursiveDeref(dd,bRes1);
+ return NULL;
+ }
+ bRes = Cudd_Not(bRes);
+ }
+ else
+ {
+ bRes = cuddUniqueInter( dd, bFR->index, bRes1, bRes0 );
+ if ( bRes == NULL )
+ {
+ Cudd_RecursiveDeref(dd,bRes0);
+ Cudd_RecursiveDeref(dd,bRes1);
+ return NULL;
+ }
+ }
+ cuddDeref( bRes0 );
+ cuddDeref( bRes1 );
+ }
+
+ /* insert the result into cache */
+ cuddCacheInsert2(dd, extraBddChangePolarity, bFunc, bVars, bRes);
+ return bRes;
+ }
+} /* end of extraBddChangePolarity */
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/hash/hashFlt.h b/src/misc/hash/hashFlt.h
index b4a8fb49..74e8503d 100644
--- a/src/misc/hash/hashFlt.h
+++ b/src/misc/hash/hashFlt.h
@@ -311,14 +311,15 @@ static inline void Hash_FltRemove( Hash_Flt_t *p, int key )
***********************************************************************/
static inline void Hash_FltFree( Hash_Flt_t *p ) {
int bin;
- Hash_Flt_Entry_t *pEntry;
+ Hash_Flt_Entry_t *pEntry, *pTemp;
// free bins
for(bin = 0; bin < p->nBins; bin++) {
pEntry = p->pArray[bin];
while(pEntry) {
+ pTemp = pEntry;
pEntry = pEntry->pNext;
- ABC_FREE( pEntry );
+ ABC_FREE( pTemp );
}
}
diff --git a/src/misc/hash/hashPtr.h b/src/misc/hash/hashPtr.h
index 9e510866..a10fb548 100644
--- a/src/misc/hash/hashPtr.h
+++ b/src/misc/hash/hashPtr.h
@@ -115,19 +115,17 @@ static inline Hash_Ptr_t * Hash_PtrAlloc( int nBins )
static inline int Hash_PtrExists( Hash_Ptr_t *p, int key )
{
int bin;
- Hash_Ptr_Entry_t *pEntry, **pLast;
+ Hash_Ptr_Entry_t *pEntry;
// find the bin where this key would live
bin = (*(p->fHash))(key, p->nBins);
// search for key
- pLast = &(p->pArray[bin]);
pEntry = p->pArray[bin];
while(pEntry) {
if (pEntry->key == key) {
return 1;
}
- pLast = &(pEntry->pNext);
pEntry = pEntry->pNext;
}
@@ -310,16 +308,18 @@ static inline void* Hash_PtrRemove( Hash_Ptr_t *p, int key )
SeeAlso []
***********************************************************************/
-static inline void Hash_PtrFree( Hash_Ptr_t *p ) {
+static inline void Hash_PtrFree( Hash_Ptr_t *p )
+{
int bin;
- Hash_Ptr_Entry_t *pEntry;
+ Hash_Ptr_Entry_t *pEntry, *pTemp;
// free bins
for(bin = 0; bin < p->nBins; bin++) {
pEntry = p->pArray[bin];
while(pEntry) {
+ pTemp = pEntry;
pEntry = pEntry->pNext;
- ABC_FREE( pEntry );
+ ABC_FREE( pTemp );
}
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-11 16:14:26 +0000