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