diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-05 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-09-05 08:01:00 -0700 |
| commit | 092c7be0ffb89d869e8eaeb04de12779ce96e8b9 (patch) | |
| tree | fe4ae0c41d0481c1c3f9eec7689f49cba58cd4e8 /src/aig/ssw/sswInt.h | |
| parent | 73c8aa7c400bab320cea56529241e1d396f1e0f5 (diff) | |
| download | abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.tar.gz abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.tar.bz2 abc-092c7be0ffb89d869e8eaeb04de12779ce96e8b9.zip | |
Version abc80905
Diffstat (limited to 'src/aig/ssw/sswInt.h')
| -rw-r--r-- | src/aig/ssw/sswInt.h | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h index 0e54af32..21621c0d 100644 --- a/src/aig/ssw/sswInt.h +++ b/src/aig/ssw/sswInt.h @@ -55,7 +55,6 @@ struct Ssw_Man_t_ Aig_Man_t * pAig; // user-given AIG Aig_Man_t * pFrames; // final AIG Aig_Obj_t ** pNodeToFraig; // mapping of AIG nodes into FRAIG nodes - int nFrameNodes; // the number of nodes in the timeframes // equivalence classes Ssw_Cla_t * ppClasses; // equivalence classes of nodes // Aig_Obj_t ** pReprsProved; // equivalences proved @@ -70,6 +69,7 @@ struct Ssw_Man_t_ // constraints int nConstrTotal; // the number of total constraints int nConstrReduced; // the number of reduced constraints + int nStragers; // SAT calls statistics int nSatCalls; // the number of SAT calls int nSatProof; // the number of proofs @@ -136,6 +136,7 @@ extern Ssw_Cla_t * Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, extern int Ssw_ClassesRefine( Ssw_Cla_t * p ); extern int Ssw_ClassesRefineOneClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr, int fRecursive ); extern int Ssw_ClassesRefineConst1Group( Ssw_Cla_t * p, Vec_Ptr_t * vRoots, int fRecursive ); +extern int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive ); /*=== sswCnf.c ===================================================*/ extern void Ssw_CnfNodeAddToSolver( Ssw_Man_t * p, Aig_Obj_t * pObj ); /*=== sswMan.c ===================================================*/ @@ -148,6 +149,7 @@ extern int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj extern int Ssw_NodesAreConstrained( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ); /*=== sswSimSat.c ===================================================*/ extern void Ssw_ManResimulateCex( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f ); +extern void Ssw_ManResimulateCexTotal( Ssw_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr, int f ); /*=== sswSweep.c ===================================================*/ extern int Ssw_ManSweepBmc( Ssw_Man_t * p ); extern int Ssw_ManSweep( Ssw_Man_t * p ); |