luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Improvements to the SAT solver.

This commit is contained in:
Alan Mishchenko 2020-11-14 22:45:23 -08:00
parent f95476b45d
commit 581f2e5972
3 changed files with 15 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/proof/cec/cecSatG2.c
View File

@ -1196,7 +1196,7 @@ int Cec4_ManCandIterNext( Cec4_Man_t * p )
while ( Vec_IntSize(p->vCands) > 0 )
{
int fStop, iCand = Vec_IntEntry( p->vCands, p->iPosRead );
if ( fStop = (Gia_ObjRepr(p->pAig, iCand) != GIA_VOID) )
if ( (fStop = (Gia_ObjRepr(p->pAig, iCand) != GIA_VOID)) )
Vec_IntWriteEntry( p->vCands, p->iPosWrite++, iCand );
if ( ++p->iPosRead == Vec_IntSize(p->vCands) )
{
@ -1273,7 +1273,7 @@ void Cec4_ManSatSolverRecycle( Cec4_Man_t * p )
int Cec4_ManSolveTwo( Cec4_Man_t * p, int iObj0, int iObj1, int fPhase, int * pfEasy, int fVerbose )
{
abctime clk;
int nBTLimit = Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1) ? p->pPars->nBTLimit/10 : p->pPars->nBTLimit;
int nBTLimit = (Vec_BitEntry(p->vFails, iObj0) || Vec_BitEntry(p->vFails, iObj1)) ? p->pPars->nBTLimit/10 : p->pPars->nBTLimit;
int nConfEnd, nConfBeg, status, iVar0, iVar1, Lits[2];
int UnsatConflicts[3] = {0};
if ( iObj1 < iObj0 )
@ -1385,7 +1385,7 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
assert( p->pAig->iPatsPi > 0 && p->pAig->iPatsPi < 64 * p->pAig->nSimWords );
//Vec_IntForEachEntryDouble( &p->pNew->vCopiesTwo, IdAig, IdSat, i )
// Cec4_ObjSimSetInputBit( p->pAig, IdAig, sat_solver_read_cex_varvalue(p->pSat, IdSat) );
pCex = NULL;//sat_solver_read_cex( p->pSat );
pCex = sat_solver_read_cex( p->pSat );
Vec_IntClear( p->vPat );
if ( pCex == NULL )
{

15
src/sat/glucose2/Glucose2.cpp
View File

@ -1153,6 +1153,13 @@ lbool Solver::search(int nof_conflicts)
for (;;){
CRef confl = propagate();
// exact conflict limit
if ( !withinBudget() && confl != CRef_Undef ) {
lbdQueue.fastclear();
cancelUntil(0);
return l_Undef; }
if (confl != CRef_Undef){
// CONFLICT
@ -1395,15 +1402,15 @@ printf("c ==================================[ Search Statistics (every %6d confl
if (status == l_True){
if( justUsage() && false ){
if( justUsage() ){
assert(jheap.empty());
//JustModel.growTo(nVars());
int i = 0;
int i = 0, j = 0;
JustModel.push(toLit(0));
for (; i < trail.size(); i++)
if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) )
JustModel.push(trail[i]);
JustModel[0] = toLit(i);
JustModel.push(trail[i]), j++;
JustModel[0] = toLit(j);
} else {
// Extend & copy model:
model.growTo(nVars());

2
src/sat/glucose2/Solver.h
View File

@ -546,7 +546,7 @@ inline int Solver::nClauses () const { return clauses.size(); }
inline int Solver::nLearnts () const { return learnts.size(); }
inline int Solver::nVars () const { return vardata.size(); }
inline int Solver::nFreeVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
inline int * Solver::getCex () const { return NULL; }
inline int * Solver::getCex () const { return (int*) &JustModel[0]; }
inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
inline void Solver::setDecisionVar(Var v, bool b)
{