New MFS package.

1 files changed, 73 insertions, 38 deletions

diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index e2833121..57c5e352 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -41,6 +41,8 @@
 
 ABC_NAMESPACE_HEADER_START
 
+#define SFM_FANIN_MAX 6
+
 ////////////////////////////////////////////////////////////////////////
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
@@ -48,52 +50,76 @@ ABC_NAMESPACE_HEADER_START
 struct Sfm_Ntk_t_
 {
     // parameters
-    Sfm_Par_t *       pPars;    // parameters
+    Sfm_Par_t *       pPars;       // parameters
     // objects
-    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
+    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_Str_t *       vFixed;   // persistent objects
-    Vec_Wrd_t *       vTruths;  // truth tables
-    Vec_Wec_t         vFanins;  // fanins
+    Vec_Str_t *       vFixed;      // persistent objects
+    Vec_Wrd_t *       vTruths;     // truth tables
+    Vec_Wec_t         vFanins;     // fanins
     // attributes
-    Vec_Wec_t         vFanouts; // fanouts
-    Vec_Int_t         vLevels;  // logic level
-    Vec_Int_t         vCounts;  // fanin counters
-    Vec_Int_t         vId2Var;  // ObjId -> SatVar
-    Vec_Int_t         vVar2Id;  // SatVar -> ObjId
-    Vec_Wec_t *       vCnfs;    // CNFs
-    Vec_Int_t *       vCover;   // temporary
+    Vec_Wec_t         vFanouts;    // fanouts
+    Vec_Int_t         vLevels;     // logic level
+    Vec_Int_t         vCounts;     // fanin counters
+    Vec_Int_t         vId2Var;     // ObjId -> SatVar
+    Vec_Int_t         vVar2Id;     // SatVar -> ObjId
+    Vec_Wec_t *       vCnfs;       // CNFs
+    Vec_Int_t *       vCover;      // temporary
     // traversal IDs
-    Vec_Int_t         vTravIds; // traversal IDs
-    Vec_Int_t         vTravIds2;// traversal IDs
-    int               nTravIds; // traversal IDs
-    int               nTravIds2;// traversal IDs
+    Vec_Int_t         vTravIds;    // traversal IDs
+    Vec_Int_t         vTravIds2;   // traversal IDs
+    int               nTravIds;    // traversal IDs
+    int               nTravIds2;   // traversal IDs
     // window
     int               iNode;
-    Vec_Int_t *       vLeaves;  // leaves 
-    Vec_Int_t *       vRoots;   // roots
-    Vec_Int_t *       vNodes;   // internal
-    Vec_Int_t *       vTfo;     // TFO (excluding iNode)
-    Vec_Int_t *       vDivs;    // divisors
+    Vec_Int_t *       vLeaves;     // leaves 
+    Vec_Int_t *       vRoots;      // roots
+    Vec_Int_t *       vNodes;      // internal
+    Vec_Int_t *       vTfo;        // TFO (excluding iNode)
+    Vec_Int_t *       vDivs;       // divisors
     // 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
+    sat_solver *      pSat0;       // SAT solver for the off-set
+    sat_solver *      pSat1;       // SAT solver for the on-set
+    int               nSatVars;    // the number of variables
+    int               nTryRemoves; // number of fanin removals
+    int               nTryResubs;  // number of resubstitutions
+    int               nRemoves;    // number of fanin removals
+    int               nResubs;     // number of resubstitutions
+    // counter-examples
+    int               nCexes;      // number of CEXes
+    Vec_Wrd_t *       vDivCexes;   // counter-examples
     // intermediate data
-    Vec_Int_t *       vDivIds;  // divisors indexes
-    Vec_Int_t *       vLits;    // literals
-    Vec_Int_t *       vDiffs;   // differences
-    Vec_Wec_t *       vClauses; // CNF clauses for the node
-    Vec_Int_t *       vFaninMap;// mapping fanins into their SAT vars
+    Vec_Int_t *       vFans;       // current fanins
+    Vec_Int_t *       vOrder;      // object order
+    Vec_Int_t *       vDivVars;    // divisor SAT variables
+    Vec_Int_t *       vDivIds;     // divisors indexes
+    Vec_Int_t *       vLits;       // literals
+    Vec_Wec_t *       vClauses;    // CNF clauses for the node
+    Vec_Int_t *       vFaninMap;   // mapping fanins into their SAT vars
+    // nodes
+    int               nTotalNodesBeg;
+    int               nTotalEdgesBeg;
+    int               nTotalNodesEnd;
+    int               nTotalEdgesEnd;
+    // runtime
+    clock_t           timeWin;
+    clock_t           timeDiv;
+    clock_t           timeCnf;
+    clock_t           timeSat;
+    clock_t           timeTotal;
 };
 
 #define SFM_SAT_UNDEC 0x1234567812345678
 #define SFM_SAT_SAT   0x8765432187654321
 
 
+static inline int  Sfm_NtkPiNum( Sfm_Ntk_t * p )                        { return p->nPis;                                   }
+static inline int  Sfm_NtkPoNum( Sfm_Ntk_t * p )                        { return p->nPos;                                   }
+static inline int  Sfm_NtkNodeNum( Sfm_Ntk_t * p )                      { return p->nObjs - p->nPis - p->nPos;              }
+
 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;    }
@@ -104,6 +130,9 @@ static inline Vec_Int_t * Sfm_ObjFoArray( Sfm_Ntk_t * p, int i )        { return
 static inline int  Sfm_ObjFaninNum( Sfm_Ntk_t * p, int i )              { return Vec_IntSize(Sfm_ObjFiArray(p, i));         }
 static inline int  Sfm_ObjFanoutNum( Sfm_Ntk_t * p, int i )             { return Vec_IntSize(Sfm_ObjFoArray(p, i));         }
 
+static inline int  Sfm_ObjRefIncrement( Sfm_Ntk_t * p, int iObj )       { return ++Sfm_ObjFiArray(p, iObj)->nSize;          } 
+static inline int  Sfm_ObjRefDecrement( Sfm_Ntk_t * p, int iObj )       { return --Sfm_ObjFiArray(p, iObj)->nSize;          } 
+
 static inline int  Sfm_ObjFanin( Sfm_Ntk_t * p, int i, int k )          { return Vec_IntEntry(Sfm_ObjFiArray(p, i), k);     }
 static inline int  Sfm_ObjFanout( Sfm_Ntk_t * p, int i, int k )         { return Vec_IntEntry(Sfm_ObjFoArray(p, i), k);     }
 
@@ -112,7 +141,8 @@ static inline void Sfm_ObjSetSatVar( Sfm_Ntk_t * p, int iObj, int Num ) { assert
 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 ); }
 
-static inline int  Sfm_ObjLevel( Sfm_Ntk_t * p, int iObj )              { return Vec_IntEntry(&p->vLevels, iObj);                           }
+static inline int  Sfm_ObjLevel( Sfm_Ntk_t * p, int iObj )              { return Vec_IntEntry( &p->vLevels, iObj );                         }
+static inline void Sfm_ObjSetLevel( Sfm_Ntk_t * p, int iObj, int Lev )  { Vec_IntWriteEntry( &p->vLevels, iObj, Lev );                      }
 
 static inline int  Sfm_ObjUpdateFaninCount( Sfm_Ntk_t * p, int iObj )   { return Vec_IntAddToEntry(&p->vCounts, iObj, -1);                  }
 static inline void Sfm_ObjResetFaninCount( Sfm_Ntk_t * p, int iObj )    { Vec_IntWriteEntry(&p->vCounts, iObj, Sfm_ObjFaninNum(p, iObj)-1); }
@@ -123,8 +153,8 @@ static inline void Sfm_ObjResetFaninCount( Sfm_Ntk_t * p, int iObj )    { Vec_In
 ////////////////////////////////////////////////////////////////////////
 
 #define Sfm_NtkForEachNode( p, i )                for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
-#define Sfm_NodeForEachFanin( p, Node, Fan, i )   for ( i = 0; i < Sfm_ObjFaninNum(p, Node)  && ((Fan = Sfm_ObjFanin(p, Node, i)), 1);  i++ )
-#define Sfm_NodeForEachFanout( p, Node, Fan, i )  for ( i = 0; i < Sfm_ObjFanoutNum(p, Node) && ((Fan = Sfm_ObjFanout(p, Node, i)), 1); i++ )
+#define Sfm_ObjForEachFanin( p, Node, Fan, i )   for ( i = 0; i < Sfm_ObjFaninNum(p, Node)  && ((Fan = Sfm_ObjFanin(p, Node, i)), 1);  i++ )
+#define Sfm_ObjForEachFanout( p, Node, Fan, i )  for ( i = 0; i < Sfm_ObjFanoutNum(p, Node) && ((Fan = Sfm_ObjFanout(p, Node, i)), 1); i++ )
 
 ////////////////////////////////////////////////////////////////////////
 ///                    FUNCTION DECLARATIONS                         ///
@@ -133,15 +163,20 @@ static inline void Sfm_ObjResetFaninCount( Sfm_Ntk_t * p, int iObj )    { Vec_In
 /*=== sfmCnf.c ==========================================================*/
 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 Vec_Wec_t *  Sfm_CreateCnf( Sfm_Ntk_t * p );
 extern void         Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap );
 /*=== sfmCore.c ==========================================================*/
 /*=== sfmNtk.c ==========================================================*/
 extern Sfm_Ntk_t *  Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
+extern void         Sfm_NtkPrepare( Sfm_Ntk_t * p );
+extern void         Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth );
 /*=== sfmSat.c ==========================================================*/
-extern word         Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivs, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit );
+extern void         Sfm_NtkWindowToSolver( Sfm_Ntk_t * p );
+extern word         Sfm_ComputeInterpolant( Sfm_Ntk_t * p );
 /*=== sfmWin.c ==========================================================*/
-extern int          Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode, int fVerbose );
-extern void         Sfm_NtkWin2Sat( Sfm_Ntk_t * p );
+extern int          Sfm_ObjMffcSize( Sfm_Ntk_t * p, int iObj );
+extern int          Sfm_NtkCreateWindow( Sfm_Ntk_t * p, int iNode, int fVerbose );
+extern void         Sfm_NtkPrepareDivisors( Sfm_Ntk_t * p, int iNode );
 
 
 ABC_NAMESPACE_HEADER_END