Various changes and bug fixes.

berkeley-abc · May 19, 2024 · c64f927 · c64f927
1 parent 3616fd8
commit c64f927
Show file tree

Hide file tree

Showing 8 changed files with 38 additions and 22 deletions.
diff --git a/src/aig/gia/giaCut.c b/src/aig/gia/giaCut.c
@@ -986,10 +986,16 @@ Vec_Wec_t * Gia_ManExploreCuts( Gia_Man_t * pGia, int nCutSize0, int nCuts0, int
         Abc_PrintTime( 0, "Time", Abc_Clock() - p->clkStart );
     }
     vCutsSel = Gia_ManFilterCuts( pGia, p->vCuts, nCutSize0, nCuts0 );
-    Gia_ManConsiderCuts( pGia, vCutsSel );
+    //Gia_ManConsiderCuts( pGia, vCutsSel );
     Gia_StoFree( p );
     return vCutsSel;
 }
+void Gia_ManExploreCutsTest( Gia_Man_t * pGia, int nCutSize0, int nCuts0, int fVerbose0 )
+{
+    Vec_Wec_t * vCutSel = Gia_ManExploreCuts( pGia, nCutSize0, nCuts0, fVerbose0 );
+    Vec_WecPrint( vCutSel, 0 );
+    Vec_WecFree( vCutSel );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
@@ -5952,7 +5952,9 @@ Gia_Man_t * Gia_ManDupWindow( Gia_Man_t * p, Vec_Int_t * vCut )
         pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     Gia_ManForEachObjVec( vOuts, p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
-    printf( "Derived window with %d inputs, %d internal nodes, and %d outputs: ", Vec_IntSize(vCut), Vec_IntSize(vInner), Vec_IntSize(vOuts) );
+    printf( "Derived window with %d inputs, %d internal nodes, and %d outputs.\n", Vec_IntSize(vCut), Vec_IntSize(vInner), Vec_IntSize(vOuts) );
+    printf( "Outputs: " );
+    Vec_IntPrint( vOuts );
     Vec_IntFree( vInner );
     Vec_IntFree( vOuts );
     return pNew;

diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c
@@ -1011,16 +1011,14 @@ Vec_Int_t * Gia_ManGenCombs( Gia_Man_t * p, Vec_Int_t * vInsOuts, int fVerbose )
         Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
     return vRes;
 }
-
-
 void Gia_ManGenRel( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, char * pFileName, int fVerbose )
 {
     Vec_Int_t * vRes = Gia_ManGenCombs( pGia, vInsOuts, fVerbose ); int i, k, Mask;
     if ( vRes == NULL ) {
         printf( "Enumerating solutions did not succeed.\n" );
         return;
     }
-    Abc_RData_t * p = Abc_RDataStart( nIns, Vec_IntSize(vInsOuts)-nIns, Vec_IntSize(vRes) );    
+    Abc_RData_t * p2, * p = Abc_RDataStart( nIns, Vec_IntSize(vInsOuts)-nIns, Vec_IntSize(vRes) );    
     Vec_IntForEachEntry( vRes, Mask, i ) {
         for ( k = 0; k < Vec_IntSize(vInsOuts); k++ )
             if ( (Mask >> (Vec_IntSize(vInsOuts)-1-k)) & 1 ) { // the bit is 1
@@ -1035,6 +1033,9 @@ void Gia_ManGenRel( Gia_Man_t * pGia, Vec_Int_t * vInsOuts, int nIns, char * pFi
             }
     }
     Abc_WritePla( p, pFileName, 0 );
+    p2 = Abc_RData2Rel( p );
+    Abc_WritePla( p2, Extra_FileNameGenericAppend(pFileName, "_rel.pla"), 1 );
+    Abc_RDataStop( p2 );
     Abc_RDataStop( p );
     Vec_IntFree( vRes );
 }

diff --git a/src/aig/gia/giaResub.c b/src/aig/gia/giaResub.c
@@ -2117,7 +2117,9 @@ void Gia_ManResubRecordSolution( char * pFileName, Vec_Int_t * vRes, int nDivs )
 Gia_Man_t * Gia_ManResubUnateOne( char * pFileName, int nLimit, int nDivMax, int fWriteSol, int fVerbose )
 {
     Gia_Man_t * pNew = NULL;
-    Abc_RData_t * p = Abc_ReadPla( pFileName ); assert( p->nOuts == 1 );
+    Abc_RData_t * p = Abc_ReadPla( pFileName ); 
+    if ( p == NULL ) return NULL;
+    assert( p->nOuts == 1 );
     Vec_Ptr_t * vDivs = Vec_PtrAlloc( 2+p->nIns );
     Vec_Int_t * vRes = Vec_IntAlloc( 100 );
     Vec_PtrPush( vDivs, Vec_WrdEntryP(p->vSimsOut, 0*p->nSimWords) );
@@ -2132,7 +2134,7 @@ Gia_Man_t * Gia_ManResubUnateOne( char * pFileName, int nLimit, int nDivMax, int
     for ( k = 0; k < ArraySize; k++ )
         Vec_IntPush( vRes, pArray[k] );
     if ( ArraySize ) {
-        //printf( "Divisors = %d. Solution: ", Vec_PtrSize(vDivs) ), Vec_IntPrint( vRes );
+        //Vec_IntPrint( vRes );
         Vec_Wec_t * vGates = Vec_WecStart(1);
         Vec_IntAppend( Vec_WecEntry(vGates, 0), vRes );
         pNew = Gia_ManConstructFromGates( vGates, Vec_PtrSize(vDivs) );

diff --git a/src/aig/gia/giaResub6.c b/src/aig/gia/giaResub6.c
@@ -235,7 +235,7 @@ void Res6_ManWrite( char * pFileName, Res6_Man_t * p )
 void Res6_ManPrintProblem( Res6_Man_t * p, int fVerbose )
 {
     int i, nInputs = (p->nIns && p->nIns < 6) ? p->nIns : 6;
-    printf( "Problem:   In = %d  Div = %d  Out = %d   Pat = %d\n", p->nIns, p->nDivs - p->nIns - 1, p->nOuts, p->nPats );
+    printf( "Problem:   In = %d  Div = %d  Out  = %d  Pat = %d\n", p->nIns, p->nDivs - p->nIns - 1, p->nOuts, p->nPats );
     if ( !fVerbose )
         return;
     printf( "%02d : %s\n", 0, "const0" );

diff --git a/src/aig/gia/giaSupps.c b/src/aig/gia/giaSupps.c
@@ -1129,7 +1129,9 @@ Gia_Man_t * Supp_GenerateGia( Vec_Int_t * vRes, Vec_Int_t * vDivs )
 Gia_Man_t * Supp_ManSolveOne( char * pFileName, int nIters, int nRounds, int fWriteSol, int fVerbose )
 {
     //Abc_Random(1);
-    Abc_RData_t * p = Abc_ReadPla( pFileName ); assert( p->nOuts == 1 );
+    Abc_RData_t * p = Abc_ReadPla( pFileName ); 
+    if ( p == NULL ) return NULL;
+    assert( p->nOuts == 1 );
     Vec_Int_t * vDivs = Vec_IntAlloc( 100 );
     Vec_Int_t * vRes  = Supp_ManCompute( p->vSimsOut, NULL, NULL, p->vSimsIn, NULL, p->nSimWords, NULL, &vDivs, nIters, nRounds, fVerbose );
     if ( fVerbose && vDivs ) printf( "Divisors: " ), Vec_IntPrint( vDivs );

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
@@ -53250,7 +53250,10 @@ int Abc_CommandAbc9Window( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( argc == globalUtilOptind )
     {
-        Abc_Print( -1, "Abc_CommandAbc9Window(): Node IDs should be given on the command line.\n" );
+        int nCutSize = 6, nCuts = 30;
+        extern void Gia_ManExploreCutsTest( Gia_Man_t * pGia, int nCutSize, int nCuts, int fVerbose );
+        printf( "Here are %d the most frequently appearing %d-cuts:\n", nCutSize, nCuts );
+        Gia_ManExploreCutsTest( pAbc->pGia, nCutSize, nCuts, fVerbose );
         return 0;
     }
     if ( argc-globalUtilOptind < 1 )

diff --git a/src/sat/bmc/bmcMaj.c b/src/sat/bmc/bmcMaj.c
@@ -3420,7 +3420,7 @@ void Exa6_ManGenMint( Exa6_Man_t * p, int iMint, int fOnlyAnd, int fFancy )
         assert( t );
         if ( ~t )
         {
-            Abc_Tt6IsopCover( t, t, p->nOuts, pCover, &nCubes );
+            Abc_Tt6IsopCover( ~t, ~t, p->nOuts, pCover, &nCubes );
             for ( c = 0; c < nCubes; c++ )
             {
                 int nLits = 0;
@@ -3664,7 +3664,7 @@ Vec_Wrd_t * Exa6_ManTransformOutputs( Vec_Wrd_t * vOuts, int nOuts )
 Vec_Wrd_t * Exa6_ManTransformInputs( Vec_Wrd_t * vIns )
 {
     Vec_Wrd_t * vRes = Vec_WrdAlloc( Vec_WrdSize(vIns) );
-    int i, Polar = Vec_WrdEntry( vIns, 0 ); word Entry;
+    int i; word Entry, Polar = Vec_WrdEntry( vIns, 0 );
     Vec_WrdForEachEntry( vIns, Entry, i )
         Vec_WrdPush( vRes, Entry ^ Polar );
     return vRes;
@@ -3679,7 +3679,7 @@ void Exa_ManExactPrint( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut, int nDivs, i
         Abc_TtPrintBits( &Entry, 1 << nOuts );
     printf( "\n" );
 }
-Mini_Aig_t * Exa_ManExactSynthesis6Int( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut, int nVars, int nDivs, int nOuts, int nNodes, int fOnlyAnd, int fVerbose )
+Mini_Aig_t * Exa_ManExactSynthesis6Int( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsOut, int nVars, int nDivs, int nOuts, int nNodes, int fOnlyAnd, int fVerbose, char * pFileName )
 {
     Mini_Aig_t * pTemp, * pMini; 
     Vec_Wrd_t * vSimsDiv2, * vSimsOut2;
@@ -3701,10 +3701,10 @@ Mini_Aig_t * Exa_ManExactSynthesis6Int( Vec_Wrd_t * vSimsDiv, Vec_Wrd_t * vSimsO
             pMini = Mini_AigDupCompl( pTemp = pMini, DivCompl, OutCompl );
             Mini_AigStop( pTemp );        
         }
-        Mini_AigerWrite( "exa6.aig", pMini, 1 );
-        if ( nVars <= 6 )
-            Exa_ManMiniVerify( pMini, vSimsDiv, vSimsOut );
-        printf( "\n" );
+        Mini_AigerWrite( Extra_FileNameGenericAppend(pFileName, "_twoexact.aig"), pMini, 1 );
+        //if ( nVars <= 6 )
+        //    Exa_ManMiniVerify( pMini, vSimsDiv, vSimsOut );
+        //printf( "\n" );
         //Mini_AigStop( pMini );
     }
     Vec_WrdFreeP( &vSimsDiv2 );
@@ -3725,14 +3725,14 @@ void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName )
         nDivs = 0;
         nOuts = p->nOuts;
         nVars = p->nIns;
-        vSimsDiv = Vec_WrdStart( p->nPats );
+        vSimsDiv = Vec_WrdStart( p2->nPats );
         for ( k = 0; k < p->nIns; k++ )
-            for ( i = 0; i < p->nPats; i++ )
+            for ( i = 0; i < p2->nPats; i++ )
                 if ( Abc_RDataGetIn(p2, k, i) )
                     Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsDiv, i), 1+k);
-        vSimsOut = Vec_WrdStart( 1 << p->nOuts );
+        vSimsOut = Vec_WrdStart( p2->nPats );
         for ( k = 0; k < (1 << p->nOuts); k++ )
-            for ( i = 0; i < p->nPats; i++ )
+            for ( i = 0; i < p2->nPats; i++ )
                 if ( Abc_RDataGetOut(p2, k, i) )
                     Abc_InfoSetBit((unsigned *)Vec_WrdEntryP(vSimsOut, i), k);
         Abc_RDataStop( p );
@@ -3745,7 +3745,7 @@ void Exa_ManExactSynthesis6( Bmc_EsPar_t * pPars, char * pFileName )
     //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 );
+    pMini = Exa_ManExactSynthesis6Int( vSimsDiv, vSimsOut, nVars, nDivs, nOuts, pPars->nNodes, pPars->fOnlyAnd, pPars->fVerbose, pFileName );
     Vec_WrdFreeP( &vSimsDiv );
     Vec_WrdFreeP( &vSimsOut );
     if ( pMini ) Mini_AigStop( pMini );