absRef.h 5.73 KB
Newer Older
1 2
/**CFile****************************************************************

3
  FileName    [absRef.h]
4 5 6

  SystemName  [ABC: Logic synthesis and verification system.]

7
  PackageName [Abstraction package.]
8 9 10 11 12 13 14 15 16

  Synopsis    [Refinement manager.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

17
  Revision    [$Id: absRef.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 19 20

***********************************************************************/
 
21 22
#ifndef ABC__proof_abs__AbsRef_h
#define ABC__proof_abs__AbsRef_h
23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44


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

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

ABC_NAMESPACE_HEADER_START


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


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

45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85
typedef struct Rnm_Obj_t_ Rnm_Obj_t; // refinement object
struct Rnm_Obj_t_
{
    unsigned        Value     :  1;  // binary value
    unsigned        fVisit    :  1;  // visited object
    unsigned        fVisitJ   :  1;  // justified visited object
    unsigned        fPPi      :  1;  // PPI object
    unsigned        Prio      : 24;  // priority (0 - highest)
};

typedef struct Rnm_Man_t_ Rnm_Man_t; // refinement manager
struct Rnm_Man_t_
{
    // user data
    Gia_Man_t *     pGia;            // working AIG manager (it is completely owned by this package)
    Abc_Cex_t *     pCex;            // counter-example
    Vec_Int_t *     vMap;            // mapping of CEX inputs into objects (PI + PPI, in any order)
    int             fPropFanout;     // propagate fanouts
    int             fVerbose;        // verbose flag
    int             nRefId;          // refinement ID
    // traversing data
    Vec_Int_t *     vObjs;           // internal objects used in value propagation
    // filtering of selected objects
    Vec_Str_t *     vCounts;         // fanin counters
    Vec_Int_t *     vFanins;         // fanins
/*
    // SAT solver
    sat_solver2 *   pSat;            // incremental SAT solver
    Vec_Int_t *     vSatVars;        // SAT variables
    Vec_Int_t *     vSat2Ids;        // mapping of SAT variables into object IDs
    Vec_Int_t *     vIsopMem;        // memory for ISOP computation
*/
    // internal data
    Rnm_Obj_t *     pObjs;           // refinement objects
    int             nObjs;           // the number of used objects
    int             nObjsAlloc;      // the number of allocated objects
    int             nObjsFrame;      // the number of used objects in each frame
    int             nCalls;          // total number of calls
    int             nRefines;        // total refined objects
    int             nVisited;        // visited during justification
    // statistics  
86 87 88 89
    abctime         timeFwd;         // forward propagation
    abctime         timeBwd;         // backward propagation
    abctime         timeVer;         // ternary simulation
    abctime         timeTotal;       // other time
90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107
};

// accessing the refinement object
static inline Rnm_Obj_t * Rnm_ManObj( Rnm_Man_t * p, Gia_Obj_t * pObj, int f )  
{ 
    assert( Gia_ObjIsConst0(pObj) || pObj->Value );
    assert( (int)pObj->Value < p->nObjsFrame );
    assert( f >= 0 && f <= p->pCex->iFrame ); 
    return p->pObjs + f * p->nObjsFrame + pObj->Value;  
}
static inline void  Rnm_ManSetRefId( Rnm_Man_t * p, int RefId )               { p->nRefId = RefId; }

static inline int   Rnm_ObjCount( Rnm_Man_t * p, Gia_Obj_t * pObj )           { return Vec_StrEntry( p->vCounts, Gia_ObjId(p->pGia, pObj) );                           }
static inline void  Rnm_ObjSetCount( Rnm_Man_t * p, Gia_Obj_t * pObj, int c ) { Vec_StrWriteEntry( p->vCounts, Gia_ObjId(p->pGia, pObj), (char)c );                    }
static inline int   Rnm_ObjAddToCount( Rnm_Man_t * p, Gia_Obj_t * pObj )      { int c = Rnm_ObjCount(p, pObj); if ( c < 16 )  Rnm_ObjSetCount(p, pObj, c+1); return c; }

static inline int   Rnm_ObjIsJust( Rnm_Man_t * p, Gia_Obj_t * pObj )          { return Gia_ObjIsConst0(pObj) || (pObj->Value && Rnm_ManObj(p, pObj, 0)->fVisitJ);      }

108 109 110 111
////////////////////////////////////////////////////////////////////////
///                    FUNCTION DECLARATIONS                         ///
////////////////////////////////////////////////////////////////////////

112
/*=== absRef.c ===========================================================*/
113 114 115
extern Rnm_Man_t *  Rnm_ManStart( Gia_Man_t * pGia );
extern void         Rnm_ManStop( Rnm_Man_t * p, int fProfile );
extern double       Rnm_ManMemoryUsage( Rnm_Man_t * p );
116 117 118 119
extern Vec_Int_t *  Rnm_ManRefine( Rnm_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vMap, int fPropFanout, int fNewRefinement, int fVerbose );
/*=== absRefSelected.c ===========================================================*/
extern Vec_Int_t *  Rnm_ManFilterSelected( Rnm_Man_t * p, Vec_Int_t * vOldPPis );
extern Vec_Int_t *  Rnm_ManFilterSelectedNew( Rnm_Man_t * p, Vec_Int_t * vOldPPis );
120 121 122 123 124 125 126 127 128 129


ABC_NAMESPACE_HEADER_END

#endif

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