From: vijay_ganesh Date: Fri, 14 Aug 2009 16:24:42 +0000 (+0000) Subject: git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=32a4f50431b86cf2485ff2a47b2dfe855f346759;p=francis%2Fstp.git git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@128 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/INSTALL b/INSTALL index 7f8f181..99626a3 100644 --- a/INSTALL +++ b/INSTALL @@ -1,16 +1,23 @@ -1. To install STP perform the following steps on your Unix/GNU-Linux/MacOS X commandline: +1. To install STP perform the following steps on your +Unix/GNU-Linux/MacOS X commandline: -./configure --with-prefix=$HOME (or another installation directory) -make -make install +./clean-install.sh -2. To test the system after installation, you will need to download the regression tests. The regression are 190MB big, so are stored separately. To download them, try something like: +2. To test the system after installation, you will need to download +the regression tests. The regression are 190MB big, so are stored +separately. To download them, try something like: -svn co https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/stp-tests/test +svn co +https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/stp-tests/test -The directory of the regression tests is hard-coded in /bin/run_tests, which you may need to update, depending on where you checkout the regression tests to. +The directory of the regression tests is hard-coded in /bin/run_tests, +which you may need to update, depending on where you checkout the +regression tests to. To run the regression tests: make regressall -NB: -* If you want to compile a statically linked version of STP, run ./liblinks.sh after the configure script, and then compile adding STATIC=true to the make commands. +NB: + +* If you want to compile a statically linked version of STP, run +./liblinks.sh after the configure script, and then compile adding +STATIC=true to the make commands. diff --git a/clean-install b/clean-install.sh similarity index 88% rename from clean-install rename to clean-install.sh index bbb6746..f9355da 100755 --- a/clean-install +++ b/clean-install.sh @@ -17,8 +17,8 @@ while [ $# -gt 0 ]; do done +./make-scripts/configure --with-prefix=$PREFIX make clean -./configure --with-prefix=$PREFIX make make install diff --git a/Makefile.common b/make-scripts/Makefile.common similarity index 100% rename from Makefile.common rename to make-scripts/Makefile.common diff --git a/make-scripts/Makefile.in b/make-scripts/Makefile.in index 9be6b1d..aa42bff 100644 --- a/make-scripts/Makefile.in +++ b/make-scripts/Makefile.in @@ -4,7 +4,7 @@ # To make in optimized mode, type 'make "OPTIMIZE=-O3" -include Makefile.common make-scripts/config.info +include make-scripts/Makefile.common make-scripts/config.info BIN_DIR=$(PREFIX)/bin LIB_DIR=$(PREFIX)/lib diff --git a/make-scripts/config.info b/make-scripts/config.info index a67a797..9613a5b 100644 --- a/make-scripts/config.info +++ b/make-scripts/config.info @@ -1 +1 @@ -PREFIX=/usr/local +PREFIX=/afs/csail.mit.edu/u/v/vganesh diff --git a/configure b/make-scripts/configure similarity index 100% rename from configure rename to make-scripts/configure diff --git a/format_config.xml b/make-scripts/format_config.xml similarity index 100% rename from format_config.xml rename to make-scripts/format_config.xml diff --git a/src/AST/Makefile b/src/AST/Makefile index a91aa50..71b4879 100644 --- a/src/AST/Makefile +++ b/src/AST/Makefile @@ -1,4 +1,4 @@ -include ../../Makefile.common +include ../../make-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 printer/SMTLIBPrinter.cpp printer/dotPrinter.cpp printer/CPrinter.cpp diff --git a/src/bitvec/Makefile b/src/bitvec/Makefile index ac885f5..6f4c401 100644 --- a/src/bitvec/Makefile +++ b/src/bitvec/Makefile @@ -1,4 +1,4 @@ -include ../../Makefile.common +include ../../make-scripts/Makefile.common SRCS = consteval.cpp OBJS = $(SRCS:.cpp=.o) diff --git a/src/c_interface/Makefile b/src/c_interface/Makefile index 11cca91..ab27595 100644 --- a/src/c_interface/Makefile +++ b/src/c_interface/Makefile @@ -1,4 +1,4 @@ -include ../../Makefile.common +include ../../make-scripts/Makefile.common SRCS = c_interface.cpp OBJS = $(SRCS:.cpp=.o) diff --git a/src/constantbv/Makefile b/src/constantbv/Makefile index 9ddcb79..7d5ef9a 100644 --- a/src/constantbv/Makefile +++ b/src/constantbv/Makefile @@ -1,4 +1,4 @@ -include ../../Makefile.common +include ../../make-scripts/Makefile.common SRCS = constantbv.cpp OBJS = $(SRCS:.cpp=.o) diff --git a/ocaml-wrapper/COPYRIGHT-NOTICE b/src/ocaml-wrapper/COPYRIGHT-NOTICE similarity index 100% rename from ocaml-wrapper/COPYRIGHT-NOTICE rename to src/ocaml-wrapper/COPYRIGHT-NOTICE diff --git a/ocaml-wrapper/Makefile b/src/ocaml-wrapper/Makefile similarity index 100% rename from ocaml-wrapper/Makefile rename to src/ocaml-wrapper/Makefile diff --git a/ocaml-wrapper/OCamlMakefile b/src/ocaml-wrapper/OCamlMakefile similarity index 100% rename from ocaml-wrapper/OCamlMakefile rename to src/ocaml-wrapper/OCamlMakefile diff --git a/ocaml-wrapper/libstp.idl b/src/ocaml-wrapper/libstp.idl similarity index 100% rename from ocaml-wrapper/libstp.idl rename to src/ocaml-wrapper/libstp.idl diff --git a/ocaml-wrapper/libstp_regerrorhandler.c b/src/ocaml-wrapper/libstp_regerrorhandler.c similarity index 100% rename from ocaml-wrapper/libstp_regerrorhandler.c rename to src/ocaml-wrapper/libstp_regerrorhandler.c diff --git a/ocaml-wrapper/stpvc.ml b/src/ocaml-wrapper/stpvc.ml similarity index 100% rename from ocaml-wrapper/stpvc.ml rename to src/ocaml-wrapper/stpvc.ml diff --git a/ocaml-wrapper/stpvc.mli b/src/ocaml-wrapper/stpvc.mli similarity index 100% rename from ocaml-wrapper/stpvc.mli rename to src/ocaml-wrapper/stpvc.mli diff --git a/src/parser/Makefile b/src/parser/Makefile index f803700..82c88c7 100644 --- a/src/parser/Makefile +++ b/src/parser/Makefile @@ -1,4 +1,4 @@ -include ../../Makefile.common +include ../../make-scripts/Makefile.common LEX=flex YACC=bison -d -y --debug -v diff --git a/src/simplifier/Makefile b/src/simplifier/Makefile index b573996..030edc5 100644 --- a/src/simplifier/Makefile +++ b/src/simplifier/Makefile @@ -1,4 +1,4 @@ -include ../../Makefile.common +include ../../make-scripts/Makefile.common SRCS = simplifier.cpp bvsolver.cpp OBJS = $(SRCS:.cpp=.o)