From d2db956a618fd9be1915a6c66b063c894e540fee Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 25 Nov 2011 18:08:48 -0800 Subject: Started experiments with a new solver. --- src/base/abci/abc.c | 18 ++++++++++++------ src/base/abci/abcDar.c | 6 +++--- src/base/abci/abcIvy.c | 6 +++--- src/base/abci/abcQbf.c | 4 ++-- 4 files changed, 20 insertions(+), 14 deletions(-) (limited to 'src/base/abci') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 32ed17eb..ac0f26dd 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -17038,7 +17038,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 fVerbose ); + 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_NtkDarCec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int fPartition, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); @@ -17143,7 +17143,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, fVerbose ); + Abc_NtkDSat( pNtk1, nConfLimit, nInsLimit, 0, 0, 0, fVerbose ); else Abc_NtkDarCec( pNtk1, pNtk2, nConfLimit, fPartition, fVerbose ); @@ -18250,20 +18250,22 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) int RetValue; int fAlignPol; int fAndOuts; + int fNewSolver; int fVerbose; int nConfLimit; int nInsLimit; int clk; - extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fVerbose ); + extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose ); // set defaults fAlignPol = 0; fAndOuts = 0; + fNewSolver = 0; fVerbose = 0; nConfLimit = 100000; nInsLimit = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CIpavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CIpanvh" ) ) != EOF ) { switch ( c ) { @@ -18295,6 +18297,9 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'a': fAndOuts ^= 1; break; + case 'n': + fNewSolver ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -18329,7 +18334,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, fVerbose ); + RetValue = Abc_NtkDSat( pNtk, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose ); // verify that the pattern is correct if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 ) { @@ -18351,13 +18356,14 @@ int Abc_CommandDSat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: dsat [-C num] [-I num] [-pavh]\n" ); + Abc_Print( -2, "usage: dsat [-C num] [-I 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-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" ); Abc_Print( -2, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index dc090791..0bfd515e 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -1240,7 +1240,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 fVerbose ) +int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fAlignPol, int fAndOuts, int fNewSolver, int fVerbose ) { Aig_Man_t * pMan; int RetValue;//, clk = clock(); @@ -1248,7 +1248,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, fVerbose ); + RetValue = Fra_FraigSat( pMan, nConfLimit, nInsLimit, fAlignPol, fAndOuts, fNewSolver, fVerbose ); pNtk->pModel = (int *)pMan->pData, pMan->pData = NULL; Aig_ManStop( pMan ); return RetValue; @@ -1910,7 +1910,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 ); + RetValue = Fra_FraigSat( pTemp, pPars->nBTLimit, 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; diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 52ac5192..28ff0ee6 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); extern void Aig_ManStop( Aig_Man_t * pMan ); -//extern int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int fFlipBits, int fAndOuts, int fVerbose ); +//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 Ivy_Obj_t * Dec_GraphToNetworkIvy( Ivy_Man_t * pMan, Dec_Graph_t * pGraph ); extern void Ivy_CutComputeAll( Ivy_Man_t * p, int nInputs ); @@ -532,7 +532,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 ); + RetValue = Fra_FraigSat( pMan2, (ABC_INT64_T)pParams->nMiteringLimitStart, (ABC_INT64_T)0, 1, 0, 0, 0 ); pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL; Aig_ManStop( pMan2 ); // pNtk->pModel = Aig_ManReleaseData( pMan2 ); @@ -582,7 +582,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, pParams->fVerbose ); + RetValue = Fra_FraigSat( pMan2, pParams->nMiteringLimitLast, 0, 0, 0, 0, pParams->fVerbose ); pNtk->pModel = (int *)pMan2->pData, pMan2->pData = NULL; Aig_ManStop( pMan2 ); } diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c index 90cc0146..e6395ef3 100644 --- a/src/base/abci/abcQbf.c +++ b/src/base/abci/abcQbf.c @@ -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 fVerbose ); +extern int Abc_NtkDSat( Abc_Ntk_t * pNtk, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, 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 ); + RetValue = Abc_NtkDSat( pNtkSyn, (ABC_INT64_T)0, (ABC_INT64_T)0, 1, 0, 0, 0 ); clkS = clock() - clkS; if ( RetValue == 0 ) Abc_NtkModelToVector( pNtkSyn, vPiValues ); -- cgit v1.2.3