diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/sat/bsat/satClause.h | 9 | ||||
| -rw-r--r-- | src/sat/bsat/satSolver2.c | 4 |
2 files changed, 6 insertions, 7 deletions
diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h index d5df71ad..79a43b4e 100644 --- a/src/sat/bsat/satClause.h +++ b/src/sat/bsat/satClause.h @@ -113,10 +113,11 @@ static inline double Sat_MemMemoryAll( Sat_Mem_t * p ) { return 1. // k is page offset // this macro has to be fixed (Sat_MemClauseSize does not work for problem clauses in proof mode) -//#define Sat_MemForEachClause( p, c, i, k ) \ -// for ( i = 0; i <= p->iPage[0]; i += 2 ) \ -// for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) ) - +/* +#define Sat_MemForEachClause( p, c, i, k ) \ + for ( i = 0; i <= p->iPage[0]; i += 2 ) \ + for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) ) +*/ #define Sat_MemForEachLearned( p, c, i, k ) \ for ( i = 1; i <= p->iPage[1]; i += 2 ) \ for ( k = 2; k < Sat_MemLimit(p->pPages[i]) && ((c) = Sat_MemClause( p, i, k )); k += Sat_MemClauseSize(c) ) diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index 7597207b..bcd1921d 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -30,8 +30,6 @@ ABC_NAMESPACE_IMPL_START #define SAT_USE_PROOF_LOGGING -static int Time = 0; - //================================================================================================= // Debug: @@ -1359,7 +1357,7 @@ void sat_solver2_reducedb(sat_solver2* s) int nLearnedOld = veci_size(&s->act_clas); int * act_clas = veci_begin(&s->act_clas); int * pPerm, * pSortValues, nCutoffValue, * pClaProofs; - int i, j, k, Id, nSelected, LastSize = 0; + int i, j, k, Id, nSelected;//, LastSize = 0; int Counter, CounterStart; clock_t clk = clock(); static int Count = 0; |