Update make files so that the "-j" option will work.

On my machine (see trace below), with 4 cores, make is about 3 times quicker with the -j option.

=================

~/svn/stp-trunk$ make clean > /dev/null 2>&1
~/svn/stp-trunk$ time make > /dev/null 2>&1

real	0m45.615s
user	0m41.955s
sys	0m3.152s
~/svn/stp-trunk$ clean > /dev/null 2>&1
~/svn/stp-trunk$ time make -j > /dev/null 2>&1

real	0m17.616s
user	0m44.771s
sys	0m3.744s

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

diff --git a/Makefile b/Makefile
index 4e0bb863fa8f513490c3355039b8e6dc696a180c..2bce0e0886ef55d457c16d4cf6fefb21831ad2f5 100644 (file)
--- a/Makefile
+++ b/Makefile
@@ -16,14 +16,8 @@ LIBRARIES=lib/libstp.a
 HEADERS=$(SRC)/c_interface/*.h
 
 .PHONY: all
-all:
-       $(MAKE) -C $(SRC)/AST
-       $(MAKE) -C $(SRC)/STPManager
-       $(MAKE) -C $(SRC)/printer
-       $(MAKE) -C $(SRC)/extlib-constbv
-       $(MAKE) -C $(SRC)/simplifier
-       $(MAKE) -C $(SRC)/absrefine_counterexample
-       $(MAKE) -C $(SRC)/to-sat
+all: AST STPManager absrefine_counterexample to-sat simplifier printer c_interface extlib-constbv
+
 ifdef CRYPTOMINISAT
        $(MAKE) -C $(SRC)/sat cryptominisat
 else
@@ -31,7 +25,6 @@ else
 #      $(MAKE) -C $(SRC)/sat simp
 #      $(MAKE) -C $(SRC)/sat unsound
 endif
-       $(MAKE) -C $(SRC)/c_interface
        $(MAKE) -C $(SRC)/parser
        $(MAKE) -C $(SRC)/main
        $(AR) rc libstp.a  $(SRC)/AST/*.o $(SRC)/STPManager/*.o $(SRC)/printer/*.o $(SRC)/absrefine_counterexample/*.o \
@@ -45,6 +38,18 @@ endif
        @echo "Compilation successful."
        @echo "Type 'make install' to install STP."
 
+#
+# 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.
+
+.PHONY: AST
+AST: 
+       $(MAKE) -C $(SRC)/$@
+
+STPManager absrefine_counterexample to-sat simplifier printer c_interface extlib-constbv: AST
+       $(MAKE) -C $(SRC)/$@
+
+####
 
 .PHONY: install
 install: all

diff --git a/scripts/Makefile.in b/scripts/Makefile.in
index 4e0bb863fa8f513490c3355039b8e6dc696a180c..2bce0e0886ef55d457c16d4cf6fefb21831ad2f5 100644 (file)
--- a/scripts/Makefile.in
+++ b/scripts/Makefile.in
@@ -16,14 +16,8 @@ LIBRARIES=lib/libstp.a
 HEADERS=$(SRC)/c_interface/*.h
 
 .PHONY: all
-all:
-       $(MAKE) -C $(SRC)/AST
-       $(MAKE) -C $(SRC)/STPManager
-       $(MAKE) -C $(SRC)/printer
-       $(MAKE) -C $(SRC)/extlib-constbv
-       $(MAKE) -C $(SRC)/simplifier
-       $(MAKE) -C $(SRC)/absrefine_counterexample
-       $(MAKE) -C $(SRC)/to-sat
+all: AST STPManager absrefine_counterexample to-sat simplifier printer c_interface extlib-constbv
+
 ifdef CRYPTOMINISAT
        $(MAKE) -C $(SRC)/sat cryptominisat
 else
@@ -31,7 +25,6 @@ else
 #      $(MAKE) -C $(SRC)/sat simp
 #      $(MAKE) -C $(SRC)/sat unsound
 endif
-       $(MAKE) -C $(SRC)/c_interface
        $(MAKE) -C $(SRC)/parser
        $(MAKE) -C $(SRC)/main
        $(AR) rc libstp.a  $(SRC)/AST/*.o $(SRC)/STPManager/*.o $(SRC)/printer/*.o $(SRC)/absrefine_counterexample/*.o \
@@ -45,6 +38,18 @@ endif
        @echo "Compilation successful."
        @echo "Type 'make install' to install STP."
 
+#
+# 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.
+
+.PHONY: AST
+AST: 
+       $(MAKE) -C $(SRC)/$@
+
+STPManager absrefine_counterexample to-sat simplifier printer c_interface extlib-constbv: AST
+       $(MAKE) -C $(SRC)/$@
+
+####
 
 .PHONY: install
 install: all

diff --git a/src/AST/Makefile b/src/AST/Makefile
index 63c58140e82b38dee486e9acf588b068e6ef8551..5fa33a1fec342970f1109f971f3181abb8e9ab52 100644 (file)
--- a/src/AST/Makefile
+++ b/src/AST/Makefile
@@ -17,9 +17,11 @@ ASTKind.h ASTKind.cpp:       ASTKind.kinds genkinds.pl
 
 .PHONY: clean
 clean:
-       rm -rf *.o *~ bbtest asttest cnftest *.a  ASTKind.cpp ASTKind.h depend .#*
+       rm -rf *.o *~ *.a  ASTKind.cpp ASTKind.h depend .#*
 
-depend: $(SRCS) ASTKind.h ASTKind.cpp
+#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) > $@
 
 -include ./depend

diff --git a/src/parser/Makefile b/src/parser/Makefile
index 210d0dd8f8b4c45c6d8c6b1c602245ff8bb78ed2..1c088dc2f9d0da29b35a36b2bac02fcdd8acd223 100644 (file)
--- a/src/parser/Makefile
+++ b/src/parser/Makefile
@@ -15,18 +15,21 @@ libparser.a: $(OBJS)
 lexCVC.cpp:    CVC.lex parseCVC_defs.h ../AST/AST.h
                $(LEX)  -olexCVC.cpp -Pcvc CVC.lex
 
-parseCVC_defs.h parseCVC.cpp:  CVC.y
-               $(YACC) -p cvc CVC.y
-               @cp y.tab.c parseCVC.cpp
-               @cp y.tab.h parseCVC_defs.h
+#For rules with multiple targets. Make runs the rule once for each target. 
+#These rules are "pattern rules" which only run once (rather than twice).
+parseCV%_defs.h parseCV%.cpp:  CVC.y
+               $(YACC) -o cvc.tab.c -p cvc CVC.y
+               @cp  cvc.tab.c parseCVC.cpp
+               @cp  cvc.tab.h parseCVC_defs.h
 
 lexSMT.cpp:    parseSMT_defs.h smtlib.lex ../AST/AST.h
-               $(LEX) -olexSMT.cpp -Psmt smtlib.lex 
+               $(LEX) -o lexSMT.cpp --prefix smt smtlib.lex 
+
+parseSM%_defs.h parseSM%.cpp:smtlib.y
+               $(YACC) -o smt.tab.c -p smt smtlib.y
+               @cp  smt.tab.c parseSMT.cpp
+               @cp  smt.tab.h parseSMT_defs.h
 
-parseSMT_defs.h parseSMT.cpp:smtlib.y
-               $(YACC) -p smt smtlib.y
-               @cp y.tab.c parseSMT.cpp
-               @cp y.tab.h parseSMT_defs.h
 
 clean: 
-               rm -rf *.o *.a parseCVC_defs.h parseSMT_defs.h *~ lexSMT.cpp parseSMT.cpp lexCVC.cpp parseCVC.cpp *.output parser y.tab.* lex.yy.c .#*
+       rm -rf *.o parseCVC_defs.h parseSMT_defs.h *~ lexSMT.cpp parseSMT.cpp lexCVC.cpp parseCVC.cpp *.output parser smt.tab.* cvc.tab.* lex.yy.c .#*
\ No newline at end of file

diff --git a/src/sat/core/Makefile b/src/sat/core/Makefile
index 50d1c0404c36ad114bf5e7cada0cf9e285753821..eb2bee27a4cbfb7f015b9062df4a3d395e918f85 100644 (file)
--- a/src/sat/core/Makefile
+++ b/src/sat/core/Makefile
@@ -6,7 +6,7 @@ CFLAGS    += -I$(MTL) -Wall -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32)
 LFLAGS    = -lz
 
 include ../mtl/template.mk
-all:
+all: libminisat.a
        ranlib libminisat.a
        cp *.or ../
        cp libminisat.a ../