diff options
Diffstat (limited to 'src/aig/gia')
-rw-r--r-- | src/aig/gia/giaSatEdge.c | 4 | ||||
-rw-r--r-- | src/aig/gia/giaSatLE.c | 880 | ||||
-rw-r--r-- | src/aig/gia/module.make | 1 |
3 files changed, 882 insertions, 3 deletions
diff --git a/src/aig/gia/giaSatEdge.c b/src/aig/gia/giaSatEdge.c index 13446414..75f928ec 100644 --- a/src/aig/gia/giaSatEdge.c +++ b/src/aig/gia/giaSatEdge.c @@ -447,7 +447,6 @@ void Seg_ManComputeDelay( Gia_Man_t * pGia, int DelayInit, int nFanouts, int fTw Vec_Int_t * vEdges2 = NULL; int i, iLut, iFirst, nVars, status, Delay, nConfs; Seg_Man_t * p = Seg_ManAlloc( pGia, nFanouts ); - Vec_Int_t * vVars = Vec_IntStartNatural( p->nVars ); int DelayStart = DelayInit ? DelayInit : p->DelayMax; if ( fVerbose ) @@ -460,8 +459,7 @@ void Seg_ManComputeDelay( Gia_Man_t * pGia, int DelayInit, int nFanouts, int fTw sat_solver_set_runtime_limit( p->pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); sat_solver_set_random( p->pSat, 1 ); sat_solver_set_polarity( p->pSat, Vec_IntArray(p->vPolars), Vec_IntSize(p->vPolars) ); - sat_solver_set_var_activity( p->pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) ); - Vec_IntFree( vVars ); + sat_solver_set_var_activity( p->pSat, NULL, p->nVars ); // increment delay gradually for ( Delay = p->DelayMax; Delay >= 0; Delay-- ) { diff --git a/src/aig/gia/giaSatLE.c b/src/aig/gia/giaSatLE.c new file mode 100644 index 00000000..984bbfbf --- /dev/null +++ b/src/aig/gia/giaSatLE.c @@ -0,0 +1,880 @@ +/**CFile**************************************************************** + + FileName [giaSatLE.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Mapping with edges.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaSatLE.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "misc/extra/extra.h" +#include "misc/tim/tim.h" +#include "sat/bsat/satStore.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static inline int Sle_CutSize( int * pCut ) { return pCut[0] & 0xF; } // 4 bits +static inline int Sle_CutSign( int * pCut ) { return pCut[0] >> 4; } // 28 bits +static inline int Sle_CutSetSizeSign( int s, int S ) { return (S << 28) | s; } +static inline int * Sle_CutLeaves( int * pCut ) { return pCut + 1; } + +static inline int Sle_CutIsUsed( int * pCut ) { return pCut[1] != 0; } +static inline void Sle_CutSetUnused( int * pCut ) { pCut[1] = 0; } + +#define Sle_ForEachCut( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += Sle_CutSize(pCut) + 1 ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Cut computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Sle_CutMergeOrder( int * pCut0, int * pCut1, int * pCut, int nLutSize ) +{ + int nSize0 = Sle_CutSize(pCut0); + int nSize1 = Sle_CutSize(pCut1); + int i, * pC0 = Sle_CutLeaves(pCut0); + int k, * pC1 = Sle_CutLeaves(pCut1); + int c, * pC = Sle_CutLeaves(pCut); + // the case of the largest cut sizes + if ( nSize0 == nLutSize && nSize1 == nLutSize ) + { + for ( i = 0; i < nSize0; i++ ) + { + if ( pC0[i] != pC1[i] ) return 0; + pC[i] = pC0[i]; + } + pCut[0] = Sle_CutSetSizeSign( nLutSize, Sle_CutSign(pCut0) | Sle_CutSign(pCut1) ); + return 1; + } + // compare two cuts with different numbers + i = k = c = 0; + if ( nSize0 == 0 ) goto FlushCut1; + if ( nSize1 == 0 ) goto FlushCut0; + while ( 1 ) + { + if ( c == nLutSize ) return 0; + if ( pC0[i] < pC1[k] ) + { + pC[c++] = pC0[i++]; + if ( i >= nSize0 ) goto FlushCut1; + } + else if ( pC0[i] > pC1[k] ) + { + pC[c++] = pC1[k++]; + if ( k >= nSize1 ) goto FlushCut0; + } + else + { + pC[c++] = pC0[i++]; k++; + if ( i >= nSize0 ) goto FlushCut1; + if ( k >= nSize1 ) goto FlushCut0; + } + } + +FlushCut0: + if ( c + nSize0 > nLutSize + i ) return 0; + while ( i < nSize0 ) + pC[c++] = pC0[i++]; + pCut[0] = Sle_CutSetSizeSign( c, Sle_CutSign(pCut0) | Sle_CutSign(pCut1) ); + return 1; + +FlushCut1: + if ( c + nSize1 > nLutSize + k ) return 0; + while ( k < nSize1 ) + pC[c++] = pC1[k++]; + pCut[0] = Sle_CutSetSizeSign( c, Sle_CutSign(pCut0) | Sle_CutSign(pCut1) ); + return 1; +} +static inline int Sle_SetCutIsContainedOrder( int * pBase, int * pCut ) // check if pCut is contained in pBase +{ + int i, nSizeB = Sle_CutSize(pBase); + int k, nSizeC = Sle_CutSize(pCut); + int * pLeaveB = Sle_CutLeaves(pBase); + int * pLeaveC = Sle_CutLeaves(pCut); + if ( nSizeB == nSizeC ) + { + for ( i = 0; i < nSizeB; i++ ) + if ( pLeaveB[i] != pLeaveC[i] ) + return 0; + return 1; + } + assert( nSizeB > nSizeC ); + if ( nSizeC == 0 ) + return 1; + for ( i = k = 0; i < nSizeB; i++ ) + { + if ( pLeaveB[i] > pLeaveC[k] ) + return 0; + if ( pLeaveB[i] == pLeaveC[k] ) + { + if ( ++k == nSizeC ) + return 1; + } + } + return 0; +} +static inline int Sle_CutCountBits( unsigned i ) +{ + i = i - ((i >> 1) & 0x55555555); + i = (i & 0x33333333) + ((i >> 2) & 0x33333333); + i = ((i + (i >> 4)) & 0x0F0F0F0F); + return (i*(0x01010101))>>24; +} +static inline int Sle_SetLastCutIsContained( Vec_Int_t * vTemp, int * pBase ) +{ + int i, * pCut, * pList = Vec_IntArray(vTemp); + Sle_ForEachCut( pList, pCut, i ) + if ( Sle_CutIsUsed(pCut) && Sle_CutSize(pCut) <= Sle_CutSize(pBase) && (Sle_CutSign(pCut) & Sle_CutSign(pBase)) == Sle_CutSign(pCut) && Sle_SetCutIsContainedOrder(pBase, pCut) ) + return 1; + return 0; +} +static inline void Sle_SetAddCut( Vec_Int_t * vTemp, int * pCut ) +{ + int i, * pBase, * pList = Vec_IntArray(vTemp); + Sle_ForEachCut( pList, pBase, i ) + if ( Sle_CutIsUsed(pBase) && Sle_CutSize(pCut) < Sle_CutSize(pBase) && (Sle_CutSign(pCut) & Sle_CutSign(pBase)) == Sle_CutSign(pCut) && Sle_SetCutIsContainedOrder(pBase, pCut) ) + Sle_CutSetUnused( pBase ); + Vec_IntPushArray( vTemp, pCut, Sle_CutSize(pCut)+1 ); + Vec_IntAddToEntry( vTemp, 0, 1 ); +} +int Sle_ManCutMerge( Gia_Man_t * p, int iObj, Vec_Int_t * vCuts, Vec_Int_t * vTemp, int nLutSize ) +{ + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + int * pList0 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId0(pObj, iObj)) ); + int * pList1 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId1(pObj, iObj)) ); + int * pCut0, * pCut1, i, k, Cut[8], nCuts = 0; + Vec_IntFill( vTemp, 1, 0 ); + Sle_ForEachCut( pList0, pCut0, i ) + Sle_ForEachCut( pList1, pCut1, k ) + { + if ( Sle_CutSize(pCut0) + Sle_CutSize(pCut1) > nLutSize && Sle_CutCountBits(Sle_CutSign(pCut0) | Sle_CutSign(pCut1)) > nLutSize ) + continue; + if ( !Sle_CutMergeOrder(pCut0, pCut1, Cut, nLutSize) ) + continue; + if ( Sle_SetLastCutIsContained(vTemp, Cut) ) + continue; + Sle_SetAddCut( vTemp, Cut ); + } + // reload + Vec_IntWriteEntry( vCuts, iObj, Vec_IntSize(vCuts) ); + Vec_IntPush( vCuts, -1 ); + pList0 = Vec_IntArray(vTemp); + Sle_ForEachCut( pList0, pCut0, i ) + { + if ( !Sle_CutIsUsed(pCut0) ) + continue; + Vec_IntPushArray( vCuts, pCut0, Sle_CutSize(pCut0)+1 ); + nCuts++; + } + Vec_IntPush( vCuts, Sle_CutSetSizeSign(1, iObj % 28) ); + Vec_IntPush( vCuts, iObj ); + Vec_IntWriteEntry( vCuts, Vec_IntEntry(vCuts, iObj), nCuts+1 ); + return nCuts; +} +Vec_Int_t * Sle_ManComputeCuts( Gia_Man_t * p, int nLutSize, int fVerbose ) +{ + int i, iObj, nCuts = 0; + Vec_Int_t * vTemp = Vec_IntAlloc( 1000 ); + Vec_Int_t * vCuts = Vec_IntAlloc( 30 * Gia_ManAndNum(p) ); + assert( nLutSize <= 6 ); + Vec_IntFill( vCuts, Gia_ManObjNum(p), 0 ); + Gia_ManForEachCiId( p, iObj, i ) + { + Vec_IntWriteEntry( vCuts, iObj, Vec_IntSize(vCuts) ); + Vec_IntPush( vCuts, 1 ); + Vec_IntPush( vCuts, Sle_CutSetSizeSign(1, iObj % 28) ); + Vec_IntPush( vCuts, iObj ); + } + Gia_ManForEachAndId( p, iObj ) + nCuts += Sle_ManCutMerge( p, iObj, vCuts, vTemp, nLutSize ); + if ( fVerbose ) + printf( "Nodes = %d. Cuts = %d. Cuts/Node = %.2f. Ints/Node = %.2f. Mem = %.2f MB.\n", + Gia_ManAndNum(p), nCuts, 1.0*nCuts/Gia_ManAndNum(p), + 1.0*(Vec_IntSize(vCuts)-Gia_ManObjNum(p))/Gia_ManAndNum(p), + 1.0*Vec_IntMemory(vCuts) / (1<<20) ); + Vec_IntFree( vTemp ); + return vCuts; +} +void Sle_ManPrintCut( int * pCut ) +{ + int nSize = Sle_CutSize(pCut); + int k, * pC = Sle_CutLeaves(pCut); + printf( "{" ); + for ( k = 0; k < nSize; k++ ) + printf( " %d", pC[k] ); + printf( " }\n" ); +} +void Sle_ManPrintCuts( Gia_Man_t * p, Vec_Int_t * vCuts, int iObj ) +{ + int i, * pCut; + int * pList = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, iObj) ); + printf( "Obj %3d\n", iObj ); + Sle_ForEachCut( pList, pCut, i ) + Sle_ManPrintCut( pCut ); + printf( "\n" ); +} +void Sle_ManPrintCutsAll( Gia_Man_t * p, Vec_Int_t * vCuts ) +{ + int iObj; + Gia_ManForEachAndId( p, iObj ) + Sle_ManPrintCuts( p, vCuts, iObj ); +} +void Sle_ManComputeCutsTest( Gia_Man_t * p ) +{ + Vec_Int_t * vCuts = Sle_ManComputeCuts( p, 4, 1 ); + //Sle_ManPrintCutsAll( p, vCuts ); + Vec_IntFree( vCuts ); +} + + + +/**Function************************************************************* + + Synopsis [Derive mask representing internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Bit_t * Sle_ManInternalNodeMask( Gia_Man_t * pGia ) +{ + int iObj; + Vec_Bit_t * vMask = Vec_BitStart( Gia_ManObjNum(pGia) ); + Gia_ManForEachAndId( pGia, iObj ) + Vec_BitWriteEntry( vMask, iObj, 1 ); + return vMask; +} + +/**Function************************************************************* + + Synopsis [Derive cut fanins of each node.] + + Description [These are nodes that are fanins of some cut of this node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sle_ManCollectCutFaninsOne( Gia_Man_t * pGia, int iObj, Vec_Int_t * vCuts, Vec_Bit_t * vMask, Vec_Int_t * vCutFanins, Vec_Bit_t * vMap ) +{ + int i, iFanin, * pCut, * pList = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, iObj) ); + Sle_ForEachCut( pList, pCut, i ) + { + int nSize = Sle_CutSize(pCut); + int k, * pC = Sle_CutLeaves(pCut); + if ( nSize < 2 ) + continue; + for ( k = 0; k < nSize; k++ ) + if ( Vec_BitEntry(vMask, pC[k]) && !Vec_BitEntry(vMap, pC[k]) ) + { + Vec_BitWriteEntry( vMap, pC[k], 1 ); + Vec_IntPush( vCutFanins, pC[k] ); + } + } + Vec_IntForEachEntry( vCutFanins, iFanin, i ) + Vec_BitWriteEntry( vMap, iFanin, 0 ); +} +Vec_Wec_t * Sle_ManCollectCutFanins( Gia_Man_t * pGia, Vec_Int_t * vCuts, Vec_Bit_t * vMask ) +{ + int iObj; + Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(pGia) ); + Vec_Wec_t * vCutFanins = Vec_WecStart( Gia_ManObjNum(pGia) ); + Gia_ManForEachAndId( pGia, iObj ) + Sle_ManCollectCutFaninsOne( pGia, iObj, vCuts, vMask, Vec_WecEntry(vCutFanins, iObj), vMap ); + Vec_BitFree( vMap ); + return vCutFanins; +} + + +typedef struct Sle_Man_t_ Sle_Man_t; +struct Sle_Man_t_ +{ + // user's data + Gia_Man_t * pGia; // user's manager (with mapping and edges) + int nLevels; // total number of levels + int fVerbose; // verbose flag + // SAT variables + int nNodeVars; // node variables (Gia_ManAndNum(pGia)) + int nCutVars; // cut variables (total number of non-trivial cuts) + int nEdgeVars; // edge variables (total number of internal edges) + int nDelayVars; // delay variables (nNodeVars * nLevelsMax) + int nVarsTotal; // total number of variables + // SAT clauses + int nCutClas; // cut clauses + int nEdgeClas; // edge clauses + int nEdgeClas2; // edge clauses exclusivity + int nDelayClas; // delay clauses + // internal data + sat_solver * pSat; // SAT solver + Vec_Bit_t * vMask; // internal node mask + Vec_Int_t * vCuts; // cuts for each node + Vec_Wec_t * vCutFanins; // internal cut fanins of each node + Vec_Wec_t * vFanoutEdges; // internal cut fanins of each node + Vec_Wec_t * vEdgeCuts; // cuts of each edge for one node + Vec_Int_t * vObjMap; // temporary object map + Vec_Int_t * vCutFirst; // first cut of each node + Vec_Int_t * vEdgeFirst; // first edge of each node + Vec_Int_t * vDelayFirst; // first edge of each node + Vec_Int_t * vPolars; // initial + Vec_Int_t * vLits; // literals + // statistics + abctime timeStart; +}; + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Sle_Man_t * Sle_ManAlloc( Gia_Man_t * pGia, int nLevels, int fVerbose ) +{ + Sle_Man_t * p = ABC_CALLOC( Sle_Man_t, 1 ); + p->pGia = pGia; + p->nLevels = nLevels; + p->fVerbose = fVerbose; + p->vMask = Sle_ManInternalNodeMask( pGia ); + p->vCuts = Sle_ManComputeCuts( pGia, 4, fVerbose ); + p->vCutFanins = Sle_ManCollectCutFanins( pGia, p->vCuts, p->vMask ); + p->vFanoutEdges = Vec_WecStart( Gia_ManObjNum(pGia) ); + p->vEdgeCuts = Vec_WecAlloc( 100 ); + p->vObjMap = Vec_IntStartFull( Gia_ManObjNum(pGia) ); + p->vCutFirst = Vec_IntStartFull( Gia_ManObjNum(pGia) ); + p->vEdgeFirst = Vec_IntStartFull( Gia_ManObjNum(pGia) ); + p->vDelayFirst = Vec_IntStartFull( Gia_ManObjNum(pGia) ); + p->vPolars = Vec_IntAlloc( 100 ); + p->vLits = Vec_IntAlloc( 100 ); + return p; +} +void Sle_ManStop( Sle_Man_t * p ) +{ + sat_solver_delete( p->pSat ); + Vec_BitFree( p->vMask ); + Vec_IntFree( p->vCuts ); + Vec_WecFree( p->vCutFanins ); + Vec_WecFree( p->vFanoutEdges ); + Vec_WecFree( p->vEdgeCuts ); + Vec_IntFree( p->vObjMap ); + Vec_IntFree( p->vCutFirst ); + Vec_IntFree( p->vEdgeFirst ); + Vec_IntFree( p->vDelayFirst ); + Vec_IntFree( p->vPolars ); + Vec_IntFree( p->vLits ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sle_ManMarkupVariables( Sle_Man_t * p ) +{ + int iObj, Counter = Gia_ManObjNum(p->pGia); + // node variables + p->nNodeVars = Counter; + // cut variables + Gia_ManForEachAndId( p->pGia, iObj ) + { + int * pList = Vec_IntEntryP( p->vCuts, Vec_IntEntry(p->vCuts, iObj) ); + Vec_IntWriteEntry( p->vCutFirst, iObj, Counter ); + Counter += pList[0] - 1; + } + p->nCutVars = Counter - p->nNodeVars; + // edge variables + Gia_ManForEachAndId( p->pGia, iObj ) + { + Vec_IntWriteEntry( p->vEdgeFirst, iObj, Counter ); + Counter += Vec_IntSize( Vec_WecEntry(p->vCutFanins, iObj) ); + } + p->nEdgeVars = Counter - p->nCutVars - p->nNodeVars; + // delay variables + Gia_ManForEachAndId( p->pGia, iObj ) + { + Vec_IntWriteEntry( p->vDelayFirst, iObj, Counter ); + Counter += p->nLevels; + } + p->nDelayVars = Counter - p->nEdgeVars - p->nCutVars - p->nNodeVars; + p->nVarsTotal = Counter; + printf( "Vars: Total = %d. Node = %d. Cut = %d. Edge = %d. Delay = %d.\n", + p->nVarsTotal, p->nNodeVars, p->nCutVars, p->nEdgeVars, p->nDelayVars ); +} + + +/**Function************************************************************* + + Synopsis [Derive initial variable assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sle_ManDeriveInit( Sle_Man_t * p ) +{ + Vec_Int_t * vEdges; + int pFaninsCopy[16]; + int i, iObj, iFanin, iEdge; + if ( !Gia_ManHasMapping(p->pGia) ) + return; + // derive initial state + Vec_IntClear( p->vPolars ); + Gia_ManForEachAndId( p->pGia, iObj ) + { + int nFanins, * pFanins, * pCut, * pList, iFound = -1; + if ( !Gia_ObjIsLut(p->pGia, iObj) ) + continue; + Vec_IntPush( p->vPolars, iObj ); // node var + nFanins = Gia_ObjLutSize( p->pGia, iObj ); + pFanins = Gia_ObjLutFanins( p->pGia, iObj ); + // duplicate and sort fanins + memcpy( pFaninsCopy, pFanins, sizeof(int)*nFanins ); + Vec_IntSelectSort( pFaninsCopy, nFanins ); + // find cut + pList = Vec_IntEntryP( p->vCuts, Vec_IntEntry(p->vCuts, iObj) ); + Sle_ForEachCut( pList, pCut, i ) + if ( i < pList[0]-1 && nFanins == Sle_CutSize(pCut) && !memcmp(pFaninsCopy, Sle_CutLeaves(pCut), sizeof(int)*Sle_CutSize(pCut)) ) + { + iFound = i; + break; + } + if ( iFound == -1 ) + { + printf( "Cannot find the following cut at node %d: {", iObj ); + for ( i = 0; i < nFanins; i++ ) + printf( " %d", pFaninsCopy[i] ); + printf( " }\n" ); + Sle_ManPrintCuts( p->pGia, p->vCuts, iObj ); + fflush( stdout ); + } + assert( iFound >= 0 ); + Vec_IntPush( p->vPolars, Vec_IntEntry(p->vCutFirst, iObj) + iFound ); // cut var + // check if the cut contains only primary inputs + iFound = 0; + for ( i = 0; i < nFanins; i++ ) + if ( Vec_BitEntry(p->vMask, pFanins[i]) ) // internal node + iFound = 1; + if ( !iFound ) // did not find + Vec_IntPush( p->vPolars, Vec_IntEntry(p->vDelayFirst, iObj) ); // delay var + } + // find zero-delay edges + if ( !p->pGia->vEdge1 ) + return; + vEdges = Gia_ManEdgeToArray( p->pGia ); + Vec_IntForEachEntryDouble( vEdges, iFanin, iObj, i ) + { + assert( iFanin < iObj ); + assert( Gia_ObjIsLut(p->pGia, iFanin) ); + assert( Gia_ObjIsLut(p->pGia, iObj) ); + assert( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanin)) ); + assert( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iObj)) ); + // find edge + iEdge = Vec_IntFind( Vec_WecEntry(p->vCutFanins, iObj), iFanin ); + assert( iEdge >= 0 ); + Vec_IntPush( p->vPolars, Vec_IntEntry(p->vEdgeFirst, iObj) + iEdge ); // edge + } + Vec_IntFree( vEdges ); +} + +/**Function************************************************************* + + Synopsis [Derive CNF.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sle_ManDeriveCnf( Sle_Man_t * p ) +{ + int nBTLimit = 0; + int nTimeOut = 0; + int i, iObj, value; + Vec_Int_t * vArray; + + // start the SAT solver + p->pSat = sat_solver_new(); + sat_solver_setnvars( p->pSat, p->nVarsTotal ); + sat_solver_set_resource_limits( p->pSat, nBTLimit, 0, 0, 0 ); + sat_solver_set_runtime_limit( p->pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 ); + sat_solver_set_random( p->pSat, 1 ); + sat_solver_set_polarity( p->pSat, Vec_IntArray(p->vPolars), Vec_IntSize(p->vPolars) ); + sat_solver_set_var_activity( p->pSat, NULL, p->nVarsTotal ); + + // set drivers to be mapped + Gia_ManForEachCoDriverId( p->pGia, iObj, i ) + { + Vec_IntFill( p->vLits, 1, Abc_Var2Lit(iObj, 0) ); // pos lit + value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) ); + assert( value ); + } + + // add cover clauses and edge-to-cut clauses + Gia_ManForEachAndId( p->pGia, iObj ) + { + int e, iEdge, nEdges = 0, Entry; + int iCutVar0 = Vec_IntEntry( p->vCutFirst, iObj ); + int iEdgeVar0 = Vec_IntEntry( p->vEdgeFirst, iObj ); + int * pCut, * pList = Vec_IntEntryP( p->vCuts, Vec_IntEntry(p->vCuts, iObj) ); + Vec_Int_t * vCutFans = Vec_WecEntry( p->vCutFanins, iObj ); + assert( iCutVar0 > 0 && iEdgeVar0 > 0 ); + // node requires one of the cuts + Vec_IntFill( p->vLits, 1, Abc_Var2Lit(iObj, 1) ); // neg lit + for ( i = 0; i < pList[0]-1; i++ ) + Vec_IntPush( p->vLits, Abc_Var2Lit(iCutVar0 + i, 0) ); + value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) ); + assert( value ); + // cut required fanin nodes + Vec_WecInit( p->vEdgeCuts, Vec_IntSize(vCutFans) ); + Sle_ForEachCut( pList, pCut, i ) + { + int nSize = Sle_CutSize(pCut); + int k, * pC = Sle_CutLeaves(pCut); + if ( nSize < 2 ) + continue; + for ( k = 0; k < nSize; k++ ) + { + if ( !Vec_BitEntry(p->vMask, pC[k]) ) + continue; + Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(iCutVar0 + i, 1), Abc_Var2Lit(pC[k], 0) ); + value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) ); + assert( value ); + // find the edge ID between pC[k] and iObj + iEdge = Vec_IntEntry(p->vObjMap, pC[k]); + if ( iEdge == -1 ) + Vec_IntWriteEntry( p->vObjMap, pC[k], (iEdge = nEdges++) ); + Vec_WecPush( p->vEdgeCuts, iEdge, iCutVar0 + i ); + Vec_WecPush( p->vFanoutEdges, pC[k], iEdgeVar0 + iEdge ); + p->nCutClas++; + } + } + assert( nEdges == Vec_IntSize(vCutFans) ); + // edge requires one of the fanout cuts + Vec_WecForEachLevel( p->vEdgeCuts, vArray, e ) + { + assert( Vec_IntSize(vArray) > 0 ); + Vec_IntFill( p->vLits, 1, Abc_Var2Lit(iEdgeVar0 + e, 1) ); // neg lit (edge) + Vec_IntForEachEntry( vArray, Entry, i ) + Vec_IntPush( p->vLits, Abc_Var2Lit(Entry, 0) ); // pos lit (cut) + value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) ); + assert( value ); + p->nEdgeClas++; + } + // clean object map + Vec_IntForEachEntry( vCutFans, Entry, i ) + Vec_IntWriteEntry( p->vObjMap, Entry, -1 ); + } + + // mutual exclusivity of edges + Vec_WecForEachLevel( p->vFanoutEdges, vArray, iObj ) + { + int j, k, EdgeJ, EdgeK; + int iEdgeVar0 = Vec_IntEntry( p->vEdgeFirst, iObj ); + Vec_Int_t * vCutFans = Vec_WecEntry( p->vCutFanins, iObj ); + // add fanin edges + for ( i = 0; i < Vec_IntSize(vCutFans); i++ ) + Vec_IntPush( vArray, iEdgeVar0 + i ); + // generate pairs + Vec_IntForEachEntry( vArray, EdgeJ, j ) + Vec_IntForEachEntryStart( vArray, EdgeK, k, j+1 ) + { + Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(EdgeJ, 1), Abc_Var2Lit(EdgeK, 1) ); + value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) ); + assert( value ); + } + p->nEdgeClas2 += Vec_IntSize(vArray) * (Vec_IntSize(vArray) - 1) / 2; + } + + // add delay clauses + Gia_ManForEachAndId( p->pGia, iObj ) + { + int e, iFanin; + int iEdgeVar0 = Vec_IntEntry( p->vEdgeFirst, iObj ); + int iDelayVar0 = Vec_IntEntry( p->vDelayFirst, iObj ); + Vec_Int_t * vCutFans = Vec_WecEntry( p->vCutFanins, iObj ); + // check if the node has cuts containing only primary inputs + int * pCut, * pList = Vec_IntEntryP( p->vCuts, Vec_IntEntry(p->vCuts, iObj) ); + Sle_ForEachCut( pList, pCut, i ) + { + int nSize = Sle_CutSize(pCut); + int k, * pC = Sle_CutLeaves(pCut); + int fFound = 0; + for ( k = 0; k < nSize; k++ ) + if ( Vec_BitEntry(p->vMask, pC[k]) ) // internal node + fFound = 1; + if ( fFound ) // found internal node + continue; + Vec_IntFill( p->vLits, 1, Abc_Var2Lit(iDelayVar0, 0) ); // pos lit + value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) ); + assert( value ); + //printf( "Setting unit delay for node %d (var %d).\n", iObj, iDelayVar0 ); + break; + } + if ( i < pList[0] - 1 ) + continue; + // create delay requirements for each cut fanin of this node + Vec_IntForEachEntry( vCutFans, iFanin, e ) + { + int d, iDelayVarIn = Vec_IntEntry( p->vDelayFirst, iFanin ); + for ( d = 0; d < p->nLevels-1; d++ ) + { + Vec_IntClear( p->vLits ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iObj, 1) ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVarIn + d, 1) ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iEdgeVar0 + e, 0) ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVar0 + d+1, 0) ); + value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) ); + assert( value ); + + Vec_IntClear( p->vLits ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iObj, 1) ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVarIn + d, 1) ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iEdgeVar0 + e, 1) ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVar0 + d, 0) ); + value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) ); + assert( value ); + } + + Vec_IntClear( p->vLits ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iObj, 1) ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVarIn + d, 1) ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iEdgeVar0 + e, 0) ); + value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) ); + assert( value ); + + Vec_IntClear( p->vLits ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iObj, 1) ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVarIn + d, 1) ); + Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVar0 + d, 0) ); + value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) ); + assert( value ); + + p->nDelayClas += 2*p->nLevels; + } + } + printf( "Clas: Total = %d. Cut = %d. Edge = %d. EdgeEx = %d. Delay = %d.\n", + sat_solver_nclauses(p->pSat), p->nCutClas, p->nEdgeClas, p->nEdgeClas2, p->nDelayClas ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sle_ManDeriveResult( Sle_Man_t * p, Vec_Int_t * vEdge2, Vec_Int_t * vMapping ) +{ + int iObj; + // create mapping + Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 ); + Gia_ManForEachAndId( p->pGia, iObj ) + { + int i, iCut, iCutVar0 = Vec_IntEntry( p->vCutFirst, iObj ); + int * pCut, * pList = Vec_IntEntryP( p->vCuts, Vec_IntEntry(p->vCuts, iObj) ); + if ( !sat_solver_var_value(p->pSat, iObj) ) + continue; + Sle_ForEachCut( pList, pCut, iCut ) + if ( sat_solver_var_value(p->pSat, iCutVar0 + iCut) ) + break; + assert( iCut < pList[0] - 1 ); + Vec_IntWriteEntry( vMapping, iObj, Vec_IntSize(vMapping) ); + Vec_IntPush( vMapping, Sle_CutSize(pCut) ); + for ( i = 0; i < Sle_CutSize(pCut); i++ ) + Vec_IntPush( vMapping, Sle_CutLeaves(pCut)[i] ); + Vec_IntPush( vMapping, iObj ); + } + // collect edges + Vec_IntClear( vEdge2 ); + Gia_ManForEachAndId( p->pGia, iObj ) + { + int i, iFanin, iEdgeVar0 = Vec_IntEntry( p->vEdgeFirst, iObj ); + Vec_Int_t * vCutFans = Vec_WecEntry( p->vCutFanins, iObj ); + if ( !sat_solver_var_value(p->pSat, iObj) ) + continue; + Vec_IntForEachEntry( vCutFans, iFanin, i ) + if ( sat_solver_var_value(p->pSat, iEdgeVar0 + i) ) + Vec_IntPushTwo( vEdge2, iFanin, iObj ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Sle_ManExplore( Gia_Man_t * pGia, int DelayInit, int fVerbose ) +{ + int fVeryVerbose = 0; + abctime clk = Abc_Clock(); + Vec_Int_t * vEdges2 = Vec_IntAlloc(1000); + Vec_Int_t * vMapping = Vec_IntAlloc(1000); + int i, iLut, nConfs, status, Delay, iFirstVar; + int DelayStart = DelayInit ? DelayInit : Gia_ManLutLevel(pGia, NULL); + Sle_Man_t * p = Sle_ManAlloc( pGia, DelayStart, fVerbose ); + Sle_ManMarkupVariables( p ); + Sle_ManDeriveInit( p ); + Sle_ManDeriveCnf( p ); + for ( Delay = DelayStart; Delay >= 0; Delay-- ) + { + // we constrain COs, although it would be fine to constrain only POs + if ( Delay < DelayStart ) + { + Gia_ManForEachCoDriverId( p->pGia, iLut, i ) + { + iFirstVar = Vec_IntEntry( p->vDelayFirst, iLut ); + if ( !sat_solver_push(p->pSat, Abc_Var2Lit(iFirstVar + Delay, 1)) ) + break; + } + if ( i < Gia_ManCoNum(p->pGia) ) + { + printf( "Proved UNSAT for delay %d. ", Delay ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + break; + } + } + // solve with assumptions + //clk = Abc_Clock(); + nConfs = sat_solver_nconflicts( p->pSat ); + status = sat_solver_solve_internal( p->pSat ); + nConfs = sat_solver_nconflicts( p->pSat ) - nConfs; + if ( status == l_True ) + { + if ( fVerbose ) + { + int nNodes = 0, nEdges = 0; + for ( i = 0; i < p->nNodeVars; i++ ) + nNodes += sat_solver_var_value(p->pSat, i); + for ( i = 0; i < p->nEdgeVars; i++ ) + nEdges += sat_solver_var_value(p->pSat, p->nNodeVars + p->nCutVars + i); + printf( "Solution with delay %2d, node count %5d, and edge count %5d exists. Conf = %8d. ", Delay, nNodes, nEdges, nConfs ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + // save the result + Sle_ManDeriveResult( p, vEdges2, vMapping ); + if ( fVeryVerbose ) + { + printf( "Nodes: " ); + for ( i = 0; i < p->nNodeVars; i++ ) + if ( sat_solver_var_value(p->pSat, i) ) + printf( "%d ", i ); + printf( "\n" ); + printf( "\n" ); + + Vec_IntPrint( p->vCutFirst ); + printf( "Cuts: " ); + for ( i = 0; i < p->nCutVars; i++ ) + if ( sat_solver_var_value(p->pSat, p->nNodeVars + i) ) + printf( "%d ", p->nNodeVars + i ); + printf( "\n" ); + printf( "\n" ); + + Vec_IntPrint( p->vEdgeFirst ); + printf( "Edges: " ); + for ( i = 0; i < p->nEdgeVars; i++ ) + if ( sat_solver_var_value(p->pSat, p->nNodeVars + p->nCutVars + i) ) + printf( "%d ", p->nNodeVars + p->nCutVars + i ); + printf( "\n" ); + printf( "\n" ); + + Vec_IntPrint( p->vDelayFirst ); + printf( "Delays: " ); + for ( i = 0; i < p->nDelayVars; i++ ) + if ( sat_solver_var_value(p->pSat, p->nNodeVars + p->nCutVars + p->nEdgeVars + i) ) + printf( "%d ", p->nNodeVars + p->nCutVars + p->nEdgeVars + i ); + printf( "\n" ); + printf( "\n" ); + } + } + else + { + if ( fVerbose ) + { + if ( status == l_False ) + printf( "Proved UNSAT for delay %d. ", Delay ); + else + printf( "Resource limit reached for delay %d. ", Delay ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + } + break; + } + } + if ( Vec_IntSize(vMapping) > 0 ) + { + Gia_ManEdgeFromArray( p->pGia, vEdges2 ); + Vec_IntFree( vEdges2 ); + Vec_IntFreeP( &p->pGia->vMapping ); + p->pGia->vMapping = vMapping; + } + else + { + Vec_IntFree( vEdges2 ); + Vec_IntFree( vMapping ); + } + Sle_ManStop( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 273597a4..0066bfd2 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -56,6 +56,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaRetime.c \ src/aig/gia/giaRex.c \ src/aig/gia/giaSatEdge.c \ + src/aig/gia/giaSatLE.c \ src/aig/gia/giaSatLut.c \ src/aig/gia/giaSatMap.c \ src/aig/gia/giaScl.c \ |