summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaAbsGla2.c2
-rw-r--r--src/aig/gia/giaAbsRef.c2
-rw-r--r--src/aig/saig/saigBmc3.c70
-rw-r--r--src/sat/bsat/satSolver.c16
-rw-r--r--src/sat/bsat/satSolver.h4
5 files changed, 78 insertions, 16 deletions
diff --git a/src/aig/gia/giaAbsGla2.c b/src/aig/gia/giaAbsGla2.c
index 6527dd3f..fc6a5ef3 100644
--- a/src/aig/gia/giaAbsGla2.c
+++ b/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;
diff --git a/src/aig/gia/giaAbsRef.c b/src/aig/gia/giaAbsRef.c
index 38e51f11..4532a90b 100644
--- a/src/aig/gia/giaAbsRef.c
+++ b/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;
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
index fde874df..2fbe88de 100644
--- a/src/aig/saig/saigBmc3.c
+++ b/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) );
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 5472e25d..b2014404 100644
--- a/src/sat/bsat/satSolver.c
+++ b/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);
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index eace9eea..24350b36 100644
--- a/src/sat/bsat/satSolver.h
+++ b/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
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-02 19:19:17 +0000