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

Several changes in arithmetic circuit manipulation.

This commit is contained in:
Alan Mishchenko 2016-12-22 17:27:32 +07:00
parent cf5d4ad07f
commit b56a532682
8 changed files with 430 additions and 24 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -5463,6 +5463,10 @@ SOURCE=.\src\proof\acec\acec.h
# End Source File
# Begin Source File
SOURCE=.\src\proof\acec\acecBo.c
# End Source File
# Begin Source File
SOURCE=.\src\proof\acec\acecCl.c
# End Source File
# Begin Source File

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

@ -1403,7 +1403,7 @@ extern Gia_Man_t * Gia_ManCleanupOutputs( Gia_Man_t * p, int nOutputs );
extern Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose );
/*=== giaShow.c ===========================================================*/
extern void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders );
extern void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds );
/*=== giaShrink.c ===========================================================*/
extern Gia_Man_t * Gia_ManMapShrink4( Gia_Man_t * p, int fKeepLevel, int fVerbose );
extern Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int nFanoutMax, int fKeepLevel, int fVerbose );

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

@ -3377,6 +3377,26 @@ Gia_Man_t * Gia_ManDupOuts( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
Vec_Wec_t * Gia_ManCreateNodeSupps( Gia_Man_t * p, Vec_Int_t * vNodes, int fVerbose )
{
abctime clk = Abc_Clock();
Gia_Obj_t * pObj; int i, Id;
Vec_Wec_t * vSuppsNo = Vec_WecStart( Vec_IntSize(vNodes) );
Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) );
Gia_ManForEachCiId( p, Id, i )
Vec_IntPush( Vec_WecEntry(vSupps, Id), i );
Gia_ManForEachAnd( p, pObj, Id )
Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)),
Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)),
Vec_WecEntry(vSupps, Id) );
Gia_ManForEachObjVec( vNodes, p, pObj, i )
Vec_IntAppend( Vec_WecEntry(vSuppsNo, i), Vec_WecEntry(vSupps, Gia_ObjId(p, pObj)) );
Vec_WecFree( vSupps );
if ( fVerbose )
Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk );
return vSuppsNo;
}
Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose )
{
abctime clk = Abc_Clock();
@ -3679,6 +3699,81 @@ Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose )
return pNew;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Gia_ManDupDemiterOrderXors2( Gia_Man_t * p, Vec_Int_t * vXors )
{
int i, iObj, * pPerm;
Vec_Int_t * vSizes = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vXors, iObj, i )
Vec_IntPush( vSizes, Gia_ManSuppSize(p, &iObj, 1) );
pPerm = Abc_MergeSortCost( Vec_IntArray(vSizes), Vec_IntSize(vSizes) );
Vec_IntClear( vSizes );
for ( i = 0; i < Vec_IntSize(vXors); i++ )
Vec_IntPush( vSizes, Vec_IntEntry(vXors, pPerm[i]) );
ABC_FREE( pPerm );
Vec_IntClear( vXors );
Vec_IntAppend( vXors, vSizes );
Vec_IntFree( vSizes );
}
int Gia_ManDupDemiterFindMin( Vec_Wec_t * vSupps, Vec_Int_t * vTakenIns, Vec_Int_t * vTakenOuts )
{
Vec_Int_t * vLevel;
int i, k, iObj, iObjBest = -1;
int Count, CountBest = ABC_INFINITY;
Vec_WecForEachLevel( vSupps, vLevel, i )
{
if ( Vec_IntEntry(vTakenOuts, i) )
continue;
Count = 0;
Vec_IntForEachEntry( vLevel, iObj, k )
Count += !Vec_IntEntry(vTakenIns, iObj);
if ( CountBest > Count )
{
CountBest = Count;
iObjBest = i;
}
}
return iObjBest;
}
void Gia_ManDupDemiterOrderXors( Gia_Man_t * p, Vec_Int_t * vXors )
{
extern Vec_Wec_t * Gia_ManCreateNodeSupps( Gia_Man_t * p, Vec_Int_t * vNodes, int fVerbose );
Vec_Wec_t * vSupps = Gia_ManCreateNodeSupps( p, vXors, 0 );
Vec_Int_t * vTakenIns = Vec_IntStart( Gia_ManCiNum(p) );
Vec_Int_t * vTakenOuts = Vec_IntStart( Vec_IntSize(vXors) );
Vec_Int_t * vOrder = Vec_IntAlloc( Vec_IntSize(vXors) );
int i, k, iObj;
// add outputs in the order of increasing supports
for ( i = 0; i < Vec_IntSize(vXors); i++ )
{
int Index = Gia_ManDupDemiterFindMin( vSupps, vTakenIns, vTakenOuts );
assert( Index >= 0 && Index < Vec_IntSize(vXors) );
Vec_IntPush( vOrder, Vec_IntEntry(vXors, Index) );
assert( !Vec_IntEntry( vTakenOuts, Index ) );
Vec_IntWriteEntry( vTakenOuts, Index, 1 );
Vec_IntForEachEntry( Vec_WecEntry(vSupps, Index), iObj, k )
Vec_IntWriteEntry( vTakenIns, iObj, 1 );
}
Vec_WecFree( vSupps );
Vec_IntFree( vTakenIns );
Vec_IntFree( vTakenOuts );
// reload
Vec_IntClear( vXors );
Vec_IntAppend( vXors, vOrder );
Vec_IntFree( vOrder );
}
/**Function*************************************************************
Synopsis []
@ -3781,8 +3876,8 @@ void Gia_ManCollectTopXors_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXo
}
Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p )
{
int i, iObj, iObj2, fFlip, * pPerm, Count1 = 0;
Vec_Int_t * vXors, * vSizes, * vPart[2], * vOrder;
int i, iObj, iObj2, fFlip, Count1 = 0;
Vec_Int_t * vXors, * vPart[2], * vOrder;
Gia_Obj_t * pFan[2], * pObj = Gia_ManCo(p, 0);
assert( Gia_ManCoNum(p) == 1 );
vXors = Vec_IntAlloc( 100 );
@ -3791,17 +3886,8 @@ Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p )
else
Vec_IntPush( vXors, Gia_ObjId(p, Gia_ObjFanin0(pObj)) );
// order by support size
vSizes = Vec_IntAlloc( 100 );
Vec_IntForEachEntry( vXors, iObj, i )
Vec_IntPush( vSizes, Gia_ManSuppSize(p, &iObj, 1) );
pPerm = Abc_MergeSortCost( Vec_IntArray(vSizes), Vec_IntSize(vSizes) );
Vec_IntClear( vSizes );
for ( i = 0; i < Vec_IntSize(vXors); i++ )
Vec_IntPush( vSizes, Vec_IntEntry(vXors, pPerm[i]) );
ABC_FREE( pPerm );
Vec_IntClear( vXors );
Vec_IntAppend( vXors, vSizes );
Vec_IntFree( vSizes );
Gia_ManDupDemiterOrderXors( p, vXors );
//Vec_IntPrint( vXors );
Vec_IntReverseOrder( vXors ); // from MSB to LSB
// divide into groups
Gia_ManCleanMark01(p);

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

@ -713,11 +713,13 @@ void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In
SeeAlso []
***********************************************************************/
Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds )
Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds, int fFadds )
{
Vec_Int_t * vMapAdds = Vec_IntStartFull( Gia_ManObjNum(p) ); int i;
for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ )
{
if ( fFadds && Vec_IntEntry(vAdds, 6*i+2) == 0 )
continue;
Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+3), i );
Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+4), i );
}
@ -800,9 +802,9 @@ Vec_Int_t * Gia_ShowCollectObjs( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * v
SeeAlso []
***********************************************************************/
void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_Int_t * vXors )
void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_Int_t * vXors, int fFadds )
{
Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds );
Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds );
Vec_Int_t * vMapXors = Gia_ShowMapXors( p, vXors );
Vec_Int_t * vOrder = Gia_ShowCollectObjs( p, vAdds, vXors, vMapAdds, vMapXors );
Gia_WriteDotAig( p, pFileName, vAdds, vXors, vMapAdds, vMapXors, vOrder );
@ -810,7 +812,7 @@ void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vAdds, Vec_In
Vec_IntFree( vMapXors );
Vec_IntFree( vOrder );
}
void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders )
void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds )
{
extern Vec_Int_t * Ree_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvXors, int fVerbose );
extern void Ree_ManRemoveTrivial( Gia_Man_t * p, Vec_Int_t * vAdds );
@ -837,7 +839,7 @@ void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders )
fclose( pFile );
// generate the file
if ( fAdders )
Gia_ShowProcess( pMan, FileNameDot, vAdds, vXors );
Gia_ShowProcess( pMan, FileNameDot, vAdds, vXors, fFadds );
else
Gia_WriteDotAigSimple( pMan, FileNameDot, vBold );
// visualize the file

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

@ -28592,15 +28592,18 @@ usage:
int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Vec_Int_t * vBold = NULL;
int c, fAdders = 0;
int c, fAdders = 0, fFadds = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "afh" ) ) != EOF )
{
switch ( c )
{
case 'a':
fAdders ^= 1;
break;
case 'f':
fFadds ^= 1;
break;
case 'h':
goto usage;
default:
@ -28623,14 +28626,15 @@ int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ManForEachLut( pAbc->pGia, c )
Vec_IntPush( vBold, c );
}
Gia_ManShow( pAbc->pGia, vBold, fAdders );
Gia_ManShow( pAbc->pGia, vBold, fAdders, fFadds );
Vec_IntFreeP( &vBold );
return 0;
usage:
Abc_Print( -2, "usage: &show [-ah]\n" );
Abc_Print( -2, "usage: &show [-afh]\n" );
Abc_Print( -2, "\t shows the current GIA using GSView\n" );
Abc_Print( -2, "\t-a : toggle visualazing adders [default = %s]\n", fAdders? "yes": "no" );
Abc_Print( -2, "\t-f : toggle only showing full-adders with \"-a\" [default = %s]\n", fFadds? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}

216
src/proof/acec/acecBo.c Normal file
View File

@ -0,0 +1,216 @@
/**CFile****************************************************************
FileName [acecBo.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [CEC for arithmetic circuits.]
Synopsis [Core procedures.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - June 20, 2005.]
Revision [$Id: acecBo.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#include "acecInt.h"
#include "misc/vec/vecWec.h"
#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Acec_DetectBoothXorMux( Gia_Man_t * p, Gia_Obj_t * pMux, Gia_Obj_t * pXor, int pIns[3] )
{
Gia_Obj_t * pFan0, * pFan1;
Gia_Obj_t * pDat0, * pDat1, * pCtrl;
if ( !Gia_ObjIsMuxType(pMux) || !Gia_ObjIsMuxType(pXor) )
return 0;
if ( !Gia_ObjRecognizeExor( pXor, &pFan0, &pFan1 ) )
return 0;
pFan0 = Gia_Regular(pFan0);
pFan1 = Gia_Regular(pFan1);
if ( Gia_ObjId(p, pFan0) > Gia_ObjId(p, pFan1) )
ABC_SWAP( Gia_Obj_t *, pFan0, pFan1 );
if ( !(pCtrl = Gia_ObjRecognizeMux( pMux, &pDat0, &pDat1 )) )
return 0;
pDat0 = Gia_Regular(pDat0);
pDat1 = Gia_Regular(pDat1);
pCtrl = Gia_Regular(pCtrl);
if ( !Gia_ObjIsAnd(pDat0) || !Gia_ObjIsAnd(pDat1) )
return 0;
if ( Gia_ObjFaninId0p(p, pDat0) != Gia_ObjFaninId0p(p, pDat1) ||
Gia_ObjFaninId1p(p, pDat0) != Gia_ObjFaninId1p(p, pDat1) )
return 0;
if ( Gia_ObjFaninId0p(p, pDat0) != Gia_ObjId(p, pFan0) ||
Gia_ObjFaninId1p(p, pDat0) != Gia_ObjId(p, pFan1) )
return 0;
pIns[0] = Gia_ObjId(p, pFan0);
pIns[1] = Gia_ObjId(p, pFan1);
pIns[2] = Gia_ObjId(p, pCtrl);
return 1;
}
int Acec_DetectBoothXorFanin( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] )
{
Gia_Obj_t * pFan0, * pFan1;
//int Id = Gia_ObjId(p, pObj);
if ( !Gia_ObjIsAnd(pObj) )
return 0;
if ( !Gia_ObjFaninC0(pObj) || !Gia_ObjFaninC1(pObj) )
return 0;
pFan0 = Gia_ObjFanin0(pObj);
pFan1 = Gia_ObjFanin1(pObj);
if ( !Gia_ObjIsAnd(pFan0) || !Gia_ObjIsAnd(pFan1) )
return 0;
if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin0(pFan0), Gia_ObjFanin0(pFan1), pIns) )
{
pIns[3] = Gia_ObjId(p, Gia_ObjFanin1(pFan0));
pIns[4] = Gia_ObjId(p, Gia_ObjFanin1(pFan1));
return 1;
}
if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin0(pFan0), Gia_ObjFanin1(pFan1), pIns) )
{
pIns[3] = Gia_ObjId(p, Gia_ObjFanin1(pFan0));
pIns[4] = Gia_ObjId(p, Gia_ObjFanin0(pFan1));
return 1;
}
if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin1(pFan0), Gia_ObjFanin0(pFan1), pIns) )
{
pIns[3] = Gia_ObjId(p, Gia_ObjFanin0(pFan0));
pIns[4] = Gia_ObjId(p, Gia_ObjFanin1(pFan1));
return 1;
}
if ( Acec_DetectBoothXorMux(p, Gia_ObjFanin1(pFan0), Gia_ObjFanin1(pFan1), pIns) )
{
pIns[3] = Gia_ObjId(p, Gia_ObjFanin0(pFan0));
pIns[4] = Gia_ObjId(p, Gia_ObjFanin0(pFan1));
return 1;
}
return 0;
}
int Acec_DetectBoothOne( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] )
{
Gia_Obj_t * pFan0, * pFan1;
if ( !Gia_ObjRecognizeExor( pObj, &pFan0, &pFan1 ) )
return 0;
pFan0 = Gia_Regular(pFan0);
pFan1 = Gia_Regular(pFan1);
if ( Acec_DetectBoothXorFanin( p, pFan0, pIns ) && pIns[2] == Gia_ObjId(p, pFan1) )
return 1;
if ( Acec_DetectBoothXorFanin( p, pFan1, pIns ) && pIns[2] == Gia_ObjId(p, pFan0) )
return 1;
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Acec_DetectBoothTwoXor( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] )
{
Gia_Obj_t * pFan0, * pFan1;
if ( !Gia_ObjIsAnd(pObj) )
return 0;
if ( Gia_ObjRecognizeExor( Gia_ObjFanin0(pObj), &pFan0, &pFan1 ) )
{
pIns[0] = Gia_ObjId(p, Gia_Regular(pFan0));
pIns[1] = Gia_ObjId(p, Gia_Regular(pFan1));
pIns[2] = -1;
pIns[3] = 0;
pIns[4] = Gia_ObjId(p, Gia_ObjFanin1(pObj));
return 1;
}
if ( Gia_ObjRecognizeExor( Gia_ObjFanin1(pObj), &pFan0, &pFan1 ) )
{
pIns[0] = Gia_ObjId(p, Gia_Regular(pFan0));
pIns[1] = Gia_ObjId(p, Gia_Regular(pFan1));
pIns[2] = -1;
pIns[3] = 0;
pIns[4] = Gia_ObjId(p, Gia_ObjFanin0(pObj));
return 1;
}
return 0;
}
int Acec_DetectBoothTwo( Gia_Man_t * p, Gia_Obj_t * pObj, int pIns[5] )
{
Gia_Obj_t * pFan0, * pFan1;
if ( !Gia_ObjRecognizeExor( pObj, &pFan0, &pFan1 ) )
return 0;
pFan0 = Gia_Regular(pFan0);
pFan1 = Gia_Regular(pFan1);
if ( Acec_DetectBoothTwoXor( p, pFan0, pIns ) )
{
pIns[2] = Gia_ObjId(p, pFan1);
return 1;
}
if ( Acec_DetectBoothTwoXor( p, pFan1, pIns ) )
{
pIns[2] = Gia_ObjId(p, pFan0);
return 1;
}
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acec_DetectBoothTest( Gia_Man_t * p )
{
Gia_Obj_t * pObj;
int i, pIns[5];
Gia_ManForEachAnd( p, pObj, i )
{
if ( !Acec_DetectBoothOne(p, pObj, pIns) && !Acec_DetectBoothTwo(p, pObj, pIns) )
continue;
printf( "obj = %4d : b0 = %4d b1 = %4d b2 = %4d a0 = %4d a1 = %4d\n",
i, pIns[0], pIns[1], pIns[2], pIns[3], pIns[4] );
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

95
src/proof/acec/acecCl.c
View File

@ -127,7 +127,7 @@ Vec_Int_t * Acec_CollectXorTops( Gia_Man_t * p )
break;
}
Vec_IntPush( vRootXorSet, Gia_ObjId(p, pObj) );
Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan1)) : Gia_ObjId(p, Gia_Regular(pFan0)) );
Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan0)) : Gia_ObjId(p, Gia_Regular(pFan1)) );
Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan10)) : Gia_ObjId(p, Gia_Regular(pFan00)) );
Vec_IntPush( vRootXorSet, fXor1 ? Gia_ObjId(p, Gia_Regular(pFan11)) : Gia_ObjId(p, Gia_Regular(pFan01)) );
}
@ -173,10 +173,101 @@ int Acec_DetectLitPolarity( Gia_Man_t * p, int Node, int Leaf )
if ( Lit0 != -1 && Lit1 != -1 )
{
assert( Lit0 == Lit1 );
printf( "Problem for leaf %d\n", Leaf );
return Lit0;
}
return Lit0 != -1 ? Lit0 : Lit1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Acec_DetectComputeSuppOne_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Int_t * vNods )
{
if ( Gia_ObjIsTravIdCurrent(p, pObj) )
return;
Gia_ObjSetTravIdCurrent(p, pObj);
if ( pObj->fMark0 )
{
Vec_IntPush( vSupp, Gia_ObjId(p, pObj) );
return;
}
assert( Gia_ObjIsAnd(pObj) );
Acec_DetectComputeSuppOne_rec( p, Gia_ObjFanin0(pObj), vSupp, vNods );
Acec_DetectComputeSuppOne_rec( p, Gia_ObjFanin1(pObj), vSupp, vNods );
Vec_IntPush( vNods, Gia_ObjId(p, pObj) );
}
void Acec_DetectComputeSupports( Gia_Man_t * p, Vec_Int_t * vRootXorSet )
{
Vec_Int_t * vNods = Vec_IntAlloc( 100 );
Vec_Int_t * vPols = Vec_IntAlloc( 100 );
Vec_Int_t * vSupp = Vec_IntAlloc( 100 ); int i, k, Node, Pol;
for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ )
{
Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 1;
Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+2) )->fMark0 = 1;
Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+3) )->fMark0 = 1;
}
for ( i = 1; 4*i < Vec_IntSize(vRootXorSet); i++ )
{
Vec_IntClear( vSupp );
Gia_ManIncrementTravId( p );
Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 0;
Acec_DetectComputeSuppOne_rec( p, Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) ), vSupp, vNods );
Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 1;
Vec_IntSort( vSupp, 0 );
printf( "Out %4d : %4d \n", i, Vec_IntEntry(vRootXorSet, 4*i+1) );
Vec_IntPrint( vSupp );
printf( "Cone:\n" );
Vec_IntForEachEntry( vNods, Node, k )
Gia_ObjPrint( p, Gia_ManObj(p, Node) );
Vec_IntClear( vPols );
Vec_IntForEachEntry( vSupp, Node, k )
Vec_IntPush( vPols, Acec_DetectLitPolarity(p, Vec_IntEntry(vRootXorSet, 4*i+1), Node) );
Vec_IntForEachEntryTwo( vSupp, vPols, Node, Pol, k )
printf( "%d(%d) ", Node, Abc_LitIsCompl(Pol) );
printf( "\n" );
Vec_IntPrint( vSupp );
}
for ( i = 0; 4*i < Vec_IntSize(vRootXorSet); i++ )
{
Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+1) )->fMark0 = 0;
Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+2) )->fMark0 = 0;
Gia_ManObj( p, Vec_IntEntry(vRootXorSet, 4*i+3) )->fMark0 = 0;
}
Vec_IntFree( vSupp );
Vec_IntFree( vPols );
Vec_IntFree( vNods );
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Acec_DetectXorBuildNew( Gia_Man_t * p, Vec_Int_t * vRootXorSet )
{
Gia_Man_t * pNew;
@ -236,6 +327,8 @@ Gia_Man_t * Acec_DetectAdditional( Gia_Man_t * p, int fVerbose )
vRootXorSet = Acec_CollectXorTops( p );
if ( vRootXorSet )
{
Acec_DetectComputeSupports( p, vRootXorSet );
pNew = Acec_DetectXorBuildNew( p, vRootXorSet );
Vec_IntFree( vRootXorSet );
}

1
src/proof/acec/module.make
View File

@ -1,6 +1,7 @@
SRC += src/proof/acec/acecCl.c \
src/proof/acec/acecCore.c \
src/proof/acec/acecCo.c \
src/proof/acec/acecBo.c \
src/proof/acec/acecRe.c \
src/proof/acec/acecPa.c \
src/proof/acec/acecPo.c \