Skip to content

A
abc
Commit e7def3d4 by Alan Mishchenko
Options

Enabling variable elim in &bmcs -g.

parent b5d42e8b
Showing with 77 additions and 14 deletions
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 );
......
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);
......
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 );
......
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;
}
......
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:
......
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