Version abc80212

11 files changed, 58 insertions, 22 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 1124c2fb..9d9bf22a 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -522,7 +522,7 @@ extern Vec_Ptr_t *     Aig_ManSupportsInverse( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps );
 extern Vec_Ptr_t *     Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize );
 extern Vec_Ptr_t *     Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize );
-extern Aig_Man_t *     Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int fVerbose );
+extern Aig_Man_t *     Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose );
 /*=== aigRepr.c =========================================================*/
 extern void            Aig_ManReprStart( Aig_Man_t * p, int nIdMax );
 extern void            Aig_ManReprStop( Aig_Man_t * p );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index edf51a2e..9afc5f91 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -904,11 +904,11 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int fVerbose )
+Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose )
 {
 //    extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
 //    extern void * Abc_FrameGetGlobalFrame();
-    extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
+    extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
 
     Vec_Ptr_t * vOutsTotal, * vOuts;
     Aig_Man_t * pAigTotal, * pAigPart, * pAig;
@@ -972,7 +972,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int fVer
             i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), 
             Aig_ManNodeNum(pAigPart), Aig_ManLevelNum(pAigPart) );
         // compute equivalence classes (to be stored in pNew->pReprs)
-        pAig = Fra_FraigChoice( pAigPart, 1000 );
+        pAig = Fra_FraigChoice( pAigPart, nConfMax, nLevelMax );
         Aig_ManStop( pAig );
         // reset the pData pointers
         Aig_ManForEachObj( pAigPart, pObj, k )
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 5ee6c9af..3a7e382c 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -429,7 +429,6 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
         pRepr = Aig_ObjFindRepr( p, pObj );
         if ( pRepr == NULL )
             continue;
-        assert( pObj->nRefs == 0 );
         // skip constant and PI classes
         if ( !Aig_ObjIsNode(pRepr) )
         {
@@ -444,6 +443,7 @@ void Aig_ManMarkValidChoices( Aig_Man_t * p )
         }
 //printf( "Node %d is represented by node %d.\n", pObj->Id, pRepr->Id );
         // add choice to the choice node
+        assert( pObj->nRefs == 0 );
         p->pEquivs[pObj->Id] = p->pEquivs[pRepr->Id];
         p->pEquivs[pRepr->Id] = pObj;
     }
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 72e7d3d1..c4c7db0a 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -92,7 +92,7 @@ extern Aig_Man_t *     Dar_ManRewriteDefault( Aig_Man_t * pAig );
 extern Aig_Man_t *     Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
 extern Aig_Man_t *     Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
 extern Aig_Man_t *     Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
-extern Aig_Man_t *     Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
+extern Aig_Man_t *     Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 530e913e..e690a61b 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -353,7 +353,7 @@ Vec_Ptr_t * Dar_ManChoiceSynthesisExt()
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose )
+Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose )
 {
     Aig_Man_t * pMan, * pTemp;
     Vec_Ptr_t * vAigs;
@@ -374,7 +374,7 @@ if ( fVerbose )
 PRT( "Synthesis time", clock() - clk );
 }
 clk = clock();
-    pMan = Aig_ManChoicePartitioned( vAigs, 300, fVerbose );
+    pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
     Vec_PtrForEachEntry( vAigs, pTemp, i )
         Aig_ManStop( pTemp );
     Vec_PtrFree( vAigs );
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 64268358..2ee84f39 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -73,6 +73,7 @@ struct Fra_Par_t_
     int              fConeBias;         // bias variables in the cone (good for unsat runs)
     int              nBTLimitNode;      // conflict limit at a node
     int              nBTLimitMiter;     // conflict limit at an output
+    int              nLevelMax;         // the max level to consider seriously
     int              nFramesP;          // the number of timeframes to in the prefix
     int              nFramesK;          // the number of timeframes to unroll
     int              nMaxImps;          // the maximum number of implications to consider
@@ -266,7 +267,7 @@ extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
 extern int                 Fra_FraigMiterStatus( Aig_Man_t * p );
 extern int                 Fra_FraigMiterAssertedOutput( Aig_Man_t * p );
 extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
-extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
+extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
 extern Aig_Man_t *         Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax, int fProve );
 /*=== fraHot.c ========================================================*/
 extern Vec_Int_t *         Fra_OneHotCompute( Fra_Man_t * p, Fra_Sml_t * pSim );
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 0157421b..0a81105b 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -303,6 +303,7 @@ void Fra_FraigSweep( Fra_Man_t * p )
 //    Bar_Progress_t * pProgress = NULL;
     Aig_Obj_t * pObj, * pObjNew;
     int i, Pos = 0;
+    int nBTracksOld;
     // fraig latch outputs
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
     {
@@ -315,6 +316,7 @@ void Fra_FraigSweep( Fra_Man_t * p )
     // fraig internal nodes
 //    if ( !p->pPars->fDontShowBar )
 //        pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) );
+    nBTracksOld = p->pPars->nBTLimitNode;
     Aig_ManForEachNode( p->pManAig, pObj, i )
     {
 //        if ( pProgress )
@@ -327,7 +329,12 @@ void Fra_FraigSweep( Fra_Man_t * p )
         if ( p->pManFraig->pData )
             continue;
         // perform fraiging
+        if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
+            p->pPars->nBTLimitNode = 5;
         Fra_FraigNode( p, pObj );
+        if ( p->pPars->nLevelMax && (int)pObj->Level > p->pPars->nLevelMax )
+            p->pPars->nBTLimitNode = nBTracksOld;
+        // check implications
         if ( p->pPars->fUseImps )
             Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
     }
@@ -382,7 +389,7 @@ clk = clock();
     // finalize the fraiged manager
     Fra_ManFinalizeComb( p );
     if ( p->pPars->fChoicing )
-    {
+    { 
 int clk2 = clock();
         Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
         pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
@@ -419,7 +426,7 @@ p->timeTotal = clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
+Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax )
 {
     Fra_Par_t Pars, * pPars = &Pars; 
     Fra_ParamsDefault( pPars );
@@ -430,6 +437,7 @@ Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
     pPars->fProve       = 0;
     pPars->fVerbose     = 0;
     pPars->fDontShowBar = 1;
+    pPars->nLevelMax    = nLevelMax;
     return Fra_FraigPerform( pManAig, pPars );
 }
  
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 3e0fca6a..a43d83b1 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -211,8 +211,8 @@ PRT( "Time", clock() - clk );
         } 
 
         // perform retiming
-//        if ( fRetimeFirst && pNew->nRegs )
-        if ( pNew->nRegs )
+        if ( fRetimeFirst && pNew->nRegs )
+//        if ( pNew->nRegs )
         {
 clk = clock();
         pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index 4079b6ed..46dddab2 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2009,9 +2009,9 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld )
     if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node
          (!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node
     {
-        assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
-        assert( pObjNew != Ivy_Regular(pFanin0New) );
-        assert( pObjNew != Ivy_Regular(pFanin1New) );
+//        assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) );
+//        assert( pObjNew != Ivy_Regular(pFanin0New) );
+//        assert( pObjNew != Ivy_Regular(pFanin1New) );
         return pObjNew;
     }
     // get the fraiged representative
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4b872aa3..31c09fd2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7675,8 +7675,9 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int fBalance, fVerbose, fUpdateLevel, c;
+    int nConfMax, nLevelMax;
 
-    extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -7685,12 +7686,36 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     fBalance     = 1;
     fUpdateLevel = 1;
+    nConfMax     = 1000;
+    nLevelMax    = 0;
     fVerbose     = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "blvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CLblvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfMax < 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nLevelMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nLevelMax < 0 ) 
+                goto usage;
+            break;
         case 'b':
             fBalance ^= 1;
             break;
@@ -7716,7 +7741,7 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "This command works only for strashed networks.\n" );
         return 1;
     }
-    pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, fVerbose );
+    pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -7727,8 +7752,10 @@ int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dchoice [-blvh]\n" );
+    fprintf( pErr, "usage: dchoice [-C num] [-L num] [-blvh]\n" );
     fprintf( pErr, "\t         performs partitioned choicing using a new AIG package\n" );
+    fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nConfMax );
+    fprintf( pErr, "\t-L num : the max level of nodes to consider (0 = not used) [default = %d]\n", nLevelMax );
     fprintf( pErr, "\t-b     : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index d703cfc4..6c5cabce 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -720,7 +720,7 @@ clk = clock();
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose )
+Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int nConfMax, int nLevelMax, int fVerbose )
 {
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
@@ -728,7 +728,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
     pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
-    pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fVerbose );
+    pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, nConfMax, nLevelMax, fVerbose );
     Aig_ManStop( pTemp );
     pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
     Aig_ManStop( pMan );