Added switch 'dch -r' to skip choices with structural support redundancy.

4 files changed, 64 insertions, 8 deletions

diff --git a/src/proof/dch/dch.h b/src/proof/dch/dch.h
index ff29f0da..e887ba26 100644
--- a/src/proof/dch/dch.h
+++ b/src/proof/dch/dch.h
@@ -53,6 +53,7 @@ struct Dch_Pars_t_
     int              fUseGia;       // uses GIA package 
     int              fUseCSat;      // uses circuit-based solver
     int              fLightSynth;   // uses lighter version of synthesis
+    int              fSkipRedSupp;  // skip choices with redundant support vars
     int              fVerbose;      // verbose stats
     clock_t          timeSynth;     // synthesis runtime
     int              nNodesAhead;   // the lookahead in terms of nodes
diff --git a/src/proof/dch/dchChoice.c b/src/proof/dch/dchChoice.c
index 7a763d84..ff8002d9 100644
--- a/src/proof/dch/dchChoice.c
+++ b/src/proof/dch/dchChoice.c
@@ -185,6 +185,41 @@ static inline Aig_Obj_t * Aig_ObjGetRepr( Aig_Man_t * p, Aig_Obj_t * pObj )
 static inline Aig_Obj_t * Aig_ObjChild0CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild0Copy(pObj) ); }
 static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj ) { return Aig_ObjGetRepr( p, Aig_ObjChild1Copy(pObj) ); }
 
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI of the node.]
+
+  Description [Returns 1 if there is a CI not marked with previous ID.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dch_ObjMarkTfi_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    int RetValue;
+    if ( pObj == NULL )
+        return 0;
+    if ( Aig_ObjIsTravIdCurrent( p, pObj ) )
+        return 0;
+    if ( Aig_ObjIsCi(pObj) )
+    {
+        RetValue = !Aig_ObjIsTravIdPrevious( p, pObj );
+        Aig_ObjSetTravIdCurrent( p, pObj );
+        return RetValue;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    Aig_ObjSetTravIdCurrent( p, pObj );
+    RetValue  = Dch_ObjMarkTfi_rec( p, Aig_ObjFanin0(pObj) );
+    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjFanin1(pObj) );
+    RetValue += Dch_ObjMarkTfi_rec( p, Aig_ObjEquiv(p, pObj) );
+    return (RetValue > 0);
+}
+
 /**Function*************************************************************
 
   Synopsis    [Derives the AIG with choices from representatives.]
@@ -196,7 +231,7 @@ static inline Aig_Obj_t * Aig_ObjChild1CopyRepr( Aig_Man_t * p, Aig_Obj_t * pObj
   SeeAlso     []
 
 ***********************************************************************/
-void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj )
+void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_t * pObj, int fSkipRedSupps )
 {
     Aig_Obj_t * pRepr, * pObjNew, * pReprNew;
     // get the new node
@@ -227,6 +262,25 @@ void Dch_DeriveChoiceAigNode( Aig_Man_t * pAigNew, Aig_Man_t * pAigOld, Aig_Obj_
     // skip choices with combinational loops
     if ( Dch_ObjCheckTfi( pAigNew, pObjNew, pReprNew ) )
         return;
+    // don't add choice if structural support of pObjNew and pReprNew differ
+    if ( fSkipRedSupps )
+    {
+        int fSkipChoice = 0;
+        // mark support of the representative node (pReprNew)
+        Aig_ManIncrementTravId( pAigNew );
+        Dch_ObjMarkTfi_rec( pAigNew, pReprNew );
+        // detect if the new node (pObjNew) depends on any additional variables
+        Aig_ManIncrementTravId( pAigNew );
+        if ( Dch_ObjMarkTfi_rec( pAigNew, pObjNew ) )
+            fSkipChoice = 1;//, printf( "1" );
+        // detect if the representative node (pReprNew) depends on any additional variables
+        Aig_ManIncrementTravId( pAigNew );
+        if ( Dch_ObjMarkTfi_rec( pAigNew, pReprNew ) )
+            fSkipChoice = 1;//, printf( "2" );
+        // skip the choice if this is what is happening
+        if ( fSkipChoice )
+            return;
+    }
     // add choice
     pAigNew->pEquivs[pObjNew->Id]  = pAigNew->pEquivs[pReprNew->Id];
     pAigNew->pEquivs[pReprNew->Id] = pObjNew;
@@ -260,7 +314,7 @@ Aig_Man_t * Dch_DeriveChoiceAig_old( Aig_Man_t * pAig )
     // construct choices for the internal nodes
     assert( pAig->pReprs != NULL );
     Aig_ManForEachNode( pAig, pObj, i )
-        Dch_DeriveChoiceAigNode( pChoices, pAig, pObj );
+        Dch_DeriveChoiceAigNode( pChoices, pAig, pObj, 0 );
     Aig_ManForEachCo( pAig, pObj, i )
         Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
     Dch_DeriveChoiceCountEquivs( pChoices );
@@ -442,7 +496,7 @@ void Aig_ManFixLoopProblem( Aig_Man_t * p, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig )
+Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig, int fSkipRedSupps )
 {
     Aig_Man_t * pChoices;
     Aig_Obj_t * pObj;
@@ -459,7 +513,7 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig )
     // construct choices for the internal nodes
     assert( pAig->pReprs != NULL );
     Aig_ManForEachNode( pAig, pObj, i )
-        Dch_DeriveChoiceAigNode( pChoices, pAig, pObj );
+        Dch_DeriveChoiceAigNode( pChoices, pAig, pObj, fSkipRedSupps );
     Aig_ManForEachCo( pAig, pObj, i )
         Aig_ObjCreateCo( pChoices, Aig_ObjChild0CopyRepr(pChoices, pObj) );
     Dch_DeriveChoiceCountEquivs( pChoices );
@@ -478,12 +532,12 @@ Aig_Man_t * Dch_DeriveChoiceAigInt( Aig_Man_t * pAig )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig )
+Aig_Man_t * Dch_DeriveChoiceAig( Aig_Man_t * pAig, int fSkipRedSupps )
 {
     extern int Aig_ManCheckAcyclic( Aig_Man_t * pAig, int fVerbose );
     Aig_Man_t * pChoices, * pTemp;
     int fVerbose = 0;
-    pChoices = Dch_DeriveChoiceAigInt( pAig );
+    pChoices = Dch_DeriveChoiceAigInt( pAig, fSkipRedSupps );
 //    pChoices = Dch_DeriveChoiceAigInt( pTemp = pChoices );
 //    Aig_ManStop( pTemp );
     // there is no need for cleanup
diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c
index bfef8d8c..0d2e8c0d 100644
--- a/src/proof/dch/dchCore.c
+++ b/src/proof/dch/dchCore.c
@@ -53,6 +53,7 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p )
     p->fSimulateTfo   =     1;  // simulate TFO
     p->fPower         =     0;  // power-aware rewriting
     p->fLightSynth    =     0;  // uses lighter version of synthesis
+    p->fSkipRedSupp   =     0;  // skips choices with redundant structural support
     p->fVerbose       =     0;  // verbose stats
     p->nNodesAhead    =  1000;  // the lookahead in terms of nodes
     p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
@@ -107,7 +108,7 @@ p->timeTotal = clock() - clkTotal;
     Dch_ManStop( p );
     // create choices
     ABC_FREE( pAig->pTable );
-    pResult = Dch_DeriveChoiceAig( pAig );
+    pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp );
     // count the number of representatives
     if ( pPars->fVerbose ) 
         Abc_Print( 1, "STATS:  Reprs = %6d.  Equivs = %6d.  Choices = %6d.\n", 
diff --git a/src/proof/dch/dchInt.h b/src/proof/dch/dchInt.h
index 05f4271d..d1dd2c51 100644
--- a/src/proof/dch/dchInt.h
+++ b/src/proof/dch/dchInt.h
@@ -123,7 +123,7 @@ static inline void Dch_ObjSetConst1Cand( Aig_Man_t * pAig, Aig_Obj_t * pObj )
 /*=== dchChoice.c ===================================================*/
 extern int           Dch_DeriveChoiceCountReprs( Aig_Man_t * pAig );
 extern int           Dch_DeriveChoiceCountEquivs( Aig_Man_t * pAig );
-extern Aig_Man_t *   Dch_DeriveChoiceAig( Aig_Man_t * pAig );
+extern Aig_Man_t *   Dch_DeriveChoiceAig( Aig_Man_t * pAig, int fSkipRedSupps );
 /*=== dchClass.c =================================================*/
 extern Dch_Cla_t *   Dch_ClassesStart( Aig_Man_t * pAig );
 extern void          Dch_ClassesSetData( Dch_Cla_t * p, void * pManData,