From 230b759d16624973821cbd860a476791526c31f8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 16 Nov 2020 08:42:04 -0800 Subject: Extending sweeper to handle XORs. --- src/proof/cec/cecSatG2.c | 60 ++++-- src/sat/glucose2/CGlucoseCore.h | 455 ++++++++++++++++++---------------------- src/sat/glucose2/Glucose2.cpp | 7 +- src/sat/glucose2/Solver.h | 14 +- 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 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 ); -- cgit v1.2.3