luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Updates to arithmetic verification.

This commit is contained in:
Alan Mishchenko 2016-10-09 19:38:30 -07:00
parent 50e324ce11
commit 40375f8b93
3 changed files with 255 additions and 99 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

152
src/base/abci/abc.c
View File

@ -475,8 +475,8 @@ static int Abc_CommandAbc9Bmci ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9PoXsim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Demiter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Fadds ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Polyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9ATree ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Polyn ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Acec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Esop ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -1116,8 +1116,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&poxsim", Abc_CommandAbc9PoXsim, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&demiter", Abc_CommandAbc9Demiter, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&fadds", Abc_CommandAbc9Fadds, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&polyn", Abc_CommandAbc9Polyn, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&atree", Abc_CommandAbc9ATree, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&polyn", Abc_CommandAbc9Polyn, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&acec", Abc_CommandAbc9Acec, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&esop", Abc_CommandAbc9Esop, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&exorcism", Abc_CommandAbc9Exorcism, 0 );
@ -40183,15 +40183,89 @@ usage:
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
int Abc_CommandAbc9ATree( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Vec_Int_t * vOrder = NULL;
int c, fSimple = 1, fSigned = 0, fVerbose = 0, fVeryVerbose = 0;
extern Gia_Man_t * Gia_PolynCoreDetectTest( Gia_Man_t * pGia, int fAddExtra, int fAddCones, int fVerbose );
Gia_Man_t * pTemp = NULL;
int c, fAddExtra = 0, fAddCones = 0, fVerbose = 0, fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "asvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "ecvwh" ) ) != EOF )
{
switch ( c )
{
case 'e':
fAddExtra ^= 1;
break;
case 'c':
fAddCones ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" );
return 0;
}
pTemp = Gia_PolynCoreDetectTest( pAbc->pGia, fAddExtra, fAddCones, fVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &atree [-ecvwh]\n" );
Abc_Print( -2, "\t extracts adder tree rooting in primary outputs\n" );
Abc_Print( -2, "\t-e : toggles adding extra outputs [default = %s]\n", fAddExtra? "yes": "no" );
Abc_Print( -2, "\t-c : toggles duplicating complete AIG [default = %s]\n", fAddCones? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggles printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_PolynBuild2Test( Gia_Man_t * pGia, int nExtra, int fSigned, int fVerbose, int fVeryVerbose );
Vec_Int_t * vOrder = NULL;
int c, nExtra = -1, fOld = 0, fSimple = 1, fSigned = 0, fVerbose = 0, fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Noasvwh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
nExtra = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nExtra < 0 )
goto usage;
break;
case 'o':
fOld ^= 1;
break;
case 'a':
fSimple ^= 1;
break;
@ -40215,14 +40289,21 @@ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" );
return 0;
}
vOrder = fSimple ? NULL : Gia_PolynReorder( pAbc->pGia, fVerbose, fVeryVerbose );
Gia_PolynBuild( pAbc->pGia, vOrder, fSigned, fVerbose, fVeryVerbose );
Vec_IntFreeP( &vOrder );
if ( fOld )
{
vOrder = fSimple ? NULL : Gia_PolynReorder( pAbc->pGia, fVerbose, fVeryVerbose );
Gia_PolynBuild( pAbc->pGia, vOrder, fSigned, fVerbose, fVeryVerbose );
Vec_IntFreeP( &vOrder );
}
else
Gia_PolynBuild2Test( pAbc->pGia, nExtra, fSigned, fVerbose, fVeryVerbose );
return 0;
usage:
Abc_Print( -2, "usage: &polyn [-asvwh]\n" );
Abc_Print( -2, "usage: &polyn [-N num] [-oasvwh]\n" );
Abc_Print( -2, "\t derives algebraic polynomial from AIG\n" );
Abc_Print( -2, "\t-N num : the number of additional primary outputs (-1 = unused) [default = %d]\n", nExtra );
Abc_Print( -2, "\t-o : toggles old computation [default = %s]\n", fOld? "yes": "no" );
Abc_Print( -2, "\t-a : toggles simple computation [default = %s]\n", fSimple? "yes": "no" );
Abc_Print( -2, "\t-s : toggles signed computation [default = %s]\n", fSigned? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
@ -40231,57 +40312,6 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9ATree( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_PolynCoreDetectTest( Gia_Man_t * pGia );
Gia_Man_t * pTemp = NULL;
int c, fVerbose = 0, fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vwh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" );
return 0;
}
pTemp = Gia_PolynCoreDetectTest( pAbc->pGia );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &atree [-vwh]\n" );
Abc_Print( -2, "\t extracts adder tree rooting in primary outputs\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggles printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []

66
src/proof/acec/acecCo.c
View File

@ -70,7 +70,8 @@ Vec_Int_t * Gia_PolynAddHaRoots( Gia_Man_t * pGia )
Vec_IntPush( vNewOuts, Abc_Lit2Var(iRoot) );
}
Vec_IntFree( vXorPairs );
printf( "On top of %d COs, created %d new adder outputs.\n", Gia_ManCoNum(pGia), Vec_IntSize(vNewOuts) );
Vec_IntReverseOrder( vNewOuts );
// Vec_IntPop( vNewOuts );
return vNewOuts;
}
@ -220,15 +221,28 @@ Vec_Int_t * Gia_PolynCoreCollect( Gia_Man_t * pGia, Vec_Int_t * vAdds, Vec_Int_t
SeeAlso []
***********************************************************************/
void Gia_PolynCorePrintCones( Gia_Man_t * pGia, Vec_Int_t * vLeaves )
void Gia_PolynCorePrintCones( Gia_Man_t * pGia, Vec_Int_t * vLeaves, int fVerbose )
{
int i, iObj;
Vec_IntForEachEntry( vLeaves, iObj, i )
if ( fVerbose )
{
printf( "%4d : ", i );
printf( "Supp = %3d ", Gia_ManSuppSize(pGia, &iObj, 1) );
printf( "Cone = %3d ", Gia_ManConeSize(pGia, &iObj, 1) );
printf( "\n" );
Vec_IntForEachEntry( vLeaves, iObj, i )
{
printf( "%4d : ", i );
printf( "Supp = %3d ", Gia_ManSuppSize(pGia, &iObj, 1) );
printf( "Cone = %3d ", Gia_ManConeSize(pGia, &iObj, 1) );
printf( "\n" );
}
}
else
{
int SuppMax = 0, ConeMax = 0;
Vec_IntForEachEntry( vLeaves, iObj, i )
{
SuppMax = Abc_MaxInt( SuppMax, Gia_ManSuppSize(pGia, &iObj, 1) );
ConeMax = Abc_MaxInt( ConeMax, Gia_ManConeSize(pGia, &iObj, 1) );
}
printf( "Remaining cones: Count = %d. SuppMax = %d. ConeMax = %d.\n", Vec_IntSize(vLeaves), SuppMax, ConeMax );
}
}
@ -243,7 +257,16 @@ void Gia_PolynCorePrintCones( Gia_Man_t * pGia, Vec_Int_t * vLeaves )
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_PolynCoreDupTree( Gia_Man_t * p, Vec_Int_t * vAddCos, Vec_Int_t * vLeaves, Vec_Int_t * vNodes )
int Gia_PolynCoreDupTreePlus_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
{
if ( ~pObj->Value )
return pObj->Value;
assert( Gia_ObjIsAnd(pObj) );
Gia_PolynCoreDupTreePlus_rec( pNew, p, Gia_ObjFanin0(pObj) );
Gia_PolynCoreDupTreePlus_rec( pNew, p, Gia_ObjFanin1(pObj) );
return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
}
Gia_Man_t * Gia_PolynCoreDupTree( Gia_Man_t * p, Vec_Int_t * vAddCos, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, int fAddCones )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
@ -254,8 +277,18 @@ Gia_Man_t * Gia_PolynCoreDupTree( Gia_Man_t * p, Vec_Int_t * vAddCos, Vec_Int_t
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManConst0(p)->Value = 0;
Gia_ManForEachObjVec( vLeaves, p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
if ( fAddCones )
{
Gia_ManForEachPi( p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
Gia_ManForEachObjVec( vLeaves, p, pObj, i )
pObj->Value = Gia_PolynCoreDupTreePlus_rec( pNew, p, pObj );
}
else
{
Gia_ManForEachObjVec( vLeaves, p, pObj, i )
pObj->Value = Gia_ManAppendCi(pNew);
}
Gia_ManForEachObjVec( vNodes, p, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
Gia_ManForEachCo( p, pObj, i )
@ -277,7 +310,7 @@ Gia_Man_t * Gia_PolynCoreDupTree( Gia_Man_t * p, Vec_Int_t * vAddCos, Vec_Int_t
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos )
Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos, int fAddCones, int fVerbose )
{
extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, int fVerbose );
abctime clk = Abc_Clock();
@ -289,9 +322,9 @@ Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos )
Vec_IntSize(vAdds), Vec_IntSize(vLeaves), Vec_IntSize(vRoots), Vec_IntSize(vNodes), Vec_IntSize(vOrder) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Gia_PolynCorePrintCones( pGia, vLeaves );
Gia_PolynCorePrintCones( pGia, vLeaves, fVerbose );
pNew = Gia_PolynCoreDupTree( pGia, vAddCos, vLeaves, vNodes );
pNew = Gia_PolynCoreDupTree( pGia, vAddCos, vLeaves, vNodes, fAddCones );
Vec_IntFree( vAdds );
Vec_IntFree( vLeaves );
@ -300,10 +333,11 @@ Gia_Man_t * Gia_PolynCoreDetectTest_int( Gia_Man_t * pGia, Vec_Int_t * vAddCos )
Vec_IntFree( vNodes );
return pNew;
}
Gia_Man_t * Gia_PolynCoreDetectTest( Gia_Man_t * pGia )
Gia_Man_t * Gia_PolynCoreDetectTest( Gia_Man_t * pGia, int fAddExtra, int fAddCones, int fVerbose )
{
Vec_Int_t * vAddCos = Gia_PolynAddHaRoots( pGia );
Gia_Man_t * pNew = Gia_PolynCoreDetectTest_int( pGia, vAddCos );
Vec_Int_t * vAddCos = fAddExtra ? Gia_PolynAddHaRoots( pGia ) : Vec_IntAlloc(0);
Gia_Man_t * pNew = Gia_PolynCoreDetectTest_int( pGia, vAddCos, fAddCones, fVerbose );
printf( "On top of %d COs, created %d new adder outputs.\n", Gia_ManCoNum(pGia), Vec_IntSize(vAddCos) );
Vec_IntFree( vAddCos );
return pNew;
}

136
src/proof/acec/acecPo.c
View File

@ -32,6 +32,57 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Checks that items are unique and in order.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntPushOrderAbs( Vec_Int_t * p, int Entry )
{
int i;
for ( i = 0; i < p->nSize; i++ )
assert( Entry != p->pArray[i] );
if ( p->nSize == p->nCap )
{
if ( p->nCap < 16 )
Vec_IntGrow( p, 16 );
else
Vec_IntGrow( p, 2 * p->nCap );
}
p->nSize++;
for ( i = p->nSize-2; i >= 0; i-- )
if ( Abc_AbsInt(p->pArray[i]) < Abc_AbsInt(Entry) )
p->pArray[i+1] = p->pArray[i];
else
break;
p->pArray[i+1] = Entry;
}
static inline void Vec_IntAppendMinusAbs( Vec_Int_t * vVec1, Vec_Int_t * vVec2, int fMinus )
{
int Entry, i;
Vec_IntClear( vVec1 );
Vec_IntForEachEntry( vVec2, Entry, i )
Vec_IntPushOrderAbs( vVec1, fMinus ? -Entry : Entry );
}
static inline void Vec_IntCheckUniqueOrderAbs( Vec_Int_t * p )
{
int i;
for ( i = 1; i < p->nSize; i++ )
assert( Abc_AbsInt(p->pArray[i-1]) > Abc_AbsInt(p->pArray[i]) );
}
static inline void Vec_IntCheckUniqueOrder( Vec_Int_t * p )
{
int i;
for ( i = 1; i < p->nSize; i++ )
assert( p->pArray[i-1] < p->pArray[i] );
}
/**Function*************************************************************
Synopsis [Prints polynomial.]
@ -43,24 +94,27 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
void Gia_PolynPrintMono( Vec_Int_t * vConst, Vec_Int_t * vMono )
void Gia_PolynPrintMono( Vec_Int_t * vConst, Vec_Int_t * vMono, int Prev )
{
int k, Entry;
printf( "%c ", Prev != Abc_AbsInt(Vec_IntEntry(vConst, 0)) ? '|' : ' ' );
Vec_IntForEachEntry( vConst, Entry, k )
printf( "%s2^%d", Entry < 0 ? "-" : "+", Abc_AbsInt(Entry)-1 );
Vec_IntForEachEntry( vMono, Entry, k )
printf( " * %d", Entry );
printf( " * %d", Entry-1 );
printf( "\n" );
}
void Gia_PolynPrint( Vec_Wec_t * vPolyn )
{
Vec_Int_t * vConst, * vMono; int i;
Vec_Int_t * vConst, * vMono;
int i, Prev = -1;
printf( "Polynomial with %d monomials:\n", Vec_WecSize(vPolyn)/2 );
for ( i = 0; i < Vec_WecSize(vPolyn)/2; i++ )
{
vConst = Vec_WecEntry( vPolyn, 2*i+0 );
vMono = Vec_WecEntry( vPolyn, 2*i+1 );
Gia_PolynPrintMono( vConst, vMono );
Gia_PolynPrintMono( vConst, vMono, Prev );
Prev = Abc_AbsInt( Vec_IntEntry(vConst, 0) );
}
}
void Gia_PolynPrintStats( Vec_Wec_t * vPolyn )
@ -106,11 +160,17 @@ void Gia_PolynPrintStats( Vec_Wec_t * vPolyn )
SeeAlso []
***********************************************************************/
int Gia_PolynGetResultCompare( int * p0, int * p1 )
{
if ( p0[2] < p1[2] ) return -1;
if ( p0[2] > p1[2] ) return 1;
return 0;
}
Vec_Wec_t * Gia_PolynGetResult( Hsh_VecMan_t * pHashC, Hsh_VecMan_t * pHashM, Vec_Int_t * vCoefs )
{
Vec_Int_t * vClass, * vLevel, * vArray;
Vec_Wec_t * vPolyn, * vSorted;
int i, k, iConst, iMono;
int i, k, iConst, iMono, iFirst;
// find the largest
int nLargest = 0, nNonConst = 0;
Vec_IntForEachEntry( vCoefs, iConst, iMono )
@ -130,20 +190,26 @@ Vec_Wec_t * Gia_PolynGetResult( Hsh_VecMan_t * pHashC, Hsh_VecMan_t * pHashM, Ve
continue;
vArray = Hsh_VecReadEntry( pHashC, iConst );
vLevel = Vec_WecEntry( vSorted, Abc_AbsInt(Vec_IntEntry(vArray, 0)) );
Vec_IntPushTwo( vLevel, iConst, iMono );
vArray = Hsh_VecReadEntry( pHashM, iMono );
iFirst = Vec_IntSize(vArray) ? Vec_IntEntry(vArray, 0) : -1;
Vec_IntPushThree( vLevel, iConst, iMono, iFirst );
}
// reload in the given order
vPolyn = Vec_WecAlloc( 2*nNonConst );
Vec_WecForEachLevel( vSorted, vClass, i )
{
Vec_IntForEachEntryDouble( vClass, iConst, iMono, k )
// sort monomials by the index of the first variable
qsort( Vec_IntArray(vClass), Vec_IntSize(vClass)/3, 12, (int (*)(const void *, const void *))Gia_PolynGetResultCompare );
Vec_IntForEachEntryTriple( vClass, iConst, iMono, iFirst, k )
{
vArray = Hsh_VecReadEntry( pHashC, iConst );
Vec_IntCheckUniqueOrderAbs( vArray );
vLevel = Vec_WecPushLevel( vPolyn );
Vec_IntGrow( vLevel, Vec_IntSize(vArray) );
Vec_IntAppend( vLevel, vArray );
vArray = Hsh_VecReadEntry( pHashM, iMono );
Vec_IntCheckUniqueOrder( vArray );
vLevel = Vec_WecPushLevel( vPolyn );
Vec_IntGrow( vLevel, Vec_IntSize(vArray) );
Vec_IntAppend( vLevel, vArray );
@ -192,7 +258,7 @@ static inline void Gia_PolynMergeConstOne( Vec_Int_t * vConst, int New )
return;
}
}
Vec_IntPushUniqueOrder( vConst, New );
Vec_IntPushOrderAbs( vConst, New );
}
static inline void Gia_PolynMergeConst( Vec_Int_t * vTempC, Hsh_VecMan_t * pHashC, int iConstAdd )
{
@ -203,6 +269,8 @@ static inline void Gia_PolynMergeConst( Vec_Int_t * vTempC, Hsh_VecMan_t * pHash
Gia_PolynMergeConstOne( vTempC, New );
vConstAdd = Hsh_VecReadEntry( pHashC, iConstAdd );
}
Vec_IntCheckUniqueOrderAbs( vConstAdd );
//Vec_IntPrint( vConstAdd );
}
static inline int Gia_PolynBuildAdd( Hsh_VecMan_t * pHashC, Hsh_VecMan_t * pHashM, Vec_Int_t * vCoefs,
Vec_Wec_t * vLit2Mono, Vec_Int_t * vTempC, Vec_Int_t * vTempM )
@ -263,15 +331,15 @@ static inline int Gia_PolynHandleOne( Hsh_VecMan_t * pHashC, Hsh_VecMan_t * pHas
assert( status );
// create new monomial
if ( iLitNew0 == -1 && iLitNew1 == -1 ) // no new lit - the same const
Vec_IntAppendMinus( vTempC, vArrayC, 0 );
Vec_IntAppendMinusAbs( vTempC, vArrayC, 0 );
else if ( iLitNew0 > -1 && iLitNew1 == -1 ) // one new lit - opposite const
{
Vec_IntAppendMinus( vTempC, vArrayC, 1 );
Vec_IntAppendMinusAbs( vTempC, vArrayC, 1 );
Vec_IntPushUniqueOrder( vTempM, iLitNew0 );
}
else if ( iLitNew0 > -1 && iLitNew1 > -1 ) // both new lit - the same const
{
Vec_IntAppendMinus( vTempC, vArrayC, 0 );
Vec_IntAppendMinusAbs( vTempC, vArrayC, 0 );
Vec_IntPushUniqueOrder( vTempM, iLitNew0 );
Vec_IntPushUniqueOrder( vTempM, iLitNew1 );
}
@ -279,7 +347,7 @@ static inline int Gia_PolynHandleOne( Hsh_VecMan_t * pHashC, Hsh_VecMan_t * pHas
return Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC, vTempM );
}
Vec_Wec_t * Gia_PolynBuildNew2( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, int fSigned, int fVerbose, int fVeryVerbose )
Vec_Wec_t * Gia_PolynBuildNew2( Gia_Man_t * pGia, Vec_Int_t * vRootLits, int nExtra, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, int fSigned, int fVerbose, int fVeryVerbose )
{
abctime clk = Abc_Clock();
Vec_Wec_t * vPolyn;
@ -299,7 +367,8 @@ Vec_Wec_t * Gia_PolynBuildNew2( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int
// create output signature
Vec_IntForEachEntry( vRootLits, iLit, i )
{
Vec_IntFill( vTempC, 1, (fSigned && i == Vec_IntSize(vRootLits)-1) ? -i-1 : i+1 );
int Value = 1 + Abc_MinInt( i, Vec_IntSize(vRootLits)-nExtra );
Vec_IntFill( vTempC, 1, (fSigned && i == Vec_IntSize(vRootLits)-1-nExtra) ? -Value : Value );
Vec_IntFill( vTempM, 1, iLit );
nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC, vTempM );
nBuilds++;
@ -392,7 +461,7 @@ static inline void Gia_PolynPrepare4( Vec_Int_t * vTempC[4], Vec_Int_t * vTempM[
{
int i, k, Entry;
for ( i = 0; i < 4; i++ )
Vec_IntAppendMinus( vTempC[i], vConst, i & 1 );
Vec_IntAppendMinusAbs( vTempC[i], vConst, i & 1 );
for ( i = 0; i < 4; i++ )
Vec_IntClear( vTempM[i] );
Vec_IntForEachEntry( vMono, Entry, k )
@ -405,7 +474,7 @@ static inline void Gia_PolynPrepare4( Vec_Int_t * vTempC[4], Vec_Int_t * vTempM[
Vec_IntPushUniqueOrder( vTempM[3], iFan1 );
}
Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, int fSigned, int fVerbose, int fVeryVerbose )
Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Int_t * vRootLits, int nExtra, Vec_Int_t * vLeaves, Vec_Int_t * vNodes, int fSigned, int fVerbose, int fVeryVerbose )
{
abctime clk = Abc_Clock();
Vec_Wec_t * vPolyn;
@ -425,12 +494,17 @@ Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int_
Hsh_VecManAdd( pHashM, vTempM[0] );
Vec_IntPush( vCoefs, 0 );
if ( nExtra )
printf( "Assigning %d outputs from %d to %d rank %d.\n", nExtra, Vec_IntSize(vRootLits)-nExtra, Vec_IntSize(vRootLits)-1, Vec_IntSize(vRootLits)-nExtra );
// create output signature
Vec_IntForEachEntry( vRootLits, iLit, i )
{
Gia_PolynPrepare2( vTempC, vTempM, Abc_Lit2Var(iLit), i+1 );
if ( fSigned && i == Vec_IntSize(vRootLits)-1 )
int Value = 1 + Abc_MinInt( i, Vec_IntSize(vRootLits)-nExtra );
Gia_PolynPrepare2( vTempC, vTempM, Abc_Lit2Var(iLit), Value );
if ( fSigned && i >= Vec_IntSize(vRootLits)-nExtra-1 )
{
if ( fVeryVerbose ) printf( "Out %d : Negative Value = %d\n", i, Value-1 );
if ( Abc_LitIsCompl(iLit) )
{
nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC[1], vTempM[0] ); // -C
@ -442,6 +516,7 @@ Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int_
}
else
{
if ( fVeryVerbose ) printf( "Out %d : Positive Value = %d\n", i, Value-1 );
if ( Abc_LitIsCompl(iLit) )
{
nMonos += Gia_PolynBuildAdd( pHashC, pHashM, vCoefs, vLit2Mono, vTempC[0], vTempM[0] ); // C
@ -526,7 +601,7 @@ Vec_Wec_t * Gia_PolynBuildNew( Gia_Man_t * pGia, Vec_Int_t * vRootLits, Vec_Int_
SeeAlso []
***********************************************************************/
void Gia_PolynBuild2Test( Gia_Man_t * pGia )
void Gia_PolynBuild2Test( Gia_Man_t * pGia, int nExtra, int fSigned, int fVerbose, int fVeryVerbose )
{
Vec_Wec_t * vPolyn;
Vec_Int_t * vRootLits = Vec_IntAlloc( Gia_ManCoNum(pGia) );
@ -535,6 +610,21 @@ void Gia_PolynBuild2Test( Gia_Man_t * pGia )
Gia_Obj_t * pObj;
int i;
// print logic level
if ( nExtra == -1 )
{
int LevelMax = -1, iMax = -1;
Gia_ManLevelNum( pGia );
Gia_ManForEachCo( pGia, pObj, i )
if ( LevelMax < Gia_ObjLevel(pGia, pObj) )
{
LevelMax = Gia_ObjLevel(pGia, pObj);
iMax = i;
}
nExtra = Gia_ManCoNum(pGia) - iMax - 1;
printf( "Determined the number of extra outputs to be %d.\n", nExtra );
}
Gia_ManForEachObj( pGia, pObj, i )
if ( Gia_ObjIsCi(pObj) )
Vec_IntPush( vLeaves, i );
@ -543,10 +633,12 @@ void Gia_PolynBuild2Test( Gia_Man_t * pGia )
else if ( Gia_ObjIsCo(pObj) )
Vec_IntPush( vRootLits, Gia_ObjFaninLit0p(pGia, pObj) );
vPolyn = Gia_PolynBuildNew( pGia, vRootLits, vLeaves, vNodes, 0, 0, 0 );
// printf( "Polynomial has %d monomials.\n", Vec_WecSize(vPolyn)/2 );
// Gia_PolynPrintStats( vPolyn );
// Gia_PolynPrint( vPolyn );
vPolyn = Gia_PolynBuildNew( pGia, vRootLits, nExtra, vLeaves, vNodes, fSigned, fVerbose, fVeryVerbose );
//printf( "Polynomial has %d monomials.\n", Vec_WecSize(vPolyn)/2 );
if ( fVerbose || fVeryVerbose )
Gia_PolynPrintStats( vPolyn );
if ( fVeryVerbose )
Gia_PolynPrint( vPolyn );
Vec_WecFree( vPolyn );
Vec_IntFree( vRootLits );