diff --git a/src/sat/cnf/cnfFast.c b/src/sat/cnf/cnfFast.c index cfcb9e2d0..19bb842ea 100644 --- a/src/sat/cnf/cnfFast.c +++ b/src/sat/cnf/cnfFast.c @@ -202,6 +202,81 @@ static inline int Cnf_ObjGetLit( Vec_Int_t * vMap, Aig_Obj_t * pObj, int fCompl return iSatVar + iSatVar + fCompl; } +/**Function************************************************************* + + Synopsis [Remembers the ISOP cover of each distinct cut function.] + + Description [The cover computed by Kit_TruthIsop() depends on nothing but + the truth table and the number of leaves, while a cut function repeats + across the AIG as often as the gate it came from: a bit-blasted circuit is + a few adder, mux and xor functions used millions of times over. Cutting + the ISOP for a function that has already been covered saves recomputing it + and, since the cover is replayed cube for cube, leaves the CNF unchanged. + Same idea as Mf_ManDeriveCnfs(), which keys off the truth table id the + mapper already assigns.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +typedef struct Cnf_IsopCache_t_ Cnf_IsopCache_t; +struct Cnf_IsopCache_t_ +{ + Vec_Mem_t * vFuncs; // the (truth table, leaf count) keys seen so far + Vec_Int_t * vCovers; // key id -> where its cover sits in vCubes + Vec_Int_t * vCubes; // per key: the cube count, then the cubes +}; + +static Cnf_IsopCache_t * Cnf_IsopCacheStart() +{ + Cnf_IsopCache_t * p = ABC_CALLOC( Cnf_IsopCache_t, 1 ); + p->vFuncs = Vec_MemAlloc( 2, 8 ); + Vec_MemHashAlloc( p->vFuncs, 1 << 10 ); + p->vCovers = Vec_IntAlloc( 1 << 10 ); + p->vCubes = Vec_IntAlloc( 1 << 12 ); + return p; +} + +static void Cnf_IsopCacheStop( Cnf_IsopCache_t * p ) +{ + Vec_MemHashFree( p->vFuncs ); + Vec_MemFree( p->vFuncs ); + Vec_IntFree( p->vCovers ); + Vec_IntFree( p->vCubes ); + ABC_FREE( p ); +} + +// Returns the cover of Truth as *pnCubes cubes. A NULL cache computes every +// time, for the callers that derive clauses for one cone at a time. +static int * Cnf_IsopCacheCover( Cnf_IsopCache_t * p, word Truth, int nLeaves, Vec_Int_t * vCover, int * pnCubes ) +{ + word Key[2]; + int c, Cube, iFunc, iCover, RetValue; + if ( p == NULL ) + { + RetValue = Kit_TruthIsop( (unsigned *)&Truth, nLeaves, vCover, 0 ); + assert( RetValue >= 0 ); + *pnCubes = Vec_IntSize( vCover ); + return Vec_IntArray( vCover ); + } + Key[0] = Truth; + Key[1] = (word)nLeaves; + iFunc = Vec_MemHashInsert( p->vFuncs, Key ); + if ( iFunc == Vec_IntSize(p->vCovers) ) + { + RetValue = Kit_TruthIsop( (unsigned *)&Truth, nLeaves, vCover, 0 ); + assert( RetValue >= 0 ); + Vec_IntPush( p->vCovers, Vec_IntSize(p->vCubes) ); + Vec_IntPush( p->vCubes, Vec_IntSize(vCover) ); + Vec_IntForEachEntry( vCover, Cube, c ) + Vec_IntPush( p->vCubes, Cube ); + } + iCover = Vec_IntEntry( p->vCovers, iFunc ); + *pnCubes = Vec_IntEntry( p->vCubes, iCover ); + return Vec_IntArray( p->vCubes ) + iCover + 1; +} + /**Function************************************************************* Synopsis [Collects nodes inside the cone.] @@ -213,11 +288,12 @@ static inline int Cnf_ObjGetLit( Vec_Int_t * vMap, Aig_Obj_t * pObj, int fCompl SeeAlso [] ***********************************************************************/ -void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, - Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses ) +static void Cnf_ComputeClausesInt( Aig_Man_t * p, Aig_Obj_t * pRoot, + Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses, + Cnf_IsopCache_t * pCache ) { Aig_Obj_t * pLeaf; - int c, k, Cube, OutLit, RetValue; + int c, k, Cube, OutLit, nCubes, * pCubes; word Truth; assert( pRoot->fMarkA ); @@ -265,11 +341,10 @@ void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, return; } - RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 ); - assert( RetValue >= 0 ); - - Vec_IntForEachEntry( vCover, Cube, c ) + pCubes = Cnf_IsopCacheCover( pCache, Truth, Vec_PtrSize(vLeaves), vCover, &nCubes ); + for ( c = 0; c < nCubes; c++ ) { + Cube = pCubes[c]; Vec_IntPush( vClauses, 0 ); Vec_IntPush( vClauses, OutLit ); for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 ) @@ -281,12 +356,10 @@ void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, } } - Truth = ~Truth; - - RetValue = Kit_TruthIsop( (unsigned *)&Truth, Vec_PtrSize(vLeaves), vCover, 0 ); - assert( RetValue >= 0 ); - Vec_IntForEachEntry( vCover, Cube, c ) + pCubes = Cnf_IsopCacheCover( pCache, ~Truth, Vec_PtrSize(vLeaves), vCover, &nCubes ); + for ( c = 0; c < nCubes; c++ ) { + Cube = pCubes[c]; Vec_IntPush( vClauses, 0 ); Vec_IntPush( vClauses, OutLit ^ 1 ); for ( k = 0; k < Vec_PtrSize(vLeaves); k++, Cube >>= 2 ) @@ -299,6 +372,12 @@ void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, } } +void Cnf_ComputeClauses( Aig_Man_t * p, Aig_Obj_t * pRoot, + Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes, Vec_Int_t * vMap, Vec_Int_t * vCover, Vec_Int_t * vClauses ) +{ + Cnf_ComputeClausesInt( p, pRoot, vLeaves, vNodes, vMap, vCover, vClauses, NULL ); +} + /**Function************************************************************* @@ -566,6 +645,7 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) Vec_Int_t * vLits, * vClas, * vMap, * vTemp; Vec_Ptr_t * vLeaves, * vNodes; Vec_Int_t * vCover; + Cnf_IsopCache_t * pCache; Aig_Obj_t * pObj; int i, k, nVars, Entry, OutLit, DriLit; @@ -604,11 +684,12 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) vNodes = Vec_PtrAlloc( 100 ); vCover = Vec_IntAlloc( 1 << 16 ); vTemp = Vec_IntAlloc( 100 ); + pCache = Cnf_IsopCacheStart(); Aig_ManForEachNodeReverse( p, pObj, i ) { if ( !pObj->fMarkA ) continue; - Cnf_ComputeClauses( p, pObj, vLeaves, vNodes, vMap, vCover, vTemp ); + Cnf_ComputeClausesInt( p, pObj, vLeaves, vNodes, vMap, vCover, vTemp, pCache ); Vec_IntForEachEntry( vTemp, Entry, k ) { if ( Entry == 0 ) @@ -617,6 +698,7 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) Vec_IntPush( vLits, Entry ); } } + Cnf_IsopCacheStop( pCache ); Vec_PtrFree( vLeaves ); Vec_PtrFree( vNodes ); Vec_IntFree( vCover );