summaryrefslogtreecommitdiffstats
path: root/src/opt
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt')
-rw-r--r--src/opt/cgt/cgtAig.c2
-rw-r--r--src/opt/dar/darBalance.c8
-rw-r--r--src/opt/dar/darScript.c7
-rw-r--r--src/opt/dau/dauDsd.c8
-rw-r--r--src/opt/fxch/FxchSCHashTable.c4
-rw-r--r--src/opt/fxu/fxuReduce.c3
-rw-r--r--src/opt/mfs/mfsDiv.c2
-rw-r--r--src/opt/sbd/sbdCut2.c6
-rw-r--r--src/opt/sfm/sfm.h1
-rw-r--r--src/opt/sfm/sfmCore.c74
-rw-r--r--src/opt/sfm/sfmInt.h3
-rw-r--r--src/opt/sfm/sfmSat.c104
-rw-r--r--src/opt/sfm/sfmWin.c12
13 files changed, 203 insertions, 31 deletions
diff --git a/src/opt/cgt/cgtAig.c b/src/opt/cgt/cgtAig.c
index 9421b75e..2a3b342c 100644
--- a/src/opt/cgt/cgtAig.c
+++ b/src/opt/cgt/cgtAig.c
@@ -133,7 +133,7 @@ void Cgt_ManDetectFanout( Aig_Man_t * pAig, Aig_Obj_t * pObj, int nOdcMax, Vec_P
Vec_PtrWriteEntry( vFanout, k++, pObj );
}
Vec_PtrShrink( vFanout, k );
- Vec_PtrSort( vFanout, (int (*)(void))Aig_ObjCompareIdIncrease );
+ Vec_PtrSort( vFanout, (int (*)(const void *, const void *))Aig_ObjCompareIdIncrease );
assert( Vec_PtrSize(vFanout) > 0 );
}
diff --git a/src/opt/dar/darBalance.c b/src/opt/dar/darBalance.c
index f51a7852..d8195762 100644
--- a/src/opt/dar/darBalance.c
+++ b/src/opt/dar/darBalance.c
@@ -59,7 +59,7 @@ void Dar_BalanceUniqify( Aig_Obj_t * pObj, Vec_Ptr_t * vNodes, int fExor )
Aig_Obj_t * pTemp, * pTempNext;
int i, k;
// sort the nodes by their literal
- Vec_PtrSort( vNodes, (int (*)())Dar_ObjCompareLits );
+ Vec_PtrSort( vNodes, (int (*)(const void *, const void *))Dar_ObjCompareLits );
// remove duplicates
k = 0;
Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pTemp, i )
@@ -402,7 +402,7 @@ Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t
int LeftBound;
assert( vSuper->nSize > 1 );
// sort the new nodes by level in the decreasing order
- Vec_PtrSort( vSuper, (int (*)(void))Aig_NodeCompareLevelsDecrease );
+ Vec_PtrSort( vSuper, (int (*)(const void *, const void *))Aig_NodeCompareLevelsDecrease );
// balance the nodes
while ( vSuper->nSize > 1 )
{
@@ -415,7 +415,7 @@ Aig_Obj_t * Dar_BalanceBuildSuper( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Type_t
pObj2 = (Aig_Obj_t *)Vec_PtrPop(vSuper);
Dar_BalancePushUniqueOrderByLevel( vSuper, Aig_Oper(p, pObj1, pObj2, Type), Type == AIG_OBJ_EXOR );
}
- return (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0);
+ return vSuper->nSize ? (Aig_Obj_t *)Vec_PtrEntry(vSuper, 0) : Aig_ManConst0(p);
}
@@ -462,7 +462,7 @@ Aig_Obj_t * Dar_BalanceBuildSuperTop( Aig_Man_t * p, Vec_Ptr_t * vSuper, Aig_Typ
int i, nBaseSizeAll, nBaseSize;
assert( vSuper->nSize > 1 );
// sort the new nodes by level in the decreasing order
- Vec_PtrSort( vSuper, (int (*)(void))Aig_NodeCompareLevelsDecrease );
+ Vec_PtrSort( vSuper, (int (*)(const void *, const void *))Aig_NodeCompareLevelsDecrease );
// add one LUT at a time
while ( Vec_PtrSize(vSuper) > 1 )
{
diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c
index f8fa3788..d95c23d7 100644
--- a/src/opt/dar/darScript.c
+++ b/src/opt/dar/darScript.c
@@ -848,6 +848,7 @@ pPars->timeSynth = Abc_Clock() - clk;
***********************************************************************/
Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
{
+ extern Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int nConfs, int fVerbose );
extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
// extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
@@ -870,15 +871,17 @@ clk = Abc_Clock();
pPars->timeSynth = Abc_Clock() - clk;
// perform choice computation
- if ( pPars->fUseGia )
+ if ( pPars->fUseNew )
+ pMan = Cec_ComputeChoicesNew( pGia, pPars->nBTLimit, pPars->fVerbose );
+ else if ( pPars->fUseGia )
pMan = Cec_ComputeChoices( pGia, pPars );
else
{
pMan = Gia_ManToAigSkip( pGia, 3 );
- Gia_ManStop( pGia );
pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
Aig_ManStop( pTemp );
}
+ Gia_ManStop( pGia );
// create guidence
vPios = Aig_ManOrderPios( pMan, pAig );
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index b1e7e0d8..3e11a15d 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -1973,6 +1973,14 @@ void Dau_DsdPrintFromTruth( word * pTruth, int nVarsInit )
Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
fprintf( stdout, "%s\n", pRes );
}
+void Dau_DsdPrintFromTruth2( word * pTruth, int nVarsInit )
+{
+ char pRes[DAU_MAX_STR];
+ word pTemp[DAU_MAX_WORD];
+ Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
+ Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
+ fprintf( stdout, "%s", pRes );
+}
void Dau_DsdTest44()
{
diff --git a/src/opt/fxch/FxchSCHashTable.c b/src/opt/fxch/FxchSCHashTable.c
index 28f925e1..c574509f 100644
--- a/src/opt/fxch/FxchSCHashTable.c
+++ b/src/opt/fxch/FxchSCHashTable.c
@@ -17,6 +17,10 @@
***********************************************************************/
#include "Fxch.h"
+#if (__GNUC__ >= 8)
+ #pragma GCC diagnostic ignored "-Wimplicit-fallthrough"
+#endif
+
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/fxu/fxuReduce.c b/src/opt/fxu/fxuReduce.c
index 7542a432..84e2bf87 100644
--- a/src/opt/fxu/fxuReduce.c
+++ b/src/opt/fxu/fxuReduce.c
@@ -86,8 +86,7 @@ int Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTota
assert( iPair == nPairsTotal );
// allocate storage for counters of cube pairs by difference
- pnPairCounters = ABC_FALLOC( int, 2 * nBitsMax );
- memset( pnPairCounters, 0, sizeof(int) * 2 * nBitsMax );
+ pnPairCounters = ABC_CALLOC( int, 2 * nBitsMax );
// count the number of different pairs
for ( k = 0; k < nPairsTotal; k++ )
pnPairCounters[ pnLitsDiff[k] ]++;
diff --git a/src/opt/mfs/mfsDiv.c b/src/opt/mfs/mfsDiv.c
index ece8ec64..535e8d23 100644
--- a/src/opt/mfs/mfsDiv.c
+++ b/src/opt/mfs/mfsDiv.c
@@ -282,7 +282,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
p->nMaxDivs += (Vec_PtrSize(vDivs) >= p->pPars->nWinMax);
// sort the divisors by level in the increasing order
- Vec_PtrSort( vDivs, (int (*)(void))Abc_NodeCompareLevelsIncrease );
+ Vec_PtrSort( vDivs, (int (*)(const void *, const void *))Abc_NodeCompareLevelsIncrease );
// add the fanins of the node
Abc_ObjForEachFanin( pNode, pFanin, k )
diff --git a/src/opt/sbd/sbdCut2.c b/src/opt/sbd/sbdCut2.c
index b4a8be74..b9ef4d82 100644
--- a/src/opt/sbd/sbdCut2.c
+++ b/src/opt/sbd/sbdCut2.c
@@ -193,7 +193,7 @@ static inline int Sbd_ManCutExpandOne( Gia_Man_t * p, Vec_Int_t * vMirrors, Vec_
Vec_IntPushOrder( vCut, Fan1 );
return 1;
}
-void Vec_IntIsOrdered( Vec_Int_t * vCut )
+void Vec_IntOrdered( Vec_Int_t * vCut )
{
int i, Prev, Entry;
Prev = Vec_IntEntry( vCut, 0 );
@@ -229,7 +229,7 @@ void Sbd_ManCutReload( Vec_Int_t * vMirrors, Vec_Int_t * vLutLevs, int LevStop,
else
Vec_IntPush( vCutBot, Entry );
}
- Vec_IntIsOrdered( vCut );
+ Vec_IntOrdered( 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 )
{
@@ -267,7 +267,7 @@ int Sbd_ManCutReduceTop( Gia_Man_t * p, Vec_Int_t * vMirrors, int iObj, Vec_Int_
{
int i, Entry, Lit0m, Lit1m, Fan0, Fan1;
int LevStop = Vec_IntEntry(vLutLevs, iObj) - 2;
- Vec_IntIsOrdered( vCut );
+ Vec_IntOrdered( vCut );
Vec_IntForEachEntryReverse( vCutTop, Entry, i )
{
Gia_Obj_t * pObj = Gia_ManObj( p, Entry );
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 1aa8b7d0..f9c95c83 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -66,6 +66,7 @@ struct Sfm_Par_t_
int fUseAndOr; // enable internal detection of AND/OR gates
int fZeroCost; // enable zero-cost replacement
int fUseSim; // enable simulation
+ int fUseDcs; // enable deriving don't-cares
int fPrintDecs; // enable printing decompositions
int fAllBoxes; // enable preserving all boxes
int fLibVerbose; // enable library stats
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 27d584b4..356aea35 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "sfmInt.h"
+#include "bool/kit/kit.h"
ABC_NAMESPACE_IMPL_START
@@ -79,6 +80,8 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
printf( "Attempts : " );
printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
printf( "Resub %6d out of %6d (%6.2f %%) ", p->nResubs, p->nTryResubs, 100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs) );
+ if ( p->pPars->fUseDcs )
+ printf( "Improves %6d out of %6d (%6.2f %%) ", p->nImproves,p->nTryImproves,100.0*p->nImproves/Abc_MaxInt(1, p->nTryImproves));
printf( "\n" );
printf( "Reduction: " );
@@ -213,7 +216,69 @@ finish:
// update the network
Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth );
return 1;
- }
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs resubstitution for the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sfm_NodeResubOne( Sfm_Ntk_t * p, int iNode )
+{
+ int fSkipUpdate = 0;
+ int i, iFanin;
+ word uTruth;
+ abctime clk;
+ assert( Sfm_ObjIsNode(p, iNode) );
+ p->nTryImproves++;
+ // report init stats
+ if ( p->pPars->fVeryVerbose )
+ printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Div=%3d. Fanins = %d. MFFC = %d\n",
+ iNode, Sfm_ObjLevel(p, iNode), 0, Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs),
+ Sfm_ObjFaninNum(p, iNode), Sfm_ObjMffcSize(p, iNode) );
+ // collect fanins
+ Vec_IntClear( p->vDivIds );
+ Sfm_ObjForEachFanin( p, iNode, iFanin, i )
+ Vec_IntPush( p->vDivIds, Sfm_ObjSatVar(p, iFanin) );
+clk = Abc_Clock();
+ uTruth = Sfm_ComputeInterpolant2( p );
+p->timeSat += Abc_Clock() - clk;
+ // analyze outcomes
+ if ( uTruth == SFM_SAT_UNDEC )
+ {
+ p->nTimeOuts++;
+ return 0;
+ }
+ assert( uTruth != SFM_SAT_SAT );
+ if ( uTruth == Vec_WrdEntry(p->vTruths, iNode) )
+ return 0;
+ else
+ {
+ word uTruth0 = Vec_WrdEntry(p->vTruths, iNode);
+ //word uTruth0N = ~uTruth0;
+ //word uTruthN = ~uTruth;
+ int Old = Kit_TruthLitNum((unsigned*)&uTruth0, Sfm_ObjFaninNum(p, iNode), p->vCover);
+ //int OldN = Kit_TruthLitNum((unsigned*)&uTruth0N, Sfm_ObjFaninNum(p, iNode), p->vCover);
+ int New = Kit_TruthLitNum((unsigned*)&uTruth, Sfm_ObjFaninNum(p, iNode), p->vCover);
+ //int NewN = Kit_TruthLitNum((unsigned*)&uTruthN, Sfm_ObjFaninNum(p, iNode), p->vCover);
+ //if ( Abc_MinInt(New, NewN) > Abc_MinInt(Old, OldN) )
+ if ( New > Old )
+ return 0;
+ }
+ p->nImproves++;
+ if ( fSkipUpdate )
+ return 0;
+ // update truth table
+ Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
+ Sfm_TruthToCnf( uTruth, NULL, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
+ return 1;
+}
int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
{
int i, iFanin;
@@ -230,15 +295,18 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
if ( Sfm_NodeResubSolve( p, iNode, i, 0 ) )
return 1;
}
- if ( p->pPars->fArea )
- return 0;
// try removing redundant edges
+ if ( !p->pPars->fArea )
Sfm_ObjForEachFanin( p, iNode, iFanin, i )
if ( !(Sfm_ObjIsNode(p, iFanin) && Sfm_ObjFanoutNum(p, iFanin) == 1) )
{
if ( Sfm_NodeResubSolve( p, iNode, i, 1 ) )
return 1;
}
+ // try simplifying local functions
+ if ( p->pPars->fUseDcs )
+ if ( Sfm_NodeResubOne( p, iNode ) )
+ return 1;
/*
// try replacing area critical fanins while adding two new fanins
if ( Sfm_ObjFaninNum(p, iNode) < p->nFaninMax )
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 80edd54d..08edf353 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -107,8 +107,10 @@ struct Sfm_Ntk_t_
sat_solver * pSat; // SAT solver
int nSatVars; // the number of variables
int nTryRemoves; // number of fanin removals
+ int nTryImproves;// number of node improvements
int nTryResubs; // number of resubstitutions
int nRemoves; // number of fanin removals
+ int nImproves; // number of node improvements
int nResubs; // number of resubstitutions
// counter-examples
int nCexes; // number of CEXes
@@ -218,6 +220,7 @@ extern void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNe
/*=== sfmSat.c ==========================================================*/
extern int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p );
extern word Sfm_ComputeInterpolant( Sfm_Ntk_t * p );
+extern word Sfm_ComputeInterpolant2( Sfm_Ntk_t * p );
/*=== sfmTim.c ==========================================================*/
extern Sfm_Tim_t * Sfm_TimStart( Mio_Library_t * pLib, Scl_Con_t * pExt, Abc_Ntk_t * pNtk, int DeltaCrit );
extern void Sfm_TimStop( Sfm_Tim_t * p );
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index 6ccdd903..ed38e681 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -19,6 +19,7 @@
***********************************************************************/
#include "sfmInt.h"
+#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
@@ -27,15 +28,6 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static word s_Truths6[6] = {
- ABC_CONST(0xAAAAAAAAAAAAAAAA),
- ABC_CONST(0xCCCCCCCCCCCCCCCC),
- ABC_CONST(0xF0F0F0F0F0F0F0F0),
- ABC_CONST(0xFF00FF00FF00FF00),
- ABC_CONST(0xFFFF0000FFFF0000),
- ABC_CONST(0xFFFFFFFF00000000)
-};
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -228,6 +220,100 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
/**Function*************************************************************
+ Synopsis [Takes SAT solver and returns interpolant.]
+
+ Description [If interpolant does not exist, records difference variables.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Sfm_ComputeInterpolantInt( Sfm_Ntk_t * p, word Truth[2] )
+{
+ int fOnSet, iMint, iVar, nVars = sat_solver_nvars( p->pSat );
+ int iVarPivot = Sfm_ObjSatVar( p, p->iPivotNode );
+ int status, iNewLit, i, Div, nIter = 0;
+ Truth[0] = Truth[1] = 0;
+ sat_solver_setnvars( p->pSat, nVars + 1 );
+ iNewLit = Abc_Var2Lit( nVars, 0 ); // iNewLit
+ assert( Vec_IntSize(p->vDivIds) <= 6 );
+ Vec_IntFill( p->vValues, (1 << Vec_IntSize(p->vDivIds)) * Vec_IntSize(p->vDivVars), -1 );
+ while ( 1 )
+ {
+ // find care minterm
+ p->nSatCalls++; nIter++;
+ status = sat_solver_solve( p->pSat, &iNewLit, &iNewLit + 1, p->pPars->nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ return l_Undef;
+ if ( status == l_False )
+ return l_False;
+ assert( status == l_True );
+ // collect values
+ iMint = 0;
+ fOnSet = sat_solver_var_value(p->pSat, iVarPivot);
+ Vec_IntClear( p->vLits );
+ Vec_IntPush( p->vLits, Abc_LitNot(iNewLit) ); // NOT(iNewLit)
+ Vec_IntPush( p->vLits, Abc_LitNot(sat_solver_var_literal(p->pSat, iVarPivot)) );
+ Vec_IntForEachEntry( p->vDivIds, Div, i )
+ {
+ Vec_IntPush( p->vLits, Abc_LitNot(sat_solver_var_literal(p->pSat, Div)) );
+ if ( sat_solver_var_value(p->pSat, Div) )
+ iMint |= 1 << i;
+ }
+ if ( Truth[!fOnSet] & ((word)1 << iMint) )
+ break;
+ assert( !(Truth[fOnSet] & ((word)1 << iMint)) );
+ Truth[fOnSet] |= ((word)1 << iMint);
+ // remember variable values
+ Vec_IntForEachEntry( p->vDivVars, iVar, i )
+ Vec_IntWriteEntry( p->vValues, iMint * Vec_IntSize(p->vDivVars) + i, sat_solver_var_value(p->pSat, iVar) );
+ status = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
+ if ( status == 0 )
+ return l_False;
+ }
+ assert( status == l_True );
+ // store the counter-example
+ assert( iMint < (1 << Vec_IntSize(p->vDivIds)) );
+ Vec_IntForEachEntry( p->vDivVars, iVar, i )
+ {
+ int Value = Vec_IntEntry(p->vValues, iMint * Vec_IntSize(p->vDivVars) + i);
+ assert( Value != -1 );
+ if ( Value ^ sat_solver_var_value(p->pSat, iVar) ) // insert 1
+ {
+ word * pSign = Vec_WrdEntryP( p->vDivCexes, i );
+ assert( !Abc_InfoHasBit( (unsigned *)pSign, p->nCexes) );
+ Abc_InfoXorBit( (unsigned *)pSign, p->nCexes );
+ }
+ }
+ p->nCexes++;
+ return l_True;
+}
+word Sfm_ComputeInterpolant2( Sfm_Ntk_t * p )
+{
+ word Res, ResP, ResN, Truth[2];
+ int nCubesP = 0, nCubesN = 0;
+ int RetValue = Sfm_ComputeInterpolantInt( p, Truth );
+ if ( RetValue == l_Undef )
+ return SFM_SAT_UNDEC;
+ if ( RetValue == l_True )
+ return SFM_SAT_SAT;
+ assert( RetValue == l_False );
+ //printf( "Offset = %2d. Onset = %2d. DC = %2d. Total = %2d.\n",
+ // Abc_TtCountOnes(Truth[0]), Abc_TtCountOnes(Truth[1]),
+ // (1<<Vec_IntSize(p->vDivIds)) - (Abc_TtCountOnes(Truth[0]) + Abc_TtCountOnes(Truth[1])),
+ // 1<<Vec_IntSize(p->vDivIds) );
+ Truth[0] = Abc_Tt6Stretch( Truth[0], Vec_IntSize(p->vDivIds) );
+ Truth[1] = Abc_Tt6Stretch( Truth[1], Vec_IntSize(p->vDivIds) );
+ ResP = Abc_Tt6Isop( Truth[1], ~Truth[0], Vec_IntSize(p->vDivIds), &nCubesP );
+ ResN = Abc_Tt6Isop( Truth[0], ~Truth[1], Vec_IntSize(p->vDivIds), &nCubesN );
+ Res = nCubesP <= nCubesN ? ResP : ~ResN;
+ //Dau_DsdPrintFromTruth( &Res, Vec_IntSize(p->vDivIds) );
+ return Res;
+}
+
+/**Function*************************************************************
+
Synopsis [Checks resubstitution.]
Description []
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
index 63750407..53f9a71e 100644
--- a/src/opt/sfm/sfmWin.c
+++ b/src/opt/sfm/sfmWin.c
@@ -365,15 +365,15 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
Vec_IntAppend( p->vDivs, p->vNodes );
Vec_IntPop( p->vDivs );
// add non-topological divisors
- if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
+ if ( !p->pPars->nWinSizeMax || Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
{
Sfm_NtkIncrementTravId2( p );
Vec_IntForEachEntry( p->vDivs, iTemp, i )
- if ( Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
+ if ( !p->pPars->nWinSizeMax || Vec_IntSize(p->vDivs) < p->pPars->nWinSizeMax + 0 )
// Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) - 1 );
Sfm_NtkAddDivisors( p, iTemp, p->nLevelMax - Sfm_ObjLevelR(p, iNode) );
}
- if ( Vec_IntSize(p->vDivs) > p->pPars->nWinSizeMax )
+ if ( p->pPars->nWinSizeMax && Vec_IntSize(p->vDivs) > p->pPars->nWinSizeMax )
{
/*
k = 0;
@@ -383,8 +383,8 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
*/
Vec_IntShrink( p->vDivs, p->pPars->nWinSizeMax );
}
- assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );
- p->nMaxDivs += (int)(Vec_IntSize(p->vDivs) == p->pPars->nWinSizeMax);
+ assert( !p->pPars->nWinSizeMax || Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );
+ p->nMaxDivs += (int)(p->pPars->nWinSizeMax && Vec_IntSize(p->vDivs) == p->pPars->nWinSizeMax);
// remove node/fanins from divisors
// mark fanins
Sfm_NtkIncrementTravId2( p );
@@ -397,7 +397,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
if ( !Sfm_ObjIsTravIdCurrent2(p, iTemp) && Sfm_ObjIsUseful(p, iTemp) )
Vec_IntWriteEntry( p->vDivs, k++, iTemp );
Vec_IntShrink( p->vDivs, k );
- assert( Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );
+ assert( !p->pPars->nWinSizeMax || Vec_IntSize(p->vDivs) <= p->pPars->nWinSizeMax );
clkDiv = Abc_Clock() - clkDiv;
p->timeDiv += clkDiv;
p->nTotalDivs += Vec_IntSize(p->vDivs);
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-21 21:33:41 +0000