diff --git a/.gitignore b/.gitignore index e69de29..cdde729 100644 --- a/.gitignore +++ b/.gitignore @@ -0,0 +1 @@ +/Z3Prover-z3-29606b5.tar.gz diff --git a/sources b/sources index e69de29..6984e99 100644 --- a/sources +++ b/sources @@ -0,0 +1 @@ +634e88648020946f2895b77174f8f557 Z3Prover-z3-29606b5.tar.gz diff --git a/z3-sse2.patch b/z3-sse2.patch new file mode 100644 index 0000000..23bfb01 --- /dev/null +++ b/z3-sse2.patch @@ -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 + #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 + #endif + diff --git a/z3.spec b/z3.spec new file mode 100644 index 0000000..53cab32 --- /dev/null +++ b/z3.spec @@ -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 - 4.3.2-3.20150329git.29606b5 +- Fix issues found on review (bz 1206826) + +* Mon Mar 30 2015 Jerry James - 4.3.2-2.20150329git.29606b5 +- Update to latest git HEAD +- Include examples in -doc + +* Sat Mar 28 2015 Jerry James - 4.3.2-1.20150327git.ac21ffe +- Initial RPM