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

5 files changed, 70 insertions, 10 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1196cc84..940e2643 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10408,7 +10408,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Dch_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcfvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcfrvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10463,6 +10463,9 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             pPars->fLightSynth ^= 1;
             break;
+        case 'r':
+            pPars->fSkipRedSupp ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -10493,7 +10496,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: dch [-WCS num] [-sptgcfvh]\n" );
+    Abc_Print( -2, "usage: dch [-WCS num] [-sptgcfrvh]\n" );
     Abc_Print( -2, "\t         computes structural choices using a new approach\n" );
     Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@@ -10504,6 +10507,7 @@ usage:
     Abc_Print( -2, "\t-g     : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" );
     Abc_Print( -2, "\t-f     : toggle using faster logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
+    Abc_Print( -2, "\t-r     : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
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,