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

glucose2: Allow user defined marking of limited depth cones 

This does require using the version of uncheckedEnqueue that does check
whether the target lit is active in the current round.
This commit is contained in:
Jannis Harder 2024-08-19 14:06:17 +02:00
parent f36e35f735
commit 1e02c4327c
2 changed files with 20 additions and 12 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
src/sat/glucose2/CGlucoseCore.h
View File

@ -338,7 +338,7 @@ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
return Var2CRef(var(lfo));
var2NodeData[var(lfo)].dir = sign(lfo);
uncheckedEnqueue2(~mkLit(var(lfo)), Var2CRef( var(lfo) ) );
uncheckedEnqueue(~mkLit(var(lfo)), Var2CRef( var(lfo) ) );
} else {
assert( l_True == value(faninLit) );
@ -355,11 +355,11 @@ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
if( l_True == value(faninLitP) )
return Var2CRef(var(lfo));
uncheckedEnqueue2( ~faninLitP, Var2CRef( var(lfo) ) );
uncheckedEnqueue( ~faninLitP, Var2CRef( var(lfo) ) );
}
else
if( l_True == value(faninLitP) )
uncheckedEnqueue2( mkLit(var(lfo)), Var2CRef( var(lfo) ) );
uncheckedEnqueue( mkLit(var(lfo)), Var2CRef( var(lfo) ) );
}
} else { // xor scope
// check value of the other fanin
@ -374,10 +374,10 @@ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
return CRef_Undef;
else
if( l_Undef == val1 )
uncheckedEnqueue2( ~faninLitP ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( var(lfo) ) );
uncheckedEnqueue( ~faninLitP ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( var(lfo) ) );
else
if( l_Undef == valo )
uncheckedEnqueue2( ~mkLit( var(lfo), (l_True == val0) ^ (l_True == val1) ), Var2CRef( var(lfo) ) );
uncheckedEnqueue( ~mkLit( var(lfo), (l_True == val0) ^ (l_True == val1) ), Var2CRef( var(lfo) ) );
else
if( l_False == (valo ^ (val0 == val1)) )
return Var2CRef(var(lfo));
@ -398,19 +398,19 @@ inline CRef Solver::gatePropagateCheckThis( Var v ){
return CRef_Undef;
if( l_True == value(getFaninLit0(v)) )
uncheckedEnqueue2(~getFaninLit1( v ), Var2CRef( v ) );
uncheckedEnqueue(~getFaninLit1( v ), Var2CRef( v ) );
if( l_True == value(getFaninLit1(v)) )
uncheckedEnqueue2(~getFaninLit0( v ), Var2CRef( v ) );
uncheckedEnqueue(~getFaninLit0( v ), Var2CRef( v ) );
} else {
assert( l_True == value(v) );
if( l_False == value(getFaninLit0(v)) || l_False == value(getFaninLit1(v)) )
confl = Var2CRef(v);
if( l_Undef == value( getFaninLit0( v )) )
uncheckedEnqueue2( getFaninLit0( v ), Var2CRef( v ) );
uncheckedEnqueue( getFaninLit0( v ), Var2CRef( v ) );
if( l_Undef == value( getFaninLit1( v )) )
uncheckedEnqueue2( getFaninLit1( v ), Var2CRef( v ) );
uncheckedEnqueue( getFaninLit1( v ), Var2CRef( v ) );
}
} else { // xor scope
@ -421,10 +421,10 @@ inline CRef Solver::gatePropagateCheckThis( Var v ){
if( l_Undef == val0 && l_Undef == val1 )
return CRef_Undef;
if( l_Undef == val0 )
uncheckedEnqueue2(~getFaninLit0( v ) ^ ( (l_True == val1) ^ (l_True == valo) ), Var2CRef( v ) );
uncheckedEnqueue(~getFaninLit0( v ) ^ ( (l_True == val1) ^ (l_True == valo) ), Var2CRef( v ) );
else
if( l_Undef == val1 )
uncheckedEnqueue2(~getFaninLit1( v ) ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( v ) );
uncheckedEnqueue(~getFaninLit1( v ) ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( v ) );
else
if( l_False == (valo ^ (val0 == val1)) )
return Var2CRef(v);
@ -566,12 +566,17 @@ inline void Solver::markCone( Var v ){
Var var0, var1;
var0 = getFaninVar0(v);
var1 = getFaninVar1(v);
if( !isTwoFanin(v) )
if( !isTwoFanin(v) || (value(v) != l_Undef && level(v) == 0) )
return;
markCone( var0 );
markCone( var1 );
}
inline void Solver::markVar( Var v ){
var2TravId[v] = travId;
var2NodeData[v].sort = 0;
}
inline void Solver::inplace_sort( Var v ){
Lit w, next, prev;
prev= var2Fanout0[v];

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

@ -71,6 +71,7 @@ public:
void sat_solver_set_var_fanin_lit(int, int, int);
void sat_solver_start_new_round();
void sat_solver_mark_cone(int);
void sat_solver_mark_var(int);
void sat_solver_set_jftr(int);
int sat_solver_jftr();
void sat_solver_reset();
@ -486,6 +487,7 @@ public:
void setNewRound(){ travId ++ ; }
void markCone( Var v );
void markVar( Var v );
void setJust( int njftr ){ jftr = njftr; }
bool isRoundWatch( Var v ) const { return travId==var2TravId[v]; }
void justReset(){ jftr = 0; reset(); }
@ -627,6 +629,7 @@ inline void Solver::addVar(Var v) { while (v >= nVars()) newVar(); }
inline void Solver::sat_solver_set_var_fanin_lit(int v, int lit0, int lit1) { setVarFaninLits( Var(v), toLit(lit0), toLit(lit1) ); }
inline void Solver::sat_solver_start_new_round() { setNewRound(); }
inline void Solver::sat_solver_mark_cone(int v) { markCone(v); }
inline void Solver::sat_solver_mark_var(int v) { markVar(v); }
inline void Solver::sat_solver_set_jftr( int njftr ){ setJust(njftr); }
inline int Solver::sat_solver_jftr(){ return jftr; }
inline void Solver::sat_solver_reset(){ justReset(); }