Upgrading the SAT solvers.

8 files changed, 1049 insertions, 67 deletions

diff --git a/src/sat/glucose2/CGlucose.h b/src/sat/glucose2/CGlucose.h
new file mode 100644
index 00000000..32da4248
--- /dev/null
+++ b/src/sat/glucose2/CGlucose.h
@@ -0,0 +1,6 @@
+#ifndef Glucose_CGlucose_h
+#define Glucose_CGlucose_h
+
+#define CGLUCOSE_EXP 1
+
+#endif
\ No newline at end of file
diff --git a/src/sat/glucose2/CGlucoseCore.h b/src/sat/glucose2/CGlucoseCore.h
new file mode 100644
index 00000000..3400b114
--- /dev/null
+++ b/src/sat/glucose2/CGlucoseCore.h
@@ -0,0 +1,651 @@
+// The code in this file was developed by He-Teng Zhang (National Taiwan University)
+
+#ifndef Glucose_CGlucoseCore_h
+#define Glucose_CGlucoseCore_h
+
+/*
+ * justification for glucose 
+ */
+
+#include "sat/glucose2/Options.h"
+#include "sat/glucose2/Solver.h"
+
+ABC_NAMESPACE_IMPL_START
+
+namespace Gluco2 {
+
+inline int  Solver::justUsage() const {
+	return jftr;
+}
+
+inline Lit Solver::maxActiveLit(Lit lit0, Lit lit1) const {
+	return activity[var(lit0)] < activity[var(lit1)]? lit1: lit0;
+}
+
+//Lit  Solver::faninNJustLit(Var v, int idx) const {
+//	assert(isTwoFanin(v));
+//	assert(value(v) == l_False); // l_True should be handled by propagation
+//	return ~ (0 == idx? getFaninLit0(v): );
+//}
+
+// select one of fanins to justify
+inline Lit  Solver::fanin2JustLit(Var v) const {
+	assert(v < nVars());
+	Lit lit0, lit1;
+	lit0 = ~getFaninLit0(v);
+	lit1 = ~getFaninLit1(v);
+//	if( (sign(lit0) != polarity[var(lit0)]) ^ (sign(lit1) != polarity[var(lit1)]) )
+//		return sign(lit0) == polarity[var(lit0)]? lit0: lit1;
+	return maxActiveLit(lit0, lit1);
+}
+
+inline Lit  Solver::gateJustFanin(Var v) const {
+	assert(v < nVars());
+	assert(isTwoFanin(v));
+	assert(value(v) == l_False); // l_True should be handled by propagation
+
+	lbool val0, val1;
+	val0 = value(getFaninVar0(v));
+	val1 = value(getFaninVar1(v));
+
+	// phased values
+	if(l_Undef != val0) val0 = val0 ^ getFaninC0(v);
+	if(l_Undef != val1) val1 = val1 ^ getFaninC1(v);
+
+	// should be handled by conflict analysis before entering here
+	assert(value(v) != l_False || l_True  != val0 || l_True  != val1);
+
+	if(val0 == l_False || val1 == l_False)
+		return lit_Undef;
+
+	// branch 
+	if(val0 == l_True)
+		return ~getFaninLit1(v);
+	if(val1 == l_True)
+		return ~getFaninLit0(v);
+
+	// both fanins are eligible
+	//return maxActiveLit(faninNJustLit(v, 0), faninNJustLit(v, 1));
+	return fanin2JustLit(v);
+}
+
+
+// a var should at most be enqueued one time
+inline void Solver::pushJustQueue(Var v){
+	assert(v < nVars());
+	assert(value(v) == l_False); // l_True should be handled by propagation
+	assert(isTwoFanin(v));
+
+	if( ! isRoundWatch(v) )\
+		return;
+
+
+	jdata[v].act_fanin = activity[getFaninVar0(v)] > activity[getFaninVar1(v)]? activity[getFaninVar0(v)]: activity[getFaninVar1(v)];
+	jdata[v].now = true;
+
+	jheap.update(v);
+}
+
+inline void Solver::ResetJustData(bool fCleanMemory){
+	jstack.shrink_( jstack.size() );
+	jheap .clear(fCleanMemory);
+}
+
+inline Lit Solver::pickJustLit( Var& j_reason ){
+	Var next = var_Undef;
+	Lit jlit = lit_Undef;
+	//double clk = Abc_Clock();
+	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);
+	}
+	jstack.shrink_( jstack.size() );
+	while( ! jheap.empty() && var_Undef != (next = jheap.removeMin()) ){
+		if( ! jdata[next].now )
+			continue; 
+
+		assert( l_False == value(next) );
+		if( lit_Undef != (jlit = gateJustFanin(next)) )
+			break;
+		gateAddJwatch(next);
+	}
+
+
+	j_reason = next;
+	return jlit;
+}
+
+
+inline void Solver::gateAddJwatch(Var v){
+	assert(v < nVars());
+	assert(isTwoFanin(v));
+	assert(value(v) == l_False); // l_True should be handled by propagation
+
+	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);
+	var1 = getFaninVar1(v);
+	val0 = value(var0);
+	val1 = value(var1);
+
+	// phased values
+	if(l_Undef != val0) val0 = val0 ^ getFaninC0(v);
+	if(l_Undef != val1) val1 = val1 ^ getFaninC1(v);
+
+	assert( l_False == val0 || l_False == val1 );
+
+	if(val0 == l_False && val1 == l_False){
+		addJwatch(vardata[var0].level < vardata[var1].level? var0: var1, v);
+		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 );
+
+		if( vardata[member].level <= backtrack_level )
+			pushJustQueue(member);
+
+		member = next;
+	}
+}
+
+inline void Solver::updateJustActivity( Var v ){
+	for(Lit lfo = var2Fanout0[ v ]; lfo != toLit(~0); lfo = var2FanoutN[ toInt(lfo) ] ){
+		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);
+		}
+	}
+}
+
+
+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;
+}
+
+
+/*
+ * circuit propagation 
+ */
+
+inline void Solver::justCheck(){
+	Lit lit;
+	//for(int i=0; i<JustQueue.size(); i++)
+	//	if(lit_Undef!= (lit = gateJustFanin(JustQueue[i])))
+	//		printf("%d is not justified\n", JustQueue[i]);
+	int i, nJustFail = 0;
+	for(i=0; i<trail.size(); i++){
+		Var      x  = var(trail[i]);
+		if( ! isTwoFanin(x) )
+			continue;
+		if( ! isRoundWatch(x) )
+			continue;
+		if( l_False != value(x) )
+			continue;
+		if( lit_Undef != (lit = gateJustFanin(x)) ){
+			printf("\t%8d is not justified (value=%d, level=%3d)\n", x, l_True == value(x)? 1: 0, vardata[x].level), nJustFail ++ ;
+
+			assert(false);
+		}
+	}
+	if( nJustFail )
+		printf("%d just-fails\n", nJustFail);
+	
+	JustModel.clear(false);
+	JustModel.growTo(nVars(), lit_Undef);
+
+	for (i = 0; i < nVars(); i++){
+		if( l_Undef  == value(i) )
+			continue;
+		JustModel[i] = mkLit( i, l_False == value(i) );
+	}
+}
+/**
+inline void Solver::delVarFaninLits( Var v ){
+	if( toLit(~0) != getFaninLit0(v) ){
+		if( toLit(~0) == var2FanoutP[ (v<<1) + 0 ] ){
+			// head of linked-list 
+			Lit root = mkLit(getFaninVar0(v));
+			Lit next = var2FanoutN[ (v<<1) + 0 ];
+			if( toLit(~0) != next ){
+				assert( var2Fanout0[ toInt(root) ] == toLit((v<<1) + 0) );
+				assert( var2FanoutP[ toInt(next) ] == toLit((v<<1) + 0) );
+				var2Fanout0[ getFaninVar0(v) ] = next;
+				var2FanoutP[ toInt(next) ] = toLit(~0);
+			}
+		} else {
+			Lit prev = var2FanoutP[ (v<<1) + 0 ];
+			Lit next = var2FanoutN[ (v<<1) + 0 ];
+			if( toLit(~0) != next ){
+				assert( var2FanoutN[ toInt(prev) ] == toLit((v<<1) + 0) );
+				assert( var2FanoutP[ toInt(next) ] == toLit((v<<1) + 0) );
+				var2FanoutN[ toInt(prev) ] = next;
+				var2FanoutP[ toInt(next) ] = prev;
+			}
+		}
+	}
+
+
+	if( toLit(~0) != getFaninLit1(v) ){
+		if( toLit(~0) == var2FanoutP[ (v<<1) + 1 ] ){
+			// head of linked-list 
+			Lit root = mkLit(getFaninVar1(v));
+			Lit next = var2FanoutN[ (v<<1) + 1 ];
+			if( toLit(~0) != next ){
+				assert( var2Fanout0[ toInt(root) ] == toLit((v<<1) + 1) );
+				assert( var2FanoutP[ toInt(next) ] == toLit((v<<1) + 1) );
+				var2Fanout0[ getFaninVar1(v) ] = next;
+				var2FanoutP[ toInt(next) ] = toLit(~0);
+			}
+		} else {
+			Lit prev = var2FanoutP[ (v<<1) + 1 ];
+			Lit next = var2FanoutN[ (v<<1) + 1 ];
+			if( toLit(~0) != next ){
+				assert( var2FanoutN[ toInt(prev) ] == toLit((v<<1) + 1) );
+				assert( var2FanoutP[ toInt(next) ] == toLit((v<<1) + 1) );
+				var2FanoutN[ toInt(prev) ] = next;
+				var2FanoutP[ toInt(next) ] = prev;
+			}
+		}
+	}
+
+	var2FanoutP  [ (v<<1) + 0 ] = toLit(~0);
+	var2FanoutP  [ (v<<1) + 1 ] = toLit(~0);
+	var2FanoutN  [ (v<<1) + 0 ] = toLit(~0);
+	var2FanoutN  [ (v<<1) + 1 ] = toLit(~0);
+	var2FaninLits[ (v<<1) + 0 ] = toLit(~0);
+	var2FaninLits[ (v<<1) + 1 ] = toLit(~0);
+}
+**/
+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;
+
+
+	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 );
+	var2Fanout0[ var(lit2) ] = toLit( (v<<1) + 1 );
+
+	//if( toLit(~0) != var2FanoutN[ (v<<1) + 0 ] )
+	//	var2FanoutP[ toInt(var2FanoutN[ (v<<1) + 0 ]) ] = toLit((v<<1) + 0);
+
+	//if( toLit(~0) != var2FanoutN[ (v<<1) + 1 ] )
+	//	var2FanoutP[ toInt(var2FanoutN[ (v<<1) + 1 ]) ] = toLit((v<<1) + 1);
+}
+
+
+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 ];
+	assert( toLit(~0) == lit0 || var(lit0) < nVars() );
+	assert( toLit(~0) == lit1 || var(lit1) < nVars() );
+	return toLit(~0) != var2FaninLits[ (v<<1) + 0 ] && toLit(~0) != var2FaninLits[ (v<<1) + 1 ];
+}
+
+// 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) )
+		return CRef_Undef;
+
+	if( ! isRoundWatch(var(p)) )
+		return CRef_Undef;
+
+	if( ! isTwoFanin( var(p) ) )
+		goto check_fanout;
+
+
+	// check fanin consistency 
+	if( CRef_Undef != (stats = gatePropagateCheckThis( var(p) )) ){
+		confl = stats;
+		if( l_True == value(var(p)) )
+			return confl;
+	}
+
+	// check fanout consistency
+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( CRef_Undef != (stats = gatePropagateCheckFanout( var(p), lfo )) ){
+			confl = stats;
+			if( l_True == value(var(lfo)) )
+				return confl;
+		}
+	}
+
+	return confl;
+}
+
+inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
+	Lit faninLit = sign(lfo)? getFaninLit1(var(lfo)): getFaninLit0(var(lfo));
+	assert( var(faninLit) == v );
+
+	if( l_False == value(faninLit) )
+	{
+		if( l_False == value(var(lfo)) )
+			return CRef_Undef;
+
+		if( l_True == value(var(lfo)) )
+			return Var2CRef(var(lfo));
+		
+		jwatch[var(lfo)].header.dir = sign(lfo);
+		uncheckedEnqueue(~mkLit(var(lfo)), Var2CRef( var(lfo) ) );
+	} else {
+		assert( l_True == value(faninLit) );
+
+		if( l_True == value(var(lfo)) )
+			return CRef_Undef;
+		
+		// check value of the other fanin 
+		Lit faninLitP = sign(lfo)? getFaninLit0(var(lfo)): getFaninLit1(var(lfo));
+		if( l_False == value(var(lfo)) ){
+			
+			if( l_False == value(faninLitP) )
+				return CRef_Undef;
+
+			if( l_True == value(faninLitP) )
+				return Var2CRef(var(lfo));
+
+			uncheckedEnqueue( ~faninLitP, Var2CRef( var(lfo) ) );
+		}
+		else
+		if( l_True == value(faninLitP) )
+			uncheckedEnqueue( mkLit(var(lfo)), Var2CRef( var(lfo) ) );
+	}
+	return CRef_Undef;
+}
+
+inline CRef Solver::gatePropagateCheckThis( Var v ){
+	CRef confl = CRef_Undef;
+	if( l_False == value(v) ){
+		if( l_True == value(getFaninLit0(v)) && l_True == value(getFaninLit1(v)) )
+			return Var2CRef(v);
+
+		if( l_False == value(getFaninLit0(v)) || l_False == value(getFaninLit1(v)) )
+			return CRef_Undef;
+
+		if( l_True == value(getFaninLit0(v)) )
+			uncheckedEnqueue(~getFaninLit1( v ), Var2CRef( v ) );
+		if( l_True == value(getFaninLit1(v)) )
+			uncheckedEnqueue(~getFaninLit0( v ), Var2CRef( v ) );
+	} else {
+		assert( l_True == value(v) );
+		if( l_False == value(getFaninLit0(v)) || l_False == value(getFaninLit1(v)) )
+			confl = Var2CRef(v);
+
+		if( l_Undef == value( getFaninLit0( v )) )
+			uncheckedEnqueue( getFaninLit0( v ), Var2CRef( v ) );
+
+		if( l_Undef == value( getFaninLit1( v )) )
+			uncheckedEnqueue( getFaninLit1( v ), Var2CRef( v ) );
+
+	}
+
+	return confl;
+}
+
+inline CRef Solver::getConfClause( CRef r ){
+	if( !isGateCRef(r) )
+		return r;
+	Var v = CRef2Var(r);
+	assert( isTwoFanin(v) );
+
+	if( l_False == value(v) ){
+		setItpcSize(3);
+		Clause& c = ca[itpc];
+		c[0] = mkLit(v);
+		c[1] = ~getFaninLit0( v );
+		c[2] = ~getFaninLit1( v );
+	} else {
+		setItpcSize(2);
+		Clause& c = ca[itpc];
+		c[0] = ~mkLit(v);
+
+		lbool val0 = value(getFaninLit0(v));
+		lbool val1 = value(getFaninLit1(v));
+
+		if( l_False == val0 && l_False == val1 )
+			c[1] = level(getFaninVar0(v)) < level(getFaninVar1(v))? getFaninLit0( v ): getFaninLit1( v );
+		else
+		if( l_False == val0 )
+			c[1] = getFaninLit0( v );
+		else
+			c[1] = getFaninLit1( v );
+	}
+
+	return itpc;
+}
+
+inline CRef Solver::gatePropagateCheck( Var v, Var t )
+{  // check fanin consistency 
+	assert( isTwoFanin(v) );
+	CRef confl = CRef_Undef;
+	lbool val0, val1, valo;
+	Var var0, var1;
+	var0 = getFaninVar0( v );
+	var1 = getFaninVar1( v );
+	val0 = value( var0 );
+	val1 = value( var1 );
+	valo = value( v );
+
+	// phased values
+	if(l_Undef != val0) val0 = val0 ^ getFaninC0( v );
+	if(l_Undef != val1) val1 = val1 ^ getFaninC1( v );
+
+
+	if( l_True == valo ){
+
+
+		if( l_False == val0 || l_False == val1 )
+		{ // conflict 
+			return Var2CRef(v);
+		}
+
+		// propagate 1
+		if( l_Undef == val0 )
+			uncheckedEnqueue( getFaninLit0( v ), Var2CRef( v ) );
+		if( l_Undef == val1 )
+			uncheckedEnqueue( getFaninLit1( v ), Var2CRef( v ) );
+
+	} else 
+	if( l_False == valo ){
+
+		if( l_True == val0 && l_True == val1 )
+		{  // conflict 
+			confl = Var2CRef(v);
+		}
+
+		// propagate 0
+		if( l_True == val0 && l_Undef == val1 )
+			uncheckedEnqueue( ~getFaninLit1( v ), Var2CRef( v ) );
+		else
+		if( l_True == val1 && l_Undef == val0 )
+			uncheckedEnqueue( ~getFaninLit0( v ), Var2CRef( v ) );
+
+	} else
+	if( l_Undef == valo ){
+
+		if( l_True == val0 && l_True == val1 ){
+			jwatch[v].header.dir =  t == var1;
+			uncheckedEnqueue(  mkLit(v), Var2CRef( v ) );
+		} else
+		if( t == var0 && l_False == val0 ){
+			jwatch[v].header.dir = 0;
+			uncheckedEnqueue( ~mkLit(v), Var2CRef( v ) );
+		} else
+		if( t == var1 && l_False == val1 ){
+			jwatch[v].header.dir = 1;
+			uncheckedEnqueue( ~mkLit(v), Var2CRef( v ) );
+		}
+
+	}
+
+	return confl;
+}
+
+inline void Solver::setItpcSize( int sz ){
+	assert( 3 >= sz );
+	assert( CRef_Undef != itpc );
+	ca[itpc].header.size = sz;
+}
+
+inline CRef Solver::interpret( Var v, Var t )
+{ // get gate-clause on implication graph
+	assert( isTwoFanin(v) );
+
+	lbool val0, val1, valo;
+	Var var0, var1;
+	var0 = getFaninVar0( v );
+	var1 = getFaninVar1( v );
+	val0 = value(var0);
+	val1 = value(var1);
+	valo = value( v );
+
+	// phased values
+	if(l_Undef != val0) val0 = val0 ^ getFaninC0( v );
+	if(l_Undef != val1) val1 = val1 ^ getFaninC1( v );
+
+
+	if( v == t ){
+		// tracing output 
+		if( l_False == valo ){
+			setItpcSize(2);
+			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 );
+		} else {
+			setItpcSize(3);
+			Clause& c = ca[itpc];
+			c[0] = mkLit(v);
+			c[1] = ~getFaninLit0( v );
+			c[2] = ~getFaninLit1( v );
+		}
+	} else {
+		assert( t == var0 || t == var1 );
+		if( l_False == valo ){
+			setItpcSize(3);
+			Clause& c = ca[itpc];
+			c[0] = ~getFaninLit0( v );
+			c[1] = ~getFaninLit1( v );
+			c[2] = mkLit(v);
+			if( t == var1 )
+				//std::swap(c[0],c[1]);
+                c[1].x ^= c[0].x, c[0].x ^= c[1].x, c[1].x ^= c[0].x;
+		} else {
+			setItpcSize(2);
+			Clause& c = ca[itpc];
+			c[0] =  t == var0? getFaninLit0( v ): getFaninLit1( v );
+			c[1] = ~mkLit(v);
+		}
+	}
+
+	return itpc;
+}
+
+inline CRef Solver::castCRef( Lit p ){
+	CRef cr = reason( var(p) );
+	if( CRef_Undef == cr )
+		return cr;
+	if( ! isGateCRef(cr) )
+		return cr;
+	Var v = CRef2Var(cr);
+	return interpret(v,var(p));
+}
+
+inline void Solver::markCone( Var v ){
+	if( var2TravId[v] >= travId )
+		return;
+	var2TravId[v] = travId;
+
+	if( !isTwoFanin(v) )
+		return;
+	markCone( getFaninVar0(v) );
+	markCone( getFaninVar1(v) );
+}
+
+
+
+};
+
+
+ABC_NAMESPACE_IMPL_END
+
+
+#endif
\ No newline at end of file
diff --git a/src/sat/glucose2/Glucose2.cpp b/src/sat/glucose2/Glucose2.cpp
index 6f24c828..f32d1210 100644
--- a/src/sat/glucose2/Glucose2.cpp
+++ b/src/sat/glucose2/Glucose2.cpp
@@ -26,13 +26,14 @@ NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FO
 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.
 **************************************************************************************************/
-
 #include <math.h>
 
 #include "sat/glucose2/Sort.h"
-#include "sat/glucose2/Solver.h"
 #include "sat/glucose2/Constants.h"
 #include "sat/glucose2/System.h"
+#include "sat/glucose2/Solver.h"
+
+#include "sat/glucose2/CGlucose.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -40,7 +41,7 @@ using namespace Gluco2;
 
 //=================================================================================================
 // Options:
-
+namespace Gluco2 {
 static const char* _cat = "CORE";
 static const char* _cr = "CORE -- RESTART";
 static const char* _cred = "CORE -- REDUCE";
@@ -79,9 +80,9 @@ static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interv
 static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction of wasted memory allowed before a garbage collection is triggered",           0.20, DoubleRange(0, false, HUGE_VAL, false));
 
 
-BoolOption    opt2_certified_      (_certified, "certified",         "Certified UNSAT using DRUP format", false );
-StringOption  opt2_certified_file_ (_certified, "certified-output",  "Certified UNSAT output file",       "NULL");
-
+BoolOption    opt_certified_      (_certified, "certified",         "Certified UNSAT using DRUP format", false );
+StringOption  opt_certified_file_ (_certified, "certified-output",  "Certified UNSAT output file",       "NULL");
+};
 
 //=================================================================================================
 // Constructor/Destructor:
@@ -121,7 +122,7 @@ Solver::Solver() :
   , rnd_init_act     (opt_rnd_init_act)
   , garbage_frac     (opt_garbage_frac)
   , certifiedOutput  (NULL)
-  , certifiedUNSAT   (opt2_certified_) 
+  , certifiedUNSAT   (opt_certified_) 
     // Statistics: (formerly in 'SolverStats')
     //
   ,  nbRemovedClauses(0),nbReducedClauses(0), nbDL2(0),nbBin(0),nbUn(0) , nbReduceDB(0)
@@ -148,8 +149,13 @@ Solver::Solver() :
   , asynch_interrupt   (false)
   , incremental(opt_incremental)
   , nbVarsInitialFormula(INT32_MAX)
+
+  #ifdef CGLUCOSE_EXP
+  , jheap         (JustOrderLt(this))
+  #endif
 {
   MYFLAG=0;  
+
   // Initialize only first time. Useful for incremental solving, useless otherwise
   lbdQueue.initSize(sizeLBDQueue);
   trailQueue.initSize(sizeTrailQueue);
@@ -160,13 +166,24 @@ Solver::Solver() :
 
 
   if(certifiedUNSAT) {
-    if(!strcmp(opt2_certified_file_,"NULL")) {
+    if(!strcmp(opt_certified_file_,"NULL")) {
       certifiedOutput =  fopen("/dev/stdout", "wb");
     } else {
-      certifiedOutput =  fopen(opt2_certified_file_, "wb");           
+      certifiedOutput =  fopen(opt_certified_file_, "wb");           
     }
     //    fprintf(certifiedOutput,"o proof DRUP\n");
   }
+
+  #ifdef CGLUCOSE_EXP
+  travId = 0;
+  travId_prev = 0;
+
+  // allocate space for clause interpretation 
+  vec<Lit> tmp; tmp.growTo(3); 
+  itpc = ca.alloc(tmp);
+  ca[itpc].shrink( ca[itpc].size() );
+
+  #endif
 }
 
 
@@ -216,6 +233,19 @@ Var Solver::newVar(bool sign, bool dvar)
     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);
+    }
+    #endif
+
     return v;
 }
 
@@ -460,7 +490,7 @@ void Solver::minimisationWithBinaryResolution(vec<Lit> &out_learnt) {
         }
       }
       
-      out_learnt.shrink(nb);
+      out_learnt.shrink_(nb);
       
     }
   }
@@ -470,6 +500,7 @@ 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;
@@ -477,9 +508,25 @@ void Solver::cancelUntil(int level) {
                 polarity[x] = sign(trail[c]);
             insertVarOrder(x); }
         qhead = trail_lim[level];
-        trail.shrink(trail.size() - trail_lim[level]);
-        trail_lim.shrink(trail_lim.size() - 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);
+
+              jdata[x].now = false;
+          }
+        }
+        #endif
+
+        trail.shrink_(trail.size() - trail_lim[level]);
+        trail_lim.shrink_(trail_lim.size() - level);
+        jstack.shrink_( jstack.size() );
+    }
 }
 
 
@@ -528,6 +575,8 @@ 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();
+
     int pathC = 0;
     Lit p     = lit_Undef;
 
@@ -535,10 +584,15 @@ 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;
-
+    
     do{
         assert(confl != CRef_Undef); // (otherwise should be UIP)
+
+      #ifdef CGLUCOSE_EXP
+        Clause& c = ca[ lit_Undef != p ? castCRef(p): getConfClause(confl) ];
+      #else
         Clause& c = ca[confl];
+      #endif
 
         // Special case for binary clauses
         // The first one has to be SAT
@@ -554,7 +608,7 @@ 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) { 
+        if(c.learnt()  && c.lbd()>2) {
           unsigned int nblevels = computeLBD(c);
           if(nblevels+1<c.lbd() ) { // improve the LBD
             if(c.lbd()<=lbLBDFrozenClause) {
@@ -578,8 +632,14 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
                 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 {
@@ -609,7 +669,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
     for(i = 0;i<selectors.size();i++)  
       out_learnt.push(selectors[i]);       
 
-    out_learnt.copyTo(analyze_toclear);
+    out_learnt.copyTo_(analyze_toclear);
     if (ccmin_mode == 2){
         uint32_t abstract_level = 0;
         for (i = 1; i < out_learnt.size(); i++)
@@ -626,7 +686,11 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
             if (reason(x) == CRef_Undef)
                 out_learnt[j++] = out_learnt[i];
             else{
+                #ifdef CGLUCOSE_EXP
+                Clause& c = ca[castCRef(out_learnt[i])];
+                #else
                 Clause& c = ca[reason(var(out_learnt[i]))];
+                #endif
                 // Thanks to Siert Wieringa for this bug fix!
                 for (int k = ((c.size()==2) ? 0:1); k < c.size(); k++)
                     if (!seen[var(c[k])] && level(var(c[k])) > 0){
@@ -638,7 +702,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
         i = j = out_learnt.size();
 
     max_literals += out_learnt.size();
-    out_learnt.shrink(i - j);
+    out_learnt.shrink_(i - j);
     tot_literals += out_learnt.size();
 
 
@@ -687,8 +751,16 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
   // 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]));
+          varBumpActivity(var(lastDecisionLevel[i]));
+      #endif
+
     }
     lastDecisionLevel.clear();
   } 
@@ -698,6 +770,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& o
 
   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;  
+
 }
 
 
@@ -709,7 +782,11 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
     int top = analyze_toclear.size();
     while (analyze_stack.size() > 0){
         assert(reason(var(analyze_stack.last())) != CRef_Undef);
+        #ifdef CGLUCOSE_EXP
+        Clause& c = ca[castCRef(analyze_stack.last())]; analyze_stack.pop();
+        #else
         Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop();
+        #endif
         if(c.size()==2 && value(c[0])==l_False) {
           assert(value(c[1])==l_True);
           Lit tmp = c[0];
@@ -726,7 +803,7 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
                 }else{
                     for (int j = top; j < analyze_toclear.size(); j++)
                         seen[var(analyze_toclear[j])] = 0;
-                    analyze_toclear.shrink(analyze_toclear.size() - top);
+                    analyze_toclear.shrink_(analyze_toclear.size() - top);
                     return false;
                 }
             }
@@ -763,7 +840,11 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
                 assert(level(x) > 0);
                 out_conflict.push(~trail[i]);
             }else{
+              #ifdef CGLUCOSE_EXP
+                Clause& c = ca[castCRef(trail[i])];
+              #else
                 Clause& c = ca[reason(x)];
+              #endif
                 //                for (int j = 1; j < c.size(); j++) Minisat (glucose 2.0) loop 
                 // Bug in case of assumptions due to special data structures for Binary.
                 // Many thanks to Sam Bayless (sbayless@cs.ubc.ca) for discover this bug.
@@ -779,13 +860,20 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
     seen[var(p)] = 0;
 }
 
-
 void Solver::uncheckedEnqueue(Lit p, CRef from)
 {
     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( l_False == value(var(p)) );
+        if(isTwoFanin(var(p)) && l_False == value(var(p)))
+          if(l_Undef == value( getFaninVar0(var(p)) ) && l_Undef == value( getFaninVar1(var(p)) ))
+            jstack.push(var(p));
+        }
+    #endif
 }
 
 
@@ -811,7 +899,19 @@ CRef Solver::propagate()
         vec<Watcher>&  ws  = watches[p];
         Watcher        *i, *j, *end;
         num_props++;
-        
+
+        #ifdef CGLUCOSE_EXP
+        if( 2 <= justUsage() ){
+          CRef stats;
+          if( CRef_Undef != (stats = gatePropagate(p)) ){
+            confl = stats;
+            if( l_True == value(var(p)) )
+              return confl;
+            
+          }
+        }
+        #endif
+
         // First, Propagate binary clauses 
         vec<Watcher>&  wbin  = watchesBin[p];
         for(int k = 0;k<wbin.size();k++) {
@@ -824,6 +924,8 @@ CRef Solver::propagate()
           }
         }
 
+
+
         for (i = j = (Watcher*)ws, end = i + ws.size();  i != end;){
             // Try to avoid inspecting the clause:
             Lit blocker = i->blocker;
@@ -897,11 +999,15 @@ CRef Solver::propagate()
     }
     propagations += num_props;
     simpDB_props -= num_props;
-    
+
     return confl;
 }
 
 
+
+
+
+
 /*_________________________________________________________________________________________________
 |
 |  reduceDB : ()  ->  [void]
@@ -1044,24 +1150,25 @@ lbool Solver::search(int nof_conflicts)
     unsigned int nblevels,szWoutSelectors;
     bool blocked=false;
     starts++;
+
     for (;;){
         CRef confl = propagate();
         if (confl != CRef_Undef){
+
             // CONFLICT
           conflicts++; conflictC++;conflictsRestarts++;
           if(conflicts%5000==0 && var_decay<0.95)
             var_decay += 0.01;
 
           if (verbosity >= 1 && conflicts%verbEveryConflicts==0){
-            printf("c | %8d   %7d    %5d | %7d %8d %8d | %5d %8d   %6d %8d | %6.3f %% |\n", 
+            printf("c | %8d   %7d    %5d | %7d %8d %8d | %5d %8d   %6d %8d | %6.3f %% \n", 
                    (int)starts,(int)nbstopsrestarts, (int)(conflicts/starts), 
                    (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals, 
                    (int)nbReduceDB, nLearnts(), (int)nbDL2,(int)nbRemovedClauses, progressEstimate()*100);
           }
-          if (decisionLevel() == 0) {
+          if (decisionLevel() == 0) 
             return l_False;
-            
-          }
+
 
           trailQueue.push(trail.size());
           // BLOCK RESTART (CP 2012 paper)
@@ -1077,9 +1184,7 @@ lbool Solver::search(int nof_conflicts)
 
             lbdQueue.push(nblevels);
             sumLBD += nblevels;
- 
             cancelUntil(backtrack_level);
-
             if (certifiedUNSAT) {
               for (int i = 0; i < learnt_clause.size(); i++)
                 fprintf(certifiedOutput, "%i " , (var(learnt_clause[i]) + 1) *
@@ -1104,9 +1209,7 @@ lbool Solver::search(int nof_conflicts)
             varDecayActivity();
             claDecayActivity();
 
-           
         }else{
-
           // Our dynamic restart, see the SAT09 competition compagnion paper 
           if ( (conflictsRestarts && lbdQueue.isvalid() && lbdQueue.getavg()*K > sumLBD/conflictsRestarts) || (pstop && *pstop) ) {
             lbdQueue.fastclear();
@@ -1149,13 +1252,26 @@ 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);
+              
+            }
+            #endif
+
             if (next == lit_Undef){
                 // New variable decision:
                 decisions++;
                 next = pickBranchLit();
 
                 if (next == lit_Undef){
-                  //printf("c last restart ## conflicts  :  %d %d \n",conflictC,decisionLevel());
                   // Model found:
                   return l_True;
                 }
@@ -1169,6 +1285,7 @@ lbool Solver::search(int nof_conflicts)
 }
 
 
+
 double Solver::progressEstimate() const
 {
     double  progress = 0;
@@ -1209,19 +1326,31 @@ void Solver::printIncrementalStats() {
 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( isTwoFanin(v) && value(v) == l_False )
+            jstack.push(v);
+      }
+    #endif
+
   if(incremental && certifiedUNSAT) {
     printf("Can not use incremental and certified unsat in the same time\n");
     exit(-1);
   }
-    model.clear();
-    conflict.clear();
-    if (!ok) return l_False;
+    JustModel.shrink_(JustModel.size());
+    model.shrink_(model.size());
+    conflict.shrink_(conflict.size());
+    if (!ok){
+      travId_prev = travId;
+      return l_False;
+    }
     double curTime = cpuTime();
-
     
     solves++;
-            
-
     
     lbool   status        = l_Undef;
     if(!incremental && verbosity>=1) {
@@ -1240,7 +1369,7 @@ printf("c ==================================[ Search Statistics (every %6d confl
       printf("c |                                                                                                       |\n"); 
 
       printf("c |          RESTARTS           |          ORIGINAL         |              LEARNT              | Progress |\n");
-      printf("c |       NB   Blocked  Avg Cfc |    Vars  Clauses Literals |   Red   Learnts    LBD2  Removed |          |\n");
+      printf("c |       NB   Blocked  Avg Cfc |    Vars  Clauses Literals |   Red   Learnts    LBD2  Removed |          | pol-inconsist\n");
       printf("c =========================================================================================================\n");
     }
 
@@ -1265,12 +1394,29 @@ printf("c ==================================[ Search Statistics (every %6d confl
 
 
     if (status == l_True){
-        // Extend & copy model:
-        model.growTo(nVars());
-        for (int i = 0; i < nVars(); i++) model[i] = value(i);
+
+        if( justUsage() && false ){
+          assert(jheap.empty());
+          //JustModel.growTo(nVars());
+          int i = 0;
+          JustModel.push(toLit(0));
+          for (; i < trail.size(); i++) 
+            if( isRoundWatch(var(trail[i])) && !isTwoFanin(var(trail[i])) )
+              JustModel.push(trail[i]);
+          JustModel[0] = toLit(i);
+        } else {
+          // Extend & copy model:
+          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;
 
+    //#ifdef CGLUCOSE_EXP
+    //if(status == l_True && 0 < justUsage())
+    //  justCheck();
+    //#endif
+
     cancelUntil(0);
 
     double finalTime = cpuTime();
@@ -1299,6 +1445,7 @@ printf("c ==================================[ Search Statistics (every %6d confl
     else if (pCnfFunc)
         terminate_search_early = false; // for next run
 
+    travId_prev = travId;
     return status;
 }
 
@@ -1385,6 +1532,12 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
 
 void Solver::relocAll(ClauseAllocator& to)
 {
+    #ifdef CGLUCOSE_EXP
+    if( CRef_Undef != itpc ){
+      setItpcSize(3);
+      ca.reloc(itpc, to);
+    }
+    #endif
     int v, s, i, j;
     // All watchers:
     //
@@ -1408,6 +1561,10 @@ void Solver::relocAll(ClauseAllocator& to)
     for (i = 0; i < trail.size(); i++){
         Var v = var(trail[i]);
 
+        #ifdef CGLUCOSE_EXP
+        if( isGateCRef(reason(v)) )
+          continue;
+        #endif
         if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
             ca.reloc(vardata[v].reason, to);
     }
@@ -1477,27 +1634,55 @@ void Solver::reset()
     learnts.clear(false);
     //permanentLearnts.clear(false);
     //unaryWatchedClauses.clear(false);
-    model.clear(false);
-    conflict.clear(false);
-    activity.clear(false);
-    assigns.clear(false);
-    polarity.clear(false);
+    model   .shrink_(model   .size());
+    conflict.shrink_(conflict.size());
+    activity.shrink_(activity.size());
+    assigns .shrink_(assigns .size());
+    polarity.shrink_(polarity.size());
     //forceUNSAT.clear(false);
-    decision.clear(false);
-    trail.clear(false);
-    nbpos.clear(false);
-    trail_lim.clear(false);
-    vardata.clear(false);
-    assumptions.clear(false);
-    permDiff.clear(false);
-    lastDecisionLevel.clear(false);
+    decision   .shrink_(decision   .size());
+    trail      .shrink_(trail      .size());
+    trail_lim  .shrink_(trail_lim  .size());
+    vardata    .shrink_(vardata    .size());
+    assumptions.shrink_(assumptions.size());
+    nbpos      .shrink_(nbpos      .size());
+    permDiff   .shrink_(permDiff   .size());
+    #ifdef UPDATEVARACTIVITY
+    lastDecisionLevel.shrink_(lastDecisionLevel.size());
+    #endif
     ca.clear();
-    seen.clear(false);
-    analyze_stack.clear(false);
-    analyze_toclear.clear(false);
+    seen           .shrink_(seen.size());
+    analyze_stack  .shrink_(analyze_stack  .size());
+    analyze_toclear.shrink_(analyze_toclear.size());
     add_tmp.clear(false);
     assumptionPositions.clear(false);
     initialPositions.clear(false);
+
+    #ifdef CGLUCOSE_EXP
+
+    ResetJustData(false);
+
+    jwatch.shrink_(jwatch.size());
+    jdata .shrink_(jdata .size());
+
+
+    travId = 0;
+    travId_prev = 0;
+    var2TravId   .shrink_(var2TravId.size());
+    JustModel    .shrink_(JustModel .size());
+
+    var2FaninLits.shrink_(var2FaninLits.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() );
+    }
+    #endif
 }
 
 ABC_NAMESPACE_IMPL_END
diff --git a/src/sat/glucose2/SimpSolver.h b/src/sat/glucose2/SimpSolver.h
index dbb80434..00dbfa4c 100644
--- a/src/sat/glucose2/SimpSolver.h
+++ b/src/sat/glucose2/SimpSolver.h
@@ -24,6 +24,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose2/Queue.h"
 #include "sat/glucose2/Solver.h"
 
+#include "sat/glucose2/CGlucose.h"
+
 ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Gluco2 {
diff --git a/src/sat/glucose2/SimpSolver2.cpp b/src/sat/glucose2/SimpSolver2.cpp
index 70240cb1..7c2a3b26 100644
--- a/src/sat/glucose2/SimpSolver2.cpp
+++ b/src/sat/glucose2/SimpSolver2.cpp
@@ -68,6 +68,7 @@ SimpSolver::SimpSolver() :
     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
     bwdsub_tmpunit        = ca.alloc(dummy);
     remove_satisfied      = false;
+    parsing               = 0;
 }
 
 
diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h
index d71d1be8..ab73dbc5 100644
--- a/src/sat/glucose2/Solver.h
+++ b/src/sat/glucose2/Solver.h
@@ -37,6 +37,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose2/BoundedQueue.h"
 #include "sat/glucose2/Constants.h"
 
+#include "sat/glucose2/CGlucose.h"
+
 ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Gluco2 {
@@ -123,6 +125,7 @@ public:
     int     nVars      ()      const;       // The current number of variables.
     int     nFreeVars  ()      const;
     int *   getCex     ()      const;
+    int     level      (Var x) const;       // moved level() to public to compile "struct JustOrderLt" -- alanmi
 
     // Incremental mode
     void setIncrementalMode();
@@ -341,7 +344,6 @@ protected:
     int      decisionLevel    ()      const; // Gives the current decisionlevel.
     uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.
     CRef     reason           (Var x) const;
-    int      level            (Var x) const;
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
     bool     withinBudget     ()      const;
     inline bool isSelector(Var v) {return (incremental && v>nbVarsInitialFormula);}
@@ -359,6 +361,99 @@ protected:
     // Returns a random integer 0 <= x < size. Seed must never be 0.
     static inline int irand(double& seed, int size) {
         return (int)(drand(seed) * size); }
+
+
+    // 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; }
+
+    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) { }
+    };
+
+    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
+    vec<unsigned> var2TravId;
+    vec<Lit> var2Fanout0, var2FanoutN, var2FanoutP;
+    CRef itpc; // the interpreted clause of a gate 
+
+    bool isTwoFanin( Var v ) const ; // this var has two fanins 
+    Lit  getFaninLit0( Var v ) const { return var2FaninLits[ (v<<1) + 0 ]; }
+    Lit  getFaninLit1( Var v ) const { return var2FaninLits[ (v<<1) + 1 ]; }
+    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)); }
+    Var  getFaninVar1( Var v ) const { return  var(getFaninLit1(v)); }
+
+    Lit  maxActiveLit(Lit lit0, Lit lit1) const ;
+
+    Lit  fanin2JustLit(Var v) const ;
+    Lit  gateJustFanin(Var v) const ; // l_Undef=satisfied, 0/1 = fanin0/fanin1 requires justify
+    void gateAddJwatch(Var v);
+    CRef gatePropagateCheck( Var v, Var t );
+    CRef gatePropagateCheckThis( Var v );
+    CRef gatePropagateCheckFanout( Var v, Lit lfo );
+    void setItpcSize( int sz ); // sz <= 3
+
+    // directly call by original glucose functions 
+    void updateJustActivity( Var v );
+    void ResetJustData(bool fCleanMemory);
+    Lit  pickJustLit( Var& j_reason );
+    void justCheck();
+    void pushJustQueue(Var v);
+    void restoreJustQueue(int level); // call with cancelUntil
+    void gateClearJwatch( Var v, int backtrack_level );
+
+    CRef gatePropagate( Lit p );
+
+    CRef interpret( Var v, Var t );
+    CRef castCRef( Lit p );  // interpret a gate into a clause 
+    CRef getConfClause( CRef r );
+
+    CRef Var2CRef( Var  v  ) const { return v  |  (1<<(sizeof(CRef)*8-1)); }
+    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;
+public:
+    void setVarFaninLits( Var v, Lit lit1, Lit lit2 );
+    //void delVarFaninLits( Var v);
+
+    int setNewRound(){ return travId ++ ; }
+    void markCone( Var v );
+    bool isRoundWatch( Var v ) const { return travId==var2TravId[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;}
+    int varPolarity(int v){ return polarity[v]? 1: 0;}
+    vec<Lit> JustModel; // model obtained by justification enabled
+
+    int justUsage() const ;
 };
 
 
@@ -378,11 +473,24 @@ inline void Solver::varBumpActivity(Var v, double inc) {
         // 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))
-        order_heap.decrease(v); }
+        order_heap.decrease(v); 
+
+    #ifdef CGLUCOSE_EXP
+    if( justUsage() )
+        updateJustActivity(v);
+
+    #endif
+}
 
 inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
 inline void Solver::claBumpActivity (Clause& c) {
@@ -405,14 +513,27 @@ inline bool     Solver::addClause       (Lit p)                 { add_tmp.clear(
 inline bool     Solver::addClause       (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
 inline bool     Solver::addClause       (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
 inline bool     Solver::locked          (const Clause& c) const { 
+   #ifdef CGLUCOSE_EXP
+
+    if(c.size()>2) 
+     return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && !isGateCRef(reason(var(c[0]))) && ca.lea(reason(var(c[0]))) == &c; 
+   return 
+     (value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && !isGateCRef(reason(var(c[0]))) && ca.lea(reason(var(c[0]))) == &c)
+     || 
+     (value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && !isGateCRef(reason(var(c[1]))) && ca.lea(reason(var(c[1]))) == &c);
+
+   #else
+   
    if(c.size()>2) 
      return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; 
    return 
      (value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c)
      || 
      (value(c[1]) == l_True && reason(var(c[1])) != CRef_Undef && ca.lea(reason(var(c[1]))) == &c);
+
+   #endif
  }
-inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); }
+inline void     Solver::newDecisionLevel()                      {trail_lim.push(trail.size());}
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }
@@ -463,9 +584,9 @@ inline void     Solver::toDimacs      (const char* file, Lit p, Lit q, Lit r){ v
 
 inline void     Solver::addVar(Var v) { while (v >= nVars()) newVar(); }
 
-inline void     Solver::sat_solver_set_var_fanin_lit(int var, int lit0, int lit1) {}  
-inline void     Solver::sat_solver_start_new_round()  {}  
-inline void     Solver::sat_solver_mark_cone(int var) {}  
+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); }
 
 //=================================================================================================
 // Debug etc:
@@ -501,6 +622,9 @@ inline void Solver::printInitialClause(CRef cr)
 //=================================================================================================
 }
 
+
 ABC_NAMESPACE_CXX_HEADER_END
 
+#include "sat/glucose2/CGlucoseCore.h"
+
 #endif
diff --git a/src/sat/glucose2/SolverTypes.h b/src/sat/glucose2/SolverTypes.h
index b15c887f..ea0f76d0 100644
--- a/src/sat/glucose2/SolverTypes.h
+++ b/src/sat/glucose2/SolverTypes.h
@@ -38,6 +38,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "sat/glucose2/Map.h"
 #include "sat/glucose2/Alloc.h"
 
+#include "sat/glucose2/CGlucose.h"
+
 ABC_NAMESPACE_CXX_HEADER_START
 
 namespace Gluco2 {
@@ -145,6 +147,10 @@ class Clause {
 
     friend class ClauseAllocator;
 
+    #ifdef CGLUCOSE_EXP
+    friend class Solver;
+    #endif
+
     // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
     template<class V>
     Clause(const V& ps, bool use_extra, bool learnt) {
@@ -306,9 +312,15 @@ class OccLists
     }
 
     void  clear(bool free = true){
-        occs   .clear(free);
-        dirty  .clear(free);
-        dirties.clear(free);
+        if(free){
+            occs   .clear(free);
+            dirty  .clear(free);
+            dirties.clear(free);
+        } else {
+            occs   .shrink_(occs   .size());
+            dirty  .shrink_(dirty  .size());
+            dirties.shrink_(dirties.size());
+        }
     }
 };
 
diff --git a/src/sat/glucose2/Vec.h b/src/sat/glucose2/Vec.h
index 4b60e13c..711cb694 100644
--- a/src/sat/glucose2/Vec.h
+++ b/src/sat/glucose2/Vec.h
@@ -89,7 +89,8 @@ public:
     T&       operator [] (int index)       { return data[index]; }
 
     // 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.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 moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
 };