summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/dau/dauGia.c6
-rw-r--r--src/opt/dsc/dsc.c14
-rw-r--r--src/opt/lpk/lpkCore.c6
-rw-r--r--src/opt/lpk/lpkCut.c6
-rw-r--r--src/opt/sbd/module.make4
-rw-r--r--src/opt/sbd/sbd.h7
-rw-r--r--src/opt/sbd/sbdCnf.c4
-rw-r--r--src/opt/sbd/sbdCore.c951
-rw-r--r--src/opt/sbd/sbdCut.c872
-rw-r--r--src/opt/sbd/sbdCut2.c431
-rw-r--r--src/opt/sbd/sbdInt.h49
-rw-r--r--src/opt/sbd/sbdLut.c311
-rw-r--r--src/opt/sbd/sbdPath.c197
-rw-r--r--src/opt/sbd/sbdSat.c4
-rw-r--r--src/opt/sbd/sbdWin.c213
-rw-r--r--src/opt/sfm/sfmCnf.c4
16 files changed, 2917 insertions, 162 deletions
diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c
index 5e74ad21..fa757e62 100644
--- a/src/opt/dau/dauGia.c
+++ b/src/opt/dau/dauGia.c
@@ -241,7 +241,7 @@ int Dau_DsdBalance( Gia_Man_t * pGia, int * pFans, int nFans, int fAnd )
if ( pGia->pHTable == NULL )
{
if ( fAnd )
- iFan = Gia_ManAppendAnd( pGia, iFan0, iFan1 );
+ iFan = Gia_ManAppendAnd2( pGia, iFan0, iFan1 );
else if ( pGia->pMuxes )
{
int fCompl = Abc_LitIsCompl(iFan0) ^ Abc_LitIsCompl(iFan1);
@@ -249,7 +249,7 @@ int Dau_DsdBalance( Gia_Man_t * pGia, int * pFans, int nFans, int fAnd )
iFan = Abc_LitNotCond( iFan, fCompl );
}
else
- iFan = Gia_ManAppendXor( pGia, iFan0, iFan1 );
+ iFan = Gia_ManAppendXor2( pGia, iFan0, iFan1 );
}
else
{
@@ -361,7 +361,7 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
if ( pGia->pMuxes )
Res = Gia_ManAppendMux( pGia, Temp[0], Temp[1], Temp[2] );
else
- Res = Gia_ManAppendMux( pGia, Temp[0], Temp[1], Temp[2] );
+ Res = Gia_ManAppendMux2( pGia, Temp[0], Temp[1], Temp[2] );
}
else
{
diff --git a/src/opt/dsc/dsc.c b/src/opt/dsc/dsc.c
index ce180fe3..7ddeeed9 100644
--- a/src/opt/dsc/dsc.c
+++ b/src/opt/dsc/dsc.c
@@ -51,14 +51,14 @@ struct Dsc_node_t_
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-inline void xorInPlace( word * pOut, word * pIn2, int nWords)
+static inline void xorInPlace( word * pOut, word * pIn2, int nWords)
{
int w;
for ( w = 0; w < nWords; w++ )
pOut[w] ^= pIn2[w];
}
-void dsc_debug_node(Dsc_node_t * pNode, int nVars, const int TRUTH_WORDS) {
+static inline void dsc_debug_node(Dsc_node_t * pNode, int nVars, const int TRUTH_WORDS) {
int i;
printf("Node:\t%s\n",pNode->exp);
printf("\tneg cof:\t");Abc_TtPrintHexRev(stdout, pNode->pNegCof, nVars);
@@ -75,7 +75,7 @@ void dsc_debug_node(Dsc_node_t * pNode, int nVars, const int TRUTH_WORDS) {
printf("\n");
}
-inline int dsc_and_test(Dsc_node_t *ni, Dsc_node_t *nj, const int TRUTH_WORDS, int* ci, int* cj) {
+static inline int dsc_and_test(Dsc_node_t *ni, Dsc_node_t *nj, const int TRUTH_WORDS, int* ci, int* cj) {
if (Abc_TtEqual(ni->pNegCof, nj->pNegCof, TRUTH_WORDS)) {*ci=1; *cj=1; return 1;}
else if (Abc_TtEqual(ni->pNegCof, nj->pPosCof, TRUTH_WORDS)) {*ci=1; *cj=0; return 1;}
else if (Abc_TtEqual(ni->pPosCof, nj->pNegCof, TRUTH_WORDS)) {*ci=0; *cj=1; return 1;}
@@ -83,11 +83,11 @@ inline int dsc_and_test(Dsc_node_t *ni, Dsc_node_t *nj, const int TRUTH_WORDS, i
return 0;
}
-inline int dsc_xor_test(Dsc_node_t *ni, Dsc_node_t *nj, const int TRUTH_WORDS) {
+static inline int dsc_xor_test(Dsc_node_t *ni, Dsc_node_t *nj, const int TRUTH_WORDS) {
return Abc_TtEqual(ni->pBoolDiff, nj->pBoolDiff, TRUTH_WORDS);
}
-void concat(char* target, char begin, char end, char* s1, int s1Polarity, char* s2, int s2Polarity) {
+static inline void concat(char* target, char begin, char end, char* s1, int s1Polarity, char* s2, int s2Polarity) {
*target++ = begin;
//s1
if (!s1Polarity)
@@ -104,7 +104,7 @@ void concat(char* target, char begin, char end, char* s1, int s1Polarity, char*
*target = '\0';
}
-void cubeCofactor(word * const pTruth, const unsigned int * const cubeCof, const int TRUTH_WORDS) {
+static inline void cubeCofactor(word * const pTruth, const unsigned int * const cubeCof, const int TRUTH_WORDS) {
int size = cubeCof[0];
int i;
for (i = 1; i <= size; i++) {
@@ -117,7 +117,7 @@ void cubeCofactor(word * const pTruth, const unsigned int * const cubeCof, const
}
}
-void merge(unsigned int * const pOut, const unsigned int * const pIn) {
+static inline void merge(unsigned int * const pOut, const unsigned int * const pIn) {
const int elementsToCopy = pIn[0];
int i, j;
for (i = pOut[0]+1, j = 1; j <= elementsToCopy; i++, j++) {
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index a9088d10..6595b365 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -96,12 +96,12 @@ void Lpk_IfManStart( Lpk_Man_t * p )
int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
{
Vec_Ptr_t * vNodes;
- Abc_Obj_t * pTemp;
+ Abc_Obj_t * pTemp, * pTemp2;
int i;
vNodes = Vec_VecEntry( p->vVisited, iNode );
if ( Vec_PtrSize(vNodes) == 0 )
return 1;
- Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pTemp, i )
+ Vec_PtrForEachEntryDouble( Abc_Obj_t *, Abc_Obj_t *, vNodes, pTemp, pTemp2, i )
{
// check if the node has changed
pTemp = Abc_NtkObj( p->pNtk, (int)(ABC_PTRUINT_T)pTemp );
@@ -110,7 +110,7 @@ int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode )
// check if the number of fanouts has changed
// if ( Abc_ObjFanoutNum(pTemp) != (int)Vec_PtrEntry(vNodes, i+1) )
// return 1;
- i++;
+// i++;
}
return 0;
}
diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c
index 73711f2b..208facf2 100644
--- a/src/opt/lpk/lpkCut.c
+++ b/src/opt/lpk/lpkCut.c
@@ -234,7 +234,7 @@ void Lpk_NodeRecordImpact( Lpk_Man_t * p )
{
Lpk_Cut_t * pCut;
Vec_Ptr_t * vNodes = Vec_VecEntry( p->vVisited, p->pObj->Id );
- Abc_Obj_t * pNode;
+ Abc_Obj_t * pNode, * pNode2;
int i, k;
// collect the nodes that impact the given node
Vec_PtrClear( vNodes );
@@ -252,11 +252,11 @@ void Lpk_NodeRecordImpact( Lpk_Man_t * p )
}
}
// clear the marks
- Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
+ Vec_PtrForEachEntryDouble( Abc_Obj_t *, Abc_Obj_t *, vNodes, pNode, pNode2, i )
{
pNode = Abc_NtkObj( p->pNtk, (int)(ABC_PTRUINT_T)pNode );
pNode->fMarkC = 0;
- i++;
+// i++;
}
//printf( "%d ", Vec_PtrSize(vNodes) );
}
diff --git a/src/opt/sbd/module.make b/src/opt/sbd/module.make
index d966e577..fc176715 100644
--- a/src/opt/sbd/module.make
+++ b/src/opt/sbd/module.make
@@ -1,5 +1,9 @@
SRC += src/opt/sbd/sbd.c \
src/opt/sbd/sbdCnf.c \
src/opt/sbd/sbdCore.c \
+ src/opt/sbd/sbdCut.c \
+ src/opt/sbd/sbdCut2.c \
+ src/opt/sbd/sbdLut.c \
+ src/opt/sbd/sbdPath.c \
src/opt/sbd/sbdSat.c \
src/opt/sbd/sbdWin.c
diff --git a/src/opt/sbd/sbd.h b/src/opt/sbd/sbd.h
index 89d29958..9c419b16 100644
--- a/src/opt/sbd/sbd.h
+++ b/src/opt/sbd/sbd.h
@@ -39,11 +39,18 @@ typedef struct Sbd_Par_t_ Sbd_Par_t;
struct Sbd_Par_t_
{
int nLutSize; // target LUT size
+ int nLutNum; // target LUT count
+ int nCutSize; // target cut size
+ int nCutNum; // target cut count
int nTfoLevels; // the number of TFO levels (windowing)
int nTfoFanMax; // the max number of fanouts (windowing)
int nWinSizeMax; // maximum window size (windowing)
int nBTLimit; // maximum number of SAT conflicts
int nWords; // simulation word count
+ int fMapping; // generate mapping
+ int fMoreCuts; // use several cuts
+ int fFindDivs; // perform divisor search
+ int fUsePath; // optimize only critical path
int fArea; // area-oriented optimization
int fCover; // use complete cover procedure
int fVerbose; // verbose flag
diff --git a/src/opt/sbd/sbdCnf.c b/src/opt/sbd/sbdCnf.c
index 6291baed..8705858e 100644
--- a/src/opt/sbd/sbdCnf.c
+++ b/src/opt/sbd/sbdCnf.c
@@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
void Sbd_PrintCnf( Vec_Str_t * vCnf )
{
- char Entry;
+ signed char Entry;
int i, Lit;
Vec_StrForEachEntry( vCnf, Entry, i )
{
@@ -121,7 +121,7 @@ int Sbd_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf
void Sbd_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar )
{
Vec_Int_t * vClause;
- char Entry;
+ signed char Entry;
int i, Lit;
Vec_WecClear( vRes );
vClause = Vec_WecPushLevel( vRes );
diff --git a/src/opt/sbd/sbdCore.c b/src/opt/sbd/sbdCore.c
index b6ec70f9..4f560a0a 100644
--- a/src/opt/sbd/sbdCore.c
+++ b/src/opt/sbd/sbdCore.c
@@ -1,12 +1,12 @@
/**CFile****************************************************************
- FileName [sbd.c]
+ FileName [sbdCore.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [SAT-based optimization using internal don't-cares.]
- Synopsis []
+ Synopsis [Core procedures.]
Author [Alan Mishchenko]
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: sbdCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
@@ -30,7 +30,6 @@ ABC_NAMESPACE_IMPL_START
#define SBD_MAX_LUTSIZE 6
-
typedef struct Sbd_Man_t_ Sbd_Man_t;
struct Sbd_Man_t_
{
@@ -39,25 +38,34 @@ struct Sbd_Man_t_
Vec_Wec_t * vTfos; // TFO for each node (roots are marked) (windowing)
Vec_Int_t * vLutLevs; // LUT level for each node after resynthesis
Vec_Int_t * vLutCuts; // LUT cut for each nodes after resynthesis
+ Vec_Int_t * vLutCuts2; // LUT cut for each nodes after resynthesis
Vec_Int_t * vMirrors; // alternative node
Vec_Wrd_t * vSims[4]; // simulation information (main, backup, controlability)
Vec_Int_t * vCover; // temporary
Vec_Int_t * vLits; // temporary
- int nConsts; // constants
- int nChanges; // changes
+ Vec_Int_t * vLits2; // temporary
+ int nLuts[6]; // 0=const, 1=1lut, 2=2lut, 3=3lut
+ int nTried;
+ int nUsed;
abctime timeWin;
+ abctime timeCut;
+ abctime timeCov;
abctime timeCnf;
abctime timeSat;
- abctime timeCov;
- abctime timeEnu;
+ abctime timeQbf;
+ abctime timeNew;
abctime timeOther;
abctime timeTotal;
+ Sbd_Sto_t * pSto;
+ Sbd_Srv_t * pSrv;
// target node
int Pivot; // target node
+ int DivCutoff; // the place where D-2 divisors begin
Vec_Int_t * vTfo; // TFO (excludes node, includes roots) - precomputed
Vec_Int_t * vRoots; // TFO root nodes
Vec_Int_t * vWinObjs; // TFI + Pivot + sideTFI + TFO (including roots)
Vec_Int_t * vObj2Var; // SAT variables for the window (indexes of objects in vWinObjs)
+ Vec_Int_t * vDivSet; // divisor variables
Vec_Int_t * vDivVars; // divisor variables
Vec_Int_t * vDivValues; // SAT variables values for the divisor variables
Vec_Wec_t * vDivLevels; // divisors collected by levels
@@ -66,7 +74,8 @@ struct Sbd_Man_t_
sat_solver * pSat; // SAT solver
};
-static inline int * Sbd_ObjCut( Sbd_Man_t * p, int i ) { return Vec_IntEntryP( p->vLutCuts, (p->pPars->nLutSize + 1) * i ); }
+static inline int * Sbd_ObjCut( Sbd_Man_t * p, int i ) { return Vec_IntEntryP( p->vLutCuts, (p->pPars->nLutSize + 1) * i ); }
+static inline int * Sbd_ObjCut2( Sbd_Man_t * p, int i ) { return Vec_IntEntryP( p->vLutCuts2, (p->pPars->nLutSize + 1) * i ); }
static inline word * Sbd_ObjSim0( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[0], p->pPars->nWords * i ); }
static inline word * Sbd_ObjSim1( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP( p->vSims[1], p->pPars->nWords * i ); }
@@ -91,16 +100,23 @@ static inline word * Sbd_ObjSim3( Sbd_Man_t * p, int i ) { return Vec_WrdEntryP(
void Sbd_ParSetDefault( Sbd_Par_t * pPars )
{
memset( pPars, 0, sizeof(Sbd_Par_t) );
- pPars->nLutSize = 4; // target LUT size
- pPars->nTfoLevels = 2; // the number of TFO levels (windowing)
- pPars->nTfoFanMax = 4; // the max number of fanouts (windowing)
- pPars->nWinSizeMax = 0; // maximum window size (windowing)
- pPars->nBTLimit = 0; // maximum number of SAT conflicts
- pPars->nWords = 1; // simulation word count
- pPars->fArea = 0; // area-oriented optimization
- pPars->fCover = 0; // use complete cover procedure
- pPars->fVerbose = 0; // verbose flag
- pPars->fVeryVerbose = 0; // verbose flag
+ pPars->nLutSize = 4; // target LUT size
+ pPars->nLutNum = 3; // target LUT count
+ pPars->nCutSize = (pPars->nLutSize - 1) * pPars->nLutNum + 1; // target cut size
+ pPars->nCutNum = 128; // target cut count
+ pPars->nTfoLevels = 5; // the number of TFO levels (windowing)
+ pPars->nTfoFanMax = 4; // the max number of fanouts (windowing)
+ pPars->nWinSizeMax = 2000; // maximum window size (windowing)
+ pPars->nBTLimit = 0; // maximum number of SAT conflicts
+ pPars->nWords = 1; // simulation word count
+ pPars->fMapping = 1; // generate mapping
+ pPars->fMoreCuts = 0; // use several cuts
+ pPars->fFindDivs = 0; // perform divisor search
+ pPars->fUsePath = 0; // optimize only critical path
+ pPars->fArea = 0; // area-oriented optimization
+ pPars->fCover = 0; // use complete cover procedure
+ pPars->fVerbose = 0; // verbose flag
+ pPars->fVeryVerbose = 0; // verbose flag
}
/**Function*************************************************************
@@ -197,9 +213,11 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
// target node
p->vCover = Vec_IntAlloc( 100 );
p->vLits = Vec_IntAlloc( 100 );
+ p->vLits2 = Vec_IntAlloc( 100 );
p->vRoots = Vec_IntAlloc( 100 );
p->vWinObjs = Vec_IntAlloc( Gia_ManObjNum(pGia) );
p->vObj2Var = Vec_IntStart( Gia_ManObjNum(pGia) );
+ p->vDivSet = Vec_IntAlloc( 100 );
p->vDivVars = Vec_IntAlloc( 100 );
p->vDivValues = Vec_IntAlloc( 100 );
p->vDivLevels = Vec_WecAlloc( 100 );
@@ -218,6 +236,14 @@ Sbd_Man_t * Sbd_ManStart( Gia_Man_t * pGia, Sbd_Par_t * pPars )
Gia_ManForEachCiId( pGia, Id, i )
for ( w = 0; w < p->pPars->nWords; w++ )
Sbd_ObjSim0(p, Id)[w] = Gia_ManRandomW( 0 );
+ // cut enumeration
+ if ( pPars->fMoreCuts )
+ p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, !pPars->fMapping, 1 );
+ else
+ {
+ p->pSto = Sbd_StoAlloc( pGia, p->vMirrors, pPars->nLutSize, pPars->nLutSize, pPars->nCutNum, !pPars->fMapping, 1 );
+ p->pSrv = Sbd_ManCutServerStart( pGia, p->vMirrors, p->vLutLevs, NULL, NULL, pPars->nLutSize, pPars->nCutSize, pPars->nCutNum, 0 );
+ }
return p;
}
void Sbd_ManStop( Sbd_Man_t * p )
@@ -231,16 +257,20 @@ void Sbd_ManStop( Sbd_Man_t * p )
Vec_WrdFree( p->vSims[i] );
Vec_IntFree( p->vCover );
Vec_IntFree( p->vLits );
+ Vec_IntFree( p->vLits2 );
Vec_IntFree( p->vRoots );
Vec_IntFree( p->vWinObjs );
Vec_IntFree( p->vObj2Var );
+ Vec_IntFree( p->vDivSet );
Vec_IntFree( p->vDivVars );
Vec_IntFree( p->vDivValues );
Vec_WecFree( p->vDivLevels );
Vec_IntFree( p->vCounts[0] );
Vec_IntFree( p->vCounts[1] );
Vec_WrdFree( p->vMatrix );
- if ( p->pSat ) sat_solver_delete( p->pSat );
+ sat_solver_delete_p( &p->pSat );
+ if ( p->pSto ) Sbd_StoFree( p->pSto );
+ if ( p->pSrv ) Sbd_ManCutServerStop( p->pSrv );
ABC_FREE( p );
}
@@ -318,12 +348,11 @@ void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot )
Vec_WecInit( p->vDivLevels, LevelMax + 1 );
Vec_IntForEachEntry( p->vWinObjs, Node, i )
Vec_WecPush( p->vDivLevels, Vec_IntEntry(p->vLutLevs, Node), Node );
- // sort primary inputs
- Vec_IntSort( Vec_WecEntry(p->vDivLevels, 0), 0 );
// reload divisors
Vec_IntClear( p->vWinObjs );
Vec_WecForEachLevel( p->vDivLevels, vLevel, i )
{
+ Vec_IntSort( vLevel, 0 );
Vec_IntForEachEntry( vLevel, Node, k )
{
Vec_IntWriteEntry( p->vObj2Var, Node, Vec_IntSize(p->vWinObjs) );
@@ -334,8 +363,28 @@ void Sbd_ManUpdateOrder( Sbd_Man_t * p, int Pivot )
nTimeValidDivs = Vec_IntSize(p->vWinObjs);
}
assert( nTimeValidDivs > 0 );
- Vec_IntFill( p->vDivValues, Abc_MinInt(63, nTimeValidDivs), 0 );
- //printf( "%d ", Abc_MinInt(63, nTimeValidDivs) );
+ Vec_IntClear( p->vDivVars );
+ p->DivCutoff = -1;
+ Vec_IntForEachEntryStartStop( p->vWinObjs, Node, i, Abc_MaxInt(0, nTimeValidDivs-63), nTimeValidDivs )
+ {
+ if ( p->DivCutoff == -1 && Vec_IntEntry(p->vLutLevs, Node) == LevelMax - 2 )
+ p->DivCutoff = Vec_IntSize(p->vDivVars);
+ Vec_IntPush( p->vDivVars, i );
+ }
+ if ( p->DivCutoff == -1 )
+ p->DivCutoff = 0;
+ // verify
+/*
+ assert( Vec_IntSize(p->vDivVars) < 64 );
+ Vec_IntForEachEntryStart( p->vDivVars, Node, i, p->DivCutoff )
+ assert( Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Node)) == LevelMax - 2 );
+ Vec_IntForEachEntryStop( p->vDivVars, Node, i, p->DivCutoff )
+ assert( Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Node)) < LevelMax - 2 );
+*/
+ Vec_IntFill( p->vDivValues, Vec_IntSize(p->vDivVars), 0 );
+ //printf( "%d ", Vec_IntSize(p->vDivVars) );
+// printf( "Node %4d : Win = %5d. Divs = %5d. D1 = %5d. D2 = %5d.\n",
+// Pivot, Vec_IntSize(p->vWinObjs), Vec_IntSize(p->vDivVars), Vec_IntSize(p->vDivVars)-p->DivCutoff, p->DivCutoff );
}
void Sbd_ManWindowSim_rec( Sbd_Man_t * p, int NodeInit )
{
@@ -407,7 +456,14 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
Gia_ManIncrementTravId( p->pGia );
Gia_ObjSetTravIdCurrentId(p->pGia, 0);
Sbd_ManWindowSim_rec( p, Pivot );
+ if ( p->pPars->nWinSizeMax && Vec_IntSize(p->vWinObjs) > p->pPars->nWinSizeMax )
+ {
+ p->timeWin += Abc_Clock() - clk;
+ return 0;
+ }
Sbd_ManUpdateOrder( p, Pivot );
+ assert( Vec_IntSize(p->vDivVars) == Vec_IntSize(p->vDivValues) );
+ assert( Vec_IntSize(p->vDivVars) < Vec_IntSize(p->vWinObjs) );
// simulate node
Gia_ManObj(p->pGia, Pivot)->fMark0 = 1;
Abc_TtCopy( Sbd_ObjSim1(p, Pivot), Sbd_ObjSim0(p, Pivot), p->pPars->nWords, 1 );
@@ -429,6 +485,11 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
Vec_IntWriteEntry( p->vObj2Var, Abc_Lit2Var(Node), Vec_IntSize(p->vWinObjs) );
Vec_IntPush( p->vWinObjs, Abc_Lit2Var(Node) );
}
+ if ( p->pPars->nWinSizeMax && Vec_IntSize(p->vWinObjs) > p->pPars->nWinSizeMax )
+ {
+ p->timeWin += Abc_Clock() - clk;
+ return 0;
+ }
// compute controlability for node
if ( Vec_IntSize(p->vTfo) == 0 )
Abc_TtFill( Sbd_ObjSim2(p, Pivot), p->pPars->nWords );
@@ -440,8 +501,8 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
p->timeWin += Abc_Clock() - clk;
// propagate controlability to fanins for the TFI nodes starting from the pivot
Sbd_ManPropagateControl( p, Pivot );
- assert( Vec_IntSize(p->vDivValues) < 64 );
- return (int)(Vec_IntSize(p->vDivValues) >= 64);
+ assert( Vec_IntSize(p->vDivValues) <= 64 );
+ return (int)(Vec_IntSize(p->vDivValues) <= 64);
}
/**Function*************************************************************
@@ -457,24 +518,22 @@ int Sbd_ManWindow( Sbd_Man_t * p, int Pivot )
***********************************************************************/
int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
{
- extern void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot );
int nMintCount = 1;
Vec_Ptr_t * vSims;
word * pSims = Sbd_ObjSim0( p, Pivot );
word * pCtrl = Sbd_ObjSim2( p, Pivot );
int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
int RetValue, i, iObj, Ind, fFindOnset, nCares[2] = {0};
+
abctime clk = Abc_Clock();
- extern int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds );
- extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots );
- p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots );
+ p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
p->timeCnf += Abc_Clock() - clk;
if ( p->pSat == NULL )
{
- if ( p->pPars->fVerbose )
- printf( "Found stuck-at-%d node %d.\n", 0, Pivot );
+ //if ( p->pPars->fVerbose )
+ // printf( "Found stuck-at-%d node %d.\n", 0, Pivot );
Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
- p->nConsts++;
+ p->nLuts[0]++;
return 0;
}
//return -1;
@@ -494,7 +553,7 @@ int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
nCares[0] = nCares[0] < nMintCount ? nMintCount - nCares[0] : 0;
nCares[1] = nCares[1] < nMintCount ? nMintCount - nCares[1] : 0;
- if ( p->pPars->fVerbose )
+ if ( p->pPars->fVeryVerbose )
printf( "Computing %d offset and %d onset minterms for node %d.\n", nCares[0], nCares[1], Pivot );
if ( Vec_IntSize(p->vLits) >= nCares[0] + nCares[1] )
@@ -533,10 +592,10 @@ int Sbd_ManCheckConst( Sbd_Man_t * p, int Pivot )
Vec_PtrFree( vSims );
if ( RetValue >= 0 )
{
- if ( p->pPars->fVerbose )
+ if ( p->pPars->fVeryVerbose )
printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
- p->nConsts++;
+ p->nLuts[0]++;
return RetValue;
}
// set controlability of these minterms
@@ -754,15 +813,15 @@ void Sbd_ManPrintObj( Sbd_Man_t * p, int Pivot )
}
}
-void Sbd_ManMatrPrint( word Cover[64], int nCol, int nRows )
+void Sbd_ManMatrPrint( Sbd_Man_t * p, word Cover[], int nCol, int nRows )
{
int i, k;
for ( i = 0; i <= nCol; i++ )
{
printf( "%2d : ", i );
+ printf( "%d ", i == nCol ? Vec_IntEntry(p->vLutLevs, p->Pivot) : Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Vec_IntEntry(p->vDivVars, i))) );
for ( k = 0; k < nRows; k++ )
- for ( k = 0; k < nRows; k++ )
- printf( "%d", (int)((Cover[i] >> k) & 1) );
+ printf( "%d", (int)((Cover[i] >> k) & 1) );
printf( "\n");
}
printf( "\n");
@@ -778,18 +837,18 @@ static inline void Sbd_ManCoverReverseOrder( word Cover[64] )
}
}
-static inline int Sbd_ManAddCube1( word Cover[64], int nRows, word Cube )
+static inline int Sbd_ManAddCube1( int nRowLimit, word Cover[], int nRows, word Cube )
{
int n, m;
if ( 0 )
{
printf( "Adding cube: " );
- for ( n = 0; n < 64; n++ )
+ for ( n = 0; n < nRowLimit; n++ )
printf( "%d", (int)((Cube >> n) & 1) );
printf( "\n" );
}
// do not add contained Cube
- assert( nRows <= 64 );
+ assert( nRows <= nRowLimit );
for ( n = 0; n < nRows; n++ )
if ( (Cover[n] & Cube) == Cover[n] ) // Cube is contained
return nRows;
@@ -797,7 +856,7 @@ static inline int Sbd_ManAddCube1( word Cover[64], int nRows, word Cube )
for ( n = m = 0; n < nRows; n++ )
if ( (Cover[n] & Cube) != Cube ) // Cover[n] is not contained
Cover[m++] = Cover[n];
- if ( m < 64 )
+ if ( m < nRowLimit )
Cover[m++] = Cube;
for ( n = m; n < nRows; n++ )
Cover[n] = 0;
@@ -832,15 +891,15 @@ static inline int Sbd_ManAddCube2( word Cover[2][64], int nRows, word Cube[2] )
return nRows;
}
-static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDivs )
+static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[], int nDivs )
{
int c0, c1, c2, c3;
word Target = Cover[nDivs];
- Vec_IntClear( p->vDivVars );
+ Vec_IntClear( p->vDivSet );
for ( c0 = 0; c0 < nDivs; c0++ )
if ( Cover[c0] == Target )
{
- Vec_IntPush( p->vDivVars, c0 );
+ Vec_IntPush( p->vDivSet, c0 );
return 1;
}
@@ -848,8 +907,8 @@ static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDi
for ( c1 = c0+1; c1 < nDivs; c1++ )
if ( (Cover[c0] | Cover[c1]) == Target )
{
- Vec_IntPush( p->vDivVars, c0 );
- Vec_IntPush( p->vDivVars, c1 );
+ Vec_IntPush( p->vDivSet, c0 );
+ Vec_IntPush( p->vDivSet, c1 );
return 1;
}
@@ -858,9 +917,9 @@ static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDi
for ( c2 = c1+1; c2 < nDivs; c2++ )
if ( (Cover[c0] | Cover[c1] | Cover[c2]) == Target )
{
- Vec_IntPush( p->vDivVars, c0 );
- Vec_IntPush( p->vDivVars, c1 );
- Vec_IntPush( p->vDivVars, c2 );
+ Vec_IntPush( p->vDivSet, c0 );
+ Vec_IntPush( p->vDivSet, c1 );
+ Vec_IntPush( p->vDivSet, c2 );
return 1;
}
@@ -871,10 +930,10 @@ static inline int Sbd_ManFindCandsSimple( Sbd_Man_t * p, word Cover[64], int nDi
{
if ( (Cover[c0] | Cover[c1] | Cover[c2] | Cover[c3]) == Target )
{
- Vec_IntPush( p->vDivVars, c0 );
- Vec_IntPush( p->vDivVars, c1 );
- Vec_IntPush( p->vDivVars, c2 );
- Vec_IntPush( p->vDivVars, c3 );
+ Vec_IntPush( p->vDivSet, c0 );
+ Vec_IntPush( p->vDivSet, c1 );
+ Vec_IntPush( p->vDivSet, c2 );
+ Vec_IntPush( p->vDivSet, c3 );
return 1;
}
}
@@ -891,11 +950,11 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
if ( nDivs < 8 || p->pPars->fCover )
return Sbd_ManFindCandsSimple( p, Cover, nDivs );
- Vec_IntClear( p->vDivVars );
+ Vec_IntClear( p->vDivSet );
for ( c0 = 0; c0 < nDivs; c0++ )
if ( Cover[c0] == Target )
{
- Vec_IntPush( p->vDivVars, c0 );
+ Vec_IntPush( p->vDivSet, c0 );
return 1;
}
@@ -903,8 +962,8 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
for ( c1 = c0+1; c1 < nDivs; c1++ )
if ( (Cover[c0] | Cover[c1]) == Target )
{
- Vec_IntPush( p->vDivVars, c0 );
- Vec_IntPush( p->vDivVars, c1 );
+ Vec_IntPush( p->vDivSet, c0 );
+ Vec_IntPush( p->vDivSet, c1 );
return 1;
}
@@ -923,9 +982,9 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
for ( c2 = c1+1; c2 < Limits[2]; c2++ )
if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]]) == Target )
{
- Vec_IntPush( p->vDivVars, Order[c0] );
- Vec_IntPush( p->vDivVars, Order[c1] );
- Vec_IntPush( p->vDivVars, Order[c2] );
+ Vec_IntPush( p->vDivSet, Order[c0] );
+ Vec_IntPush( p->vDivSet, Order[c1] );
+ Vec_IntPush( p->vDivSet, Order[c2] );
return 1;
}
@@ -936,10 +995,10 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
{
if ( (Cover[Order[c0]] | Cover[Order[c1]] | Cover[Order[c2]] | Cover[Order[c3]]) == Target )
{
- Vec_IntPush( p->vDivVars, Order[c0] );
- Vec_IntPush( p->vDivVars, Order[c1] );
- Vec_IntPush( p->vDivVars, Order[c2] );
- Vec_IntPush( p->vDivVars, Order[c3] );
+ Vec_IntPush( p->vDivSet, Order[c0] );
+ Vec_IntPush( p->vDivSet, Order[c1] );
+ Vec_IntPush( p->vDivSet, Order[c2] );
+ Vec_IntPush( p->vDivSet, Order[c3] );
return 1;
}
}
@@ -950,12 +1009,11 @@ static inline int Sbd_ManFindCands( Sbd_Man_t * p, word Cover[64], int nDivs )
int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
{
int fVerbose = 0;
- abctime clk, clkSat = 0, clkEnu = 0, clkAll = Abc_Clock();
+ abctime clk;
int nIters, nItersMax = 32;
- extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vValues, Vec_Int_t * vTemp );
word MatrS[64] = {0}, MatrC[2][64] = {{0}}, Cubes[2][2][64] = {{{0}}}, Cover[64] = {0}, Cube, CubeNew[2];
- int i, k, n, Index, nCubes[2] = {0}, nRows = 0, nRowsOld;
+ int i, k, n, Node, Index, nCubes[2] = {0}, nRows = 0, nRowsOld;
int nDivs = Vec_IntSize(p->vDivValues);
int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
@@ -969,11 +1027,11 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
Sbd_ManPrintObj( p, Pivot );
// collect bit-matrices
- for ( i = 0; i < nDivs; i++ )
+ Vec_IntForEachEntry( p->vDivVars, Node, i )
{
- MatrS[63-i] = *Sbd_ObjSim0( p, Vec_IntEntry(p->vWinObjs, i) );
- MatrC[0][63-i] = *Sbd_ObjSim2( p, Vec_IntEntry(p->vWinObjs, i) );
- MatrC[1][63-i] = *Sbd_ObjSim3( p, Vec_IntEntry(p->vWinObjs, i) );
+ MatrS[63-i] = *Sbd_ObjSim0( p, Vec_IntEntry(p->vWinObjs, Node) );
+ MatrC[0][63-i] = *Sbd_ObjSim2( p, Vec_IntEntry(p->vWinObjs, Node) );
+ MatrC[1][63-i] = *Sbd_ObjSim3( p, Vec_IntEntry(p->vWinObjs, Node) );
}
MatrS[63-i] = *Sbd_ObjSim0( p, Pivot );
MatrC[0][63-i] = *Sbd_ObjSim2( p, Pivot );
@@ -1029,7 +1087,7 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
{
Cube = (Cubes[0][1][i] & Cubes[1][0][k]) | (Cubes[0][0][i] & Cubes[1][1][k]);
assert( Cube );
- nRows = Sbd_ManAddCube1( Cover, nRows, Cube );
+ nRows = Sbd_ManAddCube1( 64, Cover, nRows, Cube );
}
Sbd_ManCoverReverseOrder( Cover );
@@ -1049,29 +1107,25 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ )
{
if ( p->pPars->fVerbose )
- Sbd_ManMatrPrint( Cover, nDivs, nRows );
+ Sbd_ManMatrPrint( p, Cover, nDivs, nRows );
clk = Abc_Clock();
if ( !Sbd_ManFindCands( p, Cover, nDivs ) )
{
if ( p->pPars->fVerbose )
printf( "Cannot find a feasible cover.\n" );
- clkEnu += Abc_Clock() - clk;
- clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
- p->timeSat += clkSat;
- p->timeCov += clkAll;
- p->timeEnu += clkEnu;
+ p->timeCov += Abc_Clock() - clk;
return RetValue;
}
- clkEnu += Abc_Clock() - clk;
+ p->timeCov += Abc_Clock() - clk;
if ( p->pPars->fVerbose )
printf( "Candidate support: " ),
- Vec_IntPrint( p->vDivVars );
+ Vec_IntPrint( p->vDivSet );
clk = Abc_Clock();
- *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivVars, p->vDivValues, p->vLits );
- clkSat += Abc_Clock() - clk;
+ *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
+ p->timeSat += Abc_Clock() - clk;
if ( *pTruth == SBD_SAT_UNDEC )
printf( "Node %d: Undecided.\n", Pivot );
@@ -1103,21 +1157,445 @@ int Sbd_ManExplore( Sbd_Man_t * p, int Pivot, word * pTruth )
if ( p->pPars->fVerbose )
{
printf( "Node %d: UNSAT.\n", Pivot );
- Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivVars) ), printf( "\n" );
+ Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivSet) ), printf( "\n" );
}
RetValue = 1;
break;
}
//break;
}
- //printf( "Node %4d : Iter = %4d Start table = %4d Final table = %4d\n", Pivot, nIters, nRowsOld, nRows );
- clkAll = Abc_Clock() - clkAll - clkSat - clkEnu;
- p->timeSat += clkSat;
- p->timeCov += clkAll;
- p->timeEnu += clkEnu;
return RetValue;
}
+int Sbd_ManExplore2( Sbd_Man_t * p, int Pivot, word * pTruth )
+{
+ abctime clk;
+ word Onset[64] = {0}, Offset[64] = {0}, Cube;
+ word CoverRows[64] = {0}, CoverCols[64] = {0};
+ int nIters, nItersMax = 32;
+ int i, k, nRows = 0;
+
+ int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
+ int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
+ int nDivs = Vec_IntSize( p->vDivVars );
+ int nConsts = 4;
+ int RetValue;
+
+ clk = Abc_Clock();
+ //sat_solver_delete_p( &p->pSat );
+ p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
+ p->timeCnf += Abc_Clock() - clk;
+
+ assert( nConsts <= 8 );
+ clk = Abc_Clock();
+ RetValue = Sbd_ManCollectConstantsNew( p->pSat, p->vDivVars, nConsts, PivotVar, Onset, Offset );
+ p->timeSat += Abc_Clock() - clk;
+ if ( RetValue >= 0 )
+ {
+ if ( p->pPars->fVeryVerbose )
+ printf( "Found stuck-at-%d node %d.\n", RetValue, Pivot );
+ Vec_IntWriteEntry( p->vLutLevs, Pivot, 0 );
+ p->nLuts[0]++;
+ return RetValue;
+ }
+ RetValue = 0;
+
+ // create rows of the table
+ nRows = 0;
+ for ( i = 0; i < nConsts; i++ )
+ for ( k = 0; k < nConsts; k++ )
+ {
+ Cube = Onset[i] ^ Offset[k];
+ assert( Cube );
+ nRows = Sbd_ManAddCube1( 256, CoverRows, nRows, Cube );
+ }
+ assert( nRows <= 64 );
+
+ // create columns of the table
+ for ( i = 0; i < nRows; i++ )
+ for ( k = 0; k <= nDivs; k++ )
+ if ( (CoverRows[i] >> k) & 1 )
+ Abc_TtXorBit(&CoverCols[k], i);
+
+ // solve the covering problem
+ for ( nIters = 0; nIters < nItersMax && nRows < 64; nIters++ )
+ {
+ if ( p->pPars->fVeryVerbose )
+ Sbd_ManMatrPrint( p, CoverCols, nDivs, nRows );
+
+ clk = Abc_Clock();
+ if ( !Sbd_ManFindCands( p, CoverCols, nDivs ) )
+ {
+ if ( p->pPars->fVeryVerbose )
+ printf( "Cannot find a feasible cover.\n" );
+ p->timeCov += Abc_Clock() - clk;
+ return 0;
+ }
+ p->timeCov += Abc_Clock() - clk;
+
+ if ( p->pPars->fVeryVerbose )
+ printf( "Candidate support: " ),
+ Vec_IntPrint( p->vDivSet );
+
+ clk = Abc_Clock();
+ *pTruth = Sbd_ManSolve( p->pSat, PivotVar, FreeVar+nIters, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
+ p->timeSat += Abc_Clock() - clk;
+
+ if ( *pTruth == SBD_SAT_UNDEC )
+ printf( "Node %d: Undecided.\n", Pivot );
+ else if ( *pTruth == SBD_SAT_SAT )
+ {
+ if ( p->pPars->fVeryVerbose )
+ {
+ int i;
+ printf( "Node %d: SAT.\n", Pivot );
+ for ( i = 0; i < nDivs; i++ )
+ printf( "%d", Vec_IntEntry(p->vLutLevs, Vec_IntEntry(p->vWinObjs, Vec_IntEntry(p->vDivVars, i))) );
+ printf( "\n" );
+ for ( i = 0; i < nDivs; i++ )
+ printf( "%d", i % 10 );
+ printf( "\n" );
+ for ( i = 0; i < nDivs; i++ )
+ printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x4) ? '0' + (Vec_IntEntry(p->vDivValues, i) & 1) : 'x' );
+ printf( "\n" );
+ for ( i = 0; i < nDivs; i++ )
+ printf( "%c", (Vec_IntEntry(p->vDivValues, i) & 0x8) ? '0' + ((Vec_IntEntry(p->vDivValues, i) >> 1) & 1) : 'x' );
+ printf( "\n" );
+ }
+ // add row to the covering table
+ for ( i = 0; i < nDivs; i++ )
+ if ( Vec_IntEntry(p->vDivValues, i) == 0xE || Vec_IntEntry(p->vDivValues, i) == 0xD )
+ CoverCols[i] |= ((word)1 << nRows);
+ CoverCols[nDivs] |= ((word)1 << nRows);
+ nRows++;
+ }
+ else
+ {
+ if ( p->pPars->fVeryVerbose )
+ {
+ printf( "Node %d: UNSAT. ", Pivot );
+ Extra_PrintBinary( stdout, (unsigned *)pTruth, 1 << Vec_IntSize(p->vDivSet) ), printf( "\n" );
+ }
+ p->nLuts[1]++;
+ RetValue = 1;
+ break;
+ }
+ }
+ return RetValue;
+}
+
+int Sbd_ManExploreCut( Sbd_Man_t * p, int Pivot, int nLeaves, int * pLeaves, int * pnStrs, Sbd_Str_t * Strs, int * pFreeVar )
+{
+ abctime clk = Abc_Clock();
+ int PivotVar = Vec_IntEntry(p->vObj2Var, Pivot);
+ int Delay = Vec_IntEntry( p->vLutLevs, Pivot );
+ int pNodesTop[SBD_DIV_MAX], pNodesBot[SBD_DIV_MAX], pNodesBot1[SBD_DIV_MAX], pNodesBot2[SBD_DIV_MAX];
+ int nNodesTop = 0, nNodesBot = 0, nNodesBot1 = 0, nNodesBot2 = 0, nNodesDiff = 0, nNodesDiff1 = 0, nNodesDiff2 = 0;
+ int i, k, iObj, nIters, RetValue = 0;
+
+ // try to remove fanins
+ for ( nIters = 0; nIters < nLeaves; nIters++ )
+ {
+ word Truth;
+ // try to remove one variable from divisors
+ Vec_IntClear( p->vDivSet );
+ for ( i = 0; i < nLeaves; i++ )
+ if ( i != nLeaves-1-nIters && pLeaves[i] != -1 )
+ Vec_IntPush( p->vDivSet, Vec_IntEntry(p->vObj2Var, pLeaves[i]) );
+ assert( Vec_IntSize(p->vDivSet) < nLeaves );
+ // compute truth table
+ clk = Abc_Clock();
+ Truth = Sbd_ManSolve( p->pSat, PivotVar, (*pFreeVar)++, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
+ p->timeSat += Abc_Clock() - clk;
+ if ( Truth == SBD_SAT_UNDEC )
+ printf( "Node %d: Undecided.\n", Pivot );
+ else if ( Truth == SBD_SAT_SAT )
+ {
+ int DelayDiff = Vec_IntEntry(p->vLutLevs, pLeaves[nLeaves-1-nIters]) - Delay;
+ if ( DelayDiff > -2 )
+ return 0;
+ }
+ else
+ pLeaves[nLeaves-1-nIters] = -1;
+ }
+ Vec_IntClear( p->vDivSet );
+ for ( i = 0; i < nLeaves; i++ )
+ if ( pLeaves[i] != -1 )
+ Vec_IntPush( p->vDivSet, pLeaves[i] );
+ //printf( "Reduced %d -> %d\n", nLeaves, Vec_IntSize(p->vDivSet) );
+ if ( Vec_IntSize(p->vDivSet) <= p->pPars->nLutSize )
+ {
+ word Truth;
+ *pnStrs = 1;
+ // remap divisors
+ Vec_IntForEachEntry( p->vDivSet, iObj, i )
+ Vec_IntWriteEntry( p->vDivSet, i, Vec_IntEntry(p->vObj2Var, iObj) );
+ // compute truth table
+ clk = Abc_Clock();
+ Truth = Sbd_ManSolve( p->pSat, PivotVar, (*pFreeVar)++, p->vDivSet, p->vDivVars, p->vDivValues, p->vLits );
+ p->timeSat += Abc_Clock() - clk;
+ if ( Truth == SBD_SAT_SAT )
+ {
+ printf( "The cut at node %d is not topological.\n", p->Pivot );
+ return 0;
+ }
+ assert( Truth != SBD_SAT_UNDEC && Truth != SBD_SAT_SAT );
+ // create structure
+ Strs->fLut = 1;
+ Strs->nVarIns = Vec_IntSize( p->vDivSet );
+ for ( i = 0; i < Strs->nVarIns; i++ )
+ Strs->VarIns[i] = i;
+ Strs->Res = Truth;
+ p->nLuts[1]++;
+ //Extra_PrintBinary( stdout, (unsigned *)&Truth, 1 << Strs->nVarIns ), printf( "\n" );
+ return 1;
+ }
+ assert( Vec_IntSize(p->vDivSet) > p->pPars->nLutSize );
+
+ // count number of nodes on each level
+ nNodesTop = nNodesBot = nNodesBot1 = nNodesBot2 = 0;
+ Vec_IntForEachEntry( p->vDivSet, iObj, i )
+ {
+ int DelayDiff = Vec_IntEntry(p->vLutLevs, iObj) - Delay;
+ if ( DelayDiff > -2 )
+ break;
+ if ( DelayDiff == -2 )
+ pNodesTop[nNodesTop++] = i;
+ else // if ( DelayDiff < -2 )
+ {
+ pNodesBot[nNodesBot++] = i;
+ if ( DelayDiff == -3 )
+ pNodesBot1[nNodesBot1++] = i;
+ else // if ( DelayDiff < -3 )
+ pNodesBot2[nNodesBot2++] = i;
+ }
+ Vec_IntWriteEntry( p->vDivSet, i, Vec_IntEntry(p->vObj2Var, iObj) );
+ }
+ assert( nNodesBot == nNodesBot1 + nNodesBot2 );
+ if ( i < Vec_IntSize(p->vDivSet) )
+ return 0;
+ if ( nNodesTop > p->pPars->nLutSize-1 )
+ return 0;
+
+ // try 44
+ if ( Vec_IntSize(p->vDivSet) <= 2*p->pPars->nLutSize-1 )
+ {
+ int nMoved = 0;
+ if ( nNodesBot > p->pPars->nLutSize ) // need to move bottom left-over to the top
+ {
+ while ( nNodesBot > p->pPars->nLutSize )
+ pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot], nMoved++;
+ assert( nNodesBot == p->pPars->nLutSize );
+ }
+ assert( nNodesBot <= p->pPars->nLutSize );
+ assert( nNodesTop <= p->pPars->nLutSize-1 );
+
+ Strs[0].fLut = 1;
+ Strs[0].nVarIns = p->pPars->nLutSize;
+ for ( i = 0; i < nNodesTop; i++ )
+ Strs[0].VarIns[i] = pNodesTop[i];
+ for ( ; i < p->pPars->nLutSize; i++ )
+ Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop;
+ Strs[0].Res = 0;
+
+ Strs[1].fLut = 1;
+ Strs[1].nVarIns = nNodesBot;
+ for ( i = 0; i < nNodesBot; i++ )
+ Strs[1].VarIns[i] = pNodesBot[i];
+ Strs[1].Res = 0;
+
+ nNodesDiff = p->pPars->nLutSize-1 - nNodesTop;
+ assert( nNodesDiff >= 0 && nNodesDiff <= 3 );
+ for ( k = 0; k < nNodesDiff; k++ )
+ {
+ Strs[2+k].fLut = 0;
+ Strs[2+k].nVarIns = nNodesBot;
+ for ( i = 0; i < nNodesBot; i++ )
+ Strs[2+k].VarIns[i] = pNodesBot[i];
+ Strs[2+k].Res = 0;
+ }
+
+ *pnStrs = 2 + nNodesDiff;
+ clk = Abc_Clock();
+ RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, p->vDivSet, *pnStrs, Strs );
+ p->timeQbf += Abc_Clock() - clk;
+ if ( RetValue )
+ p->nLuts[2]++;
+
+ while ( nMoved-- )
+ pNodesBot[nNodesBot++] = pNodesTop[--nNodesTop];
+ }
+
+ if ( RetValue )
+ return RetValue;
+ if ( p->pPars->nLutNum < 3 )
+ return 0;
+ if ( Vec_IntSize(p->vDivSet) < 2*p->pPars->nLutSize-1 )
+ return 0;
+
+ // try 444 -- LUT(LUT, LUT)
+ if ( nNodesTop <= p->pPars->nLutSize-2 )
+ {
+ int nMoved = 0;
+ if ( nNodesBot > 2*p->pPars->nLutSize ) // need to move bottom left-over to the top
+ {
+ while ( nNodesBot > 2*p->pPars->nLutSize )
+ pNodesTop[nNodesTop++] = pNodesBot[--nNodesBot], nMoved++;
+ assert( nNodesBot == 2*p->pPars->nLutSize );
+ }
+ assert( nNodesBot > p->pPars->nLutSize );
+ assert( nNodesBot <= 2*p->pPars->nLutSize );
+ assert( nNodesTop <= p->pPars->nLutSize-2 );
+
+ Strs[0].fLut = 1;
+ Strs[0].nVarIns = p->pPars->nLutSize;
+ for ( i = 0; i < nNodesTop; i++ )
+ Strs[0].VarIns[i] = pNodesTop[i];
+ for ( ; i < p->pPars->nLutSize; i++ )
+ Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+1 + i-nNodesTop;
+ Strs[0].Res = 0;
+
+ Strs[1].fLut = 1;
+ Strs[1].nVarIns = p->pPars->nLutSize;
+ for ( i = 0; i < Strs[1].nVarIns; i++ )
+ Strs[1].VarIns[i] = pNodesBot[i];
+ Strs[1].Res = 0;
+
+ Strs[2].fLut = 1;
+ Strs[2].nVarIns = p->pPars->nLutSize;
+ for ( i = 0; i < Strs[2].nVarIns; i++ )
+ Strs[2].VarIns[i] = pNodesBot[nNodesBot-p->pPars->nLutSize+i];
+ Strs[2].Res = 0;
+
+ nNodesDiff = p->pPars->nLutSize-2 - nNodesTop;
+ assert( nNodesDiff >= 0 && nNodesDiff <= 2 );
+ for ( k = 0; k < nNodesDiff; k++ )
+ {
+ Strs[3+k].fLut = 0;
+ Strs[3+k].nVarIns = nNodesBot;
+ for ( i = 0; i < nNodesBot; i++ )
+ Strs[3+k].VarIns[i] = pNodesBot[i];
+ Strs[3+k].Res = 0;
+ }
+
+ *pnStrs = 3 + nNodesDiff;
+ clk = Abc_Clock();
+ RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, p->vDivSet, *pnStrs, Strs );
+ p->timeQbf += Abc_Clock() - clk;
+ if ( RetValue )
+ p->nLuts[3]++;
+
+ while ( nMoved-- )
+ pNodesBot[nNodesBot++] = pNodesTop[--nNodesTop];
+ }
+ if ( RetValue )
+ return RetValue;
+
+ // try 444 -- LUT(LUT(LUT))
+ if ( nNodesBot1 + nNodesTop <= 2*p->pPars->nLutSize-2 )
+ {
+ if ( nNodesBot2 > p->pPars->nLutSize ) // need to move bottom left-over to the top
+ {
+ while ( nNodesBot2 > p->pPars->nLutSize )
+ pNodesBot1[nNodesBot1++] = pNodesBot2[--nNodesBot2];
+ assert( nNodesBot2 == p->pPars->nLutSize );
+ }
+ if ( nNodesBot1 > p->pPars->nLutSize-1 ) // need to move bottom left-over to the top
+ {
+ while ( nNodesBot1 > p->pPars->nLutSize-1 )
+ pNodesTop[nNodesTop++] = pNodesBot1[--nNodesBot1];
+ assert( nNodesBot1 == p->pPars->nLutSize-1 );
+ }
+ assert( nNodesBot2 <= p->pPars->nLutSize );
+ assert( nNodesBot1 <= p->pPars->nLutSize-1 );
+ assert( nNodesTop <= p->pPars->nLutSize-1 );
+
+ Strs[0].fLut = 1;
+ Strs[0].nVarIns = p->pPars->nLutSize;
+ for ( i = 0; i < nNodesTop; i++ )
+ Strs[0].VarIns[i] = pNodesTop[i];
+ Strs[0].VarIns[i++] = Vec_IntSize(p->vDivSet)+1;
+ for ( ; i < p->pPars->nLutSize; i++ )
+ Strs[0].VarIns[i] = Vec_IntSize(p->vDivSet)+2 + i-nNodesTop;
+ Strs[0].Res = 0;
+ nNodesDiff1 = p->pPars->nLutSize-1 - nNodesTop;
+
+ Strs[1].fLut = 1;
+ Strs[1].nVarIns = p->pPars->nLutSize;
+ for ( i = 0; i < nNodesBot1; i++ )
+ Strs[1].VarIns[i] = pNodesBot1[i];
+ Strs[1].VarIns[i++] = Vec_IntSize(p->vDivSet)+2;
+ for ( ; i < p->pPars->nLutSize; i++ )
+ Strs[1].VarIns[i] = Vec_IntSize(p->vDivSet)+2+nNodesDiff1 + i-nNodesBot1;
+ Strs[1].Res = 0;
+ nNodesDiff2 = p->pPars->nLutSize-1 - nNodesBot1;
+
+ Strs[2].fLut = 1;
+ Strs[2].nVarIns = nNodesBot2;
+ for ( i = 0; i < Strs[2].nVarIns; i++ )
+ Strs[2].VarIns[i] = pNodesBot2[i];
+ Strs[2].Res = 0;
+
+ nNodesDiff = nNodesDiff1 + nNodesDiff2;
+ assert( nNodesDiff >= 0 && nNodesDiff <= 3 );
+ for ( k = 0; k < nNodesDiff; k++ )
+ {
+ Strs[3+k].fLut = 0;
+ Strs[3+k].nVarIns = nNodesBot2;
+ for ( i = 0; i < nNodesBot2; i++ )
+ Strs[3+k].VarIns[i] = pNodesBot2[i];
+ Strs[3+k].Res = 0;
+ if ( k >= nNodesDiff1 )
+ continue;
+ Strs[3+k].nVarIns += nNodesBot1;
+ for ( i = 0; i < nNodesBot1; i++ )
+ Strs[3+k].VarIns[nNodesBot2 + i] = pNodesBot1[i];
+ }
+
+ *pnStrs = 3 + nNodesDiff;
+ clk = Abc_Clock();
+ RetValue = Sbd_ProblemSolve( p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, p->vDivSet, *pnStrs, Strs );
+ p->timeQbf += Abc_Clock() - clk;
+ if ( RetValue )
+ p->nLuts[4]++;
+ }
+ return RetValue;
+}
+int Sbd_ManExplore3( Sbd_Man_t * p, int Pivot, int * pnStrs, Sbd_Str_t * Strs )
+{
+ int FreeVar = Vec_IntSize(p->vWinObjs) + Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots);
+ int FreeVarStart = FreeVar;
+ int nSize, nLeaves, pLeaves[SBD_DIV_MAX];
+ //sat_solver_delete_p( &p->pSat );
+ abctime clk = Abc_Clock();
+ p->pSat = Sbd_ManSatSolver( p->pSat, p->pGia, p->vMirrors, Pivot, p->vWinObjs, p->vObj2Var, p->vTfo, p->vRoots, 0 );
+ p->timeCnf += Abc_Clock() - clk;
+ // extract one cut
+ if ( p->pSrv )
+ {
+ nLeaves = Sbd_ManCutServerFirst( p->pSrv, Pivot, pLeaves );
+ if ( nLeaves == -1 )
+ return 0;
+ assert( nLeaves <= p->pPars->nCutSize );
+ if ( Sbd_ManExploreCut( p, Pivot, nLeaves, pLeaves, pnStrs, Strs, &FreeVar ) )
+ return 1;
+ return 0;
+ }
+ // extract one cut
+ for ( nSize = p->pPars->nLutSize + 1; nSize <= p->pPars->nCutSize; nSize++ )
+ {
+ nLeaves = Sbd_StoObjBestCut( p->pSto, Pivot, nSize, pLeaves );
+ if ( nLeaves == -1 )
+ continue;
+ assert( nLeaves == nSize );
+ if ( Sbd_ManExploreCut( p, Pivot, nLeaves, pLeaves, pnStrs, Strs, &FreeVar ) )
+ return 1;
+ }
+ assert( FreeVar - FreeVarStart <= SBD_FVAR_MAX );
+ return 0;
+}
+
+
/**Function*************************************************************
Synopsis [Computes delay-oriented k-feasible cut at the node.]
@@ -1231,9 +1709,10 @@ int Sbd_ManMergeCuts( Sbd_Man_t * p, int Node )
assert( iFan0 != iFan1 );
assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
Vec_IntWriteEntry( p->vLutLevs, Node, LevCur );
+ //Vec_IntWriteEntry( p->vLevs, Node, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, iFan0), Vec_IntEntry(p->vLevs, iFan1)) );
assert( pCutRes[0] <= p->pPars->nLutSize );
memcpy( Sbd_ObjCut(p, Node), pCutRes, sizeof(int) * (pCutRes[0] + 1) );
- //printf( "Setting node %d with delay %d.\n", Node, LevCur );
+//printf( "Setting node %d with delay %d.\n", Node, LevCur );
return LevCur == 1; // LevCur == Abc_MaxInt(Level0, Level1);
}
int Sbd_ManDelay( Sbd_Man_t * p )
@@ -1294,6 +1773,7 @@ void Sbd_ManFindCut( Sbd_Man_t * p, int Node, Vec_Int_t * vCutLits )
// create cut
assert( Vec_IntEntry(p->vLutLevs, Node) == 0 );
Vec_IntWriteEntry( p->vLutLevs, Node, LevelMax+1 );
+ //Vec_IntWriteEntry( p->vLevs, Node, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObj, Node)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObj, Node))) );
memcpy( Sbd_ObjCut(p, Node), pCut, sizeof(int) * (pCut[0] + 1) );
}
@@ -1306,7 +1786,7 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
int iNewLev;
// collect leaf literals
Vec_IntClear( p->vLits );
- Vec_IntForEachEntry( p->vDivVars, Node, i )
+ Vec_IntForEachEntry( p->vDivSet, Node, i )
{
Node = Vec_IntEntry( p->vWinObjs, Node );
if ( Vec_IntEntry(p->vMirrors, Node) >= 0 )
@@ -1355,7 +1835,99 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
// update delay of the initial node
assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
- p->nChanges++;
+ //Vec_IntWriteEntry( p->vLevs, Pivot, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObj, Pivot)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObj, Pivot))) );
+ return 0;
+}
+
+int Sbd_ManImplement2( Sbd_Man_t * p, int Pivot, int nStrs, Sbd_Str_t * pStrs )
+{
+ //Gia_Obj_t * pObj = NULL;
+ int i, k, w, iLit, Node;
+ int iObjLast = Gia_ManObjNum(p->pGia);
+ int iCurLev = Vec_IntEntry(p->vLutLevs, Pivot);
+ int iNewLev;
+ // collect leaf literals
+ Vec_IntClear( p->vLits );
+ Vec_IntForEachEntry( p->vDivSet, Node, i )
+ {
+ Node = Vec_IntEntry( p->vWinObjs, Node );
+ if ( Vec_IntEntry(p->vMirrors, Node) >= 0 )
+ Vec_IntPush( p->vLits, Vec_IntEntry(p->vMirrors, Node) );
+ else
+ Vec_IntPush( p->vLits, Abc_Var2Lit(Node, 0) );
+ }
+ // collect structure nodes
+ for ( i = 0; i < nStrs; i++ )
+ Vec_IntPush( p->vLits, -1 );
+ // implement structures
+ for ( i = nStrs-1; i >= 0; i-- )
+ {
+ if ( pStrs[i].fLut )
+ {
+ // collect local literals
+ Vec_IntClear( p->vLits2 );
+ for ( k = 0; k < (int)pStrs[i].nVarIns; k++ )
+ Vec_IntPush( p->vLits2, Vec_IntEntry(p->vLits, pStrs[i].VarIns[k]) );
+ // pretend to have MUXes
+ // assert( p->pGia->pMuxes == NULL );
+ if ( p->pGia->nXors && p->pGia->pMuxes == NULL )
+ p->pGia->pMuxes = (unsigned *)p;
+ // derive new function of the node
+ iLit = Dsm_ManTruthToGia( p->pGia, &pStrs[i].Res, p->vLits2, p->vCover );
+ if ( p->pGia->pMuxes == (unsigned *)p )
+ p->pGia->pMuxes = NULL;
+ }
+ else
+ {
+ iLit = Vec_IntEntry( p->vLits, (int)pStrs[i].Res );
+ assert( iLit > 0 );
+ }
+ // update literal
+ assert( Vec_IntEntry(p->vLits, Vec_IntSize(p->vLits)-nStrs+i) == -1 );
+ Vec_IntWriteEntry( p->vLits, Vec_IntSize(p->vLits)-nStrs+i, iLit );
+ }
+ iLit = Vec_IntEntry( p->vLits, Vec_IntSize(p->vDivSet) );
+ //assert( iObjLast == Gia_ManObjNum(p->pGia) || Abc_Lit2Var(iLit) == Gia_ManObjNum(p->pGia)-1 );
+ // remember this function
+ assert( Vec_IntEntry(p->vMirrors, Pivot) == -1 );
+ Vec_IntWriteEntry( p->vMirrors, Pivot, iLit );
+ if ( p->pPars->fVeryVerbose )
+ printf( "Replacing node %d by literal %d.\n", Pivot, iLit );
+
+ // extend data-structure to accommodate new nodes
+ assert( Vec_IntSize(p->vLutLevs) == iObjLast );
+ for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
+ {
+ assert( i == Vec_IntSize(p->vMirrors) );
+ Vec_IntPush( p->vMirrors, -1 );
+ Sbd_StoRefObj( p->pSto, i, i == Gia_ManObjNum(p->pGia)-1 ? Pivot : -1 );
+ }
+ Sbd_StoDerefObj( p->pSto, Pivot );
+ for ( i = iObjLast; i < Gia_ManObjNum(p->pGia); i++ )
+ {
+ //Gia_Obj_t * pObjI = Gia_ManObj( p->pGia, i );
+ abctime clk = Abc_Clock();
+ int Delay = Sbd_StoComputeCutsNode( p->pSto, i );
+ p->timeCut += Abc_Clock() - clk;
+ assert( i == Vec_IntSize(p->vLutLevs) );
+ Vec_IntPush( p->vLutLevs, Delay );
+ //Vec_IntPush( p->vLevs, 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObjI, i)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObjI, i))) );
+ Vec_IntPush( p->vObj2Var, 0 );
+ Vec_IntFillExtra( p->vLutCuts, Vec_IntSize(p->vLutCuts) + p->pPars->nLutSize + 1, 0 );
+ Sbd_StoSaveBestDelayCut( p->pSto, i, Sbd_ObjCut(p, i) );
+ //Sbd_ManFindCut( p, i, p->vLits );
+ for ( k = 0; k < 4; k++ )
+ for ( w = 0; w < p->pPars->nWords; w++ )
+ Vec_WrdPush( p->vSims[k], 0 );
+ }
+ // make sure delay reduction is achieved
+ iNewLev = Vec_IntEntry( p->vLutLevs, Abc_Lit2Var(iLit) );
+ assert( !iNewLev || iNewLev < iCurLev );
+ // update delay of the initial node
+ //pObj = Gia_ManObj( p->pGia, Pivot );
+ assert( Vec_IntEntry(p->vLutLevs, Pivot) == iCurLev );
+ Vec_IntWriteEntry( p->vLutLevs, Pivot, iNewLev );
+ //Vec_IntWriteEntry( p->vLevs, Pivot, Pivot ? 1+Abc_MaxInt(Vec_IntEntry(p->vLevs, Gia_ObjFaninId0(pObj, Pivot)), Vec_IntEntry(p->vLevs, Gia_ObjFaninId1(pObj, Pivot))) : 0 );
return 0;
}
@@ -1370,6 +1942,70 @@ int Sbd_ManImplement( Sbd_Man_t * p, int Pivot, word Truth )
SeeAlso []
***********************************************************************/
+void Sbd_ManDeriveMapping_rec( Sbd_Man_t * p, Gia_Man_t * pNew, int iObj )
+{
+ Gia_Obj_t * pObj; int k, * pCut;
+ if ( !iObj || Gia_ObjIsTravIdCurrentId(pNew, iObj) )
+ return;
+ Gia_ObjSetTravIdCurrentId(pNew, iObj);
+ pObj = Gia_ManObj( pNew, iObj );
+ if ( Gia_ObjIsCi(pObj) )
+ return;
+ assert( Gia_ObjIsAnd(pObj) );
+ pCut = Sbd_ObjCut2( p, iObj );
+ for ( k = 1; k <= pCut[0]; k++ )
+ Sbd_ManDeriveMapping_rec( p, pNew, pCut[k] );
+ // add mapping
+ Vec_IntWriteEntry( pNew->vMapping, iObj, Vec_IntSize(pNew->vMapping) );
+ for ( k = 0; k <= pCut[0]; k++ )
+ Vec_IntPush( pNew->vMapping, pCut[k] );
+ Vec_IntPush( pNew->vMapping, iObj );
+}
+void Sbd_ManDeriveMapping( Sbd_Man_t * p, Gia_Man_t * pNew )
+{
+ Gia_Obj_t * pObj, * pFan;
+ int i, k, iFan, iObjNew, iFanNew, * pCut, * pCutNew;
+ Vec_Int_t * vLeaves = Vec_IntAlloc( 100 );
+ // derive cuts for the new manager
+ p->vLutCuts2 = Vec_IntStart( Gia_ManObjNum(pNew) * (p->pPars->nLutSize + 1) );
+ Gia_ManForEachAnd( p->pGia, pObj, i )
+ {
+ if ( Vec_IntEntry(p->vMirrors, i) >= 0 )
+ continue;
+ if ( pObj->Value == ~0 )
+ continue;
+ iObjNew = Abc_Lit2Var( pObj->Value );
+ if ( !Gia_ObjIsAnd(Gia_ManObj(pNew, iObjNew)) )
+ continue;
+ pCutNew = Sbd_ObjCut2( p, iObjNew );
+ pCut = Sbd_ObjCut( p, i );
+ Vec_IntClear( vLeaves );
+ for ( k = 1; k <= pCut[0]; k++ )
+ {
+ iFan = Vec_IntEntry(p->vMirrors, pCut[k]) >= 0 ? Abc_Lit2Var(Vec_IntEntry(p->vMirrors, pCut[k])) : pCut[k];
+ pFan = Gia_ManObj( p->pGia, iFan );
+ if ( pFan->Value == ~0 )
+ continue;
+ iFanNew = Abc_Lit2Var( pFan->Value );
+ if ( iFanNew == 0 || iFanNew == iObjNew )
+ continue;
+ Vec_IntPushUniqueOrder( vLeaves, iFanNew );
+ }
+ assert( Vec_IntSize(vLeaves) <= p->pPars->nLutSize );
+ //assert( Vec_IntSize(vLeaves) > 1 );
+ pCutNew[0] = Vec_IntSize(vLeaves);
+ memcpy( pCutNew+1, Vec_IntArray(vLeaves), sizeof(int) * Vec_IntSize(vLeaves) );
+ }
+ Vec_IntFree( vLeaves );
+ // create new mapping
+ Vec_IntFreeP( &pNew->vMapping );
+ pNew->vMapping = Vec_IntAlloc( (p->pPars->nLutSize + 2) * Gia_ManObjNum(pNew) );
+ Vec_IntFill( pNew->vMapping, Gia_ManObjNum(pNew), 0 );
+ Gia_ManIncrementTravId( pNew );
+ Gia_ManForEachCo( pNew, pObj, i )
+ Sbd_ManDeriveMapping_rec( p, pNew, Gia_ObjFaninId0p(pNew, pObj) );
+ Vec_IntFreeP( &p->vLutCuts2 );
+}
void Sbd_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * vMirrors )
{
Gia_Obj_t * pObj;
@@ -1391,9 +2027,9 @@ void Sbd_ManDerive_rec( Gia_Man_t * pNew, Gia_Man_t * p, int Node, Vec_Int_t * v
if ( Obj != Node )
Gia_ManObj(p, Node)->Value = Abc_LitNotCond( pObj->Value, Abc_LitIsCompl(Vec_IntEntry(vMirrors, Node)) );
}
-Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
+Gia_Man_t * Sbd_ManDerive( Sbd_Man_t * pMan, Gia_Man_t * p, Vec_Int_t * vMirrors )
{
- Gia_Man_t * pNew;
+ Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i;
Gia_ManFillValue( p );
@@ -1413,6 +2049,13 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
Gia_ManHashStop( pNew );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
Gia_ManTransferTiming( pNew, p );
+ if ( pMan->pPars->fMapping )
+ Sbd_ManDeriveMapping( pMan, pNew );
+ // remove dangling nodes
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManTransferTiming( pNew, pTemp );
+ Gia_ManTransferMapping( pNew, pTemp );
+ Gia_ManStop( pTemp );
return pNew;
}
@@ -1429,81 +2072,147 @@ Gia_Man_t * Sbd_ManDerive( Gia_Man_t * p, Vec_Int_t * vMirrors )
***********************************************************************/
void Sbd_NtkPerformOne( Sbd_Man_t * p, int Pivot )
{
- int RetValue; word Truth = 0;
- if ( Sbd_ManMergeCuts( p, Pivot ) )
+ Sbd_Str_t Strs[SBD_DIV_MAX]; word Truth = 0;
+ int RetValue, nStrs = 0;
+ if ( !p->pSto && Sbd_ManMergeCuts( p, Pivot ) )
return;
- //if ( Pivot != 344 )
- // continue;
- if ( p->pPars->fVerbose )
- printf( "\nLooking at node %d\n", Pivot );
- if ( Sbd_ManWindow( p, Pivot ) )
+ if ( !Sbd_ManWindow( p, Pivot ) )
return;
+ //if ( Vec_IntSize(p->vWinObjs) > 100 )
+ // printf( "Obj %d : Win = %d TFO = %d. Roots = %d.\n", Pivot, Vec_IntSize(p->vWinObjs), Vec_IntSize(p->vTfo), Vec_IntSize(p->vRoots) );
+ p->nTried++;
+ p->nUsed++;
RetValue = Sbd_ManCheckConst( p, Pivot );
if ( RetValue >= 0 )
+ {
Vec_IntWriteEntry( p->vMirrors, Pivot, RetValue );
- else if ( Sbd_ManExplore( p, Pivot, &Truth ) )
- Sbd_ManImplement( p, Pivot, Truth );
+ //if ( p->pPars->fVerbose ) printf( "Node %5d: Detected constant %d.\n", Pivot, RetValue );
+ }
+ else if ( p->pPars->fFindDivs && p->pPars->nLutNum >= 1 && Sbd_ManExplore2( p, Pivot, &Truth ) )
+ {
+ int i;
+ Strs->fLut = 1;
+ Strs->nVarIns = Vec_IntSize( p->vDivSet );
+ for ( i = 0; i < Strs->nVarIns; i++ )
+ Strs->VarIns[i] = i;
+ Strs->Res = Truth;
+ Sbd_ManImplement2( p, Pivot, 1, Strs );
+ //if ( p->pPars->fVerbose ) printf( "Node %5d: Detected LUT%d\n", Pivot, p->pPars->nLutSize );
+ }
+ else if ( p->pPars->nLutNum >= 2 && Sbd_ManExplore3( p, Pivot, &nStrs, Strs ) )
+ {
+ Sbd_ManImplement2( p, Pivot, nStrs, Strs );
+ if ( !p->pPars->fVerbose )
+ return;
+ //if ( Vec_IntSize(p->vDivSet) <= 4 )
+ // printf( "Node %5d: Detected %d\n", Pivot, p->pPars->nLutSize );
+ //else if ( Vec_IntSize(p->vDivSet) <= 6 || (Vec_IntSize(p->vDivSet) == 7 && nStrs == 2) )
+ // printf( "Node %5d: Detected %d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize );
+ //else
+ // printf( "Node %5d: Detected %d%d%d\n", Pivot, p->pPars->nLutSize, p->pPars->nLutSize, p->pPars->nLutSize );
+ }
+ else
+ p->nUsed--;
}
Gia_Man_t * Sbd_NtkPerform( Gia_Man_t * pGia, Sbd_Par_t * pPars )
{
Gia_Man_t * pNew;
Gia_Obj_t * pObj;
+ Vec_Bit_t * vPath;
Sbd_Man_t * p = Sbd_ManStart( pGia, pPars );
- int nNodesOld = Gia_ManObjNum(pGia);//, Count = 0;
+ int nNodesOld = Gia_ManObjNum(pGia);
int k, Pivot;
assert( pPars->nLutSize <= 6 );
- //Sbd_ManMergeTest( p );
+ // prepare references
+ Gia_ManForEachObj( p->pGia, pObj, Pivot )
+ Sbd_StoRefObj( p->pSto, Pivot, -1 );
//return NULL;
+ vPath = (pPars->fUsePath && Gia_ManHasMapping(pGia)) ? Sbc_ManCriticalPath(pGia) : NULL;
if ( pGia->pManTime != NULL && Tim_ManBoxNum((Tim_Man_t*)pGia->pManTime) )
{
Vec_Int_t * vNodes = Gia_ManOrderWithBoxes( pGia );
Tim_Man_t * pTimOld = (Tim_Man_t *)pGia->pManTime;
pGia->pManTime = Tim_ManDup( pTimOld, 1 );
+ //Tim_ManPrint( pGia->pManTime );
Tim_ManIncrementTravId( (Tim_Man_t *)pGia->pManTime );
Gia_ManForEachObjVec( vNodes, pGia, pObj, k )
{
Pivot = Gia_ObjId( pGia, pObj );
if ( Pivot >= nNodesOld )
- continue;
+ break;
if ( Gia_ObjIsAnd(pObj) )
- Sbd_NtkPerformOne( p, Pivot );
+ {
+ abctime clk = Abc_Clock();
+ int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
+ Sbd_StoSaveBestDelayCut( p->pSto, Pivot, Sbd_ObjCut(p, Pivot) );
+ p->timeCut += Abc_Clock() - clk;
+ Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
+ if ( Delay > 1 && (!vPath || Vec_BitEntry(vPath, Pivot)) )
+ Sbd_NtkPerformOne( p, Pivot );
+ }
else if ( Gia_ObjIsCi(pObj) )
{
int arrTime = Tim_ManGetCiArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj) );
Vec_IntWriteEntry( p->vLutLevs, Pivot, arrTime );
+ Sbd_StoComputeCutsCi( p->pSto, Pivot, arrTime, arrTime );
}
else if ( Gia_ObjIsCo(pObj) )
{
int arrTime = Vec_IntEntry( p->vLutLevs, Gia_ObjFaninId0(pObj, Pivot) );
Tim_ManSetCoArrival( (Tim_Man_t*)pGia->pManTime, Gia_ObjCioId(pObj), arrTime );
}
- else if ( !Gia_ObjIsConst0(pObj) )
- assert( 0 );
+ else if ( Gia_ObjIsConst0(pObj) )
+ Sbd_StoComputeCutsConst0( p->pSto, 0 );
+ else assert( 0 );
}
- //Tim_ManPrint( pGia->pManTime );
Tim_ManStop( (Tim_Man_t *)pGia->pManTime );
pGia->pManTime = pTimOld;
Vec_IntFree( vNodes );
}
else
{
- Gia_ManForEachAndId( pGia, Pivot )
- if ( Pivot < nNodesOld )
- Sbd_NtkPerformOne( p, Pivot );
+ Sbd_StoComputeCutsConst0( p->pSto, 0 );
+ Gia_ManForEachObj( pGia, pObj, Pivot )
+ {
+ if ( Pivot >= nNodesOld )
+ break;
+ if ( Gia_ObjIsCi(pObj) )
+ Sbd_StoComputeCutsCi( p->pSto, Pivot, 0, 0 );
+ else if ( Gia_ObjIsAnd(pObj) )
+ {
+ abctime clk = Abc_Clock();
+ int Delay = Sbd_StoComputeCutsNode( p->pSto, Pivot );
+ Sbd_StoSaveBestDelayCut( p->pSto, Pivot, Sbd_ObjCut(p, Pivot) );
+ p->timeCut += Abc_Clock() - clk;
+ Vec_IntWriteEntry( p->vLutLevs, Pivot, Delay );
+ if ( Delay > 1 && (!vPath || Vec_BitEntry(vPath, Pivot)) )
+ Sbd_NtkPerformOne( p, Pivot );
+ }
+ //if ( nNodesOld != Gia_ManObjNum(pGia) )
+ // break;
+ }
}
- printf( "Found %d constants and %d replacements with delay %d. ", p->nConsts, p->nChanges, Sbd_ManDelay(p) );
+ Vec_BitFreeP( &vPath );
p->timeTotal = Abc_Clock() - p->timeTotal;
- Abc_PrintTime( 1, "Time", p->timeTotal );
- pNew = Sbd_ManDerive( pGia, p->vMirrors );
+ if ( p->pPars->fVerbose )
+ {
+ printf( "K = %d. S = %d. N = %d. P = %d. ",
+ p->pPars->nLutSize, p->pPars->nLutNum, p->pPars->nCutSize, p->pPars->nCutNum );
+ printf( "Try = %d. Use = %d. C = %d. 1 = %d. 2 = %d. 3a = %d. 3b = %d. Lev = %d. ",
+ p->nTried, p->nUsed, p->nLuts[0], p->nLuts[1], p->nLuts[2], p->nLuts[3], p->nLuts[4], Sbd_ManDelay(p) );
+ Abc_PrintTime( 1, "Time", p->timeTotal );
+ }
+ pNew = Sbd_ManDerive( p, pGia, p->vMirrors );
// print runtime statistics
- p->timeOther = p->timeTotal - p->timeWin - p->timeCnf - p->timeSat - p->timeCov - p->timeEnu;
- if ( 0 )
+ p->timeOther = p->timeTotal - p->timeWin - p->timeCut - p->timeCov - p->timeCnf - p->timeSat - p->timeQbf;
+ if ( p->pPars->fVerbose )
{
ABC_PRTP( "Win", p->timeWin , p->timeTotal );
+ ABC_PRTP( "Cut", p->timeCut , p->timeTotal );
+ ABC_PRTP( "Cov", p->timeCov , p->timeTotal );
ABC_PRTP( "Cnf", p->timeCnf , p->timeTotal );
ABC_PRTP( "Sat", p->timeSat , p->timeTotal );
- ABC_PRTP( "Cov", p->timeCov , p->timeTotal );
- ABC_PRTP( "Enu", p->timeEnu , p->timeTotal );
+ ABC_PRTP( "Qbf", p->timeQbf , p->timeTotal );
ABC_PRTP( "Oth", p->timeOther, p->timeTotal );
ABC_PRTP( "ALL", p->timeTotal, p->timeTotal );
}
diff --git a/src/opt/sbd/sbdCut.c b/src/opt/sbd/sbdCut.c
new file mode 100644
index 00000000..59505c98
--- /dev/null
+++ b/src/opt/sbd/sbdCut.c
@@ -0,0 +1,872 @@
+/**CFile****************************************************************
+
+ FileName [sbdCut.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis [Cut computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sbdCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define SBD_MAX_CUTSIZE 10
+#define SBD_MAX_CUTNUM 501
+#define SBD_MAX_TT_WORDS ((SBD_MAX_CUTSIZE > 6) ? 1 << (SBD_MAX_CUTSIZE-6) : 1)
+
+#define SBD_CUT_NO_LEAF 0xF
+
+typedef struct Sbd_Cut_t_ Sbd_Cut_t;
+struct Sbd_Cut_t_
+{
+ word Sign; // signature
+ int iFunc; // functionality
+ int Cost; // cut cost
+ int CostLev; // cut cost
+ unsigned nTreeLeaves : 9; // tree leaves
+ unsigned nSlowLeaves : 9; // slow leaves
+ unsigned nTopLeaves : 10; // top leaves
+ unsigned nLeaves : 4; // leaf count
+ int pLeaves[SBD_MAX_CUTSIZE]; // leaves
+};
+
+struct Sbd_Sto_t_
+{
+ int nLutSize;
+ int nCutSize;
+ int nCutNum;
+ int fCutMin;
+ int fVerbose;
+ Gia_Man_t * pGia; // user's AIG manager (will be modified by adding nodes)
+ Vec_Int_t * vMirrors; // mirrors for each node
+ Vec_Int_t * vDelays; // delays for each node
+ Vec_Int_t * vLevels; // levels for each node
+ Vec_Int_t * vRefs; // refs for each node
+ Vec_Wec_t * vCuts; // cuts for each node
+ Vec_Mem_t * vTtMem; // truth tables
+ Sbd_Cut_t pCuts[3][SBD_MAX_CUTNUM]; // temporary cuts
+ Sbd_Cut_t * ppCuts[SBD_MAX_CUTNUM]; // temporary cut pointers
+ int nCutsR; // the number of cuts
+ int Pivot; // current object
+ int iCutBest; // best-delay cut
+ int nCutsSpec; // special cuts
+ int nCutsOver; // overflow cuts
+ int DelayMin; // minimum delay
+ double CutCount[4]; // cut counters
+ abctime clkStart; // starting time
+};
+
+static inline word * Sbd_CutTruth( Sbd_Sto_t * p, Sbd_Cut_t * pCut ) { return Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut->iFunc)); }
+
+#define Sbd_ForEachCut( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 2 )
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Check correctness of cuts.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline word Sbd_CutGetSign( Sbd_Cut_t * pCut )
+{
+ word Sign = 0; int i;
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ Sign |= ((word)1) << (pCut->pLeaves[i] & 0x3F);
+ return Sign;
+}
+static inline int Sbd_CutCheck( Sbd_Cut_t * pBase, Sbd_Cut_t * pCut ) // check if pCut is contained in pBase
+{
+ int nSizeB = pBase->nLeaves;
+ int nSizeC = pCut->nLeaves;
+ int i, * pB = pBase->pLeaves;
+ int k, * pC = pCut->pLeaves;
+ for ( i = 0; i < nSizeC; i++ )
+ {
+ for ( k = 0; k < nSizeB; k++ )
+ if ( pC[i] == pB[k] )
+ break;
+ if ( k == nSizeB )
+ return 0;
+ }
+ return 1;
+}
+static inline int Sbd_CutSetCheckArray( Sbd_Cut_t ** ppCuts, int nCuts )
+{
+ Sbd_Cut_t * pCut0, * pCut1;
+ int i, k, m, n, Value;
+ assert( nCuts > 0 );
+ for ( i = 0; i < nCuts; i++ )
+ {
+ pCut0 = ppCuts[i];
+ assert( pCut0->nLeaves <= SBD_MAX_CUTSIZE );
+ assert( pCut0->Sign == Sbd_CutGetSign(pCut0) );
+ // check duplicates
+ for ( m = 0; m < (int)pCut0->nLeaves; m++ )
+ for ( n = m + 1; n < (int)pCut0->nLeaves; n++ )
+ assert( pCut0->pLeaves[m] < pCut0->pLeaves[n] );
+ // check pairs
+ for ( k = 0; k < nCuts; k++ )
+ {
+ pCut1 = ppCuts[k];
+ if ( pCut0 == pCut1 )
+ continue;
+ // check containments
+ Value = Sbd_CutCheck( pCut0, pCut1 );
+ assert( Value == 0 );
+ }
+ }
+ return 1;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Sbd_CutMergeOrder( Sbd_Cut_t * pCut0, Sbd_Cut_t * pCut1, Sbd_Cut_t * pCut, int nCutSize )
+{
+ int nSize0 = pCut0->nLeaves;
+ int nSize1 = pCut1->nLeaves;
+ int i, * pC0 = pCut0->pLeaves;
+ int k, * pC1 = pCut1->pLeaves;
+ int c, * pC = pCut->pLeaves;
+ // the case of the largest cut sizes
+ if ( nSize0 == nCutSize && nSize1 == nCutSize )
+ {
+ for ( i = 0; i < nSize0; i++ )
+ {
+ if ( pC0[i] != pC1[i] ) return 0;
+ pC[i] = pC0[i];
+ }
+ pCut->nLeaves = nCutSize;
+ pCut->iFunc = -1;
+ pCut->Sign = pCut0->Sign | pCut1->Sign;
+ return 1;
+ }
+ // compare two cuts with different numbers
+ i = k = c = 0;
+ if ( nSize0 == 0 ) goto FlushCut1;
+ if ( nSize1 == 0 ) goto FlushCut0;
+ while ( 1 )
+ {
+ if ( c == nCutSize ) return 0;
+ if ( pC0[i] < pC1[k] )
+ {
+ pC[c++] = pC0[i++];
+ if ( i >= nSize0 ) goto FlushCut1;
+ }
+ else if ( pC0[i] > pC1[k] )
+ {
+ pC[c++] = pC1[k++];
+ if ( k >= nSize1 ) goto FlushCut0;
+ }
+ else
+ {
+ pC[c++] = pC0[i++]; k++;
+ if ( i >= nSize0 ) goto FlushCut1;
+ if ( k >= nSize1 ) goto FlushCut0;
+ }
+ }
+
+FlushCut0:
+ if ( c + nSize0 > nCutSize + i ) return 0;
+ while ( i < nSize0 )
+ pC[c++] = pC0[i++];
+ pCut->nLeaves = c;
+ pCut->iFunc = -1;
+ pCut->Sign = pCut0->Sign | pCut1->Sign;
+ return 1;
+
+FlushCut1:
+ if ( c + nSize1 > nCutSize + k ) return 0;
+ while ( k < nSize1 )
+ pC[c++] = pC1[k++];
+ pCut->nLeaves = c;
+ pCut->iFunc = -1;
+ pCut->Sign = pCut0->Sign | pCut1->Sign;
+ return 1;
+}
+static inline int Sbd_CutMergeOrder2( Sbd_Cut_t * pCut0, Sbd_Cut_t * pCut1, Sbd_Cut_t * pCut, int nCutSize )
+{
+ int x0, i0 = 0, nSize0 = pCut0->nLeaves, * pC0 = pCut0->pLeaves;
+ int x1, i1 = 0, nSize1 = pCut1->nLeaves, * pC1 = pCut1->pLeaves;
+ int xMin, c = 0, * pC = pCut->pLeaves;
+ while ( 1 )
+ {
+ x0 = (i0 == nSize0) ? ABC_INFINITY : pC0[i0];
+ x1 = (i1 == nSize1) ? ABC_INFINITY : pC1[i1];
+ xMin = Abc_MinInt(x0, x1);
+ if ( xMin == ABC_INFINITY ) break;
+ if ( c == nCutSize ) return 0;
+ pC[c++] = xMin;
+ if (x0 == xMin) i0++;
+ if (x1 == xMin) i1++;
+ }
+ pCut->nLeaves = c;
+ pCut->iFunc = -1;
+ pCut->Sign = pCut0->Sign | pCut1->Sign;
+ return 1;
+}
+static inline int Sbd_CutSetCutIsContainedOrder( Sbd_Cut_t * pBase, Sbd_Cut_t * pCut ) // check if pCut is contained in pBase
+{
+ int i, nSizeB = pBase->nLeaves;
+ int k, nSizeC = pCut->nLeaves;
+ if ( nSizeB == nSizeC )
+ {
+ for ( i = 0; i < nSizeB; i++ )
+ if ( pBase->pLeaves[i] != pCut->pLeaves[i] )
+ return 0;
+ return 1;
+ }
+ assert( nSizeB > nSizeC );
+ if ( nSizeC == 0 )
+ return 1;
+ for ( i = k = 0; i < nSizeB; i++ )
+ {
+ if ( pBase->pLeaves[i] > pCut->pLeaves[k] )
+ return 0;
+ if ( pBase->pLeaves[i] == pCut->pLeaves[k] )
+ {
+ if ( ++k == nSizeC )
+ return 1;
+ }
+ }
+ return 0;
+}
+static inline int Sbd_CutSetLastCutIsContained( Sbd_Cut_t ** pCuts, int nCuts )
+{
+ int i;
+ for ( i = 0; i < nCuts; i++ )
+ if ( pCuts[i]->nLeaves <= pCuts[nCuts]->nLeaves && (pCuts[i]->Sign & pCuts[nCuts]->Sign) == pCuts[i]->Sign && Sbd_CutSetCutIsContainedOrder(pCuts[nCuts], pCuts[i]) )
+ return 1;
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Sbd_CutCompare( Sbd_Cut_t * pCut0, Sbd_Cut_t * pCut1 )
+{
+ if ( pCut0->nLeaves <= 4 && pCut1->nLeaves <= 4 )
+ {
+ if ( pCut0->nLeaves < pCut1->nLeaves ) return -1;
+ if ( pCut0->nLeaves > pCut1->nLeaves ) return 1;
+ if ( pCut0->Cost < pCut1->Cost ) return -1;
+ if ( pCut0->Cost > pCut1->Cost ) return 1;
+ if ( pCut0->CostLev < pCut1->CostLev ) return -1;
+ if ( pCut0->CostLev > pCut1->CostLev ) return 1;
+ }
+ else if ( pCut0->nLeaves <= 4 )
+ return -1;
+ else if ( pCut1->nLeaves <= 4 )
+ return 1;
+ else
+ {
+ if ( pCut0->nTreeLeaves < pCut1->nTreeLeaves ) return -1;
+ if ( pCut0->nTreeLeaves > pCut1->nTreeLeaves ) return 1;
+ if ( pCut0->Cost < pCut1->Cost ) return -1;
+ if ( pCut0->Cost > pCut1->Cost ) return 1;
+ if ( pCut0->CostLev < pCut1->CostLev ) return -1;
+ if ( pCut0->CostLev > pCut1->CostLev ) return 1;
+ if ( pCut0->nLeaves < pCut1->nLeaves ) return -1;
+ if ( pCut0->nLeaves > pCut1->nLeaves ) return 1;
+ }
+ return 0;
+}
+static inline int Sbd_CutCompare2( Sbd_Cut_t * pCut0, Sbd_Cut_t * pCut1 )
+{
+ assert( pCut0->nLeaves > 4 && pCut1->nLeaves > 4 );
+ if ( pCut0->nSlowLeaves < pCut1->nSlowLeaves ) return -1;
+ if ( pCut0->nSlowLeaves > pCut1->nSlowLeaves ) return 1;
+ if ( pCut0->nTreeLeaves < pCut1->nTreeLeaves ) return -1;
+ if ( pCut0->nTreeLeaves > pCut1->nTreeLeaves ) return 1;
+ if ( pCut0->Cost < pCut1->Cost ) return -1;
+ if ( pCut0->Cost > pCut1->Cost ) return 1;
+ if ( pCut0->CostLev < pCut1->CostLev ) return -1;
+ if ( pCut0->CostLev > pCut1->CostLev ) return 1;
+ if ( pCut0->nLeaves < pCut1->nLeaves ) return -1;
+ if ( pCut0->nLeaves > pCut1->nLeaves ) return 1;
+ return 0;
+}
+
+static inline int Sbd_CutSetLastCutContains( Sbd_Cut_t ** pCuts, int nCuts )
+{
+ int i, k, fChanges = 0;
+ for ( i = 0; i < nCuts; i++ )
+ if ( pCuts[nCuts]->nLeaves < pCuts[i]->nLeaves && (pCuts[nCuts]->Sign & pCuts[i]->Sign) == pCuts[nCuts]->Sign && Sbd_CutSetCutIsContainedOrder(pCuts[i], pCuts[nCuts]) )
+ pCuts[i]->nLeaves = SBD_CUT_NO_LEAF, fChanges = 1;
+ if ( !fChanges )
+ return nCuts;
+ for ( i = k = 0; i <= nCuts; i++ )
+ {
+ if ( pCuts[i]->nLeaves == SBD_CUT_NO_LEAF )
+ continue;
+ if ( k < i )
+ ABC_SWAP( Sbd_Cut_t *, pCuts[k], pCuts[i] );
+ k++;
+ }
+ return k - 1;
+}
+static inline void Sbd_CutSetSortByCost( Sbd_Cut_t ** pCuts, int nCuts )
+{
+ int i;
+ for ( i = nCuts; i > 0; i-- )
+ {
+ if ( Sbd_CutCompare(pCuts[i - 1], pCuts[i]) < 0 )//!= 1 )
+ return;
+ ABC_SWAP( Sbd_Cut_t *, pCuts[i - 1], pCuts[i] );
+ }
+}
+static inline int Sbd_CutSetAddCut( Sbd_Cut_t ** pCuts, int nCuts, int nCutNum )
+{
+ if ( nCuts == 0 )
+ return 1;
+ nCuts = Sbd_CutSetLastCutContains(pCuts, nCuts);
+ assert( nCuts >= 0 );
+ Sbd_CutSetSortByCost( pCuts, nCuts );
+ // add new cut if there is room
+ return Abc_MinInt( nCuts + 1, nCutNum - 1 );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Sbd_CutComputeTruth6( Sbd_Sto_t * p, Sbd_Cut_t * pCut0, Sbd_Cut_t * pCut1, int fCompl0, int fCompl1, Sbd_Cut_t * pCutR, int fIsXor )
+{
+ int nOldSupp = pCutR->nLeaves, truthId, fCompl; word t;
+ word t0 = *Sbd_CutTruth(p, pCut0);
+ word t1 = *Sbd_CutTruth(p, pCut1);
+ if ( Abc_LitIsCompl(pCut0->iFunc) ^ fCompl0 ) t0 = ~t0;
+ if ( Abc_LitIsCompl(pCut1->iFunc) ^ fCompl1 ) t1 = ~t1;
+ t0 = Abc_Tt6Expand( t0, pCut0->pLeaves, pCut0->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
+ t1 = Abc_Tt6Expand( t1, pCut1->pLeaves, pCut1->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
+ t = fIsXor ? t0 ^ t1 : t0 & t1;
+ if ( (fCompl = (int)(t & 1)) ) t = ~t;
+ pCutR->nLeaves = Abc_Tt6MinBase( &t, pCutR->pLeaves, pCutR->nLeaves );
+ assert( (int)(t & 1) == 0 );
+ truthId = Vec_MemHashInsert(p->vTtMem, &t);
+ pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
+ assert( (int)pCutR->nLeaves <= nOldSupp );
+ return (int)pCutR->nLeaves < nOldSupp;
+}
+static inline int Sbd_CutComputeTruth( Sbd_Sto_t * p, Sbd_Cut_t * pCut0, Sbd_Cut_t * pCut1, int fCompl0, int fCompl1, Sbd_Cut_t * pCutR, int fIsXor )
+{
+ if ( p->nCutSize <= 6 )
+ return Sbd_CutComputeTruth6( p, pCut0, pCut1, fCompl0, fCompl1, pCutR, fIsXor );
+ {
+ word uTruth[SBD_MAX_TT_WORDS], uTruth0[SBD_MAX_TT_WORDS], uTruth1[SBD_MAX_TT_WORDS];
+ int nOldSupp = pCutR->nLeaves, truthId;
+ int nCutSize = p->nCutSize, fCompl;
+ int nWords = Abc_Truth6WordNum(nCutSize);
+ word * pTruth0 = Sbd_CutTruth(p, pCut0);
+ word * pTruth1 = Sbd_CutTruth(p, pCut1);
+ Abc_TtCopy( uTruth0, pTruth0, nWords, Abc_LitIsCompl(pCut0->iFunc) ^ fCompl0 );
+ Abc_TtCopy( uTruth1, pTruth1, nWords, Abc_LitIsCompl(pCut1->iFunc) ^ fCompl1 );
+ Abc_TtExpand( uTruth0, nCutSize, pCut0->pLeaves, pCut0->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
+ Abc_TtExpand( uTruth1, nCutSize, pCut1->pLeaves, pCut1->nLeaves, pCutR->pLeaves, pCutR->nLeaves );
+ if ( fIsXor )
+ Abc_TtXor( uTruth, uTruth0, uTruth1, nWords, (fCompl = (int)((uTruth0[0] ^ uTruth1[0]) & 1)) );
+ else
+ Abc_TtAnd( uTruth, uTruth0, uTruth1, nWords, (fCompl = (int)((uTruth0[0] & uTruth1[0]) & 1)) );
+ pCutR->nLeaves = Abc_TtMinBase( uTruth, pCutR->pLeaves, pCutR->nLeaves, nCutSize );
+ assert( (uTruth[0] & 1) == 0 );
+//Kit_DsdPrintFromTruth( uTruth, pCutR->nLeaves ), printf("\n" ), printf("\n" );
+ truthId = Vec_MemHashInsert(p->vTtMem, uTruth);
+ pCutR->iFunc = Abc_Var2Lit( truthId, fCompl );
+ assert( (int)pCutR->nLeaves <= nOldSupp );
+ return (int)pCutR->nLeaves < nOldSupp;
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Sbd_CutCountBits( word i )
+{
+ i = i - ((i >> 1) & 0x5555555555555555);
+ i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333);
+ i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F);
+ return (i*(0x0101010101010101))>>56;
+}
+static inline int Sbd_CutCost( Sbd_Sto_t * p, Sbd_Cut_t * pCut )
+{
+ int i, Cost = 0;
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ Cost += Vec_IntEntry( p->vDelays, pCut->pLeaves[i] );
+ return Cost;
+}
+static inline int Sbd_CutCostLev( Sbd_Sto_t * p, Sbd_Cut_t * pCut )
+{
+ int i, Cost = 0;
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ Cost += Vec_IntEntry( p->vLevels, pCut->pLeaves[i] );
+ return Cost;
+}
+static inline int Sbd_CutTreeLeaves( Sbd_Sto_t * p, Sbd_Cut_t * pCut )
+{
+ int i, Cost = 0;
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ Cost += Vec_IntEntry( p->vRefs, pCut->pLeaves[i] ) == 1;
+ return Cost;
+}
+static inline int Sbd_CutSlowLeaves( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
+{
+ int i, Count = 0, Delay = Vec_IntEntry(p->vDelays, iObj);
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ Count += (Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay >= -1);
+ return Count;
+}
+static inline int Sbd_CutTopLeaves( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
+{
+ int i, Count = 0, Delay = Vec_IntEntry(p->vDelays, iObj);
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ Count += (Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay == -2);
+ return Count;
+}
+static inline void Sbd_CutAddUnit( Sbd_Sto_t * p, int iObj )
+{
+ Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
+ if ( Vec_IntSize(vThis) == 0 )
+ Vec_IntPush( vThis, 1 );
+ else
+ Vec_IntAddToEntry( vThis, 0, 1 );
+ Vec_IntPush( vThis, 1 );
+ Vec_IntPush( vThis, iObj );
+ Vec_IntPush( vThis, 2 );
+}
+static inline void Sbd_CutAddZero( Sbd_Sto_t * p, int iObj )
+{
+ Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
+ assert( Vec_IntSize(vThis) == 0 );
+ Vec_IntPush( vThis, 1 );
+ Vec_IntPush( vThis, 0 );
+ Vec_IntPush( vThis, 0 );
+}
+static inline int Sbd_StoPrepareSet( Sbd_Sto_t * p, int iObj, int Index )
+{
+ Vec_Int_t * vThis = Vec_WecEntry( p->vCuts, iObj );
+ int i, v, * pCut, * pList = Vec_IntArray( vThis );
+ Sbd_ForEachCut( pList, pCut, i )
+ {
+ Sbd_Cut_t * pCutTemp = &p->pCuts[Index][i];
+ pCutTemp->nLeaves = pCut[0];
+ for ( v = 1; v <= pCut[0]; v++ )
+ pCutTemp->pLeaves[v-1] = pCut[v];
+ pCutTemp->iFunc = pCut[pCut[0]+1];
+ pCutTemp->Sign = Sbd_CutGetSign( pCutTemp );
+ pCutTemp->Cost = Sbd_CutCost( p, pCutTemp );
+ pCutTemp->CostLev = Sbd_CutCostLev( p, pCutTemp );
+ pCutTemp->nTreeLeaves = Sbd_CutTreeLeaves( p, pCutTemp );
+ pCutTemp->nSlowLeaves = Sbd_CutSlowLeaves( p, iObj, pCutTemp );
+ pCutTemp->nTopLeaves = Sbd_CutTopLeaves( p, iObj, pCutTemp );
+ }
+ return pList[0];
+}
+static inline void Sbd_StoInitResult( Sbd_Sto_t * p )
+{
+ int i;
+ for ( i = 0; i < SBD_MAX_CUTNUM; i++ )
+ p->ppCuts[i] = &p->pCuts[2][i];
+}
+static inline void Sbd_StoStoreResult( Sbd_Sto_t * p, int iObj, Sbd_Cut_t ** pCuts, int nCuts )
+{
+ int i, v;
+ Vec_Int_t * vList = Vec_WecEntry( p->vCuts, iObj );
+ Vec_IntPush( vList, nCuts );
+ for ( i = 0; i < nCuts; i++ )
+ {
+ Vec_IntPush( vList, pCuts[i]->nLeaves );
+ for ( v = 0; v < (int)pCuts[i]->nLeaves; v++ )
+ Vec_IntPush( vList, pCuts[i]->pLeaves[v] );
+ Vec_IntPush( vList, pCuts[i]->iFunc );
+ }
+}
+static inline void Sbd_StoComputeDelay( Sbd_Sto_t * p, int iObj, Sbd_Cut_t ** pCuts, int nCuts )
+{
+ int i, v, Delay, DelayMin = ABC_INFINITY;
+ assert( nCuts > 0 );
+ p->iCutBest = -1;
+ for ( i = 0; i < nCuts; i++ )
+ {
+ if ( (int)pCuts[i]->nLeaves > p->nLutSize )
+ continue;
+ Delay = 0;
+ for ( v = 0; v < (int)pCuts[i]->nLeaves; v++ )
+ Delay = Abc_MaxInt( Delay, Vec_IntEntry(p->vDelays, pCuts[i]->pLeaves[v]) );
+ //DelayMin = Abc_MinInt( DelayMin, Delay );
+ if ( DelayMin > Delay )
+ {
+ DelayMin = Delay;
+ p->iCutBest = i;
+ }
+ else if ( DelayMin == Delay && p->iCutBest >= 0 && pCuts[p->iCutBest]->nLeaves > pCuts[i]->nLeaves )
+ p->iCutBest = i;
+ }
+ assert( p->iCutBest >= 0 );
+ assert( DelayMin < ABC_INFINITY );
+ DelayMin = (nCuts > 1 || pCuts[0]->nLeaves > 1) ? DelayMin + 1 : DelayMin;
+ Vec_IntWriteEntry( p->vDelays, iObj, DelayMin );
+ p->DelayMin = Abc_MaxInt( p->DelayMin, DelayMin );
+}
+static inline void Sbd_StoComputeSpec( Sbd_Sto_t * p, int iObj, Sbd_Cut_t ** pCuts, int nCuts )
+{
+ int i;
+ for ( i = 0; i < nCuts; i++ )
+ {
+ pCuts[i]->nTopLeaves = Sbd_CutTopLeaves( p, iObj, pCuts[i] );
+ pCuts[i]->nSlowLeaves = Sbd_CutSlowLeaves( p, iObj, pCuts[i] );
+ p->nCutsSpec += (pCuts[i]->nSlowLeaves == 0);
+ }
+}
+static inline void Sbd_CutPrint( Sbd_Sto_t * p, int iObj, Sbd_Cut_t * pCut )
+{
+ int i, nDigits = Abc_Base10Log(Gia_ManObjNum(p->pGia));
+ int Delay = Vec_IntEntry(p->vDelays, iObj);
+ if ( pCut == NULL ) { printf( "No cut.\n" ); return; }
+ printf( "%d {", pCut->nLeaves );
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ printf( " %*d", nDigits, pCut->pLeaves[i] );
+ for ( ; i < (int)p->nCutSize; i++ )
+ printf( " %*s", nDigits, " " );
+ printf( " } Cost = %3d CostL = %3d Tree = %d Slow = %d Top = %d ",
+ pCut->Cost, pCut->CostLev, pCut->nTreeLeaves, pCut->nSlowLeaves, pCut->nTopLeaves );
+ printf( "%c ", pCut->nSlowLeaves == 0 ? '*' : ' ' );
+ for ( i = 0; i < (int)pCut->nLeaves; i++ )
+ printf( "%3d ", Vec_IntEntry(p->vDelays, pCut->pLeaves[i]) - Delay );
+ printf( "\n" );
+}
+void Sbd_StoMergeCuts( Sbd_Sto_t * p, int iObj )
+{
+ Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
+ int fIsXor = Gia_ObjIsXor(pObj);
+ int nCutSize = p->nCutSize;
+ int nCutNum = p->nCutNum;
+ int Lit0m = p->vMirrors ? Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) ) : -1;
+ int Lit1m = p->vMirrors ? Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) ) : -1;
+ int fComp0 = Gia_ObjFaninC0(pObj) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
+ int fComp1 = Gia_ObjFaninC1(pObj) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
+ int Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
+ int Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
+ int nCuts0 = Sbd_StoPrepareSet( p, Fan0, 0 );
+ int nCuts1 = Sbd_StoPrepareSet( p, Fan1, 1 );
+ int i, k, nCutsR = 0;
+ Sbd_Cut_t * pCut0, * pCut1, ** pCutsR = p->ppCuts;
+ assert( !Gia_ObjIsBuf(pObj) );
+ assert( !Gia_ObjIsMux(p->pGia, pObj) );
+ Sbd_StoInitResult( p );
+ p->CutCount[0] += nCuts0 * nCuts1;
+ for ( i = 0, pCut0 = p->pCuts[0]; i < nCuts0; i++, pCut0++ )
+ for ( k = 0, pCut1 = p->pCuts[1]; k < nCuts1; k++, pCut1++ )
+ {
+ if ( (int)(pCut0->nLeaves + pCut1->nLeaves) > nCutSize && Sbd_CutCountBits(pCut0->Sign | pCut1->Sign) > nCutSize )
+ continue;
+ p->CutCount[1]++;
+ if ( !Sbd_CutMergeOrder(pCut0, pCut1, pCutsR[nCutsR], nCutSize) )
+ continue;
+ if ( Sbd_CutSetLastCutIsContained(pCutsR, nCutsR) )
+ continue;
+ p->CutCount[2]++;
+ if ( p->fCutMin && Sbd_CutComputeTruth(p, pCut0, pCut1, fComp0, fComp1, pCutsR[nCutsR], fIsXor) )
+ pCutsR[nCutsR]->Sign = Sbd_CutGetSign(pCutsR[nCutsR]);
+ pCutsR[nCutsR]->Cost = Sbd_CutCost( p, pCutsR[nCutsR] );
+ pCutsR[nCutsR]->CostLev = Sbd_CutCostLev( p, pCutsR[nCutsR] );
+ pCutsR[nCutsR]->nTreeLeaves = Sbd_CutTreeLeaves( p, pCutsR[nCutsR] );
+ nCutsR = Sbd_CutSetAddCut( pCutsR, nCutsR, nCutNum );
+ }
+ Sbd_StoComputeDelay( p, iObj, pCutsR, nCutsR );
+ Sbd_StoComputeSpec( p, iObj, pCutsR, nCutsR );
+ p->CutCount[3] += nCutsR;
+ p->nCutsOver += nCutsR == nCutNum-1;
+ p->nCutsR = nCutsR;
+ p->Pivot = iObj;
+ // debug printout
+ if ( 0 )
+ {
+ printf( "*** Obj = %4d Delay = %4d NumCuts = %4d\n", iObj, Vec_IntEntry(p->vDelays, iObj), nCutsR );
+ for ( i = 0; i < nCutsR; i++ )
+ if ( (int)pCutsR[i]->nLeaves <= p->nLutSize || pCutsR[i]->nSlowLeaves < 2 )
+ Sbd_CutPrint( p, iObj, pCutsR[i] );
+ printf( "\n" );
+ }
+ // verify
+ assert( nCutsR > 0 && nCutsR < nCutNum );
+ assert( Sbd_CutSetCheckArray(pCutsR, nCutsR) );
+ // store the cutset
+ Sbd_StoStoreResult( p, iObj, pCutsR, nCutsR );
+ if ( nCutsR > 1 || pCutsR[0]->nLeaves > 1 )
+ Sbd_CutAddUnit( p, iObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Incremental cut computation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sbd_Sto_t * Sbd_StoAlloc( Gia_Man_t * pGia, Vec_Int_t * vMirrors, int nLutSize, int nCutSize, int nCutNum, int fCutMin, int fVerbose )
+{
+ Sbd_Sto_t * p;
+ assert( nLutSize <= nCutSize );
+ assert( nCutSize < SBD_CUT_NO_LEAF );
+ assert( nCutSize > 1 && nCutSize <= SBD_MAX_CUTSIZE );
+ assert( nCutNum > 1 && nCutNum < SBD_MAX_CUTNUM );
+ p = ABC_CALLOC( Sbd_Sto_t, 1 );
+ p->clkStart = Abc_Clock();
+ p->nLutSize = nLutSize;
+ p->nCutSize = nCutSize;
+ p->nCutNum = nCutNum;
+ p->fCutMin = fCutMin;
+ p->fVerbose = fVerbose;
+ p->pGia = pGia;
+ p->vMirrors = vMirrors;
+ p->vDelays = Vec_IntStart( Gia_ManObjNum(pGia) );
+ p->vLevels = Vec_IntStart( Gia_ManObjNum(pGia) );
+ p->vRefs = Vec_IntAlloc( Gia_ManObjNum(pGia) );
+ p->vCuts = Vec_WecStart( Gia_ManObjNum(pGia) );
+ p->vTtMem = fCutMin ? Vec_MemAllocForTT( nCutSize, 0 ) : NULL;
+ return p;
+}
+void Sbd_StoFree( Sbd_Sto_t * p )
+{
+ Vec_IntFree( p->vDelays );
+ Vec_IntFree( p->vLevels );
+ Vec_IntFree( p->vRefs );
+ Vec_WecFree( p->vCuts );
+ if ( p->fCutMin )
+ Vec_MemHashFree( p->vTtMem );
+ if ( p->fCutMin )
+ Vec_MemFree( p->vTtMem );
+ ABC_FREE( p );
+}
+void Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, int Level )
+{
+ if ( iObj < Vec_IntSize(p->vDelays) )
+ {
+ Vec_IntWriteEntry( p->vDelays, iObj, Delay );
+ Vec_IntWriteEntry( p->vLevels, iObj, Level );
+ }
+ else
+ {
+ assert( iObj == Vec_IntSize(p->vDelays) );
+ assert( iObj == Vec_IntSize(p->vLevels) );
+ assert( iObj == Vec_WecSize(p->vCuts) );
+ Vec_IntPush( p->vDelays, Delay );
+ Vec_IntPush( p->vLevels, Level );
+ Vec_WecPushLevel( p->vCuts );
+ }
+}
+void Sbd_StoComputeCutsConst0( Sbd_Sto_t * p, int iObj )
+{
+ Sbd_StoComputeCutsObj( p, iObj, 0, 0 );
+ Sbd_CutAddZero( p, iObj );
+}
+void Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level )
+{
+ Sbd_StoComputeCutsObj( p, iObj, Delay, Level );
+ Sbd_CutAddUnit( p, iObj );
+}
+int Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj )
+{
+ Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
+ int Lev0 = Vec_IntEntry( p->vLevels, Gia_ObjFaninId0(pObj, iObj) );
+ int Lev1 = Vec_IntEntry( p->vLevels, Gia_ObjFaninId1(pObj, iObj) );
+ Sbd_StoComputeCutsObj( p, iObj, -1, 1 + Abc_MaxInt(Lev0, Lev1) );
+ Sbd_StoMergeCuts( p, iObj );
+ return Vec_IntEntry( p->vDelays, iObj );
+}
+void Sbd_StoSaveBestDelayCut( Sbd_Sto_t * p, int iObj, int * pCut )
+{
+ Sbd_Cut_t * pCutBest = p->ppCuts[p->iCutBest]; int i;
+ assert( iObj == p->Pivot );
+ pCut[0] = pCutBest->nLeaves;
+ for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
+ pCut[i+1] = pCutBest->pLeaves[i];
+}
+int Sbd_StoObjRefs( Sbd_Sto_t * p, int iObj )
+{
+ return Vec_IntEntry(p->vRefs, iObj);
+}
+void Sbd_StoRefObj( Sbd_Sto_t * p, int iObj, int iMirror )
+{
+ Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj);
+ assert( iObj == Vec_IntSize(p->vRefs) );
+ assert( iMirror < iObj );
+ Vec_IntPush( p->vRefs, 0 );
+//printf( "Ref %d\n", iObj );
+ if ( iMirror > 0 )
+ {
+ Vec_IntWriteEntry( p->vRefs, iObj, Vec_IntEntry(p->vRefs, iMirror) );
+ Vec_IntWriteEntry( p->vRefs, iMirror, 1 );
+ }
+ if ( Gia_ObjIsAnd(pObj) )
+ {
+ int Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+ int Lit1m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) );
+ int Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
+ int Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
+ Vec_IntAddToEntry( p->vRefs, Fan0, 1 );
+ Vec_IntAddToEntry( p->vRefs, Fan1, 1 );
+ }
+ else if ( Gia_ObjIsCo(pObj) )
+ {
+ int Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+ assert( Lit0m == -1 );
+ Vec_IntAddToEntry( p->vRefs, Gia_ObjFaninId0(pObj, iObj), 1 );
+ }
+}
+void Sbd_StoDerefObj( Sbd_Sto_t * p, int iObj )
+{
+ Gia_Obj_t * pObj;
+ int Lit0m, Lit1m, Fan0, Fan1;
+ return;
+
+ pObj = Gia_ManObj(p->pGia, iObj);
+ if ( Vec_IntEntry(p->vRefs, iObj) == 0 )
+ printf( "Ref count mismatch at node %d\n", iObj );
+ assert( Vec_IntEntry(p->vRefs, iObj) > 0 );
+ Vec_IntAddToEntry( p->vRefs, iObj, -1 );
+ if ( Vec_IntEntry( p->vRefs, iObj ) > 0 )
+ return;
+ if ( Gia_ObjIsCi(pObj) )
+ return;
+//printf( "Deref %d\n", iObj );
+ assert( Gia_ObjIsAnd(pObj) );
+ Lit0m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+ Lit1m = Vec_IntEntry( p->vMirrors, Gia_ObjFaninId1(pObj, iObj) );
+ Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
+ Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
+ if ( Fan0 ) Sbd_StoDerefObj( p, Fan0 );
+ if ( Fan1 ) Sbd_StoDerefObj( p, Fan1 );
+}
+int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves )
+{
+ int fVerbose = 0;
+ Sbd_Cut_t * pCutBest = NULL; int i;
+ assert( p->Pivot == iObj );
+ if ( fVerbose && iObj % 1000 == 0 )
+ printf( "Node %6d : \n", iObj );
+ for ( i = 0; i < p->nCutsR; i++ )
+ {
+ if ( fVerbose && iObj % 1000 == 0 )
+ Sbd_CutPrint( p, iObj, p->ppCuts[i] );
+ if ( nSize && (int)p->ppCuts[i]->nLeaves != nSize )
+ continue;
+ if ( (int)p->ppCuts[i]->nLeaves > p->nLutSize &&
+ (int)p->ppCuts[i]->nSlowLeaves <= 1 &&
+ (int)p->ppCuts[i]->nTopLeaves <= p->nLutSize-1 &&
+ (pCutBest == NULL || Sbd_CutCompare2(pCutBest, p->ppCuts[i]) == 1) )
+ pCutBest = p->ppCuts[i];
+ }
+ if ( fVerbose && iObj % 1000 == 0 )
+ {
+ printf( "Best cut of size %d:\n", nSize );
+ Sbd_CutPrint( p, iObj, pCutBest );
+ }
+ if ( pCutBest == NULL )
+ return -1;
+ assert( pCutBest->nLeaves <= SBD_DIV_MAX );
+ for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
+ pLeaves[i] = pCutBest->pLeaves[i];
+ return pCutBest->nLeaves;
+}
+void Sbd_StoComputeCutsTest( Gia_Man_t * pGia )
+{
+ Sbd_Sto_t * p = Sbd_StoAlloc( pGia, NULL, 4, 8, 100, 1, 1 );
+ Gia_Obj_t * pObj;
+ int i, iObj;
+ // prepare references
+ Gia_ManForEachObj( p->pGia, pObj, iObj )
+ Sbd_StoRefObj( p, iObj, -1 );
+ // compute cuts
+ Sbd_StoComputeCutsConst0( p, 0 );
+ Gia_ManForEachCiId( p->pGia, iObj, i )
+ Sbd_StoComputeCutsCi( p, iObj, 0, 0 );
+ Gia_ManForEachAnd( p->pGia, pObj, iObj )
+ Sbd_StoComputeCutsNode( p, iObj );
+ if ( p->fVerbose )
+ {
+ printf( "Running cut computation with LutSize = %d CutSize = %d CutNum = %d:\n", p->nLutSize, p->nCutSize, p->nCutNum );
+ printf( "CutPair = %.0f ", p->CutCount[0] );
+ printf( "Merge = %.0f (%.2f %%) ", p->CutCount[1], 100.0*p->CutCount[1]/p->CutCount[0] );
+ printf( "Eval = %.0f (%.2f %%) ", p->CutCount[2], 100.0*p->CutCount[2]/p->CutCount[0] );
+ printf( "Cut = %.0f (%.2f %%) ", p->CutCount[3], 100.0*p->CutCount[3]/p->CutCount[0] );
+ printf( "Cut/Node = %.2f ", p->CutCount[3] / Gia_ManAndNum(p->pGia) );
+ printf( "\n" );
+ printf( "Spec = %4d ", p->nCutsSpec );
+ printf( "Over = %4d ", p->nCutsOver );
+ printf( "Lev = %4d ", p->DelayMin );
+ Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart );
+ }
+ Sbd_StoFree( p );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbdCut2.c b/src/opt/sbd/sbdCut2.c
new file mode 100644
index 00000000..b4a8be74
--- /dev/null
+++ b/src/opt/sbd/sbdCut2.c
@@ -0,0 +1,431 @@
+/**CFile****************************************************************
+
+ FileName [sbdCut2.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis [Cut computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sbdCut2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+#define SBD_MAX_CUTSIZE 10
+#define SBD_MAX_CUTNUM 501
+
+#define SBD_CUT_NO_LEAF 0xF
+
+typedef struct Sbd_Cut_t_ Sbd_Cut_t;
+struct Sbd_Cut_t_
+{
+ word Sign; // signature
+ int iFunc; // functionality
+ int Cost; // cut cost
+ int CostLev; // cut cost
+ unsigned nTreeLeaves : 9; // tree leaves
+ unsigned nSlowLeaves : 9; // slow leaves
+ unsigned nTopLeaves : 10; // top leaves
+ unsigned nLeaves : 4; // leaf count
+ int pLeaves[SBD_MAX_CUTSIZE]; // leaves
+};
+
+struct Sbd_Srv_t_
+{
+ int nLutSize;
+ int nCutSize;
+ int nCutNum;
+ int fVerbose;
+ Gia_Man_t * pGia; // user's AIG manager (will be modified by adding nodes)
+ Vec_Int_t * vMirrors; // mirrors for each node
+ Vec_Int_t * vLutLevs; // delays for each node
+ Vec_Int_t * vLevs; // levels for each node
+ Vec_Int_t * vRefs; // refs for each node
+ Sbd_Cut_t pCuts[SBD_MAX_CUTNUM]; // temporary cuts
+ Sbd_Cut_t * ppCuts[SBD_MAX_CUTNUM]; // temporary cut pointers
+ abctime clkStart; // starting time
+ Vec_Int_t * vCut0; // current cut
+ Vec_Int_t * vCut; // current cut
+ Vec_Int_t * vCutTop; // current cut
+ Vec_Int_t * vCutBot; // current cut
+};
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sbd_Srv_t * Sbd_ManCutServerStart( Gia_Man_t * pGia, Vec_Int_t * vMirrors,
+ Vec_Int_t * vLutLevs, Vec_Int_t * vLevs, Vec_Int_t * vRefs,
+ int nLutSize, int nCutSize, int nCutNum, int fVerbose )
+{
+ Sbd_Srv_t * p;
+ assert( nLutSize <= nCutSize );
+ assert( nCutSize < SBD_CUT_NO_LEAF );
+ assert( nCutSize > 1 && nCutSize <= SBD_MAX_CUTSIZE );
+ assert( nCutNum > 1 && nCutNum < SBD_MAX_CUTNUM );
+ p = ABC_CALLOC( Sbd_Srv_t, 1 );
+ p->clkStart = Abc_Clock();
+ p->nLutSize = nLutSize;
+ p->nCutSize = nCutSize;
+ p->nCutNum = nCutNum;
+ p->fVerbose = fVerbose;
+ p->pGia = pGia;
+ p->vMirrors = vMirrors;
+ p->vLutLevs = vLutLevs;
+ p->vLevs = vLevs;
+ p->vRefs = vRefs;
+ p->vCut0 = Vec_IntAlloc( 100 );
+ p->vCut = Vec_IntAlloc( 100 );
+ p->vCutTop = Vec_IntAlloc( 100 );
+ p->vCutBot = Vec_IntAlloc( 100 );
+ return p;
+}
+void Sbd_ManCutServerStop( Sbd_Srv_t * p )
+{
+ Vec_IntFree( p->vCut0 );
+ Vec_IntFree( p->vCut );
+ Vec_IntFree( p->vCutTop );
+ Vec_IntFree( p->vCutBot );
+ ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sbd_ManCutIsTopo_rec( Gia_Man_t * p, Vec_Int_t * vMirrors, int iObj )
+{
+ Gia_Obj_t * pObj;
+ int Ret0, Ret1;
+ if ( Vec_IntEntry(vMirrors, iObj) >= 0 )
+ iObj = Abc_Lit2Var(Vec_IntEntry(vMirrors, iObj));
+ if ( !iObj || Gia_ObjIsTravIdCurrentId(p, iObj) )
+ return 1;
+ Gia_ObjSetTravIdCurrentId(p, iObj);
+ pObj = Gia_ManObj( p, iObj );
+ if ( Gia_ObjIsCi(pObj) )
+ return 0;
+ assert( Gia_ObjIsAnd(pObj) );
+ Ret0 = Sbd_ManCutIsTopo_rec( p, vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+ Ret1 = Sbd_ManCutIsTopo_rec( p, vMirrors, Gia_ObjFaninId1(pObj, iObj) );
+ return Ret0 && Ret1;
+}
+int Sbd_ManCutIsTopo( Gia_Man_t * p, Vec_Int_t * vMirrors, Vec_Int_t * vCut, int iObj )
+{
+ int i, Entry, RetValue;
+ Gia_ManIncrementTravId( p );
+ Vec_IntForEachEntry( vCut, Entry, i )
+ Gia_ObjSetTravIdCurrentId( p, Entry );
+ RetValue = Sbd_ManCutIsTopo_rec( p, vMirrors, iObj );
+ if ( RetValue == 0 )
+ printf( "Cut of node %d is not tological\n", iObj );
+ assert( RetValue );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline int Sbd_ManCutExpandOne( Gia_Man_t * p, Vec_Int_t * vMirrors, Vec_Int_t * vLutLevs, Vec_Int_t * vCut, int iThis, int iObj )
+{
+ int Lit0m, Lit1m, Fan0, Fan1, iPlace0, iPlace1;
+ int LutLev = Vec_IntEntry( vLutLevs, iObj );
+ Gia_Obj_t * pObj = Gia_ManObj(p, iObj);
+ if ( Gia_ObjIsCi(pObj) )
+ return 0;
+ assert( Gia_ObjIsAnd(pObj) );
+ Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) );
+ Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) );
+ Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj);
+ Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj);
+ iPlace0 = Vec_IntFind( vCut, Fan0 );
+ iPlace1 = Vec_IntFind( vCut, Fan1 );
+ if ( iPlace0 == -1 && iPlace1 == -1 )
+ return 0;
+ if ( Vec_IntEntry(vLutLevs, Fan0) > LutLev || Vec_IntEntry(vLutLevs, Fan1) > LutLev )
+ return 0;
+ Vec_IntDrop( vCut, iThis );
+ if ( iPlace0 == -1 && Fan0 )
+ Vec_IntPushOrder( vCut, Fan0 );
+ if ( iPlace1 == -1 && Fan1 )
+ Vec_IntPushOrder( vCut, Fan1 );
+ return 1;
+}
+void Vec_IntIsOrdered( Vec_Int_t * vCut )
+{
+ int i, Prev, Entry;
+ Prev = Vec_IntEntry( vCut, 0 );
+ Vec_IntForEachEntryStart( vCut, Entry, i, 1 )
+ {
+ assert( Prev < Entry );
+ Prev = Entry;
+ }
+}
+void Sbd_ManCutExpand( Gia_Man_t * p, Vec_Int_t * vMirrors, Vec_Int_t * vLutLevs, Vec_Int_t * vCut )
+{
+ int i, Entry;
+ do
+ {
+ Vec_IntForEachEntry( vCut, Entry, i )
+ if ( Sbd_ManCutExpandOne( p, vMirrors, vLutLevs, vCut, i, Entry ) )
+ break;
+ }
+ while ( i < Vec_IntSize(vCut) );
+}
+void Sbd_ManCutReload( Vec_Int_t * vMirrors, Vec_Int_t * vLutLevs, int LevStop, Vec_Int_t * vCut, Vec_Int_t * vCutTop, Vec_Int_t * vCutBot )
+{
+ int i, Entry;
+ Vec_IntClear( vCutTop );
+ Vec_IntClear( vCutBot );
+ Vec_IntForEachEntry( vCut, Entry, i )
+ {
+ assert( Entry );
+ assert( Vec_IntEntry(vMirrors, Entry) == -1 );
+ assert( Vec_IntEntry(vLutLevs, Entry) <= LevStop );
+ if ( Vec_IntEntry(vLutLevs, Entry) == LevStop )
+ Vec_IntPush( vCutTop, Entry );
+ else
+ Vec_IntPush( vCutBot, Entry );
+ }
+ Vec_IntIsOrdered( vCut );
+}
+int Sbd_ManCutCollect_rec( Gia_Man_t * p, Vec_Int_t * vMirrors, int iObj, int LevStop, Vec_Int_t * vLutLevs, Vec_Int_t * vCut )
+{
+ Gia_Obj_t * pObj;
+ int Ret0, Ret1;
+ if ( Vec_IntEntry(vMirrors, iObj) >= 0 )
+ iObj = Abc_Lit2Var(Vec_IntEntry(vMirrors, iObj));
+ if ( !iObj || Gia_ObjIsTravIdCurrentId(p, iObj) )
+ return 1;
+ Gia_ObjSetTravIdCurrentId(p, iObj);
+ pObj = Gia_ManObj( p, iObj );
+ if ( Gia_ObjIsCi(pObj) || Vec_IntEntry(vLutLevs, iObj) <= LevStop )
+ {
+ Vec_IntPush( vCut, iObj );
+ return Vec_IntEntry(vLutLevs, iObj) <= LevStop;
+ }
+ assert( Gia_ObjIsAnd(pObj) );
+ Ret0 = Sbd_ManCutCollect_rec( p, vMirrors, Gia_ObjFaninId0(pObj, iObj), LevStop, vLutLevs, vCut );
+ Ret1 = Sbd_ManCutCollect_rec( p, vMirrors, Gia_ObjFaninId1(pObj, iObj), LevStop, vLutLevs, vCut );
+ return Ret0 && Ret1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sbd_ManCutReduceTop( Gia_Man_t * p, Vec_Int_t * vMirrors, int iObj, Vec_Int_t * vLutLevs, Vec_Int_t * vCut, Vec_Int_t * vCutTop, int nCutSize )
+{
+ int i, Entry, Lit0m, Lit1m, Fan0, Fan1;
+ int LevStop = Vec_IntEntry(vLutLevs, iObj) - 2;
+ Vec_IntIsOrdered( vCut );
+ Vec_IntForEachEntryReverse( vCutTop, Entry, i )
+ {
+ Gia_Obj_t * pObj = Gia_ManObj( p, Entry );
+ if ( Gia_ObjIsCi(pObj) )
+ continue;
+ assert( Gia_ObjIsAnd(pObj) );
+ assert( Vec_IntEntry(vLutLevs, Entry) == LevStop );
+ Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, Entry) );
+ Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, Entry) );
+ Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, Entry);
+ Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, Entry);
+ if ( Vec_IntEntry(vLutLevs, Fan0) > LevStop || Vec_IntEntry(vLutLevs, Fan1) > LevStop )
+ continue;
+ assert( Vec_IntEntry(vLutLevs, Fan0) <= LevStop );
+ assert( Vec_IntEntry(vLutLevs, Fan1) <= LevStop );
+ if ( Vec_IntEntry(vLutLevs, Fan0) == LevStop && Vec_IntEntry(vLutLevs, Fan1) == LevStop )
+ continue;
+ Vec_IntRemove( vCut, Entry );
+ if ( Fan0 ) Vec_IntPushUniqueOrder( vCut, Fan0 );
+ if ( Fan1 ) Vec_IntPushUniqueOrder( vCut, Fan1 );
+ //Sbd_ManCutIsTopo( p, vMirrors, vCut, iObj );
+ return 1;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sbd_ManCutServerFirst( Sbd_Srv_t * p, int iObj, int * pLeaves )
+{
+ int RetValue, LevStop = Vec_IntEntry(p->vLutLevs, iObj) - 2;
+
+ Vec_IntClear( p->vCut );
+ Gia_ManIncrementTravId( p->pGia );
+ RetValue = Sbd_ManCutCollect_rec( p->pGia, p->vMirrors, iObj, LevStop, p->vLutLevs, p->vCut );
+ if ( RetValue == 0 ) // cannot build delay-improving cut
+ return -1;
+ // check if the current cut is good
+ Vec_IntSort( p->vCut, 0 );
+/*
+ Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
+ if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
+ {
+ //printf( "%d ", Vec_IntSize(p->vCut) );
+ memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
+ return Vec_IntSize(p->vCut);
+ }
+*/
+ // try to expand the cut
+ Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
+ Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
+ if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
+ {
+ //printf( "1=(%d,%d) ", Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
+ //printf( "%d ", Vec_IntSize(p->vCut) );
+ memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
+ return Vec_IntSize(p->vCut);
+ }
+
+ // try to reduce the topmost
+ Vec_IntClear( p->vCut0 );
+ Vec_IntAppend( p->vCut0, p->vCut );
+ if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )
+ {
+ Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
+ Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
+ assert( Vec_IntSize(p->vCut) <= p->nCutSize );
+ if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
+ {
+ //printf( "%d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
+ memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
+ return Vec_IntSize(p->vCut);
+ }
+ // try again
+ if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )
+ {
+ Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
+ Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
+ assert( Vec_IntSize(p->vCut) <= p->nCutSize );
+ if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
+ {
+ //printf( "* %d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
+ memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
+ return Vec_IntSize(p->vCut);
+ }
+ // try again
+ if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )
+ {
+ Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
+ Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
+ assert( Vec_IntSize(p->vCut) <= p->nCutSize );
+ if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
+ {
+ //printf( "** %d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
+ memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
+ return Vec_IntSize(p->vCut);
+ }
+ // try again
+ if ( Vec_IntSize(p->vCut) < p->nCutSize && Sbd_ManCutReduceTop( p->pGia, p->vMirrors, iObj, p->vLutLevs, p->vCut, p->vCutTop, p->nCutSize ) )
+ {
+ Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
+ Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
+ assert( Vec_IntSize(p->vCut) <= p->nCutSize );
+ if ( Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
+ {
+ //printf( "*** %d -> %d (%d + %d)\n", Vec_IntSize(p->vCut0), Vec_IntSize(p->vCut), Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
+ memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
+ return Vec_IntSize(p->vCut);
+ }
+ }
+ }
+ }
+ }
+
+ // recompute the cut
+ Vec_IntClear( p->vCut );
+ Gia_ManIncrementTravId( p->pGia );
+ RetValue = Sbd_ManCutCollect_rec( p->pGia, p->vMirrors, iObj, LevStop-1, p->vLutLevs, p->vCut );
+ if ( RetValue == 0 ) // cannot build delay-improving cut
+ return -1;
+ // check if the current cut is good
+ Vec_IntSort( p->vCut, 0 );
+/*
+ Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
+ if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
+ {
+ //printf( "%d ", Vec_IntSize(p->vCut) );
+ memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
+ return Vec_IntSize(p->vCut);
+ }
+*/
+ // try to expand the cut
+ Sbd_ManCutExpand( p->pGia, p->vMirrors, p->vLutLevs, p->vCut );
+ Sbd_ManCutReload( p->vMirrors, p->vLutLevs, LevStop, p->vCut, p->vCutTop, p->vCutBot );
+ if ( Vec_IntSize(p->vCut) <= p->nCutSize && Vec_IntSize(p->vCutTop) <= p->nLutSize-1 )
+ {
+ //printf( "2=(%d,%d) ", Vec_IntSize(p->vCutTop), Vec_IntSize(p->vCutBot) );
+ //printf( "%d ", Vec_IntSize(p->vCut) );
+ memcpy( pLeaves, Vec_IntArray(p->vCut), sizeof(int) * Vec_IntSize(p->vCut) );
+ return Vec_IntSize(p->vCut);
+ }
+
+ return -1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbdInt.h b/src/opt/sbd/sbdInt.h
index 4c553fb4..eabe5355 100644
--- a/src/opt/sbd/sbdInt.h
+++ b/src/opt/sbd/sbdInt.h
@@ -52,10 +52,26 @@ ABC_NAMESPACE_HEADER_START
#define SBD_SAT_UNDEC 0x1234567812345678
#define SBD_SAT_SAT 0x8765432187654321
+#define SBD_LUTS_MAX 2
+#define SBD_SIZE_MAX 4
+#define SBD_DIV_MAX 10
+#define SBD_FVAR_MAX 100
+
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
+typedef struct Sbd_Sto_t_ Sbd_Sto_t;
+typedef struct Sbd_Srv_t_ Sbd_Srv_t;
+
+typedef struct Sbd_Str_t_ Sbd_Str_t;
+struct Sbd_Str_t_
+{
+ int fLut; // LUT or SEL
+ int nVarIns; // input count
+ int VarIns[SBD_DIV_MAX]; // input vars
+ word Res; // result of solving
+};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
@@ -66,7 +82,38 @@ ABC_NAMESPACE_HEADER_START
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-/*=== sbdCnf.c ==========================================================*/
+/*=== sbdCut.c ==========================================================*/
+extern Sbd_Sto_t * Sbd_StoAlloc( Gia_Man_t * pGia, Vec_Int_t * vMirrors, int nLutSize, int nCutSize, int nCutNum, int fCutMin, int fVerbose );
+extern void Sbd_StoFree( Sbd_Sto_t * p );
+extern int Sbd_StoObjRefs( Sbd_Sto_t * p, int iObj );
+extern void Sbd_StoRefObj( Sbd_Sto_t * p, int iObj, int iMirror );
+extern void Sbd_StoDerefObj( Sbd_Sto_t * p, int iObj );
+extern void Sbd_StoComputeCutsConst0( Sbd_Sto_t * p, int iObj );
+extern void Sbd_StoComputeCutsObj( Sbd_Sto_t * p, int iObj, int Delay, int Level );
+extern void Sbd_StoComputeCutsCi( Sbd_Sto_t * p, int iObj, int Delay, int Level );
+extern int Sbd_StoComputeCutsNode( Sbd_Sto_t * p, int iObj );
+extern void Sbd_StoSaveBestDelayCut( Sbd_Sto_t * p, int iObj, int * pCut );
+extern int Sbd_StoObjBestCut( Sbd_Sto_t * p, int iObj, int nSize, int * pLeaves );
+/*=== sbdCut2.c ==========================================================*/
+extern Sbd_Srv_t * Sbd_ManCutServerStart( Gia_Man_t * pGia, Vec_Int_t * vMirrors,
+ Vec_Int_t * vLutLevs, Vec_Int_t * vLevs, Vec_Int_t * vRefs,
+ int nLutSize, int nCutSize, int nCutNum, int fVerbose );
+extern void Sbd_ManCutServerStop( Sbd_Srv_t * p );
+extern int Sbd_ManCutServerFirst( Sbd_Srv_t * p, int iObj, int * pLeaves );
+/*=== sbdWin.c ==========================================================*/
+extern word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp );
+extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
+extern int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds );
+extern int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset );
+/*=== sbdPath.c ==========================================================*/
+extern Vec_Bit_t * Sbc_ManCriticalPath( Gia_Man_t * p );
+/*=== sbdQbf.c ==========================================================*/
+extern int Sbd_ProblemSolve(
+ Gia_Man_t * p, Vec_Int_t * vMirrors,
+ int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var,
+ Vec_Int_t * vTfo, Vec_Int_t * vRoots,
+ Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0
+ );
ABC_NAMESPACE_HEADER_END
diff --git a/src/opt/sbd/sbdLut.c b/src/opt/sbd/sbdLut.c
new file mode 100644
index 00000000..ffcb71f8
--- /dev/null
+++ b/src/opt/sbd/sbdLut.c
@@ -0,0 +1,311 @@
+/**CFile****************************************************************
+
+ FileName [sbdLut.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis [CNF computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sbdLut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+#include "misc/util/utilTruth.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+// count the number of parameter variables in the structure
+int Sbd_ProblemCountParams( int nStrs, Sbd_Str_t * pStr0 )
+{
+ Sbd_Str_t * pStr; int nPars = 0;
+ for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ )
+ nPars += pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns;
+ return nPars;
+}
+// add clauses for the structure
+int Sbd_ProblemAddClauses( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 )
+{
+ // variable order: inputs, structure outputs, parameters
+ Sbd_Str_t * pStr;
+ int VarOut = nVars;
+ int VarPar = nVars + nStrs;
+ int m, k, n, status, pLits[SBD_SIZE_MAX+2];
+//printf( "Start par = %d. ", VarPar );
+ for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++, VarOut++ )
+ {
+ if ( pStr->fLut )
+ {
+ int nMints = 1 << pStr->nVarIns;
+ assert( pStr->nVarIns <= 6 );
+ for ( m = 0; m < nMints; m++, VarPar++ )
+ {
+ for ( k = 0; k < pStr->nVarIns; k++ )
+ pLits[k] = Abc_Var2Lit( pVars[pStr->VarIns[k]], (m >> k) & 1 );
+ for ( n = 0; n < 2; n++ )
+ {
+ pLits[pStr->nVarIns] = Abc_Var2Lit( pVars[VarPar], n );
+ pLits[pStr->nVarIns+1] = Abc_Var2Lit( pVars[VarOut], !n );
+ status = sat_solver_addclause( pSat, pLits, pLits + pStr->nVarIns + 2 );
+ if ( !status )
+ return 0;
+ }
+ }
+ }
+ else
+ {
+ assert( pStr->nVarIns <= SBD_DIV_MAX );
+ for ( k = 0; k < pStr->nVarIns; k++, VarPar++ )
+ {
+ for ( n = 0; n < 2; n++ )
+ {
+ pLits[0] = Abc_Var2Lit( pVars[VarPar], 1 );
+ pLits[1] = Abc_Var2Lit( pVars[VarOut], n );
+ pLits[2] = Abc_Var2Lit( pVars[pStr->VarIns[k]], !n );
+ status = sat_solver_addclause( pSat, pLits, pLits + 3 );
+ if ( !status )
+ return 0;
+ }
+ }
+ }
+ }
+ return 1;
+}
+void Sbd_ProblemAddClausesInit( sat_solver * pSat, int nVars, int nStrs, int * pVars, Sbd_Str_t * pStr0 )
+{
+ Sbd_Str_t * pStr;
+ int VarPar = nVars + nStrs;
+ int m, m2, status, pLits[SBD_DIV_MAX];
+ // make sure selector parameters are mutually exclusive
+ for ( pStr = pStr0; pStr < pStr0 + nStrs; VarPar += pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns, pStr++ )
+ {
+ if ( pStr->fLut )
+ continue;
+ // one variable should be selected
+ assert( pStr->nVarIns <= SBD_DIV_MAX );
+ for ( m = 0; m < pStr->nVarIns; m++ )
+ pLits[m] = Abc_Var2Lit( pVars[VarPar + m], 0 );
+ status = sat_solver_addclause( pSat, pLits, pLits + pStr->nVarIns );
+ assert( status );
+ // two variables cannot be selected
+ for ( m = 0; m < pStr->nVarIns; m++ )
+ for ( m2 = m+1; m2 < pStr->nVarIns; m2++ )
+ {
+ pLits[0] = Abc_Var2Lit( pVars[VarPar + m], 1 );
+ pLits[1] = Abc_Var2Lit( pVars[VarPar + m2], 1 );
+ status = sat_solver_addclause( pSat, pLits, pLits + 2 );
+ assert( status );
+ }
+ }
+}
+void Sbd_ProblemPrintSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits )
+{
+ Sbd_Str_t * pStr;
+ int m, nIters, iLit = 0;
+ printf( "Solution found:\n" );
+ for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ )
+ {
+ nIters = pStr->fLut ? 1 << pStr->nVarIns : pStr->nVarIns;
+ printf( "%s%d : ", pStr->fLut ? "LUT":"SEL", (int)(pStr-pStr0) );
+ for ( m = 0; m < nIters; m++, iLit++ )
+ printf( "%d", !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) );
+ printf( " {" );
+ for ( m = 0; m < pStr->nVarIns; m++ )
+ printf( " %d", pStr->VarIns[m] );
+ printf( " }\n" );
+ }
+ assert( iLit == Vec_IntSize(vLits) );
+}
+void Sbd_ProblemCollectSolution( int nStrs, Sbd_Str_t * pStr0, Vec_Int_t * vLits )
+{
+ Sbd_Str_t * pStr;
+ int m, nIters, iLit = 0;
+ for ( pStr = pStr0; pStr < pStr0 + nStrs; pStr++ )
+ {
+ pStr->Res = 0;
+ if ( pStr->fLut )
+ {
+ nIters = 1 << pStr->nVarIns;
+ for ( m = 0; m < nIters; m++, iLit++ )
+ if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) )
+ Abc_TtSetBit( &pStr->Res, m );
+ pStr->Res = Abc_Tt6Stretch( pStr->Res, pStr->nVarIns );
+ }
+ else
+ {
+ nIters = 0;
+ for ( m = 0; m < pStr->nVarIns; m++, iLit++ )
+ if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, iLit)) )
+ {
+ pStr->Res = pStr->VarIns[m];
+ nIters++;
+ }
+ assert( nIters == 1 );
+ }
+ }
+ assert( iLit == Vec_IntSize(vLits) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Solves QBF problem for the given window.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sbd_ProblemSolve( Gia_Man_t * p, Vec_Int_t * vMirrors,
+ int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var,
+ Vec_Int_t * vTfo, Vec_Int_t * vRoots,
+ Vec_Int_t * vDivSet, int nStrs, Sbd_Str_t * pStr0 ) // divisors, structures
+{
+ extern sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf );
+
+ int fVerbose = 0;
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vLits = Vec_IntAlloc( 100 );
+ sat_solver * pSatCec = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 1 );
+ sat_solver * pSatQbf = sat_solver_new();
+
+ int nVars = Vec_IntSize( vDivSet );
+ int nPars = Sbd_ProblemCountParams( nStrs, pStr0 );
+
+ int VarCecOut = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
+ int VarCecPar = VarCecOut + nStrs;
+
+ int VarQbfPar = 0;
+ int VarQbfFree = nPars;
+
+ int pVarsCec[256];
+ int pVarsQbf[256];
+ int i, iVar, iLit, nIters;
+ int RetValue = 0;
+
+ assert( Vec_IntSize(vDivSet) <= SBD_DIV_MAX );
+ assert( nVars + nStrs + nPars <= 256 );
+
+ // collect CEC variables
+ Vec_IntForEachEntry( vDivSet, iVar, i )
+ pVarsCec[i] = iVar;
+ for ( i = 0; i < nStrs; i++ )
+ pVarsCec[nVars + i] = VarCecOut + i;
+ for ( i = 0; i < nPars; i++ )
+ pVarsCec[nVars + nStrs + i] = VarCecPar + i;
+
+ // collect QBF variables
+ for ( i = 0; i < nVars + nStrs; i++ )
+ pVarsQbf[i] = -1;
+ for ( i = 0; i < nPars; i++ )
+ pVarsQbf[nVars + nStrs + i] = VarQbfPar + i;
+
+ // add clauses to the CEC problem
+ Sbd_ProblemAddClauses( pSatCec, nVars, nStrs, pVarsCec, pStr0 );
+
+ // create QBF solver
+ sat_solver_setnvars( pSatQbf, 1000 );
+ Sbd_ProblemAddClausesInit( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 );
+
+ // assume all parameter variables are 0
+ Vec_IntClear( vLits );
+ for ( i = 0; i < nPars; i++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, 1) );
+ for ( nIters = 0; nIters < (1 << nVars); nIters++ )
+ {
+ // check if these parameters solve the problem
+ int status = sat_solver_solve( pSatCec, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 );
+ if ( status == l_False ) // solution found
+ break;
+ assert( status == l_True );
+
+ if ( fVerbose )
+ {
+ printf( "Iter %3d : ", nIters );
+ for ( i = 0; i < nPars; i++ )
+ printf( "%d", !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) );
+ printf( " " );
+ }
+
+ Vec_IntClear( vLits );
+ // create new QBF variables
+ for ( i = 0; i < nVars + nStrs; i++ )
+ pVarsQbf[i] = VarQbfFree++;
+ // set their values
+ Vec_IntForEachEntry( vDivSet, iVar, i )
+ {
+ iLit = Abc_Var2Lit( pVarsQbf[i], !sat_solver_var_value(pSatCec, iVar) );
+ status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 );
+ assert( status );
+ if ( fVerbose )
+ printf( "%d", sat_solver_var_value(pSatCec, iVar) );
+ }
+ iLit = Abc_Var2Lit( pVarsQbf[nVars], sat_solver_var_value(pSatCec, VarCecOut) );
+ status = sat_solver_addclause( pSatQbf, &iLit, &iLit + 1 );
+ assert( status );
+ if ( fVerbose )
+ printf( " %d\n", !sat_solver_var_value(pSatCec, VarCecOut) );
+ // add clauses to the QBF problem
+ if ( !Sbd_ProblemAddClauses( pSatQbf, nVars, nStrs, pVarsQbf, pStr0 ) )
+ break; // solution does not exist
+ // check if solution still exists
+ status = sat_solver_solve( pSatQbf, NULL, NULL, 0, 0, 0, 0 );
+ if ( status == l_False ) // solution does not exist
+ break;
+ assert( status == l_True );
+ // find the new values of parameters
+ assert( Vec_IntSize(vLits) == 0 );
+ for ( i = 0; i < nPars; i++ )
+ Vec_IntPush( vLits, Abc_Var2Lit(VarCecPar + i, !sat_solver_var_value(pSatQbf, VarQbfPar + i)) );
+ }
+ if ( Vec_IntSize(vLits) > 0 )
+ {
+ //Sbd_ProblemPrintSolution( nStrs, pStr0, vLits );
+ Sbd_ProblemCollectSolution( nStrs, pStr0, vLits );
+ RetValue = 1;
+ }
+ sat_solver_delete( pSatCec );
+ sat_solver_delete( pSatQbf );
+ Vec_IntFree( vLits );
+
+ if ( fVerbose )
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbdPath.c b/src/opt/sbd/sbdPath.c
new file mode 100644
index 00000000..270c81c8
--- /dev/null
+++ b/src/opt/sbd/sbdPath.c
@@ -0,0 +1,197 @@
+/**CFile****************************************************************
+
+ FileName [sbdPath.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis [Critical path.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sbdPath.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sbdInt.h"
+#include "misc/tim/tim.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sbc_ManAddInternalToPath_rec( Gia_Man_t * p, int iObj, Vec_Bit_t * vPath )
+{
+ Gia_Obj_t * pObj;
+ int k, iFan, Value = 0;
+ if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+ return Vec_BitEntry(vPath, iObj);
+ Gia_ObjSetTravIdCurrentId(p, iObj);
+ pObj = Gia_ManObj( p, iObj );
+ if ( Gia_ObjIsCi(pObj) )
+ return Vec_BitEntry(vPath, iObj);
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_LutForEachFanin( p, iObj, iFan, k )
+ Value |= Sbc_ManAddInternalToPath_rec( p, iFan, vPath );
+ if ( Value )
+ Vec_BitWriteEntry( vPath, iObj, 1 );
+ return Value;
+}
+void Sbc_ManAddInternalToPath( Gia_Man_t * p, Vec_Bit_t * vPath )
+{
+ int k, iFan, iObj;
+ Gia_ManForEachLut( p, iObj )
+ {
+ if ( !Vec_BitEntry(vPath, iObj) )
+ continue;
+ Gia_ManIncrementTravId( p );
+ Gia_LutForEachFanin( p, iObj, iFan, k )
+ Gia_ObjSetTravIdCurrentId(p, iFan);
+ Sbc_ManAddInternalToPath_rec( p, iObj, vPath );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbc_ManCriticalPath_rec( Gia_Man_t * p, int * pLevels, int iObj, int LevelFan, Vec_Bit_t * vPath, int Slack )
+{
+ Gia_Obj_t * pObj; int k, iFan;
+ if ( Gia_ObjIsTravIdCurrentId(p, iObj) )
+ return;
+ Gia_ObjSetTravIdCurrentId(p, iObj);
+ pObj = Gia_ManObj( p, iObj );
+ Vec_BitWriteEntry( vPath, iObj, 1 );
+ if ( Gia_ObjIsCi(pObj) )
+ {
+ Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime;
+ int iBox = pManTime ? Tim_ManBoxForCi( pManTime, Gia_ObjCioId(pObj) ) : -1;
+ if ( iBox >= 0 )
+ {
+ int curCo = Tim_ManBoxInputFirst( pManTime, iBox );
+ int nBoxInputs = Tim_ManBoxInputNum( pManTime, iBox );
+ for ( k = 0; k < nBoxInputs; k++ )
+ {
+ Gia_Obj_t * pCo = Gia_ManCo( p, curCo + k );
+ int iDriver = Gia_ObjFaninId0p( p, pCo );
+ if ( (pLevels[iDriver]+Slack >= LevelFan-1) && iDriver )
+ Sbc_ManCriticalPath_rec( p, pLevels, iDriver, pLevels[iDriver], vPath, Abc_MaxInt(0, pLevels[iDriver]+Slack-(LevelFan-1)) );
+ }
+ }
+ return;
+ }
+ assert( Gia_ObjIsAnd(pObj) );
+ Gia_LutForEachFanin( p, iObj, iFan, k )
+ if ( pLevels[iFan]+Slack >= LevelFan-1 )
+ Sbc_ManCriticalPath_rec( p, pLevels, iFan, pLevels[iFan], vPath, Abc_MaxInt(0, pLevels[iFan]+Slack-(LevelFan-1)) );
+}
+Vec_Bit_t * Sbc_ManCriticalPath( Gia_Man_t * p )
+{
+ int * pLevels = NULL, k, iDriver, Slack = 1;
+ int nLevels = p->pManTime ? Gia_ManLutLevelWithBoxes(p) : Gia_ManLutLevel(p, &pLevels);
+ Vec_Bit_t * vPath = Vec_BitStart( Gia_ManObjNum(p) );
+ if ( p->pManTime )
+ pLevels = Vec_IntArray( p->vLevels );
+ Gia_ManIncrementTravId( p );
+ Gia_ManForEachCoDriverId( p, iDriver, k )
+ if ( (pLevels[iDriver] == nLevels) && iDriver )
+ Sbc_ManCriticalPath_rec( p, pLevels, iDriver, pLevels[iDriver], vPath, Slack );
+ if ( !p->pManTime )
+ ABC_FREE( pLevels );
+ Sbc_ManAddInternalToPath( p, vPath );
+ return vPath;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sbc_ManDelayTrace( Gia_Man_t * p )
+{
+ Vec_Bit_t * vPath = Vec_BitStart( Gia_ManObjNum(p) );
+ int i, k, iFan, nLevels, * pLevels;
+ int nLuts = 0, nNodes = 0, nEdges = 0, nEdgesAll = 0;
+ if ( !Gia_ManHasMapping(p) )
+ {
+ printf( "No mapping is available.\n" );
+ return;
+ }
+ assert( Gia_ManHasMapping(p) );
+ // set critical CO drivers
+ nLevels = Gia_ManLutLevel( p, &pLevels );
+ Gia_ManForEachCoDriverId( p, iFan, i )
+ if ( pLevels[iFan] == nLevels )
+ Vec_BitWriteEntry( vPath, iFan, 1 );
+ // set critical internal nodes
+ Gia_ManForEachLutReverse( p, i )
+ {
+ nLuts++;
+ if ( !Vec_BitEntry(vPath, i) )
+ continue;
+ nNodes++;
+ Gia_LutForEachFanin( p, i, iFan, k )
+ {
+ if ( pLevels[iFan] +1 < pLevels[i] )
+ continue;
+ assert( pLevels[iFan] + 1 == pLevels[i] );
+ Vec_BitWriteEntry( vPath, iFan, 1 );
+ nEdges++;
+ //printf( "%d -> %d\n", i, iFan );
+ }
+ }
+ Gia_ManForEachLut( p, i )
+ Gia_LutForEachFanin( p, i, iFan, k )
+ nEdgesAll += (Vec_BitEntry(vPath, i) && Vec_BitEntry(vPath, iFan));
+
+ ABC_FREE( pLevels );
+ Vec_BitFree( vPath );
+ printf( "AIG = %d. LUT = %d. Lev = %d. Path nodes = %d. Path edges = %d. (%d.)\n",
+ Gia_ManAndNum(p), nLuts, nLevels, nNodes, nEdges, nEdgesAll );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/opt/sbd/sbdSat.c b/src/opt/sbd/sbdSat.c
index ae865627..f0de4dbf 100644
--- a/src/opt/sbd/sbdSat.c
+++ b/src/opt/sbd/sbdSat.c
@@ -37,10 +37,6 @@ ABC_NAMESPACE_IMPL_START
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-#define SBD_LUTS_MAX 2
-#define SBD_SIZE_MAX 4
-#define SBD_DIV_MAX 16
-
// new AIG manager
typedef struct Sbd_Pro_t_ Sbd_Pro_t;
struct Sbd_Pro_t_
diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c
index d722f456..069a4125 100644
--- a/src/opt/sbd/sbdWin.c
+++ b/src/opt/sbd/sbdWin.c
@@ -39,19 +39,25 @@ ABC_NAMESPACE_IMPL_START
a DFS ordered array of objects (vWinObjs) whose indexed in the array
(which will be used as SAT variables) are given in array vObj2Var.
The TFO nodes are listed as the last ones in vWinObjs. The root nodes
- are labeled with Abc_LitIsCompl() in vTfo and also given in vRoots.]
+ are labeled with Abc_LitIsCompl() in vTfo and also given in vRoots.
+ If fQbf is 1, returns the instance meant for QBF solving. It is using
+ the last variable (LastVar) as the placeholder for the second copy
+ of the pivot node.]
SideEffects []
SeeAlso []
***********************************************************************/
-sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
+sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors,
+ int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var,
+ Vec_Int_t * vTfo, Vec_Int_t * vRoots, int fQbf )
{
Gia_Obj_t * pObj;
int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue;
int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo);
int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
+ int LastVar = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
//Vec_IntPrint( vWinObjs );
//Vec_IntPrint( vTfo );
//Vec_IntPrint( vRoots );
@@ -60,7 +66,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
pSat = sat_solver_new();
else
sat_solver_restart( pSat );
- sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + 32 );
+ sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + SBD_FVAR_MAX );
// create constant 0 clause
sat_solver_addclause( pSat, &iLit, &iLit + 1 );
// add clauses for all nodes
@@ -100,8 +106,13 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
Fan1 = Vec_IntEntry( vObj2Var, Fan1 );
Fan0 = Fan0 < TfoStart ? Fan0 : Fan0 + Vec_IntSize(vTfo);
Fan1 = Fan1 < TfoStart ? Fan1 : Fan1 + Vec_IntSize(vTfo);
- fCompl0 = Gia_ObjFaninC0(pObj) ^ (Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
- fCompl1 = Gia_ObjFaninC1(pObj) ^ (Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
+ if ( fQbf )
+ {
+ Fan0 = Fan0 == PivotVar ? LastVar : Fan0;
+ Fan1 = Fan1 == PivotVar ? LastVar : Fan1;
+ }
+ fCompl0 = Gia_ObjFaninC0(pObj) ^ (!fQbf && Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m));
+ fCompl1 = Gia_ObjFaninC1(pObj) ^ (!fQbf && Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m));
if ( Gia_ObjIsXor(pObj) )
sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 );
else
@@ -127,7 +138,18 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
sat_solver_delete( pSat );
return NULL;
}
- assert( sat_solver_nvars(pSat) == nVars + 32 );
+ assert( sat_solver_nvars(pSat) == nVars + SBD_FVAR_MAX );
+ }
+ else if ( fQbf )
+ {
+ int n, pLits[2];
+ for ( n = 0; n < 2; n++ )
+ {
+ pLits[0] = Abc_Var2Lit( PivotVar, n );
+ pLits[1] = Abc_Var2Lit( LastVar, n );
+ RetValue = sat_solver_addclause( pSat, pLits, pLits + 2 );
+ assert( RetValue );
+ }
}
// finalize
RetValue = sat_solver_simplify( pSat );
@@ -143,7 +165,7 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
Synopsis [Solves one SAT problem.]
- Description [Computes node function for PivotVar with fanins in vDivVars
+ Description [Computes node function for PivotVar with fanins in vDivSet
using don't-care represented in the SAT solver. Uses array vValues to
return the values of the first Vec_IntSize(vValues) SAT variables in case
the implementation of the node with the given fanins does not exist.]
@@ -153,12 +175,13 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMi
SeeAlso []
***********************************************************************/
-word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vValues, Vec_Int_t * vTemp )
+word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivSet, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp )
{
int nBTLimit = 0;
word uCube, uTruth = 0;
int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
assert( FreeVar < sat_solver_nvars(pSat) );
+ assert( Vec_IntSize(vDivVars) == Vec_IntSize(vDivValues) );
pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
while ( 1 )
@@ -171,12 +194,12 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
return uTruth;
assert( status == l_True );
// remember variable values
- for ( i = 0; i < Vec_IntSize(vValues); i++ )
- Vec_IntWriteEntry( vValues, i, 2*sat_solver_var_value(pSat, i) );
+ Vec_IntForEachEntry( vDivVars, iVar, i )
+ Vec_IntWriteEntry( vDivValues, i, 2*sat_solver_var_value(pSat, iVar) );
// collect divisor literals
Vec_IntClear( vTemp );
Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
- Vec_IntForEachEntry( vDivVars, iVar, i )
+ Vec_IntForEachEntry( vDivSet, iVar, i )
Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
// check against offset
status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
@@ -195,7 +218,7 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
if ( pFinal[i] == pLits[0] )
continue;
Vec_IntPush( vTemp, pFinal[i] );
- iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
+ iVar = Vec_IntFind( vDivSet, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
}
uTruth |= uCube;
@@ -205,11 +228,11 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
}
assert( status == l_True );
// store the counter-example
- for ( i = 0; i < Vec_IntSize(vValues); i++ )
- Vec_IntAddToEntry( vValues, i, sat_solver_var_value(pSat, i) );
+ Vec_IntForEachEntry( vDivVars, iVar, i )
+ Vec_IntAddToEntry( vDivValues, i, sat_solver_var_value(pSat, iVar) );
- for ( i = 0; i < Vec_IntSize(vValues); i++ )
- Vec_IntAddToEntry( vValues, i, 0xC );
+ for ( i = 0; i < Vec_IntSize(vDivValues); i++ )
+ Vec_IntAddToEntry( vDivValues, i, 0xC );
/*
// reduce the counter example
for ( n = 0; n < 2; n++ )
@@ -232,6 +255,140 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sbd_ManSolve2( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vTemp, Vec_Int_t * vSop )
+{
+ int nBTLimit = 0;
+ int status, i, iVar, nFinal, * pFinal, pLits[2], nIter = 0;
+ assert( FreeVar < sat_solver_nvars(pSat) );
+ assert( Vec_IntSize(vDivVars) == Vec_IntSize(vDivValues) );
+ pLits[0] = Abc_Var2Lit( PivotVar, 0 ); // F = 1
+ pLits[1] = Abc_Var2Lit( FreeVar, 0 ); // iNewLit
+ Vec_IntClear( vSop );
+ while ( 1 )
+ {
+ // find onset minterm
+ status = sat_solver_solve( pSat, pLits, pLits + 2, nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ return 0;
+ if ( status == l_False )
+ return 1;
+ assert( status == l_True );
+ // remember variable values
+ //for ( i = 0; i < Vec_IntSize(vValues); i++ )
+ // Vec_IntWriteEntry( vValues, i, 2*sat_solver_var_value(pSat, i) );
+ // collect divisor literals
+ Vec_IntClear( vTemp );
+ Vec_IntPush( vTemp, Abc_LitNot(pLits[0]) ); // F = 0
+ //Vec_IntForEachEntry( vDivSet, iVar, i )
+ Vec_IntForEachEntry( vDivVars, iVar, i )
+ Vec_IntPush( vTemp, sat_solver_var_literal(pSat, iVar) );
+ // check against offset
+ status = sat_solver_solve( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp), nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ return 0;
+ if ( status == l_True )
+ break;
+ assert( status == l_False );
+ // compute cube and add clause
+ nFinal = sat_solver_final( pSat, &pFinal );
+ Vec_IntClear( vTemp );
+ Vec_IntPush( vTemp, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
+ for ( i = 0; i < nFinal; i++ )
+ {
+ if ( pFinal[i] == pLits[0] )
+ continue;
+ Vec_IntPush( vTemp, pFinal[i] );
+ iVar = Vec_IntFind( vDivVars, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
+ //uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
+ Vec_IntPush( vSop, Abc_Var2Lit( iVar, !Abc_LitIsCompl(pFinal[i]) ) );
+ }
+ //uTruth |= uCube;
+ Vec_IntPush( vSop, -1 );
+ status = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntArray(vTemp) + Vec_IntSize(vTemp) );
+ assert( status );
+ nIter++;
+ }
+ assert( status == l_True );
+ // store the counter-example
+ //for ( i = 0; i < Vec_IntSize(vValues); i++ )
+ // Vec_IntAddToEntry( vValues, i, sat_solver_var_value(pSat, i) );
+ return 0;
+}
+
+word Sbd_ManSolverSupp( Vec_Int_t * vSop, int * pInds, int * pnVars )
+{
+ word Supp = 0;
+ int i, Entry, nVars = 0;
+ Vec_IntForEachEntry( vSop, Entry, i )
+ {
+ if ( Entry == -1 )
+ continue;
+ assert( Abc_Lit2Var(Entry) < 64 );
+ if ( (Supp >> Abc_Lit2Var(Entry)) & 1 )
+ continue;
+ pInds[Abc_Lit2Var(Entry)] = nVars++;
+ Supp |= (word)1 << Abc_Lit2Var(Entry);
+ }
+ *pnVars = nVars;
+ return Supp;
+}
+void Sbd_ManSolverPrint( Vec_Int_t * vSop )
+{
+ int v, i, Entry, nVars, pInds[64];
+ word Supp = Sbd_ManSolverSupp( vSop, pInds, &nVars );
+ char Cube[65] = {'\0'};
+ assert( Cube[nVars] == '\0' );
+ for ( v = 0; v < nVars; v++ )
+ Cube[v] = '-';
+ Vec_IntForEachEntry( vSop, Entry, i )
+ {
+ if ( Entry == -1 )
+ {
+ printf( "%s\n", Cube );
+ for ( v = 0; v < nVars; v++ )
+ Cube[v] = '-';
+ continue;
+ }
+ Cube[pInds[Abc_Lit2Var(Entry)]] = '1' - (char)Abc_LitIsCompl(Entry);
+ }
+ Supp = 0;
+}
+void Sbd_ManSolveSelect( Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vDivVars, Vec_Int_t * vDivValues, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots )
+{
+ Vec_Int_t * vSop = Vec_IntAlloc( 100 );
+ Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
+ sat_solver * pSat = Sbd_ManSatSolver( NULL, p, vMirrors, Pivot, vWinObjs, vObj2Var, vTfo, vRoots, 0 );
+ int PivotVar = Vec_IntEntry(vObj2Var, Pivot);
+ int FreeVar = Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots);
+ int Status = Sbd_ManSolve2( pSat, PivotVar, FreeVar, vDivVars, vDivValues, vTemp, vSop );
+ printf( "Pivot = %4d. Divs = %4d. ", Pivot, Vec_IntSize(vDivVars) );
+ if ( Status == 0 )
+ printf( "UNSAT.\n" );
+ else
+ {
+ int nVars, pInds[64];
+ word Supp = Sbd_ManSolverSupp( vSop, pInds, &nVars );
+ //Sbd_ManSolverPrint( vSop );
+ printf( "SAT with %d vars and %d cubes.\n", nVars, Vec_IntCountEntry(vSop, -1) );
+ Supp = 0;
+ }
+ Vec_IntFree( vTemp );
+ Vec_IntFree( vSop );
+ sat_solver_delete( pSat );
+}
+
+
+/**Function*************************************************************
+
Synopsis [Returns a bunch of positive/negative random care minterms.]
Description [Returns 0/1 if the functions is const 0/1.]
@@ -273,6 +430,30 @@ int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar,
return -1;
}
+int Sbd_ManCollectConstantsNew( sat_solver * pSat, Vec_Int_t * vDivVars, int nConsts, int PivotVar, word * pOnset, word * pOffset )
+{
+ int nBTLimit = 0;
+ int n, i, k, status, iLit, iVar;
+ word * pPats[2] = {pOnset, pOffset};
+ assert( Vec_IntSize(vDivVars) < 64 );
+ for ( n = 0; n < 2; n++ )
+ for ( i = 0; i < nConsts; i++ )
+ {
+ sat_solver_random_polarity( pSat );
+ iLit = Abc_Var2Lit( PivotVar, n );
+ status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ return -2;
+ if ( status == l_False )
+ return n;
+ pPats[n][i] = ((word)!n) << Vec_IntSize(vDivVars);
+ Vec_IntForEachEntry( vDivVars, iVar, k )
+ if ( sat_solver_var_value(pSat, iVar) )
+ Abc_TtXorBit(&pPats[n][i], k);
+ }
+ return -1;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c
index 0ab92258..b4dd11f8 100644
--- a/src/opt/sfm/sfmCnf.c
+++ b/src/opt/sfm/sfmCnf.c
@@ -45,7 +45,7 @@ ABC_NAMESPACE_IMPL_START
***********************************************************************/
void Sfm_PrintCnf( Vec_Str_t * vCnf )
{
- char Entry;
+ signed char Entry;
int i, Lit;
Vec_StrForEachEntry( vCnf, Entry, i )
{
@@ -153,7 +153,7 @@ Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap, int iPivotVar )
{
Vec_Int_t * vClause;
- char Entry;
+ signed char Entry;
int i, Lit;
Vec_WecClear( vRes );
vClause = Vec_WecPushLevel( vRes );
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-28 11:14:49 +0000