diff options
| -rw-r--r-- | src/misc/util/abc_global.h | 18 | ||||
| -rw-r--r-- | src/misc/util/utilBridge.c | 117 | ||||
| -rw-r--r-- | src/misc/util/utilFile.c | 58 |
3 files changed, 184 insertions, 9 deletions
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index 38a27fe7..9a5ee9de 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -256,17 +256,29 @@ enum Abc_VerbLevel ABC_VERBOSE = 2 }; +extern int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer ); + +// string printing +extern char * vnsprintf(const char* format, va_list args); +extern char * nsprintf(const char* format, ...); + static inline void Abc_Print( int level, const char * format, ... ) { + extern int in_bridge_mode; va_list args; -// if ( level > -2 ) -// return; if ( level == ABC_ERROR ) printf( "Error: " ); else if ( level == ABC_WARNING ) printf( "Warning: " ); va_start( args, format ); - vprintf( format, args ); + if ( in_bridge_mode ) + { + unsigned char * tmp = vnsprintf( format, args ); + Gia_ManToBridgeText( stdout, strlen(tmp), tmp ); + free( tmp ); + } + else + vprintf( format, args ); va_end( args ); } diff --git a/src/misc/util/utilBridge.c b/src/misc/util/utilBridge.c index fc847808..07760393 100644 --- a/src/misc/util/utilBridge.c +++ b/src/misc/util/utilBridge.c @@ -29,7 +29,6 @@ ABC_NAMESPACE_IMPL_START - //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -37,7 +36,10 @@ ABC_NAMESPACE_IMPL_START extern void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x ); extern unsigned Gia_ReadAigerDecode( unsigned char ** ppPos ); +extern void Gia_WriteAigerEncodeStr( Vec_Str_t * vStr, unsigned x ); +// this variable determines where the output goes +int in_bridge_mode = 0; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -54,7 +56,7 @@ extern unsigned Gia_ReadAigerDecode( unsigned char ** ppPos ); SeeAlso [] ***********************************************************************/ -Vec_Str_t * Gia_ManToBridgeVec( FILE * pFile, Gia_Man_t * p ) +Vec_Str_t * Gia_ManToBridgeVec( Gia_Man_t * p ) { Vec_Str_t * vBuffer; Gia_Obj_t * pObj; @@ -126,13 +128,113 @@ Vec_Str_t * Gia_ManToBridgeVec( FILE * pFile, Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Gia_ManToBridge( FILE * pFile, Gia_Man_t * pMan ) +void Gia_CreateHeader( FILE * pFile, int Type, int Size, unsigned char * pBuffer ) +{ + fprintf( pFile, "%.6d", Type ); + fprintf( pFile, " " ); + fprintf( pFile, "%.16d", Size ); + fprintf( pFile, " " ); + fwrite( pBuffer, Size, 1, pFile ); + fflush( pFile ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +#define BRIDGE_TEXT_MESSAGE 999996 +#define BRIDGE_RESULTS 101 +#define BRIDGE_ABS_NETLIST 107 +#define BRIDGE_BAD_ABS 105 + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManToBridgeText( FILE * pFile, int Size, unsigned char * pBuffer ) +{ + Gia_CreateHeader( pFile, BRIDGE_TEXT_MESSAGE, Size, pBuffer ); + return 1; +} +int Gia_ManToBridgeAbsNetlist( FILE * pFile, Gia_Man_t * p ) { Vec_Str_t * vBuffer; - vBuffer = Gia_ManToBridgeVec( pFile, pMan ); - fwrite( Vec_StrArray(vBuffer), 1, Vec_StrSize(vBuffer), pFile ); + vBuffer = Gia_ManToBridgeVec( p ); + Gia_CreateHeader( pFile, BRIDGE_ABS_NETLIST, Vec_StrSize(vBuffer), (unsigned char *)Vec_StrArray(vBuffer) ); Vec_StrFree( vBuffer ); - return 0; + return 1; +} +int Gia_ManToBridgeBadAbs( FILE * pFile ) +{ + Gia_CreateHeader( pFile, BRIDGE_BAD_ABS, 0, NULL ); + return 1; +} + +void Gia_ManFromBridgeHolds( FILE * pFile ) +{ + fputc( (char)3, pFile ); // true + fputc( (char)1, pFile ); // size of vector (Armin's encoding) + fputc( (char)0, pFile ); // number of the property (Armin's encoding) + fputc( (char)0, pFile ); // no invariant +} +void Gia_ManFromBridgeUnknown( FILE * pFile ) +{ + fputc( (char)0, pFile ); // undef + fputc( (char)1, pFile ); // size of vector (Armin's encoding) + fputc( (char)0, pFile ); // number of the property (Armin's encoding) +} +void Gia_ManFromBridgeCex( FILE * pFile, Abc_Cex_t * pCex ) +{ + int i, f, iBit; + Vec_Str_t * vStr = Vec_StrAlloc( 1000 ); + Vec_StrPush( vStr, (char)2 ); // false + Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding) + Vec_StrPush( vStr, (char)0 ); // number of the property (Armin's encoding) + Vec_StrPush( vStr, (char)1 ); // size of vector (Armin's encoding) + Gia_WriteAigerEncodeStr( vStr, pCex->iFrame ); // depth + Gia_WriteAigerEncodeStr( vStr, 1 ); // concrete + Gia_WriteAigerEncodeStr( vStr, pCex->iFrame ); // n frames + iBit = pCex->nRegs; + for ( f = 0; f <= pCex->iFrame; f++ ) + { + Gia_WriteAigerEncodeStr( vStr, pCex->nPis ); // num of inputs + for ( i = 0; i < pCex->nPis; i++ ) + Vec_StrPush( vStr, (char)(Abc_InfoHasBit(pCex->pData, iBit++)?3:2) ); // value + } + assert( iBit == pCex->nBits ); + Vec_StrPush( vStr, (char)1 ); // the number of frames (for a concrete counter-example) + for ( i = 0; i < pCex->nRegs; i++ ) + Vec_StrPush( vStr, (char)2 ); // always zero ?????????????? + fwrite( Vec_StrArray(vStr), Vec_StrSize(vStr), 1, pFile ); + Vec_StrFree( vStr ); +} +int Gia_ManToBridgeResult( FILE * pFile, int Result, Abc_Cex_t * pCex ) +{ + if ( Result == 0 ) // sat + Gia_ManFromBridgeCex( pFile, pCex ); + else if ( Result == 1 ) // unsat + Gia_ManFromBridgeHolds( pFile ); + else if ( Result == -1 ) // undef + Gia_ManFromBridgeUnknown( pFile ); + else assert( 0 ); + return 1; } @@ -222,6 +324,7 @@ Gia_Man_t * Gia_ManFromBridgeReadBody( int Size, unsigned char * pBuffer, Vec_I for ( i = 0; i < nFlops; i++ ) { iFan0 = Gia_ReadAigerDecode( &pBuffer ); + assert( (iFan0 & 3) == 2 ); Vec_IntPush( vInits, iFan0 & 3 ); // 0 = X value; 1 = not used; 2 = false; 3 = true iFan0 >>= 2; iFan0 = Abc_LitNotCond( Vec_IntEntry(vLits, iFan0 >> 1), iFan0 & 1 ); @@ -360,6 +463,8 @@ void Gia_ManFromBridgeTest( char * pFileName ) Gia_ManStop( p ); } + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/util/utilFile.c b/src/misc/util/utilFile.c index a25c5b2c..41438c57 100644 --- a/src/misc/util/utilFile.c +++ b/src/misc/util/utilFile.c @@ -154,6 +154,64 @@ int main(int argc, char** argv) } */ +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char* vnsprintf(const char* format, va_list args) +{ + unsigned n; + char* ret; + va_list args_copy; + + static FILE* dummy_file = NULL; + if (!dummy_file) + { +#if !defined(_MSC_VER) + dummy_file = fopen("/dev/null", "wb"); +#else + dummy_file = fopen("NUL", "wb"); +#endif + } + +#if defined(__va_copy) + __va_copy(args_copy, args); +#else + #if defined(va_copy) + va_copy(args_copy, args); + #else + args_copy = args; + #endif +#endif + n = vfprintf(dummy_file, format, args); + ret = ABC_ALLOC( char, n + 1 ); + ret[n] = (char)255; + args = args_copy; + vsprintf(ret, format, args); +#if !defined(__va_copy) && defined(va_copy) + va_end(args_copy); +#endif + assert(ret[n] == 0); + return ret; +} + +char* nsprintf(const char* format, ...) +{ + char* ret; + va_list args; + va_start(args, format); + ret = vnsprintf(format, args); + va_end(args); + return ret; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |