Name:           picosat
Version:        913
Release:        2%{?dist}
Summary:        A SAT solver

Group:          Applications/Engineering
License:        MIT
URL:            http://fmv.jku.at/picosat/
Source0:        http://fmv.jku.at/picosat/%{name}-%{version}.tar.gz
# Thanks to David Wheeler for the man page.
Source1:        picosat.1
# This patch was sent upstream on 2 June 2009 and (mostly) incorporated into
# the unreleased upstream version 917.  It does the following:
# - Links the binary against a shared library instead of a static library.
# - Does not build the static library.
# - Gives the resulting library an soname.
Patch0:         picosat-sharedlib.patch
# This patch is needed by csisat.  I asked upstream about it on 2 June 2009,
# and they tell me that the next release of picosat will include this
# functionality, although implemented differently.  Until that release, and
# the corresponding adapation of the csisat code, though, we need this patch.
Patch1:         picosat-proof-access.patch
BuildRoot:      %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)

# gzip required (see app.c); find-requires can't see into C code to find it
Requires:       gzip, %{name}-libs = %{version}-%{release}

%description
PicoSAT solves the SAT problem, which is the classical NP complete
problem of searching for a satisfying assignment of a propositional
formula in conjunctive normal form (CNF).  PicoSAT can generate proofs
and cores in memory by compressing the proof trace.  It supports the
proof format of TraceCheck.

%package libs
Group:          Development/Libraries
Summary:        A SAT solver library

%description libs
The PicoSAT library, which contains routines that solve the SAT problem.
The library has a simple API which is similar to that of previous
solvers by the same authors.

%package devel
Group:          Development/Libraries
Summary:        Development files for PicoSAT
Requires:       %{name}-libs = %{version}-%{release}

%description devel
Headers and other develpment files for PicoSAT.

%prep
%setup -q
%patch0 -p1
%patch1 -p1

%build
# The configure script is NOT autoconf-generated and chooses its own CFLAGS,
# so we mimic its effects instead of using it.
sed -e "s/@CC@/gcc/" \
    -e "s/@CFLAGS@/${RPM_OPT_FLAGS} -DSTATS -DTRACE -DNDEBUG/" \
    -e "s/@TARGETS@/picosat libpicosat.so/" \
  makefile.in > makefile
make %{?_smp_mflags}

%install
rm -rf $RPM_BUILD_ROOT

# Install the header file
mkdir -p $RPM_BUILD_ROOT%{_includedir}
cp -p picosat.h $RPM_BUILD_ROOT%{_includedir}

# Install the library
mkdir -p $RPM_BUILD_ROOT%{_libdir}
cp -p libpicosat.so $RPM_BUILD_ROOT%{_libdir}/libpicosat.so.0.0.%{version}
ln -s libpicosat.so.0.0.%{version} $RPM_BUILD_ROOT%{_libdir}/libpicosat.so.0
ln -s libpicosat.so.0 $RPM_BUILD_ROOT%{_libdir}/libpicosat.so

# Install the binary
mkdir -p $RPM_BUILD_ROOT%{_bindir}
cp -p picosat $RPM_BUILD_ROOT%{_bindir}

# Install the man page
mkdir -p $RPM_BUILD_ROOT%{_mandir}/man1
cp -p %{SOURCE1} $RPM_BUILD_ROOT%{_mandir}/man1

%post libs -p /sbin/ldconfig

%postun libs -p /sbin/ldconfig

%clean
rm -rf $RPM_BUILD_ROOT

# The LICENSE file is placed in the -libs package rather than the base package,
# because the -libs package is always installed when the base package is
# installed, but not vice versa.
%files
%defattr(-,root,root,-)
%{_bindir}/picosat
%{_mandir}/man1/picosat.1*

%files libs
%defattr(-,root,root,-)
%doc LICENSE NEWS
%{_libdir}/libpicosat.so.*

%files devel
%defattr(-,root,root,-)
%{_includedir}/picosat.h
%{_libdir}/libpicosat.so

%changelog
* Tue Jan 19 2010 Jerry James <loganjerry@gmail.com> - 913-2
- Spec file cleanups from review
- Man page courtesy of David Wheeler

* Wed Sep  2 2009 Jerry James <loganjerry@gmail.com> - 913-1
- Initial RPM