luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Experiment with CNF cofactoring.

This commit is contained in:
Alan Mishchenko 2023-07-24 16:21:42 -07:00
parent 19eaa55c2a
commit d9f6af51af
3 changed files with 63 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/sat/cnf/cnf.h
View File

@ -154,6 +154,7 @@ extern void Cnf_ManStop( Cnf_Man_t * p );
extern Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
extern Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals );
extern Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p );
extern Cnf_Dat_t * Cnf_DataDupCof( Cnf_Dat_t * p, int Lit );
extern void Cnf_DataFree( Cnf_Dat_t * p );
extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
extern void Cnf_DataCollectFlipLits( Cnf_Dat_t * p, int iFlipVar, Vec_Int_t * vFlips );

32
src/sat/cnf/cnfMan.c
View File

@ -103,10 +103,8 @@ void Cnf_ManStop( Cnf_Man_t * p )
***********************************************************************/
Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
{
Vec_Int_t * vCiIds;
Aig_Obj_t * pObj;
int i;
vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
Aig_Obj_t * pObj; int i;
Vec_Int_t * vCiIds = Vec_IntAlloc( Aig_ManCiNum(p) );
Aig_ManForEachCi( p, pObj, i )
Vec_IntPush( vCiIds, pCnf->pVarNums[pObj->Id] );
return vCiIds;
@ -126,9 +124,7 @@ Vec_Int_t * Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p )
Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiterals )
{
Cnf_Dat_t * pCnf;
int i;
pCnf = ABC_ALLOC( Cnf_Dat_t, 1 );
memset( pCnf, 0, sizeof(Cnf_Dat_t) );
pCnf = ABC_CALLOC( Cnf_Dat_t, 1 );
pCnf->pMan = pAig;
pCnf->nVars = nVars;
pCnf->nClauses = nClauses;
@ -136,10 +132,8 @@ Cnf_Dat_t * Cnf_DataAlloc( Aig_Man_t * pAig, int nVars, int nClauses, int nLiter
pCnf->pClauses = ABC_ALLOC( int *, nClauses + 1 );
pCnf->pClauses[0] = ABC_ALLOC( int, nLiterals );
pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals;
pCnf->pVarNums = ABC_ALLOC( int, Aig_ManObjNumMax(pAig) );
// memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(pAig) );
for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
pCnf->pVarNums[i] = -1;
if ( pCnf->pVarNums )
pCnf->pVarNums = ABC_FALLOC( int, Aig_ManObjNumMax(pAig) );
return pCnf;
}
@ -160,11 +154,27 @@ Cnf_Dat_t * Cnf_DataDup( Cnf_Dat_t * p )
int i;
pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses, p->nLiterals );
memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
if ( p->pVarNums )
memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
for ( i = 1; i < p->nClauses; i++ )
pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
return pCnf;
}
Cnf_Dat_t * Cnf_DataDupCof( Cnf_Dat_t * p, int Lit )
{
Cnf_Dat_t * pCnf;
int i;
pCnf = Cnf_DataAlloc( p->pMan, p->nVars, p->nClauses+1, p->nLiterals+1 );
memcpy( pCnf->pClauses[0], p->pClauses[0], sizeof(int) * p->nLiterals );
if ( pCnf->pVarNums )
memcpy( pCnf->pVarNums, p->pVarNums, sizeof(int) * Aig_ManObjNumMax(p->pMan) );
for ( i = 1; i < p->nClauses; i++ )
pCnf->pClauses[i] = pCnf->pClauses[0] + (p->pClauses[i] - p->pClauses[0]);
pCnf->pClauses[p->nClauses] = pCnf->pClauses[0] + p->nLiterals;
pCnf->pClauses[p->nClauses][0] = Lit;
assert( pCnf->pClauses[p->nClauses+1] == pCnf->pClauses[0] + p->nLiterals+1 );
return pCnf;
}
/**Function*************************************************************

41
src/sat/cnf/cnfUtil.c
View File

@ -469,6 +469,47 @@ int Cnf_DataSolveFromFile( char * pFileName, int nConfLimit, int nLearnedStart,
return RetValue;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Cnf_DataBestVar( Cnf_Dat_t * p, int * pSkip )
{
int * pNums = ABC_CALLOC( int, p->nVars );
int i, * pLit, NumMax = -1, iVarMax = -1;
for ( i = 0; i < p->nClauses; i++ )
for ( pLit = p->pClauses[i]; pLit < p->pClauses[i+1]; pLit++ )
pNums[Abc_Lit2Var(*pLit)]++;
for ( i = 0; i < p->nVars; i++ )
if ( (!pSkip || !pSkip[i]) && NumMax < pNums[i] )
NumMax = pNums[i], iVarMax = i;
ABC_FREE( pNums );
return iVarMax;
}
void Cnf_Experiment1()
{
Cnf_Dat_t * pTemp, * p = Cnf_DataReadFromFile( "../166b.cnf" ); int i;
int * pSkip = ABC_CALLOC( int, p->nVars );
for ( i = 0; i < 100; i++ )
{
int iVar = Cnf_DataBestVar( p, pSkip );
char FileName[100]; sprintf( FileName, "cnf/%03d.cnf", i );
Cnf_DataWriteIntoFile( p, FileName, 0, NULL, NULL );
printf( "Dumped file \"%s\".\n", FileName );
p = Cnf_DataDupCof( pTemp = p, Abc_Var2Lit(iVar, 0) );
Cnf_DataFree( pTemp );
pSkip[iVar] = 1;
}
Cnf_DataFree( p );
ABC_FREE( pSkip );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///