summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/main/mainReal.c33
-rw-r--r--src/base/wlc/wlc.h6
-rw-r--r--src/base/wlc/wlcCom.c53
-rw-r--r--src/base/wlc/wlcNtk.c2
-rw-r--r--src/base/wlc/wlcReadSmt.c25
5 files changed, 106 insertions, 13 deletions
diff --git a/src/base/main/mainReal.c b/src/base/main/mainReal.c
index 204e7491..04152ae6 100644
--- a/src/base/main/mainReal.c
+++ b/src/base/main/mainReal.c
@@ -51,6 +51,7 @@ SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
#include "base/abc/abc.h"
#include "mainInt.h"
+#include "base/wlc/wlc.h"
ABC_NAMESPACE_IMPL_START
@@ -90,7 +91,8 @@ int Abc_RealMain( int argc, char * argv[] )
INTERACTIVE, // interactive mode
BATCH, // batch mode, run a command and quit
BATCH_THEN_INTERACTIVE, // run a command, then back to interactive mode
- BATCH_QUIET // as in batch mode, but don't echo the command
+ BATCH_QUIET, // as in batch mode, but don't echo the command
+ BATCH_SMT // special batch mode, which expends SMTLIB problem via stdin
} fBatch;
// added to detect memory leaks
@@ -138,7 +140,7 @@ int Abc_RealMain( int argc, char * argv[] )
sprintf( sWriteCmd, "write" );
Extra_UtilGetoptReset();
- while ((c = Extra_UtilGetopt(argc, argv, "c:q:C:hf:F:o:st:T:xb")) != EOF) {
+ while ((c = Extra_UtilGetopt(argc, argv, "c:q:C:S:hf:F:o:st:T:xb")) != EOF) {
switch(c) {
case 'c':
strcpy( sCommandUsr, globalUtilOptarg );
@@ -155,6 +157,11 @@ int Abc_RealMain( int argc, char * argv[] )
fBatch = BATCH_THEN_INTERACTIVE;
break;
+ case 'S':
+ strcpy( sCommandUsr, globalUtilOptarg );
+ fBatch = BATCH_SMT;
+ break;
+
case 'f':
sprintf(sCommandUsr, "source %s", globalUtilOptarg);
fBatch = BATCH;
@@ -223,6 +230,28 @@ int Abc_RealMain( int argc, char * argv[] )
}
}
+ if ( fBatch == BATCH_SMT )
+ {
+ Wlc_Ntk_t * pNtk;
+ Vec_Str_t * vInput;
+ // collect stdin
+ vInput = Wlc_GenerateSmtStdin();
+ // parse the input
+ pNtk = Wlc_ReadSmtBuffer( NULL, Vec_StrArray(vInput), Vec_StrArray(vInput) + Vec_StrSize(vInput) );
+ Vec_StrFree( vInput );
+ // install current network
+ Wlc_SetNtk( pAbc, pNtk );
+ // execute command
+ fStatus = Cmd_CommandExecute( pAbc, sCommandUsr );
+ // generate output
+ if ( !fStatus )
+ Wlc_GenerateSmtStdout( pAbc );
+ else
+ Abc_Print( 1, "Something did not work out with the command \"%s\".\n", sCommandUsr );
+ Abc_Stop();
+ return 0;
+ }
+
if ( Abc_FrameIsBridgeMode() )
{
extern Gia_Man_t * Gia_ManFromBridge( FILE * pFile, Vec_Int_t ** pvInit );
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 5954ec18..f789c03c 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -32,6 +32,7 @@
#include "misc/mem/mem.h"
#include "misc/extra/extra.h"
#include "misc/util/utilTruth.h"
+#include "base/main/mainInt.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@@ -238,6 +239,10 @@ extern Wlc_Ntk_t * Wlc_NtkAbstractNodes( Wlc_Ntk_t * pNtk, Vec_Int_t * vNodes
extern Wlc_Ntk_t * Wlc_NtkUifNodePairs( Wlc_Ntk_t * pNtk, Vec_Int_t * vPairs );
/*=== wlcBlast.c ========================================================*/
extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds );
+/*=== wlcCom.c ========================================================*/
+extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk );
+extern Vec_Str_t * Wlc_GenerateSmtStdin();
+extern void Wlc_GenerateSmtStdout( Abc_Frame_t * pAbc );
/*=== wlcNtk.c ========================================================*/
extern Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc );
extern int Wlc_ObjAlloc( Wlc_Ntk_t * p, int Type, int Signed, int End, int Beg );
@@ -253,6 +258,7 @@ extern void Wlc_NtkPrintStats( Wlc_Ntk_t * p, int fDistrib, int fVerbo
extern Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p );
extern void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p );
/*=== wlcReadSmt.c ========================================================*/
+extern Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit );
extern Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName );
/*=== wlcReadVer.c ========================================================*/
extern Wlc_Ntk_t * Wlc_ReadVer( char * pFileName );
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 88c91c51..84afb394 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -78,6 +78,59 @@ void Wlc_End( Abc_Frame_t * pAbc )
Wlc_AbcFreeNtk( pAbc );
}
+/**Function********************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )
+{
+ Wlc_AbcUpdateNtk( pAbc, pNtk );
+}
+
+
+/**Function********************************************************************
+
+ Synopsis [Reads stdin and stops when "(check-sat)" is observed.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+******************************************************************************/
+static inline int Wlc_GenerateStop( Vec_Str_t * vInput, char * pLine, int LineSize )
+{
+ char * pStr = Vec_StrArray(vInput) + Vec_StrSize(vInput) - LineSize;
+ if ( Vec_StrSize(vInput) < LineSize )
+ return 0;
+ return !strncmp( pStr, pLine, LineSize );
+}
+Vec_Str_t * Wlc_GenerateSmtStdin()
+{
+ char * pLine = "(check-sat)";
+ int c, LineSize = strlen(pLine);
+ Vec_Str_t * vInput = Vec_StrAlloc( 1000 );
+ while ( (c = fgetc(stdin)) != EOF )
+ {
+ Vec_StrPush( vInput, (char)c );
+ if ( c == ')' && Wlc_GenerateStop(vInput, pLine, LineSize) )
+ break;
+ }
+ Vec_StrPush( vInput, '\0' );
+ return vInput;
+}
+void Wlc_GenerateSmtStdout( Abc_Frame_t * pAbc )
+{
+ printf( "Output produced by SMT solver will be here.\n" );
+}
/**Function********************************************************************
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 8c09467e..48171c35 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -95,7 +95,7 @@ Wlc_Ntk_t * Wlc_NtkAlloc( char * pName, int nObjsAlloc )
{
Wlc_Ntk_t * p;
p = ABC_CALLOC( Wlc_Ntk_t, 1 );
- p->pName = Extra_FileNameGeneric( pName );
+ p->pName = pName ? Extra_FileNameGeneric( pName ) : NULL;
Vec_IntGrow( &p->vPis, 111 );
Vec_IntGrow( &p->vPos, 111 );
Vec_IntGrow( &p->vCis, 111 );
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index 35d3ed87..ec1ec567 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/src/base/wlc/wlcReadSmt.c
@@ -99,13 +99,9 @@ static inline char * Prs_SmtLoadFile( char * pFileName, char ** ppLimit )
*ppLimit = pBuffer + nFileSize + 2;
return pBuffer;
}
-static inline Prs_Smt_t * Prs_SmtAlloc( char * pFileName )
+static inline Prs_Smt_t * Prs_SmtAlloc( char * pFileName, char * pBuffer, char * pLimit )
{
Prs_Smt_t * p;
- char * pBuffer, * pLimit;
- pBuffer = Prs_SmtLoadFile( pFileName, &pLimit );
- if ( pBuffer == NULL )
- return NULL;
p = ABC_CALLOC( Prs_Smt_t, 1 );
p->pName = pFileName;
p->pBuffer = pBuffer;
@@ -121,7 +117,6 @@ static inline void Prs_SmtFree( Prs_Smt_t * p )
if ( p->pStrs )
Abc_NamDeref( p->pStrs );
Vec_IntErase( &p->vData );
- ABC_FREE( p->pBuffer );
ABC_FREE( p );
}
@@ -655,22 +650,32 @@ Wlc_Ntk_t * Prs_SmtBuild( Prs_Smt_t * p )
Vec_IntFree( vFanins );
return pNtk;
}
-Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName )
+Wlc_Ntk_t * Wlc_ReadSmtBuffer( char * pFileName, char * pBuffer, char * pLimit )
{
Wlc_Ntk_t * pNtk = NULL;
- Prs_Smt_t * p = Prs_SmtAlloc( pFileName );
+ Prs_Smt_t * p = Prs_SmtAlloc( pFileName, pBuffer, pLimit );
if ( p == NULL )
return NULL;
Prs_SmtRemoveComments( p );
Prs_SmtReadLines( p );
//Prs_SmtPrintParser( p );
if ( Prs_SmtErrorPrint(p) )
- {
pNtk = Prs_SmtBuild( p );
- }
Prs_SmtFree( p );
return pNtk;
}
+Wlc_Ntk_t * Wlc_ReadSmt( char * pFileName )
+{
+ Wlc_Ntk_t * pNtk = NULL;
+ Prs_Smt_t * p = NULL;
+ char * pBuffer, * pLimit;
+ pBuffer = Prs_SmtLoadFile( pFileName, &pLimit );
+ if ( pBuffer == NULL )
+ return NULL;
+ pNtk = Wlc_ReadSmtBuffer( pFileName, pBuffer, pLimit );
+ ABC_FREE( pBuffer );
+ return pNtk;
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 22:18:42 +0000