Skip to content

cnf: cache the ISOP cover of each distinct cut function #10

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
TrevorHansen wants to merge 1 commit into
base: stp
Choose a base branch
from
Open

cnf: cache the ISOP cover of each distinct cut function #10

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
108 changes: 95 additions & 13 deletions src/sat/cnf/cnfFast.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.]
Expand All @@ -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 );

Expand Down Expand Up @@ -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 )
Expand All @@ -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 )
Expand All @@ -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*************************************************************
Expand Down Expand Up @@ -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;

Expand Down Expand Up @@ -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 )
Expand All @@ -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 );
Expand Down
Loading