Skip to content

A
abc
Commit 324d73c2 by Alan Mishchenko
Options

New fast extract.

parent ae9a4407
Showing with 55 additions and 127 deletions
abclib.dsp
......@@ -259,6 +259,10 @@ SOURCE=.\src\base\abci\abcFraig.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcFx.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcFxu.c
# End Source File
# Begin Source File
......@@ -2651,6 +2655,10 @@ SOURCE=.\src\misc\vec\vecFlt.h
# End Source File
# Begin Source File
SOURCE=.\src\misc\vec\vecHsh.h
# End Source File
# Begin Source File
SOURCE=.\src\misc\vec\vecInt.h
# End Source File
# Begin Source File
......@@ -2679,6 +2687,10 @@ SOURCE=.\src\misc\vec\vecVec.h
# End Source File
# Begin Source File
SOURCE=.\src\misc\vec\vecWec.h
# End Source File
# Begin Source File
SOURCE=.\src\misc\vec\vecWrd.h
# End Source File
# End Group
......
src/base/abci/abc.c
......@@ -3527,13 +3527,14 @@ usage:
***********************************************************************/
int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Abc_NtkFxPerform( Abc_Ntk_t * pNtk, int fVerbose );
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
Fxu_Data_t Params, * p = &Params;
int c;
int c, fNewAlgo = 0;
// set the defaults
Abc_NtkSetDefaultParams( p );
Extra_UtilGetoptReset();
while ( (c = Extra_UtilGetopt(argc, argv, "SDNWsdzcvh")) != EOF )
while ( (c = Extra_UtilGetopt(argc, argv, "SDNWsdzcnvh")) != EOF )
{
switch (c)
{
......@@ -3593,6 +3594,9 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
p->fUseCompl ^= 1;
break;
case 'n':
fNewAlgo ^= 1;
break;
case 'v':
p->fVerbose ^= 1;
break;
......@@ -3615,17 +3619,25 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( !Abc_NtkIsLogic(pNtk) )
{
Abc_Print( -1, "Fast extract can only be applied to a logic network (run \"renode\").\n" );
Abc_Print( -1, "Fast extract can only be applied to a logic network (run \"renode\" or \"if\").\n" );
return 1;
}
if ( !Abc_NtkIsSopLogic(pNtk) )
{
Abc_Print( -1, "Fast extract can only be applied to a logic network with SOP local functions (run \"bdd; sop\").\n" );
return 1;
}
// the nodes to be merged are linked into the special linked list
Abc_NtkFastExtract( pNtk, p );
if ( fNewAlgo )
Abc_NtkFxPerform( pNtk, p->fVerbose );
else
Abc_NtkFastExtract( pNtk, p );
Abc_NtkFxuFreeInfo( p );
return 0;
usage:
Abc_Print( -2, "usage: fx [-SDNW <num>] [-sdzcvh]\n");
Abc_Print( -2, "usage: fx [-SDNW <num>] [-sdzcnvh]\n");
Abc_Print( -2, "\t performs unate fast extract on the current network\n");
Abc_Print( -2, "\t-S <num> : max number of single-cube divisors to consider [default = %d]\n", p->nSingleMax );
Abc_Print( -2, "\t-D <num> : max number of double-cube divisors to consider [default = %d]\n", p->nPairsMax );
......@@ -3635,6 +3647,7 @@ usage:
Abc_Print( -2, "\t-d : use only double-cube divisors [default = %s]\n", p->fOnlyD? "yes": "no" );
Abc_Print( -2, "\t-z : use zero-weight divisors [default = %s]\n", p->fUse0? "yes": "no" );
Abc_Print( -2, "\t-c : use complement in the binary case [default = %s]\n", p->fUseCompl? "yes": "no" );
Abc_Print( -2, "\t-n : use new implementation of fast extract [default = %s]\n", fNewAlgo? "yes": "no" );
Abc_Print( -2, "\t-v : print verbose information [default = %s]\n", p->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
......
src/base/abci/module.make
......@@ -17,6 +17,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcDsd.c \
src/base/abci/abcExtract.c \
src/base/abci/abcFraig.c \
src/base/abci/abcFx.c \
src/base/abci/abcFxu.c \
src/base/abci/abcGen.c \
src/base/abci/abcHaig.c \
......
src/misc/vec/vecInt.h
......@@ -1193,6 +1193,24 @@ static inline int Vec_IntUniqify( Vec_Int_t * p )
p->nSize = k;
return RetValue;
}
static inline int Vec_IntCountDuplicates( Vec_Int_t * p )
{
int RetValue;
Vec_Int_t * pDup = Vec_IntDup( p );
Vec_IntUniqify( pDup );
RetValue = Vec_IntSize(p) - Vec_IntSize(pDup);
Vec_IntFree( pDup );
return RetValue;
}
static inline int Vec_IntCheckUniqueSmall( Vec_Int_t * p )
{
int i, k;
for ( i = 0; i < p->nSize; i++ )
for ( k = i+1; k < p->nSize; k++ )
if ( p->pArray[i] == p->pArray[k] )
return 0;
return 1;
}
/**Function*************************************************************
......
src/misc/vec/vecQue.h
......@@ -140,6 +140,10 @@ static inline int Vec_QueTop( Vec_Que_t * p )
{
return Vec_QueSize(p) > 0 ? p->pHeap[1] : -1;
}
static inline float Vec_QueTopCost( Vec_Que_t * p )
{
return Vec_QueSize(p) > 0 ? Vec_QueCost(p, p->pHeap[1]) : -ABC_INFINITY;
}
/**Function*************************************************************
......
src/misc/vec/vecVec.h
......@@ -253,6 +253,7 @@ static inline int Vec_VecCap( Vec_Vec_t * p )
***********************************************************************/
static inline int Vec_VecLevelSize( Vec_Vec_t * p, int i )
{
assert( i >= 0 && i < p->nSize );
return Vec_PtrSize( (Vec_Ptr_t *)p->pArray[i] );
}
......@@ -617,7 +618,7 @@ static inline void Vec_VecPrintInt( Vec_Vec_t * p, int fSkipSingles )
int i, k, Entry;
Vec_VecForEachEntryInt( p, Entry, i, k )
{
if ( Vec_VecLevelSize(p, i) == 1 )
if ( fSkipSingles && Vec_VecLevelSize(p, i) == 1 )
break;
if ( k == 0 )
printf( " %4d : {", i );
......
src/proof/abs/absGla.c
......@@ -1153,27 +1153,6 @@ void Ga2_ManRestart( Ga2_Man_t * p )
SeeAlso []
***********************************************************************/
int Vec_IntCheckUnique( Vec_Int_t * p )
{
int RetValue;
Vec_Int_t * pDup = Vec_IntDup( p );
Vec_IntUniqify( pDup );
RetValue = Vec_IntSize(p) - Vec_IntSize(pDup);
Vec_IntFree( pDup );
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Ga2_ObjSatValue( Ga2_Man_t * p, Gia_Obj_t * pObj, int f )
{
int Lit = Ga2_ObjFindLit( p, pObj, f );
......
src/proof/ssc/sscUtil.c
......@@ -27,27 +27,6 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Hsh_Obj_t_ Hsh_Obj_t;
struct Hsh_Obj_t_
{
int iThis;
int iNext;
};
typedef struct Hsh_Man_t_ Hsh_Man_t;
struct Hsh_Man_t_
{
unsigned * pData; // user's data
int * pTable; // hash table
Hsh_Obj_t * pObjs;
int nObjs;
int nSize;
int nTableSize;
};
static inline unsigned * Hsh_ObjData( Hsh_Man_t * p, int iThis ) { return p->pData + p->nSize * iThis; }
static inline Hsh_Obj_t * Hsh_ObjGet( Hsh_Man_t * p, int iObj ) { return iObj == -1 ? NULL : p->pObjs + iObj; }
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
......@@ -63,85 +42,6 @@ static inline Hsh_Obj_t * Hsh_ObjGet( Hsh_Man_t * p, int iObj ) { return
SeeAlso []
***********************************************************************/
Hsh_Man_t * Hsh_ManStart( unsigned * pData, int nDatas, int nSize )
{
Hsh_Man_t * p;
p = ABC_CALLOC( Hsh_Man_t, 1 );
p->pData = pData;
p->nSize = nSize;
p->nTableSize = Abc_PrimeCudd( nDatas );
p->pTable = ABC_FALLOC( int, p->nTableSize );
p->pObjs = ABC_FALLOC( Hsh_Obj_t, p->nTableSize );
return p;
}
void Hsh_ManStop( Hsh_Man_t * p )
{
ABC_FREE( p->pObjs );
ABC_FREE( p->pTable );
ABC_FREE( p );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline int Hsh_ManHash( unsigned * pData, int nSize, int nTableSize )
{
static unsigned s_BigPrimes[7] = {12582917, 25165843, 50331653, 100663319, 201326611, 402653189, 805306457};
unsigned char * pDataC = (unsigned char *)pData;
int c, nChars = nSize * 4, Key = 0;
for ( c = 0; c < nChars; c++ )
Key += pDataC[c] * s_BigPrimes[c % 7];
return Key % nTableSize;
}
int Hsh_ManAdd( Hsh_Man_t * p, int iThis )
{
Hsh_Obj_t * pObj;
unsigned * pThis = Hsh_ObjData( p, iThis );
int * pPlace = p->pTable + Hsh_ManHash( pThis, p->nSize, p->nTableSize );
for ( pObj = Hsh_ObjGet(p, *pPlace); pObj; pObj = Hsh_ObjGet(p, pObj->iNext) )
if ( !memcmp( pThis, Hsh_ObjData(p, pObj->iThis), sizeof(unsigned) * p->nSize ) )
return pObj - p->pObjs;
assert( p->nObjs < p->nTableSize );
pObj = p->pObjs + p->nObjs;
pObj->iThis = iThis;
return (*pPlace = p->nObjs++);
}
/**Function*************************************************************
Synopsis [Hashes data by value.]
Description [Array of 'nTotal' int entries, each of size 'nSize' ints,
is hashed and the resulting unique numbers is returned in the array.]
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Int_t * Hsh_ManHashData( unsigned * pData, int nDatas, int nSize, int nInts )
{
Vec_Int_t * vRes;
Hsh_Man_t * p;
int i;
assert( nDatas * nSize == nInts );
p = Hsh_ManStart( pData, nDatas, nSize );
vRes = Vec_IntAlloc( 1000 );
for ( i = 0; i < nDatas; i++ )
Vec_IntPush( vRes, Hsh_ManAdd(p, i) );
Hsh_ManStop( p );
return vRes;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment