Created a communication bridge.

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                                ///
 ////////////////////////////////////////////////////////////////////////