Name:           cvc3

Version:        2.4.1

Release:        6%{?dist}

Summary:        Validity checker of many-sorted first-order formulas with theories

Group:          Applications/Engineering

License:        BSD and MIT

URL:            http://www.cs.nyu.edu/acsys/cvc3/

Source:         http://www.cs.nyu.edu/acsys/cvc3/download/%{version}/%{name}-%{version}.tar.gz

# This patch is Fedora-specific.  Set up doxygen so that the generated

# documentation meets packaging standards.

Patch0:         %{name}-doc.patch

# This patch was sent upstream 6 Sep 2011.  It fixes some broken doxygen

# comments.

Patch1:         %{name}-doxygen.patch

# Not sent upstream, as cvc3 has reached end of life.  Add support for aarch64.

Patch2:         %{name}-aarch64.patch

BuildRequires:  bison

BuildRequires:  doxygen

BuildRequires:  emacs

BuildRequires:  flex

BuildRequires:  gmp-devel

BuildRequires:  java-devel >= 1:1.6.0

BuildRequires:  jpackage-utils

BuildRequires:  perl

BuildRequires:  python

BuildRequires:  time

BuildRequires:  transfig

BuildRequires:  tex(latex)

BuildRequires:  xemacs

%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

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}%{?_isa} = %{version}-%{release}

%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}%{?_isa} = %{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

%patch1

%patch2

# Use the appropriate compiler flags

sed -e "s|^  LOCAL_CXXFLAGS = -O2|  LOCAL_CXXFLAGS =|" \

    -e "s|^LOCAL_CXXFLAGS += -Wall|LOCAL_CXXFLAGS +=|" \

    -i Makefile.std

# We can't use loadLibrary, since the JNI libaries are not in a standard place

sed -i \

 "s|loadLibrary(\"cvc3jni\")|load(\"%{_libdir}/%{name}/libcvc3jni.so\")|" \

 java/src/cvc3/Embedded.java

# Get rid of an unused direct shared library dependency

sed -i "s|-lcvc3 \$(LD_LIBS)|-Wl,--as-needed -lcvc3 \$(LD_LIBS)|" java/Makefile

%build

%configure --with-build=optimized --enable-dynamic --enable-java \

  --disable-zchaff --with-java-home=%{java_home}

# FIXME: %%{?_smp_mflags} sometimes leads to build failures

make

# Build the documentation

make -C doc

rm -f doc/html/*.{map,md5}

%install

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

# Due to Fedora's policy of changing System.loadLibrary() with a mutable path

# to System.load() with a fixed path, it is not possible to run the Java tests,

# since the JNI shared objects are not in the fixed location until the RPM is

# installed.

sed -i "s/^BUILD_JAVA = 1/BUILD_JAVA = 0/" Makefile.local

LD_LIBRARY_PATH=`pwd`/lib make regress4

%post -p /sbin/ldconfig

%postun -p /sbin/ldconfig

%files

%doc INSTALL LICENSE PEOPLE README

%{_bindir}/cvc3

%{_libdir}/libcvc3.so.*

%files devel

%{_includedir}/cvc3

%{_libdir}/*.so

%{_libdir}/pkgconfig/%{name}.pc

%files doc

%doc doc/html

%files java

%{_libdir}/%{name}

%files emacs

%{_emacs_sitelispdir}/*.elc

%files emacs-el

%{_emacs_sitelispdir}/*.el

%files xemacs

%{_xemacs_sitelispdir}/*.elc

%files xemacs-el

%{_xemacs_sitelispdir}/*.el

%changelog

* Mon Apr 29 2013 Jerry James <loganjerry@gmail.com> - 2.4.1-6

- Add -aarch64 support (bz 925213)

- Turn off parallel builds; they sometimes fail while building the Java code

* Wed Feb 13 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.4.1-5

- Rebuilt for https://fedoraproject.org/wiki/Fedora_19_Mass_Rebuild

* Wed Jul 18 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.4.1-4

- Rebuilt for https://fedoraproject.org/wiki/Fedora_18_Mass_Rebuild

* Tue Feb 28 2012 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.4.1-3

- Rebuilt for c++ ABI breakage

* Fri Jan  6 2012 Jerry James <loganjerry@gmail.com> - 2.4.1-2

- Rebuild for GCC 4.7

* Thu Oct 20 2011 Marcela Mašláňová <mmaslano@redhat.com> - 2.4.1-1.2

- rebuild with new gmp without compat lib

* Mon Oct 10 2011 Peter Schiffer <pschiffe@redhat.com> - 2.4.1-1.1

- rebuild with new gmp

* Tue Sep  6 2011 Jerry James <loganjerry@gmail.com> - 2.4.1-1

- New upstream version

- Drop unnecessary spec file elements (BuildRoot, etc.)

- Don't run the Java tests; they can't find the JNI shared objects

* Tue Feb 08 2011 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.2-3

- Rebuilt for https://fedoraproject.org/wiki/Fedora_15_Mass_Rebuild

* Thu Jun  3 2010 Jerry James <loganjerry@gmail.com> - 2.2-2

- Add python BR (bz 599887)

* Thu Nov 19 2009 Jerry James <loganjerry@gmail.com> - 2.2-1

- Update to 2.2

- Drop upstreamed patches (gcc4 and java)

* 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