From 7a649c2d56fed828245c9033b526a3efe37f4385 Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 8 Feb 2011 12:18:01 +0000 Subject: [PATCH] Patch from Khoo Yit Phang. General clean-up of the build system. - Remove unused or unnecessary flags and rules. - Fix up automatic dependency generation. - Move final linking of bin/stp to the topmost Makefile for better dependency control. - Update versionString.cpp only if the version changed, to avoid unnecessary rebuild. - Build src/sat/libminisat.a and lib/libstp.a by concatenating their constituent archives, rather than by relisting their contained object files. - Add dependencies for bin/stp and lib/libstp.a to rebuild them only when necessary. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1126 e59a4935-1847-0410-ae03-e826735625c1 --- scripts/Makefile.common | 57 ++++++++++++++++---- scripts/Makefile.in | 77 ++++++++++++--------------- src/AST/Makefile | 26 ++++----- src/STPManager/Makefile | 14 ++--- src/absrefine_counterexample/Makefile | 15 +++--- src/c_interface/Makefile | 16 +++--- src/extlib-abc/Makefile | 19 +++---- src/extlib-abc/aig/cnf/module.make | 8 --- src/extlib-abc/aig/dar/module.make | 10 ---- src/extlib-abc/aig/kit/module.make | 10 ---- src/extlib-constbv/Makefile | 15 +++--- src/main/Makefile | 63 ++++++++++------------ src/parser/Makefile | 21 ++++---- src/printer/Makefile | 17 +++--- src/sat/Makefile | 13 ++--- src/sat/cryptominisat2/Makefile | 11 ++-- src/sat/mtl/template.mk | 3 +- src/simplifier/Makefile | 13 +++-- src/to-sat/Makefile | 16 +++--- tests/c-api-tests/Makefile | 2 +- 20 files changed, 211 insertions(+), 215 deletions(-) delete mode 100644 src/extlib-abc/aig/cnf/module.make delete mode 100644 src/extlib-abc/aig/dar/module.make delete mode 100644 src/extlib-abc/aig/kit/module.make diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 825eaa8..f64fc60 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -31,9 +31,7 @@ OPTIMIZE = -O3 -g # Maximum optimization #CFLAGS_FPIC = -fPIC CFLAGS_FPIC = -#-fno-inline CFLAGS_BASE = $(OPTIMIZE) -CFLAGS_BASE = $(OPTIMIZE) ifeq ($(WITHCBITP),yes) @@ -51,8 +49,6 @@ SHELL=/bin/bash ifdef STATIC LDFLAGS_BASE = -static-libgcc -static -else - LDFLAGS_BASE = -lstdc++ endif @@ -60,10 +56,7 @@ LDFLAGS = $(LDFLAGS_BASE) CFLAGS = $(CFLAGS_BASE) $(CFLAGS_M32) -# Used by Doug Lea's malloc that I added into minisat2. -#CFLAGS += -DONLY_MSPACES -DMSPACES - -#Required my minisat2.2 +#Required by minisat2.2 CFLAGS += -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS #CXXFLAGS = $(CFLAGS) -Wall -Wextra -DEXT_HASH_MAP -Wno-deprecated @@ -79,4 +72,50 @@ CXXFLAGS = $(CFLAGS) -DEXT_HASH_MAP -Wno-deprecated LEX = flex YACC = bison -d -y --debug -v -RANLIB = ranlib + + +# Run gcc to generate dependency rules for object files; use as follows: +# : +# $(call makedepend,,) +# -include +# +# Object files will be rebuilt if any of the following is updated: +# - the source file +# - a dependency (e.g., included header files) +# - the Makefile running this command +# - any file included by the Makefile, including this Makefile.common file, +# but excluding +# +# Note: do not use $^ as , since additional dependencies will be +# added to the dependency list of . +# +ifeq (,$(filter clean configclean distclean,$(MAKECMDGOALS))) +define makedepend + echo "Making dependencies" + $(RM) $(1) + $(foreach foo,$(2), + $(CXX) $(CXXFLAGS) \ + -MM -MG -MP \ + -MQ $(basename $(foo)).o -MQ $(1) \ + $(foo) \ + >> $(1) + ) + echo "$(addsuffix .o,$(basename $(2))) $(1) : $(filter-out $(1),$(MAKEFILE_LIST))" >> $(1) +endef +endif + + +# Concatenate ar archives: +# $(call arcat,destination.a,source1.a source2.a ...) +define arcat + $(call arcat.sh,$(abspath $(1)),$(shell mktemp -d $(CURDIR)/arcat-XXXXXXXXXX),$(abspath $(2))) +endef + +define arcat.sh + set -e; \ + trap "$(RM) -r $(2)" EXIT; \ + cd $(2); \ + $(3:%=$(AR) x %;) \ + $(RM) __.SYMDEF*; \ + $(AR) qcs $(1) * +endef diff --git a/scripts/Makefile.in b/scripts/Makefile.in index 8ba2fc2..ea56612 100644 --- a/scripts/Makefile.in +++ b/scripts/Makefile.in @@ -20,53 +20,46 @@ LIBRARIES=lib/libstp.a HEADERS=$(SRC)/c_interface/*.h .PHONY: all -all: AST STPManager absrefine_counterexample to-sat simplifier printer c_interface extlib-constbv extlib-abc - - $(MAKE) -C $(SRC)/sat core - $(MAKE) -C $(SRC)/parser - $(MAKE) -C $(SRC)/main - $(AR) rc libstp.a $(SRC)/AST/*.o \ - $(SRC)/AST/NodeFactory/*.o \ - $(SRC)/STPManager/*.o \ - $(SRC)/printer/*.o \ - $(SRC)/absrefine_counterexample/*.o \ - $(SRC)/to-sat/*.o \ - $(SRC)/to-sat/AIG/*.o \ - $(SRC)/to-sat/ASTNode/*.o \ - $(SRC)/sat/*.o \ - $(SRC)/sat/core/Solver.or \ - $(SRC)/sat/simp/SimpSolver.or \ - $(SRC)/sat/utils/System.or \ - $(SRC)/sat/cryptominisat2/*.o \ - $(SRC)/simplifier/*.o \ - $(SRC)/simplifier/constantBitP/*.o \ - $(SRC)/extlib-constbv/*.o \ - $(SRC)/extlib-abc/*/*/*.o \ - $(SRC)/c_interface/*.o \ - $(SRC)/parser/LetMgr.o \ - $(SRC)/parser/parseCVC.o \ - $(SRC)/parser/lexCVC.o \ - $(SRC)/parser/parseSMT.o \ - $(SRC)/parser/lexSMT.o \ - $(SRC)/main/Globals.o \ - $(SRC)/main/versionString.o - @# N.B.: don't put main/main.o in the library. - $(RANLIB) libstp.a - @mkdir -p lib - @mv libstp.a lib/ +all: bin/stp lib/libstp.a @echo "" @echo "Compilation successful." @echo "Type 'make install' to install STP." +# An up-to-date $(SRC)/X/libX.a file also means that its constituent +# object files are also up-to-date: the following rules use this fact to +# remake only when necessary. + +bin/stp: $(SRC)/main/main.o lib/libstp.a + mkdir -p $(@D) + $(CXX) $(CXXFLAGS) $(LDFLAGS) $^ -o $@ + +lib/libstp.a: $(addprefix $(SRC)/, \ + AST/libast.a STPManager/libstpmgr.a printer/libprinter.a \ + absrefine_counterexample/libabstractionrefinement.a \ + to-sat/libtosat.a sat/libminisat.a simplifier/libsimplifier.a \ + extlib-constbv/libconstantbv.a extlib-abc/libabc.a \ + c_interface/libcinterface.a parser/libparser.a main/libmain.a) + mkdir -p $(@D) + $(RM) $@ + $(call arcat,$@,$^) + # During the build of AST some classes are built that most of the other # classes depend upon. So in a parallel make, AST should be made first. +$(addprefix $(SRC)/, \ + STPManager/libstpmgr.a printer/libprinter.a \ + absrefine_counterexample/libabstractionrefinement.a \ + to-sat/libtosat.a simplifier/libsimplifier.a c_interface/libcinterface.a \ + extlib-constbv/libconstantbv.a extlib-abc/libabc.a parser/libparser.a \ + main/libmain.a main/main.o): $(SRC)/AST/libast.a + +$(SRC)/sat/libminisat.a: MAKEGOALS=core -.PHONY: AST -AST: - $(MAKE) -C $(SRC)/$@ +# main.o is automatically built alongside libmain.a +$(SRC)/main/main.o : $(SRC)/main/libmain.a ; -STPManager absrefine_counterexample to-sat simplifier printer c_interface extlib-constbv extlib-abc: AST - $(MAKE) -C $(SRC)/$@ +$(SRC)/%: FORCE + $(MAKE) -C $(@D) $(MAKEGOALS) +FORCE: #### @@ -101,9 +94,9 @@ clean: $(MAKE) clean -C $(SRC)/main $(MAKE) clean -C tests/c-api-tests -.PHONY: configclean -configclean: - rm -rf scripts/config.info +.PHONY: distclean configclean +distclean configclean: clean + $(RM) scripts/config.info Makefile .PHONY: regressall regressall: all diff --git a/src/AST/Makefile b/src/AST/Makefile index c801df6..fa27aa5 100644 --- a/src/AST/Makefile +++ b/src/AST/Makefile @@ -1,31 +1,27 @@ TOP = ../.. include $(TOP)/scripts/Makefile.common -SRCS=$(wildcard *.cpp) -SRCS+=$(wildcard NodeFactory/*.cpp) +SRCS = $(wildcard *.cpp) +SRCS += $(wildcard NodeFactory/*.cpp) OBJS = $(SRCS:.cpp=.o) -OBJS+= ASTKind.o -CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE) +OBJS += ASTKind.o #Make the ast library for use by other modules -libast.a:$(OBJS) depend - -rm -rf $@ - $(AR) rc $@ $(OBJS) - $(RANLIB) $@ +libast.a: $(OBJS) + $(RM) $@ + $(AR) qcs $@ $^ # ASTKind.h and ASTKind.cpp are automatically generated -ASTKind.h ASTKind.cpp: ASTKind.kinds genkinds.pl +ASTKind.h ASTKind.cpp: ASTKind.kinds genkinds.pl ./genkinds.pl .PHONY: clean clean: - rm -rf NodeFactory/*.o *.o *~ *.a ASTKind.cpp ASTKind.h depend .#* + $(RM) *.o */*.o *~ *.a .#* depend ASTKind.cpp ASTKind.h -#If this depended on ASTKind.h & ASTKind.cpp, then ./genkinds.pl -#would be called each "clean". -depend: $(SRCS) ASTKind.kinds genkinds.pl - @$(CXX) -MM -MG $(CXXFLAGS) $(SRCS) > $@ +depend: $(SRCS) + @$(call makedepend,$@,$(SRCS)) --include ./depend +-include depend diff --git a/src/STPManager/Makefile b/src/STPManager/Makefile index 2b5db76..caf4e86 100644 --- a/src/STPManager/Makefile +++ b/src/STPManager/Makefile @@ -3,17 +3,17 @@ include $(TOP)/scripts/Makefile.common SRCS = $(wildcard *.cpp) OBJS = $(SRCS:.cpp=.o) -CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE) -libstpmgr.a: $(OBJS) depend - $(AR) rc $@ $(OBJS) - $(RANLIB) $@ + +libstpmgr.a: $(OBJS) + $(RM) $@ + $(AR) qcs $@ $^ .PHONY: clean -clean: - rm -rf *.o *~ *.a .#* depend +clean: + $(RM) *.o *~ *.a .#* depend depend: $(SRCS) - @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ + @$(call makedepend,$@,$(SRCS)) -include depend diff --git a/src/absrefine_counterexample/Makefile b/src/absrefine_counterexample/Makefile index 99613a6..6372215 100644 --- a/src/absrefine_counterexample/Makefile +++ b/src/absrefine_counterexample/Makefile @@ -4,14 +4,15 @@ include $(TOP)/scripts/Makefile.common SRCS = $(wildcard *.cpp) OBJS = $(SRCS:.cpp=.o) -libabstractionrefinement.a: $(OBJS) depend - $(AR) rc $@ $(OBJS) - $(RANLIB) $@ -clean: - rm -rf *.o *~ *.a .#* depend +libabstractionrefinement.a: $(OBJS) + $(RM) $@ + $(AR) qcs $@ $^ + +clean: + $(RM) *.o *~ *.a .#* depend depend: $(SRCS) - @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ + @$(call makedepend,$@,$(SRCS)) --include depend +-include depend diff --git a/src/c_interface/Makefile b/src/c_interface/Makefile index 649b365..a65a421 100644 --- a/src/c_interface/Makefile +++ b/src/c_interface/Makefile @@ -3,18 +3,18 @@ include $(TOP)/scripts/Makefile.common SRCS = $(wildcard *.cpp) OBJS = $(SRCS:.cpp=.o) -CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE) -libcinterface.a: $(OBJS) depend - $(AR) rc $@ $(OBJS) - $(RANLIB) $@ + +libcinterface.a: $(OBJS) + $(RM) $@ + $(AR) qcs $@ $^ .PHONY: clean -clean: - rm -rf *.o *~ *.a .#* depend +clean: + $(RM) *.o *~ *.a .#* depend depend: $(SRCS) - @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ + @$(call makedepend,$@,$(SRCS)) -#-include depend +-include depend diff --git a/src/extlib-abc/Makefile b/src/extlib-abc/Makefile index ca58bda..bff1cc2 100644 --- a/src/extlib-abc/Makefile +++ b/src/extlib-abc/Makefile @@ -2,22 +2,19 @@ TOP = ../.. include $(TOP)/scripts/Makefile.common SRCS = $(wildcard aig/*/*.c) -#SRCS += $(wildcard aig/cnf/*.c) -#SRCS += $(wildcard aig/kit/*.c) -#SRCS += $(wildcard aig/dar/*.c) - OBJS = $(SRCS:.c=.o) CFLAGS += -I. -libabc.a: $(OBJS) - $(AR) rc $@ $(OBJS) - $(RANLIB) $@ + +libabc.a: $(OBJS) + $(RM) $@ + $(AR) qcs $@ $^ .PHONY: clean -clean: - rm -rf *.o *~ *.a .#* depend $(OBJS) +clean: + $(RM) $(OBJS) *~ *.a .#* depend depend: $(SRCS) - @$(CXX) -MM -MG $(CXXFLAGS) $(SRCS) > $@ + @$(call makedepend,$@,$(SRCS)) --include depend +-include depend diff --git a/src/extlib-abc/aig/cnf/module.make b/src/extlib-abc/aig/cnf/module.make deleted file mode 100644 index f0430c2..0000000 --- a/src/extlib-abc/aig/cnf/module.make +++ /dev/null @@ -1,8 +0,0 @@ -SRC += src/aig/cnf/cnfCore.c \ - src/aig/cnf/cnfCut.c \ - src/aig/cnf/cnfData.c \ - src/aig/cnf/cnfMan.c \ - src/aig/cnf/cnfMap.c \ - src/aig/cnf/cnfPost.c \ - src/aig/cnf/cnfUtil.c \ - src/aig/cnf/cnfWrite.c diff --git a/src/extlib-abc/aig/dar/module.make b/src/extlib-abc/aig/dar/module.make deleted file mode 100644 index 5109e62..0000000 --- a/src/extlib-abc/aig/dar/module.make +++ /dev/null @@ -1,10 +0,0 @@ -SRC += src/aig/dar/darBalance.c \ - src/aig/dar/darCore.c \ - src/aig/dar/darCut.c \ - src/aig/dar/darData.c \ - src/aig/dar/darLib.c \ - src/aig/dar/darMan.c \ - src/aig/dar/darPrec.c \ - src/aig/dar/darRefact.c \ - src/aig/dar/darResub.c \ - src/aig/dar/darScript.c diff --git a/src/extlib-abc/aig/kit/module.make b/src/extlib-abc/aig/kit/module.make deleted file mode 100644 index 8f1d7c6..0000000 --- a/src/extlib-abc/aig/kit/module.make +++ /dev/null @@ -1,10 +0,0 @@ -SRC += src/aig/kit/kitAig.c \ - src/aig/kit/kitBdd.c \ - src/aig/kit/kitCloud.c src/aig/kit/cloud.c \ - src/aig/kit/kitDsd.c \ - src/aig/kit/kitFactor.c \ - src/aig/kit/kitGraph.c \ - src/aig/kit/kitHop.c \ - src/aig/kit/kitIsop.c \ - src/aig/kit/kitSop.c \ - src/aig/kit/kitTruth.c diff --git a/src/extlib-constbv/Makefile b/src/extlib-constbv/Makefile index 4c76444..99e4f21 100644 --- a/src/extlib-constbv/Makefile +++ b/src/extlib-constbv/Makefile @@ -4,15 +4,16 @@ include $(TOP)/scripts/Makefile.common SRCS = $(wildcard *.cpp) OBJS = $(SRCS:.cpp=.o) -libconstantbv.a: $(OBJS) depend - $(AR) rc $@ $(OBJS) - $(RANLIB) $@ + +libconstantbv.a: $(OBJS) + $(RM) $@ + $(AR) qcs $@ $^ .PHONY: clean -clean: - rm -rf *.o *~ *.a .#* depend +clean: + $(RM) *.o *~ *.a .#* depend depend: $(SRCS) - @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ + @$(call makedepend,$@,$(SRCS)) -#-include depend \ No newline at end of file +-include depend diff --git a/src/main/Makefile b/src/main/Makefile index ca2ef94..04d3fc5 100644 --- a/src/main/Makefile +++ b/src/main/Makefile @@ -1,45 +1,36 @@ TOP = ../.. include $(TOP)/scripts/Makefile.common -SRCS=main.cpp versionString.cpp Globals.cpp +SRCS = main.cpp versionString.cpp Globals.cpp OBJS = $(SRCS:.cpp=.o) -CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE) - -LIBS = -L../STPManager -lstpmgr \ - -L../absrefine_counterexample -labstractionrefinement \ - -L../to-sat -ltosat \ - -L../simplifier -lsimplifier \ - -L../printer -lprinter \ - -L../AST -last \ - -L../extlib-constbv -lconstantbv \ - -L../sat -lminisat \ - -L../parser -lparser \ - -L../extlib-abc -labc - -# This rebuilds each time, because the target "parser" is not created -# Until the dependencies on each of the libraries is included, that's safest. -parser: $(OBJS) depend - $(CXX) $(CXXFLAGS) -I$(MTL) $(LDFLAGS) $(OBJS) $(LIBS) -o stp - @mv stp ../../bin/stp - -#.PHONY: clean -clean: - rm -rf *.o *~ *.a .#* depend versionString.cpp - -# Use svnversion to output the global revision number. -# This will be updated every time make is called. -# Because main.cpp depends on this, -# it will in turn be rebuilt every time. -versionString.cpp: ALWAYS_RUN - @echo "#include " > versionString.cpp - @echo "namespace BEEV{extern const std::string version=\"" $(shell svnversion ..) "\";}" >> versionString.cpp - -ALWAYS_RUN: -depend: $(SRCS) - @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ +# Build as a library; final linking to an executable will be done by the +# topmost Makefile. +libmain.a: $(filter-out main.o,$(OBJS)) | main.o + $(RM) $@ + $(AR) qcs $@ $^ + +.PHONY: clean +clean: + $(RM) *.o *~ *.a .#* depend versionString.stamp versionString.cpp + +# Use svnversion to output the global revision number. +versionString.stamp: FORCE + @SVNVERSION=`svnversion $(TOP)`; \ + if [ x`cat $@ 2> /dev/null` != x$$SVNVERSION ]; then \ + echo $$SVNVERSION > $@; \ + fi +# FIXME: there's some sort of memory error that causes "make regressstp" +# to fail if version isn't at least 3 characters long. +versionString.cpp: versionString.stamp + @echo "#include " > $@ + @echo "namespace BEEV{extern const std::string version = \" `cat $^` \";}" >> $@ +FORCE: + +depend: $(SRCS) + @$(call makedepend,$@,$(SRCS)) -#-include depend +-include depend diff --git a/src/parser/Makefile b/src/parser/Makefile index 9997c05..9e2fe1c 100644 --- a/src/parser/Makefile +++ b/src/parser/Makefile @@ -7,13 +7,11 @@ YACC=bison -d -y --debug -v SRCS = lexCVC.cpp parseCVC.cpp parseSMT.cpp lexSMT.cpp LetMgr.cpp parse2SMT.cpp lex2SMT.cpp OBJS = $(SRCS:.cpp=.o) -LIBS = -L../AST -last -L../sat -lminisat -L../simplifier -lsimplifier -L../bitvec -lconsteval -L../constantbv -lconstantbv -CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE) + libparser.a: $(OBJS) - rm -f $@ - $(AR) rc $@ $^ - $(RANLIB) $@ + $(RM) $@ + $(AR) qcs $@ $^ lexCVC.cpp: CVC.lex parseCVC_defs.h ../AST/AST.h $(LEX) -olexCVC.cpp -Pcvc CVC.lex @@ -28,7 +26,7 @@ parseCV%_defs.h parseCV%.cpp: CVC.y @cp cvc.tab.h parseCVC_defs.h lexSMT.cpp: parseSMT_defs.h smtlib.lex ../AST/AST.h - $(LEX) -olexSMT.cpp -Psmt smtlib.lex + $(LEX) -olexSMT.cpp -Psmt smtlib.lex parseSM%_defs.h parseSM%.cpp:smtlib.y $(YACC) -o smt.tab.c -p smt smtlib.y @@ -36,14 +34,19 @@ parseSM%_defs.h parseSM%.cpp:smtlib.y @cp smt.tab.h parseSMT_defs.h lex2SMT.cpp: parse2SMT_defs.h smtlib2.lex ../AST/AST.h - $(LEX) -olex2SMT.cpp -Psmt2 smtlib2.lex + $(LEX) -olex2SMT.cpp -Psmt2 smtlib2.lex parse2SM%_defs.h parse2SM%.cpp:smtlib2.y $(YACC) -o smt2.tab.c -p smt2 smtlib2.y @cp smt2.tab.c parse2SMT.cpp @cp smt2.tab.h parse2SMT_defs.h +clean: + $(RM) *.o parseCVC_defs.h parseSMT_defs.h *~ lexSMT.cpp parseSMT.cpp lexCVC.cpp parseCVC.cpp *.output smt.tab.* smt2.tab.* cvc.tab.* lex.yy.c libparser.a parse2SMT.cpp parse2SMT_defs.h lex2SMT.cpp .#* +ifeq (,$(filter clean configclean distclean,$(MAKECMDGOALS))) +depend: $(SRCS) + @$(call makedepend,$@,$(SRCS)) -clean: - rm -rf *.o parseCVC_defs.h parseSMT_defs.h *~ lexSMT.cpp parseSMT.cpp lexCVC.cpp parseCVC.cpp *.output parser smt.tab.* smt2.tab.* cvc.tab.* lex.yy.c libparser.a parse2SMT.cpp parse2SMT_defs.h lex2SMT.cpp .#* +-include depend +endif diff --git a/src/printer/Makefile b/src/printer/Makefile index 1f54b47..5327a78 100644 --- a/src/printer/Makefile +++ b/src/printer/Makefile @@ -1,22 +1,21 @@ TOP = ../.. include $(TOP)/scripts/Makefile.common -SRCS=$(wildcard *.cpp) +SRCS = $(wildcard *.cpp) OBJS = $(SRCS:.cpp=.o) -CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE) + #Make the ast library for use by other modules -libprinter.a:$(OBJS) depend - -rm -rf $@ - $(AR) rc $@ $(OBJS) - $(RANLIB) $@ +libprinter.a: $(OBJS) + $(RM) $@ + $(AR) qcs $@ $^ .PHONY: clean clean: - rm -rf *.o *~ *.a depend + $(RM) *.o *~ *.a .#* depend depend: $(SRCS) - @$(CXX) -MM -MG $(CXXFLAGS) $(SRCS) > $@ + @$(call makedepend,$@,$(SRCS)) --include ./depend +-include depend diff --git a/src/sat/Makefile b/src/sat/Makefile index 4559688..4a4f3f2 100644 --- a/src/sat/Makefile +++ b/src/sat/Makefile @@ -1,21 +1,22 @@ TOP = ../.. include $(TOP)/scripts/Makefile.common -SRCS=$(wildcard *.cpp) -OBJS=$(SRCS:.cpp=.o) -LIB=libminisat.a +SRCS = $(wildcard *.cpp) +OBJS = $(SRCS:.cpp=.o) +LIB = libminisat.a # exported variables override those set in recursive makefiles. export COPTIMIZE=$(CFLAGS_M32) $(CFLAGS_FPIC) -O3 + .PHONY:core core: $(LIB) # $(LIB) depends on */lib_release.a and will be rebuilt only if they have been updated $(LIB): core/lib_release.a simp/lib_release.a utils/lib_release.a cryptominisat2/libminisat.a $(OBJS) $(RM) $@ - $(AR) cq $@ $(filter-out %/Main.or,$(wildcard core/*.or simp/*.or utils/*.or cryptominisat2/*.o)) $(OBJS) - $(RANLIB) $@ + $(call arcat,$@,$(filter %.a,$^)) + $(AR) qcs $@ $(filter %.o,$^) core/lib_release.a: FORCE $(MAKE) -C core libr @@ -29,7 +30,7 @@ FORCE: .PHONY: clean clean: - $(RM) *.o *~ $(LIB) + $(RM) *.o *~ *.a .#* $(MAKE) -C core clean $(MAKE) -C simp clean $(MAKE) -C utils clean diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile index f33e25b..dbe77b4 100644 --- a/src/sat/cryptominisat2/Makefile +++ b/src/sat/cryptominisat2/Makefile @@ -17,13 +17,18 @@ CFLAGS += -I../.. -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_ EXEC = minisat LFLAGS = -lz + all: $(LIB) #$(EXEC) lib: $(LIB) $(LIB): $(OBJECTS) $(RM) $@ - $(AR) cq $@ $^ - $(RANLIB) $@ + $(AR) qcs $@ $^ clean: - $(RM) $(OBJECTS) $(LIB) + $(RM) *.o *~ *.a .#* depend + +depend: $(SOURCES) + @$(call makedepend,$@,$(SOURCES)) + +-include depend diff --git a/src/sat/mtl/template.mk b/src/sat/mtl/template.mk index 01c4036..103582e 100644 --- a/src/sat/mtl/template.mk +++ b/src/sat/mtl/template.mk @@ -88,7 +88,8 @@ libs libp libd libr: ## Clean rule clean: - @rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \ + @$(RM) $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \ + lib$(LIB).a lib$(LIB)_standard.a lib$(LIB)_profile.a lib$(LIB)_release.a lib$(LIB)_debug.a \ $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mk ## Make dependencies diff --git a/src/simplifier/Makefile b/src/simplifier/Makefile index af46f14..66fb46c 100644 --- a/src/simplifier/Makefile +++ b/src/simplifier/Makefile @@ -5,17 +5,16 @@ SRCS = $(wildcard *.cpp) SRCS += $(wildcard constantBitP/*.cpp) OBJS = $(SRCS:.cpp=.o) -CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE) -libsimplifier.a:$(OBJS) depend - $(AR) rc $@ $(OBJS) - $(RANLIB) $@ +libsimplifier.a: $(OBJS) + $(RM) $@ + $(AR) qcs $@ $^ .PHONY: clean -clean: - rm -rf *.o *~ *.a .#* depend constantBitP/*.o +clean: + $(RM) *.o */*.o *~ *.a .#* depend depend: $(SRCS) - @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ + @$(call makedepend,$@,$(SRCS)) -include depend diff --git a/src/to-sat/Makefile b/src/to-sat/Makefile index 05b3338..8fe5d80 100644 --- a/src/to-sat/Makefile +++ b/src/to-sat/Makefile @@ -6,17 +6,15 @@ SRCS += $(wildcard AIG/*.cpp) SRCS += $(wildcard ASTNode/*.cpp) OBJS = $(SRCS:.cpp=.o) -CFLAGS += -I$(MTL) -I$(SOLVER_INCLUDE) - -libtosat.a: $(OBJS) depend - $(AR) rc $@ $(OBJS) - $(RANLIB) $@ +libtosat.a: $(OBJS) + $(RM) $@ + $(AR) qcs $@ $^ .PHONY: clean -clean: - rm -rf *.o *~ *.a .#* depend AIG/*.o ASTNode/*.o +clean: + $(RM) *.o */*.o *~ *.a .#* depend depend: $(SRCS) - @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@ + @$(call makedepend,$@,$(SRCS)) --include depend +-include depend diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile index 048c49f..e5392f7 100644 --- a/tests/c-api-tests/Makefile +++ b/tests/c-api-tests/Makefile @@ -101,4 +101,4 @@ all: 0 1 2 3 4 5 6 7 8 9 10 11 11 12 13 14 15 16 17 18 19 20 21 22 23 clean: - rm -rf *~ *.out + rm -rf *~ *.out *.dSYM -- 2.47.3