Added Exorcism package, reading ESOP (read_pla -x file.esop) and deriving AIG (cubes -x; st).

16 files changed, 3921 insertions, 33 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 61bf44b2..f2332446 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -954,6 +954,38 @@ SOURCE=.\src\base\cba\cbaWriteBlif.c
 SOURCE=.\src\base\cba\cbaWriteVer.c
 # End Source File
 # End Group
+# Begin Group "exor"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\base\exor\exor.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\exor\exor.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\exor\exorBits.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\exor\exorCubes.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\exor\exorLink.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\exor\exorList.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\base\exor\exorUtil.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "bdd"
 
diff --git a/src/aig/gia/giaEsop.c b/src/aig/gia/giaEsop.c
index 9d95ccf5..db69bf02 100644
--- a/src/aig/gia/giaEsop.c
+++ b/src/aig/gia/giaEsop.c
@@ -143,6 +143,33 @@ void Eso_ManCoverPrint( Eso_Man_t * p, Vec_Int_t * vEsop )
     printf( "\n" );
     Vec_StrFree( vStr );
 }
+Vec_Wec_t * Eso_ManCoverDerive( Eso_Man_t * p, Vec_Ptr_t * vCover )
+{
+    Vec_Wec_t * vRes;
+    Vec_Int_t * vEsop, * vLevel;  int i;
+    vRes = Vec_WecAlloc( Vec_VecSizeSize((Vec_Vec_t *)vCover) );
+    Vec_PtrForEachEntry( Vec_Int_t *, vCover, vEsop, i )
+    {
+        if ( Vec_IntSize(vEsop) > 0 )
+        {
+            int c, Cube;
+            Vec_IntForEachEntry( vEsop, Cube, c )
+            {
+                vLevel = Vec_WecPushLevel( vRes );
+                if ( Cube != p->Cube1 )
+                {
+                    int k, Lit;
+                    Vec_Int_t * vCube = Eso_ManCube( p, Cube );
+                    Vec_IntForEachEntry( vCube, Lit, k )
+                        Vec_IntPush( vLevel, Lit );
+                }
+                Vec_IntPush( vLevel, -i-1 );
+            }
+        }
+    }
+    assert( Vec_WecSize(vRes) == Vec_WecCap(vRes) );
+    return vRes;
+}
 Gia_Man_t * Eso_ManCoverConvert( Eso_Man_t * p, Vec_Ptr_t * vCover )
 {
     Vec_Int_t * vEsop;
@@ -459,14 +486,15 @@ Vec_Int_t * Eso_ManTransformOne( Eso_Man_t * p, Vec_Int_t * vEsop, int fCompl, V
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose )
+Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes )
 {
     abctime clk = Abc_Clock();
     Vec_Ptr_t * vCover;
-    Gia_Man_t * pNew;
-    Gia_Obj_t * pObj; int i, nCubes = 0, nCubesUsed = 0;
+    Gia_Man_t * pNew = NULL;
+    Gia_Obj_t * pObj; 
+    int i, nCubes = 0, nCubesUsed = 0;
     Vec_Int_t * vEsop1, * vEsop2, * vEsop;
-    Eso_Man_t * p = Eso_ManAlloc( pGia );
+    Eso_Man_t * p = Eso_ManAlloc( pGia ); 
     Gia_ManForEachAnd( pGia, pObj, i )
     {
         vEsop1 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId0(pObj, i) );
@@ -482,16 +510,23 @@ Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose )
     {
         vEsop1 = Vec_WecEntry( p->vEsops, Gia_ObjFaninId0p(pGia, pObj) );
         vEsop1 = Eso_ManTransformOne( p, vEsop1, Gia_ObjFaninC0(pObj), p->vCube1 );
-        printf( "Output %3d:  ESOP has %5d cubes\n", i, Vec_IntSize(vEsop1) );
         if ( fVerbose )
-            Eso_ManCoverPrint( p, vEsop1 );
+            printf( "Output %3d:  ESOP has %5d cubes\n", i, Vec_IntSize(vEsop1) );
+//        if ( fVerbose )
+//            Eso_ManCoverPrint( p, vEsop1 );
         Vec_PtrPush( vCover, Vec_IntDup(vEsop1) );
         nCubesUsed += Vec_IntSize(vEsop1);
     }
-    printf( "Outs = %d.  Cubes = %d.  Used = %d.  Hashed = %d. ", 
-        Gia_ManCoNum(pGia), nCubes, nCubesUsed, Hsh_VecSize(p->pHash) );
-    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-    pNew = Eso_ManCoverConvert( p, vCover );
+    if ( fVerbose )
+    {
+        printf( "Outs = %d.  Cubes = %d.  Used = %d.  Hashed = %d. ", 
+            Gia_ManCoNum(pGia), nCubes, nCubesUsed, Hsh_VecSize(p->pHash) );
+        Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+    }
+    if ( pvRes )
+        *pvRes = Eso_ManCoverDerive( p, vCover );
+    else
+        pNew = Eso_ManCoverConvert( p, vCover );
     Vec_VecFree( (Vec_Vec_t *)vCover );
     Eso_ManStop( p );
     return pNew;
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index f7e0939f..59993614 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -2501,7 +2501,7 @@ float Abc_NtkComputeDelay( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NodeSopToCubes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
+void Abc_NodeSopToCubes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew, int fXor )
 {
     Abc_Obj_t * pNodeOr, * pNodeNew, * pFanin;
     char * pCube, * pSop = (char *)pNodeOld->pData;
@@ -2517,7 +2517,10 @@ void Abc_NodeSopToCubes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
     }
     // add the OR gate
     pNodeOr = Abc_NtkCreateNode( pNtkNew );
-    pNodeOr->pData = Abc_SopCreateOr( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_SopGetCubeNum(pSop), NULL );
+    if ( fXor )
+        pNodeOr->pData = Abc_SopCreateXorSpecial( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_SopGetCubeNum(pSop) );
+    else 
+        pNodeOr->pData = Abc_SopCreateOr( (Mem_Flex_t *)pNtkNew->pManFunc, Abc_SopGetCubeNum(pSop), NULL );
     // check the logic function of the node
     Abc_SopForEachCube( pSop, nVars, pCube )
     {
@@ -2525,6 +2528,12 @@ void Abc_NodeSopToCubes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
         Abc_CubeForEachVar( pCube, Value, v )
             if ( Value == '0' || Value == '1' )
                 nFanins++;
+        if ( nFanins == 0 ) // const1 cube in ESOP
+        {
+            pNodeNew = Abc_NtkCreateNodeConst1( pNtkNew );
+            Abc_ObjAddFanin( pNodeOr, pNodeNew );
+            continue;
+        }
         assert( nFanins > 0 );
         // create node
         pNodeNew = Abc_NtkCreateNode( pNtkNew );
@@ -2548,7 +2557,7 @@ void Abc_NodeSopToCubes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew )
     assert( pNodeOld->pCopy == NULL );
     pNodeOld->pCopy = pNodeOr;
 }
-Abc_Ntk_t * Abc_NtkSopToCubes( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkSopToCubes( Abc_Ntk_t * pNtk, int fXor )
 {
     Abc_Ntk_t * pNtkNew;
     Abc_Obj_t * pNode;
@@ -2560,7 +2569,7 @@ Abc_Ntk_t * Abc_NtkSopToCubes( Abc_Ntk_t * pNtk )
     // perform conversion in the topological order
     vNodes = Abc_NtkDfs( pNtk, 0 );
     Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pNode, i )
-        Abc_NodeSopToCubes( pNode, pNtkNew );
+        Abc_NodeSopToCubes( pNode, pNtkNew, fXor );
     Vec_PtrFree( vNodes );
     // make sure everything is okay
     Abc_NtkFinalize( pNtk, pNtkNew );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index eadd2ddd..fb7ee06d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -465,6 +465,7 @@ static int Abc_CommandAbc9PoXsim             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9Demiter            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Fadds              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Esop               ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Exorcism           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Mfs                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1092,6 +1093,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&demiter",      Abc_CommandAbc9Demiter,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&fadds",        Abc_CommandAbc9Fadds,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&esop",         Abc_CommandAbc9Esop,         0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&exorcism",     Abc_CommandAbc9Exorcism,     0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mfs",          Abc_CommandAbc9Mfs,          0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
@@ -8826,17 +8828,20 @@ usage:
 ***********************************************************************/
 int Abc_CommandCubes( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Abc_Ntk_t * Abc_NtkSopToCubes( Abc_Ntk_t * pNtk );
+    extern Abc_Ntk_t * Abc_NtkSopToCubes( Abc_Ntk_t * pNtk, int fXor );
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c;
+    int c, fXor = 0;
 
     pNtk = Abc_FrameReadNtk(pAbc);
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "xh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'x':
+            fXor ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -8857,7 +8862,7 @@ int Abc_CommandCubes( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkSopToCubes( pNtk );
+    pNtkRes = Abc_NtkSopToCubes( pNtk, fXor );
     if ( pNtkRes == NULL )
     {
         Abc_Print( -1, "Converting to cubes has failed.\n" );
@@ -8868,9 +8873,10 @@ int Abc_CommandCubes( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: cubes [-h]\n" );
+    Abc_Print( -2, "usage: cubes [-xh]\n" );
     Abc_Print( -2, "\t        converts the current network into a network derived by creating\n" );
     Abc_Print( -2, "\t        a separate node for each product and sum in the local SOPs\n" );
+    Abc_Print( -2, "\t-v    : toggle using XOR instead of OR [default = %s]\n", fXor? "yes": "no" );
     Abc_Print( -2, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -39186,7 +39192,7 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Esop( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose );
+    extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes );
     Gia_Man_t * pTemp;
     int c, fVerbose = 0;
     Extra_UtilGetoptReset();
@@ -39208,7 +39214,7 @@ int Abc_CommandAbc9Esop( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" );
         return 0;
     }
-    pTemp = Eso_ManCompute( pAbc->pGia, fVerbose );
+    pTemp = Eso_ManCompute( pAbc->pGia, fVerbose, NULL );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
@@ -39225,6 +39231,86 @@ usage:
   Synopsis    []
 
   Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Exorcism( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity );
+    extern Gia_Man_t * Eso_ManCompute( Gia_Man_t * pGia, int fVerbose, Vec_Wec_t ** pvRes );
+    Vec_Wec_t * vEsop = NULL;
+    char * pFileNameOut = NULL;
+    int c, Quality = 2, Verbosity = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "QVvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'Q':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-Q\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            Quality = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( Quality < 0 )
+                goto usage;
+            break;
+        case 'V':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-V\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            Verbosity = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( Verbosity < 0 )
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Exorcism(): There is no AIG.\n" );
+        return 0;
+    }
+    // get the output file name
+    if ( argc == globalUtilOptind + 1 )
+        pFileNameOut = argv[globalUtilOptind];
+    // generate starting cover and run minimization
+    Eso_ManCompute( pAbc->pGia, fVerbose, &vEsop );
+    Abc_ExorcismMain( vEsop, Gia_ManCiNum(pAbc->pGia), Gia_ManCoNum(pAbc->pGia), pFileNameOut, Quality, Verbosity );
+    Vec_WecFree( vEsop );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &exorcism [-Q N] [-V N] <file>\n" );
+    Abc_Print( -2, "                performs heuristic exclusive sum-of-project minimization\n" );
+    Abc_Print( -2, "        -Q N  : minimization quality [default = 0]\n");
+    Abc_Print( -2, "                increasing this number improves quality and adds to runtime\n");
+    Abc_Print( -2, "        -Q N  : verbosity level [default = 0]\n");
+    Abc_Print( -2, "                0 = no output; 1 = outline; 2 = verbose\n");
+    Abc_Print( -2, "        <file>: the output file name in ESOP-PLA format\n");
+    Abc_Print( -2, "\n" );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
                
   SideEffects []
 
diff --git a/src/base/exor/exor.c b/src/base/exor/exor.c
new file mode 100644
index 00000000..4d567033
--- /dev/null
+++ b/src/base/exor/exor.c
@@ -0,0 +1,832 @@
+/**CFile****************************************************************
+
+  FileName    [exor.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Exclusive sum-of-product minimization.]
+
+  Synopsis    [Main procedure.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: exor.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///                  Implementation of EXORCISM - 4                  ///
+///              An Exclusive Sum-of-Product Minimizer               ///
+///               Alan Mishchenko  <alanmi@ee.pdx.edu>               ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///                         Main Module                              ///
+///                ESOP Minimization Task Coordinator                ///
+///                                                                  ///
+///          1) interprets command line                              ///  
+///          2) calls the approapriate reading procedure             ///
+///          3) calls the minimization module                        ///
+///                                                                  ///
+///  Ver. 1.0. Started - July 18, 2000. Last update - July 20, 2000  ///
+///  Ver. 1.1. Started - July 24, 2000. Last update - July 29, 2000  ///
+///  Ver. 1.4. Started -  Aug 10, 2000. Last update -  Aug 26, 2000  ///
+///  Ver. 1.6. Started -  Sep 11, 2000. Last update -  Sep 15, 2000  ///
+///  Ver. 1.7. Started -  Sep 20, 2000. Last update -  Sep 23, 2000  ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///   This software was tested with the BDD package "CUDD", v.2.3.0  ///
+///                          by Fabio Somenzi                        ///
+///                  http://vlsi.colorado.edu/~fabio/                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "exor.h"
+
+ABC_NAMESPACE_IMPL_START
+
+///////////////////////////////////////////////////////////////////////
+///                      GLOBAL VARIABLES                            ///
+////////////////////////////////////////////////////////////////////////
+
+// information about the cube cover
+cinfo g_CoverInfo;
+
+extern int s_fDecreaseLiterals;
+
+////////////////////////////////////////////////////////////////////////
+///                       EXTERNAL FUNCTIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                        FUNCTION main()                           ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int ReduceEsopCover()
+{
+    ///////////////////////////////////////////////////////////////
+    // SIMPLIFICATION
+    ////////////////////////////////////////////////////////////////////
+
+    long clk1 = clock();
+    int nIterWithoutImprovement = 0;
+    int nIterCount = 0;
+    int GainTotal;
+    int z;
+
+    do
+    {
+//START:
+        if ( g_CoverInfo.Verbosity == 2 )
+            printf( "\nITERATION #%d\n\n", ++nIterCount );
+        else if ( g_CoverInfo.Verbosity == 1 )
+            printf( "." );
+
+        GainTotal  = 0;
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        if ( nIterWithoutImprovement > (int)(g_CoverInfo.Quality>0) )
+        {
+            GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|0 );
+
+            GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|0 );
+        }
+
+        if ( GainTotal )
+            nIterWithoutImprovement = 0;
+        else
+            nIterWithoutImprovement++;
+
+//      if ( g_CoverInfo.Quality >= 2 && nIterWithoutImprovement == 2 )
+//          s_fDecreaseLiterals = 1;
+    }
+    while ( nIterWithoutImprovement < 1 + g_CoverInfo.Quality );
+
+
+    // improve the literal count
+    s_fDecreaseLiterals = 1;
+    for ( z = 0; z < 1; z++ )
+    {
+        if ( g_CoverInfo.Verbosity == 2 )
+            printf( "\nITERATION #%d\n\n", ++nIterCount );
+        else if ( g_CoverInfo.Verbosity == 1 )
+            printf( "." );
+
+        GainTotal  = 0;
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+//      if ( GainTotal )
+//      {
+//          nIterWithoutImprovement = 0;
+//          goto START;
+//      }           
+    }
+
+
+/*  ////////////////////////////////////////////////////////////////////
+    // Print statistics
+    printf( "\nShallow simplification time is ";
+    cout << (float)(clk2 - clk1)/(float)(CLOCKS_PER_SEC) << " sec\n" );
+    printf( "Deep simplification time is ";
+    cout << (float)(clock() - clk2)/(float)(CLOCKS_PER_SEC) << " sec\n" );
+    printf( "Cover after iterative simplification = " << s_nCubesInUse << endl;
+    printf( "Reduced by initial cube writing      = " << g_CoverInfo.nCubesBefore-nCubesAfterWriting << endl;
+    printf( "Reduced by shallow simplification    = " << nCubesAfterWriting-nCubesAfterShallow << endl;
+    printf( "Reduced by deep simplification       = " << nCubesAfterWriting-s_nCubesInUse << endl;
+
+//  printf( "\nThe total number of cubes created = " << g_CoverInfo.cIDs << endl;
+//  printf( "Total number of places in a queque = " << s_nPosAlloc << endl;
+//  printf( "Minimum free places in queque-2 = " << s_nPosMax[0] << endl;
+//  printf( "Minimum free places in queque-3 = " << s_nPosMax[1] << endl;
+//  printf( "Minimum free places in queque-4 = " << s_nPosMax[2] << endl;
+*/  ////////////////////////////////////////////////////////////////////
+
+    // write the number of cubes into cover information 
+    assert ( g_CoverInfo.nCubesInUse + g_CoverInfo.nCubesFree == g_CoverInfo.nCubesAlloc );
+
+//  printf( "\nThe output cover is\n" );
+//  PrintCoverDebug( cout );
+
+    return 0;
+}
+
+//////////////////////////////////////////////////////////////////
+// quite a good script
+//////////////////////////////////////////////////////////////////
+/*
+    long clk1 = clock();
+    int nIterWithoutImprovement = 0;
+    do
+    {
+        PrintQuequeStats();
+        GainTotal  = 0;
+        GainTotal += IterativelyApplyExorLink( DIST2, 0|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 0|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        if ( nIterWithoutImprovement > 2 )
+        {
+            GainTotal += IterativelyApplyExorLink( DIST2, 0|0|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 0|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 );
+        }
+
+        if ( nIterWithoutImprovement > 6 )
+        {
+            GainTotal += IterativelyApplyExorLink( DIST2, 0|0|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 0|0|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 0|0|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 );
+        }
+
+        if ( GainTotal )
+            nIterWithoutImprovement = 0;
+        else
+            nIterWithoutImprovement++;
+    }
+    while ( nIterWithoutImprovement < 12 );
+
+    nCubesAfterShallow = s_nCubesInUse;
+
+*/
+
+/*
+    // alu4 - 439
+    long clk1 = clock();
+    int nIterWithoutImprovement = 0;
+    do
+    {
+        PrintQuequeStats();
+        GainTotal  = 0;
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|0|0 );
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        if ( nIterWithoutImprovement > 2 )
+        {
+            GainTotal += IterativelyApplyExorLink( DIST2, 0|0|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 0|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 );
+        }
+
+        if ( nIterWithoutImprovement > 6 )
+        {
+            GainTotal += IterativelyApplyExorLink( DIST2, 0|0|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 0|0|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 0|0|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 );
+        }
+
+        if ( GainTotal )
+            nIterWithoutImprovement = 0;
+        else
+            nIterWithoutImprovement++;
+    }
+    while ( nIterWithoutImprovement < 12 );
+*/
+
+/*
+// alu4 - 412 cubes, 700 sec
+
+    long clk1 = clock();
+    int nIterWithoutImprovement = 0;
+    int nIterCount = 0;
+    do
+    {
+        printf( "\nITERATION #" << ++nIterCount << endl << endl;
+
+        GainTotal  = 0;
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        if ( nIterWithoutImprovement > 3 )
+        {
+            GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|4 );
+        }
+
+        if ( nIterWithoutImprovement > 7 )
+        {
+            GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|4 );
+        }
+
+        if ( GainTotal )
+            nIterWithoutImprovement = 0;
+        else
+            nIterWithoutImprovement++;
+    }
+    while ( nIterWithoutImprovement < 12 );
+*/
+
+/*
+// pretty good script
+// alu4 = 424   in 250 sec
+
+    long clk1 = clock();
+    int nIterWithoutImprovement = 0;
+    int nIterCount = 0;
+    do
+    {
+        printf( "\nITERATION #" << ++nIterCount << "   |";
+        for ( int k = 0; k < nIterWithoutImprovement; k++ )
+            printf( "*";
+        for ( ; k < 11; k++ )
+            printf( "_";
+        printf( "|" << endl << endl;
+
+        GainTotal  = 0;
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        if ( nIterWithoutImprovement > 2 )
+        {
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+            GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
+        }
+
+        if ( nIterWithoutImprovement > 4 )
+        {
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+            GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
+        }
+
+        if ( GainTotal )
+            nIterWithoutImprovement = 0;
+        else
+            nIterWithoutImprovement++;
+    }
+    while ( nIterWithoutImprovement < 7 );
+*/
+
+/*
+alu4 = 435   70 secs
+
+    long clk1 = clock();
+    int nIterWithoutImprovement = 0;
+    int nIterCount = 0;
+
+    do
+    {
+        printf( "\nITERATION #" << ++nIterCount << endl << endl;
+
+        GainTotal  = 0;
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+
+        if ( GainTotal )
+            nIterWithoutImprovement = 0;
+        else
+            nIterWithoutImprovement++;
+    }
+    while ( nIterWithoutImprovement < 4 );
+*/
+
+/*
+  // the best previous
+  
+    long clk1 = clock();
+    int nIterWithoutImprovement = 0;
+    int nIterCount = 0;
+    int GainTotal;
+    do
+    {
+        if ( g_CoverInfo.Verbosity == 2 )
+        printf( "\nITERATION #" << ++nIterCount << endl << endl;
+        else if ( g_CoverInfo.Verbosity == 1 )
+        cout << '.';
+
+        GainTotal  = 0;
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+        GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+
+        if ( nIterWithoutImprovement > 1 )
+        {
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+            GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+            GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 );
+
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+            GainTotal += IterativelyApplyExorLink( DIST3, 1|2|0 );
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|0 );
+            GainTotal += IterativelyApplyExorLink( DIST3, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST2, 1|2|4 );
+            GainTotal += IterativelyApplyExorLink( DIST4, 1|2|0 );
+        }
+
+        if ( GainTotal )
+            nIterWithoutImprovement = 0;
+        else
+            nIterWithoutImprovement++;
+    }
+//  while ( nIterWithoutImprovement < 20 );
+//  while ( nIterWithoutImprovement < 7 );
+    while ( nIterWithoutImprovement < 1 + g_CoverInfo.Quality );
+
+*/
+
+/*
+// the last tried
+
+    long clk1 = clock();
+    int nIterWithoutImprovement = 0;
+    int nIterCount = 0;
+    int GainTotal;
+    do
+    {
+        if ( g_CoverInfo.Verbosity == 2 )
+        printf( "\nITERATION #" << ++nIterCount << endl << endl;
+        else if ( g_CoverInfo.Verbosity == 1 )
+        cout << '.';
+
+        GainTotal  = 0;
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+        GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+
+        if ( nIterWithoutImprovement > (int)(g_CoverInfo.Quality>0) )
+        {
+            GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|0 );
+
+            GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|0 );
+            GainTotal += IterativelyApplyExorLink3( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink2( 1|2|4 );
+            GainTotal += IterativelyApplyExorLink4( 1|2|0 );
+        }
+
+        if ( GainTotal )
+            nIterWithoutImprovement = 0;
+        else
+            nIterWithoutImprovement++;
+    }
+    while ( nIterWithoutImprovement < 1 + g_CoverInfo.Quality );
+*/
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void AddCubesToStartingCover( Vec_Wec_t * vEsop )
+{
+    Vec_Int_t * vCube;
+    Cube * pNew;
+    int * s_Level2Var;
+    int * s_LevelValues;
+    int c, i, k, Lit, Out;
+
+    s_Level2Var = ABC_ALLOC( int, g_CoverInfo.nVarsIn );
+    s_LevelValues = ABC_ALLOC( int, g_CoverInfo.nVarsIn );
+
+    for ( i = 0; i < g_CoverInfo.nVarsIn; i++ )
+        s_Level2Var[i] = i;
+
+    g_CoverInfo.nLiteralsBefore = 0;
+    Vec_WecForEachLevel( vEsop, vCube, c )
+    {
+        // get the output of this cube
+        Out = -Vec_IntPop(vCube) - 1;
+
+        // fill in the cube with blanks
+        for ( i = 0; i < g_CoverInfo.nVarsIn; i++ )
+            s_LevelValues[i] = VAR_ABS;
+        Vec_IntForEachEntry( vCube, Lit, k )
+        {
+            if ( Abc_LitIsCompl(Lit) )
+                s_LevelValues[Abc_Lit2Var(Lit)] = VAR_NEG;
+            else
+                s_LevelValues[Abc_Lit2Var(Lit)] = VAR_POS;
+        }
+
+        // get the new cube
+        pNew = GetFreeCube();
+        // consider the need to clear the cube
+        if ( pNew->pCubeDataIn[0] ) // this is a recycled cube
+        {
+            for ( i = 0; i < g_CoverInfo.nWordsIn; i++ )
+                pNew->pCubeDataIn[i] = 0;
+            for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+                pNew->pCubeDataOut[i] = 0;
+        }
+
+        InsertVarsWithoutClearing( pNew, s_Level2Var, g_CoverInfo.nVarsIn, s_LevelValues, Out );
+        // set literal counts
+        pNew->a = Vec_IntSize(vCube);
+        pNew->z = 1;
+        // set the ID
+        pNew->ID = g_CoverInfo.cIDs++;
+        // skip through zero-ID
+        if ( g_CoverInfo.cIDs == 256 )
+            g_CoverInfo.cIDs = 1;
+
+        // add this cube to storage
+        CheckForCloseCubes( pNew, 1 );
+
+        g_CoverInfo.nLiteralsBefore += Vec_IntSize(vCube);
+    }
+    ABC_FREE( s_Level2Var );
+    ABC_FREE( s_LevelValues );
+
+    assert ( g_CoverInfo.nCubesInUse + g_CoverInfo.nCubesFree == g_CoverInfo.nCubesAlloc );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs heuristic minimization of ESOPs.]
+
+  Description [Returns 1 on success, 0 on failure.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Exorcism( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut )
+{
+    long clk1;
+    int RemainderBits;
+    int TotalWords;
+    int MemTemp, MemTotal;
+
+    ///////////////////////////////////////////////////////////////////////
+    // STEPS of HEURISTIC ESOP MINIMIZATION
+    ///////////////////////////////////////////////////////////////////////
+    ///////////////////////////////////////////////////////////////////////
+    // STEP 1: determine the size of the starting cover
+    ///////////////////////////////////////////////////////////////////////
+    assert( nIns > 0 );
+    // inputs
+    RemainderBits = (nIns*2)%(sizeof(unsigned)*8);
+    TotalWords    = (nIns*2)/(sizeof(unsigned)*8) + (RemainderBits > 0);
+    g_CoverInfo.nVarsIn  = nIns;
+    g_CoverInfo.nWordsIn = TotalWords;
+    // outputs
+    RemainderBits = (nOuts)%(sizeof(unsigned)*8);
+    TotalWords    = (nOuts)/(sizeof(unsigned)*8) + (RemainderBits > 0);
+    g_CoverInfo.nVarsOut  = nOuts;
+    g_CoverInfo.nWordsOut = TotalWords;
+    g_CoverInfo.cIDs = 1;
+
+    // cubes
+    clk1 = clock();
+//  g_CoverInfo.nCubesBefore = CountTermsInPseudoKroneckerCover( g_Func.dd, nOuts );
+    g_CoverInfo.nCubesBefore = Vec_WecSize(vEsop);
+    g_CoverInfo.TimeStart = clock() - clk1;
+
+    if ( g_CoverInfo.Verbosity )
+    {
+    printf( "Starting cover generation time is %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeStart) );
+    printf( "The number of cubes in the starting cover is %d\n", g_CoverInfo.nCubesBefore );
+    }
+
+    if ( g_CoverInfo.nCubesBefore > 20000 )
+    {
+        printf( "\nThe size of the starting cover is more than 20000 cubes. Quitting...\n" );
+        return 0;
+    }
+
+    ///////////////////////////////////////////////////////////////////////
+    // STEP 2: prepare internal data structures
+    ///////////////////////////////////////////////////////////////////////
+    g_CoverInfo.nCubesAlloc = g_CoverInfo.nCubesBefore + ADDITIONAL_CUBES; 
+
+    // allocate cube cover
+    MemTotal = 0;
+    MemTemp = AllocateCover( g_CoverInfo.nCubesAlloc, g_CoverInfo.nWordsIn, g_CoverInfo.nWordsOut );
+    if ( MemTemp == 0 )
+    {
+        printf( "Unexpected memory allocation problem. Quitting...\n" );
+        return 0;
+    }
+    else 
+        MemTotal += MemTemp;
+
+    // allocate cube sets
+    MemTemp = AllocateCubeSets( g_CoverInfo.nVarsIn, g_CoverInfo.nVarsOut );
+    if ( MemTemp == 0 )
+    {
+        printf( "Unexpected memory allocation problem. Quitting...\n" );
+        return 0;
+    }
+    else 
+        MemTotal += MemTemp;
+
+    // allocate adjacency queques
+    MemTemp = AllocateQueques( g_CoverInfo.nCubesAlloc*g_CoverInfo.nCubesAlloc/CUBE_PAIR_FACTOR );
+    if ( MemTemp == 0 )
+    {
+        printf( "Unexpected memory allocation problem. Quitting...\n" );
+        return 0;
+    }
+    else 
+        MemTotal += MemTemp;
+
+    if ( g_CoverInfo.Verbosity )
+    printf( "Dynamically allocated memory is %dK\n",  MemTotal/1000 );
+
+    ///////////////////////////////////////////////////////////////////////
+    // STEP 3: write the cube cover into the allocated storage
+    ///////////////////////////////////////////////////////////////////////
+    ///////////////////////////////////////////////////////////////////////
+    clk1 = clock();
+    if ( g_CoverInfo.Verbosity )
+    printf( "Generating the starting cover...\n" );
+    AddCubesToStartingCover( vEsop );
+    ///////////////////////////////////////////////////////////////////////
+
+    ///////////////////////////////////////////////////////////////////////
+    // STEP 4: iteratively improve the cover 
+    ///////////////////////////////////////////////////////////////////////
+    if ( g_CoverInfo.Verbosity )
+    printf( "Performing minimization...\n" );
+    clk1 = clock();
+    ReduceEsopCover();
+    g_CoverInfo.TimeMin = clock() - clk1;
+//  g_Func.TimeMin = (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC);
+    if ( g_CoverInfo.Verbosity )
+    {
+    printf( "\nMinimization time is %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeMin) );
+    printf( "\nThe number of cubes after minimization is %d\n", g_CoverInfo.nCubesInUse );
+    }
+
+    ///////////////////////////////////////////////////////////////////////
+    // STEP 5: save the cover into file 
+    ///////////////////////////////////////////////////////////////////////
+    // if option is MULTI_OUTPUT, the output is written into the output file;
+    // if option is SINGLE_NODE, the output is added to the input file
+    // and written into the output file; in this case, the minimized nodes is
+    // also stored in the temporary file "temp.blif" for verification
+
+    // create the file name and write the output
+    {
+        char Buffer[1000];
+        sprintf( Buffer, "%s", pFileNameOut ? pFileNameOut : "temp.esop" );
+        WriteResultIntoFile( Buffer );
+        //if ( g_CoverInfo.Verbosity )
+        printf( "Minimum cover has been written into file <%s>\n", Buffer );
+    }
+
+    ///////////////////////////////////////////////////////////////////////
+    // STEP 6: delocate memory
+    ///////////////////////////////////////////////////////////////////////
+    DelocateCubeSets();
+    DelocateCover();
+    DelocateQueques();
+
+    // return success
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ExorcismMain( Vec_Wec_t * vEsop, int nIns, int nOuts, char * pFileNameOut, int Quality, int Verbosity )
+{
+    memset( &g_CoverInfo, 0, sizeof(cinfo) );
+
+    g_CoverInfo.Quality = Quality;
+    g_CoverInfo.Verbosity = Verbosity;
+
+    printf( "EXORCISM, Ver.4.7: Exclusive Sum-of-Product Minimizer\n" );
+    printf( "by Alan Mishchenko, Portland State University, July-September 2000\n" );
+
+    if ( g_CoverInfo.Verbosity )
+        printf( "Incoming ESOP has %d inputs, %d outputs, and %d cubes.\n", nIns, nOuts, Vec_WecSize(vEsop) );
+
+    PrepareBitSetModule();
+    if ( Exorcism( vEsop, nIns, nOuts, pFileNameOut ) == 0 )
+    {
+        printf( "Something went wrong when minimizing the cover\n" );
+        return 0;
+    }
+    return 1;
+}
+
+
+
+///////////////////////////////////////////////////////////////////
+////////////              End of File             /////////////////
+///////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/exor/exor.h b/src/base/exor/exor.h
new file mode 100644
index 00000000..fc1f546b
--- /dev/null
+++ b/src/base/exor/exor.h
@@ -0,0 +1,178 @@
+/**CFile****************************************************************
+
+  FileName    [exor.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Exclusive sum-of-product minimization.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: exor.h,v 1.0 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///                    Interface of EXORCISM - 4                     ///
+///              An Exclusive Sum-of-Product Minimizer               ///
+///               Alan Mishchenko  <alanmi@ee.pdx.edu>               ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///                         Main Module                              ///
+///                                                                  ///
+///  Ver. 1.0. Started - July 15, 2000. Last update - July 20, 2000  ///
+///  Ver. 1.4. Started - Aug 10, 2000.  Last update - Aug 10, 2000   ///
+///  Ver. 1.7. Started - Sep 20, 2000.  Last update - Sep 23, 2000   ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///   This software was tested with the BDD package "CUDD", v.2.3.0  ///
+///                          by Fabio Somenzi                        ///
+///                  http://vlsi.colorado.edu/~fabio/                ///
+////////////////////////////////////////////////////////////////////////
+
+#ifndef __EXORMAIN_H__
+#define __EXORMAIN_H__
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+#include <time.h>
+#include "misc/vec/vec.h"
+#include "misc/vec/vecWec.h"
+
+ABC_NAMESPACE_HEADER_START 
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+// the number of bits per integer (can be 16, 32, 64 - tested for 32)
+#define BPI                 32 
+#define BPIMASK             31 
+#define LOGBPI               5
+
+// the maximum number of input variables
+#define MAXVARS           1000
+
+// the number of cubes that are allocated additionally
+#define ADDITIONAL_CUBES    33
+
+// the factor showing how many cube pairs will be allocated
+#define CUBE_PAIR_FACTOR    20
+// the following number of cube pairs are allocated:
+// nCubesAlloc/CUBE_PAIR_FACTOR
+
+#if BPI == 64
+#define DIFFERENT   0x5555555555555555
+#define BIT_COUNT(w)   (BitCount[(w)&0xffff] + BitCount[((w)>>16)&0xffff] + BitCount[((w)>>32)&0xffff] + BitCount[(w)>>48])
+#elif BPI == 32
+#define DIFFERENT   0x55555555
+#define BIT_COUNT(w)   (BitCount[(w)&0xffff] + BitCount[(w)>>16])
+#else
+#define DIFFERENT   0x5555
+#define BIT_COUNT(w)   (BitCount[(w)])
+#endif
+
+
+#define VarWord(element)  ((element)>>LOGBPI)
+#define VarBit(element)   ((element)&BPIMASK)
+
+#define TICKS_TO_SECONDS(time) ((float)(time)/(float)(CLOCKS_PER_SEC))
+
+////////////////////////////////////////////////////////////////////////
+///                  CUBE COVER and CUBE typedefs                    ///
+////////////////////////////////////////////////////////////////////////
+
+typedef enum { MULTI_OUTPUT = 1, SINGLE_NODE, MULTI_NODE  } type;
+
+// infomation about the cover
+typedef struct cinfo_tag 
+{
+    int nVarsIn;        // number of input binary variables in the cubes
+    int nVarsOut;       // number of output binary variables in the cubes
+    int nWordsIn;       // number of input words used to represent the cover
+    int nWordsOut;      // number of output words used to represent the cover
+    int nCubesAlloc;    // the number of allocated cubes 
+    int nCubesBefore;   // number of cubes before simplification
+    int nCubesInUse;    // number of cubes after simplification
+    int nCubesFree;     // number of free cubes
+    int nLiteralsBefore;// number of literals before
+    int nLiteralsAfter; // number of literals before
+    int cIDs;           // the counter of cube IDs
+
+    int Verbosity;      // verbosity level
+    int Quality;        // quality
+
+    int TimeRead;       // reading time
+    int TimeStart;      // starting cover computation time
+    int TimeMin;        // pure minimization time
+} cinfo;
+
+// representation of one cube (24 bytes + bit info)
+typedef unsigned int  drow;
+typedef unsigned char byte;
+typedef struct cube 
+{
+    byte  fMark;        // the flag which is TRUE if the cubes is enabled
+    byte  ID;           // (almost) unique ID of the cube
+    short a;            // the number of literals
+    short z;            // the number of 1's in the output part
+    drow* pCubeDataIn;  // a pointer to the bit string representing literals
+    drow* pCubeDataOut; // a pointer to the bit string representing literals
+    struct cube* Prev;  // pointers to the previous/next cubes in the list/ring 
+    struct cube* Next;
+} Cube;
+
+
+// preparation
+extern void PrepareBitSetModule();
+extern int WriteResultIntoFile( char * pFileName );
+
+// iterative ExorLink
+extern int IterativelyApplyExorLink2( char fDistEnable );   
+extern int IterativelyApplyExorLink3( char fDistEnable );   
+extern int IterativelyApplyExorLink4( char fDistEnable );   
+
+// cube storage allocation/delocation
+extern int AllocateCubeSets( int nVarsIn, int nVarsOut );
+extern void DelocateCubeSets();
+
+// adjacency queque allocation/delocation procedures
+extern int AllocateQueques( int nPlaces );
+extern void DelocateQueques();
+
+extern int AllocateCover( int nCubes, int nWordsIn, int nWordsOut );
+extern void DelocateCover();
+
+extern void AddToFreeCubes( Cube* pC );
+extern Cube* GetFreeCube();
+// getting and returning free cubes to the heap
+
+extern void InsertVarsWithoutClearing( Cube * pC, int * pVars, int nVarsIn, int * pVarValues, int Output );
+extern int CheckForCloseCubes( Cube* p, int fAddCube );
+
+extern int FindDiffVars( int *pDiffVars, Cube* pC1, Cube* pC2 );
+// determines the variables that are different in cubes pC1 and pC2
+// returns the number of variables
+
+////////////////////////////////////////////////////////////////////////
+///              VARVALUE and CUBEDIST enum typedefs                 ///
+////////////////////////////////////////////////////////////////////////
+
+// literal values
+typedef enum { VAR_NEG = 1, VAR_POS, VAR_ABS  } varvalue;
+
+// the flag in some function calls can take one of the follwing values
+typedef enum { DIST2, DIST3, DIST4 } cubedist;
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
diff --git a/src/base/exor/exorBits.c b/src/base/exor/exorBits.c
new file mode 100644
index 00000000..41560e65
--- /dev/null
+++ b/src/base/exor/exorBits.c
@@ -0,0 +1,425 @@
+/**CFile****************************************************************
+
+  FileName    [exorBits.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Exclusive sum-of-product minimization.]
+
+  Synopsis    [Bit-level procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: exorBits.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///                  Implementation of EXORCISM - 4                  ///
+///              An Exclusive Sum-of-Product Minimizer               ///
+///                                                                  ///
+///               Alan Mishchenko  <alanmi@ee.pdx.edu>               ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///              EXOR-Oriented Bit String Manipulation               ///
+///                                                                  ///
+///  Ver. 1.0. Started - July 18, 2000. Last update - July 20, 2000  ///
+///  Ver. 1.4. Started -  Aug 10, 2000. Last update -  Aug 10, 2000  ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///   This software was tested with the BDD package "CUDD", v.2.3.0  ///
+///                          by Fabio Somenzi                        ///
+///                  http://vlsi.colorado.edu/~fabio/                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "exor.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       EXTERNAL VARIABLES                         ///
+////////////////////////////////////////////////////////////////////////
+
+// information about the cube cover
+// the number of cubes is constantly updated when the cube cover is processed
+// in this module, only the number of variables (nVarsIn) and integers (nWordsIn)
+// is used, which do not change
+extern cinfo g_CoverInfo;
+
+////////////////////////////////////////////////////////////////////////
+///                  FUNCTIONS OF THIS MODULE                        ///
+////////////////////////////////////////////////////////////////////////
+
+int GetDistance( Cube * pC1, Cube * pC2 );
+// return the distance between two cubes
+int GetDistancePlus( Cube * pC1, Cube * pC2 );
+
+int FindDiffVars( int * pDiffVars, Cube * pC1, Cube * pC2 );
+// determine different variables in cubes from pCubes[] and writes them into pDiffVars
+// returns the number of different variables
+
+void InsertVars( Cube * pC, int * pVars, int nVarsIn, int * pVarValues );
+
+//inline int VarWord( int element );
+//inline int VarBit( int element );
+varvalue GetVar( Cube * pC, int Var );
+
+void ExorVar( Cube * pC, int Var, varvalue Val );
+
+////////////////////////////////////////////////////////////////////////
+///                        STATIC VARIABLES                          ///
+////////////////////////////////////////////////////////////////////////
+
+// the bit count for the first 256 integer numbers
+static unsigned char BitCount8[256] = {
+    0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
+    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
+    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
+    3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
+};
+
+static int SparseNumbers[163] = { 
+    0,1,4,5,16,17,20,21,64,65,68,69,80,81,84,85,256,257,260,
+    261,272,273,276,277,320,321,324,325,336,337,340,1024,1025,
+    1028,1029,1040,1041,1044,1045,1088,1089,1092,1093,1104,1105,
+    1108,1280,1281,1284,1285,1296,1297,1300,1344,1345,1348,1360,
+    4096,4097,4100,4101,4112,4113,4116,4117,4160,4161,4164,4165,
+    4176,4177,4180,4352,4353,4356,4357,4368,4369,4372,4416,4417,
+    4420,4432,5120,5121,5124,5125,5136,5137,5140,5184,5185,5188,
+    5200,5376,5377,5380,5392,5440,16384,16385,16388,16389,16400,
+    16401,16404,16405,16448,16449,16452,16453,16464,16465,16468,
+    16640,16641,16644,16645,16656,16657,16660,16704,16705,16708,
+    16720,17408,17409,17412,17413,17424,17425,17428,17472,17473,
+    17476,17488,17664,17665,17668,17680,17728,20480,20481,20484,
+    20485,20496,20497,20500,20544,20545,20548,20560,20736,20737,
+    20740,20752,20800,21504,21505,21508,21520,21568,21760 
+};
+
+static unsigned char GroupLiterals[163][4] = {
+    {0}, {0}, {1}, {0,1}, {2}, {0,2}, {1,2}, {0,1,2}, {3}, {0,3},
+    {1,3}, {0,1,3}, {2,3}, {0,2,3}, {1,2,3}, {0,1,2,3}, {4}, {0,4},
+    {1,4}, {0,1,4}, {2,4}, {0,2,4}, {1,2,4}, {0,1,2,4}, {3,4},
+    {0,3,4}, {1,3,4}, {0,1,3,4}, {2,3,4}, {0,2,3,4}, {1,2,3,4}, {5},
+    {0,5}, {1,5}, {0,1,5}, {2,5}, {0,2,5}, {1,2,5}, {0,1,2,5}, {3,5},
+    {0,3,5}, {1,3,5}, {0,1,3,5}, {2,3,5}, {0,2,3,5}, {1,2,3,5},
+    {4,5}, {0,4,5}, {1,4,5}, {0,1,4,5}, {2,4,5}, {0,2,4,5},
+    {1,2,4,5}, {3,4,5}, {0,3,4,5}, {1,3,4,5}, {2,3,4,5}, {6}, {0,6},
+    {1,6}, {0,1,6}, {2,6}, {0,2,6}, {1,2,6}, {0,1,2,6}, {3,6},
+    {0,3,6}, {1,3,6}, {0,1,3,6}, {2,3,6}, {0,2,3,6}, {1,2,3,6},
+    {4,6}, {0,4,6}, {1,4,6}, {0,1,4,6}, {2,4,6}, {0,2,4,6},
+    {1,2,4,6}, {3,4,6}, {0,3,4,6}, {1,3,4,6}, {2,3,4,6}, {5,6},
+    {0,5,6}, {1,5,6}, {0,1,5,6}, {2,5,6}, {0,2,5,6}, {1,2,5,6},
+    {3,5,6}, {0,3,5,6}, {1,3,5,6}, {2,3,5,6}, {4,5,6}, {0,4,5,6},
+    {1,4,5,6}, {2,4,5,6}, {3,4,5,6}, {7}, {0,7}, {1,7}, {0,1,7},
+    {2,7}, {0,2,7}, {1,2,7}, {0,1,2,7}, {3,7}, {0,3,7}, {1,3,7},
+    {0,1,3,7}, {2,3,7}, {0,2,3,7}, {1,2,3,7}, {4,7}, {0,4,7},
+    {1,4,7}, {0,1,4,7}, {2,4,7}, {0,2,4,7}, {1,2,4,7}, {3,4,7},
+    {0,3,4,7}, {1,3,4,7}, {2,3,4,7}, {5,7}, {0,5,7}, {1,5,7},
+    {0,1,5,7}, {2,5,7}, {0,2,5,7}, {1,2,5,7}, {3,5,7}, {0,3,5,7},
+    {1,3,5,7}, {2,3,5,7}, {4,5,7}, {0,4,5,7}, {1,4,5,7}, {2,4,5,7},
+    {3,4,5,7}, {6,7}, {0,6,7}, {1,6,7}, {0,1,6,7}, {2,6,7},
+    {0,2,6,7}, {1,2,6,7}, {3,6,7}, {0,3,6,7}, {1,3,6,7}, {2,3,6,7},
+    {4,6,7}, {0,4,6,7}, {1,4,6,7}, {2,4,6,7}, {3,4,6,7}, {5,6,7},
+    {0,5,6,7}, {1,5,6,7}, {2,5,6,7}, {3,5,6,7}, {4,5,6,7} 
+};
+
+// the bit count to 16-bit numbers
+#define FULL16BITS  0x10000
+#define MARKNUMBER  200
+
+static unsigned char BitGroupNumbers[FULL16BITS];
+unsigned char BitCount[FULL16BITS];
+
+////////////////////////////////////////////////////////////////////////
+///                      FUNCTION DEFINITIONS                        ///
+////////////////////////////////////////////////////////////////////////
+
+void PrepareBitSetModule()
+// this function should be called before anything is done with the cube cover
+{   
+    // prepare bit count
+    int i, k;
+    int nLimit;
+    
+    nLimit = FULL16BITS;
+    for ( i = 0; i < nLimit; i++ )
+    {
+        BitCount[i] = BitCount8[ i & 0xff ] + BitCount8[ i>>8 ];
+        BitGroupNumbers[i] = MARKNUMBER;
+    }
+    // prepare bit groups
+    for ( k = 0; k < 163; k++ )
+        BitGroupNumbers[ SparseNumbers[k] ] = k;
+/*
+    // verify bit groups
+    int n = 4368;
+    char Buff[100];
+    cout << "The number is " << n << endl;
+    cout << "The binary is " << itoa(n,Buff,2) << endl;
+    cout << "BitGroupNumbers[n] is " << (int)BitGroupNumbers[n] << endl;
+    cout << "The group literals are ";
+    for ( int g = 0; g < 4; g++ )
+        cout << " " << (int)GroupLiterals[BitGroupNumbers[n]][g];
+*/
+}
+
+////////////////////////////////////////////////////////////////////////
+///                   INLINE FUNCTION DEFINITIONS                    ///
+////////////////////////////////////////////////////////////////////////
+/*
+int VarWord( int element )
+{
+    return ( element >> LOGBPI );
+}
+
+int VarBit( int element )
+{
+    return ( element & BPIMASK );
+}
+*/
+
+varvalue GetVar( Cube * pC, int Var )
+// returns VAR_NEG if var is neg, VAR_POS if var is pos, VAR_ABS if var is absent
+{
+    int Bit = (Var<<1);
+    int Value = ((pC->pCubeDataIn[VarWord(Bit)] >> VarBit(Bit)) & 3);
+    assert( Value == VAR_NEG || Value == VAR_POS || Value == VAR_ABS );
+    return (varvalue)Value;
+}
+
+void ExorVar( Cube * pC, int Var, varvalue Val )
+// EXORs the value Val with the value of variable Var in the given cube
+// ((cube[VAR_WORD((v)<<1)]) ^ ( (pol)<<VAR_BIT((v)<<1) ))
+{
+    int Bit = (Var<<1);
+    pC->pCubeDataIn[VarWord(Bit)] ^= ( Val << VarBit(Bit) );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                      FUNCTION DEFINITIONS                        ///
+////////////////////////////////////////////////////////////////////////
+
+static int DiffVarCounter, cVars;
+static drow Temp1, Temp2, Temp;
+static drow LastNonZeroWord;
+static int LastNonZeroWordNum;
+
+int GetDistance( Cube * pC1, Cube * pC2 )
+// finds and returns the distance between two cubes pC1 and pC2
+{
+    int i;
+    DiffVarCounter = 0;
+
+    for ( i = 0; i < g_CoverInfo.nWordsIn; i++ )
+    {
+        Temp1 = pC1->pCubeDataIn[i] ^ pC2->pCubeDataIn[i];
+        Temp2 = (Temp1|(Temp1>>1)) & DIFFERENT;
+
+        // count how many bits are one in this var difference
+        DiffVarCounter  += BIT_COUNT(Temp2);
+        if ( DiffVarCounter > 4 )
+            return 5;
+    }
+    // check whether the output parts are different
+    for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+        if ( pC1->pCubeDataOut[i] ^ pC2->pCubeDataOut[i] )
+        {
+            DiffVarCounter++;
+            break;
+        }
+    return DiffVarCounter;
+}
+
+// place to put the number of the different variable and its value in the second cube
+extern int s_DiffVarNum;
+extern int s_DiffVarValueP_old;
+extern int s_DiffVarValueP_new;
+extern int s_DiffVarValueQ;
+
+int GetDistancePlus( Cube * pC1, Cube * pC2 )
+// finds and returns the distance between two cubes pC1 and pC2
+// if the distance is 1, returns the number of diff variable in VarNum
+{
+    int i;
+
+    DiffVarCounter = 0;
+    LastNonZeroWordNum = -1;
+    for ( i = 0; i < g_CoverInfo.nWordsIn; i++ )
+    {
+        Temp1 = pC1->pCubeDataIn[i] ^ pC2->pCubeDataIn[i];
+        Temp2 = (Temp1|(Temp1>>1)) & DIFFERENT;
+
+        // save the value of var difference, in case 
+        // the distance is one and we need to return the var number
+        if ( Temp2 )
+        {
+            LastNonZeroWordNum = i;
+            LastNonZeroWord = Temp2;
+        }
+
+        // count how many bits are one in this var difference
+        DiffVarCounter  += BIT_COUNT(Temp2);
+        if ( DiffVarCounter > 4 )
+            return 5;
+    }
+    // check whether the output parts are different
+    for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+        if ( pC1->pCubeDataOut[i] ^ pC2->pCubeDataOut[i] )
+        {
+            DiffVarCounter++;
+            break;
+        }
+
+    if ( DiffVarCounter == 1 )
+    {
+        if ( LastNonZeroWordNum == -1 ) // the output is the only different variable
+            s_DiffVarNum = -1;
+        else
+        {
+            Temp = (LastNonZeroWord>>2);
+            for ( i = 0; Temp; Temp>>=2, i++ );
+            s_DiffVarNum = LastNonZeroWordNum*BPI/2 + i;
+
+            // save the old var value
+            s_DiffVarValueP_old = GetVar( pC1, s_DiffVarNum );
+            s_DiffVarValueQ = GetVar( pC2, s_DiffVarNum );
+
+            // EXOR this value with the corresponding value in p cube           
+            ExorVar( pC1, s_DiffVarNum, (varvalue)s_DiffVarValueQ );
+
+            s_DiffVarValueP_new = GetVar( pC1, s_DiffVarNum );
+        }
+    }
+
+    return DiffVarCounter;
+}
+
+int FindDiffVars( int * pDiffVars, Cube * pC1, Cube * pC2 )
+// determine different variables in two cubes and 
+// writes them into pDiffVars[]
+// -1 is written into pDiffVars[0] if the cubes have different outputs
+// returns the number of different variables (including the output)
+{
+    int i, v;
+    DiffVarCounter = 0;
+    // check whether the output parts of the cubes are different
+
+    for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+        if ( pC1->pCubeDataOut[i] != pC2->pCubeDataOut[i] )
+        { // they are different
+            pDiffVars[0] = -1;
+            DiffVarCounter = 1;
+            break;
+        }
+
+    for ( i = 0; i < g_CoverInfo.nWordsIn; i++ )
+    {
+
+        Temp1 = pC1->pCubeDataIn[i] ^ pC2->pCubeDataIn[i];
+        Temp2 = (Temp1|(Temp1>>1)) & DIFFERENT;
+
+        // check the first part of this word
+        Temp = Temp2 & 0xffff;
+        cVars = BitCount[ Temp ];
+        if ( cVars )
+        {
+            if ( cVars < 5 )
+                for ( v = 0; v < cVars; v++ )
+                {
+                    assert( BitGroupNumbers[Temp] != MARKNUMBER );
+                    pDiffVars[ DiffVarCounter++ ] = i*16 + GroupLiterals[ BitGroupNumbers[Temp] ][v];
+                }
+            else
+                return 5;
+        }
+        if ( DiffVarCounter > 4 )
+            return 5;
+
+        // check the second part of this word
+        Temp = Temp2 >> 16;
+        cVars = BitCount[ Temp ];
+        if ( cVars )
+        {
+            if ( cVars < 5 )
+                for ( v = 0; v < cVars; v++ )
+                {
+                    assert( BitGroupNumbers[Temp] != MARKNUMBER );
+                    pDiffVars[ DiffVarCounter++ ] = i*16 + 8 + GroupLiterals[ BitGroupNumbers[Temp] ][v];
+                }
+            else
+                return 5;
+        }
+        if ( DiffVarCounter > 4 )
+            return 5;
+    }
+    return DiffVarCounter;
+}
+
+void InsertVars( Cube * pC, int * pVars, int nVarsIn, int * pVarValues )
+// corrects the given number of variables (nVarsIn) in pC->pCubeDataIn[]
+// variable numbers are given in pVarNumbers[], their values are in pVarValues[]
+// arrays pVarNumbers[] and pVarValues[] are provided by the user
+{
+    int GlobalBit;
+    int LocalWord;
+    int LocalBit;
+    int i;
+    assert( nVarsIn > 0 && nVarsIn <= g_CoverInfo.nVarsIn );
+    for ( i = 0; i < nVarsIn; i++ )
+    {
+        assert( pVars[i] >= 0 && pVars[i] < g_CoverInfo.nVarsIn );
+        assert( pVarValues[i] == VAR_NEG || pVarValues[i] == VAR_POS || pVarValues[i] == VAR_ABS );
+        GlobalBit = (pVars[i]<<1);
+        LocalWord = VarWord(GlobalBit);
+        LocalBit  = VarBit(GlobalBit);
+
+        // correct this variables
+        pC->pCubeDataIn[LocalWord] = ((pC->pCubeDataIn[LocalWord]&(~(3<<LocalBit)))|(pVarValues[i]<<LocalBit));
+    }
+}
+
+void InsertVarsWithoutClearing( Cube * pC, int * pVars, int nVarsIn, int * pVarValues, int Output )
+// corrects the given number of variables (nVarsIn) in pC->pCubeDataIn[]
+// variable numbers are given in pVarNumbers[], their values are in pVarValues[]
+// arrays pVarNumbers[] and pVarValues[] are provided by the user
+{
+    int GlobalBit;
+    int LocalWord;
+    int LocalBit;
+    int i;
+    assert( nVarsIn > 0 && nVarsIn <= g_CoverInfo.nVarsIn );
+    for ( i = 0; i < nVarsIn; i++ )
+    {
+        assert( pVars[i] >= 0 && pVars[i] < g_CoverInfo.nVarsIn );
+        assert( pVarValues[i] == VAR_NEG || pVarValues[i] == VAR_POS || pVarValues[i] == VAR_ABS );
+        GlobalBit = (pVars[i]<<1);
+        LocalWord = VarWord(GlobalBit);
+        LocalBit  = VarBit(GlobalBit);
+
+        // correct this variables
+        pC->pCubeDataIn[LocalWord] |= ( pVarValues[i] << LocalBit );
+    }
+    // insert the output bit
+    pC->pCubeDataOut[VarWord(Output)] |= ( 1 << VarBit(Output) );
+}
+
+///////////////////////////////////////////////////////////////////
+////////////              End of File             /////////////////
+///////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/base/exor/exorCubes.c b/src/base/exor/exorCubes.c
new file mode 100644
index 00000000..c8b40a82
--- /dev/null
+++ b/src/base/exor/exorCubes.c
@@ -0,0 +1,190 @@
+/**CFile****************************************************************
+
+  FileName    [exorCubes.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Exclusive sum-of-product minimization.]
+
+  Synopsis    [Cube manipulation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: exorCubes.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///                  Implementation of EXORCISM - 4                  ///
+///              An Exclusive Sum-of-Product Minimizer               ///
+///                                                                  ///
+///               Alan Mishchenko  <alanmi@ee.pdx.edu>               ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///              Cube Allocation and Free Cube Management            ///
+///                                                                  ///
+///  Ver. 1.0. Started - July 18, 2000. Last update - July 20, 2000  ///
+///  Ver. 1.1. Started - July 24, 2000. Last update - July 29, 2000  ///
+///  Ver. 1.2. Started - July 30, 2000. Last update - July 30, 2000  ///
+///  Ver. 1.5. Started -  Aug 19, 2000. Last update -  Aug 19, 2000  ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///   This software was tested with the BDD package "CUDD", v.2.3.0  ///
+///                          by Fabio Somenzi                        ///
+///                  http://vlsi.colorado.edu/~fabio/                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "exor.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                       EXTERNAL FUNCTIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                       EXTERNAL VARIABLES                         ///
+////////////////////////////////////////////////////////////////////////
+
+// information about the cube cover before and after simplification
+extern cinfo g_CoverInfo;
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTIONS OF THIS MODULE                      ///
+////////////////////////////////////////////////////////////////////////
+
+// cube cover memory allocation/delocation procedures
+// (called from the ExorMain module)
+int AllocateCover( int nCubes, int nWordsIn, int nWordsOut );
+void DelocateCover();
+
+// manipulation of the free cube list
+// (called from Pseudo-Kronecker, ExorList, and ExorLink modules)
+void AddToFreeCubes( Cube * pC );
+Cube * GetFreeCube();
+
+////////////////////////////////////////////////////////////////////////
+///                      EXPORTED VARIABLES                          ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      STATIC VARIABLES                            ///
+////////////////////////////////////////////////////////////////////////
+
+// the pointer to the allocated memory
+Cube ** s_pCoverMemory;
+
+// the list of free cubes
+Cube * s_CubesFree;
+
+///////////////////////////////////////////////////////////////////
+///                  CUBE COVER MEMORY MANAGEMENT                //
+///////////////////////////////////////////////////////////////////
+
+int AllocateCover( int nCubes, int nWordsIn, int nWordsOut )
+// uses the cover parameters nCubes and nWords
+// to allocate-and-clean the cover in one large piece
+{
+    int OneCubeSize;
+    int OneInputSetSize;
+    Cube ** pp;
+    int TotalSize;
+    int i, k;
+
+    // determine the size of one cube WITH storage for bits
+    OneCubeSize = sizeof(Cube) + (nWordsIn+nWordsOut)*sizeof(unsigned);
+    // determine what is the amount of storage for the input part of the cube 
+    OneInputSetSize = nWordsIn*sizeof(unsigned);
+
+    // allocate memory for the array of pointers
+    pp = (Cube **)ABC_ALLOC( Cube *, nCubes );
+    if ( pp == NULL )
+        return 0;
+
+    // determine the size of the total cube cover
+    TotalSize = nCubes*OneCubeSize;
+    // allocate and clear memory for the cover in one large piece
+    pp[0] = (Cube *)ABC_ALLOC( char, TotalSize );
+    if ( pp[0] == NULL )
+        return 0;
+    memset( pp[0], 0, TotalSize );
+
+    // assign pointers to cubes and bit strings inside this piece
+    pp[0]->pCubeDataIn  = (unsigned*)(pp[0] + 1);
+    pp[0]->pCubeDataOut = (unsigned*)((char*)pp[0]->pCubeDataIn + OneInputSetSize);
+    for ( i = 1; i < nCubes; i++ )
+    {
+        pp[i] = (Cube *)((char*)pp[i-1] + OneCubeSize);
+        pp[i]->pCubeDataIn = (unsigned*)(pp[i] + 1);
+        pp[i]->pCubeDataOut = (unsigned*)((char*)pp[i]->pCubeDataIn + OneInputSetSize);
+    }
+
+    // connect the cubes into the list using Next pointers
+    for ( k = 0; k < nCubes-1; k++ )
+        pp[k]->Next = pp[k+1];
+    // the last pointer is already set to NULL
+
+    // assign the head of the free list
+    s_CubesFree = pp[0];
+    // set the counters of the used and free cubes
+    g_CoverInfo.nCubesInUse = 0;
+    g_CoverInfo.nCubesFree = nCubes;
+
+    // save the pointer to the allocated memory
+    s_pCoverMemory = pp;
+
+    assert ( g_CoverInfo.nCubesInUse + g_CoverInfo.nCubesFree == g_CoverInfo.nCubesAlloc );
+
+    return nCubes*sizeof(Cube *) + TotalSize;
+}
+
+void DelocateCover()
+{
+    ABC_FREE( s_pCoverMemory[0] );
+    ABC_FREE( s_pCoverMemory );
+}
+
+///////////////////////////////////////////////////////////////////
+///           FREE CUBE LIST MANIPULATION FUNCTIONS             ///
+///////////////////////////////////////////////////////////////////
+
+void AddToFreeCubes( Cube * p )
+{
+    assert( p );
+    assert( p->Prev == NULL ); // the cube should not be in use
+    assert( p->Next == NULL );
+    assert( p->ID );
+
+    p->Next = s_CubesFree;
+    s_CubesFree = p;
+
+    // set the ID of the cube to 0, 
+    // so that cube pair garbage collection could recognize it as different
+    p->ID = 0;
+
+    g_CoverInfo.nCubesFree++;
+}
+
+Cube * GetFreeCube()
+{
+    Cube * p;
+    assert( s_CubesFree );
+    p = s_CubesFree;
+    s_CubesFree = s_CubesFree->Next;
+    p->Next = NULL;
+    g_CoverInfo.nCubesFree--;
+    return p;
+}
+
+///////////////////////////////////////////////////////////////////
+////////////              End of File             /////////////////
+///////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/base/exor/exorLink.c b/src/base/exor/exorLink.c
new file mode 100644
index 00000000..032ed318
--- /dev/null
+++ b/src/base/exor/exorLink.c
@@ -0,0 +1,746 @@
+/**CFile****************************************************************
+
+  FileName    [exorLink.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Exclusive sum-of-product minimization.]
+
+  Synopsis    [Cube iterators.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: exorLink.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///                  Implementation of EXORCISM - 4                  ///
+///              An Exclusive Sum-of-Product Minimizer               ///
+///                                                                  ///
+///               Alan Mishchenko  <alanmi@ee.pdx.edu>               ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///                 Generation of ExorLinked Cubes                   ///
+///                                                                  ///
+///  Ver. 1.0. Started - July 26, 2000. Last update - July 29, 2000  ///
+///  Ver. 1.4. Started -  Aug 10, 2000. Last update -  Aug 12, 2000  ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///   This software was tested with the BDD package "CUDD", v.2.3.0  ///
+///                          by Fabio Somenzi                        ///
+///                  http://vlsi.colorado.edu/~fabio/                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "exor.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                       MACRO DEFINITIONS                          ///
+////////////////////////////////////////////////////////////////////////
+
+#define LARGE_NUM 1000000
+
+////////////////////////////////////////////////////////////////////////
+///                 EXTERNAL FUNCTION DECLARATIONS                   ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTIONS OF THIS MODULE                      ///
+////////////////////////////////////////////////////////////////////////
+
+int ExorLinkCubeIteratorStart( Cube** pGroup, Cube* pC1, Cube* pC2, cubedist Dist );
+// this function starts the Exor-Link iterator, which iterates
+// through the cube groups starting from the group with min literals
+// returns 1 on success, returns 0 if the cubes have wrong distance
+
+int ExorLinkCubeIteratorNext( Cube** pGroup );
+// give the next group in the decreasing order of sum of literals
+// returns 1 on success, returns 0 if there are no more groups
+
+int ExorLinkCubeIteratorPick( Cube** pGroup, int g );
+// gives the group #g in the order in which the groups were given
+// during iteration
+// returns 1 on success, returns 0 if something g is too large
+
+void ExorLinkCubeIteratorCleanUp( int fTakeLastGroup );
+// removes the cubes from the store back into the list of free cubes
+// if fTakeLastGroup is 0, removes all cubes
+// if fTakeLastGroup is 1, does not store the last group
+
+////////////////////////////////////////////////////////////////////////
+///                       EXTERNAL VARIABLES                         ///
+////////////////////////////////////////////////////////////////////////
+
+// information about the cube cover before
+extern cinfo g_CoverInfo;
+// new IDs are assigned only when it is known that the cubes are useful
+// this is done in ExorLinkCubeIteratorCleanUp();
+
+// the head of the list of free cubes
+extern Cube* g_CubesFree;
+
+extern byte BitCount[];
+
+////////////////////////////////////////////////////////////////////////
+///                         EXORLINK INFO                            ///
+////////////////////////////////////////////////////////////////////////
+
+const int s_ELMax = 4;
+
+// ExorLink-2: there are 4 cubes,  2 literals each, combined into 2 groups
+// ExorLink-3: there are 12 cubes, 3 literals each, combined into 6 groups
+// ExorLink-4: there are 32 cubes, 4 literals each, combined into 24 groups
+// ExorLink-5: there are 80 cubes, 5 literals each, combined into 120 groups
+// Exorlink-n: there are n*2^(n-1) cubes, n literals each, combined into n! groups
+const int s_ELnCubes[4]  = { 4, 12, 32, 80 };
+const int s_ELnGroups[4] = { 2,  6, 24, 120 };
+
+// value sets of cubes X{a0}Y{b0}Z{c0}U{d0} and X{a1}Y{b1}Z{c1}U{d1}
+// used to represent the ExorLink cube generation rules
+enum { vs0, vs1, vsX };
+// vs0 = 0, // the value set of the first cube 
+// vs1 = 1, // the value set of the second cube
+// vsX = 2  // EXOR of the value sets of the first and second cubes
+
+// representation of ExorLinked cubes
+static int s_ELCubeRules[3][32][4]  = {
+{ // ExorLink-2 Cube Generating Rules
+                       // | 0 | 1 | - sections
+                       // |-------|
+    {vsX,vs0}, // cube 0  |   |   |
+    {vsX,vs1}, // cube 1  |   | 0 |
+    {vs0,vsX}, // cube 2  |   |   |
+    {vs1,vsX}  // cube 3  | 0 |   |
+},
+{ // ExorLink-3 Cube Generating Rules
+                            // | 0 | 1 | 2 | - sections
+                            // |-----------|
+    {vsX,vs0,vs0}, // cube 0   |   |   |   |
+    {vsX,vs0,vs1}, // cube 1   |   |   | 0 |
+    {vsX,vs1,vs0}, // cube 2   |   | 0 |   |
+    {vsX,vs1,vs1}, // cube 3   |   | 1 | 1 |
+
+    {vs0,vsX,vs0}, // cube 4   |   |   |   |
+    {vs0,vsX,vs1}, // cube 5   |   |   | 2 |
+    {vs1,vsX,vs0}, // cube 6   | 0 |   |   |
+    {vs1,vsX,vs1}, // cube 7   | 1 |   | 3 |
+
+    {vs0,vs0,vsX}, // cube 8   |   |   |   |
+    {vs0,vs1,vsX}, // cube 9   |   | 2 |   |
+    {vs1,vs0,vsX}, // cube 10  | 2 |   |   |
+    {vs1,vs1,vsX}  // cube 11  | 3 | 3 |   |
+},
+{ // ExorLink-4 Rules Generating Rules
+                                // | 0 | 1 | 2 | 4 | - sections
+                                // |---------------|
+    {vsX,vs0,vs0,vs0}, // cube 0   |   |   |   |   |
+    {vsX,vs0,vs0,vs1}, // cube 1   |   |   |   | 0 |
+    {vsX,vs0,vs1,vs0}, // cube 2   |   |   | 0 |   |
+    {vsX,vs0,vs1,vs1}, // cube 3   |   |   | 1 | 1 |
+    {vsX,vs1,vs0,vs0}, // cube 4   |   | 0 |   |   |
+    {vsX,vs1,vs0,vs1}, // cube 5   |   | 1 |   | 2 |
+    {vsX,vs1,vs1,vs0}, // cube 6   |   | 2 | 2 |   |
+    {vsX,vs1,vs1,vs1}, // cube 7   |   | 3 | 3 | 3 |
+
+    {vs0,vsX,vs0,vs0}, // cube 8   |   |   |   |   |
+    {vs0,vsX,vs0,vs1}, // cube 9   |   |   |   | 4 |
+    {vs0,vsX,vs1,vs0}, // cube 10  |   |   | 4 |   |
+    {vs0,vsX,vs1,vs1}, // cube 11  |   |   | 5 | 5 |
+    {vs1,vsX,vs0,vs0}, // cube 12  | 0 |   |   |   |
+    {vs1,vsX,vs0,vs1}, // cube 13  | 1 |   |   | 6 |
+    {vs1,vsX,vs1,vs0}, // cube 14  | 2 |   | 6 |   |
+    {vs1,vsX,vs1,vs1}, // cube 15  | 3 |   | 7 | 7 |
+
+    {vs0,vs0,vsX,vs0}, // cube 16  |   |   |   |   |
+    {vs0,vs0,vsX,vs1}, // cube 17  |   |   |   | 8 |
+    {vs0,vs1,vsX,vs0}, // cube 18  |   | 4 |   |   |
+    {vs0,vs1,vsX,vs1}, // cube 19  |   | 5 |   | 9 |
+    {vs1,vs0,vsX,vs0}, // cube 20  | 4 |   |   |   |
+    {vs1,vs0,vsX,vs1}, // cube 21  | 5 |   |   | 10|
+    {vs1,vs1,vsX,vs0}, // cube 22  | 6 | 6 |   |   |
+    {vs1,vs1,vsX,vs1}, // cube 23  | 7 | 7 |   | 11|
+
+    {vs0,vs0,vs0,vsX}, // cube 24  |   |   |   |   |
+    {vs0,vs0,vs1,vsX}, // cube 25  |   |   | 8 |   |
+    {vs0,vs1,vs0,vsX}, // cube 26  |   | 8 |   |   |
+    {vs0,vs1,vs1,vsX}, // cube 27  |   | 9 | 9 |   |
+    {vs1,vs0,vs0,vsX}, // cube 28  | 8 |   |   |   |
+    {vs1,vs0,vs1,vsX}, // cube 29  | 9 |   | 10|   |
+    {vs1,vs1,vs0,vsX}, // cube 30  | 10| 10|   |   |
+    {vs1,vs1,vs1,vsX}  // cube 31  | 11| 11| 11|   |
+}
+};
+
+// these cubes are combined into groups
+static int s_ELGroupRules[3][24][4] = { 
+{ // ExorLink-2 Group Forming Rules
+    {0,3},  // group 0 - section 0
+    {2,1}   // group 1 - section 1
+},
+{ // ExorLink-3 Group Forming Rules
+    {0,6,11}, // group 0 - section 0 
+    {0,7,10}, // group 1
+    {4,2,11}, // group 2 - section 1 
+    {4,3,9},  // group 3
+    {8,1,7},  // group 4 - section 2 
+    {8,3,5}   // group 5
+},
+{ // ExorLink-4 Group Forming Rules 
+// section 0: (0-12)(1-13)(2-14)(3-15)(4-20)(5-21)(6-22)(7-23)(8-28)(9-29)(10-30)(11-31)
+    {0,12,22,31},  // group 0       // {0,6,11}, // group 0  - section 0
+    {0,12,23,30},  // group 1       // {0,7,10}, // group 1
+    {0,20,14,31},  // group 2       // {4,2,11}, // group 2
+    {0,20,15,29},  // group 3       // {4,3,9},  // group 3
+    {0,28,13,23},  // group 4       // {8,1,7},  // group 4
+    {0,28,15,21},  // group 5       // {8,3,5}   // group 5
+// section 1: (0-4)(1-5)(2-6)(3-7)(4-18)(5-19)(6-22)(7-23)(8-26)(9-27)(10-30)(11-31)
+    {8,4,22,31},   // group 6
+    {8,4,23,30},   // group 7
+    {8,18,6,31},   // group 8
+    {8,18,7,27},   // group 9
+    {8,26,5,23},   // group 10
+    {8,26,7,19},   // group 11
+// section 2: (0-2)(1-3)(2-6)(3-7)(4-10)(5-11)(6-14)(7-15)(8-25)(9-27)(10-29)(11-31)
+    {16,2,14,31},  // group 12
+    {16,2,15,29},  // group 13
+    {16,10,6,31},  // group 14
+    {16,10,7,27},  // group 15
+    {16,25,3,15},  // group 16
+    {16,25,7,11},  // group 17
+// section 3: (0-1)(1-3)(2-5)(3-7)(4-9)(5-11)(6-13)(7-15)(8-17)(9-19)(10-21)(11-23)
+    {24,1,13,23},  // group 18
+    {24,1,15,21},  // group 19
+    {24,9, 5,23},  // group 20
+    {24,9, 7,19},  // group 21
+    {24,17,3,15},  // group 22
+    {24,17,7,11}   // group 23
+}
+};
+
+// it is assumed that if literals in the first cube, second cube 
+// and their EXOR are 0 or 1 (as opposed to -), they are written
+// into a mask, which is used to count the number of literals in 
+// the cube groups cubes
+//
+// below is the set of masks selecting literals belonging
+// to the given cube of the group
+
+static drow s_CubeLitMasks[3][32] = { 
+{  // ExorLink-2 Literal Counting Masks
+//                      v3   v2   v1   v0
+//                     -xBA -xBA -xBA -xBA  
+//                     -------------------
+    0x14,  // cube 0  <0000 0000 0001 0100> {vsX,vs0}
+    0x24,  // cube 1  <0000 0000 0010 0100> {vsX,vs1}
+    0x41,  // cube 2  <0000 0000 0100 0001> {vs0,vsX}
+    0x42,  // cube 3  <0000 0000 0100 0010> {vs1,vsX}
+},
+{  // ExorLink-3 Literal Counting Masks
+    0x114, // cube 0  <0000 0001 0001 0100> {vsX,vs0,vs0}
+    0x214, // cube 1  <0000 0010 0001 0100> {vsX,vs0,vs1}
+    0x124, // cube 2  <0000 0001 0010 0100> {vsX,vs1,vs0}
+    0x224, // cube 3  <0000 0010 0010 0100> {vsX,vs1,vs1}
+    0x141, // cube 4  <0000 0001 0100 0001> {vs0,vsX,vs0}
+    0x241, // cube 5  <0000 0010 0100 0001> {vs0,vsX,vs1}
+    0x142, // cube 6  <0000 0001 0100 0010> {vs1,vsX,vs0}
+    0x242, // cube 7  <0000 0010 0100 0010> {vs1,vsX,vs1}
+    0x411, // cube 8  <0000 0100 0001 0001> {vs0,vs0,vsX}
+    0x421, // cube 9  <0000 0100 0010 0001> {vs0,vs1,vsX}
+    0x412, // cube 10 <0000 0100 0001 0010> {vs1,vs0,vsX}
+    0x422, // cube 11 <0000 0100 0010 0010> {vs1,vs1,vsX}
+},
+{  // ExorLink-4 Literal Counting Masks
+    0x1114, // cube 0   <0001 0001 0001 0100> {vsX,vs0,vs0,vs0}
+    0x2114, // cube 1   <0010 0001 0001 0100> {vsX,vs0,vs0,vs1}
+    0x1214, // cube 2   <0001 0010 0001 0100> {vsX,vs0,vs1,vs0}
+    0x2214, // cube 3   <0010 0010 0001 0100> {vsX,vs0,vs1,vs1}
+    0x1124, // cube 4   <0001 0001 0010 0100> {vsX,vs1,vs0,vs0}
+    0x2124, // cube 5   <0010 0001 0010 0100> {vsX,vs1,vs0,vs1}
+    0x1224, // cube 6   <0001 0010 0010 0100> {vsX,vs1,vs1,vs0}
+    0x2224, // cube 7   <0010 0010 0010 0100> {vsX,vs1,vs1,vs1}
+    0x1141, // cube 8   <0001 0001 0100 0001> {vs0,vsX,vs0,vs0}
+    0x2141, // cube 9   <0010 0001 0100 0001> {vs0,vsX,vs0,vs1}
+    0x1241, // cube 10  <0001 0010 0100 0001> {vs0,vsX,vs1,vs0}
+    0x2241, // cube 11  <0010 0010 0100 0001> {vs0,vsX,vs1,vs1}
+    0x1142, // cube 12  <0001 0001 0100 0010> {vs1,vsX,vs0,vs0}
+    0x2142, // cube 13  <0010 0001 0100 0010> {vs1,vsX,vs0,vs1}
+    0x1242, // cube 14  <0001 0010 0100 0010> {vs1,vsX,vs1,vs0}
+    0x2242, // cube 15  <0010 0010 0100 0010> {vs1,vsX,vs1,vs1}
+    0x1411, // cube 16  <0001 0100 0001 0001> {vs0,vs0,vsX,vs0}
+    0x2411, // cube 17  <0010 0100 0001 0001> {vs0,vs0,vsX,vs1}
+    0x1421, // cube 18  <0001 0100 0010 0001> {vs0,vs1,vsX,vs0}
+    0x2421, // cube 19  <0010 0100 0010 0001> {vs0,vs1,vsX,vs1}
+    0x1412, // cube 20  <0001 0100 0001 0010> {vs1,vs0,vsX,vs0}
+    0x2412, // cube 21  <0010 0100 0001 0010> {vs1,vs0,vsX,vs1}
+    0x1422, // cube 22  <0001 0100 0010 0010> {vs1,vs1,vsX,vs0}
+    0x2422, // cube 23  <0010 0100 0010 0010> {vs1,vs1,vsX,vs1}
+    0x4111, // cube 24  <0100 0001 0001 0001> {vs0,vs0,vs0,vsX}
+    0x4211, // cube 25  <0100 0010 0001 0001> {vs0,vs0,vs1,vsX}
+    0x4121, // cube 26  <0100 0001 0010 0001> {vs0,vs1,vs0,vsX}
+    0x4221, // cube 27  <0100 0010 0010 0001> {vs0,vs1,vs1,vsX}
+    0x4112, // cube 28  <0100 0001 0001 0010> {vs1,vs0,vs0,vsX}
+    0x4212, // cube 29  <0100 0010 0001 0010> {vs1,vs0,vs1,vsX}
+    0x4122, // cube 30  <0100 0001 0010 0010> {vs1,vs1,vs0,vsX}
+    0x4222, // cube 31  <0100 0010 0010 0010> {vs1,vs1,vs1,vsX}
+}
+};
+
+static drow s_BitMasks[32] = 
+{
+    0x00000001,0x00000002,0x00000004,0x00000008,
+    0x00000010,0x00000020,0x00000040,0x00000080,
+    0x00000100,0x00000200,0x00000400,0x00000800,
+    0x00001000,0x00002000,0x00004000,0x00008000,
+    0x00010000,0x00020000,0x00040000,0x00080000,
+    0x00100000,0x00200000,0x00400000,0x00800000,
+    0x01000000,0x02000000,0x04000000,0x08000000,
+    0x10000000,0x20000000,0x40000000,0x80000000
+};
+
+////////////////////////////////////////////////////////////////////////
+///                        STATIC VARIABLES                          ///
+////////////////////////////////////////////////////////////////////////
+
+// this flag is TRUE as long as the storage is allocated
+static int fWorking;
+
+// set these flags to have minimum literal groups generated first
+static int fMinLitGroupsFirst[4] = { 0 /*dist2*/, 0 /*dist3*/, 0 /*dist4*/};
+
+static int nDist;
+static int nCubes;
+static int nCubesInGroup;
+static int nGroups;
+static Cube *pCA, *pCB;
+
+// storage for variable numbers that are different in the cubes
+static int DiffVars[5];
+static int* pDiffVars;
+static int nDifferentVars;
+
+// storage for the bits and words of different input variables
+static int nDiffVarsIn;
+static int DiffVarWords[5];
+static int DiffVarBits[5];
+
+// literal mask used to count the number of literals in the cubes
+static drow MaskLiterals;
+// the base for counting literals
+static int StartingLiterals;
+// the number of literals in each cube
+static int CubeLiterals[32];
+static int BitShift;
+static int DiffVarValues[4][3];
+static int Value;
+
+// the sorted array of groups in the increasing order of costs
+static int GroupCosts[32];
+static int GroupCostBest;
+static int GroupCostBestNum;
+
+static int CubeNum;
+static int NewZ;
+static drow Temp;
+
+// the cubes currently created
+static Cube* ELCubes[32];
+
+// the bit string with 1's corresponding to cubes in ELCubes[] 
+// that constitute the last group
+static drow LastGroup;
+
+static int  GroupOrder[24];
+static drow VisitedGroups;
+static int  nVisitedGroups;
+
+//int RemainderBits = (nVars*2)%(sizeof(drow)*8);
+//int TotalWords    = (nVars*2)/(sizeof(drow)*8) + (RemainderBits > 0);
+static drow DammyBitData[(MAXVARS*2)/(sizeof(drow)*8)+(MAXVARS*2)%(sizeof(drow)*8)];
+
+////////////////////////////////////////////////////////////////////////
+///                       FUNCTION DEFINTIONS                        ///
+////////////////////////////////////////////////////////////////////////
+
+// IDEA! if we already used a cube to count distances and it did not improve
+// there is no need to try it again with other group
+// (this idea works only for ExorLink-2 and -3)
+
+int ExorLinkCubeIteratorStart( Cube** pGroup, Cube* pC1, Cube* pC2, cubedist Dist )
+// this function starts the Exor-Link iterator, which iterates
+// through the cube groups starting from the group with min literals
+// returns 1 on success, returns 0 if the cubes have wrong distance
+{
+    int i, c;
+
+    // check that everything is okey
+    assert( pC1 != NULL );
+    assert( pC2 != NULL );
+    assert( !fWorking );
+
+    nDist = Dist;
+    nCubes = Dist + 2;
+    nCubesInGroup = s_ELnCubes[nDist];
+    nGroups = s_ELnGroups[Dist];
+    pCA = pC1;
+    pCB = pC2;
+    // find what variables are different in these two cubes
+    // FindDiffVars returns DiffVars[0] < 0, if the output is different
+    nDifferentVars = FindDiffVars( DiffVars, pCA, pCB );
+    if ( nCubes != nDifferentVars )
+    {
+//      cout << "ExorLinkCubeIterator(): Distance mismatch";
+//      cout << " nCubes = " << nCubes << " nDiffVars = " << nDifferentVars << endl;
+        fWorking = 0;
+        return 0;
+    }
+
+    // copy the input variable cube data into DammyBitData[]
+    for ( i = 0; i < g_CoverInfo.nWordsIn; i++ )
+        DammyBitData[i] = pCA->pCubeDataIn[i];
+
+    // find the number of different input variables
+    nDiffVarsIn = ( DiffVars[0] >= 0 )? nCubes: nCubes-1;
+    // assign the pointer to the place where the number of diff input vars is stored
+    pDiffVars   = ( DiffVars[0] >= 0 )? DiffVars: DiffVars+1;
+    // find the bit offsets and remove different variables
+    for ( i = 0; i < nDiffVarsIn; i++ )
+    {
+        DiffVarWords[i] = ((2*pDiffVars[i]) >> LOGBPI) ;
+        DiffVarBits[i]  = ((2*pDiffVars[i]) & BPIMASK);
+        // clear this position
+        DammyBitData[ DiffVarWords[i] ] &= ~( 3 << DiffVarBits[i] );
+    }
+
+    // extract the values from the cubes and create the mask of literals
+    MaskLiterals = 0;
+    // initialize the base for literal counts
+    StartingLiterals = pCA->a;
+    for ( i = 0, BitShift = 0; i < nDiffVarsIn; i++, BitShift++ )
+    {
+        DiffVarValues[i][0] = ( pCA->pCubeDataIn[DiffVarWords[i]] >> DiffVarBits[i] ) & 3;
+        if ( DiffVarValues[i][0] != VAR_ABS )
+        {
+            MaskLiterals |= ( 1 << BitShift );
+            // update the base for literal counts
+            StartingLiterals--;
+        }
+        BitShift++;
+
+        DiffVarValues[i][1] = ( pCB->pCubeDataIn[DiffVarWords[i]] >> DiffVarBits[i] ) & 3;
+        if ( DiffVarValues[i][1] != VAR_ABS )
+            MaskLiterals |= ( 1 << BitShift );
+        BitShift++;
+
+        DiffVarValues[i][2] = DiffVarValues[i][0] ^ DiffVarValues[i][1];
+        if ( DiffVarValues[i][2] != VAR_ABS )
+            MaskLiterals |= ( 1 << BitShift );
+        BitShift++;
+    }
+
+    // count the number of additional literals in each cube of the group
+    for ( i = 0; i < nCubesInGroup; i++ )
+        CubeLiterals[i] = BitCount[ MaskLiterals & s_CubeLitMasks[Dist][i] ];
+
+    // compute the costs of all groups
+    for ( i = 0; i < nGroups; i++ )
+        // go over all cubes in the group
+        for ( GroupCosts[i] = 0, c = 0; c < nCubes; c++ )
+            GroupCosts[i] += CubeLiterals[ s_ELGroupRules[Dist][i][c] ];
+
+    // find the best cost group
+    if ( fMinLitGroupsFirst[Dist] ) 
+    { // find the minimum cost group
+        GroupCostBest = LARGE_NUM;
+        for ( i = 0; i < nGroups; i++ )
+            if ( GroupCostBest > GroupCosts[i] )
+            {
+                GroupCostBest = GroupCosts[i];
+                GroupCostBestNum = i;
+            }
+    }
+    else 
+    { // find the maximum cost group
+        GroupCostBest = -1;
+        for ( i = 0; i < nGroups; i++ )
+            if ( GroupCostBest < GroupCosts[i] )
+            {
+                GroupCostBest = GroupCosts[i];
+                GroupCostBestNum = i;
+            }
+    }
+
+    // create the cubes with min number of literals needed for the group
+    LastGroup = 0;
+    for ( c = 0; c < nCubes; c++ )
+    {
+        CubeNum = s_ELGroupRules[Dist][GroupCostBestNum][c];
+        LastGroup |= s_BitMasks[CubeNum];
+
+        // bring a cube from the free cube list
+        ELCubes[CubeNum] = GetFreeCube();
+
+        // copy the input bit data into the cube 
+        for ( i = 0; i < g_CoverInfo.nWordsIn; i++ )
+            ELCubes[CubeNum]->pCubeDataIn[i] = DammyBitData[i];
+
+        // copy the output bit data into the cube
+        NewZ = 0;
+        if ( DiffVars[0] >= 0 ) // the output is not involved in ExorLink
+        {
+            for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+                ELCubes[CubeNum]->pCubeDataOut[i] = pCA->pCubeDataOut[i];
+            NewZ = pCA->z;
+        }
+        else // the output is involved
+        { // determine where the output information comes from
+            Value = s_ELCubeRules[Dist][CubeNum][nDiffVarsIn];
+            if ( Value == vs0 )
+                for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+                {
+                    Temp = pCA->pCubeDataOut[i];
+                    ELCubes[CubeNum]->pCubeDataOut[i] = Temp;
+                    NewZ += BIT_COUNT(Temp);
+                }
+            else if ( Value == vs1 )
+                for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+                {
+                    Temp = pCB->pCubeDataOut[i];
+                    ELCubes[CubeNum]->pCubeDataOut[i] = Temp;
+                    NewZ += BIT_COUNT(Temp);
+                }
+            else if ( Value == vsX )
+                for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+                {
+                    Temp = pCA->pCubeDataOut[i] ^ pCB->pCubeDataOut[i];
+                    ELCubes[CubeNum]->pCubeDataOut[i] = Temp;
+                    NewZ += BIT_COUNT(Temp);
+                }
+        }
+        // set the number of literals
+        ELCubes[CubeNum]->a = StartingLiterals + CubeLiterals[CubeNum];
+        ELCubes[CubeNum]->z = NewZ;
+
+        // set the variables that should be there
+        for ( i = 0; i < nDiffVarsIn; i++ )
+        {
+            Value = DiffVarValues[i][ s_ELCubeRules[Dist][CubeNum][i] ];
+            ELCubes[CubeNum]->pCubeDataIn[ DiffVarWords[i] ] |= ( Value << DiffVarBits[i] );
+        }
+
+        // assign the ID
+        ELCubes[CubeNum]->ID = g_CoverInfo.cIDs++;
+        // skip through zero-ID
+        if ( g_CoverInfo.cIDs == 256 )
+            g_CoverInfo.cIDs = 1;
+
+        // prepare the return array
+        pGroup[c] = ELCubes[CubeNum];
+    }
+
+    // mark this group as visited 
+    VisitedGroups |= s_BitMasks[ GroupCostBestNum ];
+    // set the first visited group number
+    GroupOrder[0] = GroupCostBestNum;
+    // increment the counter of visited groups
+    nVisitedGroups = 1;
+    fWorking = 1;
+    return 1;
+}
+
+int ExorLinkCubeIteratorNext( Cube** pGroup )
+// give the next group in the decreasing order of sum of literals
+// returns 1 on success, returns 0 if there are no more groups
+{
+    int i, c;
+
+    // check that everything is okey
+    assert( fWorking );
+
+    if ( nVisitedGroups == nGroups ) 
+    // we have iterated through all groups
+        return 0;
+
+    // find the min/max cost group
+    if ( fMinLitGroupsFirst[nDist] ) 
+//  if ( nCubes == 4 ) 
+    { // find the minimum cost
+        // go through all groups
+        GroupCostBest = LARGE_NUM;
+        for ( i = 0; i < nGroups; i++ )
+            if ( !(VisitedGroups & s_BitMasks[i]) && GroupCostBest > GroupCosts[i] )
+            {
+                GroupCostBest = GroupCosts[i];
+                GroupCostBestNum = i;
+            }
+        assert( GroupCostBest != LARGE_NUM );
+    }
+    else 
+    { // find the maximum cost
+        // go through all groups
+        GroupCostBest = -1;
+        for ( i = 0; i < nGroups; i++ )
+            if ( !(VisitedGroups & s_BitMasks[i]) && GroupCostBest < GroupCosts[i] )
+            {
+                GroupCostBest = GroupCosts[i];
+                GroupCostBestNum = i;
+            }
+        assert( GroupCostBest != -1 );
+    }
+
+    // create the cubes needed for the group, if they are not created already
+    LastGroup = 0;
+    for ( c = 0; c < nCubes; c++ )
+    {
+        CubeNum = s_ELGroupRules[nDist][GroupCostBestNum][c];
+        LastGroup |= s_BitMasks[CubeNum];
+
+        if ( ELCubes[CubeNum] == NULL ) // this cube does not exist
+        {
+            // bring a cube from the free cube list
+            ELCubes[CubeNum] = GetFreeCube();
+
+            // copy the input bit data into the cube 
+            for ( i = 0; i < g_CoverInfo.nWordsIn; i++ )
+                ELCubes[CubeNum]->pCubeDataIn[i] = DammyBitData[i];
+
+            // copy the output bit data into the cube
+            NewZ = 0;
+            if ( DiffVars[0] >= 0 ) // the output is not involved in ExorLink
+            {
+                for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+                    ELCubes[CubeNum]->pCubeDataOut[i] = pCA->pCubeDataOut[i];
+                NewZ = pCA->z;
+            }
+            else // the output is involved
+            { // determine where the output information comes from
+                Value = s_ELCubeRules[nDist][CubeNum][nDiffVarsIn];
+                if ( Value == vs0 )
+                    for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+                    {
+                        Temp = pCA->pCubeDataOut[i];
+                        ELCubes[CubeNum]->pCubeDataOut[i] = Temp;
+                        NewZ += BIT_COUNT(Temp);
+                    }
+                else if ( Value == vs1 )
+                    for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+                    {
+                        Temp = pCB->pCubeDataOut[i];
+                        ELCubes[CubeNum]->pCubeDataOut[i] = Temp;
+                        NewZ += BIT_COUNT(Temp);
+                    }
+                else if ( Value == vsX )
+                    for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+                    {
+                        Temp = pCA->pCubeDataOut[i] ^ pCB->pCubeDataOut[i];
+                        ELCubes[CubeNum]->pCubeDataOut[i] = Temp;
+                        NewZ += BIT_COUNT(Temp);
+                    }
+            }
+            // set the number of literals and output ones
+            ELCubes[CubeNum]->a = StartingLiterals + CubeLiterals[CubeNum];
+            ELCubes[CubeNum]->z = NewZ;
+
+            assert( NewZ != 255 );
+
+            // set the variables that should be there
+            for ( i = 0; i < nDiffVarsIn; i++ )
+            {
+                Value = DiffVarValues[i][ s_ELCubeRules[nDist][CubeNum][i] ];
+                ELCubes[CubeNum]->pCubeDataIn[ DiffVarWords[i] ] |= ( Value << DiffVarBits[i] );
+            }
+
+            // assign the ID
+            ELCubes[CubeNum]->ID = g_CoverInfo.cIDs++;
+            // skip through zero-ID
+            if ( g_CoverInfo.cIDs == 256 )
+                g_CoverInfo.cIDs = 1;
+
+        }
+        // prepare the return array
+        pGroup[c] = ELCubes[CubeNum];
+    }
+
+    // mark this group as visited 
+    VisitedGroups |= s_BitMasks[ GroupCostBestNum ];
+    // set the next visited group number and
+    // increment the counter of visited groups
+    GroupOrder[ nVisitedGroups++ ] = GroupCostBestNum;
+    return 1;
+}
+
+int ExorLinkCubeIteratorPick( Cube** pGroup, int g )
+// gives the group #g in the order in which the groups were given
+// during iteration
+// returns 1 on success, returns 0 if something is wrong (g is too large)
+{
+    int GroupNum, c;
+
+    assert( fWorking );
+    assert( g >= 0 && g < nGroups );
+    assert( VisitedGroups & s_BitMasks[g] );
+
+    GroupNum = GroupOrder[g];
+    // form the group
+    LastGroup = 0;
+    for ( c = 0; c < nCubes; c++ )
+    {
+        CubeNum = s_ELGroupRules[nDist][GroupNum][c];
+
+        // remember this group as the last one
+        LastGroup |= s_BitMasks[CubeNum];
+
+        assert( ELCubes[CubeNum] != NULL ); // this cube should exist
+        // prepare the return array
+        pGroup[c] = ELCubes[CubeNum];
+    }
+    return 1;
+}
+
+void ExorLinkCubeIteratorCleanUp( int fTakeLastGroup )
+// removes the cubes from the store back into the list of free cubes
+// if fTakeLastGroup is 0, removes all cubes
+// if fTakeLastGroup is 1, does not store the last group
+{
+    int c;
+    assert( fWorking );
+
+    // put cubes back
+    // set the cube pointers to zero
+    if ( fTakeLastGroup == 0 )
+        for ( c = 0; c < nCubesInGroup; c++ )
+        {
+            ELCubes[c]->fMark = 0;
+            AddToFreeCubes( ELCubes[c] );
+            ELCubes[c] = NULL;
+        }
+    else
+        for ( c = 0; c < nCubesInGroup; c++ )
+        if ( ELCubes[c] )
+        {
+            ELCubes[c]->fMark = 0;
+            if ( (LastGroup & s_BitMasks[c]) == 0 ) // does not belong to the last group
+                AddToFreeCubes( ELCubes[c] );
+            ELCubes[c] = NULL;
+        }
+
+    // set the cube groups to zero
+    VisitedGroups = 0;
+    // shut down the iterator
+    fWorking = 0;
+}
+
+    
+///////////////////////////////////////////////////////////////////
+////////////              End of File             /////////////////
+///////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/base/exor/exorList.c b/src/base/exor/exorList.c
new file mode 100644
index 00000000..6388fbe3
--- /dev/null
+++ b/src/base/exor/exorList.c
@@ -0,0 +1,1140 @@
+/**CFile****************************************************************
+
+  FileName    [exorList.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Exclusive sum-of-product minimization.]
+
+  Synopsis    [Cube lists.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: exorList.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///                  Implementation of EXORCISM - 4                  ///
+///              An Exclusive Sum-of-Product Minimizer               ///
+///                                                                  ///
+///               Alan Mishchenko  <alanmi@ee.pdx.edu>               ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///                 Iterative Cube Set Minimization                  ///
+///                  Iterative ExorLink Procedure                    ///
+///                  Support of Cube Pair Queques                    ///
+///                                                                  ///
+///  Ver. 1.0. Started - July 18, 2000. Last update - July 20, 2000  ///
+///  Ver. 1.1. Started - July 24, 2000. Last update - July 29, 2000  ///
+///  Ver. 1.2. Started - July 30, 2000. Last update - July 31, 2000  ///
+///  Ver. 1.4. Started -  Aug 10, 2000. Last update -  Aug 26, 2000  ///
+///  Ver. 1.5. Started -  Aug 30, 2000. Last update -  Aug 30, 2000  ///
+///  Ver. 1.6. Started -  Sep 11, 2000. Last update -  Sep 15, 2000  ///
+///  Ver. 1.7. Started -  Sep 20, 2000. Last update -  Sep 23, 2000  ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///   This software was tested with the BDD package "CUDD", v.2.3.0  ///
+///                          by Fabio Somenzi                        ///
+///                  http://vlsi.colorado.edu/~fabio/                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "exor.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                       EXTERNAL VARIABLES                         ///
+////////////////////////////////////////////////////////////////////////
+
+// information about options and the cover
+extern cinfo g_CoverInfo;
+
+// the look-up table for the number of 1's in unsigned short
+extern unsigned char BitCount[];
+
+////////////////////////////////////////////////////////////////////////
+///                       EXTERNAL FUNCTIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+extern int GetDistance( Cube* pC1, Cube* pC2 );
+// distance computation for two cubes
+extern int GetDistancePlus( Cube* pC1, Cube* pC2 );
+
+extern void ExorVar( Cube* pC, int Var, varvalue Val );
+
+extern void AddToFreeCubes( Cube* pC );
+// returns a simplified cube back into the free list
+
+//extern void PrintCube( ostream& DebugStream, Cube* pC );
+// debug output for cubes
+
+extern Cube* GetFreeCube();
+
+////////////////////////////////////////////////////////////////////////
+/// ExorLink Functions
+extern int ExorLinkCubeIteratorStart( Cube** pGroup, Cube* pC1, Cube* pC2, cubedist Dist );
+// this function starts the Exor-Link IteratorCubePair, which iterates
+// through the cube groups starting from the group with min literals
+// returns 1 on success, returns 0 if the cubes have wrong distance
+
+extern int ExorLinkCubeIteratorNext( Cube** pGroup );
+// give the next group in the decreasing order of sum of literals
+// returns 1 on success, returns 0 if there are no more groups
+
+extern int ExorLinkCubeIteratorPick( Cube** pGroup, int g );
+// gives the group #g in the order in which the groups were given
+// during iteration
+// returns 1 on success, returns 0 if something g is too large
+
+extern void ExorLinkCubeIteratorCleanUp( int fTakeLastGroup );
+// removes the cubes from the store back into the list of free cubes
+// if fTakeLastGroup is 0, removes all cubes
+// if fTakeLastGroup is 1, does not store the last group
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTIONS OF THIS MODULE                      ///
+////////////////////////////////////////////////////////////////////////
+
+// iterative ExorLink
+int IterativelyApplyExorLink2( char fDistEnable );   
+int IterativelyApplyExorLink3( char fDistEnable );   
+int IterativelyApplyExorLink4( char fDistEnable );   
+
+// function which performs distance computation and simplifes on the fly
+// it is also called from the Pseudo-Kronecker module when cubes are added
+int CheckForCloseCubes( Cube* p, int fAddCube );
+int CheckAndInsert( Cube* p );
+
+// this function changes the cube back after it was DIST-1 transformed
+void UndoRecentChanges();
+
+////////////////////////////////////////////////////////////////////////
+// iterating through adjucency pair queques (with authomatic garbage collection)
+
+// start an iterator through cubes of dist CubeDist,
+// the resulting pointers are written into ppC1 and ppC2
+int IteratorCubePairStart( cubedist Dist, Cube** ppC1, Cube** ppC2 );
+// gives the next VALID cube pair (the previous one is automatically dequequed)
+int IteratorCubePairNext();
+
+////////////////////////////////////////////////////////////////////////
+// the cube storage
+
+// cube storage allocation/delocation
+int AllocateCubeSets( int nVarsIn, int nVarsOut );
+void DelocateCubeSets();
+
+// insert/extract a cube into/from the storage
+void CubeInsert( Cube* p );
+Cube* CubeExtract( Cube* p );
+
+////////////////////////////////////////////////////////////////////////
+// Cube Set Iterator
+Cube* IterCubeSetStart();
+// starts an iterator that traverses all the cubes in the ring
+Cube* IterCubeSetNext();
+// returns the next cube in the ring
+// to use it again after it has returned NULL, call IterCubeSetStart() first
+
+////////////////////////////////////////////////////////////////////////
+// cube adjacency queques
+
+// adjacency queque allocation/delocation procedures
+int AllocateQueques( int nPlaces );
+void DelocateQueques();
+
+// conditional adding cube pairs to queques
+// reset temporarily stored new range of cube pairs
+static void NewRangeReset();
+// add temporarily stored new range of cube pairs to the queque
+static void NewRangeAdd();
+// insert one cube pair into the new range
+static void NewRangeInsertCubePair( cubedist Dist, Cube* p1, Cube* p2 );
+
+static void MarkSet();
+static void MarkRewind();
+
+void PrintQuequeStats();
+int GetQuequeStats( cubedist Dist );
+
+// iterating through the queque (with authomatic garbage collection)
+// start an iterator through cubes of dist CubeDist,
+// the resulting pointers are written into ppC1 and ppC2
+int IteratorCubePairStart( cubedist Dist, Cube** ppC1, Cube** ppC2 );
+// gives the next VALID cube pair (the previous one is automatically dequequed)
+int IteratorCubePairNext();
+
+////////////////////////////////////////////////////////////////////////
+///                      EXPORTED VARIABLES                          ///
+////////////////////////////////////////////////////////////////////////`
+
+// the number of allocated places
+int s_nPosAlloc;
+// the maximum number of occupied places
+int s_nPosMax[3];
+
+////////////////////////////////////////////////////////////////////////
+///                      Minimization Strategy                       ///
+////////////////////////////////////////////////////////////////////////
+
+// 1) check that ExorLink for this cube pair can be performed
+//    (it may happen that the group is outdated due to recent reshaping)
+// 2) find out what is the improvement achieved by each cube group
+// 3) depending on the distance, do the following:
+//    a) if ( Dist == 2 ) 
+//           try both cube groups, 
+//           if one of them leads to improvement, take the cube group right away
+//           if none of them leads to improment
+//              - take the last one (because it reshapes)
+//              - take the last one only in case it does not increase literals
+//    b) if ( Dist == 3 )
+//           try groups one by one
+//           if one of them leads to improvement, take the group right away
+//           if none of them leads to improvement
+//              - take the group which reshapes
+//              - take the reshaping group only in case it does not increase literals
+//           if none of them leads to reshaping, do not take any of them
+//    c) if ( Dist == 4 )
+//           try groups one by one
+//           if one of the leads to reshaping, take it right away
+//           if none of them leads to reshaping, do not take any of them
+
+////////////////////////////////////////////////////////////////////////
+///                       STATIC VARIABLES                           ///
+////////////////////////////////////////////////////////////////////////
+
+// Cube set is a list of cubes
+static Cube* s_List;
+
+///////////////////////////////////////////////////////////////////////////
+// undo information
+///////////////////////////////////////////////////////////////////////////
+static struct
+{
+    int fInput;   // 1 if the input was changed
+    Cube* p;      // the pointer to the modified cube
+    int PrevQa;
+    int PrevPa;
+    int PrevPz;
+    int Var;      // the number of variable that was changed
+    int Value;    // the value what was there
+    int PrevID;   // the previous ID of the removed cube
+} s_ChangeStore;
+///////////////////////////////////////////////////////////////////////////
+
+// enable pair accumulation
+// from the begginning (while the starting cover is generated)
+// only the distance 2 accumulation is enabled
+static int s_fDistEnable2 = 1;
+static int s_fDistEnable3;
+static int s_fDistEnable4;
+
+// temporary storage for cubes generated by the ExorLink iterator
+static Cube* s_CubeGroup[5];
+// the marks telling whether the given cube is inserted
+static int s_fInserted[5];
+
+// enable selection only those Dist2 and Dist3 that do not increase literals
+int s_fDecreaseLiterals = 0;
+
+// the counters for display
+static int s_cEnquequed;
+static int s_cAttempts;
+static int s_cReshapes;
+
+// the number of cubes before ExorLink starts
+static int s_nCubesBefore;
+// the distance code specific for each ExorLink
+static cubedist s_Dist;
+
+// other variables
+static int s_Gain;
+static int s_GainTotal;
+static int s_GroupCounter;
+static int s_GroupBest;
+static Cube *s_pC1, *s_pC2;
+
+////////////////////////////////////////////////////////////////////////
+///                  Iterative ExorLink Operation                    ///
+////////////////////////////////////////////////////////////////////////
+
+int CheckAndInsert( Cube* p )
+{
+//  return CheckForCloseCubes( p, 1 );
+    CubeInsert( p );
+    return 0;
+}
+
+int IterativelyApplyExorLink2( char fDistEnable )   
+// MEMO: instead of inserting the cubes that have already been checked
+// by running CheckForCloseCubes again, try inserting them without checking
+// and observe the difference (it will save 50% of checking time)
+{
+    int z;
+
+    // this var is specific to ExorLink-2
+    s_Dist = (cubedist)0;
+
+    // enable pair accumulation
+    s_fDistEnable2 = fDistEnable & 1;
+    s_fDistEnable3 = fDistEnable & 2;
+    s_fDistEnable4 = fDistEnable & 4;
+
+    // initialize counters
+    s_cEnquequed = GetQuequeStats( s_Dist );
+    s_cAttempts  = 0;
+    s_cReshapes  = 0;
+
+    // remember the number of cubes before minimization
+    s_nCubesBefore = g_CoverInfo.nCubesInUse;
+
+    for ( z = IteratorCubePairStart( s_Dist, &s_pC1, &s_pC2 ); z; z = IteratorCubePairNext() )
+    {
+        s_cAttempts++;
+        // start ExorLink of the given Distance
+        if ( ExorLinkCubeIteratorStart( s_CubeGroup, s_pC1, s_pC2, s_Dist ) )
+        {
+            // extract old cubes from storage (to prevent EXORing with their derivitives)
+            CubeExtract( s_pC1 );
+            CubeExtract( s_pC2 );
+
+            // mark the current position in the cube pair queques
+            MarkSet();
+
+            // check the first group (generated by ExorLinkCubeIteratorStart())
+            if ( CheckForCloseCubes( s_CubeGroup[0], 0 ) ) 
+            {  // the first cube leads to improvement - it is already inserted
+                CheckForCloseCubes( s_CubeGroup[1], 1 ); // insert the second cube
+                goto SUCCESS;
+            }
+            if ( CheckForCloseCubes( s_CubeGroup[1], 0 ) ) 
+            {  // the second cube leads to improvement - it is already inserted
+                CheckForCloseCubes( s_CubeGroup[0], 1 ); // insert the first cube
+//              CheckAndInsert( s_CubeGroup[0] );
+                goto SUCCESS;
+            }
+            // the first group does not lead to improvement
+
+            // rewind to the previously marked position in the cube pair queques
+            MarkRewind();
+
+            // generate the second group
+            ExorLinkCubeIteratorNext( s_CubeGroup );
+
+            // check the second group
+            if ( CheckForCloseCubes( s_CubeGroup[0], 0 ) ) 
+            { // the first cube leads to improvement - it is already inserted
+                CheckForCloseCubes( s_CubeGroup[1], 1 ); // insert the second cube
+                goto SUCCESS;
+            }
+            if ( CheckForCloseCubes( s_CubeGroup[1], 0 ) ) 
+            { // the second cube leads to improvement - it is already inserted
+                CheckForCloseCubes( s_CubeGroup[0], 1 ); // insert the first cube
+//              CheckAndInsert( s_CubeGroup[0] );
+                goto SUCCESS;
+            }
+            // the second group does not lead to improvement
+
+            // decide whether to accept the second group, depending on literals
+            if ( s_fDecreaseLiterals )
+            {
+                if ( s_CubeGroup[0]->a + s_CubeGroup[1]->a >= s_pC1->a + s_pC2->a ) 
+                // the group increases literals
+                { // do not take the last group
+                            
+                    // rewind to the previously marked position in the cube pair queques
+                    MarkRewind();
+
+                    // return the old cubes back to storage
+                    CubeInsert( s_pC1 );
+                    CubeInsert( s_pC2 );
+                    // clean the results of generating ExorLinked cubes
+                    ExorLinkCubeIteratorCleanUp( 0 );
+                    continue;
+                }
+            }
+
+            // take the last group
+            // there is no need to test these cubes again,
+            // because they have been tested and did not yield any improvement
+            CubeInsert( s_CubeGroup[0] );
+            CubeInsert( s_CubeGroup[1] );
+//          CheckForCloseCubes( s_CubeGroup[0], 1 ); 
+//          CheckForCloseCubes( s_CubeGroup[1], 1 ); 
+
+SUCCESS:
+            // clean the results of generating ExorLinked cubes
+            ExorLinkCubeIteratorCleanUp( 1 ); // take the last group
+            // free old cubes
+            AddToFreeCubes( s_pC1 );
+            AddToFreeCubes( s_pC2 );
+            // increate the counter
+            s_cReshapes++;
+        }
+    }
+    // print the report
+    if ( g_CoverInfo.Verbosity == 2 )
+    {
+    printf( "ExLink-%d", 2 );
+    printf( ": Que= %5d", s_cEnquequed );
+    printf( "  Att= %4d", s_cAttempts );
+    printf( "  Resh= %4d", s_cReshapes );
+    printf( "  NoResh= %4d", s_cAttempts - s_cReshapes );
+    printf( "  Cubes= %3d", g_CoverInfo.nCubesInUse );
+    printf( "  (%d)", s_nCubesBefore - g_CoverInfo.nCubesInUse );
+    printf( "\n" );
+    }
+
+    // return the number of cubes gained in the process
+    return s_nCubesBefore - g_CoverInfo.nCubesInUse;
+}
+
+int IterativelyApplyExorLink3( char fDistEnable )   
+{
+    int z, c, d;
+    // this var is specific to ExorLink-3
+    s_Dist = (cubedist)1;
+
+    // enable pair accumulation
+    s_fDistEnable2 = fDistEnable & 1;
+    s_fDistEnable3 = fDistEnable & 2;
+    s_fDistEnable4 = fDistEnable & 4;
+
+    // initialize counters
+    s_cEnquequed = GetQuequeStats( s_Dist );
+    s_cAttempts  = 0;
+    s_cReshapes  = 0;
+
+    // remember the number of cubes before minimization
+    s_nCubesBefore = g_CoverInfo.nCubesInUse;
+
+    for ( z = IteratorCubePairStart( s_Dist, &s_pC1, &s_pC2 ); z; z = IteratorCubePairNext() )
+    {
+        s_cAttempts++;
+        // start ExorLink of the given Distance
+        if ( ExorLinkCubeIteratorStart( s_CubeGroup, s_pC1, s_pC2, s_Dist ) )
+        {
+            // extract old cubes from storage (to prevent EXORing with their derivitives)
+            CubeExtract( s_pC1 );
+            CubeExtract( s_pC2 );
+
+            // mark the current position in the cube pair queques
+            MarkSet();
+
+            // check cube groups one by one
+            s_GroupCounter = 0;
+            do  
+            {   // check the cubes of this group one by one
+                for ( c = 0; c < 3; c++ )
+                if ( !s_CubeGroup[c]->fMark ) // this cube has not yet been checked
+                {
+                    s_Gain = CheckForCloseCubes( s_CubeGroup[c], 0 ); // do not insert the cube, by default
+                    if ( s_Gain ) 
+                    { // this cube leads to improvement or reshaping - it is already inserted
+
+                        // decide whether to accept this group based on literal count
+                        if ( s_fDecreaseLiterals && s_Gain == 1 )
+                        if ( s_CubeGroup[0]->a + s_CubeGroup[1]->a + s_CubeGroup[2]->a >
+                             s_pC1->a + s_pC2->a + s_ChangeStore.PrevQa ) // the group increases literals
+                        { // do not take this group
+                            // remember the group
+                            s_GroupBest = s_GroupCounter;
+                            // undo changes to be able to continue checking other groups
+                            UndoRecentChanges();
+                            break;
+                        }
+
+                        // take this group
+                        for ( d = 0; d < 3; d++ ) // insert other cubes
+                            if ( d != c )
+                            {
+                                CheckForCloseCubes( s_CubeGroup[d], 1 ); 
+//                              if ( s_CubeGroup[d]->fMark )
+//                                  CheckAndInsert( s_CubeGroup[d] );
+//                                  CheckOnlyOneCube( s_CubeGroup[d] );
+//                                  CheckForCloseCubes( s_CubeGroup[d], 1 ); 
+//                              else
+//                                  CheckForCloseCubes( s_CubeGroup[d], 1 ); 
+                            }
+
+                        // clean the results of generating ExorLinked cubes
+                        ExorLinkCubeIteratorCleanUp( 1 ); // take the last group
+                        // free old cubes
+                        AddToFreeCubes( s_pC1 );
+                        AddToFreeCubes( s_pC2 );
+                        // update the counter
+                        s_cReshapes++;
+                        goto END_OF_LOOP;
+                    }
+                    else // mark the cube as checked
+                        s_CubeGroup[c]->fMark = 1;
+                }
+                // the group is not taken - find the new group
+                s_GroupCounter++;
+                                        
+                // rewind to the previously marked position in the cube pair queques
+                MarkRewind();
+            } 
+            while ( ExorLinkCubeIteratorNext( s_CubeGroup ) );
+            // none of the groups leads to improvement
+
+            // return the old cubes back to storage
+            CubeInsert( s_pC1 );
+            CubeInsert( s_pC2 );
+            // clean the results of generating ExorLinked cubes
+            ExorLinkCubeIteratorCleanUp( 0 );
+        }
+END_OF_LOOP: {}
+    }
+
+    // print the report
+    if ( g_CoverInfo.Verbosity == 2 )
+    {
+    printf( "ExLink-%d", 3 );
+    printf( ": Que= %5d", s_cEnquequed );
+    printf( "  Att= %4d", s_cAttempts );
+    printf( "  Resh= %4d", s_cReshapes );
+    printf( "  NoResh= %4d", s_cAttempts - s_cReshapes );
+    printf( "  Cubes= %3d", g_CoverInfo.nCubesInUse );
+    printf( "  (%d)", s_nCubesBefore - g_CoverInfo.nCubesInUse );
+    printf( "\n" );
+    }
+
+    // return the number of cubes gained in the process
+    return s_nCubesBefore - g_CoverInfo.nCubesInUse;
+}
+
+int IterativelyApplyExorLink4( char fDistEnable )   
+{
+    int z, c;
+    // this var is specific to ExorLink-4
+    s_Dist = (cubedist)2;
+
+    // enable pair accumulation
+    s_fDistEnable2 = fDistEnable & 1;
+    s_fDistEnable3 = fDistEnable & 2;
+    s_fDistEnable4 = fDistEnable & 4;
+
+    // initialize counters
+    s_cEnquequed = GetQuequeStats( s_Dist );
+    s_cAttempts  = 0;
+    s_cReshapes  = 0;
+
+    // remember the number of cubes before minimization
+    s_nCubesBefore = g_CoverInfo.nCubesInUse;
+
+    for ( z = IteratorCubePairStart( s_Dist, &s_pC1, &s_pC2 ); z; z = IteratorCubePairNext() )
+    {
+        s_cAttempts++;
+        // start ExorLink of the given Distance
+        if ( ExorLinkCubeIteratorStart( s_CubeGroup, s_pC1, s_pC2, s_Dist ) )
+        {
+            // extract old cubes from storage (to prevent EXORing with their derivitives)
+            CubeExtract( s_pC1 );
+            CubeExtract( s_pC2 );
+
+            // mark the current position in the cube pair queques
+            MarkSet();
+
+            // check cube groups one by one
+            do  
+            {   // check the cubes of this group one by one
+                s_GainTotal = 0;
+                for ( c = 0; c < 4; c++ )
+                if ( !s_CubeGroup[c]->fMark ) // this cube has not yet been checked
+                {
+                    s_Gain = CheckForCloseCubes( s_CubeGroup[c], 0 ); // do not insert the cube, by default
+                    // if the cube leads to gain, it is already inserted
+                    s_fInserted[c] = (int)(s_Gain>0);
+                    // increment the total gain
+                    s_GainTotal += s_Gain;
+                }
+                else
+                    s_fInserted[c] = 0; // the cube has already been checked - it is not inserted
+
+                if ( s_GainTotal == 0 ) // the group does not lead to any gain
+                { // mark the cubes
+                    for ( c = 0; c < 4; c++ )
+                        s_CubeGroup[c]->fMark = 1;
+                }
+                else if ( s_GainTotal == 1 ) // the group does not lead to substantial gain, too
+                { 
+                    // undo changes to be able to continue checking groups
+                    UndoRecentChanges();
+                    // mark those cubes that were not inserted
+                    for ( c = 0; c < 4; c++ )
+                        s_CubeGroup[c]->fMark = !s_fInserted[c];
+                }
+                else // if ( s_GainTotal > 1 ) // the group reshapes or improves
+                { // accept the group
+                    for ( c = 0; c < 4; c++ ) // insert other cubes
+                        if ( !s_fInserted[c] )
+                            CheckForCloseCubes( s_CubeGroup[c], 1 ); 
+//                          CheckAndInsert( s_CubeGroup[c] );
+                    // clean the results of generating ExorLinked cubes
+                    ExorLinkCubeIteratorCleanUp( 1 ); // take the last group
+                    // free old cubes
+                    AddToFreeCubes( s_pC1 );
+                    AddToFreeCubes( s_pC2 );
+                    // update the counter
+                    s_cReshapes++;
+                    goto END_OF_LOOP;
+                }
+                                        
+                // rewind to the previously marked position in the cube pair queques
+                MarkRewind();
+            } 
+            while ( ExorLinkCubeIteratorNext( s_CubeGroup ) );
+            // none of the groups leads to improvement
+
+            // return the old cubes back to storage
+            CubeInsert( s_pC1 );
+            CubeInsert( s_pC2 );
+            // clean the results of generating ExorLinked cubes
+            ExorLinkCubeIteratorCleanUp( 0 );
+        }
+END_OF_LOOP: {}
+    }
+
+    // print the report
+    if ( g_CoverInfo.Verbosity == 2 )
+    {
+    printf( "ExLink-%d", 4 );
+    printf( ": Que= %5d", s_cEnquequed );
+    printf( "  Att= %4d", s_cAttempts );
+    printf( "  Resh= %4d", s_cReshapes );
+    printf( "  NoResh= %4d", s_cAttempts - s_cReshapes );
+    printf( "  Cubes= %3d", g_CoverInfo.nCubesInUse );
+    printf( "  (%d)", s_nCubesBefore - g_CoverInfo.nCubesInUse );
+    printf( "\n" );
+    }
+
+    // return the number of cubes gained in the process
+    return s_nCubesBefore - g_CoverInfo.nCubesInUse;
+}
+
+// local static variables
+Cube* s_q;
+int s_Distance;
+int s_DiffVarNum;
+int s_DiffVarValueP_old;
+int s_DiffVarValueP_new;
+int s_DiffVarValueQ;
+
+int CheckForCloseCubes( Cube* p, int fAddCube )
+// checks the cube storage for a cube that is dist-0 and dist-1 removed 
+// from the given one (p) if such a cube is found, extracts it from the data 
+// structure, EXORs it with the given cube, adds the resultant cube
+// to the data structure and performed the same check for the resultant cube;
+// returns the number of cubes gained in the process of reduction;
+// if an adjacent cube is not found, inserts the cube only if (fAddCube==1)!!!
+{
+    // start the new range
+    NewRangeReset();
+
+    for ( s_q = s_List; s_q; s_q = s_q->Next )
+    {
+        s_Distance = GetDistancePlus( p, s_q );
+        if ( s_Distance > 4 )
+        {
+        }
+        else if ( s_Distance == 4 )
+        {
+            if ( s_fDistEnable4 ) 
+                NewRangeInsertCubePair( DIST4, p, s_q );
+        }
+        else if ( s_Distance == 3 )
+        {
+            if ( s_fDistEnable3 ) 
+                NewRangeInsertCubePair( DIST3, p, s_q );
+        }
+        else if ( s_Distance == 2 )
+        { 
+            if ( s_fDistEnable2 ) 
+                NewRangeInsertCubePair( DIST2, p, s_q );
+        }
+        else if ( s_Distance == 1 )
+        {   // extract the cube from the data structure
+
+            //////////////////////////////////////////////////////////
+            // store the changes
+            s_ChangeStore.fInput = (s_DiffVarNum != -1);
+            s_ChangeStore.p      = p;
+            s_ChangeStore.PrevQa = s_q->a;
+            s_ChangeStore.PrevPa = p->a;
+            s_ChangeStore.PrevPz = p->z;
+            s_ChangeStore.Var    = s_DiffVarNum;
+            s_ChangeStore.Value  = s_DiffVarValueQ;
+            s_ChangeStore.PrevID = s_q->ID;
+            //////////////////////////////////////////////////////////
+
+            CubeExtract( s_q );
+            // perform the EXOR of the two cubes and write the result into p
+
+            // it is important that the resultant cube is written into p!!!
+
+            if ( s_DiffVarNum == -1 )
+            {
+                int i;
+                // exor the output part
+                p->z = 0;
+                for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+                {
+                    p->pCubeDataOut[i] ^= s_q->pCubeDataOut[i];
+                    p->z += BIT_COUNT(p->pCubeDataOut[i]);
+                }
+            }
+            else
+            {
+                // the cube has already been updated by GetDistancePlus()
+
+                // modify the parameters of the number of literals in the new cube
+//              p->a += s_UpdateLiterals[ s_DiffVarValueP ][ s_DiffVarValueQ ];
+                if ( s_DiffVarValueP_old == VAR_NEG || s_DiffVarValueP_old == VAR_POS )
+                    p->a--;
+                if ( s_DiffVarValueP_new == VAR_NEG || s_DiffVarValueP_new == VAR_POS )
+                    p->a++;
+            }
+
+            // move q to the free cube list
+            AddToFreeCubes( s_q );
+
+            // make sure that nobody with use the pairs created so far
+//          NewRangeReset();
+            // call the function again for the new cube
+            return 1 + CheckForCloseCubes( p, 1 );
+        }
+        else // if ( Distance == 0 )
+        {   // extract the second cube from the data structure and add them both to the free list
+            AddToFreeCubes( p );
+            AddToFreeCubes( CubeExtract( s_q ) );
+
+            // make sure that nobody with use the pairs created so far
+            NewRangeReset();
+            return 2;
+        }
+    }
+    
+    // add the cube to the data structure if needed
+    if ( fAddCube )
+        CubeInsert( p );
+
+    // add temporarily stored new range of cube pairs to the queque
+    NewRangeAdd();
+
+    return 0;
+}
+
+void UndoRecentChanges()
+{
+    Cube * p, * q;
+    // get back cube q that was deleted
+    q = GetFreeCube();
+    // restore the ID
+    q->ID = s_ChangeStore.PrevID;
+    // insert the cube into storage again
+    CubeInsert( q );
+
+    // extract cube p
+    p = CubeExtract( s_ChangeStore.p );
+
+    // modify it back
+    if ( s_ChangeStore.fInput ) // the input has changed
+    {
+        ExorVar( p, s_ChangeStore.Var, (varvalue)s_ChangeStore.Value );
+        p->a = s_ChangeStore.PrevPa;
+        // p->z did not change
+    }
+    else // if ( s_ChangeStore.fInput ) // the output has changed
+    {
+        int i;
+        for ( i = 0; i < g_CoverInfo.nWordsOut; i++ )
+            p->pCubeDataOut[i] ^= q->pCubeDataOut[i];
+        p->z = s_ChangeStore.PrevPz;
+        // p->a did not change
+    }
+}
+
+///////////////////////////////////////////////////////////////////
+///               CUBE SET MANIPULATION PROCEDURES              ///
+///////////////////////////////////////////////////////////////////
+
+// Cube set is a list of cubes
+//static Cube* s_List;
+
+///////////////////////////////////////////////////////////////////
+///                 Memory Allocation/Delocation                ///
+///////////////////////////////////////////////////////////////////
+
+int AllocateCubeSets( int nVarsIn, int nVarsOut )
+{
+    s_List = NULL;
+
+    // clean other data
+    s_fDistEnable2 = 1;
+    s_fDistEnable3 = 0;
+    s_fDistEnable4 = 0;
+    memset( s_CubeGroup, 0, sizeof(void *) * 5 );
+    memset( s_fInserted, 0, sizeof(int) * 5 );
+    s_fDecreaseLiterals = 0;
+    s_cEnquequed = 0;
+    s_cAttempts = 0;
+    s_cReshapes = 0;
+    s_nCubesBefore = 0;
+    s_Gain = 0;
+    s_GainTotal = 0;
+    s_GroupCounter = 0;
+    s_GroupBest = 0;
+    s_pC1 = s_pC2 = NULL;
+
+    return 4;
+}
+
+void DelocateCubeSets()
+{
+}
+
+///////////////////////////////////////////////////////////////////
+///                     Insertion Operators                     ///
+///////////////////////////////////////////////////////////////////
+
+void CubeInsert( Cube* p )
+// inserts the cube into storage (puts it at the beginning of the list)
+{
+    assert( p->Prev == NULL && p->Next == NULL );
+    assert( p->ID );
+
+    if ( s_List == NULL )
+        s_List = p;
+    else
+    {
+        p->Next = s_List;
+
+        s_List->Prev = p;
+        s_List = p;
+    }
+
+    g_CoverInfo.nCubesInUse++;
+}
+
+Cube* CubeExtract( Cube* p )
+// extracts the cube from storage
+{
+//  assert( p->Prev && p->Next ); // can be done only with rings
+    assert( p->ID );
+
+//  if ( s_List == p )
+//      s_List = p->Next;
+//  if ( p->Prev )
+//      p->Prev->Next = p->Next;
+
+    if ( s_List == p )
+        s_List = p->Next;
+    else
+        p->Prev->Next = p->Next;
+
+    if ( p->Next )
+        p->Next->Prev = p->Prev;
+
+    p->Prev = NULL;
+    p->Next = NULL;
+
+    g_CoverInfo.nCubesInUse--;
+    return p;
+}
+
+///////////////////////////////////////////////////////////////////
+///                       CUBE ITERATOR                         ///
+///////////////////////////////////////////////////////////////////
+
+// the iterator starts from the Head and stops when it sees NULL
+Cube* s_pCubeLast;
+
+///////////////////////////////////////////////////////////////////
+///                     Cube Set Iterator                       ///
+///////////////////////////////////////////////////////////////////
+
+Cube* IterCubeSetStart()
+// starts an iterator that traverses all the cubes in the ring
+{
+    assert( s_pCubeLast == NULL );
+
+    // check whether the List has cubes
+    if ( s_List == NULL )
+        return NULL;
+
+    return ( s_pCubeLast = s_List );
+}
+
+Cube* IterCubeSetNext()
+// returns the next cube in the cube set
+// to use it again after it has returned NULL, first call IterCubeSetStart()
+{
+    assert( s_pCubeLast );
+    return ( s_pCubeLast = s_pCubeLast->Next );
+}
+
+///////////////////////////////////////////////////////////////////
+////                      ADJACENCY QUEQUES                  //////
+///////////////////////////////////////////////////////////////////
+
+typedef struct
+{
+    Cube** pC1;      // the pointer to the first cube
+    Cube** pC2;      // the pointer to the second cube
+    byte*  ID1;      // the ID of the first cube
+    byte*  ID2;      // the ID of the second cube
+    int  PosOut;     // extract position
+    int  PosIn;      // insert position
+    int  PosCur;     // temporary insert position
+    int  PosMark;    // the marked position
+    int  fEmpty;     // this flag is 1 if there is nothing in the queque
+} que;
+
+static que s_Que[3];  // Dist-2, Dist-3, Dist-4 queques
+
+// the number of allocated places
+//int s_nPosAlloc;
+// the maximum number of occupied places
+//int s_nPosMax[3];
+
+//////////////////////////////////////////////////////////////////////
+//            Conditional Adding Cube Pairs To Queques              //
+//////////////////////////////////////////////////////////////////////
+
+int GetPosDiff( int PosBeg, int PosEnd )
+{
+    return (PosEnd - PosBeg + s_nPosAlloc) % s_nPosAlloc;
+}
+
+void MarkSet()
+// sets marks in the cube pair queques
+{
+    s_Que[0].PosMark = s_Que[0].PosIn;
+    s_Que[1].PosMark = s_Que[1].PosIn;
+    s_Que[2].PosMark = s_Que[2].PosIn;
+}
+
+void MarkRewind()
+// rewinds the queques to the previously set marks
+{
+    s_Que[0].PosIn = s_Que[0].PosMark;
+    s_Que[1].PosIn = s_Que[1].PosMark;
+    s_Que[2].PosIn = s_Que[2].PosMark;
+}
+
+void NewRangeReset()
+// resets temporarily stored new range of cube pairs
+{
+    s_Que[0].PosCur = s_Que[0].PosIn;
+    s_Que[1].PosCur = s_Que[1].PosIn;
+    s_Que[2].PosCur = s_Que[2].PosIn;
+}
+
+void NewRangeAdd()
+// adds temporarily stored new range of cube pairs to the queque
+{
+    s_Que[0].PosIn = s_Que[0].PosCur;
+    s_Que[1].PosIn = s_Que[1].PosCur;
+    s_Que[2].PosIn = s_Que[2].PosCur;
+}
+
+void NewRangeInsertCubePair( cubedist Dist, Cube* p1, Cube* p2 )
+// insert one cube pair into the new range
+{
+    que* p = &s_Que[Dist];
+    int Pos = p->PosCur;
+
+    if ( p->fEmpty || Pos != p->PosOut )
+    {
+        p->pC1[Pos] = p1;
+        p->pC2[Pos] = p2;
+        p->ID1[Pos] = p1->ID;
+        p->ID2[Pos] = p2->ID;
+
+        p->PosCur = (p->PosCur+1)%s_nPosAlloc;
+    }
+    else
+        assert(0);
+//      cout << endl << "DIST-" << (int)(Dist+2) << ": Have run out of queque space!" << endl;
+}
+
+void PrintQuequeStats()
+{
+/*
+    cout << endl << "Queque statistics: ";
+    cout << " Alloc = " << s_nPosAlloc;
+    cout << "   DIST2 = " << GetPosDiff( s_Que[0].PosOut, s_Que[0].PosIn );
+    cout << "   DIST3 = " << GetPosDiff( s_Que[1].PosOut, s_Que[1].PosIn );
+    cout << "   DIST4 = " << GetPosDiff( s_Que[2].PosOut, s_Que[2].PosIn );
+    cout << endl;
+    cout << endl;
+*/
+}
+
+int GetQuequeStats( cubedist Dist )
+{
+    return GetPosDiff( s_Que[Dist].PosOut, s_Que[Dist].PosIn );
+}
+
+//////////////////////////////////////////////////////////////////////
+//                       Queque Iterators                           //
+//////////////////////////////////////////////////////////////////////
+
+// iterating through the queque (with authomatic garbage collection)
+// only one iterator can be active at a time
+static struct
+{
+    int fStarted;    // status of the iterator (1 if working)
+    cubedist Dist;   // the currently iterated queque
+    Cube** ppC1;     // the position where the first cube pointer goes
+    Cube** ppC2;     // the position where the second cube pointer goes
+    int PosStop;     // the stop position (to prevent the iterator from
+                     // choking when new pairs are added during iteration)
+    int CutValue;    // the number of literals below which the cubes are not used
+} s_Iter;
+
+static que* pQ;
+static Cube *p1, *p2;
+
+int IteratorCubePairStart( cubedist CubeDist, Cube** ppC1, Cube** ppC2 )
+// start an iterator through cubes of dist CubeDist,
+// the resulting pointers are written into ppC1 and ppC2
+// returns 1 if the first cube pair is found
+{
+    int fEntryFound;
+
+    assert( s_Iter.fStarted == 0 );
+    assert( CubeDist >= 0 && CubeDist <= 2 );
+
+    s_Iter.fStarted = 1;
+    s_Iter.Dist = CubeDist;
+    s_Iter.ppC1 = ppC1;
+    s_Iter.ppC2 = ppC2;
+
+    s_Iter.PosStop = s_Que[ CubeDist ].PosIn;
+
+    // determine the cut value
+//  s_Iter.CutValue = s_nLiteralsInUse/s_nCubesInUse/2;
+    s_Iter.CutValue = -1;
+
+    fEntryFound = 0;
+    // go through the entries while there is something in the queque
+    for ( pQ = &s_Que[ CubeDist ]; pQ->PosOut != s_Iter.PosStop; pQ->PosOut = (pQ->PosOut+1)%s_nPosAlloc )
+    {
+        p1 = pQ->pC1[ pQ->PosOut ];
+        p2 = pQ->pC2[ pQ->PosOut ];
+
+        // check whether the entry is valid
+        if ( p1->ID == pQ->ID1[ pQ->PosOut ] && 
+             p2->ID == pQ->ID2[ pQ->PosOut ] ) //&&
+             //p1->x + p1->y + p2->x + p2->y > s_Iter.CutValue )
+        {
+             fEntryFound = 1;
+             break;
+        }
+    }
+
+    if ( fEntryFound )
+    { // write the result into the pick-up place
+        *ppC1 = pQ->pC1[ pQ->PosOut ];
+        *ppC2 = pQ->pC2[ pQ->PosOut ];
+
+        pQ->PosOut = (pQ->PosOut+1)%s_nPosAlloc;
+    }
+    else
+        s_Iter.fStarted = 0;
+    return fEntryFound;
+}
+
+int IteratorCubePairNext()
+// gives the next VALID cube pair (the previous one is automatically dequequed)
+{
+    int fEntryFound = 0;
+    assert( s_Iter.fStarted );
+
+    // go through the entries while there is something in the queque
+    for ( pQ = &s_Que[ s_Iter.Dist ]; pQ->PosOut != s_Iter.PosStop; pQ->PosOut = (pQ->PosOut+1)%s_nPosAlloc )
+    {
+        p1 = pQ->pC1[ pQ->PosOut ];
+        p2 = pQ->pC2[ pQ->PosOut ];
+
+        // check whether the entry is valid
+        if ( p1->ID == pQ->ID1[ pQ->PosOut ] && 
+             p2->ID == pQ->ID2[ pQ->PosOut ] ) //&&
+             //p1->x + p1->y + p2->x + p2->y > s_Iter.CutValue )
+        {
+             fEntryFound = 1;
+             break;
+        }
+    }
+
+    if ( fEntryFound )
+    { // write the result into the pick-up place
+        *(s_Iter.ppC1) = pQ->pC1[ pQ->PosOut ];
+        *(s_Iter.ppC2) = pQ->pC2[ pQ->PosOut ];
+
+        pQ->PosOut = (pQ->PosOut+1)%s_nPosAlloc;
+    }
+    else // iteration has finished
+        s_Iter.fStarted = 0;
+
+    return fEntryFound;
+}
+
+//////////////////////////////////////////////////////////////////////
+//                     Allocation/Delocation                        //
+//////////////////////////////////////////////////////////////////////
+
+int AllocateQueques( int nPlaces )
+// nPlaces should be approximately nCubes*nCubes/10
+// allocates memory for cube pair queques
+{
+    int i;
+    s_nPosAlloc  = nPlaces;
+
+    for ( i = 0; i < 3; i++ )
+    {
+        // clean data
+        memset( &s_Que[i], 0, sizeof(que) );
+
+        s_Que[i].pC1 = (Cube**) ABC_ALLOC( Cube*, nPlaces );
+        s_Que[i].pC2 = (Cube**) ABC_ALLOC( Cube*, nPlaces );
+        s_Que[i].ID1 = (byte*) ABC_ALLOC( byte, nPlaces );
+        s_Que[i].ID2 = (byte*) ABC_ALLOC( byte, nPlaces );
+
+        if ( s_Que[i].pC1==NULL || s_Que[i].pC2==NULL || s_Que[i].ID1==NULL || s_Que[i].ID2==NULL )
+            return 0;
+
+        s_nPosMax[i] = 0;
+        s_Que[i].fEmpty = 1;
+    }
+
+    return nPlaces * (sizeof(Cube*) + sizeof(Cube*) + 2*sizeof(byte) );
+}
+
+void DelocateQueques()
+{
+    int i;
+    for ( i = 0; i < 3; i++ )
+    {
+        ABC_FREE( s_Que[i].pC1 );
+        ABC_FREE( s_Que[i].pC2 );
+        ABC_FREE( s_Que[i].ID1 );
+        ABC_FREE( s_Que[i].ID2 );
+    }
+}
+
+///////////////////////////////////////////////////////////////////
+////////////              End of File             /////////////////
+///////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
diff --git a/src/base/exor/exorUtil.c b/src/base/exor/exorUtil.c
new file mode 100644
index 00000000..fb0f40f3
--- /dev/null
+++ b/src/base/exor/exorUtil.c
@@ -0,0 +1,204 @@
+/**CFile****************************************************************
+
+  FileName    [exorUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Exclusive sum-of-product minimization.]
+
+  Synopsis    [Utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: exorUtil.c,v 1.0 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///                  Implementation of EXORCISM - 4                  ///
+///              An Exclusive Sum-of-Product Minimizer               ///
+///               Alan Mishchenko  <alanmi@ee.pdx.edu>               ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///                                                                  ///
+///                        Utility Functions                         ///
+///                                                                  ///
+///       1) allocating memory for and creating the ESOP cover       ///
+///       2) writing the resultant cover into an ESOP PLA file       ///
+///                                                                  ///
+///  Ver. 1.0. Started - July 15, 2000. Last update - July 20, 2000  ///
+///  Ver. 1.4. Started -  Aug 10, 2000. Last update -  Aug 10, 2000  ///
+///  Ver. 1.5. Started -  Aug 19, 2000. Last update -  Aug 19, 2000  ///
+///  Ver. 1.7. Started -  Sep 20, 2000. Last update -  Sep 23, 2000  ///
+///                                                                  ///
+////////////////////////////////////////////////////////////////////////
+///   This software was tested with the BDD package "CUDD", v.2.3.0  ///
+///                          by Fabio Somenzi                        ///
+///                  http://vlsi.colorado.edu/~fabio/                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "exor.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                      EXTERNAL VARIABLES                         ////
+////////////////////////////////////////////////////////////////////////
+
+// information about the options, the function, and the cover
+extern cinfo g_CoverInfo;
+
+////////////////////////////////////////////////////////////////////////
+///                        EXTERNAL FUNCTIONS                        ///
+////////////////////////////////////////////////////////////////////////
+
+// Cube Cover Iterator
+// starts an iterator that traverses all the cubes in the ring
+extern Cube* IterCubeSetStart();
+// returns the next cube in the ring
+extern Cube* IterCubeSetNext();
+
+// retrieves the variable from the cube
+extern varvalue GetVar( Cube* pC, int Var );
+
+////////////////////////////////////////////////////////////////////////
+///                      FUNCTION DECLARATIONS                       ///
+////////////////////////////////////////////////////////////////////////
+
+///////////////////////////////////////////////////////////////////
+////////////       Cover Service Procedures       /////////////////
+///////////////////////////////////////////////////////////////////
+
+int CountLiterals()
+// nCubesAlloc is the number of allocated cubes 
+{
+    Cube* p;
+    int Value, v;
+    int LitCounter = 0;
+    int LitCounterControl = 0;
+
+    for ( p = IterCubeSetStart( ); p; p = IterCubeSetNext() )
+    {
+        LitCounterControl += p->a;
+
+        assert( p->fMark == 0 );
+
+        // write the input variables
+        for ( v = 0; v < g_CoverInfo.nVarsIn; v++ )
+        {
+            Value = GetVar( p, v );
+            if ( Value == VAR_NEG )
+                LitCounter++;
+            else if ( Value == VAR_POS )
+                LitCounter++;
+            else if ( Value != VAR_ABS )
+            {
+                assert(0);
+            }
+        }
+    }
+
+    if ( LitCounterControl != LitCounter )
+        printf( "Warning! The recorded number of literals (%d) differs from the actual number (%d)\n", LitCounterControl, LitCounter );
+    return LitCounter;
+}
+
+
+void WriteTableIntoFile( FILE * pFile )
+// nCubesAlloc is the number of allocated cubes 
+{
+    int v, w;
+    Cube * p;
+    int cOutputs;
+    int nOutput;
+    int WordSize;
+
+    for ( p = IterCubeSetStart( ); p; p = IterCubeSetNext() )
+    {
+        assert( p->fMark == 0 );
+
+        // write the input variables
+        for ( v = 0; v < g_CoverInfo.nVarsIn; v++ )
+        {
+            int Value = GetVar( p, v );
+            if ( Value == VAR_NEG )
+                fprintf( pFile, "0" );
+            else if ( Value == VAR_POS )
+                fprintf( pFile, "1" );
+            else if ( Value == VAR_ABS )
+                fprintf( pFile, "-" );
+            else
+                assert(0);
+        }
+        fprintf( pFile, " " );
+
+        // write the output variables
+        cOutputs = 0;
+        nOutput = g_CoverInfo.nVarsOut;
+        WordSize = 8*sizeof( unsigned );
+        for ( w = 0; w < g_CoverInfo.nWordsOut; w++ )
+            for ( v = 0; v < WordSize; v++ )
+            {
+                if ( p->pCubeDataOut[w] & (1<<v) )
+                    fprintf( pFile, "1" );
+                else
+                    fprintf( pFile, "0" );
+                if ( ++cOutputs == nOutput )
+                    break;
+            }
+        fprintf( pFile, "\n" );
+    }
+}
+
+
+int WriteResultIntoFile( char * pFileName )
+// write the ESOP cover into the PLA file <NewFileName>
+{
+    FILE * pFile;
+    time_t ltime;
+    char * TimeStr;
+
+    pFile = fopen( pFileName, "w" );
+    if ( pFile == NULL )
+    {
+        fprintf( pFile, "\n\nCannot open the output file\n" );
+        return 1;
+    }
+
+    // get current time
+    time( &ltime );
+    TimeStr = asctime( localtime( &ltime ) );
+    // get the number of literals
+    g_CoverInfo.nLiteralsAfter = CountLiterals();
+    fprintf( pFile, "# EXORCISM-4 output for command line arguments: " );
+    fprintf( pFile, "\"-Q %d -V %d\"\n", g_CoverInfo.Quality, g_CoverInfo.Verbosity );
+    fprintf( pFile, "# Minimization performed %s", TimeStr );
+    fprintf( pFile, "# Initial statistics: " );
+    fprintf( pFile, "Cubes = %d  Literals = %d\n", g_CoverInfo.nCubesBefore, g_CoverInfo.nLiteralsBefore );
+    fprintf( pFile, "# Final   statistics: " );
+    fprintf( pFile, "Cubes = %d  Literals = %d\n", g_CoverInfo.nCubesInUse, g_CoverInfo.nLiteralsAfter );
+    fprintf( pFile, "# File reading and reordering time = %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeRead) );
+    fprintf( pFile, "# Starting cover generation time   = %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeStart) );
+    fprintf( pFile, "# Pure ESOP minimization time      = %.2f sec\n", TICKS_TO_SECONDS(g_CoverInfo.TimeMin) );
+    fprintf( pFile, ".i %d\n", g_CoverInfo.nVarsIn );
+    fprintf( pFile, ".o %d\n", g_CoverInfo.nVarsOut );
+    fprintf( pFile, ".p %d\n", g_CoverInfo.nCubesInUse );
+    fprintf( pFile, ".type esop\n" );
+    WriteTableIntoFile( pFile );
+    fprintf( pFile, ".e\n" );
+    fclose( pFile );
+    return 0;
+}
+
+///////////////////////////////////////////////////////////////////
+////////////              End of File             /////////////////
+///////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/exor/module.make b/src/base/exor/module.make
new file mode 100644
index 00000000..842f9328
--- /dev/null
+++ b/src/base/exor/module.make
@@ -0,0 +1,6 @@
+SRC +=    src/base/exor/exor.c \
+    src/base/exor/exorBits.c \
+    src/base/exor/exorCubes.c \
+    src/base/exor/exorLink.c \
+    src/base/exor/exorList.c \
+    src/base/exor/exorUtil.c 
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 83ffaf53..1abe6abf 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -903,10 +903,10 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk;
     char * pFileName;
-    int c, fZeros = 0, fBoth = 0, fCheck = 1;
+    int c, fZeros = 0, fBoth = 0, fSkipPrepro = 0, fCheck = 1;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "zbch" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "zbxch" ) ) != EOF )
     {
         switch ( c )
         {
@@ -916,6 +916,9 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
             case 'b':
                 fBoth ^= 1;
                 break;
+            case 'x':
+                fSkipPrepro ^= 1;
+                break;
             case 'c':
                 fCheck ^= 1;
                 break;
@@ -930,10 +933,10 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
     // get the input file name
     pFileName = argv[globalUtilOptind];
     // read the file using the corresponding file reader
-    if ( fZeros || fBoth )
+    if ( fZeros || fBoth || fSkipPrepro )
     {
         Abc_Ntk_t * pTemp;
-        pNtk = Io_ReadPla( pFileName, fZeros, fBoth, fCheck );
+        pNtk = Io_ReadPla( pFileName, fZeros, fBoth, fSkipPrepro, fCheck );
         if ( pNtk == NULL )
         {
             printf( "Reading PLA file has failed.\n" );
@@ -952,10 +955,11 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: read_pla [-zbch] <file>\n" );
+    fprintf( pAbc->Err, "usage: read_pla [-zbxch] <file>\n" );
     fprintf( pAbc->Err, "\t         reads the network in PLA\n" );
     fprintf( pAbc->Err, "\t-z     : toggle reading on-set and off-set [default = %s]\n", fZeros? "off-set":"on-set" );
     fprintf( pAbc->Err, "\t-b     : toggle reading both on-set and off-set as on-set [default = %s]\n", fBoth? "off-set":"on-set" );
+    fprintf( pAbc->Err, "\t-x     : toggle reading Exclusive SOP rather than SOP [default = %s]\n", fSkipPrepro? "yes":"no" );
     fprintf( pAbc->Err, "\t-c     : toggle network check after reading [default = %s]\n", fCheck? "yes":"no" );
     fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
     fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
diff --git a/src/base/io/ioAbc.h b/src/base/io/ioAbc.h
index aa532ec5..a1239558 100644
--- a/src/base/io/ioAbc.h
+++ b/src/base/io/ioAbc.h
@@ -93,7 +93,7 @@ extern Abc_Ntk_t *        Io_ReadEdif( char * pFileName, int fCheck );
 /*=== abcReadEqn.c ============================================================*/
 extern Abc_Ntk_t *        Io_ReadEqn( char * pFileName, int fCheck );
 /*=== abcReadPla.c ============================================================*/
-extern Abc_Ntk_t *        Io_ReadPla( char * pFileName, int fZeros, int fBoth, int fCheck );
+extern Abc_Ntk_t *        Io_ReadPla( char * pFileName, int fZeros, int fBoth, int fSkipPrepro, int fCheck );
 /*=== abcReadVerilog.c ========================================================*/
 extern Abc_Ntk_t *        Io_ReadVerilog( char * pFileName, int fCheck );
 /*=== abcWriteAiger.c =========================================================*/
diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c
index ceadbebc..2c261dc3 100644
--- a/src/base/io/ioReadPla.c
+++ b/src/base/io/ioReadPla.c
@@ -28,7 +28,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth );
+static Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth, int fSkipPrepro );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -326,7 +326,7 @@ void Io_ReadPlaCubePreprocess( Vec_Str_t * vSop, int iCover, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fBoth, int fCheck )
+Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fBoth, int fSkipPrepro, int fCheck )
 {
     Extra_FileReader_t * p;
     Abc_Ntk_t * pNtk;
@@ -338,7 +338,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fBoth, int fCheck )
         return NULL;
 
     // read the network
-    pNtk = Io_ReadPlaNetwork( p, fZeros, fBoth );
+    pNtk = Io_ReadPlaNetwork( p, fZeros, fBoth, fSkipPrepro );
     Extra_FileReaderFree( p );
     if ( pNtk == NULL )
         return NULL;
@@ -363,7 +363,7 @@ Abc_Ntk_t * Io_ReadPla( char * pFileName, int fZeros, int fBoth, int fCheck )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth )
+Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth, int fSkipPrepro )
 {
     ProgressBar * pProgress;
     Vec_Ptr_t * vTokens;
@@ -567,7 +567,8 @@ Abc_Ntk_t * Io_ReadPlaNetwork( Extra_FileReader_t * p, int fZeros, int fBoth )
             continue;
         }
         Vec_StrPush( ppSops[i], 0 );
-        Io_ReadPlaCubePreprocess( ppSops[i], i, 0 );
+        if ( !fSkipPrepro )
+            Io_ReadPlaCubePreprocess( ppSops[i], i, 0 );
         pNode->pData = Abc_SopRegister( (Mem_Flex_t *)pNtk->pManFunc, ppSops[i]->pArray );
         Vec_StrFree( ppSops[i] );
     }
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 2432079f..7e8ece6e 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -144,7 +144,7 @@ Abc_Ntk_t * Io_ReadNetlist( char * pFileName, Io_FileType_t FileType, int fCheck
     else if ( FileType == IO_FILE_EQN )
         pNtk = Io_ReadEqn( pFileName, fCheck );
     else if ( FileType == IO_FILE_PLA )
-        pNtk = Io_ReadPla( pFileName, 0, 0, fCheck );
+        pNtk = Io_ReadPla( pFileName, 0, 0, 0, fCheck );
     else if ( FileType == IO_FILE_VERILOG )
         pNtk = Io_ReadVerilog( pFileName, fCheck );
     else