Version abc80313

4 files changed, 94 insertions, 3 deletions

diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 4a2e96e7..4e4f7490 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/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;
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index b7fa6ef0..91395d03 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/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 );
 
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 5f947aeb..17ca40fc 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/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*************************************************************
diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c
index a3475752..88f7554c 100644
--- a/src/opt/mfs/mfsStrash.c
+++ b/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                                ///
 ////////////////////////////////////////////////////////////////////////