From 7864866866368e73b99e316fa2c693746ee511df Mon Sep 17 00:00:00 2001
From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Tue, 8 Feb 2011 11:48:30 +0000
Subject: [PATCH] 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
---
 scripts/Makefile.in             | 11 +++++-----
 src/sat/Makefile                | 38 ++++++++++++++++++++-------------
 src/sat/cryptominisat2/Makefile | 15 +++++--------
 src/sat/utils/Makefile          |  1 +
 4 files changed, 35 insertions(+), 30 deletions(-)

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index d926093..8ba2fc2 100644
--- 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 db8e1a3..4559688 100644
--- 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 eebe5fc..f33e25b 100644
--- 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 204cea5..09026ea 100644
--- 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
-- 
2.47.3