summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/sat/glucose2/AbcGlucose2.cpp27
-rw-r--r--src/sat/glucose2/AbcGlucose2.h1
-rw-r--r--src/sat/glucose2/CGlucose.h1
-rw-r--r--src/sat/glucose2/CGlucoseCore.h254
-rw-r--r--src/sat/glucose2/Glucose2.cpp390
-rw-r--r--src/sat/glucose2/Heap.h11
-rw-r--r--src/sat/glucose2/Heap2.h169
-rw-r--r--src/sat/glucose2/SimpSolver.h21
-rw-r--r--src/sat/glucose2/SimpSolver2.cpp20
-rw-r--r--src/sat/glucose2/Solver.h135
-rw-r--r--src/sat/glucose2/SolverTypes.h5
-rw-r--r--src/sat/glucose2/Vec.h19
12 files changed, 686 insertions, 367 deletions
diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp
index 23c904c8..9a8b97eb 100644
--- a/src/sat/glucose2/AbcGlucose2.cpp
+++ b/src/sat/glucose2/AbcGlucose2.cpp
@@ -99,15 +99,16 @@ void glucose2_solver_setcallback(Gluco2::SimpSolver* S, void * pman, int(*pfunc)
int glucose2_solver_solve(Gluco2::SimpSolver* S, int * plits, int nlits)
{
- vec<Lit> lits;
- for (int i=0;i<nlits;i++,plits++)
- {
- Lit p;
- p.x = *plits;
- lits.push(p);
- }
- Gluco2::lbool res = S->solveLimited(lits, 0);
- return (res == l_True ? 1 : res == l_False ? -1 : 0);
+// vec<Lit> lits;
+// for (int i=0;i<nlits;i++,plits++)
+// {
+// Lit p;
+// p.x = *plits;
+// lits.push(p);
+// }
+// Gluco2::lbool res = S->solveLimited(lits, 0);
+// return (res == l_True ? 1 : res == l_False ? -1 : 0);
+ return S->solveLimited(plits, nlits, 0);
}
int glucose2_solver_addvar(Gluco2::SimpSolver* S)
@@ -383,6 +384,10 @@ void bmcg2_sat_solver_mark_cone(bmcg2_sat_solver* s, int var)
((Gluco2::SimpSolver*)s)->sat_solver_mark_cone(var);
}
+void bmcg2_sat_solver_prelocate( bmcg2_sat_solver * s, int var_num ){
+ ((Gluco2::SimpSolver*)s)->prelocate(var_num);
+}
+
#else
/**Function*************************************************************
@@ -721,6 +726,10 @@ void bmcg2_sat_solver_mark_cone(bmcg2_sat_solver* s, int var)
((Gluco2::Solver*)s)->sat_solver_mark_cone(var);
}
+void bmcg2_sat_solver_prelocate( bmcg2_sat_solver * s, int var_num ){
+ ((Gluco2::Solver*)s)->prelocate(var_num);
+}
+
#endif
diff --git a/src/sat/glucose2/AbcGlucose2.h b/src/sat/glucose2/AbcGlucose2.h
index 7c060ccc..9299d290 100644
--- a/src/sat/glucose2/AbcGlucose2.h
+++ b/src/sat/glucose2/AbcGlucose2.h
@@ -103,6 +103,7 @@ extern void bmcg2_sat_solver_set_jftr( bmcg2_sat_solver * s, int jf
extern void bmcg2_sat_solver_set_var_fanin_lit( bmcg2_sat_solver * s, int var, int lit0, int lit1 );
extern void bmcg2_sat_solver_start_new_round( bmcg2_sat_solver * s );
extern void bmcg2_sat_solver_mark_cone( bmcg2_sat_solver * s, int var );
+extern void bmcg2_sat_solver_prelocate( bmcg2_sat_solver * s, int var_num );
extern void Glucose2_SolveCnf( char * pFilename, Glucose2_Pars * pPars );
extern int Glucose2_SolveAig( Gia_Man_t * p, Glucose2_Pars * pPars );
diff --git a/src/sat/glucose2/CGlucose.h b/src/sat/glucose2/CGlucose.h
index 32da4248..7fbf8f83 100644
--- a/src/sat/glucose2/CGlucose.h
+++ b/src/sat/glucose2/CGlucose.h
@@ -2,5 +2,6 @@
#define Glucose_CGlucose_h
#define CGLUCOSE_EXP 1
+#include "sat/glucose2/Heap2.h"
#endif \ No newline at end of file
diff --git a/src/sat/glucose2/CGlucoseCore.h b/src/sat/glucose2/CGlucoseCore.h
index b558f257..c0f96fc4 100644
--- a/src/sat/glucose2/CGlucoseCore.h
+++ b/src/sat/glucose2/CGlucoseCore.h
@@ -37,7 +37,10 @@ inline Lit Solver::gateJustFanin(Var v) const {
if(val1 == l_True)
return ~getFaninLit0(v);
+ //assert( jdata[v].act_fanin == activity[getFaninVar0(v)] || jdata[v].act_fanin == activity[getFaninVar1(v)] );
+ //assert( jdata[v].act_fanin == (jdata[v].adir? activity[getFaninVar1(v)]: activity[getFaninVar0(v)]) );
return maxActiveLit( ~getFaninLit0(v), ~getFaninLit1(v) );
+ //return jdata[v].adir? ~getFaninLit1(v): ~getFaninLit0(v);
} else { // xor scope
// should be handled by conflict analysis before entering here
assert( value(v) == l_Undef || value(v) != l_False || val0 == val1 );
@@ -54,60 +57,68 @@ inline Lit Solver::gateJustFanin(Var v) const {
// a var should at most be enqueued one time
-inline void Solver::pushJustQueue(Var v){
+inline void Solver::pushJustQueue(Var v, int index){
assert(v < nVars());
assert(isJReason(v));
if( ! isRoundWatch(v) )\
return;
+ var2NodeData[v].now = true;
- jdata[v].act_fanin = activity[getFaninVar0(v)] > activity[getFaninVar1(v)]? activity[getFaninVar0(v)]: activity[getFaninVar1(v)];
- jdata[v].now = true;
- jheap.update(v);
+ if( activity[getFaninVar1(v)] > activity[getFaninVar0(v)] )
+ jheap.update( JustKey( activity[getFaninVar1(v)], v, index ) );
+ else
+ jheap.update( JustKey( activity[getFaninVar0(v)], v, index ) );
+}
+
+inline void Solver::uncheckedEnqueue2(Lit p, CRef from)
+{
+ //assert( isRoundWatch(var(p)) ); // inplace sorting guarantee this
+ assert(value(p) == l_Undef);
+ assigns[var(p)] = lbool(!sign(p));
+ vardata[var(p)] = mkVarData(from, decisionLevel());
+ trail.push_(p);
}
inline void Solver::ResetJustData(bool fCleanMemory){
- jstack.shrink_( jstack.size() );
- jheap .clear(fCleanMemory);
+ jhead = 0;
+ jheap .clear_( fCleanMemory );
}
-inline Lit Solver::pickJustLit( Var& j_reason ){
+inline Lit Solver::pickJustLit( int& index ){
Var next = var_Undef;
Lit jlit = lit_Undef;
- for( int i = 0; i < jstack.size(); i ++ ){
- Var x = jstack[i];
- if( l_Undef != value(getFaninLit0(x)) || l_Undef != value(getFaninLit1(x)) )
- continue;
- pushJustQueue(x);
+ for( ; jhead < trail.size() ; jhead++ ){
+ Var x = var(trail[jhead]);
+ if( !decisionLevel() && !isRoundWatch(x) ) continue;
+ if( isJReason(x) && l_Undef == value( getFaninVar0(x) ) && l_Undef == value( getFaninVar1(x) ) )
+ pushJustQueue(x,jhead);
}
- jstack.shrink_( jstack.size() );
- while( ! jheap.empty() && var_Undef != (next = jheap.removeMin()) ){
- if( ! jdata[next].now )
+
+ while( ! jheap.empty() ){
+ next = jheap.removeMin(index);
+ if( ! var2NodeData[next].now )
continue;
assert(isJReason(next));
- if( lit_Undef != (jlit = gateJustFanin(next)) )
+ if( lit_Undef != (jlit = gateJustFanin(next)) ){
+ //assert( jheap.prev.key() == activity[getFaninVar0(next)] || jheap.prev.key() == activity[getFaninVar1(next)] );
break;
- gateAddJwatch(next);
+ }
+ gateAddJwatch(next,index);
}
- j_reason = next;
return jlit;
}
-inline void Solver::gateAddJwatch(Var v){
+inline void Solver::gateAddJwatch(Var v,int index){
assert(v < nVars());
assert(isJReason(v));
- if( var_Undef != jwatch[v].prev ) // already in jwatch
- return;
-
- assert( var_Undef == jwatch[v].prev );
-
lbool val0, val1;
Var var0, var1;
var0 = getFaninVar0(v);
@@ -119,73 +130,38 @@ inline void Solver::gateAddJwatch(Var v){
assert( isAND(v) || (l_Undef != val0 && l_Undef != val1) );
if( (val0 == l_False && val1 == l_False) || !isAND(v) ){
- addJwatch(vardata[var0].level < vardata[var1].level? var0: var1, v);
+ addJwatch(vardata[var0].level < vardata[var1].level? var0: var1, v, index);
return;
}
- addJwatch(l_False == val0? var0: var1, v);
-}
-
-inline void Solver::gateClearJwatch( Var v, int backtrack_level ){
- if( var_Undef == jwatch[v].head )
- return ;
-
- Var member, next;
- member = jwatch[v].head;
- while( var_Undef != member ){
- next = jwatch[member].next;
-
- delJwatch( member );
+ addJwatch(l_False == val0? var0: var1, v, index);
- if( vardata[member].level <= backtrack_level )
- pushJustQueue(member);
-
- member = next;
- }
+ return;
}
inline void Solver::updateJustActivity( Var v ){
- for(Lit lfo = var2Fanout0[ v ]; lfo != toLit(~0); lfo = var2FanoutN[ toInt(lfo) ] ){
+ if( ! var2NodeData[v].sort )
+ inplace_sort(v);
+
+ int nFanout = 0;
+ for(Lit lfo = var2Fanout0[ v ]; nFanout < var2NodeData[v].sort; lfo = var2FanoutN[ toInt(lfo) ], nFanout ++ ){
Var x = var(lfo);
- if( jdata[x].now && jheap.inHeap(x) ){
- jdata[x].act_fanin = activity[getFaninVar0(x)] > activity[getFaninVar1(x)]? activity[getFaninVar0(x)]: activity[getFaninVar1(x)];
- jheap.update(x);
+ if( var2NodeData[x].now && jheap.inHeap(x) ){
+ if( activity[getFaninVar1(x)] > activity[getFaninVar0(x)] )
+ jheap.update( JustKey( activity[getFaninVar1(x)], x, jheap.data_attr(x) ) );
+ else
+ jheap.update( JustKey( activity[getFaninVar0(x)], x, jheap.data_attr(x) ) );
}
}
}
-inline void Solver::addJwatch( Var host, Var member ){
- assert( var_Undef == jwatch[member].next && var_Undef == jwatch[member].prev );
-
- if( var_Undef != jwatch[host].head )
- jwatch[jwatch[host].head].prev = member;
-
- jwatch[member].next = jwatch[host].head;
- jwatch[member].prev = host;
- jwatch[host].head = member;
-}
-
-inline void Solver::delJwatch( Var member ){
- Var prev = jwatch[member].prev;
- Var next = jwatch[member].next;
-
- assert( var_Undef != prev ); // must be in a list to be deleted
- assert( jwatch[prev].next == member || jwatch[prev].head == member );
-
- if( jwatch[prev].next == member )
- jwatch[prev].next = next;
- else
- jwatch[prev].head = next;
-
- if( var_Undef != next )
- jwatch[next].prev = prev;
-
- jwatch[member].prev = var_Undef;
- jwatch[member].next = var_Undef;
+inline void Solver::addJwatch( Var host, Var member, int index ){
+ assert(level(host) >= level(member));
+ jnext[index] = jlevel[level(host)];
+ jlevel[level(host)] = index;
}
-
/*
* circuit propagation
*/
@@ -270,23 +246,12 @@ inline void Solver::setVarFaninLits( Var v, Lit lit1, Lit lit2 ){
int mincap = var(lit1) < var(lit2)? var(lit2): var(lit1);
mincap = (v < mincap? mincap: v) + 1;
- if( var2FaninLits.size() < (mincap<<1) )
- var2FaninLits.growTo( (mincap<<1), toLit(~0));
- assert( (toLit(~0) == lit1 && toLit(~0) == lit2) || ((v<<1)+1 < var2FaninLits.size()) );
- var2FaninLits[ (v<<1) + 0 ] = lit1;
- var2FaninLits[ (v<<1) + 1 ] = lit2;
+ var2NodeData[ v ].lit0 = lit1;
+ var2NodeData[ v ].lit1 = lit2;
assert( toLit(~0) != lit1 && toLit(~0) != lit2 );
-
- if( var2FanoutN.size() < (mincap<<1) )
- var2FanoutN.growTo( (mincap<<1), toLit(~0));
- //if( var2FanoutP.size() < (mincap<<1) )
- // var2FanoutP.growTo( (mincap<<1), toLit(~0));
- if( var2Fanout0.size() < mincap )
- var2Fanout0.growTo( mincap, toLit(~0));
-
var2FanoutN[ (v<<1) + 0 ] = var2Fanout0[ var(lit1) ];
var2FanoutN[ (v<<1) + 1 ] = var2Fanout0[ var(lit2) ];
var2Fanout0[ var(lit1) ] = toLit( (v<<1) + 0 );
@@ -301,22 +266,19 @@ inline void Solver::setVarFaninLits( Var v, Lit lit1, Lit lit2 ){
inline bool Solver::isTwoFanin( Var v ) const {
- assert(v < nVars());
- if( var2FaninLits.size() <= (v<<1)+1 )
- return false;
- Lit lit0 = var2FaninLits[ (v<<1) + 0 ];
- Lit lit1 = var2FaninLits[ (v<<1) + 1 ];
+ Lit lit0 = var2NodeData[ v ].lit0;
+ Lit lit1 = var2NodeData[ v ].lit1;
assert( toLit(~0) == lit0 || var(lit0) < nVars() );
assert( toLit(~0) == lit1 || var(lit1) < nVars() );
lit0.x = lit1.x = 0; // suppress the warning - alanmi
- return toLit(~0) != var2FaninLits[ (v<<1) + 0 ] && toLit(~0) != var2FaninLits[ (v<<1) + 1 ];
+ return toLit(~0) != var2NodeData[ v ].lit0 && toLit(~0) != var2NodeData[ v ].lit1;
}
// this implementation return the last conflict encountered
// which follows minisat concept
inline CRef Solver::gatePropagate( Lit p ){
CRef confl = CRef_Undef, stats;
- if( justUsage() < 2 || var2FaninLits.size() <= var(p) )
+ if( justUsage() < 2 )
return CRef_Undef;
if( ! isRoundWatch(var(p)) )
@@ -337,10 +299,12 @@ inline CRef Solver::gatePropagate( Lit p ){
check_fanout:
assert( var(p) < var2Fanout0.size() );
- for( Lit lfo = var2Fanout0[ var(p) ]; lfo != toLit(~0); lfo = var2FanoutN[ toInt(lfo) ] )
- {
- if( ! isRoundWatch(var(lfo)) ) continue;
+ if( ! var2NodeData[var(p)].sort )
+ inplace_sort(var(p));
+ int nFanout = 0;
+ for( Lit lfo = var2Fanout0[ var(p) ]; nFanout < var2NodeData[var(p)].sort; lfo = var2FanoutN[ toInt(lfo) ], nFanout ++ )
+ {
if( CRef_Undef != (stats = gatePropagateCheckFanout( var(p), lfo )) ){
confl = stats;
if( l_True == value(var(lfo)) )
@@ -363,8 +327,8 @@ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
if( l_True == value(var(lfo)) )
return Var2CRef(var(lfo));
- jwatch[var(lfo)].header.dir = sign(lfo);
- uncheckedEnqueue(~mkLit(var(lfo)), Var2CRef( var(lfo) ) );
+ var2NodeData[var(lfo)].dir = sign(lfo);
+ uncheckedEnqueue2(~mkLit(var(lfo)), Var2CRef( var(lfo) ) );
} else {
assert( l_True == value(faninLit) );
@@ -381,11 +345,11 @@ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
if( l_True == value(faninLitP) )
return Var2CRef(var(lfo));
- uncheckedEnqueue( ~faninLitP, Var2CRef( var(lfo) ) );
+ uncheckedEnqueue2( ~faninLitP, Var2CRef( var(lfo) ) );
}
else
if( l_True == value(faninLitP) )
- uncheckedEnqueue( mkLit(var(lfo)), Var2CRef( var(lfo) ) );
+ uncheckedEnqueue2( mkLit(var(lfo)), Var2CRef( var(lfo) ) );
}
} else { // xor scope
// check value of the other fanin
@@ -400,10 +364,10 @@ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
return CRef_Undef;
else
if( l_Undef == val1 )
- uncheckedEnqueue( ~faninLitP ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( var(lfo) ) );
+ uncheckedEnqueue2( ~faninLitP ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( var(lfo) ) );
else
if( l_Undef == valo )
- uncheckedEnqueue( ~mkLit( var(lfo), (l_True == val0) ^ (l_True == val1) ), Var2CRef( var(lfo) ) );
+ uncheckedEnqueue2( ~mkLit( var(lfo), (l_True == val0) ^ (l_True == val1) ), Var2CRef( var(lfo) ) );
else
if( l_False == (valo ^ (val0 == val1)) )
return Var2CRef(var(lfo));
@@ -424,19 +388,19 @@ inline CRef Solver::gatePropagateCheckThis( Var v ){
return CRef_Undef;
if( l_True == value(getFaninLit0(v)) )
- uncheckedEnqueue(~getFaninLit1( v ), Var2CRef( v ) );
+ uncheckedEnqueue2(~getFaninLit1( v ), Var2CRef( v ) );
if( l_True == value(getFaninLit1(v)) )
- uncheckedEnqueue(~getFaninLit0( v ), Var2CRef( v ) );
+ uncheckedEnqueue2(~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 )) )
- uncheckedEnqueue( getFaninLit0( v ), Var2CRef( v ) );
+ uncheckedEnqueue2( getFaninLit0( v ), Var2CRef( v ) );
if( l_Undef == value( getFaninLit1( v )) )
- uncheckedEnqueue( getFaninLit1( v ), Var2CRef( v ) );
+ uncheckedEnqueue2( getFaninLit1( v ), Var2CRef( v ) );
}
} else { // xor scope
@@ -447,10 +411,10 @@ inline CRef Solver::gatePropagateCheckThis( Var v ){
if( l_Undef == val0 && l_Undef == val1 )
return CRef_Undef;
if( l_Undef == val0 )
- uncheckedEnqueue(~getFaninLit0( v ) ^ ( (l_True == val1) ^ (l_True == valo) ), Var2CRef( v ) );
+ uncheckedEnqueue2(~getFaninLit0( v ) ^ ( (l_True == val1) ^ (l_True == valo) ), Var2CRef( v ) );
else
if( l_Undef == val1 )
- uncheckedEnqueue(~getFaninLit1( v ) ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( v ) );
+ uncheckedEnqueue2(~getFaninLit1( v ) ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( v ) );
else
if( l_False == (valo ^ (val0 == val1)) )
return Var2CRef(v);
@@ -530,13 +494,7 @@ inline CRef Solver::interpret( Var v, Var t )
Clause& c = ca[itpc];
c[0] = ~mkLit(v);
- if( l_False == val0 && l_False == val1 )
- c[1] = 0 == jwatch[v].header.dir ? getFaninLit0( v ): getFaninLit1( v );
- else
- if( l_False == val0 )
- c[1] = getFaninLit0( v );
- else
- c[1] = getFaninLit1( v );
+ c[1] = var2NodeData[v].dir ? getFaninLit1( v ): getFaninLit0( v );
} else {
setItpcSize(3);
Clause& c = ca[itpc];
@@ -594,11 +552,65 @@ inline void Solver::markCone( Var v ){
if( var2TravId[v] >= travId )
return;
var2TravId[v] = travId;
-
+ var2NodeData[v].sort = 0;
+ Var var0, var1;
+ var0 = getFaninVar0(v);
+ var1 = getFaninVar1(v);
if( !isTwoFanin(v) )
return;
- markCone( getFaninVar0(v) );
- markCone( getFaninVar1(v) );
+ markCone( var0 );
+ markCone( var1 );
+}
+
+inline void Solver::inplace_sort( Var v ){
+ Lit w, next, prev;
+ prev= var2Fanout0[v];
+
+ if( toLit(~0) == prev ) return;
+
+ if( isRoundWatch(var(prev)) )
+ var2NodeData[v].sort ++ ;
+
+ if( toLit(~0) == (w = var2FanoutN[toInt(prev)]) )
+ return;
+
+ while( toLit(~0) != w ){
+ next = var2FanoutN[toInt(w)];
+ if( isRoundWatch(var(w)) )
+ var2NodeData[v].sort ++ ;
+ if( isRoundWatch(var(w)) && !isRoundWatch(var(prev)) ){
+ var2FanoutN[toInt(w)] = var2Fanout0[v];
+ var2Fanout0[v] = w;
+ var2FanoutN[toInt(prev)] = next;
+ } else
+ prev = w;
+ w = next;
+ }
+}
+
+inline void Solver::prelocate( int base_var_num ){
+ if( justUsage() ){
+ var2FanoutN .prelocate( base_var_num << 1 );
+ var2Fanout0 .prelocate( base_var_num );
+ var2NodeData.prelocate( base_var_num );
+ var2TravId .prelocate( base_var_num );
+ jheap .prelocate( base_var_num );
+ jlevel .prelocate( base_var_num );
+ jnext .prelocate( base_var_num );
+ }
+ watches .prelocate( base_var_num << 1 );
+ watchesBin .prelocate( base_var_num << 1 );
+
+ decision .prelocate( base_var_num );
+ trail .prelocate( base_var_num );
+ assigns .prelocate( base_var_num );
+ vardata .prelocate( base_var_num );
+ activity .prelocate( base_var_num );
+
+
+ seen .prelocate( base_var_num );
+ permDiff .prelocate( base_var_num );
+ polarity .prelocate( base_var_num );
}
};
diff --git a/src/sat/glucose2/Glucose2.cpp b/src/sat/glucose2/Glucose2.cpp
index e7e3862b..7a8b265b 100644
--- a/src/sat/glucose2/Glucose2.cpp
+++ b/src/sat/glucose2/Glucose2.cpp
@@ -151,7 +151,8 @@ Solver::Solver() :
, nbVarsInitialFormula(INT32_MAX)
#ifdef CGLUCOSE_EXP
- , jheap (JustOrderLt(this))
+ //, jheap (JustOrderLt(this))
+ , jheap (JustOrderLt2(this))
#endif
{
MYFLAG=0;
@@ -175,6 +176,7 @@ Solver::Solver() :
}
#ifdef CGLUCOSE_EXP
+ jhead= 0;
jftr = 0;
travId = 0;
travId_prev = 0;
@@ -233,18 +235,28 @@ Var Solver::newVar(bool sign, bool dvar)
polarity .push(sign);
decision .push();
trail .capacity(v+1);
- setDecisionVar(v, dvar);
+
#ifdef CGLUCOSE_EXP
//jreason .capacity(v+1);
if( justUsage() ){
- jdata .push(mkJustData(false));
- jwatch .push(mkJustWatch());
- var2FanoutN.growTo( nVars()<<1, toLit(~0));
- //var2FanoutP.growTo( nVars()<<1, toLit(~0));
- var2Fanout0.growTo( nVars(), toLit(~0));
- var2TravId .growTo( nVars(), 0);
- }
+ //jdata .push(mkJustData(false));
+ //jwatch .push(mkJustWatch());
+
+ jlevel .push(-1);
+ jnext .push(-1);
+
+ var2FanoutN.growTo( nVars()<<1, toLit(~0));
+ //var2FanoutP.growTo( nVars()<<1, toLit(~0));
+ var2Fanout0.growTo( nVars(), toLit(~0));
+ var2NodeData.growTo( nVars(), mkNodeData());
+ var2TravId .growTo( nVars(), 0);
+
+ setDecisionVar(v, dvar, false);
+ } else
+ setDecisionVar(v, dvar);
+ #else
+ setDecisionVar(v, dvar);
#endif
return v;
@@ -283,7 +295,7 @@ bool Solver::addClause_(vec<Lit>& ps)
return true;
else if (value(ps[i]) != l_False && ps[i] != p)
ps[j++] = p = ps[i];
- ps.shrink(i - j);
+ ps.shrink_(i - j);
if ( 0 ) {
for ( int i = 0; i < ps.size(); i++ )
@@ -502,31 +514,45 @@ void Solver::minimisationWithBinaryResolution(vec<Lit> &out_learnt) {
void Solver::cancelUntil(int level) {
if (decisionLevel() > level){
- for (int c = trail.size()-1; c >= trail_lim[level]; c--){
- Var x = var(trail[c]);
- assigns [x] = l_Undef;
- if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
- polarity[x] = sign(trail[c]);
- insertVarOrder(x); }
- qhead = trail_lim[level];
-
-
-
#ifdef CGLUCOSE_EXP
if( 0 < justUsage() ){
- for (int c = trail.size()-1; c >= trail_lim[level]; c--){
- Var x = var(trail[c]);
- gateClearJwatch(x, level);
+ for (int c = trail.size()-1; c >= trail_lim[level]; c--){
+ Var x = var(trail[c]);
+ assigns [x] = l_Undef;
+ if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
+ polarity[x] = sign(trail[c]);
+ //gateClearJwatch(x, level);
- jdata[x].now = false;
- }
- }
+ var2NodeData[x].now = false;
+ }
+ for (int l = decisionLevel(); l > level; l -- ){
+ int q = jlevel[l], k;
+ jlevel[l] = -1;
+ while( -1 != q ){
+ k = jnext[q];
+ jnext[q] = -1;
+ Var v = var(trail[q]);
+ if( Solver::level(v) <= level ){
+ pushJustQueue(v,q);
+ }
+ q = k;
+ }
+ }
+ } else
#endif
+ for (int c = trail.size()-1; c >= trail_lim[level]; c--){
+ Var x = var(trail[c]);
+ assigns [x] = l_Undef;
+ if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last()))
+ polarity[x] = sign(trail[c]);
+ insertVarOrder(x);
+ }
+
+ jhead = qhead = trail_lim[level];
trail.shrink_(trail.size() - trail_lim[level]);
trail_lim.shrink_(trail_lim.size() - level);
- jstack.shrink_( jstack.size() );
}
}
@@ -577,6 +603,7 @@ Lit Solver::pickBranchLit()
void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& out_btlevel,unsigned int &lbd,unsigned int &szWithoutSelectors)
{
//double clk = Abc_Clock();
+ heap_rescale = 0;
int pathC = 0;
Lit p = lit_Undef;
@@ -586,22 +613,23 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
out_learnt.push(); // (leave room for the asserting literal)
int index = trail.size() - 1;
+ analyze_toclear.shrink_( analyze_toclear.size() );
do{
assert(confl != CRef_Undef); // (otherwise should be UIP)
- #ifdef CGLUCOSE_EXP
+ #ifdef CGLUCOSE_EXP
Clause& c = ca[ lit_Undef != p ? castCRef(p): getConfClause(confl) ];
- #else
+ #else
Clause& c = ca[confl];
- #endif
+ #endif
// Special case for binary clauses
// The first one has to be SAT
if( p != lit_Undef && c.size()==2 && value(c[0])==l_False) {
-
- assert(value(c[1])==l_True);
- Lit tmp = c[0];
- c[0] = c[1], c[1] = tmp;
+
+ assert(value(c[1])==l_True);
+ Lit tmp = c[0];
+ c[0] = c[1], c[1] = tmp;
}
if (c.learnt())
@@ -610,46 +638,51 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
#ifdef DYNAMICNBLEVEL
// DYNAMIC NBLEVEL trick (see competition'09 companion paper)
if(c.learnt() && c.lbd()>2) {
- unsigned int nblevels = computeLBD(c);
- if(nblevels+1<c.lbd() ) { // improve the LBD
- if(c.lbd()<=lbLBDFrozenClause) {
- c.setCanBeDel(false);
+ unsigned int nblevels = computeLBD(c);
+ if(nblevels+1<c.lbd() ) { // improve the LBD
+ if(c.lbd()<=lbLBDFrozenClause) {
+ c.setCanBeDel(false);
+ }
+ // seems to be interesting : keep it for the next round
+ c.setLBD(nblevels); // Update it
}
- // seems to be interesting : keep it for the next round
- c.setLBD(nblevels); // Update it
- }
}
#endif
for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
Lit q = c[j];
+ bool fBump = 0;
if (!seen[var(q)] && level(var(q)) > 0){
- if(!isSelector(var(q)))
- varBumpActivity(var(q));
- seen[var(q)] = 1;
- if (level(var(q)) >= decisionLevel()) {
- pathC++;
-#ifdef UPDATEVARACTIVITY
- // UPDATEVARACTIVITY trick (see competition'09 companion paper)
- #ifdef CGLUCOSE_EXP
- if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef)
- && ! isGateCRef(reason(var(q))) && ca[reason(var(q))].learnt())
- lastDecisionLevel.push(q);
- #else
- if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef) && ca[reason(var(q))].learnt())
- lastDecisionLevel.push(q);
- #endif
-#endif
-
- } else {
- if(isSelector(var(q))) {
- assert(value(q) == l_False);
- selectors.push(q);
- } else
- out_learnt.push(q);
- }
+ if(!isSelector(var(q))){
+ fBump = 1;
+ varBumpActivity(var(q));
+ }
+ seen[var(q)] = 1;
+ if (level(var(q)) >= decisionLevel()) {
+ if( fBump )
+ analyze_toclear.push(q);
+ pathC++;
+ #ifdef UPDATEVARACTIVITY
+ // UPDATEVARACTIVITY trick (see competition'09 companion paper)
+ #ifdef CGLUCOSE_EXP
+ if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef)
+ && ! isGateCRef(reason(var(q))) && ca[reason(var(q))].learnt())
+ lastDecisionLevel.push(q);
+ #else
+ if(!isSelector(var(q)) && (reason(var(q))!= CRef_Undef) && ca[reason(var(q))].learnt())
+ lastDecisionLevel.push(q);
+ #endif
+ #endif
+
+ } else {
+ if(isSelector(var(q))) {
+ assert(value(q) == l_False);
+ selectors.push(q);
+ } else
+ out_learnt.push(q);
+ }
}
}
@@ -667,10 +700,15 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
//
int i, j;
- for(i = 0;i<selectors.size();i++)
- out_learnt.push(selectors[i]);
+ for(i = 0;i<selectors.size();i++) out_learnt.push(selectors[i]);
+
+ #ifdef CGLUCOSE_EXP
+ for(i = 0;i<out_learnt.size();i++)
+ analyze_toclear.push(out_learnt[i]);
+ #else
out_learnt.copyTo_(analyze_toclear);
+ #endif
if (ccmin_mode == 2){
uint32_t abstract_level = 0;
for (i = 1; i < out_learnt.size(); i++)
@@ -749,29 +787,51 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
#ifdef UPDATEVARACTIVITY
- // UPDATEVARACTIVITY trick (see competition'09 companion paper)
- if(lastDecisionLevel.size()>0) {
- for(int i = 0;i<lastDecisionLevel.size();i++) {
-
- #ifdef CGLUCOSE_EXP
- Lit t = lastDecisionLevel[i];
- if( isGateCRef(reason(var(t))) || ca[reason(var(t))].lbd()<lbd )
- varBumpActivity(var(lastDecisionLevel[i]));
- #else
- if(ca[reason(var(lastDecisionLevel[i]))].lbd()<lbd)
- varBumpActivity(var(lastDecisionLevel[i]));
- #endif
-
- }
- lastDecisionLevel.clear();
- }
-#endif
+ // UPDATEVARACTIVITY trick (see competition'09 companion paper)
+ if(lastDecisionLevel.size()>0) {
+ for(int i = 0;i<lastDecisionLevel.size();i++) {
+ Lit t = lastDecisionLevel[i];
+ //assert( ca[reason(var(t))].learnt() );
+ if(ca[reason(var(t))].lbd()<lbd)
+ varBumpActivity(var(t));
+ }
+ lastDecisionLevel.shrink_( lastDecisionLevel.size() );
+ }
+#endif
+ if( justUsage() ){
+ if( heap_rescale )
+ {
+ for (j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;
+
+ analyze_toclear.shrink_( analyze_toclear.size() );
+ for (j = 0; j < jheap.size(); j++){
+ Var x = jheap[j];
+ if( var2NodeData[x].now )
+ analyze_toclear.push(mkLit(x));
+ }
+ for (j = 0; j < analyze_toclear.size(); j++){
+ Var x = var(analyze_toclear[j]);
+// jdata[x].act_fanin = activity[getFaninVar0(x)] > activity[getFaninVar1(x)]? activity[getFaninVar0(x)]: activity[getFaninVar1(x)];
+// jheap.update(x);
+ if( activity[getFaninVar1(x)] > activity[getFaninVar0(x)] )
+ jheap.update( JustKey( activity[getFaninVar1(x)], x, jheap.data_attr(x) ) );
+ else
+ jheap.update( JustKey( activity[getFaninVar0(x)], x, jheap.data_attr(x) ) );
+ }
- for (j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared)
- for(j = 0 ; j<selectors.size() ; j++) seen[var(selectors[j])] = 0;
+ } else {
+ for (j = 0; j < analyze_toclear.size(); j++)
+ {
+ seen[var(analyze_toclear[j])] = 0;
+ updateJustActivity(var(analyze_toclear[j]));
+ }
+ }
+ } else
+ for (j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared)
+ for(j = 0 ; j<selectors.size() ; j++) seen[var(selectors[j])] = 0;
}
@@ -779,7 +839,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
// visiting literals at levels that cannot be removed later.
bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
{
- analyze_stack.clear(); analyze_stack.push(p);
+ analyze_stack.shrink_( analyze_stack.size() ); analyze_stack.push(p);
int top = analyze_toclear.size();
while (analyze_stack.size() > 0){
assert(reason(var(analyze_stack.last())) != CRef_Undef);
@@ -826,7 +886,7 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
|________________________________________________________________________________________________@*/
void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
{
- out_conflict.clear();
+ out_conflict.shrink_( out_conflict.size() );
out_conflict.push(p);
if (decisionLevel() == 0)
@@ -863,17 +923,12 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
void Solver::uncheckedEnqueue(Lit p, CRef from)
{
+ if( justUsage() && !isRoundWatch(var(p)) )
+ return;
assert(value(p) == l_Undef);
assigns[var(p)] = lbool(!sign(p));
vardata[var(p)] = mkVarData(from, decisionLevel());
trail.push_(p);
- #ifdef CGLUCOSE_EXP
- if( 0 < justUsage() ){
- jdata[var(p)] = mkJustData( isJReason(var(p)) );
- if( isJReason(var(p)) && l_Undef == value( getFaninVar0(var(p)) ) && l_Undef == value( getFaninVar1(var(p)) ) )
- jstack.push(var(p));
- }
- #endif
}
@@ -902,13 +957,11 @@ CRef Solver::propagate()
#ifdef CGLUCOSE_EXP
if( 2 <= justUsage() ){
- CRef stats;
- if( CRef_Undef != (stats = gatePropagate(p)) ){
- confl = stats;
- if( l_True == value(var(p)) )
- return confl;
-
- }
+ CRef stats;
+ if( CRef_Undef != (stats = gatePropagate(p)) ){
+ confl = stats;
+ if( l_True == value(var(p)) ) return confl;
+ }
}
#endif
@@ -995,7 +1048,7 @@ CRef Solver::propagate()
}
NextClause:;
}
- ws.shrink(i - j);
+ ws.shrink_(i - j);
}
propagations += num_props;
simpDB_props -= num_props;
@@ -1065,7 +1118,7 @@ void Solver::reduceDB()
learnts[j++] = learnts[i];
}
}
- learnts.shrink(i - j);
+ learnts.shrink_(i - j);
checkGarbage();
}
@@ -1080,7 +1133,7 @@ void Solver::removeSatisfied(vec<CRef>& cs)
else
cs[j++] = cs[i];
}
- cs.shrink(i - j);
+ cs.shrink_(i - j);
}
@@ -1119,7 +1172,10 @@ bool Solver::simplify()
checkGarbage();
- rebuildOrderHeap();
+ #ifdef CGLUCOSE_EXP
+ if( !justUsage() )
+ #endif
+ rebuildOrderHeap();
simpDB_assigns = nAssigns();
simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now)
@@ -1185,8 +1241,8 @@ lbool Solver::search(int nof_conflicts)
if(!blocked) {lastblockatrestart=starts;nbstopsrestartssame++;blocked=true;}
}
- learnt_clause.clear();
- selectors.clear();
+ learnt_clause.shrink_( learnt_clause.size() );
+ selectors .shrink_( selectors.size() );
analyze(confl, learnt_clause, selectors,backtrack_level,nblevels,szWoutSelectors);
lbdQueue.push(nblevels);
@@ -1217,31 +1273,30 @@ lbool Solver::search(int nof_conflicts)
claDecayActivity();
}else{
- // Our dynamic restart, see the SAT09 competition compagnion paper
- if ( (conflictsRestarts && lbdQueue.isvalid() && lbdQueue.getavg()*K > sumLBD/conflictsRestarts) || (pstop && *pstop) ) {
- lbdQueue.fastclear();
- progress_estimate = progressEstimate();
- int bt = 0;
- if(incremental) { // DO NOT BACKTRACK UNTIL 0.. USELESS
- bt = (decisionLevel()<assumptions.size()) ? decisionLevel() : assumptions.size();
+ // Our dynamic restart, see the SAT09 competition compagnion paper
+ if ( (conflictsRestarts && lbdQueue.isvalid() && lbdQueue.getavg()*K > sumLBD/conflictsRestarts) || (pstop && *pstop) ) {
+ lbdQueue.fastclear();
+ progress_estimate = progressEstimate();
+ int bt = 0;
+ if(incremental) { // DO NOT BACKTRACK UNTIL 0.. USELESS
+ bt = (decisionLevel()<assumptions.size()) ? decisionLevel() : assumptions.size();
+ }
+ cancelUntil(bt);
+ return l_Undef;
}
- cancelUntil(bt);
- return l_Undef;
- }
- // Simplify the set of problem clauses:
- if (decisionLevel() == 0 && !simplify()) {
- return l_False;
- }
+ // Simplify the set of problem clauses:
+ if (decisionLevel() == 0 && !simplify()) {
+ return l_False;
+ }
// Perform clause database reduction !
- if(conflicts>=curRestart* nbclausesbeforereduce)
- {
-
+ if(conflicts>=curRestart* nbclausesbeforereduce)
+ {
assert(learnts.size()>0);
curRestart = (conflicts/ nbclausesbeforereduce)+1;
reduceDB();
nbclausesbeforereduce += incReduceDB;
- }
+ }
Lit next = lit_Undef;
while (decisionLevel() < assumptions.size()){
@@ -1250,10 +1305,10 @@ lbool Solver::search(int nof_conflicts)
if (value(p) == l_True){
// Dummy decision level:
newDecisionLevel();
- }else if (value(p) == l_False){
+ } else if (value(p) == l_False){
analyzeFinal(~p, conflict);
return l_False;
- }else{
+ } else {
next = p;
break;
}
@@ -1261,15 +1316,17 @@ lbool Solver::search(int nof_conflicts)
#ifdef CGLUCOSE_EXP
// pick from JustQueue
- Var j_reason = -1;
+
if (0 < justUsage())
if ( next == lit_Undef ){
- decisions++;
- next = pickJustLit( j_reason );
- if(next == lit_Undef)
- return l_True;
- addJwatch(var(next), j_reason);
-
+ int index = -1;
+ decisions++;
+ next = pickJustLit( index );
+ if(next == lit_Undef)
+ return l_True;
+ //addJwatch(var(next), j_reason);
+ jnext[index] = jlevel[decisionLevel()+1];
+ jlevel[decisionLevel()+1] = index;
}
#endif
@@ -1335,21 +1392,13 @@ lbool Solver::solve_()
#ifdef CGLUCOSE_EXP
ResetJustData(false);
-
- if( 0 < justUsage() )
- for(int i=0; i<trail.size(); i++){ // learnt unit clauses
- Var v = var(trail[i]);
- if( isJReason(v) )
- jstack.push(v);
- }
#endif
- if(incremental && certifiedUNSAT) {
- printf("Can not use incremental and certified unsat in the same time\n");
- exit(-1);
- }
- JustModel.shrink_(JustModel.size());
- model.shrink_(model.size());
+ if(incremental && certifiedUNSAT) {
+ printf("Can not use incremental and certified unsat in the same time\n");
+ exit(-1);
+ }
+
conflict.shrink_(conflict.size());
if (!ok){
travId_prev = travId;
@@ -1403,18 +1452,20 @@ printf("c ==================================[ Search Statistics (every %6d confl
if (status == l_True){
if( justUsage() ){
- assert(jheap.empty());
- //JustModel.growTo(nVars());
- 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]), j++;
- JustModel[0] = toLit(j);
+ JustModel.shrink_(JustModel.size());
+ assert(jheap.empty());
+ //JustModel.growTo(nVars());
+ 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]), j++;
+ JustModel[0] = toLit(j);
} else {
- // Extend & copy model:
- model.growTo(nVars());
- for (int i = 0; i < trail.size(); i++) model[ var(trail[i]) ] = value(var(trail[i]));
+ // Extend & copy model:
+ model.shrink_(model.size());
+ model.growTo(nVars());
+ for (int i = 0; i < trail.size(); i++) model[ var(trail[i]) ] = value(var(trail[i]));
}
}else if (status == l_False && conflict.size() == 0)
ok = false;
@@ -1669,25 +1720,28 @@ void Solver::reset()
ResetJustData(false);
- jwatch.shrink_(jwatch.size());
- jdata .shrink_(jdata .size());
-
+ //jwatch.shrink_(jwatch.size());
+ //jdata .shrink_(jdata .size());
+ jhead = 0;
travId = 0;
travId_prev = 0;
var2TravId .shrink_(var2TravId.size());
JustModel .shrink_(JustModel .size());
+ jlevel .shrink_(jlevel.size());
+ jnext .shrink_(jnext.size());
- var2FaninLits.shrink_(var2FaninLits.size());
+ //var2FaninLits.shrink_(var2FaninLits.size());
+ var2NodeData .shrink_(var2NodeData .size());
var2Fanout0 .shrink_(var2Fanout0 .size());
var2FanoutN .shrink_(var2FanoutN .size());
//var2FanoutP.clear(false);
if( CRef_Undef != itpc ){
- itpc = CRef_Undef; // clause allocator has been cleared, do not worry
- // allocate space for clause interpretation
- vec<Lit> tmp; tmp.growTo(3);
- itpc = ca.alloc(tmp);
- ca[itpc].shrink( ca[itpc].size() );
+ itpc = CRef_Undef; // clause allocator has been cleared, do not worry
+ // allocate space for clause interpretation
+ vec<Lit> tmp; tmp.growTo(3);
+ itpc = ca.alloc(tmp);
+ ca[itpc].shrink( ca[itpc].size() );
}
#endif
}
diff --git a/src/sat/glucose2/Heap.h b/src/sat/glucose2/Heap.h
index 9999fba5..d68229f6 100644
--- a/src/sat/glucose2/Heap.h
+++ b/src/sat/glucose2/Heap.h
@@ -85,7 +85,7 @@ class Heap {
void decrease (int n) { assert(inHeap(n)); percolateUp (indices[n]); }
void increase (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
-
+ void prelocate (int ext_cap){ indices.prelocate(ext_cap); }
// Safe variant of insert/decrease/increase:
void update(int n)
@@ -143,6 +143,15 @@ class Heap {
indices[heap[i]] = -1;
heap.clear(dealloc);
}
+ void clear_(bool dealloc = false)
+ {
+ int i;
+ for (i = 0; i < heap.size(); i++)
+ indices[heap[i]] = -1;
+
+ if( ! dealloc ) heap.shrink_( heap.size() );
+ else heap.clear(true);
+ }
};
diff --git a/src/sat/glucose2/Heap2.h b/src/sat/glucose2/Heap2.h
new file mode 100644
index 00000000..ef6d8302
--- /dev/null
+++ b/src/sat/glucose2/Heap2.h
@@ -0,0 +1,169 @@
+/******************************************************************************************[Heap.h]
+Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
+Copyright (c) 2007-2010, Niklas Sorensson
+
+Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
+associated documentation files (the "Software"), to deal in the Software without restriction,
+including without limitation the rights to use, copy, modify, merge, publish, distribute,
+sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all copies or
+substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
+NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
+NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
+OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+**************************************************************************************************/
+
+#ifndef Glucose_Heap2_h
+#define Glucose_Heap2_h
+
+#include "sat/glucose2/Vec.h"
+
+ABC_NAMESPACE_CXX_HEADER_START
+
+namespace Gluco2 {
+
+//=================================================================================================
+// A heap implementation with support for decrease/increase key.
+
+
+template<class Comp, class Obj>
+class Heap2 {
+ Comp lt; // The heap is a minimum-heap with respect to this comparator
+ vec<Obj> heap; // Heap of integers
+ vec<int> indices; // Each integers position (index) in the Heap
+
+ // Index "traversal" functions
+ static inline int left (int i) { return i*2+1; }
+ static inline int right (int i) { return (i+1)*2; }
+ static inline int parent(int i) { return (i-1) >> 1; }
+
+ inline int data (int i) const { return heap[i].data();}
+
+ void percolateUp(int i)
+ {
+ Obj x = heap[i];
+ int p = parent(i);
+
+ while (i != 0 && lt(x, heap[p])){
+ heap[i] = heap[p];
+ indices[data(p)] = i;
+ i = p;
+ p = parent(p);
+ }
+ heap [i] = x;
+ indices[x.data()] = i;
+ }
+
+
+ void percolateDown(int i)
+ {
+ Obj x = heap[i];
+ while (left(i) < heap.size()){
+ int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i);
+ if (!lt(heap[child], x)) break;
+ heap[i] = heap[child];
+ indices[data(i)] = i;
+ i = child;
+ }
+ heap [i] = x;
+ indices[x.data()] = i;
+ }
+
+
+ public:
+ Heap2(const Comp& c) : lt(c) { }
+
+ int size () const { return heap.size(); }
+ bool empty () const { return heap.size() == 0; }
+ bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; }
+ int operator[](int index) const { assert(index < heap.size()); return heap[index].data(); }
+
+
+ void decrease (int n) { assert(inHeap(n)); percolateUp (indices[n]); }
+ void increase (int n) { assert(inHeap(n)); percolateDown(indices[n]); }
+ void prelocate (int ext_cap){ indices.prelocate(ext_cap); }
+ int data_attr (int n) const { return heap[indices[n]].attr(); }
+ // Safe variant of insert/decrease/increase:
+ void update(const Obj& x)
+ {
+ int n = x.data();
+ if (!inHeap(n))
+ insert(x);
+ else {
+ heap[indices[x.data()]] = x;
+ percolateUp(indices[n]);
+ percolateDown(indices[n]); }
+ }
+
+
+ void insert(const Obj& x)
+ {
+ int n = x.data();
+ indices.growTo(n+1, -1);
+ assert(!inHeap(n));
+
+ indices[n] = heap.size();
+ heap.push(x);
+ percolateUp(indices[n]);
+ }
+
+ //Obj prev;
+ int removeMin(int& _attr)
+ {
+ Obj x = heap[0];
+ heap[0] = heap.last();
+ indices[heap[0].data()] = 0;
+ indices[x.data()]= -1;
+ heap.pop();
+ if (heap.size() > 1) percolateDown(0);
+ //prev = x;
+ _attr = x.attr();
+ return x.data();
+ }
+
+
+ // Rebuild the heap from scratch, using the elements in 'ns':
+// void build(vec<int>& ns) {
+// int i;
+// for (i = 0; i < heap.size(); i++)
+// indices[heap[i]] = -1;
+// heap.clear();
+//
+// for (i = 0; i < ns.size(); i++){
+// indices[ns[i]] = i;
+// heap.push(ns[i]); }
+//
+// for (i = heap.size() / 2 - 1; i >= 0; i--)
+// percolateDown(i);
+// }
+
+ void clear(bool dealloc = false)
+ {
+ int i;
+ for (i = 0; i < heap.size(); i++)
+ indices[heap[i].data()] = -1;
+ heap.clear(dealloc);
+ }
+ void clear_(bool dealloc = false)
+ {
+ int i;
+ for (i = 0; i < heap.size(); i++)
+ indices[heap[i].data()] = -1;
+
+ if( ! dealloc ) heap.shrink_( heap.size() );
+ else heap.clear(true);
+ }
+};
+
+
+//=================================================================================================
+}
+
+ABC_NAMESPACE_CXX_HEADER_END
+
+#endif
diff --git a/src/sat/glucose2/SimpSolver.h b/src/sat/glucose2/SimpSolver.h
index 00dbfa4c..36d625e9 100644
--- a/src/sat/glucose2/SimpSolver.h
+++ b/src/sat/glucose2/SimpSolver.h
@@ -61,12 +61,25 @@ class SimpSolver : public Solver {
//
bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
+ int solveLimited(int * lit0, int nlits, bool do_simp = false, bool turn_off_simp = false);
bool solve ( bool do_simp = true, bool turn_off_simp = false);
bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false);
bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification.
+ void prelocate(int base_var_num){
+ Solver::prelocate(base_var_num);
+ frozen .prelocate( base_var_num );
+ eliminated.prelocate( base_var_num );
+
+ if (use_simplification){
+ n_occ .prelocate( base_var_num << 1 );
+ occurs .prelocate( base_var_num );
+ touched .prelocate( base_var_num );
+ elim_heap .prelocate( base_var_num );
+ }
+ }
// Memory managment:
//
virtual void reset();
@@ -199,6 +212,14 @@ inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, boo
inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
+inline int SimpSolver::solveLimited(int * lit0, int nlits, bool do_simp, bool turn_off_simp){
+ assumptions.clear();
+ for(int i = 0; i < nlits; i ++)
+ assumptions.push(toLit(lit0[i]));
+ lbool res = solve_(do_simp, turn_off_simp);
+ return res == l_True ? 1 : (res == l_False ? -1 : 0);
+}
+
inline void SimpSolver::addVar(Var v) { while (v >= nVars()) newVar(); }
//=================================================================================================
diff --git a/src/sat/glucose2/SimpSolver2.cpp b/src/sat/glucose2/SimpSolver2.cpp
index 7c2a3b26..37093277 100644
--- a/src/sat/glucose2/SimpSolver2.cpp
+++ b/src/sat/glucose2/SimpSolver2.cpp
@@ -707,7 +707,7 @@ void SimpSolver::cleanUpClauses()
for (i = j = 0; i < clauses.size(); i++)
if (ca[clauses[i]].mark() == 0)
clauses[j++] = clauses[i];
- clauses.shrink(i - j);
+ clauses.shrink_(i - j);
}
@@ -760,18 +760,22 @@ void SimpSolver::reset()
Solver::reset();
grow = opt_grow;
asymm_lits = eliminated_vars = bwdsub_assigns = n_touched = 0;
- elimclauses.clear(false);
- touched.clear(false);
- occurs.clear(false);
- n_occ.clear(false);
- elim_heap.clear(false);
+
subsumption_queue.clear(false);
- frozen.clear(false);
- eliminated.clear(false);
vec<Lit> dummy(1,lit_Undef);
ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
bwdsub_tmpunit = ca.alloc(dummy);
remove_satisfied = false;
+
+ occurs.clear(false);
+
+ touched .shrink_( touched .size() );
+ n_occ .shrink_( n_occ .size() );
+ eliminated .shrink_( eliminated .size() );
+ frozen .shrink_( frozen .size() );
+ elimclauses .shrink_( elimclauses .size() );
+
+ elim_heap .clear_(false);
}
ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h
index 5394a21d..b1d38d79 100644
--- a/src/sat/glucose2/Solver.h
+++ b/src/sat/glucose2/Solver.h
@@ -71,6 +71,9 @@ 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_set_jftr(int);
+ int sat_solver_jftr();
+ void sat_solver_reset();
// Problem specification:
//
@@ -111,7 +114,7 @@ public:
// Variable mode:
//
void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'.
- void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic.
+ void setDecisionVar (Var v, bool b, bool use_oheap = true); // Declare if a variable should be eligible for selection in the decision heuristic.
// Read state:
//
@@ -365,38 +368,26 @@ protected:
// circuit-based solver
protected:
- struct JustData { unsigned now: 1; double act_fanin; };
- vec<JustData> jdata;
- static inline JustData mkJustData(bool n){ JustData d = {n,0}; return d; }
+ void uncheckedEnqueue2(Lit p, CRef from = CRef_Undef);
+ bool heap_rescale;
- struct JustOrderLt {
- const Solver * pS;
- bool operator () (Var x, Var y) const {
- if( pS->justActivity(x) != pS->justActivity(y) )
- return pS->justActivity(x) > pS->justActivity(y);
- if( pS->level(x) != pS->level(y) )
- return pS->level(x) < pS->level(y);
- return x > y;
- }
- JustOrderLt(const Solver * _pS) : pS(_pS) { }
- };
+ void addJwatch( Var host, Var member, int index );
+ //void delJwatch( Var member );
- struct JustWatch { struct { unsigned dir:1; } header; Var head; Var next; Var prev; };
- vec<JustWatch> jwatch;
- static inline JustWatch mkJustWatch(){ JustWatch w = {0, var_Undef, var_Undef, var_Undef}; return w; }
- void addJwatch( Var host, Var member );
- void delJwatch( Var member );
-
- vec<Lit> var2FaninLits; // (~0): undefine
+ struct NodeData { Lit lit0; Lit lit1; unsigned sort:30; unsigned dir:1; unsigned now:1; };
+ static inline NodeData mkNodeData(){ NodeData w; w.lit0 = toLit(~0); w.lit1 = toLit(~0); w.sort = 0; w.dir = 0; w.now = 0; return w; }
+ vec<NodeData> var2NodeData;
+ //vec<Lit> var2FaninLits; // (~0): undefine
vec<unsigned> var2TravId;
- vec<Lit> var2Fanout0, var2FanoutN, var2FanoutP;
+ vec<Lit> var2Fanout0, var2FanoutN;//, var2FanoutP;
CRef itpc; // the interpreted clause of a gate
+ void inplace_sort( Var v );
bool isTwoFanin ( Var v ) const ; // this var has two fanins
bool isAND ( Var v ) const { return getFaninVar0(v) < getFaninVar1(v); }
bool isJReason ( Var v ) const { return isTwoFanin(v) && ( l_False == value(v) || (!isAND(v) && l_Undef != value(v)) ); }
- Lit getFaninLit0( Var v ) const { return var2FaninLits[ (v<<1) + 0 ]; }
- Lit getFaninLit1( Var v ) const { return var2FaninLits[ (v<<1) + 1 ]; }
+ Lit getFaninLit0( Var v ) const { return var2NodeData[ v ].lit0; }
+ Lit getFaninLit1( Var v ) const { return var2NodeData[ v ].lit1; }
bool getFaninC0 ( Var v ) const { return sign(getFaninLit0(v)); }
bool getFaninC1 ( Var v ) const { return sign(getFaninLit1(v)); }
Var getFaninVar0( Var v ) const { return var(getFaninLit0(v)); }
@@ -406,7 +397,7 @@ protected:
Lit maxActiveLit(Lit lit0, Lit lit1) const { return activity[var(lit0)] < activity[var(lit1)]? lit1: lit0; }
Lit gateJustFanin(Var v) const ; // l_Undef=satisfied, 0/1 = fanin0/fanin1 requires justify
- void gateAddJwatch(Var v);
+ void gateAddJwatch(Var v,int index);
CRef gatePropagateCheck( Var v, Var t );
CRef gatePropagateCheckThis( Var v );
CRef gatePropagateCheckFanout( Var v, Lit lfo );
@@ -415,9 +406,9 @@ protected:
// directly call by original glucose functions
void updateJustActivity( Var v );
void ResetJustData(bool fCleanMemory);
- Lit pickJustLit( Var& j_reason );
+ Lit pickJustLit( int& index );
void justCheck();
- void pushJustQueue(Var v);
+ void pushJustQueue(Var v, int index);
void restoreJustQueue(int level); // call with cancelUntil
void gateClearJwatch( Var v, int backtrack_level );
@@ -431,31 +422,58 @@ protected:
Var CRef2Var( CRef cr ) const { return cr & ~(1<<(sizeof(CRef)*8-1)); }
bool isGateCRef( CRef cr ) const { return CRef_Undef != cr && 0 != (cr & (1<<(sizeof(CRef)*8-1))); }
- int64_t travId_prev, travId;
-
- Heap<JustOrderLt> jheap;
- /* jstack
- call by unchecked_enqueue
- consumed by pickJustLit
- cleaned by cancelUntil
- */
- vec<Var> jstack;
+ unsigned travId_prev, travId;
+
+ //Heap<JustOrderLt> jheap;
+ int jhead;
+
+ struct JustKey {
+ typedef double Key;
+ typedef Var Data;
+ typedef int Attr;
+ Key _key;
+ Data _data;
+ Attr _attr;
+ Data data() const { return _data; }
+ Key key() const { return _key; }
+ Attr attr() const { return _attr; }
+ JustKey():_key(0),_data(0),_attr(0){}
+ JustKey( const Key& nkey, const Data& ndata, const Attr& nattr ): _key(nkey), _data(ndata), _attr(nattr) {}
+ };
+ struct JustOrderLt2 {
+ const Solver * pS;
+ bool operator () (const JustKey& x, const JustKey& y) const {
+ if( x.key() != y.key() ) return x.key() > y.key();
+ if( pS->level( x.data() ) != pS->level( y.data() ) )
+ return pS->level( x.data() ) < pS->level( y.data() );
+ return x.data() > y.data();
+ }
+ JustOrderLt2(const Solver * _pS) : pS(_pS) { }
+ };
+ Heap2<JustOrderLt2, JustKey> jheap;
+ vec<int> jlevel;
+ vec<int> jnext;
public:
+ void prelocate( int var_num );
void setVarFaninLits( Var v, Lit lit1, Lit lit2 );
+ void setVarFaninLits( int v, int lit1, int lit2 ){ setVarFaninLits( Var(v), toLit(lit1), toLit(lit2) ); }
//void delVarFaninLits( Var v);
- int setNewRound(){ return travId ++ ; }
+ void setNewRound(){ travId ++ ; }
void markCone( Var v );
+ void setJust( int njftr ){ jftr = njftr; }
bool isRoundWatch( Var v ) const { return travId==var2TravId[v]; }
+ void justReset(){ jftr = 0; reset(); }
- const JustData& getJustData(int v) const { return jdata[v]; }
+ //const JustData& getJustData(int v) const { return jdata[v]; }
double varActivity(int v) const { return activity[v];}
- double justActivity(int v) const { return jdata[v].act_fanin;}
+ //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
int justUsage() const ;
+ int solveLimited( int * , int nlits );
};
@@ -466,32 +484,26 @@ inline CRef Solver::reason(Var x) const { return vardata[x].reason; }
inline int Solver::level (Var x) const { return vardata[x].level; }
inline void Solver::insertVarOrder(Var x) {
- if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
+ #ifdef CGLUCOSE_EXP
+ if (!justUsage() && !order_heap.inHeap(x) && decision[x]) order_heap.insert(x);
+ #else
+ if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x);
+ #endif
+}
inline void Solver::varDecayActivity() { var_inc *= (1 / var_decay); }
inline void Solver::varBumpActivity(Var v) { varBumpActivity(v, var_inc); }
inline void Solver::varBumpActivity(Var v, double inc) {
if ( (activity[v] += inc) > 1e100 ) {
+ heap_rescale = 1;
// Rescale:
for (int i = 0; i < nVars(); i++)
activity[i] *= 1e-100;
-
- if( justUsage() )
- for (int i = 0; i < jheap.size(); i++){
- Var j = jheap[i];
- jdata[j].act_fanin = activity[getFaninVar0(j)] > activity[getFaninVar1(j)]? activity[getFaninVar0(j)]: activity[getFaninVar1(j)];
- }
var_inc *= 1e-100; }
// Update order_heap with respect to new activity:
- if (order_heap.inHeap(v))
+ if (!justUsage() && order_heap.inHeap(v))
order_heap.decrease(v);
-
- #ifdef CGLUCOSE_EXP
- if( justUsage() )
- updateJustActivity(v);
-
- #endif
}
inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
@@ -550,13 +562,13 @@ 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 (int*) &JustModel[0]; }
inline void Solver::setPolarity (Var v, bool b) { polarity[v] = b; }
-inline void Solver::setDecisionVar(Var v, bool b)
+inline void Solver::setDecisionVar(Var v, bool b, bool use_oheap)
{
if ( b && !decision[v]) dec_vars++;
else if (!b && decision[v]) dec_vars--;
decision[v] = b;
- insertVarOrder(v);
+ if( use_oheap ) insertVarOrder(v);
}
inline void Solver::setConfBudget(int64_t x){ conflict_budget = conflicts + x; }
inline void Solver::setPropBudget(int64_t x){ propagation_budget = propagations + x; }
@@ -589,7 +601,16 @@ 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_set_jftr( int njftr ){ setJust(njftr); }
+inline int Solver::sat_solver_jftr(){ return jftr; }
+inline void Solver::sat_solver_reset(){ justReset(); }
+inline int Solver::solveLimited( int * lit0, int nlits ){
+ assumptions.clear();
+ for(int i = 0; i < nlits; i ++)
+ assumptions.push(toLit(lit0[i]));
+ lbool res = solve_();
+ return res == l_True ? 1 : (res == l_False ? -1 : 0);
+}
//=================================================================================================
// Debug etc:
diff --git a/src/sat/glucose2/SolverTypes.h b/src/sat/glucose2/SolverTypes.h
index ea0f76d0..6c57a900 100644
--- a/src/sat/glucose2/SolverTypes.h
+++ b/src/sat/glucose2/SolverTypes.h
@@ -298,6 +298,7 @@ class OccLists
OccLists(const Deleted& d) : deleted(d) {}
void init (const Idx& idx){ occs.growTo(toInt(idx)+1); dirty.growTo(toInt(idx)+1, 0); }
+ void prelocate (const int num){ occs.prelocate(num); dirty.prelocate(num); }
// Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
Vec& operator[](const Idx& idx){ return occs[toInt(idx)]; }
Vec& lookup (const Idx& idx){ if (dirty[toInt(idx)]) clean(idx); return occs[toInt(idx)]; }
@@ -332,7 +333,7 @@ void OccLists<Idx,Vec,Deleted>::cleanAll()
// Dirties may contain duplicates so check here if a variable is already cleaned:
if (dirty[toInt(dirties[i])])
clean(dirties[i]);
- dirties.clear();
+ dirties.shrink_( dirties.size() );
}
@@ -344,7 +345,7 @@ void OccLists<Idx,Vec,Deleted>::clean(const Idx& idx)
for (i = j = 0; i < vec.size(); i++)
if (!deleted(vec[i]))
vec[j++] = vec[i];
- vec.shrink(i - j);
+ vec.shrink_(i - j);
dirty[toInt(idx)] = 0;
}
diff --git a/src/sat/glucose2/Vec.h b/src/sat/glucose2/Vec.h
index 711cb694..eaeed207 100644
--- a/src/sat/glucose2/Vec.h
+++ b/src/sat/glucose2/Vec.h
@@ -67,7 +67,9 @@ public:
void shrink_ (int nelems) { assert(nelems <= sz); sz -= nelems; }
int capacity (void) const { return cap; }
void capacity (int min_cap);
+ void prelocate(int ext_cap);
void growTo (int size);
+ void growTo_ (int size);
void growTo (int size, const T& pad);
void clear (bool dealloc = false);
@@ -90,7 +92,7 @@ public:
// Duplicatation (preferred instead):
void copyTo (vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
- void copyTo_(vec<T>& copy) const { copy.shrink_(copy.size()); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
+ void copyTo_(vec<T>& copy) const { copy.shrink_(copy.size()); copy.growTo_(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
};
@@ -103,6 +105,14 @@ void vec<T>::capacity(int min_cap) {
throw OutOfMemoryException();
}
+template<class T>
+void vec<T>::prelocate(int ext_cap) {
+ if (cap >= ext_cap) return;
+ if (ext_cap > INT_MAX || (((data = (T*)::realloc(data, ext_cap * sizeof(T))) == NULL) && errno == ENOMEM))
+ throw OutOfMemoryException();
+ cap = ext_cap;
+ }
+
template<class T>
void vec<T>::growTo(int size, const T& pad) {
@@ -121,6 +131,13 @@ void vec<T>::growTo(int size) {
template<class T>
+void vec<T>::growTo_(int size) {
+ if (sz >= size) return;
+ capacity(size);
+ sz = size; }
+
+
+template<class T>
void vec<T>::clear(bool dealloc) {
if (data != NULL){
for (int i = 0; i < sz; i++) data[i].~T();
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-22 23:27:01 +0000