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

Adding several command-line arguments to 'dsat'.

This commit is contained in:
Alan Mishchenko 2012-07-09 19:24:39 -07:00
parent 22dc498374
commit 637736827a
11 changed files with 89 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/giaAig.c
View File

@ -572,7 +572,7 @@ int Gia_ManSolveSat( Gia_Man_t * p )
Aig_Man_t * pNew;
int RetValue;//, clk = clock();
pNew = Gia_ManToAig( p, 0 );
RetValue = Fra_FraigSat( pNew, 10000000, 0, 1, 1, 0, 0 );
RetValue = Fra_FraigSat( pNew, 10000000, 0, 0, 0, 0, 1, 1, 0, 0 );
if ( RetValue == 0 )
{
Gia_Obj_t * pObj;

4
src/aig/ivy/ivyFraig.c
View File

@ -2923,14 +2923,14 @@ printf( "***************\n" );
***********************************************************************/
int Ivy_FraigCheckCone( Ivy_FraigMan_t * pGlo, Ivy_Man_t * p, Ivy_Obj_t * pObj1, Ivy_Obj_t * pObj2, int nConfLimit )
{
extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
Vec_Int_t * vLeaves;
Aig_Man_t * pMan;
Aig_Obj_t * pObj;
int i, RetValue;
vLeaves = Vec_IntAlloc( 100 );
pMan = Ivy_FraigExtractCone( p, pObj1, pObj2, vLeaves );
RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 0, 1 );
RetValue = Fra_FraigSat( pMan, nConfLimit, 0, 0, 0, 0, 0, 0, 0, 1 );
if ( RetValue == 0 )
{
int Counter = 0;

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

@ -17692,7 +17692,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
int fPartition;
int fMiter;
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
extern int Abc_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose );
pNtk = Abc_FrameReadNtk(pAbc);
@ -17797,7 +17797,7 @@ int Abc_CommandDCec( Abc_Frame_t * pAbc, int argc, char ** argv )
// perform equivalence checking
if ( fSat && fMiter )
Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, 0, fVerbose );
Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, 0, 0, 0, 0, fVerbose );
else
Abc_NtkDarCec( pNtk1, pNtk2, nConfLimit, fPartition, fVerbose );
@ -18943,10 +18943,13 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
int fNewSolver;
int fVerbose;
int nConfLimit;
int nStartLearned;
int nDeltaLearned;
int nRatioLearned;
int nInsLimit;
clock_t clk;
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
// set defaults
fAlignPol = 0;
fAndOuts = 0;
@ -18954,8 +18957,11 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
fVerbose = 0;
nConfLimit = 0;
nInsLimit = 0;
nStartLearned = 0;
nDeltaLearned = 0;
nRatioLearned = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CIpanvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CISDRpanvh" ) ) != EOF )
{
switch ( c )
{
@ -18981,6 +18987,39 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nInsLimit < 0 )
goto usage;
break;
case 'S':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
goto usage;
}
nStartLearned = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nStartLearned < 0 )
goto usage;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
goto usage;
}
nDeltaLearned = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nDeltaLearned < 0 )
goto usage;
break;
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
goto usage;
}
nRatioLearned = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nRatioLearned < 0 )
goto usage;
break;
case 'p':
fAlignPol ^= 1;
break;
@ -19024,7 +19063,7 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
}
clk = clock();
RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose );
RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, nStartLearned, nDeltaLearned, nRatioLearned, fAlignPol, fAndOuts, fNewSolver, fVerbose );
// verify that the pattern is correct
if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
{
@ -19046,11 +19085,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: dsat [-C num] [-I num] [-panvh]\n" );
Abc_Print( -2, "usage: dsat [-CISDR num] [-panvh]\n" );
Abc_Print( -2, "\t solves the combinational miter using SAT solver MiniSat-1.14\n" );
Abc_Print( -2, "\t derives CNF from the current network and leave it unchanged\n" );
Abc_Print( -2, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
Abc_Print( -2, "\t-I num : limit on the number of inspections [default = %d]\n", nInsLimit );
Abc_Print( -2, "\t-S num : starting value for learned clause removal [default = %d]\n", nStartLearned );
Abc_Print( -2, "\t-D num : delta value for learned clause removal [default = %d]\n", nDeltaLearned );
Abc_Print( -2, "\t-R num : ratio percentage for learned clause removal [default = %d]\n", nRatioLearned );
Abc_Print( -2, "\t-p : alighn polarity of SAT variables [default = %s]\n", fAlignPol? "yes": "no" );
Abc_Print( -2, "\t-a : toggle ANDing/ORing of miter outputs [default = %s]\n", fAndOuts? "ANDing": "ORing" );
Abc_Print( -2, "\t-n : toggle using new solver [default = %s]\n", fNewSolver? "yes": "no" );

6
src/base/abci/abcDar.c
View File

@ -1403,7 +1403,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName, int fFastAlgo,
SeeAlso []
***********************************************************************/
int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose )
{
Aig_Man_t * pMan;
int RetValue;//, clk = clock();
@ -1411,7 +1411,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit
assert( Abc_NtkLatchNum(pNtk) == 0 );
// assert( Abc_NtkPoNum(pNtk) == 1 );
pMan = Abc_NtkToDar( pNtk, 0, 0 );
RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose );
RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, nStartLearned, nDeltaLearned, nRatioLearned, fAlignPol, fAndOuts, fNewSolver, fVerbose );
pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL;
Aig_ManStop( pMan );
return RetValue;
@ -2056,7 +2056,7 @@ int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars, Aig_Man
if ( Aig_ManRegNum(pTemp) == 0 )
{
pTemp->pSeqModel = NULL;
RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0 );
RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 0, 0, 0, 0, 0, 0, 0, 0 );
if ( pTemp->pData )
pTemp->pSeqModel = Abc_CexCreate( Aig_ManRegNum(pMan), Saig_ManPiNum(pMan), (int *)pTemp->pData, 0, i, 1 );
// pNtk->pModel = pTemp->pData, pTemp->pData = NULL;

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

@ -533,7 +533,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
// if SAT only, solve without iteration
// RetValue = Abc_NtkMiterSat( pNtk, 2*(ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, NULL, NULL );
pMan2 = Abc_NtkToDar( pNtk, 0, 0 );
RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 1, 0, 0, 0 );
RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
Aig_ManStop( pMan2 );
// pNtk->pModel = Aig_ManReleaseData( pMan2 );
@ -583,7 +583,7 @@ int Abc_NtkIvyProve( Abc_Ntk_t ** ppNtk, void * pPars )
Ioa_WriteAiger( pMan2, pFileName, 0, 0 );
printf( "Intermediate reduced miter is written into file \"%s\".\n", pFileName );
}
RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, pParams->fVerbose );
RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, 0, 0, 0, pParams->fVerbose );
pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL;
Aig_ManStop( pMan2 );
}

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

@ -41,7 +41,7 @@ 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 fNewSolver, int fVerbose );
extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -101,7 +101,7 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose )
// solve the synthesis instance
clkS = clock();
// RetValue = Abc_NtkMiterSat( pNtkSyn, 0, 0, 0, NULL, NULL );
RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0, 0 );
RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
clkS = clock() - clkS;
if ( RetValue == 0 )
Abc_NtkModelToVector( pNtkSyn, vPiValues );

2
src/proof/fra/fra.h
View File

@ -285,7 +285,7 @@ static inline int Fra_ImpCreate( int Left, int Right )
////////////////////////////////////////////////////////////////////////
/*=== fraCec.c ========================================================*/
extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose );
extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
extern int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose );
/*=== fraClass.c ========================================================*/

19
src/proof/fra/fraCec.c
View File

@ -44,7 +44,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose )
int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nStartLearned, int nDeltaLearned, int nRatioLearned, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose )
{
if ( fNewSolver )
{
@ -75,7 +75,6 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
return 1;
}
if ( fAndOuts )
{
// assert each output independently
@ -182,6 +181,14 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
return 1;
}
if ( nStartLearned )
pSat->nLearntStart = nStartLearned;
if ( nDeltaLearned )
pSat->nLearntDelta = nDeltaLearned;
if ( nRatioLearned )
pSat->nLearntRatio = nRatioLearned;
if ( fVerbose )
pSat->fVerbose = fVerbose;
if ( fAndOuts )
{
@ -225,8 +232,8 @@ int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimi
// solve the miter
clk = clock();
if ( fVerbose )
pSat->verbosity = 1;
// if ( fVerbose )
// pSat->verbosity = 1;
status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_Undef )
{
@ -303,7 +310,7 @@ int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
// if SAT only, solve without iteration
clk = clock();
RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 1, 0, 0, 0 );
RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
if ( fVerbose )
{
printf( "Initial SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
@ -371,7 +378,7 @@ ABC_PRT( "Time", clock() - clk );
if ( RetValue == -1 )
{
clk = clock();
RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 1, 0, 0, 0 );
RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
if ( fVerbose )
{
printf( "Final SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) );

4
src/proof/int/intContain.c
View File

@ -57,7 +57,7 @@ int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
RetValue = Fra_FraigMiterStatus( pAigTemp );
Aig_ManStop( pAigTemp );
// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0 );
// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0, 0, 0 );
}
assert( RetValue != -1 );
Aig_ManStop( pMiter );
@ -88,7 +88,7 @@ int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld )
pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
RetValue = Fra_FraigMiterStatus( pAigTemp );
Aig_ManStop( pAigTemp );
// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0 );
// RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0, 0, 0, 0 );
}
assert( RetValue != -1 );
Aig_ManStop( pMiter );

18
src/sat/bsat/satSolver.c
View File

@ -29,9 +29,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
ABC_NAMESPACE_IMPL_START
//#define LEARNT_MAX_START 0
#define LEARNT_MAX_START 20000
#define LEARNT_MAX_INCRE 1000
//#define LEARNT_MAX_START_DEFAULT 0
#define LEARNT_MAX_START_DEFAULT 20000
#define LEARNT_MAX_INCRE_DEFAULT 1000
#define LEARNT_MAX_RATIO_DEFAULT 50
#define SAT_USE_ANALYZE_FINAL
@ -921,7 +922,11 @@ sat_solver* sat_solver_new(void)
s->hBinary = Sat_MemAppend( &s->Mem, NULL, 2, 0 );
s->binary = clause_read( s, s->hBinary );
s->nLearntMax = LEARNT_MAX_START;
s->nLearntStart = LEARNT_MAX_START_DEFAULT; // starting learned clause limit
s->nLearntDelta = LEARNT_MAX_INCRE_DEFAULT; // delta of learned clause limit
s->nLearntRatio = LEARNT_MAX_RATIO_DEFAULT; // ratio of learned clause limit
s->nLearntMax = s->nLearntStart;
// initialize vectors
veci_new(&s->order);
@ -1188,7 +1193,7 @@ void sat_solver_reducedb(sat_solver* s)
s->nDBreduces++;
// printf( "Calling reduceDB with %d learned clause limit.\n", s->nLearntMax );
s->nLearntMax = LEARNT_MAX_START + LEARNT_MAX_INCRE * s->nDBreduces;
s->nLearntMax = s->nLearntStart + s->nLearntDelta * s->nDBreduces;
// return;
// create sorting values
@ -1205,7 +1210,7 @@ void sat_solver_reducedb(sat_solver* s)
CounterStart = nLearnedOld - (s->nLearntMax / 20);
// preserve 3/4 of most active clauses
nSelected = nLearnedOld*5/10;
nSelected = nLearnedOld*s->nLearntRatio/100;
// find non-decreasing permutation
pPerm = Abc_MergeSortCost( pSortValues, nLearnedOld );
@ -1494,6 +1499,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit
lbool status = l_Undef;
lit* i;
printf( "Running SAT solver with parameters %d and %d and %d.\n", s->nLearntStart, s->nLearntDelta, s->nLearntRatio );
////////////////////////////////////////////////
if ( s->fSolved )
{

3
src/sat/bsat/satSolver.h
View File

@ -141,6 +141,9 @@ struct sat_solver_t
int fVerbose;
stats_t stats;
int nLearntStart; // starting learned clause limit
int nLearntDelta; // delta of learned clause limit
int nLearntRatio; // ratio percentage of learned clauses
int nLearntMax; // max number of learned clauses
int nDBreduces; // number of DB reductions
// veci learned; // contain learnt clause handles