Skip to content

A
abc
Commit 2379dea4 by Alan Mishchenko
Options

Recording and reusing learned util clauses in bmc3.

parent 8d5fdf62
Showing with 78 additions and 16 deletions
src/aig/gia/giaAbsGla2.c
......@@ -48,7 +48,7 @@ struct Ga2_Man_t_
Vec_Int_t * pvLeaves; // leaves for each object
Vec_Int_t * pvCnfs0; // positive CNF
Vec_Int_t * pvCnfs1; // negative CNF
Vec_Int_t * pvMaps; // mapping into SAT vars for each frame
Vec_Int_t * pvMaps; // mapping into SAT vars for each frame (these should be organized by frame, not by object!)
// temporaries
Vec_Int_t * vCnf;
Vec_Int_t * vLits;
......
src/aig/gia/giaAbsRef.c
......@@ -327,7 +327,7 @@ int Rnm_ManSensitize( Rnm_Man_t * p )
void Rnm_ManJustifyPropFanout_rec( Rnm_Man_t * p, Gia_Obj_t * pObj, int f, Vec_Int_t * vSelect )
{
Rnm_Obj_t * pRnm0, * pRnm1, * pRnm = Rnm_ManObj( p, pObj, f );
Gia_Obj_t * pFanout;
Gia_Obj_t * pFanout = NULL;
int i, k;//, Id = Gia_ObjId(p->pGia, pObj);
assert( pRnm->fVisit == 0 );
pRnm->fVisit = 1;
......
src/aig/saig/saigBmc3.c
......@@ -50,6 +50,7 @@ struct Gia_ManBmc_t_
int nHashOver;
int nBufNum; // the number of simple nodes
int nDupNum; // the number of simple nodes
int nUniProps; // propagating learned clause values
// SAT solver
sat_solver * pSat; // SAT solver
int nSatVars; // SAT variables
......@@ -718,8 +719,8 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
{
if ( p->pPars->fVerbose )
printf( "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. Hash overs = %d.\n",
p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nHashOver );
printf( "Buffs = %d. Dups = %d. Hash hits = %d. Hash misses = %d. Hash overs = %d. UniProps = %d.\n",
p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nHashOver, p->nUniProps );
// Aig_ManCleanMarkA( p->pAig );
if ( p->vCexes )
{
......@@ -1126,7 +1127,36 @@ int Saig_ManBmcRunTerSim_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
unsigned * pInfo = (unsigned *)Vec_PtrEntry( p->vTerInfo, iFrame );
int Val0, Val1, Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
if ( Value != SAIG_TER_NON )
{
/*
// check the value of this literal in the SAT solver
if ( Value == SAIG_TER_UND && Saig_ManBmcMapping(p, pObj) )
{
int Lit = Saig_ManBmcLiteral( p, pObj, iFrame );
if ( Lit >= 0 )
{
assert( Lit >= 2 );
if ( p->pSat->assigns[Abc_Lit2Var(Lit)] < 2 )
{
p->nUniProps++;
if ( Abc_LitIsCompl(Lit) ^ (p->pSat->assigns[Abc_Lit2Var(Lit)] == 0) )
Value = SAIG_TER_ONE;
else
Value = SAIG_TER_ZER;
// Value = SAIG_TER_UND; // disable!
// use the new value
Saig_ManBmcSimInfoSet( pInfo, pObj, Value );
// transfer to the unrolling
if ( Value != SAIG_TER_UND )
Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) );
}
}
}
*/
return Value;
}
if ( Aig_ObjIsCo(pObj) )
{
Value = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame );
......@@ -1251,7 +1281,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
unsigned * pInfo;
int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
int i, f, Lit, status;
int i, f, k, Lit, status;
clock_t clk, clk2, clkOther = 0, clkTotal = clock();
clock_t nTimeToStop = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
p = Saig_Bmc3ManStart( pAig );
......@@ -1350,23 +1380,35 @@ clkOther += clock() - clk2;
RetValue = 0;
continue;
}
// solve this output
// solve th is output
fUnfinished = 0;
sat_solver_compress( p->pSat );
status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
if ( status == l_False )
{/*
Lit = lit_neg( Lit );
status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
assert( status );
sat_solver_compress( p->pSat );
*/
{
if ( 1 )
{
// add final unit clause
Lit = lit_neg( Lit );
status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
assert( status );
// add learned units
for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
{
Lit = veci_begin(&p->pSat->unit_lits)[k];
status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
assert( status );
}
veci_resize(&p->pSat->unit_lits, 0);
// propagate units
sat_solver_compress( p->pSat );
}
}
else if ( status == l_True )
{
Aig_Obj_t * pObjPi;
Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
int j, k, iBit = Saig_ManRegNum(pAig);
int j, iBit = Saig_ManRegNum(pAig);
for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(pAig) )
Saig_ManForEachPi( p->pAig, pObjPi, k )
{
......@@ -1383,7 +1425,8 @@ clkOther += clock() - clk2;
printf( "Var =%8.0f. ", (double)p->nSatVars );
printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts );
printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
// printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
printf( "Units =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
// ABC_PRT( "Time", clock() - clk );
printf( "%4.0f MB", 4.25*(f+1)*p->nObjNums /(1<<20) );
printf( "%4.0f MB", 1.0*sat_solver_memory(p->pSat)/(1<<20) );
......@@ -1446,7 +1489,8 @@ clkOther += clock() - clk2;
printf( "Var =%8.0f. ", (double)p->nSatVars );
printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
// printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
printf( "Units =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
// ABC_PRT( "Time", clock() - clk );
// printf( "%4.0f MB", 4.0*Vec_IntSize(p->vVisited) /(1<<20) );
printf( "%4.0f MB", 4.0*(f+1)*p->nObjNums /(1<<20) );
......
src/sat/bsat/satSolver.c
......@@ -505,6 +505,7 @@ static void sat_solver_canceluntil(sat_solver* s, int level) {
if (sat_solver_dl(s) <= level)
return;
assert( veci_size(&s->trail_lim) > 0 );
bound = (veci_begin(&s->trail_lim))[level];
lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1];
......@@ -536,6 +537,8 @@ static void sat_solver_record(sat_solver* s, veci* cls)
int h = (veci_size(cls) > 1) ? clause_create_new(s,begin,end,1) : 0;
sat_solver_enqueue(s,*begin,h);
assert(veci_size(cls) > 0);
if ( h == 0 )
veci_push( &s->unit_lits, *begin );
///////////////////////////////////
// add clause to internal storage
......@@ -554,6 +557,16 @@ static void sat_solver_record(sat_solver* s, veci* cls)
*/
}
int sat_solver_count_assigned(sat_solver* s)
{
// count top-level assignments
int i, Count = 0;
assert(sat_solver_dl(s) == 0);
for ( i = 0; i < s->size; i++ )
if (var_value(s, i) != varX)
Count++;
return Count;
}
static double sat_solver_progress(sat_solver* s)
{
......@@ -931,6 +944,7 @@ sat_solver* sat_solver_new(void)
veci_new(&s->stack);
// veci_new(&s->model);
veci_new(&s->act_vars);
veci_new(&s->unit_lits);
veci_new(&s->temp_clause);
veci_new(&s->conf_final);
......@@ -1052,6 +1066,7 @@ void sat_solver_delete(sat_solver* s)
veci_delete(&s->stack);
// veci_delete(&s->model);
veci_delete(&s->act_vars);
veci_delete(&s->unit_lits);
veci_delete(&s->temp_clause);
veci_delete(&s->conf_final);
......@@ -1157,6 +1172,7 @@ double sat_solver_memory( sat_solver* s )
// Mem += s->learned.cap * sizeof(int);
Mem += s->stack.cap * sizeof(int);
Mem += s->act_vars.cap * sizeof(int);
Mem += s->unit_lits.cap * sizeof(int);
Mem += s->act_clas.cap * sizeof(int);
Mem += s->temp_clause.cap * sizeof(int);
Mem += s->conf_final.cap * sizeof(int);
......
src/sat/bsat/satSolver.h
......@@ -53,6 +53,7 @@ extern int sat_solver_nvars(sat_solver* s);
extern int sat_solver_nclauses(sat_solver* s);
extern int sat_solver_nconflicts(sat_solver* s);
extern double sat_solver_memory(sat_solver* s);
extern int sat_solver_count_assigned(sat_solver* s);
extern void sat_solver_setnvars(sat_solver* s,int n);
extern int sat_solver_get_var_value(sat_solver* s, int v);
......@@ -155,7 +156,8 @@ struct sat_solver_t
double* factors; // the activity factors
int nRestarts; // the number of local restarts
int nCalls; // the number of local restarts
int nCalls2; // the number of local restarts
int nCalls2; // the number of local restarts
veci unit_lits; // variables whose activity has changed
int fSkipSimplify; // set to one to skip simplification of the clause database
int fNotUseRandom; // do not allow random decisions with a fixed probability
......
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