diff options
| -rw-r--r-- | INSTALL | 77 | ||||
| -rw-r--r-- | config/bindings.m4 | 262 | ||||
| -rw-r--r-- | configure.ac | 10 | ||||
| -rw-r--r-- | examples/SimpleVCCompat.java | 2 | ||||
| -rw-r--r-- | examples/simple_vc_compat_c.c | 2 | ||||
| -rw-r--r-- | src/bindings/Makefile.am | 10 | ||||
| -rw-r--r-- | src/bindings/compat/java/Makefile.am | 10 | ||||
| -rw-r--r-- | src/bindings/compat/java/src/cvc3/Embedded.java | 2 |
8 files changed, 231 insertions, 144 deletions
@@ -24,6 +24,10 @@ under doc/ but is not installed by "make install". 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 @@ -78,10 +82,18 @@ Boost project, please visit http://www.boost.org/. 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 @@ -106,6 +118,13 @@ Boost base library) is needed to run CVC4 in "portfolio" (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 @@ -137,6 +156,47 @@ here: 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 @@ -159,3 +219,20 @@ repository. 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/. diff --git a/config/bindings.m4 b/config/bindings.m4 index 29f9f5705..b37a46243 100644 --- a/config/bindings.m4 +++ b/config/bindings.m4 @@ -26,150 +26,146 @@ AC_ARG_ENABLE([language-bindings], [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]) diff --git a/configure.ac b/configure.ac index e4805fd0c..5e4d3a371 100644 --- a/configure.ac +++ b/configure.ac @@ -1208,6 +1208,14 @@ if test -z "$CVC4_LANGUAGE_BINDINGS"; then CVC4_BINDINGS_LIBRARY_VERSION_or_nobuild="N/A" fi +bindings_to_be_built=none +if test -n "$CVC4_LANGUAGE_BINDINGS"; then + bindings_to_be_built="$CVC4_LANGUAGE_BINDINGS" + if test -z "$SWIG"; then + bindings_to_be_built="$bindings_to_be_built (for CVC3 compatibility layer only; SWIG not found)" + fi +fi + cat <<EOF CVC4 $VERSION @@ -1235,7 +1243,7 @@ Static libs : $enable_static Shared libs : $enable_shared Static binary: $enable_static_binary Compat lib : $CVC4_BUILD_LIBCOMPAT -Bindings : ${CVC4_LANGUAGE_BINDINGS:-none} +Bindings : $bindings_to_be_built Multithreaded: $support_multithreaded TLS support : $CVC4_TLS_explanation diff --git a/examples/SimpleVCCompat.java b/examples/SimpleVCCompat.java index fea4f3b7e..65bc62f78 100644 --- a/examples/SimpleVCCompat.java +++ b/examples/SimpleVCCompat.java @@ -39,8 +39,6 @@ import cvc3.*; public class SimpleVCCompat { public static void main(String[] args) { - //System.loadLibrary("cvc4bindings_java_compat"); - ValidityChecker vc = ValidityChecker.create(); // Prove that for integers x and y: diff --git a/examples/simple_vc_compat_c.c b/examples/simple_vc_compat_c.c index f45df65f5..28ec06054 100644 --- a/examples/simple_vc_compat_c.c +++ b/examples/simple_vc_compat_c.c @@ -21,7 +21,7 @@ #include <stdio.h> #include <stdlib.h> -/* #include <cvc4/compat/c_interface.h> /* use this after CVC4 is properly installed */ +/* #include <cvc4/bindings/compat/c/c_interface.h> /* use this after CVC4 is properly installed */ #include "bindings/compat/c/c_interface.h" int main() { diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am index 65961b019..d172e5cf0 100644 --- a/src/bindings/Makefile.am +++ b/src/bindings/Makefile.am @@ -54,7 +54,8 @@ csharpdata_DATA = csharplib_LTLIBRARIES = rubylib_LTLIBRARIES = tcllib_LTLIBRARIES = -if CVC4_LANGUAGE_BINDING_JAVA +if CVC4_HAS_SWIG +if CVC4_LANGUAGE_BINDING_JAVA javalib_LTLIBRARIES += java/libcvc4jni.la javadata_DATA += CVC4.jar java_libcvc4jni_la_LDFLAGS = \ @@ -136,6 +137,8 @@ tcl_CVC4_la_LIBADD = \ -L@builddir@/.. -lcvc4 \ -L@builddir@/../parser -lcvc4parser endif +# this endif matches the "if CVC4_HAS_SWIG" above +endif nodist_java_libcvc4jni_la_SOURCES = java.cpp java_libcvc4jni_la_CXXFLAGS = -fno-strict-aliasing @@ -206,6 +209,9 @@ ruby.lo: ruby.cpp tcl.lo: tcl.cpp $(AM_V_CXX)$(LTCXXCOMPILE) -c $(TCL_CPPFLAGS) -o $@ $< #tcl.cpp:; + +if CVC4_HAS_SWIG + $(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i $(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@) $(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) $($(subst .,_,$@)_SWIGFLAGS) -o $@ $< @@ -218,4 +224,6 @@ $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.d: @srcdir@/. $(AM_V_GEN)cat $+ </dev/null >$@ @mk_include@ .swig_deps +endif + clean-local:; rm -fr $(patsubst %.cpp,%,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am index 2cc6a14d6..f0808334b 100644 --- a/src/bindings/compat/java/Makefile.am +++ b/src/bindings/compat/java/Makefile.am @@ -25,11 +25,11 @@ BUILT_SOURCES = if CVC4_LANGUAGE_BINDING_JAVA -lib_LTLIBRARIES += libcvc4bindings_java_compat.la +lib_LTLIBRARIES += libcvc4compatjni.la javadata_DATA += CVC4compat.jar -libcvc4bindings_java_compat_la_LDFLAGS = \ +libcvc4compatjni_la_LDFLAGS = \ -version-info $(LIBCVC4BINDINGS_VERSION) -libcvc4bindings_java_compat_la_LIBADD = \ +libcvc4compatjni_la_LIBADD = \ -L@builddir@/../../.. -lcvc4 \ -L@builddir@/../../../parser -lcvc4parser \ -L@builddir@/../../../compat -lcvc4compat @@ -112,8 +112,8 @@ SRC_CPP_FILES = src/cvc3/JniUtils.cpp # all cpp files (to compile) CPP_FILES = $(SRC_CPP_FILES) $(JNI_CPP_FILES) -dist_libcvc4bindings_java_compat_la_SOURCES = $(SRC_CPP_FILES) include/cvc3/JniUtils.h -nodist_libcvc4bindings_java_compat_la_SOURCES = $(JNI_CPP_FILES) +dist_libcvc4compatjni_la_SOURCES = $(SRC_CPP_FILES) include/cvc3/JniUtils.h +nodist_libcvc4compatjni_la_SOURCES = $(JNI_CPP_FILES) EXTRA_DIST = \ formula_value.h \ diff --git a/src/bindings/compat/java/src/cvc3/Embedded.java b/src/bindings/compat/java/src/cvc3/Embedded.java index fdeeef058..742e128d8 100644 --- a/src/bindings/compat/java/src/cvc3/Embedded.java +++ b/src/bindings/compat/java/src/cvc3/Embedded.java @@ -14,7 +14,7 @@ public abstract class Embedded { static { System.loadLibrary("cvc4"); System.loadLibrary("cvc4parser"); - System.loadLibrary("cvc4bindings_java_compat"); + System.loadLibrary("cvc4compatjni"); /* // for debugging: stop here by waiting for a key press, |