File bitwuzla.spec of Package bitwuzla

#
# spec file for package bitwuzla
#
# Copyright (c) 2025 Eyad Issa
#
# 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 https://bugs.opensuse.org/
#

%global symfpu_rev  22d993d
%global cadical_rev rel-2.1.2
%global sover       0

Name:           bitwuzla
Version:        0.8.0
Release:        0
Summary:        A Satisfiability Modulo Theories (SMT) solver
License:        MIT
URL:            https://bitwuzla.github.io/
Source0:        https://github.com/bitwuzla/bitwuzla/archive/%{version}/bitwuzla-%{version}.tar.gz
Source1:        https://github.com/martin-cs/symfpu/archive/%{symfpu_rev}/symfpu-%{symfpu_rev}.tar.gz
Source2:        https://github.com/arminbiere/cadical/archive/%{cadical_rev}/cadical-%{cadical_rev}.tar.gz
BuildRequires:  cmake
BuildRequires:  gcc-c++
BuildRequires:  git
BuildRequires:  gmp-devel
BuildRequires:  gtest
BuildRequires:  kissat-devel
BuildRequires:  meson >= 0.64
BuildRequires:  ninja
BuildRequires:  pkgconfig
BuildRequires:  python3 > 3.7
BuildRequires:  python3-Cython
BuildRequires:  python3-devel
BuildRequires:  python3-pytest

%description
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the
theories of fixed-size bit-vectors, floating-point arithmetic,
arrays, uninterpreted functions and their combinations.

%package devel

Summary:        Development files for the Bitwuzla SMT solver
Requires:       %{name} = %{version}-%{release}

%description devel
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the
theories of fixed-size bit-vectors, floating-point arithmetic,
arrays, uninterpreted functions and their combinations.

This package contains the development files for Bitwuzla.


%package -n libbitwuzla%{sover}
Summary:        Shared library for the Bitwuzla SMT solver

%description -n libbitwuzla%{sover}
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the
theories of fixed-size bit-vectors, floating-point arithmetic,
arrays, uninterpreted functions and their combinations.

This package contains the shared library for Bitwuzla.


%package -n python3-bitwuzla
Summary:        Python bindings for the Bitwuzla SMT solver
Requires:       %{name} = %{version}-%{release}


%description -n python3-bitwuzla
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the
theories of fixed-size bit-vectors, floating-point arithmetic,
arrays, uninterpreted functions and their combinations.

This package contains the Python bindings for Bitwuzla.


%prep
%autosetup -p1

# Extract symfpu
mkdir -p subprojects/symfpu
tar   -C subprojects/symfpu --strip-components=1 -x -f %{SOURCE1}

# Extract cadical
mkdir -p subprojects/cadical-%{cadical_rev}
tar   -C subprojects/cadical-%{cadical_rev} --strip-components=1 -x -f %{SOURCE2}


%ldconfig_scriptlets -n libbitwuzla%{sover}


%build
%{__meson} subprojects packagefiles --apply
%meson \
  -Ddefault_library=shared \
  -Dpython=true \
  -Dkissat=true \
  -Dunit_testing=disabled \
  -Dtesting=disabled \
  -Dstrip=false \
  %{nil}
%meson_build


%install
%meson_install


%check
%meson_test


%ldconfig_scriptlets


%files
%license COPYING
%doc README.md
%{_bindir}/bitwuzla

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

%files devel
%{_includedir}/bitwuzla/
%{_libdir}/libbitwuzla*.so
%{_libdir}/pkgconfig/bitwuzla.pc

%files -n python3-bitwuzla
%{python3_sitearch}/bitwuzla*

%changelog