Name:           glueminisat
Version:        2.2.5
Release:        3%{?dist}
Summary:        Boolean SAT solver that implements literal blocks distance (LBD)

License:        MIT
Group:          Applications/Engineering
URL:            http://glueminisat.nabelab.org/
# Fetching the URL below with recent releases of Chromium and Firefox works
# fine. However, fetching it with Wget currently fails for me (with the
# message: "File name too long"). Including the -O option with the explicit
# filename for the tar ball seems to work around that issue. The URL provided
# by the GlueMiniSat download page has some additional HTTP GET parameters
# appended to it;  "?attredirects=0&d=1" (without the quotes). RPM doesn't
# seem to like them, so they are omitted from the URL tag value here.
Source0:        https://sites.google.com/a/nabelab.org/glueminisat/home/download/%{name}-%{version}.tar.gz
# Simple test case input (from the 2004 International SAT Competition)
Source1:        %{name}-test.in
# Short HTML document that provides links to various online help resources
Source2:        %{name}-intro.html
# Don't try to set the FPU to double precision unless target CPU supports it
Patch0:         %{name}-FPU.patch
# Cosmetic patch to keep progress messages under 80 characters (avoids wrap)
Patch1:         %{name}-printf.patch
# Copies of both patches above sent to Hidetomo Nabeshima on Mon Apr 23, 2012
BuildRequires:  zlib-devel

%description
GlueMiniSat is a boolean, propositional satisfiability (SAT) problem
solver. It is a derivative work of the open source MiniSat 2.2 solver,
and implements a form of the literal blocks distance (LBD) evaluation
criteria to predict the quality of clauses learned when conflicts are
encountered in the search process.

The underlying concepts of literal blocks distance were first introduced
in the paper "Predicting learnt clauses quality in modern SAT solvers"
by Gilles Audemard and Laurent Simon, Proceedings of IJCAI-2009, pages
399-404, 2009. The authors' implementation of LBD, the Glucose 1.0 SAT
solver, performed admirably by placing 2-nd at the International 2009
SAT competition in the Applications (UNSAT) category.

GlueMiniSat uses a slightly restricted concept of LBD, called strict
LBD, and a dynamic restart strategy based on local averages of the
decision levels and the LBDs of learned clauses. Experimental results
show that GlueMiniSat also performs very well on SAT instances that
are unsatisfiable.  GlueMiniSat earned 1-st place at the International
2011 SAT competition in the Applications (UNSAT) category, solving 126
of 142 problem instances.

GlueMiniSat supports the same command line options as MiniSat 2.2 (see the
documentation from the minisat2 package). It can also run as a "clone"
of the MiniSat 2.2 or Glucose 1.0 SAT solvers by specifying the command
line options -minisat or -glucose, respectively.

%prep
%setup -q
%patch0 -p1 -b .orig
%patch1 -p1 -b .orig
cp -p %{SOURCE1} .
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"
# The target "r" signifies that we are building the "released" version
make %{?_smp_mflags} -C simp r \
  MROOT=`pwd` \
  COPTIMIZE="${RPM_OPT_FLAGS} -ffloat-store" \
  LFLAGS="${RPM_OPT_FLAGS} -ffloat-store -lz"
cp -p simp/%{name}_release %{name}

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

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

%files
%doc LICENSE README README.minisat
%doc %{name}-intro.html %{name}-test.in %{name}-test.out
%attr(755,root,root) %{_bindir}/%{name}

%changelog
* Wed Apr 25 2012 John C. Peterson <jcp@eskimo.com> - 2.2.5-3
- Wrote an HTML "intro" document with links to David Wheeler's MiniSat tutorial
- Fixed minor typo error in the comments about the URL tag value
- Added some additional information to the package description

* Tue Apr 24 2012 John C. Peterson <jcp@eskimo.com> - 2.2.5-2
- Replaced the usage of redundant global "myname" with standard macro "name"
- Replaced the occurrences of glueminisat with "name" macro in source, patches
- Sent the patches to upstream (Hidetomo Nabeshima, the primary author)
- Addition to glueminisat-printf.patch (based on feedback from author)

* Sat Apr 14 2012 John C. Peterson <jcp@eskimo.com> - 2.2.5-1
- Note that GlueMiniSat is a derivative work of the MiniSat 2.2 SAT solver
- Initial RPM spec file is based on the one from the Fedora minisat2 package
- Cosmetic patch to keep progress messages under 80 characters (avoids wrap)
- Adapted the FPU patch from the Fedora minisat2 package