From 4de4605836f6bea796ced63b27b7eb6c252d6880 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 2 Mar 2024 16:31:41 -0800 Subject: [PATCH] More changees to compile new code with namespaces. --- src/sat/bsat2/Alg.h | 4 ++++ src/sat/bsat2/Alloc.h | 4 ++++ src/sat/bsat2/Dimacs.h | 4 ++++ src/sat/bsat2/Heap.h | 4 ++++ src/sat/bsat2/MainSat.cpp | 5 +++++ src/sat/bsat2/MainSimp.cpp | 5 +++++ src/sat/bsat2/Map.h | 4 ++++ src/sat/bsat2/Options.cpp | 4 ++++ src/sat/bsat2/Options.h | 4 ++++ src/sat/bsat2/Queue.h | 4 ++++ src/sat/bsat2/SimpSolver.cpp | 4 ++++ src/sat/bsat2/SimpSolver.h | 3 +++ src/sat/bsat2/Solver.cpp | 4 ++++ src/sat/bsat2/Solver.h | 3 +++ src/sat/bsat2/SolverTypes.h | 4 ++++ src/sat/bsat2/Sort.h | 3 +++ src/sat/bsat2/System.cpp | 18 ++++++++++++++++++ src/sat/bsat2/System.h | 4 ++++ src/sat/bsat2/Vec.h | 4 ++++ src/sat/bsat2/XAlloc.h | 4 ++++ 20 files changed, 93 insertions(+) diff --git a/src/sat/bsat2/Alg.h b/src/sat/bsat2/Alg.h index 3e0745f1d3..2a5af3efff 100644 --- a/src/sat/bsat2/Alg.h +++ b/src/sat/bsat2/Alg.h @@ -23,6 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { //================================================================================================= @@ -81,4 +83,6 @@ static inline void append(const vec& from, vec& to){ copy(from, to, true); //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Alloc.h b/src/sat/bsat2/Alloc.h index 7f506cb5a9..c583bf3b68 100644 --- a/src/sat/bsat2/Alloc.h +++ b/src/sat/bsat2/Alloc.h @@ -24,6 +24,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "XAlloc.h" #include "Vec.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { //================================================================================================= @@ -128,4 +130,6 @@ RegionAllocator::alloc(int size) //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Dimacs.h b/src/sat/bsat2/Dimacs.h index f26f152be2..806b869422 100644 --- a/src/sat/bsat2/Dimacs.h +++ b/src/sat/bsat2/Dimacs.h @@ -26,6 +26,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "ParseUtils.h" #include "SolverTypes.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { //================================================================================================= @@ -86,4 +88,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Heap.h b/src/sat/bsat2/Heap.h index e5b4ddb56a..bdaa7edfda 100644 --- a/src/sat/bsat2/Heap.h +++ b/src/sat/bsat2/Heap.h @@ -23,6 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { //================================================================================================= @@ -146,4 +148,6 @@ class Heap { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/MainSat.cpp b/src/sat/bsat2/MainSat.cpp index 1f61f9eecc..e988ac3ac4 100644 --- a/src/sat/bsat2/MainSat.cpp +++ b/src/sat/bsat2/MainSat.cpp @@ -29,6 +29,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Dimacs.h" #include "Solver.h" +ABC_NAMESPACE_IMPL_START + using namespace Minisat; //================================================================================================= @@ -195,3 +197,6 @@ extern "C" int MainSat(int argc, char** argv) exit(0); } } + + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bsat2/MainSimp.cpp b/src/sat/bsat2/MainSimp.cpp index 4a89092108..c959e606f5 100644 --- a/src/sat/bsat2/MainSimp.cpp +++ b/src/sat/bsat2/MainSimp.cpp @@ -33,6 +33,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Dimacs.h" #include "SimpSolver.h" +ABC_NAMESPACE_IMPL_START + using namespace Minisat; //================================================================================================= @@ -204,3 +206,6 @@ extern "C" int MainSimp(int argc, char** argv) exit(0); } } + + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bsat2/Map.h b/src/sat/bsat2/Map.h index 1dd22a06d3..d9a4c56310 100644 --- a/src/sat/bsat2/Map.h +++ b/src/sat/bsat2/Map.h @@ -23,6 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "IntTypes.h" #include "Vec.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { //================================================================================================= @@ -190,4 +192,6 @@ class Map { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Options.cpp b/src/sat/bsat2/Options.cpp index b30cff0e5f..1f700dc0f0 100644 --- a/src/sat/bsat2/Options.cpp +++ b/src/sat/bsat2/Options.cpp @@ -21,6 +21,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Options.h" #include "ParseUtils.h" +ABC_NAMESPACE_IMPL_START + using namespace Minisat; int Minisat::parseOptions(int& argc, char** argv, bool strict) @@ -91,3 +93,5 @@ int Minisat::printUsageAndExit (int argc, char** argv, bool verbose) return 0; } + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bsat2/Options.h b/src/sat/bsat2/Options.h index 439cb8f216..42bc451268 100644 --- a/src/sat/bsat2/Options.h +++ b/src/sat/bsat2/Options.h @@ -29,6 +29,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Vec.h" #include "ParseUtils.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { //================================================================================================== @@ -384,4 +386,6 @@ class BoolOption : public Option //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Queue.h b/src/sat/bsat2/Queue.h index 11b4291151..dd40e2c91d 100644 --- a/src/sat/bsat2/Queue.h +++ b/src/sat/bsat2/Queue.h @@ -25,6 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA namespace Minisat { +ABC_NAMESPACE_CXX_HEADER_START + //================================================================================================= template @@ -66,4 +68,6 @@ class Queue { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/SimpSolver.cpp b/src/sat/bsat2/SimpSolver.cpp index 5a7a006c21..59820a47b0 100644 --- a/src/sat/bsat2/SimpSolver.cpp +++ b/src/sat/bsat2/SimpSolver.cpp @@ -22,6 +22,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "SimpSolver.h" #include "System.h" +ABC_NAMESPACE_IMPL_START + using namespace Minisat; //================================================================================================= @@ -718,3 +720,5 @@ void SimpSolver::garbageCollect() ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); to.moveTo(ca); } + +ABC_NAMESPACE_IMPL_END \ No newline at end of file diff --git a/src/sat/bsat2/SimpSolver.h b/src/sat/bsat2/SimpSolver.h index e24b0e4305..098254a12f 100644 --- a/src/sat/bsat2/SimpSolver.h +++ b/src/sat/bsat2/SimpSolver.h @@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Queue.h" #include "Solver.h" +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -194,4 +195,6 @@ inline lbool SimpSolver::solveLimited (const vec& assumps, bool do_simp, bo //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Solver.cpp b/src/sat/bsat2/Solver.cpp index 0f8b415a93..2a06424075 100644 --- a/src/sat/bsat2/Solver.cpp +++ b/src/sat/bsat2/Solver.cpp @@ -23,6 +23,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Sort.h" #include "Solver.h" +ABC_NAMESPACE_IMPL_START + using namespace Minisat; //================================================================================================= @@ -922,3 +924,5 @@ void Solver::garbageCollect() ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); to.moveTo(ca); } + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bsat2/Solver.h b/src/sat/bsat2/Solver.h index fc0bb4ba2e..d14b2fec82 100644 --- a/src/sat/bsat2/Solver.h +++ b/src/sat/bsat2/Solver.h @@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Options.h" #include "SolverTypes.h" +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -370,4 +371,6 @@ inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ ve //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/SolverTypes.h b/src/sat/bsat2/SolverTypes.h index f34deca1ca..6401a2a0c1 100644 --- a/src/sat/bsat2/SolverTypes.h +++ b/src/sat/bsat2/SolverTypes.h @@ -30,6 +30,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "Map.h" #include "Alloc.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { //================================================================================================= @@ -404,4 +406,6 @@ inline void Clause::strengthen(Lit p) //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Sort.h b/src/sat/bsat2/Sort.h index cc96486d8c..15b6b7d075 100644 --- a/src/sat/bsat2/Sort.h +++ b/src/sat/bsat2/Sort.h @@ -26,6 +26,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA //================================================================================================= // Some sorting algorithms for vec's +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -95,4 +96,6 @@ template void sort(vec& v) { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/System.cpp b/src/sat/bsat2/System.cpp index c2d6259e28..e617500c2d 100644 --- a/src/sat/bsat2/System.cpp +++ b/src/sat/bsat2/System.cpp @@ -25,6 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include +ABC_NAMESPACE_IMPL_START + using namespace Minisat; // TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and @@ -72,24 +74,40 @@ double Minisat::memUsedPeak() { double peak = memReadPeak() / 1024; return peak == 0 ? memUsed() : peak; } +ABC_NAMESPACE_IMPL_END + #elif defined(__FreeBSD__) +ABC_NAMESPACE_IMPL_START + double Minisat::memUsed(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_maxrss / 1024; } double MiniSat::memUsedPeak(void) { return memUsed(); } +ABC_NAMESPACE_IMPL_END #elif defined(__APPLE__) #include +ABC_NAMESPACE_IMPL_START + double Minisat::memUsed(void) { malloc_statistics_t t; malloc_zone_statistics(NULL, &t); return (double)t.max_size_in_use / (1024*1024); } +ABC_NAMESPACE_IMPL_END + #else + +ABC_NAMESPACE_IMPL_START + double Minisat::memUsed() { return 0; } double Minisat::memUsedPeak() { return 0; } + +ABC_NAMESPACE_IMPL_END + #endif + diff --git a/src/sat/bsat2/System.h b/src/sat/bsat2/System.h index d776c880c8..2952d4117b 100644 --- a/src/sat/bsat2/System.h +++ b/src/sat/bsat2/System.h @@ -29,6 +29,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA //------------------------------------------------------------------------------------------------- +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { static inline double cpuTime(void); // CPU-time in seconds. @@ -57,4 +59,6 @@ static inline double Minisat::cpuTime(void) { #endif +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Vec.h b/src/sat/bsat2/Vec.h index f0e07d016a..59b5583a8f 100644 --- a/src/sat/bsat2/Vec.h +++ b/src/sat/bsat2/Vec.h @@ -27,6 +27,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "IntTypes.h" #include "XAlloc.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { //================================================================================================= @@ -127,4 +129,6 @@ void vec::clear(bool dealloc) { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/XAlloc.h b/src/sat/bsat2/XAlloc.h index 1da176028d..9533b6b908 100644 --- a/src/sat/bsat2/XAlloc.h +++ b/src/sat/bsat2/XAlloc.h @@ -24,6 +24,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { //================================================================================================= @@ -42,4 +44,6 @@ static inline void* xrealloc(void *ptr, size_t size) //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif