diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-21 04:30:10 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-01-21 04:30:10 -0800 |
| commit | 8014f25f6db719fa62336f997963532a14c568f6 (patch) | |
| tree | c691ee91a3a2d452a2bd24ac89a8c717beaa7af7 /src/aig/saig/saigBmc3.c | |
| parent | c44cc5de9429e6b4f1c05045fcf43c9cb96437b5 (diff) | |
| download | abc-8014f25f6db719fa62336f997963532a14c568f6.tar.gz abc-8014f25f6db719fa62336f997963532a14c568f6.tar.bz2 abc-8014f25f6db719fa62336f997963532a14c568f6.zip | |
Major restructuring of the code.
Diffstat (limited to 'src/aig/saig/saigBmc3.c')
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 2035ac72..27393f32 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -19,9 +19,9 @@ ***********************************************************************/ #include "saig.h" -#include "fra.h" -#include "cnf.h" -#include "satStore.h" +#include "src/proof/fra/fra.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satStore.h" ABC_NAMESPACE_IMPL_START @@ -130,7 +130,7 @@ unsigned * Saig_ManBmcTerSimOne( Aig_Man_t * p, unsigned * pPrev ) Aig_Obj_t * pObj, * pObjLi; unsigned * pInfo; int i, Val0, Val1; - pInfo = ABC_CALLOC( unsigned, Aig_BitWordNum(2 * Aig_ManObjNumMax(p)) ); + pInfo = ABC_CALLOC( unsigned, Abc_BitWordNum(2 * Aig_ManObjNumMax(p)) ); Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(p), SAIG_TER_ONE ); Saig_ManForEachPi( p, pObj, i ) Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND ); @@ -1105,7 +1105,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) Gia_ManBmc_t * p; Aig_Obj_t * pObj; int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0; - int nOutDigits = Aig_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); + int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock(); int nTimeToStop = time(NULL) + pPars->nTimeOut; if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 ) |