diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-02-11 18:09:15 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-02-11 18:09:15 -0800 |
commit | ea2d82ab141c5a162f2c2cf0adce74a21d911d8a (patch) | |
tree | 27fe7eee9a21fb9d014e23129310d424d4a70781 /src/base/wlc/wlcCom.c | |
parent | e363727c62d5fbbf0edadb73a02e4efa324e1509 (diff) | |
download | abc-ea2d82ab141c5a162f2c2cf0adce74a21d911d8a.tar.gz abc-ea2d82ab141c5a162f2c2cf0adce74a21d911d8a.tar.bz2 abc-ea2d82ab141c5a162f2c2cf0adce74a21d911d8a.zip |
Modifications to read SMTLIB file from stdin.
Diffstat (limited to 'src/base/wlc/wlcCom.c')
-rw-r--r-- | src/base/wlc/wlcCom.c | 53 |
1 files changed, 53 insertions, 0 deletions
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******************************************************************** |