1 /**CFile****************************************************************
2
3 FileName [intCore.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Interpolation engine.]
8
9 Synopsis [Core 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: intCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "intInt.h"
22 #include "sat/bmc/bmc.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 [This procedure sets default values of interpolation parameters.]
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Inter_ManSetDefaultParams(Inter_ManParams_t * p)46 void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
47 {
48 memset( p, 0, sizeof(Inter_ManParams_t) );
49 p->nBTLimit = 0; // limit on the number of conflicts
50 p->nFramesMax = 0; // the max number timeframes to unroll
51 p->nSecLimit = 0; // time limit in seconds
52 p->nFramesK = 1; // the number of timeframes to use in induction
53 p->fRewrite = 0; // use additional rewriting to simplify timeframes
54 p->fTransLoop = 0; // add transition into the init state under new PI var
55 p->fUsePudlak = 0; // use Pudluk interpolation procedure
56 p->fUseOther = 0; // use other undisclosed option
57 p->fUseMiniSat = 0; // use MiniSat-1.14p instead of internal proof engine
58 p->fCheckKstep = 1; // check using K-step induction
59 p->fUseBias = 0; // bias decisions to global variables
60 p->fUseBackward = 0; // perform backward interpolation
61 p->fUseSeparate = 0; // solve each output separately
62 p->fUseTwoFrames = 0; // create OR of two last timeframes
63 p->fDropSatOuts = 0; // replace by 1 the solved outputs
64 p->fVerbose = 0; // print verbose statistics
65 p->iFrameMax =-1;
66 }
67
68 /**Function*************************************************************
69
70 Synopsis [Interplates while the number of conflicts is not exceeded.]
71
72 Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
73
74 SideEffects [Does not check the property in 0-th frame.]
75
76 SeeAlso []
77
78 ***********************************************************************/
Inter_ManPerformInterpolation(Aig_Man_t * pAig,Inter_ManParams_t * pPars,int * piFrame)79 int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * piFrame )
80 {
81 extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
82 Inter_Man_t * p;
83 Inter_Check_t * pCheck = NULL;
84 Aig_Man_t * pAigTemp;
85 int s, i, RetValue, Status;
86 abctime clk, clk2, clkTotal = Abc_Clock(), timeTemp = 0;
87 abctime nTimeNewOut = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
88
89 // enable ORing of the interpolants, if containment check is performed inductively with K > 1
90 if ( pPars->nFramesK > 1 )
91 pPars->fTransLoop = 1;
92
93 // sanity checks
94 assert( Saig_ManRegNum(pAig) > 0 );
95 assert( Saig_ManPiNum(pAig) > 0 );
96 assert( Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) == 1 );
97 if ( pPars->fVerbose && Saig_ManConstrNum(pAig) )
98 printf( "Performing interpolation with %d constraints...\n", Saig_ManConstrNum(pAig) );
99
100 if ( Inter_ManCheckInitialState(pAig) )
101 {
102 *piFrame = -1;
103 printf( "Property trivially fails in the initial state.\n" );
104 return 0;
105 }
106 /*
107 if ( Inter_ManCheckAllStates(pAig) )
108 {
109 printf( "Property trivially holds in all states.\n" );
110 return 1;
111 }
112 */
113 // create interpolation manager
114 // can perform SAT sweeping and/or rewriting of this AIG...
115 p = Inter_ManCreate( pAig, pPars );
116 if ( pPars->fTransLoop )
117 p->pAigTrans = Inter_ManStartOneOutput( pAig, 0 );
118 else
119 p->pAigTrans = Inter_ManStartDuplicated( pAig );
120 // derive CNF for the transformed AIG
121 clk = Abc_Clock();
122 p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) );
123 p->timeCnf += Abc_Clock() - clk;
124 if ( pPars->fVerbose )
125 {
126 printf( "AIG: PI/PO/Reg = %d/%d/%d. And = %d. Lev = %d. CNF: Var/Cla = %d/%d.\n",
127 Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
128 Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig),
129 p->pCnfAig->nVars, p->pCnfAig->nClauses );
130 }
131
132 // derive interpolant
133 *piFrame = -1;
134 p->nFrames = 1;
135 for ( s = 0; ; s++ )
136 {
137 Cnf_Dat_t * pCnfInter2;
138
139 clk2 = Abc_Clock();
140 // initial state
141 if ( pPars->fUseBackward )
142 p->pInter = Inter_ManStartOneOutput( pAig, 1 );
143 else
144 p->pInter = Inter_ManStartInitState( Aig_ManRegNum(pAig) );
145 assert( Aig_ManCoNum(p->pInter) == 1 );
146 clk = Abc_Clock();
147 p->pCnfInter = Cnf_Derive( p->pInter, 0 );
148 p->timeCnf += Abc_Clock() - clk;
149 // timeframes
150 p->pFrames = Inter_ManFramesInter( pAig, p->nFrames, pPars->fUseBackward, pPars->fUseTwoFrames );
151 clk = Abc_Clock();
152 if ( pPars->fRewrite )
153 {
154 p->pFrames = Dar_ManRwsat( pAigTemp = p->pFrames, 1, 0 );
155 Aig_ManStop( pAigTemp );
156 // p->pFrames = Fra_FraigEquivence( pAigTemp = p->pFrames, 100, 0 );
157 // Aig_ManStop( pAigTemp );
158 }
159 p->timeRwr += Abc_Clock() - clk;
160 // can also do SAT sweeping on the timeframes...
161 clk = Abc_Clock();
162 if ( pPars->fUseBackward )
163 p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManCoNum(p->pFrames) );
164 else
165 // p->pCnfFrames = Cnf_Derive( p->pFrames, 0 );
166 p->pCnfFrames = Cnf_DeriveSimple( p->pFrames, 0 );
167 p->timeCnf += Abc_Clock() - clk;
168 // report statistics
169 if ( pPars->fVerbose )
170 {
171 printf( "Step = %2d. Frames = 1 + %d. And = %5d. Lev = %5d. ",
172 s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) );
173 ABC_PRT( "Time", Abc_Clock() - clk2 );
174 }
175
176
177 //////////////////////////////////////////
178 // start containment checking
179 if ( !(pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1) )
180 {
181 pCheck = Inter_CheckStart( p->pAigTrans, pPars->nFramesK );
182 // try new containment check for the initial state
183 clk = Abc_Clock();
184 pCnfInter2 = Cnf_Derive( p->pInter, 1 );
185 p->timeCnf += Abc_Clock() - clk;
186 clk = Abc_Clock();
187 RetValue = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
188 p->timeEqu += Abc_Clock() - clk;
189 // assert( RetValue == 0 );
190 Cnf_DataFree( pCnfInter2 );
191 if ( p->vInters )
192 Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInter) );
193 }
194 //////////////////////////////////////////
195
196 // iterate the interpolation procedure
197 for ( i = 0; ; i++ )
198 {
199 if ( pPars->nFramesMax && p->nFrames + i >= pPars->nFramesMax )
200 {
201 if ( pPars->fVerbose )
202 printf( "Reached limit (%d) on the number of timeframes.\n", pPars->nFramesMax );
203 p->timeTotal = Abc_Clock() - clkTotal;
204 Inter_ManStop( p, 0 );
205 Inter_CheckStop( pCheck );
206 return -1;
207 }
208
209 // perform interpolation
210 clk = Abc_Clock();
211 #ifdef ABC_USE_LIBRARIES
212 if ( pPars->fUseMiniSat )
213 {
214 assert( !pPars->fUseBackward );
215 RetValue = Inter_ManPerformOneStepM114p( p, pPars->fUsePudlak, pPars->fUseOther );
216 }
217 else
218 #endif
219 RetValue = Inter_ManPerformOneStep( p, pPars->fUseBias, pPars->fUseBackward, nTimeNewOut );
220
221 if ( pPars->fVerbose )
222 {
223 printf( " I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d. ",
224 i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur );
225 ABC_PRT( "Time", Abc_Clock() - clk );
226 }
227 // remember the number of timeframes completed
228 pPars->iFrameMax = i - 1 + p->nFrames;
229 if ( RetValue == 0 ) // found a (spurious?) counter-example
230 {
231 if ( i == 0 ) // real counterexample
232 {
233 if ( pPars->fVerbose )
234 printf( "Found a real counterexample in frame %d.\n", p->nFrames );
235 p->timeTotal = Abc_Clock() - clkTotal;
236 *piFrame = p->nFrames;
237 // pAig->pSeqModel = (Abc_Cex_t *)Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose );
238 {
239 int RetValue;
240 Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc;
241 Saig_ParBmcSetDefaultParams( pParsBmc );
242 pParsBmc->nConfLimit = 100000000;
243 pParsBmc->nStart = p->nFrames;
244 pParsBmc->fVerbose = pPars->fVerbose;
245 RetValue = Saig_ManBmcScalable( pAig, pParsBmc );
246 if ( RetValue == 1 )
247 printf( "Error: The problem should be SAT but it is UNSAT.\n" );
248 else if ( RetValue == -1 )
249 printf( "Error: The problem timed out.\n" );
250 }
251 Inter_ManStop( p, 0 );
252 Inter_CheckStop( pCheck );
253 return 0;
254 }
255 // likely spurious counter-example
256 p->nFrames += i;
257 Inter_ManClean( p );
258 break;
259 }
260 else if ( RetValue == -1 )
261 {
262 if ( pPars->nSecLimit && Abc_Clock() > nTimeNewOut ) // timed out
263 {
264 if ( pPars->fVerbose )
265 printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit );
266 }
267 else
268 {
269 assert( p->nConfCur >= p->nConfLimit );
270 if ( pPars->fVerbose )
271 printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
272 }
273 p->timeTotal = Abc_Clock() - clkTotal;
274 Inter_ManStop( p, 0 );
275 Inter_CheckStop( pCheck );
276 return -1;
277 }
278 assert( RetValue == 1 ); // found new interpolant
279 // compress the interpolant
280 clk = Abc_Clock();
281 if ( p->pInterNew )
282 {
283 // save the timeout value
284 p->pInterNew->Time2Quit = nTimeNewOut;
285 // Ioa_WriteAiger( p->pInterNew, "interpol.aig", 0, 0 );
286 p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
287 // p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 0, 0 );
288 Aig_ManStop( pAigTemp );
289 if ( p->pInterNew == NULL )
290 {
291 printf( "Reached timeout (%d seconds) during rewriting.\n", pPars->nSecLimit );
292 p->timeTotal = Abc_Clock() - clkTotal;
293 Inter_ManStop( p, 1 );
294 Inter_CheckStop( pCheck );
295 return -1;
296 }
297 }
298 p->timeRwr += Abc_Clock() - clk;
299
300 // check if interpolant is trivial
301 if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManCo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) )
302 {
303 // printf( "interpolant is constant 0\n" );
304 if ( pPars->fVerbose )
305 printf( "The problem is trivially true for all states.\n" );
306 p->timeTotal = Abc_Clock() - clkTotal;
307 Inter_ManStop( p, 1 );
308 Inter_CheckStop( pCheck );
309 return 1;
310 }
311
312 // check containment of interpolants
313 clk = Abc_Clock();
314 if ( pPars->fCheckKstep ) // k-step unique-state induction
315 {
316 if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) )
317 {
318 if ( pPars->fTransLoop || pPars->fUseBackward || pPars->nFramesK > 1 )
319 {
320 clk2 = Abc_Clock();
321 Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, Abc_MinInt(i + 1, pPars->nFramesK), pPars->fUseBackward );
322 timeTemp = Abc_Clock() - clk2;
323 }
324 else
325 { // new containment check
326 clk2 = Abc_Clock();
327 pCnfInter2 = Cnf_Derive( p->pInterNew, 1 );
328 p->timeCnf += Abc_Clock() - clk2;
329 timeTemp = Abc_Clock() - clk2;
330
331 Status = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
332 Cnf_DataFree( pCnfInter2 );
333 if ( p->vInters )
334 Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInterNew) );
335 }
336 }
337 else
338 Status = 0;
339 }
340 else // combinational containment
341 {
342 if ( Aig_ManCiNum(p->pInterNew) == Aig_ManCiNum(p->pInter) )
343 Status = Inter_ManCheckContainment( p->pInterNew, p->pInter );
344 else
345 Status = 0;
346 }
347 p->timeEqu += Abc_Clock() - clk - timeTemp;
348 if ( Status ) // contained
349 {
350 if ( pPars->fVerbose )
351 printf( "Proved containment of interpolants.\n" );
352 p->timeTotal = Abc_Clock() - clkTotal;
353 Inter_ManStop( p, 1 );
354 Inter_CheckStop( pCheck );
355 return 1;
356 }
357 if ( pPars->nSecLimit && Abc_Clock() > nTimeNewOut )
358 {
359 printf( "Reached timeout (%d seconds).\n", pPars->nSecLimit );
360 p->timeTotal = Abc_Clock() - clkTotal;
361 Inter_ManStop( p, 1 );
362 Inter_CheckStop( pCheck );
363 return -1;
364 }
365 // save interpolant and convert it into CNF
366 if ( pPars->fTransLoop )
367 {
368 Aig_ManStop( p->pInter );
369 p->pInter = p->pInterNew;
370 }
371 else
372 {
373 if ( pPars->fUseBackward )
374 {
375 p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 );
376 Aig_ManStop( pAigTemp );
377 Aig_ManStop( p->pInterNew );
378 // compress the interpolant
379 clk = Abc_Clock();
380 p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 );
381 Aig_ManStop( pAigTemp );
382 p->timeRwr += Abc_Clock() - clk;
383 }
384 else // forward with the new containment checking (using only the frontier)
385 {
386 Aig_ManStop( p->pInter );
387 p->pInter = p->pInterNew;
388 }
389 }
390 p->pInterNew = NULL;
391 Cnf_DataFree( p->pCnfInter );
392 clk = Abc_Clock();
393 p->pCnfInter = Cnf_Derive( p->pInter, 0 );
394 p->timeCnf += Abc_Clock() - clk;
395 }
396
397 // start containment checking
398 Inter_CheckStop( pCheck );
399 }
400 assert( 0 );
401 return RetValue;
402 }
403
404
405
406 ////////////////////////////////////////////////////////////////////////
407 /// END OF FILE ///
408 ////////////////////////////////////////////////////////////////////////
409
410
411 ABC_NAMESPACE_IMPL_END
412
413