diff options
Diffstat (limited to 'src/proof/ssc')
| -rw-r--r-- | src/proof/ssc/sscCore.c | 16 | ||||
| -rw-r--r-- | src/proof/ssc/sscSat.c | 8 |
2 files changed, 17 insertions, 7 deletions
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c index d939a19a..aba5c80f 100644 --- a/src/proof/ssc/sscCore.c +++ b/src/proof/ssc/sscCore.c @@ -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 ); diff --git a/src/proof/ssc/sscSat.c b/src/proof/ssc/sscSat.c index 9992f18e..ca0933ec 100644 --- a/src/proof/ssc/sscSat.c +++ b/src/proof/ssc/sscSat.c @@ -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; |