%global myname minisat

Name:           minisat2
Version:        2.2.0
Release:        1%{?dist}
Summary:        Minimalistic SAT solver

License:        MIT
Group:          Applications/Engineering
URL:            http://minisat.se/
Source0:        https://github.com/niklasso/minisat/tarball/releases/2.2.0/niklasso-minisat-releases-%{version}-0-geb01ad6.tar.gz
# Sent sources, test, patches (below) to upstream via email on 2008-07-08:
Source1:        http://www.dwheeler.com/essays/minisat-user-guide-1.0.html
Source2:        minisat2-test.in
# Don't try to set the FPU to double precision unless the target CPU supports
# that operation
Patch0:         minisat2-FPU.patch

BuildRequires:  zlib-devel

%description
MiniSat is a minimalistic, open-source Boolean satisfiability problem
(SAT) solver, developed to help researchers and developers alike to get
started on SAT.  Together with SatELite, MiniSat was recently awarded in
the three industrial categories and one of the "crafted" categories of
the SAT 2005 competition.

A SAT solver can determine if it is possible to find assignments to
boolean variables that would make a given expression true, if the
expression is written with only AND, OR, NOT, parentheses, and boolean
variables.  If the expression is satisfiable, MiniSAT can also produce a
set of assignments that make the expression true.  Although the problem
is NP-complete, SAT solvers (like this one) are often able to decide
this problem in a reasonable time frame.

%prep
%setup -q -n niklasso-minisat-eb01ad6
%patch0

cp -p %{SOURCE1} minisat-user-guide.html
cp -p %{SOURCE2} .

# Show key execution steps, so we can see that the right flags are used.
sed -i 's/@$(CXX)/$(CXX)/' mtl/template.mk

%build
# Build "simp", which adds simplification capabilities, instead of just "core"
make %{?_smp_mflags} -C simp r \
  MROOT=`pwd` \
  COPTIMIZE="$RPM_OPT_FLAGS -ffloat-store" \
  LFLAGS="$RPM_OPT_FLAGS -ffloat-store -lz"
cp -p simp/%{myname}_release %{myname}

%install
mkdir -p $RPM_BUILD_ROOT%{_bindir}
install -m 0755 %{myname} $RPM_BUILD_ROOT%{_bindir}

%check
# Test "minisat2-test.in" is a brief quote from
# http://www.satcompetition.org/2004/format-solvers2004.html
# Exit value is 10 for satisfiable, 20 for unsatisfiable
./minisat minisat2-test.in minisat2-test.out || true
echo
echo "RESULTS:"
cat minisat2-test.out
result=`head -1 minisat2-test.out`
if [ "$result" = "SAT" ]; then
  echo "SUCCESS - Correctly found that it was satisfiable"
  true
else
  echo "Failed test."
  false
fi

%files
%doc LICENSE
%doc doc/ReleaseNotes-2.2.0.txt
%doc minisat-user-guide.html
%doc minisat2-test.in
%doc minisat2-test.out
%attr(755,root,root) %{_bindir}/%{myname}

%changelog
* Wed Jun 22 2011 Jerry James <loganjerry@gmail.com> - 2.2.0-1
- New upstream version
- Drop upstreamed template patch
- Drop unnecessary spec file elements (BuildRoot, etc.)

* Tue Feb 08 2011 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.0-10.20070721
- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild

* Sat Jul 25 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.0-9.20070721
- Rebuilt for https://fedoraproject.org/wiki/Fedora_12_Mass_Rebuild

* Wed Feb 25 2009 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.0-8.20070721
- Rebuilt for https://fedoraproject.org/wiki/Fedora_11_Mass_Rebuild

* Tue Aug 7 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-7.20070721
- Removed code for switching between -O2 and -O3, per reviewer request.

* Tue Aug 7 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-6.20070721
- Timing tests found -O3 was unhelpful; switched back to -O2, but left stub
  in case a switch to another -O level would help in the future.
  -O3 real 0m35.714s, 0m35.714s, 0m35.834s vs. -O2 real 0m35.296s, 0m35.301s

* Tue Jul 8 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-5.20070721
- Moved to higher optimization level (-O3); speed is critical for this app.

* Tue Jul 8 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-4.20070721
- Different version number convention to better conform to Fedora guidelines
- Made macro use consistent (not used for simple commands)
- Documented when patches and documentation sent upstream

* Sat Jun 28 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-3.20070721
- Use "make r" instead of "make" to create "released" version
- Wrote brief user guide, included as part of this package.

* Fri Jun 27 2008 David A. Wheeler <dwheeler at, dwheeler.com> 2.0-2.20070721
- Switched from minimal "core" to more-capable "simp" (simplifier)
- Change "make" invocation so CFLAGS includes %%{optflags}
- Add test file and %%check section (so we'd know if it worked!)
- Modified description for people who don't know what SAT solvers are.

* Thu Jun 26 2008 Earl Sammons <esammons at, hush.com> 2.0-1.20070721
- Initial build
- Include Debian patches minisat2-FPU.patch and minisat2-template.patch