Version abc61206

4 files changed, 111 insertions, 36 deletions

diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c
index 81d91499..3578139b 100644
--- a/src/base/abc/abcSop.c
+++ b/src/base/abc/abcSop.c
@@ -427,9 +427,9 @@ char * Abc_SopCreateFromIsop( Extra_MmFlex_t * pMan, int nVars, Vec_Int_t * vCov
         {
             Literal = 3 & (Entry >> (k << 1));
             if ( Literal == 1 )
-                pCube[k] = '1';
-            else if ( Literal == 2 )
                 pCube[k] = '0';
+            else if ( Literal == 2 )
+                pCube[k] = '1';
             else if ( Literal != 0 )
                 assert( 0 );
         }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 77ae4d5a..901e1df4 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2034,25 +2034,28 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
-    int nFaninMax, c;
+    int nFaninMax, nCubeMax, c;
     int fUseBdds;
+    int fUseSops;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fUseBdds, int fUseSops, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFaninMax =  8;
+    nFaninMax =  5;
+    nCubeMax  =  5;
     fUseBdds  =  0;
+    fUseSops  =  0;
     fVerbose  =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Fbvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "KCbsvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'F':
+        case 'K':
             if ( globalUtilOptind >= argc )
             {
                 fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
@@ -2063,9 +2066,23 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nFaninMax < 0 ) 
                 goto usage;
             break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nCubeMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nCubeMax < 0 ) 
+                goto usage;
+            break;
         case 'b':
             fUseBdds ^= 1;
             break;
+        case 's':
+            fUseSops ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -2076,6 +2093,12 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
 
+    if ( fUseBdds && fUseSops )
+    {
+        fprintf( pErr, "Cannot optimize both BDDs and SOPs at the same time.\n" );
+        goto usage;
+    }
+
     if ( pNtk == NULL )
     {
         fprintf( pErr, "Empty network.\n" );
@@ -2088,7 +2111,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkRenode( pNtk, nFaninMax, fUseBdds, fVerbose );
+    pNtkRes = Abc_NtkRenode( pNtk, nFaninMax, nCubeMax, fUseBdds, fUseSops, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Renoding has failed.\n" );
@@ -2099,10 +2122,13 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: renode [-F num] [-bv]\n" );
-    fprintf( pErr, "\t          transforms an AIG into a logic network by creating larger nodes\n" );
-    fprintf( pErr, "\t-F num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
-    fprintf( pErr, "\t-b      : toggles cost function (BDD nodes or FF literals) [default = %s]\n", fUseBdds? "BDD nodes": "FF literals" );
+    fprintf( pErr, "usage: renode [-K num] [-C num] [-bsv]\n" );
+    fprintf( pErr, "\t          transforms the AIG into a logic network with larger nodes\n" );
+    fprintf( pErr, "\t          while minimizing the number of FF literals of the node SOPs\n" );
+    fprintf( pErr, "\t-K num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
+    fprintf( pErr, "\t-C num  : the maximum number of cubes used at a node [default = %d]\n", nCubeMax );
+    fprintf( pErr, "\t-b      : toggles minimizing the number of BDD nodes [default = %s]\n", fUseBdds? "yes": "no" );
+    fprintf( pErr, "\t-s      : toggles minimizing the number of SOP cubes [default = %s]\n", fUseSops? "yes": "no" );
     fprintf( pErr, "\t-v      : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
     fprintf( pErr, "\t-h      : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index b76385f8..948a1d77 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -20,6 +20,7 @@
 
 #include "abc.h"
 #include "if.h"
+#include "kit.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -164,6 +165,8 @@ Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk )
     // create the new network
     if ( pIfMan->pPars->fUseBdds )
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    else if ( pIfMan->pPars->fUseSops )
+        pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
     else
         pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_AIG );
     // prepare the mapping manager
@@ -223,7 +226,6 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
     If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, i )
         Abc_ObjAddFanin( pNodeNew, Abc_NodeFromIf_rec(pNtkNew, pIfMan, pIfLeaf) );
     // derive the function of this node
-
     if ( pIfMan->pPars->fTruth )
     {
         if ( pIfMan->pPars->fUseBdds )
@@ -235,20 +237,29 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
             // reorder the fanins to minimize the BDD size
             Abc_NodeBddReorder( pIfMan->pPars->pReoMan, pNodeNew );
         }
-        else
+        else if ( pIfMan->pPars->fUseSops ) 
         {
-            typedef int Kit_Graph_t;
-            extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars );
-            extern Hop_Obj_t * Dec_GraphToNetworkAig( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
-            // transform truth table into the decomposition tree
-            Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), pCutBest->nLimit );
+            Vec_Int_t * vCover = Vec_IntAlloc( 1 << 16 );
+            // transform truth table into the SOP
+            int RetValue = Kit_TruthIsop( If_CutTruth(pCutBest), pCutBest->nLimit, vCover, 0 );
+            assert( RetValue == 0 );
             // derive the AIG for that tree
-            pNodeNew->pData = Dec_GraphToNetworkAig( pNtkNew->pManFunc, pGraph );
+            pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCutBest->nLimit, vCover );
+            Vec_IntFree( vCover );
+        }
+        else 
+        {
+            extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
+            Vec_Int_t * vMemory = Vec_IntAlloc( 1 << 16 );
+            // transform truth table into the decomposition tree
+            Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), pCutBest->nLimit, vMemory );
+            // derive the AIG for the decomposition tree
+            pNodeNew->pData = Kit_GraphToHop( pNtkNew->pManFunc, pGraph );
             Kit_GraphFree( pGraph );
+            Vec_IntFree( vMemory );
         }
     }
     else
-
         pNodeNew->pData = Abc_NodeIfToHop( pNtkNew->pManFunc, pIfMan, pIfObj );
     If_ObjSetCopy( pIfObj, pNodeNew );
     return pNodeNew;
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index a3360953..4f3003a6 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -21,6 +21,7 @@
 #include "abc.h"
 #include "reo.h"
 #include "if.h"
+#include "kit.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -28,13 +29,11 @@
 
 static int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars );
 static int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars );
+static int Abc_NtkRenodeEvalAig( unsigned * pTruth, int nVars );
 
-static reo_man * s_pReo = NULL;
-static DdManager * s_pDd  = NULL;
-
-typedef int Kit_Graph_t;
-extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars );
-extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars );
+static reo_man * s_pReo      = NULL;
+static DdManager * s_pDd     = NULL;
+static Vec_Int_t * s_vMemory = NULL;
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -51,7 +50,7 @@ extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fVerbose )
+Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int fUseBdds, int fUseSops, int fVerbose )
 {
     extern Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
     If_Par_t Pars, * pPars = &Pars;
@@ -77,7 +76,14 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fV
     pPars->pLutLib     =  NULL; // Abc_FrameReadLibLut();
     pPars->pTimesArr   =  NULL; 
     pPars->pTimesArr   =  NULL;   
-    pPars->pFuncCost   =  fUseBdds? Abc_NtkRenodeEvalBdd : Abc_NtkRenodeEvalSop;   
+    pPars->fUseBdds    =  fUseBdds;
+    pPars->fUseSops    =  fUseSops;
+    if ( fUseBdds )
+        pPars->pFuncCost = Abc_NtkRenodeEvalBdd;
+    else if ( fUseSops )
+        pPars->pFuncCost = Abc_NtkRenodeEvalSop;
+    else
+        pPars->pFuncCost = Abc_NtkRenodeEvalAig;
 
     // start the manager
     if ( fUseBdds )
@@ -85,9 +91,13 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fV
         assert( s_pReo == NULL );
         s_pDd  = Cudd_Init( nFaninMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
         s_pReo = Extra_ReorderInit( nFaninMax, 100 );
-        pPars->fUseBdds = 1;
         pPars->pReoMan  = s_pReo;
     }
+    else
+    {
+        assert( s_vMemory == NULL );
+        s_vMemory = Vec_IntAlloc( 1 << 16 );
+    }
 
     // perform mapping/renoding
     pNtkNew = Abc_NtkIf( pNtk, pPars );
@@ -98,14 +108,20 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int fUseBdds, int fV
         Extra_StopManager( s_pDd );
         Extra_ReorderQuit( s_pReo );
         s_pReo = NULL;
-        s_pDd = NULL;
+        s_pDd  = NULL;
+    }
+    else
+    {
+        Vec_IntFree( s_vMemory );
+        s_vMemory = NULL;
     }
+
     return pNtkNew;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Derives the BDD after reordering.]
+  Synopsis    [Computes the cost based on the BDD size after reordering.]
 
   Description []
                
@@ -120,7 +136,8 @@ int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars )
     int nNodes, nSupport;
     bFunc = Kit_TruthToBdd( s_pDd, pTruth, nVars );           Cudd_Ref( bFunc );
     bFuncNew = Extra_Reorder( s_pReo, s_pDd, bFunc, NULL );   Cudd_Ref( bFuncNew );
-    nSupport = Cudd_SupportSize( s_pDd, bFuncNew );
+//    nSupport = Cudd_SupportSize( s_pDd, bFuncNew );
+    nSupport = 1;
     nNodes = Cudd_DagSize( bFuncNew );
     Cudd_RecursiveDeref( s_pDd, bFuncNew );
     Cudd_RecursiveDeref( s_pDd, bFunc );
@@ -129,7 +146,7 @@ int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars )
 
 /**Function*************************************************************
 
-  Synopsis    [Derives the BDD after reordering.]
+  Synopsis    [Computes the cost based on ISOP.]
 
   Description []
                
@@ -140,11 +157,32 @@ int Abc_NtkRenodeEvalBdd( unsigned * pTruth, int nVars )
 ***********************************************************************/
 int Abc_NtkRenodeEvalSop( unsigned * pTruth, int nVars )
 {
+    int nCubes, RetValue;
+    RetValue = Kit_TruthIsop( pTruth, nVars, s_vMemory, 0 );
+    assert( RetValue == 0 );
+    nCubes = Vec_IntSize( s_vMemory );
+    return (1 << 16) | nCubes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the cost based on the factored form.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkRenodeEvalAig( unsigned * pTruth, int nVars )
+{
     Kit_Graph_t * pGraph;
     int nNodes, nDepth;
-    pGraph = Kit_TruthToGraph( pTruth, nVars );
+    pGraph = Kit_TruthToGraph( pTruth, nVars, s_vMemory );
     nNodes = Kit_GraphNodeNum( pGraph );
-    nDepth = Kit_GraphLevelNum( pGraph );
+//    nDepth = Kit_GraphLevelNum( pGraph );
+    nDepth = 1;
     Kit_GraphFree( pGraph );
     return (nDepth << 16) | nNodes;
 }