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
|
/**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 __INT_INT_H__
#define __INT_INT_H__
#ifdef __cplusplus
extern "C" {
#endif
////////////////////////////////////////////////////////////////////////
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
#include "saig.h"
#include "cnf.h"
#include "satSolver.h"
#include "satStore.h"
#include "int.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// 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
// runtime
int timeRwr;
int timeCnf;
int timeSat;
int timeInt;
int timeEqu;
int timeOther;
int timeTotal;
};
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== 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 );
/*=== 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 );
/*=== 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 );
/*=== intM114.c ==========================================================*/
extern int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward );
/*=== 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 );
#ifdef __cplusplus
}
#endif
#endif
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
|
