Version abc50902

4 files changed, 82 insertions, 173 deletions

diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index b9bab47f..6d1a6c06 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -63,7 +63,7 @@ struct Rwr_Man_t_
     int                nClasses;         // the number of NN classes
     // the result of resynthesis
     int                fCompl;           // indicates if the output of FF should be complemented
-    Vec_Int_t *        vForm;            // the decomposition tree (temporary)
+    void *             pGraph;            // the decomposition tree (temporary)
     Vec_Ptr_t *        vFanins;          // the fanins array (temporary)
     Vec_Ptr_t *        vFaninsCur;       // the fanins array (temporary)
     Vec_Int_t *        vLevNums;         // the array of levels (temporary)
@@ -125,8 +125,7 @@ extern void              Rwr_ManIncTravId( Rwr_Man_t * p );
 extern Rwr_Man_t *       Rwr_ManStart( bool fPrecompute );
 extern void              Rwr_ManStop( Rwr_Man_t * p );
 extern void              Rwr_ManPrintStats( Rwr_Man_t * p );
-extern Vec_Ptr_t *       Rwr_ManReadFanins( Rwr_Man_t * p );
-extern Vec_Int_t *       Rwr_ManReadDecs( Rwr_Man_t * p );
+extern void *            Rwr_ManReadDecs( Rwr_Man_t * p );
 extern int               Rwr_ManReadCompl( Rwr_Man_t * p );
 extern void              Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time );
 extern void              Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time );
diff --git a/src/opt/rwr/rwrDec.c b/src/opt/rwr/rwrDec.c
index 9cfc9659..d072879d 100644
--- a/src/opt/rwr/rwrDec.c
+++ b/src/opt/rwr/rwrDec.c
@@ -19,15 +19,14 @@
 ***********************************************************************/
 
 #include "rwr.h"
-#include "ft.h"
+#include "dec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Vec_Int_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode );
-static int         Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Vec_Int_t * vForm );
-static void        Rwr_FactorVerify( Vec_Int_t * vForm, unsigned uTruth );
+static Dec_Graph_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode );
+static Dec_Edge_t    Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Dec_Graph_t * pGraph );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -46,6 +45,7 @@ static void        Rwr_FactorVerify( Vec_Int_t * vForm, unsigned uTruth );
 ***********************************************************************/
 void Rwr_ManPreprocess( Rwr_Man_t * p )
 {
+    Dec_Graph_t * pGraph;
     Rwr_Node_t * pNode;
     int i, k;
     // put the nodes into the structure
@@ -62,9 +62,13 @@ void Rwr_ManPreprocess( Rwr_Man_t * p )
             Vec_VecPush( p->vClasses, p->pMap[pNode->uTruth], pNode );
         }
     }
-    // compute decomposition forms for each node
+    // compute decomposition forms for each node and verify them
     Vec_VecForEachEntry( p->vClasses, pNode, i, k )
-        pNode->pNext = (Rwr_Node_t *)Rwr_NodePreprocess( p, pNode );
+    {
+        pGraph = Rwr_NodePreprocess( p, pNode );
+        pNode->pNext = (Rwr_Node_t *)pGraph;
+        assert( pNode->uTruth == (Dec_GraphDeriveTruth(pGraph) & 0xFFFF) );
+    }
 }
 
 /**Function*************************************************************
@@ -78,28 +82,24 @@ void Rwr_ManPreprocess( Rwr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode )
+Dec_Graph_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode )
 {
-    Vec_Int_t * vForm;
-    int i, Root;
+    Dec_Graph_t * pGraph;
+    Dec_Edge_t eRoot;
+    assert( !Rwr_IsComplement(pNode) );
     // consider constant
     if ( pNode->uTruth == 0 )
-        return Ft_FactorConst( 0 );
+        return Dec_GraphCreateConst0();
     // consider the case of elementary var
     if ( pNode->uTruth == 0x00FF )
-        return Ft_FactorVar( 3, 4, 1 );
-    // start the factored form
-    vForm = Vec_IntAlloc( 10 );
-    for ( i = 0; i < 4; i++ )
-        Vec_IntPush( vForm, 0 );
+        return Dec_GraphCreateLeaf( 3, 4, 1 );
+    // start the subgraphs
+    pGraph = Dec_GraphCreate( 4 );
     // collect the nodes
     Rwr_ManIncTravId( p );
-    Root = Rwr_TravCollect_rec( p, pNode, vForm );
-    if ( Root & 1 )
-        Ft_FactorComplement( vForm );
-    // verify the factored form
-    Rwr_FactorVerify( vForm, pNode->uTruth );
-    return vForm;
+    eRoot = Rwr_TravCollect_rec( p, pNode, pGraph );
+    Dec_GraphSetRoot( pGraph, eRoot );
+    return pGraph;
 }
 
 /**Function*************************************************************
@@ -113,115 +113,31 @@ Vec_Int_t * Rwr_NodePreprocess( Rwr_Man_t * p, Rwr_Node_t * pNode )
   SeeAlso     []
 
 ***********************************************************************/
-int Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Vec_Int_t * vForm )
+Dec_Edge_t Rwr_TravCollect_rec( Rwr_Man_t * p, Rwr_Node_t * pNode, Dec_Graph_t * pGraph )
 {
-    Ft_Node_t Node, NodeA, NodeB;
-    int Node0, Node1;
+    Dec_Edge_t eNode0, eNode1, eNode;
     // elementary variable
     if ( pNode->fUsed )
-        return ((pNode->Id - 1) << 1); 
+        return Dec_EdgeCreate( pNode->Id - 1, 0 );
     // previously visited node
     if ( pNode->TravId == p->nTravIds )
-        return pNode->Volume;
+        return Dec_IntToEdge( pNode->Volume );
     pNode->TravId = p->nTravIds;
     // solve for children
-    Node0 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p0), vForm );
-    Node1 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p1), vForm );
+    eNode0 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p0), pGraph );
+    if ( Rwr_IsComplement(pNode->p0) )    
+        eNode0.fCompl = !eNode0.fCompl;
+    eNode1 = Rwr_TravCollect_rec( p, Rwr_Regular(pNode->p1), pGraph );
+    if ( Rwr_IsComplement(pNode->p1) )    
+        eNode1.fCompl = !eNode1.fCompl;
     // create the decomposition node(s)
     if ( pNode->fExor )
-    {
-        assert( !Rwr_IsComplement(pNode->p0) );
-        assert( !Rwr_IsComplement(pNode->p1) );
-        NodeA.fIntern = 1;
-        NodeA.fConst  = 0;
-        NodeA.fCompl  = 0;
-        NodeA.fCompl0 = !(Node0 & 1);
-        NodeA.fCompl1 =  (Node1 & 1);
-        NodeA.iFanin0 = (Node0 >> 1);
-        NodeA.iFanin1 = (Node1 >> 1);
-        Vec_IntPush( vForm, Ft_Node2Int(NodeA) );
-
-        NodeB.fIntern = 1;
-        NodeB.fConst  = 0;
-        NodeB.fCompl  = 0;
-        NodeB.fCompl0 =  (Node0 & 1);
-        NodeB.fCompl1 = !(Node1 & 1);
-        NodeB.iFanin0 = (Node0 >> 1);
-        NodeB.iFanin1 = (Node1 >> 1);
-        Vec_IntPush( vForm, Ft_Node2Int(NodeB) );
-
-        Node.fIntern = 1;
-        Node.fConst  = 0;
-        Node.fCompl  = 0;
-        Node.fCompl0 = 1;
-        Node.fCompl1 = 1;
-        Node.iFanin0 = vForm->nSize - 2;
-        Node.iFanin1 = vForm->nSize - 1;
-        Vec_IntPush( vForm, Ft_Node2Int(Node) );
-    }
+        eNode = Dec_GraphAddNodeXor( pGraph, eNode0, eNode1 );
     else
-    {
-        Node.fIntern = 1;
-        Node.fConst  = 0;
-        Node.fCompl  = 0;
-        Node.fCompl0 = Rwr_IsComplement(pNode->p0) ^ (Node0 & 1);
-        Node.fCompl1 = Rwr_IsComplement(pNode->p1) ^ (Node1 & 1);
-        Node.iFanin0 = (Node0 >> 1);
-        Node.iFanin1 = (Node1 >> 1);
-        Vec_IntPush( vForm, Ft_Node2Int(Node) );
-    }
-    // save the number of this node
-    pNode->Volume = ((vForm->nSize - 1) << 1) | pNode->fExor;
-    return pNode->Volume;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Verifies the factored form.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Rwr_FactorVerify( Vec_Int_t * vForm, unsigned uTruthGold )
-{
-    Ft_Node_t * pFtNode;
-    Vec_Int_t * vTruths;
-    unsigned uTruth, uTruth0, uTruth1;
-    int i;
-
-    vTruths = Vec_IntAlloc( vForm->nSize );
-    Vec_IntPush( vTruths, 0xAAAA );
-    Vec_IntPush( vTruths, 0xCCCC );
-    Vec_IntPush( vTruths, 0xF0F0 );
-    Vec_IntPush( vTruths, 0xFF00 );
-
-    assert( Ft_FactorGetNumVars( vForm ) == 4 );
-    for ( i = 4; i < vForm->nSize; i++ )
-    {
-        pFtNode = Ft_NodeRead( vForm, i );
-        // make sure there are no elementary variables
-        assert( pFtNode->iFanin0 != pFtNode->iFanin1 );
-
-        uTruth0 = vTruths->pArray[pFtNode->iFanin0];
-        uTruth0 = pFtNode->fCompl0? ~uTruth0 : uTruth0;
-
-        uTruth1 = vTruths->pArray[pFtNode->iFanin1];
-        uTruth1 = pFtNode->fCompl1? ~uTruth1 : uTruth1;
-
-        uTruth = uTruth0 & uTruth1;
-        Vec_IntPush( vTruths, uTruth );
-    }
-    // complement if necessary
-    if ( pFtNode->fCompl )
-        uTruth = ~uTruth;
-    uTruth &= 0xFFFF;
-    if ( uTruth != uTruthGold )
-        printf( "Verification failed\n" );
-    Vec_IntFree( vTruths );
+        eNode = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
+    // save the result
+    pNode->Volume = Dec_EdgeToInt( eNode );
+    return eNode;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c
index 735232af..c934dfd8 100644
--- a/src/opt/rwr/rwrEva.c
+++ b/src/opt/rwr/rwrEva.c
@@ -19,13 +19,13 @@
 ***********************************************************************/
 
 #include "rwr.h"
-#include "ft.h"
+#include "dec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest );
+static Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFITIONS                           ///
@@ -40,8 +40,8 @@ static Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t
   structures precomputed and stored in the RWR manager. 
   Determines the best rewriting and computes the gain in the number of AIG
   nodes in the final network. In the end, p->vFanins contains information 
-  about the best cut that can be used for rewriting, while p->vForm gives 
-  the decomposition tree (represented using factored form data structure).
+  about the best cut that can be used for rewriting, while p->pGraph gives 
+  the decomposition dag (represented using decomposition graph data structure).
   Returns gain in the number of nodes or -1 if node cannot be rewritten.]
                
   SideEffects []
@@ -52,14 +52,14 @@ static Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t
 int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros )
 {
     int fVeryVerbose = 0;
-    Vec_Int_t * vForm;
+    Dec_Graph_t * pGraph;
     Cut_Cut_t * pCut;
     Abc_Obj_t * pFanin;
     unsigned uPhase, uTruthBest;
     char * pPerm;
     int Required, nNodesSaved;
     int i, GainCur, GainBest = -1;
-    int clk;
+    int clk, clk2;
 
     p->nNodesConsidered++;
     // get the required times
@@ -109,14 +109,16 @@ clk = clock();
             Abc_ObjRegular(pFanin)->vFanouts.nSize--;
 
         // evaluate the cut
-        vForm = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur );
+clk2 = clock();
+        pGraph = Rwr_CutEvaluate( p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur );
+p->timeEval += clock() - clk2;
 
         // check if the cut is better than the current best one
-        if ( vForm != NULL && GainBest < GainCur )
+        if ( pGraph != NULL && GainBest < GainCur )
         {
             // save this form
             GainBest  = GainCur;
-            p->vForm  = vForm;
+            p->pGraph  = pGraph;
             p->fCompl = ((uPhase & (1<<4)) > 0);
             uTruthBest = pCut->uTruth;
             // collect fanins in the
@@ -127,8 +129,12 @@ clk = clock();
     }
 p->timeRes += clock() - clk;
 
-    if ( GainBest == -1 || GainBest == 0 && !fUseZeros )
-        return GainBest;
+    if ( GainBest == -1 )
+        return -1;
+
+    // copy the leaves
+    Vec_PtrForEachEntry( p->vFanins, pFanin, i )
+        Dec_GraphNode(p->pGraph, i)->pFunc = pFanin;
 
     p->nScores[p->pMap[uTruthBest]]++;
     p->nNodesRewritten++;
@@ -139,7 +145,7 @@ p->timeRes += clock() - clk;
     {
         printf( "Node %6s :   ", Abc_ObjName(pNode) );
         printf( "Fanins = %d. ", p->vFanins->nSize );
-        printf( "Cone = %2d.  ", p->vForm->nSize - 4 );
+        printf( "Cone = %2d.  ", Dec_GraphNodeNum(p->pGraph) );
         printf( "GAIN = %2d.  ", GainBest );
         printf( "\n" );
     }
@@ -157,37 +163,40 @@ p->timeRes += clock() - clk;
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest )
+Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest )
 {
     Vec_Ptr_t * vSubgraphs;
-    Vec_Int_t * vFormBest;
-    Rwr_Node_t * pNode;
-    int nNodesAdded, GainBest = -1, i;
-    int clk = clock();
+    Dec_Graph_t * pGraphBest, * pGraphCur;
+    Rwr_Node_t * pNode, * pFanin;
+    int nNodesAdded, GainBest, i, k;
     // find the matching class of subgraphs
     vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[pCut->uTruth] );
     p->nSubgraphs += vSubgraphs->nSize;
     // determine the best subgraph
+    GainBest = -1;
     Vec_PtrForEachEntry( vSubgraphs, pNode, i )
     {
+        // get the current graph
+        pGraphCur = (Dec_Graph_t *)pNode->pNext;
+        // copy the leaves
+        Vec_PtrForEachEntry( vFaninsCur, pFanin, k )
+            Dec_GraphNode(pGraphCur, k)->pFunc = pFanin;
         // detect how many unlabeled nodes will be reused
-        nNodesAdded = Abc_NodeStrashDecCount( pRoot->pNtk->pManFunc, pRoot, vFaninsCur, 
-            (Vec_Int_t *)pNode->pNext, p->vLevNums, nNodesSaved, LevelMax );
+        nNodesAdded = Dec_GraphToNetworkCount( pRoot, pGraphCur, nNodesSaved, LevelMax );
         if ( nNodesAdded == -1 )
             continue;
         assert( nNodesSaved >= nNodesAdded );
         // count the gain at this node
         if ( GainBest < nNodesSaved - nNodesAdded )
         {
-            GainBest  = nNodesSaved - nNodesAdded;
-            vFormBest = (Vec_Int_t *)pNode->pNext;
+            GainBest   = nNodesSaved - nNodesAdded;
+            pGraphBest = pGraphCur;
         }
     }
-p->timeEval += clock() - clk;
     if ( GainBest == -1 )
         return NULL;
     *pGainBest = GainBest;
-    return vFormBest;
+    return pGraphBest;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c
index d4772812..e7d6fec6 100644
--- a/src/opt/rwr/rwrMan.c
+++ b/src/opt/rwr/rwrMan.c
@@ -19,6 +19,8 @@
 ***********************************************************************/
 
 #include "rwr.h"
+#include "main.h"
+#include "dec.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -41,15 +43,18 @@
 ***********************************************************************/
 Rwr_Man_t * Rwr_ManStart( bool fPrecompute )
 {
+    Dec_Man_t * pManDec;
     Rwr_Man_t * p;
     int clk = clock();
+clk = clock();
     p = ALLOC( Rwr_Man_t, 1 );
     memset( p, 0, sizeof(Rwr_Man_t) );
     p->nFuncs = (1<<16);
-    // canonical forms, phases, perms
-clk = clock();
-    Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap );
-//PRT( "NPN classes precomputation time", clock() - clk ); 
+    pManDec   = Abc_FrameReadManDec(Abc_FrameGetGlobalFrame());
+    p->puCanons = pManDec->puCanons; 
+    p->pPhases  = pManDec->pPhases; 
+    p->pPerms   = pManDec->pPerms; 
+    p->pMap     = pManDec->pMap; 
     // initialize practical NPN classes
     p->pPractical  = Rwr_ManGetPractical( p );
     // create the table
@@ -104,7 +109,7 @@ void Rwr_ManStop( Rwr_Man_t * p )
         Rwr_Node_t * pNode;
         int i, k;
         Vec_VecForEachEntry( p->vClasses, pNode, i, k )
-            Vec_IntFree( (Vec_Int_t *)pNode->pNext );
+            Dec_GraphFree( (Dec_Graph_t *)pNode->pNext );
     }
     if ( p->vClasses )  Vec_VecFree( p->vClasses );
     Vec_PtrFree( p->vForest );
@@ -115,10 +120,6 @@ void Rwr_ManStop( Rwr_Man_t * p )
     free( p->pTable );
     free( p->pPractical );
     free( p->pPerms4 );
-    free( p->puCanons );
-    free( p->pPhases );
-    free( p->pPerms );
-    free( p->pMap );
     free( p );
 }
 
@@ -173,25 +174,9 @@ void Rwr_ManPrintStats( Rwr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Rwr_ManReadFanins( Rwr_Man_t * p )
-{
-    return p->vFanins;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the resynthesis manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Rwr_ManReadDecs( Rwr_Man_t * p )
+void * Rwr_ManReadDecs( Rwr_Man_t * p )
 {
-    return p->vForm;
+    return p->pGraph;
 }
 
 /**Function*************************************************************