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
|
/**CFile****************************************************************
FileName [intInt.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 - June 24, 2008.]
Revision [$Id: intInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
#ifndef ABC__aig__int__intInt_h
#define ABC__aig__int__intInt_h
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "aig/saig/saig.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satSolver.h"
#include "sat/bsat/satStore.h"
#include "int.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_HEADER_START
////////////////////////////////////////////////////////////////////////
/// BASIC TYPES ///
////////////////////////////////////////////////////////////////////////
// interpolation manager
typedef struct Inter_Man_t_ Inter_Man_t;
struct Inter_Man_t_
{
// AIG manager
Aig_Man_t * pAig; // the original AIG manager
Aig_Man_t * pAigTrans; // the transformed original AIG manager
Cnf_Dat_t * pCnfAig; // CNF for the original manager
// interpolant
Aig_Man_t * pInter; // the current interpolant
Cnf_Dat_t * pCnfInter; // CNF for the current interplant
// timeframes
Aig_Man_t * pFrames; // the timeframes
Cnf_Dat_t * pCnfFrames; // CNF for the timeframes
// other data
Vec_Int_t * vVarsAB; // the variables participating in
// temporary place for the new interpolant
Aig_Man_t * pInterNew;
Vec_Ptr_t * vInters;
// parameters
int nFrames; // the number of timeframes
int nConfCur; // the current number of conflicts
int nConfLimit; // the limit on the number of conflicts
int fVerbose; // the verbosiness flag
char * pFileName;
// runtime
abctime timeRwr;
abctime timeCnf;
abctime timeSat;
abctime timeInt;
abctime timeEqu;
abctime timeOther;
abctime timeTotal;
};
// containment checking manager
typedef struct Inter_Check_t_ Inter_Check_t;
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== intCheck.c ============================================================*/
extern Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK );
extern void Inter_CheckStop( Inter_Check_t * p );
extern int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, abctime nTimeNewOut );
/*=== intContain.c ============================================================*/
extern int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld );
extern int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld );
extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
/*=== intCtrex.c ============================================================*/
extern void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose );
/*=== intDup.c ============================================================*/
extern Aig_Man_t * Inter_ManStartInitState( int nRegs );
extern Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p );
extern Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo );
/*=== intFrames.c ============================================================*/
extern Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts, int fUseTwoFrames );
/*=== intMan.c ============================================================*/
extern Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars );
extern void Inter_ManClean( Inter_Man_t * p );
extern void Inter_ManStop( Inter_Man_t * p, int fProved );
/*=== intM114.c ============================================================*/
extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, abctime nTimeNewOut );
/*=== intM114p.c ============================================================*/
#ifdef ABC_USE_LIBRARIES
extern int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther );
#endif
/*=== intUtil.c ============================================================*/
extern int Inter_ManCheckInitialState( Aig_Man_t * p );
extern int Inter_ManCheckAllStates( Aig_Man_t * p );
ABC_NAMESPACE_HEADER_END
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
