Multi-output property solver.

1 files changed, 44 insertions, 38 deletions

diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 4fbf7c70..d662f376 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2138,56 +2138,62 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
     ABC_FREE( pNtk->pModel );
     ABC_FREE( pNtk->pSeqModel );
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
-    if ( RetValue == 1 )
-    {
-        Abc_Print( 1, "Explored all reachable states after completing %d frames.  ", 1<<Aig_ManRegNum(pMan) );
-    }
-    else if ( RetValue == -1 )
+    if ( !pPars->fSilent )
     {
-        if ( pPars->nFailOuts == 0 )
+        if ( RetValue == 1 )
         {
-            Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) );
-            if ( nTimeOut && Abc_Clock() > nTimeOut )
-                Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
-            else
-                Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
+            Abc_Print( 1, "Explored all reachable states after completing %d frames.  ", 1<<Aig_ManRegNum(pMan) );
         }
-        else
+        else if ( RetValue == -1 )
         {
-            Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
-            if ( Abc_Clock() > nTimeOut )
-                Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
+            if ( pPars->nFailOuts == 0 )
+            {
+                Abc_Print( 1, "No output asserted in %d frames. Resource limit reached ", Abc_MaxInt(pPars->iFrame,0) );
+                if ( nTimeOut && Abc_Clock() > nTimeOut )
+                    Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
+                else
+                    Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
+            }
             else
-                Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
-        }
-    }
-    else // if ( RetValue == 0 )
-    {
-        if ( !pPars->fSolveAll )
-        {
-            Abc_Cex_t * pCex = pNtk->pSeqModel;
-            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
+            {
+                Abc_Print( 1, "The total of %d outputs asserted in %d frames. Resource limit reached ", pPars->nFailOuts, pPars->iFrame );
+                if ( Abc_Clock() > nTimeOut )
+                    Abc_Print( 1, "(timeout %d sec). ", pPars->nTimeOut );
+                else
+                    Abc_Print( 1, "(conf limit %d). ", pPars->nConfLimit );
+            }
         }
-        else
+        else // if ( RetValue == 0 )
         {
-            int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
-            if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
-                Abc_Print( 1, "None of the %d outputs is found to be SAT.   ", nOutputs );
-            else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
-                Abc_Print( 1, "All %d outputs are found to be SAT.   ", nOutputs );
+            if ( !pPars->fSolveAll )
+            {
+                Abc_Cex_t * pCex = pNtk->pSeqModel;
+                Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", pCex->iPo, pNtk->pName, pCex->iFrame );
+            }
             else
             {
-                Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
-                if ( pPars->nDropOuts )
-                    Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
-                Abc_Print( 1, ".   " );
+                int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
+                if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
+                    Abc_Print( 1, "None of the %d outputs is found to be SAT.   ", nOutputs );
+                else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
+                    Abc_Print( 1, "All %d outputs are found to be SAT.   ", nOutputs );
+                else
+                {
+                    Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
+                    if ( pPars->nDropOuts )
+                        Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
+                    Abc_Print( 1, ".   " );
+                }
             }
-            if ( pNtk->vSeqModelVec )
-                Vec_PtrFreeFree( pNtk->vSeqModelVec );
-            pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
         }
+        ABC_PRT( "Time", Abc_Clock() - clk );
+    }
+    if ( RetValue == 0 && pPars->fSolveAll )
+    {
+        if ( pNtk->vSeqModelVec )
+            Vec_PtrFreeFree( pNtk->vSeqModelVec );
+        pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
     }
-    ABC_PRT( "Time", Abc_Clock() - clk );
     if ( pNtk->pSeqModel ) 
     {
         status = Saig_ManVerifyCex( pMan, pNtk->pSeqModel );