int2Int.h 5.88 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 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 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164
/**CFile****************************************************************

  FileName    [int2Int.h]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Interpolation engine.]

  Synopsis    [Internal declarations.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - Dec 1, 2013.]

  Revision    [$Id: int2Int.h,v 1.00 2013/12/01 00:00:00 alanmi Exp $]

***********************************************************************/
 
#ifndef ABC__Gia__int2__intInt_h
#define ABC__Gia__int2__intInt_h


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

#include "aig/gia/gia.h"
#include "sat/bsat/satSolver.h"
#include "sat/cnf/cnf.h"
#include "int2.h"

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

ABC_NAMESPACE_HEADER_START

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

// interpolation manager
typedef struct Int2_Man_t_ Int2_Man_t;
struct Int2_Man_t_
{
    // parameters
    Int2_ManPars_t * pPars;        // parameters
    // GIA managers
    Gia_Man_t *      pGia;         // original manager
    Gia_Man_t *      pGiaPref;     // prefix manager
    Gia_Man_t *      pGiaSuff;     // suffix manager
    // subset of the manager
    Vec_Int_t *      vSuffCis;     // suffix CIs
    Vec_Int_t *      vSuffCos;     // suffix COs
    Vec_Int_t *      vPrefCos;     // suffix POs
    Vec_Int_t *      vStack;       // temporary stack
    // preimages
    Vec_Int_t *      vImageOne;    // latest preimage
    Vec_Int_t *      vImagesAll;   // cumulative preimage
    // variable maps
    Vec_Ptr_t *      vMapFrames;   // mapping of GIA IDs into frame IDs
    Vec_Int_t *      vMapPref;     // mapping of flop inputs into SAT variables
    Vec_Int_t *      vMapSuff;     // mapping of flop outputs into SAT variables
    // initial minimization
    Vec_Int_t *      vAssign;      // assignment of PIs in pGiaSuff
    Vec_Int_t *      vPrio;        // priority of PIs in pGiaSuff
    // SAT solving
    sat_solver *     pSatPref;     // prefix solver
    sat_solver *     pSatSuff;     // suffix solver
    // runtime
    abctime          timeSatPref;
    abctime          timeSatSuff;
    abctime          timeOther;
    abctime          timeTotal;
};

static inline Int2_Man_t * Int2_ManCreate( Gia_Man_t * pGia, Int2_ManPars_t * pPars )
{
    Int2_Man_t * p;
    p = ABC_CALLOC( Int2_Man_t, 1 );
    p->pPars       = pPars;
    p->pGia        = pGia;
    p->pGiaPref    = Gia_ManStart( 10000 );
    // perform structural hashing
    Gia_ManHashAlloc( pFrames );
    // subset of the manager
    p->vSuffCis    = Vec_IntAlloc( Gia_ManCiNum(pGia) );
    p->vSuffCos    = Vec_IntAlloc( Gia_ManCoNum(pGia) );
    p->vPrefCos    = Vec_IntAlloc( Gia_ManCoNum(pGia) );
    p->vStack      = Vec_IntAlloc( 10000 );
    // preimages
    p->vImageOne   = Vec_IntAlloc( 1000 );
    p->vImagesAll  = Vec_IntAlloc( 1000 );
    // variable maps
    p->vMapFrames  = Vec_PtrAlloc( 100 );
    p->vMapPref    = Vec_IntAlloc( Gia_ManRegNum(pGia) );
    p->vMapSuff    = Vec_IntAlloc( Gia_ManRegNum(pGia) );
    // initial minimization
    p->vAssign     = Vec_IntAlloc( Gia_ManCiNum(pGia) );
    p->vPrio       = Vec_IntAlloc( Gia_ManCiNum(pGia) );
    return p;
}
static inline void Int2_ManStop( Int2_Man_t * p )
{
    // GIA managers
    Gia_ManStopP( &p->pGiaPref );
    Gia_ManStopP( &p->pGiaSuff );
    // subset of the manager
    Vec_IntFreeP( &p->vSuffCis );
    Vec_IntFreeP( &p->vSuffCos );
    Vec_IntFreeP( &p->vPrefCos );
    Vec_IntFreeP( &p->vStack );
    // preimages
    Vec_IntFreeP( &p->vImageOne );
    Vec_IntFreeP( &p->vImagesAll );
    // variable maps
    Vec_VecFree( (Vec_Vec_t *)p->vMapFrames );
    Vec_IntFreeP( &p->vMapPref );
    Vec_IntFreeP( &p->vMapSuff );
    // initial minimization
    Vec_IntFreeP( &p->vAssign );
    Vec_IntFreeP( &p->vPrio );
    // SAT solving
    if ( p->pSatPref )
        sat_solver_delete( p->pSatPref );
    if ( p->timeSatSuff )
        sat_solver_delete( p->pSatSuff );
    ABC_FREE( p );
}

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

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

/*=== int2Bmc.c =============================================================*/
extern int           Int2_ManCheckInit( Gia_Man_t * p );
extern Gia_Man_t *   Int2_ManDupInit( Gia_Man_t * p, int fVerbose );
extern sat_solver *  Int2_ManSetupBmcSolver( Gia_Man_t * p, int nFrames );
extern void          Int2_ManCreateFrames( Int2_Man_t * p, int iFrame, Vec_Int_t * vPrefCos );
extern int           Int2_ManCheckBmc( Int2_Man_t * p, Vec_Int_t * vCube );

/*=== int2Refine.c =============================================================*/
extern Vec_Int_t *   Int2_ManRefineCube( Gia_Man_t * p, Vec_Int_t * vAssign, Vec_Int_t * vPrio );

/*=== int2Util.c ============================================================*/
extern Gia_Man_t *   Int2_ManProbToGia( Gia_Man_t * p, Vec_Int_t * vSop );


ABC_NAMESPACE_HEADER_END



#endif

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