Version abc51005

47 files changed, 3362 insertions, 122 deletions

diff --git a/Makefile b/Makefile
index 00c865f0..a38d33c5 100644
--- a/Makefile
+++ b/Makefile
@@ -21,7 +21,7 @@ OPTFLAGS  := -DNDEBUG -O3
 CFLAGS   += -Wall -Wno-unused-function $(OPTFLAGS) $(patsubst %, -I%, $(MODULES)) 
 CXXFLAGS += $(CFLAGS) 
 
-LIBS := 
+LIBS := -ldl -rdynamic
 SRC  := 
 GARBAGE := core core.* *.stackdump ./tags $(PROG)
 
diff --git a/abc.dsp b/abc.dsp
index f711f9fb..6e8c1623 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -262,6 +262,10 @@ SOURCE=.\src\base\abci\abcUnreach.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcVanEijk.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcVerify.c
 # End Source File
 # End Group
@@ -1474,6 +1478,10 @@ SOURCE=.\src\misc\extra\extra.h
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\misc\extra\extraBddKmap.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\misc\extra\extraBddMisc.c
 # End Source File
 # Begin Source File
diff --git a/abc.opt b/abc.opt
index a7bb1300..1ff22b1e 100644
--- a/abc.opt
+++ b/abc.opt
diff --git a/abc.plg b/abc.plg
index be2500c6..73e95bb8 100644
--- a/abc.plg
+++ b/abc.plg
@@ -6,13 +6,15 @@
 --------------------Configuration: abc - Win32 Release--------------------
 </h3>
 <h3>Command Lines</h3>
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC8D.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1362.tmp" with contents
 [
 /nologo /ML /W3 /GX /O2 /I "src\base\abc" /I "src\base\abci" /I "src\base\abcs" /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\ft" /I "src\sat\asat" /I "src\sat\msat" /I "src\sat\fraig" /I "src\opt\cut" /I "src\opt\dec" /I "src\opt\fxu" /I "src\opt\rwr" /I "src\map\fpga" /I "src\map\pga" /I "src\map\mapper" /I "src\map\mapp" /I "src\map\mio" /I "src\map\super" /I "src\misc\extra" /I "src\misc\st" /I "src\misc\mvc" /I "src\misc\util" /I "src\misc\npn" /I "src\misc\vec" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /D "HAVE_ASSERT_H" /FR"Release/" /Fp"Release/abc.pch" /YX /Fo"Release/" /Fd"Release/" /FD /c 
-"C:\_projects\abc\src\opt\cut\cutCut.c"
+"C:\_projects\abc\src\base\abci\abcFraig.c"
+"C:\_projects\abc\src\base\abci\abcVanEijk.c"
+"C:\_projects\abc\src\sat\fraig\fraigApi.c"
 ]
-Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC8D.tmp" 
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC8E.tmp" with contents
+Creating command line "cl.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1362.tmp" 
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1363.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:no /pdb:"Release/abc.pdb" /machine:I386 /out:"_TEST/abc.exe" 
 .\Release\abcAig.obj
@@ -54,7 +56,10 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\abcSymm.obj
 .\Release\abcTiming.obj
 .\Release\abcUnreach.obj
+.\Release\abcVanEijk.obj
 .\Release\abcVerify.obj
+.\Release\abcFpgaDelay.obj
+.\Release\abcFpgaSeq.obj
 .\Release\abcRetCore.obj
 .\Release\abcRetDelay.obj
 .\Release\abcRetImpl.obj
@@ -221,6 +226,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\cutMan.obj
 .\Release\cutMerge.obj
 .\Release\cutNode.obj
+.\Release\cutOracle.obj
 .\Release\cutSeq.obj
 .\Release\cutTruth.obj
 .\Release\decAbc.obj
@@ -281,6 +287,7 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\pgaMan.obj
 .\Release\pgaMatch.obj
 .\Release\pgaUtil.obj
+.\Release\extraBddKmap.obj
 .\Release\extraBddMisc.obj
 .\Release\extraBddSymm.obj
 .\Release\extraUtilBitMatrix.obj
@@ -320,16 +327,15 @@ kernel32.lib user32.lib gdi32.lib winspool.lib comdlg32.lib advapi32.lib shell32
 .\Release\npnGenStr.obj
 .\Release\npnTruth.obj
 .\Release\npnUtil.obj
-.\Release\abcFpgaSeq.obj
-.\Release\abcFpgaDelay.obj
-.\Release\cutOracle.obj
 ]
-Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC8E.tmp"
+Creating command line "link.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1363.tmp"
 <h3>Output Window</h3>
 Compiling...
-cutCut.c
+abcFraig.c
+abcVanEijk.c
+fraigApi.c
 Linking...
-Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC90.tmp" with contents
+Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1365.tmp" with contents
 [
 /nologo /o"Release/abc.bsc" 
 .\Release\abcAig.sbr
@@ -371,7 +377,10 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC90.tmp" with conte
 .\Release\abcSymm.sbr
 .\Release\abcTiming.sbr
 .\Release\abcUnreach.sbr
+.\Release\abcVanEijk.sbr
 .\Release\abcVerify.sbr
+.\Release\abcFpgaDelay.sbr
+.\Release\abcFpgaSeq.sbr
 .\Release\abcRetCore.sbr
 .\Release\abcRetDelay.sbr
 .\Release\abcRetImpl.sbr
@@ -538,6 +547,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC90.tmp" with conte
 .\Release\cutMan.sbr
 .\Release\cutMerge.sbr
 .\Release\cutNode.sbr
+.\Release\cutOracle.sbr
 .\Release\cutSeq.sbr
 .\Release\cutTruth.sbr
 .\Release\decAbc.sbr
@@ -598,6 +608,7 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC90.tmp" with conte
 .\Release\pgaMan.sbr
 .\Release\pgaMatch.sbr
 .\Release\pgaUtil.sbr
+.\Release\extraBddKmap.sbr
 .\Release\extraBddMisc.sbr
 .\Release\extraBddSymm.sbr
 .\Release\extraUtilBitMatrix.sbr
@@ -636,11 +647,8 @@ Creating temporary file "C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC90.tmp" with conte
 .\Release\npn.sbr
 .\Release\npnGenStr.sbr
 .\Release\npnTruth.sbr
-.\Release\npnUtil.sbr
-.\Release\abcFpgaSeq.sbr
-.\Release\abcFpgaDelay.sbr
-.\Release\cutOracle.sbr]
-Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSPC90.tmp"
+.\Release\npnUtil.sbr]
+Creating command line "bscmake.exe @C:\DOCUME~1\alanmi\LOCALS~1\Temp\RSP1365.tmp"
 Creating browse info file...
 <h3>Output Window</h3>
 
diff --git a/abc.rc b/abc.rc
index 736dc73d..209f060e 100644
--- a/abc.rc
+++ b/abc.rc
@@ -28,6 +28,7 @@ alias pf print_factor
 alias pfan print_fanio
 alias pl print_level
 alias pio print_io
+alias pk print_kmap
 alias ps print_stats 
 alias psu print_supp
 alias psy print_symm
@@ -49,6 +50,7 @@ alias sa set autoexec ps
 alias so source -x
 alias st strash
 alias sw sweep
+alias ssw seq_sweep
 alias u undo
 alias wb write_blif
 alias wl write_blif
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 64df9fc5..968dc596 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -419,12 +419,13 @@ extern Abc_Obj_t *        Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_
 extern Abc_Obj_t *        Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs );
 extern void               Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel );
 extern void               Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
+extern void               Abc_AigRehash( Abc_Aig_t * pMan );
 extern bool               Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
 extern bool               Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode );
 extern void               Abc_AigPrintNode( Abc_Obj_t * pNode );
 extern bool               Abc_AigNodeIsAcyclic( Abc_Obj_t * pNode, Abc_Obj_t * pRoot );
 extern void               Abc_AigCheckFaninOrder( Abc_Aig_t * pMan );
-extern void               Abc_AigRehash( Abc_Aig_t * pMan );
+extern void               Abc_AigSetNodePhases( Abc_Ntk_t * pNtk );
 /*=== abcAttach.c ==========================================================*/
 extern int                Abc_NtkAttach( Abc_Ntk_t * pNtk );
 /*=== abcBalance.c ==========================================================*/
@@ -462,8 +463,8 @@ extern void               Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFani
 extern void               Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
 extern void               Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew );
 /*=== abcFraig.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes );
-extern void *             Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes );
+extern Abc_Ntk_t *        Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc );
+extern void *             Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc );
 extern Abc_Ntk_t *        Abc_NtkFraigTrust( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkFraigStore( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkFraigRestore();
@@ -557,9 +558,10 @@ extern void               Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkStartRead( char * pName );
 extern void               Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkDup( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis );
+extern Abc_Ntk_t *        Abc_NtkCreateOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis );
 extern Abc_Ntk_t *        Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues );
-extern Abc_Ntk_t *        Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
+extern Abc_Ntk_t *        Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode );
+extern Abc_Ntk_t *        Abc_NtkCreateWithNode( char * pSop );
 extern void               Abc_NtkDelete( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk );
 /*=== abcPrint.c ==========================================================*/
@@ -625,12 +627,13 @@ extern bool               Abc_SopIsOrType( char * pSop );
 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 );
+extern char *             Abc_SopFromTruthBin( char * pTruth );
+extern char *             Abc_SopFromTruthHex( char * pTruth );
 /*=== abcStrash.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup );
 extern Abc_Obj_t *        Abc_NodeStrash( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
 extern int                Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 );
 /*=== abcSweep.c ==========================================================*/
-extern bool               Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose );
 extern int                Abc_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
 extern int                Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose );
 /*=== abcTiming.c ==========================================================*/
@@ -666,6 +669,7 @@ extern int                Abc_NtkGetExorNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
+extern void               Abc_NtkCleanNext( Abc_Ntk_t * pNtk );
 extern Abc_Obj_t *        Abc_NodeHasUniqueCoFanout( Abc_Obj_t * pNode );
 extern bool               Abc_NtkLogicHasSimpleCos( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDuplicate );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 3f7f8d7c..45d7a6e9 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -1236,6 +1236,35 @@ void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan )
         }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Sets the correct phase of the nodes.]
+
+  Description [The AIG nodes should be in the DFS order.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_AigSetNodePhases( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkIsDfsOrdered(pNtk) );
+    Abc_AigConst1(pNtk->pManFunc)->fPhase = 1;
+//    Abc_NtkForEachCi( pNtk, pObj, i )
+//        pObj->fPhase = 0;
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        pObj->fPhase = 0;
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        pObj->fPhase = Abc_LatchIsInit1(pObj);
+    Abc_AigForEachAnd( pNtk, pObj, i )
+        pObj->fPhase = (Abc_ObjFanin0(pObj)->fPhase ^ Abc_ObjFaninC0(pObj)) & (Abc_ObjFanin1(pObj)->fPhase ^ Abc_ObjFaninC1(pObj));
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        pObj->fPhase = (Abc_ObjFanin0(pObj)->fPhase ^ Abc_ObjFaninC0(pObj));
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c
index 097ee92d..ba1443ab 100644
--- a/src/base/abc/abcDfs.c
+++ b/src/base/abc/abcDfs.c
@@ -229,6 +229,8 @@ bool Abc_NtkIsDfsOrdered( Abc_Ntk_t * pNtk )
     // go through the nodes
     Abc_NtkForEachNode( pNtk, pNode, i )
     {
+        if ( Abc_ObjFaninNum(pNode) == 0 )
+            continue;
         if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pNode)) )
             return 0;
         if ( !Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pNode)) )
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 0cdee0b3..57219eea 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -162,13 +162,16 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, ABC_FUNC_SOP );
     else
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, ABC_FUNC_BDD );
+
     // create the CI nets and remember them in the new CI nodes
     Abc_NtkForEachCi( pNtk, pObj, i )
     {
         pNet = Abc_NtkFindOrCreateNet( pNtkNew, Abc_ObjName(pObj) );
         Abc_ObjAddFanin( pNet, pObj->pCopy );
         pObj->pCopy->pCopy = pNet;
+//printf( "%s ", Abc_ObjName(pObj) );
     }
+//printf( "\n" );
     // duplicate all nodes
     Abc_NtkForEachNode( pNtk, pObj, i )
         Abc_NtkDupObj(pNtkNew, pObj);
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 2720f169..ba9ab231 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -318,7 +318,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis )
+Abc_Ntk_t * Abc_NtkCreateOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis )
 {
     Vec_Ptr_t * vNodes;
     Abc_Ntk_t * pNtkNew; 
@@ -373,13 +373,13 @@ Abc_Ntk_t * Abc_NtkSplitOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAll
     Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) );
 
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkSplitOutput(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkCreateOutput(): Network check has failed.\n" );
     return pNtkNew;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Creates the network composed of one output.]
+  Synopsis    [Creates the miter composed of one multi-output cone.]
 
   Description []
                
@@ -439,7 +439,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t *
 
 /**Function*************************************************************
 
-  Synopsis    [Deletes the Ntk.]
+  Synopsis    [Creates the network composed of one node.]
 
   Description []
                
@@ -448,7 +448,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t *
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
+Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
 {    
     Abc_Ntk_t * pNtkNew; 
     Abc_Obj_t * pFanin, * pNodePo;
@@ -471,7 +471,48 @@ Abc_Ntk_t * Abc_NtkSplitNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode )
     Abc_ObjAddFanin( pNodePo, pNode->pCopy );
     Abc_NtkLogicStoreName( pNodePo, Abc_ObjName(pNode) );
     if ( !Abc_NtkCheck( pNtkNew ) )
-        fprintf( stdout, "Abc_NtkSplitNode(): Network check has failed.\n" );
+        fprintf( stdout, "Abc_NtkCreateFromNode(): Network check has failed.\n" );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the network composed of one node with the given SOP.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop )
+{    
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pFanin, * pNode, * pNodePo;
+    Vec_Ptr_t * vNames;
+    int i, nVars;
+    // start the network
+    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP );
+    pNtkNew->pName = util_strsav("ex");
+    // create PIs
+    Vec_PtrPush( pNtkNew->vObjs, NULL );
+    nVars = Abc_SopGetVarNum( pSop );
+    vNames = Abc_NodeGetFakeNames( nVars );
+    for ( i = 0; i < nVars; i++ )
+        Abc_NtkLogicStoreName( Abc_NtkCreatePi(pNtkNew), Vec_PtrEntry(vNames, i) );
+    Abc_NodeFreeNames( vNames );
+    // create the node, add PIs as fanins, set the function
+    pNode = Abc_NtkCreateNode( pNtkNew );
+    Abc_NtkForEachPi( pNtkNew, pFanin, i )
+        Abc_ObjAddFanin( pNode, pFanin );
+    pNode->pData = Abc_SopRegister( pNtkNew->pManFunc, pSop );
+    // create the only PO
+    pNodePo = Abc_NtkCreatePo(pNtkNew);
+    Abc_ObjAddFanin( pNodePo, pNode );
+    Abc_NtkLogicStoreName( pNodePo, "F" );
+    if ( !Abc_NtkCheck( pNtkNew ) )
+        fprintf( stdout, "Abc_NtkCreateWithNode(): Network check has failed.\n" );
     return pNtkNew;
 }
 
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index cc8b90f6..2e2d758d 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -105,6 +105,7 @@ void Abc_NtkShowAig( Abc_Ntk_t * pNtk )
         fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
         return;
     }
+    fclose( pFile );
 
     // collect all nodes in the network
     vNodes = Vec_PtrAlloc( 100 );
@@ -149,6 +150,7 @@ void Abc_NtkShowMulti( Abc_Ntk_t * pNtk )
         fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", FileNameDot );
         return;
     }
+    fclose( pFile );
 
     // get the implication supergates
     Abc_NtkBalanceAttach( pNtk );
diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 28e92889..03a73787 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -731,6 +731,132 @@ void Abc_SopAddCnfToSolver( solver * pSat, char * pClauses, Vec_Int_t * vVars, V
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Derives SOP from the truth table representation.]
+
+  Description [Truth table is expected to be in the hexadecimal notation.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopFromTruthBin( char * pTruth )
+{
+    char * pSopCover, * pCube;
+    int nTruthSize, nVars, Digit, Length, Mint, i, b;
+    Vec_Int_t * vMints;
+
+    // get the number of variables
+    nTruthSize = strlen(pTruth);
+    nVars = Extra_Base2Log( nTruthSize );
+    if ( nTruthSize != (1 << (nVars)) )
+    {
+        printf( "String %s does not look like a truth table of a %d-variable function.\n", pTruth, nVars );
+        return NULL;
+    }
+
+    // collect the on-set minterms
+    vMints = Vec_IntAlloc( 100 );
+    for ( i = 0; i < nTruthSize; i++ )
+    {
+        if ( pTruth[i] >= '0' && pTruth[i] <= '1' )
+            Digit = pTruth[i] - '0';
+        else
+        {
+            printf( "String %s does not look like a binary representation of the truth table.\n", pTruth );
+            return NULL;
+        }
+        if ( Digit == 1 )
+            Vec_IntPush( vMints, nTruthSize - 1 - i );
+    }
+
+    // create the SOP representation of the minterms
+    Length = Vec_IntSize(vMints) * (nVars + 3);
+    pSopCover = ALLOC( char, Length + 1 );
+    pSopCover[Length] = 0;
+    Vec_IntForEachEntry( vMints, Mint, i )
+    {
+        pCube = pSopCover + i * (nVars + 3);
+        for ( b = 0; b < nVars; b++ )
+            if ( Mint & (1 << b) )
+                pCube[b] = '1';
+            else
+                pCube[b] = '0';
+        pCube[nVars + 0] = ' ';
+        pCube[nVars + 1] = '1';
+        pCube[nVars + 2] = '\n';
+    }
+    Vec_IntFree( vMints );
+    return pSopCover;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives SOP from the truth table representation.]
+
+  Description [Truth table is expected to be in the hexadecimal notation.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+char * Abc_SopFromTruthHex( char * pTruth )
+{
+    char * pSopCover, * pCube;
+    int nTruthSize, nVars, Digit, Length, Mint, i, b;
+    Vec_Int_t * vMints;
+
+    // get the number of variables
+    nTruthSize = strlen(pTruth);
+    nVars = Extra_Base2Log( nTruthSize ) + 2;
+    if ( nTruthSize != (1 << (nVars-2)) )
+    {
+        printf( "String %s does not look like a truth table of a %d-variable function.\n", pTruth, nVars );
+        return NULL;
+    }
+
+    // collect the on-set minterms
+    vMints = Vec_IntAlloc( 100 );
+    for ( i = 0; i < nTruthSize; i++ )
+    {
+        if ( pTruth[i] >= '0' && pTruth[i] <= '9' )
+            Digit = pTruth[i] - '0';
+        else if ( pTruth[i] >= 'a' && pTruth[i] <= 'f' )
+            Digit = 10 + pTruth[i] - 'a';
+        else if ( pTruth[i] >= 'A' && pTruth[i] <= 'F' )
+            Digit = 10 + pTruth[i] - 'A';
+        else
+        {
+            printf( "String %s does not look like a hexadecimal representation of the truth table.\n", pTruth );
+            return NULL;
+        }
+        for ( b = 0; b < 4; b++ )
+            if ( Digit & (1 << b) )
+                Vec_IntPush( vMints, 4*(nTruthSize-1-i)+b );
+    }
+
+    // create the SOP representation of the minterms
+    Length = Vec_IntSize(vMints) * (nVars + 3);
+    pSopCover = ALLOC( char, Length + 1 );
+    pSopCover[Length] = 0;
+    Vec_IntForEachEntry( vMints, Mint, i )
+    {
+        pCube = pSopCover + i * (nVars + 3);
+        for ( b = 0; b < nVars; b++ )
+            if ( Mint & (1 << b) )
+                pCube[b] = '1';
+            else
+                pCube[b] = '0';
+        pCube[nVars + 0] = ' ';
+        pCube[nVars + 1] = '1';
+        pCube[nVars + 2] = '\n';
+    }
+    Vec_IntFree( vMints );
+    return pSopCover;
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index a5605d4e..13720aeb 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -305,15 +305,32 @@ int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk )
 void Abc_NtkCleanCopy( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
-    int i;
-    i = 0;
-    // set the data filed to NULL
+    int i = 0;
     Abc_NtkForEachObj( pNtk, pObj, i )
         pObj->pCopy = NULL;
 }
 
 /**Function*************************************************************
 
+  Synopsis    [Cleans the copy field of all objects.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkCleanNext( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pObj;
+    int i = 0;
+    Abc_NtkForEachObj( pNtk, pObj, i )
+        pObj->pNext = NULL;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Checks if the internal node has a unique CO.]
 
   Description [Checks if the internal node can borrow a name from a CO
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index ca9f1dfa..cde9c16b 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -32,6 +32,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static int Abc_CommandPrintStats   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintExdc    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintIo      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintLatch   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintFanio   ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -39,6 +40,7 @@ static int Abc_CommandPrintFactor  ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandPrintLevel   ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintSupport ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPrintSymms   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandPrintKMap    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandShowBdd      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShowCut      ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -61,12 +63,16 @@ 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_CommandReorder      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMuxes        ( 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_CommandOneOutput    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandOneNode      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandShortNames   ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcFree     ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcGet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandExdcSet      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCut          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandTest         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -93,6 +99,7 @@ static int Abc_CommandUnseq        ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandRetime       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqFpga      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeqMap       ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSeqSweep     ( 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 );
@@ -114,7 +121,10 @@ static int Abc_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv
 ***********************************************************************/
 void Abc_Init( Abc_Frame_t * pAbc )
 {
+//    Abc_NtkBddImplicationTest();
+
     Cmd_CommandAdd( pAbc, "Printing",     "print_stats",   Abc_CommandPrintStats,       0 ); 
+    Cmd_CommandAdd( pAbc, "Printing",     "print_exdc",    Abc_CommandPrintExdc,        0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_io",      Abc_CommandPrintIo,          0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_latch",   Abc_CommandPrintLatch,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_fanio",   Abc_CommandPrintFanio,       0 );
@@ -122,6 +132,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Printing",     "print_level",   Abc_CommandPrintLevel,       0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_supp",    Abc_CommandPrintSupport,     0 );
     Cmd_CommandAdd( pAbc, "Printing",     "print_symm",    Abc_CommandPrintSymms,       0 );
+    Cmd_CommandAdd( pAbc, "Printing",     "print_kmap",    Abc_CommandPrintKMap,        0 );
 
     Cmd_CommandAdd( pAbc, "Printing",     "show_bdd",      Abc_CommandShowBdd,          0 );
     Cmd_CommandAdd( pAbc, "Printing",     "show_cut",      Abc_CommandShowCut,          0 );
@@ -139,17 +150,21 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "rewrite",       Abc_CommandRewrite,          1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "refactor",      Abc_CommandRefactor,         1 );
 
-    Cmd_CommandAdd( pAbc, "Various",      "logic",         Abc_CommandLogic,            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",      "reorder",       Abc_CommandReorder,          0 );
     Cmd_CommandAdd( pAbc, "Various",      "muxes",         Abc_CommandMuxes,            1 );
     Cmd_CommandAdd( pAbc, "Various",      "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
     Cmd_CommandAdd( pAbc, "Various",      "one_output",    Abc_CommandOneOutput,        1 );
     Cmd_CommandAdd( pAbc, "Various",      "one_node",      Abc_CommandOneNode,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "short_names",   Abc_CommandShortNames,       0 );
+    Cmd_CommandAdd( pAbc, "Various",      "exdc_free",     Abc_CommandExdcFree,         1 );
+    Cmd_CommandAdd( pAbc, "Various",      "exdc_get",      Abc_CommandExdcGet,          1 );
+    Cmd_CommandAdd( pAbc, "Various",      "exdc_set",      Abc_CommandExdcSet,          1 );
     Cmd_CommandAdd( pAbc, "Various",      "cut",           Abc_CommandCut,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "test",          Abc_CommandTest,             0 );
 
@@ -176,6 +191,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Sequential",   "retime",        Abc_CommandRetime,           1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "sfpga",         Abc_CommandSeqFpga,          1 );
     Cmd_CommandAdd( pAbc, "Sequential",   "smap",          Abc_CommandSeqMap,           1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "seq_sweep",     Abc_CommandSeqSweep,         1 );
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
@@ -248,7 +264,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( pNtk == NULL )
     {
-        fprintf( Abc_FrameReadErr(pAbc), "Empty network\n" );
+        fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" );
         return 1;
     }
     Abc_NtkPrintStats( pOut, pNtk, fFactor );
@@ -256,7 +272,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     fprintf( pErr, "usage: print_stats [-fh]\n" );
-    fprintf( pErr, "\t        prints the network statistics and\n" );
+    fprintf( pErr, "\t        prints the network statistics\n" );
     fprintf( pErr, "\t-f    : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
@@ -273,6 +289,98 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkTemp;
+    double Percentage;
+    bool fShort;
+    int c;
+    int fPrintDc;
+
+    extern double Abc_NtkSpacePercentage( Abc_Obj_t * pNode );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set the defaults
+    fShort  = 1;
+    fPrintDc = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "sdh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 's':
+            fShort ^= 1;
+            break;
+        case 'd':
+            fPrintDc ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" );
+        return 1;
+    }
+    if ( pNtk->pExdc == NULL )
+    {
+        fprintf( Abc_FrameReadErr(pAbc), "Network has no EXDC.\n" );
+        return 1;
+    }
+
+    if ( fPrintDc )
+    {
+        if ( !Abc_NtkIsStrash(pNtk->pExdc) )
+        {
+            pNtkTemp = Abc_NtkStrash(pNtk->pExdc, 0, 0);
+            Percentage = Abc_NtkSpacePercentage( Abc_ObjChild0( Abc_NtkPo(pNtkTemp, 0) ) );
+            Abc_NtkDelete( pNtkTemp );
+        }
+        else
+            Percentage = Abc_NtkSpacePercentage( Abc_ObjChild0( Abc_NtkPo(pNtk->pExdc, 0) ) );
+
+        printf( "EXDC network statistics: " );
+        printf( "(" );
+        if ( Percentage > 0.05 && Percentage < 99.95 )
+            printf( "%.2f", Percentage );
+        else if ( Percentage > 0.000005 && Percentage < 99.999995 )
+            printf( "%.6f", Percentage );
+        else
+            printf( "%f", Percentage );
+        printf( " %% don't-cares)\n" );
+    }
+    else
+        printf( "EXDC network statistics: \n" );
+    Abc_NtkPrintStats( pOut, pNtk->pExdc, 0 );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_exdc [-dh]\n" );
+    fprintf( pErr, "\t        prints the EXDC network statistics\n" );
+    fprintf( pErr, "\t-d    : toggles printing don't-care percentage [default = %s]\n", fPrintDc? "yes": "no" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -754,6 +862,94 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pNode;
+    int c;
+    int fUseRealNames;
+
+    extern void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fUseRealNames = 1;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "nh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'n':
+            fUseRealNames ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsBddLogic(pNtk) )
+    {
+        fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks (run \"bdd\").\n" );
+        return 1;
+    }
+    if ( argc > util_optind + 1 )
+    {
+        fprintf( pErr, "Wrong number of auguments.\n" );
+        goto usage;
+    }
+    if ( argc == util_optind )
+    {
+        pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
+        if ( !Abc_ObjIsNode(pNode) )
+        {
+            fprintf( pErr, "The driver \"%s\" of the first PO is not an internal node.\n", Abc_ObjName(pNode) );
+            return 1;
+        }
+    }
+    else
+    {
+        pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+        if ( pNode == NULL )
+        {
+            fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+            return 1;
+        }
+    }
+    Abc_NodePrintKMap( pNode, fUseRealNames );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: print_kmap [-nh] <node>\n" );
+    fprintf( pErr, "          shows the truth table of the node\n" );
+    fprintf( pErr, "\t-n    : toggles real/dummy fanin names [default = %s]\n", fUseRealNames? "real": "dummy" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    fprintf( pErr, "\tnode  : the node to consider (default = the driver of the first PO)\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -787,21 +983,32 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( !Abc_NtkIsBddLogic(pNtk) )
     {
-        fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks.\n" );
+        fprintf( pErr, "Visualizing BDDs can only be done for logic BDD networks (run \"bdd\").\n" );
         return 1;
     }
 
-    if ( argc != util_optind + 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 )
+    if ( argc == util_optind )
     {
-        fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
-        return 1;
+        pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) );
+        if ( !Abc_ObjIsNode(pNode) )
+        {
+            fprintf( pErr, "The driver \"%s\" of the first PO is not an internal node.\n", Abc_ObjName(pNode) );
+            return 1;
+        }
+    }
+    else
+    {
+        pNode = Abc_NtkFindNode( pNtk, argv[util_optind] );
+        if ( pNode == NULL )
+        {
+            fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] );
+            return 1;
+        }
     }
     Abc_NodeShowBdd( pNode );
     return 0;
@@ -813,7 +1020,7 @@ usage:
     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, "\tnode  : the node to consider [default = the driver of the first PO]\n");
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -1423,7 +1630,7 @@ int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( !Abc_NtkIsSopLogic(pNtk) && !Abc_NtkIsBddLogic(pNtk) )
     {
-        fprintf( pErr, "Sweep cannot be performed on an AIG or a mapped network (unmap it first).\n" );
+        fprintf( pErr, "Sweep cannot be performed on an AIG or a mapped network (run \"unmap\").\n" );
         return 1;
     }
     // modify the current network
@@ -1666,7 +1873,7 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         if ( !Abc_NtkIsBddLogic( pNtk ) )
         {
-            fprintf( pErr, "This command is only applicable to logic BDD networks.\n" );
+            fprintf( pErr, "This command is only applicable to logic BDD networks (run \"bdd\").\n" );
             return 1;
         }
         fprintf( stdout, "Performing simple non-recursive DSD of local functions.\n" );
@@ -2233,7 +2440,6 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    // get the new network
     if ( !Abc_NtkIsSopLogic(pNtk) )
     {
         fprintf( pErr, "Converting to BDD is possible when node functions are SOPs.\n" );
@@ -2264,6 +2470,69 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandReorder( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int fVerbose;
+    extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int 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;
+    }
+
+    // get the new network
+    if ( !Abc_NtkIsBddLogic(pNtk) )
+    {
+        fprintf( pErr, "Variable reordering is possible when node functions are BDDs (run \"bdd\").\n" );
+        return 1;
+    }
+    Abc_NtkBddReorder( pNtk, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: reorder [-vh]\n" );
+    fprintf( pErr, "\t         reorders local functions of the nodes using sifting\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;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -2559,7 +2828,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "Cannot find CO node \"%s\".\n", argv[util_optind] );
             return 1;
         }
-        pNtkRes = Abc_NtkSplitOutput( pNtk, pNode, fUseAllCis );
+        pNtkRes = Abc_NtkCreateOutput( pNtk, pNode, fUseAllCis );
     }
     else
     {
@@ -2573,7 +2842,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv )
             fprintf( pErr, "The 0-based output number (%d) is larger than the number of outputs (%d).\n", Output, Abc_NtkCoNum(pNtk) );
             return 1;
         }
-        pNtkRes = Abc_NtkSplitOutput( pNtk, Abc_NtkCo(pNtk,Output), fUseAllCis );
+        pNtkRes = Abc_NtkCreateOutput( pNtk, Abc_NtkCo(pNtk,Output), fUseAllCis );
     }
     if ( pNtkRes == NULL )
     {
@@ -2654,7 +2923,7 @@ int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    pNtkRes = Abc_NtkSplitNode( pNtk, pNode );
+    pNtkRes = Abc_NtkCreateFromNode( pNtk, pNode );
 //    pNtkRes = Abc_NtkDeriveFromBdd( pNtk->pManFunc, pNode->pData, NULL, NULL );
     if ( pNtkRes == NULL )
     {
@@ -2735,6 +3004,210 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandExdcFree( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+
+    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 ( pNtk->pExdc == NULL )
+    {
+        fprintf( pErr, "The network has no EXDC.\n" );
+        return 1;
+    }
+
+    Abc_NtkDelete( pNtk->pExdc );
+    pNtk->pExdc = NULL;
+
+    // replace the current network
+    pNtkRes = Abc_NtkDup( pNtk );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: exdc_free [-h]\n" );
+    fprintf( pErr, "\t         frees the EXDC network of the current network\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandExdcGet( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+
+    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 ( pNtk->pExdc == NULL )
+    {
+        fprintf( pErr, "The network has no EXDC.\n" );
+        return 1;
+    }
+
+    // replace the current network
+    pNtkRes = Abc_NtkDup( pNtk->pExdc );
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: exdc_get [-h]\n" );
+    fprintf( pErr, "\t         replaces the current network by the EXDC of the current network\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr, * pFile;
+    Abc_Ntk_t * pNtk, * pNtkNew, * pNtkRes;
+    char * FileName;
+    int c;
+
+    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 ( argc != util_optind + 1 )
+    {
+        goto usage;
+    }
+
+    // get the input file name
+    FileName = argv[util_optind];
+    if ( (pFile = fopen( FileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName );
+        if ( FileName = Extra_FileGetSimilarName( FileName, ".mv", ".blif", ".pla", ".eqn", ".bench" ) )
+            fprintf( pAbc->Err, "Did you mean \"%s\"?", FileName );
+        fprintf( pAbc->Err, "\n" );
+        return 1;
+    }
+    fclose( pFile );
+
+    // set the new network
+    pNtkNew = Io_Read( FileName, 1 );
+    if ( pNtkNew == NULL )
+    {
+        fprintf( pAbc->Err, "Reading network from file has failed.\n" );
+        return 1;
+    }
+
+    // replace the EXDC
+    if ( pNtk->pExdc )
+    {
+        Abc_NtkDelete( pNtk->pExdc );
+        pNtk->pExdc = NULL;
+    }
+    pNtkRes = Abc_NtkDup( pNtk );
+    pNtkRes->pExdc = pNtkNew;
+
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: exdc_set [-h] <file>\n" );
+    fprintf( pErr, "\t         sets the network from file as EXDC for the current network\n" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    fprintf( pErr, "\t<file> : file with the new EXDC network\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Cut_Params_t Params, * pParams = &Params;
@@ -3038,6 +3511,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int fAllNodes;
+    int fExdc;
     int c;
 
     pNtk = Abc_FrameReadNet(pAbc);
@@ -3045,6 +3519,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fExdc     = 0;
     fAllNodes = 0;
     memset( pParams, 0, sizeof(Fraig_Params_t) );
     pParams->nPatsRand  = 2048; // the number of words of random simulation info
@@ -3059,7 +3534,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     pParams->fVerbose   =  0;   // the verbosiness flag
     pParams->fVerboseP  =  0;   // the verbosiness flag
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "RDBrscpvah" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "RDBrscpvaeh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3115,6 +3590,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'a':
             fAllNodes ^= 1;
             break;
+        case 'e':
+            fExdc ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -3138,11 +3616,11 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the new network
     if ( Abc_NtkIsStrash(pNtk) )
-        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
+        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
     else
     {
         pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes );
-        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes );
+        pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc );
         Abc_NtkDelete( pNtk );
     }
     if ( pNtkRes == NULL )
@@ -3170,6 +3648,7 @@ usage:
     fprintf( pErr, "\t-c     : toggle accumulation of choices [default = %s]\n",              pParams->fChoicing? "yes": "no" );
     fprintf( pErr, "\t-p     : toggle proving the final miter [default = %s]\n",              pParams->fTryProve? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n",                       pParams->fVerbose?  "yes": "no" );
+    fprintf( pErr, "\t-e     : toggle functional sweeping using EXDC [default = %s]\n",       fExdc? "yes": "no" );
     fprintf( pErr, "\t-a     : toggle between all nodes and DFS nodes [default = %s]\n",      fAllNodes? "all": "dfs" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -3430,7 +3909,9 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk;
     int c;
     int fUseInv;
+    int fExdc;
     int fVerbose;
+    extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3438,15 +3919,19 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     fUseInv   = 1;
+    fExdc     = 0;
     fVerbose  = 0;
     util_getopt_reset();
-    while ( ( c = util_getopt( argc, argv, "ivh" ) ) != EOF )
+    while ( ( c = util_getopt( argc, argv, "ievh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'i':
             fUseInv ^= 1;
             break;
+        case 'e':
+            fExdc ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -3473,7 +3958,7 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     // modify the current network
-    if ( !Abc_NtkFraigSweep( pNtk, fUseInv, fVerbose ) )
+    if ( !Abc_NtkFraigSweep( pNtk, fUseInv, fExdc, fVerbose ) )
     {
         fprintf( pErr, "Sweeping has failed.\n" );
         return 1;
@@ -3481,9 +3966,9 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: fraig_sweep [-vh]\n" );
+    fprintf( pErr, "usage: fraig_sweep [-evh]\n" );
     fprintf( pErr, "\t        performs technology-dependent sweep\n" );
-//    fprintf( pErr, "\t-i    : toggle using inverter for complemented nodes [default = %s]\n", fUseInv? "yes": "no" );
+    fprintf( pErr, "\t-e    : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" );
     fprintf( pErr, "\t-v    : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
@@ -3513,6 +3998,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     int c;
     extern Abc_Ntk_t * Abc_NtkMap( Abc_Ntk_t * pNtk, double DelayTarget, int fRecovery, int fSwitching, int fVerbose );
+    extern bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose );
 
     pNtk = Abc_FrameReadNet(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -3603,7 +4089,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     if ( fSweep )
-        Abc_NtkFraigSweep( pNtkRes, 0, 0 );
+        Abc_NtkFraigSweep( pNtkRes, 0, 0, 0 );
 
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -4517,6 +5003,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
         return 1;
     }
+return 0;
 
     // get the new network
     pNtkRes = Abc_NtkFpgaSeq( pNtk, fVerbose );
@@ -4588,6 +5075,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Works only for sequential AIG (run \"seq\").\n" );
         return 1;
     }
+return 0;
 
     // get the new network
     pNtkRes = Abc_NtkMapSeq( pNtk, fVerbose );
@@ -4608,6 +5096,109 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int nFrames;
+    int fExdc;
+    int fVerbose;
+    extern Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose );
+
+    pNtk = Abc_FrameReadNet(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nFrames  = 1;
+    fExdc    = 1;
+    fVerbose = 1;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "Fevh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( util_optind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[util_optind]);
+            util_optind++;
+            if ( nFrames < 0 ) 
+                goto usage;
+            break;
+        case 'e':
+            fExdc ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( pErr, "Works only for combinational networks (run \"unseq\").\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" );
+        return 1;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Works only for structurally hashed networks (run \"strash\").\n" );
+        return 1;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Sequential FPGA mapping has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: seq_sweep [-F num] [-vh]\n" );
+    fprintf( pErr, "\t         performs sequential sweep using van Eijk's method\n" );
+    fprintf( pErr, "\t-F num : number of time frames in the base case [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
 
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index c612a1ce..9b5f7d5b 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -52,6 +52,8 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate )
     pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
     Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate );
     Abc_NtkFinalize( pNtk, pNtkAig );
+    if ( pNtk->pExdc )
+        pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
     // make sure everything is okay
     if ( !Abc_NtkCheck( pNtkAig ) )
     {
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index 8c2f5bd3..9de61389 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -69,6 +69,9 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
     // make the network minimum base
     Abc_NtkMinimumBase( pNtkNew );
 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 5b317994..7e81c579 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -76,6 +76,9 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
     Extra_StopManager( pNtk->pManGlob );
     pNtk->pManGlob = NULL;
 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c
index ea97826a..161607b5 100644
--- a/src/base/abci/abcFpga.c
+++ b/src/base/abci/abcFpga.c
@@ -88,6 +88,9 @@ Abc_Ntk_t * Abc_NtkFpga( Abc_Ntk_t * pNtk, int fRecovery, int fSwitching, int fV
     // make the network minimum base
     Abc_NtkMinimumBase( pNtkNew );
 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c
index 5657fe38..421cdfed 100644
--- a/src/base/abci/abcFraig.c
+++ b/src/base/abci/abcFraig.c
@@ -26,12 +26,16 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Abc_Ntk_t *   Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
-static Abc_Obj_t *   Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
-
-static int           Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk );
-static void          Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
-static Abc_Obj_t *   Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
+static Abc_Ntk_t *    Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+static Abc_Ntk_t *    Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+static Abc_Obj_t *    Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig );
+static void           Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs );
+extern Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc );
+static void           Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+
+static int            Abc_NtkFraigTrustCheck( Abc_Ntk_t * pNtk );
+static void           Abc_NtkFraigTrustOne( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+static Abc_Obj_t *    Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -48,19 +52,27 @@ static Abc_Obj_t *   Abc_NodeFraigTrust( Abc_Aig_t * pMan, Abc_Obj_t * pNode );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
+Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc )
 {
     Fraig_Params_t * pPars = pParams;
     Abc_Ntk_t * pNtkNew;
     Fraig_Man_t * pMan;
+    // check if EXDC is present
+    if ( fExdc && pNtk->pExdc == NULL )
+        fExdc = 0, printf( "Warning: Networks has no EXDC.\n" );
     // perform fraiging
-    pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes ); 
+    pMan = Abc_NtkToFraig( pNtk, pParams, fAllNodes, fExdc ); 
     // prove the miter if asked to
     if ( pPars->fTryProve )
         Fraig_ManProveMiter( pMan );
     // reconstruct FRAIG in the new network
-    pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
+    if ( fExdc ) 
+        pNtkNew = Abc_NtkFromFraig2( pMan, pNtk );
+    else
+        pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
     Fraig_ManFree( pMan );
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
@@ -82,14 +94,13 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
   SeeAlso     []
 
 ***********************************************************************/
-void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
+void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc )
 {
+    int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
     Fraig_Man_t * pMan;
     ProgressBar * pProgress;
-    Fraig_Node_t * pNodeFraig;
     Vec_Ptr_t * vNodes;
-    Abc_Obj_t * pNode, * pConst1;
-    int fInternal = ((Fraig_Params_t *)pParams)->fInternal;
+    Abc_Obj_t * pNode;
     int i;
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -97,11 +108,12 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
     // create the FRAIG manager
     pMan = Fraig_ManCreate( pParams );
 
-    // create PIs and remember them in the old nodes
+    // map the constant node
     Abc_NtkCleanCopy( pNtk );
+    Abc_AigConst1(pNtk->pManFunc)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
+    // create PIs and remember them in the old nodes
     Abc_NtkForEachCi( pNtk, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
-    pConst1 = Abc_AigConst1( pNtk->pManFunc );
 
     // perform strashing
     vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 );
@@ -109,21 +121,22 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
         pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize );
     Vec_PtrForEachEntry( vNodes, pNode, i )
     {
+        if ( Abc_ObjFaninNum(pNode) == 0 )
+            continue;
         if ( !fInternal )
             Extra_ProgressBarUpdate( pProgress, i, NULL );
-        if ( pNode == pConst1 )
-            pNodeFraig = Fraig_ManReadConst1(pMan);
-        else
-            pNodeFraig = Fraig_NodeAnd( pMan, 
+        pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
                 Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
                 Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
-        assert( pNode->pCopy == NULL );
-        pNode->pCopy = (Abc_Obj_t *)pNodeFraig;
     }
     if ( !fInternal )
         Extra_ProgressBarStop( pProgress );
     Vec_PtrFree( vNodes );
 
+    // use EXDC to change the mapping of nodes into FRAIG nodes
+    if ( fExdc )
+        Abc_NtkFraigRemapUsingExdc( pMan, pNtk );
+
     // set the primary outputs
     Abc_NtkForEachCo( pNtk, pNode, i )
         Fraig_ManSetPo( pMan, (Fraig_Node_t *)Abc_ObjNotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ) );
@@ -132,7 +145,123 @@ void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes )
 
 /**Function*************************************************************
 
-  Synopsis    [Transforms FRAIG into what looks like a strashed network.]
+  Synopsis    [Derives EXDC node for the given network.]
+
+  Description [Assumes that EXDCs of all POs are the same.
+  Returns the EXDC of the first PO.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtkMain, Abc_Ntk_t * pNtkExdc )
+{
+    Abc_Ntk_t * pNtkStrash;
+    Abc_Obj_t * pObj;
+    Fraig_Node_t * gResult;
+    char ** ppNames;
+    int i, k;
+    // strash the EXDC network
+    pNtkStrash = Abc_NtkStrash( pNtkExdc, 0, 0 );
+    Abc_NtkCleanCopy( pNtkStrash );
+    Abc_AigConst1(pNtkStrash->pManFunc)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
+    // set the mapping of the PI nodes
+    ppNames = Abc_NtkCollectCioNames( pNtkMain, 0 );
+    Abc_NtkForEachCi( pNtkStrash, pObj, i )
+    {
+        for ( k = 0; k < Abc_NtkCiNum(pNtkMain); k++ )
+            if ( strcmp( Abc_ObjName(pObj), ppNames[k] ) == 0 )
+            {
+                pObj->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, k);
+                break;
+            }
+        assert( pObj->pCopy != NULL );
+    }
+    free( ppNames );
+    // build FRAIG for each node
+    Abc_AigForEachAnd( pNtkStrash, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
+                Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) ),
+                Fraig_NotCond( Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC1(pObj) ) );
+    // get the EXDC to be returned
+    pObj = Abc_NtkPo( pNtkStrash, 0 );
+    gResult = Fraig_NotCond( Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+    Abc_NtkDelete( pNtkStrash );
+    return gResult;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Changes mapping of the old nodes into FRAIG nodes using EXDC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFraigRemapUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    Fraig_Node_t * gNodeNew, * gNodeExdc;
+    stmm_table * tTable;
+    stmm_generator * gen;
+    Abc_Obj_t * pNode, * pNodeBest;
+    Abc_Obj_t * pClass, ** ppSlot;
+    Vec_Ptr_t * vNexts;
+    int i;
+
+    // get the global don't-cares
+    assert( pNtk->pExdc );
+    gNodeExdc = Abc_NtkToFraigExdc( pMan, pNtk, pNtk->pExdc );
+
+    // save the next pointers
+    vNexts = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Vec_PtrWriteEntry( vNexts, pNode->Id, pNode->pNext );
+
+    // find the classes of AIG nodes which have FRAIG nodes assigned
+    Abc_NtkCleanNext( pNtk );
+    tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy )
+        {
+            gNodeNew = Fraig_NodeAnd( pMan, (Fraig_Node_t *)pNode->pCopy, Fraig_Not(gNodeExdc) );
+            if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(gNodeNew), (char ***)&ppSlot ) )
+                *ppSlot = NULL;
+            pNode->pNext = *ppSlot;
+            *ppSlot = pNode;
+        }
+
+    // for reach non-trival class, find the node with minimum level, and replace other nodes by it
+    Abc_AigSetNodePhases( pNtk );
+    stmm_foreach_item( tTable, gen, (char **)&gNodeNew, (char **)&pClass )
+    {
+        if ( pClass->pNext == NULL )
+            continue;
+        // find the node with minimum level
+        pNodeBest = pClass;
+        for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext )
+            if ( pNodeBest->Level > pNode->Level )
+                 pNodeBest = pNode;
+        // remap the class nodes
+        for ( pNode = pClass; pNode; pNode = pNode->pNext )
+            pNode->pCopy = Abc_ObjNotCond( pNodeBest->pCopy, pNode->fPhase ^ pNodeBest->fPhase );
+    }
+    stmm_free_table( tTable );
+
+    // restore the next pointers
+    Abc_NtkCleanNext( pNtk );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        pNode->pNext = Vec_PtrEntry( vNexts, pNode->Id );
+    Vec_PtrFree( vNexts );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms FRAIG into strashed network with choices.]
 
   Description []
                
@@ -229,6 +358,110 @@ Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFrai
     return Abc_ObjNotCond( pRes, Fraig_IsComplement(pNodeFraig) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Transforms FRAIG into strashed network without choices.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    stmm_table * tTable;
+    Vec_Ptr_t * vNodeReprs;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pRepr, ** ppSlot;
+    int i;
+
+    // map the nodes into their lowest level representives
+    tTable = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
+    pNode = Abc_AigConst1(pNtk->pManFunc);
+    if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
+        *ppSlot = pNode;
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
+            *ppSlot = pNode;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy )
+        {
+            if ( !stmm_find_or_add( tTable, (char *)Fraig_Regular(pNode->pCopy), (char ***)&ppSlot ) )
+                *ppSlot = pNode;
+            else if ( (*ppSlot)->Level > pNode->Level )
+                *ppSlot = pNode;
+        }
+    // save representatives for each node
+    vNodeReprs = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        if ( pNode->pCopy )
+        {           
+            if ( !stmm_lookup( tTable, (char *)Fraig_Regular(pNode->pCopy), (char **)&pRepr ) )
+                assert( 0 );
+            if ( pNode != pRepr )
+                Vec_PtrWriteEntry( vNodeReprs, pNode->Id, pRepr );
+        }
+    stmm_free_table( tTable );
+
+    // create the new network
+    pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc);
+
+    // perform strashing
+    Abc_AigSetNodePhases( pNtk );
+    Abc_NtkIncrementTravId( pNtk );
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodeReprs );
+
+    // finalize the network
+    Abc_NtkFinalize( pNtk, pNtkNew );
+    return pNtkNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms into AIG one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs )
+{
+    Abc_Obj_t * pRepr;
+    // skip the PIs and constants
+    if ( Abc_ObjFaninNum(pNode) < 2 )
+        return;
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    assert( Abc_ObjIsNode( pNode ) );
+    // get the node's representative
+    if ( pRepr = Vec_PtrEntry(vNodeReprs, pNode->Id) )
+    {
+        Abc_NtkFromFraig2_rec( pNtkNew, pRepr, vNodeReprs );
+        pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pRepr->fPhase ^ pNode->fPhase );
+        return;
+    }
+    Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin0(pNode), vNodeReprs );
+    Abc_NtkFromFraig2_rec( pNtkNew, Abc_ObjFanin1(pNode), vNodeReprs );
+    pNode->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
+}
 
 
 
@@ -507,7 +740,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore()
 
 //    Fraig_ManReportChoices( p );
     // transform it into FRAIG
-    pFraig = Abc_NtkFraig( pStore, &Params, 1 );
+    pFraig = Abc_NtkFraig( pStore, &Params, 1, 0 );
     if ( pFraig == NULL )
         return NULL;
     Abc_NtkDelete( pStore );
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 7e83b4f0..0f727006 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -113,6 +113,9 @@ clk = clock();
         return NULL;
     Map_ManFree( pMan );
 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index c5a9f5f3..0017a9de 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -31,6 +31,10 @@ static void        Abc_NtkMiterAddCone( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter,
 static void        Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtkMiter, int fComb );
 static void        Abc_NtkAddFrame( Abc_Ntk_t * pNetNew, Abc_Ntk_t * pNet, int iFrame, Vec_Ptr_t * vNodes );
 
+// to be exported 
+typedef void (*AddFrameMapping)( Abc_Obj_t*, Abc_Obj_t*, int, void*);
+extern Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg );
+static void        Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -598,6 +602,178 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_
 }
 
 
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the timeframes of the network.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg )
+{
+    char Buffer[100];
+    ProgressBar * pProgress;
+    Abc_Ntk_t * pNtkFrames;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pLatch, * pLatchNew;
+    int i, Counter;
+    assert( nFrames > 0 );
+    assert( Abc_NtkIsStrash(pNtk) );   
+    // start the new network
+    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames );
+    pNtkFrames->pName = util_strsav(Buffer);
+    // create new latches (or their initial values) and remember them in the new latches
+    if ( !fInitial )
+    {
+        Abc_NtkForEachLatch( pNtk, pLatch, i ) {
+            Abc_NtkDupObj( pNtkFrames, pLatch );
+            if (addFrameMapping) addFrameMapping(pLatch->pCopy, pLatch, 0, arg);
+        }
+    }
+    else
+    {
+        Counter = 0;
+        Abc_NtkForEachLatch( pNtk, pLatch, i )
+        {
+            if ( Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI
+            {
+                pLatch->pCopy = Abc_NtkCreatePi(pNtkFrames);
+                Abc_NtkLogicStoreName( pLatch->pCopy, Abc_ObjName(pLatch) );
+                Counter++;
+            }
+            else {
+                pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames->pManFunc), Abc_LatchIsInit0(pLatch) );
+            }
+ 
+            if (addFrameMapping) addFrameMapping(pLatch->pCopy, pLatch, 0, arg);
+        }
+        if ( Counter )
+            printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter );
+    }
+    
+    // create the timeframes
+    vNodes = Abc_NtkDfs( pNtk, 0 );
+    pProgress = Extra_ProgressBarStart( stdout, nFrames );
+    for ( i = 0; i < nFrames; i++ )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        Abc_NtkAddFrame2( pNtkFrames, pNtk, i, vNodes, addFrameMapping, arg );
+    }
+    Extra_ProgressBarStop( pProgress );
+    Vec_PtrFree( vNodes );
+    
+    // connect the new latches to the outputs of the last frame
+    if ( !fInitial )
+    {
+        Abc_NtkForEachLatch( pNtk, pLatch, i )
+        {
+            pLatchNew = Abc_NtkLatch(pNtkFrames, i);
+            Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
+
+            Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
+            Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
+            Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
+        }
+    }
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pLatch->pNext = NULL;
+
+    // remove dangling nodes
+    Abc_AigCleanup( pNtkFrames->pManFunc );
+    
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkFrames ) )
+    {
+        printf( "Abc_NtkFrames: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkFrames );
+        return NULL;
+    }
+    return pNtkFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one time frame to the new network.]
+
+  Description [Assumes that the latches of the old network point
+  to the outputs of the previous frame of the new network (pLatch->pCopy). 
+  In the end, updates the latches of the old network to point to the 
+  outputs of the current frame of the new network.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg )
+{
+    char Buffer[10];
+    Abc_Obj_t * pNode, * pNodeNew, * pLatch;
+    Abc_Obj_t * pConst1, * pConst1New;
+    int i;
+    // get the constant nodes
+    pConst1    = Abc_AigConst1( pNtk->pManFunc );
+    pConst1New = Abc_AigConst1( pNtkFrames->pManFunc );
+    // create the prefix to be added to the node names
+    sprintf( Buffer, "_%02d", iFrame );
+    // add the new PI nodes
+    Abc_NtkForEachPi( pNtk, pNode, i )
+    {
+        pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode );       
+        Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer );
+        if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg);
+    }
+    // add the internal nodes
+    Vec_PtrForEachEntry( vNodes, pNode, i )
+    {
+        if ( pNode == pConst1 )
+            pNodeNew = pConst1New;
+        else
+            pNodeNew = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
+        pNode->pCopy = pNodeNew;
+        if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg);
+    }
+    // add the new POs
+    Abc_NtkForEachPo( pNtk, pNode, i )
+    {
+        pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode );       
+        Abc_ObjAddFanin( pNodeNew, Abc_ObjChild0Copy(pNode) );
+        Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer );
+        if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg);
+    }
+    // transfer the implementation of the latch drivers to the latches
+
+    // it is important that these two steps are performed it two loops
+    // and not in the same loop
+    Abc_NtkForEachLatch( pNtk, pLatch, i ) 
+        pLatch->pNext = Abc_ObjChild0Copy(pLatch);
+    Abc_NtkForEachLatch( pNtk, pLatch, i ) 
+        pLatch->pCopy = pLatch->pNext;
+
+    Abc_NtkForEachLatch( pNtk, pLatch, i ) 
+    {
+        if (addFrameMapping) {
+            // don't give Mike complemented pointers because he doesn't like it
+            if (Abc_ObjIsComplement(pLatch->pCopy)) {            
+                pNodeNew = Abc_NtkCreateNode( pNtkFrames );
+                Abc_ObjAddFanin( pNodeNew, pLatch->pCopy );
+                assert(Abc_ObjFaninNum(pNodeNew) == 1);
+                pNodeNew->Level = 1 + Abc_ObjRegular(pLatch->pCopy)->Level;
+
+                pLatch->pNext = pNodeNew;
+                pLatch->pCopy = pNodeNew;
+            }
+            addFrameMapping(pLatch->pCopy, pLatch, iFrame+1, arg);
+        }
+    }
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index 8aee5014..d88e5370 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -394,6 +394,159 @@ void Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk )
     pNtk->vFuncsGlob = NULL;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the BDD of the logic cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj, * pNodeR;
+    DdManager * dd;
+    DdNode * bFunc;
+    double Result;
+    int i;
+    pNodeR = Abc_ObjRegular(pNode);
+    assert( Abc_NtkIsStrash(pNodeR->pNtk) );
+    Abc_NtkCleanCopy( pNodeR->pNtk );
+    // get the CIs in the support of the node
+    vNodes = Abc_NtkNodeSupport( pNodeR->pNtk, &pNodeR, 1 );
+    // start the manager
+    dd = Cudd_Init( Vec_PtrSize(vNodes), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    // assign elementary BDDs for the CIs
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = (Abc_Obj_t *)dd->vars[i];
+    // build the BDD of the cone
+    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR );  Cudd_Ref( bFunc );
+    bFunc = Cudd_NotCond( bFunc, pNode != pNodeR );
+    // count minterms
+    Result = Cudd_CountMinterm( dd, bFunc, dd->size );
+    // get the percentagle
+    Result *= 100.0;
+    for ( i = 0; i < dd->size; i++ )
+        Result /= 2;
+    // clean up
+    Cudd_Quit( dd );
+    Vec_PtrFree( vNodes );
+    return Result;
+}
+
+
+
+#include "reo.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Reorders BDD of the local function of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodeBddReorder( reo_man * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    DdNode * bFunc;
+    int * pOrder, i;
+    // create the temporary array for the variable order
+    pOrder = ALLOC( int, Abc_ObjFaninNum(pNode) );
+    for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
+        pOrder[i] = -1;
+    // reorder the BDD
+    bFunc = Extra_Reorder( p, pNode->pNtk->pManFunc, pNode->pData, pOrder ); Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( pNode->pNtk->pManFunc, pNode->pData );
+    pNode->pData = bFunc;
+    // update the fanin order
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        pOrder[i] = pNode->vFanins.pArray[ pOrder[i] ].iFan;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        pNode->vFanins.pArray[i].iFan = pOrder[i];
+    free( pOrder );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reorders BDDs of the local functions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose )
+{
+    reo_man * p;
+    Abc_Obj_t * pNode;
+    int i;
+    p = Extra_ReorderInit( Abc_NtkGetFaninMax(pNtk), 100 );
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        if ( Abc_ObjFaninNum(pNode) < 3 )
+            continue;
+        if ( fVerbose )
+            fprintf( stdout, "%10s: ", Abc_ObjName(pNode) );
+        if ( fVerbose )
+            fprintf( stdout, "Before = %5d  BDD nodes.  ", Cudd_DagSize(pNode->pData) );
+        Abc_NodeBddReorder( p, pNode );
+        if ( fVerbose )
+            fprintf( stdout, "After = %5d  BDD nodes.\n", Cudd_DagSize(pNode->pData) );
+    }
+    Extra_ReorderQuit( p );
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Experiment with BDD-based representation of implications.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBddImplicationTest()
+{
+    DdManager * dd;
+    DdNode * bImp, * bSum, * bTemp;
+    int nVars = 200;
+    int nImps = 200;
+    int i, clk;
+clk = clock();
+    dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Cudd_AutodynEnable( dd, CUDD_REORDER_SIFT );
+    bSum = b0;   Cudd_Ref( bSum );
+    for ( i = 0; i < nImps; i++ )
+    {
+        printf( "." );
+        bImp = Cudd_bddAnd( dd, dd->vars[rand()%nVars], dd->vars[rand()%nVars] );  Cudd_Ref( bImp );
+        bSum = Cudd_bddOr( dd, bTemp = bSum, bImp );     Cudd_Ref( bSum );
+        Cudd_RecursiveDeref( dd, bTemp );
+        Cudd_RecursiveDeref( dd, bImp );
+    }
+    printf( "The BDD before = %d.\n", Cudd_DagSize(bSum) );
+    Cudd_ReduceHeap( dd, CUDD_REORDER_SIFT, 1 );
+    printf( "The BDD after  = %d.\n", Cudd_DagSize(bSum) );
+PRT( "Time", clock() - clk );
+    Cudd_RecursiveDeref( dd, bSum );
+    Cudd_Quit( dd );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcPga.c b/src/base/abci/abcPga.c
index 5142d66b..5a115410 100644
--- a/src/base/abci/abcPga.c
+++ b/src/base/abci/abcPga.c
@@ -75,6 +75,9 @@ Abc_Ntk_t * Abc_NtkPga( Pga_Params_t * pParams )
     // make the network minimum base
     Abc_NtkMinimumBase( pNtkNew );
 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
+
     // make sure that everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 2e9c3cc8..aff31f4c 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -499,6 +499,33 @@ void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode )
     fprintf( pFile, "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Prints the factored form of one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NodePrintKMap( Abc_Obj_t * pNode, int fUseRealNames )
+{
+    Vec_Ptr_t * vNamesIn;
+    if ( fUseRealNames )
+    {
+        vNamesIn = Abc_NodeGetFaninNames(pNode);
+        Extra_PrintKMap( stdout, pNode->pNtk->pManFunc, pNode->pData, Cudd_Not(pNode->pData), 
+            Abc_ObjFaninNum(pNode), NULL, 0, (char **)vNamesIn->pArray );
+        Abc_NodeFreeNames( vNamesIn );
+    }
+    else
+        Extra_PrintKMap( stdout, pNode->pNtk->pManFunc, pNode->pData, Cudd_Not(pNode->pData), 
+            Abc_ObjFaninNum(pNode), NULL, 0, NULL );
+
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 3871b52c..672fd376 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -91,6 +91,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
     }
 //printf( "Maximum fanin = %d.\n", Abc_NtkGetFaninMax(pNtkNew) );
 
+    if ( pNtk->pExdc )
+        pNtkNew->pExdc = Abc_NtkDup( pNtk->pExdc );
     // make sure everything is okay
     if ( !Abc_NtkCheck( pNtkNew ) )
     {
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 8059f222..93f534ce 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -71,7 +71,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
         printf( "Cleanup has removed %d nodes.\n", nNodes );
     // duplicate EXDC 
     if ( pNtk->pExdc )
-        pNtkAig->pExdc = Abc_NtkStrash( pNtk->pExdc, 0, 1 );
+        pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
     // make sure everything is okay
     if ( !Abc_NtkCheck( pNtkAig ) )
     {
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index fa840937..62cd5b55 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -25,10 +25,11 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static stmm_table *   Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose );
+static void           Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
+static stmm_table *   Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose );
 static void           Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv, bool fVerbose );
-static void           Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv );
-static void           Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv );
+static void           Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
+static void           Abc_NtkFraigMergeClass( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUseInv, int fVerbose );
 static int            Abc_NodeDroppingCost( Abc_Obj_t * pNode );
 
 static void           Abc_NodeSweep( Abc_Obj_t * pNode, int fVerbose );
@@ -52,7 +53,7 @@ static void           Abc_NodeComplementInput( Abc_Obj_t * pNode, Abc_Obj_t * pF
   SeeAlso     []
 
 ***********************************************************************/
-bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
+bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose )
 {
     Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig;
@@ -63,11 +64,24 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
 
     // derive the AIG
     pNtkAig = Abc_NtkStrash( pNtk, 0, 1 );
+
     // perform fraiging of the AIG
     Fraig_ParamsSetDefault( &Params );
-    pMan = Abc_NtkToFraig( pNtkAig, &Params, 0 );    
+    pMan = Abc_NtkToFraig( pNtkAig, &Params, 0, 0 );   
+    // cannot use EXDC with FRAIG because it can create classes of equivalent FRAIG nodes
+    // with representative nodes that do not correspond to the nodes with the current network
+
+    // update FRAIG using EXDC
+    if ( fExdc )
+    {
+        if ( pNtk->pExdc == NULL )
+            printf( "Warning: Networks has no EXDC.\n" );
+        else
+            Abc_NtkFraigSweepUsingExdc( pMan, pNtk );
+    }
+
     // collect the classes of equivalent nets
-    tEquiv = Abc_NtkFraigEquiv( pMan, pNtk, fUseInv, fVerbose );
+    tEquiv = Abc_NtkFraigEquiv( pNtk, fUseInv, fVerbose );
 
     // transform the network into the equivalent one
     Abc_NtkFraigTransform( pNtk, tEquiv, fUseInv, fVerbose );
@@ -90,6 +104,47 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
 
 /**Function*************************************************************
 
+  Synopsis    [Sweep the network using EXDC.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkFraigSweepUsingExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk )
+{
+    Fraig_Node_t * gNodeExdc, * gNode, * gNodeRes;
+    Abc_Obj_t * pNode, * pNodeAig;
+    int i;
+    extern Fraig_Node_t * Abc_NtkToFraigExdc( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkExdc );
+
+    assert( pNtk->pExdc );
+    // derive FRAIG node representing don't-cares in the EXDC network
+    gNodeExdc = Abc_NtkToFraigExdc( pMan, pNtk, pNtk->pExdc );
+    // update the node pointers
+    Abc_NtkForEachNode( pNtk, pNode, i )
+    {
+        // skip the constant input nodes
+        if ( Abc_ObjFaninNum(pNode) == 0 )
+            continue;
+        // get the strashed node
+        pNodeAig = pNode->pCopy;
+        // skip the dangling nodes
+        if ( pNodeAig == NULL )
+            continue;
+        // get the FRAIG node
+        gNode = Fraig_NotCond( Abc_ObjRegular(pNodeAig)->pCopy, Abc_ObjIsComplement(pNodeAig) );
+        // perform ANDing with EXDC
+        gNodeRes = Fraig_NodeAnd( pMan, gNode, Fraig_Not(gNodeExdc) );
+        // write the node back
+        Abc_ObjRegular(pNodeAig)->pCopy = (Abc_Obj_t *)Fraig_NotCond( gNodeRes, Abc_ObjIsComplement(pNodeAig) );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Collects equivalence classses of node in the network.]
 
   Description []
@@ -99,7 +154,7 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-stmm_table * Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose )
+stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose )
 {
     Abc_Obj_t * pList, * pNode, * pNodeAig;
     Fraig_Node_t * gNode;
@@ -113,14 +168,14 @@ stmm_table * Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv,
     tStrash2Net = stmm_init_table(stmm_ptrcmp,stmm_ptrhash);
     Abc_NtkForEachNode( pNtk, pNode, c )
     {
+        // skip the constant input nodes
+        if ( Abc_ObjFaninNum(pNode) == 0 )
+            continue;
         // get the strashed node
         pNodeAig = pNode->pCopy;
         // skip the dangling nodes
         if ( pNodeAig == NULL )
             continue;
-        // skip the constant input nodes
-        if ( Abc_ObjFaninNum(pNode) == 0 )
-            continue;
         // skip the nodes that fanout into POs
         if ( Abc_NodeHasUniqueCoFanout(pNode) )
             continue;
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index 182d688d..e932d076 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -87,6 +87,8 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
     // allocate ZDD variables
     Cudd_zddVarsFromBddVars( dd, 2 );
     // create the EXDC network representing the unreachable states
+    if ( pNtk->pExdc )
+        Abc_NtkDelete( pNtk->pExdc );
     pNtk->pExdc = Abc_NtkConstructExdc( dd, pNtk, bUnreach );
     Cudd_RecursiveDeref( dd, bUnreach );
     Extra_StopManager( dd );
@@ -283,9 +285,13 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
 
     // start the new network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    pNtkNew->pName = util_strsav("exdc");
+    pNtkNew->pSpec = NULL;
+
     // create PIs corresponding to LOs
     Abc_NtkForEachLatch( pNtk, pNode, i )
-        pNode->pCopy = Abc_NtkCreatePi(pNtkNew);
+        Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode) );
+    // cannot ADD POs here because pLatch->pCopy point to the PIs
 
     // create a new node
     pNodeNew = Abc_NtkCreateNode(pNtkNew);
@@ -304,21 +310,22 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     free( pPermute );
     Abc_NodeMinimumBase( pNodeNew );
 
-    // make the new node drive all the COs
-    Abc_NtkForEachCo( pNtk, pNode, i )
-        Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pNodeNew );
-
-    // store the PI names of the EXDC network
+    // for each CO, create PO (skip POs equal to CIs because of name conflict)
+    Abc_NtkForEachPo( pNtk, pNode, i )
+        if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
+            Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode) );
     Abc_NtkForEachLatch( pNtk, pNode, i )
-        Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i), Abc_ObjName(pNode) );
-    // store the PO names of the EXDC network
+        Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pNode, "_in") );
+
+    // link to the POs of the network 
     Abc_NtkForEachPo( pNtk, pNode, i )
-        Abc_NtkLogicStoreName( Abc_NtkPo(pNtkNew,i), Abc_ObjName(pNode) );
+        if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) )
+            Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
     Abc_NtkForEachLatch( pNtk, pNode, i )
-        Abc_NtkLogicStoreName( Abc_NtkCo(pNtkNew,Abc_NtkPoNum(pNtk) + i), Abc_ObjNameSuffix(pNode, "_in") );
+        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
 
-    // make the network minimum base
-    Abc_NtkMinimumBase( pNtkNew );
+    // remove the extra nodes
+    Abc_AigCleanup( pNtkNew->pManFunc );
 
     // fix the problem with complemented and duplicated CO edges
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c
new file mode 100644
index 00000000..d0179514
--- /dev/null
+++ b/src/base/abci/abcVanEijk.c
@@ -0,0 +1,789 @@
+/**CFile****************************************************************
+
+  FileName    [abcVanEijk.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Implementation of van Eijk's method for finding
+  signal correspondence: C. A. J. van Eijk. "Sequential equivalence 
+  checking based on structural similarities", IEEE Trans. CAD, 
+  vol. 19(7), July 2000, pp. 814-819.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - October 2, 2005.]
+
+  Revision    [$Id: abcVanEijk.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "fraig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static Vec_Ptr_t *    Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+static Vec_Ptr_t *    Abc_NtkVanEijkClassesDeriveBase( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames );
+static Vec_Ptr_t *    Abc_NtkVanEijkClassesDeriveFirst( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame );
+static int            Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame, Vec_Ptr_t * vClasses );
+static void           Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses );
+static int            Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses );
+static void           Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses );
+static Abc_Ntk_t *    Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames );
+static void           Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames );
+static Fraig_Man_t *  Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit );
+static Abc_Ntk_t *    Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses );
+
+////////////////////////////////////////////////////////////////////////
+///                     INLINED FUNCTIONS                            ///
+////////////////////////////////////////////////////////////////////////
+
+// sets the correspondence of the node in the frame
+static inline void        Abc_NodeVanEijkWriteCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame, Abc_Obj_t * pEntry ) 
+{
+    Vec_PtrWriteEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id, pEntry ); 
+}
+// returns the correspondence of the node in the frame
+static inline Abc_Obj_t * Abc_NodeVanEijkReadCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) 
+{
+    return Vec_PtrEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id ); 
+}
+// returns the hash value of the node in the frame
+static inline Abc_Obj_t * Abc_NodeVanEijkHash( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) 
+{
+    return Abc_ObjRegular( Abc_NodeVanEijkReadCorresp(pNode, vCorresp, iFrame)->pCopy );  
+}
+// returns the representative node of the class to which the node belongs
+static inline Abc_Obj_t * Abc_NodeVanEijkRepr( Abc_Obj_t * pNode ) 
+{
+    if ( pNode->pNext == NULL )
+        return NULL;
+    while ( pNode->pNext )   
+        pNode = pNode->pNext;
+    return pNode;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derives classes of sequentially equivalent nodes.]
+
+  Description [Performs sequential sweep by combining the equivalent
+  nodes. Adds EXDC network to the current network to record the subset
+  of unreachable states computed by identifying the equivalent nodes.]
+               
+  SideEffects []
+ 
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose )
+{
+    Fraig_Params_t Params;
+    Abc_Ntk_t * pNtkSingle;
+    Vec_Ptr_t * vClasses;
+    Abc_Ntk_t * pNtkNew;
+
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // FRAIG the network to get rid of combinational equivalences
+    Fraig_ParamsSetDefaultFull( &Params );
+    pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 );
+    Abc_AigSetNodePhases( pNtkSingle );
+
+    // get the equivalence classes
+    vClasses = Abc_NtkVanEijkClasses( pNtkSingle, nFrames, fVerbose );
+    if ( Vec_PtrSize(vClasses) > 0 )
+    {
+        // transform the network by merging nodes in the equivalence classes
+        pNtkNew = Abc_NtkVanEijkFrames( pNtkSingle, NULL, 1, 0, 1 );
+//        pNtkNew = Abc_NtkDup( pNtkSingle );  
+        // derive the EXDC network if asked
+        if ( fExdc )
+            pNtkNew->pExdc = Abc_NtkVanEijkDeriveExdc( pNtk, pNtkSingle, vClasses );
+    }
+    else
+        pNtkNew = Abc_NtkDup( pNtkSingle );  
+    Abc_NtkVanEijkClassesTest( pNtkSingle, vClasses );
+    Vec_PtrFree( vClasses );
+
+    Abc_NtkDelete( pNtkSingle );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the classes of sequentially equivalent nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVerbose )
+{
+    Fraig_Man_t * pFraig;
+    Abc_Ntk_t * pNtkMulti;
+    Vec_Ptr_t * vCorresp, * vClasses;
+    int nIter, RetValue;
+
+    if ( fVerbose )
+        printf( "The number of ANDs after FRAIGing = %d.\n", Abc_NtkNodeNum(pNtkSingle) );
+
+    // get the AIG of the base case
+    vCorresp = Vec_PtrAlloc( 100 );
+    Abc_NtkCleanNext(pNtkSingle);
+    pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 0, 0 );
+    if ( fVerbose )
+        printf( "The number of ANDs in %d timeframes = %d.\n", nFrames, Abc_NtkNodeNum(pNtkMulti) );
+
+    // FRAIG the initialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys)
+    pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 1 );
+    Fraig_ManFree( pFraig );
+
+    // find initial equivalence classes
+    vClasses = Abc_NtkVanEijkClassesDeriveBase( pNtkSingle, vCorresp, nFrames );
+    if ( fVerbose )
+        printf( "The number of classes in the base case    = %5d.  Pairs = %8d.\n", Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) );
+    Abc_NtkDelete( pNtkMulti );
+
+    // refine the classes using iterative FRAIGing
+    for ( nIter = 1; Vec_PtrSize(vClasses) > 0; nIter++ )
+    {
+        // derive the network with equivalence classes
+        Abc_NtkVanEijkClassesOrder( vClasses );
+        pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 1, 0 );
+        // simulate with classes (TO DO)
+
+        // FRAIG the unitialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys)
+        pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 0 );
+        Fraig_ManFree( pFraig );
+
+        // refine the classes
+        RetValue = Abc_NtkVanEijkClassesRefine( pNtkSingle, vCorresp, nFrames, vClasses );
+        Abc_NtkDelete( pNtkMulti );
+        if ( fVerbose )
+            printf( "The number of classes after %2d iterations = %5d.  Pairs = %8d.\n", nIter, Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) );
+        // quit if there is no change
+        if ( RetValue == 0 )
+            break;
+    }
+    Vec_PtrFree( vCorresp );
+
+    if ( fVerbose )
+    {
+        Abc_Obj_t * pObj, * pClass;
+        int i, Counter;
+        printf( "The classes are: " );
+        Vec_PtrForEachEntry( vClasses, pClass, i )
+        {
+            Counter = 0;
+            for ( pObj = pClass; pObj; pObj = pObj->pNext )
+                Counter++;
+            printf( " %d", Counter );
+        }
+        printf( "\n" );
+    }
+    return vClasses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the equivalence classes of nodes using the base case.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveBase( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vCorresp, int nFrames )
+{
+    Vec_Ptr_t * vClasses;
+    int i, RetValue;
+    // derive the classes for the last frame
+    vClasses = Abc_NtkVanEijkClassesDeriveFirst( pNtkSingle, vCorresp, nFrames - 1 );
+    // refine the classes using other timeframes
+    for ( i = 0; i < nFrames - 1; i++ )
+    {
+        if ( Vec_PtrSize(vClasses) == 0 )
+            break;
+        RetValue = Abc_NtkVanEijkClassesRefine( pNtkSingle, vCorresp, i, vClasses );
+//        if ( RetValue )
+//            printf( " yes%s", (i==nFrames-2 ? "\n":"") );
+//        else
+//            printf( " no%s", (i==nFrames-2 ? "\n":"") );
+    }
+    return vClasses;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the equivalence classes of nodes.]
+
+  Description [Original network (pNtk) is mapped into the unfolded frames 
+  using given array of nodes (vCorresp). Each node in the unfolded frames 
+  is mapped into a FRAIG node (pNode->pCopy). This procedure uses next 
+  pointers (pNode->pNext) to combine the nodes into equivalence classes.
+  Each class is represented by its representative node with the minimum level.
+  Only the last frame is considered.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveFirst( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame )
+{
+    Abc_Obj_t * pNode, * pKey, ** ppSlot;
+    stmm_table * tTable;
+    stmm_generator * gen;
+    Vec_Ptr_t * vClasses;
+    int i;
+    // start the table hashing FRAIG nodes into classes of original network nodes
+    tTable = stmm_init_table( st_ptrcmp, st_ptrhash );
+    // create the table
+    Abc_NtkCleanNext( pNtk );
+    Abc_NtkForEachObj( pNtk, pNode, i )
+    {
+        if ( Abc_ObjIsPo(pNode) )
+            continue;
+        pKey = Abc_NodeVanEijkHash( pNode, vCorresp, iFrame );
+        if ( !stmm_find_or_add( tTable, (char *)pKey, (char ***)&ppSlot ) )
+            *ppSlot = NULL;
+        pNode->pNext = *ppSlot;
+        *ppSlot = pNode;
+    }
+    // collect only non-trivial classes
+    vClasses = Vec_PtrAlloc( 100 );
+    stmm_foreach_item( tTable, gen, (char **)&pKey, (char **)&pNode )
+        if ( pNode->pNext )
+            Vec_PtrPush( vClasses, pNode );
+    stmm_free_table( tTable );
+    return vClasses;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Refines the classes using one frame.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame, Vec_Ptr_t * vClasses )
+{
+    Abc_Obj_t * pHeadSame, ** ppTailSame;
+    Abc_Obj_t * pHeadDiff, ** ppTailDiff;
+    Abc_Obj_t * pNode, * pClass, * pKey;
+    int i, k, fChange = 0;
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+    {
+//        assert( pClass->pNext );
+        pKey = Abc_NodeVanEijkHash( pClass, vCorresp, iFrame );
+        for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext )
+            if ( Abc_NodeVanEijkHash(pNode, vCorresp, iFrame) != pKey )
+                break;
+        if ( pNode == NULL )
+            continue;
+        fChange = 1;
+        // create two classes
+        pHeadSame = NULL; ppTailSame = &pHeadSame;
+        pHeadDiff = NULL; ppTailDiff = &pHeadDiff;
+        for ( pNode = pClass; pNode; pNode = pNode->pNext )
+            if ( Abc_NodeVanEijkHash(pNode, vCorresp, iFrame) != pKey )
+                *ppTailDiff = pNode, ppTailDiff = &pNode->pNext;
+            else
+                *ppTailSame = pNode, ppTailSame = &pNode->pNext;
+        *ppTailSame = NULL;
+        *ppTailDiff = NULL;
+        assert( pHeadSame && pHeadDiff );
+        // put the updated class back
+        Vec_PtrWriteEntry( vClasses, i, pHeadSame );
+        // append the new class to be processed later
+        Vec_PtrPush( vClasses, pHeadDiff );
+    }
+    // remove trivial classes
+    k = 0;
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+        if ( pClass->pNext )
+            Vec_PtrWriteEntry( vClasses, k++, pClass );
+    Vec_PtrShrink( vClasses, k );
+    return fChange;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Orders nodes in the equivalence classes.]
+
+  Description [Finds a min-level representative of each class and puts it last.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses )
+{
+    Abc_Obj_t * pClass, * pNode, * pPrev, * pNodeMin, * pPrevMin;
+    int i;
+    // go through the classes
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+    {
+        assert( pClass->pNext );
+        pPrevMin = NULL;
+        pNodeMin = pClass;
+        for ( pPrev = pClass, pNode = pClass->pNext; pNode; pPrev = pNode, pNode = pNode->pNext )
+            if ( pNodeMin->Level >= pNode->Level )
+            {
+                pPrevMin = pPrev;
+                pNodeMin = pNode;
+            }
+        if ( pNodeMin->pNext == NULL ) // already last
+            continue;
+        // update the class
+        if ( pNodeMin == pClass )
+            Vec_PtrWriteEntry( vClasses, i, pNodeMin->pNext );
+        else
+            pPrevMin->pNext = pNodeMin->pNext;
+        // attach the min node
+        assert( pPrev->pNext == NULL );
+        pPrev->pNext = pNodeMin;
+        pNodeMin->pNext = NULL;
+    }
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+        assert( pClass->pNext );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Counts pairs of equivalent nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses ) 
+{
+    Abc_Obj_t * pClass, * pNode;
+    int i, nPairs = 0;
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+    {
+        assert( pClass->pNext );
+        for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext )
+            nPairs++;
+    }
+    return nPairs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sanity check for the class representation.]
+
+  Description [Checks that pNode->pNext is only used in the classes.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses )
+{
+    Abc_Obj_t * pClass, * pObj;
+    int i;
+    Abc_NtkCleanCopy( pNtkSingle );
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+        for ( pObj = pClass; pObj; pObj = pObj->pNext )
+            if ( pObj->pNext )
+                pObj->pCopy = (Abc_Obj_t *)1;
+    Abc_NtkForEachObj( pNtkSingle, pObj, i )
+        assert( (pObj->pCopy != NULL) == (pObj->pNext != NULL) );
+    Abc_NtkCleanCopy( pNtkSingle );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs DFS for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanEijkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes )
+{
+    Abc_Obj_t * pRepr;
+    // skip CI and const
+    if ( Abc_ObjFaninNum(pNode) < 2 )
+        return;
+    // if this node is already visited, skip
+    if ( Abc_NodeIsTravIdCurrent( pNode ) )
+        return;
+    // mark the node as visited
+    Abc_NodeSetTravIdCurrent( pNode );
+    assert( Abc_ObjIsNode( pNode ) );
+    // check if the node belongs to the class
+    if ( pRepr = Abc_NodeVanEijkRepr(pNode) )
+        Abc_NtkVanEijkDfs_rec( pRepr, vNodes );
+    else
+    {
+        Abc_NtkVanEijkDfs_rec( Abc_ObjFanin0(pNode), vNodes );
+        Abc_NtkVanEijkDfs_rec( Abc_ObjFanin1(pNode), vNodes );
+    }
+    // add the node after the fanins have been added
+    Vec_PtrPush( vNodes, pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds DFS ordering of nodes using equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkVanEijkDfs( Abc_Ntk_t * pNtk )
+{
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i;
+    vNodes = Vec_PtrAlloc( 100 );
+    Abc_NtkIncrementTravId( pNtk );
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Abc_NtkVanEijkDfs_rec( Abc_ObjFanin0(pObj), vNodes );
+    return vNodes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the timeframes of the network.]
+
+  Description [Returns mapping of the orig nodes into the frame nodes (vCorresp).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames )
+{
+    char Buffer[100];
+    Abc_Ntk_t * pNtkFrames;
+    Abc_Obj_t * pLatch, * pLatchNew;
+    Vec_Ptr_t * vOrder;
+    int i;
+    assert( nFrames > 0 );
+    assert( Abc_NtkIsStrash(pNtk) );
+    assert( Abc_NtkIsDfsOrdered(pNtk) );
+    // clean the array of connections
+    if ( vCorresp )
+        Vec_PtrFill( vCorresp, (nFrames + fAddLast)*Abc_NtkObjNumMax(pNtk), NULL );
+    // start the new network
+    pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG );
+    if ( fShortNames )
+    {
+        pNtkFrames->pName = util_strsav(pNtk->pName);
+        pNtkFrames->pSpec = util_strsav(pNtk->pSpec);
+    }
+    else
+    {
+        sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames + fAddLast );
+        pNtkFrames->pName = util_strsav(Buffer);
+    }
+    // map the constant nodes
+    Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkFrames->pManFunc);
+    // create new latches and remember them in the new latches
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        Abc_NtkDupObj( pNtkFrames, pLatch );
+    // collect nodes in such a way each class representative goes first
+    vOrder = Abc_NtkVanEijkDfs( pNtk );
+    // create the timeframes
+    for ( i = 0; i < nFrames; i++ )
+        Abc_NtkVanEijkAddFrame( pNtkFrames, pNtk, i, vCorresp, vOrder, fShortNames );
+    Vec_PtrFree( vOrder );
+    // add one more timeframe without class info
+    if ( fAddLast )
+        Abc_NtkVanEijkAddFrame( pNtkFrames, pNtk, nFrames, vCorresp, NULL, fShortNames );
+    // connect the new latches to the outputs of the last frame
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+    {
+        pLatchNew = Abc_NtkLatch(pNtkFrames, i);
+        Abc_ObjAddFanin( pLatchNew, pLatch->pCopy );
+        Vec_PtrPush( pNtkFrames->vCis, pLatchNew );
+        Vec_PtrPush( pNtkFrames->vCos, pLatchNew );
+        Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) );
+        pLatch->pNext = NULL;
+    }
+    // remove dangling nodes
+    Abc_AigCleanup( pNtkFrames->pManFunc );
+    // make sure that everything is okay
+    if ( !Abc_NtkCheck( pNtkFrames ) )
+        printf( "Abc_NtkVanEijkFrames: The network check has failed.\n" );
+    return pNtkFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds one time frame to the new network.]
+
+  Description [If the ordering of nodes is given, uses it. Otherwise, 
+  uses the DSF order of the nodes in the network.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames )
+{
+    char Buffer[10];
+    Abc_Obj_t * pNode, * pLatch, * pRepr;
+    Vec_Ptr_t * vTemp;
+    int i;
+    // create the prefix to be added to the node names
+    sprintf( Buffer, "_%02d", iFrame );
+    // add the new PI nodes
+    Abc_NtkForEachPi( pNtk, pNode, i )
+    {
+        pNode->pCopy = Abc_NtkCreatePi(pNtkFrames);       
+        if ( fShortNames )
+            Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) );
+        else         
+            Abc_NtkLogicStoreNamePlus( pNode->pCopy, Abc_ObjName(pNode), Buffer );
+    }
+    // remember the CI mapping 
+    if ( vCorresp )
+    {
+        pNode = Abc_AigConst1(pNtk->pManFunc);
+        Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) );
+        Abc_NtkForEachCi( pNtk, pNode, i )
+            Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) );
+    }
+    // go through the nodes in the given order or in the natural order
+    if ( vOrder )
+    {
+        // add the internal nodes
+        Vec_PtrForEachEntry( vOrder, pNode, i )
+        {
+            if ( pRepr = Abc_NodeVanEijkRepr(pNode) )
+                pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pNode->fPhase ^ pRepr->fPhase );
+            else
+                pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
+            assert( Abc_ObjRegular(pNode->pCopy) != NULL );
+            if ( vCorresp )
+                Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) );
+        }
+    }
+    else
+    {
+        // add the internal nodes
+        Abc_AigForEachAnd( pNtk, pNode, i )
+        {
+            pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) );
+            assert( Abc_ObjRegular(pNode->pCopy) != NULL );
+            if ( vCorresp )
+                Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) );
+        }
+    }
+    // add the new POs
+    Abc_NtkForEachPo( pNtk, pNode, i )
+    {
+        pNode->pCopy = Abc_NtkCreatePo(pNtkFrames);       
+        Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) );
+        if ( fShortNames )
+            Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) );
+        else         
+            Abc_NtkLogicStoreNamePlus( pNode->pCopy, Abc_ObjName(pNode), Buffer );
+    }
+    // transfer the implementation of the latch drivers to the latches
+    vTemp = Vec_PtrAlloc( 100 );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        Vec_PtrPush( vTemp, Abc_ObjChild0Copy(pLatch) );
+    Abc_NtkForEachLatch( pNtk, pLatch, i )
+        pLatch->pCopy = Vec_PtrEntry( vTemp, i );
+    Vec_PtrFree( vTemp );
+
+    Abc_AigForEachAnd( pNtk, pNode, i )
+        pNode->pCopy = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Fraigs the network with or without initialization.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit )
+{
+    Fraig_Man_t * pMan;
+    Fraig_Params_t Params;
+    ProgressBar * pProgress;
+    Abc_Obj_t * pNode;
+    int i;
+    assert( Abc_NtkIsStrash(pMulti) );
+    // create the FRAIG manager
+    Fraig_ParamsSetDefaultFull( &Params );
+    pMan = Fraig_ManCreate( &Params );
+    // clean the copy fields in the old network
+    Abc_NtkCleanCopy( pMulti );
+    // map the constant nodes
+    Abc_AigConst1(pMulti->pManFunc)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan);
+    if ( fInit )
+    {
+        // map the PI nodes
+        Abc_NtkForEachPi( pMulti, pNode, i )
+            pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
+        // map the latches
+        Abc_NtkForEachLatch( pMulti, pNode, i )
+           pNode->pCopy = (Abc_Obj_t *)Fraig_NotCond( Fraig_ManReadConst1(pMan), !Abc_LatchIsInit1(pNode) );
+    }
+    else
+    {
+        // map the CI nodes
+        Abc_NtkForEachCi( pMulti, pNode, i )
+            pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i);
+    }
+    // perform fraiging
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pMulti) );
+    Abc_AigForEachAnd( pMulti, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, 
+                Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ),
+                Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) );
+    }
+    Extra_ProgressBarStop( pProgress );
+    return pMan;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Create EXDC from the equivalence classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtkInit, Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pClass, * pNode, * pRepr, * pObj;
+    Abc_Obj_t * pMiter, * pTotal;
+    Vec_Ptr_t * vCone;
+    int i, k;
+
+    // start the network
+    pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc );
+    pNtkNew->pName = util_strsav("exdc");
+    pNtkNew->pSpec = NULL;
+
+    // map the constant nodes
+    Abc_AigConst1(pNtk->pManFunc)->pCopy = Abc_AigConst1(pNtkNew->pManFunc);
+    // for each CI, create PI
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName( Abc_NtkCi(pNtkInit,i) ) );
+    // cannot add latches here because pLatch->pCopy pointers are used
+
+    // create the cones for each pair of nodes in an equivalence class
+    pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew->pManFunc) );
+    Vec_PtrForEachEntry( vClasses, pClass, i )
+    {
+        assert( pClass->pNext );
+        // get the cone for the representative node
+        pRepr = Abc_NodeVanEijkRepr( pClass );
+        if ( Abc_ObjFaninNum(pRepr) == 2 )
+        {
+            vCone = Abc_NtkDfsNodes( pNtk, &pRepr, 1 );
+            Vec_PtrForEachEntry( vCone, pObj, k )
+                pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+            Vec_PtrFree( vCone );
+            assert( pObj == pRepr );
+        }
+        // go through the node pairs (representative is last in the list)
+        for ( pNode = pClass; pNode != pRepr; pNode = pNode->pNext )
+        {
+            // get the cone for the node
+            assert( Abc_ObjFaninNum(pNode) == 2 );
+            vCone = Abc_NtkDfsNodes( pNtk, &pNode, 1 );
+            Vec_PtrForEachEntry( vCone, pObj, k )
+                pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+            Vec_PtrFree( vCone );
+            assert( pObj == pNode );
+            // complement if there is phase difference
+            pNode->pCopy = Abc_ObjNotCond( pNode->pCopy, pNode->fPhase ^ pRepr->fPhase );
+            // add the miter
+            pMiter = Abc_AigXor( pNtkNew->pManFunc, pRepr->pCopy, pNode->pCopy );
+        }
+        // add the miter to the final
+        pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter );
+    }
+
+    // for each CO, create PO (skip POs equal to CIs because of name conflict)
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) )
+            Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName( Abc_NtkPo(pNtkInit,i) ) );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( Abc_NtkLatch(pNtkInit,i), "_in") );
+
+    // link to the POs of the network
+    Abc_NtkForEachPo( pNtk, pObj, i )
+        if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) )
+            Abc_ObjAddFanin( pObj->pCopy, pTotal );
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_ObjAddFanin( pObj->pCopy, pTotal );
+
+    // remove the extra nodes
+    Abc_AigCleanup( pNtkNew->pManFunc );
+
+    // check the result
+    if ( !Abc_NtkCheck( pNtkNew ) )
+    {
+        printf( "Abc_NtkVanEijkDeriveExdc: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkNew );
+        return NULL;
+    }
+    return pNtkNew;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 2d5493ea..08a54e80 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -60,12 +60,12 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds )
     RetValue = Abc_NtkMiterIsConstant( pMiter );
     if ( RetValue == 0 )
     {
-        Abc_NtkDelete( pMiter );
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter );
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
         FREE( pMiter->pModel );
+        Abc_NtkDelete( pMiter );
         return;
     }
     if ( RetValue == 1 )
@@ -127,18 +127,18 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     RetValue = Abc_NtkMiterIsConstant( pMiter );
     if ( RetValue == 0 )
     {
-        Abc_NtkDelete( pMiter );
         printf( "Networks are NOT EQUIVALENT after structural hashing.\n" );
         // report the error
         pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter );
         Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel );
         FREE( pMiter->pModel );
+        Abc_NtkDelete( pMiter );
         return;
     }
     if ( RetValue == 1 )
     {
-        Abc_NtkDelete( pMiter );
         printf( "Networks are equivalent after structural hashing.\n" );
+        Abc_NtkDelete( pMiter );
         return;
     }
 
@@ -146,7 +146,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV
     Fraig_ParamsSetDefault( &Params );
     Params.fVerbose = fVerbose;
     Params.nSeconds = nSeconds;
-    pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); 
+    pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
     Fraig_ManProveMiter( pMan );
 
     // analyze the result
@@ -315,7 +315,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF
     Fraig_ParamsSetDefault( &Params );
     Params.fVerbose = fVerbose;
     Params.nSeconds = nSeconds;
-    pMan = Abc_NtkToFraig( pFrames, &Params, 0 ); 
+    pMan = Abc_NtkToFraig( pFrames, &Params, 0, 0 ); 
     Fraig_ManProveMiter( pMan );
 
     // analyze the result
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 0123e213..4466cf99 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -22,4 +22,5 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcSymm.c \
     src/base/abci/abcTiming.c \
     src/base/abci/abcUnreach.c \
+    src/base/abci/abcVanEijk.c \
     src/base/abci/abcVerify.c 
diff --git a/src/base/abcs/module.make b/src/base/abcs/module.make
index 309a8871..e8d5a8db 100644
--- a/src/base/abcs/module.make
+++ b/src/base/abcs/module.make
@@ -1,4 +1,6 @@
-SRC +=    src/base/abcs/abcRetCore.c \
+SRC +=    src/base/abcs/abcFpgaDelay.c \
+    src/base/abcs/abcFpgaSeq.c \
+    src/base/abcs/abcRetCore.c \
     src/base/abcs/abcRetDelay.c \
     src/base/abcs/abcRetImpl.c \
     src/base/abcs/abcRetUtil.c \
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 2f7bd229..bffdfc10 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -32,6 +32,7 @@ static int IoCommandReadEdif    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEqn     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadPla     ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadTruth   ( Abc_Frame_t * pAbc, int argc, char **argv );
 
 static int IoCommandWriteBlif   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteBench  ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -65,6 +66,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_eqn",      IoCommandReadEqn,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_verilog",  IoCommandReadVerilog,  1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_pla",      IoCommandReadPla,      1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_truth",    IoCommandReadTruth,    1 );
 
     Cmd_CommandAdd( pAbc, "I/O", "write_blif",    IoCommandWriteBlif,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_bench",   IoCommandWriteBench,   0 );
@@ -643,6 +645,76 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk;
+    char * pSopCover;
+    int fHex;
+    int c;
+
+    fHex = 0;
+    util_getopt_reset();
+    while ( ( c = util_getopt( argc, argv, "xh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'x':
+                fHex ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    if ( argc != util_optind + 1 )
+    {
+        goto usage;
+    }
+
+    // convert truth table to SOP
+    if ( fHex )
+        pSopCover = Abc_SopFromTruthHex(argv[util_optind]);
+    else
+        pSopCover = Abc_SopFromTruthBin(argv[util_optind]);
+    if ( pSopCover == NULL )
+    {
+        fprintf( pAbc->Err, "Reading truth table has failed.\n" );
+        return 1;
+    }
+
+    pNtk = Abc_NtkCreateWithNode( pSopCover );
+    free( pSopCover );
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Err, "Deriving the network has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_truth [-xh] <truth>\n" );
+    fprintf( pAbc->Err, "\t         creates network with node having given truth table\n" );
+    fprintf( pAbc->Err, "\t-x     : toggles between bin and hex representation [default = %s]\n", fHex? "hex":"bin" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\ttruth  : truth table with most signficant bit first (e.g. 1000 for AND(a,b))\n" );
+    return 1;
+}
+
 
 /**Function*************************************************************
 
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index 09824f38..5235d9a1 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -60,7 +60,7 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName )
     // create solver with clauses
     pSat = Abc_NtkMiterSatCreate( pNtk );
     // write the clauses
-    Asat_SolverWriteDimacs( pSat, pFileName );
+    Asat_SolverWriteDimacs( pSat, pFileName, 0, 0, 1 );
     // free the solver
     solver_delete( pSat );
     return 1;
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 839aa0b4..bb776ab7 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -106,7 +106,7 @@ typedef unsigned long long uint64;
 /*     Various Utilities                                                     */
 /*===========================================================================*/
 
-/*=== extraUtilBdd.c ========================================================*/
+/*=== extraBddMisc.c ========================================================*/
 extern DdNode *     Extra_TransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );
 extern DdNode *     Extra_TransferLevelByLevel( DdManager * ddSource, DdManager * ddDestination, DdNode * f );
 extern DdNode *     Extra_bddRemapUp( DdManager * dd, DdNode * bF );
@@ -125,6 +125,14 @@ extern int *        Extra_VectorSupportArray( DdManager * dd, DdNode ** F, int n
 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 );
+extern DdNode *     Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst );
+
+/*=== extraBddKmap.c ================================================================*/
+
+/* displays the Karnaugh Map of a function */
+extern void        Extra_PrintKMap( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nVars, DdNode ** XVars, int fSuppType, char ** pVarNames );
+/* displays the Karnaugh Map of a relation */
+extern void        Extra_PrintKMapRelation( FILE * pFile, DdManager * dd, DdNode * OnSet, DdNode * OffSet, int nXVars, int nYVars, DdNode ** XVars, DdNode ** YVars );
 
 /*=== extraBddSymm.c =================================================================*/
 
diff --git a/src/misc/extra/extraBddKmap.c b/src/misc/extra/extraBddKmap.c
new file mode 100644
index 00000000..bb43db68
--- /dev/null
+++ b/src/misc/extra/extraBddKmap.c
@@ -0,0 +1,783 @@
+/**CFile****************************************************************
+
+  FileName    [extraBddKmap.c]
+
+  PackageName [extra]
+
+  Synopsis    [Visualizing the K-map.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 2.0. Started - September 1, 2003.]
+
+  Revision    [$Id: extraBddKmap.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $]
+
+***********************************************************************/
+
+///      K-map visualization using pseudo graphics      ///
+///       Version 1.0. Started - August 20, 2000        ///
+///     Version 2.0. Added to EXTRA - July 17, 2001     ///
+
+#include "extra.h"
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+// the maximum number of variables in the Karnaugh Map
+#define MAXVARS 20
+
+/*
+// single line
+#define SINGLE_VERTICAL     (char)179
+#define SINGLE_HORIZONTAL   (char)196
+#define SINGLE_TOP_LEFT     (char)218
+#define SINGLE_TOP_RIGHT    (char)191
+#define SINGLE_BOT_LEFT     (char)192
+#define SINGLE_BOT_RIGHT    (char)217
+
+// double line
+#define DOUBLE_VERTICAL     (char)186
+#define DOUBLE_HORIZONTAL   (char)205
+#define DOUBLE_TOP_LEFT     (char)201
+#define DOUBLE_TOP_RIGHT    (char)187
+#define DOUBLE_BOT_LEFT     (char)200
+#define DOUBLE_BOT_RIGHT    (char)188
+
+// line intersections
+#define SINGLES_CROSS       (char)197
+#define DOUBLES_CROSS       (char)206
+#define S_HOR_CROSS_D_VER   (char)215
+#define S_VER_CROSS_D_HOR   (char)216
+
+// single line joining
+#define S_JOINS_S_VER_LEFT  (char)180
+#define S_JOINS_S_VER_RIGHT (char)195
+#define S_JOINS_S_HOR_TOP   (char)193
+#define S_JOINS_S_HOR_BOT   (char)194
+
+// double line joining
+#define D_JOINS_D_VER_LEFT  (char)185
+#define D_JOINS_D_VER_RIGHT (char)204
+#define D_JOINS_D_HOR_TOP   (char)202
+#define D_JOINS_D_HOR_BOT   (char)203
+
+// single line joining double line
+#define S_JOINS_D_VER_LEFT  (char)182
+#define S_JOINS_D_VER_RIGHT (char)199
+#define S_JOINS_D_HOR_TOP   (char)207
+#define S_JOINS_D_HOR_BOT   (char)209
+*/
+
+// single line
+#define SINGLE_VERTICAL     (char)'|'
+#define SINGLE_HORIZONTAL   (char)'-'
+#define SINGLE_TOP_LEFT     (char)'+'
+#define SINGLE_TOP_RIGHT    (char)'+'
+#define SINGLE_BOT_LEFT     (char)'+'
+#define SINGLE_BOT_RIGHT    (char)'+'
+
+// double line
+#define DOUBLE_VERTICAL     (char)'|'
+#define DOUBLE_HORIZONTAL   (char)'-'
+#define DOUBLE_TOP_LEFT     (char)'+'
+#define DOUBLE_TOP_RIGHT    (char)'+'
+#define DOUBLE_BOT_LEFT     (char)'+'
+#define DOUBLE_BOT_RIGHT    (char)'+'
+
+// line intersections
+#define SINGLES_CROSS       (char)'+'
+#define DOUBLES_CROSS       (char)'+'
+#define S_HOR_CROSS_D_VER   (char)'+'
+#define S_VER_CROSS_D_HOR   (char)'+'
+
+// single line joining
+#define S_JOINS_S_VER_LEFT  (char)'+'
+#define S_JOINS_S_VER_RIGHT (char)'+'
+#define S_JOINS_S_HOR_TOP   (char)'+'
+#define S_JOINS_S_HOR_BOT   (char)'+'
+
+// double line joining
+#define D_JOINS_D_VER_LEFT  (char)'+'
+#define D_JOINS_D_VER_RIGHT (char)'+'
+#define D_JOINS_D_HOR_TOP   (char)'+'
+#define D_JOINS_D_HOR_BOT   (char)'+'
+
+// single line joining double line
+#define S_JOINS_D_VER_LEFT  (char)'+'
+#define S_JOINS_D_VER_RIGHT (char)'+'
+#define S_JOINS_D_HOR_TOP   (char)'+'
+#define S_JOINS_D_HOR_BOT   (char)'+'
+
+
+// other symbols
+#define UNDERSCORE          (char)95
+//#define SYMBOL_ZERO       (char)248   // degree sign
+//#define SYMBOL_ZERO         (char)'o'
+#define SYMBOL_ZERO         (char)' '
+#define SYMBOL_ONE          (char)'1'
+#define SYMBOL_DC           (char)'-'
+#define SYMBOL_OVERLAP      (char)'?'
+
+// full cells and half cells
+#define CELL_FREE           (char)32
+#define CELL_FULL           (char)219
+#define HALF_UPPER          (char)223
+#define HALF_LOWER          (char)220
+#define HALF_LEFT           (char)221
+#define HALF_RIGHT          (char)222
+
+
+/*---------------------------------------------------------------------------*/
+/* Structure declarations                                                    */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+// the array of BDD variables used internally
+static DdNode * s_XVars[MAXVARS];
+
+// flag which determines where the horizontal variable names are printed
+static int fHorizontalVarNamesPrintedAbove = 1;
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+
+/**AutomaticStart*************************************************************/
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+// Oleg's way of generating the gray code
+static int GrayCode( int BinCode );
+static int BinCode ( int GrayCode );
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+
+/**Function********************************************************************
+
+  Synopsis    [Prints the K-map of the function.]
+
+  Description [If the pointer to the array of variables XVars is NULL,
+               fSuppType determines how the support will be determined.
+               fSuppType == 0 -- takes the first nVars of the manager
+               fSuppType == 1 -- takes the topmost nVars of the manager
+               fSuppType == 2 -- determines support from the on-set and the offset
+               ]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Extra_PrintKMap( 
+  FILE * Output,  /* the output stream */
+  DdManager * dd, 
+  DdNode * OnSet, 
+  DdNode * OffSet, 
+  int nVars, 
+  DdNode ** XVars, 
+  int fSuppType, /* the flag which determines how support is computed */
+  char ** pVarNames )
+{
+    int d, p, n, s, v, h, w;
+    int nVarsVer;
+    int nVarsHor;
+    int nCellsVer;
+    int nCellsHor;
+    int nSkipSpaces;
+
+    // make sure that on-set and off-set do not overlap
+    if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) )
+    {
+        fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" );
+        return;
+    }
+/*
+    if ( OnSet == b1 )
+    {
+        fprintf( Output, "PrintKMap(): Constant 1\n" );
+        return;
+    }
+    if ( OffSet == b1 )
+    {
+        fprintf( Output, "PrintKMap(): Constant 0\n" );
+        return;
+    }
+*/
+    if ( nVars < 0 || nVars > MAXVARS )
+    {
+        fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS );
+        return;
+    }
+
+    // determine the support if it is not given
+    if ( XVars == NULL )
+    {
+        if ( fSuppType == 0 )
+        {   // assume that the support includes the first nVars of the manager
+            assert( nVars );
+            for ( v = 0; v < nVars; v++ )
+                s_XVars[v] = Cudd_bddIthVar( dd, v );
+        }
+        else if ( fSuppType == 1 )
+        {   // assume that the support includes the topmost nVars of the manager
+            assert( nVars );
+            for ( v = 0; v < nVars; v++ )
+                s_XVars[v] = Cudd_bddIthVar( dd, dd->invperm[v] );
+        }
+        else // determine the support
+        {
+            DdNode * SuppOn, * SuppOff, * Supp;
+            int cVars = 0;
+            DdNode * TempSupp;
+
+            // determine support
+            SuppOn = Cudd_Support( dd, OnSet );         Cudd_Ref( SuppOn );
+            SuppOff = Cudd_Support( dd, OffSet );       Cudd_Ref( SuppOff );
+            Supp = Cudd_bddAnd( dd, SuppOn, SuppOff );  Cudd_Ref( Supp );
+            Cudd_RecursiveDeref( dd, SuppOn );
+            Cudd_RecursiveDeref( dd, SuppOff );
+
+            nVars = Cudd_SupportSize( dd, Supp );
+            if ( nVars > MAXVARS )
+            {
+                fprintf( Output, "PrintKMap(): The number of variables is more than %d\n", MAXVARS );
+                Cudd_RecursiveDeref( dd, Supp );
+                return;
+            }
+
+            // assign variables
+            for ( TempSupp = Supp; TempSupp != dd->one; TempSupp = Cudd_T(TempSupp), cVars++ )
+                s_XVars[cVars] = Cudd_bddIthVar( dd, TempSupp->index );
+
+            Cudd_RecursiveDeref( dd, TempSupp );
+        }
+    }
+    else
+    {
+        // copy variables
+        assert( XVars );
+        for ( v = 0; v < nVars; v++ )
+            s_XVars[v] = XVars[v];
+    }
+
+    ////////////////////////////////////////////////////////////////////
+    // determine the Karnaugh map parameters
+    nVarsVer = nVars/2;
+    nVarsHor = nVars - nVarsVer;
+    nCellsVer = (1<<nVarsVer);
+    nCellsHor = (1<<nVarsHor);
+    nSkipSpaces = nVarsVer + 1;
+
+    ////////////////////////////////////////////////////////////////////
+    // print variable names
+    fprintf( Output, "\n" );
+    for ( w = 0; w < nVarsVer; w++ )
+        if ( pVarNames == NULL )
+            fprintf( Output, "%c", 'a'+nVarsHor+w );
+        else
+            fprintf( Output, " %s", pVarNames[nVarsHor+w] );
+
+    if ( fHorizontalVarNamesPrintedAbove )
+    {
+        fprintf( Output, " \\ " );
+        for ( w = 0; w < nVarsHor; w++ )
+            if ( pVarNames == NULL )
+                fprintf( Output, "%c", 'a'+w );
+            else
+                fprintf( Output, "%s ", pVarNames[w] );
+    }
+    fprintf( Output, "\n" );
+
+    if ( fHorizontalVarNamesPrintedAbove )
+    {
+        ////////////////////////////////////////////////////////////////////
+        // print horizontal digits
+        for ( d = 0; d < nVarsHor; d++ )
+        {
+            for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
+            for ( n = 0; n < nCellsHor; n++ )
+                if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
+                    fprintf( Output, "1   " );
+                else
+                    fprintf( Output, "0   " );
+            fprintf( Output, "\n" );
+        }
+    }
+
+    ////////////////////////////////////////////////////////////////////
+    // print the upper line
+    for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+    fprintf( Output, "%c", DOUBLE_TOP_LEFT );
+    for ( s = 0; s < nCellsHor; s++ )
+    {
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        if ( s != nCellsHor-1 )
+            if ( s&1 )
+                fprintf( Output, "%c", D_JOINS_D_HOR_BOT );
+            else
+                fprintf( Output, "%c", S_JOINS_D_HOR_BOT );
+    }
+    fprintf( Output, "%c", DOUBLE_TOP_RIGHT );
+    fprintf( Output, "\n" );
+
+    ////////////////////////////////////////////////////////////////////
+    // print the map
+    for ( v = 0; v < nCellsVer; v++ )
+    {
+        DdNode * CubeVerBDD;
+
+        // print horizontal digits
+//      for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+        for ( n = 0; n < nVarsVer; n++ )
+            if ( GrayCode(v) & (1<<(nVarsVer-1-n)) )
+                fprintf( Output, "1" );
+            else
+                fprintf( Output, "0" );
+        fprintf( Output, " " );
+
+        // find vertical cube
+        CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor, 1 );    Cudd_Ref( CubeVerBDD );
+
+        // print text line
+        fprintf( Output, "%c", DOUBLE_VERTICAL );
+        for ( h = 0; h < nCellsHor; h++ )
+        {
+            DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet;
+
+            fprintf( Output, " " );
+//          fprintf( Output, "x" );
+            ///////////////////////////////////////////////////////////////
+            // determine what should be printed
+            CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars, 1 );    Cudd_Ref( CubeHorBDD );
+            Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD );                   Cudd_Ref( Prod );
+            Cudd_RecursiveDeref( dd, CubeHorBDD );
+
+            ValueOnSet  = Cudd_Cofactor( dd, OnSet, Prod );                     Cudd_Ref( ValueOnSet );
+            ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod );                    Cudd_Ref( ValueOffSet );
+            Cudd_RecursiveDeref( dd, Prod );
+
+            if ( ValueOnSet == b1 && ValueOffSet == b0 )
+                fprintf( Output, "%c", SYMBOL_ONE );
+            else if ( ValueOnSet == b0 && ValueOffSet == b1 )
+                fprintf( Output, "%c", SYMBOL_ZERO );
+            else if ( ValueOnSet == b0 && ValueOffSet == b0 ) 
+                fprintf( Output, "%c", SYMBOL_DC );
+            else if ( ValueOnSet == b1 && ValueOffSet == b1 ) 
+                fprintf( Output, "%c", SYMBOL_OVERLAP );
+            else
+                assert(0);
+
+            Cudd_RecursiveDeref( dd, ValueOnSet );
+            Cudd_RecursiveDeref( dd, ValueOffSet );
+            ///////////////////////////////////////////////////////////////
+            fprintf( Output, " " );
+
+            if ( h != nCellsHor-1 )
+                if ( h&1 )
+                    fprintf( Output, "%c", DOUBLE_VERTICAL );
+                else
+                    fprintf( Output, "%c", SINGLE_VERTICAL );
+        }
+        fprintf( Output, "%c", DOUBLE_VERTICAL );
+        fprintf( Output, "\n" );
+
+        Cudd_RecursiveDeref( dd, CubeVerBDD );
+
+        if ( v != nCellsVer-1 )
+        // print separator line
+        {
+            for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+            if ( v&1 )
+            {
+                fprintf( Output, "%c", D_JOINS_D_VER_RIGHT );
+                for ( s = 0; s < nCellsHor; s++ )
+                {
+                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+                    if ( s != nCellsHor-1 )
+                        if ( s&1 )
+                            fprintf( Output, "%c", DOUBLES_CROSS );
+                        else
+                            fprintf( Output, "%c", S_VER_CROSS_D_HOR );
+                }
+                fprintf( Output, "%c", D_JOINS_D_VER_LEFT );
+            }
+            else
+            {
+                fprintf( Output, "%c", S_JOINS_D_VER_RIGHT );
+                for ( s = 0; s < nCellsHor; s++ )
+                {
+                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
+                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
+                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
+                    if ( s != nCellsHor-1 )
+                        if ( s&1 )
+                            fprintf( Output, "%c", S_HOR_CROSS_D_VER );
+                        else
+                            fprintf( Output, "%c", SINGLES_CROSS );
+                }
+                fprintf( Output, "%c", S_JOINS_D_VER_LEFT );
+            }
+            fprintf( Output, "\n" );
+        }
+    }
+    
+    ////////////////////////////////////////////////////////////////////
+    // print the lower line
+    for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+    fprintf( Output, "%c", DOUBLE_BOT_LEFT );
+    for ( s = 0; s < nCellsHor; s++ )
+    {
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        if ( s != nCellsHor-1 )
+            if ( s&1 )
+                fprintf( Output, "%c", D_JOINS_D_HOR_TOP );
+            else
+                fprintf( Output, "%c", S_JOINS_D_HOR_TOP );
+    }
+    fprintf( Output, "%c", DOUBLE_BOT_RIGHT );
+    fprintf( Output, "\n" );
+
+    if ( !fHorizontalVarNamesPrintedAbove )
+    {
+        ////////////////////////////////////////////////////////////////////
+        // print horizontal digits
+        for ( d = 0; d < nVarsHor; d++ )
+        {
+            for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
+            for ( n = 0; n < nCellsHor; n++ )
+                if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
+                    fprintf( Output, "1   " );
+                else
+                    fprintf( Output, "0   " );
+
+            /////////////////////////////////
+            fprintf( Output, "%c", (char)('a'+d) );
+            /////////////////////////////////
+            fprintf( Output, "\n" );
+        }
+    }
+}
+
+
+
+/**Function********************************************************************
+
+  Synopsis    [Prints the K-map of the relation.]
+
+  Description [Assumes that the relation depends the first nXVars of XVars and 
+  the first nYVars of YVars. Draws X and Y vars and vertical and horizontal vars.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+void Extra_PrintKMapRelation( 
+  FILE * Output,  /* the output stream */
+  DdManager * dd, 
+  DdNode * OnSet, 
+  DdNode * OffSet, 
+  int nXVars, 
+  int nYVars, 
+  DdNode ** XVars, 
+  DdNode ** YVars ) /* the flag which determines how support is computed */
+{
+    int d, p, n, s, v, h, w;
+    int nVars;
+    int nVarsVer;
+    int nVarsHor;
+    int nCellsVer;
+    int nCellsHor;
+    int nSkipSpaces;
+
+    // make sure that on-set and off-set do not overlap
+    if ( !Cudd_bddLeq( dd, OnSet, Cudd_Not(OffSet) ) )
+    {
+        fprintf( Output, "PrintKMap(): The on-set and the off-set overlap\n" );
+        return;
+    }
+
+    if ( OnSet == b1 )
+    {
+        fprintf( Output, "PrintKMap(): Constant 1\n" );
+        return;
+    }
+    if ( OffSet == b1 )
+    {
+        fprintf( Output, "PrintKMap(): Constant 0\n" );
+        return;
+    }
+
+    nVars = nXVars + nYVars;
+    if ( nVars < 0 || nVars > MAXVARS )
+    {
+        fprintf( Output, "PrintKMap(): The number of variables is less than zero or more than %d\n", MAXVARS );
+        return;
+    }
+
+
+    ////////////////////////////////////////////////////////////////////
+    // determine the Karnaugh map parameters
+    nVarsVer = nXVars;
+    nVarsHor = nYVars;
+    nCellsVer = (1<<nVarsVer);
+    nCellsHor = (1<<nVarsHor);
+    nSkipSpaces = nVarsVer + 1;
+
+    ////////////////////////////////////////////////////////////////////
+    // print variable names
+    fprintf( Output, "\n" );
+    for ( w = 0; w < nVarsVer; w++ )
+        fprintf( Output, "%c", 'a'+nVarsHor+w );
+    if ( fHorizontalVarNamesPrintedAbove )
+    {
+        fprintf( Output, " \\ " );
+        for ( w = 0; w < nVarsHor; w++ )
+            fprintf( Output, "%c", 'a'+w );
+    }
+    fprintf( Output, "\n" );
+
+    if ( fHorizontalVarNamesPrintedAbove )
+    {
+        ////////////////////////////////////////////////////////////////////
+        // print horizontal digits
+        for ( d = 0; d < nVarsHor; d++ )
+        {
+            for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
+            for ( n = 0; n < nCellsHor; n++ )
+                if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
+                    fprintf( Output, "1   " );
+                else
+                    fprintf( Output, "0   " );
+            fprintf( Output, "\n" );
+        }
+    }
+
+    ////////////////////////////////////////////////////////////////////
+    // print the upper line
+    for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+    fprintf( Output, "%c", DOUBLE_TOP_LEFT );
+    for ( s = 0; s < nCellsHor; s++ )
+    {
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        if ( s != nCellsHor-1 )
+            if ( s&1 )
+                fprintf( Output, "%c", D_JOINS_D_HOR_BOT );
+            else
+                fprintf( Output, "%c", S_JOINS_D_HOR_BOT );
+    }
+    fprintf( Output, "%c", DOUBLE_TOP_RIGHT );
+    fprintf( Output, "\n" );
+
+    ////////////////////////////////////////////////////////////////////
+    // print the map
+    for ( v = 0; v < nCellsVer; v++ )
+    {
+        DdNode * CubeVerBDD;
+
+        // print horizontal digits
+//      for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+        for ( n = 0; n < nVarsVer; n++ )
+            if ( GrayCode(v) & (1<<(nVarsVer-1-n)) )
+                fprintf( Output, "1" );
+            else
+                fprintf( Output, "0" );
+        fprintf( Output, " " );
+
+        // find vertical cube
+//      CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nVarsVer, s_XVars+nVarsHor );    Cudd_Ref( CubeVerBDD );
+        CubeVerBDD = Extra_bddBitsToCube( dd, GrayCode(v), nXVars, XVars, 1 );                 Cudd_Ref( CubeVerBDD );
+
+        // print text line
+        fprintf( Output, "%c", DOUBLE_VERTICAL );
+        for ( h = 0; h < nCellsHor; h++ )
+        {
+            DdNode * CubeHorBDD, * Prod, * ValueOnSet, * ValueOffSet;
+
+            fprintf( Output, " " );
+//          fprintf( Output, "x" );
+            ///////////////////////////////////////////////////////////////
+            // determine what should be printed
+//          CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nVarsHor, s_XVars );    Cudd_Ref( CubeHorBDD );
+            CubeHorBDD  = Extra_bddBitsToCube( dd, GrayCode(h), nYVars, YVars, 1 );        Cudd_Ref( CubeHorBDD );
+            Prod = Cudd_bddAnd( dd, CubeHorBDD, CubeVerBDD );                           Cudd_Ref( Prod );
+            Cudd_RecursiveDeref( dd, CubeHorBDD );
+
+            ValueOnSet  = Cudd_Cofactor( dd, OnSet, Prod );                     Cudd_Ref( ValueOnSet );
+            ValueOffSet = Cudd_Cofactor( dd, OffSet, Prod );                    Cudd_Ref( ValueOffSet );
+            Cudd_RecursiveDeref( dd, Prod );
+
+            if ( ValueOnSet == b1 && ValueOffSet == b0 )
+                fprintf( Output, "%c", SYMBOL_ONE );
+            else if ( ValueOnSet == b0 && ValueOffSet == b1 )
+                fprintf( Output, "%c", SYMBOL_ZERO );
+            else if ( ValueOnSet == b0 && ValueOffSet == b0 ) 
+                fprintf( Output, "%c", SYMBOL_DC );
+            else if ( ValueOnSet == b1 && ValueOffSet == b1 ) 
+                fprintf( Output, "%c", SYMBOL_OVERLAP );
+            else
+                assert(0);
+
+            Cudd_RecursiveDeref( dd, ValueOnSet );
+            Cudd_RecursiveDeref( dd, ValueOffSet );
+            ///////////////////////////////////////////////////////////////
+            fprintf( Output, " " );
+
+            if ( h != nCellsHor-1 )
+                if ( h&1 )
+                    fprintf( Output, "%c", DOUBLE_VERTICAL );
+                else
+                    fprintf( Output, "%c", SINGLE_VERTICAL );
+        }
+        fprintf( Output, "%c", DOUBLE_VERTICAL );
+        fprintf( Output, "\n" );
+
+        Cudd_RecursiveDeref( dd, CubeVerBDD );
+
+        if ( v != nCellsVer-1 )
+        // print separator line
+        {
+            for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+            if ( v&1 )
+            {
+                fprintf( Output, "%c", D_JOINS_D_VER_RIGHT );
+                for ( s = 0; s < nCellsHor; s++ )
+                {
+                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+                    fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+                    if ( s != nCellsHor-1 )
+                        if ( s&1 )
+                            fprintf( Output, "%c", DOUBLES_CROSS );
+                        else
+                            fprintf( Output, "%c", S_VER_CROSS_D_HOR );
+                }
+                fprintf( Output, "%c", D_JOINS_D_VER_LEFT );
+            }
+            else
+            {
+                fprintf( Output, "%c", S_JOINS_D_VER_RIGHT );
+                for ( s = 0; s < nCellsHor; s++ )
+                {
+                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
+                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
+                    fprintf( Output, "%c", SINGLE_HORIZONTAL );
+                    if ( s != nCellsHor-1 )
+                        if ( s&1 )
+                            fprintf( Output, "%c", S_HOR_CROSS_D_VER );
+                        else
+                            fprintf( Output, "%c", SINGLES_CROSS );
+                }
+                fprintf( Output, "%c", S_JOINS_D_VER_LEFT );
+            }
+            fprintf( Output, "\n" );
+        }
+    }
+    
+    ////////////////////////////////////////////////////////////////////
+    // print the lower line
+    for ( p = 0; p < nSkipSpaces; p++, fprintf( Output, " " ) );
+    fprintf( Output, "%c", DOUBLE_BOT_LEFT );
+    for ( s = 0; s < nCellsHor; s++ )
+    {
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        fprintf( Output, "%c", DOUBLE_HORIZONTAL );
+        if ( s != nCellsHor-1 )
+            if ( s&1 )
+                fprintf( Output, "%c", D_JOINS_D_HOR_TOP );
+            else
+                fprintf( Output, "%c", S_JOINS_D_HOR_TOP );
+    }
+    fprintf( Output, "%c", DOUBLE_BOT_RIGHT );
+    fprintf( Output, "\n" );
+
+    if ( !fHorizontalVarNamesPrintedAbove )
+    {
+        ////////////////////////////////////////////////////////////////////
+        // print horizontal digits
+        for ( d = 0; d < nVarsHor; d++ )
+        {
+            for ( p = 0; p < nSkipSpaces + 2; p++, fprintf( Output, " " ) );
+            for ( n = 0; n < nCellsHor; n++ )
+                if ( GrayCode(n) & (1<<(nVarsHor-1-d)) )
+                    fprintf( Output, "1   " );
+                else
+                    fprintf( Output, "0   " );
+
+            /////////////////////////////////
+            fprintf( Output, "%c", (char)('a'+d) );
+            /////////////////////////////////
+            fprintf( Output, "\n" );
+        }
+    }
+}
+
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static functions                                            */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int GrayCode ( int BinCode )
+{
+  return BinCode ^ ( BinCode >> 1 );
+}
+
+/**Function********************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+int BinCode ( int GrayCode )
+{
+  int bc = GrayCode;
+  while( GrayCode >>= 1 ) bc ^= GrayCode;
+  return bc;
+}
+
+
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 373ce5c5..932ed525 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: extraBddMisc.c,v 1.0 2003/09/01 00:00:00 alanmi Exp $]
+  Revision    [$Id: extraBddMisc.c,v 1.4 2005/10/04 00:19:54 alanmi Exp $]
 
 ***********************************************************************/
 
@@ -684,6 +684,41 @@ DdNode * Extra_bddComputeRangeCube( DdManager * dd, int iStart, int iStop )
     return bProd;
 }
 
+/**Function********************************************************************
+
+  Synopsis    [Computes the cube of BDD variables corresponding to bits it the bit-code]
+
+  Description [Returns a bdd composed of elementary bdds found in array BddVars[] such 
+  that the bdd vars encode the number Value of bit length CodeWidth (if fMsbFirst is 1, 
+  the most significant bit is encoded with the first bdd variable). If the variables 
+  BddVars are not specified, takes the first CodeWidth variables of the manager]
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Extra_bddBitsToCube( DdManager * dd, int Code, int CodeWidth, DdNode ** pbVars, int fMsbFirst )
+{
+    int z;
+    DdNode * bTemp, * bVar, * bVarBdd, * bResult;
+
+    bResult = b1;   Cudd_Ref( bResult );
+    for ( z = 0; z < CodeWidth; z++ )
+    {
+        bVarBdd = (pbVars)? pbVars[z]: dd->vars[z];
+        if ( fMsbFirst )
+            bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (CodeWidth-1-z)))==0 );
+        else
+            bVar = Cudd_NotCond( bVarBdd, (Code & (1 << (z)))==0 );
+        bResult = Cudd_bddAnd( dd, bTemp = bResult, bVar );     Cudd_Ref( bResult );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Cudd_Deref( bResult );
+
+    return bResult;
+}  /* end of Extra_bddBitsToCube */
+
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/
diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make
index 6cbf5d2c..42a0d84f 100644
--- a/src/misc/extra/module.make
+++ b/src/misc/extra/module.make
@@ -1,4 +1,5 @@
-SRC +=    src/misc/extra/extraBddMisc.c \
+SRC +=    src/misc/extra/extraBddKmap.c \
+    src/misc/extra/extraBddMisc.c \
     src/misc/extra/extraBddSymm.c \
     src/misc/extra/extraUtilBitMatrix.c \
     src/misc/extra/extraUtilCanon.c \
diff --git a/src/opt/cut/module.make b/src/opt/cut/module.make
index 2e7519d1..af2d8fc1 100644
--- a/src/opt/cut/module.make
+++ b/src/opt/cut/module.make
@@ -3,5 +3,6 @@ SRC +=  src/opt/cut/cutApi.c \
         src/opt/cut/cutMan.c \
         src/opt/cut/cutMerge.c \
         src/opt/cut/cutNode.c \
+        src/opt/cut/cutOracle.c \
         src/opt/cut/cutSeq.c \
         src/opt/cut/cutTruth.c 
diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c
index 786b7583..a9f0dd88 100644
--- a/src/opt/sim/simSupp.c
+++ b/src/opt/sim/simSupp.c
@@ -470,7 +470,7 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit )
         Params.nSeconds = ABC_INFINITY;
         Params.fInternal = 1;
 clk = clock();
-        pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); 
+        pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
 p->timeFraig += clock() - clk;
 clk = clock();
         Fraig_ManProveMiter( pMan );
diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c
index a98d4b5e..d9821088 100644
--- a/src/opt/sim/simSymSat.c
+++ b/src/opt/sim/simSymSat.c
@@ -147,7 +147,7 @@ int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned *
     Params.nSeconds = ABC_INFINITY;
 
 clk = clock();
-    pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); 
+    pMan = Abc_NtkToFraig( pMiter, &Params, 0, 0 ); 
 p->timeFraig += clock() - clk;
 clk = clock();
     Fraig_ManProveMiter( pMan );
diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c
index d7358749..662fe1ff 100644
--- a/src/sat/asat/added.c
+++ b/src/sat/asat/added.c
@@ -14,7 +14,7 @@
 
   Date        [Ver. 1.0. Started - June 20, 2005.]
 
-  Revision    [$Id: added.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+  Revision    [$Id: added.c,v 1.4 2005/09/16 22:55:03 casem Exp $]
 
 ***********************************************************************/
 
@@ -57,7 +57,7 @@ static void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement )
   SeeAlso     []
 
 ***********************************************************************/
-void Asat_SolverWriteDimacs( solver * p, char * pFileName )
+void Asat_SolverWriteDimacs( solver * p, char * pFileName, lit* assumptionsBegin, lit* assumptionsEnd, int incrementVars )
 {
     FILE * pFile;
     void ** pClauses;
@@ -78,18 +78,31 @@ void Asat_SolverWriteDimacs( solver * p, char * pFileName )
     nClauses = p->clauses.size;
     pClauses = p->clauses.ptr;
     for ( i = 0; i < nClauses; i++ )
-        Asat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
+        Asat_ClauseWriteDimacs( pFile, pClauses[i], incrementVars );
 
     // write the learned clauses
     nClauses = p->learnts.size;
     pClauses = p->learnts.ptr;
     for ( i = 0; i < nClauses; i++ )
-        Asat_ClauseWriteDimacs( pFile, pClauses[i], 1 );
+        Asat_ClauseWriteDimacs( pFile, pClauses[i], incrementVars );
 
     // write zero-level assertions
     for ( i = 0; i < p->size; i++ )
         if ( p->levels[i] == 0 && p->assigns[i] != l_Undef )
-            fprintf( pFile, "%s%d 0\n", (p->assigns[i] == l_False)? "-": "", i + 1 );
+            fprintf( pFile, "%s%d%s\n",
+                     (p->assigns[i] == l_False)? "-": "",
+                     i + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+
+    // write the assumptions
+    if (assumptionsBegin) {
+        for (; assumptionsBegin != assumptionsEnd; assumptionsBegin++) {
+            fprintf( pFile, "%s%d%s\n",
+                     lit_sign(*assumptionsBegin)? "-": "",
+                     lit_var(*assumptionsBegin) + (int)(incrementVars>0),
+                     (incrementVars) ? " 0" : "");
+        }
+    }
 
     fprintf( pFile, "\n" );
     fclose( pFile );
diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c
index d248b115..3927fac3 100644
--- a/src/sat/asat/solver.c
+++ b/src/sat/asat/solver.c
@@ -1099,7 +1099,7 @@ bool solver_solve(solver* s, lit* begin, lit* end, int nSeconds)
         nof_conflicts *= 1.5;
         nof_learnts   *= 1.1;
         // if the runtime limit is exceeded, quit the restart loop
-        if ( clock() - timeStart >= nSeconds * CLOCKS_PER_SEC )
+        if ( (nSeconds >= 0) && (clock() - timeStart >= nSeconds * CLOCKS_PER_SEC) )
             break;
     }
     if (s->verbosity >= 1)
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index 9f80bc7e..b82601c4 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -73,7 +73,9 @@ extern int     solver_nvars(solver* s);
 extern int     solver_nclauses(solver* s);
 
 // additional procedures
-extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName );
+extern void    Asat_SolverWriteDimacs( solver * pSat, char * pFileName,
+                                       lit* assumptionsBegin, lit* assumptionsEnd,
+                                       int incrementVars);
 
 struct stats_t
 {
diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c
index 1f324c4b..a34f3b9a 100644
--- a/src/sat/csat/csat_apis.c
+++ b/src/sat/csat/csat_apis.c
@@ -542,7 +542,7 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng )
     else if ( mng->mode == 1 ) // resource-aware fraiging
     {
         // transform the target into a fraig
-        pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0 ); 
+        pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0, 0 ); 
         Fraig_ManProveMiter( pMan );
         RetValue = Fraig_ManCheckMiter( pMan );
 
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 75dfb812..dc679907 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -149,6 +149,7 @@ extern void                Fraig_NodeSetChoice( Fraig_Man_t * pMan, Fraig_Node_t
 
 /*=== fraigMan.c =============================================================*/
 extern void                Fraig_ParamsSetDefault( Fraig_Params_t * pParams );
+extern void                Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams );
 extern Fraig_Man_t *       Fraig_ManCreate( Fraig_Params_t * pParams );
 extern void                Fraig_ManFree( Fraig_Man_t * pMan );
 extern void                Fraig_ManPrintStats( Fraig_Man_t * p );
diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c
index aa7e5999..1a34af86 100644
--- a/src/sat/fraig/fraigMan.c
+++ b/src/sat/fraig/fraigMan.c
@@ -60,6 +60,35 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams )
 
 /**Function*************************************************************
 
+  Synopsis    [Sets the default parameters of the package.]
+
+  Description [This set of parameters is tuned for complete FRAIGing.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fraig_ParamsSetDefaultFull( Fraig_Params_t * pParams )
+{
+    memset( pParams, 0, sizeof(Fraig_Params_t) );
+    pParams->nPatsRand  = FRAIG_PATTERNS_RANDOM;  // the number of words of random simulation info
+    pParams->nPatsDyna  = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info
+    pParams->nBTLimit   = -1;                     // the max number of backtracks to perform
+    pParams->nSeconds   = 20;                     // the max number of seconds to solve the miter
+    pParams->fFuncRed   =  1;                     // performs only one level hashing
+    pParams->fFeedBack  =  1;                     // enables solver feedback
+    pParams->fDist1Pats =  1;                     // enables distance-1 patterns
+    pParams->fDoSparse  =  1;                     // performs equiv tests for sparse functions 
+    pParams->fChoicing  =  0;                     // enables recording structural choices
+    pParams->fTryProve  =  0;                     // tries to solve the final miter
+    pParams->fVerbose   =  0;                     // the verbosiness flag
+    pParams->fVerboseP  =  0;                     // the verbose flag for reporting the proof
+    pParams->fInternal  =  0;                     // the flag indicates the internal run 
+}
+
+/**Function*************************************************************
+
   Synopsis    [Creates the new FRAIG manager.]
 
   Description []