// 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::gateJustFanin(Var v) const { assert(v < nVars()); assert(isJReason(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); //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 ); // 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, int index){ assert(v < nVars()); assert(isJReason(v)); if( ! isRoundWatch(v) )\ return; var2NodeData[v].now = true; 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){ jhead = 0; jheap .clear_( fCleanMemory ); } inline Lit Solver::pickJustLit( int& index ){ Var next = var_Undef; Lit jlit = lit_Undef; 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); } while( ! jheap.empty() ){ next = jheap.removeMin(index); if( ! var2NodeData[next].now ) continue; assert(isJReason(next)); if( lit_Undef != (jlit = gateJustFanin(next)) ){ //assert( jheap.prev.key() == activity[getFaninVar0(next)] || jheap.prev.key() == activity[getFaninVar1(next)] ); break; } gateAddJwatch(next,index); } return jlit; } inline void Solver::gateAddJwatch(Var v,int index){ assert(v < nVars()); assert(isJReason(v)); lbool val0, val1; Var var0, var1; var0 = getFaninVar0(v); var1 = getFaninVar1(v); val0 = value(getFaninLit0(v)); val1 = value(getFaninLit1(v)); 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) || !isAND(v) ){ addJwatch(vardata[var0].level < vardata[var1].level? var0: var1, v, index); return; } addJwatch(l_False == val0? var0: var1, v, index); return; } inline void Solver::updateJustActivity( Var v ){ 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( 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, int index ){ assert(level(host) >= level(member)); jnext[index] = jlevel[level(host)]; jlevel[level(host)] = index; } /* * circuit propagation */ inline void Solver::justCheck(){ Lit lit; int i, nJustFail = 0; for(i=0; i<trail.size(); i++){ Var x = var(trail[i]); if( ! isRoundWatch(x) ) continue; 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 ++ ; assert(false); } } if( nJustFail ) printf("%d just-fails\n", nJustFail); } /** 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 ){ assert( var(lit1) != var(lit2) ); int mincap = var(lit1) < var(lit2)? var(lit2): var(lit1); mincap = (v < mincap? mincap: v) + 1; var2NodeData[ v ].lit0 = lit1; var2NodeData[ v ].lit1 = lit2; assert( toLit(~0) != lit1 && toLit(~0) != lit2 ); 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 { 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) != 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 ) 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() ); 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)) ) 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( isAND(var(lfo)) ){ if( l_False == value(faninLit) ) { if( l_False == value(var(lfo)) ) return CRef_Undef; if( l_True == value(var(lfo)) ) return Var2CRef(var(lfo)); var2NodeData[var(lfo)].dir = sign(lfo); uncheckedEnqueue2(~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)); uncheckedEnqueue2( ~faninLitP, Var2CRef( var(lfo) ) ); } else if( l_True == value(faninLitP) ) uncheckedEnqueue2( 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)); lbool val0, val1, valo; val0 = value(faninLit ); val1 = value(faninLitP); valo = value(var(lfo)); if( l_Undef == val1 && l_Undef == valo ) return CRef_Undef; else if( l_Undef == val1 ) uncheckedEnqueue2( ~faninLitP ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( var(lfo) ) ); else if( l_Undef == valo ) uncheckedEnqueue2( ~mkLit( var(lfo), (l_True == val0) ^ (l_True == val1) ), Var2CRef( var(lfo) ) ); else if( l_False == (valo ^ (val0 == val1)) ) return Var2CRef(var(lfo)); } return CRef_Undef; } inline CRef Solver::gatePropagateCheckThis( Var v ){ CRef confl = CRef_Undef; 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_True == value(getFaninLit0(v)) ) uncheckedEnqueue2(~getFaninLit1( v ), Var2CRef( v ) ); if( l_True == value(getFaninLit1(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 )) ) uncheckedEnqueue2( getFaninLit0( v ), Var2CRef( v ) ); if( l_Undef == value( getFaninLit1( v )) ) uncheckedEnqueue2( 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 ) uncheckedEnqueue2(~getFaninLit0( v ) ^ ( (l_True == val1) ^ (l_True == valo) ), Var2CRef( v ) ); else if( l_Undef == val1 ) uncheckedEnqueue2(~getFaninLit1( v ) ^ ( (l_True == val0) ^ (l_True == valo) ), Var2CRef( v ) ); else if( l_False == (valo ^ (val0 == val1)) ) return Var2CRef(v); } return confl; } inline CRef Solver::getConfClause( CRef r ){ if( !isGateCRef(r) ) return r; Var v = CRef2Var(r); assert( isTwoFanin(v) ); 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); 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 ); } } 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 itpc; } 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( isAND(v) ){ if( v == t ){ // tracing output if( l_False == valo ){ setItpcSize(2); Clause& c = ca[itpc]; c[0] = ~mkLit(v); c[1] = var2NodeData[v].dir ? getFaninLit1( v ): getFaninLit0( 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 ) 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 { // 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 { 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)); } } 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; var2NodeData[v].sort = 0; Var var0, var1; var0 = getFaninVar0(v); var1 = getFaninVar1(v); if( !isTwoFanin(v) ) return; 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 ); } inline void Solver::markTill( Var v, int nlim ){ if( var2TravId[v] == travId ) return; vMarked.push(v); if( vMarked.size() >= nlim ) return; if( var2TravId[v] == travId-1 || !isTwoFanin(v) ) goto finalize; markTill( getFaninVar0(v), nlim ); markTill( getFaninVar1(v), nlim ); finalize: var2TravId[v] = travId; } inline void Solver::markApprox( Var v0, Var v1, int nlim ){ int i; if( travId <= 1 || nSkipMark>=4 || 0 == nlim ) goto finalize; vMarked.shrink_( vMarked.size() ); travId ++ ; // travId = t+1 assert(travId>1); markTill(v0, nlim); if( vMarked.size() >= nlim ) goto finalize; markTill(v1, nlim); if( vMarked.size() >= nlim ) goto finalize; travId -- ; // travId = t for(i = 0; i < vMarked.size(); i ++){ var2TravId [ vMarked[i] ] = travId; // set new nodes to time t var2NodeData[ vMarked[i] ].sort = 0; } nSkipMark ++ ; return; finalize: travId ++ ; nSkipMark = 0; markCone(v0); markCone(v1); } inline void Solver::loadJust_rec( Var v ){ //assert( value(v) != l_Undef ); if( var2TravId[v] == travId || value(v) == l_Undef ) return; assert( var2TravId[v] == travId-1 ); var2TravId[v] = travId; vMarked.push(v); if( !isTwoFanin(v) ){ JustModel.push( mkLit( v, value(v) == l_False ) ); return; } loadJust_rec( getFaninVar0(v) ); loadJust_rec( getFaninVar1(v) ); } inline void Solver::loadJust(){ int i; travId ++ ; JustModel.shrink_(JustModel.size()); vMarked.shrink_(vMarked.size()); JustModel.push(toLit(0)); for(i = 0; i < assumptions.size(); i ++) loadJust_rec( var(assumptions[i]) ); JustModel[0] = toLit( JustModel.size()-1 ); travId -- ; for(i = 0; i < vMarked.size(); i ++) var2TravId[ vMarked[i] ] = travId; } }; ABC_NAMESPACE_IMPL_END #endif