More changees to compile new code with namespaces.

This commit is contained in:
Alan Mishchenko 2024-03-02 16:31:41 -08:00
parent a1159d98df
commit 4de4605836
20 changed files with 93 additions and 0 deletions

View File

@ -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<T>& from, vec<T>& to){ copy(from, to, true);
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

View File

@ -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<T>::alloc(int size)
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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<class T>
@ -66,4 +68,6 @@ public:
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

View File

@ -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

View File

@ -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<Lit>& assumps, bool do_simp, bo
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

View File

@ -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

View File

@ -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

View File

@ -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

View File

@ -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 <class T> void sort(vec<T>& v) {
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

View File

@ -25,6 +25,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <stdio.h>
#include <stdlib.h>
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 <malloc/malloc.h>
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

View File

@ -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

View File

@ -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<T>::clear(bool dealloc) {
//=================================================================================================
}
ABC_NAMESPACE_CXX_HEADER_END
#endif

View File

@ -24,6 +24,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include <errno.h>
#include <stdlib.h>
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