diff options
53 files changed, 248 insertions, 262 deletions
@@ -15,22 +15,21 @@ MODULES := \ $(wildcard src/ext*) \ src/base/abc src/base/abci src/base/cmd src/base/io src/base/main \ src/base/ver src/base/wlc src/base/bac src/base/cba src/base/pla src/base/test \ - src/bdd/cudd src/bdd/dsd src/bdd/epd src/bdd/mtr src/bdd/parse \ - src/bdd/reo src/bdd/cas \ + src/bdd/cudd src/bdd/extrab src/bdd/dsd src/bdd/epd src/bdd/mtr \ + src/bdd/reo src/bdd/cas src/bdd/bbr src/bdd/llb \ src/map/mapper src/map/mio src/map/super src/map/if \ src/map/amap src/map/cov src/map/scl src/map/mpm \ src/misc/extra src/misc/mvc src/misc/st src/misc/util src/misc/nm \ src/misc/vec src/misc/hash src/misc/tim src/misc/bzlib src/misc/zlib \ - src/misc/mem src/misc/bar src/misc/bbl \ + src/misc/mem src/misc/bar src/misc/bbl src/misc/parse \ src/opt/cut src/opt/fxu src/opt/rwr src/opt/mfs src/opt/sim \ src/opt/ret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \ src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/sfm \ src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \ src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky \ src/bool/rsb src/bool/rpo \ - src/proof/pdr src/proof/abs src/proof/bbr src/proof/llb src/proof/live \ + src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \ src/proof/cec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \ - src/proof/ssc src/proof/int \ src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \ src/aig/miniaig \ src/python @@ -1242,30 +1242,6 @@ SOURCE=.\src\bdd\mtr\mtrGroup.c SOURCE=.\src\bdd\mtr\mtrInt.h # End Source File # End Group -# Begin Group "parse" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\bdd\parse\parse.h -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\parse\parseCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\parse\parseEqn.c -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\parse\parseInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\bdd\parse\parseStack.c -# End Source File -# End Group # Begin Group "dsd" # PROP Default_Filter "" @@ -1362,6 +1338,178 @@ SOURCE=.\src\bdd\cas\casCore.c SOURCE=.\src\bdd\cas\casDec.c # End Source File # End Group +# Begin Group "bbr" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\bdd\bbr\bbr.h +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\bbr\bbrCex.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\bbr\bbrImage.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\bbr\bbrNtbdd.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\bbr\bbrReach.c +# End Source File +# End Group +# Begin Group "llb" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\bdd\llb\llb.h +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb1Cluster.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb1Constr.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb1Core.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb1Group.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb1Hint.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb1Man.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb1Matrix.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb1Pivot.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb1Reach.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb1Sched.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb2Bad.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb2Core.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb2Driver.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb2Dump.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb2Flow.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb2Image.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb3Image.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb3Nonlin.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb4Cex.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb4Cluster.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb4Image.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb4Map.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb4Nonlin.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llb4Sweep.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\llb\llbInt.h +# End Source File +# End Group +# Begin Group "extrab" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\bdd\extrab\extraBdd.h +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\extrab\extraBddAuto.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\extrab\extraBddCas.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\extrab\extraBddImage.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\extrab\extraBddKmap.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\extrab\extraBddMisc.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\extrab\extraBddSymm.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\extrab\extraBddTime.c +# End Source File +# Begin Source File + +SOURCE=.\src\bdd\extrab\extraBddUnate.c +# End Source File +# End Group # End Group # Begin Group "sat" @@ -2899,42 +3047,6 @@ SOURCE=.\src\misc\extra\extra.h # End Source File # Begin Source File -SOURCE=.\src\misc\extra\extraBdd.h -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddAuto.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddCas.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddImage.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddKmap.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddMisc.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddSymm.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddTime.c -# End Source File -# Begin Source File - -SOURCE=.\src\misc\extra\extraBddUnate.c -# End Source File -# Begin Source File - SOURCE=.\src\misc\extra\extraUtilBitMatrix.c # End Source File # Begin Source File @@ -3486,6 +3598,22 @@ SOURCE=.\src\misc\tim\timTime.c SOURCE=.\src\misc\tim\timTrav.c # End Source File # End Group +# Begin Group "parse" + +# PROP Default_Filter "" +# Begin Source File + +SOURCE=.\src\misc\parse\parseEqn.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\parse\parseInt.h +# End Source File +# Begin Source File + +SOURCE=.\src\misc\parse\parseStack.c +# End Source File +# End Group # End Group # Begin Group "ai" @@ -4438,30 +4566,6 @@ SOURCE=.\src\bool\rpo\rpo.h # Begin Group "prove" # PROP Default_Filter "" -# Begin Group "bbr" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\proof\bbr\bbr.h -# End Source File -# Begin Source File - -SOURCE=.\src\proof\bbr\bbrCex.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\bbr\bbrImage.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\bbr\bbrNtbdd.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\bbr\bbrReach.c -# End Source File -# End Group # Begin Group "cec" # PROP Default_Filter "" @@ -4810,118 +4914,6 @@ SOURCE=.\src\proof\live\ltl_parser.c SOURCE=.\src\proof\live\monotone.c # End Source File # End Group -# Begin Group "llb" - -# PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\proof\llb\llb.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb.h -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb1Cluster.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb1Constr.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb1Core.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb1Group.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb1Hint.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb1Man.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb1Matrix.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb1Pivot.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb1Reach.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb1Sched.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb2Bad.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb2Core.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb2Driver.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb2Dump.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb2Flow.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb2Image.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb3Image.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb3Nonlin.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb4Cex.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb4Cluster.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb4Image.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb4Map.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb4Nonlin.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llb4Sweep.c -# End Source File -# Begin Source File - -SOURCE=.\src\proof\llb\llbInt.h -# End Source File -# End Group # Begin Group "pdr" # PROP Default_Filter "" diff --git a/src/aig/aig/aigSplit.c b/src/aig/aig/aigSplit.c index 33b353a5..9e74d1be 100644 --- a/src/aig/aig/aigSplit.c +++ b/src/aig/aig/aigSplit.c @@ -22,7 +22,7 @@ #include "aig/saig/saig.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/aig/gia/giaClp.c b/src/aig/gia/giaClp.c index d67c57eb..68f9bf56 100644 --- a/src/aig/gia/giaClp.c +++ b/src/aig/gia/giaClp.c @@ -21,7 +21,7 @@ #include "gia.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #include "bdd/dsd/dsd.h" #endif diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index dabdf539..dfeb2e43 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -586,6 +586,11 @@ Aig_Man_t * Saig_ManDupCones( Aig_Man_t * pAig, int * pPos, int nPos ) } +#ifdef ABC_USE_CUDD +int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars ) { return 0; } +void Bbr_ManSetDefaultParams( Saig_ParBbr_t * p ) {} +#endif + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcBlifMv.c b/src/base/abc/abcBlifMv.c index 30602be1..8c9b2a70 100644 --- a/src/base/abc/abcBlifMv.c +++ b/src/base/abc/abcBlifMv.c @@ -21,7 +21,7 @@ #include "abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index 53baa905..3e978bf0 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -22,7 +22,7 @@ #include "base/main/main.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c index a8fb352d..9799ee93 100644 --- a/src/base/abc/abcFunc.c +++ b/src/base/abc/abcFunc.c @@ -23,7 +23,7 @@ #include "map/mio/mio.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c index 1edeb049..d30c7051 100644 --- a/src/base/abc/abcLatch.c +++ b/src/base/abc/abcLatch.c @@ -21,7 +21,7 @@ #include "abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abc/abcMinBase.c b/src/base/abc/abcMinBase.c index b7ee005c..22d1e285 100644 --- a/src/base/abc/abcMinBase.c +++ b/src/base/abc/abcMinBase.c @@ -21,7 +21,7 @@ #include "abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index d66bb393..1b38f157 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -25,7 +25,7 @@ #include "aig/gia/gia.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index c6e78c68..533f1f73 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -24,7 +24,7 @@ #include "map/mio/mio.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c index 9753eef1..13dd9346 100644 --- a/src/base/abc/abcShow.c +++ b/src/base/abc/abcShow.c @@ -30,7 +30,7 @@ #include "base/io/ioAbc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 706201cb..158934d3 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -25,7 +25,7 @@ #include "opt/fxu/fxu.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5d707a80..bf419016 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -45,8 +45,8 @@ #include "proof/cec/cec.h" #include "proof/pdr/pdr.h" #include "misc/tim/tim.h" -#include "proof/llb/llb.h" -#include "proof/bbr/bbr.h" +#include "bdd/llb/llb.h" +#include "bdd/bbr/bbr.h" #include "map/cov/cov.h" #include "base/cmd/cmd.h" #include "proof/abs/abs.h" diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c index 5f02b6d2..18c92657 100644 --- a/src/base/abci/abcAuto.c +++ b/src/base/abci/abcAuto.c @@ -21,7 +21,7 @@ #include "base/abc/abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcBm.c b/src/base/abci/abcBm.c index ce1582dd..860b4d27 100644 --- a/src/base/abci/abcBm.c +++ b/src/base/abci/abcBm.c @@ -30,7 +30,7 @@ #include "base/abc/abc.h" #include "opt/sim/sim.h" #include "sat/bsat/satSolver.h" -//#include "misc/extra/extraBdd.h" +//#include "bdd/extrab/extraBdd.h" ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcCas.c b/src/base/abci/abcCas.c index 17aa99cb..9abdd792 100644 --- a/src/base/abci/abcCas.c +++ b/src/base/abci/abcCas.c @@ -21,7 +21,7 @@ #include "base/abc/abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcCascade.c b/src/base/abci/abcCascade.c index 9ba10c34..70f2e891 100644 --- a/src/base/abci/abcCascade.c +++ b/src/base/abci/abcCascade.c @@ -22,7 +22,7 @@ #ifdef ABC_USE_CUDD #include "bdd/reo/reo.h" -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c index cc3d74c2..e0f80c60 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcCollapse.c @@ -21,7 +21,7 @@ #include "base/abc/abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 523d6817..06592a64 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -29,7 +29,7 @@ #include "proof/dch/dch.h" #include "proof/ssw/ssw.h" #include "opt/cgt/cgt.h" -#include "proof/bbr/bbr.h" +#include "bdd/bbr/bbr.h" #include "aig/gia/gia.h" #include "proof/cec/cec.h" #include "opt/csw/csw.h" diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c index 44475cca..9104c4d6 100644 --- a/src/base/abci/abcDsd.c +++ b/src/base/abci/abcDsd.c @@ -21,7 +21,7 @@ #include "base/abc/abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #include "bdd/dsd/dsd.h" #endif diff --git a/src/base/abci/abcFpga.c b/src/base/abci/abcFpga.c index a9c3baee..a5a380a1 100644 --- a/src/base/abci/abcFpga.c +++ b/src/base/abci/abcFpga.c @@ -22,7 +22,7 @@ #include "map/fpga/fpgaInt.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 94b339bc..59481d3e 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -27,7 +27,7 @@ #include "aig/aig/aig.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcLutmin.c b/src/base/abci/abcLutmin.c index 219f2357..ad686299 100644 --- a/src/base/abci/abcLutmin.c +++ b/src/base/abci/abcLutmin.c @@ -21,7 +21,7 @@ #include "base/abc/abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcMulti.c b/src/base/abci/abcMulti.c index 53e4005a..a3abee89 100644 --- a/src/base/abci/abcMulti.c +++ b/src/base/abci/abcMulti.c @@ -21,7 +21,7 @@ #include "base/abc/abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcMv.c b/src/base/abci/abcMv.c index 3f597fcd..eb71b9cd 100644 --- a/src/base/abci/abcMv.c +++ b/src/base/abci/abcMv.c @@ -21,7 +21,7 @@ #include "base/abc/abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index 112cceb9..0225d800 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -22,7 +22,7 @@ #include "aig/saig/saig.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START @@ -607,8 +607,6 @@ ABC_PRT( "Time", Abc_Clock() - clk ); double Abc_NtkSpacePercentage( Abc_Obj_t * pNode ) { return 0.0; } Abc_Ntk_t * Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk ) { return NULL; } -int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars ) { return 0; } -void Bbr_ManSetDefaultParams( Saig_ParBbr_t * p ) {} #endif diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index cab24877..3d2c2551 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -27,7 +27,7 @@ #include "map/if/if.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif #ifdef WIN32 diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c index 4be3a398..c31e9d94 100644 --- a/src/base/abci/abcProve.c +++ b/src/base/abci/abcProve.c @@ -24,7 +24,7 @@ #include "proof/fraig/fraig.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcReach.c b/src/base/abci/abcReach.c index 97ee158f..908b16be 100644 --- a/src/base/abci/abcReach.c +++ b/src/base/abci/abcReach.c @@ -21,7 +21,7 @@ #include "base/abc/abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c index f13930bb..483234dd 100644 --- a/src/base/abci/abcReconv.c +++ b/src/base/abci/abcReconv.c @@ -21,7 +21,7 @@ #include "base/abc/abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c index 8ff1d470..af01dde7 100644 --- a/src/base/abci/abcRefactor.c +++ b/src/base/abci/abcRefactor.c @@ -22,7 +22,7 @@ #include "bool/dec/dec.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c index 5995f36d..df4c69e0 100644 --- a/src/base/abci/abcRenode.c +++ b/src/base/abci/abcRenode.c @@ -23,7 +23,7 @@ #include "bool/kit/kit.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #include "bdd/reo/reo.h" #endif diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c index 87ba3712..ef5dd451 100644 --- a/src/base/abci/abcRestruct.c +++ b/src/base/abci/abcRestruct.c @@ -23,7 +23,7 @@ #include "opt/cut/cut.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #include "bdd/dsd/dsd.h" #endif diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index e2b8864c..bc956e5e 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -24,7 +24,7 @@ #include "sat/bsat/satSolver.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index 49450e99..e970ac38 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -23,7 +23,7 @@ #include "proof/fraig/fraig.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c index 224c3968..096c3ae4 100644 --- a/src/base/abci/abcSymm.c +++ b/src/base/abci/abcSymm.c @@ -22,7 +22,7 @@ #include "opt/sim/sim.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c index 0998bd86..97b36fbe 100644 --- a/src/base/abci/abcUnate.c +++ b/src/base/abci/abcUnate.c @@ -21,7 +21,7 @@ #include "base/abc/abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index 08fc2809..679d9eed 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -21,7 +21,7 @@ #include "base/abc/abc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/io/ioWritePla.c b/src/base/io/ioWritePla.c index 389e4efa..676617a1 100644 --- a/src/base/io/ioWritePla.c +++ b/src/base/io/ioWritePla.c @@ -21,7 +21,7 @@ #include "ioAbc.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index c91a5d55..b1aa79f7 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -24,7 +24,7 @@ #include "map/if/if.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index baf3b82e..369b46f1 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -35,7 +35,7 @@ #include "proof/fra/fra.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_HEADER_START diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c index b2e06805..42c04c02 100644 --- a/src/bdd/cas/casCore.c +++ b/src/bdd/cas/casCore.c @@ -24,7 +24,7 @@ #include "base/main/main.h" #include "base/cmd/cmd.h" -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #include "cas.h" ABC_NAMESPACE_IMPL_START diff --git a/src/bdd/cas/casDec.c b/src/bdd/cas/casDec.c index 82c23240..f00bc46b 100644 --- a/src/bdd/cas/casDec.c +++ b/src/bdd/cas/casDec.c @@ -22,7 +22,7 @@ #include <string.h> #include <stdlib.h> -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #include "cas.h" ABC_NAMESPACE_IMPL_START diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h index 16a0594a..37e9746f 100644 --- a/src/bdd/dsd/dsdInt.h +++ b/src/bdd/dsd/dsdInt.h @@ -20,7 +20,7 @@ #define ABC__bdd__dsd__dsdInt_h -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #include "dsd.h" ABC_NAMESPACE_HEADER_START diff --git a/src/bdd/reo/reo.h b/src/bdd/reo/reo.h index 981b56df..a3ee844c 100644 --- a/src/bdd/reo/reo.h +++ b/src/bdd/reo/reo.h @@ -22,7 +22,7 @@ #include <stdio.h> #include <stdlib.h> -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// diff --git a/src/bool/dec/decFactor.c b/src/bool/dec/decFactor.c index 59ea6f26..05be202f 100644 --- a/src/bool/dec/decFactor.c +++ b/src/bool/dec/decFactor.c @@ -22,7 +22,7 @@ #include "dec.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/bool/dec/decUtil.c b/src/bool/dec/decUtil.c index eade1f5b..cab3f1e2 100644 --- a/src/bool/dec/decUtil.c +++ b/src/bool/dec/decUtil.c @@ -20,7 +20,7 @@ #include "dec.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif ABC_NAMESPACE_IMPL_START diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h index 29d23d68..15b27fad 100644 --- a/src/bool/kit/kit.h +++ b/src/bool/kit/kit.h @@ -35,7 +35,7 @@ #include "cloud.h" #ifdef ABC_USE_CUDD -#include "misc/extra/extraBdd.h" +#include "bdd/extrab/extraBdd.h" #endif //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/extra/module.make b/src/misc/extra/module.make index 13aa8f0f..5c1276e3 100644 --- a/src/misc/extra/module.make +++ b/src/misc/extra/module.make @@ -1,12 +1,4 @@ -SRC += src/misc/extra/extraBddAuto.c \ - src/misc/extra/extraBddCas.c \ - src/misc/extra/extraBddImage.c \ - src/misc/extra/extraBddKmap.c \ - src/misc/extra/extraBddMisc.c \ - src/misc/extra/extraBddSymm.c \ - src/misc/extra/extraBddTime.c \ - src/misc/extra/extraBddUnate.c \ - src/misc/extra/extraUtilBitMatrix.c \ +SRC += src/misc/extra/extraUtilBitMatrix.c \ src/misc/extra/extraUtilCanon.c \ src/misc/extra/extraUtilCube.c \ src/misc/extra/extraUtilDsd.c \ diff --git a/src/proof/abs/absOldRef.c b/src/proof/abs/absOldRef.c index b42053dd..315ecf89 100644 --- a/src/proof/abs/absOldRef.c +++ b/src/proof/abs/absOldRef.c @@ -21,7 +21,7 @@ #include "abs.h" #include "proof/ssw/ssw.h" #include "proof/fra/fra.h" -#include "proof/bbr/bbr.h" +#include "bdd/bbr/bbr.h" #include "proof/pdr/pdr.h" #include "sat/bmc/bmc.h" diff --git a/src/proof/fra/fraSec.c b/src/proof/fra/fraSec.c index dea2c3dc..06011d2e 100644 --- a/src/proof/fra/fraSec.c +++ b/src/proof/fra/fraSec.c @@ -23,7 +23,7 @@ #include "proof/int/int.h" #include "proof/ssw/ssw.h" #include "aig/saig/saig.h" -#include "proof/bbr/bbr.h" +#include "bdd/bbr/bbr.h" #include "proof/pdr/pdr.h" ABC_NAMESPACE_IMPL_START |