forked from openkylin/z3
Import Debian changes 4.8.7-ok1
z3 (4.8.7-ok1) yangtze; urgency=medium * Build for openKylin.
This commit is contained in:
openKylinBot
Lu zhiping
parent
65307b9f12
commit
dc061f3f95
|
|
@ -0,0 +1,5 @@
|
|||
z3 (4.8.7-ok1) yangtze; urgency=medium
|
||||
|
||||
* Build for openKylin.
|
||||
|
||||
-- openKylinBot <openKylinBot@openkylin.com> Mon, 25 Apr 2022 22:03:04 +0800
|
||||
|
|
@ -0,0 +1,96 @@
|
|||
Source: z3
|
||||
Section: science
|
||||
Priority: optional
|
||||
Maintainer: Openkylin Developers <packaging@lists.openkylin.top>
|
||||
Uploaders: Fabian Wolff <fabi.wolff@arcor.de>
|
||||
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.
|
||||
|
|
@ -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 <fabi.wolff@arcor.de>
|
||||
2011 Michael Tautschnig <mt@debian.org>
|
||||
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 <http://www.gnu.org/licenses/>
|
||||
.
|
||||
On Debian systems, the complete text of the GNU General
|
||||
Public License version 2 can be found in "/usr/share/common-licenses/GPL-2".
|
||||
|
|
@ -0,0 +1 @@
|
|||
README.md
|
||||
|
|
@ -0,0 +1,3 @@
|
|||
[DEFAULT]
|
||||
pristine-tar = True
|
||||
upstream-branch = upstream
|
||||
|
|
@ -0,0 +1 @@
|
|||
usr/lib/*/libz3.so.*
|
||||
|
|
@ -0,0 +1,2 @@
|
|||
usr/include/*
|
||||
usr/lib/*/libz3.so
|
||||
|
|
@ -0,0 +1 @@
|
|||
usr/share/java/
|
||||
|
|
@ -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
|
||||
|
|
@ -0,0 +1 @@
|
|||
usr/lib/*/jni/libz3java.so
|
||||
|
|
@ -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
|
||||
|
|
@ -0,0 +1 @@
|
|||
debian/z3.1
|
||||
|
|
@ -0,0 +1,67 @@
|
|||
Description: INTRINSICS are not universally available
|
||||
Author: Michael Tautschnig <mt@debian.org>
|
||||
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 <immintrin.h>
|
||||
-#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
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,16 @@
|
|||
Description: Remove the use of __DATE__ to make the build reproducible
|
||||
Author: Fabian Wolff <fabi.wolff@arcor.de>
|
||||
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;
|
||||
}
|
||||
|
|
@ -0,0 +1,37 @@
|
|||
Description: Set the SONAME properly
|
||||
Author: Fabian Wolff <fabi.wolff@arcor.de>
|
||||
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"
|
||||
|
|
@ -0,0 +1,17 @@
|
|||
Description: Fix build failure on riscv64
|
||||
Author: Aurelien Jarno <aurelien@aurel32.net>
|
||||
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})
|
||||
|
||||
|
|
@ -0,0 +1,4 @@
|
|||
00-intrinsics.patch
|
||||
01-reproducibility.patch
|
||||
02-soname.patch
|
||||
03-pthread.patch
|
||||
|
|
@ -0,0 +1 @@
|
|||
usr/lib/python3/dist-packages/
|
||||
|
|
@ -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
|
||||
|
|
@ -0,0 +1 @@
|
|||
3.0 (quilt)
|
||||
|
|
@ -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
|
||||
|
|
@ -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
|
||||
|
|
@ -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 <<EOF > test-include-z3-h.c
|
||||
#include <z3.h>
|
||||
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 <<EOF > test-include-z3pp-h.cc
|
||||
#include <z3++.h>
|
||||
|
||||
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
|
||||
|
|
@ -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
|
||||
|
|
@ -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 <<EOF > test.smt2
|
||||
(echo "Hello, world!")
|
||||
(exit)
|
||||
EOF
|
||||
|
||||
z3 test.smt2 > out.txt
|
||||
echo "Hello, world!" > expected.txt
|
||||
diff out.txt expected.txt
|
||||
|
|
@ -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 <<EOF > 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 <<EOF > 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
|
||||
|
|
@ -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
|
||||
|
|
@ -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 <n> 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<whatever>\fP and
|
||||
.\" \fI<whatever>\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 <level> 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 <name> parameters.
|
||||
.TP
|
||||
.B \-pp:name
|
||||
Display Z3 parameter description, if <name> 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 <mt@debian.org>,
|
||||
for the Debian project (and may be used by others).
|
||||
|
||||
|
|
@ -0,0 +1 @@
|
|||
debian/tmp/usr/bin/z3
|
||||
Loading…
Reference in New Issue