Examples/tutorials are not installed with "make install." See below.
+For more information about the build system itself (probably not
+necessary for casual users), see the Appendix at the bottom of this
+file.
+
*** Build dependences
The following tools and libraries are required to run CVC4. Versions
None of these is required, but can improve CVC4 as described below:
+ Optional: SWIG 2.0.x (Simplified Wrapper and Interface Generator)
Optional: CLN v1.3 or newer (Class Library for Numbers)
Optional: CUDD v2.4.2 or newer (Colorado University Decision Diagram package)
Optional: GNU Readline library (for an improved interactive experience)
Optional: The Boost C++ threading library (libboost_thread)
+ Optional: CxxTest unit testing framework
+
+SWIG is necessary to build the Java API (and of course a JDK is
+necessary, too). SWIG 1.x won't work; you'll need 2.0, and the more
+recent the better. On Mac, we've seen SWIG segfault when generating
+CVC4 language bindings; version 2.0.8 or higher is recommended to
+avoid this. See "Language bindings" below for build instructions.
CLN is an alternative multiprecision arithmetic package that can offer
better performance and memory footprint than GMP. CLN is covered by
(multithreaded) mode. Check your distribution for a package named
"libboost-thread-dev" or similar.
+CxxTest is necessary to run CVC4's unit tests (included with the
+distribution). Running these is not really required for users of
+CVC4; "make check" will skip unit tests if CxxTest isn't available,
+and go on to run the extensive system- and regresion-tests in the
+source tree. However, if you're interested, you can download CxxTest
+at http://cxxtest.com/ .
+
*** Building with CUDD (optional)
CUDD, if desired, must be installed delicately. The CVC4 configure
The Debian source package "cudd", available from the same repository,
includes a diff of all changes made to cudd makefiles.
+*** Language bindings
+
+There are several options available for using CVC4 from the API.
+
+First, CVC4 offers a complete and flexible API for manipulating
+expressions, maintaining a stack of assertions, and checking
+satisfiability, and related things. The C++ libraries (libcvc4.so and
+libcvc4parser.so) and required headers are installed normally via a
+"make install". This API is also available from Java (via CVC4.jar
+and libcvc4jni.so) by configuring with --enable-language-bindings=java.
+You'll also need SWIG 2.0 installed (and you might need to help
+configure find it if you installed it in a nonstandard place with
+--with-swig-dir=/path/to/swig/installation). You may also need to
+give the configure script the path to your Java headers (in
+particular, jni.h). You might do so with (for example):
+
+ ./configure --enable-language-bindings=java \
+ JAVA_CPPFLAGS=-I/usr/lib/jvm/java-6-openjdk-amd64/include
+
+There is also a "C++ compatibility API" (#include <cvc4/cvc3_compat.h>
+and link against libcvc4compat.so) that attempts to maintain
+source-level backwards-compatibility with the CVC3 C++ API. The
+compatibility library is built by default, and
+--enable-language-bindings=java enables the Java compatibility library
+(CVC4compat.jar and libcvc4compatjni.so).
+--enable-language-bindings=c enables the C compatibility library
+(#include <cvc4/bindings/compat/c/c_interface.h> and link against
+libcvc4bindings_c_compat.so), and if you want both C and Java
+bindings, use --enable-language-bindings=c,java. These compatibility
+language bindings do NOT require SWIG.
+
+The examples/ directory includes some basic examples (the "simple vc"
+and "simple vc compat" family of examples) of all these interfaces.
+
+In principle, since we use SWIG to generate the native Java API, we
+could support other languages as well. However, using CVC4 from other
+languages is not supported, nor expected to work, at this time. If
+you're interested in helping to develop, maintain, and test a language
+binding, please contact us via the users' mailing list at
+cvc-users@cs.nyu.edu.
+
*** Building CVC4 from a repository checkout
The following tools and libraries are additionally required to build
Examples are not built by "make" or "make install". See
examples/README for information on what to find in the examples/
directory, as well as information about building and installing them.
+
+*** Appendix: Build architecture
+
+The build system is generated by automake, libtool, and autoconf. It
+is somewhat nonstandard, though, which (for one thing) requires that
+GNU Make be used. If you ./configure in the top-level source
+directory, the objects will actually all appear in
+builds/${arch}/${build_id}. This is to allow multiple, separate
+builds in the same place (e.g., an assertions-enabled debugging build
+alongside a production build), without changing directories at the
+shell. The "current" build is maintained, and you can still use
+(e.g.) "make -C src/main" to rebuild objects in just one subdirectory.
+
+You can also create your own build directory inside or outside of the
+source tree and configure from there. All objects will then be built
+in that directory, and you'll ultimately find the "cvc4" binary in
+src/main/, and the libraries under src/ and src/parser/.
[cvc4_check_for_bindings=no; try_bindings=])
CVC4_LANGUAGE_BINDINGS=
if test "$noswig" = yes; then
- AC_MSG_WARN([use of swig disabled by user.])
+ AC_MSG_WARN([use of swig disabled by user, native API bindings disabled.])
SWIG=
- if test "$cvc4_check_for_bindings" = no -a -n "$try_bindings"; then
- AC_MSG_ERROR([language bindings requested by user, but swig disabled.])
- fi
else
if test -z "$SWIG"; then
- AC_CHECK_PROGS(SWIG, [swig swig2.0], swig, [])
+ AC_CHECK_PROGS(SWIG, [swig swig2.0], [], [])
else
AC_CHECK_PROG(SWIG, "$SWIG", "$SWIG", [])
fi
if test -z "$SWIG"; then
- AC_MSG_WARN([language bindings disabled, swig not found.])
- if test "$cvc4_check_for_bindings" = no -a -n "$try_bindings"; then
- AC_MSG_ERROR([language bindings requested by user, but swig disabled.])
- fi
- else
- AC_MSG_CHECKING([for requested user language bindings])
- if test "$try_bindings" = all; then
- try_bindings='CVC4_SUPPORTED_BINDINGS'
- fi
- try_bindings=$(echo "$try_bindings" | sed 's/,/ /g')
- if test -z "$try_bindings"; then
- AC_MSG_RESULT([none])
- else
- AC_MSG_RESULT([$try_bindings])
- fi
- cvc4_save_CPPFLAGS="$CPPFLAGS"
- cvc4_save_CXXFLAGS="$CXXFLAGS"
- AC_LANG_PUSH([C++])
- for binding in $try_bindings; do
- binding_error=no
- AC_MSG_CHECKING([for availability of $binding binding])
- case "$binding" in
- c++)
- AC_MSG_RESULT([C++ is built by default]);;
- c)
- cvc4_build_c_bindings=yes
- AC_MSG_RESULT([C support will be built]);;
- java)
- AC_MSG_RESULT([Java support will be built])
- AC_ARG_VAR(JAVA_CPPFLAGS, [flags to pass to compiler when building Java bindings])
- CPPFLAGS="$CPPFLAGS $JAVA_CPPFLAGS"
- AC_CHECK_HEADER([jni.h], [cvc4_build_java_bindings=yes], [binding_error=yes])
- ;;
- csharp)
- AC_MSG_RESULT([[C# support will be built]])
- AC_ARG_VAR(CSHARP_CPPFLAGS, [flags to pass to compiler when building C# bindings])
- CPPFLAGS="$CPPFLAGS $CSHARP_CPPFLAGS"
- cvc4_build_csharp_bindings=yes
- ;;
- perl)
- AC_MSG_RESULT([perl support will be built])
- AC_ARG_VAR(PERL_CPPFLAGS, [flags to pass to compiler when building perl bindings])
- CPPFLAGS="$CPPFLAGS $PERL_CPPFLAGS"
- AC_CHECK_HEADER([EXTERN.h], [cvc4_build_perl_bindings=yes], [binding_error=yes])
- ;;
- php)
- AC_MSG_RESULT([php support will be built])
- AC_ARG_VAR(PHP_CPPFLAGS, [flags to pass to compiler when building PHP bindings])
- CPPFLAGS="$CPPFLAGS $PHP_CPPFLAGS"
- AC_CHECK_HEADER([zend.h], [cvc4_build_php_bindings=yes], [binding_error=yes])
- ;;
- python)
- AC_MSG_RESULT([python support will be built])
- AM_PATH_PYTHON([2.5], [cvc4_build_python_bindings=yes], [binding_error=yes])
- AC_ARG_VAR([PYTHON_INCLUDE], [Include flags for python, bypassing python-config])
- AC_ARG_VAR([PYTHON_CONFIG], [Path to python-config])
- AS_IF([test -z "$PYTHON_INCLUDE"], [
- AS_IF([test -z "$PYTHON_CONFIG"], [
- AC_PATH_PROGS([PYTHON_CONFIG],
- [python$PYTHON_VERSION-config python-config],
- [no]
- )
- AS_IF([test "$PYTHON_CONFIG" = no], [AC_MSG_ERROR([cannot find python-config for $PYTHON.])])
- ])
- AC_MSG_CHECKING([python include flags])
- AC_SUBST(PYTHON_CXXFLAGS, `$PYTHON_CONFIG --includes`)
- AC_MSG_RESULT([$PYTHON_CXXFLAGS])
- ])
- CPPFLAGS="$CPPFLAGS $PYTHON_CXXFLAGS"
- AC_CHECK_HEADER([Python.h], [cvc4_build_python_bindings=yes], [binding_error=yes])
- ;;
- ruby)
- AC_MSG_RESULT([ruby support will be built])
- AC_ARG_VAR(RUBY_CPPFLAGS, [flags to pass to compiler when building ruby bindings])
- CPPFLAGS="$CPPFLAGS $RUBY_CPPFLAGS"
- AC_CHECK_HEADER([ruby.h], [cvc4_build_ruby_bindings=yes], [binding_error=yes])
- ;;
- tcl)
- AC_MSG_RESULT([tcl support will be built])
- AC_ARG_VAR(TCL_CPPFLAGS, [flags to pass to compiler when building tcl bindings])
- CPPFLAGS="$CPPFLAGS $TCL_CPPFLAGS"
- AC_CHECK_HEADER([tcl.h], [cvc4_build_tcl_bindings=yes], [binding_error=yes])
- ;;
- ocaml)
- AC_MSG_RESULT([OCaml support will be built])
- AC_ARG_VAR(TCL_CPPFLAGS, [flags to pass to compiler when building OCaml bindings])
- CPPFLAGS="$CPPFLAGS $OCAML_CPPFLAGS"
- AC_CHECK_HEADER([caml/misc.h], [cvc4_build_ocaml_bindings=yes], [binding_error=yes])
- if test "$binding_error" = no; then
- AC_ARG_VAR(OCAMLC, [OCaml compiler])
- if test -z "$OCAMLC"; then
- AC_CHECK_PROGS(OCAMLC, ocamlc, ocamlc, [])
- else
- AC_CHECK_PROG(OCAMLC, "$OCAMLC", "$OCAMLC", [])
- fi
- AC_ARG_VAR(OCAMLMKTOP, [OCaml runtime-maker])
- if test -z "$OCAMLMKTOP"; then
- AC_CHECK_PROGS(OCAMLMKTOP, ocamlmktop, ocamlmktop, [])
- else
- AC_CHECK_PROG(OCAMLMKTOP, "$OCAMLMKTOP", "$OCAMLMKTOP", [])
- fi
- AC_ARG_VAR(OCAMLFIND, [OCaml-find binary])
- if test -z "$OCAMLFIND"; then
- AC_CHECK_PROGS(OCAMLFIND, ocamlfind, ocamlfind, [])
- else
- AC_CHECK_PROG(OCAMLFIND, "$OCAMLFIND", "$OCAMLFIND", [])
- fi
- AC_ARG_VAR(CAMLP4O, [camlp4o binary])
- if test -z "$CAMLP4O"; then
- AC_CHECK_PROGS(CAMLP4O, camlp4o, camlp4o, [])
- else
- AC_CHECK_PROG(CAMLP4O, "$CAMLP4O", "$CAMLP4O", [])
- fi
- fi
- ;;
- *) AC_MSG_RESULT([unknown binding]); binding_error=yes;;
- esac
- if test "$binding_error" = yes; then
- if test "$cvc4_check_for_bindings" = no; then
- AC_MSG_ERROR([Language binding \`$binding' requested by user, but it cannot be built (the preceding few lines should give an indication why this is).])
+ AC_MSG_WARN([language bindings for native API disabled, swig not found.])
+ fi
+fi
+
+AC_MSG_CHECKING([for requested user language bindings])
+if test "$try_bindings" = all; then
+ try_bindings='CVC4_SUPPORTED_BINDINGS'
+fi
+try_bindings=$(echo "$try_bindings" | sed 's/,/ /g')
+if test -z "$try_bindings"; then
+ AC_MSG_RESULT([none])
+else
+ AC_MSG_RESULT([$try_bindings])
+fi
+cvc4_save_CPPFLAGS="$CPPFLAGS"
+cvc4_save_CXXFLAGS="$CXXFLAGS"
+AC_LANG_PUSH([C++])
+for binding in $try_bindings; do
+ binding_error=no
+ AC_MSG_CHECKING([for availability of $binding binding])
+ case "$binding" in
+ c++)
+ AC_MSG_RESULT([C++ is built by default]);;
+ c)
+ cvc4_build_c_bindings=yes
+ AC_MSG_RESULT([C support will be built]);;
+ java)
+ AC_MSG_RESULT([Java support will be built])
+ AC_ARG_VAR(JAVA_CPPFLAGS, [flags to pass to compiler when building Java bindings])
+ CPPFLAGS="$CPPFLAGS $JAVA_CPPFLAGS"
+ AC_CHECK_HEADER([jni.h], [cvc4_build_java_bindings=yes], [binding_error=yes])
+ ;;
+ csharp)
+ AC_MSG_RESULT([[C# support will be built]])
+ AC_ARG_VAR(CSHARP_CPPFLAGS, [flags to pass to compiler when building C# bindings])
+ CPPFLAGS="$CPPFLAGS $CSHARP_CPPFLAGS"
+ cvc4_build_csharp_bindings=yes
+ ;;
+ perl)
+ AC_MSG_RESULT([perl support will be built])
+ AC_ARG_VAR(PERL_CPPFLAGS, [flags to pass to compiler when building perl bindings])
+ CPPFLAGS="$CPPFLAGS $PERL_CPPFLAGS"
+ AC_CHECK_HEADER([EXTERN.h], [cvc4_build_perl_bindings=yes], [binding_error=yes])
+ ;;
+ php)
+ AC_MSG_RESULT([php support will be built])
+ AC_ARG_VAR(PHP_CPPFLAGS, [flags to pass to compiler when building PHP bindings])
+ CPPFLAGS="$CPPFLAGS $PHP_CPPFLAGS"
+ AC_CHECK_HEADER([zend.h], [cvc4_build_php_bindings=yes], [binding_error=yes])
+ ;;
+ python)
+ AC_MSG_RESULT([python support will be built])
+ AM_PATH_PYTHON([2.5], [cvc4_build_python_bindings=yes], [binding_error=yes])
+ AC_ARG_VAR([PYTHON_INCLUDE], [Include flags for python, bypassing python-config])
+ AC_ARG_VAR([PYTHON_CONFIG], [Path to python-config])
+ AS_IF([test -z "$PYTHON_INCLUDE"], [
+ AS_IF([test -z "$PYTHON_CONFIG"], [
+ AC_PATH_PROGS([PYTHON_CONFIG],
+ [python$PYTHON_VERSION-config python-config],
+ [no]
+ )
+ AS_IF([test "$PYTHON_CONFIG" = no], [AC_MSG_ERROR([cannot find python-config for $PYTHON.])])
+ ])
+ AC_MSG_CHECKING([python include flags])
+ AC_SUBST(PYTHON_CXXFLAGS, `$PYTHON_CONFIG --includes`)
+ AC_MSG_RESULT([$PYTHON_CXXFLAGS])
+ ])
+ CPPFLAGS="$CPPFLAGS $PYTHON_CXXFLAGS"
+ AC_CHECK_HEADER([Python.h], [cvc4_build_python_bindings=yes], [binding_error=yes])
+ ;;
+ ruby)
+ AC_MSG_RESULT([ruby support will be built])
+ AC_ARG_VAR(RUBY_CPPFLAGS, [flags to pass to compiler when building ruby bindings])
+ CPPFLAGS="$CPPFLAGS $RUBY_CPPFLAGS"
+ AC_CHECK_HEADER([ruby.h], [cvc4_build_ruby_bindings=yes], [binding_error=yes])
+ ;;
+ tcl)
+ AC_MSG_RESULT([tcl support will be built])
+ AC_ARG_VAR(TCL_CPPFLAGS, [flags to pass to compiler when building tcl bindings])
+ CPPFLAGS="$CPPFLAGS $TCL_CPPFLAGS"
+ AC_CHECK_HEADER([tcl.h], [cvc4_build_tcl_bindings=yes], [binding_error=yes])
+ ;;
+ ocaml)
+ AC_MSG_RESULT([OCaml support will be built])
+ AC_ARG_VAR(TCL_CPPFLAGS, [flags to pass to compiler when building OCaml bindings])
+ CPPFLAGS="$CPPFLAGS $OCAML_CPPFLAGS"
+ AC_CHECK_HEADER([caml/misc.h], [cvc4_build_ocaml_bindings=yes], [binding_error=yes])
+ if test "$binding_error" = no; then
+ AC_ARG_VAR(OCAMLC, [OCaml compiler])
+ if test -z "$OCAMLC"; then
+ AC_CHECK_PROGS(OCAMLC, ocamlc, ocamlc, [])
else
- AC_MSG_WARN([Language binding \`$binding' cannot be built (the preceding few lines should give an indication why this is).])
+ AC_CHECK_PROG(OCAMLC, "$OCAMLC", "$OCAMLC", [])
+ fi
+ AC_ARG_VAR(OCAMLMKTOP, [OCaml runtime-maker])
+ if test -z "$OCAMLMKTOP"; then
+ AC_CHECK_PROGS(OCAMLMKTOP, ocamlmktop, ocamlmktop, [])
+ else
+ AC_CHECK_PROG(OCAMLMKTOP, "$OCAMLMKTOP", "$OCAMLMKTOP", [])
+ fi
+ AC_ARG_VAR(OCAMLFIND, [OCaml-find binary])
+ if test -z "$OCAMLFIND"; then
+ AC_CHECK_PROGS(OCAMLFIND, ocamlfind, ocamlfind, [])
+ else
+ AC_CHECK_PROG(OCAMLFIND, "$OCAMLFIND", "$OCAMLFIND", [])
+ fi
+ AC_ARG_VAR(CAMLP4O, [camlp4o binary])
+ if test -z "$CAMLP4O"; then
+ AC_CHECK_PROGS(CAMLP4O, camlp4o, camlp4o, [])
+ else
+ AC_CHECK_PROG(CAMLP4O, "$CAMLP4O", "$CAMLP4O", [])
fi
- else
- CVC4_LANGUAGE_BINDINGS="${CVC4_LANGUAGE_BINDINGS:+$CVC4_LANGUAGE_BINDINGS }$binding"
fi
- AC_LANG_POP([C++])
- CXXFLAGS="$cvc4_save_CXXFLAGS"
- CPPFLAGS="$cvc4_save_CPPFLAGS"
- done
+ ;;
+ *) AC_MSG_RESULT([unknown binding]); binding_error=yes;;
+ esac
+ if test "$binding_error" = yes; then
+ if test "$cvc4_check_for_bindings" = no; then
+ AC_MSG_ERROR([Language binding \`$binding' requested by user, but it cannot be built (the preceding few lines should give an indication why this is).])
+ else
+ AC_MSG_WARN([Language binding \`$binding' cannot be built (the preceding few lines should give an indication why this is).])
+ fi
+ else
+ CVC4_LANGUAGE_BINDINGS="${CVC4_LANGUAGE_BINDINGS:+$CVC4_LANGUAGE_BINDINGS }$binding"
fi
-fi
+ AC_LANG_POP([C++])
+ CXXFLAGS="$cvc4_save_CXXFLAGS"
+ CPPFLAGS="$cvc4_save_CPPFLAGS"
+done
+
+AM_CONDITIONAL([CVC4_HAS_SWIG], [test "$SWIG"])
m4_foreach([lang], [CVC4_SUPPORTED_BINDINGS],
[AM_CONDITIONAL([CVC4_LANGUAGE_BINDING_]m4_toupper(lang), [test "$cvc4_build_]lang[_bindings" = yes])
projects / cvc5.git / commitdiff