diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-25 22:07:32 -0500 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-02-25 22:07:32 -0500 |
commit | 7e293ebe08aac09a7dab351731f9e97c2b4dde27 (patch) | |
tree | 515831b7fe3aa80f95a31913b4601097017b20f6 /src | |
parent | fe3b2e250bc642509e7c954b837d21d8c6bb8d42 (diff) | |
download | abc-7e293ebe08aac09a7dab351731f9e97c2b4dde27.tar.gz abc-7e293ebe08aac09a7dab351731f9e97c2b4dde27.tar.bz2 abc-7e293ebe08aac09a7dab351731f9e97c2b4dde27.zip |
User-controlable SAT sweeper.
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/gia.h | 10 | ||||
-rw-r--r-- | src/aig/gia/giaSweeper.c | 393 | ||||
-rw-r--r-- | src/map/if/ifMap.c | 4 | ||||
-rw-r--r-- | src/misc/util/abc_global.h | 3 | ||||
-rw-r--r-- | src/opt/dau/dauTree.c | 2 |
5 files changed, 404 insertions, 8 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 206c9dc4..08336ded 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -108,6 +108,7 @@ struct Gia_Man_t_ int * pHTable; // hash table int nHTable; // hash table size int fAddStrash; // performs additional structural hashing + int fSweeper; // sweeper is running int * pRefs; // the reference count Vec_Int_t * vLevels; // levels of the nodes int nLevels; // the mamixum level @@ -473,6 +474,12 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 ) Gia_ObjAddFanout( p, Gia_ObjFanin0(pObj), pObj ); Gia_ObjAddFanout( p, Gia_ObjFanin1(pObj), pObj ); } + if ( p->fSweeper ) + { + Gia_ObjFanin0(pObj)->fMark0 = Gia_ObjFanin1(pObj)->fMark0 = 1; + pObj->fPhase = (Gia_ObjPhase(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC0(pObj)) & + (Gia_ObjPhase(Gia_ObjFanin1(pObj)) ^ Gia_ObjFaninC1(pObj)); + } return Gia_ObjId( p, pObj ) << 1; } static inline int Gia_ManAppendPinType( Gia_Man_t * p, int iLit ) @@ -983,6 +990,9 @@ extern void Gia_ManStgPrint( FILE * pFile, Vec_Int_t * vLines, in extern Gia_Man_t * Gia_ManStgRead( char * pFileName, int kHot, int fVerbose ); /*=== giaSweep.c ============================================================*/ extern Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars ); +/*=== giaSweeper.c ============================================================*/ +extern Gia_Man_t * Gia_ManStartSweeper(); +extern void Gia_ManStopSweeper( Gia_Man_t * p ); /*=== giaSwitch.c ============================================================*/ extern float Gia_ManEvaluateSwitching( Gia_Man_t * p ); extern float Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne ); diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c index 32ea73e9..83c6fe6a 100644 --- a/src/aig/gia/giaSweeper.c +++ b/src/aig/gia/giaSweeper.c @@ -68,19 +68,36 @@ struct Swp_Man_t_ Vec_Int_t * vCondProbes; // conditions as probes Vec_Int_t * vCondLits; // conditions as literals // equivalence checking - int nSatVars; // counter of SAT variables - Vec_Int_t * vId2Sat; // mapping of Obj IDs into SAT vars + Vec_Int_t * vId2Lit; // mapping of Obj IDs into SAT literal + Vec_Int_t * vFront; // temporary frontier + Vec_Int_t * vFanins; // temporary fanins sat_solver * pSat; // SAT solver + int nSatVars; // counter of SAT variables // statistics int nSatCalls; int nSatCallsSat; int nSatCallsUnsat; int nSatFails; int nSatProofs; - - + clock_t timeSat; + clock_t timeSatSat; + clock_t timeSatUnsat; + clock_t timeSatUndec; }; +static inline int Swp_ManObj2Lit( Gia_Man_t * p, int Id ) +{ + return Vec_IntGetEntry( ((Swp_Man_t *)p->pData)->vId2Lit, Id ); +} +static inline void Swp_ManSetObj2Lit( Gia_Man_t * p, int Id, int Lit ) +{ + Vec_IntSetEntry( ((Swp_Man_t *)p->pData)->vId2Lit, Id, Lit ); +} +static inline int Swp_ManLit2Lit( Gia_Man_t * p, int Lit ) +{ + return Abc_Lit2LitL( Vec_IntArray(((Swp_Man_t *)p->pData)->vId2Lit), Lit ); +} + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -107,12 +124,19 @@ static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia ) p->vLit2Prob = Vec_IntStartFull( 10000 ); p->vCondProbes = Vec_IntAlloc( 100 ); p->vCondLits = Vec_IntAlloc( 100 ); + p->vFront = Vec_IntAlloc( 100 ); + p->vFanins = Vec_IntAlloc( 100 ); + p->pSat = sat_solver_new(); + p->nSatVars = 1; + Swp_ManSetObj2Lit( pGia, 0, Abc_Var2Lit(p->nSatVars++, 0) ); pGia->pData = p; return p; } static inline void Swp_ManStop( Gia_Man_t * pGia ) { Swp_Man_t * p = (Swp_Man_t *)pGia->pData; + Vec_IntFree( p->vFront ); + Vec_IntFree( p->vFanins ); Vec_IntFree( p->vProbes ); Vec_IntFree( p->vProbRefs ); Vec_IntFree( p->vLit2Prob ); @@ -121,6 +145,34 @@ static inline void Swp_ManStop( Gia_Man_t * pGia ) ABC_FREE( p ); pGia->pData = NULL; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManStartSweeper() +{ + Gia_Man_t * pGia; + pGia = Gia_ManStart( 10000 ); + Gia_ManHashStart( pGia ); + Swp_ManStart( pGia ); + pGia->fSweeper = 1; + return pGia; +} +void Gia_ManStopSweeper( Gia_Man_t * pGia ) +{ + pGia->fSweeper = 0; + Swp_ManStop( pGia ); + Gia_ManHashStop( pGia ); + Gia_ManStop( pGia ); +} /**Function************************************************************* @@ -250,7 +302,340 @@ Gia_Man_t * Gia_ManExtractUserLogic( Gia_Man_t * p, int * pProbeIds, int nProbeI } +//#if 0 + +/**Function************************************************************* + + Synopsis [Addes clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManAddClausesMux( Gia_Man_t * pGia, Gia_Obj_t * pNode ) +{ + Swp_Man_t * p = (Swp_Man_t *)pGia->pData; + Gia_Obj_t * pNodeI, * pNodeT, * pNodeE; + int pLits[4], LitF, LitI, LitT, LitE, RetValue; + assert( !Gia_IsComplement( pNode ) ); + assert( Gia_ObjIsMuxType( pNode ) ); + // get nodes (I = if, T = then, E = else) + pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); + // get the Litiable numbers + LitF = Swp_ManLit2Lit( pGia, Gia_Obj2Lit(pGia,pNode) ); + LitI = Swp_ManLit2Lit( pGia, Gia_Obj2Lit(pGia,pNodeI) ); + LitT = Swp_ManLit2Lit( pGia, Gia_Obj2Lit(pGia,pNodeT) ); + LitE = Swp_ManLit2Lit( pGia, Gia_Obj2Lit(pGia,pNodeE) ); + + // f = ITE(i, t, e) + + // i' + t' + f + // i' + t + f' + // i + e' + f + // i + e + f' + + // create four clauses + pLits[0] = Abc_LitNotCond(LitI, 1); + pLits[1] = Abc_LitNotCond(LitT, 1); + pLits[2] = Abc_LitNotCond(LitF, 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = Abc_LitNotCond(LitI, 1); + pLits[1] = Abc_LitNotCond(LitT, 0); + pLits[2] = Abc_LitNotCond(LitF, 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = Abc_LitNotCond(LitI, 0); + pLits[1] = Abc_LitNotCond(LitE, 1); + pLits[2] = Abc_LitNotCond(LitF, 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = Abc_LitNotCond(LitI, 0); + pLits[1] = Abc_LitNotCond(LitE, 0); + pLits[2] = Abc_LitNotCond(LitF, 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + + // two additional clauses + // t' & e' -> f' + // t & e -> f + + // t + e + f' + // t' + e' + f + + if ( LitT == LitE ) + { +// assert( fCompT == !fCompE ); + return; + } + + pLits[0] = Abc_LitNotCond(LitT, 0); + pLits[1] = Abc_LitNotCond(LitE, 0); + pLits[2] = Abc_LitNotCond(LitF, 1); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); + pLits[0] = Abc_LitNotCond(LitT, 1); + pLits[1] = Abc_LitNotCond(LitE, 1); + pLits[2] = Abc_LitNotCond(LitF, 0); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 ); + assert( RetValue ); +} + +/**Function************************************************************* + + Synopsis [Addes clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManAddClausesSuper( Gia_Man_t * pGia, Gia_Obj_t * pNode, Vec_Int_t * vSuper ) +{ + Swp_Man_t * p = (Swp_Man_t *)pGia->pData; + int i, RetValue, Lit, LitNode, pLits[2]; + assert( !Gia_IsComplement(pNode) ); + assert( Gia_ObjIsAnd( pNode ) ); + // suppose AND-gate is A & B = C + // add !A => !C or A + !C + LitNode = Swp_ManObj2Lit( pGia, Gia_ObjId(pGia, pNode) ); + Vec_IntForEachEntry( vSuper, Lit, i ) + { + pLits[0] = Abc_LitNot( LitNode ); + pLits[1] = Swp_ManLit2Lit( pGia, Lit ); + Vec_IntWriteEntry( vSuper, i, Abc_LitNot(pLits[1]) ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); + } + // add A & B => C or !A + !B + C + Vec_IntPush( vSuper, LitNode ); + RetValue = sat_solver_addclause( p->pSat, Vec_IntArray(vSuper), Vec_IntArray(vSuper) + Vec_IntSize(vSuper) ); + assert( RetValue ); + (void) RetValue; +} + + +/**Function************************************************************* + + Synopsis [Collects the supergate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCollectSuper_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper ) +{ + // stop at complements, shared, PIs, and MUXes + if ( Gia_IsComplement(pObj) || pObj->fMark0 || Gia_ObjIsCi(pObj) || Gia_ObjIsMuxType(pObj) ) + { + Vec_IntPushUnique( vSuper, Gia_ObjId(p, pObj) ); + return; + } + Gia_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper ); + Gia_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper ); +} +void Gia_ManCollectSuper( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSuper ) +{ + assert( !Gia_IsComplement(pObj) ); + assert( Gia_ObjIsAnd(pObj) ); + Vec_IntClear( vSuper ); + Gia_ManCollectSuper_rec( p, Gia_ObjChild0(pObj), vSuper ); + Gia_ManCollectSuper_rec( p, Gia_ObjChild1(pObj), vSuper ); +} + +/**Function************************************************************* + + Synopsis [Updates the solver clause database.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManObjAddToFrontier( Gia_Man_t * pGia, int Id, Vec_Int_t * vFront ) +{ + Swp_Man_t * p = (Swp_Man_t *)pGia->pData; + Gia_Obj_t * pObj; + if ( Id == 0 ) + return; + if ( Swp_ManObj2Lit(pGia, Id) ) + return; + pObj = Gia_ManObj( pGia, Id ); + Swp_ManSetObj2Lit( pGia, Id, Abc_Var2Lit(p->nSatVars++, pObj->fPhase) ); + sat_solver_setnvars( p->pSat, p->nSatVars + 100 ); + if ( Gia_ObjIsAnd(pObj) ) + Vec_IntPush( vFront, Id ); +} +void Gia_ManCnfNodeAddToSolver( Gia_Man_t * p, int NodeId ) +{ + Vec_Int_t * vFront, * vFanins; + Gia_Obj_t * pNode; + int i, k, Id; + // quit if CNF is ready + if ( NodeId == 0 ) + return; + if ( Swp_ManObj2Lit(p, NodeId) ) + return; + // start the frontier + vFront = ((Swp_Man_t *)p->pData)->vFront; + Vec_IntClear( vFront ); + Gia_ManObjAddToFrontier( p, NodeId, vFront ); + // explore nodes in the frontier + Gia_ManForEachObjVec( vFront, p, pNode, i ) + { + vFanins = ((Swp_Man_t *)p->pData)->vFanins; + // create the supergate + assert( Swp_ManObj2Lit(p,Gia_ObjId(p, pNode)) ); + if ( Gia_ObjIsMuxType(pNode) ) + { + Vec_IntClear( vFanins ); + Vec_IntPushUnique( vFanins, Gia_ObjFaninId0p( p, Gia_ObjFanin0(pNode) ) ); + Vec_IntPushUnique( vFanins, Gia_ObjFaninId0p( p, Gia_ObjFanin1(pNode) ) ); + Vec_IntPushUnique( vFanins, Gia_ObjFaninId1p( p, Gia_ObjFanin0(pNode) ) ); + Vec_IntPushUnique( vFanins, Gia_ObjFaninId1p( p, Gia_ObjFanin1(pNode) ) ); + Vec_IntForEachEntry( vFanins, Id, k ) + Gia_ManObjAddToFrontier( p, Id, vFront ); + Gia_ManAddClausesMux( p, pNode ); + } + else + { + Gia_ManCollectSuper( p, pNode, vFanins ); + Vec_IntForEachEntry( vFanins, Id, k ) + Gia_ManObjAddToFrontier( p, Id, vFront ); + Gia_ManAddClausesSuper( p, pNode, vFanins ); + } + assert( Vec_IntSize(vFanins) > 1 ); + } +} + + +/**Function************************************************************* + + Synopsis [Runs equivalence test for the two nodes.] + + Description [Both nodes should be regular and different from each other.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManNodesAreEquiv( Gia_Man_t * pGia, int iOld, int iNew ) +{ + Swp_Man_t * p = (Swp_Man_t *)pGia->pData; + Gia_Obj_t * pOld = Gia_Lit2Obj( pGia, iOld ); + Gia_Obj_t * pNew = Gia_Lit2Obj( pGia, iNew ); + int Lit, RetValue, RetValue1; + clock_t clk; + p->nSatCalls++; + + // sanity checks + assert( pOld != pNew ); + assert( p->pSat != NULL ); + + // if the nodes do not have SAT variables, allocate them + Gia_ManCnfNodeAddToSolver( pGia, Abc_Lit2Var(iOld) ); + Gia_ManCnfNodeAddToSolver( pGia, Abc_Lit2Var(iNew) ); + sat_solver_compress( p->pSat ); + + // solve under assumptions + // A = 1; B = 0 OR A = 1; B = 1 + Lit = Swp_ManLit2Lit( pGia, iOld ); + Vec_IntPush( p->vCondLits, Lit ); + + Lit = Swp_ManLit2Lit( pGia, iNew ); + Vec_IntPush( p->vCondLits, Abc_LitNot(Lit) ); + +clk = clock(); + RetValue1 = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondLits), Vec_IntArray(p->vCondLits) + Vec_IntSize(p->vCondLits), + (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); +p->timeSat += clock() - clk; + if ( RetValue1 == l_False ) + { + int * pLits = Vec_IntArray(p->vCondLits) + Vec_IntSize(p->vCondLits) - 2; + pLits[0] = Abc_LitNot( pLits[0] ); + pLits[1] = Abc_LitNot( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); +p->timeSatUnsat += clock() - clk; + p->nSatCallsUnsat++; + Vec_IntShrink( p->vCondLits, Vec_IntSize(p->vCondLits) - 2 ); + } + else if ( RetValue1 == l_True ) + { +p->timeSatSat += clock() - clk; + p->nSatCallsSat++; + Vec_IntShrink( p->vCondLits, Vec_IntSize(p->vCondLits) - 2 ); + return 0; + } + else // if ( RetValue1 == l_Undef ) + { +p->timeSatUndec += clock() - clk; + p->nSatFails++; + Vec_IntShrink( p->vCondLits, Vec_IntSize(p->vCondLits) - 2 ); + return -1; + } + + // if the old node was constant 0, we already know the answer + if ( Gia_ManIsConstLit(iNew) ) + { + p->nSatProofs++; + return 1; + } + + // solve under assumptions + // A = 0; B = 1 OR A = 0; B = 0 + Lit = Swp_ManLit2Lit( pGia, iOld ); + Vec_IntPush( p->vCondLits, Abc_LitNot(Lit) ); + + Lit = Swp_ManLit2Lit( pGia, iNew ); + Vec_IntPush( p->vCondLits, Lit ); + +clk = clock(); + RetValue1 = sat_solver_solve( p->pSat, Vec_IntArray(p->vCondLits), Vec_IntArray(p->vCondLits) + Vec_IntSize(p->vCondLits), + (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); +p->timeSat += clock() - clk; + if ( RetValue1 == l_False ) + { + int * pLits = Vec_IntArray(p->vCondLits) + Vec_IntSize(p->vCondLits) - 2; + pLits[0] = Abc_LitNot( pLits[0] ); + pLits[1] = Abc_LitNot( pLits[1] ); + RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 ); + assert( RetValue ); +p->timeSatUnsat += clock() - clk; + p->nSatCallsUnsat++; + Vec_IntShrink( p->vCondLits, Vec_IntSize(p->vCondLits) - 2 ); + } + else if ( RetValue1 == l_True ) + { +p->timeSatSat += clock() - clk; + p->nSatCallsSat++; + Vec_IntShrink( p->vCondLits, Vec_IntSize(p->vCondLits) - 2 ); + return 0; + } + else // if ( RetValue1 == l_Undef ) + { +p->timeSatUndec += clock() - clk; + p->nSatFails++; + Vec_IntShrink( p->vCondLits, Vec_IntSize(p->vCondLits) - 2 ); + return -1; + } + // return SAT proof + p->nSatProofs++; + return 1; +} +//#endif /**Function************************************************************* diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index d9cb4682..8fb2962e 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -286,9 +286,9 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep int Fans[2][DAU_MAX_VAR], * pFans[2] = { Fans[0], Fans[1] }; // create fanins for ( j = 0; j < (int)pCut0->nLeaves; j++ ) - pFans[0][j] = Abc_Lit2Lit( p->pPerm[0], (int)pCut0->pPerm[j] ); + pFans[0][j] = Abc_Lit2LitV( p->pPerm[0], (int)pCut0->pPerm[j] ); for ( j = 0; j < (int)pCut1->nLeaves; j++ ) - pFans[1][j] = Abc_Lit2Lit( p->pPerm[1], (int)pCut1->pPerm[j] ); + pFans[1][j] = Abc_Lit2LitV( p->pPerm[1], (int)pCut1->pPerm[j] ); // canonicize if ( iDsd[0] > iDsd[1] ) { diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index 21ae6a9c..914fd327 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -263,7 +263,8 @@ static inline int Abc_LitIsCompl( int Lit ) { return Lit & 1; static inline int Abc_LitNot( int Lit ) { return Lit ^ 1; } static inline int Abc_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); } static inline int Abc_LitRegular( int Lit ) { return Lit & ~01; } -static inline int Abc_Lit2Lit( int * pMap, int Lit ) { return Abc_Var2Lit( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) ); } +static inline int Abc_Lit2LitV( int * pMap, int Lit ) { return Abc_Var2Lit( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) ); } +static inline int Abc_Lit2LitL( int * pMap, int Lit ) { return Abc_LitNotCond( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) ); } enum Abc_VerbLevel { diff --git a/src/opt/dau/dauTree.c b/src/opt/dau/dauTree.c index db883764..3e465632 100644 --- a/src/opt/dau/dauTree.c +++ b/src/opt/dau/dauTree.c @@ -1489,7 +1489,7 @@ if ( Counter ) // translate this map into the one that maps vars of iDsdRes into literals of cut pFun->nFans = Dss_VecLitSuppSize( p->vObjs, pFun->iDsd ); for ( i = 0; i < (int)pFun->nFans; i++ ) - pFun->pFans[i] = (unsigned char)Abc_Lit2Lit( pMapDsd2Truth, pPermDsd[i] ); + pFun->pFans[i] = (unsigned char)Abc_Lit2LitV( pMapDsd2Truth, pPermDsd[i] ); // Dss_EntPrint( pEnt, pFun ); return pFun; |