1 /**CFile****************************************************************
2
3 FileName [giaSatLE.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Scalable AIG package.]
8
9 Synopsis [Mapping with edges.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: giaSatLE.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "gia.h"
22 #include "misc/extra/extra.h"
23 #include "misc/tim/tim.h"
24 #include "sat/bsat/satStore.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
Sle_CutSize(int * pCut)33 static inline int Sle_CutSize( int * pCut ) { return pCut[0] & 0xF; } // 4 bits
Sle_CutSign(int * pCut)34 static inline int Sle_CutSign( int * pCut ) { return ((unsigned)pCut[0]) >> 4; } // 28 bits
Sle_CutSetSizeSign(int s,int S)35 static inline int Sle_CutSetSizeSign( int s, int S ) { return (S << 4) | s; }
Sle_CutLeaves(int * pCut)36 static inline int * Sle_CutLeaves( int * pCut ) { return pCut + 1; }
37
Sle_CutIsUsed(int * pCut)38 static inline int Sle_CutIsUsed( int * pCut ) { return pCut[1] != 0; }
Sle_CutSetUnused(int * pCut)39 static inline void Sle_CutSetUnused( int * pCut ) { pCut[1] = 0; }
40
Sle_ListCutNum(int * pList)41 static inline int Sle_ListCutNum( int * pList ) { return pList[0]; }
42
43 #define Sle_ForEachCut( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += Sle_CutSize(pCut) + 1 ) // cuts with unit-cut
44 #define Sle_ForEachCut1( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i <= pList[0]; i++, pCut += Sle_CutSize(pCut) + 1 ) // only non-unit cuts
45
46 ////////////////////////////////////////////////////////////////////////
47 /// FUNCTION DEFINITIONS ///
48 ////////////////////////////////////////////////////////////////////////
49
50 /**Function*************************************************************
51
52 Synopsis [Cut computation.]
53
54 Description []
55
56 SideEffects []
57
58 SeeAlso []
59
60 ***********************************************************************/
Sle_CutMergeOrder(int * pCut0,int * pCut1,int * pCut,int nLutSize)61 static inline int Sle_CutMergeOrder( int * pCut0, int * pCut1, int * pCut, int nLutSize )
62 {
63 int nSize0 = Sle_CutSize(pCut0);
64 int nSize1 = Sle_CutSize(pCut1);
65 int i, * pC0 = Sle_CutLeaves(pCut0);
66 int k, * pC1 = Sle_CutLeaves(pCut1);
67 int c, * pC = Sle_CutLeaves(pCut);
68 // the case of the largest cut sizes
69 if ( nSize0 == nLutSize && nSize1 == nLutSize )
70 {
71 for ( i = 0; i < nSize0; i++ )
72 {
73 if ( pC0[i] != pC1[i] ) return 0;
74 pC[i] = pC0[i];
75 }
76 pCut[0] = Sle_CutSetSizeSign( nLutSize, Sle_CutSign(pCut0) | Sle_CutSign(pCut1) );
77 return 1;
78 }
79 // compare two cuts with different numbers
80 i = k = c = 0;
81 if ( nSize0 == 0 ) goto FlushCut1;
82 if ( nSize1 == 0 ) goto FlushCut0;
83 while ( 1 )
84 {
85 if ( c == nLutSize ) return 0;
86 if ( pC0[i] < pC1[k] )
87 {
88 pC[c++] = pC0[i++];
89 if ( i >= nSize0 ) goto FlushCut1;
90 }
91 else if ( pC0[i] > pC1[k] )
92 {
93 pC[c++] = pC1[k++];
94 if ( k >= nSize1 ) goto FlushCut0;
95 }
96 else
97 {
98 pC[c++] = pC0[i++]; k++;
99 if ( i >= nSize0 ) goto FlushCut1;
100 if ( k >= nSize1 ) goto FlushCut0;
101 }
102 }
103
104 FlushCut0:
105 if ( c + nSize0 > nLutSize + i ) return 0;
106 while ( i < nSize0 )
107 pC[c++] = pC0[i++];
108 pCut[0] = Sle_CutSetSizeSign( c, Sle_CutSign(pCut0) | Sle_CutSign(pCut1) );
109 return 1;
110
111 FlushCut1:
112 if ( c + nSize1 > nLutSize + k ) return 0;
113 while ( k < nSize1 )
114 pC[c++] = pC1[k++];
115 pCut[0] = Sle_CutSetSizeSign( c, Sle_CutSign(pCut0) | Sle_CutSign(pCut1) );
116 return 1;
117 }
Sle_SetCutIsContainedOrder(int * pBase,int * pCut)118 static inline int Sle_SetCutIsContainedOrder( int * pBase, int * pCut ) // check if pCut is contained in pBase
119 {
120 int i, nSizeB = Sle_CutSize(pBase);
121 int k, nSizeC = Sle_CutSize(pCut);
122 int * pLeaveB = Sle_CutLeaves(pBase);
123 int * pLeaveC = Sle_CutLeaves(pCut);
124 if ( nSizeB == nSizeC )
125 {
126 for ( i = 0; i < nSizeB; i++ )
127 if ( pLeaveB[i] != pLeaveC[i] )
128 return 0;
129 return 1;
130 }
131 assert( nSizeB > nSizeC );
132 if ( nSizeC == 0 )
133 return 1;
134 for ( i = k = 0; i < nSizeB; i++ )
135 {
136 if ( pLeaveB[i] > pLeaveC[k] )
137 return 0;
138 if ( pLeaveB[i] == pLeaveC[k] )
139 {
140 if ( ++k == nSizeC )
141 return 1;
142 }
143 }
144 return 0;
145 }
Sle_CutCountBits(unsigned i)146 static inline int Sle_CutCountBits( unsigned i )
147 {
148 i = i - ((i >> 1) & 0x55555555);
149 i = (i & 0x33333333) + ((i >> 2) & 0x33333333);
150 i = ((i + (i >> 4)) & 0x0F0F0F0F);
151 return (i*(0x01010101))>>24;
152 }
Sle_SetLastCutIsContained(Vec_Int_t * vTemp,int * pBase)153 static inline int Sle_SetLastCutIsContained( Vec_Int_t * vTemp, int * pBase )
154 {
155 int i, * pCut, * pList = Vec_IntArray(vTemp);
156 Sle_ForEachCut( pList, pCut, i )
157 if ( Sle_CutIsUsed(pCut) && Sle_CutSize(pCut) <= Sle_CutSize(pBase) && (Sle_CutSign(pCut) & Sle_CutSign(pBase)) == Sle_CutSign(pCut) && Sle_SetCutIsContainedOrder(pBase, pCut) )
158 return 1;
159 return 0;
160 }
Sle_SetAddCut(Vec_Int_t * vTemp,int * pCut)161 static inline void Sle_SetAddCut( Vec_Int_t * vTemp, int * pCut )
162 {
163 int i, * pBase, * pList = Vec_IntArray(vTemp);
164 Sle_ForEachCut( pList, pBase, i )
165 if ( Sle_CutIsUsed(pBase) && Sle_CutSize(pCut) < Sle_CutSize(pBase) && (Sle_CutSign(pCut) & Sle_CutSign(pBase)) == Sle_CutSign(pCut) && Sle_SetCutIsContainedOrder(pBase, pCut) )
166 Sle_CutSetUnused( pBase );
167 Vec_IntPushArray( vTemp, pCut, Sle_CutSize(pCut)+1 );
168 Vec_IntAddToEntry( vTemp, 0, 1 );
169 }
Sle_ManCutMerge(Gia_Man_t * p,int iObj,Vec_Int_t * vCuts,Vec_Int_t * vTemp,int nLutSize)170 int Sle_ManCutMerge( Gia_Man_t * p, int iObj, Vec_Int_t * vCuts, Vec_Int_t * vTemp, int nLutSize )
171 {
172 Gia_Obj_t * pObj = Gia_ManObj( p, iObj );
173 int * pList0 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId0(pObj, iObj)) );
174 int * pList1 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId1(pObj, iObj)) );
175 int * pCut0, * pCut1, i, k, Cut[8], nCuts = 0;
176 Vec_IntFill( vTemp, 1, 0 );
177 Sle_ForEachCut1( pList0, pCut0, i )
178 Sle_ForEachCut1( pList1, pCut1, k )
179 {
180 if ( Sle_CutSize(pCut0) + Sle_CutSize(pCut1) > nLutSize && Sle_CutCountBits(Sle_CutSign(pCut0) | Sle_CutSign(pCut1)) > nLutSize )
181 continue;
182 if ( !Sle_CutMergeOrder(pCut0, pCut1, Cut, nLutSize) )
183 continue;
184 if ( Sle_SetLastCutIsContained(vTemp, Cut) )
185 continue;
186 Sle_SetAddCut( vTemp, Cut );
187 }
188 // reload
189 Vec_IntWriteEntry( vCuts, iObj, Vec_IntSize(vCuts) );
190 Vec_IntPush( vCuts, -1 );
191 pList0 = Vec_IntArray(vTemp);
192 Sle_ForEachCut( pList0, pCut0, i )
193 {
194 if ( !Sle_CutIsUsed(pCut0) )
195 continue;
196 Vec_IntPushArray( vCuts, pCut0, Sle_CutSize(pCut0)+1 );
197 nCuts++;
198 }
199 // add unit cut
200 Vec_IntPush( vCuts, Sle_CutSetSizeSign(1, 1<<(iObj % 28)) );
201 Vec_IntPush( vCuts, iObj );
202 Vec_IntWriteEntry( vCuts, Vec_IntEntry(vCuts, iObj), nCuts );
203 return nCuts;
204 }
Sle_ManComputeCuts(Gia_Man_t * p,int nLutSize,int fVerbose)205 Vec_Int_t * Sle_ManComputeCuts( Gia_Man_t * p, int nLutSize, int fVerbose )
206 {
207 int i, iObj, nCuts = 0;
208 Vec_Int_t * vTemp = Vec_IntAlloc( 1000 );
209 Vec_Int_t * vCuts = Vec_IntAlloc( 30 * Gia_ManAndNum(p) );
210 assert( nLutSize <= 6 );
211 Vec_IntFill( vCuts, Gia_ManObjNum(p), 0 );
212 Gia_ManForEachCiId( p, iObj, i )
213 {
214 Vec_IntWriteEntry( vCuts, iObj, Vec_IntSize(vCuts) );
215 Vec_IntPush( vCuts, 0 );
216 Vec_IntPush( vCuts, Sle_CutSetSizeSign(1, 1<<(iObj % 28)) );
217 Vec_IntPush( vCuts, iObj );
218 }
219 Gia_ManForEachAndId( p, iObj )
220 nCuts += Sle_ManCutMerge( p, iObj, vCuts, vTemp, nLutSize );
221 if ( fVerbose )
222 printf( "Nodes = %d. Cuts = %d. Cuts/Node = %.2f. Ints/Node = %.2f. Mem = %.2f MB.\n",
223 Gia_ManAndNum(p), nCuts, 1.0*nCuts/Gia_ManAndNum(p),
224 1.0*(Vec_IntSize(vCuts)-Gia_ManObjNum(p))/Gia_ManAndNum(p),
225 1.0*Vec_IntMemory(vCuts) / (1<<20) );
226 Vec_IntFree( vTemp );
227 return vCuts;
228 }
229
230 /**Function*************************************************************
231
232 Synopsis [Cut delay computation.]
233
234 Description []
235
236 SideEffects []
237
238 SeeAlso []
239
240 ***********************************************************************/
Sle_ManComputeDelayCut(Gia_Man_t * p,int * pCut,Vec_Int_t * vTime)241 int Sle_ManComputeDelayCut( Gia_Man_t * p, int * pCut, Vec_Int_t * vTime )
242 {
243 int nSize = Sle_CutSize(pCut);
244 int k, * pC = Sle_CutLeaves(pCut);
245 int DelayMax = 0;
246 for ( k = 0; k < nSize; k++ )
247 DelayMax = Abc_MaxInt( DelayMax, Vec_IntEntry(vTime, pC[k]) );
248 return DelayMax + 1;
249 }
Sle_ManComputeDelayOne(Gia_Man_t * p,int iObj,Vec_Int_t * vCuts,Vec_Int_t * vTime)250 int Sle_ManComputeDelayOne( Gia_Man_t * p, int iObj, Vec_Int_t * vCuts, Vec_Int_t * vTime )
251 {
252 int i, * pCut, Delay, DelayMin = ABC_INFINITY;
253 int * pList = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, iObj) );
254 Sle_ForEachCut( pList, pCut, i )
255 {
256 Delay = Sle_ManComputeDelayCut( p, pCut, vTime );
257 DelayMin = Abc_MinInt( DelayMin, Delay );
258 }
259 Vec_IntWriteEntry( vTime, iObj, DelayMin );
260 return DelayMin;
261 }
Sle_ManComputeDelay(Gia_Man_t * p,Vec_Int_t * vCuts)262 int Sle_ManComputeDelay( Gia_Man_t * p, Vec_Int_t * vCuts )
263 {
264 int iObj, Delay, DelayMax = 0;
265 Vec_Int_t * vTime = Vec_IntStart( Gia_ManObjNum(p) );
266 Gia_ManForEachAndId( p, iObj )
267 {
268 Delay = Sle_ManComputeDelayOne( p, iObj, vCuts, vTime );
269 DelayMax = Abc_MaxInt( DelayMax, Delay );
270 }
271 Vec_IntFree( vTime );
272 //printf( "Delay = %d.\n", DelayMax );
273 return DelayMax;
274 }
275
276 /**Function*************************************************************
277
278 Synopsis [Cut printing.]
279
280 Description []
281
282 SideEffects []
283
284 SeeAlso []
285
286 ***********************************************************************/
Sle_ManPrintCut(int * pCut)287 void Sle_ManPrintCut( int * pCut )
288 {
289 int nSize = Sle_CutSize(pCut);
290 int k, * pC = Sle_CutLeaves(pCut);
291 printf( "{" );
292 for ( k = 0; k < nSize; k++ )
293 printf( " %d", pC[k] );
294 printf( " }\n" );
295 }
Sle_ManPrintCuts(Gia_Man_t * p,Vec_Int_t * vCuts,int iObj)296 void Sle_ManPrintCuts( Gia_Man_t * p, Vec_Int_t * vCuts, int iObj )
297 {
298 int i, * pCut;
299 int * pList = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, iObj) );
300 printf( "Obj %3d\n", iObj );
301 Sle_ForEachCut( pList, pCut, i )
302 Sle_ManPrintCut( pCut );
303 printf( "\n" );
304 }
Sle_ManPrintCutsAll(Gia_Man_t * p,Vec_Int_t * vCuts)305 void Sle_ManPrintCutsAll( Gia_Man_t * p, Vec_Int_t * vCuts )
306 {
307 int iObj;
308 Gia_ManForEachAndId( p, iObj )
309 Sle_ManPrintCuts( p, vCuts, iObj );
310 }
Sle_ManComputeCutsTest(Gia_Man_t * p)311 void Sle_ManComputeCutsTest( Gia_Man_t * p )
312 {
313 Vec_Int_t * vCuts = Sle_ManComputeCuts( p, 4, 1 );
314 //Sle_ManPrintCutsAll( p, vCuts );
315 Vec_IntFree( vCuts );
316 }
317
318
319
320 /**Function*************************************************************
321
322 Synopsis [Derive mask representing internal nodes.]
323
324 Description []
325
326 SideEffects []
327
328 SeeAlso []
329
330 ***********************************************************************/
Sle_ManInternalNodeMask(Gia_Man_t * pGia)331 Vec_Bit_t * Sle_ManInternalNodeMask( Gia_Man_t * pGia )
332 {
333 int iObj;
334 Vec_Bit_t * vMask = Vec_BitStart( Gia_ManObjNum(pGia) );
335 Gia_ManForEachAndId( pGia, iObj )
336 Vec_BitWriteEntry( vMask, iObj, 1 );
337 return vMask;
338 }
339
340 /**Function*************************************************************
341
342 Synopsis [Check if the cut contains only primary inputs.]
343
344 Description []
345
346 SideEffects []
347
348 SeeAlso []
349
350 ***********************************************************************/
Sle_ManCutHasPisOnly(int * pCut,Vec_Bit_t * vMask)351 int Sle_ManCutHasPisOnly( int * pCut, Vec_Bit_t * vMask )
352 {
353 int k, * pC = Sle_CutLeaves(pCut);
354 for ( k = 0; k < Sle_CutSize(pCut); k++ )
355 if ( Vec_BitEntry(vMask, pC[k]) ) // internal node
356 return 0;
357 return 1;
358 }
359
360 /**Function*************************************************************
361
362 Synopsis [Derive cut fanins of each node.]
363
364 Description [These are nodes that are fanins of some cut of this node.]
365
366 SideEffects []
367
368 SeeAlso []
369
370 ***********************************************************************/
Sle_ManCollectCutFaninsOne(Gia_Man_t * pGia,int iObj,Vec_Int_t * vCuts,Vec_Bit_t * vMask,Vec_Int_t * vCutFanins,Vec_Bit_t * vMap)371 void Sle_ManCollectCutFaninsOne( Gia_Man_t * pGia, int iObj, Vec_Int_t * vCuts, Vec_Bit_t * vMask, Vec_Int_t * vCutFanins, Vec_Bit_t * vMap )
372 {
373 int i, iFanin, * pCut, * pList = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, iObj) );
374 Sle_ForEachCut( pList, pCut, i )
375 {
376 int nSize = Sle_CutSize(pCut);
377 int k, * pC = Sle_CutLeaves(pCut);
378 assert( nSize > 1 );
379 for ( k = 0; k < nSize; k++ )
380 if ( Vec_BitEntry(vMask, pC[k]) && !Vec_BitEntry(vMap, pC[k]) )
381 {
382 Vec_BitWriteEntry( vMap, pC[k], 1 );
383 Vec_IntPush( vCutFanins, pC[k] );
384 }
385 }
386 Vec_IntForEachEntry( vCutFanins, iFanin, i )
387 Vec_BitWriteEntry( vMap, iFanin, 0 );
388 }
Sle_ManCollectCutFanins(Gia_Man_t * pGia,Vec_Int_t * vCuts,Vec_Bit_t * vMask)389 Vec_Wec_t * Sle_ManCollectCutFanins( Gia_Man_t * pGia, Vec_Int_t * vCuts, Vec_Bit_t * vMask )
390 {
391 int iObj;
392 Vec_Bit_t * vMap = Vec_BitStart( Gia_ManObjNum(pGia) );
393 Vec_Wec_t * vCutFanins = Vec_WecStart( Gia_ManObjNum(pGia) );
394 Gia_ManForEachAndId( pGia, iObj )
395 Sle_ManCollectCutFaninsOne( pGia, iObj, vCuts, vMask, Vec_WecEntry(vCutFanins, iObj), vMap );
396 Vec_BitFree( vMap );
397 return vCutFanins;
398 }
399
400
401 typedef struct Sle_Man_t_ Sle_Man_t;
402 struct Sle_Man_t_
403 {
404 // user's data
405 Gia_Man_t * pGia; // user's manager (with mapping and edges)
406 int nLevels; // total number of levels
407 int fVerbose; // verbose flag
408 int nSatCalls; // the number of SAT calls
409 // SAT variables
410 int nNodeVars; // node variables (Gia_ManAndNum(pGia))
411 int nCutVars; // cut variables (total number of non-trivial cuts)
412 int nEdgeVars; // edge variables (total number of internal edges)
413 int nDelayVars; // delay variables (nNodeVars * nLevelsMax)
414 int nVarsTotal; // total number of variables
415 // SAT clauses
416 int nCutClas; // cut clauses
417 int nEdgeClas; // edge clauses
418 int nEdgeClas2; // edge clauses exclusivity
419 int nDelayClas; // delay clauses
420 // internal data
421 sat_solver * pSat; // SAT solver
422 Vec_Bit_t * vMask; // internal node mask
423 Vec_Int_t * vCuts; // cuts for each node
424 Vec_Wec_t * vCutFanins; // internal cut fanins of each node
425 Vec_Wec_t * vFanoutEdges; // internal cut fanins of each node
426 Vec_Wec_t * vEdgeCuts; // cuts of each edge for one node
427 Vec_Int_t * vObjMap; // temporary object map
428 Vec_Int_t * vCutFirst; // first cut of each node
429 Vec_Int_t * vEdgeFirst; // first edge of each node
430 Vec_Int_t * vDelayFirst; // first edge of each node
431 Vec_Int_t * vPolars; // initial
432 Vec_Int_t * vLits; // literals
433 // statistics
434 abctime timeStart;
435 };
436
Sle_ManList(Sle_Man_t * p,int i)437 static inline int * Sle_ManList( Sle_Man_t * p, int i ) { return Vec_IntEntryP(p->vCuts, Vec_IntEntry(p->vCuts, i)); }
438
439 /**Function*************************************************************
440
441 Synopsis []
442
443 Description []
444
445 SideEffects []
446
447 SeeAlso []
448
449 ***********************************************************************/
Sle_ManAlloc(Gia_Man_t * pGia,int nLevels,int fVerbose)450 Sle_Man_t * Sle_ManAlloc( Gia_Man_t * pGia, int nLevels, int fVerbose )
451 {
452 Sle_Man_t * p = ABC_CALLOC( Sle_Man_t, 1 );
453 p->pGia = pGia;
454 p->nLevels = nLevels;
455 p->fVerbose = fVerbose;
456 p->vMask = Sle_ManInternalNodeMask( pGia );
457 p->vCuts = Sle_ManComputeCuts( pGia, 4, fVerbose );
458 p->vCutFanins = Sle_ManCollectCutFanins( pGia, p->vCuts, p->vMask );
459 p->vFanoutEdges = Vec_WecStart( Gia_ManObjNum(pGia) );
460 p->vEdgeCuts = Vec_WecAlloc( 100 );
461 p->vObjMap = Vec_IntStartFull( Gia_ManObjNum(pGia) );
462 p->vCutFirst = Vec_IntStartFull( Gia_ManObjNum(pGia) );
463 p->vEdgeFirst = Vec_IntStartFull( Gia_ManObjNum(pGia) );
464 p->vDelayFirst = Vec_IntStartFull( Gia_ManObjNum(pGia) );
465 p->vPolars = Vec_IntAlloc( 100 );
466 p->vLits = Vec_IntAlloc( 100 );
467 p->nLevels = Sle_ManComputeDelay( pGia, p->vCuts );
468 return p;
469 }
Sle_ManStop(Sle_Man_t * p)470 void Sle_ManStop( Sle_Man_t * p )
471 {
472 sat_solver_delete( p->pSat );
473 Vec_BitFree( p->vMask );
474 Vec_IntFree( p->vCuts );
475 Vec_WecFree( p->vCutFanins );
476 Vec_WecFree( p->vFanoutEdges );
477 Vec_WecFree( p->vEdgeCuts );
478 Vec_IntFree( p->vObjMap );
479 Vec_IntFree( p->vCutFirst );
480 Vec_IntFree( p->vEdgeFirst );
481 Vec_IntFree( p->vDelayFirst );
482 Vec_IntFree( p->vPolars );
483 Vec_IntFree( p->vLits );
484 ABC_FREE( p );
485 }
486
487 /**Function*************************************************************
488
489 Synopsis []
490
491 Description []
492
493 SideEffects []
494
495 SeeAlso []
496
497 ***********************************************************************/
Sle_ManMarkupVariables(Sle_Man_t * p)498 void Sle_ManMarkupVariables( Sle_Man_t * p )
499 {
500 int iObj, Counter = Gia_ManObjNum(p->pGia);
501 // node variables
502 p->nNodeVars = Counter;
503 // cut variables
504 Gia_ManForEachAndId( p->pGia, iObj )
505 {
506 Vec_IntWriteEntry( p->vCutFirst, iObj, Counter );
507 Counter += Sle_ListCutNum( Sle_ManList(p, iObj) );
508 }
509 p->nCutVars = Counter - p->nNodeVars;
510 // edge variables
511 Gia_ManForEachAndId( p->pGia, iObj )
512 {
513 Vec_IntWriteEntry( p->vEdgeFirst, iObj, Counter );
514 Counter += Vec_IntSize( Vec_WecEntry(p->vCutFanins, iObj) );
515 }
516 p->nEdgeVars = Counter - p->nCutVars - p->nNodeVars;
517 // delay variables
518 Gia_ManForEachAndId( p->pGia, iObj )
519 {
520 Vec_IntWriteEntry( p->vDelayFirst, iObj, Counter );
521 Counter += p->nLevels;
522 }
523 p->nDelayVars = Counter - p->nEdgeVars - p->nCutVars - p->nNodeVars;
524 p->nVarsTotal = Counter;
525 }
526
527
528 /**Function*************************************************************
529
530 Synopsis [Derive initial variable assignment.]
531
532 Description []
533
534 SideEffects []
535
536 SeeAlso []
537
538 ***********************************************************************/
539 // returns 1 if Cut can represent LUT (Cut is equal or is contained in LUT)
Sle_ManCheckContained(int * pCutLeaves,int nCutLeaves,int * pLutFanins,int nLutFanins)540 static inline int Sle_ManCheckContained( int * pCutLeaves, int nCutLeaves, int * pLutFanins, int nLutFanins )
541 {
542 int i, k;
543 if ( nCutLeaves > nLutFanins )
544 return 0;
545 for ( i = 0; i < nCutLeaves; i++ )
546 {
547 for ( k = 0; k < nLutFanins; k++ )
548 if ( pCutLeaves[i] == pLutFanins[k] )
549 break;
550 if ( k == nLutFanins ) // not found
551 return 0;
552 }
553 return 1;
554 }
Sle_ManDeriveInit(Sle_Man_t * p)555 void Sle_ManDeriveInit( Sle_Man_t * p )
556 {
557 Vec_Int_t * vEdges;
558 int i, iObj, iFanin, iEdge;
559 if ( !Gia_ManHasMapping(p->pGia) )
560 return;
561 // derive initial state
562 Vec_IntClear( p->vPolars );
563 Gia_ManForEachAndId( p->pGia, iObj )
564 {
565 int nFanins, * pFanins, * pCut, * pList, iFound = -1;
566 if ( !Gia_ObjIsLut(p->pGia, iObj) )
567 continue;
568 Vec_IntPush( p->vPolars, iObj ); // node var
569 nFanins = Gia_ObjLutSize( p->pGia, iObj );
570 pFanins = Gia_ObjLutFanins( p->pGia, iObj );
571 // find cut
572 pList = Sle_ManList( p, iObj );
573 Sle_ForEachCut( pList, pCut, i )
574 if ( Sle_ManCheckContained( Sle_CutLeaves(pCut), Sle_CutSize(pCut), pFanins, nFanins ) )
575 {
576 iFound = i;
577 break;
578 }
579 if ( iFound == -1 )
580 {
581 printf( "Cannot find the following cut at node %d: {", iObj );
582 for ( i = 0; i < nFanins; i++ )
583 printf( " %d", pFanins[i] );
584 printf( " }\n" );
585 Sle_ManPrintCuts( p->pGia, p->vCuts, iObj );
586 fflush( stdout );
587 }
588 assert( iFound >= 0 );
589 Vec_IntPush( p->vPolars, Vec_IntEntry(p->vCutFirst, iObj) + iFound ); // cut var
590 // check if the cut contains only primary inputs - if so, its delay is equal to 1
591 if ( Sle_ManCutHasPisOnly(pCut, p->vMask) )
592 Vec_IntPush( p->vPolars, Vec_IntEntry(p->vDelayFirst, iObj) ); // delay var
593 }
594 Vec_IntSort( p->vPolars, 0 );
595 // find zero-delay edges
596 if ( !p->pGia->vEdge1 )
597 return;
598 vEdges = Gia_ManEdgeToArray( p->pGia );
599 Vec_IntForEachEntryDouble( vEdges, iFanin, iObj, i )
600 {
601 assert( iFanin < iObj );
602 assert( Gia_ObjIsLut(p->pGia, iFanin) );
603 assert( Gia_ObjIsLut(p->pGia, iObj) );
604 assert( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iFanin)) );
605 assert( Gia_ObjIsAnd(Gia_ManObj(p->pGia, iObj)) );
606 // find edge
607 iEdge = Vec_IntFind( Vec_WecEntry(p->vCutFanins, iObj), iFanin );
608 if ( iEdge < 0 )
609 continue;
610 assert( iEdge >= 0 );
611 Vec_IntPush( p->vPolars, Vec_IntEntry(p->vEdgeFirst, iObj) + iEdge ); // edge
612 }
613 Vec_IntFree( vEdges );
614 }
615
616 /**Function*************************************************************
617
618 Synopsis [Derive CNF.]
619
620 Description []
621
622 SideEffects []
623
624 SeeAlso []
625
626 ***********************************************************************/
Sle_ManDeriveCnf(Sle_Man_t * p,int nBTLimit,int fDynamic)627 void Sle_ManDeriveCnf( Sle_Man_t * p, int nBTLimit, int fDynamic )
628 {
629 int nTimeOut = 0;
630 int i, iObj, value;
631 Vec_Int_t * vArray;
632
633 // start the SAT solver
634 p->pSat = sat_solver_new();
635 sat_solver_setnvars( p->pSat, p->nVarsTotal );
636 sat_solver_set_resource_limits( p->pSat, nBTLimit, 0, 0, 0 );
637 sat_solver_set_runtime_limit( p->pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
638 sat_solver_set_random( p->pSat, 1 );
639 sat_solver_set_polarity( p->pSat, Vec_IntArray(p->vPolars), Vec_IntSize(p->vPolars) );
640 //sat_solver_set_var_activity( p->pSat, NULL, p->nVarsTotal );
641
642 // set drivers to be mapped
643 Gia_ManForEachCoDriverId( p->pGia, iObj, i )
644 if ( Vec_BitEntry(p->vMask, iObj) ) // internal node
645 {
646 Vec_IntFill( p->vLits, 1, Abc_Var2Lit(iObj, 0) ); // pos lit
647 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
648 assert( value );
649 }
650
651 // add cover clauses and edge-to-cut clauses
652 Gia_ManForEachAndId( p->pGia, iObj )
653 {
654 int e, iEdge, nEdges = 0, Entry;
655 int iCutVar0 = Vec_IntEntry( p->vCutFirst, iObj );
656 int iEdgeVar0 = Vec_IntEntry( p->vEdgeFirst, iObj );
657 int * pCut, * pList = Sle_ManList( p, iObj );
658 Vec_Int_t * vCutFans = Vec_WecEntry( p->vCutFanins, iObj );
659 assert( iCutVar0 > 0 && iEdgeVar0 > 0 );
660 // node requires one of the cuts
661 Vec_IntFill( p->vLits, 1, Abc_Var2Lit(iObj, 1) ); // neg lit
662 for ( i = 0; i < Sle_ListCutNum(pList); i++ )
663 Vec_IntPush( p->vLits, Abc_Var2Lit(iCutVar0 + i, 0) );
664 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
665 assert( value );
666 // cuts are mutually exclusive
667 for ( i = 0; i < Sle_ListCutNum(pList); i++ )
668 for ( e = i+1; e < Sle_ListCutNum(pList); e++ )
669 {
670 Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(iCutVar0 + i, 1), Abc_Var2Lit(iCutVar0 + e, 1) );
671 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
672 assert( value );
673 }
674 // cut requires fanin nodes
675 Vec_WecInit( p->vEdgeCuts, Vec_IntSize(vCutFans) );
676 Sle_ForEachCut( pList, pCut, i )
677 {
678 int nSize = Sle_CutSize(pCut);
679 int k, * pC = Sle_CutLeaves(pCut);
680 assert( nSize > 1 );
681 for ( k = 0; k < nSize; k++ )
682 {
683 if ( !Vec_BitEntry(p->vMask, pC[k]) )
684 continue;
685 Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(iCutVar0 + i, 1), Abc_Var2Lit(pC[k], 0) );
686 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
687 assert( value );
688 // find the edge ID between pC[k] and iObj
689 iEdge = Vec_IntEntry(p->vObjMap, pC[k]);
690 if ( iEdge == -1 )
691 {
692 Vec_IntWriteEntry( p->vObjMap, pC[k], (iEdge = nEdges++) );
693 Vec_WecPush( p->vFanoutEdges, pC[k], iEdgeVar0 + iEdge );
694 }
695 Vec_WecPush( p->vEdgeCuts, iEdge, iCutVar0 + i );
696 p->nCutClas++;
697 }
698 // cut requires the node
699 Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(iCutVar0 + i, 1), Abc_Var2Lit(iObj, 0) );
700 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
701 assert( value );
702 }
703 assert( nEdges == Vec_IntSize(vCutFans) );
704
705 // edge requires one of the fanout cuts
706 Vec_WecForEachLevel( p->vEdgeCuts, vArray, e )
707 {
708 assert( Vec_IntSize(vArray) > 0 );
709 Vec_IntFill( p->vLits, 1, Abc_Var2Lit(iEdgeVar0 + e, 1) ); // neg lit (edge)
710 Vec_IntForEachEntry( vArray, Entry, i )
711 Vec_IntPush( p->vLits, Abc_Var2Lit(Entry, 0) ); // pos lit (cut)
712 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
713 assert( value );
714 p->nEdgeClas++;
715 }
716
717 // clean object map
718 Vec_IntForEachEntry( vCutFans, Entry, i )
719 Vec_IntWriteEntry( p->vObjMap, Entry, -1 );
720 }
721
722 // mutual exclusivity of edges
723 Vec_WecForEachLevel( p->vFanoutEdges, vArray, iObj )
724 {
725 int j, k, EdgeJ, EdgeK;
726 int iEdgeVar0 = Vec_IntEntry( p->vEdgeFirst, iObj );
727 Vec_Int_t * vCutFans = Vec_WecEntry( p->vCutFanins, iObj );
728 // add fanin edges
729 for ( i = 0; i < Vec_IntSize(vCutFans); i++ )
730 Vec_IntPush( vArray, iEdgeVar0 + i );
731 // generate pairs
732 if ( fDynamic )
733 continue;
734 Vec_IntForEachEntry( vArray, EdgeJ, j )
735 Vec_IntForEachEntryStart( vArray, EdgeK, k, j+1 )
736 {
737 Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(EdgeJ, 1), Abc_Var2Lit(EdgeK, 1) );
738 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
739 assert( value );
740 }
741 p->nEdgeClas2 += Vec_IntSize(vArray) * (Vec_IntSize(vArray) - 1) / 2;
742 }
743
744 // add delay clauses
745 Gia_ManForEachAndId( p->pGia, iObj )
746 {
747 int e, iFanin;
748 int iEdgeVar0 = Vec_IntEntry( p->vEdgeFirst, iObj );
749 int iDelayVar0 = Vec_IntEntry( p->vDelayFirst, iObj );
750 Vec_Int_t * vCutFans = Vec_WecEntry( p->vCutFanins, iObj );
751 // check if the node has cuts containing only primary inputs
752 int * pCut, * pList = Sle_ManList( p, iObj );
753 Sle_ForEachCut( pList, pCut, i )
754 if ( Sle_ManCutHasPisOnly(pCut, p->vMask) )
755 {
756 Vec_IntFill( p->vLits, 1, Abc_Var2Lit(iDelayVar0, 0) ); // pos lit
757 // Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(iObj, 1), Abc_Var2Lit(iDelayVar0, 0) );
758 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
759 assert( value );
760 break;
761 }
762 // if ( i < Sle_ListCutNum(pList) )
763 // continue;
764 // create delay requirements for each cut fanin of this node
765 Vec_IntForEachEntry( vCutFans, iFanin, e )
766 {
767 int d, iDelayVarIn = Vec_IntEntry( p->vDelayFirst, iFanin );
768 for ( d = 0; d < p->nLevels; d++ )
769 {
770 Vec_IntClear( p->vLits );
771 Vec_IntPush( p->vLits, Abc_Var2Lit(iObj, 1) );
772 Vec_IntPush( p->vLits, Abc_Var2Lit(iFanin, 1) );
773 Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVarIn + d, 1) );
774 Vec_IntPush( p->vLits, Abc_Var2Lit(iEdgeVar0 + e, 0) );
775 if ( d < p->nLevels-1 )
776 Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVar0 + d+1, 0) );
777 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
778 assert( value );
779
780 Vec_IntClear( p->vLits );
781 Vec_IntPush( p->vLits, Abc_Var2Lit(iObj, 1) );
782 Vec_IntPush( p->vLits, Abc_Var2Lit(iFanin, 1) );
783 Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVarIn + d, 1) );
784 if ( d < p->nLevels-1 )
785 Vec_IntPush( p->vLits, Abc_Var2Lit(iEdgeVar0 + e, 1) );
786 Vec_IntPush( p->vLits, Abc_Var2Lit(iDelayVar0 + d, 0) );
787 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
788 assert( value );
789 }
790 p->nDelayClas += 2*p->nLevels;
791 }
792 }
793 }
794
795 /**Function*************************************************************
796
797 Synopsis [Add edge compatibility constraints.]
798
799 Description [Returns 1 if constraints have been added.]
800
801 SideEffects []
802
803 SeeAlso []
804
805 ***********************************************************************/
Sle_ManAddEdgeConstraints(Sle_Man_t * p,int nEdges)806 int Sle_ManAddEdgeConstraints( Sle_Man_t * p, int nEdges )
807 {
808 Vec_Int_t * vArray;
809 Vec_Int_t * vTemp = Vec_IntAlloc( 100 );
810 int value, iObj, nAdded = 0;
811 assert( nEdges == 1 || nEdges == 2 );
812 Vec_WecForEachLevel( p->vFanoutEdges, vArray, iObj )
813 {
814 int j, k, EdgeJ, EdgeK;
815 // check if they are incompatible
816 Vec_IntClear( vTemp );
817 Vec_IntForEachEntry( vArray, EdgeJ, j )
818 if ( sat_solver_var_value(p->pSat, EdgeJ) )
819 Vec_IntPush( vTemp, EdgeJ );
820 if ( Vec_IntSize(vTemp) <= nEdges )
821 continue;
822 nAdded++;
823 if ( nEdges == 1 )
824 {
825 // generate pairs
826 Vec_IntForEachEntry( vTemp, EdgeJ, j )
827 Vec_IntForEachEntryStart( vTemp, EdgeK, k, j+1 )
828 {
829 Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(EdgeJ, 1), Abc_Var2Lit(EdgeK, 1) );
830 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
831 assert( value );
832 }
833 p->nEdgeClas2 += Vec_IntSize(vTemp) * (Vec_IntSize(vTemp) - 1) / 2;
834 }
835 else if ( nEdges == 2 )
836 {
837 int m, EdgeM;
838 // generate triples
839 Vec_IntForEachEntry( vTemp, EdgeJ, j )
840 Vec_IntForEachEntryStart( vTemp, EdgeK, k, j+1 )
841 Vec_IntForEachEntryStart( vTemp, EdgeM, m, k+1 )
842 {
843 Vec_IntFillTwo( p->vLits, 2, Abc_Var2Lit(EdgeJ, 1), Abc_Var2Lit(EdgeK, 1) );
844 Vec_IntPush( p->vLits, Abc_Var2Lit(EdgeM, 1) );
845 value = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntLimit(p->vLits) );
846 assert( value );
847 }
848 p->nEdgeClas2 += Vec_IntSize(vTemp) * (Vec_IntSize(vTemp) - 1) * (Vec_IntSize(vTemp) - 2) / 6;
849 }
850 else assert( 0 );
851 }
852 Vec_IntFree( vTemp );
853 //printf( "Added clauses to %d nodes.\n", nAdded );
854 return nAdded;
855 }
856
857 /**Function*************************************************************
858
859 Synopsis []
860
861 Description []
862
863 SideEffects []
864
865 SeeAlso []
866
867 ***********************************************************************/
Sle_ManDeriveResult(Sle_Man_t * p,Vec_Int_t * vEdge2,Vec_Int_t * vMapping)868 void Sle_ManDeriveResult( Sle_Man_t * p, Vec_Int_t * vEdge2, Vec_Int_t * vMapping )
869 {
870 Vec_Int_t * vMapTemp;
871 int iObj;
872 // create mapping
873 Vec_IntFill( vMapping, Gia_ManObjNum(p->pGia), 0 );
874 Gia_ManForEachAndId( p->pGia, iObj )
875 {
876 int i, iCut, iCutVar0 = Vec_IntEntry( p->vCutFirst, iObj );
877 int * pCut, * pCutThis = NULL, * pList = Sle_ManList( p, iObj );
878 if ( !sat_solver_var_value(p->pSat, iObj) )
879 continue;
880 Sle_ForEachCut( pList, pCut, iCut )
881 if ( sat_solver_var_value(p->pSat, iCutVar0 + iCut) )
882 {
883 assert( pCutThis == NULL );
884 pCutThis = pCut;
885 }
886 assert( pCutThis != NULL );
887 Vec_IntWriteEntry( vMapping, iObj, Vec_IntSize(vMapping) );
888 Vec_IntPush( vMapping, Sle_CutSize(pCutThis) );
889 for ( i = 0; i < Sle_CutSize(pCutThis); i++ )
890 Vec_IntPush( vMapping, Sle_CutLeaves(pCutThis)[i] );
891 Vec_IntPush( vMapping, iObj );
892 }
893 vMapTemp = p->pGia->vMapping;
894 p->pGia->vMapping = vMapping;
895 // collect edges
896 Vec_IntClear( vEdge2 );
897 Gia_ManForEachAndId( p->pGia, iObj )
898 {
899 int i, iFanin, iEdgeVar0 = Vec_IntEntry( p->vEdgeFirst, iObj );
900 Vec_Int_t * vCutFans = Vec_WecEntry( p->vCutFanins, iObj );
901 //int * pCut, * pList = Sle_ManList( p, iObj );
902 // int iCutVar0 = Vec_IntEntry( p->vCutFirst, iObj );
903 if ( !sat_solver_var_value(p->pSat, iObj) )
904 continue;
905 //for ( i = 0; i < Sle_ListCutNum(pList); i++ )
906 // printf( "%d", sat_solver_var_value(p->pSat, iCutVar0 + i) );
907 //printf( "\n" );
908 Vec_IntForEachEntry( vCutFans, iFanin, i )
909 if ( sat_solver_var_value(p->pSat, iFanin) && sat_solver_var_value(p->pSat, iEdgeVar0 + i) )
910 {
911 // verify edge
912 int * pFanins = Gia_ObjLutFanins( p->pGia, iObj );
913 int k, nFanins = Gia_ObjLutSize( p->pGia, iObj );
914 for ( k = 0; k < nFanins; k++ )
915 {
916 //printf( "%d ", pFanins[k] );
917 if ( pFanins[k] == iFanin )
918 break;
919 }
920 //printf( "\n" );
921 if ( k == nFanins )
922 // printf( "Cannot find LUT with input %d at node %d.\n", iFanin, iObj );
923 continue;
924 Vec_IntPushTwo( vEdge2, iFanin, iObj );
925 }
926 }
927 p->pGia->vMapping = vMapTemp;
928 }
929
930 /**Function*************************************************************
931
932 Synopsis []
933
934 Description []
935
936 SideEffects []
937
938 SeeAlso []
939
940 ***********************************************************************/
Sle_ManExplore(Gia_Man_t * pGia,int nBTLimit,int DelayInit,int fDynamic,int fTwoEdges,int fVerbose)941 void Sle_ManExplore( Gia_Man_t * pGia, int nBTLimit, int DelayInit, int fDynamic, int fTwoEdges, int fVerbose )
942 {
943 int fVeryVerbose = 0;
944 abctime clk = Abc_Clock();
945 Vec_Int_t * vEdges2 = Vec_IntAlloc(1000);
946 Vec_Int_t * vMapping = Vec_IntAlloc(1000);
947 int i, iLut, nConfs, status, Delay, iFirstVar;
948 int DelayStart = (DelayInit || !Gia_ManHasMapping(pGia)) ? DelayInit : Gia_ManLutLevel(pGia, NULL);
949 Sle_Man_t * p = Sle_ManAlloc( pGia, DelayStart, fVerbose );
950 if ( fVerbose )
951 printf( "Running solver with %d conflicts, %d initial delay, and %d edges. Dynamic constraints = %s.\n", nBTLimit, DelayInit, 1+fTwoEdges, fDynamic?"yes":"no" );
952 Sle_ManMarkupVariables( p );
953 if ( fVerbose )
954 printf( "Vars: Total = %d. Node = %d. Cut = %d. Edge = %d. Delay = %d.\n",
955 p->nVarsTotal, p->nNodeVars, p->nCutVars, p->nEdgeVars, p->nDelayVars );
956 Sle_ManDeriveInit( p );
957 Sle_ManDeriveCnf( p, nBTLimit, fDynamic || fTwoEdges );
958 if ( fVerbose )
959 printf( "Clas: Total = %d. Cut = %d. Edge = %d. EdgeEx = %d. Delay = %d.\n",
960 sat_solver_nclauses(p->pSat), p->nCutClas, p->nEdgeClas, p->nEdgeClas2, p->nDelayClas );
961 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", NULL, NULL, 0 );
962 for ( Delay = p->nLevels; Delay >= 0; Delay-- )
963 {
964 // we constrain COs, although it would be fine to constrain only POs
965 if ( Delay < p->nLevels )
966 {
967 Gia_ManForEachCoDriverId( p->pGia, iLut, i )
968 if ( Vec_BitEntry(p->vMask, iLut) ) // internal node
969 {
970 iFirstVar = Vec_IntEntry( p->vDelayFirst, iLut );
971 if ( !sat_solver_push(p->pSat, Abc_Var2Lit(iFirstVar + Delay, 1)) )
972 break;
973 }
974 if ( i < Gia_ManCoNum(p->pGia) )
975 {
976 if ( fVerbose )
977 {
978 printf( "Proved UNSAT for delay %d. ", Delay );
979 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
980 }
981 break;
982 }
983 }
984 // solve with assumptions
985 //clk = Abc_Clock();
986 nConfs = sat_solver_nconflicts( p->pSat );
987 while ( 1 )
988 {
989 p->nSatCalls++;
990 status = sat_solver_solve_internal( p->pSat );
991 if ( status != l_True )
992 break;
993 if ( !Sle_ManAddEdgeConstraints(p, 1+fTwoEdges) )
994 break;
995 }
996 nConfs = sat_solver_nconflicts( p->pSat ) - nConfs;
997 if ( status == l_True )
998 {
999 if ( fVerbose )
1000 {
1001 int nNodes = 0, nEdges = 0;
1002 for ( i = 0; i < p->nNodeVars; i++ )
1003 nNodes += sat_solver_var_value(p->pSat, i);
1004 for ( i = 0; i < p->nEdgeVars; i++ )
1005 nEdges += sat_solver_var_value(p->pSat, p->nNodeVars + p->nCutVars + i);
1006 printf( "Solution with delay %2d, node count %5d, and edge count %5d exists. Conf = %8d. ", Delay, nNodes, nEdges, nConfs );
1007 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1008 }
1009 // save the result
1010 Sle_ManDeriveResult( p, vEdges2, vMapping );
1011 if ( fVeryVerbose )
1012 {
1013 printf( "Nodes: " );
1014 for ( i = 0; i < p->nNodeVars; i++ )
1015 if ( sat_solver_var_value(p->pSat, i) )
1016 printf( "%d ", i );
1017 printf( "\n" );
1018 printf( "\n" );
1019
1020 Vec_IntPrint( p->vCutFirst );
1021 printf( "Cuts: " );
1022 for ( i = 0; i < p->nCutVars; i++ )
1023 if ( sat_solver_var_value(p->pSat, p->nNodeVars + i) )
1024 printf( "%d ", p->nNodeVars + i );
1025 printf( "\n" );
1026 printf( "\n" );
1027
1028 Vec_IntPrint( p->vEdgeFirst );
1029 printf( "Edges: " );
1030 for ( i = 0; i < p->nEdgeVars; i++ )
1031 if ( sat_solver_var_value(p->pSat, p->nNodeVars + p->nCutVars + i) )
1032 printf( "%d ", p->nNodeVars + p->nCutVars + i );
1033 printf( "\n" );
1034 printf( "\n" );
1035
1036 Vec_IntPrint( p->vDelayFirst );
1037 printf( "Delays: " );
1038 for ( i = 0; i < p->nDelayVars; i++ )
1039 if ( sat_solver_var_value(p->pSat, p->nNodeVars + p->nCutVars + p->nEdgeVars + i) )
1040 printf( "%d ", p->nNodeVars + p->nCutVars + p->nEdgeVars + i );
1041 printf( "\n" );
1042 printf( "\n" );
1043 }
1044 }
1045 else
1046 {
1047 if ( fVerbose )
1048 {
1049 if ( status == l_False )
1050 printf( "Proved UNSAT for delay %d. Conf = %8d. ", Delay, nConfs );
1051 else
1052 printf( "Resource limit reached for delay %d. Conf = %8d. ", Delay, nConfs );
1053 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1054 }
1055 break;
1056 }
1057 }
1058 if ( fVerbose )
1059 printf( "Clas: Total = %d. Cut = %d. Edge = %d. EdgeEx = %d. Delay = %d. Calls = %d.\n",
1060 sat_solver_nclauses(p->pSat), p->nCutClas, p->nEdgeClas, p->nEdgeClas2, p->nDelayClas, p->nSatCalls );
1061 if ( Vec_IntSize(vMapping) > 0 )
1062 {
1063 Gia_ManEdgeFromArray( p->pGia, vEdges2 );
1064 Vec_IntFree( vEdges2 );
1065 Vec_IntFreeP( &p->pGia->vMapping );
1066 p->pGia->vMapping = vMapping;
1067 }
1068 else
1069 {
1070 Vec_IntFree( vEdges2 );
1071 Vec_IntFree( vMapping );
1072 }
1073 Vec_IntFreeP( &p->pGia->vPacking );
1074 Sle_ManStop( p );
1075 }
1076
1077 ////////////////////////////////////////////////////////////////////////
1078 /// END OF FILE ///
1079 ////////////////////////////////////////////////////////////////////////
1080
1081
1082 ABC_NAMESPACE_IMPL_END
1083
1084