Version abc70727

1 files changed, 59 insertions, 38 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 127882ea..13e79a0e 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -49,6 +49,7 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 typedef struct Fra_Par_t_   Fra_Par_t;
+typedef struct Fra_Cla_t_   Fra_Cla_t;
 typedef struct Fra_Man_t_   Fra_Man_t;
 
 // FRAIG parameters
@@ -65,8 +66,26 @@ struct Fra_Par_t_
     int              fProve;            // prove the miter outputs
     int              fVerbose;          // verbose output
     int              fDoSparse;         // skip sparse functions
+    int              fConeBias;         // bias variables in the cone (good for unsat runs)
     int              nBTLimitNode;      // conflict limit at a node
     int              nBTLimitMiter;     // conflict limit at an output
+    int              nTimeFrames;       // the number of timeframes to unroll
+};
+
+// FRAIG equivalence classes
+struct Fra_Cla_t_
+{
+    Aig_Man_t *      pAig;              // the original AIG manager
+    Aig_Obj_t **     pMemRepr;          // pointers to representatives of each node
+    Vec_Ptr_t *      vClasses;          // equivalence classes
+    Vec_Ptr_t *      vClasses1;         // equivalence class of Const1 node
+    Vec_Ptr_t *      vClassesTemp;      // temporary storage for new classes
+    Aig_Obj_t **     pMemClasses;       // memory allocated for equivalence classes
+    Aig_Obj_t **     pMemClassesFree;   // memory allocated for equivalence classes to be used
+    Vec_Ptr_t *      vClassOld;         // old equivalence class after splitting
+    Vec_Ptr_t *      vClassNew;         // new equivalence class(es) after splitting
+    int              nPairs;            // the number of pairs of nodes
+    int              fRefinement;       // set to 1 when refinement has happened
 };
 
 // FRAIG manager
@@ -77,6 +96,9 @@ struct Fra_Man_t_
     // AIG managers
     Aig_Man_t *      pManAig;           // the starting AIG manager
     Aig_Man_t *      pManFraig;         // the final AIG manager
+    // mapping AIG into FRAIG
+    int              nFrames;           // the number of timeframes used
+    Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
     // simulation info
     unsigned *       pSimWords;         // memory for simulation information
     int              nSimWords;         // the number of simulation words
@@ -85,27 +107,17 @@ struct Fra_Man_t_
     unsigned *       pPatWords;         // the counter example
     int *            pPatScores;        // the scores of each pattern
     // equivalence classes 
-    Vec_Ptr_t *      vClasses;          // equivalence classes
-    Vec_Ptr_t *      vClasses1;         // equivalence class of Const1 node
-    Vec_Ptr_t *      vClassesTemp;      // temporary storage for new classes
-    Aig_Obj_t **     pMemClasses;       // memory allocated for equivalence classes
-    Aig_Obj_t **     pMemClassesFree;   // memory allocated for equivalence classes to be used
-    Vec_Ptr_t *      vClassOld;         // old equivalence class after splitting
-    Vec_Ptr_t *      vClassNew;         // new equivalence class(es) after splitting
-    int              nPairs;            // the number of pairs of nodes
+    Fra_Cla_t *      pCla;              // representation of (candidate) equivalent nodes
     // equivalence checking
     sat_solver *     pSat;              // SAT solver
     int              nSatVars;          // the number of variables currently used
     Vec_Ptr_t *      vPiVars;           // the PIs of the cone used 
     sint64           nBTLimitGlobal;    // resource limit
     sint64           nInsLimitGlobal;   // resource limit
-    // various data members
-    Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
-    Aig_Obj_t **     pMemRepr;          // memory allocated for points to the node representatives
-    Aig_Obj_t **     pMemReprFra;       // memory allocated for points to the node representatives in the FRAIG
-    Vec_Ptr_t **     pMemFanins;        // the arrays of fanins
-    int *            pMemSatNums;       // the array of SAT numbers
+    Vec_Ptr_t **     pMemFanins;        // the arrays of fanins for some FRAIG nodes
+    int *            pMemSatNums;       // the array of SAT numbers for some FRAIG nodes
     int              nSizeAlloc;        // allocated size of the arrays
+    Vec_Ptr_t *      vTimeouts;         // the nodes, for which equivalence checking timed out
     // statistics
     int              nSimRounds;
     int              nNodesMiter;
@@ -140,23 +152,23 @@ struct Fra_Man_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline unsigned *   Fra_ObjSim( Aig_Obj_t * pObj )   { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id;  }
+static inline unsigned *   Fra_ObjSim( Aig_Obj_t * pObj )   { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id;    }
 static inline unsigned     Fra_ObjRandomSim()               { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
 
-static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj )                              { return ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id];       }
-static inline Aig_Obj_t *  Fra_ObjRepr( Aig_Obj_t * pObj )                               { return ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id];        }
-static inline Aig_Obj_t *  Fra_ObjReprFra( Aig_Obj_t * pObj )                            { return ((Fra_Man_t *)pObj->pData)->pMemReprFra[pObj->Id];     }
-static inline Vec_Ptr_t *  Fra_ObjFaninVec( Aig_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
-static inline int          Fra_ObjSatNum( Aig_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }
+static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj, int i )                       { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFrames*pObj->Id + i];  }
+static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFrames*pObj->Id + i] = pNode; }
+
+static inline Vec_Ptr_t *  Fra_ObjFaninVec( Aig_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];               }
+static inline void         Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]  = vFanins;           }
+
+static inline int          Fra_ObjSatNum( Aig_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];              }
+static inline void         Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;               }
 
-static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode )        { ((Fra_Man_t *)pObj->pData)->pMemFraig[pObj->Id]   = pNode;    }
-static inline void         Fra_ObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode )         { ((Fra_Man_t *)pObj->pData)->pMemRepr[pObj->Id]    = pNode;    }
-static inline void         Fra_ObjSetReprFra( Aig_Obj_t * pObj, Aig_Obj_t * pNode )      { ((Fra_Man_t *)pObj->pData)->pMemReprFra[pObj->Id] = pNode;    }
-static inline void         Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id]  = vFanins;  }
-static inline void         Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }
+static inline Aig_Obj_t *  Fra_ClassObjRepr( Aig_Obj_t * pObj )                          { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id];           }
+static inline void         Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode )    { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id]    = pNode;       }
 
-static inline Aig_Obj_t *  Fra_ObjChild0Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj)) : NULL;  }
-static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj)) : NULL;  }
+static inline Aig_Obj_t *  Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }
 
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///
@@ -167,31 +179,40 @@ static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj ) { assert( !Aig_I
 ////////////////////////////////////////////////////////////////////////
 
 /*=== fraClass.c ========================================================*/
-extern void                Fra_PrintClasses( Fra_Man_t * p );
-extern void                Fra_CreateClasses( Fra_Man_t * p );
-extern int                 Fra_RefineClasses( Fra_Man_t * p );
-extern int                 Fra_RefineClasses1( Fra_Man_t * p );
+extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
+extern void                Fra_ClassesStop( Fra_Cla_t * p );
+extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
+extern void                Fra_ClassesPrint( Fra_Cla_t * p );
+extern void                Fra_ClassesPrepare( Fra_Cla_t * p );
+extern int                 Fra_ClassesRefine( Fra_Cla_t * p );
+extern int                 Fra_ClassesRefine1( Fra_Cla_t * p );
+extern int                 Fra_ClassesCountLits( Fra_Cla_t * p );
 /*=== fraCnf.c ========================================================*/
 extern void                Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
-extern Aig_Man_t *         Fra_Perform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
-extern Aig_Man_t *         Fra_Choice( Aig_Man_t * pManAig );
+extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
+extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig );
+extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
 /*=== fraDfs.c ========================================================*/
-extern int                 Fra_CheckTfi( Fra_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld );
+/*=== fraInd.c ========================================================*/
+extern Aig_Man_t *         Fra_Induction( Aig_Man_t * p, int nFrames, int fVerbose );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
+extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
 extern Fra_Man_t *         Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
-extern void                Fra_ManPrepare( Fra_Man_t * p );
+extern Aig_Man_t *         Fra_ManPrepareComb( Fra_Man_t * p );
+extern void                Fra_ManFinalizeComb( Fra_Man_t * p );
 extern void                Fra_ManStop( Fra_Man_t * p );
 extern void                Fra_ManPrint( Fra_Man_t * p );
 /*=== fraSat.c ========================================================*/
 extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSim.c ========================================================*/
-extern int                 Fra_NodeHasZeroSim( Fra_Man_t * p, Aig_Obj_t * pObj );
-extern int                 Fra_NodeCompareSims( Fra_Man_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern int                 Fra_NodeHasZeroSim( Aig_Obj_t * pObj );
+extern int                 Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern unsigned            Fra_NodeHashSims( Aig_Obj_t * pObj );
 extern void                Fra_SavePattern( Fra_Man_t * p );
-extern void                Fra_Simulate( Fra_Man_t * p );
+extern void                Fra_Simulate( Fra_Man_t * p, int fInit );
 extern void                Fra_Resimulate( Fra_Man_t * p );
 extern int                 Fra_CheckOutputSims( Fra_Man_t * p );