From feb8fb692e09a2fc7c1da4f2fcf605d398e940f2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 28 Apr 2007 08:01:00 -0700 Subject: Version abc70428 --- src/opt/kit/kit.h | 1 + src/opt/kit/kitDsd.c | 6 +++--- src/opt/kit/kitTruth.c | 55 ++++++++++++++++++++++++++++++++++++++++++++++++++ 3 files changed, 59 insertions(+), 3 deletions(-) (limited to 'src/opt') diff --git a/src/opt/kit/kit.h b/src/opt/kit/kit.h index 9e7d2bf1..4535244b 100644 --- a/src/opt/kit/kit.h +++ b/src/opt/kit/kit.h @@ -477,6 +477,7 @@ extern void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, in extern void Kit_TruthForall( unsigned * pTruth, int nVars, int iVar ); extern void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar ); extern void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask ); +extern void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar ); extern void Kit_TruthMux( unsigned * pOut, unsigned * pCof0, unsigned * pCof1, int nVars, int iVar ); extern void Kit_TruthChangePhase( unsigned * pTruth, int nVars, int iVar ); extern int Kit_TruthMinCofSuppOverlap( unsigned * pTruth, int nVars, int * pVarMin ); diff --git a/src/opt/kit/kitDsd.c b/src/opt/kit/kitDsd.c index 62ee653b..4bf8d7ef 100644 --- a/src/opt/kit/kitDsd.c +++ b/src/opt/kit/kitDsd.c @@ -1068,7 +1068,7 @@ int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit ) // Kit_DsdObj_t * pRoot; unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) }; unsigned i, * pTruth; - int fVerbose = 0; + int fVerbose = 1; int RetValue = 0; pTruth = pTruthInit; @@ -1108,8 +1108,8 @@ int Kit_DsdTestCofs( Kit_DsdNtk_t * pNtk, unsigned * pTruthInit ) Kit_DsdPrint( stdout, pNtk1 ); } - if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) ) - RetValue = 1; +// if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) ) +// RetValue = 1; Kit_DsdNtkFree( pNtk0 ); Kit_DsdNtkFree( pNtk1 ); diff --git a/src/opt/kit/kitTruth.c b/src/opt/kit/kitTruth.c index 64a6a052..73264661 100644 --- a/src/opt/kit/kitTruth.c +++ b/src/opt/kit/kitTruth.c @@ -767,6 +767,61 @@ void Kit_TruthForallNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar } } +/**Function************************************************************* + + Synopsis [Universally quantifies the variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Kit_TruthUniqueNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar ) +{ + int nWords = Kit_TruthWordNum( nVars ); + int i, k, Step; + + assert( iVar < nVars ); + switch ( iVar ) + { + case 0: + for ( i = 0; i < nWords; i++ ) + pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xAAAAAAAA) >> 1) | ((pTruth[i] & 0x55555555) << 1)); + return; + case 1: + for ( i = 0; i < nWords; i++ ) + pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xCCCCCCCC) >> 2) | ((pTruth[i] & 0x33333333) << 2)); + return; + case 2: + for ( i = 0; i < nWords; i++ ) + pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xF0F0F0F0) >> 4) | ((pTruth[i] & 0x0F0F0F0F) << 4)); + return; + case 3: + for ( i = 0; i < nWords; i++ ) + pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xFF00FF00) >> 8) | ((pTruth[i] & 0x00FF00FF) << 8)); + return; + case 4: + for ( i = 0; i < nWords; i++ ) + pRes[i] = pTruth[i] ^ (((pTruth[i] & 0xFFFF0000) >> 16) | ((pTruth[i] & 0x0000FFFF) << 16)); + return; + default: + Step = (1 << (iVar - 5)); + for ( k = 0; k < nWords; k += 2*Step ) + { + for ( i = 0; i < Step; i++ ) + { + pRes[i] = pTruth[i] ^ pTruth[Step+i]; + pRes[Step+i] = pRes[i]; + } + pRes += 2*Step; + pTruth += 2*Step; + } + return; + } +} + /**Function************************************************************* Synopsis [Universally quantifies the set of variables.] -- cgit v1.2.3