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

Experiments with SAT-based collapsing.

This commit is contained in:
Alan Mishchenko 2015-09-04 11:52:27 -07:00
parent 1ffd9aad76
commit a207f6c071
4 changed files with 491 additions and 181 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/base/abc/abc.h
View File

@ -596,6 +596,7 @@ extern ABC_DLL int Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk );
extern ABC_DLL int Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk );
/*=== abcCollapse.c ==========================================================*/
extern ABC_DLL Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
extern ABC_DLL Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fVerbose );
/*=== abcCut.c ==========================================================*/
extern ABC_DLL void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
extern ABC_DLL void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree );

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

@ -95,6 +95,7 @@ static int Abc_CommandShowBdd ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandShowCut ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSatClp ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandStrash ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBalance ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMuxStruct ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -714,6 +715,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Printing", "show_cut", Abc_CommandShowCut, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "collapse", Abc_CommandCollapse, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "satclp", Abc_CommandSatClp, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "strash", Abc_CommandStrash, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "balance", Abc_CommandBalance, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mux_struct", Abc_CommandMuxStruct, 1 );
@ -3068,6 +3070,108 @@ usage:
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes;
int nCubeLim = 1000;
int nBTLimit = 1000000;
int fCanon = 0;
int fVerbose = 0;
int c;
// set defaults
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CLcvh" ) ) != EOF )
{
switch ( c )
{
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nCubeLim = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nCubeLim < 0 )
goto usage;
break;
case 'L':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
nBTLimit = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nBTLimit < 0 )
goto usage;
break;
case 'c':
fCanon ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pNtk == NULL )
{
Abc_Print( -1, "Empty network.\n" );
return 1;
}
if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) )
{
Abc_Print( -1, "Can only collapse a logic network or an AIG.\n" );
return 1;
}
// get the new network
if ( Abc_NtkIsStrash(pNtk) )
pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, fCanon, fVerbose );
else
{
pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, fCanon, fVerbose );
Abc_NtkDelete( pNtk );
}
if ( pNtkRes == NULL )
{
Abc_Print( -1, "Collapsing has failed.\n" );
return 1;
}
// replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
Abc_Print( -2, "usage: satclp [-CL num] [-cvh]\n" );
Abc_Print( -2, "\t performs SAT based collapsing\n" );
Abc_Print( -2, "\t-C num : the limit on the SOP size of one output [default = %d]\n", nCubeLim );
Abc_Print( -2, "\t-L num : the limit on the number of conflicts in one SAT call [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-c : toggles using canonical ISOP computation [default = %s]\n", fCanon? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
@ -37135,19 +37239,23 @@ usage:
***********************************************************************/
int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern int Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fVerbose );
extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fVerbose );
int nCubeLim = 1000;
int nBTLimit = 1000000;
int c, fVerbose = 0;
int fCanon = 0;
int fVerbose = 0;
int c;
Vec_Str_t * vSop;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "LCvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CLcvh" ) ) != EOF )
{
switch ( c )
{
case 'L':
case 'C':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
goto usage;
}
nCubeLim = atoi(argv[globalUtilOptind]);
@ -37155,10 +37263,10 @@ int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nCubeLim < 0 )
goto usage;
break;
case 'C':
case 'L':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
goto usage;
}
nBTLimit = atoi(argv[globalUtilOptind]);
@ -37166,6 +37274,9 @@ int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nBTLimit < 0 )
goto usage;
break;
case 'c':
fCanon ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -37180,14 +37291,16 @@ int Abc_CommandAbc9SatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9SatClp(): There is no AIG.\n" );
return 0;
}
Bmc_CollapseOne( pAbc->pGia, nCubeLim, nBTLimit, fVerbose );
vSop = Bmc_CollapseOne( pAbc->pGia, nCubeLim, nBTLimit, fCanon, fVerbose );
Vec_StrFree( vSop );
return 0;
usage:
Abc_Print( -2, "usage: &satclp [-LC num] [-vh]\n" );
Abc_Print( -2, "usage: &satclp [-CL num] [-cvh]\n" );
Abc_Print( -2, "\t performs SAT based collapsing\n" );
Abc_Print( -2, "\t-L num : the limit on the SOP size of one output [default = %d]\n", nCubeLim );
Abc_Print( -2, "\t-C num : the limit on the number of conflicts in one call [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-C num : the limit on the SOP size of one output [default = %d]\n", nCubeLim );
Abc_Print( -2, "\t-L num : the limit on the number of conflicts in one SAT call [default = %d]\n", nBTLimit );
Abc_Print( -2, "\t-c : toggles using canonical ISOP computation [default = %s]\n", fCanon? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;

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

@ -19,6 +19,7 @@
***********************************************************************/
#include "base/abc/abc.h"
#include "aig/gia/gia.h"
#ifdef ABC_USE_CUDD
#include "bdd/extrab/extraBdd.h"
@ -32,9 +33,6 @@ ABC_NAMESPACE_IMPL_START
#ifdef ABC_USE_CUDD
static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk );
static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc );
extern int Abc_NodeSupport( DdNode * bFunc, Vec_Str_t * vSupport, int nVars );
////////////////////////////////////////////////////////////////////////
@ -117,74 +115,24 @@ int Abc_NtkMinimumBase2( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc )
{
Abc_Ntk_t * pNtkNew;
abctime clk = Abc_Clock();
assert( Abc_NtkIsStrash(pNtk) );
// compute the global BDDs
if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL )
return NULL;
if ( fVerbose )
{
DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
ABC_PRT( "BDD construction time", Abc_Clock() - clk );
}
// create the new network
pNtkNew = Abc_NtkFromGlobalBdds( pNtk );
// Abc_NtkFreeGlobalBdds( pNtk );
Abc_NtkFreeGlobalBdds( pNtk, 1 );
if ( pNtkNew == NULL )
{
// Cudd_Quit( pNtk->pManGlob );
// pNtk->pManGlob = NULL;
return NULL;
}
// Extra_StopManager( pNtk->pManGlob );
// pNtk->pManGlob = NULL;
// make the network minimum base
Abc_NtkMinimumBase2( pNtkNew );
if ( pNtk->pExdc )
pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
// make sure that everything is okay
if ( !Abc_NtkCheck( pNtkNew ) )
{
printf( "Abc_NtkCollapse: The network check has failed.\n" );
Abc_NtkDelete( pNtkNew );
return NULL;
}
return pNtkNew;
Abc_Obj_t * pNodeNew, * pTemp;
int i;
// create a new node
pNodeNew = Abc_NtkCreateNode( pNtkNew );
// add the fanins in the order, in which they appear in the reordered manager
Abc_NtkForEachCi( pNtkNew, pTemp, i )
Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, dd->invperm[i]) );
// transfer the function
pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFunc ); Cudd_Ref( (DdNode *)pNodeNew->pData );
return pNodeNew;
}
//int runtime1, runtime2;
/**Function*************************************************************
Synopsis [Derives the network with the given global BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
{
// extern void Extra_ShuffleTest( reo_man * p, DdManager * dd, DdNode * Func );
// reo_man * pReo;
ProgressBar * pProgress;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode, * pDriver, * pNodeNew;
// DdManager * dd = pNtk->pManGlob;
DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
int i;
@ -222,9 +170,6 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
Cudd_RecursiveDeref( dd, bBddDc );
}
// pReo = Extra_ReorderInit( Abc_NtkCiNum(pNtk), 1000 );
// runtime1 = runtime2 = 0;
// start the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
// make sure the new manager has the same number of inputs
@ -240,46 +185,51 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy );
continue;
}
// pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) );
pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)Abc_ObjGlobalBdd(pNode) );
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
// Extra_ShuffleTest( pReo, dd, Abc_ObjGlobalBdd(pNode) );
}
Extra_ProgressBarStop( pProgress );
return pNtkNew;
}
Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose )
{
Abc_Ntk_t * pNtkNew;
abctime clk = Abc_Clock();
// Extra_ReorderQuit( pReo );
//ABC_PRT( "Reo ", runtime1 );
//ABC_PRT( "Cudd", runtime2 );
assert( Abc_NtkIsStrash(pNtk) );
// compute the global BDDs
if ( Abc_NtkBuildGlobalBdds(pNtk, fBddSizeMax, 1, fReorder, fVerbose) == NULL )
return NULL;
if ( fVerbose )
{
DdManager * dd = (DdManager *)Abc_NtkGlobalBddMan( pNtk );
printf( "Shared BDD size = %6d nodes. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
ABC_PRT( "BDD construction time", Abc_Clock() - clk );
}
// create the new network
pNtkNew = Abc_NtkFromGlobalBdds( pNtk );
Abc_NtkFreeGlobalBdds( pNtk, 1 );
if ( pNtkNew == NULL )
return NULL;
// make the network minimum base
Abc_NtkMinimumBase2( pNtkNew );
if ( pNtk->pExdc )
pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
// make sure that everything is okay
if ( !Abc_NtkCheck( pNtkNew ) )
{
printf( "Abc_NtkCollapse: The network check has failed.\n" );
Abc_NtkDelete( pNtkNew );
return NULL;
}
return pNtkNew;
}
/**Function*************************************************************
Synopsis [Derives the network with the given global BDD.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc )
{
Abc_Obj_t * pNodeNew, * pTemp;
int i;
// create a new node
pNodeNew = Abc_NtkCreateNode( pNtkNew );
// add the fanins in the order, in which they appear in the reordered manager
Abc_NtkForEachCi( pNtkNew, pTemp, i )
Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, dd->invperm[i]) );
// transfer the function
pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFunc ); Cudd_Ref( (DdNode *)pNodeNew->pData );
return pNodeNew;
}
#else
@ -290,6 +240,175 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i
#endif
/**Function*************************************************************
Synopsis [Derives GIA for the cone of one output and computes its SOP.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_NtkClpOneGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode )
{
int iLit0, iLit1;
if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 )
return pNode->iTemp;
assert( Abc_ObjIsNode( pNode ) );
Abc_NodeSetTravIdCurrent( pNode );
iLit0 = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin0(pNode) );
iLit1 = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin1(pNode) );
iLit0 = Abc_LitNotCond( iLit0, Abc_ObjFaninC0(pNode) );
iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC1(pNode) );
return (pNode->iTemp = Gia_ManHashAnd(pNew, iLit0, iLit1));
}
Gia_Man_t * Abc_NtkClpOneGia( Abc_Ntk_t * pNtk, int iCo, Vec_Int_t * vSupp )
{
int i, iCi, iLit;
Abc_Obj_t * pNode;
Gia_Man_t * pNew, * pTemp;
pNew = Gia_ManStart( 1000 );
pNew->pName = Abc_UtilStrsav( pNtk->pName );
pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec );
Gia_ManHashStart( pNew );
// primary inputs
Abc_AigConst1(pNtk)->iTemp = 1;
Vec_IntForEachEntry( vSupp, iCi, i )
Abc_NtkCi(pNtk, iCi)->iTemp = Gia_ManAppendCi(pNew);
// create the first cone
Abc_NtkIncrementTravId( pNtk );
pNode = Abc_NtkCo( pNtk, iCo );
iLit = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin0(pNode) );
iLit = Abc_LitNotCond( iLit, Abc_ObjFaninC0(pNode) );
Gia_ManAppendCo( pNew, iLit );
// perform cleanup
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fVerbose, int fCanon, Vec_Int_t ** pvSupp )
{
extern Vec_Int_t * Abc_NtkNodeSupportInt( Abc_Ntk_t * pNtk, int iCo );
extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fVerbose );
Vec_Int_t * vSupp = Abc_NtkNodeSupportInt( pNtk, iCo );
Gia_Man_t * pGia = Abc_NtkClpOneGia( pNtk, iCo, vSupp );
Vec_Str_t * vSop;
if ( fVerbose )
printf( "Output %d:\n", iCo );
vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fVerbose );
Gia_ManStop( pGia );
*pvSupp = vSupp;
if ( vSop == NULL )
Vec_IntFree(vSupp);
else if ( Vec_StrSize(vSop) == 4 ) // constant
Vec_IntClear(vSupp);
return vSop;
}
/**Function*************************************************************
Synopsis [SAT-based collapsing.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Abc_Obj_t * Abc_NtkFromSopsOne( Abc_Ntk_t * pNtkNew, Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fVerbose )
{
Abc_Obj_t * pNodeNew;
Vec_Int_t * vSupp;
Vec_Str_t * vSop;
int i, iCi;
// compute SOP of the node
vSop = Abc_NtkClpOne( pNtk, iCo, nCubeLim, nBTLimit, fVerbose, fCanon, &vSupp );
if ( vSop == NULL )
return NULL;
// create a new node
pNodeNew = Abc_NtkCreateNode( pNtkNew );
// add fanins
Vec_IntForEachEntry( vSupp, iCi, i )
Abc_ObjAddFanin( pNodeNew, Abc_NtkCi(pNtkNew, iCi) );
Vec_IntFree( vSupp );
// transfer the function
pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Vec_StrArray(vSop) );
Vec_StrFree( vSop );
return pNodeNew;
}
Abc_Ntk_t * Abc_NtkFromSops( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fVerbose )
{
ProgressBar * pProgress;
Abc_Ntk_t * pNtkNew;
Abc_Obj_t * pNode, * pDriver, * pNodeNew;
int i;
// start the new network
pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
// process the POs
pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
Abc_NtkForEachCo( pNtk, pNode, i )
{
Extra_ProgressBarUpdate( pProgress, i, NULL );
pDriver = Abc_ObjFanin0(pNode);
if ( Abc_ObjIsCi(pDriver) && !strcmp(Abc_ObjName(pNode), Abc_ObjName(pDriver)) )
{
Abc_ObjAddFanin( pNode->pCopy, pDriver->pCopy );
continue;
}
/*
if ( Abc_ObjIsCi(pDriver) )
{
pNodeNew = Abc_NtkCreateNode( pNtkNew );
Abc_ObjAddFanin( pNodeNew, pDriver->pCopy ); // pDriver->pCopy is removed by GIA construction...
pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? "0 1\n" : "1 1\n" );
continue;
}
*/
if ( pDriver == Abc_AigConst1(pNtk) )
{
pNodeNew = Abc_NtkCreateNode( pNtkNew );
pNodeNew->pData = Abc_SopRegister( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_ObjFaninC0(pNode) ? " 0\n" : " 1\n" );
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
continue;
}
pNodeNew = Abc_NtkFromSopsOne( pNtkNew, pNtk, i, nCubeLim, nBTLimit, fCanon, fVerbose );
if ( pNodeNew == NULL )
{
Abc_NtkDelete( pNtkNew );
pNtkNew = NULL;
break;
}
Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
}
Extra_ProgressBarStop( pProgress );
return pNtkNew;
}
Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int fCanon, int fVerbose )
{
Abc_Ntk_t * pNtkNew;
assert( Abc_NtkIsStrash(pNtk) );
// create the new network
pNtkNew = Abc_NtkFromSops( pNtk, nCubeLim, nBTLimit, fCanon, fVerbose );
if ( pNtkNew == NULL )
return NULL;
if ( pNtk->pExdc )
pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
// make sure that everything is okay
if ( !Abc_NtkCheck( pNtkNew ) )
{
printf( "Abc_NtkCollapseSat: The network check has failed.\n" );
Abc_NtkDelete( pNtkNew );
return NULL;
}
return pNtkNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

223
src/sat/bmc/bmcClp.c
View File

@ -47,51 +47,15 @@ extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfOb
SeeAlso []
***********************************************************************/
int Bmc_CollapseExpand2( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit )
{
int i, Index, status, nFinal, * pFinal;
// check against offset
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return -1;
assert( status == l_False );
// get subset of literals
nFinal = sat_solver_final( pSat, &pFinal );
// collect literals
Vec_IntClear( vNums );
for ( i = 0; i < nFinal; i++ )
{
Index = Vec_IntFind( vLits, Abc_LitNot(pFinal[i]) );
assert( Index >= 0 );
Vec_IntPush( vNums, Index );
}
/*
int i;
Vec_IntClear( vNums );
for ( i = 0; i < Vec_IntSize(vLits); i++ )
Vec_IntPush( vNums, i );
*/
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Bmc_CollapseExpand( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit )
int Bmc_CollapseExpandCanon( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit )
{
int k, n, iLit, status;
// try removing one literal at a time
for ( k = Vec_IntSize(vLits) - 1; k >= 0; k-- )
{
int Save = Vec_IntEntry( vLits, k );
if ( Save == -1 )
continue;
Vec_IntWriteEntry( vLits, k, -1 );
// put into new array
Vec_IntClear( vTemp );
@ -124,15 +88,67 @@ int Bmc_CollapseExpand( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vNums,
SeeAlso []
***********************************************************************/
int Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fVerbose )
int Bmc_CollapseExpand( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vNums, Vec_Int_t * vTemp, int nBTLimit )
{
int i, k, iLit, status, nFinal, * pFinal;
// check against offset
status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return -1;
assert( status == l_False );
// get subset of literals
nFinal = sat_solver_final( pSat, &pFinal );
/*
// collect literals
Vec_IntClear( vNums );
for ( i = 0; i < nFinal; i++ )
{
iLit = Vec_IntFind( vLits, Abc_LitNot(pFinal[i]) );
assert( iLit >= 0 );
Vec_IntPush( vNums, iLit );
}
*/
// mark unused literals
Vec_IntForEachEntry( vLits, iLit, i )
{
for ( k = 0; k < nFinal; k++ )
if ( iLit == Abc_LitNot(pFinal[k]) )
break;
if ( k == nFinal )
Vec_IntWriteEntry( vLits, i, -1 );
}
Bmc_CollapseExpandCanon( pSat, vLits, vNums, vTemp, nBTLimit );
/*
int i;
Vec_IntClear( vNums );
for ( i = 0; i < Vec_IntSize(vLits); i++ )
Vec_IntPush( vNums, i );
*/
return 0;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fVerbose, int fCompl )
{
int fPrintMinterm = 0;
int nVars = Gia_ManCiNum(p);
Vec_Int_t * vVars = Vec_IntAlloc( nVars );
Vec_Int_t * vLits = Vec_IntAlloc( nVars );
Vec_Int_t * vNums = Vec_IntAlloc( nVars );
Vec_Int_t * vCube = Vec_IntAlloc( nVars );
Vec_Str_t * vStr = Vec_StrAlloc( nVars+1 );
int iOut = 0, iLit, iVar, status, n, Count;
Vec_Str_t * vSop = Vec_StrAlloc( 100 );
int iOut = 0, iLit, iVar, status, n, Count, Start;
// create SAT solver
Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
@ -152,71 +168,132 @@ int Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fVerbose )
iLit = Abc_Var2Lit( iOut + 1, n ); // n=0 => F=1 n=1 => F=0
status = sat_solver_addclause( pSat[n], &iLit, &iLit + 1 );
if ( status == 0 )
return -1; // const0/1
{
Vec_StrPrintStr( vSop, (n ^ fCompl) ? " 1\n" : " 0\n" );
Vec_StrPush( vSop, '\0' );
goto cleanup; // const0/1
}
status = sat_solver_solve( pSat[n], NULL, NULL, nBTLimit, 0, 0, 0 );
if ( status == l_Undef )
return -3; // timeout
{
Vec_StrFreeP( &vSop );
goto cleanup; // timeout
}
if ( status == l_False )
return -1; // const0/1
{
Vec_StrPrintStr( vSop, (n ^ fCompl) ? " 1\n" : " 0\n" );
Vec_StrPush( vSop, '\0' );
goto cleanup; // const0/1
}
}
Vec_StrPush( vSop, '\0' );
// prepare on-set for solving
sat_solver_prepare_enum( pSat[0], Vec_IntArray(vVars), Vec_IntSize(vVars) );
for ( Count = 0; Count < nCubeLim; )
if ( fCanon )
sat_solver_prepare_enum( pSat[0], Vec_IntArray(vVars), Vec_IntSize(vVars) );
Count = 0;
while ( 1 )
{
// get the smallest assignment
// get the assignment
status = sat_solver_solve( pSat[0], NULL, NULL, 0, 0, 0, 0 );
if ( status == l_Undef )
return -3; // timeout
{
Vec_StrFreeP( &vSop );
goto cleanup; // timeout
}
if ( status == l_False )
break;
// check number of cubes
if ( Count == nCubeLim )
{
//printf( "The number of cubes exceeded the limit (%d).\n", nCubeLim );
Vec_StrFreeP( &vSop );
goto cleanup; // cube out
}
// collect values
Vec_IntClear( vLits );
Vec_IntForEachEntry( vVars, iVar, n )
Vec_IntPush( vLits, Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[0], iVar)) );
// print minterm
// printf( "Mint: " );
// Vec_IntForEachEntry( vLits, iLit, n )
// printf( "%d", !Abc_LitIsCompl(iLit) );
// printf( "\n" );
// expand the values
status = Bmc_CollapseExpand( pSat[1], vLits, vNums, vCube, nBTLimit );
if ( status < 0 )
return -3; // timeout
Count++;
// print cube
if ( fVerbose )
if ( fPrintMinterm )
{
Vec_StrFill( vStr, nVars, '-' );
Vec_StrPush( vStr, '\0' );
Vec_IntForEachEntry( vNums, iVar, n )
Vec_StrWriteEntry( vStr, iVar, (char)('0' + !Abc_LitIsCompl(Vec_IntEntry(vLits, iVar))) );
printf( "Cube: " );
printf( "%s\n", Vec_StrArray(vStr) );
printf( "Mint: " );
Vec_IntForEachEntry( vLits, iLit, n )
printf( "%d", !Abc_LitIsCompl(iLit) );
printf( "\n" );
}
// expand the values
if ( fCanon )
status = Bmc_CollapseExpandCanon( pSat[1], vLits, vNums, vCube, nBTLimit );
else
status = Bmc_CollapseExpand( pSat[1], vLits, vNums, vCube, nBTLimit );
if ( status < 0 )
{
Vec_StrFreeP( &vSop );
goto cleanup; // timeout
}
// collect cube
Vec_StrPop( vSop );
Start = Vec_StrSize( vSop );
Vec_StrFillExtra( vSop, Start + nVars + 4, '-' );
Vec_StrWriteEntry( vSop, Start + nVars + 0, ' ' );
Vec_StrWriteEntry( vSop, Start + nVars + 1, (char)(fCompl ? '0' : '1') );
Vec_StrWriteEntry( vSop, Start + nVars + 2, '\n' );
Vec_StrWriteEntry( vSop, Start + nVars + 3, '\0' );
Vec_IntClear( vCube );
Vec_IntForEachEntry( vNums, iVar, n )
Vec_IntPush( vCube, Abc_LitNot(Vec_IntEntry(vLits, iVar)) );
{
iLit = Vec_IntEntry( vLits, iVar );
Vec_IntPush( vCube, Abc_LitNot(iLit) );
Vec_StrWriteEntry( vSop, Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
}
if ( fVerbose )
printf( "Cube %4d: %s", Count, Vec_StrArray(vSop) + Start );
Count++;
// add cube
status = sat_solver_addclause( pSat[0], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
if ( status == 0 )
break;
}
printf( "Finished enumerating %d assignments.\n", Count );
// cleanup
//printf( "Finished enumerating %d assignments.\n", Count );
cleanup:
Vec_IntFree( vVars );
Vec_IntFree( vLits );
Vec_IntFree( vNums );
Vec_IntFree( vCube );
Vec_StrFree( vStr );
sat_solver_delete( pSat[0] );
sat_solver_delete( pSat[1] );
Cnf_DataFree( pCnf );
return 1;
return vSop;
}
Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fVerbose )
{
Vec_Str_t * vSopOn, * vSopOff;
int nCubesOn = ABC_INFINITY;
int nCubesOff = ABC_INFINITY;
vSopOn = Bmc_CollapseOneInt( p, nCubeLim, nBTLimit, fCanon, fVerbose, 0 );
if ( vSopOn )
nCubesOn = Vec_StrCountEntry(vSopOn,'\n');
Gia_ObjFlipFaninC0( Gia_ManPo(p, 0) );
vSopOff = Bmc_CollapseOneInt( p, Abc_MinInt(nCubeLim, nCubesOn), nBTLimit, fCanon, fVerbose, 1 );
Gia_ObjFlipFaninC0( Gia_ManPo(p, 0) );
if ( vSopOff )
nCubesOff = Vec_StrCountEntry(vSopOff,'\n');
if ( vSopOn == NULL )
return vSopOff;
if ( vSopOff == NULL )
return vSopOn;
if ( nCubesOn <= nCubesOff )
{
Vec_StrFree( vSopOff );
return vSopOn;
}
else
{
Vec_StrFree( vSopOn );
return vSopOff;
}
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///