Upgrade to the circuit-based solver.

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();