openSUSE Build Service

Overview Repositories Revisions Requests Users Attributes Meta

File z3.spec of Package z3

#
# spec file for package z3, for use with Pharos
#
# Copyright (c) 2018 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.12.1
%define sover 4_12
Name:           z3
Version:        4.12.1
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.gz
# this patch removed the timestamp from version and may be unnecessary now
#Patch0:         remove-timestamp.patch
BuildRequires:  cmake
%if 0%{?sle_version} == 150300 && 0%{?is_opensuse}
BuildRequires:  gcc10-c++
%else
BuildRequires:  gcc-c++
%endif
BuildRequires:  gmp-devel
BuildRequires:  ninja
BuildRequires:  python3-devel
BuildRequires:  java-17-openjdk-devel

%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 -n libz3java
Summary:        Java JNI library for the Z3 SMT theorem prover
Group:          System/Libraries

%description -n libz3java
Java JNI library for the Z3 SMT theorem prover. Required for use
with the Java bindings.

%package devel
Summary:        Development files for Z3
Group:          Development/Languages/C and C++
Requires:       libz3-%{sover} = %{version}

%description devel
Development files for the Z3 library.

%package -n python3-%{name}
Summary:        Python bindings for Z3
Group:          Development/Languages/Python
Requires:       %{name} = %{version}

%description -n python3-%{name}
Python bindings for the Z3 library.

%package -n java-%{name}
Summary:        Java bindings for Z3
Group:          Development/Languages/Java
Requires:       %{name} = %{version}
Requires:       libz3java = %{version}

%description -n java-%{name}
Java bindings for the Z3 library.

%prep
#setup -q -n {name}-{version}
%setup -c -q
#patch0 -p1

%build
%define __builder ninja
%if 0%{?sle_version} == 150300 && 0%{?is_opensuse}
# perform Leap 15.3
export CC=gcc-10
export CXX=g++-10
export Z3OPTI=true
%else
# e.g. tumbleweed
export CC=gcc
export CXX=g++
export Z3OPTI=true
%endif
%cmake \
  -DZ3_BUILD_LIBZ3_SHARED=true \
  -DZ3_USE_LIB_GMP=true \
  -DZ3_BUILD_PYTHON_BINDINGS=true \
  -DZ3_INSTALL_PYTHON_BINDINGS=true \
  -DPYTHON_EXECUTABLE=%{_bindir}/python3 \
  -DZ3_BUILD_JAVA_BINDINGS=true \
  -DZ3_INSTALL_JAVA_BINDINGS=true \
  -DZ3_JAVA_JAR_INSTALLDIR=%{_javadir} \
  -DZ3_JAVA_JNI_LIB_INSTALLDIRR=%{_jnidir} \
  -DZ3_ENABLE_EXAMPLE_TARGETS=false \
  -DZ3_LINK_TIME_OPTIMIZATION=$Z3OPTI \
  -DCXX_STANDARD="14" \
  -DCXX_STANDARD_REQUIRED="ON" \
  -DCMAKE_BUILD_TYPE=Release \
  -DCMAKE_CXX_FLAGS='-D_GLIBCXX_USE_CXX11_ABI=1' \
  -DCMAKE_C_COMPILER=$CC \
  -DCMAKE_CXX_COMPILER=$CXX

%cmake_build

%install
%cmake_install

%post -n libz3-%{sover} -p /sbin/ldconfig
%postun -n libz3-%{sover} -p /sbin/ldconfig
%post -n libz3java -p /sbin/ldconfig
%postun -n libz3java -p /sbin/ldconfig

%files
%license LICENSE.txt
%doc README.md RELEASE_NOTES.md README-CMake.md
%{_bindir}/z3

%files -n libz3-%{sover}
%{_libdir}/libz3.so.*

%files -n libz3java
#{_jnidir}/libz3java.so
%{_libdir}/libz3java.so

%files devel
%{_includedir}/z3*.h
%{_libdir}/libz3.so
%dir %{_libdir}/cmake/z3/
%{_libdir}/cmake/z3/Z3Config.cmake
%{_libdir}/cmake/z3/Z3ConfigVersion.cmake
%{_libdir}/cmake/z3/Z3Targets*
%{_libdir}/pkgconfig/z3.pc

%files -n python3-%{name}
%dir %{python3_sitelib}/%{name}
%{python3_sitelib}/%{name}/*py

%files -n java-%{name}
%{_javadir}/*.jar

%changelog

Places

File z3.spec of Package z3

Places