From a6352369a5583f18c8819a40fc2968f6d8dbe93c Mon Sep 17 00:00:00 2001
From: Mathias Soeken <mathias.soeken@epfl.ch>
Date: Sat, 30 Jul 2016 15:21:57 +0200
Subject: Depth optimal synthesis.

---
 src/base/abci/abcExact.c | 25 ++++++++++++++++++-------
 1 file changed, 18 insertions(+), 7 deletions(-)

diff --git a/src/base/abci/abcExact.c b/src/base/abci/abcExact.c
index a8ad858f..40f85b79 100644
--- a/src/base/abci/abcExact.c
+++ b/src/base/abci/abcExact.c
@@ -1111,8 +1111,8 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
 {
     int l;
     Ses_Man_t * pSes;
-    char * pSol, * p;
-    int Delay;
+    char * pSol = NULL, * p;
+    int Delay = ABC_INFINITY, nMaxDepth = nVars - 1;
     abctime timeStart;
 
     /* some checks */
@@ -1120,12 +1120,25 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
 
     timeStart = Abc_Clock();
 
-    pSes = Ses_ManAlloc( pTruth, nVars, 1, nVars - 1, pArrTimeProfile, 1, 0 );
+    *Cost = ABC_INFINITY;
 
-    if ( Ses_ManFindMinimumSize( pSes ) )
+    pSes = Ses_ManAlloc( pTruth, nVars, 1 /* fSpecFunc */, nMaxDepth, pArrTimeProfile, 1 /* fMakeAIG */, 0 );
+
+    while ( 1 ) /* there is improvement */
     {
-        pSol = Ses_ManExtractSolution( pSes );
+        if ( Ses_ManFindMinimumSize( pSes ) )
+        {
+            if ( pSol )
+                ABC_FREE( pSol );
+            pSol = Ses_ManExtractSolution( pSes );
+            pSes->nMaxDepth--;
+        }
+        else
+            break;
+    }
 
+    if ( pSol )
+    {
         *Cost = pSol[ABC_EXACT_SOL_NGATES];
         p = pSol + 3 + 4 * ABC_EXACT_SOL_NGATES + 1;
         Delay = *p++;
@@ -1134,8 +1147,6 @@ int Abc_ExactDelayCost( word * pTruth, int nVars, int * pArrTimeProfile, char *
 
         ABC_FREE( pSol );
     }
-    else
-        *Cost = Delay = ABC_INFINITY;
 
     pSes->timeTotal = Abc_Clock() - timeStart;
 
-- 
cgit v1.2.3