diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/base/abc/abcShow.c | 8 | ||||
-rw-r--r-- | src/base/abci/abc.c | 31 | ||||
-rw-r--r-- | src/base/cmd/cmd.c | 4 | ||||
-rw-r--r-- | src/base/cmd/cmdUtils.c | 5 | ||||
-rw-r--r-- | src/base/io/io.c | 447 | ||||
-rw-r--r-- | src/base/main/mainReal.c | 2 | ||||
-rw-r--r-- | src/base/wln/wlnRtl.c | 4 | ||||
-rw-r--r-- | src/map/scl/sclLiberty.c | 62 | ||||
-rw-r--r-- | src/misc/util/abc_global.h | 4 | ||||
-rw-r--r-- | src/misc/util/utilFile.c | 28 | ||||
-rw-r--r-- | src/misc/util/utilSignal.c | 4 | ||||
-rw-r--r-- | src/sat/bmc/bmc.h | 4 | ||||
-rw-r--r-- | src/sat/bmc/bmcCexCare.c | 38 | ||||
-rw-r--r-- | src/sat/bmc/bmcCexTools.c | 47 | ||||
-rw-r--r-- | src/sat/bsat2/Alloc.h | 8 | ||||
-rw-r--r-- | src/sat/bsat2/Vec.h | 4 | ||||
-rw-r--r-- | src/sat/bsat2/XAlloc.h | 4 | ||||
-rw-r--r-- | src/sat/glucose/Alloc.h | 8 | ||||
-rw-r--r-- | src/sat/glucose/IntTypes.h | 14 | ||||
-rw-r--r-- | src/sat/glucose/Vec.h | 4 | ||||
-rw-r--r-- | src/sat/glucose/XAlloc.h | 4 | ||||
-rw-r--r-- | src/sat/glucose2/Alloc.h | 8 | ||||
-rw-r--r-- | src/sat/glucose2/IntTypes.h | 14 | ||||
-rw-r--r-- | src/sat/glucose2/Vec.h | 8 | ||||
-rw-r--r-- | src/sat/glucose2/XAlloc.h | 4 |
25 files changed, 676 insertions, 92 deletions
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c index ff43dbe6..dd8e9efe 100644 --- a/src/base/abc/abcShow.c +++ b/src/base/abc/abcShow.c @@ -363,7 +363,11 @@ void Abc_ShowFile( char * FileNameDot ) // generate the PostScript file using DOT sprintf( CommandDot, "%s -Tps -o %s %s", pDotName, FileNamePs, FileNameDot ); +#if defined(__wasm) + RetValue = -1; +#else RetValue = system( CommandDot ); +#endif if ( RetValue == -1 ) { fprintf( stdout, "Command \"%s\" did not succeed.\n", CommandDot ); @@ -401,7 +405,11 @@ void Abc_ShowFile( char * FileNameDot ) char CommandPs[1000]; unlink( FileNameDot ); sprintf( CommandPs, "%s %s &", pGsNameUnix, FileNamePs ); +#if defined(__wasm) + if ( 1 ) +#else if ( system( CommandPs ) == -1 ) +#endif { fprintf( stdout, "Cannot execute \"%s\".\n", CommandPs ); return; diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index a65b37e2..fd677ace 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28017,17 +28017,20 @@ usage: int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk; + Abc_Ntk_t * pNtkRes; int c; int nFrames; int nConfs; int nProps; int fRemove; + int fPurge; int fStruct; int fInvert; int fOldAlgo; int fVerbose; int nConstrs; extern void Abc_NtkDarConstr( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nProps, int fStruct, int fOldAlgo, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkMakeOnePo( Abc_Ntk_t * pNtk, int Output, int nRange ); pNtk = Abc_FrameReadNtk(pAbc); // set defaults @@ -28035,13 +28038,14 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv ) nConfs = 1000; nProps = 1000; fRemove = 0; + fPurge = 0; fStruct = 0; fInvert = 0; fOldAlgo = 0; fVerbose = 0; nConstrs = -1; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FCPNrsiavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FCPNrpsiavh" ) ) != EOF ) { switch ( c ) { @@ -28092,6 +28096,9 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fRemove ^= 1; break; + case 'p': + fPurge ^= 1; + break; case 's': fStruct ^= 1; break; @@ -28127,7 +28134,22 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Constraints are not defined.\n" ); return 0; } - Abc_Print( 1, "Constraints are converted to be primary outputs.\n" ); + + if ( fPurge ) + { + Abc_Print( 1, "Constraints are removed.\n" ); + pNtkRes = Abc_NtkMakeOnePo( pNtk, 0, Abc_NtkPoNum(pNtk) - Abc_NtkConstrNum(pNtk) ); + if ( pNtkRes == NULL ) + { + Abc_Print( 1,"Transformation has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + pNtk = Abc_FrameReadNtk(pAbc); + } + else + Abc_Print( 1, "Constraints are converted to be primary outputs.\n" ); pNtk->nConstrs = 0; return 0; } @@ -28172,7 +28194,7 @@ int Abc_CommandConstr( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_NtkDarConstr( pNtk, nFrames, nConfs, nProps, fStruct, fOldAlgo, fVerbose ); return 0; usage: - Abc_Print( -2, "usage: constr [-FCPN num] [-risavh]\n" ); + Abc_Print( -2, "usage: constr [-FCPN num] [-rpisavh]\n" ); Abc_Print( -2, "\t a toolkit for constraint manipulation\n" ); Abc_Print( -2, "\t if constraints are absent, detect them functionally\n" ); Abc_Print( -2, "\t if constraints are present, profiles them using random simulation\n" ); @@ -28181,7 +28203,8 @@ usage: Abc_Print( -2, "\t-C num : the max number of conflicts in SAT solving [default = %d]\n", nConfs ); Abc_Print( -2, "\t-P num : the max number of propagations in SAT solving [default = %d]\n", nProps ); Abc_Print( -2, "\t-N num : manually set the last <num> POs to be constraints [default = %d]\n", nConstrs ); - Abc_Print( -2, "\t-r : manually remove the constraints [default = %s]\n", fRemove? "yes": "no" ); + Abc_Print( -2, "\t-r : manually remove the constraints, converting them to POs [default = %s]\n", fRemove? "yes": "no" ); + Abc_Print( -2, "\t-p : remove constraints instead of converting them to POs [default = %s]\n", fPurge? "yes": "no" ); Abc_Print( -2, "\t-i : toggle inverting already defined constraints [default = %s]\n", fInvert? "yes": "no" ); Abc_Print( -2, "\t-s : toggle using structural detection methods [default = %s]\n", fStruct? "yes": "no" ); Abc_Print( -2, "\t-a : toggle fast implication detection [default = %s]\n", !fOldAlgo? "yes": "no" ); diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index fe7286b7..98368ef8 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -2175,7 +2175,11 @@ void Gia_ManGnuplotShow( char * pPlotFileName ) { char Command[1000]; sprintf( Command, "%s %s ", pProgNameGnuplot, pPlotFileName ); +#if defined(__wasm) + if ( 1 ) +#else if ( system( Command ) == -1 ) +#endif { fprintf( stdout, "Cannot execute \"%s\".\n", Command ); return; diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c index 2158f8e9..0759ca9c 100644 --- a/src/base/cmd/cmdUtils.c +++ b/src/base/cmd/cmdUtils.c @@ -53,6 +53,9 @@ int cmdCheckShellEscape( Abc_Frame_t * pAbc, int argc, char ** argv) int RetValue; if (argv[0][0] == '!') { +#if defined(__wasm) + RetValue = -1; +#else const int size = 4096; int i; char * buffer = ABC_ALLOC(char, 10000); @@ -71,7 +74,7 @@ int cmdCheckShellEscape( Abc_Frame_t * pAbc, int argc, char ** argv) // the parts, we lose information. So a command like // `!ls "file name"` will be sent to the system as // `ls file name` which is a BUG - +#endif return 1; } else diff --git a/src/base/io/io.c b/src/base/io/io.c index 9b3d288a..46f2641f 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -44,6 +44,7 @@ static int IoCommandReadBblif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandReadCex ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadDsd ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -114,6 +115,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlifMv, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 ); + Cmd_CommandAdd( pAbc, "I/O", "read_cex", IoCommandReadCex, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_formula", IoCommandReadDsd, 1 ); // Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 ); @@ -681,6 +683,331 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, Abc_Cex_t ** ppCexCare, int * pnFrames, int * fOldFormat, int xMode ) +{ + FILE * pFile; + Abc_Cex_t * pCex; + Abc_Cex_t * pCexCare; + Vec_Int_t * vNums; + int c, nRegs = -1, nFrames = -1; + pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + printf( "Cannot open log file for reading \"%s\".\n" , pFileName ); + return -1; + } + + vNums = Vec_IntAlloc( 100 ); + int usedX = 0; + *fOldFormat = 0; + + int MaxLine = 1000000; + char *Buffer; + int BufferLen = 0; + int state = 0; + int iPo = 0; + nFrames = -1; + int status = 0; + int i; + int nRegsNtk = 0; + Abc_Obj_t * pObj; + Abc_NtkForEachLatch( pNtk, pObj, i ) nRegsNtk++; + + Buffer = ABC_ALLOC( char, MaxLine ); + while ( fgets( Buffer, MaxLine, pFile ) != NULL ) + { + if ( Buffer[0] == '#' || Buffer[0] == 'c' || Buffer[0] == 'f' || Buffer[0] == 'u' ) + continue; + BufferLen = strlen(Buffer) - 1; + Buffer[BufferLen] = '\0'; + if (state==0 && BufferLen>1) { + // old format detected + *fOldFormat = 1; + state = 2; + iPo = 0; + status = 1; + } + if (state==1 && Buffer[0]!='b' && Buffer[0]!='j') { + // old format detected, first line was actually register + *fOldFormat = 1; + state = 3; + Vec_IntPush( vNums, status ); + status = 1; + } + if (Buffer[0] == '.' ) + break; + switch(state) { + case 0 : + { + char c = Buffer[0]; + if ( c == '0' || c == '1' || c == '2' ) { + status = c - '0' ; + state = 1; + } else if ( c == 'x' ) { + // old format with one x state latch + usedX = 1; + // set to 2 so we can Abc_LatchSetInitNone + // acts like 0 when setting bits + Vec_IntPush( vNums, 2 ); + nRegs = Vec_IntSize(vNums); + state = 3; + } else { + printf( "ERROR: Bad aiger status line.\n" ); + return -1; + } + } + break; + case 1 : + iPo = atoi(Buffer+1); + state = 2; + break; + case 2 : + for (i=0; i<BufferLen;i++) { + char c = Buffer[i]; + if ( c == '0' || c == '1' ) + Vec_IntPush( vNums, c - '0' ); + else if ( c == 'x') { + usedX = 1; + // set to 2 so we can Abc_LatchSetInitNone + // acts like 0 when setting bits + Vec_IntPush( vNums, 2 ); + } + } + nRegs = Vec_IntSize(vNums); + if ( nRegs < nRegsNtk ) + { + printf( "WARNING: Register number is smaller than in Ntk. Appending.\n" ); + for (i=0; i<nRegsNtk-nRegs;i++) { + Vec_IntPush( vNums, 0 ); + } + nRegs = Vec_IntSize(vNums); + } + else if ( nRegs > nRegsNtk ) + { + printf( "WARNING: Register number is larger than in Ntk. Truncating.\n" ); + Vec_IntShrink( vNums, nRegsNtk ); + nRegs = nRegsNtk; + } + state = 3; + break; + default: + for (i=0; i<BufferLen;i++) { + char c = Buffer[i]; + if ( c == '0' || c == '1' ) + Vec_IntPush( vNums, c - '0' ); + else if ( c == 'x') { + usedX = 1; + Vec_IntPush( vNums, 2 ); + } + } + nFrames++; + break; + } + } + fclose( pFile ); + + if (usedX && !xMode) + printf( "Warning: Using 0 instead of x in latches or primary inputs\n" ); + int iFrameCex = nFrames; + if ( nRegs < 0 ) + { + if (status == 0 || *fOldFormat == 0) + printf( "Counter-example is not available.\n" ); + else + printf( "ERROR: Cannot read register number.\n" ); + Vec_IntFree( vNums ); + return -1; + } + if ( nRegs != nRegsNtk ) + { + printf( "ERROR: Register number not coresponding to Ntk.\n" ); + Vec_IntFree( vNums ); + return -1; + } + if ( Vec_IntSize(vNums)-nRegs == 0 ) + { + printf( "ERROR: Cannot read counter example.\n" ); + Vec_IntFree( vNums ); + return -1; + } + if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 ) + { + printf( "ERROR: Incorrect number of bits.\n" ); + Vec_IntFree( vNums ); + return -1; + } + int nPi = (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1); + if ( nPi != Abc_NtkPiNum(pNtk) ) + { + printf( "ERROR: Number of primary inputs not coresponding to Ntk.\n" ); + Vec_IntFree( vNums ); + return -1; + } + if ( iPo >= Abc_NtkPoNum(pNtk) ) + { + printf( "WARNING: PO that failed verification not coresponding to Ntk, using first PO instead.\n" ); + iPo = 0; + } + Abc_NtkForEachLatch( pNtk, pObj, i ) { + if ( Vec_IntEntry(vNums, i) == 1 ) + Abc_LatchSetInit1(pObj); + else if ( Vec_IntEntry(vNums, i) == 2 && xMode ) + Abc_LatchSetInitNone(pObj); + else + Abc_LatchSetInit0(pObj); + } + + pCex = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1 ); + pCexCare = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1); + // the zero-based number of PO, for which verification failed + // fails in Bmc_CexVerify if not less than actual number of PO + pCex->iPo = iPo; + pCexCare->iPo = iPo; + // the zero-based number of the time-frame, for which verificaiton failed + pCex->iFrame = iFrameCex; + pCexCare->iFrame = iFrameCex; + assert( Vec_IntSize(vNums) == pCex->nBits ); + for ( c = 0; c < pCex->nBits; c++ ) { + if ( Vec_IntEntry(vNums, c) == 1) + { + Abc_InfoSetBit( pCex->pData, c ); + Abc_InfoSetBit( pCexCare->pData, c ); + } + else if ( Vec_IntEntry(vNums, c) == 2 && xMode ) + { + // nothing to set + } + else + Abc_InfoSetBit( pCexCare->pData, c ); + } + + Vec_IntFree( vNums ); + Abc_CexFreeP( ppCex ); + if ( ppCex ) + *ppCex = pCex; + else + Abc_CexFree( pCex ); + Abc_CexFreeP( ppCexCare ); + if ( ppCexCare ) + *ppCexCare = pCexCare; + else + Abc_CexFree( pCexCare ); + + if ( pnFrames ) + *pnFrames = nFrames; + return status; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +int IoCommandReadCex( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Abc_Ntk_t * pNtk; + Abc_Cex_t * pCex = NULL; + Abc_Cex_t * pCexCare = NULL; + char * pFileName; + FILE * pFile; + int fCheck = 1; + int fXMode = 0; + int c; + int fOldFormat = 0; + int verified; + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "cxh" ) ) != EOF ) + { + switch ( c ) + { + case 'c': + fCheck ^= 1; + break; + case 'x': + fXMode ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + + // get the input file name + pFileName = argv[globalUtilOptind]; + if ( (pFile = fopen( pFileName, "r" )) == NULL ) + { + fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName ); + return 1; + } + fclose( pFile ); + + pNtk = pAbc->pNtkCur; + if ( pNtk == NULL ) + { + fprintf( pAbc->Out, "Empty network.\n" ); + return 0; + } + Abc_FrameClearVerifStatus( pAbc ); + pAbc->Status = Abc_NtkReadCexFile( pFileName, pNtk, &pCex, &pCexCare, &pAbc->nFrames, &fOldFormat, fXMode); + if ( fOldFormat && !fCheck ) + printf( "WARNING: Old witness format detected and checking is disabled. Reading might have failed.\n" ); + + if ( fCheck && pAbc->Status==1) { + extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); + Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); + + verified = Bmc_CexCareVerify( pAig, pCex, pCexCare, false ); + if (!verified) + { + printf( "Checking CEX for any PO.\n" ); + int verified = Bmc_CexCareVerifyAnyPo( pAig, pCex, pCexCare, false ); + Aig_ManStop( pAig ); + if (verified < 0) + { + Abc_CexFreeP(&pCex); + Abc_CexFreeP(&pCexCare); + return 1; + } + pAbc->pCex->iPo = verified; + } + + Abc_CexFreeP(&pCexCare); + Abc_FrameReplaceCex( pAbc, &pCex ); + } + return 0; + +usage: + fprintf( pAbc->Err, "usage: read_cex [-ch] <file>\n" ); + fprintf( pAbc->Err, "\t reads the witness cex\n" ); + fprintf( pAbc->Err, "\t-c : toggle check after reading [default = %s]\n", fCheck? "yes":"no" ); + fprintf( pAbc->Err, "\t-x : read x bits for verification [default = %s]\n", fXMode? "yes":"no" ); + fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); + fprintf( pAbc->Err, "\tfile : the name of a file to read\n" ); + return 1; +} +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int IoCommandReadDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk; @@ -2451,10 +2778,15 @@ void Abc_NtkDumpOneCexSpecial( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex } +extern Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose ); +extern Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexCare, int fVerbose ); +extern Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose ); + void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, - int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, - int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose ) + int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, int fCexInfo, + int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose, int fExtended ) { + Abc_Cex_t * pCare = NULL; Abc_Obj_t * pObj; int i, f; if ( fPrintFull ) @@ -2470,15 +2802,17 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCexFull->pData, Abc_NtkCiNum(pNtk)*f + i) ); Abc_CexFreeP( &pCexFull ); } - else if ( fNames ) + else { - Abc_Cex_t * pCare = NULL; + if ( fNames ) + { + fprintf( pFile, "# FALSIFYING OUTPUTS:"); + fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); + } if ( fMinimize ) { extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters ); Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 ); - fprintf( pFile, "# FALSIFYING OUTPUTS:"); - fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); if ( fUseOldMin ) { pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose ); @@ -2486,21 +2820,47 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose ); } else if ( fUseSatBased ) - pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose ); + { + if ( Abc_NtkPoNum( pNtk ) == 1 ) + pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose ); + else + printf( "SAT-based CEX minimization requires having a single PO.\n" ); + } + else if ( fCexInfo ) + { + Gia_Man_t * p = Gia_ManFromAigSimple( pAig ); + Abc_Cex_t * pCexImpl = NULL; + Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose ); + Abc_Cex_t * pCexCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose ); + Abc_Cex_t * pCexEss; + + if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCexCare ) ) + printf( "Counter-example care-set verification has failed.\n" ); + + pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose ); + + // pCare is pCexMin from Bmc_CexTest + pCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose ); + + if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCare ) ) + printf( "Counter-example min-set verification has failed.\n" ); + Abc_CexFreeP( &pCexStates ); + Abc_CexFreeP( &pCexImpl ); + Abc_CexFreeP( &pCexCare ); + Abc_CexFreeP( &pCexEss ); + } else pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, fCheckCex, fVerbose ); Aig_ManStop( pAig ); - if(pCare == NULL) + if(pCare == NULL) printf( "Counter-example minimization has failed.\n" ); } - else + if (fNames) { - fprintf( pFile, "# FALSIFYING OUTPUTS:"); - fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); + fprintf( pFile, "\n"); + fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1); } - fprintf( pFile, "\n"); - fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1); - if ( fUseFfNames && Abc_NtkCheckSpecialPi(pNtk) ) + if ( fNames && fUseFfNames && Abc_NtkCheckSpecialPi(pNtk) ) { int * pValues; int nXValues = 0, iFlop = 0, iPivotPi = -1; @@ -2540,29 +2900,36 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, } else { + if (fExtended && fAiger && !fNames) { + fprintf( pFile, "1\n"); + fprintf( pFile, "b%d\n", pCex->iPo); + } // output flop values (unaffected by the minimization) Abc_NtkForEachLatch( pNtk, pObj, i ) - fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) ); + if ( fNames ) + fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) ); + else + fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) ); + if ( !fNames && fAiger) + fprintf( pFile, "\n"); // output PI values (while skipping the minimized ones) - for ( f = 0; f <= pCex->iFrame; f++ ) + for ( f = 0; f <= pCex->iFrame; f++ ) { Abc_NtkForEachPi( pNtk, pObj, i ) if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) ) - fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); + if ( fNames ) + fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); + else + fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); + else if ( !fNames ) + fprintf( pFile, "x"); + if ( !fNames && fAiger) + fprintf( pFile, "\n"); + } + if (fExtended && fAiger && !fNames) + fprintf( pFile, ".\n"); } Abc_CexFreeP( &pCare ); } - else - { - Abc_NtkForEachLatch( pNtk, pObj, i ) - fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) ); - - for ( i = pCex->nRegs; i < pCex->nBits; i++ ) - { - if ( fAiger && (i-pCex->nRegs)%pCex->nPis == 0) - fprintf( pFile, "\n"); - fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, i) ); - } - } } /**Function************************************************************* @@ -2591,9 +2958,11 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) int fPrintFull = 0; int fUseFfNames = 0; int fVerbose = 0; + int fCexInfo = 0; + int fExtended = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvhxt" ) ) != EOF ) { switch ( c ) { @@ -2630,6 +2999,12 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) case 'v': fVerbose ^= 1; break; + case 'x': + fCexInfo ^= 1; + break; + case 't': + fExtended ^= 1; + break; case 'h': goto usage; default: @@ -2678,8 +3053,8 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) if ( pAbc->pCex ) { Abc_NtkDumpOneCex( pFile, pNtk, pCex, - fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, - fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose ); + fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo, + fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended ); } else if ( pAbc->vCexVec ) { @@ -2687,10 +3062,10 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) { if ( pCex == NULL ) continue; - fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i ); + fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i ); Abc_NtkDumpOneCex( pFile, pNtk, pCex, - fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, - fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose ); + fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo, + fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended ); } } fprintf( pFile, "# DONE\n" ); @@ -2734,8 +3109,10 @@ usage: fprintf( pAbc->Err, "\t-u : use fast SAT-based CEX minimization [default = %s]\n", fUseSatBased? "yes": "no" ); fprintf( pAbc->Err, "\t-e : use high-effort SAT-based CEX minimization [default = %s]\n", fHighEffort? "yes": "no" ); fprintf( pAbc->Err, "\t-o : use old CEX minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" ); + fprintf( pAbc->Err, "\t-x : minimize using algorithm from cexinfo command [default = %s]\n", fCexInfo? "yes": "no" ); fprintf( pAbc->Err, "\t-c : check generated CEX using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" ); fprintf( pAbc->Err, "\t-a : print cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" ); + fprintf( pAbc->Err, "\t-t : extended header info when cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" ); fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s]\n", fPrintFull? "yes": "no" ); fprintf( pAbc->Err, "\t-z : toggle using saved flop names [default = %s]\n", fUseFfNames? "yes": "no" ); fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s]\n", fVerbose? "yes": "no" ); diff --git a/src/base/main/mainReal.c b/src/base/main/mainReal.c index 922e0521..420f2cf1 100644 --- a/src/base/main/mainReal.c +++ b/src/base/main/mainReal.c @@ -49,7 +49,9 @@ SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS. #include <sys/times.h> #include <sys/resource.h> #include <unistd.h> +#if !defined(__wasm) #include <signal.h> +#endif #include <stdlib.h> #endif diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c index 51e00eb6..391d168c 100644 --- a/src/base/wln/wlnRtl.c +++ b/src/base/wln/wlnRtl.c @@ -121,6 +121,9 @@ char * Wln_GetYosysName() } int Wln_ConvertToRtl( char * pCommand, char * pFileTemp ) { +#if defined(__wasm) + return 0; +#else FILE * pFile; if ( system( pCommand ) == -1 ) { @@ -134,6 +137,7 @@ int Wln_ConvertToRtl( char * pCommand, char * pFileTemp ) } fclose( pFile ); return 1; +#endif } Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose ) { diff --git a/src/map/scl/sclLiberty.c b/src/map/scl/sclLiberty.c index 49b5c237..60aaded2 100644 --- a/src/map/scl/sclLiberty.c +++ b/src/map/scl/sclLiberty.c @@ -42,20 +42,20 @@ typedef enum { typedef struct Scl_Pair_t_ Scl_Pair_t; struct Scl_Pair_t_ { - int Beg; // item beginning - int End; // item end + long Beg; // item beginning + long End; // item end }; typedef struct Scl_Item_t_ Scl_Item_t; struct Scl_Item_t_ { int Type; // Scl_LibertyType_t - int iLine; // file line where the item's spec begins + long iLine; // file line where the item's spec begins Scl_Pair_t Key; // key part Scl_Pair_t Head; // head part Scl_Pair_t Body; // body part - int Next; // next item in the list - int Child; // first child item + long Next; // next item in the list + long Child; // first child item }; typedef struct Scl_Tree_t_ Scl_Tree_t; @@ -63,10 +63,10 @@ struct Scl_Tree_t_ { char * pFileName; // input Liberty file name char * pContents; // file contents - int nContents; // file size - int nLines; // line counter - int nItems; // number of items - int nItermAlloc; // number of items allocated + long nContents; // file size + long nLines; // line counter + long nItems; // number of items + long nItermAlloc; // number of items allocated Scl_Item_t * pItems; // the items char * pError; // the error string abctime clkStart; // beginning time @@ -74,11 +74,11 @@ struct Scl_Tree_t_ }; static inline Scl_Item_t * Scl_LibertyRoot( Scl_Tree_t * p ) { return p->pItems; } -static inline Scl_Item_t * Scl_LibertyItem( Scl_Tree_t * p, int v ) { assert( v < p->nItems ); return v < 0 ? NULL : p->pItems + v; } -static inline int Scl_LibertyCompare( Scl_Tree_t * p, Scl_Pair_t Pair, char * pStr ) { return strncmp( p->pContents+Pair.Beg, pStr, Pair.End-Pair.Beg ) || ((int)strlen(pStr) != Pair.End-Pair.Beg); } +static inline Scl_Item_t * Scl_LibertyItem( Scl_Tree_t * p, long v ) { assert( v < p->nItems ); return v < 0 ? NULL : p->pItems + v; } +static inline long Scl_LibertyCompare( Scl_Tree_t * p, Scl_Pair_t Pair, char * pStr ) { return strncmp( p->pContents+Pair.Beg, pStr, Pair.End-Pair.Beg ) || ((long)strlen(pStr) != Pair.End-Pair.Beg); } static inline void Scl_PrintWord( FILE * pFile, Scl_Tree_t * p, Scl_Pair_t Pair ) { char * pBeg = p->pContents+Pair.Beg, * pEnd = p->pContents+Pair.End; while ( pBeg < pEnd ) fputc( *pBeg++, pFile ); } -static inline void Scl_PrintSpace( FILE * pFile, int nOffset ) { int i; for ( i = 0; i < nOffset; i++ ) fputc(' ', pFile); } -static inline int Scl_LibertyItemId( Scl_Tree_t * p, Scl_Item_t * pItem ) { return pItem - p->pItems; } +static inline void Scl_PrintSpace( FILE * pFile, long nOffset ) { long i; for ( i = 0; i < nOffset; i++ ) fputc(' ', pFile); } +static inline long Scl_LibertyItemId( Scl_Tree_t * p, Scl_Item_t * pItem ) { return pItem - p->pItems; } #define Scl_ItemForEachChild( p, pItem, pChild ) \ for ( pChild = Scl_LibertyItem(p, pItem->Child); pChild; pChild = Scl_LibertyItem(p, pChild->Next) ) @@ -166,9 +166,9 @@ int Scl_LibertyParseDump( Scl_Tree_t * p, char * pFileName ) SeeAlso [] ***********************************************************************/ -int Scl_LibertyCountItems( char * pBeg, char * pEnd ) +long Scl_LibertyCountItems( char * pBeg, char * pEnd ) { - int Counter = 0; + long Counter = 0; for ( ; pBeg < pEnd; pBeg++ ) Counter += (*pBeg == '(' || *pBeg == ':'); return Counter; @@ -213,11 +213,11 @@ void Scl_LibertyWipeOutComments( char * pBeg, char * pEnd ) } } } -static inline int Scl_LibertyCharIsSpace( char c ) +static inline long Scl_LibertyCharIsSpace( char c ) { return c == ' ' || c == '\t' || c == '\r' || c == '\n' || c == '\\'; } -static inline int Scl_LibertySkipSpaces( Scl_Tree_t * p, char ** ppPos, char * pEnd, int fStopAtNewLine ) +static inline long Scl_LibertySkipSpaces( Scl_Tree_t * p, char ** ppPos, char * pEnd, int fStopAtNewLine ) { char * pPos = *ppPos; for ( ; pPos < pEnd; pPos++ ) @@ -235,7 +235,7 @@ static inline int Scl_LibertySkipSpaces( Scl_Tree_t * p, char ** ppPos, char * p return pPos == pEnd; } // skips entry delimited by " :;(){}" and returns 1 if reached the end -static inline int Scl_LibertySkipEntry( char ** ppPos, char * pEnd ) +static inline long Scl_LibertySkipEntry( char ** ppPos, char * pEnd ) { char * pPos = *ppPos; if ( *pPos == '\"' ) @@ -262,7 +262,7 @@ static inline int Scl_LibertySkipEntry( char ** ppPos, char * pEnd ) // finds the matching closing symbol static inline char * Scl_LibertyFindMatch( char * pPos, char * pEnd ) { - int Counter = 0; + long Counter = 0; assert( *pPos == '(' || *pPos == '{' ); if ( *pPos == '(' ) { @@ -356,10 +356,10 @@ char * Scl_LibertyReadString( Scl_Tree_t * p, Scl_Pair_t Pair ) Buffer[Pair.End-Pair.Beg] = 0; return Buffer; } -int Scl_LibertyItemNum( Scl_Tree_t * p, Scl_Item_t * pRoot, char * pName ) +long Scl_LibertyItemNum( Scl_Tree_t * p, Scl_Item_t * pRoot, char * pName ) { Scl_Item_t * pItem; - int Counter = 0; + long Counter = 0; Scl_ItemForEachChildName( p, pRoot, pItem, pName ) Counter++; return Counter; @@ -376,7 +376,7 @@ int Scl_LibertyItemNum( Scl_Tree_t * p, Scl_Item_t * pRoot, char * pName ) SeeAlso [] ***********************************************************************/ -int Scl_LibertyBuildItem( Scl_Tree_t * p, char ** ppPos, char * pEnd ) +long Scl_LibertyBuildItem( Scl_Tree_t * p, char ** ppPos, char * pEnd ) { Scl_Item_t * pItem; Scl_Pair_t Key, Head, Body; @@ -482,7 +482,7 @@ exit: if ( p->pError == NULL ) { p->pError = ABC_ALLOC( char, 1000 ); - sprintf( p->pError, "File \"%s\". Line %6d. Failed to parse entry \"%s\".\n", + sprintf( p->pError, "File \"%s\". Line %6ld. Failed to parse entry \"%s\".\n", p->pFileName, p->nLines, Scl_LibertyReadString(p, Key) ); } return -1; @@ -506,10 +506,10 @@ void Scl_LibertyFixFileName( char * pFileName ) if ( *pHead == '>' ) *pHead = '\\'; } -int Scl_LibertyFileSize( char * pFileName ) +long Scl_LibertyFileSize( char * pFileName ) { FILE * pFile; - int nFileSize; + long nFileSize; pFile = fopen( pFileName, "rb" ); if ( pFile == NULL ) { @@ -521,11 +521,11 @@ int Scl_LibertyFileSize( char * pFileName ) fclose( pFile ); return nFileSize; } -char * Scl_LibertyFileContents( char * pFileName, int nContents ) +char * Scl_LibertyFileContents( char * pFileName, long nContents ) { FILE * pFile = fopen( pFileName, "rb" ); char * pContents = ABC_ALLOC( char, nContents+1 ); - int RetValue = 0; + long RetValue = 0; RetValue = fread( pContents, nContents, 1, pFile ); fclose( pFile ); pContents[nContents] = 0; @@ -534,7 +534,7 @@ char * Scl_LibertyFileContents( char * pFileName, int nContents ) void Scl_LibertyStringDump( char * pFileName, Vec_Str_t * vStr ) { FILE * pFile = fopen( pFileName, "wb" ); - int RetValue = 0; + long RetValue = 0; if ( pFile == NULL ) { printf( "Scl_LibertyStringDump(): The output file is unavailable.\n" ); @@ -558,7 +558,7 @@ void Scl_LibertyStringDump( char * pFileName, Vec_Str_t * vStr ) Scl_Tree_t * Scl_LibertyStart( char * pFileName ) { Scl_Tree_t * p; - int RetValue; + long RetValue; // read the file into the buffer Scl_LibertyFixFileName( pFileName ); RetValue = Scl_LibertyFileSize( pFileName ); @@ -682,10 +682,10 @@ int Scl_LibertyReadCellIsThreeState( Scl_Tree_t * p, Scl_Item_t * pCell ) return 1; return 0; } -int Scl_LibertyReadCellOutputNum( Scl_Tree_t * p, Scl_Item_t * pCell ) +long Scl_LibertyReadCellOutputNum( Scl_Tree_t * p, Scl_Item_t * pCell ) { Scl_Item_t * pPin; - int Counter = 0; + long Counter = 0; Scl_ItemForEachChildName( p, pCell, pPin, "pin" ) if ( Scl_LibertyReadPinFormula(p, pPin) ) Counter++; diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index d1a9b4d3..2217bb87 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -94,8 +94,6 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// -ABC_NAMESPACE_HEADER_START - //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// @@ -143,6 +141,8 @@ ABC_NAMESPACE_HEADER_START #endif +ABC_NAMESPACE_HEADER_START + /** * Pointer difference type; replacement for ptrdiff_t. * This is a signed integral type that is the same size as a pointer. diff --git a/src/misc/util/utilFile.c b/src/misc/util/utilFile.c index 4bb2f4c6..f64d71c2 100644 --- a/src/misc/util/utilFile.c +++ b/src/misc/util/utilFile.c @@ -25,6 +25,23 @@ #include <fcntl.h> #include <sys/stat.h> +// Handle legacy macros +#if !defined(S_IREAD) +#if defined(S_IRUSR) +#define S_IREAD S_IRUSR +#else +#error S_IREAD is undefined +#endif +#endif + +#if !defined(S_IWRITE) +#if defined(S_IWUSR) +#define S_IWRITE S_IWUSR +#else +#error S_IWRITE is undefined +#endif +#endif + #if defined(_MSC_VER) || defined(__MINGW32__) #include <windows.h> #include <process.h> @@ -102,6 +119,17 @@ int tmpFile(const char* prefix, const char* suffix, char** out_name) } assert(0); // -- could not open temporary file return 0; +#elif defined(__wasm) + static int seq = 0; // no risk of collision since we're in a sandbox + int fd; + *out_name = (char*)malloc(strlen(prefix) + strlen(suffix) + 9); + sprintf(*out_name, "%s%08d%s", prefix, seq++, suffix); + fd = open(*out_name, O_CREAT | O_EXCL | O_RDWR, S_IREAD | S_IWRITE); + if (fd == -1){ + free(*out_name); + *out_name = NULL; + } + return fd; #else int fd; *out_name = (char*)malloc(strlen(prefix) + strlen(suffix) + 7); diff --git a/src/misc/util/utilSignal.c b/src/misc/util/utilSignal.c index 03af81d1..137ff54b 100644 --- a/src/misc/util/utilSignal.c +++ b/src/misc/util/utilSignal.c @@ -43,7 +43,11 @@ ABC_NAMESPACE_IMPL_START int Util_SignalSystem(const char* cmd) { +#if defined(__wasm) + return -1; +#else return system(cmd); +#endif } int tmpFile(const char* prefix, const char* suffix, char** out_name); diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h index 844497ad..34356359 100644 --- a/src/sat/bmc/bmc.h +++ b/src/sat/bmc/bmc.h @@ -227,7 +227,8 @@ extern int Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars extern Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); extern Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose ); extern Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose ); -extern void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ); +extern int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ); +extern int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ); extern Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose ); extern Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose ); /*=== bmcCexCut.c ==========================================================*/ @@ -238,6 +239,7 @@ extern Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pC /*=== bmcCexTool.c ==========================================================*/ extern void Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose ); extern int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); +extern int Bmc_CexVerifyAnyPo( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ); /*=== bmcICheck.c ==========================================================*/ extern void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose ); extern Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose ); diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c index c274b04c..d9a677c3 100644 --- a/src/sat/bmc/bmcCexCare.c +++ b/src/sat/bmc/bmcCexCare.c @@ -455,8 +455,9 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t SeeAlso [] ***********************************************************************/ -void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ) +int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ) { + int result; Gia_Man_t * pGia = Gia_ManFromAigSimple( p ); if ( fVerbose ) { @@ -465,11 +466,13 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in printf( "Minimized: " ); Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 ); } - if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) ) + result = Bmc_CexVerify( pGia, pCex, pCexMin ); + if ( !result ) printf( "Counter-example verification has failed.\n" ); else printf( "Counter-example verification succeeded.\n" ); Gia_ManStop( pGia ); + return result; } /* { @@ -480,6 +483,37 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in } */ +/**Function************************************************************* + + Synopsis [Verifies the care set of the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose ) +{ + int iPo; + Gia_Man_t * pGia = Gia_ManFromAigSimple( p ); + if ( fVerbose ) + { + printf( "Original : " ); + Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 ); + printf( "Minimized: " ); + Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 ); + } + iPo = Bmc_CexVerifyAnyPo( pGia, pCex, pCexMin ); + if ( iPo < 0 ) + printf( "Counter-example verification has failed.\n" ); + else + printf( "Counter-example verification succeeded.\n" ); + Gia_ManStop( pGia ); + return iPo; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c index 6cc29857..6bea6fc5 100644 --- a/src/sat/bmc/bmcCexTools.c +++ b/src/sat/bmc/bmcCexTools.c @@ -376,6 +376,53 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ) /**Function************************************************************* + Synopsis [Verifies the care set of the counter-example for an arbitrary PO.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bmc_CexVerifyAnyPo( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare ) +{ + Gia_Obj_t * pObj; + int i, k; +// assert( pCex->nRegs > 0 ); +// assert( pCexCare->nRegs == 0 ); + Gia_ObjTerSimSet0( Gia_ManConst0(p) ); + Gia_ManForEachRi( p, pObj, k ) + Gia_ObjTerSimSet0( pObj ); + for ( i = 0; i <= pCex->iFrame; i++ ) + { + Gia_ManForEachPi( p, pObj, k ) + { + if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) ) + Gia_ObjTerSimSetX( pObj ); + else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) ) + Gia_ObjTerSimSet1( pObj ); + else + Gia_ObjTerSimSet0( pObj ); + } + Gia_ManForEachRo( p, pObj, k ) + Gia_ObjTerSimRo( p, pObj ); + Gia_ManForEachAnd( p, pObj, k ) + Gia_ObjTerSimAnd( pObj ); + Gia_ManForEachCo( p, pObj, k ) + Gia_ObjTerSimCo( pObj ); + } + for (i = 0; i < Gia_ManPoNum(p) - Gia_ManConstrNum(p); i++) + { + pObj = Gia_ManPo( p, i ); + if (Gia_ObjTerSimGet1(pObj)) + return i; + } + return -1; +} + +/**Function************************************************************* + Synopsis [Computes internal states of the CEX.] Description [] diff --git a/src/sat/bsat2/Alloc.h b/src/sat/bsat2/Alloc.h index 7f506cb5..9a65cf0c 100644 --- a/src/sat/bsat2/Alloc.h +++ b/src/sat/bsat2/Alloc.h @@ -97,7 +97,11 @@ void RegionAllocator<T>::capacity(uint32_t min_cap) cap += delta; if (cap <= prev_cap) +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif } // printf(" .. (%p) cap = %u\n", this, cap); @@ -119,7 +123,11 @@ RegionAllocator<T>::alloc(int size) // Handle overflow: if (sz < prev_sz) +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif return prev_sz; } diff --git a/src/sat/bsat2/Vec.h b/src/sat/bsat2/Vec.h index f0e07d01..5eea6174 100644 --- a/src/sat/bsat2/Vec.h +++ b/src/sat/bsat2/Vec.h @@ -97,7 +97,11 @@ void vec<T>::capacity(int min_cap) { if (cap >= min_cap) return; int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)) +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif } diff --git a/src/sat/bsat2/XAlloc.h b/src/sat/bsat2/XAlloc.h index 1da17602..33741e33 100644 --- a/src/sat/bsat2/XAlloc.h +++ b/src/sat/bsat2/XAlloc.h @@ -34,7 +34,11 @@ static inline void* xrealloc(void *ptr, size_t size) { void* mem = realloc(ptr, size); if (mem == NULL && errno == ENOMEM){ +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif }else return mem; } diff --git a/src/sat/glucose/Alloc.h b/src/sat/glucose/Alloc.h index e56b5441..a63de032 100644 --- a/src/sat/glucose/Alloc.h +++ b/src/sat/glucose/Alloc.h @@ -100,7 +100,11 @@ void RegionAllocator<T>::capacity(uint32_t min_cap) cap += delta; if (cap <= prev_cap) +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif } //printf(" .. (%p) cap = %u\n", this, cap); @@ -122,7 +126,11 @@ RegionAllocator<T>::alloc(int size) // Handle overflow: if (sz < prev_sz) +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif return prev_sz; } diff --git a/src/sat/glucose/IntTypes.h b/src/sat/glucose/IntTypes.h index 3f75862b..5c4176b2 100644 --- a/src/sat/glucose/IntTypes.h +++ b/src/sat/glucose/IntTypes.h @@ -28,20 +28,18 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA # include <sys/int_fmtio.h> # include <sys/int_limits.h> -#else +#elif _WIN32 -#define __STDC_LIMIT_MACROS # include "pstdint.h" -//# include <inttypes.h> -#endif +#else -#include <limits.h> +# define __STDC_LIMIT_MACROS +# include <limits.h> +# include <inttypes.h> -#ifndef PRIu64 -#define PRIu64 "lu" -#define PRIi64 "ld" #endif + //================================================================================================= #include <misc/util/abc_namespaces.h> diff --git a/src/sat/glucose/Vec.h b/src/sat/glucose/Vec.h index dd1bc20a..d2781635 100644 --- a/src/sat/glucose/Vec.h +++ b/src/sat/glucose/Vec.h @@ -100,7 +100,11 @@ void vec<T>::capacity(int min_cap) { if (cap >= min_cap) return; int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)) +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif } diff --git a/src/sat/glucose/XAlloc.h b/src/sat/glucose/XAlloc.h index 233f834e..d1f1062a 100644 --- a/src/sat/glucose/XAlloc.h +++ b/src/sat/glucose/XAlloc.h @@ -39,7 +39,11 @@ static inline void* xrealloc(void *ptr, size_t size) { void* mem = realloc(ptr, size); if (mem == NULL && errno == ENOMEM){ +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif }else { return mem; } diff --git a/src/sat/glucose2/Alloc.h b/src/sat/glucose2/Alloc.h index b7bebaca..427cd323 100644 --- a/src/sat/glucose2/Alloc.h +++ b/src/sat/glucose2/Alloc.h @@ -100,7 +100,11 @@ void RegionAllocator<T>::capacity(uint32_t min_cap) cap += delta; if (cap <= prev_cap) +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif } //printf(" .. (%p) cap = %u\n", this, cap); @@ -122,7 +126,11 @@ RegionAllocator<T>::alloc(int size) // Handle overflow: if (sz < prev_sz) +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif return prev_sz; } diff --git a/src/sat/glucose2/IntTypes.h b/src/sat/glucose2/IntTypes.h index 3f75862b..5c4176b2 100644 --- a/src/sat/glucose2/IntTypes.h +++ b/src/sat/glucose2/IntTypes.h @@ -28,20 +28,18 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA # include <sys/int_fmtio.h> # include <sys/int_limits.h> -#else +#elif _WIN32 -#define __STDC_LIMIT_MACROS # include "pstdint.h" -//# include <inttypes.h> -#endif +#else -#include <limits.h> +# define __STDC_LIMIT_MACROS +# include <limits.h> +# include <inttypes.h> -#ifndef PRIu64 -#define PRIu64 "lu" -#define PRIi64 "ld" #endif + //================================================================================================= #include <misc/util/abc_namespaces.h> diff --git a/src/sat/glucose2/Vec.h b/src/sat/glucose2/Vec.h index eaeed207..bc989217 100644 --- a/src/sat/glucose2/Vec.h +++ b/src/sat/glucose2/Vec.h @@ -102,14 +102,22 @@ void vec<T>::capacity(int min_cap) { if (cap >= min_cap) return; int add = imax((min_cap - cap + 1) & ~1, ((cap >> 1) + 2) & ~1); // NOTE: grow by approximately 3/2 if (add > INT_MAX - cap || (((data = (T*)::realloc(data, (cap += add) * sizeof(T))) == NULL) && errno == ENOMEM)) +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif } template<class T> void vec<T>::prelocate(int ext_cap) { if (cap >= ext_cap) return; if (ext_cap > INT_MAX || (((data = (T*)::realloc(data, ext_cap * sizeof(T))) == NULL) && errno == ENOMEM)) +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif cap = ext_cap; } diff --git a/src/sat/glucose2/XAlloc.h b/src/sat/glucose2/XAlloc.h index 716643ef..86e65a49 100644 --- a/src/sat/glucose2/XAlloc.h +++ b/src/sat/glucose2/XAlloc.h @@ -39,7 +39,11 @@ static inline void* xrealloc(void *ptr, size_t size) { void* mem = realloc(ptr, size); if (mem == NULL && errno == ENOMEM){ +#ifdef __wasm + abort(); +#else throw OutOfMemoryException(); +#endif }else { return mem; } |