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

Integrating Glucose into bmc3 -g.

This commit is contained in:
Alan Mishchenko 2017-09-06 19:56:53 -07:00
parent b1bf802fda
commit 97dd6019bf
8 changed files with 87 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -1943,6 +1943,10 @@ SOURCE=.\src\sat\bmc\bmcBmcAnd.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcBmcG.c
# End Source File
# Begin Source File
SOURCE=.\src\sat\bmc\bmcBmci.c
# End Source File
# Begin Source File

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

@ -24739,7 +24739,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Saig_ParBmcSetDefaultParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursvzh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "SFTHGCDJIPQRLWaxdursgvzh" ) ) != EOF )
{
switch ( c )
{
@ -24911,6 +24911,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
case 's':
pPars->fUseSatoko ^= 1;
break;
case 'g':
pPars->fUseGlucose ^= 1;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -24977,7 +24980,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axdursvzh]\n" );
Abc_Print( -2, "usage: bmc3 [-SFTHGCDJIPQR num] [-LW file] [-axdursgvzh]\n" );
Abc_Print( -2, "\t performs bounded model checking with dynamic unrolling\n" );
Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
@ -24999,6 +25002,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-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");

1
src/sat/bmc/bmc.h
View File

@ -62,6 +62,7 @@ struct Saig_ParBmc_t_
int fSkipRand; // skip random decisions
int fNoRestarts; // disables periodic restarts
int fUseSatoko; // enables using Satoko
int fUseGlucose; // enables using Glucose 3.0
int nLearnedStart; // starting learned clause limit
int nLearnedDelta; // delta of learned clause limit
int nLearnedPerce; // ratio of learned clause limit

66
src/sat/bmc/bmcBmc3.c
View File

@ -22,6 +22,7 @@
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "sat/satoko/satoko.h"
#include "sat/glucose/AbcGlucose.h"
#include "misc/vec/vecHsh.h"
#include "misc/vec/vecWec.h"
#include "bmc.h"
@ -62,6 +63,7 @@ struct Gia_ManBmc_t_
// SAT solver
sat_solver * pSat; // SAT solver
satoko_t * pSat2; // SAT solver
bmcg_sat_solver * pSat3; // SAT solver
int nSatVars; // SAT variables
int nObjNums; // SAT objects
int nWordNum; // unsigned words for ternary simulation
@ -716,7 +718,7 @@ Vec_Int_t * Saig_ManBmcComputeMappingRefs( Aig_Man_t * p, Vec_Int_t * vMap )
SeeAlso []
***********************************************************************/
Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko )
Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLimit, int fUseSatoko, int fUseGlucose )
{
Gia_ManBmc_t * p;
Aig_Obj_t * pObj;
@ -754,6 +756,13 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig, int nTimeOutOne, int nConfLi
satoko_configure(p->pSat2, &opts);
satoko_setnvars(p->pSat2, 1000);
}
else if ( fUseGlucose )
{
//opts.conf_limit = nConfLimit;
p->pSat3 = bmcg_sat_solver_start();
for ( i = 0; i < 1000; i++ )
bmcg_sat_solver_addvar( p->pSat3 );
}
else
{
p->pSat = sat_solver_new();
@ -797,9 +806,9 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
p->pSat ? p->pSat->nLearntDelta : 0,
p->pSat ? p->pSat->nLearntRatio : 0,
p->pSat ? p->pSat->nDBreduces : 0,
p->pSat ? sat_solver_nvars(p->pSat) : satoko_varnum(p->pSat2),
p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2),
nUsedVars,
100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : satoko_varnum(p->pSat2)) );
100.0*nUsedVars/(p->pSat ? sat_solver_nvars(p->pSat) : p->pSat3 ? bmcg_sat_solver_varnum(p->pSat3) : satoko_varnum(p->pSat2)) );
Abc_Print( 1, "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. UniProps = %d.\n",
p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nUniProps );
}
@ -820,6 +829,7 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
Vec_PtrFreeFree( p->vTerInfo );
if ( p->pSat ) sat_solver_delete( p->pSat );
if ( p->pSat2 ) satoko_destroy( p->pSat2 );
if ( p->pSat3 ) bmcg_sat_solver_stop( p->pSat3 );
ABC_FREE( p->pTime4Outs );
Vec_IntFree( p->vData );
Hsh_IntManStop( p->vHash );
@ -1014,6 +1024,11 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits
if ( !satoko_add_clause( p->pSat2, ClaLits, nClaLits ) )
assert( 0 );
}
else if ( p->pSat3 )
{
if ( !bmcg_sat_solver_addclause( p->pSat3, ClaLits, nClaLits ) )
assert( 0 );
}
else
{
if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) )
@ -1267,6 +1282,11 @@ int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
// extend the SAT solver
if ( p->pSat2 )
satoko_setnvars( p->pSat2, p->nSatVars );
else if ( p->pSat3 )
{
for ( i = bmcg_sat_solver_varnum(p->pSat3); i < p->nSatVars; i++ )
bmcg_sat_solver_addvar( p->pSat3 );
}
else
sat_solver_setnvars( p->pSat, p->nSatVars );
return Lit;
@ -1384,6 +1404,11 @@ Abc_Cex_t * Saig_ManGenerateCex( Gia_ManBmc_t * p, int f, int i )
if ( iLit != ~0 && satoko_read_cex_varvalue(p->pSat2, lit_var(iLit)) )
Abc_InfoSetBit( pCex->pData, iBit + k );
}
else if ( p->pSat3 )
{
if ( iLit != ~0 && bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(iLit)) )
Abc_InfoSetBit( pCex->pData, iBit + k );
}
else
{
if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
@ -1413,6 +1438,11 @@ int Saig_ManCallSolver( Gia_ManBmc_t * p, int Lit )
return l_True;
if ( p->pSat2 )
return satoko_solve_assumptions_limit( p->pSat2, &Lit, 1, p->pPars->nConfLimit );
else if ( p->pSat3 )
{
bmcg_sat_solver_set_conflict_budget( p->pSat3, p->pPars->nConfLimit );
return bmcg_sat_solver_solve( p->pSat3, &Lit, 1 );
}
else
return sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
}
@ -1450,7 +1480,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
nTimeToStop = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
// create BMC manager
p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko );
p = Saig_Bmc3ManStart( pAig, pPars->nTimeOutOne, pPars->nConfLimit, pPars->fUseSatoko, pPars->fUseGlucose );
p->pPars = pPars;
if ( p->pSat )
{
@ -1462,6 +1492,11 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
p->pSat->RunId = p->pPars->RunId;
p->pSat->pFuncStop = p->pPars->pFuncStop;
}
else if ( p->pSat3 )
{
// satoko_set_runid(p->pSat3, p->pPars->RunId);
// satoko_set_stop_func(p->pSat3, p->pPars->pFuncStop);
}
else
{
satoko_set_runid(p->pSat2, p->pPars->RunId);
@ -1483,6 +1518,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
{
if ( p->pSat2 )
satoko_set_runtime_limit( p->pSat2, nTimeToStop );
else if ( p->pSat3 )
bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop );
else
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
}
@ -1614,6 +1651,8 @@ clkOther += Abc_Clock() - clk2;
clkOne = Abc_Clock();
if ( p->pSat2 )
satoko_set_runtime_limit( p->pSat2, p->pTime4Outs[i] + Abc_Clock() );
else if ( p->pSat3 )
bmcg_sat_solver_set_runtime_limit( p->pSat3, p->pTime4Outs[i] + Abc_Clock() );
else
sat_solver_set_runtime_limit( p->pSat, p->pTime4Outs[i] + Abc_Clock() );
}
@ -1641,6 +1680,8 @@ nTimeUnsat += clkSatRun;
Lit = lit_neg( Lit );
if ( p->pSat2 )
status = satoko_add_clause( p->pSat2, &Lit, 1 );
else if ( p->pSat3 )
status = bmcg_sat_solver_addclause( p->pSat3, &Lit, 1 );
else
status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
assert( status );
@ -1672,8 +1713,8 @@ nTimeSat += clkSatRun;
{
Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : satoko_clausenum(p->pSat2)) );
Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) );
Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) );
Abc_Print( 1, "Conf =%7.0f. ", (double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
// Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
Abc_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
// ABC_PRT( "Time", Abc_Clock() - clk );
@ -1721,6 +1762,8 @@ nTimeSat += clkSatRun;
{
if ( p->pSat2 )
satoko_set_runtime_limit( p->pSat2, nTimeToStop );
else if ( p->pSat3 )
bmcg_sat_solver_set_runtime_limit( p->pSat3, nTimeToStop );
else
sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
}
@ -1740,6 +1783,11 @@ nTimeSat += clkSatRun;
if ( satoko_read_cex_varvalue(p->pSat2, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
continue;
}
else if ( p->pSat3 )
{
if ( bmcg_sat_solver_read_cex_varvalue(p->pSat3, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
continue;
}
else
{
if ( sat_solver_var_value(p->pSat, lit_var(Lit)) == Abc_LitIsCompl(Lit) )
@ -1780,7 +1828,7 @@ nTimeUndec += clkSatRun;
}
if ( pPars->fVerbose )
{
if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) > 1 )
if ( fFirst == 1 && f > 0 && (p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) > 1 )
{
fFirst = 0;
// Abc_Print( 1, "Outputs of frames up to %d are trivially UNSAT.\n", f );
@ -1788,8 +1836,8 @@ nTimeUndec += clkSatRun;
Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
// Abc_Print( 1, "Used =%8.0f. ", (double)sat_solver_count_usedvars(p->pSat) );
Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : satoko_clausenum(p->pSat2)) );
Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : satoko_conflictnum(p->pSat2)) );
Abc_Print( 1, "Cla =%9.0f. ", (double)(p->pSat ? p->pSat->stats.clauses : p->pSat3 ? bmcg_sat_solver_clausenum(p->pSat3) : satoko_clausenum(p->pSat2)) );
Abc_Print( 1, "Conf =%7.0f. ",(double)(p->pSat ? p->pSat->stats.conflicts : p->pSat3 ? bmcg_sat_solver_conflictnum(p->pSat3) : satoko_conflictnum(p->pSat2)) );
// Abc_Print( 1, "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
Abc_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
if ( pPars->fSolveAll )

15
src/sat/glucose/AbcGlucose.cpp
View File

@ -188,6 +188,21 @@ void bmcg_sat_solver_setstop(bmcg_sat_solver* s, int * pstop)
glucose_solver_setstop((Gluco::Solver*)s, pstop);
}
abctime bmcg_sat_solver_set_runtime_limit(bmcg_sat_solver* s, abctime Limit)
{
abctime nRuntimeLimit = ((Gluco::Solver*)s)->nRuntimeLimit;
((Gluco::Solver*)s)->nRuntimeLimit = Limit;
return nRuntimeLimit;
}
void bmcg_sat_solver_set_conflict_budget(bmcg_sat_solver* s, int Limit)
{
if ( Limit > 0 )
((Gluco::Solver*)s)->setConfBudget( (int64_t)Limit );
else
((Gluco::Solver*)s)->budgetOff();
}
int bmcg_sat_solver_varnum(bmcg_sat_solver* s)
{
return ((Gluco::Solver*)s)->nVars();

2
src/sat/glucose/AbcGlucose.h
View File

@ -73,6 +73,8 @@ extern int bmcg_sat_solver_solve( bmcg_sat_solver* s, int * plits,
extern int bmcg_sat_solver_addvar( bmcg_sat_solver* s );
extern int bmcg_sat_solver_read_cex_varvalue( bmcg_sat_solver* s, int );
extern void bmcg_sat_solver_setstop( bmcg_sat_solver* s, int * );
extern abctime bmcg_sat_solver_set_runtime_limit(bmcg_sat_solver* s, abctime Limit);
extern void bmcg_sat_solver_set_conflict_budget(bmcg_sat_solver* s, int Limit);
extern int bmcg_sat_solver_varnum(bmcg_sat_solver* s);
extern int bmcg_sat_solver_clausenum(bmcg_sat_solver* s);
extern int bmcg_sat_solver_learntnum(bmcg_sat_solver* s);

1
src/sat/glucose/Glucose.cpp
View File

@ -1250,6 +1250,7 @@ printf("c ==================================[ Search Statistics (every %6d confl
while (status == l_Undef){
status = search(0); // the parameter is useless in glucose, kept to allow modifications
if (!withinBudget() || terminate_search_early || (pstop && *pstop)) break;
if (nRuntimeLimit && Abc_Clock() > nRuntimeLimit) break;
curr_restarts++;
}

1
src/sat/glucose/Solver.h
View File

@ -59,6 +59,7 @@ public:
int nCallConfl; // callback will be called every this number of conflicts
bool terminate_search_early; // used to stop the solver early if it as instructed by an external caller
int * pstop; // another callback
uint64_t nRuntimeLimit; // runtime limit
// Problem specification:
//