Version abc70711

19 files changed, 1225 insertions, 10 deletions

diff --git a/Makefile b/Makefile
index 28131069..3375bc42 100644
--- a/Makefile
+++ b/Makefile
@@ -10,7 +10,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
 	src/base/io src/base/main src/base/ver \
 	src/aig/ivy src/aig/hop src/aig/rwt src/aig/deco \
 	src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
-	src/aig/ec \
+	src/aig/csw src/aig/ec \
 	src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr \
 	src/bdd/parse src/bdd/reo src/bdd/cas \
 	src/map/fpga src/map/mapper src/map/mio \
diff --git a/abc.dsp b/abc.dsp
index c2fa926c..067aaaa5 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -945,6 +945,34 @@ SOURCE=.\src\aig\cnf\cnfUtil.c
 SOURCE=.\src\aig\cnf\cnfWrite.c
 # End Source File
 # End Group
+# Begin Group "csw"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\csw\csw.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswCut.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\csw\cswTable.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "bdd"
 
diff --git a/abc.rc b/abc.rc
index f1cf78d6..4b253b07 100644
--- a/abc.rc
+++ b/abc.rc
@@ -163,6 +163,9 @@ alias tst6     "r i10_if6.blif; st; ps; r x/rec6_16_.blif; st; rec_start; r i10_
 #alias t        "r i10_if4.blif; lp"
 #alias t1        "r pj1_if4.blif; lp"
 #alias t2        "r pj1_if6.blif; lp"
-alias t        "r pj/pj1.blif; st; dfraig -v"
+#alias t        "r pj/pj1.blif; st; dfraig -v"
+#alias t        "r c/16/csat_2.bench; st; dfraig -C 100 -v -r"
+#alias t        "r c/16/csat_147.bench; st; dfraig -C 10 -v -r"
+alias t        "r i10.blif; st; ps; csweep; ps; cec"
 
 
diff --git a/src/aig/csw/csw.h b/src/aig/csw/csw.h
new file mode 100644
index 00000000..4a326414
--- /dev/null
+++ b/src/aig/csw/csw.h
@@ -0,0 +1,65 @@
+/**CFile****************************************************************
+
+  FileName    [csw.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cut sweeping.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 11, 2007.]
+
+  Revision    [$Id: csw.h,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __CSW_H__
+#define __CSW_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                           ITERATORS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== cnfCore.c ========================================================*/
+extern Dar_Man_t *     Csw_Sweep( Dar_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/csw/cswCore.c b/src/aig/csw/cswCore.c
new file mode 100644
index 00000000..ddf37035
--- /dev/null
+++ b/src/aig/csw/cswCore.c
@@ -0,0 +1,80 @@
+/**CFile****************************************************************
+
+  FileName    [cswCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cut sweeping.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 11, 2007.]
+
+  Revision    [$Id: cswCore.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dar_Man_t * Csw_Sweep( Dar_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose )
+{
+    Csw_Man_t * p;
+    Dar_Man_t * pRes;
+    Dar_Obj_t * pObj, * pObjNew, * pObjRes;
+    int i;
+    // start the manager
+    p = Csw_ManStart( pAig, nCutsMax, nLeafMax, fVerbose );
+    // set elementary cuts at the PIs
+    Dar_ManForEachPi( p->pManRes, pObj, i )
+        Csw_ObjPrepareCuts( p, pObj, 1 );
+    // process the nodes
+    Dar_ManForEachNode( pAig, pObj, i )
+    {
+        // create the new node
+        pObjNew = Dar_And( p->pManRes, Csw_ObjChild0Equiv(p, pObj), Csw_ObjChild1Equiv(p, pObj) );
+        // check if this node can be represented using another node
+        pObjRes = Csw_ObjSweep( p, Dar_Regular(pObjNew), pObj->nRefs > 1 );
+        pObjRes = Dar_NotCond( pObjRes, Dar_IsComplement(pObjNew) );
+        // set the resulting node
+        Csw_ObjSetEquiv( p, pObj, pObjRes );
+    }
+    // add the POs
+    Dar_ManForEachPo( pAig, pObj, i )
+        Dar_ObjCreatePo( p->pManRes, Csw_ObjChild0Equiv(p, pObj) );
+    // remove dangling nodes 
+    Dar_ManCleanup( p->pManRes );
+    // return the resulting manager
+    pRes = p->pManRes;
+    Csw_ManStop( p );
+    return pRes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/csw/cswCut.c b/src/aig/csw/cswCut.c
new file mode 100644
index 00000000..f1cb1fde
--- /dev/null
+++ b/src/aig/csw/cswCut.c
@@ -0,0 +1,383 @@
+/**CFile****************************************************************
+
+  FileName    [cswCut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cut sweeping.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 11, 2007.]
+
+  Revision    [$Id: cswCut.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the cost of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Csw_CutFindCost( Csw_Man_t * p, Csw_Cut_t * pCut )
+{
+    Dar_Obj_t * pObj;
+    int i, Cost = 0;
+    Csw_CutForEachLeaf( p->pManRes, pCut, pObj, i )
+        Cost += pObj->nRefs;
+    return Cost * 100 / pCut->nFanins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the next free cut to use.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Csw_Cut_t * Csw_CutFindFree( Csw_Man_t * p, Dar_Obj_t * pObj )
+{
+    Csw_Cut_t * pCut, * pCutMax;
+    int i;
+    pCutMax = NULL;
+    Csw_ObjForEachCut( p, pObj, pCut, i )
+    {
+        if ( pCut->nFanins == 0 )
+            return pCut;
+        if ( pCutMax == NULL || pCutMax->Cost < pCut->Cost )
+            pCutMax = pCut;
+    }
+    assert( pCutMax != NULL );
+    pCutMax->nFanins = 0;
+    return pCutMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the stretching phase of the cut w.r.t. the merged cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline unsigned Cut_TruthPhase( Csw_Cut_t * pCut, Csw_Cut_t * pCut1 )
+{
+    unsigned uPhase = 0;
+    int i, k;
+    for ( i = k = 0; i < pCut->nFanins; i++ )
+    {
+        if ( k == pCut1->nFanins )
+            break;
+        if ( pCut->pFanins[i] < pCut1->pFanins[k] )
+            continue;
+        assert( pCut->pFanins[i] == pCut1->pFanins[k] );
+        uPhase |= (1 << i);
+        k++;
+    }
+    return uPhase;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs truth table computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Csw_CutComputeTruth( Csw_Man_t * p, Csw_Cut_t * pCut, Csw_Cut_t * pCut0, Csw_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+    // permute the first table
+    if ( fCompl0 ) 
+        Kit_TruthNot( p->puTemp[0], Csw_CutTruth(pCut0), p->nLeafMax );
+    else
+        Kit_TruthCopy( p->puTemp[0], Csw_CutTruth(pCut0), p->nLeafMax );
+    Kit_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nFanins, p->nLeafMax, Cut_TruthPhase(pCut, pCut0), 0 );
+    // permute the second table
+    if ( fCompl1 ) 
+        Kit_TruthNot( p->puTemp[1], Csw_CutTruth(pCut1), p->nLeafMax );
+    else
+        Kit_TruthCopy( p->puTemp[1], Csw_CutTruth(pCut1), p->nLeafMax );
+    Kit_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nFanins, p->nLeafMax, Cut_TruthPhase(pCut, pCut1), 0 );
+    // produce the resulting table
+    Kit_TruthAnd( Csw_CutTruth(pCut), p->puTemp[2], p->puTemp[3], p->nLeafMax );
+    return Csw_CutTruth(pCut);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Csw_CutMergeOrdered( Csw_Man_t * p, Csw_Cut_t * pC0, Csw_Cut_t * pC1, Csw_Cut_t * pC )
+{ 
+    int i, k, c;
+    assert( pC0->nFanins >= pC1->nFanins );
+    // the case of the largest cut sizes
+    if ( pC0->nFanins == p->nLeafMax && pC1->nFanins == p->nLeafMax )
+    {
+        for ( i = 0; i < pC0->nFanins; i++ )
+            if ( pC0->pFanins[i] != pC1->pFanins[i] )
+                return 0;
+        for ( i = 0; i < pC0->nFanins; i++ )
+            pC->pFanins[i] = pC0->pFanins[i];
+        pC->nFanins = pC0->nFanins;
+        return 1;
+    }
+    // the case when one of the cuts is the largest
+    if ( pC0->nFanins == p->nLeafMax )
+    {
+        for ( i = 0; i < pC1->nFanins; i++ )
+        {
+            for ( k = pC0->nFanins - 1; k >= 0; k-- )
+                if ( pC0->pFanins[k] == pC1->pFanins[i] )
+                    break;
+            if ( k == -1 ) // did not find
+                return 0;
+        }
+        for ( i = 0; i < pC0->nFanins; i++ )
+            pC->pFanins[i] = pC0->pFanins[i];
+        pC->nFanins = pC0->nFanins;
+        return 1;
+    }
+
+    // compare two cuts with different numbers
+    i = k = 0;
+    for ( c = 0; c < p->nLeafMax; c++ )
+    {
+        if ( k == pC1->nFanins )
+        {
+            if ( i == pC0->nFanins )
+            {
+                pC->nFanins = c;
+                return 1;
+            }
+            pC->pFanins[c] = pC0->pFanins[i++];
+            continue;
+        }
+        if ( i == pC0->nFanins )
+        {
+            if ( k == pC1->nFanins )
+            {
+                pC->nFanins = c;
+                return 1;
+            }
+            pC->pFanins[c] = pC1->pFanins[k++];
+            continue;
+        }
+        if ( pC0->pFanins[i] < pC1->pFanins[k] )
+        {
+            pC->pFanins[c] = pC0->pFanins[i++];
+            continue;
+        }
+        if ( pC0->pFanins[i] > pC1->pFanins[k] )
+        {
+            pC->pFanins[c] = pC1->pFanins[k++];
+            continue;
+        }
+        pC->pFanins[c] = pC0->pFanins[i++]; 
+        k++;
+    }
+    if ( i < pC0->nFanins || k < pC1->nFanins )
+        return 0;
+    pC->nFanins = c;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the object for FPGA mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Csw_CutMerge( Csw_Man_t * p, Csw_Cut_t * pCut0, Csw_Cut_t * pCut1, Csw_Cut_t * pCut )
+{ 
+    assert( p->nLeafMax > 0 );
+    // merge the nodes
+    if ( pCut0->nFanins < pCut1->nFanins )
+    {
+        if ( !Csw_CutMergeOrdered( p, pCut1, pCut0, pCut ) )
+            return 0;
+    }
+    else
+    {
+        if ( !Csw_CutMergeOrdered( p, pCut0, pCut1, pCut ) )
+            return 0;
+    }
+    pCut->uSign = pCut0->uSign | pCut1->uSign;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Csw_Cut_t * Csw_ObjPrepareCuts( Csw_Man_t * p, Dar_Obj_t * pObj, int fTriv )
+{
+    Csw_Cut_t * pCutSet, * pCut;
+    int i;
+    // create the cutset of the node
+    pCutSet = (Csw_Cut_t *)Dar_MmFixedEntryFetch( p->pMemCuts );
+    Csw_ObjSetCuts( p, pObj, pCutSet );
+    Csw_ObjForEachCut( p, pObj, pCut, i )
+    {
+        pCut->nFanins = 0;
+        pCut->iNode = pObj->Id;
+    }
+    // add unit cut if needed
+    if ( fTriv )
+    {
+        pCut = pCutSet;
+        pCut->Cost = 0;
+        pCut->iNode = pObj->Id;
+        pCut->nFanins = 1;
+        pCut->pFanins[0] = pObj->Id;
+        pCut->uSign = Csw_ObjCutSign( pObj->Id );
+        memset( Csw_CutTruth(pCut), 0xAA, sizeof(unsigned) * p->nTruthWords );
+    }
+    return pCutSet;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dar_Obj_t * Csw_ObjSweep( Csw_Man_t * p, Dar_Obj_t * pObj, int fTriv )
+{
+    Csw_Cut_t * pCut0, * pCut1, * pCut, * pCutSet;
+    Dar_Obj_t * pFanin0 = Dar_ObjFanin0(pObj);
+    Dar_Obj_t * pFanin1 = Dar_ObjFanin1(pObj);
+    Dar_Obj_t * pObjNew;
+    unsigned * pTruth;
+    int i, k, nVars, iVar;
+
+    assert( !Dar_IsComplement(pObj) );
+    if ( !Dar_ObjIsNode(pObj) )
+        return pObj;
+    if ( Csw_ObjCuts(p, pObj) )
+        return pObj;
+    // the node is not processed yet
+    assert( Csw_ObjCuts(p, pObj) == NULL );
+    assert( Dar_ObjIsNode(pObj) );
+
+    // set up the first cut
+    pCutSet = Csw_ObjPrepareCuts( p, pObj, fTriv );
+
+    // compute pair-wise cut combinations while checking table
+    Csw_ObjForEachCut( p, pFanin0, pCut0, i )
+    if ( pCut0->nFanins > 0 )
+    Csw_ObjForEachCut( p, pFanin1, pCut1, k )
+    if ( pCut1->nFanins > 0 )
+    {
+        // make sure K-feasible cut exists
+        if ( Kit_WordCountOnes(pCut0->uSign | pCut1->uSign) > p->nLeafMax )
+            continue;
+        // get the next cut of this node
+        pCut = Csw_CutFindFree( p, pObj );
+        // assemble the new cut
+        if ( !Csw_CutMerge( p, pCut0, pCut1, pCut ) )
+        {
+            assert( pCut->nFanins == 0 );
+            continue;
+        }
+/*
+        // check containment
+        if ( Csw_CutFilter( p, pCutSet, pCut ) )
+        {
+            pCut->nFanins = 0;
+            continue;
+        }
+*/
+        // create its truth table
+        pTruth = Csw_CutComputeTruth( p, pCut, pCut0, pCut1, Dar_ObjFaninC0(pObj), Dar_ObjFaninC1(pObj) );
+        // check for trivial truth table
+        nVars = Kit_TruthSupportSize( pTruth, p->nLeafMax );
+        if ( nVars == 0 )
+            return Dar_NotCond( Dar_ManConst1(p->pManRes), !(pTruth[0] & 1) );
+        if ( nVars == 1 )
+        {
+            iVar = Kit_WordFindFirstBit( Kit_TruthSupport(pTruth, p->nLeafMax) );
+            assert( iVar < pCut->nFanins );
+            return Dar_NotCond( Dar_ManObj(p->pManRes, pCut->pFanins[iVar]), (pTruth[0] & 1) );
+        }
+        // check if an equivalent node with the same cut exists
+        if ( pObjNew = Csw_TableCutLookup( p, pCut ) )
+            return pObjNew;
+        // assign the cost
+        pCut->Cost = Csw_CutFindCost( p, pCut );
+        assert( pCut->nFanins > 0 );
+        assert( pCut->Cost > 0 );
+    }
+
+    // load the resulting cuts into the table
+    Csw_ObjForEachCut( p, pObj, pCut, i )
+        if ( pCut->nFanins > 2 )
+        {
+            assert( pCut->Cost > 0 );
+            Csw_TableCutInsert( p, pCut );
+        }
+
+    // return the node if could not replace it
+    return pObj;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/csw/cswInt.h b/src/aig/csw/cswInt.h
new file mode 100644
index 00000000..74fa417b
--- /dev/null
+++ b/src/aig/csw/cswInt.h
@@ -0,0 +1,141 @@
+/**CFile****************************************************************
+
+  FileName    [cswInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cut sweeping.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 11, 2007.]
+
+  Revision    [$Id: cswInt.h,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __CSW_INT_H__
+#define __CSW_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
+#include "dar.h"
+#include "kit.h"
+#include "csw.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Csw_Man_t_            Csw_Man_t;
+typedef struct Csw_Cut_t_            Csw_Cut_t;
+
+// the cut used to represent node in the AIG
+struct Csw_Cut_t_
+{
+    Csw_Cut_t *     pNext;           // the next cut in the table 
+    int             Cost;            // the cost of the cut
+    unsigned        uSign;           // cut signature
+    int             iNode;           // the node, for which it is the cut
+    int             nFanins;         // the number of words in truth table
+    int             pFanins[0];      // the fanins (followed by the truth table)
+};
+
+// the CNF computation manager
+struct Csw_Man_t_
+{
+    // AIG manager
+    Dar_Man_t *     pManAig;         // the input AIG manager
+    Dar_Man_t *     pManRes;         // the output AIG manager
+    Dar_Obj_t **    pEquiv;          // the equivalent nodes in the resulting manager
+    Csw_Cut_t **    pCuts;           // the cuts for each node in the output manager
+    // hash table for cuts
+    Csw_Cut_t **    pTable;          // the table composed of cuts 
+    int             nTableSize;      // the size of hash table
+    // parameters
+    int             nCutsMax;        // the max number of cuts at the node
+    int             nLeafMax;        // the max number of leaves of a cut
+    int             fVerbose;        // enables verbose output
+    // internal variables
+    int             nCutSize;        // the number of bytes needed to store one cut
+    int             nTruthWords;     // the number of truth table words
+    Dar_MmFixed_t * pMemCuts;        // memory manager for cuts
+    unsigned *      puTemp[4];       // used for the truth table computation
+};
+
+static inline unsigned     Csw_ObjCutSign( unsigned ObjId )                 { return (1 << (ObjId % 31));                         }
+
+static inline int          Csw_CutLeaveNum( Csw_Cut_t * pCut )              { return pCut->nFanins;                               }
+static inline int *        Csw_CutLeaves( Csw_Cut_t * pCut )                { return pCut->pFanins;                               }
+static inline unsigned *   Csw_CutTruth( Csw_Cut_t * pCut )                 { return (unsigned *)(pCut->pFanins + pCut->nFanins); }
+static inline Csw_Cut_t *  Csw_CutNext( Csw_Man_t * p, Csw_Cut_t * pCut )   { return (Csw_Cut_t *)(((char *)pCut) + p->nCutSize); }
+
+static inline Csw_Cut_t *  Csw_ObjCuts( Csw_Man_t * p, Dar_Obj_t * pObj )                         { return p->pCuts[pObj->Id];    }
+static inline void         Csw_ObjSetCuts( Csw_Man_t * p, Dar_Obj_t * pObj, Csw_Cut_t * pCuts )   { p->pCuts[pObj->Id] = pCuts;   }
+
+static inline Dar_Obj_t *  Csw_ObjEquiv( Csw_Man_t * p, Dar_Obj_t * pObj )                        { return p->pEquiv[pObj->Id];   }
+static inline void         Csw_ObjSetEquiv( Csw_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pEquiv ) { p->pEquiv[pObj->Id] = pEquiv; }
+
+static inline Dar_Obj_t *  Csw_ObjChild0Equiv( Csw_Man_t * p, Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin0(pObj)? Dar_NotCond(Csw_ObjEquiv(p, Dar_ObjFanin0(pObj)), Dar_ObjFaninC0(pObj)) : NULL;  }
+static inline Dar_Obj_t *  Csw_ObjChild1Equiv( Csw_Man_t * p, Dar_Obj_t * pObj ) { assert( !Dar_IsComplement(pObj) ); return Dar_ObjFanin1(pObj)? Dar_NotCond(Csw_ObjEquiv(p, Dar_ObjFanin1(pObj)), Dar_ObjFaninC1(pObj)) : NULL;  }
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                           ITERATORS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// iterator over cuts of the node
+#define Csw_ObjForEachCut( p, pObj, pCut, i )                           \
+    for ( i = 0, pCut = Csw_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Csw_CutNext(p, pCut) ) 
+// iterator over leaves of the cut
+#define Csw_CutForEachLeaf( p, pCut, pLeaf, i )                         \
+    for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Dar_ManObj(p, (pCut)->pFanins[i])); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== cnfCut.c ========================================================*/
+extern Csw_Cut_t *    Csw_ObjPrepareCuts( Csw_Man_t * p, Dar_Obj_t * pObj, int fTriv );
+extern Dar_Obj_t *    Csw_ObjSweep( Csw_Man_t * p, Dar_Obj_t * pObj, int fTriv );
+/*=== cnfMan.c ========================================================*/
+extern Csw_Man_t *    Csw_ManStart( Dar_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose );
+extern void           Csw_ManStop( Csw_Man_t * p );
+/*=== cnfTable.c ========================================================*/
+extern void           Csw_TableCutInsert( Csw_Man_t * p, Csw_Cut_t * pCut );
+extern Dar_Obj_t *    Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut );
+extern unsigned int   Cudd_PrimeCws( unsigned int p );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/csw/cswMan.c b/src/aig/csw/cswMan.c
new file mode 100644
index 00000000..180fecef
--- /dev/null
+++ b/src/aig/csw/cswMan.c
@@ -0,0 +1,108 @@
+/**CFile****************************************************************
+
+  FileName    [cswMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cut sweeping.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 11, 2007.]
+
+  Revision    [$Id: cswMan.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the cut sweeping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Csw_Man_t * Csw_ManStart( Dar_Man_t * pMan, int nCutsMax, int nLeafMax, int fVerbose )
+{
+    Csw_Man_t * p;
+    Dar_Obj_t * pObj;
+    int i;
+    assert( nCutsMax >= 2  );
+    assert( nLeafMax <= 16 );
+    // allocate the fraiging manager
+    p = ALLOC( Csw_Man_t, 1 );
+    memset( p, 0, sizeof(Csw_Man_t) );
+    p->nCutsMax = nCutsMax;
+    p->nLeafMax = nLeafMax;
+    p->fVerbose = fVerbose;
+    p->pManAig  = pMan;
+    // create the new manager
+    p->pManRes  = Dar_ManStartFrom( pMan );
+    assert( Dar_ManPiNum(p->pManAig) == Dar_ManPiNum(p->pManRes) );
+    // allocate room for cuts and equivalent nodes
+    p->pEquiv   = ALLOC( Dar_Obj_t *, Dar_ManObjIdMax(pMan) + 1 );
+    p->pCuts    = ALLOC( Csw_Cut_t *, Dar_ManObjIdMax(pMan) + 1 );
+    memset( p->pCuts, 0, sizeof(Dar_Obj_t *) * (Dar_ManObjIdMax(pMan) + 1) );
+    // allocate memory manager
+    p->nTruthWords = Dar_TruthWordNum(nLeafMax);
+    p->nCutSize = sizeof(Csw_Cut_t) + sizeof(int) * nLeafMax + sizeof(unsigned) * p->nTruthWords;
+    p->pMemCuts = Dar_MmFixedStart( p->nCutSize * p->nCutsMax, 512 );
+    // allocate hash table for cuts
+    p->nTableSize = Cudd_PrimeCws( Dar_ManNodeNum(pMan) * p->nCutsMax / 2 );
+    p->pTable = ALLOC( Csw_Cut_t *, p->nTableSize );
+    memset( p->pTable, 0, sizeof(Dar_Obj_t *) * p->nTableSize );
+    // set the pointers to the available fraig nodes
+    Csw_ObjSetEquiv( p, Dar_ManConst1(p->pManAig), Dar_ManConst1(p->pManRes) );
+    Dar_ManForEachPi( p->pManAig, pObj, i )
+        Csw_ObjSetEquiv( p, pObj, Dar_ManPi(p->pManRes, i) );
+    // room for temporary truth tables
+    p->puTemp[0] = ALLOC( unsigned, 4 * p->nTruthWords );
+    p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
+    p->puTemp[2] = p->puTemp[1] + p->nTruthWords;
+    p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the fraiging manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Csw_ManStop( Csw_Man_t * p )
+{
+    free( p->puTemp[0] );
+    Dar_MmFixedStop( p->pMemCuts, 0 );
+    free( p->pEquiv );
+    free( p->pCuts );
+    free( p->pTable );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/csw/cswTable.c b/src/aig/csw/cswTable.c
new file mode 100644
index 00000000..82f09d01
--- /dev/null
+++ b/src/aig/csw/cswTable.c
@@ -0,0 +1,176 @@
+/**CFile****************************************************************
+
+  FileName    [cswTable.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cut sweeping.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 11, 2007.]
+
+  Revision    [$Id: cswTable.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Computes hash value of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Csw_CutHash( Csw_Cut_t * pCut )
+{
+    static int s_FPrimes[128] = { 
+        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
+        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
+        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
+        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
+        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
+        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
+        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
+        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
+        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
+        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
+        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
+        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
+        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+    };
+    unsigned uHash;
+    int i;
+    assert( pCut->nFanins <= 16 );
+    uHash = 0;
+    for ( i = 0; i < pCut->nFanins; i++ )
+        uHash ^= pCut->pFanins[i] * s_FPrimes[i];
+    return uHash;
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Returns the next prime >= p.]
+
+  Description [Copied from CUDD, for stand-aloneness.]
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+unsigned int Cudd_PrimeCws( unsigned int p )
+{
+    int i,pn;
+
+    p--;
+    do {
+        p++;
+        if (p&1) {
+        pn = 1;
+        i = 3;
+        while ((unsigned) (i * i) <= p) {
+        if (p % i == 0) {
+            pn = 0;
+            break;
+        }
+        i += 2;
+        }
+    } else {
+        pn = 0;
+    }
+    } while (!pn);
+    return(p);
+
+} /* end of Cudd_Prime */
+
+/**Function*************************************************************
+
+  Synopsis    [Adds the cut to the hash table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Csw_TableCutInsert( Csw_Man_t * p, Csw_Cut_t * pCut )
+{
+    int iEntry = Csw_CutHash(pCut) % p->nTableSize;
+    pCut->pNext = p->pTable[iEntry];
+    p->pTable[iEntry] = pCut;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns an equivalent node if it exists.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dar_Obj_t * Csw_TableCutLookup( Csw_Man_t * p, Csw_Cut_t * pCut )
+{
+    Dar_Obj_t * pRes = NULL;
+    Csw_Cut_t * pEnt;
+    unsigned * pTruthNew, * pTruthOld;
+    int iEntry = Csw_CutHash(pCut) % p->nTableSize;
+    for ( pEnt = p->pTable[iEntry]; pEnt; pEnt = pEnt->pNext )
+    {
+        if ( pEnt->nFanins != pCut->nFanins )
+            continue;
+        if ( pEnt->uSign != pCut->uSign )
+            continue;
+        if ( memcmp( pEnt->pFanins, pCut->pFanins, sizeof(int) * pCut->nFanins ) )
+            continue;
+        pTruthOld = Csw_CutTruth(pEnt);
+        pTruthNew = Csw_CutTruth(pCut);
+        if ( (pTruthOld[0] & 1) == (pTruthNew[0] & 1) )
+        {
+            if ( Kit_TruthIsEqual( pTruthOld, pTruthNew, pCut->nFanins ) )
+            {
+                pRes = Dar_ManObj( p->pManRes, pEnt->iNode );
+                assert( pRes->fPhase == Dar_ManObj( p->pManRes, pCut->iNode )->fPhase );
+                break;
+            }
+        }
+        else
+        {
+            if ( Kit_TruthIsOpposite( pTruthOld, pTruthNew, pCut->nFanins ) )
+            {
+                pRes = Dar_Not( Dar_ManObj( p->pManRes, pEnt->iNode ) );
+                assert( Dar_Regular(pRes)->fPhase != Dar_ManObj( p->pManRes, pCut->iNode )->fPhase );
+                break;
+            }
+        }
+    }
+    return pRes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/csw/csw_.c b/src/aig/csw/csw_.c
new file mode 100644
index 00000000..1c59f152
--- /dev/null
+++ b/src/aig/csw/csw_.c
@@ -0,0 +1,48 @@
+/**CFile****************************************************************
+
+  FileName    [csw_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Cut sweeping.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - July 11, 2007.]
+
+  Revision    [$Id: csw_.c,v 1.00 2007/07/11 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "cswInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/csw/module.make b/src/aig/csw/module.make
new file mode 100644
index 00000000..8fdb7bef
--- /dev/null
+++ b/src/aig/csw/module.make
@@ -0,0 +1,4 @@
+SRC +=    src/aig/csw/cswCore.c \
+    src/aig/csw/cswCut.c \
+    src/aig/csw/cswMan.c \
+    src/aig/csw/cswTable.c 
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 9744da88..8e82cdf4 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -382,6 +382,7 @@ extern Vec_Int_t *     Dar_LibReadOuts();
 extern void            Dar_LibReadMsops( char ** ppSopSizes, char *** ppSops );
 /*=== darDfs.c ==========================================================*/
 extern Vec_Ptr_t *     Dar_ManDfs( Dar_Man_t * p );
+extern Vec_Ptr_t *     Dar_ManDfsNodes( Dar_Man_t * p, Dar_Obj_t ** ppNodes, int nNodes );
 extern int             Dar_ManCountLevels( Dar_Man_t * p );
 extern void            Dar_ManCreateRefs( Dar_Man_t * p );
 extern int             Dar_DagSize( Dar_Obj_t * pObj );
diff --git a/src/aig/dar/darDfs.c b/src/aig/dar/darDfs.c
index bdb23c9d..116f428c 100644
--- a/src/aig/dar/darDfs.c
+++ b/src/aig/dar/darDfs.c
@@ -90,6 +90,35 @@ Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Collects internal nodes in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Dar_ManDfsNodes( Dar_Man_t * p, Dar_Obj_t ** ppNodes, int nNodes )
+{
+    Vec_Ptr_t * vNodes;
+    Dar_Obj_t * pObj;
+    int i;
+    assert( Dar_ManLatchNum(p) == 0 );
+    Dar_ManIncrementTravId( p );
+    // mark constant and PIs
+    Dar_ObjSetTravIdCurrent( p, Dar_ManConst1(p) );
+    Dar_ManForEachPi( p, pObj, i )
+        Dar_ObjSetTravIdCurrent( p, pObj );
+    // go through the nodes
+    vNodes = Vec_PtrAlloc( Dar_ManNodeNum(p) );
+    for ( i = 0; i < nNodes; i++ )
+        Dar_ManDfs_rec( p, ppNodes[i], vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Computes the max number of levels in the manager.]
 
   Description []
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index ee52520a..29195d19 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -117,6 +117,7 @@ struct Fra_Man_t_
     int              nSatProof;
     int              nSatFails;
     int              nSatFailsReal;
+    int              nSpeculs;         
     // runtime
     int              timeSim;
     int              timeTrav;
diff --git a/src/aig/fra/fraAnd.c b/src/aig/fra/fraAnd.c
index 86cbbc9e..a360ce9b 100644
--- a/src/aig/fra/fraAnd.c
+++ b/src/aig/fra/fraAnd.c
@@ -51,6 +51,8 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
     pFanin1Fraig = Fra_ObjChild1Fra(pObjOld);
     // get the fraiged node
     pObjFraig = Dar_And( p->pManFraig, pFanin0Fraig, pFanin1Fraig );
+    if ( Dar_ObjIsConst1(Dar_Regular(pObjFraig)) )
+        return pObjFraig;
     Dar_Regular(pObjFraig)->pData = p;
     // get representative of this class
     pObjOldRepr = Fra_ObjRepr(pObjOld);
@@ -79,14 +81,26 @@ Dar_Obj_t * Fra_And( Fra_Man_t * p, Dar_Obj_t * pObjOld )
     }
     if ( RetValue == -1 ) // failed
     {
+        Dar_Obj_t * ppNodes[2] = { Dar_Regular(pObjOldReprFraig), Dar_Regular(pObjFraig) };
+        Vec_Ptr_t * vNodes;
+
         if ( !p->pPars->fSpeculate )
             return pObjFraig;
         // substitute the node
 //        pObjOld->fMarkB = 1;
+        p->nSpeculs++;
+
+        vNodes = Dar_ManDfsNodes( p->pManFraig, ppNodes, 2 );
+        printf( "%d ", Vec_PtrSize(vNodes) );
+        Vec_PtrFree( vNodes );
+
         return Dar_NotCond( pObjOldReprFraig, pObjOld->fPhase ^ pObjOldRepr->fPhase );
     }
+//    printf( "Disproved %d and %d.\n", pObjOldRepr->Id, pObjOld->Id );
     // simulate the counter-example and return the Fraig node
+//    printf( "Representaive before = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
     Fra_Resimulate( p );
+//    printf( "Representaive after  = %d.\n", Fra_ObjRepr(pObjOld)? Fra_ObjRepr(pObjOld)->Id : -1 );
     assert( Fra_ObjRepr(pObjOld) != pObjOldRepr );
     return pObjFraig;
 }
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index ac6a4f4a..33421423 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -334,6 +334,7 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
     Dar_Obj_t * pObj, ** ppThis;
     int i;
     assert( ppClass[0] != NULL && ppClass[1] != NULL );
+
     // check if the class is going to be refined
     for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
         if ( !Fra_NodeCompareSims(p, ppClass[0], pObj) )
@@ -349,6 +350,15 @@ Dar_Obj_t ** Fra_RefineClassOne( Fra_Man_t * p, Dar_Obj_t ** ppClass )
             Vec_PtrPush( p->vClassOld, pObj );
         else
             Vec_PtrPush( p->vClassNew, pObj );
+/*
+    printf( "Refining class (" );
+    Vec_PtrForEachEntry( p->vClassOld, pObj, i )
+        printf( "%d,", pObj->Id );
+    printf( ") + (" );
+    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+        printf( "%d,", pObj->Id );
+    printf( ")\n" );
+*/
     // put the nodes back into the class memory
     Vec_PtrForEachEntry( p->vClassOld, pObj, i )
     {
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 67921318..19ed6c03 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -205,6 +205,7 @@ void Fra_ManPrint( Fra_Man_t * p )
     PRT( "Class refining  ", p->timeRef   );
     PRT( "TOTAL RUNTIME   ", p->timeTotal );
     if ( p->time1 ) { PRT( "time1           ", p->time1 ); }
+    printf( "Speculations = %d.\n", p->nSpeculs );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 06f4299d..9c2c0153 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -113,6 +113,7 @@ static int Abc_CommandIResyn         ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandISat           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandCSweep         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandIProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandHaig           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMini           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -269,6 +270,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "isat",          Abc_CommandISat,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "ifraig",        Abc_CommandIFraig,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "dfraig",        Abc_CommandDFraig,           1 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "csweep",        Abc_CommandCSweep,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "mini",          Abc_CommandMini,             1 );
@@ -6919,22 +6921,23 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int c, fProve, fVerbose, fDoSparse;
+    int c, fProve, fVerbose, fDoSparse, fSpeculate;
     int nConfLimit;
 
-    extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nConfLimit   = 100;   
-    fDoSparse    = 0;
+    nConfLimit   = 100;  
+    fSpeculate   = 0;
+    fDoSparse    = 1;
     fProve       = 0;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Cspvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Csprvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -6955,6 +6958,9 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'p':
             fProve ^= 1;
             break;
+        case 'r':
+            fSpeculate ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -6970,7 +6976,7 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
 
-    pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose );
+    pNtkRes = Abc_NtkDarFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fSpeculate, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -6981,11 +6987,101 @@ int Abc_CommandDFraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dfraig [-C num] [-spvh]\n" );
+    fprintf( pErr, "usage: dfraig [-C num] [-sprvh]\n" );
     fprintf( pErr, "\t         performs fraiging using a new method\n" );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit );
     fprintf( pErr, "\t-s     : toggle considering sparse functions [default = %s]\n", fDoSparse? "yes": "no" );
     fprintf( pErr, "\t-p     : toggle proving the miter outputs [default = %s]\n", fProve? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggle speculative reduction [default = %s]\n", fSpeculate? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandCSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c, nCutsMax, nLeafMax, fVerbose;
+
+    extern Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nCutsMax  =  8;  
+    nLeafMax  =  8;
+    fVerbose  =  0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CKvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCutsMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCutsMax < 0 ) 
+                goto usage;
+            break;
+        case 'K':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLeafMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLeafMax < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    pNtkRes = Abc_NtkCSweep( pNtk, nCutsMax, nLeafMax, fVerbose );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Command has failed.\n" );
+        return 0;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: csweep [-C num] [-K num] [-vh]\n" );
+    fprintf( pErr, "\t         performs cut sweeping using a new method\n" );
+    fprintf( pErr, "\t-C num : limit on the number of cuts [default = %d]\n", nCutsMax );
+    fprintf( pErr, "\t-K num : limit on the cut size [default = %d]\n", nLeafMax );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ba3ac89d..ed6fa77e 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -455,7 +455,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fSpeculate, int fVerbose )
 {
     Fra_Par_t Params, * pParams = &Params; 
     Abc_Ntk_t * pNtkAig;
@@ -468,6 +468,7 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
     pParams->fVerbose     = fVerbose;
     pParams->fProve       = fProve;
     pParams->fDoSparse    = fDoSparse;
+    pParams->fSpeculate   = fSpeculate;
     pMan = Fra_Perform( pTemp = pMan, pParams );
     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
     Dar_ManStop( pTemp );
@@ -475,6 +476,32 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
     return pNtkAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVerbose )
+{
+    extern Dar_Man_t * Csw_Sweep( Dar_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
+    Abc_Ntk_t * pNtkAig;
+    Dar_Man_t * pMan, * pTemp;
+    pMan = Abc_NtkToDar( pNtk );
+    if ( pMan == NULL )
+        return NULL;
+    pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
+    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
+    Dar_ManStop( pTemp );
+    Dar_ManStop( pMan );
+    return pNtkAig;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////