sscInt.h 6.33 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48
/**CFile****************************************************************

  FileName    [sscInt.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Choice computation for tech-mapping.]

  Synopsis    [Internal declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 29, 2008.]

  Revision    [$Id: sscInt.h,v 1.00 2008/07/29 00:00:00 alanmi Exp $]

***********************************************************************/
 
#ifndef ABC__aig__ssc__sscInt_h
#define ABC__aig__ssc__sscInt_h


////////////////////////////////////////////////////////////////////////
///                          INCLUDES                                ///
////////////////////////////////////////////////////////////////////////

#include "aig/gia/gia.h"
#include "sat/bsat/satSolver.h"
#include "ssc.h"

////////////////////////////////////////////////////////////////////////
///                         PARAMETERS                               ///
////////////////////////////////////////////////////////////////////////


ABC_NAMESPACE_HEADER_START


////////////////////////////////////////////////////////////////////////
///                         BASIC TYPES                              ///
////////////////////////////////////////////////////////////////////////

// choicing manager
typedef struct Ssc_Man_t_ Ssc_Man_t;
struct Ssc_Man_t_
{
49
    // user data
50 51 52
    Ssc_Pars_t *     pPars;          // choicing parameters
    Gia_Man_t *      pAig;           // subject AIG
    Gia_Man_t *      pCare;          // care set AIG
53
    // internal data
54 55
    Gia_Man_t *      pFraig;         // resulting AIG
    sat_solver *     pSat;           // recyclable SAT solver
56 57 58 59 60 61 62 63 64 65 66
    Vec_Int_t *      vId2Var;        // mapping of each node into its SAT var
    Vec_Int_t *      vVar2Id;        // mapping of each SAT var into its node
    Vec_Int_t *      vPivot;         // one SAT pattern
    int              nSatVarsPivot;  // the number of variables for constraints
    int              nSatVars;       // the current number of variables  
    // temporary storage
    Vec_Int_t *      vFront;         // supergate fanins
    Vec_Int_t *      vFanins;        // supergate fanins
    Vec_Int_t *      vPattern;       // counter-example
    Vec_Int_t *      vDisPairs;      // disproved pairs
    // SAT calls statistics
67
    int              nSimRounds;     // the number of simulation rounds
68 69 70 71 72
    int              nRecycles;      // the number of times SAT solver was recycled
    int              nCallsSince;    // the number of calls since the last recycle
    int              nSatCalls;      // the number of SAT calls
    int              nSatCallsUnsat; // the number of unsat SAT calls
    int              nSatCallsSat;   // the number of sat SAT calls
73
    int              nSatCallsUndec; // the number of undec SAT calls
74
    // runtime stats
75 76 77 78 79 80 81 82 83
    abctime          timeSimInit;    // simulation and class computation
    abctime          timeSimSat;     // simulation of the counter-examples
    abctime          timeCnfGen;     // generation of CNF
    abctime          timeSat;        // total SAT time
    abctime          timeSatSat;     // sat
    abctime          timeSatUnsat;   // unsat
    abctime          timeSatUndec;   // undecided
    abctime          timeOther;      // other runtime
    abctime          timeTotal;      // total runtime
84 85 86 87 88 89
};

////////////////////////////////////////////////////////////////////////
///                      MACRO DEFINITIONS                           ///
////////////////////////////////////////////////////////////////////////

90 91 92
static inline int    Ssc_ObjSatVar( Ssc_Man_t * p, int iObj )             { return Vec_IntEntry(p->vId2Var, iObj);     }
static inline void   Ssc_ObjSetSatVar( Ssc_Man_t * p, int iObj, int Num ) { Vec_IntWriteEntry(p->vId2Var, iObj, Num);  Vec_IntWriteEntry(p->vVar2Id, Num, iObj);  }
static inline void   Ssc_ObjCleanSatVar( Ssc_Man_t * p, int Num )         { Vec_IntWriteEntry(p->vId2Var, Vec_IntEntry(p->vVar2Id, Num), Num);  Vec_IntWriteEntry(p->vVar2Id, Num, 0);                        }
93

94 95
static inline int    Ssc_ObjFraig( Ssc_Man_t * p, Gia_Obj_t * pObj )      { return pObj->Value;           }
static inline void   Ssc_ObjSetFraig( Gia_Obj_t * pObj, int iNode )       { pObj->Value = iNode;          }
96 97 98 99 100 101

////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

/*=== sscClass.c =================================================*/
102
extern void          Ssc_GiaClassesInit( Gia_Man_t * p );
103
extern int           Ssc_GiaClassesRefine( Gia_Man_t * p );
104
extern void          Ssc_GiaClassesCheckPairs( Gia_Man_t * p, Vec_Int_t * vDisPairs );
105
extern int           Ssc_GiaSimClassRefineOneBit( Gia_Man_t * p, int i );
106 107 108 109 110 111 112
/*=== sscCnf.c ===================================================*/
extern void          Ssc_CnfNodeAddToSolver( Ssc_Man_t * p, Gia_Obj_t * pObj );
/*=== sscCore.c ==================================================*/
/*=== sscSat.c ===================================================*/
extern void          Ssc_ManSatSolverRecycle( Ssc_Man_t * p );
extern void          Ssc_ManStartSolver( Ssc_Man_t * p );
extern Vec_Int_t *   Ssc_ManFindPivotSat( Ssc_Man_t * p );
113
extern int           Ssc_ManCheckEquivalence( Ssc_Man_t * p, int iRepr, int iObj, int fCompl );
114
/*=== sscSim.c ===================================================*/
115
extern void          Ssc_GiaResetPiPattern( Gia_Man_t * p, int nWords );
116
extern void          Ssc_GiaRandomPiPattern( Gia_Man_t * p, int nWords, Vec_Int_t * vPivot );
117
extern int           Ssc_GiaTransferPiPattern( Gia_Man_t * pAig, Gia_Man_t * pCare, Vec_Int_t * vPivot );
118
extern void          Ssc_GiaSavePiPattern( Gia_Man_t * p, Vec_Int_t * vPat );
119 120
extern void          Ssc_GiaSimRound( Gia_Man_t * p );
extern Vec_Int_t *   Ssc_GiaFindPivotSim( Gia_Man_t * p );
121
extern int           Ssc_GiaEstimateCare( Gia_Man_t * p, int nWords );
122 123 124 125 126 127 128 129 130 131 132 133 134 135
/*=== sscUtil.c ===================================================*/
extern Gia_Man_t *   Ssc_GenerateOneHot( int nVars );


ABC_NAMESPACE_HEADER_END



#endif

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////