* Automatically build dependencies during make. This isn't perfect because the depend...

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

diff --git a/src/AST/Makefile b/src/AST/Makefile
index 186f0cf8e607378a1b98e5f01e60d31fc71c5987..579d4db37f87cff9e2471d55c36cf470d14d19a5 100644 (file)
--- a/src/AST/Makefile
+++ b/src/AST/Makefile
@@ -17,10 +17,10 @@ ASTKind.h ASTKind.cpp:      ASTKind.kinds genkinds.pl
 
 .PHONY: clean
 clean:
-       rm -rf *.o *~ bbtest asttest cnftest *.a  ASTKind.h ASTKind.cpp .#*
+       rm -rf *.o *~ bbtest asttest cnftest *.a  ASTKind.h ASTKind.cpp .#* depend
        rm -rf printer/*.o
 
 depend: $(SRCS)
-       $(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
+       @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
 
 -include depend

diff --git a/src/AST/TestAST/asttest.cpp b/src/AST/TestAST/asttest.cpp
index 1baafe5bcb8211ea21db22d29d65dc0d6b14741a..1e33ca9edb5496df9e23b3a03048fe868a643dc9 100644 (file)
--- a/src/AST/TestAST/asttest.cpp
+++ b/src/AST/TestAST/asttest.cpp
@@ -1,4 +1,4 @@
-#include "AST.h"
+#include "../AST.h"
 
 using namespace BEEV;
 

diff --git a/src/abstraction-refinement/Makefile b/src/abstraction-refinement/Makefile
index 2ad347305c2d72ac253cf3ba4ee75e5801e6455f..c1543c18eeb5b62f53831995f1f915ebcb4501c6 100644 (file)
--- a/src/abstraction-refinement/Makefile
+++ b/src/abstraction-refinement/Makefile
@@ -1,12 +1,17 @@
 include ../../scripts/Makefile.common
 
-SRCS = AbstractionRefinement.cpp
+SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)
-CFLAGS += -I../sat/mtl -I../sat/simp -I../sat/core
 
-libabstractionrefinement.a:    $(OBJS)
-                               $(AR) rc $@ $^
+libabstractionrefinement.a:    $(OBJS) depend
+                               $(AR) rc $@ $(OBJS)
                                $(RANLIB) $@
 
 clean: 
-                               rm -rf *.o *~ *.a .#*
+                               rm -rf *.o *~ *.a .#* depend
+
+depend: $(SRCS)
+       @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
+
+-include depend
+                               
\ No newline at end of file

diff --git a/src/bitvec/Makefile b/src/bitvec/Makefile
index 1a864f747fcb6c54405e2d3cecc9e833c790a5ce..c83b8c5181743f37d3c7cc68b29f7e6b8936c066 100644 (file)
--- a/src/bitvec/Makefile
+++ b/src/bitvec/Makefile
@@ -1,12 +1,18 @@
 include ../../scripts/Makefile.common
 
-SRCS = consteval.cpp
+SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)
-CFLAGS += -I../sat/mtl -I../sat/core -I../sat/simp
 
-libconsteval.a: $(OBJS)
-       $(AR) rc $@ $^
+libconsteval.a: $(OBJS) depend
+       $(AR) rc $@ $(OBJS)
        $(RANLIB) $@
 
+.PHONY: clean
 clean: 
-       rm -rf *.o *~ *.a .#*
+       rm -rf *.o *~ *.a .#* depend
+
+depend: $(SRCS)
+       @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
+
+-include depend
+       
\ No newline at end of file

diff --git a/src/c_interface/Makefile b/src/c_interface/Makefile
index 37cf62efcff0af17903f80b779fd53dfd60fdad2..fef9b4867839aa839906008eb111cc87babf5248 100644 (file)
--- a/src/c_interface/Makefile
+++ b/src/c_interface/Makefile
@@ -1,14 +1,18 @@
 include ../../scripts/Makefile.common
 
-SRCS = c_interface.cpp
+SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)
-CFLAGS += -I../sat/mtl -I../sat/core
 
-libcinterface.a: $(OBJS)
-       $(AR) rc $@ $^
+libcinterface.a: $(OBJS) depend
+       $(AR) rc $@ $(OBJS)
        $(RANLIB) $@
 
+.PHONY: clean
 clean: 
-       rm -rf *.o *~ *.a .#*
+       rm -rf *.o *~ *.a .#* depend
+
+depend: $(SRCS)
+       @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
+
+-include depend
 
-c_interface.o: c_interface.h

diff --git a/src/constantbv/Makefile b/src/constantbv/Makefile
index 58920ad915e4c3cb34ab615267b6d0f315cdd1db..7a4fcd62ef4c7c208f64f65534a71d74ed4f7a1f 100644 (file)
--- a/src/constantbv/Makefile
+++ b/src/constantbv/Makefile
@@ -1,13 +1,17 @@
 include ../../scripts/Makefile.common
 
-SRCS = constantbv.cpp
+SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)
 
-libconstantbv.a: $(OBJS)
-       $(AR) rc $@ $^
+libconstantbv.a: $(OBJS) depend
+       $(AR) rc $@ $(OBJS)
        $(RANLIB) $@
 
+.PHONY: clean
 clean: 
-       rm -rf *.o *~ *.a .#*
+       rm -rf *.o *~ *.a .#* depend
 
-constantbv.o: constantbv.h
+depend: $(SRCS)
+       @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
+
+-include depend

diff --git a/src/main/Makefile b/src/main/Makefile
index af26bcf7b15ee0962f260db8aeee1641d223a452..0fc3a14affb5e35158963ebd6035a59d7ccdc441 100644 (file)
--- a/src/main/Makefile
+++ b/src/main/Makefile
@@ -1,6 +1,6 @@
 include ../../scripts/Makefile.common
 
-SRCS = Globals.cpp main.cpp
+SRCS=$(wildcard  *.cpp)
 OBJS = $(SRCS:.cpp=.o)
 LIBS =         -L../to-sat -ltosat -L../AST -last -L../abstraction-refinement -labstractionrefinement \
        -L../sat -lminisat  \
@@ -8,11 +8,18 @@ LIBS =        -L../to-sat -ltosat -L../AST -last -L../abstraction-refinement -labstrac
         -L../bitvec -lconsteval \
        -L../constantbv -lconstantbv \
        -L../parser -lparser
-CFLAGS += -I../sat/mtl -I../sat/core  -I../sat/simp -I../sat/unsound
 
-parser: Globals.o main.o
-       $(CXX) $(CFLAGS) $(LDFLAGS) Globals.o main.o $(LIBS) -o stp
+#This rebuilds each time, because the target "parser" is not created
+#Until the dependencies on each of the libraries is included, that's safest.
+parser: $(OBJS) depend
+       $(CXX) $(CXXFLAGS) $(LDFLAGS) $(OBJS) $(LIBS) -o stp
        @mv stp ../../bin/stp
 
+.PHONY: clean
 clean: 
-       rm -rf *.o *~ *.a .#*
+       rm -rf *.o *~ *.a .#* depend
+
+depend: $(SRCS)
+       @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
+
+-include depend

diff --git a/src/main/main.cpp b/src/main/main.cpp
index 86da6869e628ce277605032fcd51b764a462e766..9efb839f5ad55e8efec8ae1e37dbcc84aa45720c 100644 (file)
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -7,8 +7,6 @@
  ********************************************************************/
 // -*- c++ -*-
 #include "../AST/AST.h"
-#include "../sat/core/Solver.h"
-#include "../sat/core/SolverTypes.h"
 #include "../AST/printer/AssortedPrinters.h"
 
 #ifdef EXT_HASH_MAP

diff --git a/src/simplifier/Makefile b/src/simplifier/Makefile
index a486b4da0bdfbcabe7c36b3ae4cfcbb198821e43..318b0eb354a6d2c51aa57b323ce5ea8bd6f9e1d2 100644 (file)
--- a/src/simplifier/Makefile
+++ b/src/simplifier/Makefile
@@ -1,12 +1,19 @@
 include ../../scripts/Makefile.common
 
-SRCS = simplifier.cpp bvsolver.cpp
+SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)
 CFLAGS += -I../sat/mtl -I../sat/simp -I../sat/core
 
-libsimplifier.a: $(OBJS)
-       $(AR) rc $@ $^
+libsimplifier.a: $(OBJS) depend
+       $(AR) rc $@ $(OBJS)
        $(RANLIB) $@
 
+.PHONY: clean
 clean: 
-       rm -rf *.o *~ *.a .#*
+       rm -rf *.o *~ *.a .#* depend
+
+depend: $(SRCS)
+       @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
+
+-include depend
+

diff --git a/src/to-sat/Makefile b/src/to-sat/Makefile
index 803615f3ee5183f3338f11c43a28aa3365939780..e8de19812c419d2ee360243011e6a2b5a1ac6aaf 100644 (file)
--- a/src/to-sat/Makefile
+++ b/src/to-sat/Makefile
@@ -1,12 +1,19 @@
 include ../../scripts/Makefile.common
 
-SRCS = BitBlast.cpp SimpBool.cpp ToCNF.cpp ToSAT.cpp
+SRCS = $(wildcard *.cpp)
 OBJS = $(SRCS:.cpp=.o)
 CFLAGS += -I../sat/mtl -I../sat/simp -I../sat/core
 
-libtosat.a:    $(OBJS)
-               $(AR) rc $@ $^
+libtosat.a:    $(OBJS) depend
+               $(AR) rc $@ $(OBJS)
                $(RANLIB) $@
 
+.PHONY: clean
 clean: 
-               rm -rf *.o *~ *.a .#*
+               rm -rf *.o *~ *.a .#* depend
+
+depend: $(SRCS)
+       @$(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
+
+-include depend
+               
\ No newline at end of file