Skip to content

A
abc
Commit 230b759d by Alan Mishchenko
Options

Extending sweeper to handle XORs.

parent d350b1a8
Showing with 260 additions and 277 deletions
src/proof/cec/cecSatG2.c
...@@ -121,6 +121,7 @@ struct Cec4_Man_t_ ...@@ -121,6 +121,7 @@ struct Cec4_Man_t_
int nSimulates; int nSimulates;
int nRecycles; int nRecycles;
int nConflicts[2][3]; int nConflicts[2][3];
int nGates[2];
abctime timeCnf; abctime timeCnf;
abctime timeGenPats; abctime timeGenPats;
abctime timeSatSat0; abctime timeSatSat0;
...@@ -460,23 +461,48 @@ int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj ) ...@@ -460,23 +461,48 @@ int Cec4_ObjGetCnfVar( Cec4_Man_t * p, int iObj )
assert( Gia_ObjIsAnd(pObj) ); assert( Gia_ObjIsAnd(pObj) );
if ( fUseSimple ) if ( fUseSimple )
{ {
int iVar0 = Cec4_ObjGetCnfVar( p, Gia_ObjFaninId0(pObj, iObj) ); Gia_Obj_t * pFan0, * pFan1;
int iVar1 = Cec4_ObjGetCnfVar( p, Gia_ObjFaninId1(pObj, iObj) ); //if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
int iVar = Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) ); // printf( "%d", (Gia_IsComplement(pFan1) << 1) + Gia_IsComplement(pFan0) );
if ( p->pPars->jType < 2 ) if ( p->pNew->pMuxes == NULL && Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) && Gia_IsComplement(pFan0) == Gia_IsComplement(pFan1) )
{ {
if ( Gia_ObjIsXor(pObj) ) int iVar0 = Cec4_ObjGetCnfVar( p, Gia_ObjId(p->pNew, Gia_Regular(pFan0)) );
sat_solver_add_xor( p->pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pObj) ); int iVar1 = Cec4_ObjGetCnfVar( p, Gia_ObjId(p->pNew, Gia_Regular(pFan1)) );
else int iVar = Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
sat_solver_add_and( p->pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); 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 iVar0 = Cec4_ObjGetCnfVar( p, Gia_ObjFaninId0(pObj, iObj) );
int Lit1 = Abc_Var2Lit( iVar1, Gia_ObjFaninC1(pObj) ); int iVar1 = Cec4_ObjGetCnfVar( p, Gia_ObjFaninId1(pObj, iObj) );
if ( (Lit0 > Lit1) ^ Gia_ObjIsXor(pObj) ) int iVar = Cec4_ObjSetSatId( p->pNew, pObj, sat_solver_addvar(p->pSat) );
Lit1 ^= Lit0, Lit0 ^= Lit1, Lit1 ^= Lit0; if ( p->pPars->jType < 2 )
sat_solver_set_var_fanin_lit( p->pSat, iVar, Lit0, Lit1 ); {
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 ); return Cec4_ObjSatId( p->pNew, pObj );
} }
...@@ -1477,7 +1503,7 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr ) ...@@ -1477,7 +1503,7 @@ int Cec4_ManSweepNode( Cec4_Man_t * p, int iObj, int iRepr )
{ {
int * pCex = sat_solver_read_cex( p->pSat ); int * pCex = sat_solver_read_cex( p->pSat );
int * pMap = Vec_IntArray(&p->pNew->vVarMap); 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]; ) for ( i = 0; i < pCex[0]; )
Vec_IntPush( p->vPat, Abc_Lit2LitV(pMap, Abc_LitNot(pCex[++i])) ); 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 ...@@ -1685,12 +1711,12 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p
} }
finalize: finalize:
if ( pPars->fVerbose ) 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->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->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->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->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 ); Cec4_ManDestroy( pMan );
//Gia_ManStaticFanoutStop( p ); //Gia_ManStaticFanoutStop( p );
//Gia_ManEquivPrintClasses( p, 1, 0 ); //Gia_ManEquivPrintClasses( p, 1, 0 );
......
src/sat/glucose2/CGlucoseCore.h
...@@ -13,68 +13,50 @@ ...@@ -13,68 +13,50 @@
ABC_NAMESPACE_IMPL_START ABC_NAMESPACE_IMPL_START
namespace Gluco2 { namespace Gluco2 {
inline int Solver::justUsage() const { return jftr; }
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 { inline Lit Solver::gateJustFanin(Var v) const {
assert(v < nVars()); assert(v < nVars());
assert(isTwoFanin(v)); assert(isJReason(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 lbool val0, val1;
if(l_Undef != val0) val0 = val0 ^ getFaninC0(v); val0 = value(getFaninLit0(v));
if(l_Undef != val1) val1 = val1 ^ getFaninC1(v); val1 = value(getFaninLit1(v));
// should be handled by conflict analysis before entering here if(isAND(v)){
assert(value(v) != l_False || l_True != val0 || l_True != val1); // 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; if(val0 == l_False || val1 == l_False)
return lit_Undef;
// branch
if(val0 == l_True) // branch
return ~getFaninLit1(v); if(val0 == l_True)
if(val1 == l_True) return ~getFaninLit1(v);
return ~getFaninLit0(v); if(val1 == l_True)
return ~getFaninLit0(v);
// both fanins are eligible
//return maxActiveLit(faninNJustLit(v, 0), faninNJustLit(v, 1)); return maxActiveLit( ~getFaninLit0(v), ~getFaninLit1(v) );
return fanin2JustLit(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 // a var should at most be enqueued one time
inline void Solver::pushJustQueue(Var v){ inline void Solver::pushJustQueue(Var v){
assert(v < nVars()); assert(v < nVars());
assert(value(v) == l_False); // l_True should be handled by propagation assert(isJReason(v));
assert(isTwoFanin(v));
if( ! isRoundWatch(v) )\ if( ! isRoundWatch(v) )\
return; return;
...@@ -94,7 +76,7 @@ inline void Solver::ResetJustData(bool fCleanMemory){ ...@@ -94,7 +76,7 @@ inline void Solver::ResetJustData(bool fCleanMemory){
inline Lit Solver::pickJustLit( Var& j_reason ){ inline Lit Solver::pickJustLit( Var& j_reason ){
Var next = var_Undef; Var next = var_Undef;
Lit jlit = lit_Undef; Lit jlit = lit_Undef;
//double clk = Abc_Clock();
for( int i = 0; i < jstack.size(); i ++ ){ for( int i = 0; i < jstack.size(); i ++ ){
Var x = jstack[i]; Var x = jstack[i];
if( l_Undef != value(getFaninLit0(x)) || l_Undef != value(getFaninLit1(x)) ) if( l_Undef != value(getFaninLit0(x)) || l_Undef != value(getFaninLit1(x)) )
...@@ -106,13 +88,12 @@ inline Lit Solver::pickJustLit( Var& j_reason ){ ...@@ -106,13 +88,12 @@ inline Lit Solver::pickJustLit( Var& j_reason ){
if( ! jdata[next].now ) if( ! jdata[next].now )
continue; continue;
assert( l_False == value(next) ); assert(isJReason(next));
if( lit_Undef != (jlit = gateJustFanin(next)) ) if( lit_Undef != (jlit = gateJustFanin(next)) )
break; break;
gateAddJwatch(next); gateAddJwatch(next);
} }
j_reason = next; j_reason = next;
return jlit; return jlit;
} }
...@@ -120,8 +101,7 @@ inline Lit Solver::pickJustLit( Var& j_reason ){ ...@@ -120,8 +101,7 @@ inline Lit Solver::pickJustLit( Var& j_reason ){
inline void Solver::gateAddJwatch(Var v){ inline void Solver::gateAddJwatch(Var v){
assert(v < nVars()); assert(v < nVars());
assert(isTwoFanin(v)); assert(isJReason(v));
assert(value(v) == l_False); // l_True should be handled by propagation
if( var_Undef != jwatch[v].prev ) // already in jwatch if( var_Undef != jwatch[v].prev ) // already in jwatch
return; return;
...@@ -132,16 +112,13 @@ inline void Solver::gateAddJwatch(Var v){ ...@@ -132,16 +112,13 @@ inline void Solver::gateAddJwatch(Var v){
Var var0, var1; Var var0, var1;
var0 = getFaninVar0(v); var0 = getFaninVar0(v);
var1 = getFaninVar1(v); var1 = getFaninVar1(v);
val0 = value(var0); val0 = value(getFaninLit0(v));
val1 = value(var1); val1 = value(getFaninLit1(v));
// 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 ); 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); addJwatch(vardata[var0].level < vardata[var1].level? var0: var1, v);
return; return;
} }
...@@ -182,7 +159,7 @@ inline void Solver::addJwatch( Var host, Var member ){ ...@@ -182,7 +159,7 @@ inline void Solver::addJwatch( Var host, Var member ){
assert( var_Undef == jwatch[member].next && var_Undef == jwatch[member].prev ); assert( var_Undef == jwatch[member].next && var_Undef == jwatch[member].prev );
if( var_Undef != jwatch[host].head ) 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].next = jwatch[host].head;
jwatch[member].prev = host; jwatch[member].prev = host;
...@@ -197,12 +174,12 @@ inline void Solver::delJwatch( Var member ){ ...@@ -197,12 +174,12 @@ inline void Solver::delJwatch( Var member ){
assert( jwatch[prev].next == member || jwatch[prev].head == member ); assert( jwatch[prev].next == member || jwatch[prev].head == member );
if( jwatch[prev].next == member ) if( jwatch[prev].next == member )
jwatch[prev].next = next; jwatch[prev].next = next;
else else
jwatch[prev].head = next; jwatch[prev].head = next;
if( var_Undef != next ) if( var_Undef != next )
jwatch[next].prev = prev; jwatch[next].prev = prev;
jwatch[member].prev = var_Undef; jwatch[member].prev = var_Undef;
jwatch[member].next = var_Undef; jwatch[member].next = var_Undef;
...@@ -215,17 +192,12 @@ inline void Solver::delJwatch( Var member ){ ...@@ -215,17 +192,12 @@ inline void Solver::delJwatch( Var member ){
inline void Solver::justCheck(){ inline void Solver::justCheck(){
Lit lit; 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; int i, nJustFail = 0;
for(i=0; i<trail.size(); i++){ for(i=0; i<trail.size(); i++){
Var x = var(trail[i]); Var x = var(trail[i]);
if( ! isTwoFanin(x) )
continue;
if( ! isRoundWatch(x) ) if( ! isRoundWatch(x) )
continue; continue;
if( l_False != value(x) ) if( !isJReason(x) )
continue; continue;
if( lit_Undef != (lit = gateJustFanin(x)) ){ 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 ++ ; 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(){ ...@@ -235,15 +207,6 @@ inline void Solver::justCheck(){
} }
if( nJustFail ) if( nJustFail )
printf("%d just-fails\n", 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 ){ inline void Solver::delVarFaninLits( Var v ){
...@@ -303,6 +266,7 @@ 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 ){ 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); int mincap = var(lit1) < var(lit2)? var(lit2): var(lit1);
mincap = (v < mincap? mincap: v) + 1; mincap = (v < mincap? mincap: v) + 1;
...@@ -344,6 +308,7 @@ inline bool Solver::isTwoFanin( Var v ) const { ...@@ -344,6 +308,7 @@ inline bool Solver::isTwoFanin( Var v ) const {
Lit lit1 = var2FaninLits[ (v<<1) + 1 ]; Lit lit1 = var2FaninLits[ (v<<1) + 1 ];
assert( toLit(~0) == lit0 || var(lit0) < nVars() ); assert( toLit(~0) == lit0 || var(lit0) < nVars() );
assert( toLit(~0) == lit1 || var(lit1) < nVars() ); assert( toLit(~0) == lit1 || var(lit1) < nVars() );
lit0.x = lit1.x = 0; // suppress the warning - alanmi
return toLit(~0) != var2FaninLits[ (v<<1) + 0 ] && toLit(~0) != var2FaninLits[ (v<<1) + 1 ]; return toLit(~0) != var2FaninLits[ (v<<1) + 0 ] && toLit(~0) != var2FaninLits[ (v<<1) + 1 ];
} }
...@@ -389,66 +354,106 @@ check_fanout: ...@@ -389,66 +354,106 @@ check_fanout:
inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){ inline CRef Solver::gatePropagateCheckFanout( Var v, Lit lfo ){
Lit faninLit = sign(lfo)? getFaninLit1(var(lfo)): getFaninLit0(var(lfo)); Lit faninLit = sign(lfo)? getFaninLit1(var(lfo)): getFaninLit0(var(lfo));
assert( var(faninLit) == v ); 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_True == value(var(lfo)) )
{ return Var2CRef(var(lfo));
if( l_False == value(var(lfo)) )
return CRef_Undef; 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)) ) if( l_True == value(var(lfo)) )
return Var2CRef(var(lfo)); return CRef_Undef;
jwatch[var(lfo)].header.dir = sign(lfo); // check value of the other fanin
uncheckedEnqueue(~mkLit(var(lfo)), Var2CRef( var(lfo) ) ); Lit faninLitP = sign(lfo)? getFaninLit0(var(lfo)): getFaninLit1(var(lfo));
} else { if( l_False == value(var(lfo)) ){
assert( l_True == value(faninLit) );
if( l_False == value(faninLitP) )
return CRef_Undef;
if( l_True == value(var(lfo)) ) if( l_True == value(faninLitP) )
return CRef_Undef; 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 // check value of the other fanin
Lit faninLitP = sign(lfo)? getFaninLit0(var(lfo)): getFaninLit1(var(lfo)); 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) ) lbool val0, val1, valo;
return Var2CRef(var(lfo)); 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 else
if( l_True == value(faninLitP) ) if( l_False == (valo ^ (val0 == val1)) )
uncheckedEnqueue( mkLit(var(lfo)), Var2CRef( var(lfo) ) ); return Var2CRef(var(lfo));
} }
return CRef_Undef; return CRef_Undef;
} }
inline CRef Solver::gatePropagateCheckThis( Var v ){ inline CRef Solver::gatePropagateCheckThis( Var v ){
CRef confl = CRef_Undef; CRef confl = CRef_Undef;
if( l_False == value(v) ){ if( isAND(v) ){
if( l_True == value(getFaninLit0(v)) && l_True == value(getFaninLit1(v)) ) if( l_False == value(v) ){
return Var2CRef(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)) ) if( l_False == value(getFaninLit0(v)) || l_False == value(getFaninLit1(v)) )
return CRef_Undef; return CRef_Undef;
if( l_True == value(getFaninLit0(v)) ) if( l_True == value(getFaninLit0(v)) )
uncheckedEnqueue(~getFaninLit1( v ), Var2CRef( v ) ); uncheckedEnqueue(~getFaninLit1( v ), Var2CRef( v ) );
if( l_True == value(getFaninLit1(v)) ) if( l_True == value(getFaninLit1(v)) )
uncheckedEnqueue(~getFaninLit0( v ), Var2CRef( v ) ); uncheckedEnqueue(~getFaninLit0( v ), Var2CRef( v ) );
} else { } else {
assert( l_True == value(v) ); assert( l_True == value(v) );
if( l_False == value(getFaninLit0(v)) || l_False == value(getFaninLit1(v)) ) if( l_False == value(getFaninLit0(v)) || l_False == value(getFaninLit1(v)) )
confl = Var2CRef(v); confl = Var2CRef(v);
if( l_Undef == value( getFaninLit0( v )) ) if( l_Undef == value( getFaninLit0( v )) )
uncheckedEnqueue( getFaninLit0( v ), Var2CRef( v ) ); uncheckedEnqueue( getFaninLit0( v ), Var2CRef( v ) );
if( l_Undef == value( getFaninLit1( v )) ) if( l_Undef == value( getFaninLit1( v )) )
uncheckedEnqueue( getFaninLit1( v ), Var2CRef( 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; return confl;
...@@ -460,97 +465,39 @@ inline CRef Solver::getConfClause( CRef r ){ ...@@ -460,97 +465,39 @@ inline CRef Solver::getConfClause( CRef r ){
Var v = CRef2Var(r); Var v = CRef2Var(r);
assert( isTwoFanin(v) ); assert( isTwoFanin(v) );
if( l_False == value(v) ){ if(isAND(v)){
setItpcSize(3); if( l_False == value(v) ){
Clause& c = ca[itpc]; setItpcSize(3);
c[0] = mkLit(v); Clause& c = ca[itpc];
c[1] = ~getFaninLit0( v ); c[0] = mkLit(v);
c[2] = ~getFaninLit1( v ); c[1] = ~getFaninLit0( v );
} else { c[2] = ~getFaninLit1( v );
setItpcSize(2); } else {
Clause& c = ca[itpc]; setItpcSize(2);
c[0] = ~mkLit(v); 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 ) lbool val0 = value(getFaninLit0(v));
{ // conflict lbool val1 = value(getFaninLit1(v));
confl = Var2CRef(v);
}
// propagate 0 if( l_False == val0 && l_False == val1 )
if( l_True == val0 && l_Undef == val1 ) c[1] = level(getFaninVar0(v)) < level(getFaninVar1(v))? getFaninLit0( v ): getFaninLit1( v );
uncheckedEnqueue( ~getFaninLit1( v ), Var2CRef( v ) ); else
else if( l_False == val0 )
if( l_True == val1 && l_Undef == val0 ) c[1] = getFaninLit0( v );
uncheckedEnqueue( ~getFaninLit0( v ), Var2CRef( v ) ); else
c[1] = getFaninLit1( 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 ) );
} }
} 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 ){ inline void Solver::setItpcSize( int sz ){
...@@ -576,43 +523,57 @@ inline CRef Solver::interpret( Var v, Var t ) ...@@ -576,43 +523,57 @@ inline CRef Solver::interpret( Var v, Var t )
if(l_Undef != val1) val1 = val1 ^ getFaninC1( v ); if(l_Undef != val1) val1 = val1 ^ getFaninC1( v );
if( v == t ){ if( isAND(v) ){
// tracing output if( v == t ){ // tracing output
if( l_False == valo ){ if( l_False == valo ){
setItpcSize(2); setItpcSize(2);
Clause& c = ca[itpc]; Clause& c = ca[itpc];
c[0] = ~mkLit(v); c[0] = ~mkLit(v);
if( l_False == val0 && l_False == val1 ) if( l_False == val0 && l_False == val1 )
c[1] = 0 == jwatch[v].header.dir ? getFaninLit0( v ): getFaninLit1( v ); c[1] = 0 == jwatch[v].header.dir ? getFaninLit0( v ): getFaninLit1( v );
else else
if( l_False == val0 ) if( l_False == val0 )
c[1] = getFaninLit0( v ); c[1] = getFaninLit0( v );
else else
c[1] = getFaninLit1( v ); c[1] = getFaninLit1( v );
} else {
setItpcSize(3);
Clause& c = ca[itpc];
c[0] = mkLit(v);
c[1] = ~getFaninLit0( v );
c[2] = ~getFaninLit1( v );
}
} else { } else {
setItpcSize(3); assert( t == var0 || t == var1 );
Clause& c = ca[itpc]; if( l_False == valo ){
c[0] = mkLit(v); setItpcSize(3);
c[1] = ~getFaninLit0( v ); Clause& c = ca[itpc];
c[2] = ~getFaninLit1( v ); 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 { } else { // xor scope
assert( t == var0 || t == var1 ); setItpcSize(3);
if( l_False == valo ){ Clause& c = ca[itpc];
setItpcSize(3); if( v == t ){
Clause& c = ca[itpc]; c[0] = mkLit(v, l_False == value(v));
c[0] = ~getFaninLit0( v ); c[1] = mkLit(var0, l_True == value(var0));
c[1] = ~getFaninLit1( v ); c[2] = mkLit(var1, l_True == value(var1));
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 { } else {
setItpcSize(2); if( t == var0)
Clause& c = ca[itpc]; c[0] = mkLit(var0, l_False == value(var0)), c[1] = mkLit(var1, l_True == value(var1));
c[0] = t == var0? getFaninLit0( v ): getFaninLit1( v ); else
c[1] = ~mkLit(v); 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 ){ ...@@ -640,12 +601,8 @@ inline void Solver::markCone( Var v ){
markCone( getFaninVar1(v) ); markCone( getFaninVar1(v) );
} }
}; };
ABC_NAMESPACE_IMPL_END ABC_NAMESPACE_IMPL_END
#endif
#endif
\ No newline at end of file
src/sat/glucose2/Glucose2.cpp
...@@ -868,9 +868,8 @@ void Solver::uncheckedEnqueue(Lit p, CRef from) ...@@ -868,9 +868,8 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
trail.push_(p); trail.push_(p);
#ifdef CGLUCOSE_EXP #ifdef CGLUCOSE_EXP
if( 0 < justUsage() ){ if( 0 < justUsage() ){
jdata[var(p)] = mkJustData( l_False == value(var(p)) ); jdata[var(p)] = mkJustData( isJReason(var(p)) );
if(isTwoFanin(var(p)) && l_False == value(var(p))) if( isJReason(var(p)) && l_Undef == value( getFaninVar0(var(p)) ) && l_Undef == value( getFaninVar1(var(p)) ) )
if(l_Undef == value( getFaninVar0(var(p)) ) && l_Undef == value( getFaninVar1(var(p)) ))
jstack.push(var(p)); jstack.push(var(p));
} }
#endif #endif
...@@ -1339,7 +1338,7 @@ lbool Solver::solve_() ...@@ -1339,7 +1338,7 @@ lbool Solver::solve_()
if( 0 < justUsage() ) if( 0 < justUsage() )
for(int i=0; i<trail.size(); i++){ // learnt unit clauses for(int i=0; i<trail.size(); i++){ // learnt unit clauses
Var v = var(trail[i]); Var v = var(trail[i]);
if( isTwoFanin(v) && value(v) == l_False ) if( isJReason(v) )
jstack.push(v); jstack.push(v);
} }
#endif #endif
......
src/sat/glucose2/Solver.h
...@@ -392,17 +392,19 @@ protected: ...@@ -392,17 +392,19 @@ protected:
vec<Lit> var2Fanout0, var2FanoutN, var2FanoutP; vec<Lit> var2Fanout0, var2FanoutN, var2FanoutP;
CRef itpc; // the interpreted clause of a gate 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 getFaninLit0( Var v ) const { return var2FaninLits[ (v<<1) + 0 ]; }
Lit getFaninLit1( Var v ) const { return var2FaninLits[ (v<<1) + 1 ]; } Lit getFaninLit1( Var v ) const { return var2FaninLits[ (v<<1) + 1 ]; }
bool getFaninC0( Var v ) const { return sign(getFaninLit0(v)); } bool getFaninC0 ( Var v ) const { return sign(getFaninLit0(v)); }
bool getFaninC1( Var v ) const { return sign(getFaninLit1(v)); } bool getFaninC1 ( Var v ) const { return sign(getFaninLit1(v)); }
Var getFaninVar0( Var v ) const { return var(getFaninLit0(v)); } Var getFaninVar0( Var v ) const { return var(getFaninLit0(v)); }
Var getFaninVar1( Var v ) const { return var(getFaninLit1(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 Lit gateJustFanin(Var v) const ; // l_Undef=satisfied, 0/1 = fanin0/fanin1 requires justify
void gateAddJwatch(Var v); void gateAddJwatch(Var v);
CRef gatePropagateCheck( Var v, Var t ); CRef gatePropagateCheck( Var v, Var t );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment