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

Experiments with CEC for arithmetic circuits.

This commit is contained in:
Alan Mishchenko 2016-05-11 11:07:34 -07:00
parent c89f987dc7
commit 6e8efec57d
11 changed files with 169 additions and 74 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/aig/gia/gia.h
View File

@ -156,6 +156,7 @@ struct Gia_Man_t_
Vec_Int_t * vRegInits; // initial state
Vec_Int_t * vDoms; // dominators
Vec_Int_t * vBarBufs; // barrier buffers
Vec_Int_t * vXors; // temporary XORs
unsigned char* pSwitching; // switching activity for each object
Gia_Plc_t * pPlacement; // placement of the objects
Gia_Man_t * pAigExtra; // combinational logic of holes

7
src/aig/gia/giaDup.c
View File

@ -2995,7 +2995,12 @@ Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrim
// Gia_ObjRiToRo(p, pObj)->Value = Gia_ManAppendCi( pNew );
// create internal nodes
Vec_PtrForEachEntry( Gia_Obj_t *, vNodes, pObj, i )
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( Gia_ObjIsMux(p, pObj) )
pObj->Value = Gia_ManAppendMux( pNew, Gia_ObjFanin2Copy(p, pObj), Gia_ObjFanin1Copy(pObj), Gia_ObjFanin0Copy(pObj) );
else if ( Gia_ObjIsXor(pObj) )
pObj->Value = Gia_ManAppendXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
else
pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
// create COs
Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i )
// Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );

1
src/aig/gia/giaMan.c
View File

@ -109,6 +109,7 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_IntFreeP( &p->vRegInits );
Vec_IntFreeP( &p->vDoms );
Vec_IntFreeP( &p->vBarBufs );
Vec_IntFreeP( &p->vXors );
Vec_IntFreeP( &p->vLevels );
Vec_IntFreeP( &p->vTruths );
Vec_IntErase( &p->vCopies );

2
src/aig/gia/giaShow.c
View File

@ -156,7 +156,7 @@ int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds,
Vec_IntWriteEntry( vRemap, pFanins[0], pFanins[1] );
//printf( "Making HA output %d.\n", pFanins[1] );
}
else
else // if ( Attr == 3 || Attr == 0 )
{
Gia_Obj_t * pObj = Gia_ManObj( p, Node );
int pFaninsIn[2] = { Gia_ObjFaninId0(pObj, Node), Gia_ObjFaninId1(pObj, Node) };

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

@ -39306,15 +39306,18 @@ usage:
int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Vec_Int_t * vOrder = NULL;
int c, fSimple = 0, fVerbose = 0, fVeryVerbose = 0;
int c, fSimple = 0, fSigned = 0, fVerbose = 0, fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "svwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "asvwh" ) ) != EOF )
{
switch ( c )
{
case 's':
case 'a':
fSimple ^= 1;
break;
case 's':
fSigned ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -39333,14 +39336,15 @@ int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
vOrder = fSimple ? NULL : Gia_PolynReorder( pAbc->pGia, fVerbose, fVeryVerbose );
Gia_PolynBuild( pAbc->pGia, vOrder, fVerbose, fVeryVerbose );
Gia_PolynBuild( pAbc->pGia, vOrder, fSigned, fVerbose, fVeryVerbose );
Vec_IntFreeP( &vOrder );
return 0;
usage:
Abc_Print( -2, "usage: &polyn [-svwh]\n" );
Abc_Print( -2, "usage: &polyn [-asvwh]\n" );
Abc_Print( -2, "\t derives algebraic polynomial from AIG\n" );
Abc_Print( -2, "\t-s : toggles simple computation [default = %s]\n", fSimple? "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" );
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");

2
src/proof/acec/acec.h
View File

@ -59,7 +59,7 @@ extern Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose );
extern Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose );
extern Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose );
/*=== acecPolyn.c ========================================================*/
extern void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVeryVerbose );
extern void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fSigned, int fVerbose, int fVeryVerbose );
ABC_NAMESPACE_HEADER_END

4
src/proof/acec/acecCore.c
View File

@ -46,8 +46,8 @@ int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars )
{
Vec_Int_t * vOrder0 = Gia_PolynReorder( pGia0, pPars->fVerbose, pPars->fVeryVerbose );
Vec_Int_t * vOrder1 = Gia_PolynReorder( pGia1, pPars->fVerbose, pPars->fVeryVerbose );
Gia_PolynBuild( pGia0, vOrder0, pPars->fVerbose, pPars->fVeryVerbose );
Gia_PolynBuild( pGia1, vOrder1, pPars->fVerbose, pPars->fVeryVerbose );
Gia_PolynBuild( pGia0, vOrder0, 0, pPars->fVerbose, pPars->fVeryVerbose );
Gia_PolynBuild( pGia1, vOrder1, 0, pPars->fVerbose, pPars->fVeryVerbose );
Vec_IntFree( vOrder0 );
Vec_IntFree( vOrder1 );
return 1;

1
src/proof/acec/acecInt.h
View File

@ -56,6 +56,7 @@ ABC_NAMESPACE_HEADER_START
/*=== acecUtil.c ========================================================*/
extern void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose );
extern Vec_Int_t * Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose );
ABC_NAMESPACE_HEADER_END

64
src/proof/acec/acecOrder.c
View File

@ -44,20 +44,41 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int fVerbose, int fVeryVerbose )
{
int fDumpLeftOver = 0;
int i, iXor, iMaj, iAnd, Entry, Iter, fFound, fFoundAll = 1;
Vec_Int_t * vRecord = Vec_IntAlloc( 100 );
Vec_Int_t * vRecord = Vec_IntAlloc( 100 ), * vLeft, * vRecord2;
Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(pGia) );
Gia_ManForEachCoDriverId( pGia, iAnd, i )
Vec_IntWriteEntry( vMap, iAnd, 1 );
// collect the last XOR
Vec_IntFreeP( &pGia->vXors );
pGia->vXors = Gia_PolynCollectLastXor( pGia, fVerbose );
printf( "Collected %d topmost XORs\n", Vec_IntSize(pGia->vXors) );
//Vec_IntPrint( p->vXors );
Vec_IntForEachEntry( pGia->vXors, iAnd, i )
{
Gia_Obj_t * pAnd = Gia_ManObj( pGia, iAnd );
assert( Vec_IntEntry(vMap, iAnd) );
Vec_IntWriteEntry( vMap, iAnd, 0 );
Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iAnd), 1 );
Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iAnd), 1 );
Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 3) );
if ( fVeryVerbose )
printf( "Recognizing %d => XXXOR(%d %d)\n", iAnd, Gia_ObjFaninId0(pAnd, iAnd), Gia_ObjFaninId1(pAnd, iAnd) );
}
// detect FAs and HAs
for ( Iter = 0; fFoundAll; Iter++ )
{
if ( fVeryVerbose )
printf( "Iteration %d\n", Iter );
// check if we can extract FADDs
fFoundAll = 0;
do {
fFound = 0;
for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ )
for ( i = Vec_IntSize(vFadds)/5 - 1; i >= 0; i-- )
{
iXor = Vec_IntEntry(vFadds, 5*i+3);
iMaj = Vec_IntEntry(vFadds, 5*i+4);
@ -68,8 +89,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+0), 1 );
Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+1), 1 );
Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+2), 1 );
//Vec_IntPush( vRecord, iXor );
//Vec_IntPush( vRecord, iMaj );
Vec_IntPush( vRecord, Abc_Var2Lit2(i, 2) );
fFound = 1;
fFoundAll = 1;
@ -81,7 +100,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
// check if we can extract HADDs
do {
fFound = 0;
for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ )
for ( i = Vec_IntSize(vHadds)/2 - 1; i >= 0; i-- )
{
iXor = Vec_IntEntry(vHadds, 2*i+0);
iMaj = Vec_IntEntry(vHadds, 2*i+1);
@ -92,8 +111,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
Vec_IntWriteEntry( vMap, iMaj, 0 );
Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iMaj), 1 );
Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iMaj), 1 );
//Vec_IntPush( vRecord, iXor );
//Vec_IntPush( vRecord, iMaj );
Vec_IntPush( vRecord, Abc_Var2Lit2(i, 1) );
fFound = 1;
fFoundAll = 1;
@ -105,6 +122,7 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
} while ( fFound );
if ( fFoundAll )
continue;
/*
// find the last one
Vec_IntForEachEntryReverse( vMap, Entry, iAnd )
if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, iAnd)) )//&& Vec_IntFind(vFadds, iAnd) == -1 )//&& Vec_IntFind(vHadds, iAnd) == -1 )
@ -115,7 +133,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
Vec_IntWriteEntry( vMap, iAnd, 0 );
Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iAnd), 1 );
Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iAnd), 1 );
//Vec_IntPush( vRecord, iAnd );
Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 0) );
}
else
@ -123,7 +140,6 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
Vec_IntWriteEntry( vMap, iAnd, 0 );
Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan0), 1 );
Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan1), 1 );
//Vec_IntPush( vRecord, iAnd );
Vec_IntPush( vRecord, Abc_Var2Lit2(iAnd, 0) );
Vec_IntPush( vRecord, Abc_Var2Lit2(Gia_ObjFaninId0(pAnd, iAnd), 0) );
Vec_IntPush( vRecord, Abc_Var2Lit2(Gia_ObjFaninId1(pAnd, iAnd), 0) );
@ -134,21 +150,39 @@ Vec_Int_t * Gia_PolynFindOrder( Gia_Man_t * pGia, Vec_Int_t * vFadds, Vec_Int_t
printf( "Recognizing %d => AND(%d %d)\n", iAnd, Gia_ObjFaninId0(pAnd, iAnd), Gia_ObjFaninId1(pAnd, iAnd) );
break;
}
*/
}
//Vec_IntPrint( vMap );
/*
// collect remaining ones
vLeft = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vMap, Entry, i )
if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, i)) )
Vec_IntPush( vLeft, i );
Vec_IntFree( vMap );
// collect them in the topo order
vRecord2 = Vec_IntAlloc( 100 );
Gia_ManIncrementTravId( pGia );
Gia_ManCollectAnds( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), vRecord2, NULL );
Vec_IntForEachEntry( vRecord2, iAnd, i )
Vec_IntWriteEntry( vRecord2, i, Abc_Var2Lit2(iAnd, 0) );
// dump remaining nodes as an AIG
if ( fDumpLeftOver )
{
Gia_Man_t * pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vMap), Vec_IntSize(vMap), 0 );
Gia_Man_t * pNew;
pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vLeft), Vec_IntSize(vLeft), 0 );
Gia_AigerWrite( pNew, "leftover.aig", 0, 0 );
printf( "Leftover AIG with %d nodes is dumped into file \"%s\".\n", Gia_ManAndNum(pNew), "leftover.aig" );
Gia_ManStop( pNew );
}
*/
Vec_IntFree( vMap );
Vec_IntFree( vLeft );
Vec_IntReverseOrder( vRecord );
return vRecord;
Vec_IntAppend( vRecord2, vRecord );
Vec_IntFree( vRecord );
return vRecord2;
}
/**Function*************************************************************
@ -191,7 +225,9 @@ Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose, int fVeryVerbose )
}
else
Gia_ManCollectAnds_rec( pGia, Node, vOrder );
//printf( "Order = %d. Node = %d. Size = %d ", i, Node, Vec_IntSize(vOrder) );
}
//printf( "\n" );
//assert( Vec_IntSize(vOrder) == Gia_ManAndNum(pGia) );
// remap order

129
src/proof/acec/acecPolyn.c
View File

@ -54,7 +54,8 @@ struct Pln_Man_t_
Vec_Int_t * vTempC[2]; // polynomial representation
Vec_Int_t * vTempM[4]; // polynomial representation
Vec_Int_t * vOrder; // order of collapsing
int nBuilds; // builds
int nBuilds; // built monomials
int nUsed; // used monomials
};
////////////////////////////////////////////////////////////////////////
@ -144,7 +145,10 @@ void Pln_ManPrintFinal( Pln_Man_t * p, int fVerbose, int fVeryVerbose )
Count++;
if ( !fVeryVerbose )
if ( !fVerbose )
continue;
if ( Count > 25 )
continue;
vArray = Hsh_VecReadEntry( p->pHashC, iConst );
@ -159,6 +163,25 @@ void Pln_ManPrintFinal( Pln_Man_t * p, int fVerbose, int fVeryVerbose )
printf( "HashC = %d. HashM = %d. Total = %d. Used = %d.\n", Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, Count );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
static inline void Vec_IntAppendMinus2x( Vec_Int_t * vVec1, Vec_Int_t * vVec2 )
{
int Entry, i;
Vec_IntClear( vVec1 );
Vec_IntForEachEntry( vVec2, Entry, i )
Vec_IntPush( vVec1, Entry > 0 ? -Entry-1 : -Entry+1 );
}
/**Function*************************************************************
Synopsis []
@ -210,7 +233,7 @@ static inline void Gia_PolynMergeConst( Vec_Int_t * vConst, Pln_Man_t * p, int i
}
static inline void Gia_PolynBuildAdd( Pln_Man_t * p, Vec_Int_t * vTempC, Vec_Int_t * vTempM )
{
int iConst, iMono = vTempM ? Hsh_VecManAdd(p->pHashM, vTempM) : 0;
int iConst, iConstNew, iMono = vTempM ? Hsh_VecManAdd(p->pHashM, vTempM) : 0;
p->nBuilds++;
if ( iMono == Vec_IntSize(p->vCoefs) ) // new monomial
{
@ -220,14 +243,21 @@ static inline void Gia_PolynBuildAdd( Pln_Man_t * p, Vec_Int_t * vTempC, Vec_Int
Vec_FltPush( p->vCounts, (float)Vec_IntEntry(p->vOrder, Vec_IntEntryLast(vTempM)) );
Vec_QuePush( p->vQue, iMono );
// Vec_QueUpdate( p->vQue, iMono );
if ( iConst )
p->nUsed++;
return;
}
// this monomial exists
iConst = Vec_IntEntry( p->vCoefs, iMono );
if ( iConst )
Gia_PolynMergeConst( vTempC, p, iConst );
iConst = Hsh_VecManAdd( p->pHashC, vTempC );
Vec_IntWriteEntry( p->vCoefs, iMono, iConst );
iConstNew = Hsh_VecManAdd( p->pHashC, vTempC );
Vec_IntWriteEntry( p->vCoefs, iMono, iConstNew );
if ( iConst && !iConstNew )
p->nUsed--;
else if ( !iConst && iConstNew )
p->nUsed++;
//assert( p->nUsed == Vec_IntSize(p->vCoefs) - Vec_IntCountZero(p->vCoefs) );
}
void Gia_PolynBuildOne( Pln_Man_t * p, int iMono )
{
@ -242,11 +272,13 @@ void Gia_PolynBuildOne( Pln_Man_t * p, int iMono )
pObj = Gia_ManObj( p->pGia, iDriver );
if ( !Gia_ObjIsAnd(pObj) )
return;
assert( !Gia_ObjIsMux(p->pGia, pObj) );
iConst = Vec_IntEntry( p->vCoefs, iMono );
if ( iConst == 0 )
return;
Vec_IntWriteEntry( p->vCoefs, iMono, 0 );
p->nUsed--;
iFan0 = Gia_ObjFaninId0p(p->pGia, pObj);
iFan1 = Gia_ObjFaninId1p(p->pGia, pObj);
@ -264,10 +296,29 @@ void Gia_PolynBuildOne( Pln_Man_t * p, int iMono )
}
vConst = Hsh_VecReadEntry( p->pHashC, iConst );
for ( k = 0; k < 2; k++ )
Vec_IntAppendMinus( p->vTempC[k], vConst, k );
if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) // C * (1 - x) * (1 - y)
if ( !Gia_ObjIsXor(pObj) )
for ( k = 0; k < 2; k++ )
Vec_IntAppendMinus( p->vTempC[k], vConst, k );
if ( Gia_ObjIsXor(pObj) )
{
vConst = Hsh_VecReadEntry( p->pHashC, iConst );
Vec_IntAppendMinus( p->vTempC[0], vConst, 0 );
Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[1] ); // C * x
vConst = Hsh_VecReadEntry( p->pHashC, iConst );
Vec_IntAppendMinus( p->vTempC[0], vConst, 0 );
Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[2] ); // C * y
//if ( !p->pGia->vXors || Vec_IntFind(p->pGia->vXors, iDriver) > 0 )
{
vConst = Hsh_VecReadEntry( p->pHashC, iConst );
Vec_IntAppendMinus2x( p->vTempC[0], vConst );
Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] ); // -C * x * y
}
}
else if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) // C * (1 - x) * (1 - y)
{
Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * 1
Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[1] ); // -C * x
@ -290,36 +341,7 @@ void Gia_PolynBuildOne( Pln_Man_t * p, int iMono )
else
Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] ); // C * x * y
}
int Gia_PolyFindNext2( Pln_Man_t * p )
{
Gia_Obj_t * pObj;
Vec_Int_t * vArray;
int Max = 0, iBest = 0, iConst, iMono, iDriver;
Vec_IntForEachEntryStart( p->vCoefs, iConst, iMono, 1 )
{
if ( iConst == 0 )
continue;
vArray = Hsh_VecReadEntry( p->pHashM, iMono );
iDriver = Vec_IntEntryLast( vArray );
pObj = Gia_ManObj( p->pGia, iDriver );
if ( !Gia_ObjIsAnd(pObj) )
continue;
if ( Max < Vec_IntEntryLast(vArray) )
{
Max = Vec_IntEntryLast(vArray);
iBest = iMono;
}
}
//Vec_IntPrint( Hsh_VecReadEntry(p->pHashM, iBest) );
return iBest;
}
int Gia_PolyFindNext( Pln_Man_t * p )
{
int iBest = Vec_QueSize(p->vQue) ? Vec_QuePop(p->vQue) : 0;
//Vec_IntPrint( Hsh_VecReadEntry(p->pHashM, iBest) );
return iBest;
}
void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVeryVerbose )
void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fSigned, int fVerbose, int fVeryVerbose )
{
abctime clk = Abc_Clock();//, clk2 = 0;
Gia_Obj_t * pObj;
@ -334,22 +356,35 @@ void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVe
iDriver = Gia_ObjFaninId0p( pGia, pObj );
Vec_IntFill( p->vTempM[0], 1, iDriver ); // Driver
if ( Gia_ObjFaninC0(pObj) )
if ( fSigned && i == Gia_ManCoNum(pGia)-1 )
{
Gia_PolynBuildAdd( p, p->vTempC[0], NULL ); // C
Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] ); // -C * Driver
if ( Gia_ObjFaninC0(pObj) )
{
Gia_PolynBuildAdd( p, p->vTempC[1], NULL ); // -C
Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * Driver
}
else
Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] ); // -C * Driver
}
else
{
if ( Gia_ObjFaninC0(pObj) )
{
Gia_PolynBuildAdd( p, p->vTempC[0], NULL ); // C
Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] ); // -C * Driver
}
else
Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * Driver
}
else
Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * Driver
}
LevPrev = -1;
for ( Iter = 0; ; Iter++ )
{
Vec_Int_t * vTempM;
//abctime temp = Abc_Clock();
iMono = Gia_PolyFindNext(p);
if ( !iMono )
if ( Vec_QueSize(p->vQue) == 0 )
break;
iMono = Vec_QuePop(p->vQue);
// report
vTempM = Hsh_VecReadEntry( p->pHashM, iMono );
@ -366,8 +401,8 @@ void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose, int fVe
Vec_BitSetEntry( vPres, LevCur, 1 );
if ( fVerbose )
printf( "Line%5d Iter%10d : Obj =%6d. Order =%6d. HashC =%6d. HashM =%10d. Total =%10d. Used =%6d.\n",
Line++, Iter, LevCur, Vec_IntEntry(p->vOrder, LevCur), Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, -1 );
printf( "Line%5d Iter%10d : Obj =%6d. Order =%6d. HashC =%6d. HashM =%10d. Total =%10d. Used =%10d.\n",
Line++, Iter, LevCur, Vec_IntEntry(p->vOrder, LevCur), Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, p->nUsed );
}
LevPrev = LevCur;

16
src/proof/acec/acecUtil.c
View File

@ -48,11 +48,23 @@ void Gia_PolynCollectXors_rec( Gia_Man_t * pGia, int iObj, Vec_Int_t * vXors )
if ( Gia_ObjIsTravIdCurrent(pGia, pObj) )
return;
Gia_ObjSetTravIdCurrent(pGia, pObj);
if ( !Gia_ObjIsAnd(pObj) || !Gia_ObjIsXor(pObj) )
if ( !Gia_ObjIsAnd(pObj) || !Gia_ObjIsXor(pObj) || Gia_ObjRefNum(pGia, pObj) > 1 )
return;
Vec_IntPush( vXors, iObj );
Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId0(pObj, iObj), vXors );
Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId1(pObj, iObj), vXors );
Vec_IntPushUnique( vXors, iObj );
}
Vec_Int_t * Gia_PolynCollectLastXor( Gia_Man_t * pGia, int fVerbose )
{
Vec_Int_t * vXors = Vec_IntAlloc( 100 );
Gia_Obj_t * pObj = Gia_ManCo( pGia, Gia_ManCoNum(pGia)-1 );
ABC_FREE( pGia->pRefs );
Gia_ManCreateRefs( pGia );
Gia_ManIncrementTravId( pGia );
Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId0p(pGia, pObj), vXors );
Vec_IntReverseOrder( vXors );
ABC_FREE( pGia->pRefs );
return vXors;
}
void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose )
{