luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Sweeper return value normalization.

This commit is contained in:
Alan Mishchenko 2013-11-01 11:19:23 -04:00
parent ec298486b6
commit e4ab09d771
4 changed files with 42 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
src/aig/gia/gia.h
View File

@ -984,6 +984,7 @@ extern Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis );
extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState );
extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex, int nFrames );
extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupZero( Gia_Man_t * p );
extern Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm );
extern Gia_Man_t * Gia_ManDupPermFlop( Gia_Man_t * p, Vec_Int_t * vFfPerm );
extern Gia_Man_t * Gia_ManDupPermFlopGap( Gia_Man_t * p, Vec_Int_t * vFfPerm );

24
src/aig/gia/giaDup.c
View File

@ -547,6 +547,30 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG without any changes.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManDupZero( Gia_Man_t * p )
{
Gia_Man_t * pNew; int i;
pNew = Gia_ManStart( 1 + Gia_ManCiNum(p) + Gia_ManCoNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
for ( i = 0; i < Gia_ManCiNum(p); i++ )
Gia_ManAppendCi( pNew );
for ( i = 0; i < Gia_ManCoNum(p); i++ )
Gia_ManAppendCo( pNew, 0 );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
/**Function*************************************************************
Synopsis [Duplicates AIG without any changes.]

16
src/proof/ssc/sscCore.c
View File

@ -90,16 +90,22 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
Ssc_ManStartSolver( p );
if ( p->pSat == NULL )
{
printf( "Constraints are UNSAT after propagation (likely a bug!).\n" );
printf( "Constraints are UNSAT after propagation.\n" );
Ssc_ManStop( p );
return NULL;
return (Ssc_Man_t *)(ABC_PTRINT_T)1;
}
// p->vPivot = Ssc_GiaFindPivotSim( p->pFraig );
// Vec_IntFreeP( &p->vPivot );
p->vPivot = Ssc_ManFindPivotSat( p );
if ( p->vPivot == (Vec_Int_t *)(ABC_PTRINT_T)1 )
{
printf( "Constraints are UNSAT.\n" );
Ssc_ManStop( p );
return (Ssc_Man_t *)(ABC_PTRINT_T)1;
}
if ( p->vPivot == NULL )
{
printf( "Constraints are UNSAT or conflict limit is too low.\n" );
printf( "Conflict limit is reached while trying to find one SAT assignment.\n" );
Ssc_ManStop( p );
return NULL;
}
@ -229,7 +235,9 @@ clk = Abc_Clock();
Gia_ManRandom( 1 );
// sweeping manager
p = Ssc_ManStart( pAig, pCare, pPars );
if ( p == NULL )
if ( p == (Ssc_Man_t *)(ABC_PTRINT_T)1 ) // UNSAT
return Gia_ManDupZero( pAig );
if ( p == NULL ) // timeout
return Gia_ManDup( pAig );
if ( p->pPars->fVerbose )
printf( "Care set produced %d hits out of %d.\n", Ssc_GiaEstimateCare(p->pFraig, 5), 640 );

8
src/proof/ssc/sscSat.c
View File

@ -323,10 +323,12 @@ void Ssc_ManCollectSatPattern( Ssc_Man_t * p, Vec_Int_t * vPattern )
Vec_Int_t * Ssc_ManFindPivotSat( Ssc_Man_t * p )
{
Vec_Int_t * vInit;
int status;
status = sat_solver_solve( p->pSat, NULL, NULL, p->pPars->nBTLimit, 0, 0, 0 );
if ( status != l_True ) // unsat or undec
int status = sat_solver_solve( p->pSat, NULL, NULL, p->pPars->nBTLimit, 0, 0, 0 );
if ( status == l_False )
return (Vec_Int_t *)(ABC_PTRINT_T)1;
if ( status == l_Undef )
return NULL;
assert( status == l_True );
vInit = Vec_IntAlloc( Gia_ManCiNum(p->pFraig) );
Ssc_ManCollectSatPattern( p, vInit );
return vInit;