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

Experiments with SAT solving.

This commit is contained in:
Alan Mishchenko 2023-10-23 11:30:44 -07:00
parent 1bf21626c0
commit 5de12aa6b3
2 changed files with 37 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
src/base/io/io.c
View File

@ -1224,17 +1224,21 @@ usage:
***********************************************************************/
int IoCommandReadCnf( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Vec_Ptr_t * Io_FileReadCnf( char * pFileName );
extern Vec_Ptr_t * Io_FileReadCnf( char * pFileName, int fMulti );
FILE * pFile;
Abc_Ntk_t * pNtk;
Vec_Ptr_t * vSops;
int fMulti = 0;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF )
{
switch ( c )
{
case 'm':
fMulti ^= 1;
break;
case 'h':
goto usage;
default:
@ -1253,7 +1257,7 @@ int IoCommandReadCnf( Abc_Frame_t * pAbc, int argc, char ** argv )
}
else
fclose( pFile );
vSops = Io_FileReadCnf( argv[globalUtilOptind] );
vSops = Io_FileReadCnf( argv[globalUtilOptind], fMulti );
if ( Vec_PtrSize(vSops) == 0 )
{
Vec_PtrFreeFree( vSops );
@ -1273,8 +1277,9 @@ int IoCommandReadCnf( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
fprintf( pAbc->Err, "usage: read_cnf [-h] <file>\n" );
fprintf( pAbc->Err, "usage: read_cnf [-mh] <file>\n" );
fprintf( pAbc->Err, "\t creates network with one node\n" );
fprintf( pAbc->Err, "\t-m : toggles generating multi-output network [default = %s]\n", fMulti? "yes":"no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tfile : file name with the truth table\n" );
return 1;

33
src/base/io/ioUtil.c
View File

@ -931,8 +931,9 @@ void Io_TransformSF2PLA( char * pNameIn, char * pNameOut )
SeeAlso []
***********************************************************************/
char * Io_ConvertNumsToSop( Vec_Wec_t * vNums, int nVars )
Vec_Ptr_t * Io_ConvertNumsToSop( Vec_Wec_t * vNums, int nVars )
{
Vec_Ptr_t * vSops = Vec_PtrAlloc(1);
Vec_Int_t * vLevel; int i, k, Num;
int nSize = (nVars + 3)*Vec_WecSize(vNums);
char * pStr = ABC_ALLOC( char, nSize+1 );
@ -947,11 +948,30 @@ char * Io_ConvertNumsToSop( Vec_Wec_t * vNums, int nVars )
pCube[nVars+1] = '0';
pCube[nVars+2] = '\n';
}
return pStr;
Vec_PtrPush( vSops, pStr );
return vSops;
}
Vec_Ptr_t * Io_FileReadCnf( char * pFileName )
Vec_Ptr_t * Io_ConvertNumsToSopMulti( Vec_Wec_t * vNums, int nVars )
{
Vec_Ptr_t * vSops = Vec_PtrAlloc( 1 );
Vec_Ptr_t * vSops = Vec_PtrAlloc( Vec_WecSize(vNums) );
Vec_Int_t * vLevel; int i, k, Num;
Vec_WecForEachLevel( vNums, vLevel, i )
{
char * pCube = ABC_ALLOC( char, nVars + 4 );
memset( pCube, '-', nVars );
Vec_IntForEachEntry( vLevel, Num, k )
pCube[Abc_Lit2Var(Num)] = '0' + Abc_LitIsCompl(Num);
pCube[nVars+0] = ' ';
pCube[nVars+1] = '0';
pCube[nVars+2] = '\n';
pCube[nVars+3] = '\0';
Vec_PtrPush( vSops, pCube );
}
return vSops;
}
Vec_Ptr_t * Io_FileReadCnf( char * pFileName, int fMulti )
{
Vec_Ptr_t * vSops = NULL;
Vec_Wec_t * vNums = Vec_WecAlloc( 100 );
Vec_Int_t * vLevel;
char * pThis, pLine[10000];
@ -1002,7 +1022,10 @@ Vec_Ptr_t * Io_FileReadCnf( char * pFileName )
if ( nClas != Vec_WecSize(vNums) )
printf( "Warning: The number of clauses (%d) listed is different from the actual number (%d).\n", nClas, Vec_WecSize(vNums) );
//Vec_WecPrint( vNums, 0 );
Vec_PtrPush( vSops, Io_ConvertNumsToSop(vNums, nVars) );
if ( fMulti )
vSops = Io_ConvertNumsToSopMulti(vNums, nVars);
else
vSops = Io_ConvertNumsToSop(vNums, nVars);
Vec_WecFree( vNums );
return vSops;
}