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

New MFS package.

This commit is contained in:
Alan Mishchenko 2013-05-25 18:10:45 -07:00
parent f47cc6cefc
commit 94a75fe6d8
12 changed files with 111 additions and 109 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -4327,7 +4327,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
}
pPars->nFanoutsMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFanoutsMax < 1 )
if ( pPars->nFanoutsMax < 0 )
goto usage;
break;
case 'D':
@ -4496,7 +4496,7 @@ int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
}
pPars->nFanoutMax = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( pPars->nFanoutMax < 1 )
if ( pPars->nFanoutMax < 0 )
goto usage;
break;
case 'D':

11
src/base/abci/abcMfs.c
View File

@ -19,6 +19,7 @@
***********************************************************************/
#include "base/abc/abc.h"
#include "bool/kit/kit.h"
#include "opt/sfm/sfm.h"
ABC_NAMESPACE_IMPL_START
@ -120,6 +121,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk )
***********************************************************************/
void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
{
Vec_Int_t * vCover = Sfm_NodeReadCover(p);
Vec_Int_t * vMap, * vArray;
Abc_Obj_t * pNode;
int i, k, Fanin;
@ -155,7 +157,14 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
else if ( ~pTruth[0] == 0 )
pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, " 1\n" );
else
pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)pTruth );
{
// pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)pTruth );
int RetValue = Kit_TruthIsop( (unsigned *)pTruth, Vec_IntSize(vArray), vCover, 1 );
assert( RetValue == 0 || RetValue == 1 );
pNode->pData = Abc_SopCreateFromIsop( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), vCover );
if ( RetValue )
Abc_SopComplement( (char *)pNode->pData );
}
}
Vec_IntFree( vMap );
}

4
src/opt/mfs/mfsCore.c
View File

@ -48,7 +48,7 @@ void Abc_NtkMfsParsDefault( Mfs_Par_t * pPars )
{
memset( pPars, 0, sizeof(Mfs_Par_t) );
pPars->nWinTfoLevs = 2;
pPars->nFanoutsMax = 10;
pPars->nFanoutsMax = 30;
pPars->nDepthMax = 20;
pPars->nDivMax = 250;
pPars->nWinSizeMax = 300;
@ -406,7 +406,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
}
}
// perform the network sweep
Abc_NtkSweep( pNtk, 0 );
// Abc_NtkSweep( pNtk, 0 );
// convert into the AIG
if ( !Abc_NtkToAig(pNtk) )
{

4
src/opt/mfs/mfsDiv.c
View File

@ -214,7 +214,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
// (3) the node's fanins (these are treated as a special case)
Abc_NtkIncrementTravId( pNode->pNtk );
Abc_MfsWinSweepLeafTfo_rec( pNode, nLevDivMax );
Abc_MfsWinVisitMffc( pNode );
// Abc_MfsWinVisitMffc( pNode );
Abc_ObjForEachFanin( pNode, pObj, k )
Abc_NodeSetTravIdCurrent( pObj );
@ -244,7 +244,7 @@ Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDi
Abc_ObjForEachFanout( pObj, pFanout, f )
{
// stop if there are too many fanouts
if ( f > 20 )
if ( p->pPars->nFanoutsMax && f > p->pPars->nFanoutsMax )
break;
// skip nodes that are already added
if ( Abc_NodeIsTravIdPrevious(pFanout) )

4
src/opt/mfs/mfsMan.c
View File

@ -113,7 +113,7 @@ void Mfs_ManPrint( Mfs_Man_t * p )
if ( p->pPars->fResub )
{
printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n",
Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
p->nTotalNodesBeg, p->nNodesTried, p->nNodesResub, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
printf( "Attempts : " );
printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
@ -137,7 +137,7 @@ void Mfs_ManPrint( Mfs_Man_t * p )
else
{
printf( "Nodes = %d. Try = %d. Total mints = %d. Local DC mints = %d. Ratio = %5.2f.\n",
Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare,
p->nTotalNodesBeg, p->nNodesTried, p->nMintsTotal, p->nMintsTotal-p->nMintsCare,
1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal );
// printf( "Average ratio of sequential DCs in the global space = %5.2f.\n",
// 1.0-(p->dTotalRatios/p->nNodesTried) );

8
src/opt/mfs/mfsResub.c
View File

@ -164,7 +164,7 @@ p->timeGia += clock() - clk;
***********************************************************************/
int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove, int fSkipUpdate )
{
int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 200;// || pNode->Id == 556;
int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 200;// || pNode->Id == 556;
unsigned * pData;
int pCands[MFS_FANIN_MAX];
int RetValue, iVar, i, nCands, nWords, w;
@ -180,9 +180,9 @@ int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int f
if ( p->pPars->fVeryVerbose )
{
// printf( "\n" );
printf( "Node %5d : Level = %2d. Divs = %3d. Fanin = %d (out of %d). MFFC = %d\n",
pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode),
iFanin, Abc_ObjFaninNum(pNode),
printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Divs =%3d. Fanin = %4d (%d/%d), MFFC = %d\n",
pNode->Id, pNode->Level, Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes), Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode),
Abc_ObjFaninId(pNode, iFanin), iFanin, Abc_ObjFaninNum(pNode),
Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
}

25
src/opt/sfm/sfm.h
View File

@ -42,18 +42,18 @@ typedef struct Sfm_Ntk_t_ Sfm_Ntk_t;
typedef struct Sfm_Par_t_ Sfm_Par_t;
struct Sfm_Par_t_
{
int nTfoLevMax; // the maximum fanout levels
int nFanoutMax; // the maximum number of fanouts
int nDepthMax; // the maximum depth to try
int nWinSizeMax; // the maximum window size
int nDivNumMax; // the maximum number of divisors
int nBTLimit; // the maximum number of conflicts in one SAT run
int fFixLevel; // does not allow level to increase
int fRrOnly; // perform redundance removal
int fArea; // performs optimization for area
int fMoreEffort; // performs high-affort minimization
int fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats
int nTfoLevMax; // the maximum fanout levels
int nFanoutMax; // the maximum number of fanouts
int nDepthMax; // the maximum depth to try
int nWinSizeMax; // the maximum window size
int nDivNumMax; // the maximum number of divisors
int nBTLimit; // the maximum number of conflicts in one SAT run
int fFixLevel; // does not allow level to increase
int fRrOnly; // perform redundance removal
int fArea; // performs optimization for area
int fMoreEffort; // performs high-affort minimization
int fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats
};
////////////////////////////////////////////////////////////////////////
@ -75,6 +75,7 @@ extern Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i );
extern word * Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
extern int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i );
extern int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i );
extern Vec_Int_t * Sfm_NodeReadCover( Sfm_Ntk_t * p );
/*=== sfmSat.c ==========================================================*/

27
src/opt/sfm/sfmCore.c
View File

@ -33,7 +33,7 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
Synopsis []
Synopsis [Setup parameter structure.]
Description []
@ -46,7 +46,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
{
memset( pPars, 0, sizeof(Sfm_Par_t) );
pPars->nTfoLevMax = 2; // the maximum fanout levels
pPars->nFanoutMax = 10; // the maximum number of fanouts
pPars->nFanoutMax = 30; // the maximum number of fanouts
pPars->nDepthMax = 20; // the maximum depth to try
pPars->nWinSizeMax = 300; // the maximum window size
pPars->nDivNumMax = 300; // the maximum number of divisors
@ -61,7 +61,7 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
/**Function*************************************************************
Synopsis []
Synopsis [Prints statistics.]
Description []
@ -73,12 +73,12 @@ void Sfm_ParSetDefault( Sfm_Par_t * pPars )
void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
{
p->timeOther = p->timeTotal - p->timeWin - p->timeDiv - p->timeCnf - p->timeSat;
printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d.\n",
Sfm_NtkNodeNum(p), p->nNodesTried, p->nRemoves + p->nResubs, p->nTotalDivs, p->nSatCalls, p->nTimeOuts );
printf( "Nodes = %d. Try = %d. Resub = %d. Div = %d. SAT calls = %d. Timeouts = %d. MaxDivs = %d.\n",
Sfm_NtkNodeNum(p), p->nNodesTried, p->nRemoves + p->nResubs, p->nTotalDivs, p->nSatCalls, p->nTimeOuts, p->nMaxDivs );
printf( "Attempts : " );
printf( "Remove %6d out of %6d (%6.2f %%) ", p->nRemoves, p->nTryRemoves, p->nRemoves, 100.0*p->nRemoves/Abc_MaxInt(1, p->nTryRemoves) );
printf( "Resub %6d out of %6d (%6.2f %%) ", p->nResubs, p->nTryResubs, p->nResubs, 100.0*p->nResubs /Abc_MaxInt(1, p->nTryResubs) );
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) );
printf( "\n" );
printf( "Reduction: " );
@ -92,6 +92,7 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
ABC_PRTP( "Sat", p->timeSat , p->timeTotal );
ABC_PRTP( "Oth", p->timeOther, p->timeTotal );
ABC_PRTP( "ALL", p->timeTotal, p->timeTotal );
// ABC_PRTP( " ", p->time1 , p->timeTotal );
}
/**Function*************************************************************
@ -108,22 +109,18 @@ void Sfm_NtkPrintStats( Sfm_Ntk_t * p )
int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
{
int fSkipUpdate = 0;
int fVeryVerbose = 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;
word uTruth, uSign, uMask;
clock_t clk;
assert( Sfm_ObjIsNode(p, iNode) );
assert( f >= 0 && f < Sfm_ObjFaninNum(p, iNode) );
if ( iNode == 211 )
{
int i = 0;
}
p->nTryRemoves++;
// report init stats
if ( p->pPars->fVeryVerbose )
printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Div=%3d. Fanin = %d/%d. MFFC = %d\n",
iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs), f, Sfm_ObjFaninNum(p, iNode),
Sfm_ObjFanoutNum(p, Sfm_ObjFanin(p, iNode, f)) == 1 ? Sfm_ObjMffcSize(p, iNode) : 0 );
printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Div=%3d. Fanin =%4d (%d/%d). MFFC = %d\n",
iNode, Sfm_ObjLevel(p, iNode), Vec_IntSize(p->vLeaves), Vec_IntSize(p->vNodes), Vec_IntSize(p->vDivs),
Sfm_ObjFanin(p, iNode, f), f, Sfm_ObjFaninNum(p, iNode), Sfm_ObjMffcSize(p, Sfm_ObjFanin(p, iNode, f)) );
// clean simulation info
p->nCexes = 0;
Vec_WrdFill( p->vDivCexes, Vec_IntSize(p->vDivs), 0 );

11
src/opt/sfm/sfmInt.h
View File

@ -84,8 +84,7 @@ struct Sfm_Ntk_t_
Vec_Int_t * vRoots; // roots
Vec_Int_t * vTfo; // TFO (excluding iNode)
// SAT solving
sat_solver * pSat0; // SAT solver for the off-set
sat_solver * pSat1; // SAT solver for the on-set
sat_solver * pSat; // SAT solver
int nSatVars; // the number of variables
int nTryRemoves; // number of fanin removals
int nTryResubs; // number of resubstitutions
@ -95,11 +94,11 @@ struct Sfm_Ntk_t_
int nCexes; // number of CEXes
Vec_Wrd_t * vDivCexes; // counter-examples
// intermediate data
// Vec_Int_t * vFans; // current fanins
Vec_Int_t * vOrder; // object order
Vec_Int_t * vDivVars; // divisor SAT variables
Vec_Int_t * vDivIds; // divisors indexes
Vec_Int_t * vLits; // literals
Vec_Int_t * vValues; // SAT variable values
Vec_Wec_t * vClauses; // CNF clauses for the node
Vec_Int_t * vFaninMap; // mapping fanins into their SAT vars
// nodes
@ -111,6 +110,7 @@ struct Sfm_Ntk_t_
int nTotalDivs;
int nSatCalls;
int nTimeOuts;
int nMaxDivs;
// runtime
clock_t timeWin;
clock_t timeDiv;
@ -118,6 +118,7 @@ struct Sfm_Ntk_t_
clock_t timeSat;
clock_t timeOther;
clock_t timeTotal;
// clock_t time1;
};
static inline int Sfm_NtkPiNum( Sfm_Ntk_t * p ) { return p->nPis; }
@ -135,8 +136,8 @@ static inline Vec_Int_t * Sfm_ObjFoArray( Sfm_Ntk_t * p, int i ) { return
static inline int Sfm_ObjFaninNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Sfm_ObjFiArray(p, i)); }
static inline int Sfm_ObjFanoutNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Sfm_ObjFoArray(p, i)); }
static inline int Sfm_ObjRefIncrement( Sfm_Ntk_t * p, int iObj ) { return ++Sfm_ObjFiArray(p, iObj)->nSize; }
static inline int Sfm_ObjRefDecrement( Sfm_Ntk_t * p, int iObj ) { return --Sfm_ObjFiArray(p, iObj)->nSize; }
static inline int Sfm_ObjRefIncrement( Sfm_Ntk_t * p, int iObj ) { return ++Sfm_ObjFoArray(p, iObj)->nSize; }
static inline int Sfm_ObjRefDecrement( Sfm_Ntk_t * p, int iObj ) { return --Sfm_ObjFoArray(p, iObj)->nSize; }
static inline int Sfm_ObjFanin( Sfm_Ntk_t * p, int i, int k ) { return Vec_IntEntry(Sfm_ObjFiArray(p, i), k); }
static inline int Sfm_ObjFanout( Sfm_Ntk_t * p, int i, int k ) { return Vec_IntEntry(Sfm_ObjFoArray(p, i), k); }

17
src/opt/sfm/sfmNtk.c
View File

@ -169,13 +169,14 @@ void Sfm_NtkPrepare( Sfm_Ntk_t * p )
p->vRoots = Vec_IntAlloc( 1000 );
p->vTfo = Vec_IntAlloc( 1000 );
p->vDivCexes = Vec_WrdStart( p->pPars->nDivNumMax );
// p->vFans = Vec_IntAlloc( 100 );
p->vOrder = Vec_IntAlloc( 100 );
p->vDivVars = Vec_IntAlloc( 100 );
p->vDivIds = Vec_IntAlloc( 1000 );
p->vLits = Vec_IntAlloc( 100 );
p->vValues = Vec_IntAlloc( 100 );
p->vClauses = Vec_WecAlloc( 100 );
p->vFaninMap = Vec_IntAlloc( 10 );
p->pSat = sat_solver_new();
}
void Sfm_NtkFree( Sfm_Ntk_t * p )
{
@ -200,15 +201,14 @@ void Sfm_NtkFree( Sfm_Ntk_t * p )
Vec_IntFreeP( &p->vRoots );
Vec_IntFreeP( &p->vTfo );
Vec_WrdFreeP( &p->vDivCexes );
// Vec_IntFreeP( &p->vFans );
Vec_IntFreeP( &p->vOrder );
Vec_IntFreeP( &p->vDivVars );
Vec_IntFreeP( &p->vDivIds );
Vec_IntFreeP( &p->vLits );
Vec_IntFreeP( &p->vValues );
Vec_WecFreeP( &p->vClauses );
Vec_IntFreeP( &p->vFaninMap );
if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
if ( p->pSat1 ) sat_solver_delete( p->pSat1 );
if ( p->pSat ) sat_solver_delete( p->pSat );
ABC_FREE( p );
}
@ -243,10 +243,6 @@ void Sfm_NtkAddFanin( Sfm_Ntk_t * p, int iNode, int iFanin )
void Sfm_NtkDeleteObj_rec( Sfm_Ntk_t * p, int iNode )
{
int i, iFanin;
if ( iNode == 202 )
{
int s = 0;
}
if ( Sfm_ObjFanoutNum(p, iNode) > 0 || Sfm_ObjIsPi(p, iNode) )
return;
assert( Sfm_ObjIsNode(p, iNode) );
@ -272,6 +268,7 @@ void Sfm_NtkUpdateLevel_rec( Sfm_Ntk_t * p, int iNode )
void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
{
int iFanin = Sfm_ObjFanin( p, iNode, f );
assert( iFanin != iFaninNew );
// replace old fanin by new fanin
assert( Sfm_ObjIsNode(p, iNode) );
Sfm_NtkRemoveFanin( p, iNode, iFanin );
@ -312,6 +309,10 @@ int Sfm_NodeReadUsed( Sfm_Ntk_t * p, int i )
{
return (Sfm_ObjFaninNum(p, i) > 0) || (Sfm_ObjFanoutNum(p, i) > 0);
}
Vec_Int_t * Sfm_NodeReadCover( Sfm_Ntk_t * p )
{
return p->vCover;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

78
src/opt/sfm/sfmSat.c
View File

@ -54,18 +54,18 @@ static word s_Truths6[6] = {
void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
{
Vec_Int_t * vClause;
int RetValue, Lit, iNode = -1, iFanin, i, k;
int RetValue, iNode = -1, iFanin, i, k;
clock_t clk = clock();
sat_solver * pSat0 = sat_solver_new();
sat_solver * pSat1 = sat_solver_new();
sat_solver_setnvars( pSat0, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 100 );
sat_solver_setnvars( pSat1, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 100 );
// if ( p->pSat )
// printf( "%d ", p->pSat->stats.learnts );
sat_solver_restart( p->pSat );
sat_solver_setnvars( p->pSat, 1 + Vec_IntSize(p->vDivs) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) + 100 );
// create SAT variables
Sfm_NtkCleanVars( p );
p->nSatVars = 1;
Vec_IntForEachEntry( p->vOrder, iNode, i )
Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
// create divisor variables
// collect divisor variables
Vec_IntClear( p->vDivVars );
Vec_IntForEachEntry( p->vDivs, iNode, i )
Vec_IntPush( p->vDivVars, Sfm_ObjSatVar(p, iNode) );
@ -86,39 +86,15 @@ void Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
{
if ( Vec_IntSize(vClause) == 0 )
break;
RetValue = sat_solver_addclause( pSat0, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
assert( RetValue );
RetValue = sat_solver_addclause( pSat1, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
assert( RetValue );
}
}
// Sat_SolverWriteDimacs( pSat0, "test.cnf", NULL, NULL, 0 );
// get the last node
iNode = Vec_IntEntryLast( p->vNodes );
// add unit clause
Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 1 );
RetValue = sat_solver_addclause( pSat0, &Lit, &Lit + 1 );
assert( RetValue );
// add unit clause
Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 0 );
RetValue = sat_solver_addclause( pSat1, &Lit, &Lit + 1 );
assert( RetValue );
// finalize
RetValue = sat_solver_simplify( pSat0 );
RetValue = sat_solver_simplify( p->pSat );
assert( RetValue );
RetValue = sat_solver_simplify( pSat1 );
if ( RetValue == 0 )
{
Sat_SolverWriteDimacs( pSat1, "test.cnf", NULL, NULL, 0 );
}
assert( RetValue );
// return the result
if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
if ( p->pSat1 ) sat_solver_delete( p->pSat1 );
p->pSat0 = pSat0;
p->pSat1 = pSat1;
p->timeCnf += clock() - clk;
}
}
/**Function*************************************************************
@ -135,55 +111,59 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
{
word * pSign, uCube, uTruth = 0;
int status, i, Div, iVar, nFinal, * pFinal, nIter = 0;
int nVars = sat_solver_nvars( p->pSat1 );
int iNewLit = Abc_Var2Lit( nVars, 0 );
sat_solver_setnvars( p->pSat1, nVars + 1 );
int pLits[2], nVars = sat_solver_nvars( p->pSat );
sat_solver_setnvars( p->pSat, nVars + 1 );
pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, Vec_IntEntryLast(p->vNodes)), 0 ); // F = 1
pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit
while ( 1 )
{
// find onset minterm
p->nSatCalls++;
status = sat_solver_solve( p->pSat1, &iNewLit, &iNewLit + 1, p->pPars->nBTLimit, 0, 0, 0 );
status = sat_solver_solve( p->pSat, pLits, pLits + 2, p->pPars->nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return SFM_SAT_UNDEC;
if ( status == l_False )
{
// printf( "+%d ", nIter );
return uTruth;
}
assert( status == l_True );
// remember variable values
Vec_IntClear( p->vValues );
Vec_IntForEachEntry( p->vDivVars, iVar, i )
Vec_IntPush( p->vValues, sat_solver_var_value(p->pSat, iVar) );
// collect divisor literals
Vec_IntClear( p->vLits );
Vec_IntPush( p->vLits, Abc_LitNot(pLits[0]) ); // F = 0
Vec_IntForEachEntry( p->vDivIds, Div, i )
Vec_IntPush( p->vLits, sat_solver_var_literal(p->pSat1, Div) );
Vec_IntPush( p->vLits, sat_solver_var_literal(p->pSat, Div) );
// check against offset
p->nSatCalls++;
status = sat_solver_solve( p->pSat0, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits), p->pPars->nBTLimit, 0, 0, 0 );
status = sat_solver_solve( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits), p->pPars->nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return SFM_SAT_UNDEC;
if ( status == l_True )
break;
assert( status == l_False );
// compute cube and add clause
nFinal = sat_solver_final( p->pSat0, &pFinal );
nFinal = sat_solver_final( p->pSat, &pFinal );
uCube = ~(word)0;
Vec_IntClear( p->vLits );
Vec_IntPush( p->vLits, Abc_LitNot(iNewLit) );
Vec_IntPush( p->vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
for ( i = 0; i < nFinal; i++ )
{
if ( pFinal[i] == pLits[0] )
continue;
Vec_IntPush( p->vLits, pFinal[i] );
iVar = Vec_IntFind( p->vDivIds, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
}
uTruth |= uCube;
status = sat_solver_addclause( p->pSat1, 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 );
nIter++;
}
// printf( "-%d ", nIter );
assert( status == l_True );
// store the counter-example
Vec_IntForEachEntry( p->vDivVars, iVar, i )
if ( sat_solver_var_value(p->pSat1, iVar) ^ sat_solver_var_value(p->pSat0, iVar) ) // insert 1
if ( Vec_IntEntry(p->vValues, i) ^ sat_solver_var_value(p->pSat, iVar) ) // insert 1
{
pSign = Vec_WrdEntryP( p->vDivCexes, i );
assert( !Abc_InfoHasBit( (unsigned *)pSign, p->nCexes) );
@ -207,8 +187,8 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
void Sfm_ComputeInterpolantCheck( Sfm_Ntk_t * p )
{
int iNode = 3;
int iDiv0 = 5;
int iDiv1 = 4;
int iDiv0 = 6;
int iDiv1 = 7;
word uTruth;
// int i;
// Sfm_NtkForEachNode( p, i )

27
src/opt/sfm/sfmWin.c
View File

@ -89,6 +89,10 @@ int Sfm_ObjDeref( Sfm_Ntk_t * p, int iObj )
int Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj )
{
int Count1, Count2;
if ( Sfm_ObjIsPi(p, iObj) )
return 0;
if ( Sfm_ObjFanoutNum(p, iObj) != 1 )
return 0;
assert( Sfm_ObjIsNode( p, iObj ) );
Count1 = Sfm_ObjDeref( p, iObj );
Count2 = Sfm_ObjRef( p, iObj );
@ -182,10 +186,11 @@ int Sfm_NtkCheckFanouts( Sfm_Ntk_t * p, int iNode )
void Sfm_NtkAddDivisors( Sfm_Ntk_t * p, int iNode, int nLevelMax )
{
int i, iFanout;
if ( Sfm_ObjFanoutNum(p, iNode) > p->pPars->nFanoutMax )
return;
Sfm_ObjForEachFanout( p, iNode, iFanout, i )
{
// skip some of the fanouts if the number is large
if ( p->pPars->nFanoutMax && i > p->pPars->nFanoutMax )
break;
// skip TFI nodes, PO nodes, or nodes with high logic level
if ( Sfm_ObjIsTravIdCurrent(p, iFanout) || Sfm_ObjIsPo(p, iFanout) ||
(p->pPars->fFixLevel && Sfm_ObjLevel(p, iFanout) >= nLevelMax) )
@ -252,7 +257,8 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
return 0;
}
// collect TFO (currently use only one level of TFO)
if ( Sfm_NtkCheckFanouts(p, iNode) )
// if ( Sfm_NtkCheckFanouts(p, iNode) )
if ( 0 )
{
Sfm_ObjForEachFanout( p, iNode, iTemp, i )
{
@ -268,10 +274,10 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
clk = clock();
// create ordering of the nodes
Vec_IntClear( p->vOrder );
Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
Vec_IntPush( p->vOrder, iNode );
Vec_IntForEachEntry( p->vLeaves, iNode, i )
Vec_IntPush( p->vOrder, iNode );
Vec_IntForEachEntryReverse( p->vNodes, iTemp, i )
Vec_IntPush( p->vOrder, iTemp );
Vec_IntForEachEntry( p->vLeaves, iTemp, i )
Vec_IntPush( p->vOrder, iTemp );
// mark fanins
Sfm_NtkIncrementTravId2( p );
Sfm_ObjSetTravIdCurrent2( p, iNode );
@ -294,11 +300,17 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
Vec_IntShrink( p->vDivs, k );
assert( Vec_IntSize(p->vDivs) == p->pPars->nDivNumMax );
}
//Vec_IntPrint( p->vLeaves );
//Vec_IntPrint( p->vNodes );
//Vec_IntPrint( p->vDivs );
// collect additional divisors of the TFI nodes
if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
{
int nStartNew = Vec_IntSize(p->vDivs);
Sfm_NtkIncrementTravId2( p );
Sfm_ObjForEachFanin( p, iNode, iTemp, i )
if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) );
Vec_IntForEachEntry( p->vDivs, iTemp, i )
if ( Vec_IntSize(p->vDivs) < p->pPars->nDivNumMax )
Sfm_NtkAddDivisors( p, iTemp, Sfm_ObjLevel(p, iNode) );
@ -309,6 +321,7 @@ int Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose )
Vec_IntPush( p->vOrder, iTemp );
}
assert( Vec_IntSize(p->vDivs) <= p->pPars->nDivNumMax );
p->nMaxDivs += (Vec_IntSize(p->vDivs) == p->pPars->nDivNumMax);
// statistics
p->nTotalDivs += Vec_IntSize(p->vDivs);
p->timeDiv += clock() - clk;