Name:           csisat
Version:        1.2
Release:        10%{?dist}
Summary:        Tool for LA+EUF Interpolation

Group:          Applications/Engineering
License:        ASL 2.0
URL:            http://csisat.googlecode.com/
Source0:        http://csisat.googlecode.com/files/%{name}-%{version}.zip
# This patch has not been sent upstream.  Upstream wishes to distribute the
# picosat sources with their code.  This patch builds with the system picosat
# instead, and also adds missing dependencies so that parallel make works.
Patch0:         csisat-makefile.patch

BuildRequires:  glpk-devel, ocaml, picosat-devel, subversion

ExclusiveArch:  %{ocaml_arches}

%description
CSIsat reads a set of mathematical formulas that may combine variables,
addition, multiplication, comparisons (<,>, etc.), as well as boolean
expressions (and, or, not).  It determines if it is possible to set the
variables to values so that the set of formulas are all simultaneously true
(if it can, then the set of formulas is "satisfiable").

More technically, CSIsat is an interpolating decision procedure for the
quantifier-free theory of rational linear arithmetic (LA) and equality with
uninterpreted function (EUF) symbols.  This implementation combines the
efficiency of linear programming for solving the arithmetic part with the
efficiency of a SAT solver to reason about the boolean structure.

%prep
%setup -q
%patch0

# Make sure we don't use the bundled version of picosat
rm -fr picosat-*

# Get rid of inappropriate executable bits
chmod a-x *.txt
find . -name \*.c | xargs chmod a-x

%build
# FIXME: Parallel make sometimes fails
make CFLAGS="$RPM_OPT_FLAGS -I%{_libdir}/ocaml -I%{_includedir}/glpk"

%install
mkdir -p $RPM_BUILD_ROOT%{_bindir}
cp -p bin/* $RPM_BUILD_ROOT%{_bindir}

%files
%doc License.txt License_Apache-2.0.txt ReadMe.txt ToDo.txt server/README
%{_bindir}/csisat
%{_bindir}/csisatServer

%changelog
* Thu Dec 13 2012 Jerry James <loganjerry@gmail.com> - 1.2-10
- Rebuild for OCaml 4.00.1

* Mon Aug 20 2012 Jerry James <loganjerry@gmail.com> - 1.2-9
- Rebuild for new picosat

* Wed Jul 18 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.2-8
- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild

* Fri Jan  6 2012 Jerry James <loganjerry@gmail.com> - 1.2-7
- Rebuild for GCC 4.7 and Ocaml 3.12.1

* Mon Nov 14 2011 Jerry James <loganjerry@gmail.com> - 1.2-6
- Change supported arches list to %%{ocaml_arches}
- Drop unnecessary spec file elements (%%clean, etc.)

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

* Mon Jan 31 2011 Jerry James <loganjerry@gmail.com> - 1.2-4
- Don't use the OCaml dependency generators, which find no dependencies
- Update list of supported arches from the ocaml spec file

* Thu Jan 27 2011 Jerry James <loganjerry@gmail.com> - 1.2-3
- Rebuild for new picosat and new ocaml
- BR subversion to eliminate build noise from svnversion failing
- Parallel make still isn't fixed; disable until I can figure it out

* Tue Jan 19 2010 Jerry James <loganjerry@gmail.com> - 1.2-2
- Fix parallel make
- Less opaque description

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