Various changes to enable sensitization-based refinement in &gla.

4 files changed, 10 insertions, 10 deletions

diff --git a/src/opt/dar/dar.h b/src/opt/dar/dar.h
index 5c2c9bcc..ed1f4e74 100644
--- a/src/opt/dar/dar.h
+++ b/src/opt/dar/dar.h
@@ -91,7 +91,7 @@ extern void            Dar_BalancePrintStats( Aig_Man_t * p );
 /*=== 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, int fVerbose );
+extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fSkipTtMin, 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/opt/dar/darCore.c b/src/opt/dar/darCore.c
index 54e9cf84..958ab70a 100644
--- a/src/opt/dar/darCore.c
+++ b/src/opt/dar/darCore.c
@@ -281,8 +281,8 @@ int Dar_ManCutCount( Aig_Man_t * pAig, int * pnCutsK )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose )
-{
+Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fSkipTtMin, int fVerbose )
+{ 
     Dar_Man_t * p;
     Dar_RwrPar_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
@@ -306,7 +306,7 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax, int fVerbose
         Dar_ObjPrepareCuts( p, pObj );
     // compute cuts for each nodes in the topological order
     Aig_ManForEachNode( pAig, pObj, i )
-        Dar_ObjComputeCuts( p, pObj );
+        Dar_ObjComputeCuts( p, pObj, fSkipTtMin );
     // print verbose stats
     if ( fVerbose )
     {
diff --git a/src/opt/dar/darCut.c b/src/opt/dar/darCut.c
index 1056ef32..da1c9eaf 100644
--- a/src/opt/dar/darCut.c
+++ b/src/opt/dar/darCut.c
@@ -735,14 +735,14 @@ void Dar_ManCutsRestart( Dar_Man_t * p, Aig_Obj_t * pRoot )
   SeeAlso     []
 
 ***********************************************************************/
-Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
+Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj, int fSkipTtMin )
 {
     Aig_Obj_t * pFanin0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
     Aig_Obj_t * pFanin1 = Aig_ObjReal_rec( Aig_ObjChild1(pObj) );
     Aig_Obj_t * pFaninR0 = Aig_Regular(pFanin0);
     Aig_Obj_t * pFaninR1 = Aig_Regular(pFanin1);
     Dar_Cut_t * pCutSet, * pCut0, * pCut1, * pCut;
-    int i, k, RetValue; 
+    int i, k; 
 
     assert( !Aig_IsComplement(pObj) );
     assert( Aig_ObjIsNode(pObj) );
@@ -779,9 +779,9 @@ Dar_Cut_t * Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj )
         pCut->uTruth = 0xFFFF & Dar_CutTruth( pCut, pCut0, pCut1, Aig_IsComplement(pFanin0), Aig_IsComplement(pFanin1) );
 
         // minimize support of the cut
-        if ( Dar_CutSuppMinimize( pCut ) )
+        if ( !fSkipTtMin && Dar_CutSuppMinimize( pCut ) )
         {
-            RetValue = Dar_CutFilter( pObj, pCut );
+            int RetValue = Dar_CutFilter( pObj, pCut );
             assert( !RetValue );
         }
 
@@ -825,7 +825,7 @@ Dar_Cut_t * Dar_ObjComputeCuts_rec( Dar_Man_t * p, Aig_Obj_t * pObj )
         return Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) );
     Dar_ObjComputeCuts_rec( p, Aig_ObjFanin0(pObj) );
     Dar_ObjComputeCuts_rec( p, Aig_ObjFanin1(pObj) );
-    return Dar_ObjComputeCuts( p, pObj );
+    return Dar_ObjComputeCuts( p, pObj, 0 );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/dar/darInt.h b/src/opt/dar/darInt.h
index 08af70df..caea213c 100644
--- a/src/opt/dar/darInt.h
+++ b/src/opt/dar/darInt.h
@@ -137,7 +137,7 @@ extern void            Dar_ManCutsRestart( Dar_Man_t * p, Aig_Obj_t * pRoot );
 extern void            Dar_ManCutsFree( Dar_Man_t * p );
 extern Dar_Cut_t *     Dar_ObjPrepareCuts( Dar_Man_t * p, Aig_Obj_t * pObj );
 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 Dar_Cut_t *     Dar_ObjComputeCuts( Dar_Man_t * p, Aig_Obj_t * pObj, int fSkipTtMin );
 extern void            Dar_ObjCutPrint( Aig_Man_t * p, Aig_Obj_t * pObj );
 /*=== darData.c ===========================================================*/
 extern Vec_Int_t *     Dar_LibReadNodes();