Name:           csisat
Version:        1.2
Release:        16%{?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:         %{name}-makefile.patch
# Adapt to new glpk API
Patch1:         %{name}-glpk.patch
# Adapt to new picosat API
Patch2:         %{name}-picosat.patch

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

%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
%patch1
%patch2

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

# We need the picosat version with trace enabled
sed -i 's/lpicosat/lpicosat-trace/' \
    Makefile pico_ml_wrapper/Makefile pico_ml_wrapper/compile.sh

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

# Silence warnings
svn upgrade

%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 ReadMe.txt ToDo.txt server/README
%license License.txt License_Apache-2.0.txt
%{_bindir}/csisat
%{_bindir}/csisatServer

%changelog
* Fri Nov  7 2014 Jerry James <loganjerry@gmail.com> - 1.2-16
- Rebuild for picosat 960
- Fix license handling

* Sat Aug 16 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.2-15
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild

* Sat Jun 07 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 1.2-14
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild

* Fri Apr 18 2014 Jerry James <loganjerry@gmail.com> - 1.2-13
- Remove ocaml_arches macro (bz 1087794)

* Wed Jul 31 2013 Jerry James <loganjerry@gmail.com> - 1.2-12
- Rebuild for new glpk and new picosat

* Sat Feb  2 2013 Jerry James <loganjerry@gmail.com> - 1.2-11
- Rebuild for new glpk

* 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