Version abc90714

committer: Baruch Sterin <baruchs@gmail.com>

2 files changed, 71 insertions, 5 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index a2c10367..f661d2e5 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -128,13 +128,17 @@ struct Fra_Sec_t_
     int              fFraiging;         // enables fraiging at the beginning
     int              fInduction;        // enable the use of induction
     int              fInterpolation;    // enables interpolation
+    int              fInterSeparate;    // enables interpolation for each outputs separately
     int              fReachability;     // enables BDD based reachability
+    int              fReorderImage;     // enables BDD reordering during image computation
     int              fStopOnFirstFail;  // enables stopping after first output of a miter has failed to prove
     int              fUseNewProver;     // the new prover
     int              fSilent;           // disables all output
     int              fVerbose;          // enables verbose reporting of statistics
     int              fVeryVerbose;      // enables very verbose reporting  
     int              TimeLimit;         // enables the timeout
+    int              fReadUnsolved;     // inserts the unsolved model back
+    int              nSMnumber;         // the number of model written
     // internal parameters
     int              fRecursive;        // set to 1 when SEC is called recursively
     int              fReportSolution;   // enables report solution in a special form
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 8064d2ee..72af2466 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -61,7 +61,9 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
     p->fFraiging         =       1;  // enables fraiging at the beginning
     p->fInduction        =       1;  // enables the use of induction (signal correspondence)
     p->fInterpolation    =       1;  // enables interpolation
+    p->fInterSeparate    =       0;  // enables interpolation for each outputs separately
     p->fReachability     =       1;  // enables BDD based reachability
+    p->fReorderImage     =       0;  // enables variable reordering during image computation
     p->fStopOnFirstFail  =       1;  // enables stopping after first output of a miter has failed to prove
     p->fUseNewProver     =       0;  // enables new prover
     p->fSilent           =       0;  // disables all output
@@ -93,6 +95,7 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )
     int TimeOut = 0;
     int fLatchCorr = 0;
     float TimeLeft = 0.0;
+    pParSec->nSMnumber = -1;
 
     // try the miter before solving
     pNew = Aig_ManDupSimple( p );
@@ -466,14 +469,68 @@ clk = clock();
     {
         Inter_ManParams_t Pars, * pPars = &Pars;
         int Depth;
-
+        ABC_FREE( pNew->pSeqModel );
         Inter_ManSetDefaultParams( pPars );
+//        pPars->nBTLimit = 100;
         pPars->nBTLimit = pParSec->nBTLimitInter;
         pPars->fVerbose = pParSec->fVeryVerbose;
         if ( Saig_ManPoNum(pNew) == 1 )
         {
             RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
         }
+        else if ( pParSec->fInterSeparate )
+        {
+            Aig_Man_t * pTemp, * pAux;
+            Aig_Obj_t * pObjPo;
+            int i, Counter = 0;
+            Saig_ManForEachPo( pNew, pObjPo, i )
+            { 
+                if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pNew) )
+                    continue;
+                pTemp = Aig_ManDupOneOutput( pNew, i, 1 );
+                pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 );
+                Aig_ManStop( pAux );
+                if ( Saig_ManRegNum(pTemp) > 0 )
+                {
+                    RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth );
+                    if ( pTemp->pSeqModel )
+                    {
+                        Ssw_Cex_t * pCex;
+                        pCex = pNew->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+                        pCex->iPo = i;
+                        Aig_ManStop( pTemp );
+                        break;
+                    }
+                    // if solved, remove the output
+                    if ( RetValue == 1 )
+                    {
+                        Aig_ObjPatchFanin0( pNew, pObjPo, Aig_ManConst0(pNew) );
+    //                    printf( "Output %3d : Solved ", i );
+                    }
+                    else
+                    {
+                        Counter++;
+    //                    printf( "Output %3d : Undec  ", i );
+                    }
+                }
+                else
+                    Counter++;
+//                Aig_ManPrintStats( pTemp );
+                Aig_ManStop( pTemp );
+                printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pNew) );
+            }
+            Aig_ManCleanup( pNew );
+            if ( pNew->pSeqModel == NULL )
+            {
+                printf( "Interpolation left %d (out of %d) outputs unsolved              \n", Counter, Saig_ManPoNum(pNew) );
+                if ( Counter )
+                    RetValue = -1;
+            }
+            pNew = Aig_ManDupUnsolvedOutputs( pTemp = pNew, 1 );
+            Aig_ManStop( pTemp );
+            pNew = Aig_ManScl( pTemp = pNew, 1, 1, 0 );
+            Aig_ManStop( pTemp );
+        }
         else
         {
             Aig_Man_t * pNewOrpos = Said_ManDupOrpos( pNew );
@@ -481,7 +538,6 @@ clk = clock();
             if ( pNewOrpos->pSeqModel )
             {
                 Ssw_Cex_t * pCex;
-                ABC_FREE( pNew->pSeqModel );
                 pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
                 pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel );
             }
@@ -505,10 +561,10 @@ ABC_PRT( "Time", clock() - clk );
     // try reachability analysis
     if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < pParSec->nBddVarsMax )
     {
-        extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
+        extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-        RetValue = Aig_ManVerifyUsingBdds( pNew, pParSec->nBddMax, pParSec->nBddIterMax, 1, 1, 0, pParSec->fSilent );
+        RetValue = Aig_ManVerifyUsingBdds( pNew, pParSec->nBddMax, pParSec->nBddIterMax, 1, 1, pParSec->fReorderImage, 0, pParSec->fSilent );
     }
 
 finish:
@@ -541,6 +597,11 @@ ABC_PRT( "Time", clock() - clkTotal );
     }
     else 
     {
+        ///////////////////////////////////
+        // save intermediate result
+        extern void Abc_FrameSetSave1( void * pAig );
+        Abc_FrameSetSave1( Aig_ManDupSimple(pNew) );
+        ///////////////////////////////////
         if ( !pParSec->fSilent )
         {
             printf( "Networks are UNDECIDED.   " );
@@ -555,7 +616,8 @@ ABC_PRT( "Time", clock() - clkTotal );
         {
             static int Counter = 1;
             char pFileName[1000];
-            sprintf( pFileName, "sm%03d.aig", Counter++ );
+            pParSec->nSMnumber = Counter;
+            sprintf( pFileName, "sm%02d.aig", Counter++ );
             Ioa_WriteAiger( pNew, pFileName, 0, 0 );
             printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
         }