Version abc50807

Makefile

@@ -7,9 +7,10 @@ CP   := cp
 PROG := abc
 
 MODULES := src/base/abc src/base/cmd src/base/io src/base/main \
-           src/bdd/cudd src/bdd/epd src/bdd/mtr src/bdd/parse \
+           src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse src/bdd/reo \
            src/map/fpga src/map/mapper src/map/mio src/map/super \
            src/misc/extra src/misc/st src/misc/util src/misc/vec \
+	   src/opt/fxu \
            src/sat/asat src/sat/fraig src/sat/msat \
            src/seq \
            src/sop/ft src/sop/mvc

abc.dsp

@@ -189,10 +189,18 @@ SOURCE=.\src\base\abc\abcRenode.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abc\abcRes.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abc\abcSat.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abc\abcShow.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abc\abcSop.c
 # End Source File
 # Begin Source File
@@ -209,6 +217,10 @@ SOURCE=.\src\base\abc\abcTiming.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abc\abcUnreach.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abc\abcUtil.c
 # End Source File
 # Begin Source File

abc.plg

@@ -6,13 +6,13 @@
 --------------------Configuration: abc - Win32 Debug--------------------
 </h3>
 <h3>Command Lines</h3>
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP448.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84B.tmp" with contents
 [
 /nologo /MLd /W3 /Gm /GX /ZI /Od /I "src\base\abc" /I "src\base\cmd" /I "src\base\io" /I "src\base\main" /I "src\bdd\cudd" /I "src\bdd\epd" /I "src\bdd\mtr" /I "src\bdd\parse" /I "src\bdd\dsd" /I "src\bdd\reo" /I "src\sop\mvc" /I "src\sop\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\fxa" /I "src\opt\fxu" /I "src\map\fpga" /I "src\map\mapper" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\util" /I "src\misc\vec" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Debug/" /Fp"Debug/abc.pch" /YX /Fo"Debug/" /Fd"Debug/" /FD /GZ /c 
-"C:\_projects\abc\src\opt\fxu\fxu.c"
+"C:\_projects\abc\src\base\abc\abcRes.c"
 ]
-Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP448.tmp" 
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP449.tmp" with contents
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84B.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84C.tmp" with contents
 [
 kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32.lib ole32.lib oleaut32.lib uuid.lib odbc32.lib odbccp32.lib /nologo /subsystem:console /incremental:yes /pdb:"Debug/abc.pdb" /debug /machine:I386 /out:"_TEST/abc.exe" /pdbtype:sept 
 .\Debug\abc.obj
@@ -27,6 +27,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\abcFpga.obj
 .\Debug\abcFraig.obj
 .\Debug\abcFunc.obj
+.\Debug\abcFxu.obj
 .\Debug\abcLatch.obj
 .\Debug\abcMap.obj
 .\Debug\abcMinBase.obj
@@ -36,11 +37,14 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\abcPrint.obj
 .\Debug\abcRefs.obj
 .\Debug\abcRenode.obj
+.\Debug\abcRes.obj
 .\Debug\abcSat.obj
+.\Debug\abcShow.obj
 .\Debug\abcSop.obj
 .\Debug\abcStrash.obj
 .\Debug\abcSweep.obj
 .\Debug\abcTiming.obj
+.\Debug\abcUnreach.obj
 .\Debug\abcUtil.obj
 .\Debug\abcVerify.obj
 .\Debug\cmd.obj
@@ -188,6 +192,18 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\fraigTable.obj
 .\Debug\fraigUtil.obj
 .\Debug\fraigVec.obj
+.\Debug\fxu.obj
+.\Debug\fxuCreate.obj
+.\Debug\fxuHeapD.obj
+.\Debug\fxuHeapS.obj
+.\Debug\fxuList.obj
+.\Debug\fxuMatrix.obj
+.\Debug\fxuPair.obj
+.\Debug\fxuPrint.obj
+.\Debug\fxuReduce.obj
+.\Debug\fxuSelect.obj
+.\Debug\fxuSingle.obj
+.\Debug\fxuUpdate.obj
 .\Debug\fpga.obj
 .\Debug\fpgaCore.obj
 .\Debug\fpgaCreate.obj
@@ -242,26 +258,13 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Debug\safe_mem.obj
 .\Debug\strsav.obj
 .\Debug\texpand.obj
-.\Debug\fxuUpdate.obj
-.\Debug\fxu.obj
-.\Debug\fxuCreate.obj
-.\Debug\fxuHeapD.obj
-.\Debug\fxuHeapS.obj
-.\Debug\fxuList.obj
-.\Debug\fxuMatrix.obj
-.\Debug\fxuPair.obj
-.\Debug\fxuPrint.obj
-.\Debug\fxuReduce.obj
-.\Debug\fxuSelect.obj
-.\Debug\fxuSingle.obj
-.\Debug\abcFxu.obj
 ]
-Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP449.tmp"
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84C.tmp"
 <h3>Output Window</h3>
 Compiling...
-fxu.c
+abcRes.c
 Linking...
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP44A.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84D.tmp" with contents
 [
 /nologo /o"Debug/abc.bsc" 
 .\Debug\abc.sbr
@@ -276,6 +279,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP44A.tmp" with conte
 .\Debug\abcFpga.sbr
 .\Debug\abcFraig.sbr
 .\Debug\abcFunc.sbr
+.\Debug\abcFxu.sbr
 .\Debug\abcLatch.sbr
 .\Debug\abcMap.sbr
 .\Debug\abcMinBase.sbr
@@ -285,11 +289,14 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP44A.tmp" with conte
 .\Debug\abcPrint.sbr
 .\Debug\abcRefs.sbr
 .\Debug\abcRenode.sbr
+.\Debug\abcRes.sbr
 .\Debug\abcSat.sbr
+.\Debug\abcShow.sbr
 .\Debug\abcSop.sbr
 .\Debug\abcStrash.sbr
 .\Debug\abcSweep.sbr
 .\Debug\abcTiming.sbr
+.\Debug\abcUnreach.sbr
 .\Debug\abcUtil.sbr
 .\Debug\abcVerify.sbr
 .\Debug\cmd.sbr
@@ -437,6 +444,18 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP44A.tmp" with conte
 .\Debug\fraigTable.sbr
 .\Debug\fraigUtil.sbr
 .\Debug\fraigVec.sbr
+.\Debug\fxu.sbr
+.\Debug\fxuCreate.sbr
+.\Debug\fxuHeapD.sbr
+.\Debug\fxuHeapS.sbr
+.\Debug\fxuList.sbr
+.\Debug\fxuMatrix.sbr
+.\Debug\fxuPair.sbr
+.\Debug\fxuPrint.sbr
+.\Debug\fxuReduce.sbr
+.\Debug\fxuSelect.sbr
+.\Debug\fxuSingle.sbr
+.\Debug\fxuUpdate.sbr
 .\Debug\fpga.sbr
 .\Debug\fpgaCore.sbr
 .\Debug\fpgaCreate.sbr
@@ -490,21 +509,8 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP44A.tmp" with conte
 .\Debug\pathsearch.sbr
 .\Debug\safe_mem.sbr
 .\Debug\strsav.sbr
-.\Debug\texpand.sbr
-.\Debug\fxuUpdate.sbr
-.\Debug\fxu.sbr
-.\Debug\fxuCreate.sbr
-.\Debug\fxuHeapD.sbr
-.\Debug\fxuHeapS.sbr
-.\Debug\fxuList.sbr
-.\Debug\fxuMatrix.sbr
-.\Debug\fxuPair.sbr
-.\Debug\fxuPrint.sbr
-.\Debug\fxuReduce.sbr
-.\Debug\fxuSelect.sbr
-.\Debug\fxuSingle.sbr
-.\Debug\abcFxu.sbr]
-Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP44A.tmp"
+.\Debug\texpand.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP84D.tmp"
 Creating browse info file...
 <h3>Output Window</h3>
 

abc.rc

 alias b balance
 alias clp collapse
+alias esd ext_seq_dcs
 alias f fraig
 alias fs fraig_sweep
 alias pf print_factor

src/base/abc/abc.c

@@ -28,41 +28,45 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int Ntk_CommandPrintStats   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandPrintIo      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandPrintFanio   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandPrintFactor  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Ntk_CommandCollapse     ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandStrash       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandBalance      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandRenode       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandCleanup      ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFx           ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Ntk_CommandLogic        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandMiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFrames       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandSop          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandBdd          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandSat          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Ntk_CommandFraig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFraigTrust   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFraigStore   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFraigClean   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandFraigSweep   ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Ntk_CommandMap          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandUnmap        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandAttach       ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandSuperChoice  ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Ntk_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv );
-
-static int Ntk_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Ntk_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintStats   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintIo      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintFanio   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintFactor  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandShowBdd      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandCollapse     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandStrash       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBalance      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRenode       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCleanup      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFastExtract  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDisjoint     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandRes          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandLogic        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMiter        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFrames       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSop          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBdd          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSat          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExtSeqDcs    ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandFraig        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigTrust   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigStore   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigRestore ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigClean   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandFraigSweep   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandMap          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandUnmap        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAttach       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSuperChoice  ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandFpga         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+
+static int Abc_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -81,41 +85,46 @@ static int Ntk_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv
 ***********************************************************************/
 void Abc_Init( Abc_Frame_t * pAbc )
 {
-    Cmd_CommandAdd( pAbc, "Printing",     "print_stats",   Ntk_CommandPrintStats,       0 ); 
-    Cmd_CommandAdd( pAbc, "Printing",     "print_io",      Ntk_CommandPrintIo,          0 );
-    Cmd_CommandAdd( pAbc, "Printing",     "print_fanio",   Ntk_CommandPrintFanio,       0 );
-    Cmd_CommandAdd( pAbc, "Printing",     "print_factor",  Ntk_CommandPrintFactor,      0 );
-
-    Cmd_CommandAdd( pAbc, "Synthesis",    "collapse",      Ntk_CommandCollapse,         1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "strash",        Ntk_CommandStrash,           1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "balance",       Ntk_CommandBalance,          1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "renode",        Ntk_CommandRenode,           1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Ntk_CommandCleanup,          1 );
-    Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Ntk_CommandFx,               1 );
-
-    Cmd_CommandAdd( pAbc, "Various",      "logic",         Ntk_CommandLogic,            1 );
-    Cmd_CommandAdd( pAbc, "Various",      "miter",         Ntk_CommandMiter,            1 );
-    Cmd_CommandAdd( pAbc, "Various",      "frames",        Ntk_CommandFrames,           1 );
-    Cmd_CommandAdd( pAbc, "Various",      "sop",           Ntk_CommandSop,              0 );
-    Cmd_CommandAdd( pAbc, "Various",      "bdd",           Ntk_CommandBdd,              0 );
-    Cmd_CommandAdd( pAbc, "Various",      "sat",           Ntk_CommandSat,              0 );
-
-    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Ntk_CommandFraig,            1 );
-    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_trust",   Ntk_CommandFraigTrust,       1 );
-    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_store",   Ntk_CommandFraigStore,       0 );
-    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_restore", Ntk_CommandFraigRestore,     1 );
-    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_clean",   Ntk_CommandFraigClean,       0 );
-    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_sweep",   Ntk_CommandFraigSweep,       1 );
-
-    Cmd_CommandAdd( pAbc, "SC mapping",   "map",           Ntk_CommandMap,              1 );
-    Cmd_CommandAdd( pAbc, "SC mapping",   "unmap",         Ntk_CommandUnmap,            1 );
-    Cmd_CommandAdd( pAbc, "SC mapping",   "attach",        Ntk_CommandAttach,           1 );
-    Cmd_CommandAdd( pAbc, "SC mapping",   "sc",            Ntk_CommandSuperChoice,      1 );
-
-    Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Ntk_CommandFpga,             1 );
-
-    Cmd_CommandAdd( pAbc, "Verification", "cec",           Ntk_CommandCec,              0 );
-    Cmd_CommandAdd( pAbc, "Verification", "sec",           Ntk_CommandSec,              0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_stats",   Abc_CommandPrintStats,       0 ); 
+    Cmd_CommandAdd( pAbc, "Printing",     "print_io",      Abc_CommandPrintIo,          0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_fanio",   Abc_CommandPrintFanio,       0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_factor",  Abc_CommandPrintFactor,      0 );
+
+    Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
+
+    Cmd_CommandAdd( pAbc, "Synthesis",    "collapse",      Abc_CommandCollapse,         1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "strash",        Abc_CommandStrash,           1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "balance",       Abc_CommandBalance,          1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "renode",        Abc_CommandRenode,           1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Abc_CommandCleanup,          1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "fx",            Abc_CommandFastExtract,      1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "dsd",           Abc_CommandDisjoint,         1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "res",           Abc_CommandRes,              1 );
+
+    Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "miter",         Abc_CommandMiter,            1 );
+    Cmd_CommandAdd( pAbc, "Various",      "frames",        Abc_CommandFrames,           1 );
+    Cmd_CommandAdd( pAbc, "Various",      "sop",           Abc_CommandSop,              0 );
+    Cmd_CommandAdd( pAbc, "Various",      "bdd",           Abc_CommandBdd,              0 );
+    Cmd_CommandAdd( pAbc, "Various",      "sat",           Abc_CommandSat,              0 );
+    Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
+
+    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
+    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_trust",   Abc_CommandFraigTrust,       1 );
+    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_store",   Abc_CommandFraigStore,       0 );
+    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_restore", Abc_CommandFraigRestore,     1 );
+    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_clean",   Abc_CommandFraigClean,       0 );
+    Cmd_CommandAdd( pAbc, "Fraiging",     "fraig_sweep",   Abc_CommandFraigSweep,       1 );
+
+    Cmd_CommandAdd( pAbc, "SC mapping",   "map",           Abc_CommandMap,              1 );
+    Cmd_CommandAdd( pAbc, "SC mapping",   "unmap",         Abc_CommandUnmap,            1 );
+    Cmd_CommandAdd( pAbc, "SC mapping",   "attach",        Abc_CommandAttach,           1 );
+    Cmd_CommandAdd( pAbc, "SC mapping",   "sc",            Abc_CommandSuperChoice,      1 );
+
+    Cmd_CommandAdd( pAbc, "FPGA mapping", "fpga",          Abc_CommandFpga,             1 );
+
+    Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
+    Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
 
     Ft_FactorStartMan();
 }
@@ -148,7 +157,7 @@ void Abc_End()
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -202,7 +211,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -271,7 +280,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -322,7 +331,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -391,6 +400,81 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pNode;
+    int c;
+    extern void Abc_NodePrintBdd( Abc_Obj_t * pNode );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsLogicBdd(pNtk) )
+    {
+        fprintf( pErr, "Printing BDDs can only be done for logic BDD networks.\n" );
+        return 1;
+    }
+
+    if ( argc != util_optind + 1 )
+    {
+        fprintf( pErr, "Wrong number of auguments.\n" );
+        goto usage;
+    }
+
+    pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+    if ( pNode == NULL )
+    {
+        fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+        return 1;
+    }
+    Abc_NodePrintBdd( pNode );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: show_bdd [-h] <node>\n" );
+    fprintf( pErr, "       visualizes the BDD of a node using DOT and GSVIEW\n" );
+#ifdef WIN32
+    fprintf( pErr, "       \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
+    fprintf( pErr, "       (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
+#endif
+    fprintf( pErr, "\tnode  : the node to consider\n");
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
 
 /**Function*************************************************************
 
@@ -403,7 +487,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -443,7 +527,7 @@ int Ntk_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtkRes = Abc_NtkCollapse( pNtk, 1 );
     else
     {
-        pNtk = Abc_NtkStrash( pNtk );
+        pNtk = Abc_NtkStrash( pNtk, 0 );
         pNtkRes = Abc_NtkCollapse( pNtk, 1 );
         Abc_NtkDelete( pNtk );
     }
@@ -475,22 +559,27 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
+    int fAllNodes;
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fAllNodes = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "ah" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'a':
+            fAllNodes ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -505,7 +594,7 @@ int Ntk_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkStrash( pNtk );
+    pNtkRes = Abc_NtkStrash( pNtk, fAllNodes );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Strashing has failed.\n" );
@@ -516,8 +605,9 @@ int Ntk_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: strash [-h]\n" );
+    fprintf( pErr, "usage: strash [-ah]\n" );
     fprintf( pErr, "\t        transforms combinational logic into an AIG\n" );
+    fprintf( pErr, "\t-a    : toggles between using all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "DFS" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -533,7 +623,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -602,7 +692,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -709,7 +799,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -767,7 +857,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFx( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk;
     FILE * pOut, * pErr;
@@ -875,6 +965,129 @@ usage:
     return 1;       
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes, * pNtkNew;
+    int fGlobal, fRecursive, fVerbose, fPrint, fShort, c;
+
+    extern Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
+    extern int         Abc_NtkDsdRecursive( Abc_Ntk_t * pNtk, bool fVerbose );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fGlobal    = 1;
+    fRecursive = 0;
+    fVerbose   = 0;
+    fPrint     = 0;
+    fShort     = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "grvpsh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'g':
+                fGlobal ^= 1;
+                break;
+            case 'r':
+                fRecursive ^= 1;
+                break;
+            case 'v':
+                fVerbose ^= 1;
+                break;
+            case 'p':
+                fPrint ^= 1;
+                break;
+            case 's':
+                fShort ^= 1;
+                break;
+            case 'h':
+                goto usage;
+                break;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !fGlobal && !fRecursive )
+    {
+        fprintf( pErr, "Decomposition should be either global or recursive.\n" );
+        return 1;
+    }
+
+    if ( fGlobal )
+    {
+        // get the new network
+        if ( !Abc_NtkIsAig(pNtk) )
+        {
+            pNtkNew = Abc_NtkStrash( pNtk, 0 );
+            pNtkRes = Abc_NtkDsdGlobal( pNtkNew, fVerbose, fPrint, fShort );
+            Abc_NtkDelete( pNtkNew );
+        }
+        else
+        {
+            pNtkRes = Abc_NtkDsdGlobal( pNtk, fVerbose, fPrint, fShort );
+        }
+        if ( pNtkRes == NULL )
+        {
+            fprintf( pErr, "Global disjoint support decomposition has failed.\n" );
+            return 1;
+        }
+        if ( fRecursive )
+        {
+            if ( !Abc_NtkDsdRecursive( pNtkRes, fVerbose ) )
+            {
+                fprintf( pErr, "Recursive decomposition has failed.\n" );
+                Abc_NtkDelete( pNtkRes );
+                return 1;
+            }
+        }
+        // replace the current network
+        Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    }
+    else if ( fRecursive )
+    {
+        if ( !Abc_NtkIsLogicBdd( pNtk ) )
+        {
+            fprintf( pErr, "This command is only applicable to logic BDD networks.\n" );
+            return 1;
+        }
+        if ( !Abc_NtkDsdRecursive( pNtk, fVerbose ) )
+            fprintf( pErr, "Recursive decomposition has failed.\n" );
+    }
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dsd [-grvpsh]\n" );
+    fprintf( pErr, "\t     decomposes the network using disjoint-support decomposition\n" );
+    fprintf( pErr, "\t-g     : collapses the network and decomposes shared BDDs [default = %s]\n", fGlobal? "yes": "no" );  
+    fprintf( pErr, "\t-r     : applied DSD and MUX-decomposition recursively [default = %s]\n", fRecursive? "yes": "no" );  
+    fprintf( pErr, "\t-v     : prints DSD statistics and runtime [default = %s]\n", fVerbose? "yes": "no" ); 
+    fprintf( pErr, "\t-p     : prints DSD structure to the standard output [default = %s]\n", fPrint? "yes": "no" ); 
+    fprintf( pErr, "\t-s     : use short PI names when printing DSD structure [default = %s]\n", fShort? "yes": "no" ); 
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
 
 /**Function*************************************************************
 
@@ -887,7 +1100,106 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandRes( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    Abc_ManRes_t * p;
+    extern int Abc_NtkAigResynthesize( Abc_Ntk_t * pNtk, Abc_ManRes_t * p );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    p = Abc_NtkManResStart();
+    p->fVerbose     =  0;
+    p->nNodeSizeMax = 10;
+    p->nConeSizeMax = 10;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "ncvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'n':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-n\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            p->nNodeSizeMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( p->nNodeSizeMax < 0 ) 
+                goto usage;
+            break;
+        case 'c':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-c\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            p->nConeSizeMax = atoi(argv[util_optind]);
+            util_optind++;
+            if ( p->nConeSizeMax < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            p->fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        Abc_NtkManResStop( p );
+        return 1;
+    }
+    if ( !Abc_NtkIsAig(pNtk) )
+    {
+        fprintf( pErr, "This command can only be applied to an AIG.\n" );
+        Abc_NtkManResStop( p );
+        return 1;
+    }
+    if ( Abc_NtkCountChoiceNodes(pNtk) )
+    {
+        fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" );
+        Abc_NtkManResStop( p );
+        return 1;
+    }
+
+    // modify the current network
+    Abc_NtkAigResynthesize( pNtk, p );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: res [-n num] [-c num] [-vh]\n" );
+    fprintf( pErr, "\t         performs technology-independent resynthesis of the AIG\n" );
+    fprintf( pErr, "\t-n num : the max support of the collapsed node [default = %d]\n", p->nNodeSizeMax );  
+    fprintf( pErr, "\t-c num : the max support of the containing cone [default = %d]\n", p->nConeSizeMax );  
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", p->fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -951,7 +1263,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtk1, * pNtk2, * pNtkRes;
@@ -1025,7 +1337,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkTemp, * pNtkRes;
@@ -1075,7 +1387,7 @@ int Ntk_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv )
     // get the new network
     if ( !Abc_NtkIsAig(pNtk) )
     {
-        pNtkTemp = Abc_NtkStrash( pNtk );
+        pNtkTemp = Abc_NtkStrash( pNtk, 0 );
         pNtkRes  = Abc_NtkFrames( pNtkTemp, nFrames, fInitial );
         Abc_NtkDelete( pNtkTemp );
     }
@@ -1111,7 +1423,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1171,7 +1483,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1231,7 +1543,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1295,6 +1607,76 @@ usage:
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fVerbose;
+    extern int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNet, bool fVerbose );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        fprintf( stdout, "The current network has no latches.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkIsAig(pNtk) )
+    {
+        fprintf( stdout, "This command works only for AIGs.\n" );
+        return 0;
+    }
+    if ( !Abc_NtkExtractSequentialDcs( pNtk, fVerbose ) )
+    {
+        fprintf( stdout, "Extracting sequential don't-cares has failed.\n" );
+        return 1;
+    }
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: ext_seq_dcs [-vh]\n" );
+    fprintf( pErr, "\t         create EXDC network using unreachable states\n" );
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 
 
@@ -1309,7 +1691,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     char Buffer[100];
     Fraig_Params_t Params;
@@ -1419,7 +1801,7 @@ int Ntk_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
     else
     {
-        pNtk = Abc_NtkStrash( pNtk );
+        pNtk = Abc_NtkStrash( pNtk, 0 );
         pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
         Abc_NtkDelete( pNtk );
     }
@@ -1464,7 +1846,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFraigTrust( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFraigTrust( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -1528,7 +1910,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFraigStore( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFraigStore( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1589,7 +1971,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFraigRestore( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFraigRestore( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -1653,7 +2035,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFraigClean( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFraigClean( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1702,7 +2084,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1779,7 +2161,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -1840,7 +2222,7 @@ int Ntk_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsAig(pNtk) )
     {
-        pNtk = Abc_NtkStrash( pNtk );
+        pNtk = Abc_NtkStrash( pNtk, 0 );
         if ( pNtk == NULL )
         {
             fprintf( pErr, "Strashing before mapping has failed.\n" );
@@ -1909,7 +2291,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -1970,7 +2352,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -2033,7 +2415,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -2098,7 +2480,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
@@ -2141,7 +2523,7 @@ int Ntk_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( !Abc_NtkIsAig(pNtk) )
     {
         // strash and balance the network
-        pNtk = Abc_NtkStrash( pNtk );
+        pNtk = Abc_NtkStrash( pNtk, 0 );
         if ( pNtk == NULL )
         {
             fprintf( pErr, "Strashing before FPGA mapping has failed.\n" );
@@ -2202,7 +2584,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;
@@ -2273,7 +2655,7 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Ntk_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtk1, * pNtk2;

src/base/abc/abc.h

@@ -21,25 +21,6 @@
 #ifndef __ABC_H__
 #define __ABC_H__
 
-/*
-    In the netlist, the PI/PO arrays store PI/PO nets.
-    The names belongs to the nets and are stored in pNet->pData.
-    When a netlist is made combinational:
-    - LO/LI nets are added to PI/PO arrays,
-    - the array of latches is temporarily stored in vLatch2,
-    - the original number of PIs/POs is remembered in nPisOld/nPosOld.
-
-    In a logic network, the PI/PO arrays store PI/PO nodes.
-    The PO nodes have only one fanin edge, which can be complemented.
-    The arrays vNamesPi/vNamesPo/vNamesLatch store PI/PO/latch names.
-    The internal nodes are nameless.
-    When a logic network is made combinational:
-    - laches are added to the PI/PO arrays,
-    - the arrays of names are not changed,
-    - the array of latches is temporarily stored in vLatch2,
-    - the original number of PIs/POs is remembered in nPisOld/nPosOld.
-*/
-
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -103,6 +84,7 @@ typedef struct Abc_Obj_t_     Abc_Obj_t;
 typedef struct Abc_Ntk_t_     Abc_Ntk_t;
 typedef struct Abc_Aig_t_     Abc_Aig_t;
 typedef struct Abc_ManTime_t_ Abc_ManTime_t;
+typedef struct Abc_ManRes_t_  Abc_ManRes_t;
 typedef struct Abc_Time_t_    Abc_Time_t;
 
 struct Abc_Time_t_
@@ -182,6 +164,30 @@ struct Abc_Ntk_t_
     Extra_MmStep_t * pMmStep;       // memory manager for arrays
 };
 
+struct Abc_ManRes_t_
+{
+    // user specified parameters
+    int              nNodeSizeMax;  // the limit on the size of the supernode
+    int              nConeSizeMax;  // the limit on the size of the containing cone
+    int              fVerbose;      // the verbosity flag
+    // internal parameters
+    DdManager *      dd;            // the BDD manager
+    DdNode *         bCubeX;        // the cube of PI variables
+    Abc_Obj_t *      pNode;         // the node currently considered
+    Vec_Ptr_t *      vFaninsNode;   // fanins of the supernode
+    Vec_Ptr_t *      vInsideNode;   // inside of the supernode
+    Vec_Ptr_t *      vFaninsCone;   // fanins of the containing cone
+    Vec_Ptr_t *      vInsideCone;   // inside of the containing cone
+    Vec_Ptr_t *      vVisited;      // the visited nodes
+    Vec_Str_t *      vCube;         // temporary cube for generating covers
+    Vec_Int_t *      vForm;         // the factored form (temporary)
+    // runtime statistics
+    int              time1;
+    int              time2;
+    int              time3;
+    int              time4;
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
@@ -380,11 +386,12 @@ extern bool               Abc_NtkCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 /*=== abcCollapse.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose );
+extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly );
+extern void               Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk );
 /*=== abcCreate.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type );
 extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type );
 extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-extern void               Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj );
@@ -407,6 +414,7 @@ extern Abc_Obj_t *        Abc_NodeCreateBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFani
 extern Abc_Obj_t *        Abc_NodeCreateAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
 extern Abc_Obj_t *        Abc_NodeCreateOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins );
 extern Abc_Obj_t *        Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 );
+extern Abc_Obj_t *        Abc_NodeClone( Abc_Obj_t * pNode );
 /*=== abcDfs.c ==========================================================*/
 extern Vec_Ptr_t *        Abc_NtkDfs( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_AigDfs( Abc_Ntk_t * pNtk );
@@ -415,6 +423,7 @@ extern bool               Abc_NtkIsAcyclic( Abc_Ntk_t * pNtk );
 /*=== abcFanio.c ==========================================================*/
 extern void               Abc_ObjAddFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
 extern void               Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin );
+extern void               Abc_ObjRemoveFanins( Abc_Obj_t * pObj );
 extern void               Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew );
 extern void               Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
 extern void               Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
@@ -426,7 +435,7 @@ extern Abc_Ntk_t *        Abc_NtkFraigRestore();
 extern void               Abc_NtkFraigStoreClean();
 /*=== abcFunc.c ==========================================================*/
 extern int                Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
-extern char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFunc, int nFanins, Vec_Str_t * vCube, int fMode );
+extern char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode );
 extern int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk );
 extern void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 );
 extern int                Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
@@ -475,6 +484,9 @@ extern int                Abc_NodeMffcRemove( Abc_Obj_t * pNode );
 /*=== abcRenode.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple );
 extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
+/*=== abcRes.c ==========================================================*/
+extern Abc_ManRes_t *     Abc_NtkManResStart();
+extern void               Abc_NtkManResStop( Abc_ManRes_t * p );
 /*=== abcSat.c ==========================================================*/
 extern bool               Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose );
 extern solver *           Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk );
@@ -497,7 +509,7 @@ extern bool               Abc_SopCheck( char * pSop, int nFanins );
 extern void               Abc_SopWriteCnf( FILE * pFile, char * pClauses, Vec_Int_t * vVars );
 extern void               Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, Vec_Int_t * vTemp );
 /*=== abcStrash.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
 extern Abc_Ntk_t *        Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate );
 /*=== abcSweep.c ==========================================================*/
@@ -512,7 +524,7 @@ extern void               Abc_NtkTimeSetDefaultArrival( Abc_Ntk_t * pNtk, float
 extern void               Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall );
 extern void               Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall );
 extern void               Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall );
-extern void               Abc_NtkTimeFinalize( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk );
 extern void               Abc_ManTimeStop( Abc_ManTime_t * p );
 extern void               Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew );
 extern void               Abc_NtkSetNodeLevelsArrival( Abc_Ntk_t * pNtk );
@@ -549,6 +561,9 @@ extern void               Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t *
 extern int                Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
 extern int                Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 );
 extern Vec_Ptr_t *        Abc_AigCollectAll( Abc_Ntk_t * pNtk );
+extern Vec_Ptr_t *        Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
+extern void               Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames );
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/abc/abcCheck.c

@@ -108,11 +108,11 @@ bool Abc_NtkCheck( Abc_Ntk_t * pNtk )
     // check the EXDC network if present
     if ( pNtk->pExdc )
     {
-        if ( pNtk->Type != pNtk->pExdc->Type )
-        {
-            fprintf( stdout, "NetworkCheck: Network and its EXDC have different types.\n" );
-            return 0;
-        }
+//        if ( pNtk->Type != pNtk->pExdc->Type )
+//        {
+//            fprintf( stdout, "NetworkCheck: Network and its EXDC have different types.\n" );
+//            return 0;
+//        }
         return Abc_NtkCheck( pNtk->pExdc );
     }
     return 1;

src/base/abc/abcCollapse.c

@@ -24,7 +24,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk );
 static DdNode *    Abc_NtkGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode );
 static Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk );
 static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc );
@@ -52,33 +51,16 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
 
     assert( Abc_NtkIsAig(pNtk) );
 
-    // perform FPGA mapping
-    dd = Abc_NtkGlobalBdds( pNtk );    
+    // compute the global BDDs
+    dd = Abc_NtkGlobalBdds( pNtk, 0 );    
     if ( dd == NULL )
         return NULL;
     if ( fVerbose )
         printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
-/*
-    {
-        Abc_Obj_t * pNode;
-        int i;
-        Abc_NtkForEachPo( pNtk, pNode, i )
-        {
-            Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
-            pNode->pNext = NULL;
-        }
-        Abc_NtkForEachLatch( pNtk, pNode, i )
-        {
-            Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
-            pNode->pNext = NULL;
-        }
-    }
-    Extra_StopManager( dd );
-    return NULL;
-*/
 
-    // transform the result of mapping into a BDD network
+    // create the new network
     pNtkNew = Abc_NtkFromGlobalBdds( dd, pNtk );
+    Abc_NtkFreeGlobalBdds( dd, pNtk );
     if ( pNtkNew == NULL )
     {
         Cudd_Quit( dd );
@@ -110,8 +92,9 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk )
+DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
 {
+    int fReorder = 1;
     ProgressBar * pProgress;
     Abc_Obj_t * pNode;
     DdNode * bFunc;
@@ -120,7 +103,8 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk )
 
     // start the manager
     dd = Cudd_Init( Abc_NtkCiNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    if ( fReorder )
+        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
 
     // set the elementary variables
     Abc_NtkCleanCopy( pNtk );
@@ -130,31 +114,60 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk )
     pNode = Abc_AigConst1( pNtk->pManFunc );
     pNode->pCopy = (Abc_Obj_t *)dd->one;   Cudd_Ref( dd->one );
 
-    // construct the BDDs
-    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
-    Abc_NtkForEachCo( pNtk, pNode, i )
+    if ( fLatchOnly )
     {
-        Extra_ProgressBarUpdate( pProgress, i, NULL );
-        bFunc = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) );
-        if ( bFunc == NULL )
+        // construct the BDDs
+        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkLatchNum(pNtk) );
+        Abc_NtkForEachLatch( pNtk, pNode, i )
         {
-            printf( "Constructing global BDDs timed out.\n" );
-            Extra_ProgressBarStop( pProgress );
-            Cudd_Quit( dd );
-            return NULL;
+            Extra_ProgressBarUpdate( pProgress, i, NULL );
+            bFunc = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) );
+            if ( bFunc == NULL )
+            {
+                printf( "Constructing global BDDs timed out.\n" );
+                Extra_ProgressBarStop( pProgress );
+                Cudd_Quit( dd );
+                return NULL;
+            }
+            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
+            pNode->pNext = (Abc_Obj_t *)bFunc;   Cudd_Ref( bFunc );
         }
-        bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
-        pNode->pNext = (Abc_Obj_t *)bFunc;   Cudd_Ref( bFunc );
+        Extra_ProgressBarStop( pProgress );
+    }
+    else
+    {
+        // construct the BDDs
+        pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+        Abc_NtkForEachCo( pNtk, pNode, i )
+        {
+            Extra_ProgressBarUpdate( pProgress, i, NULL );
+            bFunc = Abc_NtkGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) );
+            if ( bFunc == NULL )
+            {
+                printf( "Constructing global BDDs timed out.\n" );
+                Extra_ProgressBarStop( pProgress );
+                Cudd_Quit( dd );
+                return NULL;
+            }
+            bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) );
+            pNode->pNext = (Abc_Obj_t *)bFunc;   Cudd_Ref( bFunc );
+        }
+        Extra_ProgressBarStop( pProgress );
     }
-    Extra_ProgressBarStop( pProgress );
 
     // derefence the intermediate BDDs
     Abc_NtkForEachNode( pNtk, pNode, i )
         if ( pNode->pCopy ) 
+        {
             Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
-    Abc_NtkCleanCopy( pNtk );
+            pNode->pCopy = NULL;
+        }
     // reorder one more time
-    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 0 );
+    if ( fReorder )
+    {
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
+        Cudd_AutodynDisable( dd );
+    }
     return dd;
 }
 
@@ -227,9 +240,6 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
         Extra_ProgressBarUpdate( pProgress, i, NULL );
         pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, (DdNode *)pNode->pNext );
         Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
-        // deref the BDD of the PO
-        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
-        pNode->pNext = NULL;
     }
     Extra_ProgressBarStop( pProgress );
     // transfer the names
@@ -263,6 +273,30 @@ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode
     return pNodeNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Dereferences global functions of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFreeGlobalBdds( DdManager * dd, Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        if ( pNode->pNext == NULL )
+            continue;
+        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pNext );
+        pNode->pNext = NULL;
+    }
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/abc/abcCreate.c

@@ -157,34 +157,6 @@ void Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 
 /**Function*************************************************************
 
-  Synopsis    [Finalizes the network using the existing network as a model.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
-{
-    Abc_Obj_t * pObj, * pDriver, * pDriverNew;
-    int i;
-    assert( !Abc_NtkIsNetlist(pNtk) );
-    // set the COs of the strashed network
-    Abc_NtkForEachCo( pNtk, pObj, i )
-    {
-        pDriver    = Abc_ObjFanin0(pObj);
-        pDriverNew = pDriver->pCopy;
-        Abc_ObjAddFanin( pObj->pCopy, pDriverNew );
-    }
-    // transfer the names
-    Abc_NtkDupNameArrays( pNtk, pNtkNew );
-    Abc_ManTimeDup( pNtk, pNtkNew );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Duplicate the Ntk.]
 
   Description []
@@ -635,7 +607,58 @@ void Abc_NtkRemovePoNode( Abc_Obj_t * pNode )
 ***********************************************************************/
 Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName )
 {
-    return NULL;
+    Abc_Obj_t * pNode, * pDriver;
+    int i, Num;
+    // check if the node is among CIs
+    Abc_NtkForEachCi( pNtk, pNode, i )
+    {
+        if ( strcmp( Abc_NtkNameCi(pNtk,i), pName ) == 0 )
+        {
+            if ( i < Abc_NtkPiNum(pNtk) )
+                printf( "Node \"%s\" is a primary input.\n", pName );
+            else
+                printf( "Node \"%s\" is a latch output.\n", pName );
+            return NULL;
+        }
+    }
+    // search the node among COs
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        if ( strcmp( Abc_NtkNameCo(pNtk,i), pName ) == 0 )
+        {
+            pDriver = Abc_ObjFanin0(pNode);
+            if ( !Abc_ObjIsNode(pDriver) )
+            {
+                printf( "Node \"%s\" does not have logic associated with it.\n", pName );
+                return NULL;
+            }
+            return pDriver;
+        }
+    }
+    // find the internal node
+    if ( pName[0] != '[' || pName[strlen(pName)-1] != ']' )
+    {
+        printf( "Node \"%s\" has non-standard name (expected name is \"[integer]\").\n", pName );
+        return NULL;
+    }
+    Num = atoi( pName + 1 );
+    if ( Num < 0 || Num > Abc_NtkObjNum(pNtk) )
+    {
+        printf( "The node \"%s\" with ID %d is not in the current network.\n", pName, Num );
+        return NULL;
+    }
+    pNode = Abc_NtkObj( pNtk, Num );
+    if ( pNode == NULL )
+    {
+        printf( "The node \"%s\" with ID %d has been removed from the current network.\n", pName, Num );
+        return NULL;
+    }
+    if ( !Abc_ObjIsNode(pNode) )
+    {
+        printf( "Object with ID %d is not a node.\n", Num );
+        return NULL;
+    }
+    return pNode;
 }
 
 /**Function*************************************************************
@@ -997,6 +1020,27 @@ Abc_Obj_t * Abc_NodeCreateMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t *
     return pNode;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Clones the given node but does not assign the function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NodeClone( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pClone, * pFanin;
+    int i;
+    assert( Abc_ObjIsNode(pNode) );
+    pClone = Abc_NtkCreateNode( pNode->pNtk );   
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Abc_ObjAddFanin( pClone, pFanin );
+    return pClone;
+}
 
 
 

src/base/abc/abcDsd.c

@@ -19,18 +19,443 @@
 ***********************************************************************/
 
 #include "abc.h"
+#include "dsd.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
+static Abc_Ntk_t *     Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort );
+static Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose );
+static void            Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t *     Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew );
+
+static Vec_Ptr_t *     Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk );
+static void            Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd );
+static bool            Abc_NodeIsForDsd( Abc_Obj_t * pNode );
+static int             Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Decomposes the network using disjoint-support decomposition.]
+  Synopsis    [Derives the DSD network.]
+
+  Description [Takes the strashed network (pNtk), derives global BDDs for
+  the combinational outputs of this network, and decomposes these BDDs using
+  disjoint support decomposition. Finally, constructs and return a new 
+  network, which is topologically equivalent to the decomposition tree.
+  Allocates and frees a new BDD manager and a new DSD manager.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
+{
+    int fCheck = 1;
+    Abc_Ntk_t * pNtkNew;
+    DdManager * dd;
+
+    assert( Abc_NtkIsAig(pNtk) );
+
+    // perform FPGA mapping
+    dd = Abc_NtkGlobalBdds( pNtk, 0 );    
+    if ( dd == NULL )
+        return NULL;
+    if ( fVerbose )
+        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+    // transform the result of mapping into a BDD network
+    pNtkNew = Abc_NtkDsdInternal( dd, pNtk, fVerbose, fPrint, fShort );
+    if ( pNtkNew == NULL )
+    {
+        Cudd_Quit( dd );
+        return NULL;
+    }
+    Extra_StopManager( dd );
+
+    // make sure that everything is okay
+    if ( fCheck && !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkDsdGlobal: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDsdInternal( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool fShort )
+{
+    Dsd_Manager_t * pManDsd;
+    Abc_Ntk_t * pNtkNew;
+
+    // perform the decomposition
+    pManDsd = Abc_NtkDsdPerform( dd, pNtk, fVerbose );
+    Abc_NtkFreeGlobalBdds( dd, pNtk );
+    if ( pManDsd == NULL )
+        return NULL;
+
+    // start the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC_BDD );
+    // make sure the new manager has enough inputs
+    Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 );
+    // put the results into the new network (save new CO drivers in old CO drivers)
+    Abc_NtkDsdConstruct( pManDsd, pNtk, pNtkNew );
+    // finalize the new network
+    Abc_NtkFinalize( pNtk, pNtkNew );
+
+    if ( fPrint )
+    Dsd_TreePrint( stdout, pManDsd, (char **)pNtk->vNamesPi->pArray, (char **)pNtk->vNamesPo->pArray, fShort, -1 );
+
+    // stop the DSD manager
+    Dsd_ManagerStop( pManDsd );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DSD by creating the manager and decomposing the functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dsd_Manager_t * Abc_NtkDsdPerform( DdManager * dd, Abc_Ntk_t * pNtk, bool fVerbose )
+{
+    Dsd_Manager_t * pManDsd;
+    DdNode ** pbFuncsGlo;
+    Abc_Obj_t * pNode;
+    int i;
+
+    // collect global functions into the array
+    pbFuncsGlo = ALLOC( DdNode *, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pbFuncsGlo[i] = Cudd_NotCond( pNode->pNext, Abc_ObjFaninC0(pNode) );
+//printf( "Output %3d : Support size = %3d. Nodes = %5d.\n", i, Cudd_SupportSize(dd, pbFuncsGlo[i]), Cudd_DagSize(pbFuncsGlo[i]) );
+    }
+
+    // start the DSD manager and decompose global functions
+    pManDsd = Dsd_ManagerStart( dd, Abc_NtkCiNum(pNtk), fVerbose );
+    Dsd_Decompose( pManDsd, pbFuncsGlo, Abc_NtkCoNum(pNtk) );
+    FREE( pbFuncsGlo );
+    return pManDsd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs the decomposed network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDsdConstruct( Dsd_Manager_t * pManDsd, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+{
+    Dsd_Node_t ** ppNodesDsd;
+    Dsd_Node_t * pNodeDsd;
+    Abc_Obj_t * pNode, * pNodeNew, * pDriver, * pConst1;
+    int i, nNodesDsd;
+
+    // save the CI nodes in the DSD nodes
+    Abc_NtkForEachCi( pNtk, pNode, i )
+    {
+        pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
+        Dsd_NodeSetMark( pNodeDsd, (int)pNode->pCopy );
+    }
+    // set the constant node
+    pConst1 = Abc_AigConst1(pNtk->pManFunc);
+    if ( Abc_ObjFanoutNum(pConst1) > 0 )
+        pConst1->pCopy = Abc_NodeCreateConst1(pNtkNew);
+
+    // collect DSD nodes in DFS order (leaves and const1 are not collected)
+    ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd );
+    for ( i = 0; i < nNodesDsd; i++ )
+        Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNtkNew );
+    free( ppNodesDsd );
+
+    // set the pointers to the CO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        pDriver = Abc_ObjFanin0( pNode );
+        if ( !Abc_ObjIsNode(pDriver) )
+            continue;
+        pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
+        pNodeNew = (Abc_Obj_t *)Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
+        assert( !Abc_ObjIsComplement(pNodeNew) );
+        pDriver->pCopy = Abc_ObjNotCond( pNodeNew, Dsd_IsComplement(pNodeDsd) );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DSD using the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Obj_t * Abc_NtkDsdConstructNode( Dsd_Manager_t * pManDsd, Dsd_Node_t * pNodeDsd, Abc_Ntk_t * pNtkNew )
+{
+    DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd );
+    DdManager * ddNew = pNtkNew->pManFunc;
+    Dsd_Node_t * pFaninDsd;
+    Abc_Obj_t * pNodeNew, * pFanin;
+    DdNode * bLocal, * bTemp, * bVar;
+    Dsd_Type_t Type;
+    int i, nDecs;
+
+    // create the new node
+    pNodeNew = Abc_NtkCreateNode( pNtkNew );
+    // add the fanins
+    Type  = Dsd_NodeReadType( pNodeDsd );
+    nDecs = Dsd_NodeReadDecsNum( pNodeDsd );
+    assert( nDecs > 1 );
+    for ( i = 0; i < nDecs; i++ )
+    {
+        pFaninDsd  = Dsd_NodeReadDec( pNodeDsd, i );
+        pFanin     = (Abc_Obj_t *)Dsd_NodeReadMark(Dsd_Regular(pFaninDsd));
+        Abc_ObjAddFanin( pNodeNew, pFanin );
+        assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) );
+    }
+
+    // create the local function depending on the type of the node
+    ddNew = pNtkNew->pManFunc;
+    switch ( Type )
+    {
+        case DSD_NODE_CONST1:
+        {
+            bLocal = ddNew->one; Cudd_Ref( bLocal );
+            break;
+        }
+        case DSD_NODE_OR:
+        {
+            bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal );
+            for ( i = 0; i < nDecs; i++ )
+            {
+                pFaninDsd  = Dsd_NodeReadDec( pNodeDsd, i );
+                bVar   = Cudd_NotCond( ddNew->vars[i], Dsd_IsComplement(pFaninDsd) );
+                bLocal = Cudd_bddOr( ddNew, bTemp = bLocal, bVar );               Cudd_Ref( bLocal );
+                Cudd_RecursiveDeref( ddNew, bTemp );
+            }
+            break;
+        }
+        case DSD_NODE_EXOR:
+        {
+            bLocal = Cudd_Not(ddNew->one); Cudd_Ref( bLocal );
+            for ( i = 0; i < nDecs; i++ )
+            {
+                bLocal = Cudd_bddXor( ddNew, bTemp = bLocal, ddNew->vars[i] );    Cudd_Ref( bLocal );
+                Cudd_RecursiveDeref( ddNew, bTemp );
+            }
+            break;
+        }
+        case DSD_NODE_PRIME:
+        {
+            bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd );                Cudd_Ref( bLocal );
+            bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal );
+            Cudd_RecursiveDeref( ddDsd, bTemp );
+            // bLocal is now in the new BDD manager
+            break;
+        }
+        default:
+        {
+            assert( 0 );
+            break;
+        }
+    }
+    pNodeNew->pData = bLocal;
+    Dsd_NodeSetMark( pNodeDsd, (int)pNodeNew );
+    return pNodeNew;
+}
+
+
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively decomposes internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDsdRecursive( Abc_Ntk_t * pNtk, bool fVerbose )
+{
+    int fCheck = 1;
+    Dsd_Manager_t * pManDsd;
+    DdManager * dd = pNtk->pManFunc;
+    Vec_Ptr_t * vNodes;
+    int i;
+
+    assert( Abc_NtkIsLogicBdd(pNtk) );
+
+    // make the network minimum base
+    Abc_NtkMinimumBase( pNtk );
+
+    // start the DSD manager
+    pManDsd = Dsd_ManagerStart( dd, dd->size, 0 );
+
+    // collect nodes for decomposition
+    vNodes = Abc_NtkCollectNodesForDsd( pNtk );
+    for ( i = 0; i < vNodes->nSize; i++ )
+        Abc_NodeDecompDsdAndMux( vNodes->pArray[i], vNodes, pManDsd );
+    Vec_PtrFree( vNodes );
+
+    // stop the DSD manager
+    Dsd_ManagerStop( pManDsd );
+
+    // make sure everything is okay
+    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkDsdRecursive: The network check has failed.\n" );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the nodes that may need decomposition.]
+
+  Description [The nodes that do not need decomposition are those
+  whose BDD has more internal nodes than the support size.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkCollectNodesForDsd( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pNode;
+    int i;
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_NodeIsForDsd(pNode) )
+            Vec_PtrPush( vNodes, pNode );
+    }
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager_t * pManDsd )
+{
+    DdManager * dd = pNode->pNtk->pManFunc;
+    Abc_Obj_t * pRoot, * pFanin, * pNode1, * pNode2, * pNodeC;
+    Dsd_Node_t ** ppNodesDsd, * pNodeDsd, * pFaninDsd;
+    int i, nNodesDsd, iVar, fCompl;
+
+    // try disjoint support decomposition
+    pNodeDsd = Dsd_DecomposeOne( pManDsd, pNode->pData );
+    fCompl   = Dsd_IsComplement( pNodeDsd );
+    pNodeDsd = Dsd_Regular( pNodeDsd );
+
+    // determine what decomposition to use   
+    if ( Dsd_NodeReadDecsNum(pNodeDsd) != Abc_ObjFaninNum(pNode) )
+    { // perform DSD
+
+        // set the inputs
+        Abc_ObjForEachFanin( pNode, pFanin, i )
+        {
+            pFaninDsd = Dsd_ManagerReadInput( pManDsd, i );
+            Dsd_NodeSetMark( pFaninDsd, (int)pFanin );
+        }
+
+        // construct the intermediate nodes
+        ppNodesDsd = Dsd_TreeCollectNodesDfsOne( pManDsd, pNodeDsd, &nNodesDsd );
+        for ( i = 0; i < nNodesDsd; i++ )
+        {
+            pRoot = Abc_NtkDsdConstructNode( pManDsd, ppNodesDsd[i], pNode->pNtk );
+            if ( Abc_NodeIsForDsd(pRoot) )
+                Vec_PtrPush( vNodes, pRoot );
+        }
+        free( ppNodesDsd );
+
+        // remove the current fanins
+        Abc_ObjRemoveFanins( pNode );
+        // add fanin to the root
+        Abc_ObjAddFanin( pNode, pRoot );
+        // update the function to be that of buffer
+        Cudd_RecursiveDeref( dd, pNode->pData );
+        pNode->pData = Cudd_NotCond( dd->vars[0], fCompl ); Cudd_Ref( pNode->pData );
+    }
+    else // perform MUX-decomposition
+    {
+        // get the cofactoring variable
+        iVar = Abc_NodeFindMuxVar( dd, pNode->pData, Abc_ObjFaninNum(pNode) );
+        pNodeC = Abc_ObjFanin( pNode, iVar );
+
+        // get the negative cofactor
+        pNode1 = Abc_NodeClone( pNode );
+        pNode1->pData = Cudd_Cofactor( dd, pNode->pData, Cudd_Not(dd->vars[iVar]) );  Cudd_Ref( pNode1->pData );
+        Abc_NodeMinimumBase( pNode1 );
+        if ( Abc_NodeIsForDsd(pNode1) )
+            Vec_PtrPush( vNodes, pNode1 );
+
+        // get the positive cofactor
+        pNode2 = Abc_NodeClone( pNode );
+        pNode2->pData = Cudd_Cofactor( dd, pNode->pData, dd->vars[iVar] );            Cudd_Ref( pNode2->pData );
+        Abc_NodeMinimumBase( pNode2 );
+        if ( Abc_NodeIsForDsd(pNode2) )
+            Vec_PtrPush( vNodes, pNode2 );
+
+        // remove the current fanins
+        Abc_ObjRemoveFanins( pNode );
+        // add new fanins
+        Abc_ObjAddFanin( pNode, pNodeC );
+        Abc_ObjAddFanin( pNode, pNode2 );
+        Abc_ObjAddFanin( pNode, pNode1 );
+        // update the function to be that of MUX
+        Cudd_RecursiveDeref( dd, pNode->pData );
+        pNode->pData = Cudd_bddIte( dd, dd->vars[0], dd->vars[1], dd->vars[2] );    Cudd_Ref( pNode->pData );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one node.]
 
   Description []
                
@@ -39,7 +464,64 @@
   SeeAlso     []
 
 ***********************************************************************/
+bool Abc_NodeIsForDsd( Abc_Obj_t * pNode )
+{
+    assert( Abc_ObjIsNode(pNode) );
+    if ( Cudd_DagSize(pNode->pData)-1 > Abc_ObjFaninNum(pNode) )
+        return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Determines a cofactoring variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeFindMuxVar( DdManager * dd, DdNode * bFunc, int nVars )
+{
+    DdNode * bVar, * bCof0, * bCof1;
+    int SuppSumMin = 1000000;
+    int i, nSSD, nSSQ, iVar;
+
+//    printf( "\n\nCofactors:\n\n" );
+    iVar = -1;
+    for ( i = 0; i < nVars; i++ )
+    {
+        bVar = dd->vars[i];
+
+        bCof0 = Cudd_Cofactor( dd, bFunc, Cudd_Not(bVar) );  Cudd_Ref( bCof0 );
+        bCof1 = Cudd_Cofactor( dd, bFunc,          bVar  );  Cudd_Ref( bCof1 );
+
+//        nodD = Cudd_DagSize(bCof0);
+//        nodQ = Cudd_DagSize(bCof1);
+//        printf( "+%02d: D=%2d. Q=%2d.  ", i, nodD, nodQ );
+//        printf( "S=%2d. D=%2d.  ", nodD + nodQ, abs(nodD-nodQ) );
+
+        nSSD = Cudd_SupportSize( dd, bCof0 );
+        nSSQ = Cudd_SupportSize( dd, bCof1 );
+
+//        printf( "SD=%2d. SQ=%2d.  ", nSSD, nSSQ );
+//        printf( "S=%2d. D=%2d.  ", nSSD + nSSQ, abs(nSSD - nSSQ) );
+//        printf( "Cost=%3d. ", Cost(nodD,nodQ,nSSD,nSSQ) );
+//        printf( "\n" );
+
+        Cudd_RecursiveDeref( dd, bCof0 );
+        Cudd_RecursiveDeref( dd, bCof1 );
 
+        if ( SuppSumMin > nSSD + nSSQ )
+        {
+             SuppSumMin = nSSD + nSSQ;
+             iVar = i;
+        }
+    }
+    return iVar;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/abc/abcFanio.c

@@ -85,6 +85,32 @@ void Abc_ObjDeleteFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFanin )
     }
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Destroys fanout/fanin relationship between the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ObjRemoveFanins( Abc_Obj_t * pObj )
+{
+    Vec_Fan_t * vFaninsOld;
+    Abc_Obj_t * pFanin;
+    int k;
+    // remove old fanins
+    vFaninsOld = &pObj->vFanins;
+    for ( k = vFaninsOld->nSize - 1; k >= 0; k-- )
+    {
+        pFanin = Abc_NtkObj( pObj->pNtk, vFaninsOld->pArray[k].iFan );
+        Abc_ObjDeleteFanin( pObj, pFanin );
+    }
+}
+
 /**Function*************************************************************
 
   Synopsis    [Replaces a fanin of the node.]

src/base/abc/abcFraig.c

@@ -435,7 +435,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk )
     if ( pStore == NULL )
     {
         // start the stored network
-        pStore = Abc_NtkStrash( pNtk );
+        pStore = Abc_NtkStrash( pNtk, 0 );
         if ( pStore == NULL )
         {
             printf( "Abc_NtkFraigStore: Initial strashing has failed.\n" );

src/base/abc/abcFunc.c

@@ -166,7 +166,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
         assert( pNode->pData );
         bFunc = pNode->pData;
 //Extra_bddPrint( dd, bFunc ); printf( "\n" ); printf( "\n" );
-        pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, Abc_ObjFaninNum(pNode), vCube, -1 );
+        pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, -1 );
         if ( pNode->pData == NULL )
             return 0;
         Cudd_RecursiveDeref( dd, bFunc );
@@ -193,18 +193,20 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFunc, int nFanins, Vec_Str_t * vCube, int fMode )
+char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode )
 {
+    int fVerify = 1;
     char * pSop;
     DdNode * bFuncNew, * bCover, * zCover, * zCover0, * zCover1;
     int nCubes, nCubes0, nCubes1, fPhase;
 
-    if ( Cudd_IsConstant(bFunc) )
+    assert( bFuncOn == bFuncOnDc || Cudd_bddLeq( dd, bFuncOn, bFuncOnDc ) );
+    if ( Cudd_IsConstant(bFuncOn) || Cudd_IsConstant(bFuncOnDc) )
     {
         Vec_StrFill( vCube, nFanins, '-' );
         Vec_StrPush( vCube, '\0' );
         pSop = Extra_MmFlexEntryFetch( pMan, nFanins + 4 );
-        if ( bFunc == Cudd_ReadLogicZero(dd) )
+        if ( bFuncOn == Cudd_ReadLogicZero(dd) )
             sprintf( pSop, "%s 0\n", vCube->pArray );
         else
             sprintf( pSop, "%s 1\n", vCube->pArray );
@@ -216,14 +218,14 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     { // try both phases
 
         // get the ZDD of the negative polarity
-        bCover = Cudd_zddIsop( dd, Cudd_Not(bFunc), Cudd_Not(bFunc), &zCover0 );
+        bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover0 );
         Cudd_Ref( zCover0 );
         Cudd_Ref( bCover );
         Cudd_RecursiveDeref( dd, bCover );
         nCubes0 = Abc_CountZddCubes( dd, zCover0 );
 
         // get the ZDD of the positive polarity
-        bCover = Cudd_zddIsop( dd, bFunc, bFunc, &zCover1 );
+        bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover1 );
         Cudd_Ref( zCover1 );
         Cudd_Ref( bCover );
         Cudd_RecursiveDeref( dd, bCover );
@@ -248,7 +250,7 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     else if ( fMode == 0 )
     {
         // get the ZDD of the positive polarity
-        bCover = Cudd_zddIsop( dd, Cudd_Not(bFunc), Cudd_Not(bFunc), &zCover );
+        bCover = Cudd_zddIsop( dd, Cudd_Not(bFuncOnDc), Cudd_Not(bFuncOn), &zCover );
         Cudd_Ref( zCover );
         Cudd_Ref( bCover );
         Cudd_RecursiveDeref( dd, bCover );
@@ -258,7 +260,7 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     else if ( fMode == 1 )
     {
         // get the ZDD of the positive polarity
-        bCover = Cudd_zddIsop( dd, bFunc, bFunc, &zCover );
+        bCover = Cudd_zddIsop( dd, bFuncOn, bFuncOnDc, &zCover );
         Cudd_Ref( zCover );
         Cudd_Ref( bCover );
         Cudd_RecursiveDeref( dd, bCover );
@@ -271,7 +273,10 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     }
 
     // allocate memory for the cover
-    pSop = Extra_MmFlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 );
+    if ( pMan )
+        pSop = Extra_MmFlexEntryFetch( pMan, (nFanins + 3) * nCubes + 1 );
+    else 
+        pSop = ALLOC( char, (nFanins + 3) * nCubes + 1 );
     pSop[(nFanins + 3) * nCubes] = 0;
     // create the SOP
     Vec_StrFill( vCube, nFanins, '-' );
@@ -280,12 +285,21 @@ char * Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFun
     Cudd_RecursiveDerefZdd( dd, zCover );
 
     // verify
-    bFuncNew = Abc_ConvertSopToBdd( dd, pSop, nFanins );  Cudd_Ref( bFuncNew );
-//Extra_bddPrint( dd, bFunc );
-//Extra_bddPrint( dd, bFuncNew );
-    if ( bFuncNew != bFunc )
-        printf( "Verification failed.\n" );
-    Cudd_RecursiveDeref( dd, bFuncNew );
+    if ( fVerify )
+    {
+        bFuncNew = Abc_ConvertSopToBdd( dd, pSop, nFanins );  Cudd_Ref( bFuncNew );
+        if ( bFuncOn == bFuncOnDc )
+        {
+            if ( bFuncNew != bFuncOn )
+                printf( "Verification failed.\n" );
+        }
+        else
+        {
+            if ( !Cudd_bddLeq(dd, bFuncOn, bFuncNew) || !Cudd_bddLeq(dd, bFuncNew, bFuncOnDc) )
+                printf( "Verification failed.\n" );
+        }
+        Cudd_RecursiveDeref( dd, bFuncNew );
+    }
     return pSop;
 }
 
@@ -359,8 +373,8 @@ int Abc_ConvertZddToSop( DdManager * dd, DdNode * zCover, char * pSop, int nFani
 void Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 )
 {
     assert( Abc_NtkIsLogicBdd(pNode->pNtk) ); 
-    *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 0 );
-    *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 1 );
+    *ppSop0 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 0 );
+    *ppSop1 = Abc_ConvertBddToSop( pMmMan, pNode->pNtk->pManFunc, pNode->pData, pNode->pData, Abc_ObjFaninNum(pNode), vCube, 1 );
 }
 
 

src/base/abc/abcFxu.c

@@ -52,6 +52,8 @@ static void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p );
 ***********************************************************************/
 bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 {
+    int fCheck = 1;
+
     assert( Abc_NtkIsLogicBdd(pNtk) || Abc_NtkIsLogicSop(pNtk) );
     // convert nodes to SOPs
     if ( Abc_NtkIsLogicBdd(pNtk) )
@@ -70,20 +72,19 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
     // sweep removes useless nodes
     Abc_NtkCleanup( pNtk, 0 );
     // collect information about the covers
-    // make sure all covers are SCC free
-    // allocate literal array for each cover
     Abc_NtkFxuCollectInfo( pNtk, p );
     // call the fast extract procedure
-    // returns the number of divisor extracted
     if ( Fxu_FastExtract(p) > 0 )
     {
         // update the network
         Abc_NtkFxuReconstruct( pNtk, p );
         // make sure everything is okay
-        if ( !Abc_NtkCheck( pNtk ) )
+        if ( fCheck && !Abc_NtkCheck( pNtk ) )
             printf( "Abc_NtkFastExtract: The network check has failed.\n" );
         return 1;
     }
+    else
+        printf( "Warning: The network has not been changed by \"fx\".\n" );
     return 0;
 }
 
@@ -199,7 +200,6 @@ void Abc_NtkFxuFreeInfo( Fxu_Data_t * p )
 ***********************************************************************/
 void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
 {
-    Vec_Fan_t * vFaninsOld;
     Vec_Int_t * vFanins;
     Abc_Obj_t * pNode, * pFanin;
     int i, k;
@@ -221,12 +221,7 @@ void Abc_NtkFxuReconstruct( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
             continue;
         // remove old fanins
         pNode = Abc_NtkObj( pNtk, i );
-        vFaninsOld = &pNode->vFanins;
-        for ( k = vFaninsOld->nSize - 1; k >= 0; k-- )
-        {
-            pFanin = Abc_NtkObj( pNtk, vFaninsOld->pArray[k].iFan );
-            Abc_ObjDeleteFanin( pNode, pFanin );
-        }
+        Abc_ObjRemoveFanins( pNode );
         // add new fanins
         vFanins = p->vFaninsNew->pArray[i];
         for ( k = 0; k < vFanins->nSize; k++ )

src/base/abc/abcMap.c

@@ -353,7 +353,7 @@ Abc_Obj_t * Abc_NodeFromMapSuper_rec( Abc_Ntk_t * pNtkNew, Map_Node_t * pNodeMap
         }
         else
         {  
-            assert( 0 );
+//            assert( 0 );
             /* It might happen that a super gate with 5 inputs is constructed that
              * actually depends only on the first four variables; i.e the fifth is a
              * don't care -- in that case we connect constant node for the fifth

src/base/abc/abcMiter.c

@@ -51,8 +51,8 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb )
     Abc_Ntk_t * pTemp = NULL;
     int fRemove1, fRemove2;
     // make sure the circuits are strashed 
-    fRemove1 = (!Abc_NtkIsAig(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1));
-    fRemove2 = (!Abc_NtkIsAig(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2));
+    fRemove1 = (!Abc_NtkIsAig(pNtk1)) && (pNtk1 = Abc_NtkStrash(pNtk1, 0));
+    fRemove2 = (!Abc_NtkIsAig(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0));
     if ( pNtk1 && pNtk2 )
     {
         // check that the networks have the same PIs/POs/latches

src/base/abc/abcPrint.c

@@ -52,7 +52,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
     }
     else if ( Abc_NtkIsAig(pNtk) )
+    {
         fprintf( pFile, "  and = %5d", Abc_NtkNodeNum(pNtk) );
+        fprintf( pFile, "  choice = %5d", Abc_NtkCountChoiceNodes(pNtk) );
+    }
     else 
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
 
@@ -86,19 +89,19 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk )
 ***********************************************************************/
 void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk )
 {
-    Abc_Obj_t * pNet, * pLatch;
+    Abc_Obj_t * pObj, * pLatch;
     int i;
 
     if ( Abc_NtkIsNetlist(pNtk) )
     {
         fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) );    
-        Abc_NtkForEachPi( pNtk, pNet, i )
-            fprintf( pFile, " %s", Abc_ObjName(pNet) );
+        Abc_NtkForEachPi( pNtk, pObj, i )
+            fprintf( pFile, " %s", Abc_ObjName(pObj) );
         fprintf( pFile, "\n" );   
     
         fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) );    
-        Abc_NtkForEachPo( pNtk, pNet, i )
-            fprintf( pFile, " %s", Abc_ObjName(pNet) );
+        Abc_NtkForEachPo( pNtk, pObj, i )
+            fprintf( pFile, " %s", Abc_ObjName(pObj) );
         fprintf( pFile, "\n" );    
   
         fprintf( pFile, "Latches (%d):  ", Abc_NtkLatchNum(pNtk) );  
@@ -109,12 +112,12 @@ void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk )
     else
     {
         fprintf( pFile, "Primary inputs (%d): ", Abc_NtkPiNum(pNtk) );    
-        Abc_NtkForEachPi( pNtk, pNet, i )
+        Abc_NtkForEachPi( pNtk, pObj, i )
             fprintf( pFile, " %s", pNtk->vNamesPi->pArray[i] );
         fprintf( pFile, "\n" );   
     
         fprintf( pFile, "Primary outputs (%d):", Abc_NtkPoNum(pNtk) );    
-        Abc_NtkForEachPo( pNtk, pNet, i )
+        Abc_NtkForEachPo( pNtk, pObj, i )
             fprintf( pFile, " %s", pNtk->vNamesPo->pArray[i] );
         fprintf( pFile, "\n" );    
   
@@ -280,7 +283,6 @@ void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode )
     Vec_IntFree( vFactor );
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/abc/abcRes.c

+/**CFile****************************************************************
+
+  FileName    [abcRes.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Technology-independent resynthesis of the AIG.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcRes.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "ft.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+static void        Abc_NodeResyn( Abc_ManRes_t * p );
+
+static void        Abc_NodeFindCut( Abc_ManRes_t * p );
+static int         Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit );
+static int         Abc_NodeGetFaninCost( Abc_Obj_t * pNode );
+static void        Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited );
+static void        Abc_NodeConeMark( Vec_Ptr_t * vVisited );
+static void        Abc_NodeConeUnmark( Vec_Ptr_t * vVisited );
+
+static Vec_Int_t * Abc_NodeRefactor( Abc_ManRes_t * p );
+static DdNode *    Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited );
+
+static int         Abc_NodeDecide( Abc_ManRes_t * p );
+static void        Abc_NodeUpdate( Abc_ManRes_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs incremental resynthesis of the AIG.]
+
+  Description [Starting from each node, computes a reconvergence-driven cut, 
+  derives BDD of the cut function, constructs ISOP, factors the cover, 
+  and replaces the current implementation of the MFFC of the cut by the 
+  new factored form if the number of AIG nodes is reduced. Returns the
+  number of AIG nodes saved.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkAigResynthesize( Abc_Ntk_t * pNtk, Abc_ManRes_t * p )
+{
+    int fCheck = 1;
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode;
+    int i, Counter, Approx;
+
+    assert( Abc_NtkIsAig(pNtk) );
+
+    // start the BDD manager
+    p->dd = Cudd_Init( p->nNodeSizeMax + p->nConeSizeMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_zddVarsFromBddVars( p->dd, 2 );
+    p->bCubeX = Extra_bddComputeRangeCube( p->dd, p->nNodeSizeMax, p->dd->size );   Cudd_Ref( p->bCubeX );
+
+    // remember the number of nodes
+    Counter = Abc_NtkNodeNum( pNtk );
+    // resynthesize each node
+    pProgress = Extra_ProgressBarStart( stdout, 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        Approx = (int)(100.0 * i / pNtk->vObjs->nSize );
+        Extra_ProgressBarUpdate( pProgress, Approx, NULL );
+        p->pNode = pNode;
+        Abc_NodeResyn( p );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Abc_NtkManResStop( p );
+
+    // check
+    if ( fCheck && !Abc_NtkCheck( pNtk ) )
+    {
+        printf( "Abc_NtkAigResynthesize: The network check has failed.\n" );
+        return -1;
+    }
+    return Abc_NtkNodeNum(pNtk) - Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs resynthesis of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeResyn( Abc_ManRes_t * p )
+{
+    int RetValue;
+    int clk;
+
+    assert( Abc_ObjIsNode(p->pNode) );
+
+clk = clock();
+    // detect the cut
+    Abc_NodeFindCut( p );
+p->time1 += clock() - clk;
+
+    // refactor the cut
+clk = clock();
+    p->vForm = Abc_NodeRefactor( p );
+p->time2 += clock() - clk;
+
+    // accept or reject the factored form
+clk = clock();
+    RetValue = Abc_NodeDecide( p );
+p->time3 += clock() - clk;
+
+    // modify the network
+clk = clock();
+    if ( RetValue )
+        Abc_NodeUpdate( p );
+p->time4 += clock() - clk;
+
+    // cleanup
+    Vec_IntFree( p->vForm );
+    p->vForm = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds a reconvergence-driven cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFindCut( Abc_ManRes_t * p )
+{
+    Abc_Obj_t * pNode = p->pNode;
+    int i;
+
+    // mark TFI using fMarkA
+    Vec_PtrClear( p->vVisited );
+    Abc_NodeConeMarkCollect_rec( pNode, p->vVisited );
+
+    // start the reconvergence-driven node
+    Vec_PtrClear( p->vInsideNode );
+    Vec_PtrClear( p->vFaninsNode );
+    Vec_PtrPush( p->vFaninsNode, pNode );
+    pNode->fMarkB = 1;
+
+    // compute reconvergence-driven node
+    while ( Abc_NodeFindCut_int( p->vInsideNode, p->vFaninsNode, p->nNodeSizeMax ) );
+
+    // compute reconvergence-driven cone
+    Vec_PtrClear( p->vInsideCone );
+    Vec_PtrClear( p->vFaninsCone );
+    if ( p->nConeSizeMax > p->nNodeSizeMax )
+    {
+        // copy the node into the cone
+        Vec_PtrForEachEntry( p->vInsideNode, pNode, i )
+            Vec_PtrPush( p->vInsideCone, pNode );
+        Vec_PtrForEachEntry( p->vFaninsNode, pNode, i )
+            Vec_PtrPush( p->vFaninsCone, pNode );
+        // compute reconvergence-driven cone
+        while ( Abc_NodeFindCut_int( p->vInsideCone, p->vFaninsCone, p->nConeSizeMax ) );
+        // unmark the nodes of the sets
+        Vec_PtrForEachEntry( p->vInsideCone, pNode, i )
+            pNode->fMarkB = 0;
+        Vec_PtrForEachEntry( p->vFaninsCone, pNode, i )
+            pNode->fMarkB = 0;
+    }
+    else
+    {
+        // unmark the nodes of the sets
+        Vec_PtrForEachEntry( p->vInsideNode, pNode, i )
+            pNode->fMarkB = 0;
+        Vec_PtrForEachEntry( p->vFaninsNode, pNode, i )
+            pNode->fMarkB = 0;
+    }
+
+    // unmark TFI using fMarkA
+    Abc_NodeConeUnmark( p->vVisited );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds a reconvergence-driven cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeFindCut_int( Vec_Ptr_t * vInside, Vec_Ptr_t * vFanins, int nSizeLimit )
+{
+    Abc_Obj_t * pNode, * pFaninBest, * pNext;
+    int CostBest, CostCur, i;
+    // find the best fanin
+    CostBest   = 100;
+    pFaninBest = NULL;
+    Vec_PtrForEachEntry( vFanins, pNode, i )
+    {
+        CostCur = Abc_NodeGetFaninCost( pNode );
+        if ( CostBest > CostCur )
+        {
+            CostBest   = CostCur;
+            pFaninBest = pNode;
+        }
+    }
+    if ( pFaninBest == NULL )
+        return 0;
+    assert( CostBest < 3 );
+    if ( vFanins->nSize - 1 + CostBest > nSizeLimit )
+        return 0;
+    assert( Abc_ObjIsNode(pFaninBest) );
+    // remove the node from the array
+    Vec_PtrRemove( vFanins, pFaninBest );
+    // add the node to the set
+    Vec_PtrPush( vInside, pFaninBest );
+    // add the left child to the fanins
+    pNext = Abc_ObjFanin0(pFaninBest);
+    if ( !pNext->fMarkB )
+    {
+        pNext->fMarkB = 1;
+        Vec_PtrPush( vFanins, pNext );
+    }
+    // add the right child to the fanins
+    pNext = Abc_ObjFanin1(pFaninBest);
+    if ( !pNext->fMarkB )
+    {
+        pNext->fMarkB = 1;
+        Vec_PtrPush( vFanins, pNext );
+    }
+    assert( vFanins->nSize <= nSizeLimit );
+    // keep doing this
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluate the fanin cost.]
+
+  Description [Returns the number of fanins that will be brought in.
+  Returns large number if the node cannot be added.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NodeGetFaninCost( Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    assert( pNode->fMarkA == 1 );  // this node is in the TFI
+    assert( pNode->fMarkB == 1 );  // this node is in the constructed cone
+    // check the PI node
+    if ( !Abc_ObjIsNode(pNode) )
+        return 999;
+    // check the fanouts
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        if ( pFanout->fMarkA && pFanout->fMarkB == 0 ) // in the cone but not in the set
+            return 999;
+    // the fanouts are in the TFI and inside the constructed cone
+    // return the number of fanins that will be on the boundary if this node is added
+    return (!Abc_ObjFanin0(pNode)->fMarkB) + (!Abc_ObjFanin1(pNode)->fMarkB);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
+{
+    if ( pNode->fMarkA == 1 )
+        return;
+    // visit transitive fanin 
+    if ( Abc_ObjIsNode(pNode) )
+    {
+        Abc_NodeConeMarkCollect_rec( Abc_ObjFanin0(pNode), vVisited );
+        Abc_NodeConeMarkCollect_rec( Abc_ObjFanin1(pNode), vVisited );
+    }
+    assert( pNode->fMarkA == 0 );
+    pNode->fMarkA = 1;
+    Vec_PtrPush( vVisited, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConeMark( Vec_Ptr_t * vVisited )
+{
+    int i;
+    for ( i = 0; i < vVisited->nSize; i++ )
+        ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Unmarks the TFI cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeConeUnmark( Vec_Ptr_t * vVisited )
+{
+    int i;
+    for ( i = 0; i < vVisited->nSize; i++ )
+        ((Abc_Obj_t *)vVisited->pArray)->fMarkA = 0;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the factored form of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Abc_NodeRefactor( Abc_ManRes_t * p )
+{
+    Vec_Int_t * vForm;
+    DdManager * dd = p->dd;
+    DdNode * bFuncNode, * bFuncCone, * bCare, * bFuncOn, * bFuncOnDc;
+    char * pSop;
+    int nFanins;
+
+    assert( p->vFaninsNode->nSize < p->nNodeSizeMax );
+    assert( p->vFaninsCone->nSize < p->nConeSizeMax );
+
+    // get the function of the node
+    bFuncNode = Abc_NodeConeBdd( dd, p->dd->vars, p->pNode, p->vFaninsNode, p->vVisited );  
+    Cudd_Ref( bFuncNode );
+    nFanins = p->vFaninsNode->nSize;
+    if ( p->nConeSizeMax > p->nNodeSizeMax )
+    {
+        // get the function of the cone
+        bFuncCone = Abc_NodeConeBdd( dd, p->dd->vars + p->nNodeSizeMax, p->pNode, p->vFaninsCone, p->vVisited );  
+        Cudd_Ref( bFuncCone );
+        // get the care set
+        bCare = Cudd_bddXorExistAbstract( p->dd, Cudd_Not(bFuncNode), bFuncCone, p->bCubeX );   Cudd_Ref( bCare );
+        Cudd_RecursiveDeref( dd, bFuncCone );
+        // compute the on-set and off-set of the function of the node
+        bFuncOn   = Cudd_bddAnd( dd, bFuncNode, bCare );                Cudd_Ref( bFuncOn );
+        bFuncOnDc = Cudd_bddAnd( dd, Cudd_Not(bFuncNode), bCare );      Cudd_Ref( bFuncOnDc );
+        bFuncOnDc = Cudd_Not( bFuncOnDc );
+        Cudd_RecursiveDeref( dd, bCare );
+        // get the cover
+        pSop = Abc_ConvertBddToSop( NULL, dd, bFuncOn, bFuncOnDc, nFanins, p->vCube, -1 );
+        Cudd_RecursiveDeref( dd, bFuncOn );
+        Cudd_RecursiveDeref( dd, bFuncOnDc );
+    }
+    else
+    {
+        // get the cover
+        pSop = Abc_ConvertBddToSop( NULL, dd, bFuncNode, bFuncNode, nFanins, p->vCube, -1 );
+    }
+    Cudd_RecursiveDeref( dd, bFuncNode );
+    // derive the factored form
+    vForm = Ft_Factor( pSop );
+    free( pSop );
+    return vForm;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns BDD representing the logic function of the cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, Vec_Ptr_t * vVisited )
+{
+    DdNode * bFunc0, * bFunc1, * bFunc;
+    int i;
+    // mark the fanins of the cone
+    Abc_NodeConeMark( vFanins );
+    // collect the nodes in the DFS order
+    Vec_PtrClear( vVisited );
+    Abc_NodeConeMarkCollect_rec( pNode, vVisited );
+    // unmark both sets
+    Abc_NodeConeUnmark( vFanins );
+    Abc_NodeConeUnmark( vVisited );
+    // set the elementary BDDs
+    Vec_PtrForEachEntry( vFanins, pNode, i )
+        pNode->pCopy = (Abc_Obj_t *)pbVars[i];
+    // compute the BDDs for the collected nodes
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+    {
+        bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
+        bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
+        bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );    Cudd_Ref( bFunc );
+        pNode->pCopy = (Abc_Obj_t *)bFunc;
+    }
+    Cudd_Ref( bFunc );
+    // dereference the intermediate ones
+    Vec_PtrForEachEntry( vVisited, pNode, i )
+        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy );
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Decides whether to accept the given factored form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int  Abc_NodeDecide( Abc_ManRes_t * p )
+{
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Replaces MFFC of the node by the new factored.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeUpdate( Abc_ManRes_t * p )
+{
+}
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_ManRes_t * Abc_NtkManResStart()
+{
+    Abc_ManRes_t * p;
+    p = ALLOC( Abc_ManRes_t, 1 );
+    p->vFaninsNode = Vec_PtrAlloc( 100 );
+    p->vInsideNode = Vec_PtrAlloc( 100 );
+    p->vFaninsCone = Vec_PtrAlloc( 100 );
+    p->vInsideCone = Vec_PtrAlloc( 100 );
+    p->vVisited    = Vec_PtrAlloc( 100 );
+    p->vCube       = Vec_StrAlloc( 100 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkManResStop( Abc_ManRes_t * p )
+{
+    if ( p->bCubeX ) Cudd_RecursiveDeref( p->dd, p->bCubeX );
+    if ( p->dd )     Extra_StopManager( p->dd );
+    Vec_PtrFree( p->vFaninsNode );
+    Vec_PtrFree( p->vInsideNode );
+    Vec_PtrFree( p->vFaninsCone );
+    Vec_PtrFree( p->vInsideCone );
+    Vec_PtrFree( p->vVisited    );
+    Vec_StrFree( p->vCube       );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcShow.c

+/**CFile****************************************************************
+
+  FileName    [abcShow.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Visualization procedures using DOT software and GSView.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcShow.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#ifdef WIN32
+#include "process.h" 
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the factored form of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodePrintBdd( Abc_Obj_t * pNode )
+{
+    FILE * pFile;
+    Vec_Ptr_t * vNamesIn;
+    char * FileNameIn;
+    char * FileNameOut;
+    char * FileGeneric;
+    char * pCur, * pNameOut;
+    char FileNameDot[200];
+    char FileNamePs[200];
+    char CommandDot[1000];
+#ifndef WIN32
+    char CommandPs[1000];
+#endif
+    char * pProgDotName;
+    char * pProgGsViewName;
+    int RetValue;
+
+    assert( Abc_NtkIsLogicBdd(pNode->pNtk) );
+
+#ifdef WIN32
+    pProgDotName = "dot.exe";
+    pProgGsViewName = NULL;
+#else
+    pProgDotName = "dot";
+    pProgGsViewName = "gv";
+#endif
+
+    FileNameIn  = NULL;
+    FileNameOut = NULL;
+
+    // get the generic file name
+    pNode->pCopy = NULL;
+    FileGeneric = Abc_ObjName(pNode);
+    // get rid of not-alpha-numeric characters
+    for ( pCur = FileGeneric; *pCur; pCur++ )
+        if ( !((*pCur >= '0' && *pCur <= '9') || (*pCur >= 'a' && *pCur <= 'z') || (*pCur >= 'A' && *pCur <= 'Z')) )
+            *pCur = '_';
+    // create the file names
+    sprintf( FileNameDot, "%s.dot", FileGeneric ); 
+    sprintf( FileNamePs,  "%s.ps",  FileGeneric ); 
+
+    // write the DOT file
+    if ( (pFile = fopen( FileNameDot, "w" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+        return;
+    }
+    // set the node names 
+    Abc_NtkLogicTransferNames( pNode->pNtk );
+    vNamesIn = Abc_NodeGetFaninNames( pNode );
+    pNameOut = Abc_ObjName(pNode);
+    Cudd_DumpDot( pNode->pNtk->pManFunc, 1, (DdNode **)&pNode->pData, (char **)vNamesIn->pArray, &pNameOut, pFile );
+    Abc_NodeFreeFaninNames( vNamesIn );
+    Abc_NtkCleanCopy( pNode->pNtk );
+    fclose( pFile );
+
+    // check that the input file is okay
+    if ( (pFile = fopen( FileNameDot, "r" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
+        return;
+    }
+    fclose( pFile );
+
+    // generate the DOT file
+    sprintf( CommandDot,  "%s -Tps -o %s %s", pProgDotName, FileNamePs, FileNameDot ); 
+    RetValue = system( CommandDot );
+#ifdef WIN32
+        _unlink( FileNameDot );
+#else
+        unlink( FileNameDot );
+#endif
+    if ( RetValue == -1 )
+    {
+        fprintf( stdout, "Cannot find \"%s\".\n", pProgDotName );
+        return;
+    }
+
+    // check that the input file is okay
+    if ( (pFile = fopen( FileNamePs, "r" )) == NULL )
+    {
+        fprintf( stdout, "Cannot open intermediate file \"%s\".\n", FileNamePs );
+        return;
+    }
+    fclose( pFile ); 
+
+#ifdef WIN32
+    if ( _spawnl( _P_NOWAIT, "gsview32.exe", "gsview32.exe", FileNamePs, NULL ) == -1 )
+        if ( _spawnl( _P_NOWAIT, "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", 
+            "C:\\Program Files\\Ghostgum\\gsview\\gsview32.exe", FileNamePs, NULL ) == -1 )
+        {
+            fprintf( stdout, "Cannot find \"%s\".\n", "gsview32.exe" );
+            return;
+        }
+#else
+    sprintf( CommandPs,  "%s %s &", pProgGsViewName, FileNamePs ); 
+    if ( system( CommandPs ) == -1 )
+    {
+        fprintf( stdout, "Cannot execute \"%s\".\n", FileNamePs );
+        return;
+    }
+#endif
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcStrash.c

@@ -27,7 +27,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 // static functions
-static void        Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig );
+static void        Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fAllNodes );
 static Abc_Obj_t * Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 static Abc_Obj_t * Abc_NodeStrashSop( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
 static Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pNode, char * pSop );
@@ -53,7 +53,7 @@ extern char *      Mio_GateReadSop( void * pGate );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes )
 {
     int fCheck = 1;
     Abc_Ntk_t * pNtkAig;
@@ -68,14 +68,14 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
     // perform strashing
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_AIG );
-    Abc_NtkStrashPerform( pNtk, pNtkAig );
+    Abc_NtkStrashPerform( pNtk, pNtkAig, fAllNodes );
     Abc_NtkFinalize( pNtk, pNtkAig );
     // print warning about self-feed latches
     if ( Abc_NtkCountSelfFeedLatches(pNtkAig) )
         printf( "The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) );
     // duplicate EXDC 
     if ( pNtk->pExdc )
-        pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc );
+        pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0 );
     // make sure everything is okay
     if ( fCheck && !Abc_NtkCheck( pNtkAig ) )
     {
@@ -97,7 +97,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, bool fAllNodes )
 {
     ProgressBar * pProgress;
     Abc_Aig_t * pMan = pNtkNew->pManFunc;
@@ -106,8 +106,10 @@ void Abc_NtkStrashPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
     int i;
 
     // perform strashing
-    vNodes = Abc_NtkDfs( pNtk );
-//    vNodes = Abc_AigCollectAll( pNtk );
+    if ( fAllNodes )
+        vNodes = Abc_AigCollectAll( pNtk );
+    else
+        vNodes = Abc_NtkDfs( pNtk );
     pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     for ( i = 0; i < vNodes->nSize; i++ )
     {
@@ -255,7 +257,7 @@ Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * pS
     assert( vForm->nSize > nVars );
     assert( nVars == Abc_ObjFaninNum(pRoot) );
 
-    // check for constant Andtion
+    // check for constant function
     pFtNode = Ft_NodeRead( vForm, 0 );
     if ( pFtNode->fConst )
     {
@@ -268,7 +270,7 @@ Abc_Obj_t * Abc_NodeStrashFactor( Abc_Aig_t * pMan, Abc_Obj_t * pRoot, char * pS
     Abc_ObjForEachFanin( pRoot, pFanin, i )
         Vec_PtrPush( vAnds, pFanin->pCopy );
 
-    // compute the Andtions of other nodes
+    // compute the function of other nodes
     for ( i = nVars; i < vForm->nSize; i++ )
     {
         pFtNode = Ft_NodeRead( vForm, i );
@@ -322,7 +324,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     Abc_NtkForEachCi( pNtk2, pObj, i )
         pObj->pCopy = Abc_NtkCi(pNtk1, i); 
     // add pNtk2 to pNtk1 while strashing
-    Abc_NtkStrashPerform( pNtk2, pNtk1 );
+    Abc_NtkStrashPerform( pNtk2, pNtk1, 1 );
     // make sure that everything is okay
     if ( fCheck && !Abc_NtkCheck( pNtk1 ) )
     {

src/base/abc/abcSweep.c

@@ -61,7 +61,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
     assert( !Abc_NtkIsAig(pNtk) );
 
     // derive the AIG
-    pNtkAig = Abc_NtkStrash( pNtk );
+    pNtkAig = Abc_NtkStrash( pNtk, 0 );
     // perform fraiging of the AIG
     Fraig_ParamsSetDefault( &Params );
     pMan = Abc_NtkToFraig( pNtkAig, &Params, 0 );    

src/base/abc/abcTiming.c

@@ -228,7 +228,7 @@ void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkTimeFinalize( Abc_Ntk_t * pNtk )
+void Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
     Abc_Time_t ** ppTimes, * pTime;
@@ -283,11 +283,12 @@ void Abc_NtkTimePrepare( Abc_Ntk_t * pNtk )
     if ( pNtk->pManTime == NULL )
     {
         pNtk->pManTime = Abc_ManTimeStart();
-        Abc_NtkTimeFinalize( pNtk );
+        Abc_NtkTimeInitialize( pNtk );
         return;
     }
-    // if timing manager is given, clean arrivals except for PIs
-    // and required except for POs
+    // if timing manager is given, expand it if necessary
+    Abc_ManTimeExpand( pNtk->pManTime, Abc_NtkObjNum(pNtk), 0 );
+    // clean arrivals except for PIs
     ppTimes = (Abc_Time_t **)pNtk->pManTime->vArrs->pArray;
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
@@ -299,6 +300,7 @@ void Abc_NtkTimePrepare( Abc_Ntk_t * pNtk )
         pTime = ppTimes[pObj->Id];
         pTime->Fall = pTime->Rise = pTime->Worst = -ABC_INFINITY;
     }
+    // clean required except for POs
 }
 
 
@@ -392,7 +394,7 @@ void Abc_ManTimeDup( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Expends the storage for timing information.]
 
   Description []
                

src/base/abc/abcUnreach.c

+/**CFile****************************************************************
+
+  FileName    [abcUnreach.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Computes unreachable states for small benchmarks.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcUnreach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static DdNode *    Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose );
+static DdNode *    Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose );
+static DdNode *    Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bRelation, DdNode * bInitial, bool fVerbose );
+static Abc_Ntk_t * Abc_NtkConstructExdc     ( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Extracts sequential DCs of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
+{
+    int fCheck   = 1;
+    int fReorder = 1;
+    DdManager * dd;
+    DdNode * bRelation, * bInitial, * bUnreach;
+
+    // remove EXDC network if present
+    if ( pNtk->pExdc )
+    {
+        Abc_NtkDelete( pNtk->pExdc );
+        pNtk->pExdc = NULL; 
+    }
+
+    // compute the global BDDs of the latches
+    dd = Abc_NtkGlobalBdds( pNtk, 1 );    
+    if ( dd == NULL )
+        return 0;
+    if ( fVerbose )
+        printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+    // create the transition relation (dereferenced global BDDs)
+    bRelation = Abc_NtkTransitionRelation( dd, pNtk, fVerbose );              Cudd_Ref( bRelation );
+    // create the initial state and the variable map
+    bInitial  = Abc_NtkInitStateAndVarMap( dd, pNtk, fVerbose );              Cudd_Ref( bInitial );
+    // compute the unreachable states
+    bUnreach  = Abc_NtkComputeUnreachable( dd, pNtk, bRelation, bInitial, fVerbose );   Cudd_Ref( bUnreach );
+    Cudd_RecursiveDeref( dd, bRelation );
+    Cudd_RecursiveDeref( dd, bInitial );
+
+    // reorder and disable reordering
+    if ( fReorder )
+    {
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the unreachable states before reordering %d.\n", Cudd_DagSize(bUnreach) );
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
+        Cudd_AutodynDisable( dd );
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the unreachable states after reordering %d.\n", Cudd_DagSize(bUnreach) );
+    }
+
+    // allocate ZDD variables
+    Cudd_zddVarsFromBddVars( dd, 2 );
+    // create the EXDC network representing the unreachable states
+    pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach );
+    Cudd_RecursiveDeref( dd, bUnreach );
+    Extra_StopManager( dd );
+
+    // make sure that everything is okay
+    if ( fCheck && !Abc_NtkCheck( pNtk->pExdc ) )
+    {
+        printf( "Abc_NtkExtractSequentialDcs: The network check has failed.\n" );
+        Abc_NtkDelete( pNtk->pExdc );
+        return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the transition relation of the network.]
+
+  Description [Assumes that the global BDDs are computed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkTransitionRelation( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
+{
+    DdNode * bRel, * bTemp, * bProd, * bVar, * bInputs;
+    Abc_Obj_t * pNode;
+    int fReorder = 1;
+    int i;
+
+    // extand the BDD manager to represent NS variables
+    assert( dd->size == Abc_NtkCiNum(pNtk) );
+    Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 );
+
+    // enable reordering
+    if ( fReorder )
+        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    else
+        Cudd_AutodynDisable( dd );
+
+    // compute the transition relation
+    bRel = b1;   Cudd_Ref( bRel );
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+    {
+        bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
+        bProd = Cudd_bddXnor( dd, bVar, (DdNode *)pNode->pNext );   Cudd_Ref( bProd );
+        bRel  = Cudd_bddAnd( dd, bTemp = bRel, bProd );             Cudd_Ref( bRel );
+        Cudd_RecursiveDeref( dd, bTemp ); 
+        Cudd_RecursiveDeref( dd, bProd ); 
+    }
+    // free the global BDDs
+    Abc_NtkFreeGlobalBdds( dd, pNtk );
+
+    // quantify the PI variables
+    bInputs = Extra_bddComputeRangeCube( dd, 0, Abc_NtkPiNum(pNtk) );    Cudd_Ref( bInputs );
+    bRel    = Cudd_bddExistAbstract( dd, bTemp = bRel, bInputs );    Cudd_Ref( bRel );
+    Cudd_RecursiveDeref( dd, bTemp ); 
+    Cudd_RecursiveDeref( dd, bInputs ); 
+
+    // reorder and disable reordering
+    if ( fReorder )
+    {
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the transition relation before reordering %d.\n", Cudd_DagSize(bRel) );
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+        Cudd_AutodynDisable( dd );
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the transition relation after reordering %d.\n", Cudd_DagSize(bRel) );
+    }
+    Cudd_Deref( bRel );
+    return bRel;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the initial state and sets up the variable map.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkInitStateAndVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
+{
+    DdNode ** pbVarsX, ** pbVarsY;
+    DdNode * bTemp, * bProd, * bVar;
+    Abc_Obj_t * pLatch;
+    int i;
+
+    // set the variable mapping for Cudd_bddVarMap()
+    pbVarsX = ALLOC( DdNode *, dd->size );
+    pbVarsY = ALLOC( DdNode *, dd->size );
+    bProd = b1;         Cudd_Ref( bProd );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];
+        pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
+        // get the initial value of the latch
+        bVar  = Cudd_NotCond( pbVarsX[i], (((int)pLatch->pData) != 1) );
+        bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar );      Cudd_Ref( bProd );
+        Cudd_RecursiveDeref( dd, bTemp ); 
+    }
+    Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
+    FREE( pbVarsX );
+    FREE( pbVarsY );
+
+    Cudd_Deref( bProd );
+    return bProd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the set of unreachable states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bTrans, DdNode * bInitial, bool fVerbose )
+{
+    DdNode * bRelation, * bReached, * bCubeCs;
+    DdNode * bCurrent, * bNext, * bTemp;
+    int nIters;
+
+    // perform reachability analisys
+    bCurrent  = bInitial;   Cudd_Ref( bCurrent );
+    bReached  = bInitial;   Cudd_Ref( bReached );
+    bRelation = bTrans;     Cudd_Ref( bRelation );
+    bCubeCs   = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) );    Cudd_Ref( bCubeCs );
+    for ( nIters = 1; ; nIters++ )
+    {
+        // compute the next states
+        bNext = Cudd_bddAndAbstract( dd, bRelation, bCurrent, bCubeCs );  Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( dd, bCurrent );
+        // remap these states into the current state vars
+        bNext = Cudd_bddVarMap( dd, bTemp = bNext );                      Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( dd, bTemp );
+        // check if there are any new states
+        if ( Cudd_bddLeq( dd, bNext, bReached ) )
+            break;
+        // get the new states
+        bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );          Cudd_Ref( bCurrent );
+        // minimize the new states with the reached states
+//        bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
+//        Cudd_RecursiveDeref( dd, bTemp );
+        // add to the reached states
+        bReached = Cudd_bddOr( dd, bTemp = bReached, bNext );             Cudd_Ref( bReached );
+        Cudd_RecursiveDeref( dd, bTemp );
+        Cudd_RecursiveDeref( dd, bNext );
+        // minimize the transition relation
+//        bRelation = Cudd_bddConstrain( dd, bTemp = bRelation, Cudd_Not(bReached) ); Cudd_Ref( bRelation );
+//        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Cudd_RecursiveDeref( dd, bRelation );
+    Cudd_RecursiveDeref( dd, bCubeCs );
+    Cudd_RecursiveDeref( dd, bNext );
+    // report the stats
+    if ( fVerbose )
+    {
+    fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
+    fprintf( stdout, "The number of minterms in the reachable state set = %d.\n", 
+                        (int)Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) ) ); 
+    }
+//PRB( dd, bReached );
+    Cudd_Deref( bReached );
+    return Cudd_Not( bReached );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the EXDC network.]
+
+  Description [The set of unreachable states depends on CS variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach )
+{
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pNodeNew;
+    int * pPermute;
+    int i;
+
+    // start the new network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC_BDD );
+    // create PIs corresponding to LOs
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        pNode->pCopy = Abc_NtkCreateTermPi(pNtkNew);
+
+    // create a new node
+    pNodeNew = Abc_NtkCreateNode(pNtkNew);
+    // add the fanins corresponding to latch outputs
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
+
+    // create the logic function
+    pPermute = ALLOC( int, dd->size );
+    for ( i = 0; i < dd->size; i++ )
+        pPermute[i] = -1;
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        pPermute[Abc_NtkPiNum(pNtk) + i] = i;
+    // remap the functions
+    pNodeNew->pData = Extra_TransferPermute( dd, pNtkNew->pManFunc, bUnreach, pPermute );   Cudd_Ref( pNodeNew->pData );
+    free( pPermute );
+    Abc_NodeMinimumBase( pNodeNew );
+
+    // make the new node drive all the COs
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_ObjAddFanin( Abc_NtkCreateTermPo(pNtkNew), pNodeNew );
+
+    // copy the CI/CO names
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        Abc_NtkLogicStoreName( pNtkNew->vPis->pArray[i], Abc_NtkNameLatch(pNtk, i) );
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        Abc_NtkLogicStoreName( pNtkNew->vPos->pArray[i], Abc_NtkNamePo(pNtk, i) );
+    Abc_NtkForEachLatch( pNtk, pNode, i )
+        Abc_NtkLogicStoreName( pNtkNew->vPos->pArray[Abc_NtkPoNum(pNtk) + i], Abc_NtkNameLatchInput(pNtk, i) );
+
+    // transform the network to the SOP representation
+    Abc_NtkBddToSop( pNtkNew );
+    return pNtkNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+

src/base/abc/abcUtil.c

@@ -777,6 +777,47 @@ Vec_Ptr_t * Abc_AigCollectAll( Abc_Ntk_t * pNtk )
     return vNodes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Gets fanin node names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pFanin;
+    int i;
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        Vec_PtrPush( vNodes, util_strsav(Abc_ObjName(pFanin)) );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gets fanin node names.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeFreeFaninNames( Vec_Ptr_t * vNames )
+{
+    int i;
+    for ( i = 0; i < vNames->nSize; i++ )
+        free( vNames->pArray[i] );
+    Vec_PtrFree( vNames );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/base/abc/module.make

@@ -10,6 +10,7 @@ SRC +=    src/base/abc/abc.c \
     src/base/abc/abcFpga.c \
     src/base/abc/abcFraig.c \
     src/base/abc/abcFunc.c \
+        src/base/abc/abcFxu.c \
     src/base/abc/abcLatch.c \
     src/base/abc/abcMap.c \
     src/base/abc/abcMinBase.c \
@@ -19,10 +20,13 @@ SRC +=    src/base/abc/abc.c \
     src/base/abc/abcPrint.c \
     src/base/abc/abcRefs.c \
     src/base/abc/abcRenode.c \
+    src/base/abc/abcRes.c \
     src/base/abc/abcSat.c \
+    src/base/abc/abcShow.c \
     src/base/abc/abcSop.c \
     src/base/abc/abcStrash.c \
     src/base/abc/abcSweep.c \
     src/base/abc/abcTiming.c \
+    src/base/abc/abcUnreach.c \
     src/base/abc/abcUtil.c \
     src/base/abc/abcVerify.c 

src/base/io/ioReadBlif.c

@@ -88,7 +88,7 @@ Abc_Ntk_t * Io_ReadBlif( char * pFileName, int fCheck )
         Io_ReadBlifFree( p );
         return NULL;
     }
-    Abc_NtkTimeFinalize( pNtk );
+    Abc_NtkTimeInitialize( pNtk );
 
     // read the EXDC network
     if ( p->fParsingExdc )

src/base/main/main.h

@@ -84,6 +84,7 @@ extern void            Abc_FrameRestart( Abc_Frame_t * p );
 extern void            Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
 extern void            Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p );
 extern void            Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet );
+extern void            Abc_FrameUnmapAllNetworks( Abc_Frame_t * p );
 extern void            Abc_FrameDeleteAllNetworks( Abc_Frame_t * p );
 
 extern void               Abc_FrameSetGlobalFrame( Abc_Frame_t * p );

src/base/main/mainFrame.c

@@ -205,19 +205,19 @@ bool Abc_FrameSetMode( Abc_Frame_t * p, bool fNameMode )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNetNew )
+void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtkNew )
 {
-    Abc_Ntk_t * pNet, * pNet2, * pNet3;
+    Abc_Ntk_t * pNtk, * pNtk2, * pNtk3;
     int nNetsPresent;
     int nNetsToSave;
     char * pValue;
 
     // link it to the previous network
-    Abc_NtkSetBackup( pNetNew, p->pNtkCur );
+    Abc_NtkSetBackup( pNtkNew, p->pNtkCur );
     // set the step of this network
-    Abc_NtkSetStep( pNetNew, ++p->nSteps );
+    Abc_NtkSetStep( pNtkNew, ++p->nSteps );
     // set this network to be the current network
-    p->pNtkCur = pNetNew;
+    p->pNtkCur = pNtkNew;
 
     // remove any extra network that may happen to be in the stack
     pValue = Cmd_FlagReadByName( p, "savesteps" );
@@ -229,20 +229,20 @@ void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNetNew )
     
     // count the network, remember the last one, and the one before the last one
     nNetsPresent = 0;
-    pNet2 = pNet3 = NULL;
-    for ( pNet = p->pNtkCur; pNet; pNet = Abc_NtkBackup(pNet2) )
+    pNtk2 = pNtk3 = NULL;
+    for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk2) )
     {
         nNetsPresent++;
-        pNet3 = pNet2;
-        pNet2 = pNet;
+        pNtk3 = pNtk2;
+        pNtk2 = pNtk;
     }
 
     // remove the earliest backup network if it is more steps away than we store
     if ( nNetsPresent - 1 > nNetsToSave )
     { // delete the last network
-        Abc_NtkDelete( pNet2 );
+        Abc_NtkDelete( pNtk2 );
         // clean the pointer of the network before the last one
-        Abc_NtkSetBackup( pNet3, NULL );
+        Abc_NtkSetBackup( pNtk3, NULL );
     }
 }
 
@@ -259,31 +259,31 @@ void Abc_FrameSetCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNetNew )
 ***********************************************************************/
 void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p )
 {
-    Abc_Ntk_t * pNtkCur, * pNetBack, * pNetBack2;
+    Abc_Ntk_t * pNtkCur, * pNtkBack, * pNtkBack2;
     int iStepCur, iStepBack;
 
     pNtkCur  = p->pNtkCur;
-    pNetBack = Abc_NtkBackup( pNtkCur );
+    pNtkBack = Abc_NtkBackup( pNtkCur );
     iStepCur = Abc_NtkStep  ( pNtkCur );
 
     // if there is no backup nothing to reset
-    if ( pNetBack == NULL )
+    if ( pNtkBack == NULL )
         return;
 
     // remember the backup of the backup
-    pNetBack2 = Abc_NtkBackup( pNetBack );
-    iStepBack = Abc_NtkStep  ( pNetBack );
+    pNtkBack2 = Abc_NtkBackup( pNtkBack );
+    iStepBack = Abc_NtkStep  ( pNtkBack );
 
     // set pNtkCur to be the next after the backup's backup
-    Abc_NtkSetBackup( pNtkCur, pNetBack2 );
+    Abc_NtkSetBackup( pNtkCur, pNtkBack2 );
     Abc_NtkSetStep  ( pNtkCur, iStepBack );
 
     // set pNtkCur to be the next after the backup
-    Abc_NtkSetBackup( pNetBack, pNtkCur );
-    Abc_NtkSetStep  ( pNetBack, iStepCur );
+    Abc_NtkSetBackup( pNtkBack, pNtkCur );
+    Abc_NtkSetStep  ( pNtkBack, iStepCur );
 
     // set the current network
-    p->pNtkCur = pNetBack;
+    p->pNtkCur = pNtkBack;
 }
 
 
@@ -299,26 +299,45 @@ void Abc_FrameSwapCurrentAndBackup( Abc_Frame_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet )
+void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNtk )
 {
-    if ( pNet == NULL )
+    if ( pNtk == NULL )
         return;
 
     // transfer the parameters to the new network
     if ( p->pNtkCur )
     {
-        Abc_NtkSetBackup( pNet, Abc_NtkBackup(p->pNtkCur) );
-        Abc_NtkSetStep( pNet, Abc_NtkStep(p->pNtkCur) );
+        Abc_NtkSetBackup( pNtk, Abc_NtkBackup(p->pNtkCur) );
+        Abc_NtkSetStep( pNtk, Abc_NtkStep(p->pNtkCur) );
         // delete the current network
         Abc_NtkDelete( p->pNtkCur );
     }
     else
     {
-        Abc_NtkSetBackup( pNet, NULL );
-        Abc_NtkSetStep( pNet, ++p->nSteps );
+        Abc_NtkSetBackup( pNtk, NULL );
+        Abc_NtkSetStep( pNtk, ++p->nSteps );
     }
     // set the new current network
-    p->pNtkCur = pNet;
+    p->pNtkCur = pNtk;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes library binding of all currently stored networks.]
+
+  Description [This procedure is called when the library is freed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FrameUnmapAllNetworks( Abc_Frame_t * p )
+{
+    Abc_Ntk_t * pNtk;
+    for ( pNtk = p->pNtkCur; pNtk; pNtk = Abc_NtkBackup(pNtk) )
+        if ( Abc_NtkIsLogicMap(pNtk) )
+            Abc_NtkUnmap( pNtk );
 }
 
 /**Function*************************************************************
@@ -334,14 +353,14 @@ void Abc_FrameReplaceCurrentNetwork( Abc_Frame_t * p, Abc_Ntk_t * pNet )
 ***********************************************************************/
 void Abc_FrameDeleteAllNetworks( Abc_Frame_t * p )
 {
-    Abc_Ntk_t * pNet, * pNet2;
+    Abc_Ntk_t * pNtk, * pNtk2;
     // delete all the currently saved networks
-    for ( pNet  = p->pNtkCur, 
-          pNet2 = pNet? Abc_NtkBackup(pNet): NULL; 
-          pNet; 
-          pNet  = pNet2, 
-          pNet2 = pNet? Abc_NtkBackup(pNet): NULL )
-        Abc_NtkDelete( pNet );
+    for ( pNtk  = p->pNtkCur, 
+          pNtk2 = pNtk? Abc_NtkBackup(pNtk): NULL; 
+          pNtk; 
+          pNtk  = pNtk2, 
+          pNtk2 = pNtk? Abc_NtkBackup(pNtk): NULL )
+        Abc_NtkDelete( pNtk );
     // set the current network empty
     p->pNtkCur = NULL;
     fprintf( p->Out, "All networks have been deleted.\n" );

src/bdd/dsd/dsd.h

@@ -88,6 +88,7 @@ extern Dsd_Node_t *    Dsd_NodeReadDec ( Dsd_Node_t * p, int i );
 extern int             Dsd_NodeReadDecsNum( Dsd_Node_t * p );
 extern int             Dsd_NodeReadMark( Dsd_Node_t * p );
 extern void            Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ); 
+extern DdManager *     Dsd_ManagerReadDd( Dsd_Manager_t * pMan );
 extern Dsd_Node_t *    Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i );
 extern Dsd_Node_t *    Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i );
 /*=== dsdMan.c =======================================================*/
@@ -95,6 +96,7 @@ extern Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerb
 extern void            Dsd_ManagerStop( Dsd_Manager_t * dMan );
 /*=== dsdProc.c =======================================================*/
 extern void            Dsd_Decompose( Dsd_Manager_t * dMan, DdNode ** pbFuncs, int nFuncs );
+extern Dsd_Node_t *    Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc );
 /*=== dsdTree.c =======================================================*/
 extern void            Dsd_TreeNodeGetInfo( Dsd_Manager_t * dMan, int * DepthMax, int * GateSizeMax );
 extern void            Dsd_TreeNodeGetInfoOne( Dsd_Node_t * pNode, int * DepthMax, int * GateSizeMax );
@@ -104,6 +106,7 @@ extern int             Dsd_TreeCountPrimeNodes( Dsd_Manager_t * pDsdMan );
 extern int             Dsd_TreeCountPrimeNodesOne( Dsd_Node_t * pRoot );
 extern int             Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * dMan, int * pVars );
 extern Dsd_Node_t **   Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNodes );
+extern Dsd_Node_t **   Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes );
 extern void            Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output );
 /*=== dsdLocal.c =======================================================*/
 extern DdNode *        Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode );

src/bdd/dsd/dsdApi.c

@@ -89,6 +89,7 @@ void          Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark;     }
 ***********************************************************************/
 Dsd_Node_t *  Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i )  { return pMan->pRoots[i];  } 
 Dsd_Node_t *  Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ) { return pMan->pInputs[i]; } 
+DdManager *   Dsd_ManagerReadDd( Dsd_Manager_t * pMan )           { return pMan->dd;         } 
 
 ////////////////////////////////////////////////////////////////////////
 ///                           END OF FILE                            ///

src/bdd/dsd/dsdInt.h

@@ -61,6 +61,8 @@ struct Dsd_Node_t_
 ///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
+#define MAXINPUTS 1000
+
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////

src/bdd/dsd/dsdProc.c

@@ -225,6 +225,22 @@ s_Loops2Useless = 0;
 
 /**Function*************************************************************
 
+  Synopsis    [Performs decomposition for one function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dsd_Node_t * Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc )
+{
+    return dsdKernelDecompose_rec( pDsdMan, bFunc );
+}
+
+/**Function*************************************************************
+
   Synopsis    [The main function of this module. Recursive implementation of DSD.]
 
   Description []
@@ -1053,7 +1069,7 @@ if ( s_Show )
                     // go through the decomposition list of pPrev and find components 
                     // whose support does not overlap with supp(Lower) 
 
-                    Dsd_Node_t ** pNonOverlap = ALLOC( Dsd_Node_t *, dd->size );
+                    static Dsd_Node_t * pNonOverlap[MAXINPUTS];
                     int i, nNonOverlap = 0;
                     for ( i = 0; i < pPrev->nDecs; i++ )
                     {
@@ -1089,7 +1105,6 @@ if ( s_Show )
                         // assign the support to be subtracted from both components
                         bSuppSubract = pDENew->S;
                     }
-                    free( pNonOverlap );
                 }
                 
                 // subtract its support from the support of upper component
@@ -1106,8 +1121,8 @@ if ( s_Show )
             } // end of if ( !fEqualLevel )
             else // if ( fEqualLevel ) -- they have the same top level var
             {
-                Dsd_Node_t ** pMarkedLeft = ALLOC( Dsd_Node_t *, dd->size ); // the pointers to the marked blocks
-                char * pMarkedPols = ALLOC( char, dd->size );                // polarities of the marked blocks
+                static Dsd_Node_t * pMarkedLeft[MAXINPUTS]; // the pointers to the marked blocks
+                static char pMarkedPols[MAXINPUTS]; // polarities of the marked blocks
                 int nMarkedLeft = 0;
 
                 int fPolarity = 0;
@@ -1198,9 +1213,6 @@ if ( s_Show )
                 SuppH = Cudd_bddExistAbstract( dd, bTemp = SuppH, bSuppSubract ), Cudd_Ref( SuppH );
                 Cudd_RecursiveDeref(dd, bTemp);
 
-                free( pMarkedLeft );
-                free( pMarkedPols );
-
             } // end of if ( fEqualLevel ) 
 
         } // end of decomposition list comparison
@@ -1333,7 +1345,7 @@ Dsd_Node_t * dsdKernelFindContainingComponent( Dsd_Manager_t * pDsdMan, Dsd_Node
 ***********************************************************************/
 int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd_Node_t * pH, Dsd_Node_t *** pCommon, Dsd_Node_t ** pLastDiffL, Dsd_Node_t ** pLastDiffH )
 {
-    Dsd_Node_t ** Common = ALLOC( Dsd_Node_t *, pDsdMan->dd->size );
+    static Dsd_Node_t * Common[MAXINPUTS];
     int nCommon = 0;
 
     // pointers to the current decomposition entries
@@ -1402,7 +1414,6 @@ int dsdKernelFindCommonComponents( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pL, Dsd
     // return the pointer to the array
     *pCommon = Common;
     // return the number of common components
-    free( Common );
     return nCommon;            
 }
 
@@ -1567,7 +1578,7 @@ int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE )
     else if ( pR->Type == DSD_NODE_PRIME )
     {
         int i;
-        DdNode ** bGVars = ALLOC( DdNode *, dd->size );
+        static DdNode * bGVars[MAXINPUTS];
         // transform the function of this block, so that it depended on inputs
         // corresponding to the formal inputs
         DdNode * bNewFunc = Dsd_TreeGetPrimeFunctionOld( dd, pR, 1 );  Cudd_Ref( bNewFunc );
@@ -1589,7 +1600,6 @@ int dsdKernelVerifyDecomposition( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pDE )
         RetValue = (int)( bRes == pR->G );//|| bRes == Cudd_Not(pR->G) );
         /////////////////////////////////////////////////////////
         Cudd_Deref( bRes );
-        free( bGVars );
     }
     else
     {

src/bdd/dsd/dsdTree.c

@@ -517,6 +517,33 @@ Dsd_Node_t ** Dsd_TreeCollectNodesDfs( Dsd_Manager_t * pDsdMan, int * pnNodes )
     return ppNodes;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates the DFS ordered array of DSD nodes in the tree.]
+
+  Description [The collected nodes do not include the terminal nodes
+  and the constant 1 node. The array of nodes is returned. The number
+  of entries in the array is returned in the variale pnNodes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dsd_Node_t ** Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes )
+{
+    Dsd_Node_t ** ppNodes;
+    int nNodes, nNodesAlloc;
+    nNodesAlloc = Dsd_TreeCountNonTerminalNodesOne(pNode);
+    nNodes  = 0;
+    ppNodes = ALLOC( Dsd_Node_t *, nNodesAlloc );
+    Dsd_TreeCollectNodesDfs_rec( Dsd_Regular(pNode), ppNodes, &nNodes );
+    Dsd_TreeUnmark_rec(Dsd_Regular(pNode));
+    assert( nNodesAlloc == nNodes );
+    *pnNodes = nNodes;
+    return ppNodes;
+}
+
 
 /**Function*************************************************************
 
@@ -777,9 +804,7 @@ DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fR
     DdNode * bCof0,  * bCof1, * bCube0, * bCube1, * bNewFunc, * bTemp;
     int i;
     int fAllBuffs = 1;
-    int * pPermute;
-
-    pPermute = ALLOC( int, dd->size );
+    static int Permute[MAXINPUTS];
 
     assert( pNode );
     assert( !Dsd_IsComplement( pNode ) );
@@ -821,14 +846,13 @@ DdNode * Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fR
         // remap the function to the first variables of the manager
         for ( i = 0; i < pNode->nDecs; i++ )
     //        Permute[ pNode->pDecs[i]->S->index ] = dd->invperm[i];
-            pPermute[ pNode->pDecs[i]->S->index ] = i;
+            Permute[ pNode->pDecs[i]->S->index ] = i;
 
-        bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, pPermute );   Cudd_Ref( bNewFunc );
+        bNewFunc = Cudd_bddPermute( dd, bTemp = bNewFunc, Permute );   Cudd_Ref( bNewFunc );
         Cudd_RecursiveDeref( dd, bTemp );
     }
 
     Cudd_Deref( bNewFunc );
-    free( pPermute );
     return bNewFunc;
 }
 

src/map/fpga/fpgaCreate.c

@@ -172,7 +172,7 @@ Fpga_Man_t * Fpga_ManCreate( int nInputs, int nOutputs, int fVerbose )
     p->fAreaRecovery = 1;
     p->fTree     = 0;
     p->fRefCount = 1;
-    p->fEpsilon  = (float)0.00001;
+    p->fEpsilon  = (float)0.001;
 
     Fpga_TableCreate( p );
 //if ( p->fVerbose )

src/map/mapper/mapperCreate.c

@@ -193,7 +193,6 @@ Map_Man_t * Map_ManCreate( int nInputs, int nOutputs, int fVerbose )
     p->pSuperLib = Abc_FrameReadLibSuper(Abc_FrameGetGlobalFrame());
     p->nVarsMax  = p->pSuperLib->nVarsMax;
     p->fVerbose  = fVerbose;
-//    p->fEpsilon  = (float)0.00001;
     p->fEpsilon  = (float)0.001;
     assert( p->nVarsMax > 0 );
 

src/map/mio/mioFunc.c

@@ -213,7 +213,7 @@ int Mio_GateParseFormula( Mio_Gate_t * pGate )
     Cudd_Ref( pGate->bFunc );
 
     // derive the cover (SOP)
-    pGate->pSop = Abc_ConvertBddToSop( pGate->pLib->pMmFlex, dd, pGate->bFunc, nPins, pGate->pLib->vCube, -1 );
+    pGate->pSop = Abc_ConvertBddToSop( pGate->pLib->pMmFlex, dd, pGate->bFunc, pGate->bFunc, nPins, pGate->pLib->vCube, -1 );
     return 0;
 }
 

src/map/mio/mioUtils.c

@@ -48,7 +48,7 @@ void Mio_LibraryDelete( Mio_Library_t * pLib )
     if ( pLib == NULL )
         return;
     // free the bindings of nodes to gates from this library for all networks
-//    Mv_FrameFreeNetworkBindings( Mv_FrameGetGlobalFrame() );
+    Abc_FrameUnmapAllNetworks( Abc_FrameGetGlobalFrame() );
     // free the library
     FREE( pLib->pName );
     Mio_LibraryForEachGateSafe( pLib, pGate, pGate2 )

src/misc/extra/extra.h

@@ -111,6 +111,7 @@ extern int *        Extra_SupportArray( DdManager * dd, DdNode * F, int * suppor
 extern int *        Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n, int * support );
 extern DdNode *     Extra_bddFindOneCube( DdManager * dd, DdNode * bF );
 extern DdNode *     Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc );
+extern DdNode *     Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
 
 /*=== extraUtilFile.c ========================================================*/
 

src/misc/extra/extraUtilBdd.c

@@ -656,6 +656,34 @@ DdNode * Extra_bddGetOneCube( DdManager * dd, DdNode * bFunc )
     return bRes;
 }
 
+/**Function********************************************************************
+
+  Synopsis    [Performs the reordering-sensitive step of Extra_bddMove().]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop )
+{
+    DdNode * bTemp, * bProd;
+    int i;
+    assert( iStart <= iStop );
+    assert( iStart >= 0 && iStart <= dd->size );
+    assert( iStop >= 0  && iStop  <= dd->size );
+    bProd = b1;         Cudd_Ref( bProd );
+    for ( i = iStart; i < iStop; i++ )
+    {
+        bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] );      Cudd_Ref( bProd );
+        Cudd_RecursiveDeref( dd, bTemp ); 
+    }
+    Cudd_Deref( bProd );
+    return bProd;
+}
+
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/

src/misc/vec/vecFan.h

@@ -57,6 +57,8 @@ struct Vec_Fan_t_
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
+#define Vec_FanForEachEntry( vVec, Entry, i )                                               \
+    for ( i = 0; (i < Vec_FanSize(vVec)) && (((Entry) = Vec_FanEntry(vVec, i)), 1); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///

src/misc/vec/vecInt.h

@@ -48,6 +48,9 @@ struct Vec_Int_t_
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
+#define Vec_IntForEachEntry( vVec, Entry, i )                                               \
+    for ( i = 0; (i < Vec_IntSize(vVec)) && (((Entry) = Vec_IntEntry(vVec, i)), 1); i++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////

src/misc/vec/vecPtr.h

@@ -48,6 +48,9 @@ struct Vec_Ptr_t_
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
+#define Vec_PtrForEachEntry( vVec, pEntry, i )                                               \
+    for ( i = 0; (i < Vec_PtrSize(vVec)) && (((pEntry) = Vec_PtrEntry(vVec, i)), 1); i++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -418,6 +421,29 @@ static inline void * Vec_PtrPop( Vec_Ptr_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_PtrRemove( Vec_Ptr_t * p, void * Entry )
+{
+    int i;
+    for ( i = 0; i < p->nSize; i++ )
+        if ( p->pArray[i] == Entry )
+            break;
+    assert( i < p->nSize );
+    for ( i++; i < p->nSize; i++ )
+        p->pArray[i-1] = p->pArray[i];
+    p->nSize--;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Moves the first nItems to the end.]
 
   Description []

src/misc/vec/vecStr.h

@@ -48,6 +48,9 @@ struct Vec_Str_t_
 ///                      MACRO DEFITIONS                             ///
 ////////////////////////////////////////////////////////////////////////
 
+#define Vec_StrForEachEntry( vVec, Entry, i )                                               \
+    for ( i = 0; (i < Vec_StrSize(vVec)) && (((Entry) = Vec_StrEntry(vVec, i)), 1); i++ )   
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////

src/opt/fxu/fxu.c

@@ -39,21 +39,14 @@ static int s_MemoryPeak;
 
   Synopsis    [Performs fast_extract on a set of covers.]
 
-  Description [All the covers are given in the array p->ppCovers. 
-  The resulting covers are returned in the array p->ppCoversNew.
-  The number of entries in both cover arrays is equal to the number
-  of all values in the current nodes plus the max expected number 
-  of extracted nodes (p->nValuesCi + p->nValuesInt + p->nValuesExtMax). 
-  The first p->nValuesCi entries, corresponding to the CI nodes, are NULL.
-  The next p->nValuesInt entries, corresponding to the int nodes, are covers
-  from which the divisors are extracted. The last p->nValuesExtMax entries  
-  are reserved for the new covers to be extracted. The number of extracted 
-  covers is returned. This number does not exceed the given number (p->nNodesExt). 
+  Description [All the covers are given in the array p->vSops. 
+  The resulting covers are returned in the array p->vSopsNew.
+  The entries in these arrays correspond to objects in the network.
+  The entries corresponding to the PI and objects with trivial covers are NULL.
+  The number of extracted covers (not exceeding p->nNodesExt) is returned. 
   Two other things are important for the correct operation of this procedure:
-  (1) The input covers should be SCC-free. (2) The literal array (pCover->pLits) 
-  is allocated in each cover. The i-th entry in the literal array of a cover
-  is the number of the cover in the array p->ppCovers, which represents this
-  literal (variable value) in the given cover.]
+  (1) The input covers do not have duplicated fanins and are SCC-free. 
+  (2) The fanins array contains the numbers of the fanin objects.]
                
   SideEffects []
 

src/opt/fxu/fxu.h

@@ -48,37 +48,8 @@ struct FxuDataStruct
     bool              fUse0;            // set to 1 to have 0-weight also extracted
     bool              fUseCompl;        // set to 1 to have complement taken into account
     bool              fVerbose;         // set to 1 to have verbose output
-    int               nPairsMax;        // the maximum number of cube pairs to consider
-/*
-    // parameters of the network
-    int               fMvNetwork;       // the network has some MV nodes
-    // the information about nodes
-    int               nNodesCi;         // the number of CI nodes of the network
-    int               nNodesInt;        // the number of internal nodes of the network
-    int               nNodesOld;        // the number of CI and int nodes
-    int               nNodesNew;        // the number of added nodes
-    int               nNodesExt;        // the max number of (binary) nodes to be added by FX
-    int               nNodesAlloc;      // the total number of all nodes
-    int *             pNode2Value;      // for each node, the number of its first value
-    // the information about values
-    int               nValuesCi;        // the total number of values of CI nodes
-    int               nValuesInt;       // the total number of values of int nodes
-    int               nValuesOld;       // the number of CI and int values
-    int               nValuesNew;       // the number of values added nodes
-    int               nValuesExt;       // the total number of values of the added nodes
-    int               nValuesAlloc;     // the total number of all values of all nodes
-    int *             pValue2Node;      // for each value, the number of its node
-    // the information about covers
-    Mvc_Cover_t **    ppCovers;         // for each value, the corresponding cover
-    Mvc_Cover_t **    ppCoversNew;      // for each value, the corresponding cover after FX
-    // the MVC manager
-    Mvc_Manager_t *   pManMvc;
-*/
-    // statistics   
-    int               nNodesOld;        // the old number of nodes
     int               nNodesExt;        // the number of divisors to extract
-    int               nNodesNew;        // the number of divisors extracted
-
+    int               nPairsMax;        // the maximum number of cube pairs to consider
     // the input information
     Vec_Ptr_t *       vSops;            // the SOPs for each node in the network
     Vec_Ptr_t *       vFanins;          // the fanins of each node in the network
@@ -87,6 +58,9 @@ struct FxuDataStruct
     Vec_Ptr_t *       vFaninsNew;       // the fanins of each node in the network after extraction
     // the SOP manager
     Extra_MmFlex_t *  pManSop;
+    // statistics   
+    int               nNodesOld;        // the old number of nodes
+    int               nNodesNew;        // the number of divisors actually extracted
 };
 
 ////////////////////////////////////////////////////////////////////////

src/opt/fxu/fxuCreate.c

@@ -24,21 +24,21 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern int         Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
-
 static void        Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube, Vec_Fan_t * vFanins, int * pOrder );
 static int         Fxu_CreateMatrixLitCompare( int * ptrX, int * ptrY );
 static void        Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext );
 static Fxu_Cube *  Fxu_CreateCoversFirstCube( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode );
 static Abc_Fan_t * s_pLits;
 
+extern int         Fxu_PreprocessCubePairs( Fxu_Matrix * p, Vec_Ptr_t * vCovers, int nPairsTotal, int nPairsMax );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Creates the sparse matrix from the array of Sop covers.]
+  Synopsis    [Creates the sparse matrix from the array of SOPs.]
 
   Description []
                
@@ -53,6 +53,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
     Fxu_Var * pVar;
     Fxu_Cube * pCubeFirst, * pCubeNew;
     Fxu_Cube * pCube1, * pCube2;
+    Vec_Fan_t * vFanins;
     char * pSopCover;
     char * pSopCube;
     int * pOrder, nBitsMax;
@@ -63,12 +64,11 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
     int nCubes;
     int iCube, iPair;
     int nFanins;
-    Vec_Fan_t * vFanins;
 
     // collect all sorts of statistics
-    nCubesTotal = 0;
-    nPairsTotal = 0;
-    nPairsStore = 0;
+    nCubesTotal =  0;
+    nPairsTotal =  0;
+    nPairsStore =  0;
     nBitsMax    = -1;
     for ( i = 0; i < pData->nNodesOld; i++ )
         if ( pSopCover = pData->vSops->pArray[i] )
@@ -158,12 +158,11 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
         Abc_SopForEachCube( pSopCover, nFanins, pSopCube )
         {
             // create the cube
-            pCubeNew = Fxu_MatrixAddCube( p, pVar, c );
+            pCubeNew = Fxu_MatrixAddCube( p, pVar, c++ );
             Fxu_CreateMatrixAddCube( p, pCubeNew, pSopCube, vFanins, pOrder );
             if ( pCubeFirst == NULL )
                 pCubeFirst = pCubeNew;
             pCubeNew->pFirst = pCubeFirst;
-            c++;
         }
         // set the first cube of this var
         pVar->pFirst = pCubeFirst;
@@ -185,10 +184,7 @@ Fxu_Matrix * Fxu_CreateMatrix( Fxu_Data_t * pData )
     // add the var pairs to the heap
     Fxu_MatrixComputeSingles( p );
 
-    // allocate temporary storage for pairs
-    if ( pData->nPairsMax < 1000 )
-        pData->nPairsMax = 1000;
-    p->pPairsTemp = ALLOC( Fxu_Pair *, pData->nPairsMax * 10 + 100 );
+    // print stats
     if ( pData->fVerbose )
     {
         double Density;
@@ -254,8 +250,8 @@ void Fxu_CreateMatrixAddCube( Fxu_Matrix * p, Fxu_Cube * pCube, char * pSopCube,
 void Fxu_CreateCovers( Fxu_Matrix * p, Fxu_Data_t * pData )
 {
     Fxu_Cube * pCube, * pCubeFirst, * pCubeNext;
-    int iNode, n;
     char * pSopCover;
+    int iNode, n;
 
     // get the first cube of the first internal node 
     pCubeFirst = Fxu_CreateCoversFirstCube( p, pData, 0 );
@@ -306,13 +302,11 @@ void Fxu_CreateCovers( Fxu_Matrix * p, Fxu_Data_t * pData )
 void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cube * pCubeFirst, Fxu_Cube * pCubeNext )
 {
     Vec_Int_t * vInputsNew;
-    char * pSopCover;
-    char * pSopCube;
+    char * pSopCover, * pSopCube;
     Fxu_Var * pVar;
     Fxu_Cube * pCube;
     Fxu_Lit * pLit;
     int iNum, nCubes, v;
-    int fEmptyCube;
 
     // collect positive polarity variable in the cubes between pCubeFirst and pCubeNext
     Fxu_MatrixRingVarsStart( p );
@@ -362,7 +356,6 @@ void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cu
         // get hold of the SOP cube
         pSopCube = pSopCover + nCubes * (vInputsNew->nSize + 3);
         // insert literals
-        fEmptyCube = 1;
         for ( pLit = pCube->lLits.pHead; pLit; pLit = pLit->pHNext )
         {
             iNum = pLit->pVar->lLits.nItems; // hack - reuse lLits.nItems
@@ -371,14 +364,13 @@ void Fxu_CreateCoversNode( Fxu_Matrix * p, Fxu_Data_t * pData, int iNode, Fxu_Cu
                 pSopCube[iNum] = (pLit->pVar->iVar & 1)? '0' : '1';   // reverse CST
             else
                 pSopCube[iNum] = (pLit->pVar->iVar & 1)? '1' : '0';   // no CST
-            fEmptyCube = 0;
         }
-        assert( !fEmptyCube );
         // count the cube
         nCubes++;
     }
     assert( nCubes == Abc_SopGetCubeNum(pSopCover) );
 
+    // set the new cover and the array of fanins
     pData->vSopsNew->pArray[iNode]   = pSopCover;
     pData->vFaninsNew->pArray[iNode] = vInputsNew;
 }

src/opt/fxu/fxuInt.h

@@ -25,6 +25,7 @@
 
 #include "util.h"
 #include "extra.h"
+#include "vec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -158,9 +159,6 @@ struct FxuHeapSingle
 // sparse matrix
 struct FxuMatrix // ~ 30 words
 {
-    // information about the network
-//    int              fMvNetwork;  // set to 1 if the network has MV nodes
-//    int *            pValue2Node; // the mapping of values into nodes
     // the cubes
     Fxu_ListCube     lCubes;      // the double linked list of cubes
     // the values (binary literals)
@@ -185,9 +183,7 @@ struct FxuMatrix // ~ 30 words
     Fxu_Var *        pOrderVars;
     Fxu_Var **       ppTailVars;
     // temporary storage for pairs
-    Fxu_Pair **      pPairsTemp;
-    int              nPairsTemp;
-//    int              nPairsMax;
+    Vec_Ptr_t *      vPairs;
     // statistics
     int              nEntries;    // the total number of entries in the sparse matrix
     int              nDivs1;      // the single cube divisors taken

src/opt/fxu/fxuMatrix.c

@@ -77,6 +77,7 @@ Fxu_Matrix * Fxu_MatrixAllocate()
 #endif
     p->pHeapDouble = Fxu_HeapDoubleStart();
     p->pHeapSingle = Fxu_HeapSingleStart();
+    p->vPairs = Vec_PtrAlloc( 100 );
     return p;
 }
 
@@ -132,9 +133,10 @@ void Fxu_MatrixDelete( Fxu_Matrix * p )
     Extra_MmFixedStop( p->pMemMan, 0 );
 #endif
 
+    Vec_PtrFree( p->vPairs );
     FREE( p->pppPairs );
     FREE( p->ppPairs );
-    FREE( p->pPairsTemp );
+//    FREE( p->pPairsTemp );
     FREE( p->pTable );
     FREE( p->ppVars );
     FREE( p );
@@ -305,20 +307,8 @@ void Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2
 
     // canonicize the pair
     Fxu_PairCanonicize( &pCube1, &pCube2 );
-
-/*
     // compute the hash key
-    if ( p->fMvNetwork )
-//    if ( 0 )
-    {   // in case of MV network, if all the values in the cube-free divisor
-        // belong to the same MV variable, this cube pair is not a divisor
-        Key = Fxu_PairHashKeyMv( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
-        if ( Key == 0 )
-            return;
-    }
-    else
-*/
-        Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
+    Key = Fxu_PairHashKey( p, pCube1, pCube2, &nBase, &nLits1, &nLits2 );
 
     // create the cube pair
     pPair = Fxu_PairAlloc( p, pCube1, pCube2 );
@@ -330,11 +320,13 @@ void Fxu_MatrixAddDivisor( Fxu_Matrix * p, Fxu_Cube * pCube1, Fxu_Cube * pCube2
     fFound = 0;
     Key %= p->nTableSize;
     Fxu_TableForEachDouble( p, Key, pDiv )
+    {
         if ( Fxu_PairCompare( pPair, pDiv->lPairs.pTail ) ) // they are equal
         {
             fFound = 1;
             break;
         }
+    }
 
     if ( !fFound )
     {   // create the new divisor

src/opt/fxu/fxuUpdate.c

@@ -287,10 +287,12 @@ void Fxu_UpdateDoublePairs( Fxu_Matrix * p, Fxu_Double * pDouble, Fxu_Var * pVar
 
     // collect and sort the pairs
     Fxu_UpdatePairsSort( p, pDouble );
-    for ( i = 0; i < p->nPairsTemp; i++ )
+//    for ( i = 0; i < p->nPairsTemp; i++ )
+    for ( i = 0; i < p->vPairs->nSize; i++ )
     {
         // get the pair
-        pPair = p->pPairsTemp[i];
+//        pPair = p->pPairsTemp[i];
+        pPair = p->vPairs->pArray[i];
         // out of the two cubes, select the one which comes earlier
         pCubeUse = Fxu_PairMinCube( pPair );
         pCubeRem = Fxu_PairMaxCube( pPair );
@@ -312,7 +314,7 @@ void Fxu_UpdateDoublePairs( Fxu_Matrix * p, Fxu_Double * pDouble, Fxu_Var * pVar
         // remove the pair
         MEM_FREE_FXU( p, Fxu_Pair, 1, pPair );
     }
-    p->nPairsTemp = 0;
+    p->vPairs->nSize = 0;
 }
 
 /**Function*************************************************************
@@ -575,18 +577,17 @@ void Fxu_UpdateMatrixSingleClean( Fxu_Matrix * p, Fxu_Var * pVar1, Fxu_Var * pVa
 void Fxu_UpdatePairsSort( Fxu_Matrix * p, Fxu_Double * pDouble )
 {
     Fxu_Pair * pPair;
-    // order the pairs by the first cube to ensure that 
-    // new literals are added to the matrix from top to bottom
-    // collect pairs into the array
-    p->nPairsTemp = 0;
+    // order the pairs by the first cube to ensure that new literals are added 
+    // to the matrix from top to bottom - collect pairs into the array
+    p->vPairs->nSize = 0;
     Fxu_DoubleForEachPair( pDouble, pPair )
-        p->pPairsTemp[ p->nPairsTemp++ ] = pPair;
-    if ( p->nPairsTemp > 1 )
-    {   // sort
-        qsort( (void *)p->pPairsTemp, p->nPairsTemp, sizeof(Fxu_Pair *), 
-            (int (*)(const void *, const void *)) Fxu_UpdatePairCompare );
-        assert( Fxu_UpdatePairCompare( p->pPairsTemp, p->pPairsTemp + p->nPairsTemp - 1 ) < 0 );
-    }
+        Vec_PtrPush( p->vPairs, pPair );
+    if ( p->vPairs->nSize < 2 )
+        return;
+    // sort
+    qsort( (void *)p->vPairs->pArray, p->vPairs->nSize, sizeof(Fxu_Pair *), 
+        (int (*)(const void *, const void *)) Fxu_UpdatePairCompare );
+    assert( Fxu_UpdatePairCompare( (Fxu_Pair**)p->vPairs->pArray, (Fxu_Pair**)p->vPairs->pArray + p->vPairs->nSize - 1 ) < 0 );
 }
 
 /**Function*************************************************************

src/opt/module.make

-SRC +=