# NOTE: upstream does not make releases and has no version numbering scheme.
# We check the code out of git and use the date of the last commit as the
# version number.
%global owner    CVC4
%global gittag   fcd0cb325cef48c361c0eb182a3f87c199273b92
%global shorttag %(cut -b -7 <<< %{gittag})

Name:           lfsc
Version:        0.20180322
Release:        2%{?dist}
Summary:        SMT proof checker

License:        BSD
URL:            https://github.com/%{owner}/LFSC
Source0:        https://github.com/%{owner}/LFSC/archive/%{gittag}/%{name}-%{shorttag}.tar.gz
# Proof file used to check the validity of a build.
Source1:        check.plf
# The next few sources contain commonly used proof definitions
Source2:        http://clc.cs.uiowa.edu/lfsc/sat.plf
Source3:        http://clc.cs.uiowa.edu/lfsc/smt.plf
Source4:        http://clc.cs.uiowa.edu/lfsc/th_base.plf
Source5:        http://clc.cs.uiowa.edu/lfsc/th_real.plf
Source6:        http://clc.cs.uiowa.edu/lfsc/th_lra.plf
Source7:        http://clc.cs.uiowa.edu/lfsc/th_lra-cvc3.plf
Source8:        http://clc.cs.uiowa.edu/lfsc/color_base.plf
Source9:        http://clc.cs.uiowa.edu/lfsc/color_euf.plf
Source10:       http://clc.cs.uiowa.edu/lfsc/euf_interpolation.plf

BuildRequires:  cmake
BuildRequires:  gcc-c++
BuildRequires:  gmp-devel

%description
This package contains an SMT proof checker.

%package devel
Summary:        Files needed to compile side conditions
Requires:       %{name}%{?_isa} = %{version}-%{release}

%description devel
This package contains the files needed to compile a version of %{name} that
can execute a side condition.

%prep
%autosetup -n LFSC-%{gittag}

# We want to know about use of deprecated interfaces, and the code assumes that
# char == signed char
sed -i 's/Wno-deprecated/fsigned-char/' CMakeLists.txt

# Build a shared library instead of a static library, and give it an soname
sed -e 's/STATIC/SHARED/' \
    -e '/^[[:blank:]]*OUTPUT_NAME lfscc/i\  VERSION 0.0.0\  SOVERSION 0' \
    -e 's/ARCHIVE DESTINATION/LIBRARY DESTINATION/' \
    -i src/CMakeLists.txt

# Fix the library install path
if [ "%{_lib}" = "lib64" ]; then
  sed -i 's,/lib,/lib64,' src/CMakeLists.txt
fi

%build
%cmake
%make_build

%install
%make_install

# Install the proof files
mkdir -p %{buildroot}%{_datadir}/%{name}
cp -p %{SOURCE2} %{SOURCE3} %{SOURCE4} %{SOURCE5} %{SOURCE6} %{SOURCE7} \
   %{SOURCE8} %{SOURCE9} %{SOURCE10} %{buildroot}%{_datadir}/%{name}

%check
src/lfscc %{SOURCE2} %{SOURCE1}

%files
%license COPYING
%doc AUTHORS README.md
%{_bindir}/lfscc
%{_datadir}/%{name}/
%{_libdir}/liblfscc.so.*

%files devel
%{_includedir}/lfscc.h
%{_libdir}/liblfscc.so

%changelog
* Fri Jul 13 2018 Fedora Release Engineering <releng@fedoraproject.org> - 0.20180322-2
- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild

* Thu Jul  5 2018 Jerry James <loganjerry@gmail.com> - 0.20180322-1
- Initial RPM (unretired)