Skip to content

A
abc
Commit c7e85561 by Alan Mishchenko
Options

Variable timeframe abstraction.

parent 94d35a25
Showing with 44 additions and 24 deletions
src/aig/gia/giaAbsVta.c
......@@ -939,8 +939,8 @@ Abc_Cex_t * Vta_ManRefineAbstraction( Vta_Man_t * p, int f )
// check the output
if ( !Vta_ValIs1(pTop, Gia_ObjFaninC0(Gia_ManPo(p->pGia, 0))) )
printf( "Vta_ManRefineAbstraction(): Terminary simulation verification failed!\n" );
else
printf( "Verification OK.\n" );
// else
// printf( "Verification OK.\n" );
// produce true counter-example
if ( pTop->Prio == 0 )
......@@ -1285,6 +1285,7 @@ void Vga_ManLoadSlice( Vta_Man_t * p, Vec_Int_t * vOne, int Lift )
int i, Entry;
Vec_IntForEachEntry( vOne, Entry, i )
Vga_ManAddClausesOne( p, Entry & p->nObjMask, (Entry >> p->nObjBits) + Lift );
sat_solver2_simplify( p->pSat );
printf( "\n\n" );
}
......
src/sat/bsat/satSolver2.c
......@@ -469,6 +469,17 @@ static inline int solver2_enqueue(sat_solver2* s, lit l, cla from)
s->reasons[v] = from; // = from << 1;
s->trail[s->qtail++] = l;
order_assigned(s, v);
/*
if ( solver2_dlevel(s) == 0 )
{
satset * c = from ? clause_read( s, from ) : NULL;
printf( "Enqueing var %d on level %d with reason clause ", v, solver2_dlevel(s) );
if ( c )
satset_print( c );
else
printf( "<none>\n" );
}
*/
return true;
}
}
......@@ -491,6 +502,11 @@ static void solver2_canceluntil(sat_solver2* s, int level) {
int lastLev;
int c, x;
if ( level == 0 )
{
int ss = 0;
}
if (solver2_dlevel(s) <= level)
return;
......@@ -501,12 +517,9 @@ static void solver2_canceluntil(sat_solver2* s, int level) {
for (c = s->qtail-1; c >= bound; c--)
{
x = lit_var(trail[c]);
s->reasons[x] = 0;
// if ( s->units[x] == 0 || var_level(s, x) > 0 )
{
var_set_value(s, x, varX);
s->reasons[x] = 0;
s->units[x] = 0; // temporary?
}
if ( c < lastLev )
var_set_polar(s, x, !lit_sign(trail[c]));
}
......@@ -519,7 +532,7 @@ static void solver2_canceluntil(sat_solver2* s, int level) {
}
static void solver2_record(sat_solver2* s, veci* cls, int proof_id)
static void solver2_record(sat_solver2* s, veci* cls, int proof_id, int fSkipUnit)
{
lit* begin = veci_begin(cls);
lit* end = begin + veci_size(cls);
......@@ -527,7 +540,7 @@ static void solver2_record(sat_solver2* s, veci* cls, int proof_id)
assert(veci_size(cls) > 0);
if ( veci_size(cls) == 1 )
{
if ( s->fProofLogging )
if ( s->fProofLogging && !fSkipUnit)
var_set_unit_clause(s, lit_var(begin[0]), Cid);
Cid = 0;
}
......@@ -1009,11 +1022,16 @@ static lbool clause_simplify(sat_solver2* s, satset* c)
int sat_solver2_simplify(sat_solver2* s)
{
int TailOld = s->qtail;
// int type;
int Counter = 0;
assert(solver2_dlevel(s) == 0);
// reset the head
s->qhead = 0;
if (solver2_propagate(s) != 0)
return false;
// printf( "Tail moved from %d to %d.\n", TailOld, s->qtail );
if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0)
return true;
/*
......@@ -1108,8 +1126,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
#ifdef SAT_USE_ANALYZE_FINAL
proof_id = solver2_analyze_final(s, confl, 0);
assert( proof_id > 0 );
// if ( proof_id > 0 )
solver2_record(s,&s->conf_final, proof_id);
solver2_record(s,&s->conf_final, proof_id, 0);
#endif
veci_delete(&learnt_clause);
return l_False;
......@@ -1120,7 +1137,7 @@ static lbool solver2_search(sat_solver2* s, ABC_INT64_T nof_conflicts)
blevel = veci_size(&learnt_clause) > 1 ? var_level(s, lit_var(veci_begin(&learnt_clause)[1])) : s->root_level;
blevel = s->root_level > blevel ? s->root_level : blevel;
solver2_canceluntil(s,blevel);
solver2_record(s,&learnt_clause, proof_id);
solver2_record(s,&learnt_clause, proof_id, 0);
#ifdef SAT_USE_ANALYZE_FINAL
// if (learnt_clause.size() == 1) level[var(learnt_clause[0])] = 0;
// (this is ugly (but needed for 'analyzeFinal()') -- in future versions, we will backtrack past the 'root_level' and redo the assumptions)
......@@ -1584,13 +1601,20 @@ void sat_solver2_rollback( sat_solver2* s )
if ( s->units[i] && !clause_is_used(s, s->units[i]) )
s->units[i] = 0;
}
// reset
// reset implication queue
assert( (&s->trail_lim)->ptr[0] == s->simpdb_assigns );
assert( s->simpdb_assigns >= s->iSimpPivot );
(&s->trail_lim)->ptr[0] = s->iSimpPivot;
s->simpdb_assigns = s->iSimpPivot;
solver2_canceluntil( s, 0 );
// reset problem clauses
if ( s->hClausePivot < veci_size(&s->clauses) )
{
satset* first = satset_read(&s->clauses, s->hClausePivot);
s->stats.clauses = first->Id;
veci_resize(&s->clauses, s->hClausePivot);
}
// resetn learned clauses
if ( s->hLearntPivot < veci_size(&s->learnts) )
{
satset* first = satset_read(&s->learnts, s->hLearntPivot);
......@@ -1602,6 +1626,7 @@ void sat_solver2_rollback( sat_solver2* s )
s->stats.learnts = first->Id;
veci_resize(&s->learnts, s->hLearntPivot);
}
// reset watcher lists
for ( i = 2*s->iVarPivot; i < 2*s->size; i++ )
s->wlists[i].size = 0;
s->size = s->iVarPivot;
......@@ -1804,7 +1829,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
if (var_level(s, lit_var(p)) > 0)
veci_push(&s->conf_final, p);
}
solver2_record(s, &s->conf_final, proof_id);
solver2_record(s, &s->conf_final, proof_id, 1);
solver2_canceluntil(s, 0);
return l_False;
}
......@@ -1815,7 +1840,7 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
proof_id = solver2_analyze_final(s, confl, 0);
assert(s->conf_final.size > 0);
solver2_canceluntil(s, 0);
solver2_record(s,&s->conf_final, proof_id);
solver2_record(s,&s->conf_final, proof_id, 1);
return l_False;
}
}
......@@ -1866,8 +1891,8 @@ int sat_solver2_solve(sat_solver2* s, lit* begin, lit* end, ABC_INT64_T nConfLim
printf("==============================================================================\n");
solver2_canceluntil(s,0);
if ( status == l_True )
sat_solver2_verify( s );
// if ( status == l_True )
// sat_solver2_verify( s );
return status;
}
......
src/sat/bsat/satSolver2.h
......@@ -115,6 +115,7 @@ struct sat_solver2_t
int hLearntPivot; // the pivot among learned clause
int hLearntLast; // in proof-logging mode, the ID of the final conflict clause (conf_final)
int iVarPivot; // the pivot among the variables
int iSimpPivot; // marker of unit-clauses
veci claActs; // clause activities
veci claProofs; // clause proofs
......@@ -223,14 +224,6 @@ static inline void sat_solver2_act_var_clear(sat_solver2* s)
s->activity[i] = 0;//.0;
s->var_inc = 1.0;
}
static inline void sat_solver2_compress(sat_solver2* s)
{
if ( s->qtail != s->qhead )
{
int RetValue = sat_solver2_simplify(s);
assert( RetValue != 0 );
}
}
static inline int sat_solver2_final(sat_solver2* s, int ** ppArray)
{
......@@ -257,6 +250,7 @@ static inline void sat_solver2_bookmark(sat_solver2* s)
s->hLearntPivot = veci_size(&s->learnts);
s->hClausePivot = veci_size(&s->clauses);
s->iVarPivot = s->size;
s->iSimpPivot = s->simpdb_assigns;
}
static inline int sat_solver2_add_const( sat_solver2 * pSat, int iVar, int fCompl, int fMark )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment