1 Summary: Validity checker of many-sorted first-order formulas with theories
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
12 BuildRequires: doxygen
14 BuildRequires: gmp-devel
16 BuildRequires: jpackage-utils
19 BuildRequires: texlive-latex
21 BuildRequires: transfig
22 BuildRoot: %{tmpdir}/%{name}-%{version}-root-%(id -u -n)
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.
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.
35 CVC3 works with a version of first-order logic with polymorphic types
36 and has a wide variety of features including:
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
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
56 Summary: Header files for development with CVC3
57 Group: Development/Libraries
58 Requires: %{name} = %{version}-%{release}
61 Header files need to develop with CVC3.
64 Summary: API documentation for CVC3
66 Requires: %{name} = %{version}-%{release}
70 API documentation for CVC3.
73 Summary: Java interface for CVC3
74 Group: Development/Languages/Java
75 Requires: %{name} = %{version}-%{release}
77 Requires: jpackage-utils
80 Java interface for CVC3.
86 # Use the appropriate compiler flags
87 sed -e "s|^ LOCAL_CXXFLAGS = -O2| LOCAL_CXXFLAGS =|" \
88 -e "s|^LOCAL_CXXFLAGS += -Wall|LOCAL_CXXFLAGS +=|" \
91 # We can't use loadLibrary, since the JNI libaries are not in a standard place
93 "s|loadLibrary(\"cvc3jni\")|load(\"%{_libdir}/%{name}/libcvc3jni.so\")|" \
94 java/src/cvc3/Embedded.java
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
101 --with-build=optimized \
105 --with-java-home=%{java_home}
109 # Build the documentation
111 rm -f doc/html/*.{map,md5}
114 rm -rf $RPM_BUILD_ROOT
115 install -d $RPM_BUILD_ROOT%{_libdir}/%{name}
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}
127 # Add missing executable bits to the shared libraries
128 chmod a+x $RPM_BUILD_ROOT%{_libdir}/*.so.*
130 # Move the JNI libraries to the right place
131 %{__mv} $RPM_BUILD_ROOT%{_libdir}/libcvc3jni.* $RPM_BUILD_ROOT%{_libdir}/%{name}
134 rm -rf $RPM_BUILD_ROOT
136 %post -p /sbin/ldconfig
137 %postun -p /sbin/ldconfig
140 %defattr(644,root,root,755)
141 %doc INSTALL LICENSE PEOPLE README
142 %attr(755,root,root) %{_bindir}/cvc3
143 %{_libdir}/libcvc3.so.*
146 %defattr(644,root,root,755)
149 %{_pkgconfigdir}/%{name}.pc
152 %defattr(644,root,root,755)
156 %defattr(644,root,root,755)