cvc3.spec

   1 Summary:        Validity checker of many-sorted first-order formulas with theories
   2 Name:           cvc3
   3 Version:        2.4.1
   4 Release:        1
   5 License:        BSD and MIT
   6 Group:          Applications/Engineering
   7 URL:            http://www.cs.nyu.edu/acsys/cvc3/
   8 Source0:        http://www.cs.nyu.edu/acsys/cvc3/download/%{version}/%{name}-%{version}.tar.gz
   9 # Source0-md5:  9b082b0e8c80e1459e9653de044e0d6e
  10 Patch0:         %{name}-doxygen.patch
  11 BuildRequires:  bison
  12 BuildRequires:  doxygen
  13 BuildRequires:  flex
  14 BuildRequires:  gmp-devel
  15 BuildRequires:  jdk
  16 BuildRequires:  jpackage-utils
  17 BuildRequires:  perl
  18 BuildRequires:  python
  19 BuildRequires:  texlive-latex
  20 BuildRequires:  time
  21 BuildRequires:  transfig
  22 BuildRoot:      %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
  23
  24 %description
  25 CVC3 is an automatic theorem prover for Satisfiability Modulo Theories
  26 (SMT) problems. It can be used to prove the validity (or, dually, the
  27 satisfiability) of first-order formulas in a large number of built-in
  28 logical theories and their combination.
  29
  30 CVC3 is the latest offspring of a series of popular SMT provers, which
  31 originated at Stanford University with the SVC system. In particular,
  32 it builds on the code base of CVC Lite, its most recent predecessor.
  33 Its high level design follows that of the Sammy prover.
  34
  35 CVC3 works with a version of first-order logic with polymorphic types
  36 and has a wide variety of features including:
  37
  38  - several built-in base theories: rational and integer linear
  39    arithmetic, arrays, tuples, records, inductive data types, bit
  40    vectors, and equality over uninterpreted function symbols;
  41  - support for quantifiers;
  42  - an interactive text-based interface;
  43  - a rich C and C++ API for embedding in other systems;
  44  - proof and model generation abilities;
  45  - predicate subtyping;
  46  - essentially no limit on its use for research or commercial purposes
  47    (see license).
  48
  49 For example, if you run 'cvc3 +interactive' and submit: i, j: INT;
  50 ASSERT i = j + 1; QUERY i>j; it will determine "Valid." If you then
  51 ask: QUERY i<j; COUNTERMODEL; it will determine "Invalid." and show an
  52 example demonstrating when the formula is not true (e.g., i = 0 and j
  53 = -1).
  54
  55 %package devel
  56 Summary:        Header files for development with CVC3
  57 Group:          Development/Libraries
  58 Requires:       %{name} = %{version}-%{release}
  59
  60 %description devel
  61 Header files need to develop with CVC3.
  62
  63 %package doc
  64 Summary:        API documentation for CVC3
  65 Group:          Documentation
  66 Requires:       %{name} = %{version}-%{release}
  67 BuildArch:      noarch
  68
  69 %description doc
  70 API documentation for CVC3.
  71
  72 %package java
  73 Summary:        Java interface for CVC3
  74 Group:          Development/Languages/Java
  75 Requires:       %{name} = %{version}-%{release}
  76 Requires:       java
  77 Requires:       jpackage-utils
  78
  79 %description java
  80 Java interface for CVC3.
  81
  82 %prep
  83 %setup -q
  84 %patch0
  85
  86 # Use the appropriate compiler flags
  87 sed -e "s|^  LOCAL_CXXFLAGS = -O2|  LOCAL_CXXFLAGS =|" \
  88     -e "s|^LOCAL_CXXFLAGS += -Wall|LOCAL_CXXFLAGS +=|" \
  89     -i Makefile.std
  90
  91 # We can't use loadLibrary, since the JNI libaries are not in a standard place
  92 sed -i \
  93  "s|loadLibrary(\"cvc3jni\")|load(\"%{_libdir}/%{name}/libcvc3jni.so\")|" \
  94  java/src/cvc3/Embedded.java
  95
  96 # Get rid of an unused direct shared library dependency
  97 sed -i "s|-lcvc3 \$(LD_LIBS)|-Wl,--as-needed -lcvc3 \$(LD_LIBS)|" java/Makefile
  98
  99 %build
 100 %configure \
 101         --with-build=optimized \
 102         --enable-dynamic \
 103         --enable-java \
 104         --disable-zchaff \
 105         --with-java-home=%{java_home}
 106
 107 %{__make}
 108
 109 # Build the documentation
 110 %{__make} -C doc
 111 rm -f doc/html/*.{map,md5}
 112
 113 %install
 114 rm -rf $RPM_BUILD_ROOT
 115 install -d $RPM_BUILD_ROOT%{_libdir}/%{name}
 116
 117 %{__make} install \
 118         datarootdir=$RPM_BUILD_ROOT%{_datadir} \
 119         prefix=$RPM_BUILD_ROOT%{_prefix} \
 120         exec_prefix=$RPM_BUILD_ROOT%{_prefix} \
 121         libdir=$RPM_BUILD_ROOT%{_libdir} \
 122         bindir=$RPM_BUILD_ROOT%{_bindir} \
 123         mandir=$RPM_BUILD_ROOT%{_mandir} \
 124         incdir=$RPM_BUILD_ROOT%{_includedir}/%{name} \
 125         javadir=$RPM_BUILD_ROOT%{_libdir}/%{name}
 126
 127 # Add missing executable bits to the shared libraries
 128 chmod a+x $RPM_BUILD_ROOT%{_libdir}/*.so.*
 129
 130 # Move the JNI libraries to the right place
 131 %{__mv} $RPM_BUILD_ROOT%{_libdir}/libcvc3jni.* $RPM_BUILD_ROOT%{_libdir}/%{name}
 132
 133 %clean
 134 rm -rf $RPM_BUILD_ROOT
 135
 136 %post -p /sbin/ldconfig
 137 %postun -p /sbin/ldconfig
 138
 139 %files
 140 %defattr(644,root,root,755)
 141 %doc INSTALL LICENSE PEOPLE README
 142 %attr(755,root,root) %{_bindir}/cvc3
 143 %{_libdir}/libcvc3.so.*
 144
 145 %files devel
 146 %defattr(644,root,root,755)
 147 %{_includedir}/cvc3
 148 %{_libdir}/*.so
 149 %{_pkgconfigdir}/%{name}.pc
 150
 151 %files doc
 152 %defattr(644,root,root,755)
 153 %doc doc/html
 154
 155 %files java
 156 %defattr(644,root,root,755)
 157 %{_libdir}/%{name}