New MFS package.

1 files changed, 61 insertions, 44 deletions

diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 9dad053f..d52b46e4 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -32,6 +32,7 @@
 #include <assert.h>
 
 #include "misc/vec/vec.h"
+#include "sat/bsat/satSolver.h"
 #include "sfm.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -46,72 +47,88 @@ ABC_NAMESPACE_HEADER_START
 
 struct Sfm_Ntk_t_
 {
+    // parameters
+    Sfm_Par_t *       pPars;    // parameters
     // objects
-    int *             pMem;   // memory for objects
-    Vec_Int_t         vObjs;  // ObjId -> Offset
-    Vec_Int_t         vPis;   // PiId -> ObjId
-    Vec_Int_t         vPos;   // PoId -> ObjId
-    // fanins/fanouts
-    Vec_Int_t         vMem;   // memory for overflow fanin/fanouts
+    int               nPis;     // PI count (PIs should be first objects)
+    int               nPos;     // PO count (POs should be last objects)
+    int               nNodes;   // internal nodes
+    int               nObjs;    // total objects
+    // user data
+    Vec_Wec_t *       vFanins;  // fanins
+    Vec_Str_t *       vFixed;   // persistent objects
+    Vec_Wrd_t *       vTruths;  // truth tables
     // attributes
-    Vec_Int_t         vLevels;
-    Vec_Int_t         vTravIds;
-    Vec_Int_t         vSatVars;
-    Vec_Wrd_t         vTruths;
-};
-
-typedef struct Sfm_Obj_t_ Sfm_Obj_t;
-struct Sfm_Obj_t_
-{
-    unsigned          Type   :  2;
-    unsigned          Id     : 30;
-    unsigned          fOpt   :  1;
-    unsigned          fTfo   :  1;
-    unsigned          nFanis :  4;
-    unsigned          nFanos : 26;
-    int               Fanio[0];
-};
-
-struct Sfm_Man_t_
-{
-    Sfm_Ntk_t *       pNtk;
+    Vec_Wec_t *       vFanouts; // fanouts
+    Vec_Int_t *       vLevels;  // logic level
+    Vec_Int_t         vTravIds; // traversal IDs
+    Vec_Int_t         vId2Var;  // ObjId -> SatVar
+    Vec_Int_t         vVar2Id;  // SatVar -> ObjId
+    Vec_Wec_t *       vCnfs;    // CNFs
+    Vec_Int_t *       vCover;   // temporary
+    int               nTravIds; // traversal IDs
     // window
-    Sfm_Obj_t *       pNode;
-    Vec_Int_t *       vLeaves;      // leaves 
-    Vec_Int_t *       vRoots;       // roots
-    Vec_Int_t *       vNodes;       // internal
-    Vec_Int_t *       vTfo;         // TFO (including pNode)
+    int               iNode;
+    Vec_Int_t *       vLeaves;  // leaves 
+    Vec_Int_t *       vRoots;   // roots
+    Vec_Int_t *       vNodes;   // internal
+    Vec_Int_t *       vTfo;     // TFO (excluding iNode)
     // SAT solving
+    int               nSatVars; // the number of variables
+    sat_solver *      pSat1;    // SAT solver for the on-set
+    sat_solver *      pSat0;    // SAT solver for the off-set
+    // intermediate data
+    Vec_Int_t *       vDivs;    // divisors
+    Vec_Int_t *       vLits;    // literals
+    Vec_Int_t *       vFani;    // iterator fanins
+    Vec_Int_t *       vFano;    // iterator fanouts
+    Vec_Wec_t *       vClauses; // CNF clauses for the node
+    Vec_Int_t *       vFaninMap;// mapping fanins into their SAT vars
 };
 
+#define SFM_SAT_UNDEC 0x1234567812345678
+#define SFM_SAT_SAT   0x8765432187654321
+
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline Sfm_Obj_t * Sfm_ManObj( Sfm_Ntk_t * p, int Id ) { return (Sfm_Obj_t *)Vec_IntEntryP( &p->vObjs, Id ); }
+#define Sfm_NtkForEachNode( p, i )                for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
+#define Sfm_NodeForEachFanin( p, Node, Fan, i )   for ( p->vFani = Vec_WecEntry(p->vFanins,  Node), i = 0; i < Vec_IntSize(p->vFani) && ((Fan = Vec_IntEntry(p->vFani, i)), 1); i++ )
+#define Sfm_NodeForEachFanout( p, Node, Fan, i )  for ( p->vFano = Vec_WecEntry(p->vFanouts, Node), i = 0; i < Vec_IntSize(p->vFani) && ((Fan = Vec_IntEntry(p->vFano, i)), 1); i++ )
+
+static inline int  Sfm_ObjIsPi( Sfm_Ntk_t * p, int i )      { return i < p->nPis;                               }
+static inline int  Sfm_ObjIsPo( Sfm_Ntk_t * p, int i )      { return i + p->nPos < p->nObjs;                    }
+static inline int  Sfm_ObjIsNode( Sfm_Ntk_t * p, int i )    { return i >= p->nPis && i + p->nPos < p->nObjs;    }
+
+static inline int  Sfm_ObjFaninNum( Sfm_Ntk_t * p, int i )  { return Vec_IntSize(Vec_WecEntry(p->vFanins, i));  }
+static inline int  Sfm_ObjFanoutNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Vec_WecEntry(p->vFanouts, i)); }
+
+static inline int  Sfm_ObjSatVar( Sfm_Ntk_t * p, int iObj )             { return Vec_IntEntry(&p->vId2Var, iObj);     }
+static inline void Sfm_ObjSetSatVar( Sfm_Ntk_t * p, int iObj, int Num ) { assert(Sfm_ObjSatVar(p, iObj) == -1); Vec_IntWriteEntry(&p->vId2Var, iObj, Num);  Vec_IntWriteEntry(&p->vVar2Id, Num, iObj);                            }
+static inline void Sfm_ObjCleanSatVar( Sfm_Ntk_t * p, int Num )         { assert(Sfm_ObjSatVar(p, Vec_IntEntry(&p->vVar2Id, Num)) != -1); Vec_IntWriteEntry(&p->vId2Var, Vec_IntEntry(&p->vVar2Id, Num), Num);  Vec_IntWriteEntry(&p->vVar2Id, Num, -1);    }
+static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p, int nSize )         { int i; for ( i = 1; i < nSize; i++ )  Sfm_ObjCleanSatVar( p, i ); }
 
-#define Sfm_ManForEachObj( p, pObj, i )                                \
-    for ( i = 0; (i < Vec_IntSize(&p->vObjs) && ((pObj) = Sfm_ManObj(p, i))); i++ )
-#define Sfm_ManForEachPi( p, pObj, i )                                 \
-    for ( i = 0; (i < Vec_IntSize(&p->vPis) && ((pObj) = Sfm_ManObj(p, Vec_IntEntry(&p->vPis, i)))); i++ )
-#define Sfm_ManForEachPo( p, pObj, i )                                 \
-    for ( i = 0; (i < Vec_IntSize(&p->vPos) && ((pObj) = Sfm_ManObj(p, Vec_IntEntry(&p->vPos, i)))); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== sfmCnf.c ==========================================================*/
-extern int          Sfm_DeriveCnfs( Vec_Wrd_t * vTruths, Vec_Int_t * vFanins, Vec_Str_t ** pvCnfs, Vec_Int_t ** pvOffsets );
+extern void         Sfm_PrintCnf( Vec_Str_t * vCnf );
+extern int          Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf );
+extern void         Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap );
 /*=== sfmCore.c ==========================================================*/
-/*=== sfmMan.c ==========================================================*/
 /*=== sfmNtk.c ==========================================================*/
+extern Sfm_Ntk_t *  Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
 /*=== sfmSat.c ==========================================================*/
-extern int          Sfm_CreateSatWindow( Sfm_Ntk_t * p );
-
-ABC_NAMESPACE_HEADER_END
+extern word         Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivs, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit );
+/*=== sfmWin.c ==========================================================*/
+extern int          Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode );
+extern void         Sfm_NtkWin2Sat( Sfm_Ntk_t * p );
 
 
+ABC_NAMESPACE_HEADER_END
 
 #endif