ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
mfsResub.c File Reference
#include "mfsInt.h"
Include dependency graph for mfsResub.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START void Abc_NtkMfsUpdateNetwork (Mfs_Man_t *p, Abc_Obj_t *pObj, Vec_Ptr_t *vMfsFanins, Hop_Obj_t *pFunc)
 DECLARATIONS ///.
 
void Abc_NtkMfsPrintResubStats (Mfs_Man_t *p)
 
int Abc_NtkMfsTryResubOnce (Mfs_Man_t *p, int *pCands, int nCands)
 
int Abc_NtkMfsSolveSatResub (Mfs_Man_t *p, Abc_Obj_t *pNode, int iFanin, int fOnlyRemove, int fSkipUpdate)
 DECLARATIONS ///.
 
int Abc_NtkMfsSolveSatResub2 (Mfs_Man_t *p, Abc_Obj_t *pNode, int iFanin, int iFanin2)
 
int Abc_NtkMfsEdgeSwapEval (Mfs_Man_t *p, Abc_Obj_t *pNode)
 
int Abc_NtkMfsEdgePower (Mfs_Man_t *p, Abc_Obj_t *pNode)
 
int Abc_NtkMfsResubNode (Mfs_Man_t *p, Abc_Obj_t *pNode)
 
int Abc_NtkMfsResubNode2 (Mfs_Man_t *p, Abc_Obj_t *pNode)
 

Function Documentation

◆ Abc_NtkMfsEdgePower()

int Abc_NtkMfsEdgePower ( Mfs_Man_t * p,
Abc_Obj_t * pNode )

Function*************************************************************

Synopsis [Evaluates the possibility of replacing given edge by another edge.]

Description []

SideEffects []

SeeAlso []

Definition at line 508 of file mfsResub.c.

509{
510 Abc_Obj_t * pFanin;
511 int i;
512 // try replacing area critical fanins
513 Abc_ObjForEachFanin( pNode, pFanin, i )
514 {
515 if ( Abc_MfsObjProb(p, pFanin) >= 0.35 )
516 {
517 if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
518 return 1;
519 } else if ( Abc_MfsObjProb(p, pFanin) >= 0.25 ) // sjang
520 {
521 if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
522 return 1;
523 }
524 }
525 return 0;
526}
Abc_Obj_t
struct Abc_Obj_t_ Abc_Obj_t
Definition abc.h:116
Abc_ObjForEachFanin
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition abc.h:527
p
Cube * p
Definition exorList.c:222
Abc_NtkMfsSolveSatResub
int Abc_NtkMfsSolveSatResub(Mfs_Man_t *p, Abc_Obj_t *pNode, int iFanin, int fOnlyRemove, int fSkipUpdate)
DECLARATIONS ///.
Definition mfsResub.c:165
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NtkMfsEdgeSwapEval()

int Abc_NtkMfsEdgeSwapEval ( Mfs_Man_t * p,
Abc_Obj_t * pNode )

Function*************************************************************

Synopsis [Evaluates the possibility of replacing given edge by another edge.]

Description []

SideEffects []

SeeAlso []

Definition at line 488 of file mfsResub.c.

489{
490 Abc_Obj_t * pFanin;
491 int i;
492 Abc_ObjForEachFanin( pNode, pFanin, i )
493 Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 1 );
494 return 0;
495}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NtkMfsPrintResubStats()

void Abc_NtkMfsPrintResubStats ( Mfs_Man_t * p)

Function*************************************************************

Synopsis [Prints resub candidate stats.]

Description []

SideEffects []

SeeAlso []

Definition at line 72 of file mfsResub.c.

73{
74 Abc_Obj_t * pFanin, * pNode;
75 int i, k, nAreaCrits = 0, nAreaExpanse = 0;
76 int nFaninMax = Abc_NtkGetFaninMax(p->pNtk);
77 Abc_NtkForEachNode( p->pNtk, pNode, i )
78 Abc_ObjForEachFanin( pNode, pFanin, k )
79 {
80 if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
81 {
82 nAreaCrits++;
83 nAreaExpanse += (int)(Abc_ObjFaninNum(pNode) < nFaninMax);
84 }
85 }
86// printf( "Total area-critical fanins = %d. Belonging to expandable nodes = %d.\n",
87// nAreaCrits, nAreaExpanse );
88}
Abc_NtkGetFaninMax
ABC_DLL int Abc_NtkGetFaninMax(Abc_Ntk_t *pNtk)
Definition abcUtil.c:486
Abc_NtkForEachNode
#define Abc_NtkForEachNode(pNtk, pNode, i)
Definition abc.h:464
Here is the call graph for this function:

◆ Abc_NtkMfsResubNode()

int Abc_NtkMfsResubNode ( Mfs_Man_t * p,
Abc_Obj_t * pNode )

Function*************************************************************

Synopsis [Performs resubstitution for the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 539 of file mfsResub.c.

540{
541 Abc_Obj_t * pFanin;
542 int i;
543 // try replacing area critical fanins
544 Abc_ObjForEachFanin( pNode, pFanin, i )
545 if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
546 {
547 if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
548 return 1;
549 }
550 // try removing redundant edges
551 if ( !p->pPars->fArea )
552 {
553 Abc_ObjForEachFanin( pNode, pFanin, i )
554 if ( Abc_ObjIsCi(pFanin) || Abc_ObjFanoutNum(pFanin) != 1 )
555 {
556 if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1, 0 ) )
557 return 1;
558 }
559 }
560 if ( Abc_ObjFaninNum(pNode) == p->nFaninMax )
561 return 0;
562/*
563 // try replacing area critical fanins while adding two new fanins
564 Abc_ObjForEachFanin( pNode, pFanin, i )
565 if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
566 {
567 if ( Abc_NtkMfsSolveSatResub2( p, pNode, i, -1 ) )
568 return 1;
569 }
570*/
571 return 0;
572}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NtkMfsResubNode2()

int Abc_NtkMfsResubNode2 ( Mfs_Man_t * p,
Abc_Obj_t * pNode )

Function*************************************************************

Synopsis [Performs resubstitution for the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 585 of file mfsResub.c.

586{
587 Abc_Obj_t * pFanin, * pFanin2;
588 int i, k;
589/*
590 Abc_ObjForEachFanin( pNode, pFanin, i )
591 if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
592 {
593 if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0, 0 ) )
594 return 1;
595 }
596*/
597 if ( Abc_ObjFaninNum(pNode) < 2 )
598 return 0;
599 // try replacing one area critical fanin and one other fanin while adding two new fanins
600 Abc_ObjForEachFanin( pNode, pFanin, i )
601 {
602 if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
603 {
604 // consider second fanin to remove at the same time
605 Abc_ObjForEachFanin( pNode, pFanin2, k )
606 {
607 if ( i != k && Abc_NtkMfsSolveSatResub2( p, pNode, i, k ) )
608 return 1;
609 }
610 }
611 }
612 return 0;
613}
Abc_NtkMfsSolveSatResub2
int Abc_NtkMfsSolveSatResub2(Mfs_Man_t *p, Abc_Obj_t *pNode, int iFanin, int iFanin2)
Definition mfsResub.c:319
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NtkMfsSolveSatResub()

int Abc_NtkMfsSolveSatResub ( Mfs_Man_t * p,
Abc_Obj_t * pNode,
int iFanin,
int fOnlyRemove,
int fSkipUpdate )

DECLARATIONS ///.

Function*************************************************************

Synopsis [Performs resubstitution for the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 165 of file mfsResub.c.

166{
167 int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 200;// || pNode->Id == 556;
168 unsigned * pData;
169 int pCands[MFS_FANIN_MAX];
170 int RetValue, iVar, i, nCands, nWords, w;
171 abctime clk;
172 Abc_Obj_t * pFanin;
173 Hop_Obj_t * pFunc;
174 assert( iFanin >= 0 );
175 p->nTryRemoves++;
176
177 // clean simulation info
178 Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords );
179 p->nCexes = 0;
180 if ( p->pPars->fVeryVerbose )
181 {
182// printf( "\n" );
183 printf( "%5d : Lev =%3d. Leaf =%3d. Node =%3d. Divs =%3d. Fanin = %4d (%d/%d), MFFC = %d\n",
184 pNode->Id, pNode->Level, Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes), Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode),
185 Abc_ObjFaninId(pNode, iFanin), iFanin, Abc_ObjFaninNum(pNode),
186 Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin), NULL) : 0 );
187 }
188
189 // try fanins without the critical fanin
190 nCands = 0;
191 Vec_PtrClear( p->vMfsFanins );
192 Abc_ObjForEachFanin( pNode, pFanin, i )
193 {
194 if ( i == iFanin )
195 continue;
196 Vec_PtrPush( p->vMfsFanins, pFanin );
197 iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
198 pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
199 }
200 RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
201 if ( RetValue == -1 )
202 return 0;
203 if ( RetValue == 1 )
204 {
205 if ( p->pPars->fVeryVerbose )
206 printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
207 p->nNodesResub++;
208 p->nNodesGainedLevel++;
209 if ( fSkipUpdate )
210 return 1;
211clk = Abc_Clock();
212 // derive the function
213 pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
214 if ( pFunc == NULL )
215 return 0;
216 // update the network
217 Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
218p->timeInt += Abc_Clock() - clk;
219 p->nRemoves++;
220 return 1;
221 }
222
223 if ( fOnlyRemove || p->pPars->fRrOnly )
224 return 0;
225
226 p->nTryResubs++;
227 if ( fVeryVerbose )
228 {
229 for ( i = 0; i < 9; i++ )
230 printf( " " );
231 for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
232 printf( "%d", i % 10 );
233 for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
234 if ( i == iFanin )
235 printf( "*" );
236 else
237 printf( "%c", 'a' + i );
238 printf( "\n" );
239 }
240 iVar = -1;
241 while ( 1 )
242 {
243 if ( fVeryVerbose )
244 {
245 printf( "%3d: %3d ", p->nCexes, iVar );
246 for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
247 {
248 pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
249 printf( "%d", Abc_InfoHasBit(pData, p->nCexes-1) );
250 }
251 printf( "\n" );
252 }
253
254 // find the next divisor to try
255 nWords = Abc_BitWordNum(p->nCexes);
256 assert( nWords <= p->nDivWords );
257 for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
258 {
259 if ( p->pPars->fPower )
260 {
261 Abc_Obj_t * pDiv = (Abc_Obj_t *)Vec_PtrEntry(p->vDivs, iVar);
262 // only accept the divisor if it is "cool"
263 if ( Abc_MfsObjProb(p, pDiv) >= 0.15 )
264 continue;
265 }
266 pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, iVar );
267 for ( w = 0; w < nWords; w++ )
268 if ( pData[w] != ~0 )
269 break;
270 if ( w == nWords )
271 break;
272 }
273 if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
274 return 0;
275
276 pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
277 RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 );
278 if ( RetValue == -1 )
279 return 0;
280 if ( RetValue == 1 )
281 {
282 if ( p->pPars->fVeryVerbose )
283 printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
284 p->nNodesResub++;
285 p->nNodesGainedLevel++;
286 if ( fSkipUpdate )
287 return 1;
288clk = Abc_Clock();
289 // derive the function
290 pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
291 if ( pFunc == NULL )
292 return 0;
293 // update the network
294 Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
295 Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
296p->timeInt += Abc_Clock() - clk;
297 p->nResubs++;
298 return 1;
299 }
300 if ( p->nCexes >= p->pPars->nWinMax )
301 break;
302 }
303 if ( p->pPars->fVeryVerbose )
304 printf( "Node %d: Cannot find replacement for fanin %d.\n", pNode->Id, iFanin );
305 return 0;
306}
nWords
int nWords
Definition abcNpn.c:127
Abc_NodeMffcLabel
ABC_DLL int Abc_NodeMffcLabel(Abc_Obj_t *pNode, Vec_Ptr_t *vNodes)
Definition abcRefs.c:439
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
Hop_Obj_t
struct Hop_Obj_t_ Hop_Obj_t
Definition hop.h:50
Abc_NtkMfsInterplate
Hop_Obj_t * Abc_NtkMfsInterplate(Mfs_Man_t *p, int *pCands, int nCands)
Definition mfsInter.c:329
MFS_FANIN_MAX
#define MFS_FANIN_MAX
INCLUDES ///.
Definition mfsInt.h:47
Abc_NtkMfsTryResubOnce
int Abc_NtkMfsTryResubOnce(Mfs_Man_t *p, int *pCands, int nCands)
Definition mfsResub.c:101
Abc_NtkMfsUpdateNetwork
ABC_NAMESPACE_IMPL_START void Abc_NtkMfsUpdateNetwork(Mfs_Man_t *p, Abc_Obj_t *pObj, Vec_Ptr_t *vMfsFanins, Hop_Obj_t *pFunc)
DECLARATIONS ///.
Definition mfsResub.c:45
Abc_Obj_t_::Id
int Id
Definition abc.h:132
Abc_Obj_t_::Level
unsigned Level
Definition abc.h:142
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NtkMfsSolveSatResub2()

int Abc_NtkMfsSolveSatResub2 ( Mfs_Man_t * p,
Abc_Obj_t * pNode,
int iFanin,
int iFanin2 )

Function*************************************************************

Synopsis [Performs resubstitution for the node.]

Description []

SideEffects []

SeeAlso []

Definition at line 319 of file mfsResub.c.

320{
321 int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
322 unsigned * pData, * pData2;
323 int pCands[MFS_FANIN_MAX];
324 int RetValue, iVar, iVar2, i, w, nCands, nWords, fBreak;
325 abctime clk;
326 Abc_Obj_t * pFanin;
327 Hop_Obj_t * pFunc;
328 assert( iFanin >= 0 );
329 assert( iFanin2 >= 0 || iFanin2 == -1 );
330
331 // clean simulation info
332 Vec_PtrFillSimInfo( p->vDivCexes, 0, p->nDivWords );
333 p->nCexes = 0;
334 if ( fVeryVerbose )
335 {
336 printf( "\n" );
337 printf( "Node %5d : Level = %2d. Divs = %3d. Fanins = %d/%d (out of %d). MFFC = %d\n",
338 pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode),
339 iFanin, iFanin2, Abc_ObjFaninNum(pNode),
340 Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin), NULL) : 0 );
341 }
342
343 // try fanins without the critical fanin
344 nCands = 0;
345 Vec_PtrClear( p->vMfsFanins );
346 Abc_ObjForEachFanin( pNode, pFanin, i )
347 {
348 if ( i == iFanin || i == iFanin2 )
349 continue;
350 Vec_PtrPush( p->vMfsFanins, pFanin );
351 iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
352 pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVarsSat, iVar ), 1 );
353 }
354 RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands );
355 if ( RetValue == -1 )
356 return 0;
357 if ( RetValue == 1 )
358 {
359 if ( fVeryVerbose )
360 printf( "Node %d: Fanins %d/%d can be removed.\n", pNode->Id, iFanin, iFanin2 );
361 p->nNodesResub++;
362 p->nNodesGainedLevel++;
363clk = Abc_Clock();
364 // derive the function
365 pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
366 if ( pFunc == NULL )
367 return 0;
368 // update the network
369 Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
370p->timeInt += Abc_Clock() - clk;
371 return 1;
372 }
373
374 if ( fVeryVerbose )
375 {
376 for ( i = 0; i < 11; i++ )
377 printf( " " );
378 for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
379 printf( "%d", i % 10 );
380 for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
381 if ( i == iFanin || i == iFanin2 )
382 printf( "*" );
383 else
384 printf( "%c", 'a' + i );
385 printf( "\n" );
386 }
387 iVar = iVar2 = -1;
388 while ( 1 )
389 {
390#if 1 // sjang
391#endif
392 if ( fVeryVerbose )
393 {
394 printf( "%3d: %2d %2d ", p->nCexes, iVar, iVar2 );
395 for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
396 {
397 pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
398 printf( "%d", Abc_InfoHasBit(pData, p->nCexes-1) );
399 }
400 printf( "\n" );
401 }
402
403 // find the next divisor to try
404 nWords = Abc_BitWordNum(p->nCexes);
405 assert( nWords <= p->nDivWords );
406 fBreak = 0;
407 for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
408 {
409 pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, iVar );
410#if 1 // sjang
411 if ( p->pPars->fPower )
412 {
413 Abc_Obj_t * pDiv = (Abc_Obj_t *)Vec_PtrEntry(p->vDivs, iVar);
414 // only accept the divisor if it is "cool"
415 if ( Abc_MfsObjProb(p, pDiv) >= 0.12 )
416 continue;
417 }
418#endif
419 for ( iVar2 = 0; iVar2 < iVar; iVar2++ )
420 {
421 pData2 = (unsigned *)Vec_PtrEntry( p->vDivCexes, iVar2 );
422#if 1 // sjang
423 if ( p->pPars->fPower )
424 {
425 Abc_Obj_t * pDiv = (Abc_Obj_t *)Vec_PtrEntry(p->vDivs, iVar2);
426 // only accept the divisor if it is "cool"
427 if ( Abc_MfsObjProb(p, pDiv) >= 0.12 )
428 continue;
429 }
430#endif
431 for ( w = 0; w < nWords; w++ )
432 if ( (pData[w] | pData2[w]) != ~0 )
433 break;
434 if ( w == nWords )
435 {
436 fBreak = 1;
437 break;
438 }
439 }
440 if ( fBreak )
441 break;
442 }
443 if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
444 return 0;
445
446 pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar2), 1 );
447 pCands[nCands+1] = toLitCond( Vec_IntEntry(p->vProjVarsSat, iVar), 1 );
448 RetValue = Abc_NtkMfsTryResubOnce( p, pCands, nCands+2 );
449 if ( RetValue == -1 )
450 return 0;
451 if ( RetValue == 1 )
452 {
453 if ( fVeryVerbose )
454 printf( "Node %d: Fanins %d/%d can be replaced by divisors %d/%d.\n", pNode->Id, iFanin, iFanin2, iVar, iVar2 );
455 p->nNodesResub++;
456 p->nNodesGainedLevel++;
457clk = Abc_Clock();
458 // derive the function
459 pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+2 );
460 if ( pFunc == NULL )
461 return 0;
462 // update the network
463 Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar2) );
464 Vec_PtrPush( p->vMfsFanins, Vec_PtrEntry(p->vDivs, iVar) );
465 assert( Vec_PtrSize(p->vMfsFanins) == nCands + 2 );
466 Abc_NtkMfsUpdateNetwork( p, pNode, p->vMfsFanins, pFunc );
467p->timeInt += Abc_Clock() - clk;
468 return 1;
469 }
470 if ( p->nCexes >= p->pPars->nWinMax )
471 break;
472 }
473 return 0;
474}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_NtkMfsTryResubOnce()

int Abc_NtkMfsTryResubOnce ( Mfs_Man_t * p,
int * pCands,
int nCands )

Function*************************************************************

Synopsis [Tries resubstitution.]

Description [Returns 1 if it is feasible, or 0 if c-ex is found.]

SideEffects []

SeeAlso []

Definition at line 101 of file mfsResub.c.

102{
103 int fVeryVerbose = 0;
104 unsigned * pData;
105 int RetValue, RetValue2 = -1, iVar, i;//, clk = Abc_Clock();
106/*
107 if ( p->pPars->fGiaSat )
108 {
109 RetValue2 = Abc_NtkMfsTryResubOnceGia( p, pCands, nCands );
110p->timeGia += Abc_Clock() - clk;
111 return RetValue2;
112 }
113*/
114 p->nSatCalls++;
115 RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (ABC_INT64_T)p->pPars->nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
116// assert( RetValue == l_False || RetValue == l_True );
117
118 if ( RetValue != l_Undef && RetValue2 != -1 )
119 {
120 assert( (RetValue == l_False) == (RetValue2 == 1) );
121 }
122
123 if ( RetValue == l_False )
124 {
125 if ( fVeryVerbose )
126 printf( "U " );
127 return 1;
128 }
129 if ( RetValue != l_True )
130 {
131 if ( fVeryVerbose )
132 printf( "T " );
133 p->nTimeOuts++;
134 return -1;
135 }
136 if ( fVeryVerbose )
137 printf( "S " );
138 p->nSatCexes++;
139 // store the counter-example
140 Vec_IntForEachEntry( p->vProjVarsSat, iVar, i )
141 {
142 pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i );
143 if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!!
144 {
145 assert( Abc_InfoHasBit(pData, p->nCexes) );
146 Abc_InfoXorBit( pData, p->nCexes );
147 }
148 }
149 p->nCexes++;
150 return 0;
151
152}
l_True
#define l_True
Definition bmcBmcS.c:35
l_Undef
#define l_Undef
Definition bmcBmcS.c:34
l_False
#define l_False
Definition bmcBmcS.c:36
sat_solver_solve
#define sat_solver_solve
Definition cecSatG2.c:45
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the caller graph for this function:

◆ Abc_NtkMfsUpdateNetwork()

ABC_NAMESPACE_IMPL_START void Abc_NtkMfsUpdateNetwork ( Mfs_Man_t * p,
Abc_Obj_t * pObj,
Vec_Ptr_t * vMfsFanins,
Hop_Obj_t * pFunc )

DECLARATIONS ///.

CFile****************************************************************

FileName [mfsResub.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [The good old minimization with complete don't-cares.]

Synopsis [Procedures to perform resubstitution.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id
mfsResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

] FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Updates the network after resubstitution.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file mfsResub.c.

46{
47 Abc_Obj_t * pObjNew, * pFanin;
48 int k;
49 // create the new node
50 pObjNew = Abc_NtkCreateNode( pObj->pNtk );
51 pObjNew->pData = pFunc;
52 Vec_PtrForEachEntry( Abc_Obj_t *, vMfsFanins, pFanin, k )
53 Abc_ObjAddFanin( pObjNew, pFanin );
54 // replace the old node by the new node
55//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
56//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
57 // update the level of the node
58 Abc_NtkUpdate( pObj, pObjNew, p->vLevels );
59}
Abc_ObjAddFanin
ABC_DLL void Abc_ObjAddFanin(Abc_Obj_t *pObj, Abc_Obj_t *pFanin)
Definition abcFanio.c:84
Abc_NtkUpdate
ABC_DLL void Abc_NtkUpdate(Abc_Obj_t *pObj, Abc_Obj_t *pObjNew, Vec_Vec_t *vLevels)
Definition abcTiming.c:1423
Abc_Obj_t_::pData
void * pData
Definition abc.h:145
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition abc.h:130
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function: