Version abc80313

src/aig/aig/aigInter.c

@@ -45,6 +45,104 @@ extern int timeInt;
   SeeAlso     []
 
 ***********************************************************************/
+void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
+{
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnfOn, * pCnfOff;
+    Aig_Obj_t * pObj, * pObj2;
+    int Lits[3], status, i;
+    int clk = clock();
+
+    assert( Aig_ManPiNum(pManOn) == Aig_ManPiNum(pManOff) );
+    assert( Aig_ManPoNum(pManOn) == Aig_ManPoNum(pManOff) );
+
+    // derive CNFs
+    pManOn->nRegs = Aig_ManPoNum(pManOn);
+    pCnfOn  = Cnf_Derive( pManOn, Aig_ManPoNum(pManOn) );
+    pManOn->nRegs = 0;
+
+    pManOff->nRegs = Aig_ManPoNum(pManOn);
+    pCnfOff = Cnf_Derive( pManOff, Aig_ManPoNum(pManOff) );
+    pManOff->nRegs = 0;
+
+//    pCnfOn  = Cnf_DeriveSimple( pManOn, Aig_ManPoNum(pManOn) );
+//    pCnfOff = Cnf_DeriveSimple( pManOff, Aig_ManPoNum(pManOn) );
+    Cnf_DataLift( pCnfOff, pCnfOn->nVars );
+
+    // start the solver
+    pSat = sat_solver_new();
+    sat_solver_setnvars( pSat, pCnfOn->nVars + pCnfOff->nVars );
+
+    // add clauses of A
+    for ( i = 0; i < pCnfOn->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfOn->pClauses[i], pCnfOn->pClauses[i+1] ) )
+        {
+            Cnf_DataFree( pCnfOn );
+            Cnf_DataFree( pCnfOff );
+            sat_solver_delete( pSat );
+            return;
+        }
+    }
+
+    // add clauses of B
+    for ( i = 0; i < pCnfOff->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfOff->pClauses[i], pCnfOff->pClauses[i+1] ) )
+        {
+            Cnf_DataFree( pCnfOn );
+            Cnf_DataFree( pCnfOff );
+            sat_solver_delete( pSat );
+            return;
+        }
+    }
+
+    // add PI clauses
+    // collect the common variables
+    Aig_ManForEachPi( pManOn, pObj, i )
+    {
+        pObj2 = Aig_ManPi( pManOff, i );
+
+        Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 1 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 0 );
+        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    status = sat_solver_simplify( pSat );
+    assert( status != 0 );
+
+    // solve incremental SAT problems
+    Aig_ManForEachPo( pManOn, pObj, i )
+    {
+        pObj2 = Aig_ManPo( pManOff, i );
+
+        Lits[0] = toLitCond( pCnfOn->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfOff->pVarNums[pObj2->Id], 0 );
+        status = sat_solver_solve( pSat, Lits, Lits+2, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+        if ( status != l_False )
+            printf( "The incremental SAT problem is not UNSAT.\n" );
+    }
+    Cnf_DataFree( pCnfOn );
+    Cnf_DataFree( pCnfOff );
+    sat_solver_delete( pSat );
+//    PRT( "Fast interpolation time", clock() - clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose )
 {
     void * pSatCnf = NULL;
@@ -56,6 +154,7 @@ Aig_Man_t * Aig_ManInter( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose
     Aig_Obj_t * pObj, * pObj2;
     int Lits[3], status, i;
     int clk;
+    int iLast;
 
     assert( Aig_ManPiNum(pManOn) == Aig_ManPiNum(pManOff) );
 
@@ -87,6 +186,12 @@ clk = clock();
     }
     sat_solver_store_mark_clauses_a( pSat );
 
+    // update the last clause
+    {
+        extern int sat_solver_store_change_last( sat_solver * pSat );
+//        iLast = sat_solver_store_change_last( pSat );
+    }
+
     // add clauses of B
     for ( i = 0; i < pCnfOff->nClauses; i++ )
     {
@@ -102,6 +207,8 @@ clk = clock();
     // add PI clauses
     // collect the common variables
     vVarsAB = Vec_IntAlloc( Aig_ManPiNum(pManOn) );
+//    Vec_IntPush( vVarsAB, iLast );
+
     Aig_ManForEachPi( pManOn, pObj, i )
     {
         Vec_IntPush( vVarsAB, pCnfOn->pVarNums[pObj->Id] );
@@ -175,6 +282,8 @@ timeInt += clock() - clk;
 */
     Vec_IntFree( vVarsAB );
     Sto_ManFree( pSatCnf );
+
+//    Ioa_WriteAiger( pRes, "inter2.aig", 0, 0 );
     return pRes;
 }
 

src/aig/bdc/bdc.h

@@ -58,7 +58,7 @@ struct Bdc_Par_t_
 /*=== bdcCore.c ==========================================================*/
 extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
 extern void        Bdc_ManFree( Bdc_Man_t * p );
-extern int         Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesLimit );
+extern int         Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax );
 
 
 #ifdef __cplusplus

src/aig/bdc/bdcCore.c

@@ -42,15 +42,12 @@
 Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
 {
     Bdc_Man_t * p;
-    unsigned * pData;
-    int i, k, nBits;
     p = ALLOC( Bdc_Man_t, 1 );
     memset( p, 0, sizeof(Bdc_Man_t) );
     assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 );
     p->pPars = pPars;
     p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
     p->nDivsLimit = 200;
-    p->nNodesLimit = 0; // will be set later
     // memory
     p->vMemory = Vec_IntStart( 1 << 16 );
     // internal nodes
@@ -62,22 +59,11 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
     memset( p->pTable, 0, sizeof(Bdc_Fun_t *) * p->nTableSize );
     p->vSpots = Vec_IntAlloc( 256 );
     // truth tables
-    p->vTruths = Vec_PtrAllocSimInfo( pPars->nVarsMax + 5, p->nWords );
-    // set elementary truth tables
-    nBits = (1 << pPars->nVarsMax);
-    Kit_TruthFill( Vec_PtrEntry(p->vTruths, 0), p->nVars );
-    for ( k = 0; k < pPars->nVarsMax; k++ )
-    {
-        pData = Vec_PtrEntry( p->vTruths, k+1 );
-        Kit_TruthClear( pData, p->nVars );
-        for ( i = 0; i < nBits; i++ )
-            if ( i & (1 << k) )
-                pData[i>>5] |= (1 << (i&31));
-    }
-    p->puTemp1 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 1 );
-    p->puTemp2 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 2 );
-    p->puTemp3 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 3 );
-    p->puTemp4 = Vec_PtrEntry( p->vTruths, pPars->nVarsMax + 4 );
+    p->vTruths = Vec_PtrAllocTruthTables( p->pPars->nVarsMax );
+    p->puTemp1 = ALLOC( unsigned, 4 * p->nWords );
+    p->puTemp2 = p->puTemp1 + p->nWords;
+    p->puTemp3 = p->puTemp2 + p->nWords;
+    p->puTemp4 = p->puTemp3 + p->nWords;
     // start the internal ISFs
     p->pIsfOL = &p->IsfOL;  Bdc_IsfStart( p, p->pIsfOL );
     p->pIsfOR = &p->IsfOR;  Bdc_IsfStart( p, p->pIsfOR );
@@ -102,6 +88,7 @@ void Bdc_ManFree( Bdc_Man_t * p )
     Vec_IntFree( p->vMemory );
     Vec_IntFree( p->vSpots );
     Vec_PtrFree( p->vTruths );
+    free( p->puTemp1 );
     free( p->pNodes );
     free( p->pTable );
     free( p );
@@ -126,16 +113,25 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
     Bdc_TableClear( p );
     Vec_IntClear( p->vMemory );
     // add constant 1 and elementary vars
-    p->nNodes = p->nNodesNew = 0;
-    for ( i = 0; i <= p->pPars->nVarsMax; i++ )
+    p->nNodes = 0;
+    p->nNodesNew = - 1 - p->nVars - (vDivs? Vec_PtrSize(vDivs) : 0);
+    // add constant 1
+    pNode = Bdc_FunNew( p );
+    pNode->Type = BDC_TYPE_CONST1;
+    pNode->puFunc = NULL;
+    pNode->uSupp = 0;
+    Bdc_TableAdd( p, pNode );
+    // add variables
+    for ( i = 0; i < p->nVars; i++ )
     {
         pNode = Bdc_FunNew( p );
         pNode->Type = BDC_TYPE_PI;
         pNode->puFunc = Vec_PtrEntry( p->vTruths, i );
-        pNode->uSupp = i? (1 << (i-1)) : 0;
+        pNode->uSupp = (1 << i);
         Bdc_TableAdd( p, pNode );
     }
     // add the divisors
+    if ( vDivs )
     Vec_PtrForEachEntry( vDivs, puTruth, i )
     {
         pNode = Bdc_FunNew( p );
@@ -146,6 +142,40 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
         if ( i == p->nDivsLimit )
             break;
     }
+    assert( p->nNodesNew == 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Clears the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_ManDecPrint( Bdc_Man_t * p )
+{
+    Bdc_Fun_t * pNode;
+    int i;
+    printf( " 0 : Const 1\n" );
+    for ( i = 1; i < p->nNodes; i++ )
+    {
+        printf( " %d : ", i );
+        pNode = p->pNodes + i;
+        if ( pNode->Type == BDC_TYPE_PI )
+            printf( "PI   " );
+        else
+        {
+            printf( "%s%d &", Bdc_IsComplement(pNode->pFan0)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) );
+            printf( " %s%d   ", Bdc_IsComplement(pNode->pFan1)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) );
+        }
+        Extra_PrintBinary( stdout, pNode->puFunc, (1<<p->nVars) );
+        printf( "\n" );
+    }
+    printf( "Root = %s%d.\n", Bdc_IsComplement(p->pRoot)? "-":"", Bdc_FunId(p,Bdc_Regular(p->pRoot)) );
 }
 
 /**Function*************************************************************
@@ -162,25 +192,67 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
 int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax )
 {
     Bdc_Isf_t Isf, * pIsf = &Isf;
+    assert( nVars <= p->pPars->nVarsMax );
     // set current manager parameters
     p->nVars = nVars;
     p->nWords = Kit_TruthWordNum( nVars );
+    p->nNodesMax = nNodesMax;
     Bdc_ManPrepare( p, vDivs );
-    p->nNodesLimit = (p->nNodes + nNodesMax < p->nNodesAlloc)? p->nNodes + nNodesMax : p->nNodesAlloc;
     // copy the function
     Bdc_IsfStart( p, pIsf );
-    Bdc_IsfClean( pIsf );
-    pIsf->uSupp = Kit_TruthSupport( puFunc, p->nVars ) | Kit_TruthSupport( puCare, p->nVars );
+    if ( puCare )
+    {
         Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars );
         Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars );
-    // call decomposition
+    }
+    else
+    {
+        Kit_TruthCopy( pIsf->puOn, puFunc, p->nVars );
+        Kit_TruthNot( pIsf->puOff, puFunc, p->nVars );
+    }
     Bdc_SuppMinimize( p, pIsf );
+    // call decomposition
     p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
     if ( p->pRoot == NULL )
         return -1;
     return p->nNodesNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_ManDecomposeTest( unsigned uTruth, int nVars )
+{
+    static int Counter = 0;
+    static int Total = 0;
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    Bdc_Man_t * p;
+    int RetValue;
+//    unsigned uCare = ~0x888f888f;
+    unsigned uCare = ~0;
+//    unsigned uFunc =  0x88888888;
+//    unsigned uFunc =  0xf888f888;
+//    unsigned uFunc =  0x117e117e;
+//    unsigned uFunc =  0x018b018b;
+    unsigned uFunc = uTruth; 
+
+    pPars->nVarsMax = 8;
+    p = Bdc_ManAlloc( pPars );
+    RetValue = Bdc_ManDecompose( p, &uFunc, &uCare, nVars, NULL, 1000 );
+    Total += RetValue;
+    printf( "%5d : Nodes = %5d. Total = %8d.\n", ++Counter, RetValue, Total );
+//    Bdc_ManDecPrint( p );
+    Bdc_ManFree( p );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///

src/aig/bdc/bdcDec.c

@@ -24,75 +24,12 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR );
-static int        Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, unsigned * puTruth, Bdc_Type_t Type );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Performs one step of bi-decomposition.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
-{
-    Bdc_Fun_t * pFunc;
-    Bdc_Isf_t IsfL, * pIsfL = &IsfL;
-    Bdc_Isf_t IsfB, * pIsfR = &IsfB;
-    // check computed results
-    if ( pFunc = Bdc_TableLookup( p, pIsf ) )
-        return pFunc;
-    // decide on the decomposition type
-    pFunc = Bdc_FunNew( p );
-    if ( pFunc == NULL )
-        return NULL;
-    pFunc->Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
-    // decompose the left branch
-    pFunc->pFan0 = Bdc_ManDecompose_rec( p, pIsfL );
-    if ( pFunc->pFan0 == NULL )
-        return NULL;
-    // decompose the right branch
-    if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc->pFan0->puFunc, pFunc->Type ) )
-    {
-        p->nNodes--;
-        return pFunc->pFan0;
-    }
-    pFunc->pFan1 = Bdc_ManDecompose_rec( p, pIsfL );
-    if ( pFunc->pFan1 == NULL )
-        return NULL;
-    // compute the function of node
-    pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); 
-    if ( pFunc->Type == BDC_TYPE_AND )
-        Kit_TruthAnd( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars );
-    else if ( pFunc->Type == BDC_TYPE_OR )
-        Kit_TruthOr( pFunc->puFunc, pFunc->pFan0->puFunc, pFunc->pFan1->puFunc, p->nVars );
-    else 
-        assert( 0 );
-    // verify correctness
-    assert( Bdc_TableCheckContainment(p, pIsf, pFunc->puFunc) );
-    // convert from OR to AND
-    if ( pFunc->Type == BDC_TYPE_OR )
-    {
-        pFunc->Type = BDC_TYPE_AND;
-        pFunc->pFan0 = Bdc_Not(pFunc->pFan0);
-        pFunc->pFan1 = Bdc_Not(pFunc->pFan1);
-        Kit_TruthNot( pFunc->puFunc, pFunc->puFunc, p->nVars );
-        pFunc = Bdc_Not(pFunc);
-    }
-    Bdc_TableAdd( p, Bdc_Regular(pFunc) );
-    return pFunc;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Updates the ISF of the right after the left was decompoosed.]
 
   Description []
@@ -102,8 +39,15 @@ Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
   SeeAlso     []
 
 ***********************************************************************/
-int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, unsigned * puTruth, Bdc_Type_t Type )
+int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR, Bdc_Fun_t * pFunc0, Bdc_Type_t Type )
 {
+    unsigned * puTruth = p->puTemp1;
+    // get the truth table of the left branch
+    if ( Bdc_IsComplement(pFunc0) )
+        Kit_TruthNot( puTruth, Bdc_Regular(pFunc0)->puFunc, p->nVars );
+    else
+        Kit_TruthCopy( puTruth, pFunc0->puFunc, p->nVars );
+    // split into parts
     if ( Type == BDC_TYPE_OR ) 
     {
 //        Right.Q = bdd_appex( Q, CompSpecLeftF, bddop_diff, setRightRes );
@@ -118,8 +62,9 @@ int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
 //        return (int)( pR->Q == b0 );
 
         Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
-        Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp ); 
-        Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp ); 
+        Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uUniq ); 
+        Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uUniq ); 
+//        assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
         assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
         return Kit_TruthIsConst0(pIsfR->puOn, p->nVars);
     }
@@ -136,11 +81,12 @@ int Bdc_DecomposeUpdateRight( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
 //        assert( pR->Q != b0 );
 //        return (int)( pR->R == b0 );
 
-        Kit_TruthSharp( pIsfR->puOn, pIsf->puOn, puTruth, p->nVars );
-        Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp ); 
-        Kit_TruthExistSet( pIsfR->puOff, pIsf->puOff, p->nVars, pIsfL->uSupp ); 
-        assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
-        return Kit_TruthIsConst0(pIsfR->puOn, p->nVars);
+        Kit_TruthAnd( pIsfR->puOff, pIsf->puOff, puTruth, p->nVars );
+        Kit_TruthExistSet( pIsfR->puOff, pIsfR->puOff, p->nVars, pIsfL->uUniq ); 
+        Kit_TruthExistSet( pIsfR->puOn, pIsf->puOn, p->nVars, pIsfL->uUniq ); 
+//        assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
+        assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) );
+        return Kit_TruthIsConst0(pIsfR->puOff, p->nVars);
     }
     return 0;
 }
@@ -201,10 +147,8 @@ int Bdc_DecomposeFindInitialVarSet( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t *
             Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pVars[End] ); 
             if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp1, p->puTemp2, p->nVars) )
             {
-                pIsfL->uSupp = (1 << Beg);
-                pIsfR->uSupp = (1 << End);
-                pIsfL->Var = Beg;
-                pIsfR->Var = End;
+                pIsfL->uUniq = (1 << pVars[Beg]);
+                pIsfR->uUniq = (1 << pVars[End]);
                 return 1;
             }
         }
@@ -229,15 +173,17 @@ int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc
 
     for ( v = 0; v < p->nVars; v++ )
     {
-        Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v );
+        if ( (pIsf->uSupp & (1 << v)) == 0 )
+            continue;
 //        if ( (Q & !bdd_exist( R, VarSetXa )) != bddfalse )
 //        Exist = Cudd_bddExistAbstract( dd, pF->R, Var );   Cudd_Ref( Exist );
 //        if ( Cudd_bddIteConstant( dd, pF->Q, Cudd_Not(Exist), b0 ) != b0 )
+
+        Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, v );
         if ( !Kit_TruthIsImply( pIsf->puOn, p->puTemp1, p->nVars ) )
         {
             // measure the cost of this variable
 //            VarCost = bdd_satcountset( bdd_forall( Q, VarSetXa ), VarCube );
-
 //            Univ = Cudd_bddUnivAbstract( dd, pF->Q, Var );   Cudd_Ref( Univ );
 //            VarCost = Kit_TruthCountOnes( Univ, p->nVars );
 //            Cudd_RecursiveDeref( dd, Univ );
@@ -258,7 +204,6 @@ int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc
     if ( VarCostBest )
     {
 //        funQLeftRes = Q & bdd_exist( R, setRightORweak );
-
 //        Temp = Cudd_bddExistAbstract( dd, pF->R, VarBest );     Cudd_Ref( Temp );
 //        pL->Q = Cudd_bddAnd( dd, pF->Q, Temp );                    Cudd_Ref( pL->Q );
 //        Cudd_RecursiveDeref( dd, Temp );
@@ -269,11 +214,13 @@ int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc
 //        pL->R = pF->R;                                            Cudd_Ref( pL->R );
 //        pL->V = VarBest;                                        Cudd_Ref( pL->V );
         Kit_TruthCopy( pIsfL->puOff, pIsf->puOff, p->nVars );
-        pIsfL->Var = VarBest;
+        pIsfL->uUniq = (1 << VarBest);
+        pIsfR->uUniq = 0;
 
 //        assert( pL->Q != b0 );
 //        assert( pL->R != b0 );
 //        assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
+//        assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
 
         // express cost in percents of the covered boolean space
         Cost = VarCostBest * BDC_SCALE / (1<<p->nVars);
@@ -297,23 +244,25 @@ int Bdc_DecomposeWeakOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc
 ***********************************************************************/
 int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
 {
-    unsigned uSuppRem;
+    unsigned uSupportRem;
     int v, nLeftVars = 1, nRightVars = 1; 
     // clean the var sets
-    Bdc_IsfClean( pIsfL );
-    Bdc_IsfClean( pIsfR );
+    Bdc_IsfStart( p, pIsfL );
+    Bdc_IsfStart( p, pIsfR );
+    // check that the support is correct
+    assert( Kit_TruthSupport(pIsf->puOn, p->nVars) == Kit_TruthSupport(pIsf->puOff, p->nVars) );
+    assert( pIsf->uSupp == Kit_TruthSupport(pIsf->puOn, p->nVars) );
     // find initial variable sets
     if ( !Bdc_DecomposeFindInitialVarSet( p, pIsf, pIsfL, pIsfR ) )
         return Bdc_DecomposeWeakOr( p, pIsf, pIsfL, pIsfR );
     // prequantify the variables in the offset
-    Kit_TruthExistNew( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->Var ); 
-    Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->Var );
+    Kit_TruthExistSet( p->puTemp1, pIsf->puOff, p->nVars, pIsfL->uUniq ); 
+    Kit_TruthExistSet( p->puTemp2, pIsf->puOff, p->nVars, pIsfR->uUniq );
     // go through the remaining variables
-    uSuppRem = pIsf->uSupp & ~pIsfL->uSupp & ~pIsfR->uSupp;
-    assert( Kit_WordCountOnes(uSuppRem) > 0 );
+    uSupportRem = pIsf->uSupp & ~pIsfL->uUniq & ~pIsfR->uUniq;
     for ( v = 0; v < p->nVars; v++ )
     {
-        if ( (uSuppRem & (1 << v)) == 0 )
+        if ( (uSupportRem & (1 << v)) == 0 )
             continue;
         // prequantify this variable
         Kit_TruthExistNew( p->puTemp3, p->puTemp1, p->nVars, v );
@@ -325,15 +274,17 @@ int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf
             if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
             {
 //                pL->V &= VarNew;
-                pIsfL->uSupp |= (1 << v);
+                pIsfL->uUniq |= (1 << v);
                 nLeftVars++;
+                Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars );
             }
 //            else if ( (Q & bdd_exist( pF->R, pR->V & VarNew ) & bdd_exist( pF->R, pL->V )) == bddfalse )
             else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
             {
 //                pR->V &= VarNew;
-                pIsfR->uSupp |= (1 << v);
+                pIsfR->uUniq |= (1 << v);
                 nRightVars++;
+                Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars );
             }
         }
         else
@@ -342,15 +293,17 @@ int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf
             if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp4, p->puTemp1, p->nVars) )
             {
 //                pR->V &= VarNew;
-                pIsfR->uSupp |= (1 << v);
+                pIsfR->uUniq |= (1 << v);
                 nRightVars++;
+                Kit_TruthCopy( p->puTemp2, p->puTemp4, p->nVars );
             }
 //            else if ( (Q & bdd_exist( pF->R, pL->V & VarNew ) & bdd_exist( pF->R, pR->V )) == bddfalse )
             else if ( Kit_TruthIsDisjoint3(pIsf->puOn, p->puTemp3, p->puTemp2, p->nVars) )
             {
 //                pL->V &= VarNew;
-                pIsfL->uSupp |= (1 << v);
+                pIsfL->uUniq |= (1 << v);
                 nLeftVars++;
+                Kit_TruthCopy( p->puTemp1, p->puTemp3, p->nVars );
             }
         }
     }
@@ -365,28 +318,32 @@ int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf
 //    pL->R = Cudd_bddExistAbstract( dd, pF->R, pR->V );     Cudd_Ref( pL->R );
 
     Kit_TruthAnd( pIsfL->puOn, pIsf->puOn, p->puTemp1, p->nVars );
-    Kit_TruthExistSet( pIsfL->puOn, pIsfL->puOn, p->nVars, pIsfR->uSupp );
+    Kit_TruthExistSet( pIsfL->puOn, pIsfL->puOn, p->nVars, pIsfR->uUniq );
     Kit_TruthCopy( pIsfL->puOff, p->puTemp2, p->nVars );
 
+//    assert( pL->Q != b0 );
+//    assert( pL->R != b0 );
+//    assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
+    assert( !Kit_TruthIsConst0(pIsfL->puOn, p->nVars) );
+    assert( !Kit_TruthIsConst0(pIsfL->puOff, p->nVars) );
+//    assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
+
     // derive the functions Q and R for the right branch
 //    Temp = Cudd_bddExistAbstract( dd, pF->R, pR->V );      Cudd_Ref( Temp );
 //    pR->Q = Cudd_bddAndAbstract( dd, pF->Q, Temp, pL->V ); Cudd_Ref( pR->Q );
 //    Cudd_RecursiveDeref( dd, Temp );
 //    pR->R = Cudd_bddExistAbstract( dd, pF->R, pL->V );     Cudd_Ref( pR->R );
 
-/*
     Kit_TruthAnd( pIsfR->puOn, pIsf->puOn, p->puTemp2, p->nVars );
-    Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uSupp );
+    Kit_TruthExistSet( pIsfR->puOn, pIsfR->puOn, p->nVars, pIsfL->uUniq );
     Kit_TruthCopy( pIsfR->puOff, p->puTemp1, p->nVars );
-*/
 
-//    assert( pL->Q != b0 );
-//    assert( pL->R != b0 );
-//    assert( Cudd_bddIteConstant( dd, pL->Q, pL->R, b0 ) == b0 );
-    assert( !Kit_TruthIsConst0(pIsfL->puOn, p->nVars) );
-    assert( !Kit_TruthIsConst0(pIsfL->puOff, p->nVars) );
-    assert( Kit_TruthIsDisjoint(pIsfL->puOn, pIsfL->puOff, p->nVars) );
+    assert( !Kit_TruthIsConst0(pIsfR->puOn, p->nVars) );
+    assert( !Kit_TruthIsConst0(pIsfR->puOff, p->nVars) );
+//    assert( Kit_TruthIsDisjoint(pIsfR->puOn, pIsfR->puOff, p->nVars) );
 
+    assert( pIsfL->uUniq );
+    assert( pIsfR->uUniq );
     return Bdc_DecomposeGetCost( p, nLeftVars, nRightVars );        
 }
 
@@ -403,7 +360,7 @@ int Bdc_DecomposeOr( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf
 ***********************************************************************/
 Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
 {
-    int CostOr, CostAnd, CostOrL, CostOrR, CostAndL, CostAndR;
+    int WeightOr, WeightAnd, WeightOrL, WeightOrR, WeightAndL, WeightAndR;
 
     Bdc_IsfClean( p->pIsfOL );
     Bdc_IsfClean( p->pIsfOR );
@@ -411,33 +368,61 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
     Bdc_IsfClean( p->pIsfAR );
 
     // perform OR decomposition
-    CostOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR );
+    WeightOr = Bdc_DecomposeOr( p, pIsf, p->pIsfOL, p->pIsfOR );
 
     // perform AND decomposition
     Bdc_IsfNot( pIsf );
-    CostAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR );
+    WeightAnd = Bdc_DecomposeOr( p, pIsf, p->pIsfAL, p->pIsfAR );
     Bdc_IsfNot( pIsf );
     Bdc_IsfNot( p->pIsfAL );
     Bdc_IsfNot( p->pIsfAR );
 
+    // check the case when decomposition does not exist
+    if ( WeightOr == 0 && WeightAnd == 0 )
+    {
+        Bdc_IsfCopy( pIsfL, p->pIsfOL );
+        Bdc_IsfCopy( pIsfR, p->pIsfOR );
+        return BDC_TYPE_MUX;
+    }
     // check the hash table
+    assert( WeightOr || WeightAnd );
+    WeightOrL = WeightOrR = 0;
+    if ( WeightOr )
+    {
+        if ( p->pIsfOL->uUniq )
+        {
             Bdc_SuppMinimize( p, p->pIsfOL );
-    CostOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL);
+            WeightOrL = (Bdc_TableLookup(p, p->pIsfOL) != NULL);
+        }
+        if ( p->pIsfOR->uUniq )
+        {
             Bdc_SuppMinimize( p, p->pIsfOR );
-    CostOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL);
+            WeightOrR = (Bdc_TableLookup(p, p->pIsfOR) != NULL);
+        }
+    }
+    WeightAndL = WeightAndR = 0;
+    if ( WeightAnd )
+    {
+        if ( p->pIsfAL->uUniq )
+        {
             Bdc_SuppMinimize( p, p->pIsfAL );
-    CostAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL);
+            WeightAndL = (Bdc_TableLookup(p, p->pIsfAL) != NULL);
+        }
+        if ( p->pIsfAR->uUniq )
+        {
             Bdc_SuppMinimize( p, p->pIsfAR );
-    CostAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL);
+            WeightAndR = (Bdc_TableLookup(p, p->pIsfAR) != NULL);
+        }
+    }
 
     // check if there is any reuse for the components
-    if ( CostOrL + CostOrR < CostAndL + CostAndR )
+    if ( WeightOrL + WeightOrR > WeightAndL + WeightAndR )
     {
         Bdc_IsfCopy( pIsfL, p->pIsfOL );
         Bdc_IsfCopy( pIsfR, p->pIsfOR );
         return BDC_TYPE_OR;
     }
-    if ( CostOrL + CostOrR > CostAndL + CostAndR )
+    if ( WeightOrL + WeightOrR < WeightAndL + WeightAndR )
     {
         Bdc_IsfCopy( pIsfL, p->pIsfAL );
         Bdc_IsfCopy( pIsfR, p->pIsfAR );
@@ -445,15 +430,207 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
     }
 
     // compare the two-component costs
-    if ( CostOr < CostAnd )
+    if ( WeightOr > WeightAnd )
     {
         Bdc_IsfCopy( pIsfL, p->pIsfOL );
         Bdc_IsfCopy( pIsfR, p->pIsfOR );
         return BDC_TYPE_OR;
     }
+    Bdc_IsfCopy( pIsfL, p->pIsfAL );
+    Bdc_IsfCopy( pIsfR, p->pIsfAR );
     return BDC_TYPE_AND;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Find variable that leads to minimum sum of support sizes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bdc_Isf_t * pIsfR )
+{
+    int Var, VarMin, nSuppMin, nSuppCur;
+    unsigned uSupp0, uSupp1;
+    VarMin = -1;
+    nSuppMin = 1000;
+    for ( Var = 0; Var < p->nVars; Var++ )
+    {
+        if ( (pIsf->uSupp & (1 << Var)) == 0 )
+            continue;
+        Kit_TruthCofactor0New( pIsfL->puOn,  pIsf->puOn,  p->nVars, Var );
+        Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, Var );
+        Kit_TruthCofactor1New( pIsfR->puOn,  pIsf->puOn,  p->nVars, Var );
+        Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, Var );
+        uSupp0 = Kit_TruthSupport( pIsfL->puOn, p->nVars ) & Kit_TruthSupport( pIsfL->puOff, p->nVars );
+        uSupp1 = Kit_TruthSupport( pIsfR->puOn, p->nVars ) & Kit_TruthSupport( pIsfR->puOff, p->nVars );
+        nSuppCur = Kit_WordCountOnes(uSupp0) + Kit_WordCountOnes(uSupp1);  
+        if ( nSuppMin > nSuppCur )
+        {
+            nSuppMin = nSuppCur;
+            VarMin = Var;
+//            break;
+        }
+    }
+    if ( VarMin >= 0 )
+    {
+        Kit_TruthCofactor0New( pIsfL->puOn,  pIsf->puOn,  p->nVars, VarMin );
+        Kit_TruthCofactor0New( pIsfL->puOff, pIsf->puOff, p->nVars, VarMin );
+        Kit_TruthCofactor1New( pIsfR->puOn,  pIsf->puOn,  p->nVars, VarMin );
+        Kit_TruthCofactor1New( pIsfR->puOff, pIsf->puOff, p->nVars, VarMin );
+        Bdc_SuppMinimize( p, pIsfL );
+        Bdc_SuppMinimize( p, pIsfR );
+    }
+    return VarMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc )
+{
+    unsigned * puTruth = p->puTemp1;
+    if ( Bdc_IsComplement(pFunc) )
+        Kit_TruthNot( puTruth, Bdc_Regular(pFunc)->puFunc, p->nVars );
+    else
+        Kit_TruthCopy( puTruth, pFunc->puFunc, p->nVars );
+    return Bdc_TableCheckContainment( p, pIsf, puTruth );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates gates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bdc_Fun_t * Bdc_ManCreateGate( Bdc_Man_t * p, Bdc_Fun_t * pFunc0, Bdc_Fun_t * pFunc1, Bdc_Type_t Type )
+{
+    Bdc_Fun_t * pFunc;
+    pFunc = Bdc_FunNew( p );
+    if ( pFunc == NULL )
+        return NULL;
+    pFunc->Type = Type;
+    pFunc->pFan0 = pFunc0;
+    pFunc->pFan1 = pFunc1;
+    pFunc->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords); 
+    // get the truth table of the left branch
+    if ( Bdc_IsComplement(pFunc0) )
+        Kit_TruthNot( p->puTemp1, Bdc_Regular(pFunc0)->puFunc, p->nVars );
+    else
+        Kit_TruthCopy( p->puTemp1, pFunc0->puFunc, p->nVars );
+    // get the truth table of the right branch
+    if ( Bdc_IsComplement(pFunc1) )
+        Kit_TruthNot( p->puTemp2, Bdc_Regular(pFunc1)->puFunc, p->nVars );
+    else
+        Kit_TruthCopy( p->puTemp2, pFunc1->puFunc, p->nVars );
+    // compute the function of node
+    if ( pFunc->Type == BDC_TYPE_AND )
+    {
+        Kit_TruthAnd( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars );
+    }
+    else if ( pFunc->Type == BDC_TYPE_OR )
+    {
+        Kit_TruthOr( pFunc->puFunc, p->puTemp1, p->puTemp2, p->nVars );
+        // transform to AND gate
+        pFunc->Type = BDC_TYPE_AND;
+        pFunc->pFan0 = Bdc_Not(pFunc->pFan0);
+        pFunc->pFan1 = Bdc_Not(pFunc->pFan1);
+        Kit_TruthNot( pFunc->puFunc, pFunc->puFunc, p->nVars );
+        pFunc = Bdc_Not(pFunc);
+    }
+    else 
+        assert( 0 );
+    // add to table
+    Bdc_Regular(pFunc)->uSupp = Kit_TruthSupport( Bdc_Regular(pFunc)->puFunc, p->nVars );
+    Bdc_TableAdd( p, Bdc_Regular(pFunc) );
+    return pFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one step of bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+    int static Counter = 0;
+    int LocalCounter = Counter++;
+    Bdc_Type_t Type;
+    Bdc_Fun_t * pFunc, * pFunc0, * pFunc1;
+    Bdc_Isf_t IsfL, * pIsfL = &IsfL;
+    Bdc_Isf_t IsfB, * pIsfR = &IsfB;
+/*
+printf( "Init function (%d):\n", LocalCounter );
+Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n");
+Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
+*/
+    // check computed results
+    assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) );
+    if ( pFunc = Bdc_TableLookup( p, pIsf ) )
+        return pFunc;
+    // decide on the decomposition type
+    Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
+    if ( Type == BDC_TYPE_MUX )
+    {
+        int iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
+        pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
+        pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
+        if ( pFunc0 == NULL || pFunc1 == NULL )
+            return NULL;
+        pFunc  = Bdc_FunWithId( p, iVar + 1 );
+        pFunc0 = Bdc_ManCreateGate( p, Bdc_Not(pFunc), pFunc0, BDC_TYPE_AND );
+        pFunc1 = Bdc_ManCreateGate( p, pFunc,  pFunc1, BDC_TYPE_AND );
+        if ( pFunc0 == NULL || pFunc1 == NULL )
+            return NULL;
+        pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, BDC_TYPE_OR );
+    }
+    else
+    {
+        pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
+        if ( pFunc0 == NULL )
+            return NULL;
+        // decompose the right branch
+        if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfL, pIsfR, pFunc0, Type ) )
+        {
+            p->nNodesNew--;
+            return pFunc0;
+        }
+        Bdc_SuppMinimize( p, pIsfR );
+        pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
+        if ( pFunc1 == NULL )
+            return NULL;
+        // create new gate
+        pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type );
+    }
+    if ( pFunc == NULL )
+        return NULL;
+    assert( Bdc_ManNodeVerify( p, pIsf, pFunc ) );
+    return pFunc;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/bdc/bdcInt.h

@@ -36,7 +36,7 @@ extern "C" {
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
 
-#define BDC_SCALE 100  // value used to compute the cost
+#define BDC_SCALE 1000  // value used to compute the cost
 
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
@@ -47,11 +47,11 @@ typedef enum {
     BDC_TYPE_NONE = 0,  // 0:  unknown
     BDC_TYPE_CONST1,    // 1:  constant 1
     BDC_TYPE_PI,        // 2:  primary input
-    BDC_TYPE_AND,       // 4:  AND-gate
-    BDC_TYPE_OR,        // 5:  OR-gate (temporary)
-    BDC_TYPE_XOR,       // 6:  XOR-gate
-    BDC_TYPE_MUX,       // 7:  MUX-gate
-    BDC_TYPE_OTHER      // 8:  unused
+    BDC_TYPE_AND,       // 3:  AND-gate
+    BDC_TYPE_OR,        // 4:  OR-gate (temporary)
+    BDC_TYPE_XOR,       // 5:  XOR-gate
+    BDC_TYPE_MUX,       // 6:  MUX-gate
+    BDC_TYPE_OTHER      // 7:  unused
 } Bdc_Type_t;
 
 typedef struct Bdc_Fun_t_ Bdc_Fun_t;
@@ -60,7 +60,6 @@ struct Bdc_Fun_t_
     int              Type;         // Const1, PI, AND, XOR, MUX
     Bdc_Fun_t *      pFan0;        // fanin of the given node
     Bdc_Fun_t *      pFan1;        // fanin of the given node
-    Bdc_Fun_t *      pFan2;        // fanin of the given node
     unsigned         uSupp;        // bit mask of current support
     unsigned *       puFunc;       // the function of the node
     Bdc_Fun_t *      pNext;        // next function with same support
@@ -70,8 +69,8 @@ struct Bdc_Fun_t_
 typedef struct Bdc_Isf_t_ Bdc_Isf_t;
 struct Bdc_Isf_t_
 {
-    int              Var;          // the first variable assigned
-    unsigned         uSupp;        // the current support
+    unsigned         uSupp;        // the complete support of this component
+    unsigned         uUniq;        // the unique variables of this component
     unsigned *       puOn;         // on-set
     unsigned *       puOff;        // off-set
 };
@@ -82,13 +81,13 @@ struct Bdc_Man_t_
     Bdc_Par_t *      pPars;        // parameter set
     int              nVars;        // the number of variables
     int              nWords;       // the number of words 
-    int              nNodesLimit;  // the limit on the number of new nodes
+    int              nNodesMax;    // the limit on the number of new nodes
     int              nDivsLimit;   // the limit on the number of divisors
     // internal nodes
     Bdc_Fun_t *      pNodes;       // storage for decomposition nodes
-    int              nNodes;       // the number of nodes used
-    int              nNodesNew;    // the number of nodes used
     int              nNodesAlloc;  // the number of nodes allocated  
+    int              nNodes;       // the number of all nodes created so far
+    int              nNodesNew;    // the number of new AND nodes created so far
     Bdc_Fun_t *      pRoot;        // the root node
     // resub candidates
     Bdc_Fun_t **     pTable;       // hash table of candidates
@@ -115,9 +114,11 @@ static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p )                  { return
 static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p )                      { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^  (PORT_PTRUINT_T)01);     }
 static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c )           { return (Bdc_Fun_t *)((PORT_PTRUINT_T)p ^  (PORT_PTRUINT_T)(c!=0)); }
 
-static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p )                   { Bdc_Fun_t * pRes; if ( p->nNodes == p->nNodesLimit ) return NULL; pRes = p->pNodes + p->nNodes++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); p->nNodesNew++; return pRes; }
-static inline void        Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); }
-static inline void        Bdc_IsfClean( Bdc_Isf_t * p )                 { p->uSupp = 0; p->Var = 0;                                        }
+static inline Bdc_Fun_t * Bdc_FunNew( Bdc_Man_t * p )                   { Bdc_Fun_t * pRes; if ( p->nNodes >= p->nNodesAlloc || p->nNodesNew >= p->nNodesMax ) return NULL; pRes = p->pNodes + p->nNodes++; p->nNodesNew++; memset( pRes, 0, sizeof(Bdc_Fun_t) ); return pRes; }
+static inline Bdc_Fun_t * Bdc_FunWithId( Bdc_Man_t * p, int Id )        { assert( Id < p->nNodes ); return p->pNodes + Id; }
+static inline int         Bdc_FunId( Bdc_Man_t * p, Bdc_Fun_t * pFun )  { return pFun - p->pNodes; }
+static inline void        Bdc_IsfStart( Bdc_Man_t * p, Bdc_Isf_t * pF ) { pF->uSupp = 0; pF->uUniq = 0; pF->puOn = Vec_IntFetch( p->vMemory, p->nWords ); pF->puOff = Vec_IntFetch( p->vMemory, p->nWords ); }
+static inline void        Bdc_IsfClean( Bdc_Isf_t * p )                 { p->uSupp = 0; p->uUniq = 0;                                      }
 static inline void        Bdc_IsfCopy( Bdc_Isf_t * p, Bdc_Isf_t * q )   { Bdc_Isf_t T = *p; *p = *q; *q = T;                               }
 static inline void        Bdc_IsfNot( Bdc_Isf_t * p )                   { unsigned * puT = p->puOn; p->puOn = p->puOff; p->puOff = puT;    }
 

src/aig/bdc/bdcTable.c

@@ -42,6 +42,9 @@
 void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
 {
     int v;
+    // compute support
+    pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) | 
+        Kit_TruthSupport( pIsf->puOff, p->nVars );
     // go through the support variables
     for ( v = 0; v < p->nVars; v++ )
     {
@@ -72,7 +75,7 @@ void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
 int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth )
 {
     return Kit_TruthIsImply( pIsf->puOn, puTruth, p->nVars ) &&
-         Kit_TruthIsDisjoint( pIsf->puOff, puTruth, p->nVars );
+         Kit_TruthIsDisjoint( puTruth, pIsf->puOff, p->nVars );
 }
 
 /**Function*************************************************************
@@ -88,10 +91,29 @@ int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTru
 ***********************************************************************/
 Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
 {
+    int fDisableCache = 0;
     Bdc_Fun_t * pFunc;
+    if ( fDisableCache && Kit_WordCountOnes(pIsf->uSupp) > 1 )
+        return NULL;
+    if ( pIsf->uSupp == 0 )
+    {
+        assert( p->pTable[pIsf->uSupp] == p->pNodes );
+        if ( Kit_TruthIsConst1( pIsf->puOn, p->nVars ) )
+            return p->pNodes;
+        assert( Kit_TruthIsConst1( pIsf->puOff, p->nVars ) );
+        return Bdc_Not(p->pNodes);
+    }
     for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext )
         if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) )
              return pFunc;
+    Bdc_IsfNot( pIsf );
+    for ( pFunc = p->pTable[pIsf->uSupp]; pFunc; pFunc = pFunc->pNext )
+        if ( Bdc_TableCheckContainment( p, pIsf, pFunc->puFunc ) )
+        {
+            Bdc_IsfNot( pIsf );
+            return Bdc_Not(pFunc);
+        }
+    Bdc_IsfNot( pIsf );
     return NULL;
 }
 

src/aig/fra/fra.h

@@ -334,6 +334,7 @@ extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
 extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
 extern int                 Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
 extern int                 Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right );
+extern int                 Fra_SmlNodeCountOnes( Fra_Sml_t * p, Aig_Obj_t * pObj );
 extern int                 Fra_SmlCheckOutput( Fra_Man_t * p );
 extern void                Fra_SmlSavePattern( Fra_Man_t * p );
 extern void                Fra_SmlSimulate( Fra_Man_t * p, int fInit );

src/aig/fra/fraSim.c

@@ -159,6 +159,27 @@ int Fra_SmlNodeIsZero( Fra_Sml_t * p, Aig_Obj_t * pObj )
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of one's in the patten of the output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_SmlNodeCountOnes( Fra_Sml_t * p, Aig_Obj_t * pObj )
+{
+    unsigned * pSims;
+    int i, Counter = 0;
+    pSims = Fra_ObjSim(p, pObj->Id);
+    for ( i = 0; i < p->nWordsTotal; i++ )
+        Counter += Aig_WordCountOnes( pSims[i] );
+    return Counter;
+}
+
 
 
 /**Function*************************************************************

src/base/abc/abcSop.c

@@ -931,6 +931,21 @@ char * Abc_SopFromTruthHex( char * pTruth )
         pCube[nVars + 1] = '1';
         pCube[nVars + 2] = '\n';
     }
+/*
+    // create TT representation
+    {
+        extern void Bdc_ManDecomposeTest( unsigned uTruth, int nVars );
+        unsigned uTruth = 0;
+        int nVarsAll = 4;
+        assert( nVarsAll == 4 );
+        assert( nVars <= nVarsAll );
+        Vec_IntForEachEntry( vMints, Mint, i )
+            uTruth |= (1 << Mint);
+//        uTruth = uTruth | (uTruth << 8) | (uTruth << 16) | (uTruth << 24);
+        uTruth = uTruth | (uTruth << 16);
+        Bdc_ManDecomposeTest( uTruth, nVarsAll );
+    }
+*/
     Vec_IntFree( vMints );
     return pSopCover;
 }

src/base/abci/abc.c

@@ -391,6 +391,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
         extern void Dar_LibStart();
         Dar_LibStart();
     }
+    {
+        extern Bdc_ManDecomposeTest( unsigned uTruth, int nVars );
+//        Bdc_ManDecomposeTest( 0x0f0f0f0f, 3 );
+    }
 } 
 
 /**Function*************************************************************
@@ -10771,6 +10775,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->fEdge       =  0;
     pPars->fCutMin     =  0;
     pPars->fSeqMap     =  0;
+    pPars->fBidec      =  0;
     pPars->fVerbose    =  0;
     // internal parameters
     pPars->fTruth      =  0;
@@ -10782,7 +10787,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
     pPars->pFuncCost   =  NULL;   
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEpaflemrstvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCFADEpaflemrstbvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10880,6 +10885,9 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             pPars->fLiftLeaves ^= 1;
             break;
+        case 'b':
+            pPars->fBidec ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -11008,7 +11016,7 @@ usage:
         sprintf( LutSize, "library" );
     else
         sprintf( LutSize, "%d", pPars->nLutSize );
-    fprintf( pErr, "usage: if [-KCFA num] [-DE float] [-parlemsvh]\n" );
+    fprintf( pErr, "usage: if [-KCFA num] [-DE float] [-parlemsbvh]\n" );
     fprintf( pErr, "\t           performs FPGA technology mapping of the network\n" );
     fprintf( pErr, "\t-K num   : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
     fprintf( pErr, "\t-C num   : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -11025,6 +11033,7 @@ usage:
     fprintf( pErr, "\t-m       : enables cut minimization by removing vacuous variables [default = %s]\n", pPars->fCutMin? "yes": "no" );
     fprintf( pErr, "\t-s       : toggles sequential mapping [default = %s]\n", pPars->fSeqMap? "yes": "no" );
 //    fprintf( pErr, "\t-t       : toggles the use of true sequential cuts [default = %s]\n", pPars->fLiftLeaves? "yes": "no" );
+    fprintf( pErr, "\t-b       : toggles deriving local AIGs using bi-decomposition [default = %s]\n", pPars->fBidec? "yes": "no" );
     fprintf( pErr, "\t-v       : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : prints the command usage\n");
     return 1;

src/base/abci/abcDar.c

@@ -1567,6 +1567,32 @@ Abc_Ntk_t * Abc_NtkInterOne( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbo
     return pNtkAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Fast interpolation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkInterFast( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose )
+{
+    extern void Aig_ManInterFast( Aig_Man_t * pManOn, Aig_Man_t * pManOff, int fVerbose );
+    Aig_Man_t * pManOn, * pManOff;
+    // create internal AIGs
+    pManOn = Abc_NtkToDar( pNtkOn, 0 );
+    if ( pManOn == NULL )
+        return;
+    pManOff = Abc_NtkToDar( pNtkOff, 0 );
+    if ( pManOff == NULL )
+        return;
+    Aig_ManInterFast( pManOn, pManOff, fVerbose );
+    Aig_ManStop( pManOn );
+    Aig_ManStop( pManOff );
+}
 
 int timeCnf;
 int timeSat;
@@ -1587,12 +1613,15 @@ Abc_Ntk_t * Abc_NtkInter( Abc_Ntk_t * pNtkOn, Abc_Ntk_t * pNtkOff, int fVerbose
 {
     Abc_Ntk_t * pNtkOn1, * pNtkOff1, * pNtkInter1, * pNtkInter;
     Abc_Obj_t * pObj;
-    int i;
+    int i, clk = clock();
     if ( Abc_NtkCoNum(pNtkOn) != Abc_NtkCoNum(pNtkOff) )
     {
         printf( "Currently works only for networks with equal number of POs.\n" );
         return NULL;
     }
+    // compute the fast interpolation time
+//    Abc_NtkInterFast( pNtkOn, pNtkOff, fVerbose );
+    // consider the case of one output
     if ( Abc_NtkCoNum(pNtkOn) == 1 )
         return Abc_NtkInterOne( pNtkOn, pNtkOff, fVerbose );
     // start the new newtork
@@ -1636,6 +1665,7 @@ timeInt = 0;
 //    PRT( "CNF", timeCnf );
 //    PRT( "SAT", timeSat );
 //    PRT( "Int", timeInt );
+//    PRT( "Slow interpolation time", clock() - clk );
 
     // return the network
     if ( !Abc_NtkCheck( pNtkInter ) )

src/base/abci/abcIf.c

@@ -34,6 +34,7 @@ static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_O
 static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk );
 
 extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
+extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk );
  
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -84,6 +85,8 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
     if ( pNtkNew == NULL )
         return NULL;
     If_ManStop( pIfMan );
+    if ( pPars->fBidec && pPars->nLutSize <= 8 )
+        Abc_NtkBidecResyn( pNtkNew );
 
     // duplicate EXDC
     if ( pNtk->pExdc )
@@ -309,7 +312,9 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
             Abc_NodeComplement( pNodeNew );
     }
     else
+    {
         pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pIfObj );
+    }
     If_ObjSetCopy( pIfObj, pNodeNew );
     return pNodeNew;
 }
@@ -545,6 +550,88 @@ Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk )
     return vNodes;
 }
 
+
+#include "bdc.h"
+#include "bdcInt.h"
+
+static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj )  { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) );  }
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth )
+{
+    unsigned * pTruth;
+    Bdc_Fun_t * pFunc;
+    int i;
+    // derive truth table
+    pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
+    if ( Hop_IsComplement(pRoot) )
+        Extra_TruthNot( pTruth, pTruth, nVars );
+    // decompose truth table
+    Bdc_ManDecompose( p, pTruth, NULL, nVars, NULL, 1000 );
+    // convert back into HOP
+    Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop );
+    for ( i = 0; i < nVars; i++ )
+        Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i );
+    for ( i = nVars + 1; i < p->nNodes; i++ )
+    {
+        pFunc = Bdc_FunWithId( p, i );
+        pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) );
+    }
+    return Bdc_FunCopyHop(p->pRoot);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Resynthesizes nodes using bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk )
+{
+    Bdc_Par_t Pars = {0}, * pPars = &Pars;
+    Bdc_Man_t * p;
+    Abc_Obj_t * pObj;
+    Vec_Int_t * vTruth;
+    int i, nGainTotal = 0, nNodes1, nNodes2;
+    int clk = clock();
+    pPars->nVarsMax = Abc_NtkGetFaninMax( pNtk );
+    if ( pPars->nVarsMax > 8 )
+    {
+        printf( "Resynthesis is not performed.\n" );
+        return;
+    }
+    vTruth = Vec_IntAlloc( 0 );
+    p = Bdc_ManAlloc( pPars );
+    Abc_NtkForEachNode( pNtk, pObj, i )
+    {
+        nNodes1 = Hop_DagSize(pObj->pData);
+        pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth );
+        nNodes2 = Hop_DagSize(pObj->pData);
+        nGainTotal += nNodes1 - nNodes2;
+    }
+//    printf( "LUTs = %d.  Total gain in AIG nodes = %d.  ", Abc_NtkNodeNum(pNtk), nGainTotal );
+//    PRT( "Time", clock() - clk );
+    Bdc_ManFree( p );
+    Vec_IntFree( vTruth );
+}
+
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/base/cmd/cmd.c

@@ -149,12 +149,17 @@ void Cmd_End( Abc_Frame_t * pAbc )
 int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     int c;
+    int fClear;
 
+    fClear = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'c':
+            fClear ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -162,11 +167,19 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv )
         }
     }
 
+    if ( fClear )
+    {
+        pAbc->TimeTotal += pAbc->TimeCommand;
+        pAbc->TimeCommand = 0.0;
+        return 0;
+    }
+
     if ( argc != globalUtilOptind )
     {
         goto usage;
     }
 
+
     pAbc->TimeTotal += pAbc->TimeCommand;
     fprintf( pAbc->Out, "elapse: %3.2f seconds, total: %3.2f seconds\n", 
         pAbc->TimeCommand, pAbc->TimeTotal );
@@ -182,7 +195,9 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
   usage:
-    fprintf( pAbc->Err, "usage: time [-h]\n" );
+    fprintf( pAbc->Err, "usage: time [-ch]\n" );
+    fprintf( pAbc->Err, "      \t\tprint the runtime since the last call\n" );
+    fprintf( pAbc->Err, "   -c \t\tclears the elapsed time without printing it\n" );
     fprintf( pAbc->Err, "   -h \t\tprint the command usage\n" );
     return 1;
 }

src/map/if/if.h

@@ -90,6 +90,7 @@ struct If_Par_t_
     int                fEdge;         // uses edge-based cut selection heuristics
     int                fCutMin;       // performs cut minimization by removing functionally reducdant variables
     int                fSeqMap;       // sequential mapping
+    int                fBidec;        // use bi-decomposition
     int                fVerbose;      // the verbosity flag
     // internal parameters
     int                fAreaOnly;     // area only mode

src/opt/mfs/mfsCore.c

@@ -110,6 +110,8 @@ clk = clock();
     p->vSupp  = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
     p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
 p->timeWin += clock() - clk;
+    // count the number of patterns
+//    p->dTotalRatios += Abc_NtkConstraintRatio( p, pNode );
     // construct AIG for the window
 clk = clock();
     p->pAigWin = Abc_NtkConstructAig( p, pNode );
@@ -121,6 +123,8 @@ p->timeCnf += clock() - clk;
     // create the SAT problem
 clk = clock();
     p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
+    if ( p->pSat == NULL )
+        return 0;
     // solve the SAT problem
     Abc_NtkMfsSolveSat( p, pNode );
 p->timeSat += clock() - clk;

src/opt/mfs/mfsInt.h

@@ -86,6 +86,7 @@ struct Mfs_Man_t_
     int                 nTotalDivs;
     int                 nTimeOuts;
     int                 nDcMints;
+    double              dTotalRatios;
     // node/edge stats
     int                 nTotalNodesBeg;
     int                 nTotalNodesEnd;
@@ -132,6 +133,7 @@ extern int              Abc_NtkMfsResubNode2( Mfs_Man_t * p, Abc_Obj_t * pNode )
 extern void             Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsStrash.c ==========================================================*/
 extern Aig_Man_t *      Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern double           Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode );
 /*=== mfsWin.c ==========================================================*/
 extern Vec_Ptr_t *      Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit );
 

src/opt/mfs/mfsMan.c

@@ -126,9 +126,13 @@ void Mfs_ManPrint( Mfs_Man_t * p )
     }
     else
     {
-        printf( "Nodes = %d.  Care mints = %d. Total mints = %d. Ratio = %5.2f.\n", 
-            p->nNodesTried, p->nMintsCare, p->nMintsTotal, 1.0 * p->nMintsCare / p->nMintsTotal );
+        printf( "Nodes = %d.  DC mints in local space = %d. Total mints = %d. Ratio = %5.2f.\n", 
+            p->nNodesTried, p->nMintsTotal-p->nMintsCare, p->nMintsTotal, 
+            1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal );
+//        printf( "Average ratio of sequential DCs in the global space = %5.2f.\n", 
+//            1.0-(p->dTotalRatios/p->nNodesTried) );
     }
+/*
     PRTP( "Win", p->timeWin            ,  p->timeTotal );
     PRTP( "Div", p->timeDiv            ,  p->timeTotal );
     PRTP( "Aig", p->timeAig            ,  p->timeTotal );
@@ -136,7 +140,7 @@ void Mfs_ManPrint( Mfs_Man_t * p )
     PRTP( "Sat", p->timeSat-p->timeInt ,  p->timeTotal );
     PRTP( "Int", p->timeInt            ,  p->timeTotal );
     PRTP( "ALL", p->timeTotal          ,  p->timeTotal );
-
+*/
 }
 
 /**Function*************************************************************

src/opt/mfs/mfsStrash.c

@@ -255,6 +255,87 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
     return pMan;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Creates AIG for the window with constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Abc_NtkAigForConstraints( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    Abc_Obj_t * pFanin;
+    Aig_Man_t * pMan;
+    Aig_Obj_t * pPi, * pPo, * pObjAig, * pObjRoot;
+    Vec_Int_t * vOuts;
+    int i, k, iOut;
+    if ( p->pCare == NULL )
+        return NULL;
+    pMan = Aig_ManStart( 1000 );
+    // mark the care set
+    Aig_ManIncrementTravId( p->pCare );
+    Vec_PtrForEachEntry( p->vSupp, pFanin, i )
+    {
+        pPi = Aig_ManPi( p->pCare, (int)pFanin->pData );
+        Aig_ObjSetTravIdCurrent( p->pCare, pPi );
+        pPi->pData = Aig_ObjCreatePi(pMan);
+    }
+    // construct the constraints
+    pObjRoot = Aig_ManConst1(pMan);
+    Vec_PtrForEachEntry( p->vSupp, pFanin, i )
+    {
+        vOuts = Vec_PtrEntry( p->vSuppsInv, (int)pFanin->pData );
+        Vec_IntForEachEntry( vOuts, iOut, k )
+        {
+            pPo = Aig_ManPo( p->pCare, iOut );
+            if ( Aig_ObjIsTravIdCurrent( p->pCare, pPo ) )
+                continue;
+            Aig_ObjSetTravIdCurrent( p->pCare, pPo );
+            if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
+                continue;
+            pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
+            if ( pObjAig == NULL )
+                continue;
+            pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
+            pObjRoot = Aig_And( pMan, pObjRoot, pObjAig );
+        }
+    }
+    Aig_ObjCreatePo( pMan, pObjRoot );
+    Aig_ManCleanup( pMan );
+    return pMan;
+}
+
+#include "fra.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the ratio of don't-cares.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+double Abc_NtkConstraintRatio( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    int nSimWords = 256;
+    Aig_Man_t * pMan;
+    Fra_Sml_t * pSim;
+    int Counter;
+    pMan = Abc_NtkAigForConstraints( p, pNode );
+    pSim = Fra_SmlSimulateComb( pMan, nSimWords );
+    Counter = Fra_SmlNodeCountOnes( pSim, Aig_ManPo(pMan, 0) );
+    Aig_ManStop( pMan );
+    Fra_SmlStop( pSim );
+    return 1.0 * Counter / (32 * nSimWords);
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/sat/bsat/satSolver.c

@@ -1294,6 +1294,13 @@ void sat_solver_store_free( sat_solver * s )
     s->pStore = NULL;
 }
 
+int sat_solver_store_change_last( sat_solver * s )
+{
+    extern int Sto_ManChangeLastClause( void * p );
+    if ( s->pStore ) return Sto_ManChangeLastClause( s->pStore );
+    return -1;
+}
+ 
 void sat_solver_store_mark_roots( sat_solver * s )
 {
     extern void Sto_ManMarkRoots( void * p );

src/sat/bsat/satStore.c

@@ -260,6 +260,31 @@ void Sto_ManMarkClausesA( Sto_Man_t * p )
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the literal of the last clause.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sto_ManChangeLastClause( Sto_Man_t * p )
+{
+    Sto_Cls_t * pClause, * pPrev;
+    pPrev = NULL;
+    Sto_ManForEachClause( p, pClause )
+        pPrev = pClause;
+    assert( pPrev != NULL );
+    assert( pPrev->fA == 1 );
+    assert( pPrev->nLits == 1 );
+    p->nClausesA--;
+    pPrev->fA = 0;
+    return pPrev->pLits[0] >> 1;
+}
+
 
 /**Function*************************************************************