Remove from SVN files that are automatically generated in the

configure and build processes. Copy the changes to Makefile back to
the original Makefile.in. After this change, you'll need to re-run
"configure".

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

diff --git a/Makefile b/Makefile
deleted file mode 100644 (file)
index abd8739..0000000
--- a/Makefile
+++ /dev/null
@@ -1,145 +0,0 @@
- # STP (Simple Theorem Prover) top level makefile
- #
- # To make in debug mode, type 'make "CLFAGS=-ggdb"
- # To make in optimized mode, type 'make "CFLAGS=-O2" 
-
-
-include Makefile.common config.info
-
-BIN_DIR=$(PREFIX)/bin
-LIB_DIR=$(PREFIX)/lib
-INCLUDE_DIR=$(PREFIX)/include/stp
-
-BINARIES=bin/stp
-LIBRARIES=lib/libstp.a
-HEADERS=c_interface/*.h
-
-# NB: the TAGS target is a hack to get around this recursive make nonsense
-# we want all the source and header files generated before we make tags
-.PHONY: all
-all:
-       $(MAKE) -C AST
-       $(MAKE) -C sat/core lib
-       $(MAKE) -C simplifier
-       $(MAKE) -C bitvec
-       $(MAKE) -C c_interface
-       $(MAKE) -C constantbv
-       $(MAKE) -C parser
-       $(AR) rc libstp.a  AST/*.o sat/core/*.or simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o
-       $(RANLIB) libstp.a
-       @mkdir -p lib
-       @mv libstp.a lib/
-#      $(MAKE) TAGS
-       @echo ""
-       @echo "Compilation successful."
-       @echo "Type 'make install' to install STP."
-
-
-.PHONY: install
-install: all
-       @cp -f $(BINARIES) $(BIN_DIR)
-       @cp -f $(LIBRARIES) $(LIB_DIR)
-       @cp -f $(HEADERS) $(INCLUDE_DIR)
-       @echo "STP installed successfully."
-
-.PHONY: clean
-clean:
-       rm -rf *~
-       rm -rf *.a
-       rm -rf lib/*.a
-       rm -rf test/*~
-       rm -rf bin/*~
-       rm -rf bin/stp
-       rm -rf *.log
-       #rm -rf Makefile
-       #rm -rf config.info
-       rm -f TAGS
-       $(MAKE) clean -C AST
-       $(MAKE) clean -C sat/core
-       $(MAKE) clean -C simplifier
-       $(MAKE) clean -C bitvec
-       $(MAKE) clean -C parser
-       $(MAKE) clean -C c_interface
-       $(MAKE) clean -C constantbv
-
-# this is make way too difficult because of the recursive Make junk, it 
-# should be removed
-TAGS: FORCE
-       find . -name "*.[h]" -or -name "*.cpp" -or -name "*.C" | grep -v SCCS | etags -
-
-FORCE:
-
-# The higher the level, the more tests are run (3 = all)
-REGRESS_TESTS0 = test \
- test/EGT
-REGRESS_LEVEL=4
-REGRESS_TESTS=$(REGRESS_TESTS0)
-REGRESS_LOG = `date +%Y-%m-%d`"-regress.log"
-PROGNAME=bin/stp
-ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
-
-.PHONY: regress
-regress:
-       @echo "*********************************************************" \
-          | tee -a $(REGRESS_LOG)
-       @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
-       @echo "*********************************************************" \
-          | tee -a $(REGRESS_LOG)
-       bin/run_tests $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
-       @echo "*********************************************************" \
-          | tee -a $(REGRESS_LOG)
-       @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
-       @echo "*********************************************************" \
-          | tee -a $(REGRESS_LOG)
-
-# The higher the level, the more tests are run (3 = all)
-REGRESS_TESTS0 = test \
- test/EGT
-REGRESS_LEVEL=4
-REGRESS_TESTS=$(REGRESS_TESTS0)
-#REGRESS_LOG = `date +%Y-%m-%d`"-regress-bigarray.log"
-PROGNAME=bin/stp
-ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
-
-.PHONY: regressbigarray
-regressbigarray:
-       @echo "*********************************************************" \
-          | tee -a $(REGRESS_LOG)
-       @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
-       @echo "*********************************************************" \
-          | tee -a $(REGRESS_LOG)
-       bin/run_bigarray_tests $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
-       @echo "*********************************************************" \
-          | tee -a $(REGRESS_LOG)
-       @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
-       @echo "*********************************************************" \
-          | tee -a $(REGRESS_LOG)
-
-.PHONY: regressall
-regressall:
-       $(MAKE) install
-       $(MAKE) regress
-
-GRIND_LOG = `date +%Y-%m-%d`"-grind.log"
-GRINDPROG = valgrind --leak-check=full --undef-value-errors=no
-GRIND_TAR  = $(BIN_DIR)/stp -d
-GRIND_CALL = -vc "$(GRINDPROG) $(GRIND_TAR)" 
-GRIND_OPTIONS = -l $(REGRESS_LEVEL) -rt $(GRIND_CALL) $(REGRESS_TESTS)
-
-
-.PHONY: grind
-grind:
-
-       $(MAKE) install CFLAGS="-ggdb -pg -g"
-       @echo "*********************************************************" \
-          | tee -a $(GRIND_LOG)
-       @echo "Starting tests at" `date` | tee -a $(GRIND_LOG)
-       @echo "*********************************************************" \
-          | tee -a $(GRIND_LOG)
-       bin/run_tests $(GRIND_OPTIONS) 2>&1 | tee -a $(GRIND_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
-       @echo "*********************************************************" \
-          | tee -a $(GRIND_LOG)
-       @echo "Output is saved in $(GRIND_LOG)" | tee -a $(GRIND_LOG)
-       @echo "*********************************************************" \
-          | tee -a $(GRIND_LOG)
-

diff --git a/Makefile.in b/Makefile.in
index ae1307899e06e0319d839a5568aefbda77ff3d1e..e9ab2a37677727cc3afcc496d96e9eeb7ea7025f 100644 (file)
--- a/Makefile.in
+++ b/Makefile.in
@@ -1,6 +1,6 @@
  # STP (Simple Theorem Prover) top level makefile
  #
- # To make in debug mode, type 'make "CLFAGS=-ggdb"
+ # To make in debug mode, type 'make "CFLAGS=-ggdb"
  # To make in optimized mode, type 'make "CFLAGS=-O2" 
 
 
@@ -19,13 +19,13 @@ HEADERS=c_interface/*.h
 .PHONY: all
 all:
        $(MAKE) -C AST
-       $(MAKE) -C sat
+       $(MAKE) -C sat/core lib
        $(MAKE) -C simplifier
        $(MAKE) -C bitvec
        $(MAKE) -C c_interface
        $(MAKE) -C constantbv
        $(MAKE) -C parser
-       $(AR) rc libstp.a  AST/*.o sat/*.o simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o
+       $(AR) rc libstp.a  AST/*.o sat/core/*.or simplifier/*.o bitvec/*.o constantbv/*.o c_interface/*.o
        $(RANLIB) libstp.a
        @mkdir -p lib
        @mv libstp.a lib/
@@ -34,6 +34,7 @@ all:
        @echo "Compilation successful."
        @echo "Type 'make install' to install STP."
 
+
 .PHONY: install
 install: all
        @cp -f $(BINARIES) $(BIN_DIR)
@@ -50,11 +51,11 @@ clean:
        rm -rf bin/*~
        rm -rf bin/stp
        rm -rf *.log
-       rm -rf Makefile
-       rm -rf config.info
+       #rm -rf Makefile
+       #rm -rf config.info
        rm -f TAGS
        $(MAKE) clean -C AST
-       $(MAKE) clean -C sat
+       $(MAKE) clean -C sat/core
        $(MAKE) clean -C simplifier
        $(MAKE) clean -C bitvec
        $(MAKE) clean -C parser
@@ -84,8 +85,30 @@ regress:
        @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
        @echo "*********************************************************" \
           | tee -a $(REGRESS_LOG)
-#      bin/run_tests $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
-       bin/run_tests $(ALL_OPTIONS) 2>&1 | grep -v "ulimit" | grep -v "elapsed" | grep -v "swaps" | tee -a $(REGRESS_LOG);
+       bin/run_tests $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
+       @echo "*********************************************************" \
+          | tee -a $(REGRESS_LOG)
+       @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)
+       @echo "*********************************************************" \
+          | tee -a $(REGRESS_LOG)
+
+# The higher the level, the more tests are run (3 = all)
+REGRESS_TESTS0 = test \
+ test/EGT
+REGRESS_LEVEL=4
+REGRESS_TESTS=$(REGRESS_TESTS0)
+#REGRESS_LOG = `date +%Y-%m-%d`"-regress-bigarray.log"
+PROGNAME=bin/stp
+ALL_OPTIONS= -l $(REGRESS_LEVEL) $(PROGNAME) $(REGRESS_TESTS)
+
+.PHONY: regressbigarray
+regressbigarray:
+       @echo "*********************************************************" \
+          | tee -a $(REGRESS_LOG)
+       @echo "Starting tests at" `date` | tee -a $(REGRESS_LOG)
+       @echo "*********************************************************" \
+          | tee -a $(REGRESS_LOG)
+       bin/run_bigarray_tests $(ALL_OPTIONS) 2>&1 | tee -a $(REGRESS_LOG); [ $${PIPESTATUS[0]} -eq 0 ]
        @echo "*********************************************************" \
           | tee -a $(REGRESS_LOG)
        @echo "Output is saved in $(REGRESS_LOG)" | tee -a $(REGRESS_LOG)

diff --git a/config.info b/config.info
deleted file mode 100644 (file)
index 75dc56b..0000000
--- a/config.info
+++ /dev/null
@@ -1 +0,0 @@
-PREFIX=/Users/katelman/Work/projects/stp/svn/stp-fast-prover/trunk/stp

diff --git a/sat/core/depend.mk b/sat/core/depend.mk
deleted file mode 100644 (file)
index 4320d89..0000000
--- a/sat/core/depend.mk
+++ /dev/null
@@ -1,16 +0,0 @@
-Main.o: Main.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \
-  ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h
-Solver.o: Solver.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \
-  ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h ../mtl/Sort.h ../mtl/Vec.h
-Main.op: Main.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \
-  ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h
-Solver.op: Solver.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \
-  ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h ../mtl/Sort.h ../mtl/Vec.h
-Main.od: Main.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \
-  ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h
-Solver.od: Solver.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \
-  ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h ../mtl/Sort.h ../mtl/Vec.h
-Main.or: Main.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \
-  ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h
-Solver.or: Solver.C Solver.h ../mtl/Map.h ../mtl/Vec.h ../mtl/Heap.h \
-  ../mtl/Vec.h ../mtl/Alg.h SolverTypes.h ../mtl/Sort.h ../mtl/Vec.h