diff options
Diffstat (limited to 'src/opt/mfs')
-rw-r--r-- | src/opt/mfs/mfs.h | 4 | ||||
-rw-r--r-- | src/opt/mfs/mfsGia.c | 2 | ||||
-rw-r--r-- | src/opt/mfs/mfsInt.h | 19 | ||||
-rw-r--r-- | src/opt/mfs/mfsInter.c | 2 | ||||
-rw-r--r-- | src/opt/mfs/mfsMan.c | 2 | ||||
-rw-r--r-- | src/opt/mfs/mfsResub.c | 12 | ||||
-rw-r--r-- | src/opt/mfs/mfsSat.c | 6 | ||||
-rw-r--r-- | src/opt/mfs/mfsStrash.c | 2 |
8 files changed, 24 insertions, 25 deletions
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h index 02fcc21b..9916b582 100644 --- a/src/opt/mfs/mfs.h +++ b/src/opt/mfs/mfs.h @@ -18,8 +18,8 @@ ***********************************************************************/ -#ifndef __MFS_H__ -#define __MFS_H__ +#ifndef ABC__opt__mfs__mfs_h +#define ABC__opt__mfs__mfs_h //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/mfs/mfsGia.c b/src/opt/mfs/mfsGia.c index af6cc159..07c258ab 100644 --- a/src/opt/mfs/mfsGia.c +++ b/src/opt/mfs/mfsGia.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "mfsInt.h" -#include "giaAig.h" +#include "aig/gia/giaAig.h" ABC_NAMESPACE_IMPL_START diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h index 650a154a..fe154093 100644 --- a/src/opt/mfs/mfsInt.h +++ b/src/opt/mfs/mfsInt.h @@ -18,23 +18,22 @@ ***********************************************************************/ -#ifndef __MFS_INT_H__ -#define __MFS_INT_H__ +#ifndef ABC__opt__mfs__mfsInt_h +#define ABC__opt__mfs__mfsInt_h //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -#include "abc.h" -#include "extra.h" +#include "src/base/abc/abc.h" #include "mfs.h" -#include "aig.h" -#include "cnf.h" -#include "satSolver.h" -#include "satStore.h" -#include "bdc.h" -#include "gia.h" +#include "src/aig/aig/aig.h" +#include "src/sat/cnf/cnf.h" +#include "src/sat/bsat/satSolver.h" +#include "src/sat/bsat/satStore.h" +#include "src/bool/bdc/bdc.h" +#include "src/aig/gia/gia.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c index 0934513b..d18613c7 100644 --- a/src/opt/mfs/mfsInter.c +++ b/src/opt/mfs/mfsInter.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "mfsInt.h" -#include "kit.h" +#include "src/bool/kit/kit.h" ABC_NAMESPACE_IMPL_START diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c index df331b43..caa82e68 100644 --- a/src/opt/mfs/mfsMan.c +++ b/src/opt/mfs/mfsMan.c @@ -52,7 +52,7 @@ Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars ) p->vProjVarsCnf = Vec_IntAlloc( 100 ); p->vProjVarsSat = Vec_IntAlloc( 100 ); p->vDivLits = Vec_IntAlloc( 100 ); - p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX); + p->nDivWords = Abc_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX); p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords ); p->pMan = Int_ManAlloc(); p->vMem = Vec_IntAlloc( 0 ); diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index 40cb6198..45f75674 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -142,8 +142,8 @@ p->timeGia += clock() - clk; pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); if ( !sat_solver_var_value( p->pSat, iVar ) ) // remove 0s!!! { - assert( Aig_InfoHasBit(pData, p->nCexes) ); - Aig_InfoXorBit( pData, p->nCexes ); + assert( Abc_InfoHasBit(pData, p->nCexes) ); + Abc_InfoXorBit( pData, p->nCexes ); } } p->nCexes++; @@ -242,13 +242,13 @@ p->timeInt += clock() - clk; for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ ) { pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); - printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) ); + printf( "%d", Abc_InfoHasBit(pData, p->nCexes-1) ); } printf( "\n" ); } // find the next divisor to try - nWords = Aig_BitWordNum(p->nCexes); + nWords = Abc_BitWordNum(p->nCexes); assert( nWords <= p->nDivWords ); for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ ) { @@ -387,13 +387,13 @@ p->timeInt += clock() - clk; for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ ) { pData = (unsigned *)Vec_PtrEntry( p->vDivCexes, i ); - printf( "%d", Aig_InfoHasBit(pData, p->nCexes-1) ); + printf( "%d", Abc_InfoHasBit(pData, p->nCexes-1) ); } printf( "\n" ); } // find the next divisor to try - nWords = Aig_BitWordNum(p->nCexes); + nWords = Abc_BitWordNum(p->nCexes); assert( nWords <= p->nDivWords ); fBreak = 0; for ( iVar = 1; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ ) diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c index 37ee2b39..e5e9de1a 100644 --- a/src/opt/mfs/mfsSat.c +++ b/src/opt/mfs/mfsSat.c @@ -72,8 +72,8 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p ) Lits[b] = lit_neg( Lits[b] ); } } - assert( !Aig_InfoHasBit(p->uCare, Mint) ); - Aig_InfoSetBit( p->uCare, Mint ); + assert( !Abc_InfoHasBit(p->uCare, Mint) ); + Abc_InfoSetBit( p->uCare, Mint ); // add the blocking clause RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVarsSat) ); if ( RetValue == 0 ) @@ -106,7 +106,7 @@ int Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode ) // prepare the truth table of care set p->nFanins = Vec_IntSize( p->vProjVarsSat ); - p->nWords = Aig_TruthWordNum( p->nFanins ); + p->nWords = Abc_TruthWordNum( p->nFanins ); memset( p->uCare, 0, sizeof(unsigned) * p->nWords ); // iterate through the SAT assignments diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c index a5c7b987..922af3a8 100644 --- a/src/opt/mfs/mfsStrash.c +++ b/src/opt/mfs/mfsStrash.c @@ -367,7 +367,7 @@ Aig_Man_t * Abc_NtkAigForConstraints( Mfs_Man_t * p, Abc_Obj_t * pNode ) ABC_NAMESPACE_IMPL_END -#include "fra.h" +#include "src/proof/fra/fra.h" ABC_NAMESPACE_IMPL_START |