diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-10-17 13:53:48 +0900 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-10-17 13:53:48 +0900 |
commit | c1b4b79e99a5338eb6aaf895711b37c4e69414a6 (patch) | |
tree | 3a6f63bceb0e029c7eb078c47cbd0d95028ecdb7 | |
parent | 1e1d41f3b8d7e52659e6d9f9cbe4b26c0da71a50 (diff) | |
download | abc-c1b4b79e99a5338eb6aaf895711b37c4e69414a6.tar.gz abc-c1b4b79e99a5338eb6aaf895711b37c4e69414a6.tar.bz2 abc-c1b4b79e99a5338eb6aaf895711b37c4e69414a6.zip |
Integrating Glucose into &qbf.
-rw-r--r-- | src/aig/gia/giaQbf.c | 41 | ||||
-rw-r--r-- | src/base/abci/abc.c | 17 | ||||
-rw-r--r-- | src/sat/glucose/AbcGlucose.cpp | 2 | ||||
-rw-r--r-- | src/sat/glucose/AbcGlucose.h | 2 | ||||
-rw-r--r-- | src/sat/glucose/AbcGlucoseCmd.cpp | 2 |
5 files changed, 46 insertions, 18 deletions
diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index 2dfd83fc..5917a3ef 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -22,6 +22,7 @@ #include "sat/cnf/cnf.h" #include "sat/bsat/satStore.h" #include "misc/extra/extra.h" +#include "sat/glucose/AbcGlucose.h" ABC_NAMESPACE_IMPL_START @@ -41,6 +42,7 @@ struct Qbf_Man_t_ int iParVarBeg; // SAT var ID of the first par variable in the ver solver sat_solver * pSatVer; // verification instance sat_solver * pSatSyn; // synthesis instance + bmcg_sat_solver*pSatSynG; // synthesis instance Vec_Int_t * vValues; // variable values Vec_Int_t * vParMap; // parameter mapping Vec_Int_t * vLits; // literals for the SAT solver @@ -284,7 +286,7 @@ void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ) SeeAlso [] ***********************************************************************/ -Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose ) +Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fGlucose, int fVerbose ) { Qbf_Man_t * p; Cnf_Dat_t * pCnf; @@ -300,10 +302,12 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose ) p->iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1; p->pSatVer = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); p->pSatSyn = sat_solver_new(); + p->pSatSynG = fGlucose ? bmcg_sat_solver_start() : NULL; p->vValues = Vec_IntAlloc( Gia_ManPiNum(pGia) ); p->vParMap = Vec_IntStartFull( nPars ); p->vLits = Vec_IntAlloc( nPars ); sat_solver_setnvars( p->pSatSyn, nPars ); + if ( p->pSatSynG ) bmcg_sat_solver_set_nvars( p->pSatSynG, nPars ); Cnf_DataFree( pCnf ); return p; } @@ -311,6 +315,7 @@ void Gia_QbfFree( Qbf_Man_t * p ) { sat_solver_delete( p->pSatVer ); sat_solver_delete( p->pSatSyn ); + if ( p->pSatSynG ) bmcg_sat_solver_stop( p->pSatSynG ); Vec_IntFree( p->vLits ); Vec_IntFree( p->vValues ); Vec_IntFree( p->vParMap ); @@ -481,6 +486,21 @@ int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof ) return 0; return 1; } +int Gia_QbfAddCofactorG( Qbf_Man_t * p, Gia_Man_t * pCof ) +{ + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 1, 0, 0 ); + int i, iFirstVar = pCnf->nVars - Gia_ManPiNum(pCof); //-1 + pCnf->pMan = NULL; + Cnf_SpecialDataLift( pCnf, bmcg_sat_solver_varnum(p->pSatSynG), iFirstVar, iFirstVar + Gia_ManPiNum(p->pGia) ); + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !bmcg_sat_solver_addclause( p->pSatSynG, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) + { + Cnf_DataFree( pCnf ); + return 0; + } + Cnf_DataFree( pCnf ); + return 1; +} /**Function************************************************************* @@ -498,16 +518,16 @@ void Gia_QbfOnePattern( Qbf_Man_t * p, Vec_Int_t * vValues ) int i; Vec_IntClear( vValues ); for ( i = 0; i < p->nPars; i++ ) - Vec_IntPush( vValues, sat_solver_var_value(p->pSatSyn, i) ); + Vec_IntPush( vValues, p->pSatSynG ? bmcg_sat_solver_read_cex_varvalue(p->pSatSynG, i) : sat_solver_var_value(p->pSatSyn, i) ); } void Gia_QbfPrint( Qbf_Man_t * p, Vec_Int_t * vValues, int Iter ) { printf( "%5d : ", Iter ); assert( Vec_IntSize(vValues) == p->nVars ); Vec_IntPrintBinary( vValues ); printf( " " ); - printf( "Var = %6d ", sat_solver_nvars(p->pSatSyn) ); - printf( "Cla = %6d ", sat_solver_nclauses(p->pSatSyn) ); - printf( "Conf = %6d ", sat_solver_nconflicts(p->pSatSyn) ); + printf( "Var = %6d ", p->pSatSynG ? bmcg_sat_solver_varnum(p->pSatSynG) : sat_solver_nvars(p->pSatSyn) ); + printf( "Cla = %6d ", p->pSatSynG ? bmcg_sat_solver_clausenum(p->pSatSynG) : sat_solver_nclauses(p->pSatSyn) ); + printf( "Conf = %6d ", p->pSatSynG ? bmcg_sat_solver_conflictnum(p->pSatSynG) : sat_solver_nconflicts(p->pSatSyn) ); Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); } @@ -601,9 +621,9 @@ void Gia_QbfLearnConstraint( Qbf_Man_t * p, Vec_Int_t * vValues ) SeeAlso [] ***********************************************************************/ -int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fVerbose ) +int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fGlucose, int fVerbose ) { - Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fVerbose ); + Qbf_Man_t * p = Gia_QbfAlloc( pGia, nPars, fGlucose, fVerbose ); Gia_Man_t * pCof; int i, status, RetValue = 0; abctime clk; @@ -618,12 +638,15 @@ int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, i // generate next constraint assert( Vec_IntSize(p->vValues) == p->nVars ); pCof = Gia_QbfCofactor( pGia, nPars, p->vValues, p->vParMap ); - status = Gia_QbfAddCofactor( p, pCof ); + status = p->pSatSynG ? Gia_QbfAddCofactorG( p, pCof ) : Gia_QbfAddCofactor( p, pCof ); Gia_ManStop( pCof ); if ( status == 0 ) { RetValue = 1; break; } // synthesize next assignment clk = Abc_Clock(); - status = sat_solver_solve( p->pSatSyn, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 ); + if ( p->pSatSynG ) + status = bmcg_sat_solver_solve( p->pSatSynG, NULL, 0 ); + else + status = sat_solver_solve( p->pSatSyn, NULL, NULL, (ABC_INT64_T)nConfLimit, 0, 0, 0 ); p->clkSat += Abc_Clock() - clk; if ( fVerbose ) Gia_QbfPrint( p, p->vValues, i ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9dc7b285..92394196 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -25173,7 +25173,7 @@ usage: Abc_Print( -2, "\t-u : toggle performing structural OR-decomposition [default = %s]\n", fOrDecomp? "yes": "not" ); Abc_Print( -2, "\t-r : toggle disabling periodic restarts [default = %s]\n", pPars->fNoRestarts? "yes": "no" ); Abc_Print( -2, "\t-s : toggle using Satoko instead of build-in MiniSAT [default = %s]\n", pPars->fUseSatoko? "yes": "no" ); - Abc_Print( -2, "\t-g : toggle using Glucose instead of build-in MiniSAT [default = %s]\n",pPars->fUseGlucose? "yes": "no" ); + Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n",pPars->fUseGlucose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -40402,7 +40402,7 @@ usage: Abc_Print( -2, "\t-F num : the maximum number of timeframes [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-A num : the number of additional frames to unroll [default = %d]\n", pPars->nFramesAdd ); Abc_Print( -2, "\t-T num : approximate timeout in seconds [default = %d]\n", pPars->nTimeOut ); - Abc_Print( -2, "\t-g : toggle using Glucose 3.0 [default = %s]\n", pPars->fUseGlucose? "Glucose" : "Satoko" ); + Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fUseGlucose? "Glucose" : "Satoko" ); Abc_Print( -2, "\t-e : toggle using variable eliminatation [default = %s]\n", pPars->fUseEliminate?"yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing information about unfolding [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); @@ -41017,15 +41017,16 @@ usage: int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ); - extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fVerbose ); + extern int Gia_QbfSolve( Gia_Man_t * pGia, int nPars, int nIterLimit, int nConfLimit, int nTimeOut, int fGlucose, int fVerbose ); int c, nPars = -1; int nIterLimit = 0; int nConfLimit = 0; int nTimeOut = 0; int fDumpCnf = 0; + int fGlucose = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PICTdvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PICTdgvh" ) ) != EOF ) { switch ( c ) { @@ -41076,6 +41077,9 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': fDumpCnf ^= 1; break; + case 'g': + fGlucose ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -41108,17 +41112,18 @@ int Abc_CommandAbc9Qbf( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fDumpCnf ) Gia_QbfDumpFile( pAbc->pGia, nPars ); else - Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, fVerbose ); + Gia_QbfSolve( pAbc->pGia, nPars, nIterLimit, nConfLimit, nTimeOut, fGlucose, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: &qbf [-PICT num] [-dvh]\n" ); + Abc_Print( -2, "usage: &qbf [-PICT num] [-dgvh]\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", nIterLimit ); Abc_Print( -2, "\t-C num : conflict limit per problem [default = %d]\n", nConfLimit ); Abc_Print( -2, "\t-T num : global timeout [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-d : toggle dumping QDIMACS file instead of solving [default = %s]\n", fDumpCnf? "yes": "no" ); + Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", fGlucose? "yes": "no" ); 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; diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index 84927daa..60171155 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [SAT solver Glucose 3.0.] + PackageName [SAT solver Glucose 3.0 by Gilles Audemard and Laurent Simon.] Synopsis [Interface to Glucose.] diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h index 3484c008..e2c05e1b 100644 --- a/src/sat/glucose/AbcGlucose.h +++ b/src/sat/glucose/AbcGlucose.h @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [SAT solver Glucose 3.0.] + PackageName [SAT solver Glucose 3.0 by Gilles Audemard and Laurent Simon.] Synopsis [Interface to Glucose.] diff --git a/src/sat/glucose/AbcGlucoseCmd.cpp b/src/sat/glucose/AbcGlucoseCmd.cpp index 74a58c33..404685cf 100644 --- a/src/sat/glucose/AbcGlucoseCmd.cpp +++ b/src/sat/glucose/AbcGlucoseCmd.cpp @@ -4,7 +4,7 @@ SystemName [ABC: Logic synthesis and verification system.] - PackageName [SAT solver Glucose 3.0.] + PackageName [SAT solver Glucose 3.0 by Gilles Audemard and Laurent Simon.] Synopsis [Interface to Glucose.] |