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

glucose2: Add option to include inner gates in the justification model

This commit is contained in:
Jannis Harder 2024-08-19 13:38:14 +02:00
parent a6512064bc
commit b7ea0adc9f
2 changed files with 4 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -154,6 +154,8 @@ Solver::Solver() :
, trace_default_tag(~0)
, trace_qhead(0)
, produceInnerModel(false)
#ifdef CGLUCOSE_EXP
//, jheap (JustOrderLt(this))
, jheap (JustOrderLt2(this))
@ -1579,7 +1581,7 @@ printf("c ==================================[ Search Statistics (every %6d confl
int i = 0, j = 0;
JustModel.push(toLit(0));
for (; i < trail.size(); i++)
if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) )
if( isRoundWatch(var(trail[i])) && (produceInnerModel || !isTwoFanin(var(trail[i])) ))
JustModel.push(trail[i]), j++;
JustModel[0] = toLit(j);
}

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

@ -495,6 +495,7 @@ public:
//double justActivity(int v) const { return jdata[v].act_fanin;}
int varPolarity(int v){ return polarity[v]? 1: 0;}
vec<Lit> JustModel; // model obtained by justification enabled
bool produceInnerModel;
int justUsage() const ;
int solveLimited( int * , int nlits );