Supporting new resub problem format.

6 files changed, 200 insertions, 2 deletions

diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 431be5b7..d8130550 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -3080,7 +3080,55 @@ Gia_Man_t * Gia_ManTransformCond( Gia_Man_t * p )
     Abc_PrintTime( 0, "Time", Abc_Clock() - clk );
     return NULL;
 }
-
+void Gia_ManWriteSol( Gia_Man_t * p, char * pFileName )
+{
+    char * pBasicName = Extra_FileNameGeneric( pFileName ); 
+    char * pFileName2 = Abc_UtilStrsavTwo( pBasicName, ".sol" ); 
+    FILE * pFile = fopen( pFileName2, "wb" );
+    ABC_FREE( pBasicName );
+    if ( pFile == NULL )
+        printf( "Cannot open output file \"%s\".\n", pFileName2 );
+    else
+    {
+        Gia_Obj_t * pObj; int i;
+        Gia_ManForEachAnd( p, pObj, i )
+            fprintf( pFile, "%d %d ", Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i) );
+        Gia_ManForEachCo( p, pObj, i )
+            fprintf( pFile, "%d %d ", Gia_ObjFaninLit0p(p, pObj), Gia_ObjFaninLit0p(p, pObj) );
+        fclose( pFile );   
+        printf( "Finished writing solution file \"%s\".\n", pFileName2 );
+    }
+    ABC_FREE( pFileName2 );
+}
+void Gia_ManWriteResub( Gia_Man_t * p, char * pFileName )
+{
+    FILE * pFile = fopen( pFileName, "wb" ); 
+    if ( pFile == NULL )
+        printf( "Cannot open output file \"%s\".\n", pFileName );
+    else
+    {
+        Vec_Wrd_t * vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(p) );
+        Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( p, vSimsPi, 1 );
+        int i, k, nWords = Vec_WrdSize(vSimsPi) / Gia_ManCiNum(p);
+        word * pTemp = ABC_ALLOC( word, nWords );
+        fprintf( pFile, "%d %d %d %d\n", Gia_ManCiNum(p), 0, Gia_ManCoNum(p), 1 << Gia_ManCiNum(p) );
+        for ( i = 0; i < Gia_ManCiNum(p); i++ )
+            Abc_TtPrintBinary1( pFile, Vec_WrdEntryP(vSimsPi, i*nWords), Gia_ManCiNum(p) ), fprintf(pFile, "\n");
+        for ( i = 0; i < (1 << Gia_ManCoNum(p)); i++ )
+        {
+            Abc_TtFill( pTemp, nWords );
+            for ( k = 0; k < Gia_ManCoNum(p); k++ )
+                Abc_TtAndCompl( pTemp, pTemp, 0, Vec_WrdEntryP(vSimsPo, k*nWords), !((i>>k)&1), nWords );
+            Abc_TtPrintBinary1( pFile, pTemp, Gia_ManCiNum(p) ), fprintf(pFile, "\n");
+        }
+        ABC_FREE( pTemp );
+        fclose( pFile );
+        Vec_WrdFree( vSimsPi );
+        Vec_WrdFree( vSimsPo );
+        printf( "Finished writing resub file \"%s\".\n", pFileName );
+        Gia_ManWriteSol( p, pFileName );
+    }
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 26bfb1f4..9b3d288a 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -84,6 +84,7 @@ static int IoCommandWriteTruths ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteStatus ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteSmv    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteJson   ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteResub  ( Abc_Frame_t * pAbc, int argc, char **argv );
 
 extern void Abc_FrameCopyLTLDataBase( Abc_Frame_t *pAbc, Abc_Ntk_t * pNtk );
 
@@ -155,6 +156,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_status",  IoCommandWriteStatus,  0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_smv",     IoCommandWriteSmv,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_json",    IoCommandWriteJson,    0 );
+    Cmd_CommandAdd( pAbc, "I/O", "&write_resub",  IoCommandWriteResub,   0 );
 }
 
 /**Function*************************************************************
@@ -3480,6 +3482,57 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandWriteResub( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    extern void Gia_ManWriteResub( Gia_Man_t * p, char * pFileName );
+    char * pFileName;
+    int c;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+    pFileName = argv[globalUtilOptind];
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "IoCommandWriteResub(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManCiNum(pAbc->pGia) > 20 )
+    {
+        Abc_Print( -1, "IoCommandWriteResub(): The number of inputs is wrong.\n" );
+        return 1;
+    }
+    Gia_ManWriteResub( pAbc->pGia, pFileName );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: &write_resub [-ch] <file>\n" );
+    fprintf( pAbc->Err, "\t         write the network in resub format\n" );
+    fprintf( pAbc->Err, "\t-h     : print the help message\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write (extension .json)\n" );
+    return 1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c
index bb6d0a31..377299fd 100644
--- a/src/base/main/mainUtils.c
+++ b/src/base/main/mainUtils.c
@@ -160,7 +160,7 @@ void Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName )
 void Abc_UtilsSource( Abc_Frame_t * pAbc )
 {  
 #ifdef WIN32
-    if ( Cmd_CommandExecute(pAbc, "source -s abc.rc") )
+    if ( Cmd_CommandExecute(pAbc, "source abc.rc") )
     {
         if ( Cmd_CommandExecute(pAbc, "source ..\\abc.rc") == 0 )
             printf( "Loaded \"abc.rc\" from the parent directory.\n" );
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index d9efa55f..bc8ac3f0 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1471,6 +1471,24 @@ static inline void Abc_TtPrintBinary( word * pTruth, int nVars )
             printf( "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
     printf( "\n" );
 }
+static inline void Abc_TtPrintBinary1( FILE * pFile, word * pTruth, int nVars )
+{
+    word * pThis, * pLimit = pTruth + Abc_TtWordNum(nVars);
+    int k, Limit = Abc_MinInt( 64, (1 << nVars) );
+    assert( nVars >= 2 );
+    for ( pThis = pTruth; pThis < pLimit; pThis++ )
+        for ( k = 0; k < Limit; k++ )
+            fprintf( pFile, "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
+}
+static inline void Abc_TtPrintBinary2( FILE * pFile, word * pTruth, int nVars )
+{
+    word * pThis;
+    int k, Limit = Abc_MinInt( 64, (1 << nVars) );
+    assert( nVars >= 2 );
+    for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
+        for ( k = Limit-1; k >= 0; k-- )
+            fprintf( pFile, "%d", Abc_InfoHasBit( (unsigned *)pThis, k ) );
+}
 
 /**Function*************************************************************
 
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index c15369d2..e4ea6cfe 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -61,6 +61,8 @@ struct Vec_Int_t_
     for ( i = Start; (i < Stop) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
 #define Vec_IntForEachEntryReverse( vVec, pEntry, i )                                       \
     for ( i = Vec_IntSize(vVec) - 1; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- )
+#define Vec_IntForEachEntryReverseStart( vVec, pEntry, i, Start )                           \
+    for ( i = Start; (i >= 0) && (((pEntry) = Vec_IntEntry(vVec, i)), 1); i-- )
 #define Vec_IntForEachEntryTwo( vVec1, vVec2, Entry1, Entry2, i )                           \
     for ( i = 0; (i < Vec_IntSize(vVec1)) && (((Entry1) = Vec_IntEntry(vVec1, i)), 1) && (((Entry2) = Vec_IntEntry(vVec2, i)), 1); i++ )
 #define Vec_IntForEachEntryTwoStart( vVec1, vVec2, Entry1, Entry2, i, Start )               \
diff --git a/src/proof/acec/acecBo.c b/src/proof/acec/acecBo.c
index 9cddcd13..51af0214 100644
--- a/src/proof/acec/acecBo.c
+++ b/src/proof/acec/acecBo.c
@@ -21,6 +21,7 @@
 #include "acecInt.h"
 #include "misc/vec/vecWec.h"
 #include "misc/extra/extra.h"
+#include "misc/util/utilTruth.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -207,6 +208,82 @@ void Acec_DetectBoothTest( Gia_Man_t * p )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManResubTest4()
+{
+    Vec_Int_t * vRes = Vec_IntAlloc( 100 );
+    unsigned T = 0xF335ACC0;
+    int a, b, c;
+    int i, k, f, y;
+    int Count = 0;
+    for ( a = 0; a < 2; a++ )
+    {
+        unsigned A = s_Truths5[a];
+        for ( b = 0; b < 3; b++ )
+        {
+            unsigned B = s_Truths5[2+b];
+            for ( c = 0; c < 3; c++ ) if ( c != b )
+            {
+                unsigned C = s_Truths5[2+c];
+                Vec_IntPush( vRes, A & B &  C );
+                Vec_IntPush( vRes, A & B & ~C );
+            }
+        }
+    }
+    printf( "Size = %d.\n", Vec_IntSize(vRes) );
+    for ( i = 0; i < (1 << Vec_IntSize(vRes)); i++ )
+    {
+        unsigned F[7] = {0};
+        unsigned Y[3] = {0};
+        if ( Abc_TtCountOnes( (word)i ) >= 8 )
+            continue;
+        for ( f = k = 0; k < Vec_IntSize(vRes); k++ )
+            if ( ((i >> k) & 1) )
+                F[f++] = Vec_IntEntry(vRes, k);
+        {
+            unsigned S1 = (F[0] & F[1]) | (F[0] & F[2]) | (F[1] & F[2]);
+            unsigned C1 = F[0] ^ F[1] ^ F[2];
+            unsigned S2 = (F[3] & F[4]) | (F[3] & F[5]) | (F[4] & F[5]);
+            unsigned C2 = F[3] ^ F[4] ^ F[5];
+            unsigned S3 = (F[6] & S1) | (F[6] & S2) | (S1 & S2);
+            unsigned C3 = F[6] ^ S1 ^ S2;
+            unsigned S4 = (C1 & C2) | (C1 & C3) | (C2 & C3);
+            unsigned C4 = C1 ^ C2 ^ C3;
+            Y[0] = S3;
+            Y[1] = S4;
+            Y[2] = C4;
+        }
+        for ( y = 0; y < 3; y++ )
+            if ( Y[y] == T )
+                printf( "Found!\n" );
+        Count++;
+    }
+    printf( "Tried = %d.\n", Count );
+    Vec_IntFree( vRes );
+}
+void Gia_ManResubTest5()
+{
+    unsigned T = 0xF335ACC0;
+    int i;
+    for ( i = 0; i < 4; i++ )
+    {
+        unsigned x = i%2 ? Abc_Tt5Cofactor1(T, 0) : Abc_Tt5Cofactor0(T, 0);
+        unsigned y = i/2 ? Abc_Tt5Cofactor1(x, 1) : Abc_Tt5Cofactor0(x, 1);
+        word F = y;
+        F |= F << 32;
+        //Dau_DsdPrintFromTruth2( &F, 6 ); printf( "\n" );
+    }
+}
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////