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

4 files changed, 9 insertions, 3 deletions

diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index dd4bf490..904a2d7f 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -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 )
diff --git a/src/sat/satoko/satoko.h b/src/sat/satoko/satoko.h
index fb646c01..7ee8cd85 100644
--- a/src/sat/satoko/satoko.h
+++ b/src/sat/satoko/satoko.h
@@ -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;
diff --git a/src/sat/satoko/solver.c b/src/sat/satoko/solver.c
index 9f5d3424..6e58e8a5 100644
--- a/src/sat/satoko/solver.c
+++ b/src/sat/satoko/solver.c
@@ -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 */
diff --git a/src/sat/satoko/solver_api.c b/src/sat/satoko/solver_api.c
index a0b26b5c..adf30cef 100644
--- a/src/sat/satoko/solver_api.c
+++ b/src/sat/satoko/solver_api.c
@@ -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)