/**CFile****************************************************************
FileName [dauDsd.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [DAG-aware unmapping.]
Synopsis [Disjoint-support decomposition.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: dauDsd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "dauInt.h"
#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*
This code performs truth-table-based decomposition for 6-variable functions.
Representation of operations:
! = not;
(ab) = a and b;
[ab] = a xor b;
<abc> = ITE( a, b, c )
FUNCTION{abc} = FUNCTION( a, b, c )
*/
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Elementary truth tables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline word ** Dau_DsdTtElems()
{
static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR+1] = {NULL};
if ( pTtElems[0] == NULL )
{
int v;
for ( v = 0; v <= DAU_MAX_VAR; v++ )
pTtElems[v] = TtElems[v];
Abc_TtElemInit( pTtElems, DAU_MAX_VAR );
}
return pTtElems;
}
/**Function*************************************************************
Synopsis [DSD formula manipulation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int * Dau_DsdComputeMatches( char * p )
{
static int pMatches[DAU_MAX_STR];
int pNested[DAU_MAX_VAR];
int v, nNested = 0;
for ( v = 0; p[v]; v++ )
{
pMatches[v] = 0;
if ( p[v] == '(' || p[v] == '[' || p[v] == '<' || p[v] == '{' )
pNested[nNested++] = v;
else if ( p[v] == ')' || p[v] == ']' || p[v] == '>' || p[v] == '}' )
pMatches[pNested[--nNested]] = v;
assert( nNested < DAU_MAX_VAR );
}
assert( nNested == 0 );
return pMatches;
}
/**Function*************************************************************
Synopsis [Generate random permutation.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dau_DsdFindVarNum( char * pDsd )
{
int vMax = 0;
pDsd--;
while ( *++pDsd )
if ( *pDsd >= 'a' && *pDsd <= 'z' )
vMax = Abc_MaxInt( vMax, *pDsd - 'a' );
return vMax + 1;
}
void Dau_DsdGenRandPerm( int * pPerm, int nVars )
{
int v, vNew;
for ( v = 0; v < nVars; v++ )
pPerm[v] = v;
for ( v = 0; v < nVars; v++ )
{
vNew = rand() % nVars;
ABC_SWAP( int, pPerm[v], pPerm[vNew] );
}
}
void Dau_DsdPermute( char * pDsd )
{
int pPerm[16];
int nVars = Dau_DsdFindVarNum( pDsd );
Dau_DsdGenRandPerm( pPerm, nVars );
pDsd--;
while ( *++pDsd )
if ( *pDsd >= 'a' && *pDsd < 'a' + nVars )
*pDsd = 'a' + pPerm[*pDsd - 'a'];
}
/**Function*************************************************************
Synopsis [Normalize the ordering of components.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
char * Dau_DsdNormalizeCopy( char * pDest, char * pSour, int * pMarks, int i )
{
int s;
for ( s = pMarks[i]; s < pMarks[i+1]; s++ )
*pDest++ = pSour[s];
return pDest;
}
int Dau_DsdNormalizeCompare( char * pStr, int * pMarks, int i, int j )
{
char * pStr1 = pStr + pMarks[i];
char * pStr2 = pStr + pMarks[j];
char * pLimit1 = pStr + pMarks[i+1];
char * pLimit2 = pStr + pMarks[j+1];
for ( ; pStr1 < pLimit1 && pStr2 < pLimit2; pStr1++, pStr2++ )
{
if ( !(*pStr1 >= 'a' && *pStr1 <= 'z') )
{
pStr2--;
continue;
}
if ( !(*pStr2 >= 'a' && *pStr2 <= 'z') )
{
pStr1--;
continue;
}
if ( *pStr1 < *pStr2 )
return -1;
if ( *pStr1 > *pStr2 )
return 1;
}
assert( pStr1 < pLimit1 || pStr2 < pLimit2 );
if ( pStr1 == pLimit1 )
return -1;
if ( pStr2 == pLimit2 )
return 1;
assert( 0 );
return 0;
}
int * Dau_DsdNormalizePerm( char * pStr, int * pMarks, int nMarks )
{
static int pPerm[DAU_MAX_VAR];
int i, k;
for ( i = 0; i < nMarks; i++ )
pPerm[i] = i;
for ( i = 0; i < nMarks; i++ )
{
int iBest = i;
for ( k = i + 1; k < nMarks; k++ )
if ( Dau_DsdNormalizeCompare( pStr, pMarks, pPerm[iBest], pPerm[k] ) == 1 )
iBest = k;
ABC_SWAP( int, pPerm[i], pPerm[iBest] );
}
return pPerm;
}
void Dau_DsdNormalize_rec( char * pStr, char ** p, int * pMatches )
{
static char pBuffer[DAU_MAX_STR];
if ( **p == '!' )
(*p)++;
while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
(*p)++;
if ( **p == '<' )
{
char * q = pStr + pMatches[*p - pStr];
if ( *(q+1) == '{' )
*p = q+1;
}
if ( **p >= 'a' && **p <= 'z' ) // var
return;
if ( **p == '(' || **p == '[' ) // and/or/xor
{
char * pStore, * pOld = *p + 1;
char * q = pStr + pMatches[ *p - pStr ];
int i, * pPerm, nMarks = 0, pMarks[DAU_MAX_VAR+1];
assert( *q == **p + 1 + (**p != '(') );
for ( (*p)++; *p < q; (*p)++ )
{
pMarks[nMarks++] = *p - pStr;
Dau_DsdNormalize_rec( pStr, p, pMatches );
}
pMarks[nMarks] = *p - pStr;
assert( *p == q );
// add to buffer in good order
pPerm = Dau_DsdNormalizePerm( pStr, pMarks, nMarks );
// copy to the buffer
pStore = pBuffer;
for ( i = 0; i < nMarks; i++ )
pStore = Dau_DsdNormalizeCopy( pStore, pStr, pMarks, pPerm[i] );
assert( pStore - pBuffer == *p - pOld );
memcpy( pOld, pBuffer, (size_t)(pStore - pBuffer) );
return;
}
if ( **p == '<' || **p == '{' ) // mux
{
char * q = pStr + pMatches[ *p - pStr ];
assert( *q == **p + 1 + (**p != '(') );
if ( (**p == '<') && (*(q+1) == '{') )
{
*p = q+1;
Dau_DsdNormalize_rec( pStr, p, pMatches );
return;
}
for ( (*p)++; *p < q; (*p)++ )
Dau_DsdNormalize_rec( pStr, p, pMatches );
assert( *p == q );
return;
}
assert( 0 );
}
void Dau_DsdNormalize( char * pDsd )
{
if ( pDsd[1] != 0 )
Dau_DsdNormalize_rec( pDsd, &pDsd, Dau_DsdComputeMatches(pDsd) );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dau_DsdCountAnds_rec( char * pStr, char ** p, int * pMatches )
{
if ( **p == '!' )
(*p)++;
while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
(*p)++;
if ( **p == '<' )
{
char * q = pStr + pMatches[*p - pStr];
if ( *(q+1) == '{' )
*p = q+1;
}
if ( **p >= 'a' && **p <= 'z' ) // var
return 0;
if ( **p == '(' || **p == '[' ) // and/or/xor
{
int Counter = 0, AddOn = (**p == '(')? 1 : 3;
char * q = pStr + pMatches[ *p - pStr ];
assert( *q == **p + 1 + (**p != '(') );
for ( (*p)++; *p < q; (*p)++ )
Counter += AddOn + Dau_DsdCountAnds_rec( pStr, p, pMatches );
assert( *p == q );
return Counter - AddOn;
}
if ( **p == '<' || **p == '{' ) // mux
{
int Counter = 3;
char * q = pStr + pMatches[ *p - pStr ];
assert( *q == **p + 1 + (**p != '(') );
for ( (*p)++; *p < q; (*p)++ )
Counter += Dau_DsdCountAnds_rec( pStr, p, pMatches );
assert( *p == q );
return Counter;
}
assert( 0 );
return 0;
}
int Dau_DsdCountAnds( char * pDsd )
{
if ( pDsd[1] == 0 )
return 0;
return Dau_DsdCountAnds_rec( pDsd, &pDsd, Dau_DsdComputeMatches(pDsd) );
}
/**Function*************************************************************
Synopsis [Computes truth table for the DSD formula.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
word Dau_Dsd6TruthCompose_rec( word Func, word * pFanins, int nVars )
{
word t0, t1;
if ( Func == 0 )
return 0;
if ( Func == ~(word)0 )
return ~(word)0;
assert( nVars > 0 );
if ( --nVars == 0 )
{
assert( Func == s_Truths6[0] || Func == s_Truths6Neg[0] );
return (Func == s_Truths6[0]) ? pFanins[0] : ~pFanins[0];
}
if ( !Abc_Tt6HasVar(Func, nVars) )
return Dau_Dsd6TruthCompose_rec( Func, pFanins, nVars );
t0 = Dau_Dsd6TruthCompose_rec( Abc_Tt6Cofactor0(Func, nVars), pFanins, nVars );
t1 = Dau_Dsd6TruthCompose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, nVars );
return (~pFanins[nVars] & t0) | (pFanins[nVars] & t1);
}
word Dau_Dsd6ToTruth_rec( char * pStr, char ** p, int * pMatches, word * pTruths )
{
int fCompl = 0;
if ( **p == '!' )
(*p)++, fCompl = 1;
if ( **p >= 'a' && **p <= 'f' ) // var
{
assert( **p - 'a' >= 0 && **p - 'a' < 6 );
return fCompl ? ~pTruths[**p - 'a'] : pTruths[**p - 'a'];
}
if ( **p == '(' ) // and/or
{
char * q = pStr + pMatches[ *p - pStr ];
word Res = ~(word)0;
assert( **p == '(' && *q == ')' );
for ( (*p)++; *p < q; (*p)++ )
Res &= Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths );
assert( *p == q );
return fCompl ? ~Res : Res;
}
if ( **p == '[' ) // xor
{
char * q = pStr + pMatches[ *p - pStr ];
word Res = 0;
assert( **p == '[' && *q == ']' );
for ( (*p)++; *p < q; (*p)++ )
Res ^= Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths );
assert( *p == q );
return fCompl ? ~Res : Res;
}
if ( **p == '<' ) // mux
{
int nVars = 0;
word Temp[3], * pTemp = Temp, Res;
word Fanins[6], * pTruths2;
char * pOld = *p;
char * q = pStr + pMatches[ *p - pStr ];
// read fanins
if ( *(q+1) == '{' )
{
char * q2;
*p = q+1;
q2 = pStr + pMatches[ *p - pStr ];
assert( **p == '{' && *q2 == '}' );
for ( nVars = 0, (*p)++; *p < q2; (*p)++, nVars++ )
Fanins[nVars] = Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths );
assert( *p == q2 );
pTruths2 = Fanins;
}
else
pTruths2 = pTruths;
// read MUX
*p = pOld;
q = pStr + pMatches[ *p - pStr ];
assert( **p == '<' && *q == '>' );
// verify internal variables
if ( nVars )
for ( ; pOld < q; pOld++ )
if ( *pOld >= 'a' && *pOld <= 'z' )
assert( *pOld - 'a' < nVars );
// derive MAX components
for ( (*p)++; *p < q; (*p)++ )
*pTemp++ = Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths2 );
assert( pTemp == Temp + 3 );
assert( *p == q );
if ( *(q+1) == '{' ) // and/or
{
char * q = pStr + pMatches[ ++(*p) - pStr ];
assert( **p == '{' && *q == '}' );
*p = q;
}
Res = (Temp[0] & Temp[1]) | (~Temp[0] & Temp[2]);
return fCompl ? ~Res : Res;
}
if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
{
word Func, Fanins[6], Res;
char * q;
int i, nVars = Abc_TtReadHex( &Func, *p );
*p += Abc_TtHexDigitNum( nVars );
q = pStr + pMatches[ *p - pStr ];
assert( **p == '{' && *q == '}' );
for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
Fanins[i] = Dau_Dsd6ToTruth_rec( pStr, p, pMatches, pTruths );
assert( i == nVars );
assert( *p == q );
Res = Dau_Dsd6TruthCompose_rec( Func, Fanins, nVars );
return fCompl ? ~Res : Res;
}
assert( 0 );
return 0;
}
word Dau_Dsd6ToTruth( char * p )
{
word Res;
if ( *p == '0' && *(p+1) == 0 )
Res = 0;
else if ( *p == '1' && *(p+1) == 0 )
Res = ~(word)0;
else
Res = Dau_Dsd6ToTruth_rec( p, &p, Dau_DsdComputeMatches(p), s_Truths6 );
assert( *++p == 0 );
return Res;
}
/**Function*************************************************************
Synopsis [Computes truth table for the DSD formula.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dau_DsdTruth6Compose_rec( word Func, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR )
{
if ( Func == 0 )
{
Abc_TtConst0( pRes, nWordsR );
return;
}
if ( Func == ~(word)0 )
{
Abc_TtConst1( pRes, nWordsR );
return;
}
assert( nVars > 0 );
if ( --nVars == 0 )
{
assert( Func == s_Truths6[0] || Func == s_Truths6Neg[0] );
Abc_TtCopy( pRes, pFanins[0], nWordsR, Func == s_Truths6Neg[0] );
return;
}
if ( !Abc_Tt6HasVar(Func, nVars) )
{
Dau_DsdTruth6Compose_rec( Func, pFanins, pRes, nVars, nWordsR );
return;
}
{
word pTtTemp[2][DAU_MAX_WORD];
Dau_DsdTruth6Compose_rec( Abc_Tt6Cofactor0(Func, nVars), pFanins, pTtTemp[0], nVars, nWordsR );
Dau_DsdTruth6Compose_rec( Abc_Tt6Cofactor1(Func, nVars), pFanins, pTtTemp[1], nVars, nWordsR );
Abc_TtMux( pRes, pFanins[nVars], pTtTemp[1], pTtTemp[0], nWordsR );
return;
}
}
void Dau_DsdTruthCompose_rec( word * pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR )
{
int nWordsF;
if ( nVars <= 6 )
{
Dau_DsdTruth6Compose_rec( pFunc[0], pFanins, pRes, nVars, nWordsR );
return;
}
nWordsF = Abc_TtWordNum( nVars );
assert( nWordsF > 1 );
if ( Abc_TtIsConst0(pFunc, nWordsF) )
{
Abc_TtConst0( pRes, nWordsR );
return;
}
if ( Abc_TtIsConst1(pFunc, nWordsF) )
{
Abc_TtConst1( pRes, nWordsR );
return;
}
if ( !Abc_TtHasVar( pFunc, nVars, nVars-1 ) )
{
Dau_DsdTruthCompose_rec( pFunc, pFanins, pRes, nVars-1, nWordsR );
return;
}
{
word pTtTemp[2][DAU_MAX_WORD];
nVars--;
Dau_DsdTruthCompose_rec( pFunc, pFanins, pTtTemp[0], nVars, nWordsR );
Dau_DsdTruthCompose_rec( pFunc + nWordsF/2, pFanins, pTtTemp[1], nVars, nWordsR );
Abc_TtMux( pRes, pFanins[nVars], pTtTemp[1], pTtTemp[0], nWordsR );
return;
}
}
void Dau_DsdToTruth_rec( char * pStr, char ** p, int * pMatches, word ** pTtElems, word * pRes, int nVars )
{
int nWords = Abc_TtWordNum( nVars );
int fCompl = 0;
if ( **p == '!' )
(*p)++, fCompl = 1;
if ( **p >= 'a' && **p <= 'z' ) // var
{
assert( **p - 'a' >= 0 && **p - 'a' < nVars );
Abc_TtCopy( pRes, pTtElems[**p - 'a'], nWords, fCompl );
return;
}
if ( **p == '(' ) // and/or
{
char * q = pStr + pMatches[ *p - pStr ];
word pTtTemp[DAU_MAX_WORD];
assert( **p == '(' && *q == ')' );
Abc_TtConst1( pRes, nWords );
for ( (*p)++; *p < q; (*p)++ )
{
Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pTtTemp, nVars );
Abc_TtAnd( pRes, pRes, pTtTemp, nWords, 0 );
}
assert( *p == q );
if ( fCompl ) Abc_TtNot( pRes, nWords );
return;
}
if ( **p == '[' ) // xor
{
char * q = pStr + pMatches[ *p - pStr ];
word pTtTemp[DAU_MAX_WORD];
assert( **p == '[' && *q == ']' );
Abc_TtConst0( pRes, nWords );
for ( (*p)++; *p < q; (*p)++ )
{
Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pTtTemp, nVars );
Abc_TtXor( pRes, pRes, pTtTemp, nWords, 0 );
}
assert( *p == q );
if ( fCompl ) Abc_TtNot( pRes, nWords );
return;
}
if ( **p == '<' ) // mux
{
char * q = pStr + pMatches[ *p - pStr ];
word pTtTemp[3][DAU_MAX_WORD];
int i;
assert( **p == '<' && *q == '>' );
for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pTtTemp[i], nVars );
assert( i == 3 );
Abc_TtMux( pRes, pTtTemp[0], pTtTemp[1], pTtTemp[2], nWords );
assert( *p == q );
if ( fCompl ) Abc_TtNot( pRes, nWords );
return;
}
if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
{
word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], pFunc[DAU_MAX_WORD];
char * q;
int i, nVarsF = Abc_TtReadHex( pFunc, *p );
*p += Abc_TtHexDigitNum( nVarsF );
q = pStr + pMatches[ *p - pStr ];
assert( **p == '{' && *q == '}' );
for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
Dau_DsdToTruth_rec( pStr, p, pMatches, pTtElems, pFanins[i], nVars );
assert( i == nVarsF );
assert( *p == q );
Dau_DsdTruthCompose_rec( pFunc, pFanins, pRes, nVarsF, nWords );
if ( fCompl ) Abc_TtNot( pRes, nWords );
return;
}
assert( 0 );
}
word * Dau_DsdToTruth( char * p, int nVars )
{
int nWords = Abc_TtWordNum( nVars );
word ** pTtElems = Dau_DsdTtElems();
word * pRes = pTtElems[DAU_MAX_VAR];
assert( nVars <= DAU_MAX_VAR );
if ( Dau_DsdIsConst0(p) )
Abc_TtConst0( pRes, nWords );
else if ( Dau_DsdIsConst1(p) )
Abc_TtConst1( pRes, nWords );
else
Dau_DsdToTruth_rec( p, &p, Dau_DsdComputeMatches(p), pTtElems, pRes, nVars );
assert( *++p == 0 );
return pRes;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dau_DsdTest2()
{
// char * p = Abc_UtilStrsav( "!(ab!(de[cf]))" );
// char * p = Abc_UtilStrsav( "!(a![d<ecf>]b)" );
// word t = Dau_Dsd6ToTruth( p );
}
/**Function*************************************************************
Synopsis [Performs DSD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dau_DsdPerformReplace( char * pBuffer, int PosStart, int Pos, int Symb, char * pNext )
{
static char pTemp[DAU_MAX_STR];
char * pCur = pTemp;
int i, k, RetValue;
for ( i = PosStart; i < Pos; i++ )
if ( pBuffer[i] != Symb )
*pCur++ = pBuffer[i];
else
for ( k = 0; pNext[k]; k++ )
*pCur++ = pNext[k];
RetValue = PosStart + (pCur - pTemp);
for ( i = PosStart; i < RetValue; i++ )
pBuffer[i] = pTemp[i-PosStart];
return RetValue;
}
int Dau_DsdPerform_rec( word t, char * pBuffer, int Pos, int * pVars, int nVars )
{
char pNest[10];
word Cof0[6], Cof1[6], Cof[4];
int pVarsNew[6], nVarsNew, PosStart;
int v, u, vBest, CountBest;
assert( Pos < DAU_MAX_STR );
// perform support minimization
nVarsNew = 0;
for ( v = 0; v < nVars; v++ )
if ( Abc_Tt6HasVar( t, pVars[v] ) )
pVarsNew[ nVarsNew++ ] = pVars[v];
assert( nVarsNew > 0 );
// special case when function is a var
if ( nVarsNew == 1 )
{
if ( t == s_Truths6[ pVarsNew[0] ] )
{
pBuffer[Pos++] = 'a' + pVarsNew[0];
return Pos;
}
if ( t == ~s_Truths6[ pVarsNew[0] ] )
{
pBuffer[Pos++] = '!';
pBuffer[Pos++] = 'a' + pVarsNew[0];
return Pos;
}
assert( 0 );
return Pos;
}
// decompose on the output side
for ( v = 0; v < nVarsNew; v++ )
{
Cof0[v] = Abc_Tt6Cofactor0( t, pVarsNew[v] );
Cof1[v] = Abc_Tt6Cofactor1( t, pVarsNew[v] );
assert( Cof0[v] != Cof1[v] );
if ( Cof0[v] == 0 ) // ax
{
pBuffer[Pos++] = '(';
pBuffer[Pos++] = 'a' + pVarsNew[v];
Pos = Dau_DsdPerform_rec( Cof1[v], pBuffer, Pos, pVarsNew, nVarsNew );
pBuffer[Pos++] = ')';
return Pos;
}
if ( Cof0[v] == ~(word)0 ) // !(ax)
{
pBuffer[Pos++] = '!';
pBuffer[Pos++] = '(';
pBuffer[Pos++] = 'a' + pVarsNew[v];
Pos = Dau_DsdPerform_rec( ~Cof1[v], pBuffer, Pos, pVarsNew, nVarsNew );
pBuffer[Pos++] = ')';
return Pos;
}
if ( Cof1[v] == 0 ) // !ax
{
pBuffer[Pos++] = '(';
pBuffer[Pos++] = '!';
pBuffer[Pos++] = 'a' + pVarsNew[v];
Pos = Dau_DsdPerform_rec( Cof0[v], pBuffer, Pos, pVarsNew, nVarsNew );
pBuffer[Pos++] = ')';
return Pos;
}
if ( Cof1[v] == ~(word)0 ) // !(!ax)
{
pBuffer[Pos++] = '!';
pBuffer[Pos++] = '(';
pBuffer[Pos++] = '!';
pBuffer[Pos++] = 'a' + pVarsNew[v];
Pos = Dau_DsdPerform_rec( ~Cof0[v], pBuffer, Pos, pVarsNew, nVarsNew );
pBuffer[Pos++] = ')';
return Pos;
}
if ( Cof0[v] == ~Cof1[v] ) // a^x
{
pBuffer[Pos++] = '[';
pBuffer[Pos++] = 'a' + pVarsNew[v];
Pos = Dau_DsdPerform_rec( Cof0[v], pBuffer, Pos, pVarsNew, nVarsNew );
pBuffer[Pos++] = ']';
return Pos;
}
}
// decompose on the input side
for ( v = 0; v < nVarsNew; v++ )
for ( u = v+1; u < nVarsNew; u++ )
{
Cof[0] = Abc_Tt6Cofactor0( Cof0[v], pVarsNew[u] );
Cof[1] = Abc_Tt6Cofactor1( Cof0[v], pVarsNew[u] );
Cof[2] = Abc_Tt6Cofactor0( Cof1[v], pVarsNew[u] );
Cof[3] = Abc_Tt6Cofactor1( Cof1[v], pVarsNew[u] );
if ( Cof[0] == Cof[1] && Cof[0] == Cof[2] ) // vu
{
PosStart = Pos;
sprintf( pNest, "(%c%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[3]) | (~s_Truths6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
if ( Cof[0] == Cof[1] && Cof[0] == Cof[3] ) // v!u
{
PosStart = Pos;
sprintf( pNest, "(%c!%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[2]) | (~s_Truths6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
if ( Cof[0] == Cof[2] && Cof[0] == Cof[3] ) // !vu
{
PosStart = Pos;
sprintf( pNest, "(!%c%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[1]) | (~s_Truths6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
if ( Cof[1] == Cof[2] && Cof[1] == Cof[3] ) // !v!u
{
PosStart = Pos;
sprintf( pNest, "(!%c!%c)", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[0]) | (~s_Truths6[pVarsNew[u]] & Cof[1]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
if ( Cof[0] == Cof[3] && Cof[1] == Cof[2] ) // v+u
{
PosStart = Pos;
sprintf( pNest, "[%c%c]", 'a' + pVarsNew[v], 'a' + pVarsNew[u] );
Pos = Dau_DsdPerform_rec( (s_Truths6[pVarsNew[u]] & Cof[1]) | (~s_Truths6[pVarsNew[u]] & Cof[0]), pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerformReplace( pBuffer, PosStart, Pos, 'a' + pVarsNew[u], pNest );
return Pos;
}
}
// find best variable for MUX decomposition
vBest = -1;
CountBest = 10;
for ( v = 0; v < nVarsNew; v++ )
{
int CountCur = 0;
for ( u = 0; u < nVarsNew; u++ )
if ( u != v && Abc_Tt6HasVar(Cof0[v], pVarsNew[u]) && Abc_Tt6HasVar(Cof1[v], pVarsNew[u]) )
CountCur++;
if ( CountBest > CountCur )
{
CountBest = CountCur;
vBest = v;
}
if ( CountCur == 0 )
break;
}
// perform MUX decomposition
pBuffer[Pos++] = '<';
pBuffer[Pos++] = 'a' + pVarsNew[vBest];
Pos = Dau_DsdPerform_rec( Cof1[vBest], pBuffer, Pos, pVarsNew, nVarsNew );
Pos = Dau_DsdPerform_rec( Cof0[vBest], pBuffer, Pos, pVarsNew, nVarsNew );
pBuffer[Pos++] = '>';
return Pos;
}
char * Dau_DsdPerform( word t )
{
static char pBuffer[DAU_MAX_STR];
int pVarsNew[6] = {0, 1, 2, 3, 4, 5};
int Pos = 0;
if ( t == 0 )
pBuffer[Pos++] = '0';
else if ( t == ~(word)0 )
pBuffer[Pos++] = '1';
else
Pos = Dau_DsdPerform_rec( t, pBuffer, Pos, pVarsNew, 6 );
pBuffer[Pos++] = 0;
// printf( "%d ", strlen(pBuffer) );
// printf( "%s ->", pBuffer );
Dau_DsdRemoveBraces( pBuffer, Dau_DsdComputeMatches(pBuffer) );
// printf( " %s\n", pBuffer );
return pBuffer;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Dau_DsdTest3()
{
// word t = s_Truths6[0] & s_Truths6[1] & s_Truths6[2];
// word t = ~s_Truths6[0] | (s_Truths6[1] ^ ~s_Truths6[2]);
// word t = (s_Truths6[1] & s_Truths6[2]) | (s_Truths6[0] & s_Truths6[3]);
// word t = (~s_Truths6[1] & ~s_Truths6[2]) | (s_Truths6[0] ^ s_Truths6[3]);
// word t = ((~s_Truths6[1] & ~s_Truths6[2]) | (s_Truths6[0] ^ s_Truths6[3])) ^ s_Truths6[5];
// word t = ((s_Truths6[1] & ~s_Truths6[2]) ^ (s_Truths6[0] & s_Truths6[3])) & s_Truths6[5];
// word t = (~(~s_Truths6[0] & ~s_Truths6[4]) & s_Truths6[2]) | (~s_Truths6[1] & ~s_Truths6[0] & ~s_Truths6[4]);
// word t = 0x0000000000005F3F;
// word t = 0xF3F5030503050305;
// word t = (s_Truths6[0] & s_Truths6[1] & (s_Truths6[2] ^ s_Truths6[4])) | (~s_Truths6[0] & ~s_Truths6[1] & ~(s_Truths6[2] ^ s_Truths6[4]));
// word t = 0x05050500f5f5f5f3;
word t = ABC_CONST(0x9ef7a8d9c7193a0f);
char * p = Dau_DsdPerform( t );
word t2 = Dau_Dsd6ToTruth( p );
if ( t != t2 )
printf( "Verification failed.\n" );
}
/**Function*************************************************************
Synopsis [Find the best cofactoring variable.]
Description [Return -2 if non-DSD; -1 if full DSD; otherwise,
returns cofactoring variables i (i >= 0).]
SideEffects []
SeeAlso []
***********************************************************************/
int Dau_DsdCheck1Step( void * p, word * pTruth, int nVarsInit, int * pVarLevels )
{
word pCofTemp[DAU_MAX_WORD];
int pVarPrios[DAU_MAX_VAR];
int nWords = Abc_TtWordNum(nVarsInit);
int nSizeNonDec, nSizeNonDec0, nSizeNonDec1;
int i, vBest = -2, nSumCofsBest = ABC_INFINITY, nSumCofs;
nSizeNonDec = Dau_DsdDecompose( pTruth, nVarsInit, 0, 0, NULL );
if ( nSizeNonDec == 0 )
return -1;
assert( nSizeNonDec > 0 );
// find variable priority
for ( i = 0; i < nVarsInit; i++ )
pVarPrios[i] = i;
if ( pVarLevels )
{
extern int Dau_DsdLevelVar( void * pMan, int iVar );
int pVarLevels[DAU_MAX_VAR];
for ( i = 0; i < nVarsInit; i++ )
pVarLevels[i] = -Dau_DsdLevelVar( p, i );
// for ( i = 0; i < nVarsInit; i++ )
// printf( "%d ", -pVarLevels[i] );
// printf( "\n" );
Vec_IntSelectSortCost2( pVarPrios, nVarsInit, pVarLevels );
// for ( i = 0; i < nVarsInit; i++ )
// printf( "%d ", pVarPrios[i] );
// printf( "\n\n" );
}
for ( i = 0; i < nVarsInit; i++ )
{
assert( pVarPrios[i] >= 0 && pVarPrios[i] < nVarsInit );
// try first cofactor
Abc_TtCofactor0p( pCofTemp, pTruth, nWords, pVarPrios[i] );
nSumCofs = Abc_TtSupportSize( pCofTemp, nVarsInit );
nSizeNonDec0 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, 0, NULL );
// try second cofactor
Abc_TtCofactor1p( pCofTemp, pTruth, nWords, pVarPrios[i] );
nSumCofs += Abc_TtSupportSize( pCofTemp, nVarsInit );
nSizeNonDec1 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, 0, NULL );
// compare cofactors
if ( nSizeNonDec0 || nSizeNonDec1 )
continue;
if ( nSumCofsBest > nSumCofs )
{
vBest = pVarPrios[i];
nSumCofsBest = nSumCofs;
}
}
return vBest;
}
/**Function*************************************************************
Synopsis [Data-structure to store DSD information.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
typedef struct Dau_Dsd_t_ Dau_Dsd_t;
struct Dau_Dsd_t_
{
int nVarsInit; // the initial number of variables
int nVarsUsed; // the current number of variables
int nPos; // writing position
int nSizeNonDec; // size of the largest non-decomposable block
int nConsts; // the number of constant decompositions
int uConstMask; // constant decomposition mask
int fSplitPrime; // represent prime function as 1-step DSD
int fWriteTruth; // writing truth table as a hex string
int * pVarLevels; // variable levels
char pVarDefs[32][8]; // variable definitions
char Cache[32][32]; // variable cache
char pOutput[DAU_MAX_STR]; // output stream
};
static abctime s_Times[3] = {0};
/**Function*************************************************************
Synopsis [Manipulation of DSD data-structure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Dau_DsdInitialize( Dau_Dsd_t * p, int nVarsInit )
{
int i, v, u;
assert( nVarsInit >= 0 && nVarsInit <= 16 );
p->nVarsInit = nVarsInit;
p->nVarsUsed = nVarsInit;
p->nPos = 0;
p->nSizeNonDec = 0;
p->nConsts = 0;
p->uConstMask = 0;
for ( i = 0; i < nVarsInit; i++ )
p->pVarDefs[i][0] = 'a' + i, p->pVarDefs[i][1] = 0;
for ( v = 0; v < nVarsInit; v++ )
for ( u = 0; u < nVarsInit; u++ )
p->Cache[v][u] = 0;
}
static inline void Dau_DsdWriteString( Dau_Dsd_t * p, char * pStr )
{
while ( *pStr )
p->pOutput[ p->nPos++ ] = *pStr++;
}
static inline void Dau_DsdWriteVar( Dau_Dsd_t * p, int iVar, int fInv )
{
char * pStr;
if ( fInv )
p->pOutput[ p->nPos++ ] = '!';
for ( pStr = p->pVarDefs[iVar]; *pStr; pStr++ )
if ( *pStr >= 'a' + p->nVarsInit && *pStr < 'a' + p->nVarsUsed )
Dau_DsdWriteVar( p, *pStr - 'a', 0 );
else
p->pOutput[ p->nPos++ ] = *pStr;
}
int Dau_DsdLevelVar( void * pMan, int iVar )
{
Dau_Dsd_t * p = (Dau_Dsd_t *)pMan;
char * pStr;
int LevelMax = 0, Level;
for ( pStr = p->pVarDefs[iVar]; *pStr; pStr++ )
{
if ( *pStr >= 'a' + p->nVarsInit && *pStr < 'a' + p->nVarsUsed )
Level = 1 + Dau_DsdLevelVar( p, *pStr - 'a' );
else
Level = p->pVarLevels[*pStr - 'a'];
LevelMax = Abc_MaxInt( LevelMax, Level );
}
return LevelMax;
}
static inline void Dau_DsdTranslate( Dau_Dsd_t * p, int * pVars, int nVars, char * pStr )
{
for ( ; *pStr; pStr++ )
if ( *pStr >= 'a' && *pStr < 'a' + nVars )
Dau_DsdWriteVar( p, pVars[*pStr - 'a'], 0 );
else
p->pOutput[ p->nPos++ ] = *pStr;
}
static inline int Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{
int v, RetValue = 2;
assert( nVars > 2 );
if ( p->fSplitPrime )
{
word pCofTemp[DAU_MAX_WORD];
int nWords = Abc_TtWordNum(nVars);
int vBest = Dau_DsdCheck1Step( p, pTruth, nVars, p->pVarLevels );
assert( vBest != -1 );
if ( vBest == -2 ) // non-dec
p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars );
else
{
char pRes[DAU_MAX_STR];
int nNonDecSize;
// compose the result
Dau_DsdWriteString( p, "<" );
Dau_DsdWriteVar( p, vBest, 0 );
// split decomposition
Abc_TtCofactor1p( pCofTemp, pTruth, nWords, vBest );
nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, p->fWriteTruth, pRes );
assert( nNonDecSize == 0 );
Dau_DsdWriteString( p, pRes );
// split decomposition
Abc_TtCofactor0p( pCofTemp, pTruth, nWords, vBest );
nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, p->fWriteTruth, pRes );
assert( nNonDecSize == 0 );
Dau_DsdWriteString( p, pRes );
Dau_DsdWriteString( p, ">" );
RetValue = 1;
}
}
else if ( p->fWriteTruth )
p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars );
Dau_DsdWriteString( p, "{" );
for ( v = 0; v < nVars; v++ )
Dau_DsdWriteVar( p, pVars[v], 0 );
Dau_DsdWriteString( p, "}" );
p->nSizeNonDec = nVars;
return RetValue;
}
static inline void Dau_DsdFinalize( Dau_Dsd_t * p )
{
int i;
for ( i = 0; i < p->nConsts; i++ )
p->pOutput[ p->nPos++ ] = ((p->uConstMask >> (p->nConsts-1-i)) & 1) ? ']' : ')';
p->pOutput[ p->nPos++ ] = 0;
}
static inline int Dau_DsdAddVarDef( Dau_Dsd_t * p, char * pStr )
{
int u;
assert( strlen(pStr) < 8 );
assert( p->nVarsUsed < 32 );
for ( u = 0; u < p->nVarsUsed; u++ )
p->Cache[p->nVarsUsed][u] = 0;
for ( u = 0; u < p->nVarsUsed; u++ )
p->Cache[u][p->nVarsUsed] = 0;
sprintf( p->pVarDefs[p->nVarsUsed++], "%s", pStr );
return p->nVarsUsed - 1;
}
static inline int Dau_DsdFindVarDef( int * pVars, int nVars, int VarDef )
{
int v;
for ( v = 0; v < nVars; v++ )
if ( pVars[v] == VarDef )
break;
assert( v < nVars );
return v;
}
static inline void Dau_DsdInsertVarCache( Dau_Dsd_t * p, int v, int u, int Status )
{
assert( v != u );
assert( Status > 0 && Status < 4 );
assert( p->Cache[v][u] == 0 );
p->Cache[v][u] = Status;
}
static inline int Dau_DsdLookupVarCache( Dau_Dsd_t * p, int v, int u )
{
return p->Cache[v][u];
}
/**Function*************************************************************
Synopsis [Procedures specialized for 6-variable functions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dau_Dsd6DecomposeSingleVarOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
{
// consider negative cofactors
if ( pTruth[0] & 1 )
{
if ( Abc_Tt6Cof0IsConst1( pTruth[0], v ) ) // !(ax)
{
Dau_DsdWriteString( p, "!(" );
pTruth[0] = ~Abc_Tt6Cofactor1( pTruth[0], v );
goto finish;
}
}
else
{
if ( Abc_Tt6Cof0IsConst0( pTruth[0], v ) ) // ax
{
Dau_DsdWriteString( p, "(" );
pTruth[0] = Abc_Tt6Cofactor1( pTruth[0], v );
goto finish;
}
}
// consider positive cofactors
if ( pTruth[0] >> 63 )
{
if ( Abc_Tt6Cof1IsConst1( pTruth[0], v ) ) // !(!ax)
{
Dau_DsdWriteString( p, "!(!" );
pTruth[0] = ~Abc_Tt6Cofactor0( pTruth[0], v );
goto finish;
}
}
else
{
if ( Abc_Tt6Cof1IsConst0( pTruth[0], v ) ) // !ax
{
Dau_DsdWriteString( p, "(!" );
pTruth[0] = Abc_Tt6Cofactor0( pTruth[0], v );
goto finish;
}
}
// consider equal cofactors
if ( Abc_Tt6CofsOpposite( pTruth[0], v ) ) // [ax]
{
Dau_DsdWriteString( p, "[" );
pTruth[0] = Abc_Tt6Cofactor0( pTruth[0], v );
p->uConstMask |= (1 << p->nConsts);
goto finish;
}
return 0;
finish:
p->nConsts++;
Dau_DsdWriteVar( p, pVars[v], 0 );
pVars[v] = pVars[nVars-1];
Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
return 1;
}
int Dau_Dsd6DecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{
abctime clk = Abc_Clock();
assert( nVars > 1 );
while ( 1 )
{
int v;
for ( v = nVars - 1; v >= 0 && nVars > 1; v-- )
if ( Dau_Dsd6DecomposeSingleVarOne( p, pTruth, pVars, nVars, v ) )
{
nVars--;
break;
}
if ( v == -1 || nVars == 1 )
break;
}
if ( nVars == 1 )
Dau_DsdWriteVar( p, pVars[--nVars], (int)(pTruth[0] & 1) );
s_Times[0] += Abc_Clock() - clk;
return nVars;
}
static inline int Dau_Dsd6FindSupportOne( Dau_Dsd_t * p, word tCof0, word tCof1, int * pVars, int nVars, int v, int u )
{
int Status = p ? Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ) : 0;
if ( Status == 0 )
{
Status = (Abc_Tt6HasVar(tCof1, u) << 1) | Abc_Tt6HasVar(tCof0, u);
if ( p )
Dau_DsdInsertVarCache( p, pVars[v], pVars[u], Status );
}
return Status;
}
static inline unsigned Dau_Dsd6FindSupports( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
{
int u;
unsigned uSupports = 0;
word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v );
word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v );
//Kit_DsdPrintFromTruth( (unsigned *)&tCof0, 6 );printf( "\n" );
//Kit_DsdPrintFromTruth( (unsigned *)&tCof1, 6 );printf( "\n" );
for ( u = 0; u < nVars; u++ )
if ( u != v )
uSupports |= (Dau_Dsd6FindSupportOne( p, tCof0, tCof1, pVars, nVars, v, u ) << (2 * u));
return uSupports;
}
static inline void Dau_DsdPrintSupports( unsigned uSupp, int nVars )
{
int v, Value;
printf( "Cofactor supports: " );
for ( v = nVars - 1; v >= 0; v-- )
{
Value = ((uSupp >> (2*v)) & 3);
if ( Value == 1 )
printf( "01" );
else if ( Value == 2 )
printf( "10" );
else if ( Value == 3 )
printf( "11" );
else
printf( "00" );
if ( v )
printf( "-" );
}
printf( "\n" );
}
// checks decomposability with respect to the pair (v, u)
static inline int Dau_Dsd6DecomposeDoubleVarsOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, int u )
{
char pBuffer[10] = { 0 };
word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v );
word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v );
int Status = Dau_Dsd6FindSupportOne( p, tCof0, tCof1, pVars, nVars, v, u );
assert( v > u );
//printf( "Checking %s and %s.\n", p->pVarDefs[pVars[v]], p->pVarDefs[pVars[u]] );
// Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 );printf( "\n" );
if ( Status == 3 )
{
// both F(v=0) and F(v=1) depend on u
if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) && Abc_Tt6Cof0EqualCof1(tCof1, tCof0, u) ) // v+u
{
pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
sprintf( pBuffer, "[%c%c]", 'a' + pVars[v], 'a' + pVars[u] );
goto finish;
}
}
else if ( Status == 2 )
{
// F(v=0) does not depend on u; F(v=1) depends on u
if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) ) // vu
{
sprintf( pBuffer, "(%c%c)", 'a' + pVars[v], 'a' + pVars[u] );
pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
goto finish;
}
if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // v!u
{
sprintf( pBuffer, "(%c!%c)", 'a' + pVars[v], 'a' + pVars[u] );
pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
goto finish;
}
}
else if ( Status == 1 )
{
// F(v=0) depends on u; F(v=1) does not depend on u
if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // !vu
{
sprintf( pBuffer, "(!%c%c)", 'a' + pVars[v], 'a' + pVars[u] );
pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
goto finish;
}
if ( Abc_Tt6Cof1EqualCof1(tCof0, tCof1, u) ) // !v!u
{
sprintf( pBuffer, "(!%c!%c)", 'a' + pVars[v], 'a' + pVars[u] );
pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u));
goto finish;
}
}
return nVars;
finish:
// finalize decomposition
assert( pBuffer[0] );
pVars[u] = Dau_DsdAddVarDef( p, pBuffer );
pVars[v] = pVars[nVars-1];
Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
if ( Dau_Dsd6DecomposeSingleVarOne( p, pTruth, pVars, --nVars, u ) )
nVars = Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, --nVars );
return nVars;
}
int Dau_Dsd6DecomposeDoubleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{
abctime clk = Abc_Clock();
while ( 1 )
{
int v, u, nVarsOld;
for ( v = nVars - 1; v > 0; v-- )
{
for ( u = v - 1; u >= 0; u-- )
{
if ( Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ) )
continue;
nVarsOld = nVars;
nVars = Dau_Dsd6DecomposeDoubleVarsOne( p, pTruth, pVars, nVars, v, u );
if ( nVars == 0 )
{
s_Times[1] += Abc_Clock() - clk;
return 0;
}
if ( nVarsOld > nVars )
break;
}
if ( u >= 0 ) // found
break;
}
if ( v == 0 ) // not found
break;
}
s_Times[1] += Abc_Clock() - clk;
return nVars;
}
// look for MUX-decomposable variable on top or at the bottom
static inline int Dau_Dsd6DecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
{
extern int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit );
Dau_Dsd_t P1, * p1 = &P1;
word tCof0, tCof1;
p1->fSplitPrime = 0;
p1->fWriteTruth = p->fWriteTruth;
// move this variable to the top
ABC_SWAP( int, pVars[v], pVars[nVars-1] );
Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
// cofactor w.r.t the last variable
tCof0 = Abc_Tt6Cofactor0( pTruth[0], nVars - 1 );
tCof1 = Abc_Tt6Cofactor1( pTruth[0], nVars - 1 );
// compose the result
Dau_DsdWriteString( p, "<" );
Dau_DsdWriteVar( p, pVars[nVars - 1], 0 );
// split decomposition
Dau_DsdDecomposeInt( p1, &tCof1, nVars - 1 );
Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
p->nSizeNonDec = p1->nSizeNonDec;
if ( p1->nSizeNonDec )
*pTruth = tCof1;
// split decomposition
Dau_DsdDecomposeInt( p1, &tCof0, nVars - 1 );
Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
Dau_DsdWriteString( p, ">" );
p->nSizeNonDec = Abc_MaxInt( p->nSizeNonDec, p1->nSizeNonDec );
if ( p1->nSizeNonDec )
*pTruth = tCof0;
return 0;
}
static inline int Dau_Dsd6DecomposeTripleVarsInner( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, unsigned uSupports )
{
int iVar0 = Abc_TtSuppFindFirst( uSupports & (~uSupports >> 1) & 0x55555555 ) >> 1;
int iVar1 = Abc_TtSuppFindFirst( ~uSupports & ( uSupports >> 1) & 0x55555555 ) >> 1;
word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v );
word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v );
word C00 = Abc_Tt6Cofactor0( tCof0, iVar0 );
word C01 = Abc_Tt6Cofactor1( tCof0, iVar0 );
word C10 = Abc_Tt6Cofactor0( tCof1, iVar1 );
word C11 = Abc_Tt6Cofactor1( tCof1, iVar1 );
int fEqual0 = (C00 == C10) && (C01 == C11);
int fEqual1 = (C00 == C11) && (C01 == C10);
if ( fEqual0 || fEqual1 )
{
char pBuffer[10];
int VarId = pVars[iVar0];
pTruth[0] = (s_Truths6[v] & C11) | (~s_Truths6[v] & C10);
sprintf( pBuffer, "<%c%c%s%c>", 'a' + pVars[v], 'a' + pVars[iVar1], fEqual1 ? "!":"", 'a' + pVars[iVar0] );
pVars[v] = Dau_DsdAddVarDef( p, pBuffer );
// remove iVar1
ABC_SWAP( int, pVars[iVar1], pVars[nVars-1] );
Abc_TtSwapVars( pTruth, nVars, iVar1, nVars-1 ); nVars--;
// remove iVar0
iVar0 = Dau_DsdFindVarDef( pVars, nVars, VarId );
ABC_SWAP( int, pVars[iVar0], pVars[nVars-1] );
Abc_TtSwapVars( pTruth, nVars, iVar0, nVars-1 ); nVars--;
// find the new var
v = Dau_DsdFindVarDef( pVars, nVars, p->nVarsUsed-1 );
// remove single variables if possible
if ( Dau_Dsd6DecomposeSingleVarOne( p, pTruth, pVars, nVars, v ) )
nVars = Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, --nVars );
return nVars;
}
return nVars;
}
int Dau_Dsd6DecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{
abctime clk = Abc_Clock();
while ( 1 )
{
int v;
// Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 ); printf( "\n" );
for ( v = nVars - 1; v >= 0; v-- )
{
unsigned uSupports = Dau_Dsd6FindSupports( p, pTruth, pVars, nVars, v );
// Dau_DsdPrintSupports( uSupports, nVars );
if ( (uSupports & (uSupports >> 1) & 0x55555555) == 0 ) // non-overlapping supports
return Dau_Dsd6DecomposeTripleVarsOuter( p, pTruth, pVars, nVars, v );
if ( Abc_TtSuppOnlyOne( uSupports & (~uSupports >> 1) & 0x55555555) &&
Abc_TtSuppOnlyOne(~uSupports & ( uSupports >> 1) & 0x55555555) ) // one unique variable in each cofactor
{
int nVarsNew = Dau_Dsd6DecomposeTripleVarsInner( p, pTruth, pVars, nVars, v, uSupports );
if ( nVarsNew == nVars )
continue;
if ( nVarsNew == 0 )
{
s_Times[2] += Abc_Clock() - clk;
return 0;
}
nVars = Dau_Dsd6DecomposeDoubleVars( p, pTruth, pVars, nVarsNew );
if ( nVars == 0 )
{
s_Times[2] += Abc_Clock() - clk;
return 0;
}
break;
}
}
if ( v == -1 )
{
s_Times[2] += Abc_Clock() - clk;
return nVars;
}
}
assert( 0 );
return -1;
}
int Dau_Dsd6DecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{
// decompose single variales on the output side
nVars = Dau_Dsd6DecomposeSingleVar( p, pTruth, pVars, nVars );
if ( nVars == 0 )
return 0;
// decompose double variables on the input side
nVars = Dau_Dsd6DecomposeDoubleVars( p, pTruth, pVars, nVars );
if ( nVars == 0 )
return 0;
// decompose MUX on the output/input side
nVars = Dau_Dsd6DecomposeTripleVars( p, pTruth, pVars, nVars );
if ( nVars == 0 )
return 0;
// write non-decomposable function
return Dau_DsdWritePrime( p, pTruth, pVars, nVars );
}
/**Function*************************************************************
Synopsis [Procedures specialized for 6-variable functions.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Dau_DsdDecomposeSingleVarOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
{
int nWords = Abc_TtWordNum(nVars);
// consider negative cofactors
if ( pTruth[0] & 1 )
{
if ( Abc_TtCof0IsConst1( pTruth, nWords, v ) ) // !(ax)
{
Dau_DsdWriteString( p, "!(" );
Abc_TtCofactor1( pTruth, nWords, v );
Abc_TtNot( pTruth, nWords );
goto finish;
}
}
else
{
if ( Abc_TtCof0IsConst0( pTruth, nWords, v ) ) // ax
{
Dau_DsdWriteString( p, "(" );
Abc_TtCofactor1( pTruth, nWords, v );
goto finish;
}
}
// consider positive cofactors
if ( pTruth[nWords-1] >> 63 )
{
if ( Abc_TtCof1IsConst1( pTruth, nWords, v ) ) // !(!ax)
{
Dau_DsdWriteString( p, "!(!" );
Abc_TtCofactor0( pTruth, nWords, v );
Abc_TtNot( pTruth, nWords );
goto finish;
}
}
else
{
if ( Abc_TtCof1IsConst0( pTruth, nWords, v ) ) // !ax
{
Dau_DsdWriteString( p, "(!" );
Abc_TtCofactor0( pTruth, nWords, v );
goto finish;
}
}
// consider equal cofactors
if ( Abc_TtCofsOpposite( pTruth, nWords, v ) ) // [ax]
{
Dau_DsdWriteString( p, "[" );
Abc_TtCofactor0( pTruth, nWords, v );
p->uConstMask |= (1 << p->nConsts);
goto finish;
}
return 0;
finish:
p->nConsts++;
Dau_DsdWriteVar( p, pVars[v], 0 );
pVars[v] = pVars[nVars-1];
Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
return 1;
}
int Dau_DsdDecomposeSingleVar( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{
abctime clk = Abc_Clock();
assert( nVars > 1 );
while ( 1 )
{
int v;
for ( v = nVars - 1; v >= 0 && nVars > 1; v-- )
if ( Dau_DsdDecomposeSingleVarOne( p, pTruth, pVars, nVars, v ) )
{
nVars--;
break;
}
if ( v == -1 || nVars == 1 )
break;
}
if ( nVars == 1 )
Dau_DsdWriteVar( p, pVars[--nVars], (int)(pTruth[0] & 1) );
s_Times[0] += Abc_Clock() - clk;
return nVars;
}
static inline int Dau_DsdFindSupportOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, int u )
{
int nWords = Abc_TtWordNum(nVars);
int Status = p ? Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ) : 0;
if ( Status == 0 )
{
// Status = (Abc_Tt6HasVar(tCof1, u) << 1) | Abc_Tt6HasVar(tCof0, u);
if ( v < u )
Status = (!Abc_TtCheckEqualCofs(pTruth, nWords, v, u, 1, 3) << 1) | !Abc_TtCheckEqualCofs(pTruth, nWords, v, u, 0, 2);
else // if ( v > u )
Status = (!Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 2, 3) << 1) | !Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 1);
assert( Status != 0 );
if ( p )
Dau_DsdInsertVarCache( p, pVars[v], pVars[u], Status );
}
return Status;
}
static inline unsigned Dau_DsdFindSupports( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
{
int u;
unsigned uSupports = 0;
//Kit_DsdPrintFromTruth( (unsigned *)&tCof0, 6 );printf( "\n" );
//Kit_DsdPrintFromTruth( (unsigned *)&tCof1, 6 );printf( "\n" );
for ( u = 0; u < nVars; u++ )
if ( u != v )
uSupports |= (Dau_DsdFindSupportOne( p, pTruth, pVars, nVars, v, u ) << (2 * u));
return uSupports;
}
// checks decomposability with respect to the pair (v, u)
static inline int Dau_DsdDecomposeDoubleVarsOne( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, int u )
{
char pBuffer[10] = { 0 };
int nWords = Abc_TtWordNum(nVars);
int Status = Dau_DsdFindSupportOne( p, pTruth, pVars, nVars, v, u );
assert( v > u );
//printf( "Checking %s and %s.\n", p->pVarDefs[pVars[v]], p->pVarDefs[pVars[u]] );
if ( Status == 3 )
{
// both F(v=0) and F(v=1) depend on u
// if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) && Abc_Tt6Cof0EqualCof1(tCof1, tCof0, u) ) // v+u
if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 3) && Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 1, 2) ) // 00=11 01=10 v+u
{
word pTtTemp[2][DAU_MAX_WORD];
sprintf( pBuffer, "[%c%c]", 'a' + pVars[v], 'a' + pVars[u] );
// pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
Abc_TtCofactor0p( pTtTemp[0], pTruth, nWords, v );
Abc_TtCofactor0( pTtTemp[0], nWords, u );
Abc_TtCofactor0p( pTtTemp[1], pTruth, nWords, v );
Abc_TtCofactor1( pTtTemp[1], nWords, u );
Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
goto finish;
}
}
else if ( Status == 2 )
{
// F(v=0) does not depend on u; F(v=1) depends on u
// if ( Abc_Tt6Cof0EqualCof0(tCof0, tCof1, u) ) // vu
if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 2) ) // 00=10 vu
{
word pTtTemp[2][DAU_MAX_WORD];
sprintf( pBuffer, "(%c%c)", 'a' + pVars[v], 'a' + pVars[u] );
// pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
Abc_TtCofactor0p( pTtTemp[0], pTruth, nWords, v );
Abc_TtCofactor0( pTtTemp[0], nWords, u );
Abc_TtCofactor1p( pTtTemp[1], pTruth, nWords, v );
Abc_TtCofactor1( pTtTemp[1], nWords, u );
Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
goto finish;
}
// if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // v!u
if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 3) ) // 00=11 v!u
{
word pTtTemp[2][DAU_MAX_WORD];
sprintf( pBuffer, "(%c!%c)", 'a' + pVars[v], 'a' + pVars[u] );
// pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof1, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
Abc_TtCofactor0p( pTtTemp[0], pTruth, nWords, v );
Abc_TtCofactor0( pTtTemp[0], nWords, u );
Abc_TtCofactor1p( pTtTemp[1], pTruth, nWords, v );
Abc_TtCofactor0( pTtTemp[1], nWords, u );
Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
goto finish;
}
}
else if ( Status == 1 )
{
// F(v=0) depends on u; F(v=1) does not depend on u
// if ( Abc_Tt6Cof0EqualCof1(tCof0, tCof1, u) ) // !vu
if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 0, 3) ) // 00=11 !vu
{
word pTtTemp[2][DAU_MAX_WORD];
sprintf( pBuffer, "(!%c%c)", 'a' + pVars[v], 'a' + pVars[u] );
// pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor1(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u));
Abc_TtCofactor0p( pTtTemp[0], pTruth, nWords, v );
Abc_TtCofactor0( pTtTemp[0], nWords, u );
Abc_TtCofactor0p( pTtTemp[1], pTruth, nWords, v );
Abc_TtCofactor1( pTtTemp[1], nWords, u );
Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
goto finish;
}
// if ( Abc_Tt6Cof1EqualCof1(tCof0, tCof1, u) ) // !v!u
if ( Abc_TtCheckEqualCofs(pTruth, nWords, u, v, 1, 3) ) // 01=11 !v!u
{
word pTtTemp[2][DAU_MAX_WORD];
sprintf( pBuffer, "(!%c!%c)", 'a' + pVars[v], 'a' + pVars[u] );
// pTruth[0] = (s_Truths6[u] & Abc_Tt6Cofactor0(tCof0, u)) | (~s_Truths6[u] & Abc_Tt6Cofactor1(tCof1, u));
Abc_TtCofactor1p( pTtTemp[0], pTruth, nWords, v );
Abc_TtCofactor1( pTtTemp[0], nWords, u );
Abc_TtCofactor0p( pTtTemp[1], pTruth, nWords, v );
Abc_TtCofactor0( pTtTemp[1], nWords, u );
Abc_TtMux( pTruth, Dau_DsdTtElems()[u], pTtTemp[1], pTtTemp[0], nWords );
goto finish;
}
}
return nVars;
finish:
// finalize decomposition
assert( pBuffer[0] );
pVars[u] = Dau_DsdAddVarDef( p, pBuffer );
pVars[v] = pVars[nVars-1];
Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
if ( Dau_DsdDecomposeSingleVarOne( p, pTruth, pVars, --nVars, u ) )
nVars = Dau_DsdDecomposeSingleVar( p, pTruth, pVars, --nVars );
return nVars;
}
int Dau_DsdDecomposeDoubleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{
abctime clk = Abc_Clock();
while ( 1 )
{
int v, u, nVarsOld;
for ( v = nVars - 1; v > 0; v-- )
{
for ( u = v - 1; u >= 0; u-- )
{
if ( Dau_DsdLookupVarCache( p, pVars[v], pVars[u] ) )
continue;
nVarsOld = nVars;
nVars = Dau_DsdDecomposeDoubleVarsOne( p, pTruth, pVars, nVars, v, u );
if ( nVars == 0 )
{
s_Times[1] += Abc_Clock() - clk;
return 0;
}
if ( nVarsOld > nVars )
break;
}
if ( u >= 0 ) // found
break;
}
if ( v == 0 ) // not found
break;
}
s_Times[1] += Abc_Clock() - clk;
return nVars;
}
// look for MUX-decomposable variable on top or at the bottom
static inline int Dau_DsdDecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v )
{
extern int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit );
Dau_Dsd_t P1, * p1 = &P1;
word pTtCof[2][DAU_MAX_WORD];
int nWords = Abc_TtWordNum(nVars);
p1->fSplitPrime = 0;
p1->fWriteTruth = p->fWriteTruth;
// move this variable to the top
ABC_SWAP( int, pVars[v], pVars[nVars-1] );
Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
// cofactor w.r.t the last variable
// tCof0 = Abc_Tt6Cofactor0( pTruth[0], nVars - 1 );
// tCof1 = Abc_Tt6Cofactor1( pTruth[0], nVars - 1 );
Abc_TtCofactor0p( pTtCof[0], pTruth, nWords, nVars - 1 );
Abc_TtCofactor1p( pTtCof[1], pTruth, nWords, nVars - 1 );
// compose the result
Dau_DsdWriteString( p, "<" );
Dau_DsdWriteVar( p, pVars[nVars - 1], 0 );
// split decomposition
Dau_DsdDecomposeInt( p1, pTtCof[1], nVars - 1 );
Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
p->nSizeNonDec = p1->nSizeNonDec;
if ( p1->nSizeNonDec )
Abc_TtCopy( pTruth, pTtCof[1], Abc_TtWordNum(p1->nSizeNonDec), 0 );
// split decomposition
Dau_DsdDecomposeInt( p1, pTtCof[0], nVars - 1 );
Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
Dau_DsdWriteString( p, ">" );
p->nSizeNonDec = Abc_MaxInt( p->nSizeNonDec, p1->nSizeNonDec );
if ( p1->nSizeNonDec )
Abc_TtCopy( pTruth, pTtCof[0], Abc_TtWordNum(p1->nSizeNonDec), 0 );
return 0;
}
static inline int Dau_DsdDecomposeTripleVarsInner( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, unsigned uSupports )
{
int nWords = Abc_TtWordNum(nVars);
int iVar0 = Abc_TtSuppFindFirst( uSupports & (~uSupports >> 1) & 0x55555555 ) >> 1;
int iVar1 = Abc_TtSuppFindFirst( ~uSupports & ( uSupports >> 1) & 0x55555555 ) >> 1;
int fEqual0, fEqual1;
// word tCof0 = Abc_Tt6Cofactor0( pTruth[0], v );
// word tCof1 = Abc_Tt6Cofactor1( pTruth[0], v );
// word C00 = Abc_Tt6Cofactor0( tCof0, iVar0 );
// word C01 = Abc_Tt6Cofactor1( tCof0, iVar0 );
// word C10 = Abc_Tt6Cofactor0( tCof1, iVar1 );
// word C11 = Abc_Tt6Cofactor1( tCof1, iVar1 );
// int fEqual0 = (C00 == C10) && (C01 == C11);
// int fEqual1 = (C00 == C11) && (C01 == C10);
word pTtCof[2][DAU_MAX_WORD];
word pTtFour[2][2][DAU_MAX_WORD];
Abc_TtCofactor0p( pTtCof[0], pTruth, nWords, v );
Abc_TtCofactor1p( pTtCof[1], pTruth, nWords, v );
Abc_TtCofactor0p( pTtFour[0][0], pTtCof[0], nWords, iVar0 );
Abc_TtCofactor1p( pTtFour[0][1], pTtCof[0], nWords, iVar0 );
Abc_TtCofactor0p( pTtFour[1][0], pTtCof[1], nWords, iVar1 );
Abc_TtCofactor1p( pTtFour[1][1], pTtCof[1], nWords, iVar1 );
fEqual0 = Abc_TtEqual(pTtFour[0][0], pTtFour[1][0], nWords) && Abc_TtEqual(pTtFour[0][1], pTtFour[1][1], nWords);
fEqual1 = Abc_TtEqual(pTtFour[0][0], pTtFour[1][1], nWords) && Abc_TtEqual(pTtFour[0][1], pTtFour[1][0], nWords);
if ( fEqual0 || fEqual1 )
{
char pBuffer[10];
int VarId = pVars[iVar0];
// pTruth[0] = (s_Truths6[v] & C11) | (~s_Truths6[v] & C10);
Abc_TtMux( pTruth, Dau_DsdTtElems()[v], pTtFour[1][1], pTtFour[1][0], nWords );
sprintf( pBuffer, "<%c%c%s%c>", 'a' + pVars[v], 'a' + pVars[iVar1], fEqual1 ? "!":"", 'a' + pVars[iVar0] );
pVars[v] = Dau_DsdAddVarDef( p, pBuffer );
// remove iVar1
ABC_SWAP( int, pVars[iVar1], pVars[nVars-1] );
Abc_TtSwapVars( pTruth, nVars, iVar1, nVars-1 ); nVars--;
// remove iVar0
iVar0 = Dau_DsdFindVarDef( pVars, nVars, VarId );
ABC_SWAP( int, pVars[iVar0], pVars[nVars-1] );
Abc_TtSwapVars( pTruth, nVars, iVar0, nVars-1 ); nVars--;
// find the new var
v = Dau_DsdFindVarDef( pVars, nVars, p->nVarsUsed-1 );
// remove single variables if possible
if ( Dau_DsdDecomposeSingleVarOne( p, pTruth, pVars, nVars, v ) )
nVars = Dau_DsdDecomposeSingleVar( p, pTruth, pVars, --nVars );
return nVars;
}
return nVars;
}
int Dau_DsdDecomposeTripleVars( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{
abctime clk = Abc_Clock();
while ( 1 )
{
int v;
// Kit_DsdPrintFromTruth( (unsigned *)pTruth, 6 ); printf( "\n" );
for ( v = nVars - 1; v >= 0; v-- )
{
unsigned uSupports = Dau_DsdFindSupports( p, pTruth, pVars, nVars, v );
// Dau_DsdPrintSupports( uSupports, nVars );
if ( (uSupports & (uSupports >> 1) & 0x55555555) == 0 ) // non-overlapping supports
return Dau_DsdDecomposeTripleVarsOuter( p, pTruth, pVars, nVars, v );
if ( Abc_TtSuppOnlyOne( uSupports & (~uSupports >> 1) & 0x55555555) &&
Abc_TtSuppOnlyOne(~uSupports & ( uSupports >> 1) & 0x55555555) ) // one unique variable in each cofactor
{
int nVarsNew = Dau_DsdDecomposeTripleVarsInner( p, pTruth, pVars, nVars, v, uSupports );
if ( nVarsNew == nVars )
continue;
if ( nVarsNew == 0 )
{
s_Times[2] += Abc_Clock() - clk;
return 0;
}
nVars = Dau_DsdDecomposeDoubleVars( p, pTruth, pVars, nVarsNew );
if ( nVars == 0 )
{
s_Times[2] += Abc_Clock() - clk;
return 0;
}
break;
}
}
if ( v == -1 )
{
s_Times[2] += Abc_Clock() - clk;
return nVars;
}
}
assert( 0 );
return -1;
}
int Dau_DsdDecomposeInternal( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars )
{
// decompose single variales on the output side
nVars = Dau_DsdDecomposeSingleVar( p, pTruth, pVars, nVars );
if ( nVars == 0 )
return 0;
// decompose double variables on the input side
nVars = Dau_DsdDecomposeDoubleVars( p, pTruth, pVars, nVars );
if ( nVars == 0 )
return 0;
// decompose MUX on the output/input side
nVars = Dau_DsdDecomposeTripleVars( p, pTruth, pVars, nVars );
if ( nVars == 0 )
return 0;
// write non-decomposable function
return Dau_DsdWritePrime( p, pTruth, pVars, nVars );
}
/**Function*************************************************************
Synopsis [Fast DSD for truth tables.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Dau_DsdMinBase( word * pTruth, int nVars, int * pVarsNew )
{
int v;
for ( v = 0; v < nVars; v++ )
pVarsNew[v] = v;
for ( v = nVars - 1; v >= 0; v-- )
{
if ( Abc_TtHasVar( pTruth, nVars, v ) )
continue;
Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
pVarsNew[v] = pVarsNew[--nVars];
}
return nVars;
}
int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit )
{
int Status = 0, nVars, pVars[16];
Dau_DsdInitialize( p, nVarsInit );
nVars = Dau_DsdMinBase( pTruth, nVarsInit, pVars );
assert( nVars > 0 && nVars <= nVarsInit );
if ( nVars == 1 )
Dau_DsdWriteVar( p, pVars[0], (int)(pTruth[0] & 1) );
else if ( nVars <= 6 )
Status = Dau_Dsd6DecomposeInternal( p, pTruth, pVars, nVars );
else
Status = Dau_DsdDecomposeInternal( p, pTruth, pVars, nVars );
Dau_DsdFinalize( p );
return Status;
}
int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes )
{
Dau_Dsd_t P, * p = &P;
p->fSplitPrime = fSplitPrime;
p->fWriteTruth = fWriteTruth;
p->pVarLevels = NULL;
p->nSizeNonDec = 0;
if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
{ if ( pRes ) pRes[0] = '0', pRes[1] = 0; }
else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) )
{ if ( pRes ) pRes[0] = '1', pRes[1] = 0; }
else
{
int Status = Dau_DsdDecomposeInt( p, pTruth, nVarsInit );
Dau_DsdRemoveBraces( p->pOutput, Dau_DsdComputeMatches(p->pOutput) );
if ( pRes )
strcpy( pRes, p->pOutput );
assert( fSplitPrime || Status != 1 );
if ( fSplitPrime && Status == 2 )
return -1;
}
// assert( p->nSizeNonDec == 0 );
return p->nSizeNonDec;
}
int Dau_DsdDecomposeLevel( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes, int * pVarLevels )
{
Dau_Dsd_t P, * p = &P;
p->fSplitPrime = fSplitPrime;
p->fWriteTruth = fWriteTruth;
p->pVarLevels = pVarLevels;
p->nSizeNonDec = 0;
if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
{ if ( pRes ) pRes[0] = '0', pRes[1] = 0; }
else if ( (pTruth[0] & 1) && Abc_TtIsConst1(pTruth, Abc_TtWordNum(nVarsInit)) )
{ if ( pRes ) pRes[0] = '1', pRes[1] = 0; }
else
{
int Status = Dau_DsdDecomposeInt( p, pTruth, nVarsInit );
Dau_DsdRemoveBraces( p->pOutput, Dau_DsdComputeMatches(p->pOutput) );
if ( pRes )
strcpy( pRes, p->pOutput );
assert( fSplitPrime || Status != 1 );
if ( fSplitPrime && Status == 2 )
return -1;
}
// assert( p->nSizeNonDec == 0 );
return p->nSizeNonDec;
}
void Dau_DsdPrintFromTruthFile( FILE * pFile, word * pTruth, int nVarsInit )
{
char pRes[DAU_MAX_STR];
word pTemp[DAU_MAX_WORD];
Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
fprintf( pFile, "%s\n", pRes );
}
void Dau_DsdPrintFromTruth( word * pTruth, int nVarsInit )
{
char pRes[DAU_MAX_STR];
word pTemp[DAU_MAX_WORD];
Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
fprintf( stdout, "%s\n", pRes );
}
void Dau_DsdPrintFromTruth2( word * pTruth, int nVarsInit )
{
char pRes[DAU_MAX_STR];
word pTemp[DAU_MAX_WORD];
Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
fprintf( stdout, "%s", pRes );
}
void Dau_DsdTest44()
{
char pRes[DAU_MAX_STR];
// char * pStr = "(!(!a<bcd>)!(!fe))";
// char * pStr = "([acb]<!edf>)";
// char * pStr = "!(f!(b!c!(d[ea])))";
// char * pStr = "[!(a[be])!(c!df)]";
// char * pStr = "<(e<bca>)fd>";
// char * pStr = "[d8001{abef}c]";
char * pStr = "[dc<a(cbd)(!c!b!d)>{abef}]";
// char * pStr3;
word t = Dau_Dsd6ToTruth( pStr );
// return;
int nNonDec = Dau_DsdDecompose( &t, 6, 1, 1, pRes );
// Dau_DsdNormalize( pStr2 );
// Dau_DsdExtract( pStr, 2, 0 );
t = 0;
nNonDec = 0;
}
void Dau_DsdTest888()
{
char pDsd[DAU_MAX_STR];
int nVars = 9;
// char * pStr = "[(abc)(def)(ghi)]";
// char * pStr = "[a!b!(c!d[e(fg)hi])]";
// char * pStr = "[(abc)(def)]";
// char * pStr = "[(abc)(def)]";
// char * pStr = "[abcdefg]";
// char * pStr = "[<abc>(de[ghi])]";
char * pStr = "(<abc>(<def><ghi>))";
word * pTruth = Dau_DsdToTruth( pStr, 9 );
int i, Status;
// Kit_DsdPrintFromTruth( (unsigned *)pTruth, 9 ); printf( "\n" );
/*
for ( i = 0; i < 6; i++ )
{
unsigned uSupp = Dau_Dsd6FindSupports( NULL, pTruth, NULL, 6, i );
Dau_DsdPrintSupports( uSupp, 6 );
}
*/
/*
printf( "\n" );
for ( i = 0; i < nVars; i++ )
{
unsigned uSupp = Dau_DsdFindSupports( NULL, pTruth, NULL, nVars, i );
Dau_DsdPrintSupports( uSupp, nVars );
}
*/
Status = Dau_DsdDecompose( pTruth, nVars, 0, 0, pDsd );
i = 0;
}
void Dau_DsdTest555()
{
int nVars = 10;
int nWords = Abc_TtWordNum(nVars);
char * pFileName = "_npn/npn/dsd10.txt";
FILE * pFile = fopen( pFileName, "rb" );
word Tru[2][DAU_MAX_WORD], * pTruth;
char pBuffer[DAU_MAX_STR];
char pRes[DAU_MAX_STR];
int nSizeNonDec;
int i, Counter = 0;
abctime clk = Abc_Clock(), clkDec = 0, clk2;
// return;
while ( fgets( pBuffer, DAU_MAX_STR, pFile ) != NULL )
{
char * pStr2 = pBuffer + strlen(pBuffer)-1;
if ( *pStr2 == '\n' )
*pStr2-- = 0;
if ( *pStr2 == '\r' )
*pStr2-- = 0;
if ( pBuffer[0] == 'V' || pBuffer[0] == 0 )
continue;
Counter++;
for ( i = 0; i < 1; i++ )
{
// Dau_DsdPermute( pBuffer );
pTruth = Dau_DsdToTruth( pBuffer[0] == '*' ? pBuffer + 1 : pBuffer, nVars );
Abc_TtCopy( Tru[0], pTruth, nWords, 0 );
Abc_TtCopy( Tru[1], pTruth, nWords, 0 );
clk2 = Abc_Clock();
nSizeNonDec = Dau_DsdDecompose( Tru[1], nVars, 0, 1, pRes );
clkDec += Abc_Clock() - clk2;
Dau_DsdNormalize( pRes );
// pStr2 = Dau_DsdPerform( t ); nSizeNonDec = 0;
assert( nSizeNonDec == 0 );
pTruth = Dau_DsdToTruth( pRes, nVars );
if ( !Abc_TtEqual( pTruth, Tru[0], nWords ) )
{
// Kit_DsdPrintFromTruth( (unsigned *)&t, 6 );
// printf( " " );
// Kit_DsdPrintFromTruth( (unsigned *)&t2, 6 );
printf( "%s -> %s \n", pBuffer, pRes );
printf( "Verification failed.\n" );
}
}
}
printf( "Finished trying %d decompositions. ", Counter );
Abc_PrintTime( 1, "Time", clkDec );
Abc_PrintTime( 1, "Total", Abc_Clock() - clk );
Abc_PrintTime( 1, "Time1", s_Times[0] );
Abc_PrintTime( 1, "Time2", s_Times[1] );
Abc_PrintTime( 1, "Time3", s_Times[2] );
fclose( pFile );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END