diff --git a/debian/changelog b/debian/changelog new file mode 100644 index 0000000..0ef170b --- /dev/null +++ b/debian/changelog @@ -0,0 +1,5 @@ +z3 (4.8.7-ok1) yangtze; urgency=medium + + * Build for openKylin. + + -- openKylinBot Mon, 25 Apr 2022 22:03:04 +0800 diff --git a/debian/control b/debian/control new file mode 100644 index 0000000..342a504 --- /dev/null +++ b/debian/control @@ -0,0 +1,96 @@ +Source: z3 +Section: science +Priority: optional +Maintainer: Openkylin Developers +Uploaders: Fabian Wolff +Build-Depends: debhelper-compat (= 12), + dh-python, python3, cmake, + javahelper [!hppa !hurd-i386 !m68k !sh4], + default-jdk [!hppa !hurd-i386 !m68k !sh4] +Standards-Version: 4.4.1 +Homepage: https://github.com/Z3Prover/z3 +Vcs-Git: https://salsa.debian.org/pkg-llvm-team/z3.git +Vcs-Browser: https://salsa.debian.org/pkg-llvm-team/z3 + +Package: z3 +Architecture: any +Depends: ${misc:Depends}, ${shlibs:Depends} +Description: theorem prover from Microsoft Research + Z3 is a state-of-the art theorem prover from Microsoft Research. It can be + used to check the satisfiability of logical formulas over one or more + theories. Z3 offers a compelling match for software analysis and verification + tools, since several common software constructs map directly into supported + theories. + . + The Z3 input format is an extension of the one defined by the SMT-LIB 2.0 + standard. + +Package: libz3-4 +Architecture: any +Multi-Arch: same +Section: libs +Depends: ${shlibs:Depends}, + ${misc:Depends} +Breaks: libz3-dev (<< 4.4.1) +Replaces: libz3-dev (<< 4.4.1) +Description: theorem prover from Microsoft Research - runtime libraries + Z3 is a state-of-the art theorem prover from Microsoft Research. It can be + used to check the satisfiability of logical formulas over one or more + theories. Z3 offers a compelling match for software analysis and verification + tools, since several common software constructs map directly into supported + theories. + . + This package contains runtime libraries. You shouldn't have to install it + manually. + +Package: libz3-dev +Section: libdevel +Architecture: any +Multi-Arch: same +Depends: libz3-4 (= ${binary:Version}), ${misc:Depends} +Description: theorem prover from Microsoft Research - development files + Z3 is a state-of-the art theorem prover from Microsoft Research. It can be + used to check the satisfiability of logical formulas over one or more + theories. Z3 offers a compelling match for software analysis and verification + tools, since several common software constructs map directly into supported + theories. + . + This package can be used to invoke Z3 via its C++ API. + +Package: python3-z3 +Section: python +Architecture: any +Pre-Depends: ${misc:Pre-Depends} +Depends: libz3-dev (= ${binary:Version}), + python3-pkg-resources, + ${misc:Depends}, + ${python3:Depends}, + ${shlibs:Depends} +Description: theorem prover from Microsoft Research - Python 3 bindings + Z3 is a state-of-the art theorem prover from Microsoft Research. See the z3 + package for a detailed description. + . + This package can be used to invoke Z3 via its Python 3 API. + +Package: libz3-java +Section: java +Architecture: amd64 arm64 armel armhf i386 mips mips64el mipsel powerpc ppc64el s390x alpha kfreebsd-amd64 kfreebsd-i386 powerpcspe riscv64 sparc64 x32 +Multi-Arch: foreign +Depends: libz3-jni (>= ${binary:Version}), libz3-jni (<< ${source:Version}.1~), libz3-dev, ${misc:Depends}, ${java:Depends} +Description: theorem prover from Microsoft Research - java bindings + Z3 is a state-of-the art theorem prover from Microsoft Research. See the z3 + package for a detailed description. + . + This package can be used to invoke Z3 via its Java API. + +Package: libz3-jni +Section: java +Architecture: amd64 arm64 armel armhf i386 mips mips64el mipsel powerpc ppc64el s390x alpha kfreebsd-amd64 kfreebsd-i386 powerpcspe riscv64 sparc64 x32 +Multi-Arch: same +Pre-Depends: ${misc:Pre-Depends} +Depends: libz3-dev (= ${binary:Version}), ${misc:Depends}, ${shlibs:Depends} +Description: theorem prover from Microsoft Research - JNI library + Z3 is a state-of-the art theorem prover from Microsoft Research. See the z3 + package for a detailed description. + . + This package provides the JNI library to invoke Z3 via its Java API. diff --git a/debian/copyright b/debian/copyright new file mode 100644 index 0000000..edbdfb1 --- /dev/null +++ b/debian/copyright @@ -0,0 +1,47 @@ +Format: https://www.debian.org/doc/packaging-manuals/copyright-format/1.0/ +Upstream-Name: z3 +Source: https://github.com/Z3Prover/z3 + +Files: * +Copyright: 2006-2019 Microsoft Corporation + 2006, 2010, 2017-2019 Arie Gurfinkel + 2017-2018 Saint-Petersburg State University + 2017 Matteo Marescotti +License: Expat + Permission is hereby granted, free of charge, to any person obtaining a copy of + this software and associated documentation files (the ""Software""), to deal in + the Software without restriction, including without limitation the rights to + use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies + of the Software, and to permit persons to whom the Software is furnished to do + so, subject to the following conditions: + . + The above copyright notice and this permission notice shall be included in all + copies or substantial portions of the Software. + . + THE SOFTWARE IS PROVIDED *AS IS*, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR + IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, + FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE + AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER + LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, + OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE + SOFTWARE. + +Files: debian/* +Copyright: 2016-2019 Fabian Wolff + 2011 Michael Tautschnig +License: GPL-2+ + This package is free software; you can redistribute it and/or modify + it under the terms of the GNU General Public License as published by + the Free Software Foundation; either version 2 of the License, or + (at your option) any later version. + . + This package is distributed in the hope that it will be useful, + but WITHOUT ANY WARRANTY; without even the implied warranty of + MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + GNU General Public License for more details. + . + You should have received a copy of the GNU General Public License + along with this program. If not, see + . + On Debian systems, the complete text of the GNU General + Public License version 2 can be found in "/usr/share/common-licenses/GPL-2". diff --git a/debian/docs b/debian/docs new file mode 100644 index 0000000..b43bf86 --- /dev/null +++ b/debian/docs @@ -0,0 +1 @@ +README.md diff --git a/debian/gbp.conf b/debian/gbp.conf new file mode 100644 index 0000000..3d9547a --- /dev/null +++ b/debian/gbp.conf @@ -0,0 +1,3 @@ +[DEFAULT] +pristine-tar = True +upstream-branch = upstream diff --git a/debian/libz3-4.install b/debian/libz3-4.install new file mode 100644 index 0000000..df4e0dc --- /dev/null +++ b/debian/libz3-4.install @@ -0,0 +1 @@ +usr/lib/*/libz3.so.* diff --git a/debian/libz3-dev.install b/debian/libz3-dev.install new file mode 100644 index 0000000..c9b7a13 --- /dev/null +++ b/debian/libz3-dev.install @@ -0,0 +1,2 @@ +usr/include/* +usr/lib/*/libz3.so diff --git a/debian/libz3-java.install b/debian/libz3-java.install new file mode 100644 index 0000000..65d015e --- /dev/null +++ b/debian/libz3-java.install @@ -0,0 +1 @@ +usr/share/java/ diff --git a/debian/libz3-java.preinst b/debian/libz3-java.preinst new file mode 100644 index 0000000..e1f24f3 --- /dev/null +++ b/debian/libz3-java.preinst @@ -0,0 +1,21 @@ +#!/bin/sh +set -e + +case "$1" in + install|upgrade) + # dpkg does not replace directories with symlinks. + if dpkg --compare-versions "$2" lt "4.4.0-3" ; then + rm -rf /usr/share/doc/libz3-java + fi + ;; + abort-upgrade) + ;; + *) + echo "preinst called with unknown argument \`$1'" >&2 + exit 1 + ;; +esac + +#DEBHELPER# + +exit 0 diff --git a/debian/libz3-jni.install b/debian/libz3-jni.install new file mode 100644 index 0000000..42eff51 --- /dev/null +++ b/debian/libz3-jni.install @@ -0,0 +1 @@ +usr/lib/*/jni/libz3java.so diff --git a/debian/libz3-jni.preinst b/debian/libz3-jni.preinst new file mode 100644 index 0000000..4b706dd --- /dev/null +++ b/debian/libz3-jni.preinst @@ -0,0 +1,21 @@ +#!/bin/sh +set -e + +case "$1" in + install|upgrade) + # dpkg does not replace directories with symlinks. + if dpkg --compare-versions "$2" lt "4.4.0-3" ; then + rm -rf /usr/share/doc/libz3-jni + fi + ;; + abort-upgrade) + ;; + *) + echo "preinst called with unknown argument \`$1'" >&2 + exit 1 + ;; +esac + +#DEBHELPER# + +exit 0 diff --git a/debian/manpages b/debian/manpages new file mode 100644 index 0000000..de180f0 --- /dev/null +++ b/debian/manpages @@ -0,0 +1 @@ +debian/z3.1 diff --git a/debian/patches/00-intrinsics.patch b/debian/patches/00-intrinsics.patch new file mode 100644 index 0000000..5a054b4 --- /dev/null +++ b/debian/patches/00-intrinsics.patch @@ -0,0 +1,67 @@ +Description: INTRINSICS are not universally available +Author: Michael Tautschnig +Forwarded: no +Last-Update: 2016-07-08 +--- +This patch header follows DEP-3: http://dep.debian.net/deps/dep3/ +--- a/src/util/hwf.cpp ++++ b/src/util/hwf.cpp +@@ -48,7 +48,7 @@ + // clear to the compiler what instructions should be used. E.g., for sqrt(), the Windows compiler selects + // the x87 FPU, even when /arch:SSE2 is on. + // Luckily, these are kind of standardized, at least for Windows/Linux/macOS. +-#if defined(__clang__) || defined(_M_ARM) && defined(_M_ARM64) ++#if defined(__clang__) || (defined(__GNUC__) && !defined(__SSE2__)) || defined(_M_ARM) && defined(_M_ARM64) + #undef USE_INTRINSICS + #endif + +--- a/src/util/mpz.cpp ++++ b/src/util/mpz.cpp +@@ -46,39 +46,24 @@ + #define LEHMER_GCD + #endif + +- +-#if defined(_WINDOWS) && !defined(_M_ARM) && !defined(_M_ARM64) +-// This is needed for _tzcnt_u32 and friends. +-#include +-#define _trailing_zeros32(X) _tzcnt_u32(X) +-#endif +- + #if defined(__GNUC__) + #define _trailing_zeros32(X) __builtin_ctz(X) ++#else ++inline uint32_t _trailing_zeros32(uint32_t x) { ++ uint32_t r = 0; ++ for (; 0 == (x & 1) && r < 32; ++r, x >>= 1); ++ return r; ++} + #endif + +-#if (defined(__LP64__) || defined(_WIN64)) && !defined(_M_ARM) && !defined(_M_ARM64) +- #if defined(__GNUC__) +- #define _trailing_zeros64(X) __builtin_ctzll(X) +- #else +- #define _trailing_zeros64(X) _tzcnt_u64(X) +- #endif ++#if defined(__LP64__) && !defined(_M_ARM) && !defined(_M_ARM64) && defined(__GNUC__) ++#define _trailing_zeros64(X) __builtin_ctzll(X) + #else + inline uint64_t _trailing_zeros64(uint64_t x) { + uint64_t r = 0; + for (; 0 == (x & 1) && r < 64; ++r, x >>= 1); + return r; + } +- +-#if defined(_WINDOWS) && !defined(_M_ARM) && !defined(_M_ARM64) +-// _trailing_zeros32 already defined using intrinsics +-#else +-inline uint32_t _trailing_zeros32(uint32_t x) { +- uint32_t r = 0; +- for (; 0 == (x & 1) && r < 32; ++r, x >>= 1); +- return r; +-} +-#endif + #endif + + diff --git a/debian/patches/01-reproducibility.patch b/debian/patches/01-reproducibility.patch new file mode 100644 index 0000000..56c706c --- /dev/null +++ b/debian/patches/01-reproducibility.patch @@ -0,0 +1,16 @@ +Description: Remove the use of __DATE__ to make the build reproducible +Author: Fabian Wolff +Last-Update: 2019-09-29 +--- +This patch header follows DEP-3: http://dep.debian.net/deps/dep3/ +--- a/src/api/api_log.cpp ++++ b/src/api/api_log.cpp +@@ -54,7 +54,7 @@ + res = false; + } + else { +- *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << " " << __DATE__ << "\"\n"; ++ *g_z3_log << "V \"" << Z3_MAJOR_VERSION << "." << Z3_MINOR_VERSION << "." << Z3_BUILD_NUMBER << "." << Z3_REVISION_NUMBER << "\"\n"; + g_z3_log->flush(); + g_z3_log_enabled = true; + } diff --git a/debian/patches/02-soname.patch b/debian/patches/02-soname.patch new file mode 100644 index 0000000..d20c127 --- /dev/null +++ b/debian/patches/02-soname.patch @@ -0,0 +1,37 @@ +Description: Set the SONAME properly +Author: Fabian Wolff +Last-Update: 2020-01-08 +--- +This patch header follows DEP-3: http://dep.debian.net/deps/dep3/ +--- a/src/CMakeLists.txt ++++ b/src/CMakeLists.txt +@@ -119,8 +119,8 @@ + # libz3.so.W.X. + # This indicates that no breaking API changes will be made within a single + # minor version. +- VERSION ${Z3_VERSION} +- SOVERSION ${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}) ++ VERSION 4 ++ SOVERSION 4) + + if (NOT MSVC) + # On UNIX like platforms if we don't change the OUTPUT_NAME +--- a/src/api/java/CMakeLists.txt ++++ b/src/api/java/CMakeLists.txt +@@ -52,6 +52,7 @@ + + # This prevents CMake from automatically defining ``z3java_EXPORTS`` + set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "") ++set_property(TARGET z3java PROPERTY NO_SONAME ON) + + # Rule to generate the ``com.microsoft.z3.enumerations`` package + # FIXME: This list of files is fragile +@@ -223,7 +224,7 @@ + ) + # FIXME: I don't think this the right installation location + set(Z3_JAVA_JNI_LIB_INSTALLDIR +- "${CMAKE_INSTALL_LIBDIR}" ++ "${CMAKE_INSTALL_LIBDIR}/jni" + CACHE + PATH + "Directory to install Z3 Java JNI bridge library relative to install prefix" diff --git a/debian/patches/03-pthread.patch b/debian/patches/03-pthread.patch new file mode 100644 index 0000000..db924b9 --- /dev/null +++ b/debian/patches/03-pthread.patch @@ -0,0 +1,17 @@ +Description: Fix build failure on riscv64 +Author: Aurelien Jarno +Origin: vendor, https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=948109#75 +Bug-Debian: https://bugs.debian.org/948109 +Last-Update: 2020-01-10 +--- +This patch header follows DEP-3: http://dep.debian.net/deps/dep3/ +--- a/CMakeLists.txt ++++ b/CMakeLists.txt +@@ -314,6 +314,7 @@ + ################################################################################ + # Threading support + ################################################################################ ++set(THREADS_PREFER_PTHREAD_FLAG TRUE) + find_package(Threads) + list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT}) + diff --git a/debian/patches/series b/debian/patches/series new file mode 100644 index 0000000..30b8e0e --- /dev/null +++ b/debian/patches/series @@ -0,0 +1,4 @@ +00-intrinsics.patch +01-reproducibility.patch +02-soname.patch +03-pthread.patch diff --git a/debian/python3-z3.install b/debian/python3-z3.install new file mode 100644 index 0000000..2f63d6b --- /dev/null +++ b/debian/python3-z3.install @@ -0,0 +1 @@ +usr/lib/python3/dist-packages/ diff --git a/debian/rules b/debian/rules new file mode 100755 index 0000000..3620e07 --- /dev/null +++ b/debian/rules @@ -0,0 +1,35 @@ +#!/usr/bin/make -f + +# Uncomment this to turn on verbose mode. +# export DH_VERBOSE=1 + +export DEB_BUILD_MAINT_OPTIONS = hardening=+all +export DEB_CXXFLAGS_MAINT_APPEND = -fPIC + +DEB_HOST_MULTIARCH ?= $(shell dpkg-architecture -qDEB_HOST_MULTIARCH) + +ifneq (,$(shell dh_listpackages -a | grep libz3-jni)) + WITH_JAVA ?= ON + WITH_JAVAHELPER ?= ,javahelper +else + WITH_JAVA ?= OFF + WITH_JAVAHELPER ?= +endif + +%: + dh $@ --with python3$(WITH_JAVAHELPER) + +override_dh_auto_configure: + dh_auto_configure --buildsystem=cmake+makefile -- \ + -DCMAKE_INSTALL_PYTHON_PKG_DIR=lib/python3/dist-packages \ + -DCMAKE_BUILD_TYPE=RelWithDebInfo \ + -DZ3_BUILD_PYTHON_BINDINGS=ON \ + -DZ3_BUILD_DOTNET_BINDINGS=OFF \ + -DZ3_BUILD_JAVA_BINDINGS=$(WITH_JAVA) + +override_dh_installchangelogs: + dh_installchangelogs RELEASE_NOTES + for p in python3-z3 libz3-java libz3-jni ; do \ + $(RM) -rf debian/$$p/usr/share/doc/$$p/ ; \ + ln -s libz3-dev debian/$$p/usr/share/doc/$$p || true ; \ + done diff --git a/debian/source/format b/debian/source/format new file mode 100644 index 0000000..163aaf8 --- /dev/null +++ b/debian/source/format @@ -0,0 +1 @@ +3.0 (quilt) diff --git a/debian/tests/control b/debian/tests/control new file mode 100644 index 0000000..ab0cbb1 --- /dev/null +++ b/debian/tests/control @@ -0,0 +1,6 @@ +Tests: import-z3-test include-z3-test run-z3-test +Depends: @, build-essential, python3 +Restrictions: superficial + +Tests: z3-int-logic-test python3-z3-int-logic-test +Depends: @, build-essential, python3 diff --git a/debian/tests/import-z3-test b/debian/tests/import-z3-test new file mode 100755 index 0000000..1da7304 --- /dev/null +++ b/debian/tests/import-z3-test @@ -0,0 +1,6 @@ +#!/usr/bin/env python3 + +# This is a superficial test that checks that the Python 3 module can +# actually be imported. + +import z3 diff --git a/debian/tests/include-z3-test b/debian/tests/include-z3-test new file mode 100755 index 0000000..b18ba8c --- /dev/null +++ b/debian/tests/include-z3-test @@ -0,0 +1,54 @@ +#!/bin/sh + +# This is a relatively superficial test that checks that one can +# include and compile with the z3.h (C) and z3++.h (C++) header files, +# and link with -lz3, to produce working executables. + +set -e + +TMPDIR=$(mktemp -d) +trap "rm -rf $TMPDIR" EXIT +cd $TMPDIR + +cat < test-include-z3-h.c +#include +int main () +{ + Z3_config cfg; + Z3_context ctx; + + cfg = Z3_mk_config (); + ctx = Z3_mk_context (cfg); + Z3_del_config (cfg); + + return 0; +} +EOF + +cat < test-include-z3pp-h.cc +#include + +using namespace z3; + +int main () +{ + context c; + + expr x = c.bool_const("x"); + expr y = c.bool_const("y"); + expr conj = (!(x && y)) == (!x || !y); + + solver s(c); + s.add(!conj); + + return 0; +} +EOF + +cc -o test-include-z3-h test-include-z3-h.c -lz3 +[ -x test-include-z3-h ] +./test-include-z3-h + +c++ -o test-include-z3pp-h test-include-z3pp-h.cc -lz3 +[ -x test-include-z3pp-h ] +./test-include-z3pp-h diff --git a/debian/tests/python3-z3-int-logic-test b/debian/tests/python3-z3-int-logic-test new file mode 100755 index 0000000..bee458c --- /dev/null +++ b/debian/tests/python3-z3-int-logic-test @@ -0,0 +1,18 @@ +#!/usr/bin/env python3 + +# This is a test that checks that the Python 3 module is functional by +# trying out a small example involving integer logic. + +from z3 import * + +x, y = Ints("x y") + +s = Solver() +s.add(x > 0, y > 0, x <= 2, y <= 2, x + 1 <= y) + +assert s.check() + +m = s.model() + +assert m[x] == 1 +assert m[y] == 2 diff --git a/debian/tests/run-z3-test b/debian/tests/run-z3-test new file mode 100755 index 0000000..9b6ddaf --- /dev/null +++ b/debian/tests/run-z3-test @@ -0,0 +1,23 @@ +#!/bin/sh + +# This is a superficial test that checks that the z3 executable is +# installed properly, and that one can execute a simple SMT-LIBv2 +# script with it. + +set -e + +TMPDIR=$(mktemp -d) +trap "rm -rf $TMPDIR" EXIT +cd $TMPDIR + +# Check that z3 runs at all +z3 --version > /dev/null + +cat < test.smt2 +(echo "Hello, world!") +(exit) +EOF + +z3 test.smt2 > out.txt +echo "Hello, world!" > expected.txt +diff out.txt expected.txt diff --git a/debian/tests/z3-int-logic-test b/debian/tests/z3-int-logic-test new file mode 100755 index 0000000..b2c7992 --- /dev/null +++ b/debian/tests/z3-int-logic-test @@ -0,0 +1,40 @@ +#!/bin/sh + +# This is a test that checks that the z3 executable is installed +# properly, and that one can execute a simple SMT-LIBv2 script +# involving some integer logic with the expected output. + +set -e + +TMPDIR=$(mktemp -d) +trap "rm -rf $TMPDIR" EXIT +cd $TMPDIR + +cat < test-sat.smt2 +(set-logic QF_LIA) +(declare-const x Int) +(declare-const y Int) +(assert (> x 0)) +(assert (> y x)) +(assert (> y 0)) +(check-sat) +EOF + +cat < test-unsat.smt2 +(set-logic QF_LIA) +(declare-const x Int) +(declare-const y Int) +(assert (> x 0)) +(assert (> y x)) +(assert (< y 0)) +(check-sat) +EOF + +echo "sat" > sat.txt +echo "unsat" > unsat.txt + +z3 test-sat.smt2 > out-sat.txt +diff out-sat.txt sat.txt + +z3 test-unsat.smt2 > out-unsat.txt +diff out-unsat.txt unsat.txt diff --git a/debian/watch b/debian/watch new file mode 100644 index 0000000..1e955f1 --- /dev/null +++ b/debian/watch @@ -0,0 +1,3 @@ +version=4 +opts=filenamemangle=s/.+\/(z3|Z3)-(\d\S*)\.tar\.gz/z3-$2\.tar\.gz/ \ + https://github.com/Z3Prover/z3/tags .*/(?:z3|Z3)-(\d\S*)\.tar\.gz diff --git a/debian/z3.1 b/debian/z3.1 new file mode 100644 index 0000000..540c008 --- /dev/null +++ b/debian/z3.1 @@ -0,0 +1,114 @@ +.\" Hey, EMACS: -*- nroff -*- +.\" First parameter, NAME, should be all caps +.\" Second parameter, SECTION, should be 1-8, maybe w/ subsection +.\" other parameters are allowed: see man(7), man(1) +.TH Z3 1 "May 25, 2015" +.\" Please adjust this date whenever revising the manpage. +.\" +.\" Some roff macros, for reference: +.\" .nh disable hyphenation +.\" .hy enable hyphenation +.\" .ad l left justify +.\" .ad b justify to both left and right margins +.\" .nf disable filling +.\" .fi enable filling +.\" .br insert line break +.\" .sp insert n+1 empty lines +.\" for manpage-specific macros, see man(7) +.SH NAME +z3 \- a state-of-the art theorem prover from Microsoft Research +.SH SYNOPSIS +.B z3 +.RI [ options ] +.RI [\-file:]file +.SH DESCRIPTION +This manual page documents briefly the +.B z3 +command. +.PP +.\" TeX users may be more comfortable with the \fB\fP and +.\" \fI\fP escape sequences to invode bold face and italics, +.\" respectively. +\fBz3\fP Z3 is a state-of-the art theorem prover from Microsoft Research. It can +be used to check the satisfiability of logical formulas over one or more +theories. Z3 offers a compelling match for software analysis and verification +tools, since several common software constructs map directly into supported +theories. +.SH Input format +.TP +.B \-smt +Use parser for SMT input format. +.TP +.B \-smt2 +Use parser for SMT 2 input format. +.TP +.B \-dl +Use parser for Datalog input format. +.TP +.B \-dimacs +Use parser for DIMACS input format. +.TP +.B \-log +Use parser for Z3 log input format. +.TP +.B \-in +Read formula from standard input. +.SH Miscellaneous +.TP +.B \-h | -? +Prints the usage information. +.TP +.B \-version +Prints version number of Z3. +.TP +.B \-v:level +Be verbose, where is the verbosity level. +.TP +.B \-nw +Disable warning messages. +.TP +.B \-p +Display Z3 global (and module) parameters. +.TP +.B \-pd +Display Z3 global (and module) parameter descriptions. +.TP +.B \-pm:name +Display Z3 module parameters. +.TP +.B \-pp:name +Display Z3 parameter description, if is not provided, then all module +names are listed. +.TP +.B \-\- +All remaining arguments are assumed to be part of the input file name. This +option allows Z3 to read files with strange names such as: \-foo.smt2. +.SH Resources +.TP +.B \-T:timeout +Set the timeout (in seconds). +.TP +.B \-t:timeout +Set the soft timeout (in milli seconds). It only kills the current query. +.TP +.B \-memory:Megabytes +Set a limit for virtual memory consumption. +.SH Output +.TP +.B \-st +Display statistics. +.SH Parameter setting +Global and module parameters can be set in the command line. +Use 'z3 \-p' for the complete list of global and module parameters. +.TP +.B param_name=value +For setting global parameters. +.TP +.B module_name.param_name=value +For setting module parameters. +.SH AUTHOR +Z3 Copyright 2006-2014 Microsoft Corp. +.PP +This manual page was written by Michael Tautschnig , +for the Debian project (and may be used by others). + diff --git a/debian/z3.install b/debian/z3.install new file mode 100644 index 0000000..6a54013 --- /dev/null +++ b/debian/z3.install @@ -0,0 +1 @@ +debian/tmp/usr/bin/z3