diff --git a/CMakeLists.txt b/CMakeLists.txt index ce541b994..db9d724f2 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -3,6 +3,8 @@ cmake_minimum_required(VERSION 3.5.0) include(CMakeParseArguments) include(CheckCCompilerFlag) include(CheckCXXCompilerFlag) +# Generate compilation database compile_commands.json +set(CMAKE_EXPORT_COMPILE_COMMANDS ON) # Default c++ standard used unless otherwise specified in target_compile_features. set(CMAKE_CXX_STANDARD 17 CACHE STRING "the C++ standard to use for this project") diff --git a/Makefile b/Makefile index a546f65fd..50cff2d17 100644 --- a/Makefile +++ b/Makefile @@ -27,7 +27,7 @@ MODULES := \ src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \ src/opt/cut src/opt/fxu src/opt/fxch src/opt/rwr src/opt/mfs src/opt/sim \ src/opt/ret src/opt/fret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt src/opt/rar \ - src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd \ + src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/dsc src/opt/sfm src/opt/sbd src/opt/eslim \ src/sat/bsat src/sat/xsat src/sat/satoko src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc src/sat/glucose src/sat/glucose2 src/sat/kissat src/sat/cadical \ src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \ src/bool/rsb src/bool/rpo \ diff --git a/abclib.dsp b/abclib.dsp index 921030b34..2bcb6e1b8 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -4114,6 +4114,46 @@ SOURCE=.\src\opt\sbd\sbdSat.c SOURCE=.\src\opt\sbd\sbdWin.c # End Source File # End Group +# Begin Group "eslim" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\opt\eslim\eSLIM.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\eSLIM.h +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\eSLIMMan.hpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\relationGeneration.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\relationGeneration.hpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\satInterfaces.hpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\selectionStrategy.hpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\utils.hpp +# End Source File +# Begin Source File + +SOURCE=.\src\opt\eslim\synthesisEngine.hpp +# End Source File +# End Group # End Group # Begin Group "map" diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index b950da4be..273c530ec 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1808,7 +1808,7 @@ extern Gia_Man_t * Gia_ManTransductionBdd( Gia_Man_t * pGia, int nType, extern Gia_Man_t * Gia_ManTransductionTt( Gia_Man_t * pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t * pExdc, int fNewLine, int nVerbose ); /*=== giaRrr.cpp ===========================================================*/ -extern Gia_Man_t * Gia_ManRrr( Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nPartitionerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow, int nDistance, int nRestarts, int nThreads, int nWindowSize, int fDeterministic ); +extern Gia_Man_t * Gia_ManRrr( Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nPartitionerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow, int nPartitionType, int nDistance, int nJobs, int nThreads, int nPartitionSize, int nPartitionSizeMin, int fDeterministic, int nParallelPartitions, int fOptOnInsert, int fGreedy ); /*=== giaCTas.c ===========================================================*/ typedef struct Tas_Man_t_ Tas_Man_t; diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 9c6ca8992..107faaceb 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -406,24 +406,24 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi if ( *pType == 'i' ) { if ( vNamesIn == NULL ) - vNamesIn = Vec_PtrAlloc( nInputs + nLatches ); - if ( Vec_PtrSize(vNamesIn) != iTerm ) + vNamesIn = Vec_PtrStart( nInputs ); + if ( Vec_PtrSize(vNamesIn) <= iTerm ) { fError = 1; break; } - Vec_PtrPush( vNamesIn, Abc_UtilStrsav(pName) ); + Vec_PtrWriteEntry( vNamesIn, iTerm, Abc_UtilStrsav(pName) ); } else if ( *pType == 'o' ) { if ( vNamesOut == NULL ) - vNamesOut = Vec_PtrAlloc( nOutputs + nLatches ); - if ( Vec_PtrSize(vNamesOut) != iTerm ) + vNamesOut = Vec_PtrStart( nOutputs ); + if ( Vec_PtrSize(vNamesOut) <= iTerm ) { fError = 1; break; } - Vec_PtrPush( vNamesOut, Abc_UtilStrsav(pName) ); + Vec_PtrWriteEntry( vNamesOut, iTerm, Abc_UtilStrsav(pName) ); } else if ( *pType == 'l' ) { @@ -431,16 +431,16 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi assert( strlen(pName) < 995 ); sprintf( Buffer, "%s_in", pName ); if ( vNamesRegIn == NULL ) - vNamesRegIn = Vec_PtrAlloc( nLatches ); + vNamesRegIn = Vec_PtrStart( nLatches ); if ( vNamesRegOut == NULL ) - vNamesRegOut = Vec_PtrAlloc( nLatches ); - if ( Vec_PtrSize(vNamesRegIn) != iTerm ) + vNamesRegOut = Vec_PtrStart( nLatches ); + if ( Vec_PtrSize(vNamesRegIn) <= iTerm ) { fError = 1; break; } - Vec_PtrPush( vNamesRegIn, Abc_UtilStrsav(Buffer) ); - Vec_PtrPush( vNamesRegOut, Abc_UtilStrsav(pName) ); + Vec_PtrWriteEntry( vNamesRegIn, iTerm, Abc_UtilStrsav(Buffer) ); + Vec_PtrWriteEntry( vNamesRegOut, iTerm, Abc_UtilStrsav(pName) ); } else if ( *pType == 'n' ) { diff --git a/src/aig/gia/giaNf.c b/src/aig/gia/giaNf.c index f70a63135..8bcf76b33 100644 --- a/src/aig/gia/giaNf.c +++ b/src/aig/gia/giaNf.c @@ -2674,6 +2674,9 @@ Gia_Man_t * Nf_ManPerformMapping( Gia_Man_t * p, Jf_Par_t * pPars ) pNew = Nf_ManPerformMappingInt( p, pPars ); Gia_ManTransferTiming( pNew, p ); //Gia_ManCellMappingVerify( pNew ); + // remove choices after mapping + ABC_FREE( pNew->pReprs ); + ABC_FREE( pNew->pNexts ); } //pNew->MappedDelay = (int)((If_Par_t *)pp)->FinalDelay; //pNew->MappedArea = (int)((If_Par_t *)pp)->FinalArea; diff --git a/src/aig/gia/giaRrr.cpp b/src/aig/gia/giaRrr.cpp index df3b91e60..1eccd4dc2 100644 --- a/src/aig/gia/giaRrr.cpp +++ b/src/aig/gia/giaRrr.cpp @@ -5,7 +5,7 @@ ABC_NAMESPACE_IMPL_START -Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nPartitionerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow, int nDistance, int nRestarts, int nThreads, int nWindowSize, int fDeterministic) { +Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int nSchedulerVerbose, int nPartitionerVerbose, int nOptimizerVerbose, int nAnalyzerVerbose, int nSimulatorVerbose, int nSatSolverVerbose, int fUseBddCspf, int fUseBddMspf, int nConflictLimit, int nSortType, int nOptimizerFlow, int nSchedulerFlow, int nPartitionType, int nDistance, int nJobs, int nThreads, int nPartitionSize, int nPartitionSizeMin, int fDeterministic, int nParallelPartitions, int fOptOnInsert, int fGreedy) { rrr::AndNetwork ntk; ntk.Read(pGia, rrr::GiaReader); rrr::Parameter Par; @@ -24,11 +24,16 @@ Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int Par.nSortType = nSortType; Par.nOptimizerFlow = nOptimizerFlow; Par.nSchedulerFlow = nSchedulerFlow; + Par.nPartitionType = nPartitionType; Par.nDistance = nDistance; - Par.nRestarts = nRestarts; + Par.nJobs = nJobs; Par.nThreads = nThreads; - Par.nWindowSize = nWindowSize; + Par.nPartitionSize = nPartitionSize; + Par.nPartitionSizeMin = nPartitionSizeMin; Par.fDeterministic = fDeterministic; + Par.nParallelPartitions = nParallelPartitions; + Par.fOptOnInsert = fOptOnInsert; + Par.fGreedy = fGreedy; rrr::Perform(&ntk, &Par); Gia_Man_t *pNew = rrr::CreateGia(&ntk); return pNew; diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c index ba25ec90e..cc6068a96 100644 --- a/src/aig/gia/giaSatLut.c +++ b/src/aig/gia/giaSatLut.c @@ -20,6 +20,7 @@ #include "gia.h" #include "misc/tim/tim.h" +#include "misc/util/utilTruth.h" #include "sat/bsat/satStore.h" #include "misc/util/utilNam.h" #include "map/scl/sclCon.h" @@ -1233,7 +1234,7 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int LutSize, int nNumber, int nImproves, i SeeAlso [] ***********************************************************************/ -Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimit, int TimeOut, int fVerbose ) +Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int Seed, int nBTLimit, int TimeOut, int fVerbose, int * pStatus ) { extern Vec_Int_t * Exa4_ManParse( char *pFileName ); int fVerboseSolver = 0; @@ -1242,20 +1243,25 @@ Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimi #ifdef _WIN32 char * pKadical = "kadical.exe"; #else - char * pKadical = "kadical"; + char * pKadical = "./kadical"; + FILE * pFile = fopen( pKadical, "rb" ); + if ( pFile == NULL ) + pKadical += 2; + else + fclose( pFile ); #endif char Command[1000], * pCommand = (char *)&Command; if ( nBTLimit ) { if ( TimeOut ) - sprintf( pCommand, "%s -c %d -t %d %s %s > %s", pKadical, nBTLimit, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); + sprintf( pCommand, "%s --seed=%d -c %d -t %d %s %s > %s", pKadical, Seed, nBTLimit, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); else - sprintf( pCommand, "%s -c %d %s %s > %s", pKadical, nBTLimit, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); + sprintf( pCommand, "%s --seed=%d -c %d %s %s > %s", pKadical, Seed, nBTLimit, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); } else { if ( TimeOut ) - sprintf( pCommand, "%s -t %d %s %s > %s", pKadical, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); + sprintf( pCommand, "%s --seed=%d -t %d %s %s > %s", pKadical, Seed, TimeOut, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); else - sprintf( pCommand, "%s %s %s > %s", pKadical, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); + sprintf( pCommand, "%s --seed=%d %s %s > %s", pKadical, Seed, fVerboseSolver ? "": "-q", pFileNameIn, pFileNameOut ); } #ifdef __wasm if ( 1 ) @@ -1270,11 +1276,11 @@ Vec_Int_t * Gia_RunKadical( char * pFileNameIn, char * pFileNameOut, int nBTLimi if ( fVerbose ) { if ( vRes ) - printf( "The problem has a solution. " ); + printf( "The problem has a solution. " ), *pStatus = 0; else if ( vRes == NULL && TimeOut == 0 ) - printf( "The problem has no solution. " ); + printf( "The problem has no solution. " ), *pStatus = 1; else if ( vRes == NULL ) - printf( "The problem has no solution or reached a resource limit after %d sec. ", TimeOut ); + printf( "The problem has no solution or reached a resource limit after %d sec. ", TimeOut ), *pStatus = -1; Abc_PrintTime( 1, "SAT solver time", Abc_Clock() - clkTotal ); } return vRes; @@ -1535,10 +1541,41 @@ int Gia_ManDumpCnf( char * pFileName, Vec_Str_t * vStr, int nVars ) fclose( pFile ); return 1; } -int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, int fVerbose ) +int Gia_ManDumpCnf2( Vec_Str_t * vStr, int nVars, int argc, char ** argv, abctime Time, int Status ) { - char * pFileNameI = (char *)"__temp__.cnf"; - char * pFileNameO = (char *)"__temp__.out"; + Vec_Str_t * vFileName = Vec_StrAlloc( 100 ); int c; + 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" ); + Vec_StrPush( vFileName, '\0' ); + 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 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, "\" 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" ); + if ( Status == 0 ) + fprintf( pFile, "SAT" ); + if ( Status == -1 ) + 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; +} +int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int Seed, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv ) +{ + abctime clkStart = Abc_Clock(); + srand(time(NULL)); + int Status, Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFFF; + char pFileNameI[32]; sprintf( pFileNameI, "_%06x_.cnf", Rand ); + char pFileNameO[32]; sprintf( pFileNameO, "_%06x_.out", Rand ); if ( nBound == 0 ) nBound = 5 * Gia_ManAndNum(p); Vec_Str_t * vStr = Gia_ManSimpleCnf( p, nBound/2 ); @@ -1550,12 +1587,11 @@ int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, if ( fVerbose ) printf( "SAT variables = %d. SAT clauses = %d. Cardinality bound = %d. Conflict limit = %d. Timeout = %d.\n", nVars, Vec_StrCountEntry(vStr, '\n'), nBound, nBTLimit, nTimeout ); - //char pFileName[100]; sprintf( pFileName, "temp%02d.cnf", nBound/2 ); - //Gia_ManDumpCnf( pFileName, vStr, nVars ); - Vec_StrFree( vStr ); - Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, nBTLimit, nTimeout, 1 ); + Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, Seed, nBTLimit, nTimeout, fVerbose, &Status ); unlink( pFileNameI ); //unlink( pFileNameO ); + if ( fKeepFile ) Gia_ManDumpCnf2( vStr, nVars, argc, argv, Abc_Clock() - clkStart, Status ); + Vec_StrFree( vStr ); if ( vRes == NULL ) return 0; Vec_IntFreeP( &p->vCellMapping ); @@ -1564,9 +1600,487 @@ int Gia_ManSimpleMapping( Gia_Man_t * p, int nBound, int nBTLimit, int nTimeout, if ( fVerbose ) Gia_ManSimplePrintMapping( vRes, Gia_ManCiNum(p) ); p->vCellMapping = Gia_ManDeriveSimpleMapping( p, vRes ); Vec_IntFree( vRes ); + if ( fVerbose ) Abc_PrintTime( 0, "Total time", Abc_Clock() - clkStart ); return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +#define KSAT_OBJS 24 +#define KSAT_MINTS 64 +#define KSAT_SPACE (4+3*KSAT_OBJS+3*KSAT_MINTS) + +int Gia_KSatVarInv( int * pMap, int i ) { return pMap[i*KSAT_SPACE+0]; } +int Gia_KSatVarAnd( int * pMap, int i ) { return pMap[i*KSAT_SPACE+1]; } +int Gia_KSatVarEqu( int * pMap, int i ) { return pMap[i*KSAT_SPACE+2]; } +int Gia_KSatVarRef( int * pMap, int i ) { return pMap[i*KSAT_SPACE+3]; } +int Gia_KSatVarFan( int * pMap, int i, int f, int k ) { return pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k]; } +int Gia_KSatVarMin( int * pMap, int i, int m, int k ) { return pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k]; } + +void Gia_KSatSetInv( int * pMap, int i, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+0] ); pMap[i*KSAT_SPACE+0] = iVar; } +void Gia_KSatSetAnd( int * pMap, int i, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+1] ); pMap[i*KSAT_SPACE+1] = iVar; } +void Gia_KSatSetEqu( int * pMap, int i, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+2] ); pMap[i*KSAT_SPACE+2] = iVar; } +void Gia_KSatSetRef( int * pMap, int i, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+3] ); pMap[i*KSAT_SPACE+3] = iVar; } +void Gia_KSatSetFan( int * pMap, int i, int f, int k, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] = iVar; } +void Gia_KSatSetMin( int * pMap, int i, int m, int k, int iVar ) { assert( -1 == pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k] ); pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k] = iVar; } + +int Gia_KSatValInv( int * pMap, int i, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+0] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+0] ); } +int Gia_KSatValAnd( int * pMap, int i, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+1] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+1] ); } +int Gia_KSatValEqu( int * pMap, int i, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+2] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+2] ); } +int Gia_KSatValRef( int * pMap, int i, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+3] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+3] ); } +int Gia_KSatValFan( int * pMap, int i, int f, int k, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+4+f*KSAT_OBJS+k] ); } +int Gia_KSatValMin( int * pMap, int i, int m, int k, Vec_Int_t * vRes ) { assert( -1 != pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k] ); return Vec_IntEntry( vRes, pMap[i*KSAT_SPACE+4+3*KSAT_OBJS+3*m+k] ); } + +int * Gia_KSatMapInit( int nIns, int nNodes, word Truth, int * pnVars ) +{ + assert( nIns + nNodes <= KSAT_OBJS ); + assert( (1 << nIns) <= KSAT_MINTS ); + int n, m, f, k, nVars = 2, * pMap = ABC_FALLOC( int, KSAT_OBJS*KSAT_SPACE ); + for ( n = nIns; n < nIns+nNodes; n++ ) { + Gia_KSatSetInv(pMap, n, nVars++); + Gia_KSatSetAnd(pMap, n, nVars++); + Gia_KSatSetEqu(pMap, n, nVars++); + Gia_KSatSetRef(pMap, n, nVars++); + } + for ( n = nIns; n < nIns+nNodes; n++ ) { + for ( f = 0; f < 2; f++ ) + for ( k = 0; k < n; k++ ) + Gia_KSatSetFan(pMap, n, f, k, nVars++); + for ( k = n+1; k < nIns+nNodes; k++ ) + Gia_KSatSetFan(pMap, n, 2, k, nVars++); + } + for ( m = 0; m < (1<> n) & 1 ); + Gia_KSatSetMin(pMap, nIns+nNodes-1, m, 0, (Truth >> m) & 1 ); + for ( n = nIns; n < nIns+nNodes; n++ ) + for ( k = 0; k < 3; k++ ) + if ( k || n < nIns+nNodes-1 ) + Gia_KSatSetMin(pMap, n, m, k, nVars++); + + } + if ( pnVars ) *pnVars = nVars; + return pMap; +} + +int Gia_KSatFindFan( int * pMap, int i, int f, Vec_Int_t * vRes ) +{ + assert( f < 2 ); + for ( int k = 0; k < i; k++ ) + if ( Gia_KSatValFan( pMap, i, f, k, vRes ) ) + return k; + assert( 0 ); + return -1; +} + +Vec_Int_t * Gia_ManKSatGenLevels( char * pGuide, int nIns, int nNodes ) +{ + Vec_Int_t * vRes; + int i, k, Count = 0; + for ( i = 0; pGuide[i]; i++ ) + Count += pGuide[i] - '0'; + if ( Count != nNodes ) { + printf( "Guidance %s has %d nodes while the problem has %d nodes.\n", pGuide, Count, nNodes ); + return NULL; + } + int FirstPrev = 0; + int FirstThis = nIns; + int FirstNext = FirstThis; + vRes = Vec_IntStartFull( 2*nIns ); + for ( i = 0; pGuide[i]; i++ ) { + FirstNext += pGuide[i] - '0'; + for ( k = FirstThis; k < FirstNext; k++ ) + Vec_IntPushTwo( vRes, FirstPrev, FirstThis ); + FirstPrev = FirstThis; + FirstThis = FirstNext; + } + assert( Vec_IntSize(vRes) == 2*(nIns + nNodes) ); + Count = 0; + //int Start, Stop; + //Vec_IntForEachEntryDouble(vRes, Start, Stop, i) + // printf( "%2d : Start %2d Stop %2d\n", Count++, Start, Stop ); + return vRes; +} + +Vec_Str_t * Gia_ManKSatCnf( int * pMap, int nIns, int nNodes, int nBound, int fMultiLevel, char * pGuide ) +{ + Vec_Str_t * vStr = Vec_StrAlloc( 10000 ); + Vec_Int_t * vRes = pGuide ? Gia_ManKSatGenLevels( pGuide, nIns, nNodes ) : NULL; + int i, j, m, n, f, c, a, Start, Stop, nLits = 0, pLits[256] = {0}; + Gia_SatDumpLiteral( vStr, 1 ); + Gia_SatDumpLiteral( vStr, 2 ); + if ( vRes ) { + n = nIns; + Vec_IntForEachEntryDoubleStart( vRes, Start, Stop, i, 2*nIns ) { + for ( j = 0; j < Start; j++ ) + Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 ) ); + for ( f = 0; f < 2; f++ ) + for ( j = Stop; j < n; j++ ) + Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, j), 1 ) ); + n++; + } + assert( n == nIns + nNodes ); + } + // 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 + for ( i = 0; i < n; i++ ) { + pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, i), 1 ); + pLits[2] = Abc_Var2Lit( Gia_KSatVarEqu(pMap, n), 0 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + } + for ( i = 0; i < n; i++ ) + for ( j = i+1; j < n; j++ ) { + pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 ); + pLits[2] = Abc_Var2Lit( Gia_KSatVarEqu(pMap, n), 1 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + } + // if fanins are equal, inv is used + pLits[0] = Abc_Var2Lit( Gia_KSatVarEqu(pMap, n), 1 ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 ); + Gia_SatDumpClause( vStr, pLits, 2 ); + // fanin ordering + for ( i = 0; i < n; i++ ) + for ( j = 0; j < i; j++ ) { + pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 ); + Gia_SatDumpClause( vStr, pLits, 2 ); + } + } + for ( n = nIns; n < nIns+nNodes-1; n++ ) { + // there is a fanout to the node above + for ( i = n+1; i < nIns+nNodes; i++ ) { + for ( f = 0; f < 2; f++ ) { + pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, i, f, n), 1 ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 0 ); + Gia_SatDumpClause( vStr, pLits, 2 ); + } + pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, i, 0, n), 0 ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, i, 1, n), 0 ); + pLits[2] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 1 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + } + // there is at least one fanout, except the last one + nLits = 0; + for ( i = n+1; i < nIns+nNodes; i++ ) + pLits[nLits++] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 0 ); + assert( nLits > 0 ); + Gia_SatDumpClause( vStr, pLits, nLits ); + } + // there is more than one fanout, except the last one + for ( n = nIns; n < nIns+nNodes-1; n++ ) { + for ( i = n+1; i < nIns+nNodes; i++ ) + for ( j = i+1; j < nIns+nNodes; j++ ) { + pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, i), 1 ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 2, j), 1 ); + pLits[2] = Abc_Var2Lit( Gia_KSatVarRef(pMap, n), 0 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + } + // if more than one fanout, inv is used + pLits[0] = Abc_Var2Lit( Gia_KSatVarRef(pMap, n), 1 ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 ); + Gia_SatDumpClause( vStr, pLits, 2 ); + // if inv is not used, its fanins' invs are used + if ( !fMultiLevel ) { + pLits[0] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), 0 ); + for ( i = nIns; i < n; i++ ) + for ( f = 0; f < 2; f++ ) { + pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 ); + pLits[2] = Abc_Var2Lit( Gia_KSatVarInv(pMap, i), 0 ); + Gia_SatDumpClause( vStr, pLits, 3 ); + } + } + } + // the last one always uses inverter + Gia_SatDumpLiteral( vStr, Abc_Var2Lit( Gia_KSatVarInv(pMap, nIns+nNodes-1), 0 ) ); +/* + // for each minterm, for each pair of possible fanins, the node's output is determined using and/or and inv (4*N*N*M) + for ( m = 0; m < (1 << nIns); m++ ) + for ( n = nIns; n < nIns+nNodes; n++ ) + for ( c = 0; c < 2; c++ ) + for ( a = 0; a < 2; a++ ) { + // implications: Fan(f) & Mint(m) & !And & !Inv -> Val1 + for ( f = 0; f < 2; f++ ) + for ( i = 0; i < n; i++ ) { + pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m, 0), !a ); + pLits[2] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a ); + pLits[3] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c ); + pLits[4] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 0), a^c ); + Gia_SatDumpClause( vStr, pLits, 5 ); + } + // large clauses: Fan(0) & Fan(1) & !Mint(m) & !Mint(m) & !And & !Inv -> Val0 + for ( i = 0; i < n; i++ ) + for ( j = i; j < n; j++ ) { + pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 0, i), 1 ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, 1, j), 1 ); + pLits[2] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m, 0), a ); + pLits[3] = Abc_Var2Lit( Gia_KSatVarMin(pMap, j, m, 0), a ); + pLits[4] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a ); + pLits[5] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c ); + pLits[6] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 0), a==c ); + Gia_SatDumpClause( vStr, pLits, 7 ); + } + } +*/ + // for each minterm, define a fanin variable and use it to get the node's output based on and/or and inv (4*N*N*M) + for ( m = 0; m < (1 << nIns); m++ ) + for ( n = nIns; n < nIns+nNodes; n++ ) { + for ( i = 0; i < n; i++ ) + for ( f = 0; f < 2; f++ ) + for ( c = 0; c < 2; c++ ) { + pLits[0] = Abc_Var2Lit( Gia_KSatVarFan(pMap, n, f, i), 1 ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarMin(pMap, i, m, 0), c ); + pLits[2] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 1+f), !c ); + Gia_SatDumpClause( vStr, pLits, 3 ); + } + for ( c = 0; c < 2; c++ ) + for ( a = 0; a < 2; a++ ) { + // implications: Mint(m,f) & !And & !Inv -> Val1 + for ( f = 0; f < 2; f++ ) { + pLits[0] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 1+f), !a ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a ); + pLits[2] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c ); + pLits[3] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 0), a^c ); + Gia_SatDumpClause( vStr, pLits, 4 ); + } + // large clauses: !Mint(m,0) & !Mint(m,1) & !And & !Inv -> Val0 + pLits[0] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 1), a ); + pLits[1] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 2), a ); + pLits[2] = Abc_Var2Lit( Gia_KSatVarAnd(pMap, n), a ); + pLits[3] = Abc_Var2Lit( Gia_KSatVarInv(pMap, n), c ); + pLits[4] = Abc_Var2Lit( Gia_KSatVarMin(pMap, n, m, 0), a==c ); + Gia_SatDumpClause( vStr, pLits, 5 ); + } + } + // the number of nodes with duplicated fanins and without inv is maximized + if ( nBound && 2*nNodes > nBound ) { + Vec_StrPrintF( vStr, "k %d ", 2*nNodes-nBound ); + nLits = 0; + for ( n = nIns; n < nIns+nNodes; n++ ) { + pLits[nLits++] = Abc_Var2Lit(Gia_KSatVarEqu(pMap, n), 0); + pLits[nLits++] = Abc_Var2Lit(Gia_KSatVarInv(pMap, n), 1); + } + Gia_SatDumpClause( vStr, pLits, nLits ); + } + Vec_StrPush( vStr, '\0' ); + Vec_IntFreeP( &vRes ); + return vStr; +} + + +typedef enum { + GIA_GATE2_ZERO, // 0: + GIA_GATE2_ONE, // 1: + GIA_GATE2_BUF, // 2: + GIA_GATE2_INV, // 3: + GIA_GATE2_NAN2, // 4: + GIA_GATE2_NOR2, // 5: + GIA_GATE2_AOI21, // 6: + GIA_GATE2_NAN3, // 7: + GIA_GATE2_NOR3, // 8: + GIA_GATE2_OAI21, // 9: + GIA_GATE2_NOR4, // 10: + GIA_GATE2_AOI211, // 11: + GIA_GATE2_AOI22, // 12: + GIA_GATE2_NAN4, // 13: + GIA_GATE2_OAI211, // 14: + GIA_GATE2_OAI22, // 15: + GIA_GATE2_VOID // 16: unused value +} Gia_ManGate2_t; + +Vec_Int_t * Gia_ManDeriveKSatMappingArray( Gia_Man_t * p, Vec_Int_t * vRes ) +{ + Vec_Int_t * vMapping = Vec_IntStart( 2*Gia_ManObjNum(p) ); + int i, Id; Gia_Obj_t * pObj; + Gia_ManForEachCiId( p, Id, i ) + if ( Vec_IntEntry(vRes, Id) ) + Vec_IntWriteEntry( vMapping, Abc_Var2Lit(Id, 1), -1 ); + Gia_ManForEachAnd( p, pObj, i ) { + assert( Vec_IntEntry(vRes, i) > 0 ); + if ( (Vec_IntEntry(vRes, i) & 2) == 0 ) { + assert( (Vec_IntEntry(vRes, i) & 1) == 0 ); + continue; + } + Gia_Obj_t * pFans[2] = { Gia_ObjFanin0(pObj), Gia_ObjFanin1(pObj) }; + int fComp = ((Vec_IntEntry(vRes, i) >> 2) & 1) != 0; + int fFan0 = ((Vec_IntEntry(vRes, Gia_ObjFaninId0(pObj, i)) >> 1) & 1) == 0 && Gia_ObjIsAnd(pFans[0]); + int fFan1 = ((Vec_IntEntry(vRes, Gia_ObjFaninId1(pObj, i)) >> 1) & 1) == 0 && Gia_ObjIsAnd(pFans[1]); + if ( Vec_IntEntry(vRes, i) & 1 ) + Vec_IntWriteEntry( vMapping, Abc_Var2Lit(i, !fComp), -1 ); + Vec_IntWriteEntry( vMapping, Abc_Var2Lit(i, fComp), Vec_IntSize(vMapping) ); + if ( fFan0 && fFan1 ) { + Vec_IntPush( vMapping, 4 ); + if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) { + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) ); + } + else { + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) ); + } + if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) + Vec_IntPush( vMapping, fComp ? GIA_GATE2_OAI22 : GIA_GATE2_AOI22 ); + else if ( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) ) + Vec_IntPush( vMapping, fComp ? GIA_GATE2_NAN4 : GIA_GATE2_NOR4 ); + else + Vec_IntPush( vMapping, fComp ? GIA_GATE2_OAI211 : GIA_GATE2_AOI211 ); + } else if ( fFan0 ) { + Vec_IntPush( vMapping, 3 ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC0(pFans[0]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[0]), !(fComp ^ Gia_ObjFaninC0(pObj) ^ Gia_ObjFaninC1(pFans[0]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pObj), !(fComp ^ Gia_ObjFaninC1(pObj))) ); + if ( Gia_ObjFaninC0(pObj) ) + Vec_IntPush( vMapping, fComp ? GIA_GATE2_OAI21 : GIA_GATE2_AOI21 ); + else + Vec_IntPush( vMapping, fComp ? GIA_GATE2_NAN3 : GIA_GATE2_NOR3 ); + } else if ( fFan1 ) { + Vec_IntPush( vMapping, 3 ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC0(pFans[1]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pFans[1]), !(fComp ^ Gia_ObjFaninC1(pObj) ^ Gia_ObjFaninC1(pFans[1]))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pObj), !(fComp ^ Gia_ObjFaninC0(pObj))) ); + if ( Gia_ObjFaninC1(pObj) ) + Vec_IntPush( vMapping, fComp ? GIA_GATE2_OAI21 : GIA_GATE2_AOI21 ); + else + Vec_IntPush( vMapping, fComp ? GIA_GATE2_NAN3 : GIA_GATE2_NOR3 ); + } else { + Vec_IntPush( vMapping, 2 ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId0p(p, pObj), !(fComp ^ Gia_ObjFaninC0(pObj))) ); + Vec_IntPush( vMapping, Abc_Var2Lit(Gia_ObjFaninId1p(p, pObj), !(fComp ^ Gia_ObjFaninC1(pObj))) ); + Vec_IntPush( vMapping, fComp ? GIA_GATE2_NAN2 : GIA_GATE2_NOR2 ); + } + } + return vMapping; +} + +Gia_Man_t * Gia_ManDeriveKSatMapping( Vec_Int_t * vRes, int * pMap, int nIns, int nNodes, int fVerbose ) +{ + Vec_Int_t * vGuide = Vec_IntStart( 1000 ); + Gia_Man_t * pNew = Gia_ManStart( nIns + nNodes + 2 ); + pNew->pName = Abc_UtilStrsav( "test" ); + int i, nSave = 0, pCopy[256] = {0}; + for ( i = 1; i <= nIns; i++ ) + pCopy[i] = Gia_ManAppendCi( pNew ); + for ( i = nIns; i < nIns+nNodes; i++ ) { + int iFan0 = Gia_KSatFindFan( pMap, i, 0, vRes ); + int iFan1 = Gia_KSatFindFan( pMap, i, 1, vRes ); + if ( iFan0 == iFan1 ) + pCopy[i+1] = pCopy[iFan0+1]; + else if ( Gia_KSatValAnd(pMap, i, vRes) ) + pCopy[i+1] = Gia_ManAppendAnd( pNew, pCopy[iFan0+1], pCopy[iFan1+1] ); + else + pCopy[i+1] = Gia_ManAppendOr( pNew, pCopy[iFan0+1], pCopy[iFan1+1] ); + pCopy[i+1] = Abc_LitNotCond( pCopy[i+1], Gia_KSatValInv(pMap, i, vRes) ); + if ( iFan0 == iFan1 ) + *Vec_IntEntryP(vGuide, Abc_Lit2Var(pCopy[i+1])) ^= 1; + else if ( Gia_KSatValAnd(pMap, i, vRes) ) + *Vec_IntEntryP(vGuide, Abc_Lit2Var(pCopy[i+1])) ^= 4 | (2*Gia_KSatValInv(pMap, i, vRes)); + else + *Vec_IntEntryP(vGuide, Abc_Lit2Var(pCopy[i+1])) ^= 8 | (2*Gia_KSatValInv(pMap, i, vRes)); + if ( fVerbose ) { + if ( i == nIns+nNodes-1 ) + printf( " F = " ); + else + printf( "%2d = ", i ); + if ( iFan0 == iFan1 ) + printf( "INV( %d )\n", iFan0 ); + else if ( Gia_KSatValAnd(pMap, i, vRes) ) + printf( "%sAND( %d, %d )\n", Gia_KSatValInv(pMap, i, vRes) ? "N":"", iFan0, iFan1 ); + else + printf( "%sOR( %d, %d )\n", Gia_KSatValInv(pMap, i, vRes) ? "N":"", iFan0, iFan1 ); + nSave += (iFan0 == iFan1) || !Gia_KSatValInv(pMap, i, vRes); + if ( i == nIns+nNodes-1 ) + printf( "Solution cost = %d\n", 2*(2*nNodes - nSave) ); + } + } + Gia_ManAppendCo( pNew, pCopy[nIns+nNodes] ); + //pNew->vCellMapping = Gia_ManDeriveKSatMappingArray( pNew, vGuide ); + Vec_IntFree( vGuide ); + return pNew; +} + +word Gia_ManGetTruth( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; int i, Id; + word pFuncs[256] = {0}, Const[2] = {0, ~(word)0}; + assert( Gia_ManObjNum(p) <= 256 ); + Gia_ManForEachCiId( p, Id, i ) + pFuncs[Id] = s_Truths6[i]; + Gia_ManForEachAnd( p, pObj, i ) + pFuncs[i] = (Const[Gia_ObjFaninC0(pObj)] ^ pFuncs[Gia_ObjFaninId0(pObj, i)]) & (Const[Gia_ObjFaninC1(pObj)] ^ pFuncs[Gia_ObjFaninId1(pObj, i)]); + pObj = Gia_ManCo(p, 0); + return Const[Gia_ObjFaninC0(pObj)] ^ pFuncs[Gia_ObjFaninId0p(p, pObj)]; +} + +Gia_Man_t * Gia_ManKSatMapping( word Truth, int nIns, int nNodes, int nBound, int Seed, int fMultiLevel, int nBTLimit, int nTimeout, int fVerbose, int fKeepFile, int argc, char ** argv, char * pGuide ) +{ + abctime clkStart = Abc_Clock(); + Gia_Man_t * pNew = NULL; + srand(time(NULL)); + int Status, Rand = ((((unsigned)rand()) << 12) ^ ((unsigned)rand())) & 0xFFFFFF; + char pFileNameI[32]; sprintf( pFileNameI, "_%06x_.cnf", Rand ); + char pFileNameO[32]; sprintf( pFileNameO, "_%06x_.out", Rand ); + int nVars = 0, * pMap = Gia_KSatMapInit( nIns, nNodes, Truth, &nVars ); + Vec_Str_t * vStr = Gia_ManKSatCnf( pMap, nIns, nNodes, nBound/2, fMultiLevel, pGuide ); + if ( !Gia_ManDumpCnf(pFileNameI, vStr, nVars) ) { + Vec_StrFree( vStr ); + return NULL; + } + if ( fVerbose ) + printf( "Vars = %d. Nodes = %d. Cardinality bound = %d. SAT vars = %d. SAT clauses = %d. Conflict limit = %d. Timeout = %d.\n", + nIns, nNodes, nBound, nVars, Vec_StrCountEntry(vStr, '\n'), nBTLimit, nTimeout ); + Vec_Int_t * vRes = Gia_RunKadical( pFileNameI, pFileNameO, Seed, nBTLimit, nTimeout, 1, &Status ); + unlink( pFileNameI ); + //unlink( pFileNameO ); + if ( fKeepFile ) Gia_ManDumpCnf2( vStr, nVars, argc, argv, Abc_Clock() - clkStart, Status ); + Vec_StrFree( vStr ); + if ( vRes == NULL ) + return 0; + Vec_IntDrop( vRes, 0 ); + pNew = Gia_ManDeriveKSatMapping( vRes, pMap, nIns, nNodes, fVerbose ); + printf( "Verification %s. ", Truth == Gia_ManGetTruth(pNew) ? "passed" : "failed" ); + Abc_PrintTime( 0, "Total time", Abc_Clock() - clkStart ); + Vec_IntFree( vRes ); + ABC_FREE( pMap ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index 87614c490..b5c3c0802 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -3199,7 +3199,7 @@ Vec_Int_t * Gia_ManRelDeriveSimple( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_Int_t * vOuts, Vec_Int_t * vRel, Vec_Int_t * vDivs ) { - extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose ); + extern Mini_Aig_t * Exa4_ManGenTest( Vec_Wrd_t * vSimsIn, Vec_Wrd_t * vSimsOut, int nIns, int nDivs, int nOuts, int nNodes, int TimeOut, int fOnlyAnd, int fFancy, int fOrderNodes, int fUniqFans, int fVerbose, int fCard, char * pGuide ); int i, m, iObj, Entry, iMint = 0, nMints = Vec_IntSize(vRel) - Vec_IntCountEntry(vRel, -1); Vec_Wrd_t * vSimsIn = Vec_WrdStart( nMints ); @@ -3232,7 +3232,7 @@ void Gia_ManRelSolve( Gia_Man_t * p, Vec_Wrd_t * vSims, Vec_Int_t * vIns, Vec_In } assert( iMint == nMints ); printf( "Created %d minterms.\n", iMint ); - Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1 ); + Exa4_ManGenTest( vSimsIn, vSimsOut, Vec_IntSize(vIns), Vec_IntSize(vDivs), Vec_IntSize(vOuts), 10, 0, 0, 0, 0, 0, 1, 0, NULL ); Vec_WrdFree( vSimsIn ); Vec_WrdFree( vSimsOut ); } diff --git a/src/aig/saig/saigIso.c b/src/aig/saig/saigIso.c index 7ab8486e4..03ec21f3a 100644 --- a/src/aig/saig/saigIso.c +++ b/src/aig/saig/saigIso.c @@ -600,7 +600,7 @@ Aig_Man_t * Iso_ManTest888( Aig_Man_t * pAig1, int fVerbose ) Vec_Int_t * vMap; pNtk = Abc_NtkFromAigPhase( pAig1 ); - Abc_NtkPermute( pNtk, 1, 0, 1, NULL ); + Abc_NtkPermute( pNtk, 1, 0, 1, NULL, NULL, NULL ); pAig2 = Abc_NtkToDar( pNtk, 0, 1 ); Abc_NtkDelete( pNtk ); diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index ada1f499f..1d4bde4d7 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -792,7 +792,7 @@ extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateWithNodes( Vec_Ptr_t * vSops ); extern ABC_DLL void Abc_NtkDelete( Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkMakeComb( Abc_Ntk_t * pNtk, int fRemoveLatches ); -extern ABC_DLL void Abc_NtkPermute( Abc_Ntk_t * pNtk, int fInputs, int fOutputs, int fFlops, char * pFlopPermFile ); +extern ABC_DLL void Abc_NtkPermute( Abc_Ntk_t * pNtk, int fInputs, int fOutputs, int fFlops, char * pInPermFile, char * pOutPermFile, char * pFlopPermFile ); extern ABC_DLL void Abc_NtkUnpermute( Abc_Ntk_t * pNtk ); extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateFromSops( char * pName, Vec_Ptr_t * vSops ); extern ABC_DLL Abc_Ntk_t * Abc_NtkCreateFromGias( char * pName, Vec_Ptr_t * vGias, Gia_Man_t * pMulti ); diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index c9eeb79c6..c4dbb36ee 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -1727,6 +1727,58 @@ void Abc_NtkMakeSeq( Abc_Ntk_t * pNtk, int nLatchesToAdd ) } +/**Function************************************************************* + + Synopsis [Keeps POs in the array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkSelectPos( Abc_Ntk_t * pNtkInit, Vec_Int_t * vPoIds ) +{ + Abc_Ntk_t * pNtk; + Vec_Ptr_t * vPosLeft; + Vec_Ptr_t * vCosLeft; + Abc_Obj_t * pNodePo; + int i, Index; + assert( !Abc_NtkIsNetlist(pNtkInit) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtkInit) ); + pNtk = Abc_NtkDup( pNtkInit ); + if ( Abc_NtkPoNum(pNtk) == 1 ) + return pNtk; + vPosLeft = Vec_PtrAlloc( Vec_IntSize(vPoIds) ); + Vec_IntForEachEntry( vPoIds, Index, i ) { + Vec_PtrPush( vPosLeft, Abc_NtkPo(pNtk, Index) ); + Vec_PtrWriteEntry( pNtk->vPos, Index, NULL ); + } + // filter COs + vCosLeft = Vec_PtrDup( vPosLeft ); + for ( i = Abc_NtkPoNum(pNtk); i < Abc_NtkCoNum(pNtk); i++ ) + Vec_PtrPush( vCosLeft, Abc_NtkCo(pNtk, i) ); + // remove remaiing POs + Abc_NtkForEachPo( pNtk, pNodePo, i ) + if ( pNodePo ) + Abc_NtkDeleteObjPo( pNodePo ); + // update arrays + Vec_PtrFree( pNtk->vPos ); pNtk->vPos = vPosLeft; + Vec_PtrFree( pNtk->vCos ); pNtk->vCos = vCosLeft; + // clean the network + if ( Abc_NtkIsStrash(pNtk) ) { + Abc_AigCleanup( (Abc_Aig_t *)pNtk->pManFunc ); + if ( Abc_NtkLatchNum(pNtk) ) printf( "Run sequential cleanup (\"scl\") to get rid of dangling logic.\n" ); + } + else { + if ( Abc_NtkLatchNum(pNtk) ) printf( "Run sequential cleanup (\"st; scl\") to get rid of dangling logic.\n" ); + } + if ( !Abc_NtkCheck( pNtk ) ) + fprintf( stdout, "Abc_NtkMakeComb(): Network check has failed.\n" ); + return pNtk; +} + /**Function************************************************************* Synopsis [Removes all POs, except one.] @@ -1779,11 +1831,11 @@ Abc_Ntk_t * Abc_NtkMakeOnePo( Abc_Ntk_t * pNtkInit, int Output, int nRange ) if ( Abc_NtkIsStrash(pNtk) ) { Abc_AigCleanup( (Abc_Aig_t *)pNtk->pManFunc ); - printf( "Run sequential cleanup (\"scl\") to get rid of dangling logic.\n" ); + if ( Abc_NtkLatchNum(pNtk) ) printf( "Run sequential cleanup (\"scl\") to get rid of dangling logic.\n" ); } else { - printf( "Run sequential cleanup (\"st; scl\") to get rid of dangling logic.\n" ); + if ( Abc_NtkLatchNum(pNtk) ) printf( "Run sequential cleanup (\"st; scl\") to get rid of dangling logic.\n" ); } if ( !Abc_NtkCheck( pNtk ) ) @@ -2007,11 +2059,11 @@ void Abc_NtkRemovePo( Abc_Ntk_t * pNtk, int iOutput, int fRemoveConst0 ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Abc_NtkReadFlopPerm( char * pFileName, int nFlops ) +Vec_Int_t * Abc_NtkReadSignalPerm2( char * pFileName, int nSignals ) { char Buffer[1000]; FILE * pFile; - Vec_Int_t * vFlops; + Vec_Int_t * vSignals; int iFlop = -1; pFile = fopen( pFileName, "rb" ); if ( pFile == NULL ) @@ -2019,30 +2071,63 @@ Vec_Int_t * Abc_NtkReadFlopPerm( char * pFileName, int nFlops ) printf( "Cannot open input file \"%s\".\n", pFileName ); return NULL; } - vFlops = Vec_IntAlloc( nFlops ); + vSignals = Vec_IntAlloc( nSignals ); while ( fgets( Buffer, 1000, pFile ) != NULL ) { if ( Buffer[0] == ' ' || Buffer[0] == '\r' || Buffer[0] == '\n' ) continue; iFlop = atoi( Buffer ); - if ( iFlop < 0 || iFlop >= nFlops ) + if ( iFlop < 0 || iFlop >= nSignals ) { - printf( "Flop ID (%d) is out of range.\n", iFlop ); + printf( "The zero-based signal ID (%d) is out of range.\n", iFlop ); fclose( pFile ); - Vec_IntFree( vFlops ); + Vec_IntFree( vSignals ); return NULL; } - Vec_IntPush( vFlops, iFlop ); + Vec_IntPush( vSignals, iFlop ); } fclose( pFile ); - if ( Vec_IntSize(vFlops) != nFlops ) + if ( Vec_IntSize(vSignals) != nSignals ) { - printf( "The number of flops read in from file (%d) is different from the number of flops in the circuit (%d).\n", iFlop, nFlops ); - Vec_IntFree( vFlops ); + printf( "The number of indexes read in from file (%d) is different from the number of signals in the circuit (%d).\n", Vec_IntSize(vSignals), nSignals ); + Vec_IntFree( vSignals ); return NULL; } - return vFlops; + return vSignals; } + +Vec_Int_t * Abc_NtkReadSignalPerm( char * pFileName, int nSignals ) +{ + int Num = -1; + Vec_Int_t * vSignals; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open input file \"%s\".\n", pFileName ); + return NULL; + } + vSignals = Vec_IntAlloc( nSignals ); + while ( fscanf( pFile, "%d", &Num ) == 1 ) + { + if ( Num <= 0 || Num > nSignals ) + { + printf( "The one-based signal ID (%d) is out of range (%d).\n", Num, nSignals ); + fclose( pFile ); + Vec_IntFree( vSignals ); + return NULL; + } + Vec_IntPush( vSignals, Num-1 ); + } + fclose( pFile ); + if ( Vec_IntSize(vSignals) != nSignals ) + { + printf( "The number of indexes read in from file (%d) is different from the number of signals in the circuit (%d).\n", Vec_IntSize(vSignals), nSignals ); + Vec_IntFree( vSignals ); + return NULL; + } + return vSignals; +} + /**Function************************************************************* Synopsis [] @@ -2054,61 +2139,98 @@ Vec_Int_t * Abc_NtkReadFlopPerm( char * pFileName, int nFlops ) SeeAlso [] ***********************************************************************/ -void Abc_NtkPermute( Abc_Ntk_t * pNtk, int fInputs, int fOutputs, int fFlops, char * pFlopPermFile ) +void Abc_NtkPermute( Abc_Ntk_t * pNtk, int fInputs, int fOutputs, int fFlops, char * pInPermFile, char * pOutPermFile, char * pFlopPermFile ) { Abc_Obj_t * pTemp; Vec_Int_t * vInputs, * vOutputs, * vFlops, * vTemp; int i, k, Entry; // start permutation arrays + if ( pInPermFile ) + { + vInputs = Abc_NtkReadSignalPerm( pInPermFile, Abc_NtkPiNum(pNtk) ); + if ( vInputs == NULL ) + return; + fInputs = 1; + } + else + vInputs = Vec_IntStartNatural( Abc_NtkPiNum(pNtk) ); + if ( pOutPermFile ) + { + vOutputs = Abc_NtkReadSignalPerm( pOutPermFile, Abc_NtkPoNum(pNtk) ); + if ( vOutputs == NULL ) + return; + fOutputs = 1; + } + else + vOutputs = Vec_IntStartNatural( Abc_NtkPoNum(pNtk) ); if ( pFlopPermFile ) { - vFlops = Abc_NtkReadFlopPerm( pFlopPermFile, Abc_NtkLatchNum(pNtk) ); + vFlops = Abc_NtkReadSignalPerm( pFlopPermFile, Abc_NtkLatchNum(pNtk) ); if ( vFlops == NULL ) return; - fInputs = 0; - fOutputs = 0; - fFlops = 0; + fFlops = 1; } else vFlops = Vec_IntStartNatural( Abc_NtkLatchNum(pNtk) ); - vInputs = Vec_IntStartNatural( Abc_NtkPiNum(pNtk) ); - vOutputs = Vec_IntStartNatural( Abc_NtkPoNum(pNtk) ); // permute inputs + Vec_Ptr_t * vCis = Vec_PtrDup(pNtk->vCis); + Vec_Ptr_t * vCos = Vec_PtrDup(pNtk->vCos); + Vec_Ptr_t * vFfs = Vec_PtrDup(pNtk->vBoxes); if ( fInputs ) for ( i = 0; i < Abc_NtkPiNum(pNtk); i++ ) { - k = rand() % Abc_NtkPiNum(pNtk); - // swap indexes - Entry = Vec_IntEntry( vInputs, i ); - Vec_IntWriteEntry( vInputs, i, Vec_IntEntry(vInputs, k) ); - Vec_IntWriteEntry( vInputs, k, Entry ); - // swap PIs - pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vPis, i ); - Vec_PtrWriteEntry( pNtk->vPis, i, Vec_PtrEntry(pNtk->vPis, k) ); - Vec_PtrWriteEntry( pNtk->vPis, k, pTemp ); - // swap CIs - pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCis, i ); - Vec_PtrWriteEntry( pNtk->vCis, i, Vec_PtrEntry(pNtk->vCis, k) ); - Vec_PtrWriteEntry( pNtk->vCis, k, pTemp ); + if ( pInPermFile ) + { + k = Vec_IntEntry( vInputs, i ); + pTemp = (Abc_Obj_t *)Vec_PtrEntry( vCis, k ); + Vec_PtrWriteEntry( pNtk->vPis, i, pTemp ); + Vec_PtrWriteEntry( pNtk->vCis, i, pTemp ); + } + else + { + k = rand() % Abc_NtkPiNum(pNtk); + // swap indexes + Entry = Vec_IntEntry( vInputs, i ); + Vec_IntWriteEntry( vInputs, i, Vec_IntEntry(vInputs, k) ); + Vec_IntWriteEntry( vInputs, k, Entry ); + // swap PIs + pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vPis, i ); + Vec_PtrWriteEntry( pNtk->vPis, i, Vec_PtrEntry(pNtk->vPis, k) ); + Vec_PtrWriteEntry( pNtk->vPis, k, pTemp ); + // swap CIs + pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCis, i ); + Vec_PtrWriteEntry( pNtk->vCis, i, Vec_PtrEntry(pNtk->vCis, k) ); + Vec_PtrWriteEntry( pNtk->vCis, k, pTemp ); + } //printf( "Swapping PIs %d and %d.\n", i, k ); } // permute outputs if ( fOutputs ) for ( i = 0; i < Abc_NtkPoNum(pNtk); i++ ) { - k = rand() % Abc_NtkPoNum(pNtk); - // swap indexes - Entry = Vec_IntEntry( vOutputs, i ); - Vec_IntWriteEntry( vOutputs, i, Vec_IntEntry(vOutputs, k) ); - Vec_IntWriteEntry( vOutputs, k, Entry ); - // swap POs - pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vPos, i ); - Vec_PtrWriteEntry( pNtk->vPos, i, Vec_PtrEntry(pNtk->vPos, k) ); - Vec_PtrWriteEntry( pNtk->vPos, k, pTemp ); - // swap COs - pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCos, i ); - Vec_PtrWriteEntry( pNtk->vCos, i, Vec_PtrEntry(pNtk->vCos, k) ); - Vec_PtrWriteEntry( pNtk->vCos, k, pTemp ); + if ( pOutPermFile ) + { + k = Vec_IntEntry( vOutputs, i ); + pTemp = (Abc_Obj_t *)Vec_PtrEntry( vCos, k ); + Vec_PtrWriteEntry( pNtk->vPos, i, pTemp ); + Vec_PtrWriteEntry( pNtk->vCos, i, pTemp ); + } + else + { + k = rand() % Abc_NtkPoNum(pNtk); + // swap indexes + Entry = Vec_IntEntry( vOutputs, i ); + Vec_IntWriteEntry( vOutputs, i, Vec_IntEntry(vOutputs, k) ); + Vec_IntWriteEntry( vOutputs, k, Entry ); + // swap POs + pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vPos, i ); + Vec_PtrWriteEntry( pNtk->vPos, i, Vec_PtrEntry(pNtk->vPos, k) ); + Vec_PtrWriteEntry( pNtk->vPos, k, pTemp ); + // swap COs + pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCos, i ); + Vec_PtrWriteEntry( pNtk->vCos, i, Vec_PtrEntry(pNtk->vCos, k) ); + Vec_PtrWriteEntry( pNtk->vCos, k, pTemp ); + } //printf( "Swapping POs %d and %d.\n", i, k ); } // permute flops @@ -2116,26 +2238,42 @@ void Abc_NtkPermute( Abc_Ntk_t * pNtk, int fInputs, int fOutputs, int fFlops, ch if ( fFlops ) for ( i = 0; i < Abc_NtkLatchNum(pNtk); i++ ) { - k = rand() % Abc_NtkLatchNum(pNtk); - // swap indexes - Entry = Vec_IntEntry( vFlops, i ); - Vec_IntWriteEntry( vFlops, i, Vec_IntEntry(vFlops, k) ); - Vec_IntWriteEntry( vFlops, k, Entry ); - // swap flops - pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vBoxes, i ); - Vec_PtrWriteEntry( pNtk->vBoxes, i, Vec_PtrEntry(pNtk->vBoxes, k) ); - Vec_PtrWriteEntry( pNtk->vBoxes, k, pTemp ); - // swap CIs - pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCis, Abc_NtkPiNum(pNtk)+i ); - Vec_PtrWriteEntry( pNtk->vCis, Abc_NtkPiNum(pNtk)+i, Vec_PtrEntry(pNtk->vCis, Abc_NtkPiNum(pNtk)+k) ); - Vec_PtrWriteEntry( pNtk->vCis, Abc_NtkPiNum(pNtk)+k, pTemp ); - // swap COs - pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCos, Abc_NtkPoNum(pNtk)+i ); - Vec_PtrWriteEntry( pNtk->vCos, Abc_NtkPoNum(pNtk)+i, Vec_PtrEntry(pNtk->vCos, Abc_NtkPoNum(pNtk)+k) ); - Vec_PtrWriteEntry( pNtk->vCos, Abc_NtkPoNum(pNtk)+k, pTemp ); + if ( pFlopPermFile ) + { + k = Vec_IntEntry( vFlops, i ); + pTemp = (Abc_Obj_t *)Vec_PtrEntry( vFfs, k ); + Vec_PtrWriteEntry( pNtk->vBoxes, i, pTemp ); + pTemp = (Abc_Obj_t *)Vec_PtrEntry( vCis, Abc_NtkPiNum(pNtk)+k ); + Vec_PtrWriteEntry( pNtk->vCis, Abc_NtkPiNum(pNtk)+i, pTemp ); + pTemp = (Abc_Obj_t *)Vec_PtrEntry( vCos, Abc_NtkPoNum(pNtk)+k ); + Vec_PtrWriteEntry( pNtk->vCos, Abc_NtkPoNum(pNtk)+i, pTemp ); + } + else + { + k = rand() % Abc_NtkLatchNum(pNtk); + // swap indexes + Entry = Vec_IntEntry( vFlops, i ); + Vec_IntWriteEntry( vFlops, i, Vec_IntEntry(vFlops, k) ); + Vec_IntWriteEntry( vFlops, k, Entry ); + // swap flops + pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vBoxes, i ); + Vec_PtrWriteEntry( pNtk->vBoxes, i, Vec_PtrEntry(pNtk->vBoxes, k) ); + Vec_PtrWriteEntry( pNtk->vBoxes, k, pTemp ); + // swap CIs + pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCis, Abc_NtkPiNum(pNtk)+i ); + Vec_PtrWriteEntry( pNtk->vCis, Abc_NtkPiNum(pNtk)+i, Vec_PtrEntry(pNtk->vCis, Abc_NtkPiNum(pNtk)+k) ); + Vec_PtrWriteEntry( pNtk->vCis, Abc_NtkPiNum(pNtk)+k, pTemp ); + // swap COs + pTemp = (Abc_Obj_t *)Vec_PtrEntry( pNtk->vCos, Abc_NtkPoNum(pNtk)+i ); + Vec_PtrWriteEntry( pNtk->vCos, Abc_NtkPoNum(pNtk)+i, Vec_PtrEntry(pNtk->vCos, Abc_NtkPoNum(pNtk)+k) ); + Vec_PtrWriteEntry( pNtk->vCos, Abc_NtkPoNum(pNtk)+k, pTemp ); + } //printf( "Swapping flops %d and %d.\n", i, k ); } + Vec_PtrFree(vCis); + Vec_PtrFree(vCos); + Vec_PtrFree(vFfs); // invert arrays vInputs = Vec_IntInvert( vTemp = vInputs, -1 ); Vec_IntFree( vTemp ); diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c index f24c55593..adc1639a6 100644 --- a/src/base/abc/abcSop.c +++ b/src/base/abc/abcSop.c @@ -21,6 +21,11 @@ #include "abc.h" #include "bool/kit/kit.h" +#ifdef _MSC_VER +# include +# define __builtin_popcount __popcnt +#endif + ABC_NAMESPACE_IMPL_START @@ -1135,6 +1140,31 @@ Vec_Ptr_t * Abc_SopFromTruthsHex( char * pTruth ) return vRes; } +Vec_Ptr_t * Abc_SopGenerateCounters( int nVars ) +{ + int m, i, o, nOuts = Abc_Base2Log( nVars + 1 ); + Vec_Ptr_t * vRes = Vec_PtrAlloc( nOuts ); + for ( o = 0; o < nOuts; o++ ) + { + Vec_Str_t * vStr = Vec_StrAlloc( 1000 ); + for ( m = 0; m < (1 << nVars); m++ ) { + int nOnes = __builtin_popcount(m); + if ( !((nOnes >> o) & 1) ) + continue; + for ( i = 0; i < nVars; i++ ) + Vec_StrPush( vStr, ((m >> i) & 1) ? '1' : '0' ); + Vec_StrPush( vStr, ' ' ); + Vec_StrPush( vStr, '1' ); + Vec_StrPush( vStr, '\n' ); + } + Vec_StrPush( vStr, '\0' ); + //printf( "%s\n", Vec_StrArray(vStr) ); + Vec_PtrPush( vRes, Vec_StrReleaseArray(vStr) ); + Vec_StrFree( vStr ); + } + return vRes; +} + /**Function************************************************************* Synopsis [Creates one encoder node.] diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 88a16e7b6..fddc04beb 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -24,6 +24,7 @@ #include "bool/dec/dec.h" #include "opt/fxu/fxu.h" #include "aig/miniaig/ndr.h" +#include "misc/util/utilTruth.h" #ifdef ABC_USE_CUDD #include "bdd/extrab/extraBdd.h" @@ -3352,6 +3353,211 @@ Abc_Ntk_t * Abc_NtkFromArray() return pNtkNew; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_PrintAT( Vec_Int_t * vRanks ) +{ + int i, Entry; + Vec_IntForEachEntryReverse( vRanks, Entry, i ) + if ( Entry == 0 ) + printf( " " ); + else + printf( "%4d", Entry ); + //printf( "\n" ); +} +int Abc_NtkMatchGpcPattern( Vec_Int_t * vRanks, int i, char * pGPC ) +{ + int k, Cur, Min = ABC_INFINITY; + for ( k = 0; pGPC[k] != ':' && i+k < Vec_IntSize(vRanks); k++ ) { + if ( Abc_TtReadHexDigit(pGPC[k]) == 0 ) + continue; + Cur = Vec_IntEntry(vRanks, i+k) / Abc_TtReadHexDigit(pGPC[k]); + if ( Min > Cur ) + Min = Cur; + } + return Min; +} +void Abc_NtkUpdateGpcPattern( Vec_Int_t * vRank, int i, char * pGPC, int nGpcs, Vec_Int_t * vRank2, Vec_Int_t * vLevel ) +{ + int k; char * pOut = strstr(pGPC, ":"); + assert( pOut && pOut[0] == ':' ); + pOut++; + Vec_IntAddToEntry( vLevel, i, nGpcs ); + for ( k = 0; pGPC[k] != ':'; k++ ) + Vec_IntAddToEntry( vRank, i+k, -nGpcs * Abc_TtReadHexDigit(pGPC[k]) ); + for ( k = 0; pOut[k] != ':'; k++ ) + Vec_IntAddToEntry( vRank2, i+k, nGpcs * Abc_TtReadHexDigit(pOut[k]) ); +} +int Abc_NtkGetGpcLutCount( char * pGPC ) +{ + char * pOut = strstr(pGPC, ":"); + char * pLut = strstr(pOut+1, ":"); + return atoi(pLut+1); +} +static inline int Vec_WecSum( Vec_Wec_t * p ) +{ + Vec_Int_t * vVec; + int i, Counter = 0; + Vec_WecForEachLevel( p, vVec, i ) + Counter += Vec_IntSum(vVec); + return Counter; +} +char ** Abc_NtkTransformGPCs( char ** pGPCs, int nGPCs ) +{ + char * pOut, * pLut, ** pRes = ABC_ALLOC( char *, nGPCs ); + int i, k, nLength; + for ( i = 0; i < nGPCs; i++ ) { + pRes[i] = Abc_UtilStrsav(pGPCs[i]); + pOut = strstr(pRes[i], ":"); + nLength = (int)(pOut-pRes[i]); + for ( k = 0; k < nLength/2; k++ ) + ABC_SWAP( char, pRes[i][k], pRes[i][nLength-1-k] ) + pLut = strstr(pOut+1, ":"); + nLength = (int)(pLut-pOut-1); + for ( k = 0; k < nLength/2; k++ ) + ABC_SWAP( char, pOut[1+k], pOut[1+nLength-1-k] ) + } + return pRes; +} +int Abc_NtkCheckGpc( char * pGPC, char * pGPC0 ) +{ + int RetValue = 0, k, Sum[2] = {0}; + char * pOut = strstr(pGPC, ":"); + for ( k = 0; pGPC[k] != ':'; k++ ) + Sum[0] += (1 << k) * Abc_TtReadHexDigit(pGPC[k]); + for ( k = 0; pOut[1+k] != ':'; k++ ) + Sum[1] += (1 << k) * Abc_TtReadHexDigit(pOut[1+k]); + //printf( "GPC %s has input sum %d and output sum %d\n", pGPC0, Sum[0], Sum[1] ); + if ( Sum[0]+1 > (1 << Abc_Base2Log(Sum[1]+1)) ) + printf( "The largest value of GPC inputs (%d) exceeds the capacity of outputs (%d) for GPC %s.\n", Sum[0], Sum[1], pGPC0 ); + else if ( Sum[1]+1 > (1 << Abc_Base2Log(Sum[0]+1)) ) + printf( "The largest value of GPC outputs (%d) exceeds the capacity of inputs (%d) for GPC %s.\n", Sum[1], Sum[0], pGPC0 ); + else + RetValue = 1; + return RetValue; +} +void Abc_NtkATMap( int nXVars, int nYVars, int nAdder, char ** pGPCs0, int nGPCs, int fReturn, int fVerbose ) +{ + abctime clkStart = Abc_Clock(); + char ** pGPCs = Abc_NtkTransformGPCs(pGPCs0, nGPCs); + int i, nGPCluts[100] = {0}; + for ( i = 0; i < nGPCs; i++ ) + if ( !Abc_NtkCheckGpc(pGPCs[i], pGPCs0[i]) ) + return; + for ( i = 0; i < nGPCs; i++ ) + nGPCluts[i] = Abc_NtkGetGpcLutCount(pGPCs[i]); + int x, n, Entry, iLevel = 0, Sum = 0, nGpcs = 0, nBits, fFinished, nRcaLuts = 0, nLuts = 0; + for ( x = 0; x < nXVars; x++ ) + Sum += (1 << x) * nYVars; + nBits = Abc_Base2Log( Sum+1 ); + printf( "Rectangular adder tree (X=%d Y=%d Sum=%d Out=%d) mapped with", nXVars, nYVars, Sum, nBits ); + for ( i = 0; i < nGPCs; i++ ) + printf( " GPC%d=%s", i, pGPCs0[i] ); + printf( "\n" ); + Vec_Int_t * vLevel; + Vec_Int_t * vRank[3] = { Vec_IntAlloc(100), Vec_IntAlloc(100), Vec_IntAlloc(100) }; + Vec_Wec_t ** vGPCs = ABC_ALLOC( Vec_Wec_t *, nGPCs ); + for ( i = 0; i < nGPCs; i++ ) + vGPCs[i] = Vec_WecAlloc(100); + Vec_IntFill( vRank[0], nBits, 0 ); + for ( x = 0; x < nXVars; x++ ) + Vec_IntAddToEntry( vRank[0], x, nYVars ); + if ( fVerbose ) { + printf( "Ranks: " ); + for ( i = nBits-1; i >= 0; i-- ) + printf( "%4d", i ); + printf( " : " ); + for ( i = nBits-1; i >= 0; i-- ) + printf( "%4d", i ); + printf( " LUT6\n" ); + } + for ( n = 0; n < nGPCs; n++ ) + for ( i = 0, fFinished = 0; !fFinished; i++ ) + { + int fAdded = 0; + vLevel = Vec_WecPushLevel( vGPCs[n] ); + Vec_IntFill( vLevel, nBits, 0 ); + Vec_IntFill( vRank[1], nBits, 0 ); + Vec_IntClear( vRank[2] ); + Vec_IntAppend( vRank[2], vRank[0] ); + fFinished = 1; + if ( Vec_IntFindMax(vRank[0]) > nAdder ) { + for ( x = 0; x < nBits; x++ ) + if ( (nGpcs = Abc_NtkMatchGpcPattern(vRank[0], x, pGPCs[n])) ) + Abc_NtkUpdateGpcPattern(vRank[0], x, pGPCs[n], nGpcs, vRank[1], vLevel), fFinished = 0, fAdded = 1; + nLuts += Vec_IntSum(vLevel) * nGPCluts[n]; + Vec_IntForEachEntry( vRank[1], Entry, x ) + Vec_IntAddToEntry( vRank[0], x, Entry ); + } + if ( fVerbose && (fAdded || Vec_IntFindMax(vRank[2]) <= nAdder ) ) { + printf( "Lev%02d: ", iLevel++ ); + Abc_PrintAT( vRank[2] ); + if ( fAdded ) { + printf( " GPC%d: ", n ); + Abc_PrintAT( vLevel ); + printf( " %4d", Vec_IntSum(vLevel) * nGPCluts[n] ); + } + else if ( Vec_IntFindMax(vRank[2]) <= nAdder ) { + printf( " ADD%d: ", nAdder ); + for ( x = 0; x < nBits; x++ ) + if ( Vec_IntEntry(vRank[2], x) > 1 ) + break; + for ( i = nBits-1; i >= x; i-- ) + printf( "%4d", 1 ); + for ( ; i >= 0; i-- ) + printf( " " ); + printf( " %4d", (nBits-x)*(nAdder == 4 ? 2 : 1) ); + } + printf( "\n" ); + } + if ( fAdded ) { + if ( fReturn ) { + fFinished = 1; + n = -1; + } + } + else if ( Vec_IntFindMax(vRank[2]) <= nAdder ) { + fFinished = 1; + n = nGPCs; + } + } + if ( Vec_IntFindMax(vRank[0]) > nAdder ) + printf( "Synthesis of the adder tree is incomplete. Try using the full adder \"3:11:1\" as the last GPC.\n" ); + else if ( fVerbose && Vec_IntFindMax(vRank[0]) <= nAdder ) { + printf( "Lev%02d: ", iLevel++ ); + for ( i = nBits-1; i >= 0; i-- ) + printf( "%4d", 1 ); + printf( "\n" ); + } + printf( "Statistics: " ); + for ( n = 0; n < nGPCs; n++ ) + printf( "GPC%d = %d. ", n, Vec_WecSum(vGPCs[n]) ); + for ( x = 0; x < nBits; x++ ) + if ( Vec_IntEntry(vRank[0], x) > 1 ) + break; + nRcaLuts = (nBits-x)*(nAdder == 4 ? 2 : 1); + printf( "ADD%d = %d. ", nAdder, nRcaLuts ); + printf( "Total LUT count = %d. ", nLuts+nRcaLuts ); + for ( i = 0; i < 3; i++ ) + Vec_IntFree( vRank[i] ); + for ( i = 0; i < nGPCs; i++ ) + Vec_WecFree( vGPCs[i] ); + ABC_FREE( vGPCs ); + for ( i = 0; i < nGPCs; i++ ) + ABC_FREE( pGPCs[i] ); + ABC_FREE( pGPCs ); + Abc_PrintTime( 0, "Total time", Abc_Clock() - clkStart ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c126df352..6db456e5c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -65,6 +65,7 @@ #include "opt/nwk/nwkMerge.h" #include "base/acb/acbPar.h" #include "misc/extra/extra.h" +#include "opt/eslim/eSLIM.h" #ifndef _WIN32 @@ -140,6 +141,8 @@ static int Abc_CommandTestDec ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandTestNpn ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestRPO ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestTruth ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTestSupp ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTestRand ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunEco ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -340,6 +343,7 @@ static int Abc_CommandClockGate ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandExtWin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandInsWin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSymFun ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandATMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPermute ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandUnpermute ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCubeEnum ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -513,6 +517,7 @@ static int Abc_CommandAbc9Mf ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Nf ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Of ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Simap ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Exmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Pack ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Edge ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9SatLut ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -549,6 +554,7 @@ static int Abc_CommandAbc9Mesh ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Iso ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9IsoNpn ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9IsoSt ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Store ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Compare ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9RevEng ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Uif ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -636,6 +642,8 @@ static int Abc_CommandAbc9MulFind ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9eSLIM ( Abc_Frame_t * pAbc, int argc, char ** argv ); + extern int Abc_CommandAbcLivenessToSafety ( Abc_Frame_t * pAbc, int argc, char ** argv ); extern int Abc_CommandAbcLivenessToSafetySim ( Abc_Frame_t * pAbc, int argc, char ** argv ); extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -949,6 +957,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "testnpn", Abc_CommandTestNpn, 0 ); Cmd_CommandAdd( pAbc, "LogiCS", "testrpo", Abc_CommandTestRPO, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "testtruth", Abc_CommandTestTruth, 0 ); + Cmd_CommandAdd( pAbc, "Synthesis", "testsupp", Abc_CommandTestSupp, 0 ); + Cmd_CommandAdd( pAbc, "Synthesis", "testrand", Abc_CommandTestRand, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "runsat", Abc_CommandRunSat, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "runeco", Abc_CommandRunEco, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "rungen", Abc_CommandRunGen, 0 ); @@ -1145,6 +1155,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Sequential", "extwin", Abc_CommandExtWin, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "inswin", Abc_CommandInsWin, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "symfun", Abc_CommandSymFun, 0 ); + Cmd_CommandAdd( pAbc, "Sequential", "atmap", Abc_CommandATMap, 0 ); Cmd_CommandAdd( pAbc, "Sequential", "permute", Abc_CommandPermute, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "unpermute", Abc_CommandUnpermute, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "cubeenum", Abc_CommandCubeEnum, 0 ); @@ -1321,6 +1332,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&nf", Abc_CommandAbc9Nf, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&of", Abc_CommandAbc9Of, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&simap", Abc_CommandAbc9Simap, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&exmap", Abc_CommandAbc9Exmap, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&pack", Abc_CommandAbc9Pack, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&edge", Abc_CommandAbc9Edge, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&satlut", Abc_CommandAbc9SatLut, 0 ); @@ -1357,6 +1369,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&iso", Abc_CommandAbc9Iso, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&isonpn", Abc_CommandAbc9IsoNpn, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&isost", Abc_CommandAbc9IsoSt, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&store", Abc_CommandAbc9Store, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&compare", Abc_CommandAbc9Compare, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reveng", Abc_CommandAbc9RevEng, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&uif", Abc_CommandAbc9Uif, 0 ); @@ -1449,6 +1462,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&mulfind", Abc_CommandAbc9MulFind, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); + + Cmd_CommandAdd( pAbc, "ABC9", "&eslim", Abc_CommandAbc9eSLIM, 0 ); { // extern Mf_ManTruthCount(); // Mf_ManTruthCount(); @@ -7256,6 +7271,130 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTestSupp( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Abc_NtkSuppMinFile( char * pFileName ); + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + { + Abc_Print( 1,"Input file is not given.\n" ); + return 0; + } + Abc_NtkSuppMinFile( argv[globalUtilOptind] ); + return 0; + +usage: + Abc_Print( -2, "usage: testsupp [-vh] \n" ); + Abc_Print( -2, "\t reads truth tables from file and support-minimizes them\n" ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : file to read the truth tables from\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandTestRand( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Abc_NtkRandFile( char * pFileName, int nVars, int nFuncs, int nMints ); + int c, nVars = 0, nFuncs = 0, nMints = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NFMvh" ) ) != EOF ) + { + switch ( c ) + { + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nVars = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nVars < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFuncs = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + nMints = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + { + Abc_Print( 1,"Input file is not given.\n" ); + return 0; + } + Abc_NtkRandFile( argv[globalUtilOptind], nVars, nFuncs, nMints ); + return 0; + +usage: + Abc_Print( -2, "usage: testrand [-NFMvh] \n" ); + Abc_Print( -2, "\t generates truth tables and writes them into a file\n" ); + Abc_Print( -2, "\t-N : the number of input variables [default = %d]\n", nVars ); + Abc_Print( -2, "\t-F : the number of random functions to generate [default = %d]\n", nFuncs ); + Abc_Print( -2, "\t-M : the number of positive minterms in the random function [default = %d]\n", nMints ); + Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : file to write the truth tables to\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -8918,10 +9057,11 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Abc_Ntk_t * Abc_NtkLutCascadeGen( int nLutSize, int nStages, int nRails, int nShared, int fVerbose ); extern Abc_Ntk_t * Abc_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nLuts, int nRails, int nIters, int fVerbose, char * pGuide ); - Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; char * pGuide = NULL; - int c, nLutSize = 6, nStages = 8, nRails = 1, nShared = 2, nIters = 1, fGen = 0, fVerbose = 0; + extern void Abc_NtkLutCascadeFile( char * pFileName, int nVarNum, int nLutSize, int nLuts, int nRails, int nIters, int fVerbose, int fVeryVerbose ); + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; char * pGuide = NULL, * pFileName = NULL; + int c, nVarNum = -1, nLutSize = 6, nStages = 8, nRails = 1, nShared = 2, nIters = 10, fGen = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KMRSIgvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KMRSINFgvwh" ) ) != EOF ) { switch ( c ) { @@ -8980,18 +9120,51 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nIters < 0 ) goto usage; break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nVarNum = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nVarNum < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" ); + goto usage; + } + pFileName = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'g': fGen ^= 1; break; case 'v': fVerbose ^= 1; break; + case 'w': + fVeryVerbose ^= 1; + break; case 'h': goto usage; default: goto usage; } } + if ( pFileName ) + { + if ( nVarNum == -1 ) + { + Abc_Print( -1, "The number of variables should be given on the command line using switch \"-N \".\n" ); + return 1; + } + Abc_NtkLutCascadeFile( pFileName, nVarNum, nLutSize, nStages, nRails, nIters, fVerbose, fVeryVerbose ); + return 1; + } if ( fGen ) { pNtkRes = Abc_NtkLutCascadeGen( nLutSize, nStages, nRails, nShared, fVerbose ); @@ -9003,7 +9176,6 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); return 0; } - if ( pNtk == NULL ) { Abc_Print( -1, "Empty network.\n" ); @@ -9037,15 +9209,18 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutcasdec [-KMRSI ] [-vh]\n" ); + Abc_Print( -2, "usage: lutcasdec [-KMRSIN ] [-F ] [-vwh]\n" ); Abc_Print( -2, "\t decomposes the primary output functions into LUT cascades\n" ); Abc_Print( -2, "\t-K : the number of LUT inputs [default = %d]\n", nLutSize ); Abc_Print( -2, "\t-M : the maximum delay (the number of stages) [default = %d]\n", nStages ); Abc_Print( -2, "\t-R : the number of direct connections (rails) [default = %d]\n", nRails ); Abc_Print( -2, "\t-S : the number of shared variables in each stage [default = %d]\n", nShared ); Abc_Print( -2, "\t-I : the number of iterations when looking for a solution [default = %d]\n", nIters ); + Abc_Print( -2, "\t-N : the number of support variables (for truth table files only) [default = unused]\n" ); + Abc_Print( -2, "\t-F : a text file with truth tables in hexadecimal listed one per line\n"); Abc_Print( -2, "\t-g : toggle generating random cascade with these parameters [default = %s]\n", fGen? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle additional verbose printout [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -10059,7 +10234,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INTGabdconugklvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INTGSabdconugklmvh" ) ) != EOF ) { switch ( c ) { @@ -10107,6 +10282,15 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( GateSize < 0 ) goto usage; break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by a file name.\n" ); + goto usage; + } + pPars->pGuide = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'a': pPars->fOnlyAnd ^= 1; break; @@ -10137,6 +10321,9 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'l': fKissat2 ^= 1; break; + case 'm': + pPars->fCard ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -10177,7 +10364,7 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( fUseNands ) Exa_ManExactSynthesis7( pPars, GateSize ); - else if ( fKissat ) + else if ( fKissat || pPars->fCard ) Exa_ManExactSynthesis4( pPars ); else if ( fKissat2 ) Exa_ManExactSynthesis5( pPars ); @@ -10188,12 +10375,13 @@ int Abc_CommandTwoExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: twoexact [-INTG ] [-abdconugklvh] \n" ); + Abc_Print( -2, "usage: twoexact [-INTG ] [-S str] [-abdconugklmvh] \n" ); Abc_Print( -2, "\t exact synthesis of multi-input function using two-input gates\n" ); Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N : the number of two-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); Abc_Print( -2, "\t-G : the largest allowed gate size (NANDs only) [default = %d]\n", GateSize ); + Abc_Print( -2, "\t-S : structural guidance from the user [default = %s]\n", pPars->pGuide ? pPars->pGuide : "unknown" ); Abc_Print( -2, "\t-a : toggle using only AND-gates (without XOR-gates) [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); Abc_Print( -2, "\t-b : toggle using only NAND-gates [default = %s]\n", fUseNands ? "yes" : "no" ); Abc_Print( -2, "\t-d : toggle using dynamic constraint addition [default = %s]\n", pPars->fDynConstr ? "yes" : "no" ); @@ -10204,6 +10392,7 @@ usage: Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" ); Abc_Print( -2, "\t-k : toggle using Kissat by Armin Biere [default = %s]\n", fKissat ? "yes" : "no" ); Abc_Print( -2, "\t-l : toggle using Kissat by Armin Biere [default = %s]\n", fKissat2 ? "yes" : "no" ); + Abc_Print( -2, "\t-m : toggle using CaDiCaL by Armin Biere [default = %s]\n", pPars->fCard ? "yes" : "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" ); Abc_Print( -2, "\t-h : print the command usage\n" ); Abc_Print( -2, "\t : truth table in hex notation\n" ); @@ -10236,7 +10425,7 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INKTSRMiaocgvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INKTSFMiaocgvh" ) ) != EOF ) { switch ( c ) { @@ -10293,10 +10482,10 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pSymStr = argv[globalUtilOptind]; globalUtilOptind++; break; - case 'R': + case 'F': if ( globalUtilOptind >= argc ) { - Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } pPars->nRandFuncs = atoi(argv[globalUtilOptind]); @@ -10378,13 +10567,13 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutexact [-INKTRM ] [-S string] [-iaocgvh] \n" ); + Abc_Print( -2, "usage: lutexact [-INKTFM ] [-S string] [-iaocgvh] \n" ); Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N : the number of K-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-K : the number of node fanins [default = %d]\n", pPars->nLutSize ); Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); - Abc_Print( -2, "\t-R : the number of random functions to try [default = unused]\n" ); + Abc_Print( -2, "\t-F : the number of random functions to try [default = unused]\n" ); Abc_Print( -2, "\t-M : the number of positive minterms in the random function [default = unused]\n" ); Abc_Print( -2, "\t-S : charasteristic string of a symmetric function [default = %d]\n", pPars->pSymStr ); Abc_Print( -2, "\t-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" ); @@ -13074,6 +13263,16 @@ usage: return 1; } +Vec_Int_t * Vec_IntReadList( char * pStr, char Separ ) +{ + Vec_Int_t * vRes = Vec_IntAlloc( 10 ); + Vec_IntPush( vRes, atoi(pStr) ); + for ( int c = 0; c < strlen(pStr); c++ ) + if ( pStr[c] == Separ ) + Vec_IntPush( vRes, atoi(pStr+c+1) ); + return vRes; +} + /**Function************************************************************* Synopsis [] @@ -13089,24 +13288,23 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk, * pNtkRes; Abc_Obj_t * pNode, * pNodeCo; + Vec_Int_t * vPoIds = NULL; int c; int fUseAllCis; int fUseMffc; - int fSeq; int Output; int nRange; - extern Abc_Ntk_t * Abc_NtkMakeOnePo( Abc_Ntk_t * pNtk, int Output, int nRange ); + extern Abc_Ntk_t * Abc_NtkSelectPos( Abc_Ntk_t * pNtkInit, Vec_Int_t * vPoIds ); pNtk = Abc_FrameReadNtk(pAbc); // set defaults fUseAllCis = 0; fUseMffc = 0; - fSeq = 0; Output = -1; nRange = -1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ORmash" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ORNmah" ) ) != EOF ) { switch ( c ) { @@ -13132,15 +13330,23 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nRange < 0 ) goto usage; break; + case 'N': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + vPoIds = Vec_IntReadList( argv[globalUtilOptind], ',' ); + globalUtilOptind++; + if ( vPoIds == NULL ) + goto usage; + break; case 'm': fUseMffc ^= 1; break; case 'a': fUseAllCis ^= 1; break; - case 's': - fSeq ^= 1; - break; case 'h': goto usage; default: @@ -13180,27 +13386,60 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv ) else pNtkRes = Abc_NtkCreateCone( pNtk, pNode, argv[globalUtilOptind], fUseAllCis ); } + else if ( vPoIds ) + { + pNtkRes = Abc_NtkSelectPos( pNtk, vPoIds ); + Vec_IntFree( vPoIds ); + } + else if ( nRange > 0 ) + { + if ( Output == -1 ) + { + Abc_Print( -1, "The starting PO ID is not specified.\n" ); + return 1; + } + if ( Output >= Abc_NtkPoNum(pNtk) ) + { + Abc_Print( -1, "The 0-based output number (%d) is larger than the number of primary outputs (%d).\n", Output, Abc_NtkPoNum(pNtk) ); + return 1; + } assert( vPoIds == NULL ); + vPoIds = Vec_IntAlloc( nRange ); + for ( c = Output; c < Output + nRange; c++ ) + Vec_IntPush( vPoIds, c ); + pNtkRes = Abc_NtkSelectPos( pNtk, vPoIds ); + Vec_IntFree( vPoIds ); + } + else if ( Output >= 0 ) + { + if ( Output >= Abc_NtkPoNum(pNtk) ) + { + Abc_Print( -1, "The 0-based output number (%d) is larger than the number of primary outputs (%d).\n", Output, Abc_NtkPoNum(pNtk) ); + return 1; + } assert( vPoIds == NULL ); + vPoIds = Vec_IntAlloc( 1 ); + Vec_IntPush( vPoIds, Output ); + pNtkRes = Abc_NtkSelectPos( pNtk, vPoIds ); + Vec_IntFree( vPoIds ); + } else { if ( Output == -1 ) { - Abc_Print( -1, "The node is not specified.\n" ); + Abc_Print( -1, "The starting PO ID is not specified.\n" ); return 1; } if ( Output >= Abc_NtkCoNum(pNtk) ) { - Abc_Print( -1, "The 0-based output number (%d) is larger than the number of outputs (%d).\n", Output, Abc_NtkCoNum(pNtk) ); + Abc_Print( -1, "The 0-based output number (%d) is larger than the number of combinational outputs (%d).\n", Output, Abc_NtkCoNum(pNtk) ); return 1; } pNodeCo = Abc_NtkCo( pNtk, Output ); - if ( fSeq ) - pNtkRes = Abc_NtkMakeOnePo( pNtk, Output, nRange ); - else if ( fUseMffc ) + if ( fUseMffc ) pNtkRes = Abc_NtkCreateMffc( pNtk, Abc_ObjFanin0(pNodeCo), Abc_ObjName(pNodeCo) ); else pNtkRes = Abc_NtkCreateCone( pNtk, Abc_ObjFanin0(pNodeCo), Abc_ObjName(pNodeCo), fUseAllCis ); } - if ( pNodeCo && Abc_ObjFaninC0(pNodeCo) && !fSeq ) + if ( pNodeCo && Abc_ObjFaninC0(pNodeCo) ) { Abc_NtkPo(pNtkRes, 0)->fCompl0 ^= 1; // Abc_Print( -1, "The extracted cone represents the complement function of the CO.\n" ); @@ -13215,14 +13454,14 @@ int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: cone [-OR num] [-amsh] \n" ); - Abc_Print( -2, "\t replaces the current network by one logic cone\n" ); + Abc_Print( -2, "usage: cone [-ORN num] [-amh] \n" ); + Abc_Print( -2, "\t replaces the current network by one or more logic cones\n" ); Abc_Print( -2, "\t-a : toggle keeping all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" ); Abc_Print( -2, "\t-m : toggle keeping only MFFC or complete TFI cone [default = %s]\n", fUseMffc? "MFFC": "TFI cone" ); - Abc_Print( -2, "\t-s : toggle comb or sequential cone (works with \"-O num\") [default = %s]\n", fSeq? "seq": "comb" ); Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-O num : (optional) the 0-based number of the CO to extract\n"); Abc_Print( -2, "\t-R num : (optional) the number of outputs to extract\n"); + Abc_Print( -2, "\t-N : (optional) a comma-separated list of zero-based primary output indexes\n"); Abc_Print( -2, "\tname : (optional) the name of the node to extract\n"); return 1; } @@ -19960,10 +20199,10 @@ usage: int Abc_CommandStochMap( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); - extern void Abc_NtkStochMap( int nSuppMax, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs ); - int c, nMaxSize = 14, nIters = 1, TimeOut = 0, Seed = 0, nProcs = 1, fVerbose = 0; char * pScript; + extern void Abc_NtkStochMap( int nSuppMax, int nIters, int TimeOut, int Seed, int fOverlap, int fVerbose, char * pScript, int nProcs ); + int c, nMaxSize = 14, nIters = 1, TimeOut = 0, Seed = 0, nProcs = 1, fOverlap = 0, fVerbose = 0; char * pScript; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NITSPvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NITSPovh" ) ) != EOF ) { switch ( c ) { @@ -20022,6 +20261,9 @@ int Abc_CommandStochMap( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nProcs < 0 ) goto usage; break; + case 'o': + fOverlap ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -20047,18 +20289,19 @@ int Abc_CommandStochMap( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } pScript = Abc_UtilStrsav( argv[globalUtilOptind] ); - Abc_NtkStochMap( nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript, nProcs ); + Abc_NtkStochMap( nMaxSize, nIters, TimeOut, Seed, fOverlap, fVerbose, pScript, nProcs ); ABC_FREE( pScript ); return 0; usage: - Abc_Print( -2, "usage: stochmap [-NITSP ] [-tvh]