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

Improvements to the QBF solver.

This commit is contained in:
Alan Mishchenko 2011-10-25 17:22:33 +08:00
parent a8e1ba40b9
commit f7fd329787
3 changed files with 38 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -11016,14 +11016,16 @@ int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c;
int nPars;
int nIters;
int fVerbose;
extern void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int fVerbose );
extern void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nIters, int fVerbose );
// set defaults
nPars = -1;
nIters = -1;
fVerbose = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Pvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "PIvh" ) ) != EOF )
{
switch ( c )
{
@ -11038,6 +11040,17 @@ int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nPars < 0 )
goto usage;
break;
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
goto usage;
}
nIters = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nIters < 0 )
goto usage;
break;
case 'v':
fVerbose ^= 1;
break;
@ -11068,19 +11081,20 @@ int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1;
}
if ( Abc_NtkIsStrash(pNtk) )
Abc_NtkQbf( pNtk, nPars, fVerbose );
Abc_NtkQbf( pNtk, nPars, nIters, fVerbose );
else
{
pNtk = Abc_NtkStrash( pNtk, 0, 1, 0 );
Abc_NtkQbf( pNtk, nPars, fVerbose );
Abc_NtkQbf( pNtk, nPars, nIters, fVerbose );
Abc_NtkDelete( pNtk );
}
return 0;
usage:
Abc_Print( -2, "usage: qbf [-P num] [-vh]\n" );
Abc_Print( -2, "usage: qbf [-PI num] [-vh]\n" );
Abc_Print( -2, "\t solves QBF problem EpVxM(p,x)\n" );
Abc_Print( -2, "\t-P num : number of parameters p (should be the first PIs) [default = %d]\n", nPars );
Abc_Print( -2, "\t-I num : quit after the given iteration even if unsolved [default = %d]\n", nIters );
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;

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

@ -442,8 +442,8 @@ void Abc_GenFpga( char * pFileName, int nLutSize, int nLuts, int nVars )
fprintf( pFile, ".inputs" );
for ( i = 0; i < nParsLut; i++ )
{
if ( i % (1 << nLutSize) == 0 && i != (nLuts - 1) * (1 << nLutSize) )
continue;
// if ( i % (1 << nLutSize) == 0 && i != (nLuts - 1) * (1 << nLutSize) )
// continue;
fprintf( pFile, " pl%02d", i );
}
fprintf( pFile, "\n" );

19
src/base/abci/abcQbf.c
View File

@ -41,6 +41,8 @@ static void Abc_NtkVectorClearVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int
static void Abc_NtkVectorPrintPars( Vec_Int_t * vPiValues, int nPars );
static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int nPars );
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@ -58,7 +60,7 @@ static void Abc_NtkVectorPrintVars( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues, int
SeeAlso []
***********************************************************************/
void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int fVerbose )
void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose )
{
Abc_Ntk_t * pNtkVer, * pNtkSyn, * pNtkSyn2, * pNtkTemp;
Vec_Int_t * vPiValues;
@ -74,6 +76,15 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int fVerbose )
// initialize the synthesized network with 0000-combination
vPiValues = Vec_IntStart( Abc_NtkPiNum(pNtk) );
// create random init value
{
int i;
srand( time(NULL) );
for ( i = nPars; i < Abc_NtkPiNum(pNtk); i++ )
Vec_IntWriteEntry( vPiValues, i, rand() & 1 );
}
Abc_NtkVectorClearPars( vPiValues, nPars );
pNtkSyn = Abc_NtkMiterCofactor( pNtk, vPiValues );
if ( fVerbose )
@ -147,6 +158,8 @@ clkV = clock() - clkV;
ABC_PRT( "Syn", clkS );
// ABC_PRT( "Ver", clkV );
}
if ( nIters+1 == nItersMax )
break;
}
Abc_NtkDelete( pNtkSyn );
// report the results
@ -159,7 +172,9 @@ clkV = clock() - clkV;
}
else if ( nIters == nIterMax )
printf( "Unsolved after %d interations. ", nIters );
else
else if ( nIters == nItersMax )
printf( "Quit after %d interatios. ", nItersMax );
else
printf( "Implementation does not exist. " );
ABC_PRT( "Total runtime", clock() - clkTotal );
Vec_IntFree( vPiValues );