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

Adding global conflict counter to Satoko (to make it apple-to-apple with other solvers).

This commit is contained in:
Alan Mishchenko 2017-09-06 20:33:53 -07:00
parent 97dd6019bf
commit 3ffb098d64
4 changed files with 9 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1716,8 +1716,9 @@ nTimeSat += clkSatRun;
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_Print( 1, "Uni =%7.0f. ",(double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
// ABC_PRT( "Time", Abc_Clock() - clk );
Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
Abc_Print( 1, "%4.0f MB", 4.25*(f+1)*p->nObjNums /(1<<20) );
Abc_Print( 1, "%4.0f MB", 1.0*(p->pSat ? sat_solver_memory(p->pSat) : 0)/(1<<20) );
Abc_Print( 1, "%9.2f sec ", (float)(Abc_Clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
@ -1839,7 +1840,8 @@ nTimeUndec += clkSatRun;
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_Print( 1, "Uni =%7.0f. ", (double)(p->pSat ? sat_solver_count_assigned(p->pSat) : 0) );
Abc_Print( 1, "Learn =%7.0f. ", (double)(p->pSat ? p->pSat->stats.learnts : p->pSat3 ? bmcg_sat_solver_learntnum(p->pSat3) : satoko_learntnum(p->pSat2)) );
if ( pPars->fSolveAll )
Abc_Print( 1, "CEX =%5d. ", pPars->nFailOuts );
if ( pPars->nTimeOutOne )

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

@ -78,6 +78,7 @@ struct satoko_stats {
long n_propagations;
long n_inspects;
long n_conflicts;
long n_conflicts_all;
long n_original_lits;
long n_learnt_lits;

1
src/sat/satoko/solver.c
View File

@ -631,6 +631,7 @@ char solver_search(solver_t *s)
unsigned confl_cref = solver_propagate(s);
if (confl_cref != UNDEF) {
s->stats.n_conflicts++;
s->stats.n_conflicts_all++;
if (solver_dlevel(s) == 0)
return SATOKO_UNSAT;
/* Restart heuristic */

4
src/sat/satoko/solver_api.c
View File

@ -45,7 +45,9 @@ static inline int clause_is_satisfied(solver_t *s, struct clause *clause)
static inline void solver_clean_stats(solver_t *s)
{
int n_conflicts_all = s->stats.n_conflicts_all;
memset(&(s->stats), 0, sizeof(struct satoko_stats));
s->stats.n_conflicts_all = n_conflicts_all;
}
static inline void print_opts(solver_t *s)
@ -629,7 +631,7 @@ int satoko_learntnum(satoko_t *s)
int satoko_conflictnum(satoko_t *s)
{
return satoko_stats(s)->n_conflicts;
return satoko_stats(s)->n_conflicts_all;
}
void satoko_set_stop(satoko_t *s, int * pstop)