# If the xemacs-devel package has installed a pkgconfig file, use that to
# determine version at build time, otherwise set a default.
%if %($(pkg-config xemacs) ; echo $?)
%define xemacs_version 21.5
%else
%define xemacs_version %(pkg-config xemacs --modversion)
%endif

Name:           cvc3
Version:        2.1
Release:        3%{?dist}
Summary:        Validity checker of many-sorted first-order formulas with theories

Group:          Applications/Engineering
License:        BSD
URL:            http://www.cs.nyu.edu/acsys/cvc3/
Source:         http://www.cs.nyu.edu/acsys/cvc3/download/%{version}/cvc3-%{version}.tar.gz
# Override compiler flag selection so that $RPM_OPT_FLAGS will take effect.
# Submitted upstream June 2008.
Patch0:         cvc3-build.patch
# Fix a few problems in the doxygen documentation.
# Submitted upstream June 2008, with an update in August 2008.
Patch1:         cvc3-doc.patch
# GCC 4.3+ uses a streamlined header architecture, so more includes are needed.
# This patch was last submitted upstream on 16 Oct 2009.
Patch2:         cvc3-gcc4.patch
BuildRoot:      %{_tmppath}/%{name}-%{version}-%{release}-root-%(%{__id_u} -n)
# Fix Java build problems.  This patch was last sent upstream on 19 Oct 2009.
Patch3:         cvc3-java.patch

BuildRequires:  bison, doxygen, emacs, emacs-el, flex, gnu-free-sans-fonts
BuildRequires:  gmp-devel, java-devel, jpackage-utils, perl, time
BuildRequires:  transfig, tex(latex), xemacs, xemacs-devel
Requires:       gnu-free-sans-fonts

%description
CVC3 is an automatic theorem prover for Satisfiability Modulo Theories (SMT)
problems.  It can be used to prove the validity (or, dually, the
satisfiability) of first-order formulas in a large number of built-in logical
theories and their combination.

CVC3 is the latest offspring of a series of popular SMT provers, which
originated at Stanford University with the SVC system.  In particular, it
builds on the code base of CVC Lite, its most recent predecessor.  Its high
level design follows that of the Sammy prover.

CVC3 works with a version of first-order logic with polymorphic types and has
a wide variety of features including:

 * several built-in base theories: rational and integer linear arithmetic,
   arrays, tuples, records, inductive data types, bit vectors, and equality
   over uninterpreted function symbols;
 * support for quantifiers;
 * an interactive text-based interface;
 * a rich C and C++ API for embedding in other systems;
 * proof and model generation abilities;
 * predicate subtyping;
 * essentially no limit on its use for research or commercial purposes (see
   license).

For example, if you run 'cvc3 +interactive' and submit:
  i, j: INT; ASSERT i = j + 1; QUERY i>j;
it will determine "Valid."  If you then ask:
  QUERY i<j; COUNTERMODEL;
it will determine "Invalid." and show an example demonstrating when the formula
is not true (e.g., i = 0 and j = -1).

%package devel
Group:          Development/Libraries
Summary:        Header files for development with CVC3
Requires:       %{name} = %{version}-%{release}
BuildArch:      noarch

%description devel
Header files need to develop with CVC3.

%package doc
Group:          Documentation
Summary:        API documentation for CVC3
Requires:       %{name} = %{version}-%{release}
BuildArch:      noarch

%description doc
API documentation for CVC3.

%package java
Group:          Development/Libraries/Java
Summary:        Java interface for CVC3
Requires:       %{name} = %{version}-%{release}, java, jpackage-utils

%description java
Java interface for CVC3.

%package emacs
Group:          Applications/Engineering
Summary:        Compiled Emacs mode for CVC3
Requires:       emacs(bin) >= %{_emacs_version}
Requires:       %{name} = %{version}-%{release}
BuildArch:      noarch

%description emacs
This package contains the byte compiled CVC3 mode for Emacs.

%package emacs-el
Group:          Applications/Engineering
Summary:        Elisp source files for the CVC3 Emacs mode
Requires:       %{name} = %{version}-%{release}
BuildArch:      noarch

%description emacs-el
This package contains the source Elisp files for the CVC3 mode for Emacs.  You
do not need to install this package to run %{name}.  Install the %{name}-emacs
package to use %{name} with Emacs.

%package xemacs
Group:          Applications/Engineering
Summary:        Compiled XEmacs mode for CVC3
Requires:       xemacs(bin) >= %{xemacs_version}
Requires:       %{name} = %{version}-%{release}
BuildArch:      noarch

%description xemacs
This package contains the byte compiled CVC3 mode for XEmacs.

%package xemacs-el
Group:          Applications/Engineering
Summary:        Elisp source files for the CVC3 XEmacs mode
Requires:       %{name} = %{version}-%{release}
BuildArch:      noarch

%description xemacs-el
This package contains the source Elisp files for the CVC3 mode for XEmacs.  You
do not need to install this package to run %{name}.  Install the %{name}-xemacs
package to use %{name} with XEmacs.

%prep
%setup -q
%patch0 -p1
%patch1 -p1
%patch2 -p1
%patch3 -p1

# We can't use loadLibrary, since the JNI libaries are not in a standard place
sed -i \
 -e "s|loadLibrary(\"cvc3jni\")|load(\"%{_libdir}/%{name}/libcvc3jni.so\")|" \
 java/src/cvc3/Embedded.java

%build
%configure --with-build=optimized --enable-dynamic --enable-java \
  --with-java-home=/usr/lib/jvm/java
make %{?_smp_mflags}

# Build the documentation
cd doc
make
rm -f html/*.{map,md5}

%install
rm -rf %{buildroot}

mkdir -p %{buildroot}%{_libdir}/%{name}
%makeinstall javadir=%{buildroot}%{_libdir}/%{name}

# Byte compile the CVC3 mode file for Emacs
mkdir -p %{buildroot}%{_emacs_sitelispdir}
cp -p emacs/cvc-mode.el %{buildroot}%{_emacs_sitelispdir}
pushd %{buildroot}%{_emacs_sitelispdir}
%{_emacs_bytecompile} cvc-mode.el
popd

# Byte compile the CVC3 mode file for XEmacs
mkdir -p %{buildroot}%{_xemacs_sitelispdir}
cp -p emacs/cvc-mode.el %{buildroot}%{_xemacs_sitelispdir}
pushd %{buildroot}%{_xemacs_sitelispdir}
%{_xemacs_bytecompile} cvc-mode.el
popd

# Add missing executable bits to the shared libraries
chmod a+x %{buildroot}%{_libdir}/*.so.*

# Move the JNI libraries to the right place
mv %{buildroot}%{_libdir}/libcvc3jni.* %{buildroot}%{_libdir}/%{name}

%check
LD_LIBRARY_PATH=`pwd`/lib make regressonly4

%post -p /sbin/ldconfig

%postun -p /sbin/ldconfig

%clean
rm -rf %{buildroot}

%files
%defattr(-,root,root,-)
%doc INSTALL LICENSE PEOPLE README VERSION
%{_bindir}/cvc3
%{_libdir}/libcvc3.so.*

%files devel
%defattr(-,root,root,-)
%{_includedir}/cvc3
%{_libdir}/*.so

%files doc
%defattr(-,root,root,-)
%doc doc/html

%files java
%defattr(-,root,root,-)
%{_libdir}/%{name}

%files emacs
%defattr(-,root,root,-)
%{_emacs_sitelispdir}/*.elc

%files emacs-el
%defattr(-,root,root,-)
%{_emacs_sitelispdir}/*.el

%files xemacs
%defattr(-,root,root,-)
%{_xemacs_sitelispdir}/*.elc

%files xemacs-el
%defattr(-,root,root,-)
%{_xemacs_sitelispdir}/*.el

%changelog
* Tue Oct 27 2009 Jerry James <loganjerry@gmail.com> - 2.1-3
- Drop the graphviz BR to block generation of huge class graphs
- Use the new (X)Emacs RPM macros to simplify the spec file

* Mon Oct 19 2009 Jerry James <loganjerry@gmail.com> - 2.1-2
- Fix problems found on review
- Enable the Java interface

* Thu Oct 15 2009 Jerry James <loganjerry@gmail.com> - 2.1-1
- Initial RPM