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

Disabling CNF simplification in &bmcs -g.

This commit is contained in:
Alan Mishchenko 2017-09-07 19:37:46 -07:00
parent ba0d855fd4
commit af4c76e21a
4 changed files with 36 additions and 31 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -40120,7 +40120,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-gevwh]\n" );
Abc_Print( -2, "usage: &bmcs [-PCFAT num] [-gvwh]\n" );
Abc_Print( -2, "\t performs bounded model checking\n" );
Abc_Print( -2, "\t-P num : the number of parallel solvers [default = %d]\n", pPars->nProcs );
Abc_Print( -2, "\t-C num : the SAT solver conflict limit [default = %d]\n", pPars->nConfLimit );
@ -40128,7 +40128,7 @@ usage:
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-e : toggle using variable eliminatation [default = %s]\n", pPars->fUseEliminate?"yes": "no" );
// 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" );
Abc_Print( -2, "\t-h : print the command usage\n");

5
src/sat/bmc/bmcBmcG.c
View File

@ -337,7 +337,7 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
if ( pCnf == NULL )
{
Bmcg_ManPrintFrame( p, f, nClauses, -1, clkStart );
if( pPars->pFuncOnFrameDone)
if( pPars->pFuncOnFrameDone )
for ( k = 0; k < pPars->nFramesAdd; k++ )
for ( i = 0; i < Gia_ManPoNum(pGia); i++ )
pPars->pFuncOnFrameDone(f+k, i, 0);
@ -372,6 +372,7 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
pPars->iFrame = f+k;
pGia->pCexSeq = Bmcg_ManGenerateCex( p, i, f+k, 0 );
pPars->nFailOuts++;
Bmcg_ManPrintFrame( p, f+k, nClauses, -1, clkStart );
if ( !pPars->fNotVerbose )
{
int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) );
@ -379,7 +380,7 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
nOutDigits, i, f+k, nOutDigits, pPars->nFailOuts, nOutDigits, Gia_ManPoNum(pGia) );
fflush( stdout );
}
if( pPars->pFuncOnFrameDone)
if( pPars->pFuncOnFrameDone )
pPars->pFuncOnFrameDone(f+k, i, 1);
}
break;

2
src/sat/bmc/bmcBmcS.c
View File

@ -682,6 +682,7 @@ int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
pPars->iFrame = f+k;
pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f+k, 0 );
pPars->nFailOuts++;
Bmcs_ManPrintFrame( p, f+k, nClauses, -1, clkStart );
if ( !pPars->fNotVerbose )
{
int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) );
@ -872,6 +873,7 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
pPars->iFrame = f+k;
pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f+k, Solver );
pPars->nFailOuts++;
Bmcs_ManPrintFrame( p, f+k, nClauses, Solver, clkStart );
if ( !pPars->fNotVerbose )
{
int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) );

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

@ -54,19 +54,19 @@ extern "C" {
SeeAlso []
***********************************************************************/
Gluco::SimpSolver * glucose_solver_start()
Gluco::Solver * glucose_solver_start()
{
SimpSolver * S = new SimpSolver;
Solver * S = new Solver;
S->setIncrementalMode();
return S;
}
void glucose_solver_stop(Gluco::SimpSolver* S)
void glucose_solver_stop(Gluco::Solver* S)
{
delete S;
}
int glucose_solver_addclause(Gluco::SimpSolver* S, int * plits, int nlits)
int glucose_solver_addclause(Gluco::Solver* S, int * plits, int nlits)
{
vec<Lit> lits;
for ( int i = 0; i < nlits; i++,plits++)
@ -81,14 +81,14 @@ int glucose_solver_addclause(Gluco::SimpSolver* S, int * plits, int nlits)
return S->addClause(lits); // returns 0 if the problem is UNSAT
}
void glucose_solver_setcallback(Gluco::SimpSolver* S, void * pman, int(*pfunc)(void*, int, int*))
void glucose_solver_setcallback(Gluco::Solver* S, void * pman, int(*pfunc)(void*, int, int*))
{
S->pCnfMan = pman;
S->pCnfFunc = pfunc;
S->nCallConfl = 1000;
}
int glucose_solver_solve(Gluco::SimpSolver* S, int * plits, int nlits)
int glucose_solver_solve(Gluco::Solver* S, int * plits, int nlits)
{
vec<Lit> lits;
for (int i=0;i<nlits;i++,plits++)
@ -97,22 +97,22 @@ int glucose_solver_solve(Gluco::SimpSolver* S, int * plits, int nlits)
p.x = *plits;
lits.push(p);
}
Gluco::lbool res = S->solveLimited(lits, 0);
Gluco::lbool res = S->solveLimited(lits);
return (res == l_True ? 1 : res == l_False ? -1 : 0);
}
int glucose_solver_addvar(Gluco::SimpSolver* S)
int glucose_solver_addvar(Gluco::Solver* S)
{
S->newVar();
return S->nVars() - 1;
}
int glucose_solver_read_cex_varvalue(Gluco::SimpSolver* S, int ivar)
int glucose_solver_read_cex_varvalue(Gluco::Solver* S, int ivar)
{
return S->model[ivar] == l_True;
}
void glucose_solver_setstop(Gluco::SimpSolver* S, int * pstop)
void glucose_solver_setstop(Gluco::Solver* S, int * pstop)
{
S->pstop = pstop;
}
@ -155,33 +155,33 @@ bmcg_sat_solver * bmcg_sat_solver_start()
}
void bmcg_sat_solver_stop(bmcg_sat_solver* s)
{
glucose_solver_stop((Gluco::SimpSolver*)s);
glucose_solver_stop((Gluco::Solver*)s);
}
int bmcg_sat_solver_addclause(bmcg_sat_solver* s, int * plits, int nlits)
{
return glucose_solver_addclause((Gluco::SimpSolver*)s,plits,nlits);
return glucose_solver_addclause((Gluco::Solver*)s,plits,nlits);
}
void bmcg_sat_solver_setcallback(bmcg_sat_solver* s, void * pman, int(*pfunc)(void*, int, int*))
{
glucose_solver_setcallback((Gluco::SimpSolver*)s,pman,pfunc);
glucose_solver_setcallback((Gluco::Solver*)s,pman,pfunc);
}
int bmcg_sat_solver_solve(bmcg_sat_solver* s, int * plits, int nlits)
{
return glucose_solver_solve((Gluco::SimpSolver*)s,plits,nlits);
return glucose_solver_solve((Gluco::Solver*)s,plits,nlits);
}
int bmcg_sat_solver_final(bmcg_sat_solver* s, int ** ppArray)
{
*ppArray = (int *)(Lit *)((Gluco::SimpSolver*)s)->conflict;
return ((Gluco::SimpSolver*)s)->conflict.size();
*ppArray = (int *)(Lit *)((Gluco::Solver*)s)->conflict;
return ((Gluco::Solver*)s)->conflict.size();
}
int bmcg_sat_solver_addvar(bmcg_sat_solver* s)
{
return glucose_solver_addvar((Gluco::SimpSolver*)s);
return glucose_solver_addvar((Gluco::Solver*)s);
}
void bmcg_sat_solver_set_nvars( bmcg_sat_solver* s, int nvars )
@ -193,54 +193,56 @@ void bmcg_sat_solver_set_nvars( bmcg_sat_solver* s, int nvars )
int bmcg_sat_solver_eliminate( bmcg_sat_solver* s, int turn_off_elim )
{
return 1;
return ((Gluco::SimpSolver*)s)->eliminate(turn_off_elim != 0);
}
int bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v )
{
return 0;
return ((Gluco::SimpSolver*)s)->isEliminated(v);
}
int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver* s, int ivar)
{
return glucose_solver_read_cex_varvalue((Gluco::SimpSolver*)s, ivar);
return glucose_solver_read_cex_varvalue((Gluco::Solver*)s, ivar);
}
void bmcg_sat_solver_set_stop(bmcg_sat_solver* s, int * pstop)
{
glucose_solver_setstop((Gluco::SimpSolver*)s, pstop);
glucose_solver_setstop((Gluco::Solver*)s, pstop);
}
abctime bmcg_sat_solver_set_runtime_limit(bmcg_sat_solver* s, abctime Limit)
{
abctime nRuntimeLimit = ((Gluco::SimpSolver*)s)->nRuntimeLimit;
((Gluco::SimpSolver*)s)->nRuntimeLimit = 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::SimpSolver*)s)->setConfBudget( (int64_t)Limit );
((Gluco::Solver*)s)->setConfBudget( (int64_t)Limit );
else
((Gluco::SimpSolver*)s)->budgetOff();
((Gluco::Solver*)s)->budgetOff();
}
int bmcg_sat_solver_varnum(bmcg_sat_solver* s)
{
return ((Gluco::SimpSolver*)s)->nVars();
return ((Gluco::Solver*)s)->nVars();
}
int bmcg_sat_solver_clausenum(bmcg_sat_solver* s)
{
return ((Gluco::SimpSolver*)s)->nClauses();
return ((Gluco::Solver*)s)->nClauses();
}
int bmcg_sat_solver_learntnum(bmcg_sat_solver* s)
{
return ((Gluco::SimpSolver*)s)->nLearnts();
return ((Gluco::Solver*)s)->nLearnts();
}
int bmcg_sat_solver_conflictnum(bmcg_sat_solver* s)
{
return ((Gluco::SimpSolver*)s)->conflicts;
return ((Gluco::Solver*)s)->conflicts;
}
/**Function*************************************************************