Sweeper return value normalization.

4 files changed, 42 insertions, 7 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 36c53c71..9e82939d 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -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 );
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 3cef3f5b..30f9140d 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -558,6 +558,30 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p )
   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.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm )
 {
 //    Vec_Int_t * vPiPermInv;
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;