#CFLAGS_FPIC = -fPIC
CFLAGS_FPIC =
-#-fno-inline
CFLAGS_BASE = $(OPTIMIZE)
-CFLAGS_BASE = $(OPTIMIZE)
ifeq ($(WITHCBITP),yes)
ifdef STATIC
LDFLAGS_BASE = -static-libgcc -static
-else
- LDFLAGS_BASE = -lstdc++
endif
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
LEX = flex
YACC = bison -d -y --debug -v
-RANLIB = ranlib
+
+
+# Run gcc to generate dependency rules for object files; use as follows:
+# <dependency file> : <input files>
+# $(call makedepend,<dependency file>,<input files>)
+# -include <dependency file>
+#
+# 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 <dependency file>
+#
+# Note: do not use $^ as <input files>, since additional dependencies will be
+# added to the dependency list of <dependency file>.
+#
+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
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:
####
$(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
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
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
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
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
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
+++ /dev/null
-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
+++ /dev/null
-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
+++ /dev/null
-SRC += src/aig/kit/kitAig.c \\r
- src/aig/kit/kitBdd.c \\r
- src/aig/kit/kitCloud.c src/aig/kit/cloud.c \\r
- src/aig/kit/kitDsd.c \\r
- src/aig/kit/kitFactor.c \\r
- src/aig/kit/kitGraph.c \\r
- src/aig/kit/kitHop.c \\r
- src/aig/kit/kitIsop.c \\r
- src/aig/kit/kitSop.c \\r
- src/aig/kit/kitTruth.c\r
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
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 <string>" > 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 <string>" > $@
+ @echo "namespace BEEV{extern const std::string version = \" `cat $^` \";}" >> $@
+FORCE:
+
+depend: $(SRCS)
+ @$(call makedepend,$@,$(SRCS))
-#-include depend
+-include depend
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
@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
@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
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
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
.PHONY: clean
clean:
- $(RM) *.o *~ $(LIB)
+ $(RM) *.o *~ *.a .#*
$(MAKE) -C core clean
$(MAKE) -C simp clean
$(MAKE) -C utils clean
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
## 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
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
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
clean:
- rm -rf *~ *.out
+ rm -rf *~ *.out *.dSYM
projects / francis / stp.git / commitdiff