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
|
/**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 );
/*=== 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 );
/*=== 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 ///
////////////////////////////////////////////////////////////////////////
|
