Skip to content

Commit

Permalink
Adding an option to dump satisfying assignments into a BLIF file.
Browse files Browse the repository at this point in the history
  • Loading branch information
@alanminko
alanminko committed Aug 14, 2024
1 parent c099e62 commit 2055b1b
Show file tree
Hide file tree
Showing 3 changed files with 80 additions and 13 deletions.
14 changes: 7 additions & 7 deletions src/aig/gia/giaClp.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ extern int Gia_ManFactorNode( Gia_Man_t * p, char * pSop, Vec_Int_t * vLeaves );
SeeAlso []
***********************************************************************/
Vec_Ptr_t * Gia_GetFakeNames( int nNames )
Vec_Ptr_t * Gia_GetFakeNames( int nNames, int fCaps )
{
Vec_Ptr_t * vNames;
char Buffer[5];
Expand All @@ -64,12 +64,12 @@ Vec_Ptr_t * Gia_GetFakeNames( int nNames )
{
if ( nNames < 26 )
{
Buffer[0] = 'a' + i;
Buffer[0] = (fCaps ? 'A' : 'a') + i;
Buffer[1] = 0;
}
else
{
Buffer[0] = 'a' + i%26;
Buffer[0] = (fCaps ? 'A' : 'a') + i%26;
Buffer[1] = '0' + i/26;
Buffer[2] = 0;
}
Expand Down Expand Up @@ -378,8 +378,8 @@ Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
if ( fVerbose )
{
Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) );
Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p), 0 );
Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p), 1 );
char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, 0 );
Expand Down Expand Up @@ -464,8 +464,8 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )

if ( fVerbose )
{
Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) );
Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p), 0 );
Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p), 1 );
char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, OffSet );
Expand Down
66 changes: 64 additions & 2 deletions src/aig/gia/giaPat2.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1372,6 +1372,65 @@ void Min_ManTest2( Gia_Man_t * p )
SeeAlso []
***********************************************************************/
void Gia_GenerateCexesDumpBlif( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCexes )
{
extern Vec_Ptr_t * Gia_GetFakeNames( int nNames, int fCaps );
FILE * pFile = fopen( pFileName, "wb" );
if ( pFile == NULL ) {
printf( "Cannot open output file name \"%s\".\n", pFileName );
return;
}
int fFakeIns = 0, fFakeOuts = 0;
if ( p->vNamesIn == NULL )
p->vNamesIn = Gia_GetFakeNames( Gia_ManCiNum(p), 0 ), fFakeIns = 1;
if ( p->vNamesOut == NULL )
p->vNamesOut = Gia_GetFakeNames( Gia_ManCoNum(p), 1 ), fFakeOuts = 1;

Gia_Obj_t * pObj, * pObj2;
char * pLine = ABC_CALLOC( char, Gia_ManCiNum(p)+3 );
int i, k, c, iLit, nOuts[2] = {0}, nCexes = Vec_WecSize(vCexes) / Gia_ManCoNum(p);
fprintf( pFile, "# Satisfying assignments for the primary outputs generated by ABC on %s\n", Gia_TimeStamp() );
fprintf( pFile, ".model %s\n", p->pName );
fprintf( pFile, ".inputs" );
Gia_ManForEachCi( p, pObj, i )
fprintf( pFile, " %s", Gia_ObjCiName(p, i) );
fprintf( pFile, "\n.outputs" );
Gia_ManForEachCo( p, pObj, i )
fprintf( pFile, " %s", Gia_ObjCoName(p, i) );
fprintf( pFile, "\n" );
Gia_ManForEachCo( p, pObj, i ) {
if ( Gia_ObjFaninLit0p(p, pObj) == 0 ) {
fprintf( pFile, ".names %s\n", Gia_ObjCoName(p, i) );
nOuts[0]++;
}
else if ( Gia_ObjFaninLit0p(p, pObj) == 1 ) {
fprintf( pFile, ".names %s\n 1\n", Gia_ObjCiName(p, i) );
nOuts[1]++;
}
else {
fprintf( pFile, ".names" );
Gia_ManForEachCi( p, pObj2, c )
fprintf( pFile, " %s", Gia_ObjCiName(p, c) );
fprintf( pFile, " %s\n", Gia_ObjCoName(p, i) );
for ( c = 0; c < nCexes; c++ ) {
Vec_Int_t * vPat = Vec_WecEntry( vCexes, i*nCexes+c );
memset(pLine, '-', Gia_ManCiNum(p) );
Vec_IntForEachEntry( vPat, iLit, k )
pLine[Abc_Lit2Var(iLit)-1] = '1' - Abc_LitIsCompl(iLit);
fprintf( pFile, "%s 1\n", pLine );
}
nOuts[1]++;
}
}
fprintf( pFile, ".end\n\n" );
fclose( pFile );
printf( "Information about %d sat, %d unsat, and %d undecided primary outputs was written into BLIF file \"%s\".\n",
nOuts[1], nOuts[0], Gia_ManCoNum(p)-nOuts[1]-nOuts[0], pFileName );
free( pLine );

if ( fFakeIns ) Vec_PtrFreeFree( p->vNamesIn ), p->vNamesIn = NULL;
if ( fFakeOuts ) Vec_PtrFreeFree( p->vNamesOut ), p->vNamesOut = NULL;
}
void Gia_GenerateCexesDumpFile( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCexes, int fShort )
{
FILE * pFile = fopen( pFileName, "wb" );
Expand Down Expand Up @@ -1416,13 +1475,16 @@ void Gia_GenerateCexesDumpFile( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCe
fclose( pFile );
free( pLine );
}
void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fVerbose, int fVeryVerbose )
void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fBlif, int fVerbose, int fVeryVerbose )
{
unsigned Start = Abc_Random(1);
Vec_Int_t * vStats[3] = {0}; int i;
Vec_Wec_t * vCexes = Min_ManComputeCexes( p, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose );
assert( Vec_WecSize(vCexes) == Gia_ManCoNum(p) * nMinCexes );
Gia_GenerateCexesDumpFile( pFileName, p, vCexes, fShort );
if ( fBlif )
Gia_GenerateCexesDumpBlif( pFileName, p, vCexes );
else
Gia_GenerateCexesDumpFile( pFileName, p, vCexes, fShort );
for ( i = 0; i < 3; i++ )
Vec_IntFreeP( &vStats[i] );
Vec_WecFree( vCexes );
Expand Down
13 changes: 9 additions & 4 deletions src/base/abci/abc.c
View file
Original file line number Diff line number Diff line change
Expand Up @@ -53541,17 +53541,18 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
***********************************************************************/
int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fVerbose, int fVeryVerbose );
extern void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fBlif, int fVerbose, int fVeryVerbose );
char * pFileName = (char *)"cexes.txt";
int nMinCexes = 1;
int nMaxTries = 10;
int fUseSim = 1;
int fUseSat = 1;
int fShort = 0;
int fBlif = 0;
int fVerbose = 0;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "CMFstcvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CMFstcbvh" ) ) != EOF )
{
switch ( c )
{
Expand Down Expand Up @@ -53595,6 +53596,9 @@ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'c':
fShort ^= 1;
break;
case 'b':
fBlif ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
Expand All @@ -53609,18 +53613,19 @@ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Bmci(): There is no AIG.\n" );
return 0;
}
Gia_GenerateCexes( pFileName, pAbc->pGia, nMaxTries, nMinCexes, fUseSim, fUseSat, fShort, fVerbose, 0 );
Gia_GenerateCexes( pFileName, pAbc->pGia, nMaxTries, nMinCexes, fUseSim, fUseSat, fShort, fBlif, fVerbose, 0 );
return 0;

usage:
Abc_Print( -2, "usage: &gencex [-CM num] [-F file] [-stcvh]\n" );
Abc_Print( -2, "usage: &gencex [-CM num] [-F file] [-stcbvh]\n" );
Abc_Print( -2, "\t generates satisfying assignments for each output of the miter\n" );
Abc_Print( -2, "\t-C num : the number of timeframes [default = %d]\n", nMinCexes );
Abc_Print( -2, "\t-M num : the max simulation runs before using SAT [default = %d]\n", nMaxTries );
Abc_Print( -2, "\t-F file : the output file name [default = %s]\n", pFileName );
Abc_Print( -2, "\t-s : toggles using reverse simulation [default = %s]\n", fUseSim ? "yes": "no" );
Abc_Print( -2, "\t-t : toggles using SAT solving [default = %s]\n", fUseSat ? "yes": "no" );
Abc_Print( -2, "\t-c : toggles outputing care literals only [default = %s]\n", fShort ? "yes": "no" );
Abc_Print( -2, "\t-b : toggles outputing the BLIF file [default = %s]\n", fBlif ? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose ? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
Expand Down

0 comments on commit 2055b1b

Please sign in to comment.