diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-19 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-19 08:01:00 -0700 |
| commit | 3429e6309d0fc9a2d35d81f6483258c6af2fab50 (patch) | |
| tree | 6ea42f73528c9f456d5b0dea28173806cd45742d /src/aig/ssw/sswInt.h | |
| parent | 655a50101e18176f1163ccfc67cf69d86623d1f2 (diff) | |
| download | abc-3429e6309d0fc9a2d35d81f6483258c6af2fab50.tar.gz abc-3429e6309d0fc9a2d35d81f6483258c6af2fab50.tar.bz2 abc-3429e6309d0fc9a2d35d81f6483258c6af2fab50.zip | |
Version abc80919
Diffstat (limited to 'src/aig/ssw/sswInt.h')
| -rw-r--r-- | src/aig/ssw/sswInt.h | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 6824e239..5b4377c7 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -67,6 +67,11 @@ struct Ssw_Man_t_ Vec_Ptr_t * vFanins; // fanins of the CNF node Vec_Ptr_t * vSimRoots; // the roots of cand const 1 nodes to simulate Vec_Ptr_t * vSimClasses; // the roots of cand equiv classes to simulate + // SAT solving (latch corr only) + int nCallsSince; // the number of calls since last recycling + int nRecycles; // the number of time SAT solver was recycled + Vec_Ptr_t * vUsedNodes; // the nodes with SAT variables + Vec_Ptr_t * vUsedPis; // the PIs with SAT variables // sequential simulator Ssw_Sml_t * pSml; // counter example storage @@ -145,6 +150,7 @@ extern int Ssw_ClassesCand1Num( Ssw_Cla_t * p ); extern int Ssw_ClassesClassNum( Ssw_Cla_t * p ); extern int Ssw_ClassesLitNum( Ssw_Cla_t * p ); extern Aig_Obj_t ** Ssw_ClassesReadClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int * pnSize ); +extern void Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, Vec_Ptr_t * vClass ); extern void Ssw_ClassesCheck( Ssw_Cla_t * p ); extern void Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose ); extern void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj ); @@ -161,6 +167,8 @@ extern int Ssw_NodesAreEqualCex( void * p, Aig_Obj_t * pObj0, Aig_Obj_ extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ); /*=== sswCore.c ===================================================*/ extern Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p ); +/*=== sswLcorr.c ==========================================================*/ +extern int Ssw_ManSweepLatch( Ssw_Man_t * p ); /*=== sswMan.c ===================================================*/ extern Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars ); extern void Ssw_ManCleanup( Ssw_Man_t * p ); |