From c906dfb7489c1e97cf0f80be2aaaef23d65a8ac2 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 15 May 2024 09:33:57 -0700
Subject: [PATCH] Upgrading "twoexact" to read relations in an updated format.

---
 src/misc/vec/vecWrd.h | 22 ++++++++++++++++++++++
 src/sat/bmc/bmcMaj.c  | 29 ++++++++++++++++++++++++++++-
 2 files changed, 50 insertions(+), 1 deletion(-)

diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h
index b0d16efe6..5bfee43fb 100644
--- a/src/misc/vec/vecWrd.h
+++ b/src/misc/vec/vecWrd.h
@@ -1368,6 +1368,27 @@ static inline void Vec_WrdDumpBool( char * pFileName, Vec_Wrd_t * p, int nWords,
         printf( "Written %d bits of simulation data for %d objects into file \"%s\".\n", nBits, Vec_WrdSize(p)/nWords, pFileName );
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_WrdPrintBin( Vec_Wrd_t * p, int nWords )
+{
+    int i, k, nNodes = Vec_WrdSize(p) / nWords;
+    assert( Vec_WrdSize(p) % nWords == 0 );
+    printf( "The array contains %d bit-strings of %d bits:\n", nNodes, 64*nWords );
+    for ( i = 0; i < nNodes; i++, printf("\n") )
+        for ( k = 0; k < 64*nWords; k++ )
+            printf( "%d", Abc_InfoHasBit((unsigned*)Vec_WrdEntryP(p, i*nWords), k) );
+}
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -1396,6 +1417,7 @@ static inline void Vec_WrdPrintHex( Vec_Wrd_t * p, int nWords )
 {
     int i, nNodes = Vec_WrdSize(p) / nWords;
     assert( Vec_WrdSize(p) % nWords == 0 );
+    printf( "The array contains %d bit-strings of %d bits:\n", nNodes, 64*nWords );
     for ( i = 0; i < nNodes; i++ )
         Vec_WrdDumpHexOne( stdout, Vec_WrdEntryP(p, i*nWords), nWords );
 }
diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
index 40ecd4a5e..1a7395727 100644
--- a/src/sat/bmc/bmcMaj.c
+++ b/src/sat/bmc/bmcMaj.c
@@ -23,6 +23,7 @@
 #include "misc/util/utilTruth.h"
 #include "sat/glucose/AbcGlucose.h"
 #include "aig/miniaig/miniaig.h"
+#include "base/io/ioResub.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -3714,9 +3715,35 @@ void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName )
 {
     Mini_Aig_t * pMini = NULL;
     Vec_Wrd_t * vSimsDiv = NULL, * vSimsOut = NULL;
-    int nDivs, nOuts, nVars = Exa6_ReadFile( pFileName, &vSimsDiv, &vSimsOut, &nDivs, &nOuts );
+    int i, k, nDivs, nOuts, nVars = 0;
+    if ( !strcmp(pFileName + strlen(pFileName) - 3, "rel") )
+        nVars = Exa6_ReadFile( pFileName, &vSimsDiv, &vSimsOut, &nDivs, &nOuts );
+    else if ( !strcmp(pFileName + strlen(pFileName) - 3, "pla") ) {
+        Abc_RData_t * p  = Abc_ReadPla( pFileName );
+        Abc_RData_t * p2 = p ? Abc_RData2Rel( p ) : NULL;
+        if ( !p || !p2 ) return;
+        //Abc_WritePla(p, "_/_rel/test.pla", 0);
+        //Abc_WritePla(p2, "_/_rel/test2.pla", 1);        
+        nDivs = 0;
+        nOuts = p->nOuts;
+        nVars = p->nIns;
+        vSimsDiv = Vec_WrdStart( p->nPats );
+        for ( k = 0; k < p->nIns; k++ )
+            for ( i = 0; i < p->nPats; i++ )
+                if ( Abc_RDataGetIn(p2, k, i) )
+                    Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsDiv, i), 1+k);
+        vSimsOut = Vec_WrdStart( 1 << p->nOuts );
+        for ( k = 0; k < (1 << p->nOuts); k++ )
+            for ( i = 0; i < p->nPats; i++ )
+                if ( Abc_RDataGetOut(p2, k, i) )
+                    Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsOut, i), k);
+    }
+    else
+        printf( "Unknown file extension in file \"%s\".\n", pFileName );        
     if ( nVars == 0 )
         return;
+    //Vec_WrdPrintBin( vSimsDiv, 1 );
+    //Vec_WrdPrintBin( vSimsOut, 1 );
     Exa6_SortSims( vSimsDiv, vSimsOut );
     pMini = Exa_ManExactSynthesis6Int( vSimsDiv, vSimsOut, nVars, nDivs, nOuts, pPars->nNodes, pPars->fOnlyAnd, pPars->fVerbose );
     Vec_WrdFreeP( &vSimsDiv );