summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abcShow.c8
-rw-r--r--src/base/cmd/cmd.c4
-rw-r--r--src/base/cmd/cmdUtils.c5
-rw-r--r--src/base/io/io.c400
-rw-r--r--src/base/main/mainReal.c6
5 files changed, 386 insertions, 37 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/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..b8d1d7db 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,291 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, int * pnFrames, int * fOldFormat )
+{
+ FILE * pFile;
+ Abc_Cex_t * pCex;
+ 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 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;
+ Buffer[strlen(Buffer) - 1] = '\0';
+ if (state==0 && strlen(Buffer)>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<strlen(Buffer);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 then 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 then in Ntk. Truncating.\n" );
+ Vec_IntShrink( vNums, nRegsNtk );
+ nRegs = nRegsNtk;
+ }
+ state = 3;
+ break;
+ default:
+ for (i=0; i<strlen(Buffer);i++) {
+ char c = Buffer[i];
+ if ( c == '0' || c == '1' )
+ Vec_IntPush( vNums, c - '0' );
+ else if ( c == 'x') {
+ usedX = 1;
+ Vec_IntPush( vNums, 0 );
+ }
+ }
+ nFrames++;
+ break;
+ }
+ }
+ fclose( pFile );
+
+ if (usedX)
+ printf( "Warning: Using 0 instead of x in latches or primary inputs\n" );
+ int iFrameCex = nFrames;
+ int nPiNtk = 0;
+ int nPoNtk = 0;
+ Abc_NtkForEachPi(pNtk, pObj, i ) nPiNtk++;
+ Abc_NtkForEachPo(pNtk, pObj, i ) nPoNtk++;
+ 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 != nPiNtk )
+ {
+ printf( "ERROR: Number of primary inputs not coresponding to Ntk.\n" );
+ Vec_IntFree( vNums );
+ return -1;
+ }
+ if ( iPo >= nPoNtk )
+ {
+ printf( "ERROR: PO that failed verification not coresponding to Ntk.\n" );
+ Vec_IntFree( vNums );
+ return -1;
+ }
+ Abc_NtkForEachLatch( pNtk, pObj, i ) {
+ if ( Vec_IntEntry(vNums, i) ==0)
+ Abc_LatchSetInit0(pObj);
+ else if ( Vec_IntEntry(vNums, i) ==2)
+ Abc_LatchSetInitNone(pObj);
+ else
+ Abc_LatchSetInit1(pObj);
+ }
+
+ pCex = 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;
+ // the zero-based number of the time-frame, for which verificaiton failed
+ pCex->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 );
+ Vec_IntFree( vNums );
+ if ( ppCex )
+ *ppCex = pCex;
+ else
+ ABC_FREE( pCex );
+
+ 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;
+ char * pFileName;
+ FILE * pFile;
+ int fCheck;
+ int c;
+ int fOldFormat = 0;
+
+ fCheck = 1;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'c':
+ fCheck ^= 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, &pAbc->pCex, &pAbc->nFrames, &fOldFormat );
+
+ 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 );
+ Bmc_CexCareVerify( pAig, pAbc->pCex, pAbc->pCex, false );
+ Aig_ManStop( pAig );
+ } else if (fOldFormat) {
+ fprintf( pAbc->Err, "Using old aiger format with no checks enabled.\n" );
+ return -1;
+ }
+ 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-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 +2738,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 +2762,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 );
@@ -2487,20 +2781,41 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
}
else if ( fUseSatBased )
pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose );
+ 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 +2855,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 +2913,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 +2954,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 +3008,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 +3017,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 +3064,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..a13be5e5 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
@@ -132,7 +134,7 @@ int Abc_RealMain( int argc, char * argv[] )
break;
case 'm': {
-#if !defined(WIN32) && !defined(ABC_NO_RLIMIT)
+#if !defined(WIN32) && !defined(__wasm)
int maxMb = atoi(globalUtilOptarg);
printf("Limiting memory use to %d MB\n", maxMb);
struct rlimit limit = {
@@ -144,7 +146,7 @@ int Abc_RealMain( int argc, char * argv[] )
break;
}
case 'l': {
-#if !defined(WIN32) && !defined(ABC_NO_RLIMIT)
+#if !defined(WIN32) && !defined(__wasm)
rlim_t maxTime = atoi(globalUtilOptarg);
printf("Limiting time to %d seconds\n", (int)maxTime);
struct rlimit limit = {
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 11:25:18 +0000