* Update the AST/Makefile to automatically build a "depend" file that contains the...

* Move AST tests into a test sub-directory.
* Clean up the make file to remove redundant rules, and to use wildcard rules

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

diff --git a/src/AST/Makefile b/src/AST/Makefile
index b9bedad0d0169d6a555070c07be99881a56eb1ad..d976865c541f7676e7e6d256dbee2b1c02345b93 100644 (file)
--- a/src/AST/Makefile
+++ b/src/AST/Makefile
@@ -1,63 +1,26 @@
 include ../../scripts/Makefile.common
 
-#SRCS = AST.cpp ASTKind.cpp  ASTUtil.cpp BitBlast.cpp SimpBool.cpp  ToCNF.cpp DPLLMgr.cpp ToSAT.cpp Transform.cpp
-SRCS = AST.cpp ASTKind.cpp  ASTUtil.cpp BitBlast.cpp SimpBool.cpp  ToCNF.cpp ToSAT.cpp Transform.cpp AbstractionRefinement.cpp printer/AssortedPrinters.cpp printer/SMTLIBPrinter.cpp  printer/dotPrinter.cpp  printer/CPrinter.cpp printer/PLPrinter.cpp printer/LispPrinter.cpp
+SRCS=$(wildcard  *.cpp printer/*.cpp)
+SRCS+= ASTKind.cpp
 OBJS = $(SRCS:.cpp=.o)
 CFLAGS += -I../sat/mtl -I../sat/core
 
 #Make the ast library for use by other modules
-libast.a:      $(OBJS)
+libast.a:      $(OBJS) depend
        -rm -rf $@
-       $(AR) rc libast.a $(OBJS)
-       $(RANLIB) libast.a
-
-ASTKind.o:     ASTKind.kinds
-       $(CXX) $(CXXFLAGS)   -c -o ASTKind.o ASTKind.cpp
+       $(AR) rc $@ $(OBJS)
+       $(RANLIB) $@
 
 # ASTKind.h and ASTKind.cpp are automatically generated
 ASTKind.h ASTKind.cpp: ASTKind.kinds genkinds.pl
        ./genkinds.pl
 
-# cnftest:     cnftest.o ToCNF.o AST.o ASTUtil.o ASTKind.o BitBlast.o AST.h
-#      $(CC) $(LDFLAGS) ToCNF.o BitBlast.o ASTKind.o  ASTUtil.o AST.o  cnftest.o  -o cnftest 
-
-# bbtest: $(OBJS)
-#      $(CC) $(LDFLAGS) BitBlast.o ASTKind.o  ASTUtil.o AST.o  bbtest.o -o bbtest 
-
-# asttest: $(OBJS)
-#      $(CC) $(LDFLAGS) ASTKind.o  ASTUtil.o AST.o asttest.o  -lstdc++ -o asttest
-
+.PHONY: clean
 clean:
        rm -rf *.o *~ bbtest asttest cnftest *.a  ASTKind.h ASTKind.cpp .#*
-       rm -rf printer/*.o printer/*~
+       rm -rf printer/*.o
 
-depend:
-       makedepend -Y -- $(CFLAGS) -- $(SRCS)
-# DO NOT DELETE
+depend: $(SRCS)
+       $(CXX) -MM $(CXXFLAGS) $(SRCS) > $@
 
-AST.o: AST.h ../AST/ASTUtil.h ASTKind.h ../sat/core/Solver.h
-AST.o: ../sat/core/SolverTypes.h   ../sat/mtl/Heap.h
-AST.o: ../sat/core/SolverTypes.h 
-asttest.o: AST.h ../AST/ASTUtil.h ../AST/ASTKind.h ../sat/core/Solver.h
-asttest.o: ../sat/core/SolverTypes.h  
-asttest.o: ../sat/mtl/Heap.h ../sat/core/SolverTypes.h 
-ASTUtil.o: ASTUtil.h
-bbtest.o: AST.h ../AST/ASTUtil.h ../AST/ASTKind.h ../sat/core/Solver.h
-bbtest.o: ../sat/core/SolverTypes.h  
-bbtest.o: ../sat/mtl/Heap.h ../sat/core/SolverTypes.h 
-BitBlast.o: AST.h ../AST/ASTUtil.h ../AST/ASTKind.h ../sat/core/Solver.h
-BitBlast.o: ../sat/core/SolverTypes.h  
-BitBlast.o: ../sat/mtl/Heap.h ../sat/core/SolverTypes.h 
-cnftest.o: AST.h ../AST/ASTUtil.h ../AST/ASTKind.h ../sat/core/Solver.h
-cnftest.o: ../sat/core/SolverTypes.h  
-cnftest.o: ../sat/mtl/Heap.h ../sat/core/SolverTypes.h 
-ToCNF.o: AST.h ../AST/ASTUtil.h ../AST/ASTKind.h ../sat/core/Solver.h
-ToCNF.o: ../sat/core/SolverTypes.h   ../sat/mtl/Heap.h
-ToCNF.o: ../sat/core/SolverTypes.h 
-ToSAT.o: AST.h ../AST/ASTUtil.h ../AST/ASTKind.h ../sat/core/Solver.h
-ToSAT.o: ../sat/core/SolverTypes.h   ../sat/mtl/Heap.h
-ToSAT.o: ../sat/core/SolverTypes.h 
-Transform.o : AST.h ../AST/ASTUtil.h ../AST/ASTKind.h
-#DPLLMgr.o: AST.h ../AST/ASTUtil.h ../AST/ASTKind.h ../sat/core/Solver.h
-#DPLLMgr.o: ../sat/core/SolverTypes.h   ../sat/mtl/Heap.h
-#DPLLMgr.o: ../sat/core/SolverTypes.h 
+-include depend

diff --git a/src/AST/bbtest.cpp b/src/AST/test/bbtest.cpp
similarity index 99%
rename from src/AST/bbtest.cpp
rename to src/AST/test/bbtest.cpp
index 900ddc361cac104355ab59891202d7ab835d21a9..838b3c41a76842b0a56ab0a73ef6b2cebc66257c 100644 (file)
--- a/src/AST/bbtest.cpp
+++ b/src/AST/test/bbtest.cpp
@@ -1,4 +1,4 @@
-#include "AST.h"
+#include "../AST.h"
 
 using namespace BEEV;
 

diff --git a/src/AST/cnftest.cpp b/src/AST/test/cnftest.cpp
similarity index 98%
rename from src/AST/cnftest.cpp
rename to src/AST/test/cnftest.cpp
index 7db61663a1fbc6a401e1de89fb6094986fa0d281..efffde5bb94f4a89dd9da22f09b11833ec5e85ad 100644 (file)
--- a/src/AST/cnftest.cpp
+++ b/src/AST/test/cnftest.cpp
@@ -2,7 +2,7 @@
 
 // Test program for CNF conversion.
 
-#include "AST.h"
+#include "../AST.h"
 
 using namespace BEEV;