Version abc81014

3 files changed, 12 insertions, 5 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index dc98adc9..e7cd0550 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -118,6 +118,8 @@ struct Fra_Sec_t_
     int              nFramesMax;        // the max number of frames used for induction
     int              nBTLimit;          // the conflict limit at a node
     int              nBTLimitGlobal;    // the global conflict limit
+    int              nBTLimitInter;     // the conflict limit for interpolation
+    int              nBddVarsMax;       // the state space limit for BDD reachability
     int              nBddMax;           // the max number of BDD nodes
     int              nBddIterMax;       // the limit on the number of BDD iterations
     int              fPhaseAbstract;    // enables phase abstraction
@@ -361,7 +363,7 @@ extern int                 Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld,
 extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSec.c ========================================================*/
 extern void                Fra_SecSetDefaultParams( Fra_Sec_t * p );
-extern int                 Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec );
+extern int                 Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult );
 /*=== fraSim.c ========================================================*/
 extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
 extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index f7674f7d..c8b35b28 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -32,7 +32,7 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Performs AIG rewriting on the constaint manager.]
+  Synopsis    [Performs AIG rewriting on the constraint manager.]
 
   Description []
                
@@ -536,7 +536,7 @@ p->timeTrav += clock() - clk2;
         // report the intermediate results
         if ( pPars->fVerbose )
         {
-            printf( "%3d : Const = %6d. Cl = %6d.  L = %6d. LR = %6d.  ", 
+            printf( "%3d : C = %6d. Cl = %6d.  L = %6d. LR = %6d.  ", 
                 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
                 Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
             if ( p->pCla->vImps )
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 216ed8df..cae37f85 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -51,6 +51,8 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
     p->nFramesMax        =       4;  // the max number of frames used for induction
     p->nBTLimit          =    1000;  // conflict limit at a node during induction 
     p->nBTLimitGlobal    = 5000000;  // global conflict limit during induction
+    p->nBTLimitInter     =   10000;  // conflict limit during interpolation
+    p->nBddVarsMax       =     150;  // the limit on the number of registers in BDD reachability
     p->nBddMax           =   50000;  // the limit on the number of BDD nodes 
     p->nBddIterMax       = 1000000;  // the limit on the number of BDD iterations
     p->fPhaseAbstract    =       0;  // enables phase abstraction
@@ -81,7 +83,7 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
+int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )
 {
     Ssw_Pars_t Pars2, * pPars2 = &Pars2;
     Fra_Ssw_t Pars, * pPars = &Pars;
@@ -461,6 +463,7 @@ clk = clock();
         int Depth;
 
         Inter_ManSetDefaultParams( pPars );
+        pPars->nBTLimit = pParSec->nBTLimitInter;
         pPars->fVerbose = pParSec->fVeryVerbose;
         if ( Saig_ManPoNum(pNew) == 1 )
         {
@@ -495,7 +498,7 @@ PRT( "Time", clock() - clk );
     }
 
     // try reachability analysis
-    if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < 150 )
+    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 );
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
@@ -563,6 +566,8 @@ PRT( "Time", clock() - clkTotal );
         FREE( pNew->pSeqModel );
         }
     }
+    if ( ppResult != NULL )
+        *ppResult = Aig_ManDupSimpleDfs( pNew );
     if ( pNew )
         Aig_ManStop( pNew );
     return RetValue;