Version abc90410

5 files changed, 71 insertions, 26 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c48b7e95..8ac8b241 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -9515,7 +9515,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, "WCSsptvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -9561,6 +9561,12 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             pPars->fSimulateTfo ^= 1;
             break;
+        case 'g':
+            pPars->fUseGia ^= 1;
+            break;
+        case 'c':
+            pPars->fUseCSat ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -9591,7 +9597,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dch [-WCS num] [-sptvh]\n" );
+    fprintf( pErr, "usage: dch [-WCS num] [-sptgcvh]\n" );
     fprintf( pErr, "\t         computes structural choices using a new approach\n" );
     fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@@ -9599,6 +9605,8 @@ usage:
     fprintf( pErr, "\t-s     : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
     fprintf( pErr, "\t-p     : toggle power-aware rewriting [default = %s]\n", pPars->fPower? "yes": "no" );
     fprintf( pErr, "\t-t     : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
+    fprintf( pErr, "\t-g     : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" );
+    fprintf( pErr, "\t-c     : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -21820,6 +21828,7 @@ usage:
 int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+    extern Aig_Man_t * Abc_NtkToDarChoices( Abc_Ntk_t * pNtk );
     Gia_Man_t * pAig;
     Aig_Man_t * pMan;
     int c, fVerbose = 0;
@@ -21845,12 +21854,15 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "The current network should be strashed.\n" );
         return 1;
     }
+//    if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) )
+//    {
+//        printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pAbc->pNtkCur) );
+//        Abc_AigCleanup(pAbc->pNtkCur->pManFunc);
+//    }
     if ( Abc_NtkGetChoiceNum(pAbc->pNtkCur) )
-    {
-        printf( "Removing %d choices from the AIG.\n", Abc_NtkGetChoiceNum(pAbc->pNtkCur) );
-        Abc_AigCleanup(pAbc->pNtkCur->pManFunc);
-    }
-    pMan = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
+        pMan = Abc_NtkToDarChoices( pAbc->pNtkCur );
+    else
+        pMan = Abc_NtkToDar( pAbc->pNtkCur, 0, 1 );
     pAig = Gia_ManFromAig( pMan );
     Aig_ManStop( pMan );
     if ( pAig == NULL )
@@ -21886,6 +21898,7 @@ usage:
 int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+    extern Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan );
     Aig_Man_t * pMan;
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
@@ -21917,9 +21930,27 @@ int Abc_CommandAbc9Put( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Empty network.\n" );
         return 1;
     }
-    pMan = Gia_ManToAig( pAbc->pAig );
-    pNtk = Abc_NtkFromAigPhase( pMan );
-    Aig_ManStop( pMan );
+    if ( Gia_ManHasDandling(pAbc->pAig) == 0 )
+    {
+        pMan = Gia_ManToAig( pAbc->pAig, 0 );
+        pNtk = Abc_NtkFromAigPhase( pMan );
+        Aig_ManStop( pMan );
+    }
+    else
+    {
+        Abc_Ntk_t * pNtkNoCh;
+//        printf( "Transforming AIG with %d choice nodes.\n", Gia_ManEquivCountClasses(pAbc->pAig) );
+        // create network without choices
+        pMan = Gia_ManToAig( pAbc->pAig, 0 );
+        pNtkNoCh = Abc_NtkFromAigPhase( pMan );
+        pNtkNoCh->pName = Extra_UtilStrsav(pMan->pName);
+        Aig_ManStop( pMan );
+        // derive network with choices
+        pMan = Gia_ManToAig( pAbc->pAig, 1 );
+        pNtk = Abc_NtkFromDarChoices( pNtkNoCh, pMan );
+        Abc_NtkDelete( pNtkNoCh );
+        Aig_ManStop( pMan );
+    }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
     return 0;
@@ -22204,7 +22235,7 @@ int Abc_CommandAbc9Show( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Show(): There is no AIG.\n" );
         return 1;
     } 
-    pMan = Gia_ManToAig( pAbc->pAig );
+    pMan = Gia_ManToAig( pAbc->pAig, 0 );
     Aig_ManShow( pMan, 0, NULL );
     Aig_ManStop( pMan );
     return 0;
@@ -23400,7 +23431,7 @@ usage:
     fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
     fprintf( stdout, "\t-f     : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
-    fprintf( stdout, "\t-r     : toggle using implication rings for equivalence classes [default = %s]\n", pPars->fUseRings? "yes": "no" );
+    fprintf( stdout, "\t-r     : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
     fprintf( stdout, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
@@ -23425,7 +23456,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Cec_ManCorSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCfrecvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23457,6 +23488,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             pPars->fUseRings ^= 1;
             break;
+        case 'e':
+            pPars->fMakeChoices ^= 1;
+            break;
         case 'c':
             pPars->fUseCSat ^= 1;
             break;
@@ -23483,12 +23517,13 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &scorr [-FC num] [-frcvh]\n" );
+    fprintf( stdout, "usage: &scorr [-FC num] [-frecvh]\n" );
     fprintf( stdout, "\t         performs signal correpondence computation\n" );
     fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     fprintf( stdout, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
     fprintf( stdout, "\t-f     : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
-    fprintf( stdout, "\t-r     : toggle using implication rings for equivalence classes [default = %s]\n", pPars->fUseRings? "yes": "no" );
+    fprintf( stdout, "\t-r     : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
+    fprintf( stdout, "\t-e     : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
     fprintf( stdout, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
@@ -23513,7 +23548,7 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Cec_ManChcSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Cvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Ccvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23528,6 +23563,9 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nBTLimit < 0 ) 
                 goto usage;
             break;
+        case 'c':
+            pPars->fUseCSat ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -23540,8 +23578,6 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Choice(): There is no AIG.\n" );
         return 1;
     } 
-    printf("The command is not yet ready.\n" );
-    return 0;
     pAbc->pAig = Cec_ManChoiceComputation( pTemp = pAbc->pAig, pPars );
     if ( pAbc->pAig == NULL )
     {
@@ -23553,9 +23589,10 @@ int Abc_CommandAbc9Choice( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &choice [-C num] [-vh]\n" );
+    fprintf( stdout, "usage: &choice [-C num] [-cvh]\n" );
     fprintf( stdout, "\t         performs computation of structural choices\n" );
     fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
+    fprintf( stdout, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 48c2f8e0..cc97796f 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -586,7 +586,7 @@ Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk )
     Abc_Obj_t * pObj;//, * pTemp;
     int i;//, k;
     int nNodesTotal = 0, nMffcsTotal = 0;
-    extern Vec_Ptr_t * Abc_NodeMffsInsideCollect( Abc_Obj_t * pNode );
+    extern Vec_Ptr_t * Abc_NodeMffcInsideCollect( Abc_Obj_t * pNode );
 
     vAttrs = Vec_IntStart( Abc_NtkObjNumMax(pNtk) + 1 );
 //    Abc_NtkForEachCi( pNtk, pObj, i )
@@ -615,7 +615,7 @@ Vec_Int_t * Abc_NtkGetNodeAttributes( Abc_Ntk_t * pNtk )
     {
         if ( Vec_IntEntry( vAttrs, pObj->Id ) )
         {
-            vNodes = Abc_NodeMffsInsideCollect( pObj );
+            vNodes = Abc_NodeMffcInsideCollect( pObj );
             Vec_PtrForEachEntry( vNodes, pTemp, k )
                 if ( pTemp != pObj )
                     Vec_IntWriteEntry( vAttrs, pTemp->Id, 0 );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 840068d6..a5973153 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -896,6 +896,7 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
 Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
 {
     extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
+    extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
 
     Vec_Ptr_t * vAigs;
     Aig_Man_t * pMan, * pTemp;
@@ -911,6 +912,10 @@ clk = clock();
 //        vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fVerbose );
         vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 );
         Aig_ManStop( pMan );
+        // swap around the first and the last
+        pTemp = Vec_PtrPop( vAigs );
+        Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
+        Vec_PtrWriteEntry( vAigs, 0, pTemp );
     }
     else
     {
@@ -918,7 +923,10 @@ clk = clock();
         Vec_PtrPush( vAigs, pMan );
     }
 pPars->timeSynth = clock() - clk;
-    pMan = Dch_ComputeChoices( vAigs, pPars );
+    if ( pPars->fUseGia )
+        pMan = Cec_ComputeChoices( vAigs, pPars );
+    else
+        pMan = Dch_ComputeChoices( vAigs, pPars );
     pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
 //    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
     Aig_ManStop( pMan );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index d47dfe1f..10e3ba2d 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -704,9 +704,9 @@ void Abc_NtkPrintMffc( FILE * pFile, Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pNode;
     int i;
-    extern void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode );
+    extern void Abc_NodeMffcConeSuppPrint( Abc_Obj_t * pNode );
     Abc_NtkForEachNode( pNtk, pNode, i )
-        Abc_NodeMffsConeSuppPrint( pNode );
+        Abc_NodeMffcConeSuppPrint( pNode );
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index 861a5e66..655f158e 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -1624,7 +1624,7 @@ void Abc_ManResubCleanup( Abc_ManRes_t * p )
 ***********************************************************************/
 Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps, bool fUpdateLevel, bool fVerbose )
 {
-    extern int Abc_NodeMffsInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside );
+    extern int Abc_NodeMffcInside( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vInside );
     Dec_Graph_t * pGraph;
     int Required;
     int clk;
@@ -1639,7 +1639,7 @@ Dec_Graph_t * Abc_ManResubEval( Abc_ManRes_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t *
 
     // collect the MFFC
 clk = clock();
-    p->nMffc = Abc_NodeMffsInside( pRoot, vLeaves, p->vTemp );
+    p->nMffc = Abc_NodeMffcInside( pRoot, vLeaves, p->vTemp );
 p->timeMffc += clock() - clk;
     assert( p->nMffc > 0 );