1 /**CFile****************************************************************
2
3 FileName [fraClaus.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [New FRAIG package.]
8
9 Synopsis [Induction with clause strengthening.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 30, 2007.]
16
17 Revision [$Id: fraClau.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "fra.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satSolver.h"
24
25 ABC_NAMESPACE_IMPL_START
26
27
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31
32 typedef struct Clu_Man_t_ Clu_Man_t;
33 struct Clu_Man_t_
34 {
35 // parameters
36 int nFrames; // the K of the K-step induction
37 int nPref; // the number of timeframes to skip
38 int nClausesMax; // the max number of 4-clauses to consider
39 int nLutSize; // the max cut size
40 int nLevels; // the number of levels for cut computation
41 int nCutsMax; // the maximum number of cuts to compute at a node
42 int nBatches; // the number of clause batches to use
43 int fStepUp; // increase cut size for each batch
44 int fTarget; // tries to prove the property
45 int fVerbose;
46 int fVeryVerbose;
47 // internal parameters
48 int nSimWords; // the number of simulation words
49 int nSimWordsPref; // the number of simulation words in the prefix
50 int nSimFrames; // the number of frames to simulate
51 int nBTLimit; // the largest number of backtracks (0 = infinite)
52 // the network
53 Aig_Man_t * pAig;
54 // SAT solvers
55 sat_solver * pSatMain;
56 sat_solver * pSatBmc;
57 // CNF for the test solver
58 Cnf_Dat_t * pCnf;
59 int fFail;
60 int fFiltering;
61 int fNothingNew;
62 // clauses
63 Vec_Int_t * vLits;
64 Vec_Int_t * vClauses;
65 Vec_Int_t * vCosts;
66 int nClauses;
67 int nCuts;
68 int nOneHots;
69 int nOneHotsProven;
70 // clauses proven
71 Vec_Int_t * vLitsProven;
72 Vec_Int_t * vClausesProven;
73 // counter-examples
74 Vec_Ptr_t * vCexes;
75 int nCexes;
76 int nCexesAlloc;
77 };
78
79 ////////////////////////////////////////////////////////////////////////
80 /// FUNCTION DEFINITIONS ///
81 ////////////////////////////////////////////////////////////////////////
82
83 /**Function*************************************************************
84
85 Synopsis [Runs the SAT solver on the problem.]
86
87 Description []
88
89 SideEffects []
90
91 SeeAlso []
92
93 ***********************************************************************/
Fra_ClausRunBmc(Clu_Man_t * p)94 int Fra_ClausRunBmc( Clu_Man_t * p )
95 {
96 Aig_Obj_t * pObj;
97 int Lits[2], nLitsTot, RetValue, i;
98 // set the output literals
99 nLitsTot = 2 * p->pCnf->nVars;
100 pObj = Aig_ManCo(p->pAig, 0);
101 for ( i = 0; i < p->nPref + p->nFrames; i++ )
102 {
103 Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
104 RetValue = sat_solver_solve( p->pSatBmc, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
105 if ( RetValue != l_False )
106 return 0;
107 }
108 return 1;
109 }
110
111 /**Function*************************************************************
112
113 Synopsis [Runs the SAT solver on the problem.]
114
115 Description []
116
117 SideEffects []
118
119 SeeAlso []
120
121 ***********************************************************************/
Fra_ClausRunSat(Clu_Man_t * p)122 int Fra_ClausRunSat( Clu_Man_t * p )
123 {
124 Aig_Obj_t * pObj;
125 int * pLits;
126 int i, RetValue;
127 pLits = ABC_ALLOC( int, p->nFrames + 1 );
128 // set the output literals
129 pObj = Aig_ManCo(p->pAig, 0);
130 for ( i = 0; i <= p->nFrames; i++ )
131 pLits[i] = i * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObj->Id], i != p->nFrames );
132 // try to solve the problem
133 RetValue = sat_solver_solve( p->pSatMain, pLits, pLits + p->nFrames + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
134 ABC_FREE( pLits );
135 if ( RetValue == l_False )
136 return 1;
137 // get the counter-example
138 assert( RetValue == l_True );
139 return 0;
140 }
141
142 /**Function*************************************************************
143
144 Synopsis [Runs the SAT solver on the problem.]
145
146 Description []
147
148 SideEffects []
149
150 SeeAlso []
151
152 ***********************************************************************/
Fra_ClausRunSat0(Clu_Man_t * p)153 int Fra_ClausRunSat0( Clu_Man_t * p )
154 {
155 Aig_Obj_t * pObj;
156 int Lits[2], RetValue;
157 pObj = Aig_ManCo(p->pAig, 0);
158 Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 0 );
159 RetValue = sat_solver_solve( p->pSatMain, Lits, Lits + 1, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
160 if ( RetValue == l_False )
161 return 1;
162 return 0;
163 }
164
165 /**Function*************************************************************
166
167 Synopsis [Return combinations appearing in the cut.]
168
169 Description [This procedure is taken from "Hacker's Delight" by H.S.Warren.]
170
171 SideEffects []
172
173 SeeAlso []
174
175 ***********************************************************************/
transpose32a(unsigned a[32])176 void transpose32a( unsigned a[32] )
177 {
178 int j, k;
179 unsigned long m, t;
180 for ( j = 16, m = 0x0000FFFF; j; j >>= 1, m ^= m << j )
181 {
182 for ( k = 0; k < 32; k = ((k | j) + 1) & ~j )
183 {
184 t = (a[k] ^ (a[k|j] >> j)) & m;
185 a[k] ^= t;
186 a[k|j] ^= (t << j);
187 }
188 }
189 }
190
191 /**Function*************************************************************
192
193 Synopsis [Return combinations appearing in the cut.]
194
195 Description []
196
197 SideEffects []
198
199 SeeAlso []
200
201 ***********************************************************************/
Fra_ClausProcessClausesCut(Clu_Man_t * p,Fra_Sml_t * pSimMan,Dar_Cut_t * pCut,int * pScores)202 int Fra_ClausProcessClausesCut( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
203 {
204 unsigned Matrix[32];
205 unsigned * pSims[16], uWord;
206 int nSeries, i, k, j;
207 int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
208 // compute parameters
209 assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
210 assert( nWordsForSim % 8 == 0 );
211 // get parameters
212 for ( i = 0; i < (int)pCut->nLeaves; i++ )
213 pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref;
214 // add combinational patterns
215 memset( pScores, 0, sizeof(int) * 16 );
216 nSeries = nWordsForSim / 8;
217 for ( i = 0; i < nSeries; i++ )
218 {
219 memset( Matrix, 0, sizeof(unsigned) * 32 );
220 for ( k = 0; k < 8; k++ )
221 for ( j = 0; j < (int)pCut->nLeaves; j++ )
222 Matrix[31-(k*4+j)] = pSims[j][i*8+k];
223 transpose32a( Matrix );
224 for ( k = 0; k < 32; k++ )
225 for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 )
226 pScores[uWord & 0xF]++;
227 }
228 // collect patterns
229 uWord = 0;
230 for ( i = 0; i < 16; i++ )
231 if ( pScores[i] )
232 uWord |= (1 << i);
233 // Extra_PrintBinary( stdout, &uWord, 16 ); printf( "\n" );
234 return (int)uWord;
235 }
236
237 /**Function*************************************************************
238
239 Synopsis [Return combinations appearing in the cut.]
240
241 Description []
242
243 SideEffects []
244
245 SeeAlso []
246
247 ***********************************************************************/
Fra_ClausProcessClausesCut2(Clu_Man_t * p,Fra_Sml_t * pSimMan,Dar_Cut_t * pCut,int * pScores)248 int Fra_ClausProcessClausesCut2( Clu_Man_t * p, Fra_Sml_t * pSimMan, Dar_Cut_t * pCut, int * pScores )
249 {
250 unsigned * pSims[16], uWord;
251 int iMint, i, k, b;
252 int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
253 // compute parameters
254 assert( pCut->nLeaves > 1 && pCut->nLeaves < 5 );
255 assert( nWordsForSim % 8 == 0 );
256 // get parameters
257 for ( i = 0; i < (int)pCut->nLeaves; i++ )
258 pSims[i] = Fra_ObjSim( pSimMan, pCut->pLeaves[i] ) + p->nSimWordsPref;
259 // add combinational patterns
260 memset( pScores, 0, sizeof(int) * 16 );
261 for ( i = 0; i < nWordsForSim; i++ )
262 for ( k = 0; k < 32; k++ )
263 {
264 iMint = 0;
265 for ( b = 0; b < (int)pCut->nLeaves; b++ )
266 if ( pSims[b][i] & (1 << k) )
267 iMint |= (1 << b);
268 pScores[iMint]++;
269 }
270 // collect patterns
271 uWord = 0;
272 for ( i = 0; i < 16; i++ )
273 if ( pScores[i] )
274 uWord |= (1 << i);
275 // Extra_PrintBinary( stdout, &uWord, 16 ); printf( "\n" );
276 return (int)uWord;
277 }
278
279 /**Function*************************************************************
280
281 Synopsis [Return the number of combinations appearing in the cut.]
282
283 Description []
284
285 SideEffects []
286
287 SeeAlso []
288
289 ***********************************************************************/
Fra_ClausProcessClausesCut3(Clu_Man_t * p,Fra_Sml_t * pSimMan,Aig_Cut_t * pCut,int * pScores)290 void Fra_ClausProcessClausesCut3( Clu_Man_t * p, Fra_Sml_t * pSimMan, Aig_Cut_t * pCut, int * pScores )
291 {
292 unsigned Matrix[32];
293 unsigned * pSims[16], uWord;
294 int iMint, i, j, k, b, nMints, nSeries;
295 int nWordsForSim = pSimMan->nWordsTotal - p->nSimWordsPref;
296
297 // compute parameters
298 assert( pCut->nFanins > 1 && pCut->nFanins < 17 );
299 assert( nWordsForSim % 8 == 0 );
300 // get parameters
301 for ( i = 0; i < (int)pCut->nFanins; i++ )
302 pSims[i] = Fra_ObjSim( pSimMan, pCut->pFanins[i] ) + p->nSimWordsPref;
303 // add combinational patterns
304 nMints = (1 << pCut->nFanins);
305 memset( pScores, 0, sizeof(int) * nMints );
306
307 if ( pCut->nLeafMax == 4 )
308 {
309 // convert the simulation patterns
310 nSeries = nWordsForSim / 8;
311 for ( i = 0; i < nSeries; i++ )
312 {
313 memset( Matrix, 0, sizeof(unsigned) * 32 );
314 for ( k = 0; k < 8; k++ )
315 for ( j = 0; j < (int)pCut->nFanins; j++ )
316 Matrix[31-(k*4+j)] = pSims[j][i*8+k];
317 transpose32a( Matrix );
318 for ( k = 0; k < 32; k++ )
319 for ( j = 0, uWord = Matrix[k]; j < 8; j++, uWord >>= 4 )
320 pScores[uWord & 0xF]++;
321 }
322 }
323 else
324 {
325 // go through the simulation patterns
326 for ( i = 0; i < nWordsForSim; i++ )
327 for ( k = 0; k < 32; k++ )
328 {
329 iMint = 0;
330 for ( b = 0; b < (int)pCut->nFanins; b++ )
331 if ( pSims[b][i] & (1 << k) )
332 iMint |= (1 << b);
333 pScores[iMint]++;
334 }
335 }
336 }
337
338
339 /**Function*************************************************************
340
341 Synopsis [Returns the cut-off cost.]
342
343 Description []
344
345 SideEffects []
346
347 SeeAlso []
348
349 ***********************************************************************/
Fra_ClausSelectClauses(Clu_Man_t * p)350 int Fra_ClausSelectClauses( Clu_Man_t * p )
351 {
352 int * pCostCount, nClauCount, Cost, CostMax, i, c;
353 assert( Vec_IntSize(p->vClauses) > p->nClausesMax );
354 // count how many implications have each cost
355 CostMax = p->nSimWords * 32 + 1;
356 pCostCount = ABC_ALLOC( int, CostMax );
357 memset( pCostCount, 0, sizeof(int) * CostMax );
358 Vec_IntForEachEntry( p->vCosts, Cost, i )
359 {
360 if ( Cost == -1 )
361 continue;
362 assert( Cost < CostMax );
363 pCostCount[ Cost ]++;
364 }
365 assert( pCostCount[0] == 0 );
366 // select the bound on the cost (above this bound, implication will be included)
367 nClauCount = 0;
368 for ( c = CostMax - 1; c > 0; c-- )
369 {
370 assert( pCostCount[c] >= 0 );
371 nClauCount += pCostCount[c];
372 if ( nClauCount >= p->nClausesMax )
373 break;
374 }
375 // collect implications with the given costs
376 nClauCount = 0;
377 Vec_IntForEachEntry( p->vCosts, Cost, i )
378 {
379 if ( Cost >= c && nClauCount < p->nClausesMax )
380 {
381 nClauCount++;
382 continue;
383 }
384 Vec_IntWriteEntry( p->vCosts, i, -1 );
385 }
386 ABC_FREE( pCostCount );
387 p->nClauses = nClauCount;
388 if ( p->fVerbose )
389 printf( "Selected %d clauses. Cost range: [%d < %d < %d]\n", nClauCount, 1, c, CostMax );
390 return c;
391 }
392
393
394 /**Function*************************************************************
395
396 Synopsis [Processes the clauses.]
397
398 Description []
399
400 SideEffects []
401
402 SeeAlso []
403
404 ***********************************************************************/
Fra_ClausRecordClause(Clu_Man_t * p,Dar_Cut_t * pCut,int iMint,int Cost)405 void Fra_ClausRecordClause( Clu_Man_t * p, Dar_Cut_t * pCut, int iMint, int Cost )
406 {
407 int i;
408 for ( i = 0; i < (int)pCut->nLeaves; i++ )
409 Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pLeaves[i]], (iMint&(1<<i)) ) );
410 Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
411 Vec_IntPush( p->vCosts, Cost );
412 }
413
414 /**Function*************************************************************
415
416 Synopsis [Processes the clauses.]
417
418 Description []
419
420 SideEffects []
421
422 SeeAlso []
423
424 ***********************************************************************/
Fra_ClausRecordClause2(Clu_Man_t * p,Aig_Cut_t * pCut,int iMint,int Cost)425 void Fra_ClausRecordClause2( Clu_Man_t * p, Aig_Cut_t * pCut, int iMint, int Cost )
426 {
427 int i;
428 for ( i = 0; i < (int)pCut->nFanins; i++ )
429 Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pCut->pFanins[i]], (iMint&(1<<i)) ) );
430 Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
431 Vec_IntPush( p->vCosts, Cost );
432 }
433
434 /**Function*************************************************************
435
436 Synopsis [Returns 1 if simulation info is composed of all zeros.]
437
438 Description []
439
440 SideEffects []
441
442 SeeAlso []
443
444 ***********************************************************************/
Fra_ClausSmlNodeIsConst(Fra_Sml_t * pSeq,Aig_Obj_t * pObj)445 int Fra_ClausSmlNodeIsConst( Fra_Sml_t * pSeq, Aig_Obj_t * pObj )
446 {
447 unsigned * pSims;
448 int i;
449 pSims = Fra_ObjSim(pSeq, pObj->Id);
450 for ( i = pSeq->nWordsPref; i < pSeq->nWordsTotal; i++ )
451 if ( pSims[i] )
452 return 0;
453 return 1;
454 }
455
456 /**Function*************************************************************
457
458 Synopsis [Returns 1 if implications holds.]
459
460 Description []
461
462 SideEffects []
463
464 SeeAlso []
465
466 ***********************************************************************/
Fra_ClausSmlNodesAreImp(Fra_Sml_t * pSeq,Aig_Obj_t * pObj1,Aig_Obj_t * pObj2)467 int Fra_ClausSmlNodesAreImp( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
468 {
469 unsigned * pSimL, * pSimR;
470 int k;
471 pSimL = Fra_ObjSim(pSeq, pObj1->Id);
472 pSimR = Fra_ObjSim(pSeq, pObj2->Id);
473 for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
474 if ( pSimL[k] & ~pSimR[k] ) // !(Obj1 -> Obj2)
475 return 0;
476 return 1;
477 }
478
479 /**Function*************************************************************
480
481 Synopsis [Returns 1 if implications holds.]
482
483 Description []
484
485 SideEffects []
486
487 SeeAlso []
488
489 ***********************************************************************/
Fra_ClausSmlNodesAreImpC(Fra_Sml_t * pSeq,Aig_Obj_t * pObj1,Aig_Obj_t * pObj2)490 int Fra_ClausSmlNodesAreImpC( Fra_Sml_t * pSeq, Aig_Obj_t * pObj1, Aig_Obj_t * pObj2 )
491 {
492 unsigned * pSimL, * pSimR;
493 int k;
494 pSimL = Fra_ObjSim(pSeq, pObj1->Id);
495 pSimR = Fra_ObjSim(pSeq, pObj2->Id);
496 for ( k = pSeq->nWordsPref; k < pSeq->nWordsTotal; k++ )
497 if ( pSimL[k] & pSimR[k] )
498 return 0;
499 return 1;
500 }
501
502 /**Function*************************************************************
503
504 Synopsis [Processes the clauses.]
505
506 Description []
507
508 SideEffects []
509
510 SeeAlso []
511
512 ***********************************************************************/
Fra_ClausCollectLatchClauses(Clu_Man_t * p,Fra_Sml_t * pSeq)513 int Fra_ClausCollectLatchClauses( Clu_Man_t * p, Fra_Sml_t * pSeq )
514 {
515 Aig_Obj_t * pObj1, * pObj2;
516 unsigned * pSims1, * pSims2;
517 int CostMax, i, k, nCountConst, nCountImps;
518
519 nCountConst = nCountImps = 0;
520 CostMax = p->nSimWords * 32;
521 /*
522 // add the property
523 {
524 Aig_Obj_t * pObj;
525 int Lits[1];
526 pObj = Aig_ManCo( p->pAig, 0 );
527 Lits[0] = toLitCond( p->pCnf->pVarNums[pObj->Id], 1 );
528 Vec_IntPush( p->vLits, Lits[0] );
529 Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
530 Vec_IntPush( p->vCosts, CostMax );
531 nCountConst++;
532 // printf( "Added the target property to the set of clauses to be inductively checked.\n" );
533 }
534 */
535
536 pSeq->nWordsPref = p->nSimWordsPref;
537 Aig_ManForEachLoSeq( p->pAig, pObj1, i )
538 {
539 pSims1 = Fra_ObjSim( pSeq, pObj1->Id );
540 if ( Fra_ClausSmlNodeIsConst( pSeq, pObj1 ) )
541 {
542 Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
543 Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
544 Vec_IntPush( p->vCosts, CostMax );
545 nCountConst++;
546 continue;
547 }
548 Aig_ManForEachLoSeq( p->pAig, pObj2, k )
549 {
550 pSims2 = Fra_ObjSim( pSeq, pObj2->Id );
551 if ( Fra_ClausSmlNodesAreImp( pSeq, pObj1, pObj2 ) )
552 {
553 Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
554 Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 0 ) );
555 Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
556 Vec_IntPush( p->vCosts, CostMax );
557 nCountImps++;
558 continue;
559 }
560 if ( Fra_ClausSmlNodesAreImp( pSeq, pObj2, pObj1 ) )
561 {
562 Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) );
563 Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 0 ) );
564 Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
565 Vec_IntPush( p->vCosts, CostMax );
566 nCountImps++;
567 continue;
568 }
569 if ( Fra_ClausSmlNodesAreImpC( pSeq, pObj1, pObj2 ) )
570 {
571 Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj1->Id], 1 ) );
572 Vec_IntPush( p->vLits, toLitCond( p->pCnf->pVarNums[pObj2->Id], 1 ) );
573 Vec_IntPush( p->vClauses, Vec_IntSize(p->vLits) );
574 Vec_IntPush( p->vCosts, CostMax );
575 nCountImps++;
576 continue;
577 }
578 }
579 if ( nCountConst + nCountImps > p->nClausesMax / 2 )
580 break;
581 }
582 pSeq->nWordsPref = 0;
583 if ( p->fVerbose )
584 printf( "Collected %d register constants and %d one-hotness implications.\n", nCountConst, nCountImps );
585 p->nOneHots = nCountConst + nCountImps;
586 p->nOneHotsProven = 0;
587 return 0;
588 }
589
590 /**Function*************************************************************
591
592 Synopsis [Processes the clauses.]
593
594 Description []
595
596 SideEffects []
597
598 SeeAlso []
599
600 ***********************************************************************/
Fra_ClausProcessClauses(Clu_Man_t * p,int fRefs)601 int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
602 {
603 Aig_MmFixed_t * pMemCuts;
604 // Aig_ManCut_t * pManCut;
605 Fra_Sml_t * pComb, * pSeq;
606 Aig_Obj_t * pObj;
607 Dar_Cut_t * pCut;
608 int Scores[16], uScores, i, k, j, nCuts = 0;
609 abctime clk;
610
611 // simulate the AIG
612 clk = Abc_Clock();
613 // srand( 0xAABBAABB );
614 Aig_ManRandom(1);
615 pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
616 if ( p->fTarget && pSeq->fNonConstOut )
617 {
618 printf( "Property failed after sequential simulation!\n" );
619 Fra_SmlStop( pSeq );
620 return 0;
621 }
622 if ( p->fVerbose )
623 {
624 ABC_PRT( "Sim-seq", Abc_Clock() - clk );
625 }
626
627
628 clk = Abc_Clock();
629 if ( fRefs )
630 {
631 Fra_ClausCollectLatchClauses( p, pSeq );
632 if ( p->fVerbose )
633 {
634 ABC_PRT( "Lat-cla", Abc_Clock() - clk );
635 }
636 }
637
638
639 // generate cuts for all nodes, assign cost, and find best cuts
640 clk = Abc_Clock();
641 pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 );
642 // pManCut = Aig_ComputeCuts( p->pAig, 10, 4, 0, 1 );
643 if ( p->fVerbose )
644 {
645 ABC_PRT( "Cuts ", Abc_Clock() - clk );
646 }
647
648 // collect sequential info for each cut
649 clk = Abc_Clock();
650 Aig_ManForEachNode( p->pAig, pObj, i )
651 Dar_ObjForEachCut( pObj, pCut, k )
652 if ( pCut->nLeaves > 1 )
653 {
654 pCut->uTruth = Fra_ClausProcessClausesCut( p, pSeq, pCut, Scores );
655 // uScores = Fra_ClausProcessClausesCut2( p, pSeq, pCut, Scores );
656 // if ( uScores != pCut->uTruth )
657 // {
658 // int x = 0;
659 // }
660 }
661 if ( p->fVerbose )
662 {
663 ABC_PRT( "Infoseq", Abc_Clock() - clk );
664 }
665 Fra_SmlStop( pSeq );
666
667 // perform combinational simulation
668 clk = Abc_Clock();
669 // srand( 0xAABBAABB );
670 Aig_ManRandom(1);
671 pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 );
672 if ( p->fVerbose )
673 {
674 ABC_PRT( "Sim-cmb", Abc_Clock() - clk );
675 }
676
677 // collect combinational info for each cut
678 clk = Abc_Clock();
679 Aig_ManForEachNode( p->pAig, pObj, i )
680 Dar_ObjForEachCut( pObj, pCut, k )
681 if ( pCut->nLeaves > 1 )
682 {
683 nCuts++;
684 uScores = Fra_ClausProcessClausesCut( p, pComb, pCut, Scores );
685 uScores &= ~pCut->uTruth; pCut->uTruth = 0;
686 if ( uScores == 0 )
687 continue;
688 // write the clauses
689 for ( j = 0; j < (1<<pCut->nLeaves); j++ )
690 if ( uScores & (1 << j) )
691 Fra_ClausRecordClause( p, pCut, j, Scores[j] );
692
693 }
694 Fra_SmlStop( pComb );
695 Aig_MmFixedStop( pMemCuts, 0 );
696 // Aig_ManCutStop( pManCut );
697 if ( p->fVerbose )
698 {
699 ABC_PRT( "Infocmb", Abc_Clock() - clk );
700 }
701
702 if ( p->fVerbose )
703 printf( "Node = %5d. Non-triv cuts = %7d. Clauses = %6d. Clause per cut = %6.2f.\n",
704 Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
705
706 if ( Vec_IntSize(p->vClauses) > p->nClausesMax )
707 Fra_ClausSelectClauses( p );
708 else
709 p->nClauses = Vec_IntSize( p->vClauses );
710 return 1;
711 }
712
713 /**Function*************************************************************
714
715 Synopsis [Processes the clauses.]
716
717 Description []
718
719 SideEffects []
720
721 SeeAlso []
722
723 ***********************************************************************/
Fra_ClausProcessClauses2(Clu_Man_t * p,int fRefs)724 int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
725 {
726 // Aig_MmFixed_t * pMemCuts;
727 Aig_ManCut_t * pManCut;
728 Fra_Sml_t * pComb, * pSeq;
729 Aig_Obj_t * pObj;
730 Aig_Cut_t * pCut;
731 int i, k, j, nCuts = 0;
732 abctime clk;
733 int ScoresSeq[1<<12], ScoresComb[1<<12];
734 assert( p->nLutSize < 13 );
735
736 // simulate the AIG
737 clk = Abc_Clock();
738 // srand( 0xAABBAABB );
739 Aig_ManRandom(1);
740 pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames, 1 );
741 if ( p->fTarget && pSeq->fNonConstOut )
742 {
743 printf( "Property failed after sequential simulation!\n" );
744 Fra_SmlStop( pSeq );
745 return 0;
746 }
747 if ( p->fVerbose )
748 {
749 //ABC_PRT( "Sim-seq", Abc_Clock() - clk );
750 }
751
752 // perform combinational simulation
753 clk = Abc_Clock();
754 // srand( 0xAABBAABB );
755 Aig_ManRandom(1);
756 pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref, 0 );
757 if ( p->fVerbose )
758 {
759 //ABC_PRT( "Sim-cmb", Abc_Clock() - clk );
760 }
761
762
763 clk = Abc_Clock();
764 if ( fRefs )
765 {
766 Fra_ClausCollectLatchClauses( p, pSeq );
767 if ( p->fVerbose )
768 {
769 //ABC_PRT( "Lat-cla", Abc_Clock() - clk );
770 }
771 }
772
773
774 // generate cuts for all nodes, assign cost, and find best cuts
775 clk = Abc_Clock();
776 // pMemCuts = Dar_ManComputeCuts( p->pAig, 10, 0, 1 );
777 pManCut = Aig_ComputeCuts( p->pAig, p->nCutsMax, p->nLutSize, 0, p->fVerbose );
778 if ( p->fVerbose )
779 {
780 //ABC_PRT( "Cuts ", Abc_Clock() - clk );
781 }
782
783 // collect combinational info for each cut
784 clk = Abc_Clock();
785 Aig_ManForEachNode( p->pAig, pObj, i )
786 {
787 if ( pObj->Level > (unsigned)p->nLevels )
788 continue;
789 Aig_ObjForEachCut( pManCut, pObj, pCut, k )
790 if ( pCut->nFanins > 1 )
791 {
792 nCuts++;
793 Fra_ClausProcessClausesCut3( p, pSeq, pCut, ScoresSeq );
794 Fra_ClausProcessClausesCut3( p, pComb, pCut, ScoresComb );
795 // write the clauses
796 for ( j = 0; j < (1<<pCut->nFanins); j++ )
797 if ( ScoresComb[j] != 0 && ScoresSeq[j] == 0 )
798 Fra_ClausRecordClause2( p, pCut, j, ScoresComb[j] );
799
800 }
801 }
802 Fra_SmlStop( pSeq );
803 Fra_SmlStop( pComb );
804 p->nCuts = nCuts;
805 // Aig_MmFixedStop( pMemCuts, 0 );
806 Aig_ManCutStop( pManCut );
807 p->pAig->pManCuts = NULL;
808
809 if ( p->fVerbose )
810 {
811 printf( "Node = %5d. Cuts = %7d. Clauses = %6d. Clause/cut = %6.2f.\n",
812 Aig_ManNodeNum(p->pAig), nCuts, Vec_IntSize(p->vClauses), 1.0*Vec_IntSize(p->vClauses)/nCuts );
813 ABC_PRT( "Processing sim-info to find candidate clauses (unoptimized)", Abc_Clock() - clk );
814 }
815
816 // filter out clauses that are contained in the already proven clauses
817 assert( p->nClauses == 0 );
818 p->nClauses = Vec_IntSize( p->vClauses );
819 if ( Vec_IntSize( p->vClausesProven ) > 0 )
820 {
821 int RetValue, k, Beg;
822 int End = -1; // Suppress "might be used uninitialized"
823 int * pStart;
824 // reset the solver
825 if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
826 p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
827 if ( p->pSatMain == NULL )
828 {
829 printf( "Error: Main solver is unsat.\n" );
830 return -1;
831 }
832
833 // add the proven clauses
834 Beg = 0;
835 pStart = Vec_IntArray(p->vLitsProven);
836 Vec_IntForEachEntry( p->vClausesProven, End, i )
837 {
838 assert( End - Beg <= p->nLutSize );
839 // add the clause to all timeframes
840 RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
841 if ( RetValue == 0 )
842 {
843 printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
844 return -1;
845 }
846 Beg = End;
847 }
848 assert( End == Vec_IntSize(p->vLitsProven) );
849
850 // check the clauses
851 Beg = 0;
852 pStart = Vec_IntArray(p->vLits);
853 Vec_IntForEachEntry( p->vClauses, End, i )
854 {
855 assert( Vec_IntEntry( p->vCosts, i ) >= 0 );
856 assert( End - Beg <= p->nLutSize );
857 // check the clause
858 for ( k = Beg; k < End; k++ )
859 pStart[k] = lit_neg( pStart[k] );
860 RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
861 for ( k = Beg; k < End; k++ )
862 pStart[k] = lit_neg( pStart[k] );
863 // the clause holds
864 if ( RetValue == l_False )
865 {
866 Vec_IntWriteEntry( p->vCosts, i, -1 );
867 p->nClauses--;
868 }
869 Beg = End;
870 }
871 assert( End == Vec_IntSize(p->vLits) );
872 if ( p->fVerbose )
873 printf( "Already proved clauses filtered out %d candidate clauses (out of %d).\n",
874 Vec_IntSize(p->vClauses) - p->nClauses, Vec_IntSize(p->vClauses) );
875 }
876
877 p->fFiltering = 0;
878 if ( p->nClauses > p->nClausesMax )
879 {
880 Fra_ClausSelectClauses( p );
881 p->fFiltering = 1;
882 }
883 return 1;
884 }
885
886 /**Function*************************************************************
887
888 Synopsis [Converts AIG into the SAT solver.]
889
890 Description []
891
892 SideEffects []
893
894 SeeAlso []
895
896 ***********************************************************************/
Fra_ClausBmcClauses(Clu_Man_t * p)897 int Fra_ClausBmcClauses( Clu_Man_t * p )
898 {
899 int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f;
900 /*
901 for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
902 printf( "%d ", p->vLits->pArray[i] );
903 printf( "\n" );
904 */
905 // add the clauses
906 Counter = 0;
907 // skip through the prefix variables
908 if ( p->nPref )
909 {
910 nLitsTot = p->nPref * 2 * p->pCnf->nVars;
911 for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
912 p->vLits->pArray[i] += nLitsTot;
913 }
914 // go through the timeframes
915 nLitsTot = 2 * p->pCnf->nVars;
916 pStart = Vec_IntArray(p->vLits);
917 for ( f = 0; f < p->nFrames; f++ )
918 {
919 Beg = 0;
920 Vec_IntForEachEntry( p->vClauses, End, i )
921 {
922 if ( Vec_IntEntry( p->vCosts, i ) == -1 )
923 {
924 Beg = End;
925 continue;
926 }
927 assert( Vec_IntEntry( p->vCosts, i ) > 0 );
928 assert( End - Beg <= p->nLutSize );
929
930 for ( k = Beg; k < End; k++ )
931 pStart[k] = lit_neg( pStart[k] );
932 RetValue = sat_solver_solve( p->pSatBmc, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
933 for ( k = Beg; k < End; k++ )
934 pStart[k] = lit_neg( pStart[k] );
935
936 if ( RetValue != l_False )
937 {
938 Beg = End;
939 Vec_IntWriteEntry( p->vCosts, i, -1 );
940 Counter++;
941 continue;
942 }
943 /*
944 // add the clause
945 RetValue = sat_solver_addclause( p->pSatBmc, pStart + Beg, pStart + End );
946 // assert( RetValue == 1 );
947 if ( RetValue == 0 )
948 {
949 printf( "Error: Solver is UNSAT after adding BMC clauses.\n" );
950 return -1;
951 }
952 */
953 Beg = End;
954
955 // simplify the solver
956 if ( p->pSatBmc->qtail != p->pSatBmc->qhead )
957 {
958 RetValue = sat_solver_simplify(p->pSatBmc);
959 assert( RetValue != 0 );
960 assert( p->pSatBmc->qtail == p->pSatBmc->qhead );
961 }
962 }
963 // increment literals
964 for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
965 p->vLits->pArray[i] += nLitsTot;
966 }
967
968 // return clauses back to normal
969 nLitsTot = (p->nPref + p->nFrames) * nLitsTot;
970 for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
971 p->vLits->pArray[i] -= nLitsTot;
972 /*
973 for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
974 printf( "%d ", p->vLits->pArray[i] );
975 printf( "\n" );
976 */
977 return Counter;
978 }
979
980 /**Function*************************************************************
981
982 Synopsis [Cleans simulation info.]
983
984 Description []
985
986 SideEffects []
987
988 SeeAlso []
989
990 ***********************************************************************/
Fra_ClausSimInfoClean(Clu_Man_t * p)991 void Fra_ClausSimInfoClean( Clu_Man_t * p )
992 {
993 assert( p->pCnf->nVars <= Vec_PtrSize(p->vCexes) );
994 Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
995 p->nCexes = 0;
996 }
997
998 /**Function*************************************************************
999
1000 Synopsis [Reallocs simulation info.]
1001
1002 Description []
1003
1004 SideEffects []
1005
1006 SeeAlso []
1007
1008 ***********************************************************************/
Fra_ClausSimInfoRealloc(Clu_Man_t * p)1009 void Fra_ClausSimInfoRealloc( Clu_Man_t * p )
1010 {
1011 assert( p->nCexes == p->nCexesAlloc );
1012 Vec_PtrReallocSimInfo( p->vCexes );
1013 Vec_PtrCleanSimInfo( p->vCexes, p->nCexesAlloc/32, 2 * p->nCexesAlloc/32 );
1014 p->nCexesAlloc *= 2;
1015 }
1016
1017 /**Function*************************************************************
1018
1019 Synopsis [Records simulation info.]
1020
1021 Description []
1022
1023 SideEffects []
1024
1025 SeeAlso []
1026
1027 ***********************************************************************/
Fra_ClausSimInfoRecord(Clu_Man_t * p,int * pModel)1028 void Fra_ClausSimInfoRecord( Clu_Man_t * p, int * pModel )
1029 {
1030 int i;
1031 if ( p->nCexes == p->nCexesAlloc )
1032 Fra_ClausSimInfoRealloc( p );
1033 assert( p->nCexes < p->nCexesAlloc );
1034 for ( i = 0; i < p->pCnf->nVars; i++ )
1035 {
1036 if ( pModel[i] == l_True )
1037 {
1038 assert( Abc_InfoHasBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes ) == 0 );
1039 Abc_InfoSetBit( (unsigned *)Vec_PtrEntry(p->vCexes, i), p->nCexes );
1040 }
1041 }
1042 p->nCexes++;
1043 }
1044
1045 /**Function*************************************************************
1046
1047 Synopsis [Uses the simulation info.]
1048
1049 Description [Returns 1 if the simulation info disproved the clause.]
1050
1051 SideEffects []
1052
1053 SeeAlso []
1054
1055 ***********************************************************************/
Fra_ClausSimInfoCheck(Clu_Man_t * p,int * pLits,int nLits)1056 int Fra_ClausSimInfoCheck( Clu_Man_t * p, int * pLits, int nLits )
1057 {
1058 unsigned * pSims[16], uWord;
1059 int nWords, iVar, i, w;
1060 for ( i = 0; i < nLits; i++ )
1061 {
1062 iVar = lit_var(pLits[i]) - p->nFrames * p->pCnf->nVars;
1063 assert( iVar > 0 && iVar < p->pCnf->nVars );
1064 pSims[i] = (unsigned *)Vec_PtrEntry( p->vCexes, iVar );
1065 }
1066 nWords = p->nCexes / 32;
1067 for ( w = 0; w < nWords; w++ )
1068 {
1069 uWord = ~(unsigned)0;
1070 for ( i = 0; i < nLits; i++ )
1071 uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
1072 if ( uWord )
1073 return 1;
1074 }
1075 if ( p->nCexes % 32 )
1076 {
1077 uWord = ~(unsigned)0;
1078 for ( i = 0; i < nLits; i++ )
1079 uWord &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
1080 if ( uWord & Abc_InfoMask( p->nCexes % 32 ) )
1081 return 1;
1082 }
1083 return 0;
1084 }
1085
1086
1087 /**Function*************************************************************
1088
1089 Synopsis [Converts AIG into the SAT solver.]
1090
1091 Description []
1092
1093 SideEffects []
1094
1095 SeeAlso []
1096
1097 ***********************************************************************/
Fra_ClausInductiveClauses(Clu_Man_t * p)1098 int Fra_ClausInductiveClauses( Clu_Man_t * p )
1099 {
1100 // Aig_Obj_t * pObjLi, * pObjLo;
1101 int * pStart, nLitsTot, RetValue, Beg, End, Counter, i, k, f, fFlag;//, Lits[2];
1102 p->fFail = 0;
1103
1104 // reset the solver
1105 if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
1106 p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
1107 if ( p->pSatMain == NULL )
1108 {
1109 printf( "Error: Main solver is unsat.\n" );
1110 return -1;
1111 }
1112 Fra_ClausSimInfoClean( p );
1113
1114 /*
1115 // check if the property holds
1116 if ( Fra_ClausRunSat0( p ) )
1117 printf( "Property holds without strengthening.\n" );
1118 else
1119 printf( "Property does not hold without strengthening.\n" );
1120 */
1121 /*
1122 // add constant registers
1123 Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
1124 if ( Aig_ObjFanin0(pObjLi) == Aig_ManConst1(p->pAig) )
1125 {
1126 for ( k = 0; k < p->nFrames; k++ )
1127 {
1128 Lits[0] = k * 2 * p->pCnf->nVars + toLitCond( p->pCnf->pVarNums[pObjLo->Id], Aig_ObjFaninC0(pObjLi) );
1129 RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
1130 if ( RetValue == 0 )
1131 {
1132 printf( "Error: Solver is UNSAT after adding constant-register clauses.\n" );
1133 return -1;
1134 }
1135 }
1136 }
1137 */
1138
1139
1140 // add the proven clauses
1141 nLitsTot = 2 * p->pCnf->nVars;
1142 pStart = Vec_IntArray(p->vLitsProven);
1143 for ( f = 0; f < p->nFrames; f++ )
1144 {
1145 Beg = 0;
1146 Vec_IntForEachEntry( p->vClausesProven, End, i )
1147 {
1148 assert( End - Beg <= p->nLutSize );
1149 // add the clause to all timeframes
1150 RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
1151 if ( RetValue == 0 )
1152 {
1153 printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
1154 return -1;
1155 }
1156 Beg = End;
1157 }
1158 // increment literals
1159 for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
1160 p->vLitsProven->pArray[i] += nLitsTot;
1161 }
1162 // return clauses back to normal
1163 nLitsTot = (p->nFrames) * nLitsTot;
1164 for ( i = 0; i < Vec_IntSize(p->vLitsProven); i++ )
1165 p->vLitsProven->pArray[i] -= nLitsTot;
1166
1167 /*
1168 // add the proven clauses
1169 nLitsTot = 2 * p->pCnf->nVars;
1170 pStart = Vec_IntArray(p->vLitsProven);
1171 Beg = 0;
1172 Vec_IntForEachEntry( p->vClausesProven, End, i )
1173 {
1174 assert( End - Beg <= p->nLutSize );
1175 // add the clause to all timeframes
1176 RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
1177 if ( RetValue == 0 )
1178 {
1179 printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
1180 return -1;
1181 }
1182 Beg = End;
1183 }
1184 */
1185
1186 // add the clauses
1187 nLitsTot = 2 * p->pCnf->nVars;
1188 pStart = Vec_IntArray(p->vLits);
1189 for ( f = 0; f < p->nFrames; f++ )
1190 {
1191 Beg = 0;
1192 Vec_IntForEachEntry( p->vClauses, End, i )
1193 {
1194 if ( Vec_IntEntry( p->vCosts, i ) == -1 )
1195 {
1196 Beg = End;
1197 continue;
1198 }
1199 assert( Vec_IntEntry( p->vCosts, i ) > 0 );
1200 assert( End - Beg <= p->nLutSize );
1201 // add the clause to all timeframes
1202 RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
1203 if ( RetValue == 0 )
1204 {
1205 printf( "Error: Solver is UNSAT after adding assumption clauses.\n" );
1206 return -1;
1207 }
1208 Beg = End;
1209 }
1210 // increment literals
1211 for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
1212 p->vLits->pArray[i] += nLitsTot;
1213 }
1214
1215 // simplify the solver
1216 if ( p->pSatMain->qtail != p->pSatMain->qhead )
1217 {
1218 RetValue = sat_solver_simplify(p->pSatMain);
1219 assert( RetValue != 0 );
1220 assert( p->pSatMain->qtail == p->pSatMain->qhead );
1221 }
1222
1223 // check if the property holds
1224 if ( p->fTarget )
1225 {
1226 if ( Fra_ClausRunSat0( p ) )
1227 {
1228 if ( p->fVerbose )
1229 printf( " Property holds. " );
1230 }
1231 else
1232 {
1233 if ( p->fVerbose )
1234 printf( " Property fails. " );
1235 // return -2;
1236 p->fFail = 1;
1237 }
1238 }
1239
1240 /*
1241 // add the property for the first K frames
1242 for ( i = 0; i < p->nFrames; i++ )
1243 {
1244 Aig_Obj_t * pObj;
1245 int Lits[2];
1246 // set the output literals
1247 pObj = Aig_ManCo(p->pAig, 0);
1248 Lits[0] = i * nLitsTot + toLitCond( p->pCnf->pVarNums[pObj->Id], 1 );
1249 // add the clause
1250 RetValue = sat_solver_addclause( p->pSatMain, Lits, Lits + 1 );
1251 // assert( RetValue == 1 );
1252 if ( RetValue == 0 )
1253 {
1254 printf( "Error: Solver is UNSAT after adding property for the first K frames.\n" );
1255 return -1;
1256 }
1257 }
1258 */
1259
1260 // simplify the solver
1261 if ( p->pSatMain->qtail != p->pSatMain->qhead )
1262 {
1263 RetValue = sat_solver_simplify(p->pSatMain);
1264 assert( RetValue != 0 );
1265 assert( p->pSatMain->qtail == p->pSatMain->qhead );
1266 }
1267
1268
1269 // check the clause in the last timeframe
1270 Beg = 0;
1271 Counter = 0;
1272 Vec_IntForEachEntry( p->vClauses, End, i )
1273 {
1274 if ( Vec_IntEntry( p->vCosts, i ) == -1 )
1275 {
1276 Beg = End;
1277 continue;
1278 }
1279 assert( Vec_IntEntry( p->vCosts, i ) > 0 );
1280 assert( End - Beg <= p->nLutSize );
1281
1282 if ( Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg) )
1283 {
1284 fFlag = 1;
1285 // printf( "s-" );
1286
1287 Beg = End;
1288 Vec_IntWriteEntry( p->vCosts, i, -1 );
1289 Counter++;
1290 continue;
1291 }
1292 else
1293 {
1294 fFlag = 0;
1295 // printf( "s?" );
1296 }
1297
1298 for ( k = Beg; k < End; k++ )
1299 pStart[k] = lit_neg( pStart[k] );
1300 RetValue = sat_solver_solve( p->pSatMain, pStart + Beg, pStart + End, (ABC_INT64_T)p->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1301 for ( k = Beg; k < End; k++ )
1302 pStart[k] = lit_neg( pStart[k] );
1303
1304 // the problem is not solved
1305 if ( RetValue != l_False )
1306 {
1307 // printf( "S- " );
1308 // Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model.ptr + p->nFrames * p->pCnf->nVars );
1309 Fra_ClausSimInfoRecord( p, (int*)p->pSatMain->model + p->nFrames * p->pCnf->nVars );
1310 // RetValue = Fra_ClausSimInfoCheck(p, pStart + Beg, End - Beg);
1311 // assert( RetValue );
1312
1313 Beg = End;
1314 Vec_IntWriteEntry( p->vCosts, i, -1 );
1315 Counter++;
1316 continue;
1317 }
1318 // printf( "S+ " );
1319 // assert( !fFlag );
1320
1321 /*
1322 // add the clause
1323 RetValue = sat_solver_addclause( p->pSatMain, pStart + Beg, pStart + End );
1324 // assert( RetValue == 1 );
1325 if ( RetValue == 0 )
1326 {
1327 printf( "Error: Solver is UNSAT after adding proved clauses.\n" );
1328 return -1;
1329 }
1330 */
1331 Beg = End;
1332
1333 // simplify the solver
1334 if ( p->pSatMain->qtail != p->pSatMain->qhead )
1335 {
1336 RetValue = sat_solver_simplify(p->pSatMain);
1337 assert( RetValue != 0 );
1338 assert( p->pSatMain->qtail == p->pSatMain->qhead );
1339 }
1340 }
1341
1342 // return clauses back to normal
1343 nLitsTot = p->nFrames * nLitsTot;
1344 for ( i = 0; i < Vec_IntSize(p->vLits); i++ )
1345 p->vLits->pArray[i] -= nLitsTot;
1346
1347 // if ( fFail )
1348 // return -2;
1349 return Counter;
1350 }
1351
1352
1353
1354 /**Function*************************************************************
1355
1356 Synopsis [Converts AIG into the SAT solver.]
1357
1358 Description []
1359
1360 SideEffects []
1361
1362 SeeAlso []
1363
1364 ***********************************************************************/
Fra_ClausAlloc(Aig_Man_t * pAig,int nFrames,int nPref,int nClausesMax,int nLutSize,int nLevels,int nCutsMax,int nBatches,int fStepUp,int fTarget,int fVerbose,int fVeryVerbose)1365 Clu_Man_t * Fra_ClausAlloc( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fTarget, int fVerbose, int fVeryVerbose )
1366 {
1367 Clu_Man_t * p;
1368 p = ABC_ALLOC( Clu_Man_t, 1 );
1369 memset( p, 0, sizeof(Clu_Man_t) );
1370 p->pAig = pAig;
1371 p->nFrames = nFrames;
1372 p->nPref = nPref;
1373 p->nClausesMax = nClausesMax;
1374 p->nLutSize = nLutSize;
1375 p->nLevels = nLevels;
1376 p->nCutsMax = nCutsMax;
1377 p->nBatches = nBatches;
1378 p->fStepUp = fStepUp;
1379 p->fTarget = fTarget;
1380 p->fVerbose = fVerbose;
1381 p->fVeryVerbose = fVeryVerbose;
1382 p->nSimWords = 512;//1024;//64;
1383 p->nSimFrames = 32;//8;//32;
1384 p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
1385
1386 p->vLits = Vec_IntAlloc( 1<<14 );
1387 p->vClauses = Vec_IntAlloc( 1<<12 );
1388 p->vCosts = Vec_IntAlloc( 1<<12 );
1389
1390 p->vLitsProven = Vec_IntAlloc( 1<<14 );
1391 p->vClausesProven= Vec_IntAlloc( 1<<12 );
1392
1393 p->nCexesAlloc = 1024;
1394 p->vCexes = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p->pAig)+1, p->nCexesAlloc/32 );
1395 Vec_PtrCleanSimInfo( p->vCexes, 0, p->nCexesAlloc/32 );
1396 return p;
1397 }
1398
1399 /**Function*************************************************************
1400
1401 Synopsis [Converts AIG into the SAT solver.]
1402
1403 Description []
1404
1405 SideEffects []
1406
1407 SeeAlso []
1408
1409 ***********************************************************************/
Fra_ClausFree(Clu_Man_t * p)1410 void Fra_ClausFree( Clu_Man_t * p )
1411 {
1412 if ( p->vCexes ) Vec_PtrFree( p->vCexes );
1413 if ( p->vLits ) Vec_IntFree( p->vLits );
1414 if ( p->vClauses ) Vec_IntFree( p->vClauses );
1415 if ( p->vLitsProven ) Vec_IntFree( p->vLitsProven );
1416 if ( p->vClausesProven ) Vec_IntFree( p->vClausesProven );
1417 if ( p->vCosts ) Vec_IntFree( p->vCosts );
1418 if ( p->pCnf ) Cnf_DataFree( p->pCnf );
1419 if ( p->pSatMain ) sat_solver_delete( p->pSatMain );
1420 if ( p->pSatBmc ) sat_solver_delete( p->pSatBmc );
1421 ABC_FREE( p );
1422 }
1423
1424
1425 /**Function*************************************************************
1426
1427 Synopsis [Converts AIG into the SAT solver.]
1428
1429 Description []
1430
1431 SideEffects []
1432
1433 SeeAlso []
1434
1435 ***********************************************************************/
Fra_ClausAddToStorage(Clu_Man_t * p)1436 void Fra_ClausAddToStorage( Clu_Man_t * p )
1437 {
1438 int * pStart;
1439 int Beg, End, Counter, i, k;
1440 Beg = 0;
1441 Counter = 0;
1442 pStart = Vec_IntArray( p->vLits );
1443 Vec_IntForEachEntry( p->vClauses, End, i )
1444 {
1445 if ( Vec_IntEntry( p->vCosts, i ) == -1 )
1446 {
1447 Beg = End;
1448 continue;
1449 }
1450 assert( Vec_IntEntry( p->vCosts, i ) > 0 );
1451 assert( End - Beg <= p->nLutSize );
1452 for ( k = Beg; k < End; k++ )
1453 Vec_IntPush( p->vLitsProven, pStart[k] );
1454 Vec_IntPush( p->vClausesProven, Vec_IntSize(p->vLitsProven) );
1455 Beg = End;
1456 Counter++;
1457
1458 if ( i < p->nOneHots )
1459 p->nOneHotsProven++;
1460 }
1461 if ( p->fVerbose )
1462 printf( "Added to storage %d proved clauses (including %d one-hot clauses)\n", Counter, p->nOneHotsProven );
1463
1464 Vec_IntClear( p->vClauses );
1465 Vec_IntClear( p->vLits );
1466 Vec_IntClear( p->vCosts );
1467 p->nClauses = 0;
1468
1469 p->fNothingNew = (int)(Counter == 0);
1470 }
1471
1472 /**Function*************************************************************
1473
1474 Synopsis [Converts AIG into the SAT solver.]
1475
1476 Description []
1477
1478 SideEffects []
1479
1480 SeeAlso []
1481
1482 ***********************************************************************/
Fra_ClausPrintIndClauses(Clu_Man_t * p)1483 void Fra_ClausPrintIndClauses( Clu_Man_t * p )
1484 {
1485 int Counters[9] = {0};
1486 int * pStart;
1487 int Beg, End, i;
1488 Beg = 0;
1489 pStart = Vec_IntArray( p->vLitsProven );
1490 Vec_IntForEachEntry( p->vClausesProven, End, i )
1491 {
1492 if ( End - Beg >= 8 )
1493 Counters[8]++;
1494 else
1495 Counters[End - Beg]++;
1496 //printf( "%d ", End-Beg );
1497 Beg = End;
1498 }
1499 printf( "SUMMARY: Total proved clauses = %d. ", Vec_IntSize(p->vClausesProven) );
1500 printf( "Clause per lit: " );
1501 for ( i = 0; i < 8; i++ )
1502 if ( Counters[i] )
1503 printf( "%d=%d ", i, Counters[i] );
1504 if ( Counters[8] )
1505 printf( ">7=%d ", Counters[8] );
1506 printf( "\n" );
1507 }
1508
1509 /**Function*************************************************************
1510
1511 Synopsis [Writes the clauses into an AIGER file.]
1512
1513 Description []
1514
1515 SideEffects []
1516
1517 SeeAlso []
1518
1519 ***********************************************************************/
Fra_ClausGetLiteral(Clu_Man_t * p,int * pVar2Id,int Lit)1520 Aig_Obj_t * Fra_ClausGetLiteral( Clu_Man_t * p, int * pVar2Id, int Lit )
1521 {
1522 Aig_Obj_t * pLiteral;
1523 int NodeId = pVar2Id[ lit_var(Lit) ];
1524 assert( NodeId >= 0 );
1525 pLiteral = (Aig_Obj_t *)Aig_ManObj( p->pAig, NodeId )->pData;
1526 return Aig_NotCond( pLiteral, lit_sign(Lit) );
1527 }
1528
1529 /**Function*************************************************************
1530
1531 Synopsis [Writes the clauses into an AIGER file.]
1532
1533 Description []
1534
1535 SideEffects []
1536
1537 SeeAlso []
1538
1539 ***********************************************************************/
Fra_ClausWriteIndClauses(Clu_Man_t * p)1540 void Fra_ClausWriteIndClauses( Clu_Man_t * p )
1541 {
1542 extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
1543 Aig_Man_t * pNew;
1544 Aig_Obj_t * pClause, * pLiteral;
1545 char * pName;
1546 int * pStart, * pVar2Id;
1547 int Beg, End, i, k;
1548 // create mapping from SAT vars to node IDs
1549 pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
1550 memset( pVar2Id, 0xFF, sizeof(int) * p->pCnf->nVars );
1551 for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
1552 if ( p->pCnf->pVarNums[i] >= 0 )
1553 {
1554 assert( p->pCnf->pVarNums[i] < p->pCnf->nVars );
1555 pVar2Id[ p->pCnf->pVarNums[i] ] = i;
1556 }
1557 // start the manager
1558 pNew = Aig_ManDupWithoutPos( p->pAig );
1559 // add the clauses
1560 Beg = 0;
1561 pStart = Vec_IntArray( p->vLitsProven );
1562 Vec_IntForEachEntry( p->vClausesProven, End, i )
1563 {
1564 pClause = Fra_ClausGetLiteral( p, pVar2Id, pStart[Beg] );
1565 for ( k = Beg + 1; k < End; k++ )
1566 {
1567 pLiteral = Fra_ClausGetLiteral( p, pVar2Id, pStart[k] );
1568 pClause = Aig_Or( pNew, pClause, pLiteral );
1569 }
1570 Aig_ObjCreateCo( pNew, pClause );
1571 Beg = End;
1572 }
1573 ABC_FREE( pVar2Id );
1574 Aig_ManCleanup( pNew );
1575 pName = Ioa_FileNameGenericAppend( p->pAig->pName, "_care.aig" );
1576 printf( "Care one-hotness clauses will be written into file \"%s\".\n", pName );
1577 Ioa_WriteAiger( pNew, pName, 0, 1 );
1578 Aig_ManStop( pNew );
1579 }
1580
1581 /**Function*************************************************************
1582
1583 Synopsis [Checks if the clause holds using the given simulation info.]
1584
1585 Description []
1586
1587 SideEffects []
1588
1589 SeeAlso []
1590
1591 ***********************************************************************/
Fra_ClausEstimateCoverageOne(Fra_Sml_t * pSim,int * pLits,int nLits,int * pVar2Id,unsigned * pResult)1592 void Fra_ClausEstimateCoverageOne( Fra_Sml_t * pSim, int * pLits, int nLits, int * pVar2Id, unsigned * pResult )
1593 {
1594 unsigned * pSims[16];
1595 int iVar, i, w;
1596 for ( i = 0; i < nLits; i++ )
1597 {
1598 iVar = lit_var(pLits[i]);
1599 pSims[i] = Fra_ObjSim( pSim, pVar2Id[iVar] );
1600 }
1601 for ( w = 0; w < pSim->nWordsTotal; w++ )
1602 {
1603 pResult[w] = ~(unsigned)0;
1604 for ( i = 0; i < nLits; i++ )
1605 pResult[w] &= (lit_sign(pLits[i])? pSims[i][w] : ~pSims[i][w]);
1606 }
1607 }
1608
1609 /**Function*************************************************************
1610
1611 Synopsis [Estimates the coverage of state space by clauses.]
1612
1613 Description []
1614
1615 SideEffects []
1616
1617 SeeAlso []
1618
1619 ***********************************************************************/
Fra_ClausEstimateCoverage(Clu_Man_t * p)1620 void Fra_ClausEstimateCoverage( Clu_Man_t * p )
1621 {
1622 int nCombSimWords = (1<<11);
1623 Fra_Sml_t * pComb;
1624 unsigned * pResultTot, * pResultOne;
1625 int nCovered, Beg, End, i, w;
1626 int * pStart, * pVar2Id;
1627 abctime clk = Abc_Clock();
1628 // simulate the circuit with nCombSimWords * 32 = 64K patterns
1629 // srand( 0xAABBAABB );
1630 Aig_ManRandom(1);
1631 pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords, 0 );
1632 // create mapping from SAT vars to node IDs
1633 pVar2Id = ABC_ALLOC( int, p->pCnf->nVars );
1634 memset( pVar2Id, 0, sizeof(int) * p->pCnf->nVars );
1635 for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
1636 if ( p->pCnf->pVarNums[i] >= 0 )
1637 {
1638 assert( p->pCnf->pVarNums[i] < p->pCnf->nVars );
1639 pVar2Id[ p->pCnf->pVarNums[i] ] = i;
1640 }
1641 // get storage for one assignment and all assignments
1642 assert( Aig_ManCoNum(p->pAig) > 2 );
1643 pResultOne = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 0)->Id );
1644 pResultTot = Fra_ObjSim( pComb, Aig_ManCo(p->pAig, 1)->Id );
1645 // start the OR of don't-cares
1646 for ( w = 0; w < nCombSimWords; w++ )
1647 pResultTot[w] = 0;
1648 // check clauses
1649 Beg = 0;
1650 pStart = Vec_IntArray( p->vLitsProven );
1651 Vec_IntForEachEntry( p->vClausesProven, End, i )
1652 {
1653 Fra_ClausEstimateCoverageOne( pComb, pStart + Beg, End-Beg, pVar2Id, pResultOne );
1654 Beg = End;
1655 for ( w = 0; w < nCombSimWords; w++ )
1656 pResultTot[w] |= pResultOne[w];
1657 }
1658 // count the total number of patterns contained in the don't-care
1659 nCovered = 0;
1660 for ( w = 0; w < nCombSimWords; w++ )
1661 nCovered += Aig_WordCountOnes( pResultTot[w] );
1662 Fra_SmlStop( pComb );
1663 ABC_FREE( pVar2Id );
1664 // print the result
1665 printf( "Care states ratio = %f. ", 1.0 * (nCombSimWords * 32 - nCovered) / (nCombSimWords * 32) );
1666 printf( "(%d out of %d patterns) ", nCombSimWords * 32 - nCovered, nCombSimWords * 32 );
1667 ABC_PRT( "Time", Abc_Clock() - clk );
1668 }
1669
1670
1671 /**Function*************************************************************
1672
1673 Synopsis [Converts AIG into the SAT solver.]
1674
1675 Description []
1676
1677 SideEffects []
1678
1679 SeeAlso []
1680
1681 ***********************************************************************/
Fra_Claus(Aig_Man_t * pAig,int nFrames,int nPref,int nClausesMax,int nLutSize,int nLevels,int nCutsMax,int nBatches,int fStepUp,int fBmc,int fRefs,int fTarget,int fVerbose,int fVeryVerbose)1682 int Fra_Claus( Aig_Man_t * pAig, int nFrames, int nPref, int nClausesMax, int nLutSize, int nLevels, int nCutsMax, int nBatches, int fStepUp, int fBmc, int fRefs, int fTarget, int fVerbose, int fVeryVerbose )
1683 {
1684 Clu_Man_t * p;
1685 abctime clk, clkTotal = Abc_Clock(), clkInd;
1686 int b, Iter, Counter, nPrefOld;
1687 int nClausesBeg = 0;
1688
1689 // create the manager
1690 p = Fra_ClausAlloc( pAig, nFrames, nPref, nClausesMax, nLutSize, nLevels, nCutsMax, nBatches, fStepUp, fTarget, fVerbose, fVeryVerbose );
1691 if ( p->fVerbose )
1692 {
1693 printf( "PARAMETERS: Frames = %d. Pref = %d. Clauses max = %d. Cut size = %d.\n", nFrames, nPref, nClausesMax, nLutSize );
1694 printf( "Level max = %d. Cuts max = %d. Batches = %d. Increment cut size = %s.\n", nLevels, nCutsMax, nBatches, fStepUp? "yes":"no" );
1695 //ABC_PRT( "Sim-seq", Abc_Clock() - clk );
1696 }
1697
1698 assert( !p->fTarget || Aig_ManCoNum(pAig) - Aig_ManRegNum(pAig) == 1 );
1699
1700 clk = Abc_Clock();
1701 // derive CNF
1702 // if ( p->fTarget )
1703 // p->pAig->nRegs++;
1704 p->pCnf = Cnf_DeriveSimple( p->pAig, Aig_ManCoNum(p->pAig) );
1705 // if ( p->fTarget )
1706 // p->pAig->nRegs--;
1707 if ( fVerbose )
1708 {
1709 //ABC_PRT( "CNF ", Abc_Clock() - clk );
1710 }
1711
1712 // check BMC
1713 clk = Abc_Clock();
1714 p->pSatBmc = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nPref + p->nFrames, 1 );
1715 if ( p->pSatBmc == NULL )
1716 {
1717 printf( "Error: BMC solver is unsat.\n" );
1718 Fra_ClausFree( p );
1719 return 1;
1720 }
1721 if ( p->fTarget && !Fra_ClausRunBmc( p ) )
1722 {
1723 printf( "Problem fails the base case after %d frame expansion.\n", p->nPref + p->nFrames );
1724 Fra_ClausFree( p );
1725 return 1;
1726 }
1727 if ( fVerbose )
1728 {
1729 //ABC_PRT( "SAT-bmc", Abc_Clock() - clk );
1730 }
1731
1732 // start the SAT solver
1733 clk = Abc_Clock();
1734 p->pSatMain = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, p->nFrames+1, 0 );
1735 if ( p->pSatMain == NULL )
1736 {
1737 printf( "Error: Main solver is unsat.\n" );
1738 Fra_ClausFree( p );
1739 return 1;
1740 }
1741
1742
1743 for ( b = 0; b < p->nBatches; b++ )
1744 {
1745 // if ( fVerbose )
1746 printf( "*** BATCH %d: ", b+1 );
1747 if ( b && p->nLutSize < 12 && (!p->fFiltering || p->fNothingNew || p->fStepUp) )
1748 p->nLutSize++;
1749 printf( "Using %d-cuts.\n", p->nLutSize );
1750
1751 // try solving without additional clauses
1752 if ( p->fTarget && Fra_ClausRunSat( p ) )
1753 {
1754 printf( "Problem is inductive without strengthening.\n" );
1755 Fra_ClausFree( p );
1756 return 1;
1757 }
1758 if ( fVerbose )
1759 {
1760 // ABC_PRT( "SAT-ind", Abc_Clock() - clk );
1761 }
1762
1763 // collect the candidate inductive clauses using 4-cuts
1764 clk = Abc_Clock();
1765 nPrefOld = p->nPref; p->nPref = 0; p->nSimWordsPref = 0;
1766 // Fra_ClausProcessClauses( p, fRefs );
1767 Fra_ClausProcessClauses2( p, fRefs );
1768 p->nPref = nPrefOld;
1769 p->nSimWordsPref = p->nPref*p->nSimWords/p->nSimFrames;
1770 nClausesBeg = p->nClauses;
1771
1772 //ABC_PRT( "Clauses", Abc_Clock() - clk );
1773
1774
1775 // check clauses using BMC
1776 if ( fBmc )
1777 {
1778 clk = Abc_Clock();
1779 Counter = Fra_ClausBmcClauses( p );
1780 p->nClauses -= Counter;
1781 if ( fVerbose )
1782 {
1783 printf( "BMC disproved %d clauses. ", Counter );
1784 ABC_PRT( "Time", Abc_Clock() - clk );
1785 }
1786 }
1787
1788
1789 // prove clauses inductively
1790 clkInd = clk = Abc_Clock();
1791 Counter = 1;
1792 for ( Iter = 0; Counter > 0; Iter++ )
1793 {
1794 if ( fVerbose )
1795 printf( "Iter %3d : Begin = %5d. ", Iter, p->nClauses );
1796 Counter = Fra_ClausInductiveClauses( p );
1797 if ( Counter > 0 )
1798 p->nClauses -= Counter;
1799 if ( fVerbose )
1800 {
1801 printf( "End = %5d. Exs = %5d. ", p->nClauses, p->nCexes );
1802 // printf( "\n" );
1803 ABC_PRT( "Time", Abc_Clock() - clk );
1804 }
1805 clk = Abc_Clock();
1806 }
1807 // add proved clauses to storage
1808 Fra_ClausAddToStorage( p );
1809 // report the results
1810 if ( p->fTarget )
1811 {
1812 if ( Counter == -1 )
1813 printf( "Fra_Claus(): Internal error. " );
1814 else if ( p->fFail )
1815 printf( "Property FAILS during refinement. " );
1816 else
1817 printf( "Property HOLDS inductively after strengthening. " );
1818 ABC_PRT( "Time ", Abc_Clock() - clkTotal );
1819 if ( !p->fFail )
1820 break;
1821 }
1822 else
1823 {
1824 printf( "Finished proving inductive clauses. " );
1825 ABC_PRT( "Time ", Abc_Clock() - clkTotal );
1826 }
1827 }
1828
1829 // verify the computed interpolant
1830 Fra_InvariantVerify( pAig, nFrames, p->vClausesProven, p->vLitsProven );
1831 // printf( "THIS COMMAND IS KNOWN TO HAVE A BUG!\n" );
1832
1833 // if ( !p->fTarget && p->fVerbose )
1834 if ( p->fVerbose )
1835 {
1836 Fra_ClausPrintIndClauses( p );
1837 Fra_ClausEstimateCoverage( p );
1838 }
1839
1840 if ( !p->fTarget )
1841 {
1842 Fra_ClausWriteIndClauses( p );
1843 }
1844 /*
1845 // print the statistic into a file
1846 {
1847 FILE * pTable;
1848 assert( p->nBatches == 1 );
1849 pTable = fopen( "stats.txt", "a+" );
1850 fprintf( pTable, "%s ", pAig->pName );
1851 fprintf( pTable, "%d ", Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig) );
1852 fprintf( pTable, "%d ", Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig) );
1853 fprintf( pTable, "%d ", Aig_ManRegNum(pAig) );
1854 fprintf( pTable, "%d ", Aig_ManNodeNum(pAig) );
1855 fprintf( pTable, "%d ", p->nCuts );
1856 fprintf( pTable, "%d ", nClausesBeg );
1857 fprintf( pTable, "%d ", p->nClauses );
1858 fprintf( pTable, "%d ", Iter );
1859 fprintf( pTable, "%.2f ", (float)(clkInd-clkTotal)/(float)(CLOCKS_PER_SEC) );
1860 fprintf( pTable, "%.2f ", (float)(Abc_Clock()-clkInd)/(float)(CLOCKS_PER_SEC) );
1861 fprintf( pTable, "%.2f ", (float)(Abc_Clock()-clkTotal)/(float)(CLOCKS_PER_SEC) );
1862 fprintf( pTable, "\n" );
1863 fclose( pTable );
1864 }
1865 */
1866 // clean the manager
1867 Fra_ClausFree( p );
1868 return 1;
1869 }
1870
1871 ////////////////////////////////////////////////////////////////////////
1872 /// END OF FILE ///
1873 ////////////////////////////////////////////////////////////////////////
1874
1875
1876 ABC_NAMESPACE_IMPL_END
1877
1878