diff --git a/Makefile.in b/Makefile.in index 1db2dca76..9aef78a13 100644 --- a/Makefile.in +++ b/Makefile.in @@ -297,124 +297,6 @@ clean: find . -name 'a.exe' -exec rm -f '{}' ';' find . -name 'core' -exec rm -f '{}' ';' -################################ -# -# Release -# -# NOTE: In 64-bit systems it is not possible to build a dynamic library using static gmp. -# So, EXTRA_LIBS="" in 64-bit systems. -# EXTRA_LIBS="$(BIN_DIR)/lib$(Z3)-gmp.so" in 32-bit systems. -# -# Remark: disable ocaml bindings in the release. -# They will be re-enabled in the future. -# To re-enable them, I just have to include ocamlrelease in the list of dependencies. -# I had to disable them because the stub generator uses non-portable scripts, and -# were not included at z3.codeplex.com. Thus, this part is temporarily broken. -# -# iZ3 is also temporarily removed from the release package. To re-enable it, we just have to include iz3release in the -# list of dependencies. -# -# I also permanently removed test_user_theory example. Now, that the source code -# is available, we don't need it anymore. -# -################################ -release: $(BIN_DIR)/$(Z3) $(BIN_DIR)/lib$(Z3).@SO_EXT@ @EXTRA_LIBS@ $(BIN_DIR)/lib$(Z3).a - @rm -f -r z3 - @mkdir -p z3 - @mkdir -p z3/bin - @mkdir -p z3/lib - @mkdir -p z3/include - @mkdir -p z3/examples - @mkdir -p z3/python - @mkdir -p z3/examples/c - @mkdir -p z3/examples/c++ - @mkdir -p z3/examples/python - @mkdir -p z3/examples/maxsat - @cp lib/z3.h z3/include - @cp lib/z3_v1.h z3/include - @cp lib/z3_api.h z3/include - @cp lib/z3_macros.h z3/include - @$(DOS2UNIX) z3/include/* - @cp $(BIN_DIR)/$(Z3) z3/bin - @cp $(BIN_DIR)/lib$(Z3).@SO_EXT@ z3/lib - @cp $(BIN_DIR)/lib$(Z3).a z3/lib - @cp test_capi/test_capi.c z3/examples/c - @$(DOS2UNIX) z3/examples/c/test_capi.c - @cp test_capi/README-$(PLATFORM).txt z3/examples/c/README - @$(DOS2UNIX) z3/examples/c/README - @cp test_capi/build-external-$(PLATFORM).sh z3/examples/c/build.sh - @cp test_capi/build-static-$(PLATFORM).sh z3/examples/c/build-static.sh - @$(DOS2UNIX) z3/examples/c/build.sh - @chmod +rwx z3/examples/c/build.sh - @$(DOS2UNIX) z3/examples/c/build-static.sh - @chmod +rwx z3/examples/c/build-static.sh - @cp test_capi/exec-external-$(PLATFORM).sh z3/examples/c/exec.sh - @$(DOS2UNIX) z3/examples/c/exec.sh - @chmod +rwx z3/examples/c/exec.sh - @cp maxsat/maxsat.c z3/examples/maxsat - @$(DOS2UNIX) z3/examples/maxsat/maxsat.c - @cp maxsat/README-$(PLATFORM).txt z3/examples/maxsat/README - @$(DOS2UNIX) z3/examples/maxsat/README - @cp maxsat/build-external-$(PLATFORM).sh z3/examples/maxsat/build.sh - @cp maxsat/build-static-$(PLATFORM).sh z3/examples/maxsat/build-static.sh - @$(DOS2UNIX) z3/examples/maxsat/build.sh - @chmod +rwx z3/examples/maxsat/build.sh - @$(DOS2UNIX) z3/examples/maxsat/build-static.sh - @chmod +rwx z3/examples/maxsat/build-static.sh - @cp maxsat/exec-external-$(PLATFORM).sh z3/examples/maxsat/exec.sh - @$(DOS2UNIX) z3/examples/maxsat/exec.sh - @chmod +rwx z3/examples/maxsat/exec.sh - @cp c++/z3++.h z3/include - @cp c++/example.cpp z3/examples/c++ - @cp c++/build-external-$(PLATFORM).sh z3/examples/c++/build.sh - @$(DOS2UNIX) z3/examples/c++/build.sh - @chmod +rwx z3/examples/c++/build.sh - @cp c++/exec-external-$(PLATFORM).sh z3/examples/c++/exec.sh - @$(DOS2UNIX) z3/examples/c++/exec.sh - @chmod +rwx z3/examples/c++/exec.sh - @cp python/z3.py z3/python - @cp python/z3core.py z3/python - @cp python/z3types.py z3/python - @cp python/z3consts.py z3/python - @cp python/z3tactics.py z3/python - @cp python/z3printer.py z3/python - @cp python/README-$(PLATFORM).txt z3/examples/python/README - @cp python/exec-$(PLATFORM).sh z3/examples/python/exec.sh - @cp python/example.py z3/examples/python - @$(DOS2UNIX) z3/python/*.py - @$(DOS2UNIX) z3/examples/python/*.py - @$(DOS2UNIX) z3/examples/python/*.sh - @chmod +rwx z3/examples/python/*.sh - @tar -cvzf z3.tar.gz z3 - -ocamlrelease: - @mkdir -p z3/ocaml - @mkdir -p z3/examples/ocaml - @cp ml/z3_stubs.c z3/ocaml - @cp ml/z3_theory_stubs.c z3/ocaml - @cp ml/z3.mli z3/ocaml - @cp ml/z3.ml z3/ocaml - @cp ml_release/build-lib.sh z3/ocaml - @$(DOS2UNIX) z3/ocaml/build-lib.sh - @chmod +rwx z3/ocaml/build-lib.sh - @cp ml_release/README_$(PLATFORM) z3/ocaml/README - @$(DOS2UNIX) z3/ocaml/README - @cp ml_release/build-test.sh z3/examples/ocaml - @$(DOS2UNIX) z3/examples/ocaml/build-test.sh - @chmod +rwx z3/examples/ocaml/build-test.sh - @cp ml_release/README_test_$(PLATFORM) z3/examples/ocaml/README - @$(DOS2UNIX) z3/examples/ocaml/README - @cp ml_release/exec-$(PLATFORM).sh z3/examples/ocaml/exec.sh - @$(DOS2UNIX) z3/examples/ocaml/exec.sh - @chmod +rwx z3/examples/ocaml/exec.sh - @cp ml/test_mlapi.ml z3/examples/ocaml - @$(DOS2UNIX) z3/examples/ocaml/test_mlapi.ml - -iz3release: - @$(DOS2UNIX) iZ3/pack-iz3-$(PLATFORM).sh - @chmod +rwx iZ3/pack-iz3-$(PLATFORM).sh - @iZ3/pack-iz3-$(PLATFORM).sh - ################################ # # Support diff --git a/c++/README.txt b/c++/README.txt index 05d1be082..e1350f503 100644 --- a/c++/README.txt +++ b/c++/README.txt @@ -14,10 +14,11 @@ example.exe can find z3.dll. 2) Using gcc +You must install Z3 before running this example. +To install Z3, execute the following command in the Z3 root directory. + + sudo make install + Use 'build.sh' to build the test application using g++. -The script 'exec.sh' adds the bin directory to the path. So, -example.exe can find z3.dll. - -Remark: the scripts 'build.sh' and 'exec.sh' assumes you are in a -Cygwin or Mingw shell. +It generates the executable 'example'. diff --git a/c++/build-external-linux.sh b/c++/build-external-linux.sh deleted file mode 100644 index d439d5995..000000000 --- a/c++/build-external-linux.sh +++ /dev/null @@ -1 +0,0 @@ -g++ -fopenmp -o example -I ../../include example.cpp -L ../../lib -lz3 diff --git a/c++/build-external-osx.sh b/c++/build-external-osx.sh deleted file mode 100644 index d439d5995..000000000 --- a/c++/build-external-osx.sh +++ /dev/null @@ -1 +0,0 @@ -g++ -fopenmp -o example -I ../../include example.cpp -L ../../lib -lz3 diff --git a/c++/build-external.sh b/c++/build-external.sh deleted file mode 100644 index f338ca44b..000000000 --- a/c++/build-external.sh +++ /dev/null @@ -1 +0,0 @@ -g++ -fopenmp -o example.exe -I ../../include ../../bin/z3.dll example.cpp diff --git a/c++/exec-external-linux.sh b/c++/exec-external-linux.sh deleted file mode 100644 index f46e9ea89..000000000 --- a/c++/exec-external-linux.sh +++ /dev/null @@ -1,2 +0,0 @@ -export LD_LIBRARY_PATH=../../lib:$LD_LIBRARY_PATH -./example diff --git a/c++/exec-external-osx.sh b/c++/exec-external-osx.sh deleted file mode 100644 index 9f9762b54..000000000 --- a/c++/exec-external-osx.sh +++ /dev/null @@ -1,2 +0,0 @@ -export DYLD_LIBRARY_PATH=../../lib:$DYLD_LIBRARY_PATH -./example diff --git a/c++/exec-external.sh b/c++/exec-external.sh deleted file mode 100644 index 39e7eb58c..000000000 --- a/c++/exec-external.sh +++ /dev/null @@ -1,2 +0,0 @@ -export PATH=../../bin:$PATH -./example.exe