Skip to content

Commit

Permalink
fix c++11 std compliance and mac compatibility
Browse files Browse the repository at this point in the history
  • Loading branch information
@Udopia
Udopia committed Aug 2, 2023
1 parent 37dc6c6 commit 37a907d
Show file tree
Hide file tree
Showing 6 changed files with 70 additions and 24 deletions.
3 changes: 3 additions & 0 deletions CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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:

Expand Down
67 changes: 55 additions & 12 deletions Makefile
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,9 @@ config:

## Configurable options end #######################################################################

# determine operating system name
UNAME_S := $(shell uname -s)

INSTALL ?= install

# GNU Standard Install Variables
Expand All @@ -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
Expand Down Expand Up @@ -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)
Expand All @@ -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)
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
10 changes: 5 additions & 5 deletions minisat/core/Solver.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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);
}
Expand Down
4 changes: 2 additions & 2 deletions minisat/core/SolverTypes.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -52,15 +52,15 @@ 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; }
bool operator < (Lit p) const { return x < p.x; } // '<' makes p, ~p adjacent in the ordering.
};


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; }
Expand Down
6 changes: 3 additions & 3 deletions minisat/utils/Options.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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");
Expand Down
4 changes: 2 additions & 2 deletions minisat/utils/System.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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


Expand Down

0 comments on commit 37a907d

Please sign in to comment.