Initial import.
This commit is contained in:
parent
8d8257e102
commit
4dc7a51663
1
.gitignore
vendored
1
.gitignore
vendored
@ -0,0 +1 @@
|
|||||||
|
/Z3Prover-z3-29606b5.tar.gz
|
22
z3-sse2.patch
Normal file
22
z3-sse2.patch
Normal file
@ -0,0 +1,22 @@
|
|||||||
|
diff --git a/src/util/hwf.cpp b/src/util/hwf.cpp
|
||||||
|
index 40d20b6..afcde2d 100644
|
||||||
|
--- a/src/util/hwf.cpp
|
||||||
|
+++ b/src/util/hwf.cpp
|
||||||
|
@@ -31,7 +31,7 @@ Revision History:
|
||||||
|
#include <fenv.h>
|
||||||
|
#endif
|
||||||
|
|
||||||
|
-#ifndef _M_IA64
|
||||||
|
+#ifdef __x86_64
|
||||||
|
#define USE_INTRINSICS
|
||||||
|
#endif
|
||||||
|
|
||||||
|
@@ -51,7 +51,7 @@ Revision History:
|
||||||
|
// Luckily, these are kind of standardized, at least for Windows/Linux/OSX.
|
||||||
|
#ifdef __clang__
|
||||||
|
#undef USE_INTRINSICS
|
||||||
|
-#else
|
||||||
|
+#elif defined(USE_INTRINSICS)
|
||||||
|
#include <emmintrin.h>
|
||||||
|
#endif
|
||||||
|
|
268
z3.spec
Normal file
268
z3.spec
Normal file
@ -0,0 +1,268 @@
|
|||||||
|
# Python 3 NOTE: Although there are references to python 3 support in the
|
||||||
|
# source tree, building with python 3 currently fails. I fixed several
|
||||||
|
# problems before giving up. If someone would like to fix all of the problems
|
||||||
|
# and submit the results upstream, I'm sure many people would be grateful.
|
||||||
|
|
||||||
|
%global opt %(test -x %{_bindir}/ocamlopt && echo 1 || echo 0)
|
||||||
|
%global gitdate 20150329
|
||||||
|
%global gittag 29606b5179f76783ffb0c2ca0ed9d614847064b3
|
||||||
|
%global shorttag %(cut -b -7 <<< %{gittag})
|
||||||
|
%global medtag %(cut -b -12 <<< %{gittag})
|
||||||
|
%global user Z3Prover
|
||||||
|
|
||||||
|
Name: z3
|
||||||
|
Version: 4.3.2
|
||||||
|
Release: 3.%{gitdate}git.%{shorttag}%{?dist}
|
||||||
|
Summary: Satisfiability Modulo Theories (SMT) solver
|
||||||
|
|
||||||
|
License: MIT
|
||||||
|
URL: https://github.com/Z3Prover/z3
|
||||||
|
Source0: https://github.com/%{user}/%{name}/tarball/%{gittag}/%{user}-%{name}-%{shorttag}.tar.gz
|
||||||
|
# Do not try to build with SSE2 on non-x86_64 arches
|
||||||
|
Patch0: %{name}-sse2.patch
|
||||||
|
|
||||||
|
BuildRequires: doxygen
|
||||||
|
BuildRequires: gmp-devel
|
||||||
|
BuildRequires: graphviz
|
||||||
|
BuildRequires: java-devel
|
||||||
|
BuildRequires: jpackage-utils
|
||||||
|
BuildRequires: ocaml
|
||||||
|
BuildRequires: ocaml-camlidl-devel
|
||||||
|
BuildRequires: python2-devel
|
||||||
|
|
||||||
|
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
||||||
|
|
||||||
|
%description
|
||||||
|
Z3 is a satisfiability modulo theories (SMT) solver; given a set of
|
||||||
|
constraints with variables, it reports a set of values for those
|
||||||
|
variables that would meet the constraints. The Z3 input format is an
|
||||||
|
extension of the one defined by the SMT-LIB 2.0 standard. Z3 supports
|
||||||
|
arithmetic, fixed-size bit-vectors, extensional arrays, datatypes,
|
||||||
|
uninterpreted functions, and quantifiers.
|
||||||
|
|
||||||
|
%package libs
|
||||||
|
Summary: Library for applications that use z3 functionality
|
||||||
|
|
||||||
|
%description libs
|
||||||
|
Library for applications that use z3 functionality.
|
||||||
|
|
||||||
|
%package devel
|
||||||
|
Summary: Header files for build applications that use z3
|
||||||
|
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
||||||
|
|
||||||
|
%description devel
|
||||||
|
Header files for build applications that use z3.
|
||||||
|
|
||||||
|
%package doc
|
||||||
|
Summary: API documentation for Z3
|
||||||
|
BuildArch: noarch
|
||||||
|
|
||||||
|
%description doc
|
||||||
|
API documentation for Z3.
|
||||||
|
|
||||||
|
%package -n java-%{name}
|
||||||
|
Summary: Java interface to z3
|
||||||
|
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
||||||
|
Requires: java
|
||||||
|
Requires: jpackage-utils
|
||||||
|
|
||||||
|
%description -n java-%{name}
|
||||||
|
Java interface to z3.
|
||||||
|
|
||||||
|
%package -n ocaml-%{name}
|
||||||
|
Summary: Ocaml interface to z3
|
||||||
|
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
||||||
|
|
||||||
|
%description -n ocaml-%{name}
|
||||||
|
Ocaml interface to z3.
|
||||||
|
|
||||||
|
%package -n ocaml-%{name}-devel
|
||||||
|
Summary: Files for building ocaml applications that use z3
|
||||||
|
Requires: ocaml-%{name}%{?_isa} = %{version}-%{release}
|
||||||
|
|
||||||
|
%description -n ocaml-%{name}-devel
|
||||||
|
Files for building ocaml applications that use z3.
|
||||||
|
|
||||||
|
%package -n python-%{name}
|
||||||
|
Summary: Python 2 interface to z3
|
||||||
|
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
|
||||||
|
|
||||||
|
%description -n python-%{name}
|
||||||
|
Python 2 interface to z3.
|
||||||
|
|
||||||
|
%prep
|
||||||
|
%setup -q -n %{user}-%{name}-%{shorttag}
|
||||||
|
%patch0 -p1
|
||||||
|
|
||||||
|
# Install python objects into the right place, enable verbose builds, use
|
||||||
|
# Fedora CFLAGS, preserve timestamps when installing, include the entire
|
||||||
|
# contents of the archives in the library, link the library with the correct
|
||||||
|
# flags, build the library with -fPIC on all arches, and use an soname.
|
||||||
|
sed -e "s|^\(PYTHON_PACKAGE_DIR=\).*|\1'%{python2_sitearch}/z3'|" \
|
||||||
|
-e "s|\(PYTHON_PACKAGE_DIR = \).*|\1'%{buildroot}%{python2_sitearch}/z3'|" \
|
||||||
|
-e 's/@$(CXX)/$(CXX)/' \
|
||||||
|
-e 's/ -O3//;s/ -fomit-frame-pointer//' \
|
||||||
|
-e "s/@cp /&-p /" \
|
||||||
|
-e "s/\(SLIBEXTRAFLAGS = '\)'/\1-Wl,--no-whole-archive -Wl,--as-needed'/" \
|
||||||
|
-e "s|-shared|& $RPM_LD_FLAGS -Wl,--whole-archive|" \
|
||||||
|
-e 's/\(libz3$(SO_EXT)\)\(\\n\)/\1 -Wl,--no-whole-archive\2/' \
|
||||||
|
-e '/fPIC/d;' \
|
||||||
|
-e "s/'tstomp\.cpp',/& '-fPIC',/" \
|
||||||
|
-e 's/-shared/& -Wl,-h,lib%{name}.so.0/' \
|
||||||
|
-i scripts/mk_util.py
|
||||||
|
|
||||||
|
# Do not try to build with SSE2 support on non-x86_64 arches.
|
||||||
|
%ifnarch x86_64
|
||||||
|
sed -i '/msse2/d;s/ -mfpmath=sse//' scripts/mk_util.py
|
||||||
|
%endif
|
||||||
|
|
||||||
|
# Comply with the Java packaging guidelines
|
||||||
|
sed -e "s/\(System\.load\)Library/\1/" \
|
||||||
|
-e "s,get_component('java')\.dll_name.*,'%{_libdir}/z3/libz3java.so')," \
|
||||||
|
-i scripts/update_api.py
|
||||||
|
|
||||||
|
# Fix character encoding
|
||||||
|
iconv -f iso8859-1 -t utf-8 RELEASE_NOTES > RELEASE_NOTES.utf8
|
||||||
|
touch -r RELEASE_NOTES RELEASE_NOTES.utf8
|
||||||
|
mv -f RELEASE_NOTES.utf8 RELEASE_NOTES
|
||||||
|
|
||||||
|
# Fix permissions
|
||||||
|
chmod a-x examples/interp/iz3.cpp
|
||||||
|
|
||||||
|
%build
|
||||||
|
export CXXFLAGS="$RPM_OPT_FLAGS -fPIC"
|
||||||
|
export LDFLAGS="$RPM_LD_FLAGS -Wl,--as-needed"
|
||||||
|
export LANG="en_US.UTF-8"
|
||||||
|
export PYTHON="%{__python2}"
|
||||||
|
|
||||||
|
# This is NOT an autoconf-generated configure script.
|
||||||
|
./configure -p %{buildroot}%{_prefix} --githash=%{medtag} --gmp --java
|
||||||
|
make %{?_smp_mflags} -C build
|
||||||
|
|
||||||
|
# The z3 binary is NOT linked with libz3, but instead has duplicate copies of a
|
||||||
|
# lot of object files, so rebuild it. But first, add library links.
|
||||||
|
pushd build
|
||||||
|
mv libz3.so libz3.so.0.0.0
|
||||||
|
ln -s libz3.so.0.0.0 libz3.so.0
|
||||||
|
ln -s libz3.so.0 libz3.so
|
||||||
|
g++ $CXXFLAGS -fopenmp -o z3 shell/*.o $LDFLAGS -L. -lz3
|
||||||
|
popd
|
||||||
|
|
||||||
|
# Build the ocaml interface
|
||||||
|
pushd src/api/ml
|
||||||
|
./generate_mlapi.sh
|
||||||
|
%if %{opt}
|
||||||
|
ocamlopt -c -g -ccopt -g -ccopt -fomit-frame-pointer -ccopt -Wno-cast-qual \
|
||||||
|
-I .. z3_stubs.c z3_theory_stubs.c z3.mli z3.ml
|
||||||
|
ar rcs libz3stubs.a z3.o z3_stubs.o z3_theory_stubs.o
|
||||||
|
ocamlopt -a -g -ccopt -g -cclib -L$PWD/../../../build -cclib -lz3 \
|
||||||
|
-cclib -lcamlidl -cclib -lz3stubs z3.cmx -o z3.cmxa
|
||||||
|
%endif
|
||||||
|
ocamlc -c -g -ccopt -g -ccopt -fomit-frame-pointer -ccopt -Wno-cast-qual \
|
||||||
|
-I .. z3_stubs.c z3_theory_stubs.c z3.mli z3.ml
|
||||||
|
ar rcs libz3stubs.a z3.o z3_stubs.o z3_theory_stubs.o
|
||||||
|
ocamlc -custom -a -g -ccopt -g -cclib -L$PWD/../../../build -cclib -lz3 \
|
||||||
|
-cclib -lcamlidl -cclib -lz3stubs z3.cmo -o z3.cma
|
||||||
|
ocamlmktop -o ocamlz3 z3.cma -ccopt -L. -cclib -lz3 -cclib -lcamlidl
|
||||||
|
popd
|
||||||
|
|
||||||
|
# Build the documentation
|
||||||
|
pushd doc
|
||||||
|
%{__python2} mk_api_doc.py
|
||||||
|
popd
|
||||||
|
|
||||||
|
%install
|
||||||
|
export LANG="en_US.UTF-8"
|
||||||
|
|
||||||
|
mkdir -p %{buildroot}%{python2_sitearch}/%{name}
|
||||||
|
make -C build install
|
||||||
|
|
||||||
|
# On 64-bit systems, move the library to the right directory
|
||||||
|
if [ "%{_libdir}" != "%{_prefix}/lib" ]; then
|
||||||
|
mkdir -p %{buildroot}%{_libdir}
|
||||||
|
mv %{buildroot}%{_prefix}/lib/libz3.so* %{buildroot}%{_libdir}
|
||||||
|
fi
|
||||||
|
|
||||||
|
# Make library links
|
||||||
|
mv %{buildroot}%{_libdir}/libz3.so %{buildroot}%{_libdir}/libz3.so.0.0.0
|
||||||
|
ln -s libz3.so.0.0.0 %{buildroot}%{_libdir}/libz3.so.0
|
||||||
|
ln -s libz3.so.0 %{buildroot}%{_libdir}/libz3.so
|
||||||
|
|
||||||
|
# Move the header files into their own directory
|
||||||
|
mkdir -p %{buildroot}%{_includedir}/%{name}
|
||||||
|
mv %{buildroot}%{_includedir}/*.h %{buildroot}%{_includedir}/%{name}
|
||||||
|
|
||||||
|
# Link, rather than copy, the library into the python dir
|
||||||
|
rm -f %{buildroot}%{python2_sitearch}/%{name}/lib%{name}.so
|
||||||
|
ln -s %{_libdir}/lib%{name}.so.0 \
|
||||||
|
%{buildroot}%{python2_sitearch}/%{name}/lib%{name}.so
|
||||||
|
|
||||||
|
# Install the Ocaml interface
|
||||||
|
mkdir -p %{buildroot}%{_libdir}/ocaml/%{name}
|
||||||
|
cp -p src/api/ml/ocamlz3 %{buildroot}%{_bindir}
|
||||||
|
%if %{opt}
|
||||||
|
cp -p src/api/ml/%{name}.cmxa %{buildroot}%{_libdir}/ocaml/%{name}
|
||||||
|
%endif
|
||||||
|
cp -p src/api/ml/%{name}.{cma,mli} %{buildroot}%{_libdir}/ocaml/%{name}
|
||||||
|
|
||||||
|
# Install the Java interface
|
||||||
|
mkdir -p %{buildroot}%{_libdir}/%{name}
|
||||||
|
mkdir -p %{buildroot}%{_jnidir}
|
||||||
|
cp -p build/com.microsoft.z3.jar %{buildroot}%{_jnidir}
|
||||||
|
ln -s %{_jnidir}/com.microsoft.z3.jar %{buildroot}%{_libdir}/%{name}
|
||||||
|
cp -p build/lib%{name}java.so %{buildroot}%{_libdir}/%{name}
|
||||||
|
|
||||||
|
# Fix permissions
|
||||||
|
chmod 0755 %{buildroot}%{_bindir}/* %{buildroot}%{_libdir}/*.so.0.0.0 \
|
||||||
|
%{buildroot}%{_libdir}/%{name}/*.so
|
||||||
|
|
||||||
|
%check
|
||||||
|
export LANG="en_US.UTF-8"
|
||||||
|
pushd build
|
||||||
|
make test
|
||||||
|
./test-z3 /a
|
||||||
|
popd
|
||||||
|
|
||||||
|
%post libs -p /sbin/ldconfig
|
||||||
|
|
||||||
|
%postun libs -p /sbin/ldconfig
|
||||||
|
|
||||||
|
%files
|
||||||
|
%doc README RELEASE_NOTES
|
||||||
|
%{_bindir}/%{name}
|
||||||
|
|
||||||
|
%files libs
|
||||||
|
%license LICENSE.txt
|
||||||
|
%{_libdir}/lib%{name}.so.*
|
||||||
|
|
||||||
|
%files devel
|
||||||
|
%{_includedir}/%{name}/
|
||||||
|
%{_libdir}/lib%{name}.so
|
||||||
|
|
||||||
|
%files doc
|
||||||
|
%doc doc/api/html examples
|
||||||
|
%license LICENSE.txt
|
||||||
|
|
||||||
|
%files -n java-%{name}
|
||||||
|
%{_libdir}/%{name}/
|
||||||
|
%{_jnidir}/com.microsoft.z3.jar
|
||||||
|
|
||||||
|
%files -n ocaml-%{name}
|
||||||
|
%{_bindir}/ocaml%{name}
|
||||||
|
|
||||||
|
%files -n ocaml-%{name}-devel
|
||||||
|
%{_libdir}/ocaml/%{name}/
|
||||||
|
|
||||||
|
%files -n python-%{name}
|
||||||
|
%{python2_sitearch}/%{name}/
|
||||||
|
|
||||||
|
%changelog
|
||||||
|
* Wed Apr 22 2015 Jerry James <loganjerry@gmail.com> - 4.3.2-3.20150329git.29606b5
|
||||||
|
- Fix issues found on review (bz 1206826)
|
||||||
|
|
||||||
|
* Mon Mar 30 2015 Jerry James <loganjerry@gmail.com> - 4.3.2-2.20150329git.29606b5
|
||||||
|
- Update to latest git HEAD
|
||||||
|
- Include examples in -doc
|
||||||
|
|
||||||
|
* Sat Mar 28 2015 Jerry James <loganjerry@gmail.com> - 4.3.2-1.20150327git.ac21ffe
|
||||||
|
- Initial RPM
|
Loading…
Reference in New Issue
Block a user