diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-25 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2008-07-25 08:01:00 -0700 |
| commit | 1afa8a2f38bacb9f2f8faaf06b4f01c70560a419 (patch) | |
| tree | 8aa41b5eea9d26befaf1604e8cc6c61b59eaef1b /src/base/abci/abcDar.c | |
| parent | 2c96c8af36446d3b855e07d78975cfad50c2917c (diff) | |
| download | abc-1afa8a2f38bacb9f2f8faaf06b4f01c70560a419.tar.gz abc-1afa8a2f38bacb9f2f8faaf06b4f01c70560a419.tar.bz2 abc-1afa8a2f38bacb9f2f8faaf06b4f01c70560a419.zip | |
Version abc80725
Diffstat (limited to 'src/base/abci/abcDar.c')
| -rw-r--r-- | src/base/abci/abcDar.c | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 03790c4b..71f84272 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -25,6 +25,7 @@ #include "cnf.h" #include "fra.h" #include "fraig.h" +#include "int.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -1295,7 +1296,7 @@ PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose ) +int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars ) { Aig_Man_t * pMan; int RetValue, Depth, clk = clock(); @@ -1307,7 +1308,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fR return -1; } assert( pMan->nRegs > 0 ); - RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose, &Depth ); + RetValue = Inter_ManPerformInterpolation( pMan, pPars, &Depth ); if ( RetValue == 1 ) printf( "Property proved. " ); else if ( RetValue == 0 ) |