Name:           csisat
Version:        1.2
Release:        5%{?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/csisat-%{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

# This list should match the one in the ocaml spec file
ExclusiveArch:  alpha armv4l %{ix86} ia64 x86_64 ppc sparc sparcv9 ppc64

%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
rm -rf $RPM_BUILD_ROOT
mkdir -p $RPM_BUILD_ROOT%{_bindir}
cp -p bin/* $RPM_BUILD_ROOT%{_bindir}

%clean
rm -rf $RPM_BUILD_ROOT

%files
%defattr(-,root,root,-)
%doc License.txt License_Apache-2.0.txt ReadMe.txt ToDo.txt server/README
%{_bindir}/csisat
%{_bindir}/csisatServer

%changelog
* 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