diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-07 02:05:03 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-02-07 02:05:03 -0800 |
| commit | 80f5070dbe270f7b1e90df07c5f52c46f0c0c969 (patch) | |
| tree | 7413127e5b99a844223e55d328fd50d1c52242ea /src/sat/bsat | |
| parent | 44dbf992a7e32f3e09a789b95222a18ed54f8f5b (diff) | |
| download | abc-80f5070dbe270f7b1e90df07c5f52c46f0c0c969.tar.gz abc-80f5070dbe270f7b1e90df07c5f52c46f0c0c969.tar.bz2 abc-80f5070dbe270f7b1e90df07c5f52c46f0c0c969.zip | |
Re-introducing floating-point activity in the SAT solver.
Diffstat (limited to 'src/sat/bsat')
| -rw-r--r-- | src/sat/bsat/satSolver.c | 20 |
1 files changed, 18 insertions, 2 deletions
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 73d0cf36..1a2a393d 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -492,7 +492,7 @@ int sat_solver_clause_new(sat_solver* s, lit* begin, lit* end, int learnt) #ifdef USE_FLOAT_ACTIVITY_NEW veci_push(&s->act_clas, xSat_Float2Uint(xSat_FloatCreateConst1())); #else - veci_push(&s->act_clas, 0); + veci_push(&s->act_clas, s->cla_inc); #endif #else veci_push(&s->act_clas, (1<<10)); @@ -1532,8 +1532,16 @@ void sat_solver_reducedb(sat_solver* s) Sat_MemForEachLearned( pMem, c, i, k ) { Id = clause_id(c); - pSortValues[Id] = (((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4)); // pSortValues[Id] = act[Id]; +#ifdef USE_FLOAT_ACTIVITY +#ifdef USE_FLOAT_ACTIVITY_NEW + pSortValues[Id] = ((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4); +#else + pSortValues[Id] = ((7 - Abc_MinInt(c->lbd, 7)) << 28);// | (act_clas[Id] >> 4); +#endif +#else + pSortValues[Id] = ((7 - Abc_MinInt(c->lbd, 7)) << 28) | (act_clas[Id] >> 4); +#endif assert( pSortValues[Id] >= 0 ); } @@ -1639,7 +1647,15 @@ void sat_solver_rollback( sat_solver* s ) if ( s->activity2 ) { s->var_inc = s->var_inc2; +#ifdef USE_FLOAT_ACTIVITY +#ifdef USE_FLOAT_ACTIVITY_NEW + memcpy( s->activity, s->activity2, sizeof(xFloat_t) * s->iVarPivot ); +#else + memcpy( s->activity, s->activity2, sizeof(double) * s->iVarPivot ); +#endif +#else memcpy( s->activity, s->activity2, sizeof(unsigned) * s->iVarPivot ); +#endif } veci_resize(&s->order, 0); for ( i = 0; i < s->iVarPivot; i++ ) |