From 2cb0f49bc6564ca695f9b5cc197c0c02454671a3 Mon Sep 17 00:00:00 2001 From: vijay_ganesh Date: Wed, 12 Aug 2009 15:33:20 +0000 Subject: [PATCH] git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@114 e59a4935-1847-0410-ae03-e826735625c1 --- Makefile.cvc | 145 ---------------------------------------------- Makefile.in | 2 +- src/AST/ToSAT.cpp | 2 +- 3 files changed, 2 insertions(+), 147 deletions(-) delete mode 100644 Makefile.cvc diff --git a/Makefile.cvc b/Makefile.cvc deleted file mode 100644 index 184666d..0000000 --- a/Makefile.cvc +++ /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/simp libp - $(MAKE) -C simplifier - $(MAKE) -C bitvec - $(MAKE) -C c_interface - $(MAKE) -C constantbv - $(MAKE) -C parser - $(AR) rc libstp.a AST/*.o sat/simp/*.op sat/core/*.op 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/simp - $(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 71c5b8c..e154e34 100644 --- a/Makefile.in +++ b/Makefile.in @@ -18,7 +18,7 @@ HEADERS=$(SRC)/c_interface/*.h .PHONY: all all: $(MAKE) -C $(SRC)/AST - $(MAKE) -C $(SRC)/sat core + $(MAKE) -C $(SRC)/sat simp $(MAKE) -C $(SRC)/simplifier $(MAKE) -C $(SRC)/bitvec $(MAKE) -C $(SRC)/c_interface diff --git a/src/AST/ToSAT.cpp b/src/AST/ToSAT.cpp index c99807a..8d6b542 100644 --- a/src/AST/ToSAT.cpp +++ b/src/AST/ToSAT.cpp @@ -1186,7 +1186,7 @@ int BeevMgr::TopLevelSATAux(const ASTNode& inputasserts) int res; //solver instantiated here - MINISAT::Solver newS; + MINISAT::SimpSolver newS; if (arrayread_refinement) { counterexample_checking_during_refinement = true; -- 2.47.3