Extending sweeper to handle XORs.

4 files changed, 260 insertions, 276 deletions

diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index d924fe6c..72285f23 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -121,6 +121,7 @@ struct Cec4_Man_t_
     int              nSimulates;
     int              nRecycles;
     int              nConflicts[2][3];
+    int              nGates[2];
     abctime          timeCnf;
     abctime          timeGenPats;
     abctime          timeSatSat0;
@@ -460,23 +461,48 @@ int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj )
     assert( Gia_ObjIsAnd(pObj) );
     if ( fUseSimple )
     {
-        int iVar0 = Cec4_ObjGetCnfVar( p, Gia_ObjFaninId0(pObj, iObj) );
-        int iVar1 = Cec4_ObjGetCnfVar( p, Gia_ObjFaninId1(pObj, iObj) );
-        int iVar  = Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
-        if ( p->pPars->jType < 2 )
+        Gia_Obj_t * pFan0, * pFan1;
+        //if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
+        //    printf( "%d", (Gia_IsComplement(pFan1) << 1) + Gia_IsComplement(pFan0) );
+        if ( p->pNew->pMuxes == NULL && Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) && Gia_IsComplement(pFan0) == Gia_IsComplement(pFan1) )
         {
-            if ( Gia_ObjIsXor(pObj) )
-                sat_solver_add_xor( p->pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
-            else
-                sat_solver_add_and( p->pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
+            int iVar0 = Cec4_ObjGetCnfVar( p, Gia_ObjId(p->pNew, Gia_Regular(pFan0)) );
+            int iVar1 = Cec4_ObjGetCnfVar( p, Gia_ObjId(p->pNew, Gia_Regular(pFan1)) );
+            int iVar  = Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
+            if ( p->pPars->jType < 2 )
+                sat_solver_add_xor( p->pSat, iVar, iVar0, iVar1, 0 );
+            if ( p->pPars->jType > 0 )
+            {
+                int Lit0 = Abc_Var2Lit( iVar0, 0 );
+                int Lit1 = Abc_Var2Lit( iVar1, 0 );
+                if ( Lit0 < Lit1 )
+                     Lit1 ^= Lit0, Lit0 ^= Lit1, Lit1 ^= Lit0;
+                assert( Lit0 > Lit1 );
+                sat_solver_set_var_fanin_lit( p->pSat, iVar, Lit0, Lit1 );
+                p->nGates[1]++;
+            }
         }
-        if ( 0 < p->pPars->jType )
+        else
         {
-            int Lit0 = Abc_Var2Lit( iVar0, Gia_ObjFaninC0(pObj) );
-            int Lit1 = Abc_Var2Lit( iVar1, Gia_ObjFaninC1(pObj) );
-            if ( (Lit0 > Lit1) ^ Gia_ObjIsXor(pObj) )
-                 Lit1 ^= Lit0, Lit0 ^= Lit1, Lit1 ^= Lit0;
-            sat_solver_set_var_fanin_lit( p->pSat, iVar, Lit0, Lit1 );
+            int iVar0 = Cec4_ObjGetCnfVar( p, Gia_ObjFaninId0(pObj, iObj) );
+            int iVar1 = Cec4_ObjGetCnfVar( p, Gia_ObjFaninId1(pObj, iObj) );
+            int iVar  = Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
+            if ( p->pPars->jType < 2 )
+            {
+                if ( Gia_ObjIsXor(pObj) )
+                    sat_solver_add_xor( p->pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) );
+                else
+                    sat_solver_add_and( p->pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 );
+            }
+            if ( p->pPars->jType > 0 )
+            {
+                int Lit0 = Abc_Var2Lit( iVar0, Gia_ObjFaninC0(pObj) );
+                int Lit1 = Abc_Var2Lit( iVar1, Gia_ObjFaninC1(pObj) );
+                if ( (Lit0 > Lit1) ^ Gia_ObjIsXor(pObj) )
+                     Lit1 ^= Lit0, Lit0 ^= Lit1, Lit1 ^= Lit0;
+                sat_solver_set_var_fanin_lit( p->pSat, iVar, Lit0, Lit1 );
+                p->nGates[Gia_ObjIsXor(pObj)]++;
+            }
         }
         return Cec4_ObjSatId( p->pNew, pObj );
     }
@@ -1477,7 +1503,7 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
         {
             int * pCex = sat_solver_read_cex( p->pSat );
             int * pMap = Vec_IntArray(&p->pNew->vVarMap);
-            assert( p->pAig->pMuxes == NULL ); // no xors
+            //assert( p->pAig->pMuxes == NULL ); // no xors
             for ( i = 0; i < pCex[0]; )
                 Vec_IntPush( p->vPat, Abc_Lit2LitV(pMap, Abc_LitNot(pCex[++i])) );
         }
@@ -1685,12 +1711,12 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
     }
 finalize:
     if ( pPars->fVerbose )
-        printf( "Performed %d SAT calls:  P = %d (0=%d a=%.2f m=%d)  D = %d (0=%d a=%.2f m=%d)  F = %d   Sim = %d  Recyc = %d\n", 
+        printf( "SAT calls = %d:  P = %d (0=%d a=%.2f m=%d)  D = %d (0=%d a=%.2f m=%d)  F = %d   Sim = %d  Recyc = %d  Xor = %.2f %%\n", 
             pMan->nSatUnsat + pMan->nSatSat + pMan->nSatUndec, 
             pMan->nSatUnsat, pMan->nConflicts[1][0], (float)pMan->nConflicts[1][1]/Abc_MaxInt(1, pMan->nSatUnsat-pMan->nConflicts[1][0]), pMan->nConflicts[1][2],
             pMan->nSatSat,   pMan->nConflicts[0][0], (float)pMan->nConflicts[0][1]/Abc_MaxInt(1, pMan->nSatSat  -pMan->nConflicts[0][0]), pMan->nConflicts[0][2],  
             pMan->nSatUndec,  
-            pMan->nSimulates, pMan->nRecycles );
+            pMan->nSimulates, pMan->nRecycles, 100.0*pMan->nGates[1]/Abc_MaxInt(1, pMan->nGates[0]+pMan->nGates[1]) );
     Cec4_ManDestroy( pMan );
     //Gia_ManStaticFanoutStop( p );
     //Gia_ManEquivPrintClasses( p, 1, 0 );
diff --git a/src/sat/glucose2/CGlucoseCore.h b/src/sat/glucose2/CGlucoseCore.h
index 3400b114..b558f257 100644
--- a/src/sat/glucose2/CGlucoseCore.h
+++ b/src/sat/glucose2/CGlucoseCore.h
@@ -13,68 +13,50 @@
 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 int  Solver::justUsage() const { return jftr; }
 
 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
+	assert(isJReason(v));
 
-	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);
+	lbool val0, val1;
+	val0 = value(getFaninLit0(v));
+	val1 = value(getFaninLit1(v));
+
+	if(isAND(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);
+
+		return maxActiveLit( ~getFaninLit0(v), ~getFaninLit1(v) );
+	} else { // xor scope
+		// should be handled by conflict analysis before entering here
+		assert( value(v) == l_Undef || value(v) != l_False || val0 == val1 );
+
+		// both are assigned
+		if( l_Undef != val0 && l_Undef != val1 )
+			return lit_Undef;
+
+		// should be handled by propagation before entering here
+		assert( l_Undef == val0 && l_Undef == val1 );
+		return maxActiveLit( getFaninPlt0(v), getFaninPlt1(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));
+	assert(isJReason(v));
 
 	if( ! isRoundWatch(v) )\
 		return;
@@ -94,7 +76,7 @@ inline void Solver::ResetJustData(bool 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)) )
@@ -106,13 +88,12 @@ inline Lit Solver::pickJustLit( Var& j_reason ){
 		if( ! jdata[next].now )
 			continue; 
 
-		assert( l_False == value(next) );
+		assert(isJReason(next));
 		if( lit_Undef != (jlit = gateJustFanin(next)) )
 			break;
 		gateAddJwatch(next);
 	}
 
-
 	j_reason = next;
 	return jlit;
 }
@@ -120,8 +101,7 @@ inline Lit Solver::pickJustLit( Var& j_reason ){
 
 inline void Solver::gateAddJwatch(Var v){
 	assert(v < nVars());
-	assert(isTwoFanin(v));
-	assert(value(v) == l_False); // l_True should be handled by propagation
+	assert(isJReason(v));
 
 	if( var_Undef != jwatch[v].prev ) // already in jwatch
 		return;
@@ -132,16 +112,13 @@ inline void Solver::gateAddJwatch(Var v){
 	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);
+	val0 = value(getFaninLit0(v));
+	val1 = value(getFaninLit1(v));
 
-	assert( l_False == val0 || l_False == val1 );
+	assert( !isAND(v) ||  l_False == val0 || l_False == val1  );
+	assert(  isAND(v) || (l_Undef != val0 && l_Undef != val1) );
 
-	if(val0 == l_False && val1 == l_False){
+	if( (val0 == l_False && val1 == l_False) || !isAND(v) ){
 		addJwatch(vardata[var0].level < vardata[var1].level? var0: var1, v);
 		return;
 	}
@@ -182,7 +159,7 @@ 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[jwatch[host].head].prev = member;
 
 	jwatch[member].next = jwatch[host].head;
 	jwatch[member].prev = host;
@@ -197,12 +174,12 @@ inline void Solver::delJwatch( Var member ){
 	assert( jwatch[prev].next == member || jwatch[prev].head == member );
 
 	if( jwatch[prev].next == member )
-	jwatch[prev].next = next;
+		jwatch[prev].next = next;
 	else 
-	jwatch[prev].head = next;
+		jwatch[prev].head = next;
 
 	if( var_Undef != next )
-	jwatch[next].prev = prev;
+		jwatch[next].prev = prev;
 
 	jwatch[member].prev = var_Undef;
 	jwatch[member].next = var_Undef;
@@ -215,17 +192,12 @@ inline void Solver::delJwatch( Var member ){
 
 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) )
+		if( !isJReason(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 ++ ;
@@ -235,15 +207,6 @@ inline void Solver::justCheck(){
 	}
 	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 ){
@@ -303,6 +266,7 @@ inline void Solver::delVarFaninLits( Var v ){
 }
 **/
 inline void Solver::setVarFaninLits( Var v, Lit lit1, Lit lit2 ){
+	assert( var(lit1) != var(lit2) );
 	int mincap = var(lit1) < var(lit2)? var(lit2): var(lit1);
 	mincap = (v < mincap? mincap: v) + 1;
 
@@ -344,6 +308,7 @@ inline bool Solver::isTwoFanin( Var v ) const {
 	Lit lit1 = var2FaninLits[ (v<<1) + 1 ];
 	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 ];
 }
 
@@ -389,66 +354,106 @@ check_fanout:
 inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
 	Lit faninLit = sign(lfo)? getFaninLit1(var(lfo)): getFaninLit0(var(lfo));
 	assert( var(faninLit) == v );
+	if( isAND(var(lfo)) ){
+		if( l_False == value(faninLit) )
+		{
+			if( l_False == value(var(lfo)) )
+				return CRef_Undef;
 
-	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 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(var(lfo)) )
-			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) ) );
+		}
+	} else { // xor scope
 		// 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));
+		lbool val0, val1, valo;
+		val0 = value(faninLit );
+		val1 = value(faninLitP);
+		valo = value(var(lfo));
 
-			uncheckedEnqueue( ~faninLitP, Var2CRef( var(lfo) ) );
-		}
+		if( l_Undef == val1 && l_Undef == valo )
+			return CRef_Undef;
+		else
+		if( l_Undef == val1 )
+			uncheckedEnqueue( ~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) ) );
 		else
-		if( l_True == value(faninLitP) )
-			uncheckedEnqueue( mkLit(var(lfo)), Var2CRef( var(lfo) ) );
+		if( l_False  == (valo ^ (val0 == val1)) )
+			return 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( isAND(v) ){
+		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_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_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( getFaninLit0( v )) )
+				uncheckedEnqueue( getFaninLit0( v ), Var2CRef( v ) );
 
-		if( l_Undef == value( getFaninLit1( v )) )
-			uncheckedEnqueue( getFaninLit1( v ), Var2CRef( v ) );
+			if( l_Undef == value( getFaninLit1( v )) )
+				uncheckedEnqueue( getFaninLit1( v ), Var2CRef( v ) );
 
+		}
+	} else { // xor scope
+		lbool val0, val1, valo;
+		val0 = value(getFaninLit0(v));
+		val1 = value(getFaninLit1(v));
+		valo = value(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 ) );
+		else
+		if( l_Undef == val1 )
+			uncheckedEnqueue(~getFaninLit1( v ) ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( v ) );
+		else
+		if( l_False == (valo ^ (val0 == val1)) )
+			return Var2CRef(v);
 	}
 
 	return confl;
@@ -460,97 +465,39 @@ inline CRef Solver::getConfClause( CRef 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(isAND(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);
 
-		if( l_True == val0 && l_True == val1 )
-		{  // conflict 
-			confl = Var2CRef(v);
-		}
+			lbool val0 = value(getFaninLit0(v));
+			lbool val1 = value(getFaninLit1(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 ) );
+			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 );
 		}
-
+	} else { // xor scope
+		setItpcSize(3);
+		Clause& c = ca[itpc];
+		c[0] = mkLit(v, l_True == value(v));
+		c[1] = mkLit(getFaninVar0(v), l_True == value(getFaninVar0(v)));
+		c[2] = mkLit(getFaninVar1(v), l_True == value(getFaninVar1(v)));
 	}
+	
 
-	return confl;
+	return itpc;
 }
 
 inline void Solver::setItpcSize( int sz ){
@@ -576,43 +523,57 @@ inline CRef Solver::interpret( Var v, Var t )
 	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 );
+	if( isAND(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 {
-			setItpcSize(3);
-			Clause& c = ca[itpc];
-			c[0] = mkLit(v);
-			c[1] = ~getFaninLit0( v );
-			c[2] = ~getFaninLit1( v );
+			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 )
+	                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);
+			}
 		}
-	} 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 { // xor scope
+		setItpcSize(3);
+		Clause& c = ca[itpc];
+		if( v == t ){
+			c[0] = mkLit(v, l_False == value(v));
+			c[1] = mkLit(var0, l_True == value(var0));
+			c[2] = mkLit(var1, l_True == value(var1));
 		} else {
-			setItpcSize(2);
-			Clause& c = ca[itpc];
-			c[0] =  t == var0? getFaninLit0( v ): getFaninLit1( v );
-			c[1] = ~mkLit(v);
+			if( t == var0)
+				c[0] = mkLit(var0, l_False == value(var0)), c[1] = mkLit(var1, l_True  == value(var1));
+			else
+				c[1] = mkLit(var0, l_True  == value(var0)), c[0] = mkLit(var1, l_False == value(var1));
+			c[2] = mkLit(v, l_True == value(v));
 		}
 	}
 
@@ -640,12 +601,8 @@ inline void Solver::markCone( Var v ){
 	markCone( getFaninVar1(v) );
 }
 
-
-
 };
 
-
 ABC_NAMESPACE_IMPL_END
 
-
-#endif
\ No newline at end of file
+#endif
diff --git a/src/sat/glucose2/Glucose2.cpp b/src/sat/glucose2/Glucose2.cpp
index aa3d361f..07525474 100644
--- a/src/sat/glucose2/Glucose2.cpp
+++ b/src/sat/glucose2/Glucose2.cpp
@@ -868,9 +868,8 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
     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)) ))
+        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
@@ -1339,7 +1338,7 @@ lbool Solver::solve_()
     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 )
+          if( isJReason(v) )
             jstack.push(v);
       }
     #endif
diff --git a/src/sat/glucose2/Solver.h b/src/sat/glucose2/Solver.h
index 26b3bdcb..5394a21d 100644
--- a/src/sat/glucose2/Solver.h
+++ b/src/sat/glucose2/Solver.h
@@ -392,17 +392,19 @@ protected:
     vec<Lit> var2Fanout0, var2FanoutN, var2FanoutP;
     CRef itpc; // the interpreted clause of a gate 
 
-    bool isTwoFanin( Var v ) const ; // this var has two fanins 
+    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 ]; }
-    bool getFaninC0( Var v )   const { return sign(getFaninLit0(v)); }
-    bool getFaninC1( Var v )   const { return sign(getFaninLit1(v)); }
+    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  getFaninPlt0( Var v ) const { return mkLit(getFaninVar0(v), 1 == polarity[getFaninVar0(v)]); }
+    Lit  getFaninPlt1( Var v ) const { return mkLit(getFaninVar1(v), 1 == polarity[getFaninVar1(v)]); }
+    Lit  maxActiveLit(Lit lit0, Lit lit1) const { return activity[var(lit0)] < activity[var(lit1)]? lit1: lit0; }
 
-    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 );