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

Go to the source code of this file.

Functions

void Min_SopMinimize (Min_Man_t *p)
 FUNCTION DEFINITIONS ///.
 
int Min_SopAddCubeInt (Min_Man_t *p, Min_Cube_t *pCube)
 
void Min_SopAddCube (Min_Man_t *p, Min_Cube_t *pCube)
 
void Min_SopContain (Min_Man_t *p)
 
void Min_SopDist1Merge (Min_Man_t *p)
 
Min_Cube_t * Min_SopComplement (Min_Man_t *p, Min_Cube_t *pSharp)
 
int Min_SopCheck (Min_Man_t *p)
 

Function Documentation

◆ Min_SopAddCube()

void Min_SopAddCube ( Min_Man_t * p,
Min_Cube_t * pCube )

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

Synopsis [Adds the cube to storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 433 of file covMinSop.c.

434{
435 assert( Min_CubeCheck( pCube ) );
436 assert( pCube != p->pBubble );
437 assert( (int)pCube->nLits == Min_CubeCountLits(pCube) );
438 while ( Min_SopAddCubeInt( p, pCube ) );
439}
Min_CubeCheck
int Min_CubeCheck(Min_Cube_t *pCube)
Definition covMinUtil.c:244
Min_SopAddCubeInt
int Min_SopAddCubeInt(Min_Man_t *p, Min_Cube_t *pCube)
Definition covMinSop.c:361
p
Cube * p
Definition exorList.c:222
Min_Cube_t_::nLits
unsigned nLits
Definition covInt.h:59
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:

◆ Min_SopAddCubeInt()

int Min_SopAddCubeInt ( Min_Man_t * p,
Min_Cube_t * pCube )

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

Synopsis [Adds cube to the SOP cover stored in the manager.]

Description [Returns 0 if the cube is added or removed. Returns 1 if the cube is glued with some other cube and has to be added again.]

SideEffects []

SeeAlso []

Definition at line 361 of file covMinSop.c.

362{
363 Min_Cube_t * pThis, * pThis2, ** ppPrev;
364 int i;
365 // try to find the identical cube
366 Min_CoverForEachCube( p->ppStore[pCube->nLits], pThis )
367 {
368 if ( Min_CubesAreEqual( pCube, pThis ) )
369 {
370 Min_CubeRecycle( p, pCube );
371 return 0;
372 }
373 }
374 // try to find a containing cube
375 for ( i = 0; i < (int)pCube->nLits; i++ )
376 Min_CoverForEachCube( p->ppStore[i], pThis )
377 {
378 if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
379 {
380 Min_CubeRecycle( p, pCube );
381 return 0;
382 }
383 }
384 // try to find distance one in the same bin
385 Min_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev )
386 {
387 if ( Min_CubesDistOne( pCube, pThis, NULL ) )
388 {
389 *ppPrev = pThis->pNext;
390 Min_CubesTransformOr( pCube, pThis );
391 pCube->nLits--;
392 Min_CubeRecycle( p, pThis );
393 p->nCubes--;
394 return 1;
395 }
396 }
397
398 // clean the other cubes using this one
399 for ( i = pCube->nLits + 1; i <= (int)pCube->nVars; i++ )
400 {
401 ppPrev = &p->ppStore[i];
402 Min_CoverForEachCubeSafe( p->ppStore[i], pThis, pThis2 )
403 {
404 if ( pThis != p->pBubble && Min_CubeIsContained( pCube, pThis ) )
405 {
406 *ppPrev = pThis->pNext;
407 Min_CubeRecycle( p, pThis );
408 p->nCubes--;
409 }
410 else
411 ppPrev = &pThis->pNext;
412 }
413 }
414
415 // add the cube
416 pCube->pNext = p->ppStore[pCube->nLits];
417 p->ppStore[pCube->nLits] = pCube;
418 p->nCubes++;
419 return 0;
420}
Min_Cube_t
struct Min_Cube_t_ Min_Cube_t
Definition covInt.h:35
Min_CoverForEachCube
#define Min_CoverForEachCube(pCover, pCube)
Definition covInt.h:65
Min_CoverForEachCubePrev
#define Min_CoverForEachCubePrev(pCover, pCube, ppPrev)
Definition covInt.h:75
Min_CoverForEachCubeSafe
#define Min_CoverForEachCubeSafe(pCover, pCube, pCube2)
Definition covInt.h:69
Min_Cube_t_::nVars
unsigned nVars
Definition covInt.h:57
Min_Cube_t_::pNext
Min_Cube_t * pNext
Definition covInt.h:56
Here is the caller graph for this function:

◆ Min_SopCheck()

int Min_SopCheck ( Min_Man_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 585 of file covMinSop.c.

586{
587 Min_Cube_t * pCube, * pThis;
588 int i;
589
590 pCube = Min_CubeAlloc( p );
591 Min_CubeXorBit( pCube, 2*0+1 );
592 Min_CubeXorBit( pCube, 2*1+1 );
593 Min_CubeXorBit( pCube, 2*2+0 );
594 Min_CubeXorBit( pCube, 2*3+0 );
595 Min_CubeXorBit( pCube, 2*4+0 );
596 Min_CubeXorBit( pCube, 2*5+1 );
597 Min_CubeXorBit( pCube, 2*6+1 );
598 pCube->nLits = 7;
599
600// Min_CubeWrite( stdout, pCube );
601
602 // check that the cubes contain it
603 for ( i = 0; i <= p->nVars; i++ )
604 Min_CoverForEachCube( p->ppStore[i], pThis )
605 if ( pThis != p->pBubble && Min_CubeIsContained( pThis, pCube ) )
606 {
607 Min_CubeRecycle( p, pCube );
608 return 1;
609 }
610 Min_CubeRecycle( p, pCube );
611 return 0;
612}

◆ Min_SopComplement()

Min_Cube_t * Min_SopComplement ( Min_Man_t * p,
Min_Cube_t * pSharp )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 526 of file covMinSop.c.

527{
528 Vec_Int_t * vVars;
529 Min_Cube_t * pCover, * pCube, * pNext, * pReady, * pThis, ** ppPrev;
530 int Num, Value, i;
531
532 // get the variables
533 vVars = Vec_IntAlloc( 100 );
534 // create the tautology cube
535 pCover = Min_CubeAlloc( p );
536 // sharp it with all cubes
537 Min_CoverForEachCube( pSharp, pCube )
538 Min_CoverForEachCubePrev( pCover, pThis, ppPrev )
539 {
540 if ( Min_CubesDisjoint( pThis, pCube ) )
541 continue;
542 // remember the next pointer
543 pNext = pThis->pNext;
544 // get the variables, in which pThis is '-' while pCube is fixed
545 Min_CoverGetDisjVars( pThis, pCube, vVars );
546 // generate the disjoint cubes
547 pReady = pThis;
548 Vec_IntForEachEntryReverse( vVars, Num, i )
549 {
550 // correct the literal
551 Min_CubeXorVar( pReady, vVars->pArray[i], 3 );
552 if ( i == 0 )
553 break;
554 // create the new cube and clean this value
555 Value = Min_CubeGetVar( pReady, vVars->pArray[i] );
556 pReady = Min_CubeDup( p, pReady );
557 Min_CubeXorVar( pReady, vVars->pArray[i], 3 ^ Value );
558 // add to the cover
559 *ppPrev = pReady;
560 ppPrev = &pReady->pNext;
561 }
562 pThis = pReady;
563 pThis->pNext = pNext;
564 }
565 Vec_IntFree( vVars );
566
567 // perform dist-1 merge and contain
568 Min_CoverExpandRemoveEqual( p, pCover );
569 Min_SopDist1Merge( p );
570 Min_SopContain( p );
571 return Min_CoverCollect( p, p->nVars );
572}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Min_CoverCollect
Min_Cube_t * Min_CoverCollect(Min_Man_t *p, int nSuppSize)
Definition covMinUtil.c:264
Min_SopContain
void Min_SopContain(Min_Man_t *p)
Definition covMinSop.c:456
Min_SopDist1Merge
void Min_SopDist1Merge(Min_Man_t *p)
Definition covMinSop.c:494
Vec_IntForEachEntryReverse
#define Vec_IntForEachEntryReverse(vVec, pEntry, i)
Definition vecInt.h:62
Here is the call graph for this function:

◆ Min_SopContain()

void Min_SopContain ( Min_Man_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 456 of file covMinSop.c.

457{
458 Min_Cube_t * pCube, * pCube2, ** ppPrev;
459 int i, k;
460 for ( i = 0; i <= p->nVars; i++ )
461 {
462 Min_CoverForEachCube( p->ppStore[i], pCube )
463 Min_CoverForEachCubePrev( pCube->pNext, pCube2, ppPrev )
464 {
465 if ( !Min_CubesAreEqual( pCube, pCube2 ) )
466 continue;
467 *ppPrev = pCube2->pNext;
468 Min_CubeRecycle( p, pCube2 );
469 p->nCubes--;
470 }
471 for ( k = i + 1; k <= p->nVars; k++ )
472 Min_CoverForEachCubePrev( p->ppStore[k], pCube2, ppPrev )
473 {
474 if ( !Min_CubeIsContained( pCube, pCube2 ) )
475 continue;
476 *ppPrev = pCube2->pNext;
477 Min_CubeRecycle( p, pCube2 );
478 p->nCubes--;
479 }
480 }
481}
Here is the caller graph for this function:

◆ Min_SopDist1Merge()

void Min_SopDist1Merge ( Min_Man_t * p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 494 of file covMinSop.c.

495{
496 Min_Cube_t * pCube, * pCube2, * pCubeNew;
497 int i;
498 for ( i = p->nVars; i >= 0; i-- )
499 {
500 Min_CoverForEachCube( p->ppStore[i], pCube )
501 Min_CoverForEachCube( pCube->pNext, pCube2 )
502 {
503 assert( pCube->nLits == pCube2->nLits );
504 if ( !Min_CubesDistOne( pCube, pCube2, NULL ) )
505 continue;
506 pCubeNew = Min_CubesXor( p, pCube, pCube2 );
507 assert( pCubeNew->nLits == pCube->nLits - 1 );
508 pCubeNew->pNext = p->ppStore[pCubeNew->nLits];
509 p->ppStore[pCubeNew->nLits] = pCubeNew;
510 p->nCubes++;
511 }
512 }
513}
Here is the caller graph for this function:

◆ Min_SopMinimize()

void Min_SopMinimize ( Min_Man_t * p)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file covMinSop.c.

48{
49 int nCubesInit, nCubesOld, nIter;
50 if ( p->nCubes < 3 )
51 return;
52 nIter = 0;
53 nCubesInit = p->nCubes;
54 do {
55 nCubesOld = p->nCubes;
56 Min_SopRewrite( p );
57 nIter++;
58// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes );
59 }
60 while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 );
61// printf( "\n" );
62
63}
Here is the caller graph for this function: