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

Experiments with mapping.

This commit is contained in:
Alan Mishchenko 2025-03-14 20:24:08 -07:00
parent aaba1b9a5f
commit 839f3e18dd
2 changed files with 16 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
src/aig/gia/giaSatLut.c
View File

@ -1539,7 +1539,7 @@ int Gia_ManDumpCnf( char * pFileName, Vec_Str_t * vStr, int nVars )
int Gia_ManDumpCnf2( Vec_Str_t * vStr, int nVars, int argc, char ** argv, abctime Time, int Status )
{
Vec_Str_t * vFileName = Vec_StrAlloc( 100 ); int c;
Vec_StrPrintF( vFileName, "%s", argv[0] );
Vec_StrPrintF( vFileName, "%s", argv[0] + (argv[0][0] == '&') );
for ( c = 1; c < argc; c++ )
Vec_StrPrintF( vFileName, "_%s", argv[c] + (argv[c][0] == '-') );
Vec_StrPrintF( vFileName, ".cnf" );
@ -1547,19 +1547,19 @@ int Gia_ManDumpCnf2( Vec_Str_t * vStr, int nVars, int argc, char ** argv, abctim
FILE * pFile = fopen( Vec_StrArray(vFileName), "wb" );
if ( pFile == NULL ) { printf( "Cannot open output file \"%s\".\n", Vec_StrArray(vFileName) ); Vec_StrFree(vFileName); return 0; }
Vec_StrFree(vFileName);
fprintf( pFile, "c ABC command line: \"" );
fprintf( pFile, "c This file was generated by ABC command: \"" );
fprintf( pFile, "%s", argv[0] );
for ( c = 1; c < argc; c++ )
fprintf( pFile, " %s", argv[c] );
fprintf( pFile, "\" " );
fprintf( pFile, "\" on %s\n", Gia_TimeStamp() );
fprintf( pFile, "c Cardinality CDCL (https://github.com/jreeves3/Cardinality-CDCL) found it to be " );
if ( Status == 1 )
fprintf( pFile, "UNSAT after " );
fprintf( pFile, "UNSAT" );
if ( Status == 0 )
fprintf( pFile, "SAT after " );
fprintf( pFile, "SAT" );
if ( Status == -1 )
fprintf( pFile, "UNDECIDED after " );
fprintf( pFile, "%.2f sec by CaDiCal on ", 1.0*((double)(Time))/((double)CLOCKS_PER_SEC) );
fprintf( pFile, "%s\n", Gia_TimeStamp() );
fprintf( pFile, "UNDECIDED" );
fprintf( pFile, " in %.2f sec\n", 1.0*((double)(Time))/((double)CLOCKS_PER_SEC) );
fprintf( pFile, "p knf %d %d\n%s\n", nVars, Vec_StrCountEntry(vStr, '\n'), Vec_StrArray(vStr) );
fclose( pFile );
return 1;
@ -1687,16 +1687,23 @@ Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound, int fM
// fanins are connected once
for ( n = nIns; n < nIns+nNodes; n++ )
for ( f = 0; f < 2; f++ ) {
nLits = 0;
for ( i = 0; i < n; i++ )
pLits[nLits++] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 0 );
Gia_SatDumpClause( vStr, pLits, nLits );
/*
for ( i = 0; i < n; i++ )
for ( j = 0; j < i; j++ ) {
pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, j), 1 );
Gia_SatDumpClause( vStr, pLits, 2 );
}
*/
Vec_StrPrintF( vStr, "k %d ", n-1 );
for ( i = 0; i < n; i++ )
pLits[i] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 );
Gia_SatDumpClause( vStr, pLits, n );
}
for ( n = nIns; n < nIns+nNodes; n++ ) {
// fanins are equal

2
src/base/abci/abc.c
View File

@ -55359,7 +55359,7 @@ usage:
Abc_Print( -2, "\t generates Boolean relation for the given logic window\n" );
Abc_Print( -2, "\t-I list : comma-separated list of window inputs [default = undefined]\n" );
Abc_Print( -2, "\t-O list : comma-separated list of window outputs [default = undefined]\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %d]\n", fVerbose ? "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");
Abc_Print( -2, "\t<file> : the output file name (PLA format extended to represented Boolean relations)\n");
return 1;