* fix compatibility library naming for SMT-LIBv1

* change name of JNI library to "libcvc4jni", which works better with Java's
  System.loadLibrary().

(this commit was certified error- and warning-free by the test-and-commit script.)

diff --git a/examples/SimpleVC.java b/examples/SimpleVC.java
index a5e2d4e4f30b57d51ce2c2ab9a04ef1ea6771fc6..41c4542fddf6d5c1bf2f630feaaa7db2d8657c4b 100644 (file)
--- a/examples/SimpleVC.java
+++ b/examples/SimpleVC.java
@@ -37,7 +37,7 @@ import edu.nyu.acsys.CVC4.*;
 
 public class SimpleVC {
   public static void main(String[] args) {
-    System.loadLibrary("CVC4");
+    System.loadLibrary("cvc4jni");
 
     ExprManager em = new ExprManager();
     SmtEngine smt = new SmtEngine(em);

diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index 82c45fe92a36dd451649617b5e9e4aeb03bfcbdd..65961b019aa17455155c0e888bd5f3a2d606d9bd 100644 (file)
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -55,12 +55,12 @@ csharplib_LTLIBRARIES =
 rubylib_LTLIBRARIES =
 tcllib_LTLIBRARIES =
 if CVC4_LANGUAGE_BINDING_JAVA
-javalib_LTLIBRARIES += java/CVC4.la
+javalib_LTLIBRARIES += java/libcvc4jni.la
 javadata_DATA += CVC4.jar
-java_CVC4_la_LDFLAGS = \
+java_libcvc4jni_la_LDFLAGS = \
        -module \
        -version-info $(LIBCVC4BINDINGS_VERSION)
-java_CVC4_la_LIBADD = \
+java_libcvc4jni_la_LIBADD = \
        -L@builddir@/.. -lcvc4 \
        -L@builddir@/../parser -lcvc4parser
 endif
@@ -137,8 +137,8 @@ tcl_CVC4_la_LIBADD = \
        -L@builddir@/../parser -lcvc4parser
 endif
 
-nodist_java_CVC4_la_SOURCES = java.cpp
-java_CVC4_la_CXXFLAGS = -fno-strict-aliasing
+nodist_java_libcvc4jni_la_SOURCES = java.cpp
+java_libcvc4jni_la_CXXFLAGS = -fno-strict-aliasing
 nodist_csharp_CVC4_la_SOURCES = csharp.cpp
 nodist_perl_CVC4_la_SOURCES = perl.cpp
 nodist_php_CVC4_la_SOURCES = php.cpp
@@ -164,7 +164,7 @@ MOSTLYCLEANFILES = \
        $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) \
        CVC4.jar
 
-java_CVC4_la-java.lo java.lo: java.cpp
+java_libcvc4jni_la-java.lo java.lo: java.cpp
        $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) -o $@ $<
 CVC4.jar: java.cpp
        $(AM_V_GEN) \

diff --git a/src/compat/cvc3_compat.h b/src/compat/cvc3_compat.h
index c140d29948aec2bb0558825db2cc49c0ba5a99a3..31d914b58618dbb55a2a4f6094132d4238cab281 100644 (file)
--- a/src/compat/cvc3_compat.h
+++ b/src/compat/cvc3_compat.h
@@ -472,7 +472,7 @@ public:
 typedef CVC4::Statistics Statistics;
 
 #define PRESENTATION_LANG ::CVC4::language::input::LANG_CVC4
-#define SMTLIB_LANG ::CVC4::language::input::LANG_SMTLIB
+#define SMTLIB_LANG ::CVC4::language::input::LANG_SMTLIB_V1
 #define SMTLIB_V2_LANG ::CVC4::language::input::LANG_SMTLIB_V2
 #define TPTP_LANG ::CVC4::language::input::LANG_TPTP
 #define AST_LANG ::CVC4::language::input::LANG_AST

diff --git a/test/system/CVC4JavaTest.java b/test/system/CVC4JavaTest.java
index 168961b5cd98c76e06c3fd80f456080e6e03b03f..5a654d03f9af26d2f1c9f126ce6df254c5851390 100644 (file)
--- a/test/system/CVC4JavaTest.java
+++ b/test/system/CVC4JavaTest.java
@@ -17,7 +17,7 @@ import edu.nyu.acsys.CVC4.ParserBuilder;
 public class CVC4JavaTest {
   public static void main(String[] args) {
     try {
-      System.loadLibrary("CVC4");
+      System.loadLibrary("cvc4jni");
 
       //CVC4.getDebugChannel().on("current");
 
@@ -42,7 +42,7 @@ public class CVC4JavaTest {
       Result r = smt.checkSat(e);
       boolean correct = r.isSat() == Result.Sat.UNSAT;
 
-      System.out.println(smt.getStatisticsRegistry());
+      System.out.println(smt.getStatistics());
 
       System.exit(correct ? 0 : 1);
     } catch(Exception e) {