1 /**CFile****************************************************************
2 
3   FileName    [fraInd.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [New FRAIG package.]
8 
9   Synopsis    [Inductive prover.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - June 30, 2007.]
16 
17   Revision    [$Id: fraInd.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 "opt/dar/dar.h"
24 #include "aig/saig/saig.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 ///                        DECLARATIONS                              ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 ////////////////////////////////////////////////////////////////////////
34 ///                     FUNCTION DEFINITIONS                         ///
35 ////////////////////////////////////////////////////////////////////////
36 
37 /**Function*************************************************************
38 
39   Synopsis    [Performs AIG rewriting on the constraint manager.]
40 
41   Description []
42 
43   SideEffects []
44 
45   SeeAlso     []
46 
47 ***********************************************************************/
Fra_FraigInductionRewrite(Fra_Man_t * p)48 void Fra_FraigInductionRewrite( Fra_Man_t * p )
49 {
50     Aig_Man_t * pTemp;
51     Aig_Obj_t * pObj, * pObjPo;
52     int nTruePis, k, i;
53     abctime clk = Abc_Clock();
54     // perform AIG rewriting on the speculated frames
55 //    pTemp = Dar_ManRwsat( pTemp, 1, 0 );
56     pTemp = Dar_ManRewriteDefault( p->pManFraig );
57 //    printf( "Before = %6d.  After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) );
58 //Aig_ManDumpBlif( p->pManFraig, "1.blif", NULL, NULL );
59 //Aig_ManDumpBlif( pTemp, "2.blif", NULL, NULL );
60 //    Fra_FramesWriteCone( pTemp );
61 //    Aig_ManStop( pTemp );
62     // transfer PI/register pointers
63     assert( p->pManFraig->nRegs == pTemp->nRegs );
64     assert( p->pManFraig->nAsserts == pTemp->nAsserts );
65     nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
66     memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
67     Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) );
68     Aig_ManForEachPiSeq( p->pManAig, pObj, i )
69         Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManCi(pTemp,nTruePis*p->pPars->nFramesK+i) );
70     k = 0;
71     assert( Aig_ManRegNum(p->pManAig) == Aig_ManCoNum(pTemp) - pTemp->nAsserts );
72     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
73     {
74         pObjPo = Aig_ManCo(pTemp, pTemp->nAsserts + k++);
75         Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) );
76     }
77     // exchange
78     Aig_ManStop( p->pManFraig );
79     p->pManFraig = pTemp;
80 p->timeRwr += Abc_Clock() - clk;
81 }
82 
83 /**Function*************************************************************
84 
85   Synopsis    [Performs speculative reduction for one node.]
86 
87   Description []
88 
89   SideEffects []
90 
91   SeeAlso     []
92 
93 ***********************************************************************/
Fra_FramesConstrainNode(Aig_Man_t * pManFraig,Aig_Obj_t * pObj,int iFrame)94 static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, int iFrame )
95 {
96     Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
97     // skip nodes without representative
98     if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
99         return;
100     assert( pObjRepr->Id < pObj->Id );
101     // get the new node
102     pObjNew = Fra_ObjFraig( pObj, iFrame );
103     // get the new node of the representative
104     pObjReprNew = Fra_ObjFraig( pObjRepr, iFrame );
105     // if this is the same node, no need to add constraints
106     if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
107         return;
108     // these are different nodes - perform speculative reduction
109     pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
110     // set the new node
111     Fra_ObjSetFraig( pObj, iFrame, pObjNew2 );
112     // add the constraint
113     pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew );
114     pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
115     assert( Aig_ObjPhaseReal(pMiter) == 1 );
116     Aig_ObjCreateCo( pManFraig, pMiter );
117 }
118 
119 /**Function*************************************************************
120 
121   Synopsis    [Prepares the inductive case with speculative reduction.]
122 
123   Description []
124 
125   SideEffects []
126 
127   SeeAlso     []
128 
129 ***********************************************************************/
Fra_FramesWithClasses(Fra_Man_t * p)130 Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
131 {
132     Aig_Man_t * pManFraig;
133     Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
134     int i, k, f;
135     assert( p->pManFraig == NULL );
136     assert( Aig_ManRegNum(p->pManAig) > 0 );
137     assert( Aig_ManRegNum(p->pManAig) < Aig_ManCiNum(p->pManAig) );
138 
139     // start the fraig package
140     pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll );
141     pManFraig->pName = Abc_UtilStrsav( p->pManAig->pName );
142     pManFraig->pSpec = Abc_UtilStrsav( p->pManAig->pSpec );
143     pManFraig->nRegs = p->pManAig->nRegs;
144     // create PI nodes for the frames
145     for ( f = 0; f < p->nFramesAll; f++ )
146         Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) );
147     for ( f = 0; f < p->nFramesAll; f++ )
148         Aig_ManForEachPiSeq( p->pManAig, pObj, i )
149             Fra_ObjSetFraig( pObj, f, Aig_ObjCreateCi(pManFraig) );
150     // create latches for the first frame
151     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
152         Fra_ObjSetFraig( pObj, 0, Aig_ObjCreateCi(pManFraig) );
153 
154     // add timeframes
155 //    pManFraig->fAddStrash = 1;
156     for ( f = 0; f < p->nFramesAll - 1; f++ )
157     {
158         // set the constraints on the latch outputs
159         Aig_ManForEachLoSeq( p->pManAig, pObj, i )
160             Fra_FramesConstrainNode( pManFraig, pObj, f );
161         // add internal nodes of this frame
162         Aig_ManForEachNode( p->pManAig, pObj, i )
163         {
164             pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) );
165             Fra_ObjSetFraig( pObj, f, pObjNew );
166             Fra_FramesConstrainNode( pManFraig, pObj, f );
167         }
168         // transfer latch input to the latch outputs
169         Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k )
170             Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) );
171     }
172 //    pManFraig->fAddStrash = 0;
173     // mark the asserts
174     pManFraig->nAsserts = Aig_ManCoNum(pManFraig);
175     // add the POs for the latch outputs of the last frame
176     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
177         Aig_ObjCreateCo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
178 
179     // remove dangling nodes
180     Aig_ManCleanup( pManFraig );
181     // make sure the satisfying assignment is node assigned
182     assert( pManFraig->pData == NULL );
183     return pManFraig;
184 }
185 
186 /**Function*************************************************************
187 
188   Synopsis    [Prepares the inductive case with speculative reduction.]
189 
190   Description []
191 
192   SideEffects []
193 
194   SeeAlso     []
195 
196 ***********************************************************************/
Fra_FramesAddMore(Aig_Man_t * p,int nFrames)197 void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
198 {
199     Aig_Obj_t * pObj, ** pLatches;
200     int i, k, f, nNodesOld;
201     // set copy pointer of each object to point to itself
202     Aig_ManForEachObj( p, pObj, i )
203         pObj->pData = pObj;
204     // iterate and add objects
205     nNodesOld = Aig_ManObjNumMax(p);
206     pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
207     for ( f = 0; f < nFrames; f++ )
208     {
209         // clean latch inputs and outputs
210         Aig_ManForEachLiSeq( p, pObj, i )
211             pObj->pData = NULL;
212         Aig_ManForEachLoSeq( p, pObj, i )
213             pObj->pData = NULL;
214         // save the latch input values
215         k = 0;
216         Aig_ManForEachLiSeq( p, pObj, i )
217         {
218             if ( Aig_ObjFanin0(pObj)->pData )
219                 pLatches[k++] = Aig_ObjChild0Copy(pObj);
220             else
221                 pLatches[k++] = NULL;
222         }
223         // insert them as the latch output values
224         k = 0;
225         Aig_ManForEachLoSeq( p, pObj, i )
226             pObj->pData = pLatches[k++];
227         // create the next time frame of nodes
228         Aig_ManForEachNode( p, pObj, i )
229         {
230             if ( i > nNodesOld )
231                 break;
232             if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData )
233                 pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
234             else
235                 pObj->pData = NULL;
236         }
237     }
238     ABC_FREE( pLatches );
239 }
240 
241 
242 /**Function*************************************************************
243 
244   Synopsis    [Performs partitioned sequential SAT sweepingG.]
245 
246   Description []
247 
248   SideEffects []
249 
250   SeeAlso     []
251 
252 ***********************************************************************/
Fra_FraigInductionPart(Aig_Man_t * pAig,Fra_Ssw_t * pPars)253 Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
254 {
255     int fPrintParts = 0;
256     char Buffer[100];
257     Aig_Man_t * pTemp, * pNew;
258     Vec_Ptr_t * vResult;
259     Vec_Int_t * vPart;
260     int * pMapBack;
261     int i, nCountPis, nCountRegs;
262     int nClasses, nPartSize, fVerbose;
263     abctime clk = Abc_Clock();
264 
265     // save parameters
266     nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
267     fVerbose  = pPars->fVerbose;  pPars->fVerbose = 0;
268     // generate partitions
269     if ( pAig->vClockDoms )
270     {
271         // divide large clock domains into separate partitions
272         vResult = Vec_PtrAlloc( 100 );
273         Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
274         {
275             if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
276                 Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
277             else
278                 Vec_PtrPush( vResult, Vec_IntDup(vPart) );
279         }
280     }
281     else
282         vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
283 //    vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 );
284 //    vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
285     if ( fPrintParts )
286     {
287         // print partitions
288         printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
289         Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
290         {
291             sprintf( Buffer, "part%03d.aig", i );
292             pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
293             Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
294             printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
295                 i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
296             Aig_ManStop( pTemp );
297         }
298     }
299 
300     // perform SSW with partitions
301     Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
302     Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
303     {
304         pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
305         // create the projection of 1-hot registers
306         if ( pAig->vOnehots )
307             pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
308         // run SSW
309         pNew = Fra_FraigInduction( pTemp, pPars );
310         nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
311         if ( fVerbose )
312             printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
313                 i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
314         Aig_ManStop( pNew );
315         Aig_ManStop( pTemp );
316         ABC_FREE( pMapBack );
317     }
318     // remap the AIG
319     pNew = Aig_ManDupRepr( pAig, 0 );
320     Aig_ManSeqCleanup( pNew );
321 //    Aig_ManPrintStats( pAig );
322 //    Aig_ManPrintStats( pNew );
323     Vec_VecFree( (Vec_Vec_t *)vResult );
324     pPars->nPartSize = nPartSize;
325     pPars->fVerbose = fVerbose;
326     if ( fVerbose )
327     {
328         ABC_PRT( "Total time", Abc_Clock() - clk );
329     }
330     return pNew;
331 }
332 
333 /**Function*************************************************************
334 
335   Synopsis    [Performs sequential SAT sweeping.]
336 
337   Description []
338 
339   SideEffects []
340 
341   SeeAlso     []
342 
343 ***********************************************************************/
Fra_FraigInduction(Aig_Man_t * pManAig,Fra_Ssw_t * pParams)344 Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
345 {
346     int fUseSimpleCnf = 0;
347     int fUseOldSimulation = 0;
348     // other paramaters affecting performance
349     // - presence of FRAIGing in Abc_NtkDarSeqSweep()
350     // - using distance-1 patterns in Fra_SmlAssignDist1()
351     // - the number of simulation patterns
352     // - the number of BMC frames
353 
354     Fra_Man_t * p;
355     Fra_Par_t Pars, * pPars = &Pars;
356     Aig_Obj_t * pObj;
357     Cnf_Dat_t * pCnf;
358     Aig_Man_t * pManAigNew = NULL;
359     int nNodesBeg, nRegsBeg;
360     int nIter = -1; // Suppress "might be used uninitialized"
361     int i;
362     abctime clk = Abc_Clock(), clk2;
363     abctime TimeToStop = pParams->TimeLimit ? pParams->TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
364 
365     if ( Aig_ManNodeNum(pManAig) == 0 )
366     {
367         pParams->nIters = 0;
368         // Ntl_ManFinalize() needs the following to satisfy an assertion
369         Aig_ManReprStart(pManAig,Aig_ManObjNumMax(pManAig));
370         return Aig_ManDupOrdered(pManAig);
371     }
372     assert( Aig_ManRegNum(pManAig) > 0 );
373     assert( pParams->nFramesK > 0 );
374 //Aig_ManShow( pManAig, 0, NULL );
375 
376     if ( pParams->fWriteImps && pParams->nPartSize > 0 )
377     {
378         pParams->nPartSize = 0;
379         printf( "Partitioning was disabled to allow implication writing.\n" );
380     }
381     // perform partitioning
382     if ( (pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig))
383          || (pManAig->vClockDoms && Vec_VecSize(pManAig->vClockDoms) > 0)  )
384         return Fra_FraigInductionPart( pManAig, pParams );
385 
386     nNodesBeg = Aig_ManNodeNum(pManAig);
387     nRegsBeg  = Aig_ManRegNum(pManAig);
388 
389     // enhance the AIG by adding timeframes
390 //    Fra_FramesAddMore( pManAig, 3 );
391 
392     // get parameters
393     Fra_ParamsDefaultSeq( pPars );
394     pPars->nFramesP   = pParams->nFramesP;
395     pPars->nFramesK   = pParams->nFramesK;
396     pPars->nMaxImps   = pParams->nMaxImps;
397     pPars->nMaxLevs   = pParams->nMaxLevs;
398     pPars->fVerbose   = pParams->fVerbose;
399     pPars->fRewrite   = pParams->fRewrite;
400     pPars->fLatchCorr = pParams->fLatchCorr;
401     pPars->fUseImps   = pParams->fUseImps;
402     pPars->fWriteImps = pParams->fWriteImps;
403     pPars->fUse1Hot   = pParams->fUse1Hot;
404 
405     assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) );
406     assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) );
407 
408     // start the fraig manager for this run
409     p = Fra_ManStart( pManAig, pPars );
410     p->pPars->nBTLimitNode = 0;
411     // derive and refine e-classes using K initialized frames
412     if ( fUseOldSimulation )
413     {
414         if ( pPars->nFramesP > 0 )
415         {
416             pPars->nFramesP = 0;
417             printf( "Fra_FraigInduction(): Prefix cannot be used.\n" );
418         }
419         p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
420         Fra_SmlSimulate( p, 1 );
421     }
422     else
423     {
424         // bug:  r iscas/blif/s5378.blif    ; st; ssw -v
425         // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
426         // refine the classes with more simulation rounds
427 if ( pPars->fVerbose )
428 printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
429         p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1, 1  ); //pPars->nFramesK + 1, 1 );
430 if ( pPars->fVerbose )
431 {
432 ABC_PRT( "Time", Abc_Clock() - clk );
433 }
434         Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
435 //        Fra_ClassesPostprocess( p->pCla );
436         // compute one-hotness conditions
437         if ( p->pPars->fUse1Hot )
438             p->vOneHots = Fra_OneHotCompute( p, p->pSml );
439         // allocate new simulation manager for simulating counter-examples
440         Fra_SmlStop( p->pSml );
441         p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
442     }
443 
444     // select the most expressive implications
445     if ( pPars->fUseImps )
446         p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
447 
448     if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
449     {
450         if ( !pParams->fSilent )
451             printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
452         goto finish;
453     }
454 
455     // perform BMC (for the min number of frames)
456     Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement
457 //Fra_ClassesPrint( p->pCla, 1 );
458 //    if ( p->vCex == NULL )
459 //        p->vCex = Vec_IntAlloc( 1000 );
460 
461     p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
462     p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig);
463     p->nRegsBeg  = nRegsBeg; // Aig_ManRegNum(pManAig);
464 
465     // dump AIG of the timeframes
466 //    pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
467 //    Aig_ManDumpBlif( pManAigNew, "frame_aig.blif", NULL, NULL );
468 //    Fra_ManPartitionTest2( pManAigNew );
469 //    Aig_ManStop( pManAigNew );
470 
471     // iterate the inductive case
472     p->pCla->fRefinement = 1;
473     for ( nIter = 0; p->pCla->fRefinement; nIter++ )
474     {
475         int nLitsOld = Fra_ClassesCountLits(p->pCla);
476         int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
477         int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
478         abctime clk3 = Abc_Clock();
479 
480         if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
481         {
482             if ( !pParams->fSilent )
483                 printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
484             goto finish;
485         }
486 
487         // mark the classes as non-refined
488         p->pCla->fRefinement = 0;
489         // derive non-init K-timeframes while implementing e-classes
490 clk2 = Abc_Clock();
491         p->pManFraig = Fra_FramesWithClasses( p );
492 p->timeTrav += Abc_Clock() - clk2;
493 //Aig_ManDumpBlif( p->pManFraig, "testaig.blif", NULL, NULL );
494 
495         // perform AIG rewriting
496         if ( p->pPars->fRewrite )
497             Fra_FraigInductionRewrite( p );
498 
499         // convert the manager to SAT solver (the last nLatches outputs are inputs)
500         if ( fUseSimpleCnf || pPars->fUseImps )
501             pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
502         else
503             pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
504 //        Cnf_DataTranformPolarity( pCnf, 0 );
505 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
506 
507         p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
508         p->nSatVars = pCnf->nVars;
509         assert( p->pSat != NULL );
510         if ( p->pSat == NULL )
511             printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" );
512         if ( pPars->fUseImps )
513         {
514             Fra_ImpAddToSolver( p, p->pCla->vImps, pCnf->pVarNums );
515             if ( p->pSat == NULL )
516                 printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
517         }
518 
519         // set the pointers to the manager
520         Aig_ManForEachObj( p->pManFraig, pObj, i )
521             pObj->pData = p;
522 
523         // prepare solver for fraiging the last timeframe
524         Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) );
525 
526         // transfer PI/LO variable numbers
527         Aig_ManForEachObj( p->pManFraig, pObj, i )
528         {
529             if ( pCnf->pVarNums[pObj->Id] == -1 )
530                 continue;
531             Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
532             Fra_ObjSetFaninVec( pObj, (Vec_Ptr_t *)1 );
533         }
534         Cnf_DataFree( pCnf );
535 
536         // add one-hotness clauses
537         if ( p->pPars->fUse1Hot )
538             Fra_OneHotAssume( p, p->vOneHots );
539 //        if ( p->pManAig->vOnehots )
540 //            Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots );
541 
542         // report the intermediate results
543         if ( pPars->fVerbose )
544         {
545             printf( "%3d : C = %6d. Cl = %6d.  L = %6d. LR = %6d.  ",
546                 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
547                 Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
548             if ( p->pCla->vImps )
549                 printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) );
550             if ( p->pPars->fUse1Hot )
551                 printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) );
552             printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
553 //            printf( "\n" );
554         }
555 
556         // perform sweeping
557         p->nSatCallsRecent = 0;
558         p->nSatCallsSkipped = 0;
559 clk2 = Abc_Clock();
560         if ( p->pPars->fUse1Hot )
561             Fra_OneHotCheck( p, p->vOneHots );
562         Fra_FraigSweep( p );
563         if ( pPars->fVerbose )
564         {
565             ABC_PRT( "T", Abc_Clock() - clk3 );
566         }
567 
568 //        Sat_SolverPrintStats( stdout, p->pSat );
569         // remove FRAIG and SAT solver
570         Aig_ManStop( p->pManFraig );   p->pManFraig = NULL;
571 //        printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size );
572         sat_solver_delete( p->pSat );  p->pSat = NULL;
573         memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
574 //        printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
575         assert( p->vTimeouts == NULL );
576         if ( p->vTimeouts )
577            printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
578         // check if refinement has happened
579 //        p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
580         if ( p->pCla->fRefinement &&
581             nLitsOld == Fra_ClassesCountLits(p->pCla) &&
582             nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) &&
583             nHotsOld == (p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0) )
584         {
585             printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" );
586             break;
587         }
588     }
589 /*
590     // verify implications using simulation
591     if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
592     {
593         int Temp;
594         abctime clk = Abc_Clock();
595         if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
596             printf( "Implications failing the simulation test = %d (out of %d).  ", Temp, Vec_IntSize(p->pCla->vImps) );
597         else
598             printf( "All %d implications have passed the simulation test.  ", Vec_IntSize(p->pCla->vImps) );
599         ABC_PRT( "Time", Abc_Clock() - clk );
600     }
601 */
602 
603     // move the classes into representatives and reduce AIG
604 clk2 = Abc_Clock();
605     if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
606     {
607         extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
608         Aig_Man_t * pNew;
609         char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
610         printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
611         pManAigNew = Aig_ManDupOrdered( pManAig );
612         pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
613         Ioa_WriteAiger( pNew, pFileName, 0, 1 );
614         Aig_ManStop( pNew );
615     }
616     else
617     {
618     //    Fra_ClassesPrint( p->pCla, 1 );
619         Fra_ClassesSelectRepr( p->pCla );
620         Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
621         pManAigNew = Aig_ManDupRepr( pManAig, 0 );
622     }
623     // add implications to the manager
624 //    if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
625 //        Fra_ImpRecordInManager( p, pManAigNew );
626     // cleanup the new manager
627     Aig_ManSeqCleanup( pManAigNew );
628     // remove pointers to the dead nodes
629 //    Aig_ManForEachObj( pManAig, pObj, i )
630 //        if ( pObj->pData && Aig_ObjIsNone(pObj->pData) )
631 //            pObj->pData = NULL;
632 //    Aig_ManCountMergeRegs( pManAigNew );
633 p->timeTrav += Abc_Clock() - clk2;
634 p->timeTotal = Abc_Clock() - clk;
635     // get the final stats
636     p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
637     p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
638     p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
639     // free the manager
640 finish:
641     Fra_ManStop( p );
642     // check the output
643 //    if ( Aig_ManCoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
644 //        if ( Aig_ObjChild0( Aig_ManCo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
645 //            printf( "Proved output constant 0.\n" );
646     pParams->nIters = nIter;
647     return pManAigNew;
648 }
649 
650 /**Function*************************************************************
651 
652   Synopsis    [Outputs a set of pairs of equivalent nodes.]
653 
654   Description []
655 
656   SideEffects []
657 
658   SeeAlso     []
659 
660 ***********************************************************************/
Fra_FraigInductionTest(char * pFileName,Fra_Ssw_t * pParams)661 int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams )
662 {
663     FILE * pFile;
664     char * pFilePairs;
665     Aig_Man_t * pMan, * pNew;
666     Aig_Obj_t * pObj, * pRepr;
667     int * pNum2Id;
668     int i, Counter = 0;
669     pMan = Saig_ManReadBlif( pFileName );
670     if ( pMan == NULL )
671         return 0;
672     // perform seq SAT sweeping
673     pNew = Fra_FraigInduction( pMan, pParams );
674     if ( pNew == NULL )
675     {
676         Aig_ManStop( pMan );
677         return 0;
678     }
679     if ( pParams->fVerbose )
680     {
681         printf( "Original AIG: " );
682         Aig_ManPrintStats( pMan );
683         printf( "Reduced  AIG: " );
684         Aig_ManPrintStats( pNew );
685     }
686     Aig_ManStop( pNew );
687     pNum2Id = (int *)pMan->pData;
688     // write the output file
689     pFilePairs = Aig_FileNameGenericAppend( pFileName, ".pairs" );
690     pFile = fopen( pFilePairs, "w" );
691     Aig_ManForEachObj( pMan, pObj, i )
692         if ( (pRepr = pMan->pReprs[pObj->Id]) )
693         {
694             fprintf( pFile, "%d %d %c\n", pNum2Id[pObj->Id], pNum2Id[pRepr->Id], (Aig_ObjPhase(pObj) ^ Aig_ObjPhase(pRepr))? '-' : '+' );
695             Counter++;
696         }
697     fclose( pFile );
698     if ( pParams->fVerbose )
699     {
700         printf( "Result: %d pairs of seq equiv nodes are written into file \"%s\".\n", Counter, pFilePairs );
701     }
702     Aig_ManStop( pMan );
703     return 1;
704 }
705 
706 ////////////////////////////////////////////////////////////////////////
707 ///                       END OF FILE                                ///
708 ////////////////////////////////////////////////////////////////////////
709 
710 
711 ABC_NAMESPACE_IMPL_END
712 
713