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 71292bfafdd861d6672b106822d1ce4d6a8fc5f2..a0115a86a5ceafab1ac825fe426d969099c9f420 100644 (file)
--- 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 cb6f336a773b1784fb64f6f9392d12a8c1c74b89..be4ea8495ce700522846856cd7012dd832544835 100644 (file)
--- 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 57de857b8b9a4233c733bc745b388e3ac2dd7598..db8e1a38cf0d23cd25e5808cdcd0d8c0d7d34d2f 100644 (file)
--- 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 9e2f509454faefbcd4291a593312d1e5b1fe9f68..048c49f87081f5634318784fb73646def9496b0f 100644 (file)
--- 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