summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/sat/bmc/bmcBmcG.c43
-rw-r--r--src/sat/glucose/AbcGlucose.cpp39
-rw-r--r--src/sat/glucose/AbcGlucose.h2
-rw-r--r--src/sat/glucose/SimpSolver.cpp6
-rw-r--r--src/sat/glucose/SimpSolver.h1
5 files changed, 77 insertions, 14 deletions
diff --git a/src/sat/bmc/bmcBmcG.c b/src/sat/bmc/bmcBmcG.c
index 8fef2ef6..af141d30 100644
--- a/src/sat/bmc/bmcBmcG.c
+++ b/src/sat/bmc/bmcBmcG.c
@@ -42,9 +42,12 @@ struct Bmcg_Man_t_
Vec_Int_t vCiMap; // maps CIs of pFrames into CIs/frames of GIA
bmcg_sat_solver * pSats[PAR_THR_MAX]; // concurrent SAT solvers
int nSatVars; // number of SAT variables used
+ int nOldFrPis; // number of primary inputs
+ int nOldFrPos; // number of primary output
int fStopNow; // signal when it is time to stop
abctime timeUnf; // runtime of unfolding
abctime timeCnf; // runtime of CNF generation
+ abctime timeSmp; // runtime of CNF simplification
abctime timeSat; // runtime of the solvers
abctime timeOth; // other runtime
};
@@ -165,7 +168,7 @@ int Bmcg_ManCollect_rec( Bmcg_Man_t * p, int iObj )
return iLitClean;
pObj = Gia_ManObj( p->pFrames, iObj );
iSatVar = Vec_IntEntry( &p->vFr2Sat, iObj );
- if ( (iSatVar > 0 && !bmcg_sat_solver_var_is_elim(p->pSats[0], iSatVar)) || Gia_ObjIsCi(pObj) )
+ if ( iSatVar > 0 || Gia_ObjIsCi(pObj) )
iLitClean = Gia_ManAppendCi( p->pClean );
else if ( Gia_ObjIsAnd(pObj) )
{
@@ -277,7 +280,7 @@ void Bmcg_ManPrintFrame( Bmcg_Man_t * p, int f, int nClauses, int Solver, abctim
Abc_Print( 1, "%4d %s : ", f, fUnfinished ? "-" : "+" );
// Abc_Print( 1, "Var =%8.0f. ", (double)p->nSatVars );
// Abc_Print( 1, "Cla =%9.0f. ", (double)nClauses );
- Abc_Print( 1, "Var =%8.0f. ", (double)bmcg_sat_solver_varnum(p->pSats[0]) );
+ Abc_Print( 1, "Var =%8.0f. ", (double)(bmcg_sat_solver_varnum(p->pSats[0])-bmcg_sat_solver_elim_varnum(p->pSats[0])) );
Abc_Print( 1, "Cla =%9.0f. ", (double)bmcg_sat_solver_clausenum(p->pSats[0]) );
Abc_Print( 1, "Learn =%9.0f. ",(double)bmcg_sat_solver_learntnum(p->pSats[0]) );
Abc_Print( 1, "Conf =%9.0f. ", (double)bmcg_sat_solver_conflictnum(p->pSats[0]) );
@@ -290,11 +293,12 @@ void Bmcg_ManPrintFrame( Bmcg_Man_t * p, int f, int nClauses, int Solver, abctim
}
void Bmcg_ManPrintTime( Bmcg_Man_t * p )
{
- abctime clkTotal = p->timeUnf + p->timeCnf + p->timeSat + p->timeOth;
+ abctime clkTotal = p->timeUnf + p->timeCnf + p->timeSmp + p->timeSat + p->timeOth;
if ( !p->pPars->fVerbose )
return;
ABC_PRTP( "Unfolding ", p->timeUnf, clkTotal );
ABC_PRTP( "CNF generation", p->timeCnf, clkTotal );
+ ABC_PRTP( "CNF simplify ", p->timeSmp, clkTotal );
ABC_PRTP( "SAT solving ", p->timeSat, clkTotal );
ABC_PRTP( "Other ", p->timeOth, clkTotal );
ABC_PRTP( "TOTAL ", clkTotal , clkTotal );
@@ -317,13 +321,38 @@ Abc_Cex_t * Bmcg_ManGenerateCex( Bmcg_Man_t * p, int i, int f, int s )
}
void Bmcg_ManAddCnf( Bmcg_Man_t * p, bmcg_sat_solver * pSat, Cnf_Dat_t * pCnf )
{
- int i;
+ int i, iSatVar;
+ abctime clk = Abc_Clock();
bmcg_sat_solver_set_nvars( pSat, p->nSatVars );
+ if ( p->pPars->fUseEliminate )
+ {
+ for ( i = p->nOldFrPis; i < Gia_ManPiNum(p->pFrames); i++ )
+ {
+ Gia_Obj_t * pObj = Gia_ManPi( p->pFrames, i );
+ int iSatVar = Vec_IntEntry( &p->vFr2Sat, Gia_ObjId(p->pFrames, pObj) );
+ if ( iSatVar > 0 )
+ bmcg_sat_solver_var_set_frozen( pSat, iSatVar, 1 );
+ }
+ for ( i = p->nOldFrPos; i < Gia_ManPoNum(p->pFrames); i++ )
+ {
+ Gia_Obj_t * pObj = Gia_ManPo( p->pFrames, i );
+ int iSatVar = Vec_IntEntry( &p->vFr2Sat, Gia_ObjId(p->pFrames, pObj) );
+ if ( iSatVar > 0 )
+ bmcg_sat_solver_var_set_frozen( pSat, iSatVar, 1 );
+ }
+ p->nOldFrPis = Gia_ManPiNum(p->pFrames);
+ p->nOldFrPos = Gia_ManPoNum(p->pFrames);
+ }
for ( i = 0; i < pCnf->nClauses; i++ )
if ( !bmcg_sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) )
assert( 0 );
- if ( p->pPars->fUseEliminate )
- bmcg_sat_solver_eliminate( pSat, 0 );
+ if ( !p->pPars->fUseEliminate )
+ return;
+ bmcg_sat_solver_eliminate( pSat, 0 );
+ Vec_IntForEachEntry( &p->vFr2Sat, iSatVar, i )
+ if ( iSatVar > 0 && bmcg_sat_solver_var_is_elim(pSat, iSatVar) )
+ Vec_IntWriteEntry( &p->vFr2Sat, i, -1 );
+ p->timeSmp += Abc_Clock() - clk;
}
int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
@@ -391,7 +420,7 @@ int Bmcg_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
if ( k < pPars->nFramesAdd )
break;
}
- p->timeOth = Abc_Clock() - clkStart - p->timeUnf - p->timeCnf - p->timeSat;
+ p->timeOth = Abc_Clock() - clkStart - p->timeUnf - p->timeCnf - p->timeSmp - p->timeSat;
if ( RetValue == -1 && !pPars->fNotVerbose )
printf( "No output failed in %d frames. ", f + (k < pPars->nFramesAdd ? k+1 : 0) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp
index f4bc41b7..064c723e 100644
--- a/src/sat/glucose/AbcGlucose.cpp
+++ b/src/sat/glucose/AbcGlucose.cpp
@@ -40,7 +40,7 @@ extern "C" {
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-//#define USE_SIMP_SOLVER 1
+#define USE_SIMP_SOLVER 1
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -188,6 +188,17 @@ int bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v )
return ((Gluco::SimpSolver*)s)->isEliminated(v);
}
+void bmcg_sat_solver_var_set_frozen( bmcg_sat_solver* s, int v, int freeze )
+{
+ ((Gluco::SimpSolver*)s)->setFrozen(v, freeze != 0);
+}
+
+int bmcg_sat_solver_elim_varnum(bmcg_sat_solver* s)
+{
+// return 0;
+ return ((Gluco::SimpSolver*)s)->eliminated_vars;
+}
+
int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver* s, int ivar)
{
return glucose_solver_read_cex_varvalue((Gluco::SimpSolver*)s, ivar);
@@ -407,13 +418,24 @@ void bmcg_sat_solver_set_nvars( bmcg_sat_solver* s, int nvars )
int bmcg_sat_solver_eliminate( bmcg_sat_solver* s, int turn_off_elim )
{
return 1;
-// return ((Gluco::Solver*)s)->eliminate(turn_off_elim != 0);
+// return ((Gluco::SimpSolver*)s)->eliminate(turn_off_elim != 0);
}
int bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v )
{
return 0;
-// return ((Gluco::Solver*)s)->isEliminated(v);
+// return ((Gluco::SimpSolver*)s)->isEliminated(v);
+}
+
+void bmcg_sat_solver_var_set_frozen( bmcg_sat_solver* s, int v, int freeze )
+{
+// ((Gluco::SimpSolver*)s)->setFrozen(v, freeze);
+}
+
+int bmcg_sat_solver_elim_varnum(bmcg_sat_solver* s)
+{
+ return 0;
+// return ((Gluco::SimpSolver*)s)->eliminated_vars;
}
int bmcg_sat_solver_read_cex_varvalue(bmcg_sat_solver* s, int ivar)
@@ -618,7 +640,12 @@ void Glucose_SolveCnf( char * pFileName, Glucose_Pars * pPars )
printf("c | Number of clauses: %12d |\n", S.nClauses());
}
- if ( pPars->pre ) S.eliminate(true);
+ if ( pPars->pre )
+ {
+ S.eliminate(true);
+ printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
vec<Lit> dummy;
lbool ret = S.solveLimited(dummy, 0);
@@ -773,7 +800,11 @@ int Glucose_SolveAig(Gia_Man_t * p, Glucose_Pars * pPars)
}
if (pPars->pre)
+ {
S.eliminate(true);
+ printf( "c Simplication removed %d variables and %d clauses. ", S.eliminated_vars, S.eliminated_clauses );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
vec<Lit> dummy;
lbool ret = S.solveLimited(dummy, 0);
diff --git a/src/sat/glucose/AbcGlucose.h b/src/sat/glucose/AbcGlucose.h
index c0078845..e36b7a24 100644
--- a/src/sat/glucose/AbcGlucose.h
+++ b/src/sat/glucose/AbcGlucose.h
@@ -75,6 +75,8 @@ extern int bmcg_sat_solver_addvar( bmcg_sat_solver* s );
extern void bmcg_sat_solver_set_nvars( bmcg_sat_solver* s, int nvars );
extern int bmcg_sat_solver_eliminate( bmcg_sat_solver* s, int turn_off_elim );
extern int bmcg_sat_solver_var_is_elim( bmcg_sat_solver* s, int v );
+extern void bmcg_sat_solver_var_set_frozen( bmcg_sat_solver* s, int v, int freeze );
+extern int bmcg_sat_solver_elim_varnum(bmcg_sat_solver* s);
extern int bmcg_sat_solver_read_cex_varvalue( bmcg_sat_solver* s, int );
extern void bmcg_sat_solver_set_stop( bmcg_sat_solver* s, int * pstop );
extern abctime bmcg_sat_solver_set_runtime_limit( bmcg_sat_solver* s, abctime Limit );
diff --git a/src/sat/glucose/SimpSolver.cpp b/src/sat/glucose/SimpSolver.cpp
index 43d98146..0c6639fb 100644
--- a/src/sat/glucose/SimpSolver.cpp
+++ b/src/sat/glucose/SimpSolver.cpp
@@ -54,6 +54,7 @@ SimpSolver::SimpSolver() :
, merges (0)
, asymm_lits (0)
, eliminated_vars (0)
+ , eliminated_clauses (0)
, elimorder (1)
, use_simplification (true)
, occurs (ClauseDeleted(ca))
@@ -523,10 +524,12 @@ bool SimpSolver::eliminateVar(Var v)
for (i = 0; i < neg.size(); i++)
mkElimClause(elimclauses, v, ca[neg[i]]);
mkElimClause(elimclauses, mkLit(v));
+ eliminated_clauses += neg.size();
}else{
for (i = 0; i < pos.size(); i++)
mkElimClause(elimclauses, v, ca[pos[i]]);
mkElimClause(elimclauses, ~mkLit(v));
+ eliminated_clauses += pos.size();
}
@@ -690,9 +693,6 @@ bool SimpSolver::eliminate(bool turn_off_elim)
if (verbosity >= 1 && elimclauses.size() > 0)
printf("c | Eliminated clauses: %10.2f Mb |\n",
double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
-
- printf( "c Simplication removed %d variables and %d clauses. ", eliminated_vars, elimclauses.size() );
- Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
return ok;
}
diff --git a/src/sat/glucose/SimpSolver.h b/src/sat/glucose/SimpSolver.h
index 260ab5e3..520a5cc9 100644
--- a/src/sat/glucose/SimpSolver.h
+++ b/src/sat/glucose/SimpSolver.h
@@ -97,6 +97,7 @@ class SimpSolver : public Solver {
int merges;
int asymm_lits;
int eliminated_vars;
+ int eliminated_clauses;
protected:
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-30 21:22:59 +0000