summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.gitattributes1
-rw-r--r--.gitcommit1
-rw-r--r--Makefile9
-rw-r--r--src/base/abc/abcShow.c8
-rw-r--r--src/base/abci/abc.c31
-rw-r--r--src/base/cmd/cmd.c4
-rw-r--r--src/base/cmd/cmdUtils.c5
-rw-r--r--src/base/io/io.c447
-rw-r--r--src/base/main/mainReal.c2
-rw-r--r--src/base/wln/wlnRtl.c4
-rw-r--r--src/map/scl/sclLiberty.c62
-rw-r--r--src/misc/util/abc_global.h4
-rw-r--r--src/misc/util/utilFile.c28
-rw-r--r--src/misc/util/utilSignal.c4
-rw-r--r--src/sat/bmc/bmc.h4
-rw-r--r--src/sat/bmc/bmcCexCare.c38
-rw-r--r--src/sat/bmc/bmcCexTools.c47
-rw-r--r--src/sat/bsat2/Alloc.h8
-rw-r--r--src/sat/bsat2/Vec.h4
-rw-r--r--src/sat/bsat2/XAlloc.h4
-rw-r--r--src/sat/glucose/Alloc.h8
-rw-r--r--src/sat/glucose/IntTypes.h14
-rw-r--r--src/sat/glucose/Vec.h4
-rw-r--r--src/sat/glucose/XAlloc.h4
-rw-r--r--src/sat/glucose2/Alloc.h8
-rw-r--r--src/sat/glucose2/IntTypes.h14
-rw-r--r--src/sat/glucose2/Vec.h8
-rw-r--r--src/sat/glucose2/XAlloc.h4
28 files changed, 684 insertions, 95 deletions
diff --git a/.gitattributes b/.gitattributes
index 400b529f..93b5c864 100644
--- a/.gitattributes
+++ b/.gitattributes
@@ -1,3 +1,4 @@
+/.gitcommit export-subst
* text=auto
*.c text
diff --git a/.gitcommit b/.gitcommit
new file mode 100644
index 00000000..46b7856f
--- /dev/null
+++ b/.gitcommit
@@ -0,0 +1 @@
+$Format:%h$
diff --git a/Makefile b/Makefile
index 3976cf7b..032f3a8d 100644
--- a/Makefile
+++ b/Makefile
@@ -137,11 +137,11 @@ endif
# LIBS := -ldl -lrt
LIBS += -lm
-ifneq ($(OS), FreeBSD)
+ifneq ($(OS), $(filter $(OS), FreeBSD OpenBSD))
LIBS += -ldl
endif
-ifneq ($(findstring Darwin, $(shell uname)), Darwin)
+ifneq ($(OS), $(filter $(OS), FreeBSD OpenBSD Darwin))
LIBS += -lrt
endif
@@ -206,7 +206,10 @@ depend: $(DEP)
clean:
@echo "$(MSG_PREFIX)\`\` Cleaning up..."
- $(VERBOSE)rm -rvf $(PROG) lib$(PROG).a $(OBJ) $(GARBAGE) $(OBJ:.o=.d)
+ $(VERBOSE)rm -rvf $(PROG) lib$(PROG).a
+ $(VERBOSE)rm -rvf $(OBJ)
+ $(VERBOSE)rm -rvf $(GARBAGE)
+ $(VERBOSE)rm -rvf $(OBJ:.o=.d)
tags:
etags `find . -type f -regex '.*\.\(c\|h\)'`
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;
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-06-08 16:00:46 +0000