Concurrency for Boolean matching.

src/aig/gia/giaKf.c

@@ -21,7 +21,7 @@
 #include "gia.h"
 #include "misc/vec/vecSet.h"
 
-//#ifdef ABC_USE_PTHREADS
+#ifdef ABC_USE_PTHREADS
 
 #ifdef _WIN32
 #include "../lib/pthread.h"
@@ -30,7 +30,7 @@
 #include <unistd.h>
 #endif
 
-//#endif
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -38,6 +38,13 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifndef ABC_USE_PTHREADS
+
+void Kf_ManSetDefaultPars( Jf_Par_t * pPars ) {}
+Gia_Man_t * Kf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) { return NULL; }
+
+#else // pthreads are used
+
 #define KF_LEAF_MAX  16
 #define KF_CUT_MAX   32
 #define KF_PROC_MAX  32
@@ -1328,6 +1335,7 @@ Gia_Man_t * Kf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#endif // pthreads are used
 
 ABC_NAMESPACE_IMPL_END
 

src/base/abci/abc.c

@@ -15489,7 +15489,14 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
         if ( p == NULL )
+        {
+            if ( LutSize > DAU_MAX_VAR || pPars->nLutSize > DAU_MAX_VAR )
+            {
+                printf( "Size of required DSD manager (%d) exceeds the precompiled limit (%d) (change parameter DAU_MAX_VAR).\n", LutSize, DAU_MAX_VAR );
+                return 0;
+            }
             Abc_FrameSetManDsd( If_DsdManAlloc(pPars->nLutSize, LutSize) );
+        }
     }
 
     if ( pPars->fUserRecLib )
@@ -15913,7 +15920,7 @@ int Abc_CommandDsdFree( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         if ( !Abc_FrameReadManDsd2() )
         {
-            Abc_Print( 1, "The DSD manager is not started.\n" );
+            Abc_Print( -1, "The DSD manager is not started.\n" );
             return 0;
         }
         Abc_FrameSetManDsd2( NULL );
@@ -15922,7 +15929,7 @@ int Abc_CommandDsdFree( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         if ( !Abc_FrameReadManDsd() )
         {
-            Abc_Print( 1, "The DSD manager is not started.\n" );
+            Abc_Print( -1, "The DSD manager is not started.\n" );
             return 0;
         }
         Abc_FrameSetManDsd( NULL );
@@ -16000,7 +16007,7 @@ int Abc_CommandDsdPs( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         if ( !Abc_FrameReadManDsd2() )
         {
-            Abc_Print( 1, "The DSD manager is not started.\n" );
+            Abc_Print( -1, "The DSD manager is not started.\n" );
             return 0;
         }
         If_DsdManPrint( (If_DsdMan_t *)Abc_FrameReadManDsd2(), NULL, Number, Support, fOccurs, fTtDump, fVerbose );
@@ -16009,7 +16016,7 @@ int Abc_CommandDsdPs( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         if ( !Abc_FrameReadManDsd() )
         {
-            Abc_Print( 1, "The DSD manager is not started.\n" );
+            Abc_Print( -1, "The DSD manager is not started.\n" );
             return 0;
         }
         If_DsdManPrint( (If_DsdMan_t *)Abc_FrameReadManDsd(), NULL, Number, Support, fOccurs, fTtDump, fVerbose );
@@ -16043,10 +16050,10 @@ usage:
 int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     char * pStruct = NULL;
-    int c, fVerbose = 0, fFast = 0, fAdd = 0, fSpec = 0, LutSize = 0, nConfls = 10000;
+    int c, fVerbose = 0, fFast = 0, fAdd = 0, fSpec = 0, LutSize = 0, nConfls = 10000, nProcs = 1;
     If_DsdMan_t * pDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd();
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCSfasvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCPSfasvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -16070,6 +16077,15 @@ int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
             nConfls = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
             break;
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-P\" should be followed by a floating point number.\n" );
+                goto usage;
+            }
+            nProcs = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            break;
         case 'S':
             if ( globalUtilOptind >= argc )
             {
@@ -16099,20 +16115,21 @@ int Abc_CommandDsdTune( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_FrameReadManDsd() )
     {
-        Abc_Print( 1, "The DSD manager is not started.\n" );
+        Abc_Print( -1, "The DSD manager is not started.\n" );
         return 0;
     }
     if ( pStruct )
-        Id_DsdManTuneStr( pDsdMan, pStruct, nConfls, fVerbose );
+        Id_DsdManTuneStr( pDsdMan, pStruct, nConfls, nProcs, fVerbose );
     else
         If_DsdManTune( pDsdMan, LutSize, fFast, fAdd, fSpec, fVerbose );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dsd_tune [-KC num] [-fasvh] [-S str]\n" );
+    Abc_Print( -2, "usage: dsd_tune [-KCP num] [-fasvh] [-S str]\n" );
     Abc_Print( -2, "\t         tunes DSD manager for the given LUT size\n" );
     Abc_Print( -2, "\t-K num : LUT size used for tuning [default = %d]\n",        LutSize );
     Abc_Print( -2, "\t-C num : the maximum number of conflicts [default = %d]\n", nConfls );
+    Abc_Print( -2, "\t-P num : the maximum number of processes [default = %d]\n", nProcs );
     Abc_Print( -2, "\t-f     : toggles using fast check [default = %s]\n",        fFast? "yes": "no" );
     Abc_Print( -2, "\t-a     : toggles adding tuning to the current one [default = %s]\n",    fAdd? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggles using specialized check [default = %s]\n", fSpec? "yes": "no" );
@@ -16153,7 +16170,7 @@ int Abc_CommandDsdMerge( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_FrameReadManDsd() )
     {
-        Abc_Print( 1, "The DSD manager is not started.\n" );
+        Abc_Print( -1, "The DSD manager is not started.\n" );
         return 0;
     }
     pArgvNew = argv + globalUtilOptind;
@@ -16223,7 +16240,7 @@ int Abc_CommandDsdClean( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_FrameReadManDsd() )
     {
-        Abc_Print( 1, "The DSD manager is not started.\n" );
+        Abc_Print( -1, "The DSD manager is not started.\n" );
         return 0;
     }
     If_DsdManClean( (If_DsdMan_t *)Abc_FrameReadManDsd(), fVerbose );
@@ -30804,6 +30821,16 @@ int Abc_CommandAbc9Dsdb( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Dsdb(): There is no AIG.\n" );
         return 1;
     }
+    if ( nLutSize > DAU_MAX_VAR )
+    {
+        printf( "Abc_CommandAbc9Dsdb(): Size of the required DSD manager (%d) exceeds the precompiled limit (%d) (change parameter DAU_MAX_VAR).\n", nLutSize, DAU_MAX_VAR );
+        return 0;
+    }
+    if ( Abc_FrameReadManDsd2() && nLutSize > If_DsdManVarNum(Abc_FrameReadManDsd2()) )
+    {
+        printf( "Abc_CommandAbc9Dsdb(): Incompatible size of the DSD manager (run \"dsd_free -b\").\n" );
+        return 0;
+    }
     if ( nLevelMax || nTimeWindow )
         pTemp = Gia_ManPerformDsdBalanceWin( pAbc->pGia, nLevelMax, nTimeWindow, nLutSize, nCutNum, nRelaxRatio, fVerbose );
     else
@@ -31329,7 +31356,14 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
             return 0;
         }
         if ( p == NULL )
+        {
+            if ( LutSize > DAU_MAX_VAR || pPars->nLutSize > DAU_MAX_VAR )
+            {
+                printf( "Size of required DSD manager (%d) exceeds the precompiled limit (%d) (change parameter DAU_MAX_VAR).\n", LutSize, DAU_MAX_VAR );
+                return 0;
+            }
             Abc_FrameSetManDsd( If_DsdManAlloc(pPars->nLutSize, LutSize) );
+        }
     }
 
     if ( pPars->fUserRecLib )

src/base/cmd/cmdStarter.c

@@ -248,7 +248,7 @@ void Cmd_RunStarter( char * pFileName, char * pBinary, char * pCommand, int nCor
     fflush( stdout );
 }
 
-#endif
+#endif // pthreads are used
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/wlc/wlcReadVer.c

@@ -134,7 +134,7 @@ int Wlc_PrsWriteErrorMessage( Wlc_Prs_t * p, char * pCur, const char * format, .
                 break;
         sprintf( p->sError, "%s (line %d): %s\n", p->pFileName, iLine+1, pMessage );
     }
-    free( pMessage );
+    ABC_FREE( pMessage );
     return 0;
 }
 void Wlc_PrsPrintErrorMessage( Wlc_Prs_t * p )

src/map/if/if.h

@@ -539,7 +539,7 @@ extern If_DsdMan_t *   If_DsdManAlloc( int nVars, int nLutSize );
 extern void            If_DsdManAllocIsops( If_DsdMan_t * p, int nLutSize );
 extern void            If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, int fOccurs, int fTtDump, int fVerbose );
 extern void            If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec, int fVerbose );
-extern void            Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbose );
+extern void            Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, int fVerbose );
 extern void            If_DsdManFree( If_DsdMan_t * p, int fVerbose );
 extern void            If_DsdManSave( If_DsdMan_t * p, char * pFileName );
 extern If_DsdMan_t *   If_DsdManLoad( char * pFileName );

src/map/if/ifTest.c

@@ -21,7 +21,7 @@
 #include "if.h"
 #include "aig/gia/gia.h"
 
-//#ifdef ABC_USE_PTHREADS
+#ifdef ABC_USE_PTHREADS
 
 #ifdef _WIN32
 #include "../lib/pthread.h"
@@ -30,7 +30,7 @@
 #include <unistd.h>
 #endif
 
-//#endif
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -38,6 +38,12 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifndef ABC_USE_PTHREADS
+
+// do nothing
+
+#else // pthreads are used
+
 static inline word * Gia_ParTestObj( Gia_Man_t * p, int Id )         { return (word *)p->pData + Id * p->iData; }
 static inline void   Gia_ParTestAlloc( Gia_Man_t * p, int nWords )   { assert( !p->pData ); p->pData = (unsigned *)ABC_ALLOC(word, Gia_ManObjNum(p) * nWords); p->iData = nWords; }
 static inline void   Gia_ParTestFree( Gia_Man_t * p )                { ABC_FREE( p->pData ); p->iData = 0; }
@@ -339,6 +345,8 @@ void Gia_ParTest( Gia_Man_t * p, int nWords, int nProcs )
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
+#endif // pthreads are used
+
 
 ABC_NAMESPACE_IMPL_END
 

src/map/if/ifTune.c

@@ -166,6 +166,10 @@ int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p )
             LutSize = Abc_MaxInt( LutSize, (int)p->Nodes[i].nFanins );
     return LutSize;
 }
+int Ifn_NtkInputNum( Ifn_Ntk_t * p )
+{
+    return p->nInps;
+}
 
 /**Function*************************************************************
 
@@ -240,18 +244,24 @@ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs )
     *pnObjs = MaxDef;
     return 1;
 }
-Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
+int Ifn_ErrorMessage( const char * format, ...  )
+{
+    char * pMessage;
+    va_list args;
+    va_start( args, format );
+    pMessage = vnsprintf( format, args );
+    va_end( args );
+    printf( "%s", pMessage );
+    ABC_FREE( pMessage );
+    return 0;
+}
+int Ifn_NtkParseInt( char * pStr, Ifn_Ntk_t * p )
 {
     int i, k, n, f, nFans, iFan;
-    static Ifn_Ntk_t P, * p = &P;
-    memset( p, 0, sizeof(Ifn_Ntk_t) );
     if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) )
-        return NULL;
+        return 0;
     if ( p->nInps > IFN_INS )
-    {
-        printf( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
-        return NULL;
-    }
+        return Ifn_ErrorMessage( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS );
     assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS );
     for ( i = p->nInps; i < p->nObjs; i++ )
     {
@@ -260,10 +270,7 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
             if ( pStr[k] == 'a' + i && pStr[k+1] == '=' )
                 break;
         if ( pStr[k] == 0 )
-        {
-            printf( "Cannot find definition of signal %c.\n", 'a' + i );
-            return NULL;
-        }
+            return Ifn_ErrorMessage( "Cannot find definition of signal %c.\n", 'a' + i );
         if ( pStr[k+2] == '(' )
             p->Nodes[i].Type = IF_DSD_AND, Next = ')';
         else if ( pStr[k+2] == '[' )
@@ -273,32 +280,20 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
         else if ( pStr[k+2] == '{' )
             p->Nodes[i].Type = IF_DSD_PRIME, Next = '}';
         else 
-        {
-            printf( "Cannot find openning operation symbol in the defition of of signal %c.\n", 'a' + i );
-            return NULL;
-        }
+            return Ifn_ErrorMessage( "Cannot find openning operation symbol in the defition of of signal %c.\n", 'a' + i );
         for ( n = k + 3; pStr[n]; n++ )
             if ( pStr[n] == Next )
                 break;
         if ( pStr[n] == 0 )
-        {
-            printf( "Cannot find closing operation symbol in the defition of of signal %c.\n", 'a' + i );
-            return NULL;
-        }
+            return Ifn_ErrorMessage( "Cannot find closing operation symbol in the defition of of signal %c.\n", 'a' + i );
         nFans = n - k - 3;
         if ( nFans < 1 || nFans > 8 )
-        {
-            printf( "Cannot find matching operation symbol in the defition of of signal %c.\n", 'a' + i );
-            return NULL;
-        }
+            return Ifn_ErrorMessage( "Cannot find matching operation symbol in the defition of of signal %c.\n", 'a' + i );
         for ( f = 0; f < nFans; f++ )
         {
             iFan = pStr[k + 3 + f] - 'a';
             if ( iFan < 0 || iFan >= i )
-            {
-                printf( "Fanin number %d is signal %d is out of range.\n", f, 'a' + i );
-                return NULL;
-            }
+                return Ifn_ErrorMessage( "Fanin number %d is signal %d is out of range.\n", f, 'a' + i );
             p->Nodes[i].Fanins[f] = iFan;
         }
         p->Nodes[i].nFanins = nFans;
@@ -316,19 +311,15 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
             }
 //    if ( p->nConstr )
 //        printf( "Total constraints = %d\n", p->nConstr );
-
-/*
-    // constraints
-    p->nConstr = 5;
-    p->pConstr[0] = (0 << 16) | 1;
-
-    p->pConstr[1] = (2 << 16) | 3;
-    p->pConstr[2] = (3 << 16) | 4;
-
-    p->pConstr[3] = (6 << 16) | 7;
-    p->pConstr[4] = (7 << 16) | 8;
-*/
-    return p;
+    return 1;
+}
+Ifn_Ntk_t * Ifn_NtkParse( char * pStr )
+{
+    Ifn_Ntk_t * p = ABC_CALLOC( Ifn_Ntk_t, 1 );
+    if ( Ifn_NtkParseInt( pStr, p ) )
+        return p;
+    ABC_FREE( p );
+    return NULL;
 }
 
 /**Function*************************************************************
@@ -805,6 +796,7 @@ void Ifn_NtkRead()
     Dau_DsdPrintFromTruth( pTruth, nVars );
     // get the given function
     RetValue = Ifn_NtkMatch( p, pTruth, nVars, 0, 1, 1 );
+    ABC_FREE( p );
 }
 
 ////////////////////////////////////////////////////////////////////////

src/proof/abs/absPth.c

@@ -194,7 +194,7 @@ int Gia_GlaProveCheck( int fVerbose )
     return 1;
 }
 
-#endif
+#endif // pthreads are used
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/proof/cec/cecSplit.c

@@ -26,7 +26,7 @@
 #include "misc/util/utilTruth.h"
 //#include "bdd/cudd/cuddInt.h"
 
-//#ifdef ABC_USE_PTHREADS
+#ifdef ABC_USE_PTHREADS
 
 #ifdef _WIN32
 #include "../lib/pthread.h"
@@ -35,7 +35,7 @@
 #include <unistd.h>
 #endif
 
-//#endif
+#endif
 
 ABC_NAMESPACE_IMPL_START
 
@@ -44,6 +44,12 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifndef ABC_USE_PTHREADS
+
+int Cec_GiaSplitTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nIterMax, int LookAhead, int fVerbose, int fVeryVerbose ) { return -1; }
+
+#else // pthreads are used
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -822,6 +828,8 @@ void Cec_GiaPrintCofStats2( Gia_Man_t * p )
     }
 }
 
+#endif // pthreads are used
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////