Name:           yices
Version:        2.5.4
Release:        3%{?dist}
Summary:        SMT solver

License:        GPLv3+
URL:            http://yices.csl.sri.com/
Source0:        https://github.com/SRI-CSL/yices2/archive/Yices-%{version}.tar.gz

BuildRequires:  gcc
BuildRequires:  gmp-devel
BuildRequires:  gperf
BuildRequires:  libpoly-devel
BuildRequires:  libtool
BuildRequires:  tex(latex)

%description
Yices 2 is an efficient SMT solver that decides the satisfiability of
formulas containing uninterpreted function symbols with equality, linear
real and integer arithmetic, bitvectors, scalar types, and tuples.

Yices 2 can process input written in the SMT-LIB notation (both versions
2.0 and 1.2 are supported).

Alternatively, you can write specifications using the Yices 2
specification language, which includes tuples and scalar types.

Yices 2 can also be used as a library in other software.

%package devel
Summary:        Development files for yices
Requires:       %{name}%{?_isa} = %{version}-%{release}
Requires:       gmp-devel%{?_isa}

%description devel
This package contains the header files necessary for developing programs
which use yices.

%package tools
Summary:        Command line tools that use the yices library
Requires:       %{name}%{?_isa} = %{version}-%{release}

%description tools
Command line tools that use the yices library.

%package doc
Summary:        Documentation for yices

%description doc
This package contains yices documentation.

%prep
%setup -q -n yices2-Yices-%{version}

# Do not try to avoid -fstack-protector
sed -i '/NO_STACK_PROTECTOR=""/,/AC_SUBST(NO_STACK_PROTECTOR)/d' configure.ac

# Generate the configure script
autoreconf -fi

# Fix end of line encodings
sed -i 's/\r//' examples/{jinpeng,problem_with_input}.ys

# Fix permissions
sed -i 's/cp/install -m 0644/' utils/make_source_version

%build
%configure --enable-mcsat
mv configs/make.include.%{_host} configs/make.include.$(./config.guess)
make %{?_smp_mflags} MODE=debug

# Build the manual
pushd doc/manual
pdflatex manual
bibtex manual
pdflatex manual
pdflatex manual
popd

%install
make install prefix=%{buildroot}%{_prefix} exec_prefix=%{buildroot}%{_prefix} \
     bindir=%{buildroot}%{_bindir} libdir=%{buildroot}%{_libdir} \
     includedir=%{buildroot}%{_includedir}/%{name} MODE=debug
rm -f %{buildroot}%{_libdir}/libyices.a
mkdir -p %{buildroot}%{_mandir}/man1
cp -p doc/*.1 %{buildroot}%{_mandir}/man1

%check
make check MODE=debug

%post -p /sbin/ldconfig

%postun -p /sbin/ldconfig

%files
%doc doc/YICES-LANGUAGE
%license LICENSE.txt
%{_libdir}/*.so.*

%files devel
%{_includedir}/%{name}/
%{_libdir}/*.so

%files tools
%{_bindir}/yices
%{_bindir}/yices-sat
%{_bindir}/yices-smt
%{_bindir}/yices-smt2
%{_mandir}/man1/*

%files doc
%doc doc/manual/manual.pdf examples
%license LICENSE.txt

%changelog
* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.4-3
- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild

* Tue Jan  2 2018 Jerry James <loganjerry@gmail.com> - 2.5.4-2
- Add a -doc subpackage
- Fix end of line encodings
- Fix permissions on yices_debug_version.c

* Mon Jan  1 2018 Jerry James <loganjerry@gmail.com> - 2.5.4-1
- Initial RPM