diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-11-30 20:56:43 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-11-30 20:56:43 -0800 |
commit | 3b5527b620c943d84ee4ba38d969c114c042ae89 (patch) | |
tree | 90fb9d4578223b74ca74fa68eae7f641d66a2327 /src/opt/sbd/sbdWin.c | |
parent | b3514ee7e000972ecb43603eb08bf56368c0d634 (diff) | |
download | abc-3b5527b620c943d84ee4ba38d969c114c042ae89.tar.gz abc-3b5527b620c943d84ee4ba38d969c114c042ae89.tar.bz2 abc-3b5527b620c943d84ee4ba38d969c114c042ae89.zip |
New SAT-based optimization package.
Diffstat (limited to 'src/opt/sbd/sbdWin.c')
-rw-r--r-- | src/opt/sbd/sbdWin.c | 91 |
1 files changed, 76 insertions, 15 deletions
diff --git a/src/opt/sbd/sbdWin.c b/src/opt/sbd/sbdWin.c index 8f320038..50837e1f 100644 --- a/src/opt/sbd/sbdWin.c +++ b/src/opt/sbd/sbdWin.c @@ -46,46 +46,62 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots ) +sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, Vec_Int_t * vMirrors, int Pivot, Vec_Int_t * vWinObjs, Vec_Int_t * vObj2Var, Vec_Int_t * vTfo, Vec_Int_t * vRoots ) { Gia_Obj_t * pObj; - int i, iObj, Fan0, Fan1, Node, fCompl0, fCompl1, RetValue; + int i, iLit = 1, iObj, Fan0, Fan1, Lit0m, Lit1m, Node, fCompl0, fCompl1, RetValue; + int TfoStart = Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo); int PivotVar = Vec_IntEntry(vObj2Var, Pivot); + //Vec_IntPrint( vWinObjs ); + //Vec_IntPrint( vTfo ); + //Vec_IntPrint( vRoots ); // create SAT solver if ( pSat == NULL ) pSat = sat_solver_new(); else sat_solver_restart( pSat ); sat_solver_setnvars( pSat, Vec_IntSize(vWinObjs) + Vec_IntSize(vTfo) + Vec_IntSize(vRoots) + 32 ); + // create constant 0 clause + sat_solver_addclause( pSat, &iLit, &iLit + 1 ); // add clauses for all nodes - Vec_IntForEachEntry( vWinObjs, iObj, i ) + Vec_IntForEachEntryStart( vWinObjs, iObj, i, 1 ) { pObj = Gia_ManObj( p, iObj ); if ( Gia_ObjIsCi(pObj) ) continue; assert( Gia_ObjIsAnd(pObj) ); + assert( Vec_IntEntry( vMirrors, iObj ) < 0 ); Node = Vec_IntEntry( vObj2Var, iObj ); - Fan0 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId0(pObj, iObj) ); - Fan1 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId1(pObj, iObj) ); - fCompl0 = Gia_ObjFaninC0(pObj); - fCompl1 = Gia_ObjFaninC1(pObj); + Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) ); + Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) ); + Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj); + Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj); + Fan0 = Vec_IntEntry( vObj2Var, Fan0 ); + Fan1 = Vec_IntEntry( vObj2Var, Fan1 ); + fCompl0 = Gia_ObjFaninC0(pObj) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m)); + fCompl1 = Gia_ObjFaninC1(pObj) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m)); if ( Gia_ObjIsXor(pObj) ) sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 ); else sat_solver_add_and( pSat, Node, Fan0, Fan1, fCompl0, fCompl1, 0 ); } // add second clauses for the TFO - Vec_IntForEachEntryStart( vWinObjs, iObj, i, Vec_IntSize(vWinObjs) - Vec_IntSize(vTfo) ) + Vec_IntForEachEntryStart( vWinObjs, iObj, i, TfoStart ) { pObj = Gia_ManObj( p, iObj ); assert( Gia_ObjIsAnd(pObj) ); + assert( Vec_IntEntry( vMirrors, iObj ) < 0 ); Node = Vec_IntEntry( vObj2Var, iObj ) + Vec_IntSize(vTfo); - Fan0 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId0(pObj, iObj) ); - Fan1 = Vec_IntEntry( vObj2Var, Gia_ObjFaninId1(pObj, iObj) ); - Fan0 = Fan0 <= PivotVar ? Fan0 : Fan0 + Vec_IntSize(vTfo); - Fan1 = Fan1 <= PivotVar ? Fan1 : Fan1 + Vec_IntSize(vTfo); - fCompl0 = Gia_ObjFaninC0(pObj) ^ (Fan0 == PivotVar); - fCompl1 = Gia_ObjFaninC1(pObj) ^ (Fan1 == PivotVar); + Lit0m = Vec_IntEntry( vMirrors, Gia_ObjFaninId0(pObj, iObj) ); + Lit1m = Vec_IntEntry( vMirrors, Gia_ObjFaninId1(pObj, iObj) ); + Fan0 = Lit0m >= 0 ? Abc_Lit2Var(Lit0m) : Gia_ObjFaninId0(pObj, iObj); + Fan1 = Lit1m >= 0 ? Abc_Lit2Var(Lit1m) : Gia_ObjFaninId1(pObj, iObj); + Fan0 = Vec_IntEntry( vObj2Var, Fan0 ); + Fan1 = Vec_IntEntry( vObj2Var, Fan1 ); + Fan0 = Fan0 < TfoStart ? Fan0 : Fan0 + Vec_IntSize(vTfo); + Fan1 = Fan1 < TfoStart ? Fan1 : Fan1 + Vec_IntSize(vTfo); + fCompl0 = Gia_ObjFaninC0(pObj) ^ (Fan0 == PivotVar) ^ (Lit0m >= 0 && Abc_LitIsCompl(Lit0m)); + fCompl1 = Gia_ObjFaninC1(pObj) ^ (Fan1 == PivotVar) ^ (Lit1m >= 0 && Abc_LitIsCompl(Lit1m)); if ( Gia_ObjIsXor(pObj) ) sat_solver_add_xor( pSat, Node, Fan0, Fan1, fCompl0 ^ fCompl1 ); else @@ -98,8 +114,9 @@ sat_solver * Sbd_ManSatSolver( sat_solver * pSat, Gia_Man_t * p, int Pivot, Vec_ Vec_Int_t * vFaninVars = Vec_IntAlloc( Vec_IntSize(vRoots) ); Vec_IntForEachEntry( vRoots, iObj, i ) { - Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) ); + assert( Vec_IntEntry( vMirrors, iObj ) < 0 ); Node = Vec_IntEntry( vObj2Var, iObj ); + Vec_IntPush( vFaninVars, Abc_Var2Lit(nVars, 0) ); sat_solver_add_xor( pSat, Node, Node + Vec_IntSize(vTfo), nVars++, 0 ); } // make OR clause for the last nRoots variables @@ -190,6 +207,50 @@ word Sbd_ManSolve( sat_solver * pSat, int PivotVar, int FreeVar, Vec_Int_t * vDi return SBD_SAT_SAT; } +/**Function************************************************************* + + Synopsis [Returns a bunch of positive/negative random care minterms.] + + Description [Returns 0/1 if the functions is const 0/1.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void sat_solver_random_polarity(sat_solver* s) +{ + int i, k; + for ( i = 0; i < s->size; i += 64 ) + { + word Polar = Gia_ManRandomW(0); + for ( k = 0; k < 64 && (i << 6) + k < s->size; k++ ) + s->polarity[(i << 6) + k] = Abc_TtGetBit(&Polar, k); + } +} +int Sbd_ManCollectConstants( sat_solver * pSat, int nCareMints[2], int PivotVar, word * pVarSims[], Vec_Int_t * vInds ) +{ + int nBTLimit = 0; + int i, Ind; + assert( Vec_IntSize(vInds) == nCareMints[0] + nCareMints[1] ); + Vec_IntForEachEntry( vInds, Ind, i ) + { + int fOffSet = (int)(i < nCareMints[0]); + int status, k, iLit = Abc_Var2Lit( PivotVar, fOffSet ); + sat_solver_random_polarity( pSat ); + status = sat_solver_solve( pSat, &iLit, &iLit + 1, nBTLimit, 0, 0, 0 ); + if ( status == l_Undef ) + return -2; + if ( status == l_False ) + return fOffSet; + for ( k = 0; k <= PivotVar; k++ ) + if ( Abc_TtGetBit(pVarSims[k], Ind) != sat_solver_var_value(pSat, k) ) + Abc_TtXorBit(pVarSims[k], Ind); + } + return -1; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |