Towards better Boolean matching.

abclib.dsp

@@ -733,154 +733,10 @@ SOURCE=.\src\base\test\test.c
 # Begin Group "abc2"
 
 # PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2_.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Blifi.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Blifo.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Core.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Dup.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Equiv.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Extract.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Flatten.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Func.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Fx.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Gia.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Hash.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Insert.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Logic.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Map.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Mfs.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Multi.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Ntk.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Part.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Print.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Rec.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Slack.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Strash.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Time.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Truth.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Util.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Veri.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Verify.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Vero.c
-# End Source File
 # End Group
 # Begin Group "abc2d"
 
 # PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\abc2d.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\ast2.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\magic.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\magic.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\util.c
-# End Source File
 # End Group
 # End Group
 # Begin Group "bdd"
@@ -2227,6 +2083,10 @@ SOURCE=.\src\opt\dau\dauMerge.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\opt\dau\dauNonDsd.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\opt\dau\dauTree.c
 # End Source File
 # End Group

src/aig/gia/gia.h

@@ -193,6 +193,7 @@ struct Gps_Par_t_
     int            fCut;
     int            fNpn;
     int            fLutProf;
+    int            fDumpFile;
 };
 
 typedef struct Emb_Par_t_ Emb_Par_t;
@@ -1077,7 +1078,7 @@ extern void                Gia_ManHashProfile( Gia_Man_t * p );
 extern int                 Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 );
 extern int                 Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits );
 /*=== giaIf.c ===========================================================*/
-extern void                Gia_ManPrintMappingStats( Gia_Man_t * p );
+extern void                Gia_ManPrintMappingStats( Gia_Man_t * p, int fDumpFile );
 extern void                Gia_ManPrintPackingStats( Gia_Man_t * p );
 extern void                Gia_ManPrintLutStats( Gia_Man_t * p );
 extern int                 Gia_ManLutFaninCount( Gia_Man_t * p );

src/aig/gia/giaIf.c

@@ -303,7 +303,7 @@ int Gia_ManComputeOverlap( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Gia_ManPrintMappingStats( Gia_Man_t * p )
+void Gia_ManPrintMappingStats( Gia_Man_t * p, int fDumpFile )
 {
     int * pLevels;
     int i, k, iFan, nLutSize = 0, nLuts = 0, nFanins = 0, LevelMax = 0;
@@ -328,7 +328,8 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p )
     Abc_Print( 1, "over =%5.1f %%  ", 100.0 * Gia_ManComputeOverlap(p) / Gia_ManAndNum(p) );
     Abc_Print( 1, "mem =%5.2f MB", 4.0*(Gia_ManObjNum(p) + 2*nLuts + nFanins)/(1<<20) );
     Abc_Print( 1, "\n" );
-/*
+
+    if ( fDumpFile )
     {
         char * pFileName = "stats_map.txt";
         static char FileNameOld[1000] = {0};
@@ -355,7 +356,7 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p )
         }
         fclose( pTable );
     }
-*/
+
 }
 
 /**Function*************************************************************
@@ -782,6 +783,8 @@ int Gia_ManFromIfLogicCreateLutSpecial( Gia_Man_t * pNew, word * pRes, Vec_Int_t
     for ( i = 0; i < 4; i++ )
     {
         int v = (int)((z >> (16+(i<<2))) & 7);
+        if ( v == 6 && Vec_IntSize(vLeaves) == 5 )
+            continue;
         Vec_IntPush( vLeavesTemp, Vec_IntEntry(vLeaves, v) );
     }
     Truth = (z & 0xffff);
@@ -793,6 +796,8 @@ int Gia_ManFromIfLogicCreateLutSpecial( Gia_Man_t * pNew, word * pRes, Vec_Int_t
     for ( i = 0; i < 4; i++ )
     {
         int v =  (int)((z >> (48+(i<<2))) & 7);
+        if ( v == 6 && Vec_IntSize(vLeaves) == 5 )
+            continue;
         if ( v == 7 )
             Vec_IntPush( vLeavesTemp, iObjLit1 );
         else
@@ -1204,8 +1209,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
     word Truth = 0, * pTruthTable;
     int i, k, Entry;
     assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth );
-    if ( pIfMan->pPars->fEnableCheck07 )
-        pIfMan->pPars->fDeriveLuts = 0;
+//    if ( pIfMan->pPars->fEnableCheck07 )
+//        pIfMan->pPars->fDeriveLuts = 0;
     // start mapping and packing
     vMapping  = Vec_IntStart( If_ManObjNum(pIfMan) );
     vMapping2 = Vec_IntStart( 1 );

src/aig/gia/giaMan.c

@@ -366,7 +366,7 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
     if ( p->pSibls )
         Gia_ManPrintChoiceStats( p );
     if ( Gia_ManHasMapping(p) )
-        Gia_ManPrintMappingStats( p );
+        Gia_ManPrintMappingStats( p, pPars->fDumpFile );
     if ( pPars && pPars->fNpn && Gia_ManHasMapping(p) && Gia_ManLutSizeMax(p) <= 4 )
         Gia_ManPrintNpnClasses( p );
     if ( p->vPacking )

src/base/abci/abc.c

@@ -994,10 +994,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     if ( Sdm_ManCanRead() )
         Sdm_ManRead();
-    {
-//        extern void Scl_LibertyTest();
-//        Scl_LibertyTest();
-    }
 }
 
 /**Function*************************************************************
@@ -2221,16 +2217,19 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCofactor;
     int nCofLevel;
     int fProfile;
+    int fPrintDec;
 
     extern void Kit_DsdTest( unsigned * pTruth, int nVars );
     extern void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose );
+    extern void Dau_DecTrySets( word * p, int nVars );
 
     // set defaults
     nCofLevel = 1;
     fCofactor = 0;
     fProfile  = 0;
+    fPrintDec = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Npch" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Npcdh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2245,11 +2244,14 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nCofLevel < 0 )
                 goto usage;
             break;
+        case 'p':
+            fProfile ^= 1;
+            break;
         case 'c':
             fCofactor ^= 1;
             break;
-        case 'p':
-            fProfile ^= 1;
+        case 'd':
+            fPrintDec ^= 1;
             break;
         case 'h':
             goto usage;
@@ -2291,6 +2293,8 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
             Extra_TruthNot( pTruth, pTruth, Abc_ObjFaninNum(pObj) );
 //        Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
 //        Abc_Print( -1, "\n" );
+        if ( fPrintDec && Abc_ObjFaninNum(pObj) <= 6 )
+            Dau_DecTrySets( (word *)pTruth, Abc_ObjFaninNum(pObj) );
         if ( fProfile )
             Kit_TruthPrintProfile( pTruth, Abc_ObjFaninNum(pObj) );
         else if ( fCofactor )
@@ -2302,10 +2306,11 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: print_dsd [-pch] [-N <num>]\n" );
+    Abc_Print( -2, "usage: print_dsd [-pcdh] [-N <num>]\n" );
     Abc_Print( -2, "\t           print DSD formula for a single-output function with less than 16 variables\n" );
     Abc_Print( -2, "\t-p       : toggle printing profile [default = %s]\n", fProfile? "yes": "no" );
     Abc_Print( -2, "\t-c       : toggle recursive cofactoring [default = %s]\n", fCofactor? "yes": "no" );
+    Abc_Print( -2, "\t-d       : toggle printing decompositions [default = %s]\n", fPrintDec? "yes": "no" );
     Abc_Print( -2, "\t-N <num> : the number of levels to cofactor [default = %d]\n", nCofLevel );
     Abc_Print( -2, "\t-h       : print the command usage\n");
     return 1;
@@ -25318,7 +25323,7 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     memset( pPars, 0, sizeof(Gps_Par_t) );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "tpcnlh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "tpcnldh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -25337,6 +25342,9 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'l':
             pPars->fLutProf ^= 1;
             break;
+        case 'd':
+            pPars->fDumpFile ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -25352,13 +25360,14 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &ps [-tpcnlh]\n" );
+    Abc_Print( -2, "usage: &ps [-tpcnldh]\n" );
     Abc_Print( -2, "\t        prints stats of the current AIG\n" );
-    Abc_Print( -2, "\t-t    : toggle printing BMC tents [default = %s]\n", pPars->fTents? "yes": "no" );
-    Abc_Print( -2, "\t-p    : toggle printing switching activity [default = %s]\n", pPars->fSwitch? "yes": "no" );
+    Abc_Print( -2, "\t-t    : toggle printing BMC tents [default = %s]\n",                pPars->fTents? "yes": "no" );
+    Abc_Print( -2, "\t-p    : toggle printing switching activity [default = %s]\n",       pPars->fSwitch? "yes": "no" );
     Abc_Print( -2, "\t-c    : toggle printing the size of frontier cut [default = %s]\n", pPars->fCut? "yes": "no" );
     Abc_Print( -2, "\t-n    : toggle printing NPN classes of functions [default = %s]\n", pPars->fNpn? "yes": "no" );
-    Abc_Print( -2, "\t-l    : toggle printing LUT size profile [default = %s]\n", pPars->fLutProf? "yes": "no" );
+    Abc_Print( -2, "\t-l    : toggle printing LUT size profile [default = %s]\n",         pPars->fLutProf? "yes": "no" );
+    Abc_Print( -2, "\t-d    : toggle dumping statistics into a file [default = %s]\n",    pPars->fDumpFile? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -33697,7 +33706,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //    pTemp = Llb_ReachableStatesGia( pAbc->pGia );
 //    Abc_FrameUpdateGia( pAbc, pTemp );
 //    Unm_ManTest( pAbc->pGia );
-    Agi_ManTest( pAbc->pGia );
+//    Agi_ManTest( pAbc->pGia );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-F num] [-svh]\n" );

src/misc/util/utilTruth.h

@@ -1064,6 +1064,19 @@ static inline void Abc_TtSwapVars( word * pTruth, int nVars, int iVar, int jVar
         return;
     }    
 }
+// moves one var (v) to the given position (p)
+static inline void Abc_TtMoveVar( word * pF, int nVars, int * V2P, int * P2V, int v, int p )
+{
+    int iVar = V2P[v], jVar = p;
+    if ( iVar == jVar )
+        return;
+    Abc_TtSwapVars( pF, nVars, iVar, jVar );
+    V2P[P2V[iVar]] = jVar;
+    V2P[P2V[jVar]] = iVar;
+    P2V[iVar] ^= P2V[jVar];
+    P2V[jVar] ^= P2V[iVar];
+    P2V[iVar] ^= P2V[jVar];
+}
 
 /**Function*************************************************************
 

src/opt/dau/dauDsd.c

@@ -1900,7 +1900,9 @@ int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteT
 void Dau_DsdPrintFromTruth( FILE * pFile, word * pTruth, int nVarsInit )
 {
     char pRes[DAU_MAX_STR];
-    Dau_DsdDecompose( pTruth, nVarsInit, 0, 1, pRes );
+    word pTemp[DAU_MAX_WORD];
+    Abc_TtCopy( pTemp, pTruth, Abc_TtWordNum(nVarsInit), 0 );
+    Dau_DsdDecompose( pTemp, nVarsInit, 0, 1, pRes );
     fprintf( pFile, "%s\n", pRes );
 }
 

src/opt/dau/module.make

@@ -5,4 +5,5 @@ SRC +=    src/opt/dau/dauCanon.c \
     src/opt/dau/dauEnum.c \
     src/opt/dau/dauGia.c \
     src/opt/dau/dauMerge.c \
+    src/opt/dau/dauNonDsd.c \
     src/opt/dau/dauTree.c