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

Adding rollback for the other solver.

This commit is contained in:
Alan Mishchenko 2013-04-25 16:02:40 -07:00
parent ecf75a075b
commit ae9a4407c4
4 changed files with 142 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/proof/pdr/pdrSat.c
View File

@ -87,7 +87,7 @@ sat_solver * Pdr_ManFetchSolver( Pdr_Man_t * p, int k )
p->nStarts++;
// sat_solver_delete( pSat );
// pSat = sat_solver_new();
sat_solver_rollback( pSat );
sat_solver_restart( pSat );
// create new SAT solver
pSat = Pdr_ManNewSolver( pSat, p, k, (int)(k == 0) );
// write new SAT solver

119
src/sat/bsat/satSolver.c
View File

@ -531,6 +531,26 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
veci_resize(&s->trail_lim,level);
}
static void sat_solver_canceluntil_rollback(sat_solver* s, int NewBound) {
int c, x;
assert( sat_solver_dl(s) == 0 );
assert( s->qtail == s->qhead );
assert( s->qtail >= NewBound );
for (c = s->qtail-1; c >= NewBound; c--)
{
x = lit_var(s->trail[c]);
var_set_value(s, x, varX);
s->reasons[x] = 0;
}
for (c = s->qhead-1; c >= NewBound; c--)
order_unassigned(s,lit_var(s->trail[c]));
s->qhead = s->qtail = NewBound;
}
static void sat_solver_record(sat_solver* s, veci* cls)
{
lit* begin = veci_begin(cls);
@ -1011,6 +1031,7 @@ void sat_solver_setnvars(sat_solver* s,int n)
s->activity = ABC_REALLOC(double, s->activity, s->cap);
#else
s->activity = ABC_REALLOC(unsigned, s->activity, s->cap);
s->activity2 = ABC_REALLOC(unsigned, s->activity2,s->cap);
#endif
if ( s->factors )
s->factors = ABC_REALLOC(double, s->factors, s->cap);
@ -1084,6 +1105,7 @@ void sat_solver_delete(sat_solver* s)
ABC_FREE(s->polarity );
ABC_FREE(s->tags );
ABC_FREE(s->activity );
ABC_FREE(s->activity2);
ABC_FREE(s->factors );
ABC_FREE(s->orderpos );
ABC_FREE(s->reasons );
@ -1095,7 +1117,7 @@ void sat_solver_delete(sat_solver* s)
ABC_FREE(s);
}
void sat_solver_rollback( sat_solver* s )
void sat_solver_restart( sat_solver* s )
{
int i;
Sat_MemRestart( &s->Mem );
@ -1160,6 +1182,8 @@ double sat_solver_memory( sat_solver* s )
Mem += s->cap * sizeof(double); // ABC_FREE(s->activity );
#else
Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity );
if ( s->activity2 )
Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity2);
#endif
if ( s->factors )
Mem += s->cap * sizeof(double); // ABC_FREE(s->factors );
@ -1305,6 +1329,99 @@ void sat_solver_reducedb(sat_solver* s)
}
}
// reverses to the previously bookmarked point
void sat_solver_rollback( sat_solver* s )
{
Sat_Mem_t * pMem = &s->Mem;
int i, k, j;
static int Count = 0;
Count++;
assert( s->iVarPivot >= 0 && s->iVarPivot <= s->size );
assert( s->iTrailPivot >= 0 && s->iTrailPivot <= s->qtail );
// reset implication queue
sat_solver_canceluntil_rollback( s, s->iTrailPivot );
// update order
if ( s->iVarPivot < s->size )
{
if ( s->activity2 )
{
s->var_inc = s->var_inc2;
memcpy( s->activity, s->activity2, sizeof(unsigned) * s->iVarPivot );
}
veci_resize(&s->order, 0);
for ( i = 0; i < s->iVarPivot; i++ )
{
if ( var_value(s, i) != varX )
continue;
s->orderpos[i] = veci_size(&s->order);
veci_push(&s->order,i);
order_update(s, i);
}
}
// compact watches
for ( i = 0; i < s->iVarPivot*2; i++ )
{
cla* pArray = veci_begin(&s->wlists[i]);
for ( j = k = 0; k < veci_size(&s->wlists[i]); k++ )
if ( Sat_MemClauseUsed(pMem, pArray[k]) )
pArray[j++] = pArray[k];
veci_resize(&s->wlists[i],j);
}
// reset watcher lists
for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
s->wlists[i].size = 0;
// reset clause counts
s->stats.clauses = pMem->BookMarkE[0];
s->stats.learnts = pMem->BookMarkE[1];
// rollback clauses
Sat_MemRollBack( pMem );
// resize learned arrays
veci_resize(&s->act_clas, s->stats.learnts);
// initialize other vars
s->size = s->iVarPivot;
if ( s->size == 0 )
{
// s->size = 0;
// s->cap = 0;
s->qhead = 0;
s->qtail = 0;
#ifdef USE_FLOAT_ACTIVITY
s->var_inc = 1;
s->cla_inc = 1;
s->var_decay = (float)(1 / 0.95 );
s->cla_decay = (float)(1 / 0.999 );
#else
s->var_inc = (1 << 5);
s->cla_inc = (1 << 11);
#endif
s->root_level = 0;
s->random_seed = 91648253;
s->progress_estimate = 0;
s->verbosity = 0;
s->stats.starts = 0;
s->stats.decisions = 0;
s->stats.propagations = 0;
s->stats.inspects = 0;
s->stats.conflicts = 0;
s->stats.clauses = 0;
s->stats.clauses_literals = 0;
s->stats.learnts = 0;
s->stats.learnts_literals = 0;
s->stats.tot_literals = 0;
// initialize rollback
s->iVarPivot = 0; // the pivot for variables
s->iTrailPivot = 0; // the pivot for trail
s->hProofPivot = 1; // the pivot for proof records
}
}
int sat_solver_addclause(sat_solver* s, lit* begin, lit* end)
{
lit *i,*j;

21
src/sat/bsat/satSolver.h
View File

@ -47,6 +47,7 @@ extern void sat_solver_delete(sat_solver* s);
extern int sat_solver_addclause(sat_solver* s, lit* begin, lit* end);
extern int sat_solver_simplify(sat_solver* s);
extern int sat_solver_solve(sat_solver* s, lit* begin, lit* end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal);
extern void sat_solver_restart( sat_solver* s );
extern void sat_solver_rollback( sat_solver* s );
extern int sat_solver_nvars(sat_solver* s);
@ -101,6 +102,11 @@ struct sat_solver_t
veci* wlists; // watcher lists
veci act_clas; // contain clause activities
// rollback
int iVarPivot; // the pivot for variables
int iTrailPivot; // the pivot for trail
int hProofPivot; // the pivot for proof records
// activities
#ifdef USE_FLOAT_ACTIVITY
double var_inc; // Amount to bump next variable with.
@ -110,8 +116,10 @@ struct sat_solver_t
double* activity; // A heuristic measurement of the activity of a variable.
#else
int var_inc; // Amount to bump next variable with.
int var_inc2; // Amount to bump next variable with.
int cla_inc; // Amount to bump next clause with.
unsigned* activity; // A heuristic measurement of the activity of a variable.
unsigned* activity2; // backup variable activity
#endif
// varinfo * vi; // variable information
@ -227,6 +235,19 @@ static int sat_solver_set_random(sat_solver* s, int fNotUseRandom)
return fNotUseRandomOld;
}
static inline void sat_solver_bookmark(sat_solver* s)
{
assert( s->qhead == s->qtail );
s->iVarPivot = s->size;
s->iTrailPivot = s->qhead;
Sat_MemBookMark( &s->Mem );
if ( s->activity2 )
{
s->var_inc2 = s->var_inc;
memcpy( s->activity2, s->activity, sizeof(unsigned) * s->iVarPivot );
}
}
static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
{
lit Lits[1];

4
src/sat/bsat/satSolver2.c
View File

@ -1638,7 +1638,7 @@ void sat_solver2_rollback( sat_solver2* s )
// s->cap = 0;
s->qhead = 0;
s->qtail = 0;
#ifdef USE_FLOAT_ACTIVITY
#ifdef USE_FLOAT_ACTIVITY2
s->var_inc = 1;
s->cla_inc = 1;
s->var_decay = (float)(1 / 0.95 );
@ -1689,7 +1689,7 @@ double sat_solver2_memory( sat_solver2* s, int fAll )
Mem += s->cap * sizeof(varinfo2); // ABC_FREE(s->vi );
Mem += s->cap * sizeof(int); // ABC_FREE(s->levels );
Mem += s->cap * sizeof(char); // ABC_FREE(s->assigns );
#ifdef USE_FLOAT_ACTIVITY
#ifdef USE_FLOAT_ACTIVITY2
Mem += s->cap * sizeof(double); // ABC_FREE(s->activity );
#else
Mem += s->cap * sizeof(unsigned); // ABC_FREE(s->activity );