Version abc70624

1 files changed, 64 insertions, 9 deletions

diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 9bb79262..f71470cf 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -49,12 +49,13 @@ typedef struct Dar_Par_t_            Dar_Par_t;
 typedef struct Dar_Man_t_            Dar_Man_t;
 typedef struct Dar_Obj_t_            Dar_Obj_t;
 typedef struct Dar_Cut_t_            Dar_Cut_t;
+typedef struct Dar_Cnf_t_            Dar_Cnf_t;
 typedef struct Dar_MmFixed_t_        Dar_MmFixed_t;    
 typedef struct Dar_MmFlex_t_         Dar_MmFlex_t;     
 typedef struct Dar_MmStep_t_         Dar_MmStep_t;     
 
 // the maximum number of cuts stored at a node
-#define DAR_CUT_BASE                 32 
+#define DAR_CUT_BASE                 64 
 
 // object types
 typedef enum { 
@@ -82,11 +83,14 @@ struct Dar_Par_t_
 struct Dar_Cut_t_  // 8 words
 {
     unsigned         uSign;
-    unsigned         uTruth  : 16;
-    unsigned         nLeaves :  3;
-    int              pLeaves[4];
-    unsigned char    pIndices[4];
-    float            aFlow;
+    unsigned         uTruth  : 16;   // the truth table of the cut function
+    unsigned         Cost    :  6;   // the cost of the cut in terms of CNF clauses
+    unsigned         FanRefs :  4;   // the average number of fanin references
+    unsigned         NoRefs  :  3;   // the average number of fanin references
+    unsigned         nLeaves :  3;   // the number of leaves
+    int              pLeaves[4];     // the array of leaves
+//    unsigned char    pIndices[4];
+    float            Area;           // the area flow or exact area of the cut
 };
 
 // the AIG node
@@ -130,31 +134,59 @@ struct Dar_Man_t_
     Dar_Cut_t        BaseCuts[DAR_CUT_BASE];
     int              nBaseCuts;
     int              nCutsUsed;
+    int              nCutsFiltered;
     // current rewriting step
+    int              nNodesInit;     // the original number of nodes
     Vec_Ptr_t *      vLeavesBest;    // the best set of leaves
     int              OutBest;        // the best output (in the library)
     int              GainBest;       // the best gain
+    int              LevelBest;      // the level of node with the best gain
+    int              ClassBest;      // the equivalence class of the best replacement
+    int              nTotalSubgs;    // the total number of subgraphs tried
+    int              ClassTimes[222];// the runtimes for each class
+    int              ClassGains[222];// the gains for each class
+    int              ClassSubgs[222];// the graphs for each class
     // various data members
     Dar_MmFixed_t *  pMemObjs;       // memory manager for objects
     Dar_MmFlex_t *   pMemCuts;       // memory manager for cuts
     Vec_Int_t *      vRequired;      // the required times
+    int              nLevelMax;      // maximum number of levels
     void *           pData;          // the temporary data
     int              nTravIds;       // the current traversal ID
     int              fCatchExor;     // enables EXOR nodes
+    // CNF mapping
+    char *           pSopSizes;      // sizes of SOPs for 4-variable functions
+    char **          pSops;          // the SOPs for 4-variable functions
+    int              aArea;          // the area of the mapping
     // rewriting statistics
     int              nCutsBad;
     int              nCutsGood;
     // timing statistics
+    int              timeCuts;
+    int              timeEval;
+    int              timeOther;
+    int              timeTotal;
     int              time1;
     int              time2;
 };
 
+// the CNF asserting outputs of AIG to be 1
+struct Dar_Cnf_t_
+{
+    Dar_Man_t *     pMan;            // the AIG manager, for which CNF is computed
+    int             nLiterals;       // the number of CNF literals
+    int             nClauses;        // the number of CNF clauses
+    int **          pClauses;        // the CNF clauses
+    int *           pVarNums;        // the number of CNF variable for each node ID (-1 if unused)
+};
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 #define DAR_MIN(a,b)       (((a) < (b))? (a) : (b))
 #define DAR_MAX(a,b)       (((a) > (b))? (a) : (b))
+#define DAR_INFINITY       (100000000)
 
 #ifndef PRT
 #define PRT(a,t)  printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))
@@ -187,6 +219,7 @@ static inline int          Dar_ManLatchNum( Dar_Man_t * p )       { return p->nO
 static inline int          Dar_ManNodeNum( Dar_Man_t * p )        { return p->nObjs[DAR_AIG_AND]+p->nObjs[DAR_AIG_EXOR];   }
 static inline int          Dar_ManGetCost( Dar_Man_t * p )        { return p->nObjs[DAR_AIG_AND]+3*p->nObjs[DAR_AIG_EXOR]; }
 static inline int          Dar_ManObjNum( Dar_Man_t * p )         { return p->nCreated - p->nDeleted;               }
+static inline int          Dar_ManObjIdMax( Dar_Man_t * p )       { return Vec_PtrSize(p->vObjs);                   }
 
 static inline Dar_Type_t   Dar_ObjType( Dar_Obj_t * pObj )        { return (Dar_Type_t)pObj->Type;               }
 static inline int          Dar_ObjIsNone( Dar_Obj_t * pObj )      { return pObj->Type == DAR_AIG_NONE;   }
@@ -241,6 +274,8 @@ static inline int          Dar_ObjFanoutC( Dar_Obj_t * pObj, Dar_Obj_t * pFanout
     if ( Dar_ObjFanin1(pFanout) == pObj ) return Dar_ObjFaninC1(pObj); 
     assert(0); return -1; 
 }
+static inline Dar_Cut_t *  Dar_ObjBestCut( Dar_Obj_t * pObj ) { return (Dar_Cut_t *)pObj->pNext;  }
+static inline void         Dar_ObjSetBestCut( Dar_Obj_t * pObj, Dar_Cut_t * pCut )   { pObj->pNext = (Dar_Obj_t *)pCut; }
 
 // create the ghost of the new node
 static inline Dar_Obj_t *  Dar_ObjCreateGhost( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t Type )    
@@ -278,9 +313,10 @@ static inline Dar_Obj_t * Dar_ManFetchMemory( Dar_Man_t * p )
 static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry )
 {
     extern void Dar_MmFixedEntryRecycle( Dar_MmFixed_t * p, char * pEntry );
-    p->nDeleted++;
+    assert( pEntry->nRefs == 0 );
     pEntry->Type = DAR_AIG_NONE; // distinquishes a dead node from a live node
     Dar_MmFixedEntryRecycle( p->pMemObjs, (char *)pEntry );
+    p->nDeleted++;
 }
 
 
@@ -297,6 +333,12 @@ static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry )
 // iterator over all objects, including those currently not used
 #define Dar_ManForEachObj( p, pObj, i )                                         \
     Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else
+// iterator over all cuts of the node
+#define Dar_ObjForEachCut( pObj, pCut, i )                                      \
+    for ( pCut = pObj->pData, i = 0; i < (int)pObj->nCuts; i++, pCut++ ) if ( i==0 ) {} else
+// iterator over leaves of the cut
+#define Dar_CutForEachLeaf( p, pCut, pLeaf, i )                                 \
+    for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = Dar_ManObj(p, (pCut)->pLeaves[i])); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -307,15 +349,25 @@ extern Dar_Man_t *     Dar_ManBalance( Dar_Man_t * p, int fUpdateLevel );
 extern Dar_Obj_t *     Dar_NodeBalanceBuildSuper( Dar_Man_t * p, Vec_Ptr_t * vSuper, Dar_Type_t Type, int fUpdateLevel );
 /*=== darCheck.c ========================================================*/
 extern int             Dar_ManCheck( Dar_Man_t * p );
+/*=== darCnf.c ========================================================*/
+extern Dar_Cnf_t *     Dar_ManDeriveCnf( Dar_Man_t * p );
+extern Dar_Cut_t *     Dar_ObjFindBestCut( Dar_Obj_t * pObj );
+extern void            Dar_CutAssignAreaFlow( Dar_Man_t * p, Dar_Cut_t * pCut );
+extern void            Dar_CutAssignArea( Dar_Man_t * p, Dar_Cut_t * pCut );
+extern void            Dar_CnfFree( Dar_Cnf_t * pCnf );
 /*=== darCore.c ========================================================*/
 extern int             Dar_ManRewrite( Dar_Man_t * p );
+extern int             Dar_ManComputeCuts( Dar_Man_t * p );
 /*=== darCut.c ========================================================*/
 extern void            Dar_ManSetupPis( Dar_Man_t * p );
-extern void            Dar_ObjComputeCuts_rec( Dar_Man_t * p, Dar_Obj_t * pObj );
+extern Dar_Cut_t *     Dar_ObjComputeCuts_rec( Dar_Man_t * p, Dar_Obj_t * pObj );
+extern Dar_Cut_t *     Dar_ObjComputeCuts( Dar_Man_t * p, Dar_Obj_t * pObj );
 extern void            Dar_ManCutsFree( Dar_Man_t * p );
 /*=== darData.c ========================================================*/
 extern Vec_Int_t *     Dar_LibReadNodes();
 extern Vec_Int_t *     Dar_LibReadOuts();
+/*=== darData2.c ========================================================*/
+extern void            Dar_LibReadMsops( char ** ppSopSizes, char *** ppSops );
 /*=== darDfs.c ==========================================================*/
 extern Vec_Ptr_t *     Dar_ManDfs( Dar_Man_t * p );
 extern int             Dar_ManCountLevels( Dar_Man_t * p );
@@ -327,7 +379,7 @@ extern Dar_Obj_t *     Dar_Compose( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Obj_t
 /*=== darLib.c ==========================================================*/
 extern void            Dar_LibStart();
 extern void            Dar_LibStop();
-extern int             Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
+extern void            Dar_LibEval( Dar_Man_t * p, Dar_Obj_t * pRoot, Dar_Cut_t * pCut, int Required );
 extern Dar_Obj_t *     Dar_LibBuildBest( Dar_Man_t * p );
 /*=== darMan.c ==========================================================*/
 extern Dar_Man_t *     Dar_ManStart();
@@ -335,6 +387,7 @@ extern Dar_Man_t *     Dar_ManDup( Dar_Man_t * p );
 extern void            Dar_ManStop( Dar_Man_t * p );
 extern int             Dar_ManCleanup( Dar_Man_t * p );
 extern void            Dar_ManPrintStats( Dar_Man_t * p );
+extern void            Dar_ManPrintRuntime( Dar_Man_t * p );
 /*=== darMem.c ==========================================================*/
 extern void            Dar_ManStartMemory( Dar_Man_t * p );
 extern void            Dar_ManStopMemory( Dar_Man_t * p );
@@ -372,12 +425,14 @@ extern void            Dar_TableProfile( Dar_Man_t * p );
 /*=== darUtil.c =========================================================*/
 extern Dar_Par_t *     Dar_ManDefaultParams();
 extern void            Dar_ManIncrementTravId( Dar_Man_t * p );
+extern int             Dar_ManLevels( Dar_Man_t * p );
 extern void            Dar_ManCleanData( Dar_Man_t * p );
 extern void            Dar_ObjCleanData_rec( Dar_Obj_t * pObj );
 extern void            Dar_ObjCollectMulti( Dar_Obj_t * pFunc, Vec_Ptr_t * vSuper );
 extern int             Dar_ObjIsMuxType( Dar_Obj_t * pObj );
 extern int             Dar_ObjRecognizeExor( Dar_Obj_t * pObj, Dar_Obj_t ** ppFan0, Dar_Obj_t ** ppFan1 );
 extern Dar_Obj_t *     Dar_ObjRecognizeMux( Dar_Obj_t * pObj, Dar_Obj_t ** ppObjT, Dar_Obj_t ** ppObjE );
+extern Dar_Obj_t *     Dar_ObjReal_rec( Dar_Obj_t * pObj );
 extern void            Dar_ObjPrintEqn( FILE * pFile, Dar_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
 extern void            Dar_ObjPrintVerilog( FILE * pFile, Dar_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
 extern void            Dar_ObjPrintVerbose( Dar_Obj_t * pObj, int fHaig );