File z3.spec of Package z3
#
# spec file for package z3
#
# Copyright (c) 2017 SUSE LINUX GmbH, Nuernberg, Germany.
#
# All modifications and additions to the file contributed by third parties
# remain the property of their copyright owners, unless otherwise agreed
# upon. The license for this file, and modifications and additions to the
# file, is the same license as for the pristine package itself (unless the
# license for the pristine package is not an Open Source License, in which
# case the license is the MIT License). An "Open Source License" is a
# license that conforms to the Open Source Definition (Version 1.9)
# published by the Open Source Initiative.
# Please submit bugfixes or comments via http://bugs.opensuse.org/
#
%define version_unconverted 4.5.0+git.20170313
%define sover 4_5
Name: z3
Version: 4.5.0+git.20170313
Release: 0
Summary: Theorem prover from Microsoft Research
License: MIT
Group: Productivity/Scientific/Other
Url: https://github.com/Z3Prover/z3/wiki
Source0: %{name}-%{version}.tar.xz
Patch0: remove-timestamp.patch
BuildRequires: cmake
BuildRequires: gcc-c++
BuildRequires: gmp-devel
BuildRequires: ninja
BuildRequires: python-devel
BuildRequires: xz
%description
Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates
several decision procedures: Linear real and integer arithmetic,
fixed-size bit vectors, uninterpreted functions, extensional arrays,
quantifiers and model generation.
%package -n libz3-%{sover}
Summary: Library for the Z3 SMT theorem prover
Group: System/Libraries
%description -n libz3-%{sover}
Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates
several decision procedures.
This subpackage contains the Z3 runtime library needed for Z3 and
other projects.
%package devel
Summary: Development files for Z3
Group: Development/Languages/C and C++
Requires: libz3-%{sover} = %{version}
%description devel
Developmnet files for the Z3 library.
%package -n python-%{name}
Summary: Python bindings for Z3
Group: Development/Languages/Python
Requires: %{name} = %{version}
Provides: %{name}-python = %{version}
Obsoletes: %{name}-python < %{version}
%description -n python-%{name}
Python bindings for the Z3 library.
%prep
%setup -q
%patch0 -p1
%build
%define __builder ninja
python contrib/cmake/bootstrap.py create
%cmake \
-DBUILD_LIBZ3_SHARED=true \
-DUSE_LIB_GMP=true \
-DBUILD_PYTHON_BINDINGS=true \
-DINSTALL_PYTHON_BINDINGS=true \
-DCMAKE_EXE_LINKER_FLAGS="" \
-DCMAKE_SHARED_LINKER_FLAGS="" \
-DENABLE_EXAMPLE_TARGETS=false
%make_jobs
%install
%cmake_install
%post -n libz3-%{sover} -p /sbin/ldconfig
%postun -n libz3-%{sover} -p /sbin/ldconfig
%files
%defattr(-,root,root)
%doc LICENSE.txt README.md RELEASE_NOTES
%{_bindir}/z3
%files -n libz3-%{sover}
%defattr(-,root,root)
%{_libdir}/libz3.so.*
%files devel
%defattr(-,root,root)
%{_includedir}/z3*.h
%{_libdir}/libz3.so
%dir %{_libdir}/cmake/z3/
%{_libdir}/cmake/z3/Z3Config.cmake
%{_libdir}/cmake/z3/Z3Targets*
%files -n python-%{name}
%defattr(-,root,root)
%dir %{python_sitelib}/%{name}
%{python_sitelib}/%{name}/*py
%changelog