Skip to content

A
abc
Commit fa585973 by Alan Mishchenko
Options

Updating mfs2 and &mfs to work with larger nodes.

parent e7ecaee9
Showing with 60 additions and 29 deletions
src/aig/gia/giaMfs.c
...@@ -67,7 +67,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) ...@@ -67,7 +67,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
int nBoxes = Gia_ManBoxNum(p), nVars; int nBoxes = Gia_ManBoxNum(p), nVars;
int nRealPis = nBoxes ? Tim_ManPiNum(pManTime) : Gia_ManPiNum(p); int nRealPis = nBoxes ? Tim_ManPiNum(pManTime) : Gia_ManPiNum(p);
int nRealPos = nBoxes ? Tim_ManPoNum(pManTime) : Gia_ManPoNum(p); int nRealPos = nBoxes ? Tim_ManPoNum(pManTime) : Gia_ManPoNum(p);
int i, j, k, curCi, curCo, nBoxIns, nBoxOuts; int i, j, k, curCi, curCo, nBoxIns, nBoxOuts, w, nWords;
int Id, iFan, nMfsVars, nBbIns = 0, nBbOuts = 0, Counter = 0; int Id, iFan, nMfsVars, nBbIns = 0, nBbOuts = 0, Counter = 0;
int nLutSizeMax = Gia_ManLutSizeMax( p ); int nLutSizeMax = Gia_ManLutSizeMax( p );
nLutSizeMax = Abc_MaxInt( nLutSizeMax, 6 ); nLutSizeMax = Abc_MaxInt( nLutSizeMax, 6 );
...@@ -113,15 +113,11 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) ...@@ -113,15 +113,11 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, Id), vLeaves ); pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, Id), vLeaves );
nVars = Abc_TtMinBase( pTruth, Vec_IntArray(vArray), Vec_IntSize(vArray), Vec_IntSize(vLeaves) ); nVars = Abc_TtMinBase( pTruth, Vec_IntArray(vArray), Vec_IntSize(vArray), Vec_IntSize(vLeaves) );
Vec_IntShrink( vArray, nVars ); Vec_IntShrink( vArray, nVars );
if ( nVars <= 6 ) Vec_WrdWriteEntry( vTruths, Counter, pTruth[0] );
Vec_WrdWriteEntry( vTruths, Counter, pTruth[0] ); nWords = Abc_Truth6WordNum( nVars );
else Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) );
{ for ( w = 0; w < nWords; w++ )
int w, nWords = Abc_Truth6WordNum( nVars ); Vec_WrdPush( vTruths2, pTruth[w] );
Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) );
for ( w = 0; w < nWords; w++ )
Vec_WrdPush( vTruths2, pTruth[w] );
}
if ( Gia_ObjLutIsMux(p, Id) ) if ( Gia_ObjLutIsMux(p, Id) )
{ {
Vec_StrWriteEntry( vFixed, Counter, (char)1 ); Vec_StrWriteEntry( vFixed, Counter, (char)1 );
...@@ -143,6 +139,8 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p ) ...@@ -143,6 +139,8 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
Vec_StrWriteEntry( vEmpty, Counter, (char)1 ); Vec_StrWriteEntry( vEmpty, Counter, (char)1 );
uTruth = Gia_ObjFaninC0(pObj) ? ~uTruths6[0]: uTruths6[0]; uTruth = Gia_ObjFaninC0(pObj) ? ~uTruths6[0]: uTruths6[0];
Vec_WrdWriteEntry( vTruths, Counter, uTruth ); Vec_WrdWriteEntry( vTruths, Counter, uTruth );
Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) );
Vec_WrdPush( vTruths2, uTruth );
} }
Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), Counter++ ); Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), Counter++ );
} }
......
src/base/abci/abcMfs.c
...@@ -100,6 +100,8 @@ Vec_Int_t * Abc_NtkAssignStarts( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, int * pnT ...@@ -100,6 +100,8 @@ Vec_Int_t * Abc_NtkAssignStarts( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, int * pnT
Vec_IntWriteEntry( vStarts, pObj->iTemp, Counter ); Vec_IntWriteEntry( vStarts, pObj->iTemp, Counter );
Counter += Abc_Truth6WordNum( Abc_ObjFaninNum(pObj) ); Counter += Abc_Truth6WordNum( Abc_ObjFaninNum(pObj) );
} }
Abc_NtkForEachCo( pNtk, pObj, i )
Vec_IntWriteEntry( vStarts, pObj->iTemp, Counter++ );
*pnTotal = Counter; *pnTotal = Counter;
return vStarts; return vStarts;
} }
...@@ -167,6 +169,8 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed ) ...@@ -167,6 +169,8 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed )
if ( Abc_ObjFaninNum(pObj) <= 6 ) if ( Abc_ObjFaninNum(pObj) <= 6 )
{ {
word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj)); word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj));
int Offset = Vec_IntEntry( vStarts, pObj->iTemp );
Vec_WrdWriteEntry( vTruths2, Offset, uTruth );
Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth ); Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth );
if ( uTruth == 0 || ~uTruth == 0 ) if ( uTruth == 0 || ~uTruth == 0 )
continue; continue;
...@@ -177,6 +181,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed ) ...@@ -177,6 +181,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed )
int Offset = Vec_IntEntry( vStarts, pObj->iTemp ); int Offset = Vec_IntEntry( vStarts, pObj->iTemp );
word * pRes = Vec_WrdEntryP( vTruths2, Offset ); word * pRes = Vec_WrdEntryP( vTruths2, Offset );
Abc_SopToTruthBig( (char *)pObj->pData, Abc_ObjFaninNum(pObj), pTruths, pCube, pRes ); Abc_SopToTruthBig( (char *)pObj->pData, Abc_ObjFaninNum(pObj), pTruths, pCube, pRes );
Vec_WrdWriteEntry( vTruths, pObj->iTemp, pRes[0] );
// check const0 // check const0
for ( k = 0; k < nWords; k++ ) for ( k = 0; k < nWords; k++ )
if ( pRes[k] ) if ( pRes[k] )
...@@ -324,11 +329,13 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p ) ...@@ -324,11 +329,13 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
} }
// update fanins // update fanins
vArray = Sfm_NodeReadFanins( p, pNode->iTemp ); vArray = Sfm_NodeReadFanins( p, pNode->iTemp );
Vec_IntForEachEntry( vArray, Fanin, k )
Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) );
pTruth = Sfm_NodeReadTruth( p, pNode->iTemp ); pTruth = Sfm_NodeReadTruth( p, pNode->iTemp );
pNode->pData = Abc_SopCreateFromTruthIsop( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), pTruth, vCover ); pNode->pData = Abc_SopCreateFromTruthIsop( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), pTruth, vCover );
if ( Abc_SopGetVarNum((char *)pNode->pData) == 0 )
continue;
assert( Abc_SopGetVarNum((char *)pNode->pData) == Vec_IntSize(vArray) ); assert( Abc_SopGetVarNum((char *)pNode->pData) == Vec_IntSize(vArray) );
Vec_IntForEachEntry( vArray, Fanin, k )
Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) );
} }
Vec_IntFree( vCover ); Vec_IntFree( vCover );
Vec_IntFree( vMap ); Vec_IntFree( vMap );
......
src/opt/sfm/sfmCore.c
...@@ -115,6 +115,7 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly ) ...@@ -115,6 +115,7 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556; int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556;
int i, iFanin, iVar = -1; int i, iFanin, iVar = -1;
int iFaninRem = -1, iFaninSkip = -1; int iFaninRem = -1, iFaninSkip = -1;
int nFanins = Sfm_ObjFaninNum(p, iNode);
word uTruth, uSign, uMask; word uTruth, uSign, uMask;
abctime clk; abctime clk;
assert( Sfm_ObjIsNode(p, iNode) ); assert( Sfm_ObjIsNode(p, iNode) );
...@@ -214,7 +215,10 @@ finish: ...@@ -214,7 +215,10 @@ finish:
if ( fSkipUpdate ) if ( fSkipUpdate )
return 0; return 0;
// update the network // update the network
Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth ); Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth, p->pTruth );
// the number of fanins cannot increase
assert( nFanins >= Sfm_ObjFaninNum(p, iNode) );
//printf( "Modifying node %d with %d fanins (resulting in %d fanins).\n", iNode, nFanins, Sfm_ObjFaninNum(p, iNode) );
return 1; return 1;
} }
...@@ -304,7 +308,7 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode ) ...@@ -304,7 +308,7 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
return 1; return 1;
} }
// try simplifying local functions // try simplifying local functions
if ( p->pPars->fUseDcs ) if ( p->pPars->fUseDcs && Sfm_ObjFaninNum(p, iNode) <= 6 )
if ( Sfm_NodeResubOne( p, iNode ) ) if ( Sfm_NodeResubOne( p, iNode ) )
return 1; return 1;
/* /*
...@@ -360,7 +364,7 @@ void Sfm_NtkPrint( Sfm_Ntk_t * p ) ...@@ -360,7 +364,7 @@ void Sfm_NtkPrint( Sfm_Ntk_t * p )
***********************************************************************/ ***********************************************************************/
int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ) int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
{ {
int i, k, Counter = 0; int i, k, Counter = 0, CounterLarge = 0;
//Sfm_NtkPrint( p ); //Sfm_NtkPrint( p );
p->timeTotal = Abc_Clock(); p->timeTotal = Abc_Clock();
if ( pPars->fVerbose ) if ( pPars->fVerbose )
...@@ -382,8 +386,13 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ) ...@@ -382,8 +386,13 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
continue; continue;
if ( p->pPars->nDepthMax && Sfm_ObjLevel(p, i) > p->pPars->nDepthMax ) if ( p->pPars->nDepthMax && Sfm_ObjLevel(p, i) > p->pPars->nDepthMax )
continue; continue;
if ( Sfm_ObjFaninNum(p, i) < 2 || Sfm_ObjFaninNum(p, i) > 6 ) if ( Sfm_ObjFaninNum(p, i) < 2 )
continue;
if ( Sfm_ObjFaninNum(p, i) > SFM_SUPP_MAX )
{
CounterLarge++;
continue; continue;
}
for ( k = 0; Sfm_NodeResub(p, i); k++ ) for ( k = 0; Sfm_NodeResub(p, i); k++ )
{ {
// Counter++; // Counter++;
...@@ -396,6 +405,8 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ) ...@@ -396,6 +405,8 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
p->nTotalNodesEnd = Vec_WecSizeUsedLimits( &p->vFanins, Sfm_NtkPiNum(p), Vec_WecSize(&p->vFanins) - Sfm_NtkPoNum(p) ); p->nTotalNodesEnd = Vec_WecSizeUsedLimits( &p->vFanins, Sfm_NtkPiNum(p), Vec_WecSize(&p->vFanins) - Sfm_NtkPoNum(p) );
p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p); p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p);
p->timeTotal = Abc_Clock() - p->timeTotal; p->timeTotal = Abc_Clock() - p->timeTotal;
if ( pPars->fVerbose && CounterLarge )
printf( "MFS skipped %d (out of %d) nodes with more than %d fanins.\n", CounterLarge, p->nNodes, SFM_SUPP_MAX );
if ( pPars->fVerbose ) if ( pPars->fVerbose )
Sfm_NtkPrintStats( p ); Sfm_NtkPrintStats( p );
//Sfm_NtkPrint( p ); //Sfm_NtkPrint( p );
......
src/opt/sfm/sfmInt.h
...@@ -39,6 +39,7 @@ ...@@ -39,6 +39,7 @@
#include "misc/st/st.h" #include "misc/st/st.h"
#include "map/mio/mio.h" #include "map/mio/mio.h"
#include "base/abc/abc.h" #include "base/abc/abc.h"
#include "misc/util/utilTruth.h"
#include "sfm.h" #include "sfm.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -47,7 +48,8 @@ ...@@ -47,7 +48,8 @@
ABC_NAMESPACE_HEADER_START ABC_NAMESPACE_HEADER_START
#define SFM_FANIN_MAX 6 #define SFM_FANIN_MAX 12
#define SFM_WORDS_MAX ((SFM_FANIN_MAX>6) ? (1<<(SFM_FANIN_MAX-6)) : 1)
#define SFM_SAT_UNDEC 0x1234567812345678 #define SFM_SAT_UNDEC 0x1234567812345678
#define SFM_SAT_SAT 0x8765432187654321 #define SFM_SAT_SAT 0x8765432187654321
...@@ -123,6 +125,10 @@ struct Sfm_Ntk_t_ ...@@ -123,6 +125,10 @@ struct Sfm_Ntk_t_
Vec_Int_t * vValues; // SAT variable values Vec_Int_t * vValues; // SAT variable values
Vec_Wec_t * vClauses; // CNF clauses for the node Vec_Wec_t * vClauses; // CNF clauses for the node
Vec_Int_t * vFaninMap; // mapping fanins into their SAT vars Vec_Int_t * vFaninMap; // mapping fanins into their SAT vars
word TtElems[SFM_FANIN_MAX][SFM_WORDS_MAX];
word * pTtElems[SFM_FANIN_MAX];
word pTruth[SFM_WORDS_MAX];
word pCube[SFM_WORDS_MAX];
// nodes // nodes
int nTotalNodesBeg; int nTotalNodesBeg;
int nTotalEdgesBeg; int nTotalEdgesBeg;
...@@ -216,7 +222,7 @@ extern int Sfm_LibImplementGatesDelay( Sfm_Lib_t * p, int * pFanins, Mi ...@@ -216,7 +222,7 @@ extern int Sfm_LibImplementGatesDelay( Sfm_Lib_t * p, int * pFanins, Mi
/*=== sfmNtk.c ==========================================================*/ /*=== sfmNtk.c ==========================================================*/
extern Sfm_Ntk_t * Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos ); extern Sfm_Ntk_t * Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
extern void Sfm_NtkPrepare( Sfm_Ntk_t * p ); extern void Sfm_NtkPrepare( Sfm_Ntk_t * p );
extern void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth ); extern void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth, word * pTruth );
/*=== sfmSat.c ==========================================================*/ /*=== sfmSat.c ==========================================================*/
extern int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ); extern int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p );
extern word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ); extern word Sfm_ComputeInterpolant( Sfm_Ntk_t * p );
......
src/opt/sfm/sfmNtk.c
...@@ -166,7 +166,7 @@ void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * v ...@@ -166,7 +166,7 @@ void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * v
***********************************************************************/ ***********************************************************************/
Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 ) Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 )
{ {
Sfm_Ntk_t * p; Sfm_Ntk_t * p; int i;
Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed ); Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
p = ABC_CALLOC( Sfm_Ntk_t, 1 ); p = ABC_CALLOC( Sfm_Ntk_t, 1 );
p->nObjs = Vec_WecSize( vFanins ); p->nObjs = Vec_WecSize( vFanins );
...@@ -192,6 +192,10 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t ...@@ -192,6 +192,10 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
Vec_IntFill( &p->vVar2Id, 2*p->nObjs, -1 ); Vec_IntFill( &p->vVar2Id, 2*p->nObjs, -1 );
p->vCover = Vec_IntAlloc( 1 << 16 ); p->vCover = Vec_IntAlloc( 1 << 16 );
p->vCnfs = Sfm_CreateCnf( p ); p->vCnfs = Sfm_CreateCnf( p );
// elementary truth tables
for ( i = 0; i < SFM_FANIN_MAX; i++ )
p->pTtElems[i] = p->TtElems[i];
Abc_TtElemInit( p->pTtElems, SFM_FANIN_MAX );
return p; return p;
} }
void Sfm_NtkPrepare( Sfm_Ntk_t * p ) void Sfm_NtkPrepare( Sfm_Ntk_t * p )
...@@ -315,13 +319,14 @@ void Sfm_NtkUpdateLevelR_rec( Sfm_Ntk_t * p, int iNode ) ...@@ -315,13 +319,14 @@ void Sfm_NtkUpdateLevelR_rec( Sfm_Ntk_t * p, int iNode )
Sfm_ObjForEachFanin( p, iNode, iFanin, i ) Sfm_ObjForEachFanin( p, iNode, iFanin, i )
Sfm_NtkUpdateLevelR_rec( p, iFanin ); Sfm_NtkUpdateLevelR_rec( p, iFanin );
} }
void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth ) void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth, word * pTruth )
{ {
int iFanin = Sfm_ObjFanin( p, iNode, f ); int iFanin = Sfm_ObjFanin( p, iNode, f );
int nWords = Abc_Truth6WordNum( Sfm_ObjFaninNum(p, iNode) );
assert( Sfm_ObjIsNode(p, iNode) ); assert( Sfm_ObjIsNode(p, iNode) );
assert( iFanin != iFaninNew ); assert( iFanin != iFaninNew );
assert( Sfm_ObjFaninNum(p, iNode) <= 6 ); assert( Sfm_ObjFaninNum(p, iNode) <= SFM_FANIN_MAX );
if ( uTruth == 0 || ~uTruth == 0 ) if ( Abc_TtIsConst0(pTruth, nWords) || Abc_TtIsConst1(pTruth, nWords) )
{ {
Sfm_ObjForEachFanin( p, iNode, iFanin, f ) Sfm_ObjForEachFanin( p, iNode, iFanin, f )
{ {
...@@ -346,7 +351,9 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth ...@@ -346,7 +351,9 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth
Sfm_NtkUpdateLevelR_rec( p, iFanin ); Sfm_NtkUpdateLevelR_rec( p, iFanin );
// update truth table // update truth table
Vec_WrdWriteEntry( p->vTruths, iNode, uTruth ); Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
Sfm_TruthToCnf( uTruth, NULL, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) ); if ( p->vTruths2 && Vec_WrdSize(p->vTruths2) )
Abc_TtCopy( Vec_WrdEntryP(p->vTruths2, Vec_IntEntry(p->vStarts, iNode)), pTruth, nWords, 0 );
Sfm_TruthToCnf( uTruth, pTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
} }
/**Function************************************************************* /**Function*************************************************************
......
src/opt/sfm/sfmSat.c
...@@ -153,13 +153,15 @@ int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p ) ...@@ -153,13 +153,15 @@ int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
***********************************************************************/ ***********************************************************************/
word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ) word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
{ {
word * pSign, uCube, uTruth = 0; word * pSign;
int status, i, Div, iVar, nFinal, * pFinal, nIter = 0; int status, i, Div, iVar, nFinal, * pFinal, nIter = 0;
int pLits[2], nVars = sat_solver_nvars( p->pSat ); int pLits[2], nVars = sat_solver_nvars( p->pSat );
int nWords = Abc_Truth6WordNum( Vec_IntSize(p->vDivIds) );
sat_solver_setnvars( p->pSat, nVars + 1 ); sat_solver_setnvars( p->pSat, nVars + 1 );
pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1 pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1
pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit
assert( Vec_IntSize(p->vDivIds) <= 6 ); assert( Vec_IntSize(p->vDivIds) <= SFM_FANIN_MAX );
Abc_TtClear( p->pTruth, nWords );
while ( 1 ) while ( 1 )
{ {
// find onset minterm // find onset minterm
...@@ -168,7 +170,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ) ...@@ -168,7 +170,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
if ( status == l_Undef ) if ( status == l_Undef )
return SFM_SAT_UNDEC; return SFM_SAT_UNDEC;
if ( status == l_False ) if ( status == l_False )
return uTruth; return p->pTruth[0];
assert( status == l_True ); assert( status == l_True );
// remember variable values // remember variable values
Vec_IntClear( p->vValues ); Vec_IntClear( p->vValues );
...@@ -189,7 +191,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ) ...@@ -189,7 +191,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
assert( status == l_False ); assert( status == l_False );
// compute cube and add clause // compute cube and add clause
nFinal = sat_solver_final( p->pSat, &pFinal ); nFinal = sat_solver_final( p->pSat, &pFinal );
uCube = ~(word)0; Abc_TtFill( p->pCube, nWords );
Vec_IntClear( p->vLits ); Vec_IntClear( p->vLits );
Vec_IntPush( p->vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit) Vec_IntPush( p->vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
for ( i = 0; i < nFinal; i++ ) for ( i = 0; i < nFinal; i++ )
...@@ -198,9 +200,9 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p ) ...@@ -198,9 +200,9 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
continue; continue;
Vec_IntPush( p->vLits, pFinal[i] ); Vec_IntPush( p->vLits, pFinal[i] );
iVar = Vec_IntFind( p->vDivIds, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 ); iVar = Vec_IntFind( p->vDivIds, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar]; Abc_TtAndSharp( p->pCube, p->pCube, p->pTtElems[iVar], nWords, !Abc_LitIsCompl(pFinal[i]) );
} }
uTruth |= uCube; Abc_TtOr( p->pTruth, p->pTruth, p->pCube, nWords );
status = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) ); status = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
assert( status ); assert( status );
nIter++; nIter++;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment