From 8eb651c3d380168aeb752f90f16b37fff6d39142 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 10 Jun 2022 16:55:12 -0700
Subject: Adding command to check resub problem solution.

---
 src/aig/gia/giaResub6.c | 52 +++++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 50 insertions(+), 2 deletions(-)

(limited to 'src/aig/gia/giaResub6.c')

diff --git a/src/aig/gia/giaResub6.c b/src/aig/gia/giaResub6.c
index 567bf30b..3203a699 100644
--- a/src/aig/gia/giaResub6.c
+++ b/src/aig/gia/giaResub6.c
@@ -119,7 +119,7 @@ Res6_Man_t * Res6_ManRead( char * pFileName )
         printf( "Cannot open input file \"%s\".\n", pFileName );
     else
     {
-        int i, k, nIns, nNodes, nOuts, nPats, iLit = 0;
+        int i, k, nIns, nNodes, nOuts, nPats;
         char Temp[100], Buffer[100];
         char * pLine = fgets( Buffer, 100, pFile );
         if ( pLine == NULL )
@@ -279,11 +279,57 @@ static inline void Res6_LitPrint( int iLit, int nDivs )
             printf( "%d", Abc_Lit2Var(iLit) );
     }
 }
+Vec_Int_t * Res6_FindSupport( Vec_Int_t * vSol, int nDivs )
+{
+    int i, iLit;
+    Vec_Int_t * vSupp = Vec_IntAlloc( 10 );
+    Vec_IntForEachEntry( vSol, iLit, i )
+        if ( iLit >= 2 && iLit < 2*nDivs )
+            Vec_IntPushUnique( vSupp, Abc_Lit2Var(iLit) );
+    return vSupp;
+}
+void Res6_PrintSuppSims( Vec_Int_t * vSol, word ** ppLits, int nWords, int nDivs )
+{
+    Vec_Int_t * vSupp = Res6_FindSupport( vSol, nDivs );
+    int i, k, iObj;
+    Vec_IntForEachEntry( vSupp, iObj, i )
+    {
+        for ( k = 0; k < 64*nWords; k++ )
+            if ( Abc_TtGetBit(ppLits[2*iObj+1], k) )
+                printf( "0" );
+            else if ( Abc_TtGetBit(ppLits[2*iObj], k) )
+                printf( "1" );
+            else
+                printf( "-" );
+        printf( "\n" );
+    }
+    for ( k = 0; k < 64*nWords; k++ )
+    {
+        Vec_IntForEachEntry( vSupp, iObj, i )
+            if ( Abc_TtGetBit(ppLits[2*iObj+1], k) )
+                printf( "0" );
+            else if ( Abc_TtGetBit(ppLits[2*iObj+0], k) )
+                printf( "1" );
+            else
+                printf( "-" );
+        printf( "\n" );
+        if ( k == 9 )
+            break;
+    }
+    Vec_IntFree( vSupp );
+}                        
+int Res6_FindSupportSize( Vec_Int_t * vSol, int nDivs )
+{
+    Vec_Int_t * vSupp = Res6_FindSupport( vSol, nDivs );
+    int Res = Vec_IntSize(vSupp);
+    Vec_IntFree( vSupp );
+    return Res;
+}
 void Res6_PrintSolution( Vec_Int_t * vSol, int nDivs )
 {
     int iNode, nNodes = Vec_IntSize(vSol)/2-1;
     assert( Vec_IntSize(vSol) % 2 == 0 );
-    printf( "Solution:  In+Div = %d  Node = %d  Out = %d\n", nDivs-1, nNodes, 1 );
+    printf( "Solution:  In = %d  Div = %d  Node = %d  Out = %d\n", Res6_FindSupportSize(vSol, nDivs), nDivs-1, nNodes, 1 );
     for ( iNode = 0; iNode <= nNodes; iNode++ )
     {
         int * pLits = Vec_IntEntryP( vSol, 2*iNode );
@@ -386,6 +432,8 @@ void Res6_ManResubCheck( char * pFileNameRes, char * pFileNameSol, int fVerbose
             Res6_ManPrintProblem( p, 0 );
         if ( fVerbose )
             Res6_PrintSolution( vSol, p->nDivs );
+        //if ( fVerbose )
+        //    Res6_PrintSuppSims( vSol, p->ppLits, p->nWords, p->nDivs );
         Res6_ManResubVerify( p, vSol );
         Vec_IntFree( vSol );
         Res6_ManStop( p );
-- 
cgit v1.2.3