Version abc80126

author: Alan Mishchenko <alanmi@berkeley.edu> 2008-01-26 08:01:00 -0800
committer: Alan Mishchenko <alanmi@berkeley.edu> 2008-01-26 08:01:00 -0800
commit: 6537f941887b06e588d3acfc97b5fdf48875cc4e (patch)
tree: 61e11fbdd1bbcb781cf05f91f5095f559a58ab25 /src/aig
parent: 6c68b76bff33daa7cd94b78c51bdd4cdaf65059c (diff)
download: abc-6537f941887b06e588d3acfc97b5fdf48875cc4e.tar.gz
abc-6537f941887b06e588d3acfc97b5fdf48875cc4e.tar.bz2
abc-6537f941887b06e588d3acfc97b5fdf48875cc4e.zip
8 files changed, 1245 insertions, 71 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index e871373a..5bff39f7 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -137,6 +137,7 @@ struct Aig_Man_t_
     void (*pImpFunc) (void*, void*); // implication checking precedure
     void *           pImpData;       // implication checking data
     void *           pManTime;       // the timing manager
+    void *           pManCuts;
     Vec_Ptr_t *      vMapped;
     Vec_Int_t *      vFlopNums;      
     void *           pSeqModel;
@@ -146,6 +147,56 @@ struct Aig_Man_t_
     int              time2;
 };
 
+// cut computation
+typedef struct Aig_ManCut_t_         Aig_ManCut_t;
+typedef struct Aig_Cut_t_            Aig_Cut_t;
+
+// the cut used to represent node in the AIG
+struct Aig_Cut_t_
+{
+    Aig_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
+    short           nCutSize;        // the number of bytes in the cut
+    char            nLeafMax;        // the maximum number of fanins
+    char            nFanins;         // the current number of fanins
+    int             pFanins[0];      // the fanins (followed by the truth table)
+};
+
+// the CNF computation manager
+struct Aig_ManCut_t_
+{
+    // AIG manager
+    Aig_Man_t *     pAig;            // the input AIG manager
+    Aig_Cut_t **    pCuts;           // the cuts for each node in the output manager
+    // parameters
+    int             nCutsMax;        // the max number of cuts at the node
+    int             nLeafMax;        // the max number of leaves of a cut
+    int             fTruth;          // enables truth table computation
+    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
+    Aig_MmFixed_t * pMemCuts;        // memory manager for cuts
+    unsigned *      puTemp[4];       // used for the truth table computation
+};
+
+static inline Aig_Cut_t *  Aig_ObjCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj )                         { return p->pCuts[pObj->Id];  }
+static inline void         Aig_ObjSetCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj, Aig_Cut_t * pCuts )   { p->pCuts[pObj->Id] = pCuts; }
+
+static inline int          Aig_CutLeaveNum( Aig_Cut_t * pCut )          { return pCut->nFanins;                                    }
+static inline int *        Aig_CutLeaves( Aig_Cut_t * pCut )            { return pCut->pFanins;                                    }
+static inline unsigned *   Aig_CutTruth( Aig_Cut_t * pCut )             { return (unsigned *)(pCut->pFanins + pCut->nLeafMax);     }
+static inline Aig_Cut_t *  Aig_CutNext( Aig_Cut_t * pCut )              { return (Aig_Cut_t *)(((char *)pCut) + pCut->nCutSize);   }
+
+// iterator over cuts of the node
+#define Aig_ObjForEachCut( p, pObj, pCut, i )                           \
+    for ( i = 0, pCut = Aig_ObjCuts(p, pObj); i < p->nCutsMax; i++, pCut = Aig_CutNext(pCut) ) 
+// iterator over leaves of the cut
+#define Aig_CutForEachLeaf( p, pCut, pLeaf, i )                         \
+    for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -386,6 +437,9 @@ static inline int     Aig_ObjFanoutNext( Aig_Man_t * p, int iFan )   { assert(iF
 extern int             Aig_ManCheck( Aig_Man_t * p );
 extern void            Aig_ManCheckMarkA( Aig_Man_t * p );
 extern void            Aig_ManCheckPhase( Aig_Man_t * p );
+/*=== aigCuts.c ========================================================*/
+extern Aig_ManCut_t *  Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fTruth, int fVerbose );
+extern void            Aig_ManCutStop( Aig_ManCut_t * p );
 /*=== aigDfs.c ==========================================================*/
 extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsPio( Aig_Man_t * p );
diff --git a/src/aig/aig/aigCuts.c b/src/aig/aig/aigCuts.c
new file mode 100644
index 00000000..494d0d5b
--- /dev/null
+++ b/src/aig/aig/aigCuts.c
@@ -0,0 +1,669 @@
+/**CFile****************************************************************
+
+  FileName    [aigCuts.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Computation of K-feasible priority cuts.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigCuts.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the cut sweeping manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_ManCut_t * Aig_ManCutStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fTruth, int fVerbose )
+{
+    Aig_ManCut_t * p;
+    assert( nCutsMax >= 2  );
+    assert( nLeafMax <= 16 );
+    // allocate the fraiging manager
+    p = ALLOC( Aig_ManCut_t, 1 );
+    memset( p, 0, sizeof(Aig_ManCut_t) );
+    p->nCutsMax = nCutsMax;
+    p->nLeafMax = nLeafMax;
+    p->fTruth   = fTruth;
+    p->fVerbose = fVerbose;
+    p->pAig     = pMan;
+    // allocate room for cuts and equivalent nodes
+    p->pCuts    = ALLOC( Aig_Cut_t *, Aig_ManObjNumMax(pMan) );
+    memset( p->pCuts, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pMan) );
+    // allocate memory manager
+    p->nTruthWords = Aig_TruthWordNum(nLeafMax);
+    p->nCutSize = sizeof(Aig_Cut_t) + sizeof(int) * nLeafMax + fTruth * sizeof(unsigned) * p->nTruthWords;
+    p->pMemCuts = Aig_MmFixedStart( p->nCutSize * p->nCutsMax, 512 );
+    // room for temporary truth tables
+    if ( fTruth )
+    {
+        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 Aig_ManCutStop( Aig_ManCut_t * p )
+{
+    Aig_MmFixedStop( p->pMemCuts, 0 );
+    FREE( p->puTemp[0] );
+    free( p->pCuts );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_CutPrint( Aig_Cut_t * pCut )
+{
+    int i;
+    printf( "{" );
+    for ( i = 0; i < pCut->nFanins; i++ )
+        printf( " %d", pCut->pFanins[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjCutPrint( Aig_ManCut_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Cut_t * pCut;
+    int i;
+    printf( "Cuts for node %d:\n", pObj->Id );
+    Aig_ObjForEachCut( p, pObj, pCut, i )
+        if ( pCut->nFanins )
+            Aig_CutPrint( pCut );
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the total number of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCutCount( Aig_ManCut_t * p, int * pnCutsK )
+{
+    Aig_Cut_t * pCut;
+    Aig_Obj_t * pObj;
+    int i, k, nCuts = 0, nCutsK = 0;
+    Aig_ManForEachNode( p->pAig, pObj, i )
+        Aig_ObjForEachCut( p, pObj, pCut, k )
+        {
+            if ( pCut->nFanins == 0 )
+                continue;
+            nCuts++;
+            if ( pCut->nFanins == p->nLeafMax )
+                nCutsK++;
+        }
+    if ( pnCutsK )
+        *pnCutsK = nCutsK;
+    return nCuts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the cost of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_CutFindCost( Aig_ManCut_t * p, Aig_Cut_t * pCut )
+{
+    Aig_Obj_t * pLeaf;
+    int i, Cost = 0;
+    assert( pCut->nFanins > 0 );
+    Aig_CutForEachLeaf( p->pAig, pCut, pLeaf, i )
+        Cost += pLeaf->nRefs;
+    return Cost * 1000 / pCut->nFanins;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the cost of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline float Aig_CutFindCost2( Aig_ManCut_t * p, Aig_Cut_t * pCut )
+{
+    Aig_Obj_t * pLeaf;
+    float Cost = 0.0;
+    int i;
+    assert( pCut->nFanins > 0 );
+    Aig_CutForEachLeaf( p->pAig, pCut, pLeaf, i )
+        Cost += (float)1.0/pLeaf->nRefs;
+    return 1/Cost;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the next free cut to use.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline Aig_Cut_t * Aig_CutFindFree( Aig_ManCut_t * p, Aig_Obj_t * pObj )
+{
+    Aig_Cut_t * pCut, * pCutMax;
+    int i;
+    pCutMax = NULL;
+    Aig_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 Aig_CutTruthPhase( Aig_Cut_t * pCut, Aig_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 * Aig_CutComputeTruth( Aig_ManCut_t * p, Aig_Cut_t * pCut, Aig_Cut_t * pCut0, Aig_Cut_t * pCut1, int fCompl0, int fCompl1 )
+{
+    // permute the first table
+    if ( fCompl0 ) 
+        Kit_TruthNot( p->puTemp[0], Aig_CutTruth(pCut0), p->nLeafMax );
+    else
+        Kit_TruthCopy( p->puTemp[0], Aig_CutTruth(pCut0), p->nLeafMax );
+    Kit_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nFanins, p->nLeafMax, Aig_CutTruthPhase(pCut, pCut0), 0 );
+    // permute the second table
+    if ( fCompl1 ) 
+        Kit_TruthNot( p->puTemp[1], Aig_CutTruth(pCut1), p->nLeafMax );
+    else
+        Kit_TruthCopy( p->puTemp[1], Aig_CutTruth(pCut1), p->nLeafMax );
+    Kit_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nFanins, p->nLeafMax, Aig_CutTruthPhase(pCut, pCut1), 0 );
+    // produce the resulting table
+    Kit_TruthAnd( Aig_CutTruth(pCut), p->puTemp[2], p->puTemp[3], p->nLeafMax );
+//    assert( pCut->nFanins >= Kit_TruthSupportSize( Aig_CutTruth(pCut), p->nLeafMax ) );
+    return Aig_CutTruth(pCut);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs support minimization for the truth table.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_CutSupportMinimize( Aig_ManCut_t * p, Aig_Cut_t * pCut )
+{
+    unsigned * pTruth;
+    int uSupp, nFansNew, i, k;
+    // get truth table
+    pTruth = Aig_CutTruth( pCut );
+    // get support 
+    uSupp = Kit_TruthSupport( pTruth, p->nLeafMax );
+    // get the new support size
+    nFansNew = Kit_WordCountOnes( uSupp );
+    // check if there are redundant variables
+    if ( nFansNew == pCut->nFanins )
+        return nFansNew;
+    assert( nFansNew < pCut->nFanins );
+    // minimize support
+    Kit_TruthShrink( p->puTemp[0], pTruth, nFansNew, p->nLeafMax, uSupp, 1 );
+    for ( i = k = 0; i < pCut->nFanins; i++ )
+        if ( uSupp & (1 << i) )
+            pCut->pFanins[k++] = pCut->pFanins[i];
+    assert( k == nFansNew );
+    pCut->nFanins = nFansNew;
+//    assert( nFansNew == Kit_TruthSupportSize( pTruth, p->nLeafMax ) );
+//Extra_PrintBinary( stdout, pTruth, (1<<p->nLeafMax) ); printf( "\n" );
+    return nFansNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if pDom is contained in pCut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_CutCheckDominance( Aig_Cut_t * pDom, Aig_Cut_t * pCut )
+{
+    int i, k;
+    for ( i = 0; i < (int)pDom->nFanins; i++ )
+    {
+        for ( k = 0; k < (int)pCut->nFanins; k++ )
+            if ( pDom->pFanins[i] == pCut->pFanins[k] )
+                break;
+        if ( k == (int)pCut->nFanins ) // node i in pDom is not contained in pCut
+            return 0;
+    }
+    // every node in pDom is contained in pCut
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the cut is contained.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_CutFilter( Aig_ManCut_t * p, Aig_Obj_t * pObj, Aig_Cut_t * pCut )
+{ 
+    Aig_Cut_t * pTemp;
+    int i;
+    // go through the cuts of the node
+    Aig_ObjForEachCut( p, pObj, pTemp, i )
+    {
+        if ( pTemp->nFanins < 2 )
+            continue;
+        if ( pTemp == pCut )
+            continue;
+        if ( pTemp->nFanins > pCut->nFanins )
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pCut->uSign )
+                continue;
+            // check containment seriously
+            if ( Aig_CutCheckDominance( pCut, pTemp ) )
+            {
+                // remove contained cut
+                pTemp->nFanins = 0;
+            }
+         }
+        else
+        {
+            // skip the non-contained cuts
+            if ( (pTemp->uSign & pCut->uSign) != pTemp->uSign )
+                continue;
+            // check containment seriously
+            if ( Aig_CutCheckDominance( pTemp, pCut ) )
+            {
+                // remove the given
+                pCut->nFanins = 0;
+                return 1;
+            }
+        }
+    }
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Aig_CutMergeOrdered( Aig_ManCut_t * p, Aig_Cut_t * pC0, Aig_Cut_t * pC1, Aig_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 Aig_CutMerge( Aig_ManCut_t * p, Aig_Cut_t * pCut0, Aig_Cut_t * pCut1, Aig_Cut_t * pCut )
+{ 
+    assert( p->nLeafMax > 0 );
+    // merge the nodes
+    if ( pCut0->nFanins < pCut1->nFanins )
+    {
+        if ( !Aig_CutMergeOrdered( p, pCut1, pCut0, pCut ) )
+            return 0;
+    }
+    else
+    {
+        if ( !Aig_CutMergeOrdered( p, pCut0, pCut1, pCut ) )
+            return 0;
+    }
+    pCut->uSign = pCut0->uSign | pCut1->uSign;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Cut_t * Aig_ObjPrepareCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj, int fTriv )
+{
+    Aig_Cut_t * pCutSet, * pCut;
+    int i;
+    // create the cutset of the node
+    pCutSet = (Aig_Cut_t *)Aig_MmFixedEntryFetch( p->pMemCuts );
+    Aig_ObjSetCuts( p, pObj, pCutSet );
+    Aig_ObjForEachCut( p, pObj, pCut, i )
+    {
+        pCut->nFanins  = 0;
+        pCut->iNode    = pObj->Id;
+        pCut->nCutSize = p->nCutSize;
+        pCut->nLeafMax = p->nLeafMax;
+    }
+    // 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 = Aig_ObjCutSign( pObj->Id );
+        if ( p->fTruth )
+        memset( Aig_CutTruth(pCut), 0xAA, sizeof(unsigned) * p->nTruthWords );
+    }
+    return pCutSet;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives cuts for one node and sweeps this node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjComputeCuts( Aig_ManCut_t * p, Aig_Obj_t * pObj, int fTriv )
+{
+    Aig_Cut_t * pCut0, * pCut1, * pCut, * pCutSet;
+    Aig_Obj_t * pFanin0 = Aig_ObjFanin0(pObj);
+    Aig_Obj_t * pFanin1 = Aig_ObjFanin1(pObj);
+    int i, k;
+    // the node is not processed yet
+    assert( Aig_ObjIsNode(pObj) );
+    assert( Aig_ObjCuts(p, pObj) == NULL );
+    // set up the first cut
+    pCutSet = Aig_ObjPrepareCuts( p, pObj, fTriv );
+    // compute pair-wise cut combinations while checking table
+    Aig_ObjForEachCut( p, pFanin0, pCut0, i )
+    if ( pCut0->nFanins > 0 )
+    Aig_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 = Aig_CutFindFree( p, pObj );
+        // assemble the new cut
+        if ( !Aig_CutMerge( p, pCut0, pCut1, pCut ) )
+        {
+            assert( pCut->nFanins == 0 );
+            continue;
+        }
+        // check containment
+        if ( Aig_CutFilter( p, pObj, pCut ) )
+        {
+            assert( pCut->nFanins == 0 );
+            continue;
+        }
+        // create its truth table
+        if ( p->fTruth )
+            Aig_CutComputeTruth( p, pCut, pCut0, pCut1, Aig_ObjFaninC0(pObj), Aig_ObjFaninC1(pObj) );
+        // assign the cost
+        pCut->Cost = Aig_CutFindCost( p, pCut );
+        assert( pCut->nFanins > 0 );
+        assert( pCut->Cost > 0 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cuts for all nodes in the static AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_ManCut_t * Aig_ComputeCuts( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fTruth, int fVerbose )
+{
+    Aig_ManCut_t * p;
+    Aig_Obj_t * pObj;
+    int i, clk = clock();
+    assert( pAig->pManCuts == NULL );
+    // start the manager
+    p = Aig_ManCutStart( pAig, nCutsMax, nLeafMax, fTruth, fVerbose );
+    // set elementary cuts at the PIs
+    Aig_ManForEachPi( pAig, pObj, i )
+        Aig_ObjPrepareCuts( p, pObj, 1 );
+    // process the nodes
+    Aig_ManForEachNode( pAig, pObj, i )
+        Aig_ObjComputeCuts( p, pObj, 1 );
+    // print stats
+    if ( fVerbose )
+    {
+        int nCuts, nCutsK;
+        nCuts = Aig_ManCutCount( p, &nCutsK );
+        printf( "Nodes = %6d. Total cuts = %6d. %d-input cuts = %6d.\n",
+            Aig_ManObjNum(pAig), nCuts, nLeafMax, nCutsK );
+        printf( "Cut size = %2d. Truth size = %2d. Total mem = %5.2f Mb  ",
+            p->nCutSize, 4*p->nTruthWords, 1.0*Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) );
+        PRT( "Runtime", clock() - clk );
+/*
+        Aig_ManForEachNode( pAig, pObj, i )
+            if ( i % 300 == 0 )
+                Aig_ObjCutPrint( p, pObj );
+*/
+    }
+    // remember the cut manager
+    pAig->pManCuts = p;
+    return p;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
index 06731451..e1d62de0 100644
--- a/src/aig/cnf/cnfCore.c
+++ b/src/aig/cnf/cnfCore.c
@@ -57,7 +57,7 @@ Cnf_Dat_t * Cnf_Derive( Aig_Man_t * pAig, int nOutputs )
 
     // generate cuts for all nodes, assign cost, and find best cuts
 clk = clock();
-    pMemCuts = Dar_ManComputeCuts( pAig, 10 );
+    pMemCuts = Dar_ManComputeCuts( pAig, 10, 0 );
 p->timeCuts = clock() - clk;
 
     // find the mapping
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 2a4fcaf3..72e7d3d1 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -83,7 +83,7 @@ extern Aig_Man_t *     Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel );
 /*=== darCore.c ========================================================*/
 extern void            Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars );
 extern int             Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars );
-extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax );
+extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose );
 /*=== darRefact.c ========================================================*/
 extern void            Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
 extern int             Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index f4041dd1..141d9b79 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -195,6 +195,34 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
 
 /**Function*************************************************************
 
+  Synopsis    [Computes the total number of cuts.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ManCutCount( Aig_Man_t * pAig, int * pnCutsK )
+{
+    Dar_Cut_t * pCut;
+    Aig_Obj_t * pObj;
+    int i, k, nCuts = 0, nCutsK = 0;
+    Aig_ManForEachNode( pAig, pObj, i )
+        Dar_ObjForEachCut( pObj, pCut, k )
+        {
+            nCuts++;
+            if ( pCut->nLeaves == 4 )
+                nCutsK++;
+        }
+    if ( pnCutsK )
+        *pnCutsK = nCutsK;
+    return nCuts;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -204,13 +232,13 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
   SeeAlso     []
 
 ***********************************************************************/
-Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax )
+Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose )
 {
     Dar_Man_t * p;
     Dar_RwrPar_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Aig_MmFixed_t * pMemCuts;
-    int i, nNodes;
+    int i, nNodes, clk = clock();
     // remove dangling nodes
     if ( (nNodes = Aig_ManCleanup( pAig )) )
     {
@@ -226,6 +254,23 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax )
     // compute cuts for each nodes in the topological order
     Aig_ManForEachNode( pAig, pObj, i )
         Dar_ObjComputeCuts( p, pObj );
+    // print verbose stats
+    if ( fVerbose )
+    {
+//        Aig_Obj_t * pObj;
+        int nCuts, nCutsK;//, i;
+        nCuts = Dar_ManCutCount( pAig, &nCutsK );
+        printf( "Nodes = %6d. Total cuts = %6d. 4-input cuts = %6d.\n",
+            Aig_ManObjNum(pAig), nCuts, nCutsK );
+        printf( "Cut size = %2d. Truth size = %2d. Total mem = %5.2f Mb  ",
+            sizeof(Dar_Cut_t), 4, 1.0*Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20) );
+        PRT( "Runtime", clock() - clk );
+/*
+        Aig_ManForEachNode( pAig, pObj, i )
+            if ( i % 300 == 0 )
+                Dar_ObjCutPrint( pAig, pObj );
+*/
+    }
     // free the cuts
     pMemCuts = p->pMemCuts;
     p->pMemCuts = NULL;
diff --git a/src/aig/dar/darCut.c b/src/aig/dar/darCut.c
index b0aff095..79e4dcc4 100644
--- a/src/aig/dar/darCut.c
+++ b/src/aig/dar/darCut.c
@@ -30,6 +30,47 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_CutPrint( Dar_Cut_t * pCut )
+{
+    unsigned i;
+    printf( "{" );
+    for ( i = 0; i < pCut->nLeaves; i++ )
+        printf( " %d", pCut->pLeaves[i] );
+    printf( " }\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Dar_ObjCutPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    Dar_Cut_t * pCut;
+    int i;
+    printf( "Cuts for node %d:\n", pObj->Id );
+    Dar_ObjForEachCut( pObj, pCut, i )
+        Dar_CutPrint( pCut );
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns the number of 1s in the machine word.]
 
   Description []
diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h
index 4da793f5..afa3bd07 100644
--- a/src/aig/dar/darInt.h
+++ b/src/aig/dar/darInt.h
@@ -134,6 +134,7 @@ extern void            Dar_ManCutsStart( Dar_Man_t * p );
 extern void            Dar_ManCutsFree( Dar_Man_t * p );
 extern Dar_Cut_t *     Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj );
 extern Dar_Cut_t *     Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
+extern void            Dar_ObjCutPrint( Aig_Man_t * p, Aig_Obj_t * pObj );
 /*=== darData.c ===========================================================*/
 extern Vec_Int_t *     Dar_LibReadNodes();
 extern Vec_Int_t *     Dar_LibReadOuts();
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index e3ac9aa3..7e8d7dd1 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -33,6 +33,11 @@ struct Clu_Man_t_
     int              nFrames;        // the K of the K-step induction
     int              nPref;          // the number of timeframes to skip  
     int              nClausesMax;    // the max number of 4-clauses to consider
+    int              nLutSize;       // the max cut size
+    int              nLevels;        // the number of levels for cut computation
+    int              nCutsMax;       // the maximum number of cuts to compute at a node
+    int              nBatches;       // the number of clause batches to use
+    int              fStepUp;        // increase cut size for each batch
     int              fVerbose;       
     int              fVeryVerbose;
     // internal parameters
@@ -40,18 +45,25 @@ struct Clu_Man_t_
     int              nSimWordsPref;  // the number of simulation words in the prefix
     int              nSimFrames;     // the number of frames to simulate 
     int              nBTLimit;       // the largest number of backtracks (0 = infinite)
-    // the network
+    // the network 
     Aig_Man_t *      pAig;
     // SAT solvers
     sat_solver *     pSatMain;
     sat_solver *     pSatBmc;
     // CNF for the test solver
     Cnf_Dat_t *      pCnf;
+    int              fFail;
+    int              fFiltering; 
+    int              fNothingNew;
     // clauses
     Vec_Int_t *      vLits;
     Vec_Int_t *      vClauses;
     Vec_Int_t *      vCosts;
     int              nClauses;
+    // clauses proven
+    Vec_Int_t *      vLitsProven;
+    Vec_Int_t *      vClausesProven;
+    int              nClausesProven;
     // counter-examples
     Vec_Ptr_t *      vCexes;
     int              nCexes;
@@ -184,7 +196,7 @@ void transpose32a( unsigned a[32] )
 int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
 {
     unsigned Matrix[32];
-    unsigned * pSims[4], uWord;
+    unsigned * pSims[16], uWord;
     int nSeries, i, k, j;
     int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
     // compute parameters
@@ -229,7 +241,7 @@ int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
 ***********************************************************************/
 int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
 {
-    unsigned * pSims[4], uWord;
+    unsigned * pSims[16], uWord;
     int iMint, i, k, b;
     int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
     // compute parameters
@@ -258,6 +270,43 @@ int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t *
     return (int)uWord;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Return the number of combinations appearing in the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausProcessClausesCut3( Clu_Man_t * p, Fra_Sml_t * pSimMan, Aig_Cut_t * pCut, int * pScores )
+{
+    unsigned * pSims[16];
+    int iMint, i, k, b, nMints;
+    int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
+    // compute parameters
+    assert( pCut->nFanins > 1 && pCut->nFanins < 17 );
+    assert( nWordsForSim % 8 == 0 );
+    // get parameters
+    for ( i = 0; i < (int)pCut->nFanins; i++ )
+        pSims[i] = Fra_ObjSim( pSimMan, pCut->pFanins[i] ) + p->nSimWordsPref;
+    // add combinational patterns
+    nMints = (1 << pCut->nFanins);
+    memset( pScores, 0, sizeof(int) * nMints );
+    // go through the simulation patterns
+    for ( i = 0; i < nWordsForSim; i++ )
+        for ( k = 0; k < 32; k++ )
+        {
+            iMint = 0;
+            for ( b = 0; b < (int)pCut->nFanins; b++ )
+                if ( pSims[b][i] & (1 << k) )
+                    iMint |= (1 << b);
+            pScores[iMint]++;
+        }
+}
+
 
 /**Function*************************************************************
 
@@ -280,6 +329,8 @@ int Fra_ClausSelectClauses( Clu_Man_t * p )
     memset( pCostCount, 0, sizeof(int) * CostMax );
     Vec_IntForEachEntry( p->vCosts, Cost, i )
     {
+        if ( Cost == -1 )
+            continue;
         assert( Cost < CostMax );
         pCostCount[ Cost ]++;
     }
@@ -334,6 +385,26 @@ void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost
 
 /**Function*************************************************************
 
+  Synopsis    [Processes the clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausRecordClause2( Clu_Man_t * p, Aig_Cut_t * pCut, int iMint, int Cost )
+{
+    int i;
+    for ( i = 0; i < (int)pCut->nFanins; i++ )
+        Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pFanins[i]], (iMint&(1<<i)) ) );
+    Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
+    Vec_IntPush( p->vCosts, Cost );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if simulation info is composed of all zeros.]
 
   Description []
@@ -485,6 +556,7 @@ int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
 int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
 {
     Aig_MmFixed_t * pMemCuts;
+//    Aig_ManCut_t * pManCut;
     Fra_Sml_t * pComb, * pSeq;
     Aig_Obj_t * pObj;
     Dar_Cut_t * pCut;
@@ -519,7 +591,8 @@ PRT( "Lat-cla", clock() - clk );
 
     // generate cuts for all nodes, assign cost, and find best cuts
 clk = clock();
-    pMemCuts = Dar_ManComputeCuts( p->pAig, 10 );
+    pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 1 );
+//    pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 );
 if ( p->fVerbose )
 {
 PRT( "Cuts   ", clock() - clk );
@@ -572,6 +645,7 @@ clk = clock();
             }
     Fra_SmlStop( pComb );
     Aig_MmFixedStop( pMemCuts, 0 );
+//    Aig_ManCutStop( pManCut );
 if ( p->fVerbose )
 {
 PRT( "Infocmb", clock() - clk );
@@ -590,6 +664,174 @@ PRT( "Infocmb", clock() - clk );
 
 /**Function*************************************************************
 
+  Synopsis    [Processes the clauses.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
+{
+//    Aig_MmFixed_t * pMemCuts;
+    Aig_ManCut_t * pManCut;
+    Fra_Sml_t * pComb, * pSeq;
+    Aig_Obj_t * pObj;
+    Aig_Cut_t * pCut;
+    int i, k, j, clk, nCuts = 0;
+    int ScoresSeq[1<<12], ScoresComb[1<<12];
+    assert( p->nLutSize < 13 );
+
+    // simulate the AIG
+clk = clock();
+    srand( 0xAABBAABB );
+    pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
+    if ( pSeq->fNonConstOut )
+    {
+        printf( "Property failed after sequential simulation!\n" );
+        Fra_SmlStop( pSeq );
+        return 0;
+    }
+if ( p->fVerbose )
+{
+PRT( "Sim-seq", clock() - clk );
+}
+
+    // perform combinational simulation
+clk = clock();
+    srand( 0xAABBAABB );
+    pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref  );
+if ( p->fVerbose )
+{
+PRT( "Sim-cmb", clock() - clk );
+}
+
+
+clk = clock();
+    if ( fRefs )
+    {
+    Fra_ClausCollectLatchClauses( p, pSeq );
+if ( p->fVerbose )
+{
+PRT( "Lat-cla", clock() - clk );
+}
+    }
+
+
+    // generate cuts for all nodes, assign cost, and find best cuts
+clk = clock();
+//    pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 1 );
+    pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose );
+if ( p->fVerbose )
+{
+PRT( "Cuts   ", clock() - clk );
+}
+
+    // collect combinational info for each cut
+clk = clock();
+    Aig_ManForEachNode( p->pAig, pObj, i )
+    {
+        if ( pObj->Level > (unsigned)p->nLevels )
+            continue;
+        Aig_ObjForEachCut( pManCut, pObj, pCut, k )
+            if ( pCut->nFanins > 1 )
+            {
+                nCuts++;
+                Fra_ClausProcessClausesCut3( p, pSeq, pCut, ScoresSeq );
+                Fra_ClausProcessClausesCut3( p, pComb, pCut, ScoresComb );
+                // write the clauses
+                for ( j = 0; j < (1<<pCut->nFanins); j++ )
+                    if ( ScoresComb[j] != 0 && ScoresSeq[j] == 0 )
+                        Fra_ClausRecordClause2( p, pCut, j, ScoresComb[j] );
+
+            }
+    }
+    Fra_SmlStop( pSeq );
+    Fra_SmlStop( pComb );
+//    Aig_MmFixedStop( pMemCuts, 0 );
+    Aig_ManCutStop( pManCut );
+    p->pAig->pManCuts = NULL;
+if ( p->fVerbose )
+{
+PRT( "Infosim", clock() - clk );
+}
+
+    if ( p->fVerbose )
+    printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n", 
+        Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
+
+    // filter out clauses that are contained in the already proven clauses
+    assert( p->nClauses == 0 );
+    p->nClauses = Vec_IntSize( p->vClauses );
+    if ( Vec_IntSize( p->vClausesProven ) > 0 )
+    {
+        int RetValue, k, Beg, End, * pStart;
+        // reset the solver
+        if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
+        p->pSatMain = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
+        if ( p->pSatMain == NULL )
+        {
+            printf( "Error: Main solver is unsat.\n" );
+            return -1;
+        }  
+
+        // add the proven clauses
+        Beg = 0;
+        pStart = Vec_IntArray(p->vLitsProven);
+        Vec_IntForEachEntry( p->vClausesProven, End, i )
+        {
+            assert( End - Beg <= p->nLutSize );
+            // add the clause to all timeframes
+            RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
+            if ( RetValue == 0 )
+            {
+                printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
+                return -1;
+            }
+            Beg = End;
+        }
+        assert( End == Vec_IntSize(p->vLitsProven) );
+
+        // check the clauses
+        Beg = 0;
+        pStart = Vec_IntArray(p->vLits);
+        Vec_IntForEachEntry( p->vClauses, End, i )
+        {
+            assert( Vec_IntEntry( p->vCosts, i ) >= 0 );
+            assert( End - Beg <= p->nLutSize );
+            // check the clause
+            for ( k = Beg; k < End; k++ )
+                pStart[k] = lit_neg( pStart[k] );
+            RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (sint64)p->nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            for ( k = Beg; k < End; k++ )
+                pStart[k] = lit_neg( pStart[k] );
+            // the clause holds
+            if ( RetValue == l_False )
+            {
+                Vec_IntWriteEntry( p->vCosts, i, -1 );
+                p->nClauses--;
+            }
+            Beg = End;
+        }
+        assert( End == Vec_IntSize(p->vLits) );
+        if ( p->fVerbose )
+        printf( "Already proved clauses filtered out %d candidate clauses (out of %d).\n", 
+            Vec_IntSize(p->vClauses) - p->nClauses, Vec_IntSize(p->vClauses) );
+    }
+
+    p->fFiltering = 0;
+    if ( p->nClauses > p->nClausesMax )
+    {
+        Fra_ClausSelectClauses( p );
+        p->fFiltering = 1;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Converts AIG into the SAT solver.]
 
   Description []
@@ -630,7 +872,7 @@ int Fra_ClausBmcClauses( Clu_Man_t * p )
                 continue;
             }
             assert( Vec_IntEntry( p->vCosts, i ) > 0 );
-            assert( End - Beg < 5 );
+            assert( End - Beg <= p->nLutSize );
 
             for ( k = Beg; k < End; k++ )
                 pStart[k] = lit_neg( pStart[k] );
@@ -760,7 +1002,7 @@ void Fra_ClausSimInfoRecord( Clu_Man_t * p, int * pModel )
 ***********************************************************************/
 int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits )
 {
-    unsigned * pSims[4], uWord;
+    unsigned * pSims[16], uWord;
     int nWords, iVar, i, w;
     for ( i = 0; i < nLits; i++ )
     {
@@ -803,7 +1045,8 @@ int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits )
 int Fra_ClausInductiveClauses( Clu_Man_t * p )
 {
 //    Aig_Obj_t * pObjLi, * pObjLo;
-    int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFail = 0, fFlag;//, Lits[2];
+    int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFlag;//, Lits[2];
+    p->fFail = 0;
 
     // reset the solver
     if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
@@ -839,6 +1082,54 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
             }
         }
 */
+
+
+    // add the proven clauses
+    nLitsTot = 2 * p->pCnf->nVars;
+    pStart = Vec_IntArray(p->vLitsProven);
+    for ( f = 0; f < p->nFrames; f++ )
+    {
+        Beg = 0;
+        Vec_IntForEachEntry( p->vClausesProven, End, i )
+        {
+            assert( End - Beg <= p->nLutSize );
+            // add the clause to all timeframes
+            RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
+            if ( RetValue == 0 )
+            {
+                printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
+                return -1;
+            }
+            Beg = End;
+        }
+        // increment literals
+        for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
+            p->vLitsProven->pArray[i] += nLitsTot;
+    }
+    // return clauses back to normal
+    nLitsTot = (p->nFrames) * nLitsTot;
+    for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
+        p->vLitsProven->pArray[i] -= nLitsTot;
+
+/*
+    // add the proven clauses
+    nLitsTot = 2 * p->pCnf->nVars;
+    pStart = Vec_IntArray(p->vLitsProven);
+    Beg = 0;
+    Vec_IntForEachEntry( p->vClausesProven, End, i )
+    {
+        assert( End - Beg <= p->nLutSize );
+        // add the clause to all timeframes
+        RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
+        if ( RetValue == 0 )
+        {
+            printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
+            return -1;
+        }
+        Beg = End;
+    }
+*/
+    
     // add the clauses
     nLitsTot = 2 * p->pCnf->nVars;
     pStart = Vec_IntArray(p->vLits);
@@ -853,7 +1144,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
                 continue;
             }
             assert( Vec_IntEntry( p->vCosts, i ) > 0 );
-            assert( End - Beg < 5 );
+            assert( End - Beg <= p->nLutSize );
             // add the clause to all timeframes
             RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
             if ( RetValue == 0 )
@@ -887,7 +1178,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
         if ( p->fVerbose )
         printf( " Property fails.  " );
 //        return -2;
-        fFail = 1;
+        p->fFail = 1;
     }
 
 /*
@@ -930,7 +1221,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
             continue;
         }
         assert( Vec_IntEntry( p->vCosts, i ) > 0 );
-        assert( End - Beg < 5 );
+        assert( End - Beg <= p->nLutSize );
 
         if ( Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg) )
         {
@@ -996,8 +1287,8 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
     for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
         p->vLits->pArray[i] -= nLitsTot;
 
-    if ( fFail )
-        return -2;
+//    if ( fFail )
+//        return -2;
     return Counter;
 }
 
@@ -1014,7 +1305,7 @@ int Fra_ClausInductiveClauses( Clu_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int fVerbose, int fVeryVerbose )
+Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fVerbose, int fVeryVerbose )
 {
     Clu_Man_t * p;
     p = ALLOC( Clu_Man_t, 1 );
@@ -1023,6 +1314,11 @@ Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClaus
     p->nFrames       = nFrames;
     p->nPref         = nPref;
     p->nClausesMax   = nClausesMax;
+    p->nLutSize      = nLutSize;
+    p->nLevels       = nLevels;
+    p->nCutsMax      = nCutsMax;
+    p->nBatches      = nBatches;
+    p->fStepUp       = fStepUp;
     p->fVerbose      = fVerbose;
     p->fVeryVerbose  = fVeryVerbose;
     p->nSimWords     = 512;//1024;//64;
@@ -1033,6 +1329,9 @@ Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClaus
     p->vClauses      = Vec_IntAlloc( 1<<12 );
     p->vCosts        = Vec_IntAlloc( 1<<12 );
 
+    p->vLitsProven   = Vec_IntAlloc( 1<<14 );
+    p->vClausesProven= Vec_IntAlloc( 1<<12 );
+
     p->nCexesAlloc   = 1024;
     p->vCexes        = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig)+1, p->nCexesAlloc/32 );
     Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
@@ -1055,6 +1354,8 @@ void Fra_ClausFree( Clu_Man_t * p )
     if ( p->vCexes )    Vec_PtrFree( p->vCexes );
     if ( p->vLits )     Vec_IntFree( p->vLits );
     if ( p->vClauses )  Vec_IntFree( p->vClauses );
+    if ( p->vLitsProven )     Vec_IntFree( p->vLitsProven );
+    if ( p->vClausesProven )  Vec_IntFree( p->vClausesProven );
     if ( p->vCosts )    Vec_IntFree( p->vCosts );
     if ( p->pCnf )      Cnf_DataFree( p->pCnf );
     if ( p->pSatMain )  sat_solver_delete( p->pSatMain );
@@ -1062,6 +1363,51 @@ void Fra_ClausFree( Clu_Man_t * p )
     free( p );
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Converts AIG into the SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClausAddToStorage( Clu_Man_t * p )
+{
+    int * pStart; 
+    int Beg, End, Counter, i, k;
+    Beg = 0;
+    Counter = 0;
+    pStart = Vec_IntArray( p->vLits );
+    Vec_IntForEachEntry( p->vClauses, End, i )
+    {
+        if ( Vec_IntEntry( p->vCosts, i ) == -1 )
+        {
+            Beg = End;
+            continue;
+        }
+        assert( Vec_IntEntry( p->vCosts, i ) > 0 );
+        assert( End - Beg <= p->nLutSize );
+        for ( k = Beg; k < End; k++ )
+            Vec_IntPush( p->vLitsProven, pStart[k] );
+        Vec_IntPush( p->vClausesProven, Vec_IntSize(p->vLitsProven) );
+        Beg = End;
+        Counter++;
+    }
+    if ( p->fVerbose )
+    printf( "Added to storage %d proved clauses\n", Counter );
+
+    Vec_IntClear( p->vClauses );
+    Vec_IntClear( p->vLits );
+    Vec_IntClear( p->vCosts );
+    p->nClauses = 0;
+
+    p->fNothingNew = (int)(Counter == 0);
+}
+
 /**Function*************************************************************
 
   Synopsis    [Converts AIG into the SAT solver.]
@@ -1073,16 +1419,16 @@ void Fra_ClausFree( Clu_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
+int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fVerbose, int fVeryVerbose )
 {
     Clu_Man_t * p;
     int clk, clkTotal = clock();
-    int Iter, Counter, nPrefOld;
+    int b, Iter, Counter, nPrefOld;
 
     assert( Aig_ManPoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
 
     // create the manager
-    p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, fVerbose, fVeryVerbose );
+    p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fVerbose, fVeryVerbose );
 
 clk = clock();
     // derive CNF
@@ -1123,67 +1469,85 @@ clk = clock();
         Fra_ClausFree( p );
         return 1;
     } 
-    // try solving without additional clauses
-    if ( Fra_ClausRunSat( p ) )
+
+
+    for ( b = 0; b < p->nBatches; b++ )
     {
-        printf( "Problem is inductive without strengthening.\n" );
-        Fra_ClausFree( p );
-        return 1;
-    }
-if ( fVerbose )
-{
-PRT( "SAT-ind", clock() - clk );
-}
+//        if ( fVerbose )
+        printf( "*** BATCH %d:  ", b+1 );
+        if ( b && (!p->fFiltering || p->fNothingNew || p->fStepUp) )
+            p->nLutSize++;
+        printf( "Using %d-cuts.\n", p->nLutSize );
+
+        // try solving without additional clauses
+        if ( Fra_ClausRunSat( p ) )
+        {
+            printf( "Problem is inductive without strengthening.\n" );
+            Fra_ClausFree( p );
+            return 1;
+        }
+        if ( fVerbose )
+        {
+        PRT( "SAT-ind", clock() - clk );
+        }
  
-    // collect the candidate inductive clauses using 4-cuts
-clk = clock();
-    nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
-    Fra_ClausProcessClauses( p, fRefs );
-    p->nPref = nPrefOld;
-    p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
+        // collect the candidate inductive clauses using 4-cuts
+        clk = clock();
+        nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
+    //    Fra_ClausProcessClauses( p, fRefs );
+        Fra_ClausProcessClauses2( p, fRefs );
+        p->nPref = nPrefOld;
+        p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
 
-//PRT( "Clauses", clock() - clk );
+    //PRT( "Clauses", clock() - clk );
 
 
-    // check clauses using BMC
-    if ( fBmc ) 
-    {
-clk = clock();
-        Counter = Fra_ClausBmcClauses( p );
-        p->nClauses -= Counter;
-if ( fVerbose )
-{
-        printf( "BMC disproved %d clauses.\n", Counter );
-PRT( "Cla-bmc", clock() - clk );
-}
-    }
+        // check clauses using BMC
+        if ( fBmc ) 
+        {
+            clk = clock();
+            Counter = Fra_ClausBmcClauses( p );
+            p->nClauses -= Counter;
+            if ( fVerbose )
+            {
+                printf( "BMC disproved %d clauses.\n", Counter );
+                PRT( "Cla-bmc", clock() - clk );
+            }
+        }
 
 
-    // prove clauses inductively
-clk = clock();
-    Counter = 1;
-    for ( Iter = 0; Counter > 0; Iter++ )
-    {
-        if ( fVerbose )
-        printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
-        Counter = Fra_ClausInductiveClauses( p );
-        if ( Counter > 0 )
-           p->nClauses -= Counter;
-        if ( fVerbose )
+        // prove clauses inductively
+        clk = clock();
+        Counter = 1;
+        for ( Iter = 0; Counter > 0; Iter++ )
         {
-        printf( "End = %5d. Exs = %5d.  ", p->nClauses, p->nCexes );
-//        printf( "\n" );
-        PRT( "Time", clock() - clk );
+            if ( fVerbose )
+            printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
+            Counter = Fra_ClausInductiveClauses( p );
+            if ( Counter > 0 )
+               p->nClauses -= Counter;
+            if ( fVerbose )
+            {
+            printf( "End = %5d. Exs = %5d.  ", p->nClauses, p->nCexes );
+    //        printf( "\n" );
+            PRT( "Time", clock() - clk );
+            }
+            clk = clock();
         }
-        clk = clock();
+        if ( Counter == -1 )
+            printf( "Fra_Claus(): Internal error.  " );
+        else if ( p->fFail )
+            printf( "Property FAILS during refinement.  " );
+        else
+            printf( "Property HOLDS inductively after strengthening.  " );
+        PRT( "Time  ", clock() - clkTotal );
+
+        if ( !p->fFail )
+            break;
+
+        // add proved clauses to storage
+        Fra_ClausAddToStorage( p );
     }
-    if ( Counter == -1 )
-        printf( "Fra_Claus(): Internal error.  " );
-    else if ( Counter == -2 )
-        printf( "Property FAILS during refinement.  " );
-    else
-        printf( "Property HOLDS inductively after strengthening.  " );
-    PRT( "Time  ", clock() - clkTotal );
 
     // clean the manager
     Fra_ClausFree( p );
author	Alan Mishchenko <alanmi@berkeley.edu>	2008-01-26 08:01:00 -0800
committer	Alan Mishchenko <alanmi@berkeley.edu>	2008-01-26 08:01:00 -0800
commit	6537f941887b06e588d3acfc97b5fdf48875cc4e (patch)
tree	61e11fbdd1bbcb781cf05f91f5095f559a58ab25 /src/aig
parent	6c68b76bff33daa7cd94b78c51bdd4cdaf65059c (diff)
download	abc-6537f941887b06e588d3acfc97b5fdf48875cc4e.tar.gz abc-6537f941887b06e588d3acfc97b5fdf48875cc4e.tar.bz2 abc-6537f941887b06e588d3acfc97b5fdf48875cc4e.zip