1 /**CFile****************************************************************
2
3 FileName [intMan.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Interpolation engine.]
8
9 Synopsis [Interpolation manager procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 24, 2008.]
16
17 Revision [$Id: intMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "intInt.h"
22 #include "aig/ioa/ioa.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34
35 /**Function*************************************************************
36
37 Synopsis [Creates the interpolation manager.]
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Inter_ManCreate(Aig_Man_t * pAig,Inter_ManParams_t * pPars)46 Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars )
47 {
48 Inter_Man_t * p;
49 // create interpolation manager
50 p = ABC_ALLOC( Inter_Man_t, 1 );
51 memset( p, 0, sizeof(Inter_Man_t) );
52 p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) );
53 p->nConfLimit = pPars->nBTLimit;
54 p->fVerbose = pPars->fVerbose;
55 p->pFileName = pPars->pFileName;
56 p->pAig = pAig;
57 if ( pPars->fDropInvar )
58 p->vInters = Vec_PtrAlloc( 100 );
59 return p;
60 }
61
62 /**Function*************************************************************
63
64 Synopsis [Cleans the interpolation manager.]
65
66 Description []
67
68 SideEffects []
69
70 SeeAlso []
71
72 ***********************************************************************/
Inter_ManClean(Inter_Man_t * p)73 void Inter_ManClean( Inter_Man_t * p )
74 {
75 if ( p->vInters )
76 {
77 Aig_Man_t * pMan;
78 int i;
79 Vec_PtrForEachEntry( Aig_Man_t *, p->vInters, pMan, i )
80 Aig_ManStop( pMan );
81 Vec_PtrClear( p->vInters );
82 }
83 if ( p->pCnfInter )
84 Cnf_DataFree( p->pCnfInter );
85 if ( p->pCnfFrames )
86 Cnf_DataFree( p->pCnfFrames );
87 if ( p->pInter )
88 Aig_ManStop( p->pInter );
89 if ( p->pFrames )
90 Aig_ManStop( p->pFrames );
91 }
92
93 /**Function*************************************************************
94
95 Synopsis [Writes interpolant into a file.]
96
97 Description []
98
99 SideEffects []
100
101 SeeAlso []
102
103 ***********************************************************************/
Inter_ManInterDump(Inter_Man_t * p,int fProved)104 void Inter_ManInterDump( Inter_Man_t * p, int fProved )
105 {
106 char * pFileName = p->pFileName ? p->pFileName : (char *)"invar.aig";
107 Aig_Man_t * pMan;
108 pMan = Aig_ManDupArray( p->vInters );
109 Ioa_WriteAiger( pMan, pFileName, 0, 0 );
110 Aig_ManStop( pMan );
111 if ( fProved )
112 printf( "Inductive invariant is dumped into file \"%s\".\n", pFileName );
113 else
114 printf( "Interpolants are dumped into file \"%s\".\n", pFileName );
115 }
116
117 /**Function*************************************************************
118
119 Synopsis [Frees the interpolation manager.]
120
121 Description []
122
123 SideEffects []
124
125 SeeAlso []
126
127 ***********************************************************************/
Inter_ManStop(Inter_Man_t * p,int fProved)128 void Inter_ManStop( Inter_Man_t * p, int fProved )
129 {
130 if ( p->fVerbose )
131 {
132 p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu;
133 printf( "Runtime statistics:\n" );
134 ABC_PRTP( "Rewriting ", p->timeRwr, p->timeTotal );
135 ABC_PRTP( "CNF mapping", p->timeCnf, p->timeTotal );
136 ABC_PRTP( "SAT solving", p->timeSat, p->timeTotal );
137 ABC_PRTP( "Interpol ", p->timeInt, p->timeTotal );
138 ABC_PRTP( "Containment", p->timeEqu, p->timeTotal );
139 ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
140 ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
141 }
142
143 if ( p->vInters )
144 Inter_ManInterDump( p, fProved );
145
146 if ( p->pCnfAig )
147 Cnf_DataFree( p->pCnfAig );
148 if ( p->pAigTrans )
149 Aig_ManStop( p->pAigTrans );
150 if ( p->pInterNew )
151 Aig_ManStop( p->pInterNew );
152 Inter_ManClean( p );
153 Vec_PtrFreeP( &p->vInters );
154 Vec_IntFreeP( &p->vVarsAB );
155 ABC_FREE( p );
156 }
157
158
159 ////////////////////////////////////////////////////////////////////////
160 /// END OF FILE ///
161 ////////////////////////////////////////////////////////////////////////
162
163
164 ABC_NAMESPACE_IMPL_END
165
166