diff --git a/CMakeLists.txt b/CMakeLists.txt index ae4da001..23845b89 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -35,6 +35,9 @@ include_directories(${minisat_SOURCE_DIR}) add_definitions(-D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS) +set(CMAKE_CXX_STANDARD 11) +set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -std=c++11") + #-------------------------------------------------------------------------------------------------- # Build Targets: diff --git a/Makefile b/Makefile index ceb9d77d..187a2c69 100644 --- a/Makefile +++ b/Makefile @@ -38,6 +38,9 @@ config: ## Configurable options end ####################################################################### +# determine operating system name +UNAME_S := $(shell uname -s) + INSTALL ?= install # GNU Standard Install Variables @@ -52,7 +55,13 @@ mandir ?= $(datarootdir)/man MINISAT = minisat# Name of MiniSat main executable. MINISAT_CORE = minisat_core# Name of simplified MiniSat executable (only core solver support). MINISAT_SLIB = lib$(MINISAT).a# Name of MiniSat static library. -MINISAT_DLIB = lib$(MINISAT).so# Name of MiniSat shared library. +ifeq ($(UNAME_S), Darwin) + MINISAT_DLIB_MAC_PRE = lib$(MINISAT) + MINISAT_DLIB_MAC_POST = dylib + MINISAT_DLIB = $(MINISAT_DLIB_MAC_PRE).$(MINISAT_DLIB_MAC_POST) +else + MINISAT_DLIB = lib$(MINISAT).so# Name of MiniSat shared library (for Linux). +endif # Shared Library Version SOMAJOR=2 @@ -86,7 +95,11 @@ csh: $(BUILD_DIR)/dynamic/bin/$(MINISAT_CORE) lr: $(BUILD_DIR)/release/lib/$(MINISAT_SLIB) ld: $(BUILD_DIR)/debug/lib/$(MINISAT_SLIB) lp: $(BUILD_DIR)/profile/lib/$(MINISAT_SLIB) -lsh: $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE) +ifeq ($(UNAME_S), Darwin) + lsh: $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB_MAC_PRE).$(SOMAJOR).$(SOMINOR).$(MINISAT_DLIB_MAC_POST) +else + lsh: $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE) +endif ## Build-type Compile-flags: $(BUILD_DIR)/release/%.o: MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_RELSYM) @@ -96,9 +109,14 @@ $(BUILD_DIR)/dynamic/%.o: MINISAT_CXXFLAGS +=$(MINISAT_REL) $(MINISAT_FPIC) ## Build-type Link-flags: $(BUILD_DIR)/profile/bin/$(MINISAT): MINISAT_LDFLAGS += -pg -$(BUILD_DIR)/release/bin/$(MINISAT): MINISAT_LDFLAGS += --static $(MINISAT_RELSYM) $(BUILD_DIR)/profile/bin/$(MINISAT_CORE): MINISAT_LDFLAGS += -pg -$(BUILD_DIR)/release/bin/$(MINISAT_CORE): MINISAT_LDFLAGS += --static $(MINISAT_RELSYM) +ifeq ($(UNAME_S), Darwin) + $(BUILD_DIR)/release/bin/$(MINISAT): MINISAT_LDFLAGS += $(MINISAT_RELSYM) + $(BUILD_DIR)/release/bin/$(MINISAT_CORE): MINISAT_LDFLAGS += $(MINISAT_RELSYM) +else + $(BUILD_DIR)/release/bin/$(MINISAT): MINISAT_LDFLAGS += --static $(MINISAT_RELSYM) + $(BUILD_DIR)/release/bin/$(MINISAT_CORE): MINISAT_LDFLAGS += --static $(MINISAT_RELSYM) +endif ## Executable dependencies $(BUILD_DIR)/release/bin/$(MINISAT): $(BUILD_DIR)/release/minisat/simp/Main.o $(BUILD_DIR)/release/lib/$(MINISAT_SLIB) @@ -118,9 +136,15 @@ $(BUILD_DIR)/dynamic/bin/$(MINISAT_CORE): $(BUILD_DIR)/dynamic/minisat/core/Mai $(BUILD_DIR)/release/lib/$(MINISAT_SLIB): $(foreach o,$(OBJS),$(BUILD_DIR)/release/$(o)) $(BUILD_DIR)/debug/lib/$(MINISAT_SLIB): $(foreach o,$(OBJS),$(BUILD_DIR)/debug/$(o)) $(BUILD_DIR)/profile/lib/$(MINISAT_SLIB): $(foreach o,$(OBJS),$(BUILD_DIR)/profile/$(o)) -$(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\ - $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\ - $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB): $(foreach o,$(OBJS),$(BUILD_DIR)/dynamic/$(o)) +ifeq ($(UNAME_S), Darwin) + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB_MAC_PRE).$(SOMAJOR).$(SOMINOR).$(MINISAT_DLIB_MAC_POST)\ + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB_MAC_PRE).$(SOMAJOR).$(MINISAT_DLIB_MAC_POST)\ + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB): $(foreach o,$(OBJS),$(BUILD_DIR)/dynamic/$(o)) +else + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\ + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\ + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB): $(foreach o,$(OBJS),$(BUILD_DIR)/dynamic/$(o)) +endif ## Compile rules (these should be unified, buit I have not yet found a way which works in GNU Make) $(BUILD_DIR)/release/%.o: %.cc @@ -157,14 +181,27 @@ $(BUILD_DIR)/release/bin/$(MINISAT_CORE) $(BUILD_DIR)/debug/bin/$(MINISAT_CORE) $(VERB) $(AR) -rcs $@ $^ ## Shared Library rule -$(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\ - $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\ - $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB): +ifeq ($(UNAME_S), Darwin) + ## Shared Library on Mac OS + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB_MAC_PRE).$(SOMAJOR).$(SOMINOR).$(MINISAT_DLIB_MAC_POST)\ + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB_MAC_PRE).$(SOMAJOR).$(MINISAT_DLIB_MAC_POST)\ + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB): + $(ECHO) Linking Shared Library: $@ + $(VERB) mkdir -p $(dir $@) + $(VERB) $(CXX) $(MINISAT_LDFLAGS) $(LDFLAGS) -o $@ -dynamiclib -current_version $(SOMAJOR).$(SOMINOR) -compatibility_version $(SOMAJOR).$(SOMINOR) $^ + $(VERB) ln -sf $(MINISAT_DLIB_MAC_PRE).$(SOMAJOR).$(SOMINOR).$(MINISAT_DLIB_MAC_POST) $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB_MAC_PRE).$(SOMAJOR).$(MINISAT_DLIB_MAC_POST) + $(VERB) ln -sf $(MINISAT_DLIB_MAC_PRE).$(SOMAJOR).$(MINISAT_DLIB_MAC_POST) $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB) +else + ## Shared Library on Linux + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\ + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\ + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB): $(ECHO) Linking Shared Library: $@ $(VERB) mkdir -p $(dir $@) $(VERB) $(CXX) $(MINISAT_LDFLAGS) $(LDFLAGS) -o $@ -shared -Wl,-soname,$(MINISAT_DLIB).$(SOMAJOR) $^ $(VERB) ln -sf $(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE) $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR) $(VERB) ln -sf $(MINISAT_DLIB).$(SOMAJOR) $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB) +endif install: install-headers install-lib install-bin install-debug: install-headers install-lib-debug @@ -199,10 +236,16 @@ clean: rm -f $(foreach t, release debug profile dynamic, $(foreach o, $(SRCS:.cc=.o), $(BUILD_DIR)/$t/$o)) \ $(foreach t, release debug profile dynamic, $(foreach d, $(SRCS:.cc=.d), $(BUILD_DIR)/$t/$d)) \ $(foreach t, release debug profile dynamic, $(BUILD_DIR)/$t/bin/$(MINISAT_CORE) $(BUILD_DIR)/$t/bin/$(MINISAT)) \ - $(foreach t, release debug profile, $(BUILD_DIR)/$t/lib/$(MINISAT_SLIB)) \ - $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\ + $(foreach t, release debug profile, $(BUILD_DIR)/$t/lib/$(MINISAT_SLIB)) +ifeq ($(UNAME_S), Darwin) + rm -f $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB_MAC_PRE).$(SOMAJOR).$(SOMINOR).$(MINISAT_DLIB_MAC_POST)\ + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB_MAC_PRE).$(SOMAJOR).$(MINISAT_DLIB_MAC_POST)\ + $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB) +else + rm -f $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR).$(SOMINOR)$(SORELEASE)\ $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB).$(SOMAJOR)\ $(BUILD_DIR)/dynamic/lib/$(MINISAT_DLIB) +endif distclean: clean rm -f config.mk diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index 0b4f77ad..6175cb4f 100644 --- a/minisat/core/Solver.cc +++ b/minisat/core/Solver.cc @@ -992,11 +992,11 @@ void Solver::printStats() const { double cpu_time = cpuTime(); double mem_used = memUsedPeak(); - printf("restarts : %"PRIu64"\n", starts); - printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", conflicts , conflicts /cpu_time); - printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time); - printf("propagations : %-12"PRIu64" (%.0f /sec)\n", propagations, propagations/cpu_time); - printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals); + printf("restarts : %" PRIu64 "\n", starts); + printf("conflicts : %-12" PRIu64 " (%.0f /sec)\n", conflicts , conflicts /cpu_time); + printf("decisions : %-12" PRIu64 " (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time); + printf("propagations : %-12" PRIu64 " (%.0f /sec)\n", propagations, propagations/cpu_time); + printf("conflict literals : %-12" PRIu64 " (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals); if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); printf("CPU time : %g s\n", cpu_time); } diff --git a/minisat/core/SolverTypes.h b/minisat/core/SolverTypes.h index 89986d1e..aa45ddb2 100644 --- a/minisat/core/SolverTypes.h +++ b/minisat/core/SolverTypes.h @@ -52,7 +52,7 @@ struct Lit { int x; // Use this as a constructor: - friend Lit mkLit(Var var, bool sign = false); + friend Lit mkLit(Var var, bool sign); bool operator == (Lit p) const { return x == p.x; } bool operator != (Lit p) const { return x != p.x; } @@ -60,7 +60,7 @@ struct Lit { }; -inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; } +inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; } inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; } inline bool sign (Lit p) { return p.x & 1; } diff --git a/minisat/utils/Options.h b/minisat/utils/Options.h index 4e71a18c..7d2e83a8 100644 --- a/minisat/utils/Options.h +++ b/minisat/utils/Options.h @@ -282,15 +282,15 @@ class Int64Option : public Option if (range.begin == INT64_MIN) fprintf(stderr, "imin"); else - fprintf(stderr, "%4"PRIi64, range.begin); + fprintf(stderr, "%4" PRIi64, range.begin); fprintf(stderr, " .. "); if (range.end == INT64_MAX) fprintf(stderr, "imax"); else - fprintf(stderr, "%4"PRIi64, range.end); + fprintf(stderr, "%4" PRIi64, range.end); - fprintf(stderr, "] (default: %"PRIi64")\n", value); + fprintf(stderr, "] (default: %" PRIi64 ")\n", value); if (verbose){ fprintf(stderr, "\n %s\n", description); fprintf(stderr, "\n"); diff --git a/minisat/utils/System.cc b/minisat/utils/System.cc index 21aa4ff4..d2ed07e4 100644 --- a/minisat/utils/System.cc +++ b/minisat/utils/System.cc @@ -87,11 +87,11 @@ double Minisat::memUsed() { malloc_statistics_t t; malloc_zone_statistics(NULL, &t); return (double)t.max_size_in_use / (1024*1024); } -double Minisat::memUsedPeak() { return memUsed(); } +double Minisat::memUsedPeak(bool strictlyPeak) { return memUsed(); } #else double Minisat::memUsed() { return 0; } -double Minisat::memUsedPeak() { return 0; } +double Minisat::memUsedPeak(bool strictlyPeak) { return 0; } #endif