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 ///
////////////////////////////////////////////////////////////////////////
|
