Name: cvc3
Version: 2.4.1
Release: 14%{?dist}
Summary: Validity checker of many-sorted first-order formulas with theories
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<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
Summary: Header files for development with CVC3
Requires: %{name}%{?_isa} = %{version}-%{release}
%description devel
Header files need to develop with CVC3.
%package doc
Summary: API documentation for CVC3
Requires: %{name} = %{version}-%{release}
BuildArch: noarch
Provides: bundled(jquery)
%description doc
API documentation for CVC3.
%package java
Summary: Java interface for CVC3
Requires: %{name}%{?_isa} = %{version}-%{release}
Requires: java-headless
Requires: jpackage-utils
%description java
Java interface for CVC3.
%package emacs
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
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
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
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 PEOPLE README
%license LICENSE
%{_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
* Wed Feb 03 2016 Fedora Release Engineering <releng@fedoraproject.org> - 2.4.1-14
- Rebuilt for https://fedoraproject.org/wiki/Fedora_24_Mass_Rebuild
* Wed Jun 17 2015 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.4.1-13
- Rebuilt for https://fedoraproject.org/wiki/Fedora_23_Mass_Rebuild
* Sat May 02 2015 Kalev Lember <kalevlember@gmail.com> - 2.4.1-12
- Rebuilt for GCC 5 C++11 ABI change
* Thu Feb 12 2015 Jerry James <loganjerry@gmail.com> - 2.4.1-11
- Use license macro
- Note bundled jquery
* Sat Aug 16 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.4.1-10
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_22_Mass_Rebuild
* Sat Jun 07 2014 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.4.1-9
- Rebuilt for https://fedoraproject.org/wiki/Fedora_21_Mass_Rebuild
* Mon Feb 24 2014 Jerry James <loganjerry@gmail.com> - 2.4.1-8
- Make the -java subpackage R java-headless instead of java (bz 1068020)
* Sat Aug 03 2013 Fedora Release Engineering <rel-eng@lists.fedoraproject.org> - 2.4.1-7
- Rebuilt for https://fedoraproject.org/wiki/Fedora_20_Mass_Rebuild
* 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