From: smccam <smccam@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 18 Dec 2010 01:23:07 +0000 (+0000)
Subject: Makefile changes to improve the build of libstp.a. Don't include
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=7d4e01ecbd740f5cc1620c77e21c7112c1e7f396;p=francis%2Fstp.git

Makefile changes to improve the build of libstp.a. Don't include
Main.or files from MiniSAT, since we don't need them, and they bring
in main() functions and zlib dependencies we don't want. Add a c-api
test to try to keep this from regressing again.
Make it easier to pass -fPIC through to the MiniSAT build.
Clean up some comments and trailing whitespace in Makefiles.


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

diff --git a/scripts/Makefile.common b/scripts/Makefile.common
index 71292bf..a0115a8 100644
--- a/scripts/Makefile.common
+++ b/scripts/Makefile.common
@@ -26,6 +26,11 @@ OPTIMIZE      = -O3  -g            # Maximum optimization
 #2) You need STP to use about half the memory.
 #CFLAGS_M32   = -m32
 
+# If you're compiling a 64-bit version of STP, and you want to use
+# libstp.a in a shared library, you need the -fPIC option.
+#CFLAGS_FPIC = -fPIC
+CFLAGS_FPIC =
+
 #-fno-inline
 CFLAGS_BASE   = $(OPTIMIZE)
 CFLAGS_BASE    = $(OPTIMIZE) 
@@ -70,8 +75,7 @@ ifeq ($(shell uname -s), DarwinX)
   CFLAGS = -isysroot $(UNIVERSAL_SDK) $(UNIVERSAL_ARCH) $(CFLAGS_BASE)
 else
   LDFLAGS = $(LDFLAGS_BASE)
-  CFLAGS = $(CFLAGS_BASE)		
-  CFLAGS = $(CFLAGS_BASE) $(CFLAGS_M32) -I../AST
+  CFLAGS = $(CFLAGS_BASE) $(CFLAGS_M32) $(CFLAGS_FPIC) -I../AST
 endif
 
 # Used by Doug Lea's malloc that I added into minisat2.
diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index cb6f336..be4ea84 100644
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -33,8 +33,8 @@ all: AST STPManager absrefine_counterexample to-sat simplifier printer c_interfa
 			   $(SRC)/to-sat/*.o \
 		       $(SRC)/to-sat/AIG/*.o  \
 			   $(SRC)/sat/*.o \
-			   $(SRC)/sat/core/*.o? \
-			   $(SRC)/sat/simp/*.o? \
+			   $(SRC)/sat/core/Solver.or \
+			   $(SRC)/sat/simp/SimpSolver.or \
 			   $(SRC)/sat/utils/*.o \
 			   $(SRC)/simplifier/*.o  \
 		       $(SRC)/simplifier/constantBitP/*.o  \
@@ -118,7 +118,7 @@ regressall: all
 	$(MAKE) regresscrypto
 	$(MAKE) unit_test
 	$(MAKE) regresscapi
-	
+
 
 # Checks that simplifications are working.
 .PHONY: unit_test
diff --git a/src/sat/Makefile b/src/sat/Makefile
index 57de857..db8e1a3 100644
--- a/src/sat/Makefile
+++ b/src/sat/Makefile
@@ -10,11 +10,11 @@ COPTIMIZE="-O3 -m32"
 
 .PHONY:core
 core: $(OBJS)
-	#Command line variables override those set in the makefile.
-	$(MAKE) -C core libr COPTIMIZE="$(CFLAGS_M32) -O3"
-	$(MAKE) -C simp libr COPTIMIZE="$(CFLAGS_M32) -O3"
+	@ #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"
 	$(MAKE) -C cryptominisat2 lib all
-	
+	@#
 	rm -f $(LIB)
 	ar cq $(LIB) ./core/*.or ./simp/*.or *.o utils/*.o *.o
 	ranlib $(LIB)
diff --git a/tests/c-api-tests/Makefile b/tests/c-api-tests/Makefile
index 9e2f509..048c49f 100644
--- a/tests/c-api-tests/Makefile
+++ b/tests/c-api-tests/Makefile
@@ -2,8 +2,9 @@
 # either leak, or use of unitialised values.
 TOP = ../..
 include $(TOP)/scripts/Makefile.common
-CXXFLAGS= -DEXT_HASH_MAP $(CFLAGS) -I../../src/c_interface -L../../lib 
-LIBS= -lstp 
+CXXFLAGS= -DEXT_HASH_MAP $(CFLAGS) -I../../src/c_interface
+LDFLAGS=-L../../lib
+LIBS=$(LDFLAGS) -lstp 
 
 VALGRINDPATH=`which valgrind`
 ifeq   "$(VALGRINDPATH)" ""
@@ -13,7 +14,7 @@ else
 endif
 
 
-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
+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
 	rm -rf *.out
 
 0:	
@@ -90,5 +91,14 @@ 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
 	g++ $(CXXFLAGS) parsestring-using-cinterface.c -o a22.out $(LIBS)
 	./a22.out
 
+# Test 23 is the same as test 0, except linked in a different order.
+# This is meant to catch problems in which libstp.a contains a
+# main() function or has extra dependencies.
+23:
+	g++ $(CXXFLAGS) -o a23.out \
+         ../../lib/libstp.a array-cvcl-02.c ../../lib/libstp.a
+	./a23.out
+
+
 clean:
 	rm -rf *~ *.out