Patch from Khoo Yit Phang.

Clean up the build system of MiniSat.
- Set up dependencies for recursive Makefile to avoid unnecessary rebuilds.
- Correctly propagate configuration to recursive Makefiles by exporting flags and removing unnecessary rules.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1123 e59a4935-1847-0410-ae03-e826735625c1

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index d9260934af8601a03895ecc0e24f0e360a40fb5a..8ba2fc265e7b09afa5ce9f46ff91707def2aba1f 100644 (file)
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -29,16 +29,17 @@ all: AST STPManager absrefine_counterexample to-sat simplifier printer c_interfa
                           $(SRC)/AST/NodeFactory/*.o \
                           $(SRC)/STPManager/*.o \
                           $(SRC)/printer/*.o \
-                          $(SRC)/absrefine_counterexample/*.o \
+                          $(SRC)/absrefine_counterexample/*.o \
                           $(SRC)/to-sat/*.o \
-                      $(SRC)/to-sat/AIG/*.o  \
-                      $(SRC)/to-sat/ASTNode/*.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/*.o \
+                          $(SRC)/sat/utils/System.or \
+                          $(SRC)/sat/cryptominisat2/*.o \
                           $(SRC)/simplifier/*.o  \
-                      $(SRC)/simplifier/constantBitP/*.o  \
+                          $(SRC)/simplifier/constantBitP/*.o  \
                           $(SRC)/extlib-constbv/*.o \
                           $(SRC)/extlib-abc/*/*/*.o \
                           $(SRC)/c_interface/*.o \

diff --git a/src/sat/Makefile b/src/sat/Makefile
index db8e1a38cf0d23cd25e5808cdcd0d8c0d7d34d2f..455968839039786480a684a723f38e275ffff52d 100644 (file)
--- a/src/sat/Makefile
+++ b/src/sat/Makefile
@@ -1,30 +1,38 @@
 TOP = ../..
 include $(TOP)/scripts/Makefile.common
 
-SRCS=$(wildcard  *.cpp)
+SRCS=$(wildcard *.cpp)
 OBJS=$(SRCS:.cpp=.o)
-SRCS+=utils/System.cc
-OBJS+=utils/System.o
 LIB=libminisat.a
-COPTIMIZE="-O3 -m32"
+
+# exported variables override those set in recursive makefiles.
+export COPTIMIZE=$(CFLAGS_M32) $(CFLAGS_FPIC) -O3
 
 .PHONY:core
-core: $(OBJS)
-       @ #Command line variables override those set in the makefile.
-       $(MAKE) -C core libr COPTIMIZE="$(CFLAGS_M32) $(CFLAGS_FPIC) -O3"
-       $(MAKE) -C simp libr COPTIMIZE="$(CFLAGS_M32) $(CFLAGS_FPIC) -O3"
+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) $@
+
+core/lib_release.a: FORCE
+       $(MAKE) -C core libr
+simp/lib_release.a: FORCE
+       $(MAKE) -C simp libr
+utils/lib_release.a: FORCE
+       $(MAKE) -C utils libr
+cryptominisat2/libminisat.a: FORCE
        $(MAKE) -C cryptominisat2 lib all
-       @#
-       rm -f $(LIB)
-       ar cq $(LIB) ./core/*.or ./simp/*.or *.o utils/*.o *.o
-       ranlib $(LIB)
+FORCE:
 
 .PHONY: clean
 clean:
-       rm -rf *.o core/*.o *~ $(LIB)
+       $(RM) *.o *~ $(LIB)
        $(MAKE) -C core    clean
        $(MAKE) -C simp    clean
+       $(MAKE) -C utils   clean
        $(MAKE) -C cryptominisat2 clean
 
-CryptoMinisat.o: CryptoMinisat.cpp
-       $(CC) $(CFLAGS) -Icryptominisat2/mtl -Imtl CryptoMinisat.cpp -c -I$(TOP)/src
+CryptoMinisat.o: CFLAGS += -Icryptominisat2/mtl -Imtl -I$(TOP)/src

diff --git a/src/sat/cryptominisat2/Makefile b/src/sat/cryptominisat2/Makefile
index eebe5fc2715480784fb7835d7a53355df48660b5..f33e25b81f4ca61e623e67dccf22e0679099a96a 100644 (file)
--- a/src/sat/cryptominisat2/Makefile
+++ b/src/sat/cryptominisat2/Makefile
@@ -13,7 +13,7 @@ SOURCES   = Logger.cpp Solver.cpp PackedRow.cpp \
            OnlyNonLearntBins.cpp
 OBJECTS   = $(SOURCES:.cpp=.o)
 LIB       = libminisat.a
-CFLAGS    += -I../.. -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c 
+CFLAGS    += -I../.. -I$(MTL) -I$(MTRAND) -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) -c
 EXEC      = minisat
 LFLAGS    = -lz
 
@@ -21,14 +21,9 @@ all: $(LIB) #$(EXEC)
 lib: $(LIB)
 
 $(LIB): $(OBJECTS)
-       rm -f $@
-       ar cq $@ $(OBJECTS)
-       ranlib $@
-       cp $(LIB) ../
-       cp $(OBJECTS) ../
+       $(RM) $@
+       $(AR) cq $@ $^
+       $(RANLIB) $@
 
 clean:
-       rm -f $(OBJECTS) $(LIB)
-
-.cpp.o:
-       $(CC) $(CFLAGS) $< -o $@
+       $(RM) $(OBJECTS) $(LIB)

diff --git a/src/sat/utils/Makefile b/src/sat/utils/Makefile
index 204cea5418642ed534d358c76ca1774156fab13f..09026eabf0f7bb17c67aed645768a5f012e3d22b 100644 (file)
--- a/src/sat/utils/Makefile
+++ b/src/sat/utils/Makefile
@@ -1,4 +1,5 @@
 EXEC      = system_test
 DEPDIR    = mtl
+MROOT     = ..
 
 include $(MROOT)/mtl/template.mk