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

Windowing for technology mapping.

This commit is contained in:
Alan Mishchenko 2016-03-30 21:51:50 -07:00
parent 31430043c2
commit 7724dfcca2
9 changed files with 460 additions and 190 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -32,6 +32,7 @@
#include <assert.h> #include <assert.h>
#include "misc/vec/vec.h" #include "misc/vec/vec.h"
#include "misc/vec/vecWec.h"
#include "misc/util/utilCex.h" #include "misc/util/utilCex.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
@ -130,7 +131,9 @@ struct Gia_Man_t_
Vec_Int_t * vFanoutNums; // static fanout Vec_Int_t * vFanoutNums; // static fanout
Vec_Int_t * vFanout; // static fanout Vec_Int_t * vFanout; // static fanout
Vec_Int_t * vMapping; // mapping for each node Vec_Int_t * vMapping; // mapping for each node
Vec_Wec_t * vMapping2; // mapping for each node
Vec_Int_t * vCellMapping; // mapping for each node Vec_Int_t * vCellMapping; // mapping for each node
void * pSatlutWinman; // windowing for SAT-based mapping
Vec_Int_t * vPacking; // packing information Vec_Int_t * vPacking; // packing information
Vec_Int_t * vConfigs; // cell configurations Vec_Int_t * vConfigs; // cell configurations
char * pCellStr; // cell description char * pCellStr; // cell description
@ -986,6 +989,12 @@ static inline int Gia_ObjLutFanin( Gia_Man_t * p, int Id, int i ) { re
static inline int Gia_ObjLutMuxId( Gia_Man_t * p, int Id ) { return Gia_ObjLutFanins(p, Id)[Gia_ObjLutSize(p, Id)]; } static inline int Gia_ObjLutMuxId( Gia_Man_t * p, int Id ) { return Gia_ObjLutFanins(p, Id)[Gia_ObjLutSize(p, Id)]; }
static inline int Gia_ObjLutIsMux( Gia_Man_t * p, int Id ) { return (int)(Gia_ObjLutMuxId(p, Id) < 0); } static inline int Gia_ObjLutIsMux( Gia_Man_t * p, int Id ) { return (int)(Gia_ObjLutMuxId(p, Id) < 0); }
static inline int Gia_ManHasMapping2( Gia_Man_t * p ) { return p->vMapping2 != NULL; }
static inline int Gia_ObjIsLut2( Gia_Man_t * p, int Id ) { return Vec_IntSize(Vec_WecEntry(p->vMapping2, Id)) != 0; }
static inline int Gia_ObjLutSize2( Gia_Man_t * p, int Id ) { return Vec_IntSize(Vec_WecEntry(p->vMapping2, Id)); }
static inline Vec_Int_t * Gia_ObjLutFanins2( Gia_Man_t * p, int Id ) { return Vec_WecEntry(p->vMapping2, Id); }
static inline int Gia_ObjLutFanin2( Gia_Man_t * p, int Id, int i ) { return Vec_IntEntry(Vec_WecEntry(p->vMapping2, Id), i); }
static inline int Gia_ManHasCellMapping( Gia_Man_t * p ) { return p->vCellMapping != NULL; } static inline int Gia_ManHasCellMapping( Gia_Man_t * p ) { return p->vCellMapping != NULL; }
static inline int Gia_ObjIsCell( Gia_Man_t * p, int iLit ) { return Vec_IntEntry(p->vCellMapping, iLit) != 0; } static inline int Gia_ObjIsCell( Gia_Man_t * p, int iLit ) { return Vec_IntEntry(p->vCellMapping, iLit) != 0; }
static inline int Gia_ObjIsCellInv( Gia_Man_t * p, int iLit ) { return Vec_IntEntry(p->vCellMapping, iLit) == -1; } static inline int Gia_ObjIsCellInv( Gia_Man_t * p, int iLit ) { return Vec_IntEntry(p->vCellMapping, iLit) == -1; }
@ -1002,6 +1011,15 @@ static inline int Gia_ObjCellId( Gia_Man_t * p, int iLit ) { re
#define Gia_LutForEachFaninObj( p, i, pFanin, k ) \ #define Gia_LutForEachFaninObj( p, i, pFanin, k ) \
for ( k = 0; k < Gia_ObjLutSize(p,i) && ((pFanin = Gia_ManObj(p, Gia_ObjLutFanins(p,i)[k])),1); k++ ) for ( k = 0; k < Gia_ObjLutSize(p,i) && ((pFanin = Gia_ManObj(p, Gia_ObjLutFanins(p,i)[k])),1); k++ )
#define Gia_ManForEachLut2( p, i ) \
for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsLut2(p, i) ) {} else
#define Gia_LutForEachFanin2( p, i, iFan, k ) \
for ( k = 0; k < Gia_ObjLutSize2(p,i) && ((iFan = Gia_ObjLutFanin2(p,i,k)),1); k++ )
#define Gia_ManForEachLut2Vec( vIds, p, vVec, iObj, i ) \
for ( i = 0; i < Vec_IntSize(vIds) && (vVec = Vec_WecEntry(p->vMapping2, (iObj = Vec_IntEntry(vIds, i)))); i++ )
#define Gia_ManForEachLut2VecReverse( vIds, p, vVec, iObj, i ) \
for ( i = Vec_IntSize(vIds)-1; i >= 0 && (vVec = Vec_WecEntry(p->vMapping2, (iObj = Vec_IntEntry(vIds, i)))); i-- )
#define Gia_ManForEachCell( p, i ) \ #define Gia_ManForEachCell( p, i ) \
for ( i = 2; i < 2*Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsCell(p, i) ) {} else for ( i = 2; i < 2*Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsCell(p, i) ) {} else
#define Gia_CellForEachFanin( p, i, iFanLit, k ) \ #define Gia_CellForEachFanin( p, i, iFanLit, k ) \
@ -1118,7 +1136,7 @@ extern Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs
extern Gia_Man_t * Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose ); extern Gia_Man_t * Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose );
/*=== giaDfs.c ============================================================*/ /*=== giaDfs.c ============================================================*/
extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp ); extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp );
extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes ); extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes, Vec_Int_t * vLeaves );
extern Vec_Int_t * Gia_ManCollectNodesCis( Gia_Man_t * p, int * pNodes, int nNodes ); extern Vec_Int_t * Gia_ManCollectNodesCis( Gia_Man_t * p, int * pNodes, int nNodes );
extern int Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes ); extern int Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes );
extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes ); extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
@ -1359,6 +1377,9 @@ extern void Gia_ManSimulateRound( Gia_ManSim_t * p );
extern float Gia_ManDelayTraceLut( Gia_Man_t * p ); extern float Gia_ManDelayTraceLut( Gia_Man_t * p );
extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose ); extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose );
extern Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int Degree, int fVerbose, int fVeryVerbose ); extern Gia_Man_t * Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int Degree, int fVerbose, int fVeryVerbose );
/*=== giaSplit.c ============================================================*/
extern void Gia_ManComputeOneWinStart( Gia_Man_t * p, int fReverse );
extern int Gia_ManComputeOneWin( Gia_Man_t * p, int iPivot, Vec_Int_t ** pvRoots, Vec_Int_t ** pvNodes, Vec_Int_t ** pvLeaves, Vec_Int_t ** pvAnds );
/*=== giaStg.c ============================================================*/ /*=== giaStg.c ============================================================*/
extern void Gia_ManStgPrint( FILE * pFile, Vec_Int_t * vLines, int nIns, int nOuts, int nStates ); extern void Gia_ManStgPrint( FILE * pFile, Vec_Int_t * vLines, int nIns, int nOuts, int nStates );
extern Gia_Man_t * Gia_ManStgRead( char * pFileName, int kHot, int fVerbose ); extern Gia_Man_t * Gia_ManStgRead( char * pFileName, int kHot, int fVerbose );

34
src/aig/gia/giaDfs.c
View File

@ -96,17 +96,19 @@ void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSu
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Gia_ManCollectAnds_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes ) void Gia_ManCollectAnds_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes )
{ {
if ( Gia_ObjIsTravIdCurrent(p, pObj) ) Gia_Obj_t * pObj;
if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
return; return;
Gia_ObjSetTravIdCurrent(p, pObj); Gia_ObjSetTravIdCurrentId(p, iObj);
pObj = Gia_ManObj( p, iObj );
if ( Gia_ObjIsCi(pObj) ) if ( Gia_ObjIsCi(pObj) )
return; return;
assert( Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsAnd(pObj) );
Gia_ManCollectAnds_rec( p, Gia_ObjFanin0(pObj), vNodes ); Gia_ManCollectAnds_rec( p, Gia_ObjFaninId0(pObj, iObj), vNodes );
Gia_ManCollectAnds_rec( p, Gia_ObjFanin1(pObj), vNodes ); Gia_ManCollectAnds_rec( p, Gia_ObjFaninId1(pObj, iObj), vNodes );
Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); Vec_IntPush( vNodes, iObj );
} }
/**Function************************************************************* /**Function*************************************************************
@ -120,20 +122,22 @@ void Gia_ManCollectAnds_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes ) void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes, Vec_Int_t * vLeaves )
{ {
Gia_Obj_t * pObj; int i, iLeaf;
int i;
Vec_IntClear( vNodes );
// Gia_ManIncrementTravId( p ); // Gia_ManIncrementTravId( p );
Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); Gia_ObjSetTravIdCurrentId( p, 0 );
if ( vLeaves )
Vec_IntForEachEntry( vLeaves, iLeaf, i )
Gia_ObjSetTravIdCurrentId( p, iLeaf );
Vec_IntClear( vNodes );
for ( i = 0; i < nNodes; i++ ) for ( i = 0; i < nNodes; i++ )
{ {
pObj = Gia_ManObj( p, pNodes[i] ); Gia_Obj_t * pObj = Gia_ManObj( p, pNodes[i] );
if ( Gia_ObjIsCo(pObj) ) if ( Gia_ObjIsCo(pObj) )
Gia_ManCollectAnds_rec( p, Gia_ObjFanin0(pObj), vNodes ); Gia_ManCollectAnds_rec( p, Gia_ObjFaninId0(pObj, pNodes[i]), vNodes );
else else
Gia_ManCollectAnds_rec( p, pObj, vNodes ); Gia_ManCollectAnds_rec( p, pNodes[i], vNodes );
} }
} }
@ -216,7 +220,7 @@ void Gia_ManCollectTest( Gia_Man_t * p )
Gia_ManForEachCo( p, pObj, i ) Gia_ManForEachCo( p, pObj, i )
{ {
iNode = Gia_ObjId(p, pObj); iNode = Gia_ObjId(p, pObj);
Gia_ManCollectAnds( p, &iNode, 1, vNodes ); Gia_ManCollectAnds( p, &iNode, 1, vNodes, NULL );
} }
Vec_IntFree( vNodes ); Vec_IntFree( vNodes );
ABC_PRT( "DFS from each output", Abc_Clock() - clk ); ABC_PRT( "DFS from each output", Abc_Clock() - clk );

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

@ -706,7 +706,7 @@ void Gia_ManFraSupports( Gia_ManFra_t * p )
vIns = Vec_IntAlloc( 100 ); vIns = Vec_IntAlloc( 100 );
Gia_ManCollectCis( p->pAig, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vIns ); Gia_ManCollectCis( p->pAig, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vIns );
vAnds = Vec_IntAlloc( 100 ); vAnds = Vec_IntAlloc( 100 );
Gia_ManCollectAnds( p->pAig, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vAnds ); Gia_ManCollectAnds( p->pAig, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vAnds, NULL );
Vec_PtrWriteEntry( p->vIns, f, vIns ); Vec_PtrWriteEntry( p->vIns, f, vIns );
Vec_PtrWriteEntry( p->vAnds, f, vAnds ); Vec_PtrWriteEntry( p->vAnds, f, vAnds );
Vec_PtrWriteEntry( p->vOuts, f, vOuts ); Vec_PtrWriteEntry( p->vOuts, f, vOuts );

10
src/aig/gia/giaIf.c
View File

@ -249,10 +249,10 @@ void Gia_ManSetRefsMapped( Gia_Man_t * p )
ABC_FREE( p->pRefs ); ABC_FREE( p->pRefs );
p->pRefs = ABC_CALLOC( int, Gia_ManObjNum(p) ); p->pRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
Gia_ManForEachCo( p, pObj, i ) Gia_ManForEachCo( p, pObj, i )
Gia_ObjRefInc( p, Gia_ObjFanin0(pObj) ); Gia_ObjRefIncId( p, Gia_ObjFaninId0p(p, pObj) );
Gia_ManForEachLut( p, i ) Gia_ManForEachLut( p, i )
Gia_LutForEachFanin( p, i, iFan, k ) Gia_LutForEachFanin( p, i, iFan, k )
Gia_ObjRefInc( p, Gia_ManObj(p, iFan) ); Gia_ObjRefIncId( p, iFan );
} }
/**Function************************************************************* /**Function*************************************************************
@ -273,10 +273,10 @@ void Gia_ManSetLutRefs( Gia_Man_t * p )
ABC_FREE( p->pLutRefs ); ABC_FREE( p->pLutRefs );
p->pLutRefs = ABC_CALLOC( int, Gia_ManObjNum(p) ); p->pLutRefs = ABC_CALLOC( int, Gia_ManObjNum(p) );
Gia_ManForEachCo( p, pObj, i ) Gia_ManForEachCo( p, pObj, i )
Gia_ObjLutRefInc( p, Gia_ObjFanin0(pObj) ); Gia_ObjLutRefIncId( p, Gia_ObjFaninId0p(p, pObj) );
Gia_ManForEachLut( p, i ) Gia_ManForEachLut( p, i )
Gia_LutForEachFanin( p, i, iFan, k ) Gia_LutForEachFanin( p, i, iFan, k )
Gia_ObjLutRefInc( p, Gia_ManObj(p, iFan) ); Gia_ObjLutRefIncId( p, iFan );
} }
/**Function************************************************************* /**Function*************************************************************
@ -1568,7 +1568,7 @@ int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t *
// collect nodes // collect nodes
Gia_ManIncrementTravId( pTemp ); Gia_ManIncrementTravId( pTemp );
Id = Abc_Lit2Var( iLit ); Id = Abc_Lit2Var( iLit );
Gia_ManCollectAnds( pTemp, &Id, 1, vCover ); Gia_ManCollectAnds( pTemp, &Id, 1, vCover, NULL );
Vec_IntPrint( vCover ); Vec_IntPrint( vCover );
Gia_ManForEachObjVec( vCover, pTemp, pObj, i ) Gia_ManForEachObjVec( vCover, pTemp, pObj, i )
Gia_ObjPrint( pTemp, pObj ); Gia_ObjPrint( pTemp, pObj );

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

@ -113,6 +113,7 @@ void Gia_ManStop( Gia_Man_t * p )
Vec_WrdFreeP( &p->vTtMemory ); Vec_WrdFreeP( &p->vTtMemory );
Vec_PtrFreeP( &p->vTtInputs ); Vec_PtrFreeP( &p->vTtInputs );
Vec_IntFreeP( &p->vMapping ); Vec_IntFreeP( &p->vMapping );
Vec_WecFreeP( &p->vMapping2 );
Vec_IntFreeP( &p->vCellMapping ); Vec_IntFreeP( &p->vCellMapping );
Vec_IntFreeP( &p->vPacking ); Vec_IntFreeP( &p->vPacking );
Vec_IntFreeP( &p->vConfigs ); Vec_IntFreeP( &p->vConfigs );

231
src/aig/gia/giaSatLut.c
View File

@ -20,7 +20,6 @@
#include "gia.h" #include "gia.h"
#include "sat/bsat/satStore.h" #include "sat/bsat/satStore.h"
#include "misc/vec/vecWec.h"
#include "misc/util/utilNam.h" #include "misc/util/utilNam.h"
#include "map/scl/sclCon.h" #include "map/scl/sclCon.h"
@ -40,13 +39,12 @@ struct Sbl_Man_t_
int FirstVar; // first variable to be used int FirstVar; // first variable to be used
int LitShift; // shift in terms of literals (2*Gia_ManCiNum(pGia)+2) int LitShift; // shift in terms of literals (2*Gia_ManCiNum(pGia)+2)
int nInputs; // the number of inputs int nInputs; // the number of inputs
// mapping
Vec_Wec_t * vMapping; // current mapping
// window // window
Gia_Man_t * pGia; Gia_Man_t * pGia;
Vec_Int_t * vLeaves; // leaf nodes Vec_Int_t * vLeaves; // leaf nodes
Vec_Int_t * vNodes; // internal nodes Vec_Int_t * vAnds; // AND-gates
Vec_Int_t * vRoots; // driver nodes (a subset of vNodes) Vec_Int_t * vNodes; // internal LUTs
Vec_Int_t * vRoots; // driver nodes (a subset of vAnds)
Vec_Int_t * vRootVars; // driver nodes (as SAT variables) Vec_Int_t * vRootVars; // driver nodes (as SAT variables)
// cuts // cuts
Vec_Wrd_t * vCutsI; // input bit patterns Vec_Wrd_t * vCutsI; // input bit patterns
@ -79,55 +77,55 @@ struct Sbl_Man_t_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Vec_Wec_t * Sbl_ManToMapping( Gia_Man_t * p )
{
Vec_Wec_t * vMapping = Vec_WecStart( Gia_ManObjNum(p) );
int Obj, Fanin, k;
Gia_ManForEachLut( p, Obj )
Gia_LutForEachFanin( p, Obj, Fanin, k )
Vec_WecPush( vMapping, Obj, Fanin );
return vMapping;
}
Vec_Int_t * Sbl_ManFromMapping( Gia_Man_t * p, Vec_Wec_t * vMap )
{
Vec_Int_t * vMapping, * vVec; int i, k, Obj;
vMapping = Vec_IntAlloc( Gia_ManObjNum(p) + Vec_WecSizeSize(vMap) + 2*Vec_WecSizeUsed(vMap) );
Vec_IntFill( vMapping, Gia_ManObjNum(p), 0 );
Vec_WecForEachLevel( vMap, vVec, i )
if ( Vec_IntSize(vVec) > 0 )
{
Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) );
Vec_IntPush( vMapping, Vec_IntSize(vVec) );
Vec_IntForEachEntry( vVec, Obj, k )
Vec_IntPush( vMapping, Obj );
Vec_IntPush( vMapping, i );
}
assert( Vec_IntSize(vMapping) < 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) );
return vMapping;
}
void Sbl_ManUpdateMapping( Sbl_Man_t * p ) void Sbl_ManUpdateMapping( Sbl_Man_t * p )
{ {
// Gia_Obj_t * pObj;
Vec_Int_t * vObj; Vec_Int_t * vObj;
int i, c, b, iObj;
word CutI, CutN; word CutI, CutN;
int i, c, b, iObj, iTemp;
assert( Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) ); assert( Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) );
Vec_IntForEachEntry( p->vNodes, iObj, i ) Vec_IntForEachEntry( p->vAnds, iObj, i )
Vec_IntClear( Vec_WecEntry(p->vMapping, iObj) ); {
vObj = Vec_WecEntry(p->pGia->vMapping2, iObj);
Vec_IntForEachEntry( vObj, iTemp, b )
Gia_ObjLutRefDecId( p->pGia, iTemp );
Vec_IntClear( vObj );
}
Vec_IntForEachEntry( p->vSolCuts2, c, i ) Vec_IntForEachEntry( p->vSolCuts2, c, i )
{ {
CutI = Vec_WrdEntry( p->vCutsI, c ); CutI = Vec_WrdEntry( p->vCutsI, c );
CutN = Vec_WrdEntry( p->vCutsN, c ); CutN = Vec_WrdEntry( p->vCutsN, c );
iObj = Vec_IntEntry( p->vCutsObj, c ); iObj = Vec_IntEntry( p->vCutsObj, c );
iObj = Vec_IntEntry( p->vNodes, iObj ); iObj = Vec_IntEntry( p->vAnds, iObj );
vObj = Vec_WecEntry( p->vMapping, iObj ); vObj = Vec_WecEntry( p->pGia->vMapping2, iObj );
assert( Vec_IntSize(vObj) == 0 ); assert( Vec_IntSize(vObj) == 0 );
for ( b = 0; b < 64; b++ ) for ( b = 0; b < 64; b++ )
if ( (CutI >> b) & 1 ) if ( (CutI >> b) & 1 )
Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, b) ); Vec_IntPush( vObj, Vec_IntEntry(p->vLeaves, b) );
for ( b = 0; b < 64; b++ ) for ( b = 0; b < 64; b++ )
if ( (CutN >> b) & 1 ) if ( (CutN >> b) & 1 )
Vec_IntPush( vObj, Vec_IntEntry(p->vNodes, b) ); Vec_IntPush( vObj, Vec_IntEntry(p->vAnds, b) );
Vec_IntForEachEntry( vObj, iTemp, b )
Gia_ObjLutRefIncId( p->pGia, iTemp );
} }
/*
// verify
Gia_ManForEachLut2Vec( p->pGia, vObj, i )
Vec_IntForEachEntry( vObj, iTemp, b )
Gia_ObjLutRefDecId( p->pGia, iTemp );
Gia_ManForEachCo( p->pGia, pObj, i )
Gia_ObjLutRefDecId( p->pGia, Gia_ObjFaninId0p(p->pGia, pObj) );
for ( i = 0; i < Gia_ManObjNum(p->pGia); i++ )
if ( p->pGia->pLutRefs[i] )
printf( "Object %d has %d refs\n", i, p->pGia->pLutRefs[i] );
Gia_ManForEachCo( p->pGia, pObj, i )
Gia_ObjLutRefIncId( p->pGia, Gia_ObjFaninId0p(p->pGia, pObj) );
Gia_ManForEachLut2Vec( p->pGia, vObj, i )
Vec_IntForEachEntry( vObj, iTemp, b )
Gia_ObjLutRefIncId( p->pGia, iTemp );
*/
} }
/**Function************************************************************* /**Function*************************************************************
@ -147,11 +145,11 @@ static int Sbl_ManPrintCut( word CutI, word CutN, int nInputs )
printf( "{ " ); printf( "{ " );
for ( b = 0; b < 64; b++ ) for ( b = 0; b < 64; b++ )
if ( (CutI >> b) & 1 ) if ( (CutI >> b) & 1 )
printf( "i%d ", b + 1 ), Count++; printf( "i%d ", b ), Count++;
printf( " " ); printf( " " );
for ( b = 0; b < 64; b++ ) for ( b = 0; b < 64; b++ )
if ( (CutN >> b) & 1 ) if ( (CutN >> b) & 1 )
printf( "n%d ", nInputs + b + 1 ), Count++; printf( "n%d ", b ), Count++;
printf( "};\n" ); printf( "};\n" );
return Count; return Count;
} }
@ -219,12 +217,12 @@ static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN )
int Start0 = Vec_IntEntry( p->vCutsStart, Obj ); int Start0 = Vec_IntEntry( p->vCutsStart, Obj );
int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Obj ); int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Obj );
int i; int i;
// printf( "Looking for:\n" ); //printf( "\nLooking for:\n" );
// Sbl_ManPrintCut( CutI, CutN, p->nInputs ); //Sbl_ManPrintCut( CutI, CutN, p->nInputs );
// printf( "\n" ); //printf( "\n" );
for ( i = Start0; i < Limit0; i++ ) for ( i = Start0; i < Limit0; i++ )
{ {
// Sbl_ManPrintCut( pCutsI[i], pCutsN[i], p->nInputs ); //Sbl_ManPrintCut( pCutsI[i], pCutsN[i], p->nInputs );
if ( pCutsI[i] == CutI && pCutsN[i] == CutN ) if ( pCutsI[i] == CutI && pCutsN[i] == CutN )
return i; return i;
} }
@ -232,9 +230,9 @@ static inline int Sbl_ManFindCut( Sbl_Man_t * p, int Obj, word CutI, word CutN )
} }
int Sbl_ManComputeCuts( Sbl_Man_t * p ) int Sbl_ManComputeCuts( Sbl_Man_t * p )
{ {
Gia_Obj_t * pObj, * pFanin; Gia_Obj_t * pObj; Vec_Int_t * vFanins;
int i, k, Index, nObjs = Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes); int i, k, Index, Fanin, nObjs = Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vAnds);
assert( Vec_IntSize(p->vLeaves) <= 64 && Vec_IntSize(p->vNodes) <= 64 ); assert( Vec_IntSize(p->vLeaves) <= 64 && Vec_IntSize(p->vAnds) <= 64 );
// assign leaf cuts // assign leaf cuts
Vec_IntClear( p->vCutsStart ); Vec_IntClear( p->vCutsStart );
Vec_IntClear( p->vCutsObj ); Vec_IntClear( p->vCutsObj );
@ -251,7 +249,7 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
pObj->Value = i; pObj->Value = i;
} }
// assign internal cuts // assign internal cuts
Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i ) Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
{ {
assert( Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsAnd(pObj) );
assert( ~Gia_ObjFanin0(pObj)->Value ); assert( ~Gia_ObjFanin0(pObj)->Value );
@ -270,27 +268,30 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
int Obj = Gia_ObjId(p->pGia, pObj); int Obj = Gia_ObjId(p->pGia, pObj);
if ( Gia_ObjIsCi(pObj) ) if ( Gia_ObjIsCi(pObj) )
continue; continue;
assert( Gia_ObjIsLut(p->pGia, Obj) ); assert( Gia_ObjIsLut2(p->pGia, Obj) );
assert( ~pObj->Value ); assert( ~pObj->Value );
Vec_IntPush( p->vRootVars, pObj->Value - Vec_IntSize(p->vLeaves) ); Vec_IntPush( p->vRootVars, pObj->Value - Vec_IntSize(p->vLeaves) );
} }
// create current solution // create current solution
Vec_IntClear( p->vPolar ); Vec_IntClear( p->vPolar );
Vec_IntClear( p->vSolCuts ); Vec_IntClear( p->vSolCuts );
Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i ) Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
{ {
word CutI = 0, CutN = 0; word CutI = 0, CutN = 0;
int Obj = Gia_ObjId(p->pGia, pObj); int Obj = Gia_ObjId(p->pGia, pObj);
if ( !Gia_ObjIsLut(p->pGia, Obj) ) if ( !Gia_ObjIsLut2(p->pGia, Obj) )
continue; continue;
assert( (int)pObj->Value == Vec_IntSize(p->vLeaves) + i ); assert( (int)pObj->Value == Vec_IntSize(p->vLeaves) + i );
// add node // add node
Vec_IntPush( p->vPolar, i ); Vec_IntPush( p->vPolar, i );
Vec_IntPush( p->vSolCuts, i ); Vec_IntPush( p->vSolCuts, i );
// add its cut // add its cut
Gia_LutForEachFaninObj( p->pGia, Obj, pFanin, k ) //Gia_LutForEachFaninObj( p->pGia, Obj, pFanin, k )
vFanins = Gia_ObjLutFanins2( p->pGia, Obj );
Vec_IntForEachEntry( vFanins, Fanin, k )
{ {
assert( (int)pFanin->Value < Vec_IntSize(p->vLeaves) || Gia_ObjIsLut(p->pGia, Gia_ObjId(p->pGia, pFanin)) ); Gia_Obj_t * pFanin = Gia_ManObj( p->pGia, Fanin );
assert( (int)pFanin->Value < Vec_IntSize(p->vLeaves) || Gia_ObjIsLut2(p->pGia, Fanin) );
assert( ~pFanin->Value ); assert( ~pFanin->Value );
if ( (int)pFanin->Value < Vec_IntSize(p->vLeaves) ) if ( (int)pFanin->Value < Vec_IntSize(p->vLeaves) )
CutI |= ((word)1 << pFanin->Value); CutI |= ((word)1 << pFanin->Value);
@ -299,13 +300,18 @@ int Sbl_ManComputeCuts( Sbl_Man_t * p )
} }
// find the new cut // find the new cut
Index = Sbl_ManFindCut( p, Vec_IntSize(p->vLeaves) + i, CutI, CutN ); Index = Sbl_ManFindCut( p, Vec_IntSize(p->vLeaves) + i, CutI, CutN );
if ( Index < 0 )
{
printf( "Cannot find the available cut.\n" );
continue;
}
assert( Index >= 0 ); assert( Index >= 0 );
Vec_IntPush( p->vPolar, p->FirstVar+Index ); Vec_IntPush( p->vPolar, p->FirstVar+Index );
} }
// clean value // clean value
Gia_ManForEachObjVec( p->vLeaves, p->pGia, pObj, i ) Gia_ManForEachObjVec( p->vLeaves, p->pGia, pObj, i )
pObj->Value = ~0; pObj->Value = ~0;
Gia_ManForEachObjVec( p->vNodes, p->pGia, pObj, i ) Gia_ManForEachObjVec( p->vAnds, p->pGia, pObj, i )
pObj->Value = ~0; pObj->Value = ~0;
return Vec_WrdSize(p->vCutsI); return Vec_WrdSize(p->vCutsI);
} }
@ -316,7 +322,7 @@ int Sbl_ManCreateCnf( Sbl_Man_t * p )
assert( p->FirstVar == sat_solver_nvars(p->pSat) ); assert( p->FirstVar == sat_solver_nvars(p->pSat) );
sat_solver_setnvars( p->pSat, sat_solver_nvars(p->pSat) + Vec_WrdSize(p->vCutsI) ); sat_solver_setnvars( p->pSat, sat_solver_nvars(p->pSat) + Vec_WrdSize(p->vCutsI) );
//printf( "\n" ); //printf( "\n" );
for ( i = 0; i < Vec_IntSize(p->vNodes); i++ ) for ( i = 0; i < Vec_IntSize(p->vAnds); i++ )
{ {
int Start0 = Vec_IntEntry( p->vCutsStart, Vec_IntSize(p->vLeaves) + i ); int Start0 = Vec_IntEntry( p->vCutsStart, Vec_IntSize(p->vLeaves) + i );
int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Vec_IntSize(p->vLeaves) + i ) - 1; int Limit0 = Start0 + Vec_IntEntry( p->vCutsNum, Vec_IntSize(p->vLeaves) + i ) - 1;
@ -380,6 +386,7 @@ Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN )
// window // window
p->pGia = pGia; p->pGia = pGia;
p->vLeaves = Vec_IntAlloc( 64 ); p->vLeaves = Vec_IntAlloc( 64 );
p->vAnds = Vec_IntAlloc( 64 );
p->vNodes = Vec_IntAlloc( 64 ); p->vNodes = Vec_IntAlloc( 64 );
p->vRoots = Vec_IntAlloc( 64 ); p->vRoots = Vec_IntAlloc( 64 );
p->vRootVars = Vec_IntAlloc( 64 ); p->vRootVars = Vec_IntAlloc( 64 );
@ -399,7 +406,6 @@ Sbl_Man_t * Sbl_ManAlloc( Gia_Man_t * pGia, int LogN )
p->vPolar = Vec_IntAlloc( 1000 ); p->vPolar = Vec_IntAlloc( 1000 );
// other // other
Gia_ManFillValue( pGia ); Gia_ManFillValue( pGia );
p->vMapping = Sbl_ManToMapping( pGia );
return p; return p;
} }
@ -407,9 +413,9 @@ void Sbl_ManStop( Sbl_Man_t * p )
{ {
sat_solver_delete( p->pSat ); sat_solver_delete( p->pSat );
Vec_IntFree( p->vCardVars ); Vec_IntFree( p->vCardVars );
Vec_WecFree( p->vMapping );
// internal // internal
Vec_IntFree( p->vLeaves ); Vec_IntFree( p->vLeaves );
Vec_IntFree( p->vAnds );
Vec_IntFree( p->vNodes ); Vec_IntFree( p->vNodes );
Vec_IntFree( p->vRoots ); Vec_IntFree( p->vRoots );
Vec_IntFree( p->vRootVars ); Vec_IntFree( p->vRootVars );
@ -439,25 +445,68 @@ void Sbl_ManWindow( Sbl_Man_t * p )
Gia_ManForEachCiId( p->pGia, ObjId, i ) Gia_ManForEachCiId( p->pGia, ObjId, i )
Vec_IntPush( p->vLeaves, ObjId ); Vec_IntPush( p->vLeaves, ObjId );
// collect internal // collect internal
Vec_IntClear( p->vNodes ); Vec_IntClear( p->vAnds );
Gia_ManForEachAndId( p->pGia, ObjId ) Gia_ManForEachAndId( p->pGia, ObjId )
Vec_IntPush( p->vNodes, ObjId ); Vec_IntPush( p->vAnds, ObjId );
// collect roots // collect roots
Vec_IntClear( p->vRoots ); Vec_IntClear( p->vRoots );
Gia_ManForEachCoDriverId( p->pGia, ObjId, i ) Gia_ManForEachCoDriverId( p->pGia, ObjId, i )
Vec_IntPush( p->vRoots, ObjId ); Vec_IntPush( p->vRoots, ObjId );
} }
int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose ) int Sbl_ManWindow2( Sbl_Man_t * p, int iPivot )
{ {
Vec_Int_t * vRoots, * vNodes, * vLeaves, * vAnds;
int Count = Gia_ManComputeOneWin( p->pGia, iPivot, &vRoots, &vNodes, &vLeaves, &vAnds );
if ( Count == 0 )
return 0;
Vec_IntClear( p->vRoots ); Vec_IntAppend( p->vRoots, vRoots );
Vec_IntClear( p->vNodes ); Vec_IntAppend( p->vNodes, vNodes );
Vec_IntClear( p->vLeaves ); Vec_IntAppend( p->vLeaves, vLeaves );
Vec_IntClear( p->vAnds ); Vec_IntAppend( p->vAnds, vAnds );
//Vec_IntPrint( vRoots );
//Vec_IntPrint( vAnds );
//Vec_IntPrint( vLeaves );
// recompute internal nodes
// Gia_ManIncrementTravId( p->pGia );
// Gia_ManCollectAnds( p->pGia, Vec_IntArray(p->vRoots), Vec_IntSize(p->vRoots), p->vAnds, p->vLeaves );
return Count;
}
int Sbl_ManTestSat( Gia_Man_t * pGia, int nBTLimit, int iPivot, int fVerbose )
{
int fKeepTrying = 1;
abctime clk = Abc_Clock(), clk2; abctime clk = Abc_Clock(), clk2;
int i, LogN = 6, nVars = 1 << LogN, status, Root; int i, LogN = 6, nVars = 1 << LogN, status, Root;
Sbl_Man_t * p = Sbl_ManAlloc( pGia, LogN ); Sbl_Man_t * p = Sbl_ManAlloc( pGia, LogN );
int fKeepTrying = 1; int StartSol, Count, nConfTotal = 0;
int StartSol;
// compute one window
Count = Sbl_ManWindow2( p, iPivot );
if ( Count == 0 )
{
printf( "Obj %d: Window with less than %d inputs does not exist.\n", iPivot, 64 );
Sbl_ManStop( p );
return 0;
}
if ( fVerbose )
printf( "\nObj = %6d : Leaf = %2d. LUT = %2d. AND = %2d. Root = %2d.\n",
iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vAnds), Vec_IntSize(p->vRoots) );
if ( Vec_IntSize(p->vLeaves) > 64 || Vec_IntSize(p->vAnds) > 64 )
{
printf( "Obj %d: Encountered window with %d inputs and %d internal nodes.\n", iPivot, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds) );
Sbl_ManStop( p );
return 0;
}
if ( Vec_IntSize(p->vAnds) < 20 )
{
if ( fVerbose )
printf( "Skipping.\n" );
Sbl_ManStop( p );
return 0;
}
// derive window
Sbl_ManWindow( p );
// derive cuts // derive cuts
Sbl_ManComputeCuts( p ); Sbl_ManComputeCuts( p );
// derive SAT instance // derive SAT instance
@ -468,7 +517,7 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose )
if ( fVerbose ) if ( fVerbose )
printf( "All clauses = %d. Multi clauses = %d. Binary clauses = %d. Other clauses = %d.\n\n", printf( "All clauses = %d. Multi clauses = %d. Binary clauses = %d. Other clauses = %d.\n\n",
sat_solver_nclauses(p->pSat), Vec_IntSize(p->vNodes), Vec_WrdSize(p->vCutsI) - Vec_IntSize(p->vNodes), sat_solver_nclauses(p->pSat), Vec_IntSize(p->vAnds), Vec_WrdSize(p->vCutsI) - Vec_IntSize(p->vAnds),
sat_solver_nclauses(p->pSat) - Vec_WrdSize(p->vCutsI) ); sat_solver_nclauses(p->pSat) - Vec_WrdSize(p->vCutsI) );
// create assumptions // create assumptions
@ -476,17 +525,19 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose )
Vec_IntClear( p->vAssump ); Vec_IntClear( p->vAssump );
Vec_IntPush( p->vAssump, -1 ); Vec_IntPush( p->vAssump, -1 );
// unused variables // unused variables
for ( i = Vec_IntSize(p->vNodes); i < nVars; i++ ) for ( i = Vec_IntSize(p->vAnds); i < nVars; i++ )
Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) ); Vec_IntPush( p->vAssump, Abc_Var2Lit(i, 1) );
// root variables // root variables
Vec_IntForEachEntry( p->vRootVars, Root, i ) Vec_IntForEachEntry( p->vRootVars, Root, i )
Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) ); Vec_IntPush( p->vAssump, Abc_Var2Lit(Root, 0) );
// Vec_IntPrint( p->vAssump ); // Vec_IntPrint( p->vAssump );
Vec_IntClear( p->vSolCuts2 );
StartSol = Vec_IntSize(p->vSolCuts) + 1; StartSol = Vec_IntSize(p->vSolCuts) + 1;
// StartSol = 30; // StartSol = 30;
while ( fKeepTrying && StartSol-fKeepTrying > 0 ) while ( fKeepTrying && StartSol-fKeepTrying > 0 )
{ {
int nConfBef, nConfAft;
if ( fVerbose ) if ( fVerbose )
printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying ); printf( "Trying to find mapping with %d gates.\n", StartSol-fKeepTrying );
// for ( i = Vec_IntSize(p->vSolCuts)-5; i < nVars; i++ ) // for ( i = Vec_IntSize(p->vSolCuts)-5; i < nVars; i++ )
@ -494,19 +545,24 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose )
Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1) ); Vec_IntWriteEntry( p->vAssump, 0, Abc_Var2Lit(Vec_IntEntry(p->vCardVars, StartSol-fKeepTrying), 1) );
// solve the problem // solve the problem
clk2 = Abc_Clock(); clk2 = Abc_Clock();
status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), 0, 0, 0, 0 ); nConfBef = (int)p->pSat->stats.conflicts;
status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssump), Vec_IntLimit(p->vAssump), nBTLimit, 0, 0, 0 );
nConfAft = (int)p->pSat->stats.conflicts;
nConfTotal += nConfAft - nConfBef;
if ( status == l_Undef )
break;
if ( status == l_True ) if ( status == l_True )
{ {
int Count = 0, LitCount = 0; int Count = 0, LitCount = 0;
if ( fVerbose ) if ( fVerbose )
{ {
printf( "Inputs = %d. ANDs = %d. Total = %d. All vars = %d.\n", printf( "Inputs = %d. ANDs = %d. Total = %d. All vars = %d.\n",
Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vLeaves), Vec_IntSize(p->vAnds),
Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vNodes), nVars ); Vec_IntSize(p->vLeaves)+Vec_IntSize(p->vAnds), nVars );
for ( i = 0; i < Vec_IntSize(p->vNodes); i++ ) for ( i = 0; i < Vec_IntSize(p->vAnds); i++ )
printf( "%d", sat_solver_var_value(p->pSat, i) ); printf( "%d", sat_solver_var_value(p->pSat, i) );
printf( "\n" ); printf( "\n" );
for ( i = 0; i < Vec_IntSize(p->vNodes); i++ ) for ( i = 0; i < Vec_IntSize(p->vAnds); i++ )
if ( sat_solver_var_value(p->pSat, i) ) if ( sat_solver_var_value(p->pSat, i) )
{ {
printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) ); printf( "%d=%d ", i, sat_solver_var_value(p->pSat, i) );
@ -523,13 +579,18 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose )
if ( sat_solver_var_value(p->pSat, i) ) if ( sat_solver_var_value(p->pSat, i) )
{ {
if ( fVerbose ) if ( fVerbose )
printf( "Cut %3d : ", Count++ ); printf( "Cut %3d : Node = %3d Node = %6d ", Count++, Vec_IntEntry(p->vCutsObj, i-p->FirstVar), Vec_IntEntry(p->vAnds, Vec_IntEntry(p->vCutsObj, i-p->FirstVar)) );
if ( fVerbose ) if ( fVerbose )
LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar ); LitCount += Sbl_ManFindAndPrintCut( p, i-p->FirstVar );
Vec_IntPush( p->vSolCuts2, i-p->FirstVar ); Vec_IntPush( p->vSolCuts2, i-p->FirstVar );
} }
if ( fVerbose ) if ( fVerbose )
printf( "LitCount = %d.\n", LitCount ); printf( "LitCount = %d.\n", LitCount );
if ( fVerbose )
Vec_IntPrint( p->vRootVars );
//Vec_IntPrint( p->vRoots );
//Vec_IntPrint( p->vAnds );
//Vec_IntPrint( p->vLeaves );
} }
fKeepTrying = status == l_True ? fKeepTrying + 1 : 0; fKeepTrying = status == l_True ? fKeepTrying + 1 : 0;
if ( fVerbose ) if ( fVerbose )
@ -547,18 +608,30 @@ int Sbl_ManTestSat( Gia_Man_t * pGia, int fVerbose )
} }
// update solution // update solution
Sbl_ManUpdateMapping( p ); if ( Vec_IntSize(p->vSolCuts2) > 0 && Vec_IntSize(p->vSolCuts2) < Vec_IntSize(p->vSolCuts) )
{
Vec_IntFreeP( &pGia->vMapping ); Sbl_ManUpdateMapping( p );
pGia->vMapping = Sbl_ManFromMapping( pGia, p->vMapping ); printf( "Object %d : Saved %d nodes. (Conf = %d.)\n", iPivot, Vec_IntSize(p->vSolCuts)-Vec_IntSize(p->vSolCuts2), nConfTotal );
Sbl_ManStop( p );
return 2;
}
Sbl_ManStop( p ); Sbl_ManStop( p );
return 1; return 1;
} }
void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nConfl, int fVerbose ) void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nConfl, int fReverse, int fVerbose )
{ {
Sbl_ManTestSat( p, fVerbose ); int iLut;
Gia_ManComputeOneWinStart( pGia, fReverse );
Gia_ManForEachLut2( pGia, iLut )
{
// if ( iLut > 259 )
// break;
if ( Sbl_ManTestSat( pGia, nConfl, iLut, fVerbose ) != 2 )
continue;
// break;
}
Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL );
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

332
src/aig/gia/giaSplit.c
View File

@ -35,14 +35,16 @@ struct Spl_Man_t_
Gia_Man_t * pGia; // user AIG with nodes marked Gia_Man_t * pGia; // user AIG with nodes marked
int iObj; // object ID int iObj; // object ID
int Limit; // limit on AIG nodes int Limit; // limit on AIG nodes
int Count; // count of AIG nodes int fReverse; // enable reverse search
// intermediate // intermediate
Vec_Bit_t * vMarksCIO; // CI/CO marks Vec_Bit_t * vMarksCIO; // CI/CO marks
Vec_Bit_t * vMarksIn; // input marks Vec_Bit_t * vMarksIn; // input marks
Vec_Bit_t * vMarksNo; // node marks Vec_Bit_t * vMarksNo; // node marks
Vec_Int_t * vNodes; // nodes used in the window Vec_Bit_t * vMarksAnd; // AND node marks
Vec_Int_t * vRoots; // nodes pointing to Nodes Vec_Int_t * vRoots; // nodes pointing to Nodes
Vec_Int_t * vNodes; // nodes used in the window
Vec_Int_t * vLeaves; // nodes pointed by Nodes Vec_Int_t * vLeaves; // nodes pointed by Nodes
Vec_Int_t * vAnds; // AND nodes used in the window
// temporary // temporary
Vec_Int_t * vFanouts; // fanouts of the node Vec_Int_t * vFanouts; // fanouts of the node
Vec_Int_t * vCands; // candidate nodes Vec_Int_t * vCands; // candidate nodes
@ -55,7 +57,7 @@ struct Spl_Man_t_
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Transforming to the internal LUT representation.]
Description [] Description []
@ -64,45 +66,103 @@ struct Spl_Man_t_
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Spl_Man_t * Spl_ManAlloc( Gia_Man_t * pGia, int Limit ) Vec_Wec_t * Spl_ManToWecMapping( Gia_Man_t * p )
{
Vec_Wec_t * vMapping = Vec_WecStart( Gia_ManObjNum(p) );
int Obj, Fanin, k;
assert( Gia_ManHasMapping(p) );
Gia_ManForEachLut( p, Obj )
Gia_LutForEachFanin( p, Obj, Fanin, k )
Vec_WecPush( vMapping, Obj, Fanin );
return vMapping;
}
Vec_Int_t * Spl_ManFromWecMapping( Gia_Man_t * p, Vec_Wec_t * vMap )
{
Vec_Int_t * vMapping, * vVec; int i, k, Obj;
assert( Gia_ManHasMapping2(p) );
vMapping = Vec_IntAlloc( Gia_ManObjNum(p) + Vec_WecSizeSize(vMap) + 2*Vec_WecSizeUsed(vMap) );
Vec_IntFill( vMapping, Gia_ManObjNum(p), 0 );
Vec_WecForEachLevel( vMap, vVec, i )
if ( Vec_IntSize(vVec) > 0 )
{
Vec_IntWriteEntry( vMapping, i, Vec_IntSize(vMapping) );
Vec_IntPush( vMapping, Vec_IntSize(vVec) );
Vec_IntForEachEntry( vVec, Obj, k )
Vec_IntPush( vMapping, Obj );
Vec_IntPush( vMapping, i );
}
assert( Vec_IntSize(vMapping) < 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) );
return vMapping;
}
/**Function*************************************************************
Synopsis [Creating manager.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Spl_Man_t * Spl_ManAlloc( Gia_Man_t * pGia, int Limit, int fReverse )
{ {
int i, iObj; int i, iObj;
Spl_Man_t * p = ABC_CALLOC( Spl_Man_t, 1 ); Spl_Man_t * p = ABC_CALLOC( Spl_Man_t, 1 );
assert( Gia_ManHasMapping(pGia) );
p->pGia = pGia; p->pGia = pGia;
p->Limit = Limit; p->Limit = Limit;
p->fReverse = fReverse;
// intermediate // intermediate
p->vMarksCIO = Vec_BitStart( Gia_ManObjNum(pGia) ); p->vMarksCIO = Vec_BitStart( Gia_ManObjNum(pGia) );
p->vMarksIn = Vec_BitStart( Gia_ManObjNum(pGia) ); p->vMarksIn = Vec_BitStart( Gia_ManObjNum(pGia) );
p->vMarksNo = Vec_BitStart( Gia_ManObjNum(pGia) ); p->vMarksNo = Vec_BitStart( Gia_ManObjNum(pGia) );
p->vMarksAnd = Vec_BitStart( Gia_ManObjNum(pGia) );
p->vRoots = Vec_IntAlloc( 100 ); p->vRoots = Vec_IntAlloc( 100 );
p->vNodes = Vec_IntAlloc( 100 ); p->vNodes = Vec_IntAlloc( 100 );
p->vLeaves = Vec_IntAlloc( 100 ); p->vLeaves = Vec_IntAlloc( 100 );
p->vAnds = Vec_IntAlloc( 100 );
// temporary // temporary
p->vFanouts = Vec_IntAlloc( 100 ); p->vFanouts = Vec_IntAlloc( 100 );
p->vCands = Vec_IntAlloc( 100 ); p->vCands = Vec_IntAlloc( 100 );
p->vInputs = Vec_IntAlloc( 100 ); p->vInputs = Vec_IntAlloc( 100 );
// mark CIs/COs // mark CIs/COs
Vec_BitWriteEntry( p->vMarksCIO, 0, 1 );
Gia_ManForEachCiId( pGia, iObj, i ) Gia_ManForEachCiId( pGia, iObj, i )
Vec_BitWriteEntry( p->vMarksCIO, iObj, 1 ); Vec_BitWriteEntry( p->vMarksCIO, iObj, 1 );
Gia_ManForEachCoId( pGia, iObj, i ) Gia_ManForEachCoId( pGia, iObj, i )
Vec_BitWriteEntry( p->vMarksCIO, iObj, 1 ); Vec_BitWriteEntry( p->vMarksCIO, iObj, 1 );
// prepare AIG // mapping
Gia_ManStaticFanoutStart( pGia ); ABC_FREE( pGia->pRefs );
Gia_ManSetLutRefs( pGia );
Gia_ManCreateRefs( pGia ); Gia_ManCreateRefs( pGia );
Gia_ManSetLutRefs( pGia );
assert( Gia_ManHasMapping(pGia) );
assert( !Gia_ManHasMapping2(pGia) );
pGia->vMapping2 = Spl_ManToWecMapping( pGia );
Vec_IntFreeP( &pGia->vMapping );
// fanout
Gia_ManStaticFanoutStart( pGia );
return p; return p;
} }
void Spl_ManStop( Spl_Man_t * p ) void Spl_ManStop( Spl_Man_t * p )
{ {
// fanout
Gia_ManStaticFanoutStop( p->pGia ); Gia_ManStaticFanoutStop( p->pGia );
// mapping
assert( !Gia_ManHasMapping(p->pGia) );
assert( Gia_ManHasMapping2(p->pGia) );
p->pGia->vMapping = Spl_ManFromWecMapping( p->pGia, p->pGia->vMapping2 );
Vec_WecFreeP( &p->pGia->vMapping2 );
// intermediate // intermediate
Vec_BitFree( p->vMarksCIO ); Vec_BitFree( p->vMarksCIO );
Vec_BitFree( p->vMarksIn ); Vec_BitFree( p->vMarksIn );
Vec_BitFree( p->vMarksNo ); Vec_BitFree( p->vMarksNo );
Vec_BitFree( p->vMarksAnd );
Vec_IntFree( p->vRoots ); Vec_IntFree( p->vRoots );
Vec_IntFree( p->vNodes ); Vec_IntFree( p->vNodes );
Vec_IntFree( p->vLeaves ); Vec_IntFree( p->vLeaves );
Vec_IntFree( p->vAnds );
// temporary // temporary
Vec_IntFree( p->vFanouts ); Vec_IntFree( p->vFanouts );
Vec_IntFree( p->vCands ); Vec_IntFree( p->vCands );
@ -123,31 +183,55 @@ void Spl_ManStop( Spl_Man_t * p )
***********************************************************************/ ***********************************************************************/
void Spl_ManWinFindLeavesRoots( Spl_Man_t * p ) void Spl_ManWinFindLeavesRoots( Spl_Man_t * p )
{ {
Vec_Int_t * vVec;
int iObj, iFan, i, k; int iObj, iFan, i, k;
// collect leaves // collect leaves
/*
Vec_IntClear( p->vLeaves ); Vec_IntClear( p->vLeaves );
Vec_IntForEachEntry( p->vNodes, iObj, i ) Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
{ {
assert( Vec_BitEntry(p->vMarksNo, iObj) ); assert( Vec_BitEntry(p->vMarksNo, iObj) );
Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) Vec_IntForEachEntry( vVec, iFan, k )
if ( !Vec_BitEntry(p->vMarksNo, iFan) ) if ( !Vec_BitEntry(p->vMarksNo, iFan) )
{ {
Vec_BitWriteEntry(p->vMarksNo, iFan, 1); Vec_BitWriteEntry(p->vMarksNo, iFan, 1);
Vec_IntPush( p->vLeaves, iFan ); Vec_IntPush( p->vLeaves, iFan );
} }
} }
Vec_IntForEachEntry( p->vLeaves, iObj, i ) Vec_IntForEachEntry( p->vLeaves, iFan, i )
Vec_BitWriteEntry(p->vMarksNo, iObj, 0); Vec_BitWriteEntry(p->vMarksNo, iFan, 0);
*/
Vec_IntClear( p->vLeaves );
Vec_IntForEachEntry( p->vAnds, iObj, i )
{
Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj );
assert( Vec_BitEntry(p->vMarksAnd, iObj) );
iFan = Gia_ObjFaninId0( pObj, iObj );
if ( !Vec_BitEntry(p->vMarksAnd, iFan) )
{
Vec_BitWriteEntry(p->vMarksAnd, iFan, 1);
Vec_IntPush( p->vLeaves, iFan );
}
iFan = Gia_ObjFaninId1( pObj, iObj );
if ( !Vec_BitEntry(p->vMarksAnd, iFan) )
{
Vec_BitWriteEntry(p->vMarksAnd, iFan, 1);
Vec_IntPush( p->vLeaves, iFan );
}
}
Vec_IntForEachEntry( p->vLeaves, iFan, i )
Vec_BitWriteEntry(p->vMarksAnd, iFan, 0);
// collect roots // collect roots
Vec_IntClear( p->vRoots ); Vec_IntClear( p->vRoots );
Vec_IntForEachEntry( p->vNodes, iObj, i ) Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) Vec_IntForEachEntry( vVec, iFan, k )
Gia_ObjLutRefDecId( p->pGia, iFan ); Gia_ObjLutRefDecId( p->pGia, iFan );
Vec_IntForEachEntry( p->vNodes, iObj, i ) Vec_IntForEachEntry( p->vAnds, iObj, i )
if ( Gia_ObjLutRefNumId(p->pGia, iObj) ) if ( Gia_ObjLutRefNumId(p->pGia, iObj) )
Vec_IntPush( p->vRoots, iObj ); Vec_IntPush( p->vRoots, iObj );
Vec_IntForEachEntry( p->vNodes, iObj, i ) Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) Vec_IntForEachEntry( vVec, iFan, k )
Gia_ObjLutRefIncId( p->pGia, iFan ); Gia_ObjLutRefIncId( p->pGia, iFan );
} }
@ -170,7 +254,7 @@ void Spl_ManLutFanouts_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_B
int iFanout, i; int iFanout, i;
if ( Vec_BitEntry(vMarksNo, iObj) || Vec_BitEntry(vMarksCIO, iObj) ) if ( Vec_BitEntry(vMarksNo, iObj) || Vec_BitEntry(vMarksCIO, iObj) )
return; return;
if ( Gia_ObjIsLut(p, iObj) ) if ( Gia_ObjIsLut2(p, iObj) )
{ {
Vec_BitWriteEntry( vMarksCIO, iObj, 1 ); Vec_BitWriteEntry( vMarksCIO, iObj, 1 );
Vec_IntPush( vFanouts, iObj ); Vec_IntPush( vFanouts, iObj );
@ -182,7 +266,7 @@ void Spl_ManLutFanouts_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_B
int Spl_ManLutFanouts( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_Bit_t * vMarksNo, Vec_Bit_t * vMarksCIO ) int Spl_ManLutFanouts( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_Bit_t * vMarksNo, Vec_Bit_t * vMarksCIO )
{ {
int i, iFanout; int i, iFanout;
assert( Gia_ObjIsLut(p, iObj) ); assert( Gia_ObjIsLut2(p, iObj) );
Vec_IntClear( vFanouts ); Vec_IntClear( vFanouts );
Gia_ObjForEachFanoutStaticId( p, iObj, iFanout, i ) Gia_ObjForEachFanoutStaticId( p, iObj, iFanout, i )
Spl_ManLutFanouts_rec( p, iFanout, vFanouts, vMarksNo, vMarksCIO ); Spl_ManLutFanouts_rec( p, iFanout, vFanouts, vMarksNo, vMarksCIO );
@ -195,30 +279,7 @@ int Spl_ManLutFanouts( Gia_Man_t * p, int iObj, Vec_Int_t * vFanouts, Vec_Bit_t
/**Function************************************************************* /**Function*************************************************************
Synopsis [Compute MFFC size of one node.] Synopsis [Returns the number of fanins beloning to the set.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Spl_ManLutMffcSize( Gia_Man_t * p, int iObj )
{
int Res, iFan, i;
assert( Gia_ObjIsLut(p, iObj) );
Gia_LutForEachFanin( p, iObj, iFan, i )
Gia_ObjRefIncId( p, iFan );
Res = Gia_NodeMffcSize( p, Gia_ManObj(p, iObj) );
Gia_LutForEachFanin( p, iObj, iFan, i )
Gia_ObjRefDecId( p, iFan );
return Res;
}
/**Function*************************************************************
Synopsis [Returns the number of fanins not beloning to the set.]
Description [] Description []
@ -229,8 +290,9 @@ int Spl_ManLutMffcSize( Gia_Man_t * p, int iObj )
***********************************************************************/ ***********************************************************************/
int Spl_ManCountMarkedFanins( Gia_Man_t * p, int iObj, Vec_Bit_t * vMarks ) int Spl_ManCountMarkedFanins( Gia_Man_t * p, int iObj, Vec_Bit_t * vMarks )
{ {
int k, iFan, Count = 0; int i, iFan, Count = 0;
Gia_LutForEachFanin( p, iObj, iFan, k ) Vec_Int_t * vFanins = Gia_ObjLutFanins2(p, iObj);
Vec_IntForEachEntry( vFanins, iFan, i )
if ( Vec_BitEntry(vMarks, iFan) ) if ( Vec_BitEntry(vMarks, iFan) )
Count++; Count++;
return Count; return Count;
@ -249,27 +311,46 @@ int Spl_ManCountMarkedFanins( Gia_Man_t * p, int iObj, Vec_Bit_t * vMarks )
***********************************************************************/ ***********************************************************************/
int Spl_ManFindOne( Spl_Man_t * p ) int Spl_ManFindOne( Spl_Man_t * p )
{ {
Vec_Int_t * vVec;
int nFanouts, iObj, iFan, i, k; int nFanouts, iObj, iFan, i, k;
int Res = 0, InCount, InCountMax = -1; int Res = 0, InCount, InCountMax = -1;
Vec_IntClear( p->vCands ); Vec_IntClear( p->vCands );
Vec_IntClear( p->vInputs ); Vec_IntClear( p->vInputs );
// deref // deref
Vec_IntForEachEntry( p->vNodes, iObj, i ) Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) Vec_IntForEachEntry( vVec, iFan, k )
Gia_ObjLutRefDecId( p->pGia, iFan ); Gia_ObjLutRefDecId( p->pGia, iFan );
// consider LUT inputs - get one that has no refs // consider LUT inputs - get one that has no refs
Vec_IntForEachEntry( p->vNodes, iObj, i ) if ( p->fReverse )
Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) {
if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) ) Gia_ManForEachLut2VecReverse( p->vNodes, p->pGia, vVec, iObj, i )
{ Vec_IntForEachEntry( vVec, iFan, k )
if ( !Gia_ObjLutRefNumId(p->pGia, iFan) ) if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) )
{ {
Res = iFan; if ( !Gia_ObjLutRefNumId(p->pGia, iFan) )
goto finish; {
Res = iFan;
goto finish;
}
Vec_IntPush( p->vCands, iFan );
Vec_IntPush( p->vInputs, iFan );
} }
Vec_IntPush( p->vCands, iFan ); }
Vec_IntPush( p->vInputs, iFan ); else
} {
Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
Vec_IntForEachEntry( vVec, iFan, k )
if ( !Vec_BitEntry(p->vMarksNo, iFan) && !Vec_BitEntry(p->vMarksCIO, iFan) )
{
if ( !Gia_ObjLutRefNumId(p->pGia, iFan) )
{
Res = iFan;
goto finish;
}
Vec_IntPush( p->vCands, iFan );
Vec_IntPush( p->vInputs, iFan );
}
}
// all inputs have refs - collect external nodes // all inputs have refs - collect external nodes
Vec_IntForEachEntry( p->vNodes, iObj, i ) Vec_IntForEachEntry( p->vNodes, iObj, i )
@ -277,7 +358,7 @@ int Spl_ManFindOne( Spl_Man_t * p )
if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 0 ) if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 0 )
continue; continue;
assert( Gia_ObjLutRefNumId(p->pGia, iObj) > 0 ); assert( Gia_ObjLutRefNumId(p->pGia, iObj) > 0 );
if ( Gia_ObjLutRefNumId(p->pGia, iObj) >= 5 ) if ( Gia_ObjLutRefNumId(p->pGia, iObj) >= 5 ) // skip nodes with high fanout!
continue; continue;
nFanouts = Spl_ManLutFanouts( p->pGia, iObj, p->vFanouts, p->vMarksNo, p->vMarksCIO ); nFanouts = Spl_ManLutFanouts( p->pGia, iObj, p->vFanouts, p->vMarksNo, p->vMarksCIO );
if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 1 && nFanouts == 1 ) if ( Gia_ObjLutRefNumId(p->pGia, iObj) == 1 && nFanouts == 1 )
@ -310,9 +391,9 @@ int Spl_ManFindOne( Spl_Man_t * p )
Res = Vec_IntEntry( p->vCands, 0 ); Res = Vec_IntEntry( p->vCands, 0 );
finish: finish:
// deref // ref
Vec_IntForEachEntry( p->vNodes, iObj, i ) Gia_ManForEachLut2Vec( p->vNodes, p->pGia, vVec, iObj, i )
Gia_LutForEachFanin( p->pGia, iObj, iFan, k ) Vec_IntForEachEntry( vVec, iFan, k )
Gia_ObjLutRefIncId( p->pGia, iFan ); Gia_ObjLutRefIncId( p->pGia, iFan );
return Res; return Res;
} }
@ -321,7 +402,7 @@ finish:
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Computing window for one pivot node.]
Description [] Description []
@ -330,50 +411,137 @@ finish:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
void Spl_ManComputeOne( Spl_Man_t * p, int iPivot ) int Spl_ManLutMffcSize( Gia_Man_t * p, int iObj, Vec_Int_t * vTemp, Vec_Bit_t * vMarksAnd )
{
int iTemp, i, k = 0;
assert( Gia_ObjIsLut2(p, iObj) );
//Vec_IntPrint( Gia_ObjLutFanins2(p, iObj) );
Gia_ManIncrementTravId( p );
Gia_ManCollectAnds( p, &iObj, 1, vTemp, Gia_ObjLutFanins2(p, iObj) );
Vec_IntForEachEntry( vTemp, iTemp, i )
if ( !Vec_BitEntry(vMarksAnd, iTemp) )
Vec_IntWriteEntry( vTemp, k++, iTemp );
Vec_IntShrink( vTemp, k );
return k;
}
void Spl_ManAddNode( Spl_Man_t * p, int iPivot, Vec_Int_t * vCands )
{
int i, iObj;
Vec_IntPush( p->vNodes, iPivot );
Vec_BitWriteEntry( p->vMarksNo, iPivot, 1 );
Vec_IntAppend( p->vAnds, vCands );
Vec_IntForEachEntry( vCands, iObj, i )
Vec_BitWriteEntry( p->vMarksAnd, iObj, 1 );
}
int Spl_ManComputeOne( Spl_Man_t * p, int iPivot )
{ {
int CountAdd, iObj, i; int CountAdd, iObj, i;
assert( Gia_ObjIsLut(p->pGia, iPivot) ); assert( Gia_ObjIsLut2(p->pGia, iPivot) );
//Gia_ManPrintCone2( p->pGia, Gia_ManObj(p->pGia, iPivot) );
// assume it was previously filled in // assume it was previously filled in
Vec_IntForEachEntry( p->vNodes, iObj, i ) Vec_IntForEachEntry( p->vNodes, iObj, i )
Vec_BitWriteEntry( p->vMarksNo, iObj, 0 ); Vec_BitWriteEntry( p->vMarksNo, iObj, 0 );
Vec_IntForEachEntry( p->vAnds, iObj, i )
Vec_BitWriteEntry( p->vMarksAnd, iObj, 0 );
// double check that it is empty // double check that it is empty
//Gia_ManForEachLut( p->pGia, iObj ) //Gia_ManForEachLut2( p->pGia, iObj )
// assert( !Vec_BitEntry(p->vMarksNo, iObj) ); // assert( !Vec_BitEntry(p->vMarksNo, iObj) );
//Gia_ManForEachLut2( p->pGia, iObj )
// assert( !Vec_BitEntry(p->vMarksAnd, iObj) );
// clean arrays
Vec_IntClear( p->vNodes );
Vec_IntClear( p->vAnds );
// add root node // add root node
Vec_IntFill( p->vNodes, 1, iPivot ); Spl_ManLutMffcSize( p->pGia, iPivot, p->vCands, p->vMarksAnd );
Vec_BitWriteEntry( p->vMarksNo, iPivot, 1 ); Spl_ManAddNode( p, iPivot, p->vCands );
if ( Vec_IntSize(p->vAnds) > p->Limit )
return 0;
//printf( "%d ", iPivot ); //printf( "%d ", iPivot );
// add one node at a time // add one node at a time
p->Count = Spl_ManLutMffcSize( p->pGia, iPivot );
while ( (iObj = Spl_ManFindOne(p)) ) while ( (iObj = Spl_ManFindOne(p)) )
{ {
assert( Gia_ObjIsLut(p->pGia, iObj) ); assert( Gia_ObjIsLut2(p->pGia, iObj) );
CountAdd = Spl_ManLutMffcSize( p->pGia, iObj ); assert( !Vec_BitEntry(p->vMarksNo, iObj) );
if ( p->Count + CountAdd > p->Limit ) CountAdd = Spl_ManLutMffcSize( p->pGia, iObj, p->vCands, p->vMarksAnd );
if ( Vec_IntSize(p->vAnds) + CountAdd > p->Limit )
break; break;
p->Count += CountAdd; Spl_ManAddNode( p, iObj, p->vCands );
Vec_IntPush( p->vNodes, iObj );
Vec_BitWriteEntry( p->vMarksNo, iObj, 1 );
//printf( "+%d ", iObj ); //printf( "+%d ", iObj );
} }
//printf( "\n" ); //printf( "\n" );
Vec_IntSort( p->vNodes, 0 ); Vec_IntSort( p->vNodes, 0 );
Vec_IntSort( p->vAnds, 0 );
Spl_ManWinFindLeavesRoots( p );
Vec_IntSort( p->vLeaves, 0 );
Vec_IntSort( p->vRoots, 0 );
return 1;
} }
/**Function*************************************************************
Synopsis [External procedures.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Gia_ManComputeOneWin( Gia_Man_t * pGia, int iPivot, Vec_Int_t ** pvRoots, Vec_Int_t ** pvNodes, Vec_Int_t ** pvLeaves, Vec_Int_t ** pvAnds )
{
Spl_Man_t * p = (Spl_Man_t *)pGia->pSatlutWinman;
assert( p != NULL );
if ( iPivot == -1 )
{
Spl_ManStop( p );
pGia->pSatlutWinman = NULL;
return 0;
}
if ( !Spl_ManComputeOne( p, iPivot ) )
{
*pvRoots = NULL;
*pvNodes = NULL;
*pvLeaves = NULL;
*pvAnds = NULL;
return 0;
}
*pvRoots = p->vRoots;
*pvNodes = p->vNodes;
*pvLeaves = p->vLeaves;
*pvAnds = p->vAnds;
// Vec_IntPrint( p->vNodes );
return Vec_IntSize(p->vAnds);
}
void Gia_ManComputeOneWinStart( Gia_Man_t * pGia, int fReverse )
{
assert( pGia->pSatlutWinman == NULL );
pGia->pSatlutWinman = Spl_ManAlloc( pGia, 64, fReverse );
}
/**Function*************************************************************
Synopsis [Testing procedure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void Spl_ManComputeOneTest( Gia_Man_t * pGia ) void Spl_ManComputeOneTest( Gia_Man_t * pGia )
{ {
int iLut; int iLut, Count;
Spl_Man_t * p = Spl_ManAlloc( pGia, 64 ); Gia_ManComputeOneWinStart( pGia, 0 );
Gia_ManForEachLut( pGia, iLut ) Gia_ManForEachLut2( pGia, iLut )
{ {
Spl_ManComputeOne( p, iLut ); Vec_Int_t * vRoots, * vNodes, * vLeaves, * vAnds;
Spl_ManWinFindLeavesRoots( p ); Count = Gia_ManComputeOneWin( pGia, iLut, &vRoots, &vNodes, &vLeaves, &vAnds );
// Vec_IntPrint( p->vNodes );
printf( "Obj = %6d : Leaf = %2d. Node = %2d. Root = %2d. AND = %3d.\n", printf( "Obj = %6d : Leaf = %2d. Node = %2d. Root = %2d. AND = %3d.\n",
iLut, Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vRoots), p->Count ); iLut, Vec_IntSize(vLeaves), Vec_IntSize(vNodes), Vec_IntSize(vRoots), Count );
} }
Spl_ManStop( p ); Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL );
} }
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////

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

@ -34822,10 +34822,10 @@ usage:
***********************************************************************/ ***********************************************************************/
int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv ) int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
extern void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nConfl, int fVerbose ); extern void Gia_ManLutSat( Gia_Man_t * p, int nNumber, int nConfl, int fReverse, int fVerbose );
int c, nNumber = 32, nConfl = 0, fVerbose = 0; int c, nNumber = 64, nConfl = 500, fReverse = 0, fVerbose = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "NCvh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "NCrvh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -34852,6 +34852,9 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
nConfl = atoi(argv[globalUtilOptind]); nConfl = atoi(argv[globalUtilOptind]);
globalUtilOptind++; globalUtilOptind++;
break; break;
case 'r':
fReverse ^= 1;
break;
case 'v': case 'v':
fVerbose ^= 1; fVerbose ^= 1;
break; break;
@ -34873,14 +34876,15 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
if ( Gia_ManLutSizeMax(pAbc->pGia) > 4 ) if ( Gia_ManLutSizeMax(pAbc->pGia) > 4 )
Abc_Print( 0, "Current AIG has mapping into %d-LUTs.\n", Gia_ManLutSizeMax(pAbc->pGia) ); Abc_Print( 0, "Current AIG has mapping into %d-LUTs.\n", Gia_ManLutSizeMax(pAbc->pGia) );
Gia_ManLutSat( pAbc->pGia, nNumber, nConfl, fVerbose ); Gia_ManLutSat( pAbc->pGia, nNumber, nConfl, fReverse, fVerbose );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &satlut [-NC num] [-vh]\n" ); Abc_Print( -2, "usage: &satlut [-NC num] [-rvh]\n" );
Abc_Print( -2, "\t performs SAT-based remapping of the 4-LUT network\n" ); Abc_Print( -2, "\t performs SAT-based remapping of the 4-LUT network\n" );
Abc_Print( -2, "\t-N num : the limit on the number of AIG nodes in the window [default = %d]\n", nNumber ); Abc_Print( -2, "\t-N num : the limit on the number of AIG nodes in the window [default = %d]\n", nNumber );
Abc_Print( -2, "\t-C num : the limit on the number of conflicts [default = %d]\n", nNumber ); Abc_Print( -2, "\t-C num : the limit on the number of conflicts [default = %d]\n", nNumber );
Abc_Print( -2, "\t-r : toggles using reverse search [default = %s]\n", fReverse? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : prints the command usage\n"); Abc_Print( -2, "\t-h : prints the command usage\n");
return 1; return 1;
@ -40616,7 +40620,6 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
// Gia_ParTest( pAbc->pGia, nWords, nProcs ); // Gia_ParTest( pAbc->pGia, nWords, nProcs );
Gia_Iso3Test( pAbc->pGia ); Gia_Iso3Test( pAbc->pGia );
// printf( "\nThis command is currently disabled.\n\n" ); // printf( "\nThis command is currently disabled.\n\n" );
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" ); Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" );

2
src/base/abci/abcCollapse.c
View File

@ -750,7 +750,7 @@ Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCu
Gia_ManForEachCiVec( vSupp, p, pObj, i ) Gia_ManForEachCiVec( vSupp, p, pObj, i )
Vec_IntPush( vSuppObjs, Gia_ObjId(p, pObj) ); Vec_IntPush( vSuppObjs, Gia_ObjId(p, pObj) );
Gia_ManIncrementTravId( p ); Gia_ManIncrementTravId( p );
Gia_ManCollectAnds( p, &iCoObjId, 1, vAnds ); Gia_ManCollectAnds( p, &iCoObjId, 1, vAnds, NULL );
assert( Vec_IntSize(vAnds) > 0 ); assert( Vec_IntSize(vAnds) > 0 );
// pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat1, &pSat2, &pSat3 ); // pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, &pSat1, &pSat2, &pSat3 );
pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, NULL, NULL, NULL ); pSat = Abc_NtkClpDeriveSatSolver( pCnf, iCoObjId, vSuppObjs, vAnds, vMap, NULL, NULL, NULL );