Version abc71001

1 files changed, 162 insertions, 0 deletions

diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
new file mode 100644
index 00000000..5c7a594e
--- /dev/null
+++ b/src/aig/cnf/cnf.h
@@ -0,0 +1,162 @@
+/**CFile****************************************************************
+
+  FileName    [cnf.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [DAG-aware AIG rewriting.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: cnf.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __CNF_H__
+#define __CNF_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif 
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+#include <time.h>
+
+#include "vec.h"
+#include "aig.h"
+#include "darInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Cnf_Man_t_            Cnf_Man_t;
+typedef struct Cnf_Dat_t_            Cnf_Dat_t;
+typedef struct Cnf_Cut_t_            Cnf_Cut_t;
+
+// the CNF asserting outputs of AIG to be 1
+struct Cnf_Dat_t_
+{
+    Aig_Man_t *     pMan;            // the AIG manager, for which CNF is computed
+    int             nVars;           // the number of variables
+    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)
+};
+
+// the cut used to represent node in the AIG
+struct Cnf_Cut_t_
+{
+    char            nFanins;         // the number of leaves
+    char            Cost;            // the cost of this cut
+    short           nWords;          // the number of words in truth table
+    Vec_Int_t *     vIsop[2];        // neg/pos ISOPs
+    int             pFanins[0];      // the fanins (followed by the truth table)
+};
+
+// the CNF computation manager
+struct Cnf_Man_t_
+{
+    Aig_Man_t *     pManAig;         // the underlying AIG manager
+    char *          pSopSizes;       // sizes of SOPs for 4-variable functions
+    char **         pSops;           // the SOPs for 4-variable functions
+    int             aArea;           // the area of the mapping
+    Aig_MmFlex_t *  pMemCuts;        // memory manager for cuts
+    int             nMergeLimit;     // the limit on the size of merged cut
+    unsigned *      pTruths[4];      // temporary truth tables
+    Vec_Int_t *     vMemory;         // memory for intermediate ISOP representation
+    int             timeCuts; 
+    int             timeMap;
+    int             timeSave;
+};
+
+
+static inline Dar_Cut_t *  Dar_ObjBestCut( Aig_Obj_t * pObj ) { Dar_Cut_t * pCut; int i; Dar_ObjForEachCut( pObj, pCut, i ) if ( pCut->fBest ) return pCut; return NULL; }
+
+static inline int          Cnf_CutSopCost( Cnf_Man_t * p, Dar_Cut_t * pCut ) { return p->pSopSizes[pCut->uTruth] + p->pSopSizes[0xFFFF & ~pCut->uTruth]; }
+
+static inline int          Cnf_CutLeaveNum( Cnf_Cut_t * pCut )    { return pCut->nFanins;                               }
+static inline int *        Cnf_CutLeaves( Cnf_Cut_t * pCut )      { return pCut->pFanins;                               }
+static inline unsigned *   Cnf_CutTruth( Cnf_Cut_t * pCut )       { return (unsigned *)(pCut->pFanins + pCut->nFanins); }
+
+static inline Cnf_Cut_t *  Cnf_ObjBestCut( Aig_Obj_t * pObj )                       { return pObj->pData;  }
+static inline void         Cnf_ObjSetBestCut( Aig_Obj_t * pObj, Cnf_Cut_t * pCut )  { pObj->pData = pCut;  }
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                           ITERATORS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// iterator over leaves of the cut
+#define Cnf_CutForEachLeaf( p, pCut, pLeaf, i )                         \
+    for ( i = 0; (i < (int)(pCut)->nFanins) && ((pLeaf) = Aig_ManObj(p, (pCut)->pFanins[i])); i++ )
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== cnfCore.c ========================================================*/
+extern Cnf_Dat_t *     Cnf_Derive( Aig_Man_t * pAig, int nOutputs );
+extern Cnf_Man_t *     Cnf_ManRead();
+extern void            Cnf_ClearMemory();
+/*=== cnfCut.c ========================================================*/
+extern Cnf_Cut_t *     Cnf_CutCreate( Cnf_Man_t * p, Aig_Obj_t * pObj );
+extern void            Cnf_CutPrint( Cnf_Cut_t * pCut );
+extern void            Cnf_CutFree( Cnf_Cut_t * pCut );
+extern void            Cnf_CutUpdateRefs( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, Cnf_Cut_t * pCutRes );
+extern Cnf_Cut_t *     Cnf_CutCompose( Cnf_Man_t * p, Cnf_Cut_t * pCut, Cnf_Cut_t * pCutFan, int iFan );
+/*=== cnfData.c ========================================================*/
+extern void            Cnf_ReadMsops( char ** ppSopSizes, char *** ppSops );
+/*=== cnfMan.c ========================================================*/
+extern Cnf_Man_t *     Cnf_ManStart();
+extern void            Cnf_ManStop( Cnf_Man_t * p );
+extern Vec_Int_t *     Cnf_DataCollectPiSatNums( Cnf_Dat_t * pCnf, Aig_Man_t * p );
+extern void            Cnf_DataFree( Cnf_Dat_t * p );
+extern void            Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
+void *                 Cnf_DataWriteIntoSolver( Cnf_Dat_t * p );
+/*=== cnfMap.c ========================================================*/
+extern void            Cnf_DeriveMapping( Cnf_Man_t * p );
+extern int             Cnf_ManMapForCnf( Cnf_Man_t * p );
+/*=== cnfPost.c ========================================================*/
+extern void            Cnf_ManTransferCuts( Cnf_Man_t * p );
+extern void            Cnf_ManFreeCuts( Cnf_Man_t * p );
+extern void            Cnf_ManPostprocess( Cnf_Man_t * p );
+/*=== cnfUtil.c ========================================================*/
+extern Vec_Ptr_t *     Aig_ManScanMapping( Cnf_Man_t * p, int fCollect );
+extern Vec_Ptr_t *     Cnf_ManScanMapping( Cnf_Man_t * p, int fCollect, int fPreorder );
+/*=== cnfWrite.c ========================================================*/
+extern void            Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover );
+extern Cnf_Dat_t *     Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs );
+extern Cnf_Dat_t *     Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+