Java binding now working. Some interface types still need some work (e.g. iterators...

diff --git a/config/bindings.m4 b/config/bindings.m4
index 8231411edd8c379a5da67582cfff523536e14dc0..5758518ef62ea94e7c14d56a19ee0a1fda13a953 100644 (file)
--- a/config/bindings.m4
+++ b/config/bindings.m4
@@ -50,14 +50,12 @@ else
       try_bindings=$(echo "$try_bindings" | sed 's/,/ /g')
     fi
     AC_MSG_RESULT([$try_bindings])
-    JAVA_INCLUDES=
     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]);;
         java)
-          JAVA_INCLUDES="-I/usr/lib/jvm/java-6-sun-1.6.0.26/include -I/usr/lib/jvm/java-6-sun-1.6.0.26/include/linux"
           cvc4_build_java_bindings=yes
           AC_MSG_RESULT([Java support will be built]);;
         csharp)
@@ -96,7 +94,6 @@ m4_foreach([lang], [CVC4_SUPPORTED_BINDINGS],
 ])dnl
 
 AC_SUBST(SWIG)
-AC_SUBST(JAVA_INCLUDES)
 AC_SUBST(CVC4_LANGUAGE_BINDINGS)
 
 ])# CVC4_CHECK_BINDINGS

diff --git a/configure.ac b/configure.ac
index d4ea2ef48f68acacc13fb2813ac70654941e544f..b08c32099f7f9b4b8252eac7f867104bf83a54a2 100644 (file)
--- a/configure.ac
+++ b/configure.ac
@@ -839,6 +839,7 @@ fi
 AC_ARG_VAR(JAVA, [Java interpreter (used when testing Java interface)])
 AC_ARG_VAR(JAVAC, [Java compiler (used when building and testing Java interface)])
 AC_ARG_VAR(JAR, [Jar archiver (used when building Java interface)])
+AC_ARG_VAR(JAVA_INCLUDES, [flags to pass to C compiler when building JNI libraries])
 if test "$cvc4_build_java_bindings"; then
   dnl AM_PROG_GCJ
   if test -z "$JAVA"; then

diff --git a/src/cvc4.i b/src/cvc4.i
index e69150b7b3d85aaa1cb9a3738a81c4ca440791ef..03c2587789767d52c789132ef6252167fa144f60 100644 (file)
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -19,7 +19,15 @@ using namespace CVC4;
   }
 }
 
-%include "std_string.i" // map std::string to java.lang.String
+// This is unfortunate, but seems to be necessary; if we leave NULL
+// defined, swig will expand it to "(void*) 0", and some of swig's
+// helper functions won't compile properly.
+#undef NULL
+
+%include "java/typemaps.i" // primitive pointers and references
+%include "java/std_string.i" // map std::string to java.lang.String
+%include "java/arrays_java.i" // C arrays to Java arrays
+%include "java/various.i" // map char** to java.lang.String[]
 
 %include "util/integer.i"
 %include "util/rational.i"

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index b8bdfabeb46db403ebbf9d1f070d70dddbffcd1b..f3aba34cd6044455a77ddbf8ae8a47f841877dc4 100644 (file)
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -97,15 +97,12 @@ endif
 
 %_tags.h: %_tags
        $(AM_V_GEN)( \
-       echo 'static char const *const $^[] = {'; \
-       first=1; \
-       for tag in `cat $^`; \
-       do \
-           if [ $$first -eq 1 ]; then first=0; else echo ','; fi; \
-               echo -n "\"$$tag\""; \
-       done; \
-       echo; \
-       echo '};' \
+         echo 'static char const* const $^[] = {'; \
+         for tag in `cat $^`; do \
+           echo "\"$$tag\","; \
+         done; \
+         echo 'NULL'; \
+         echo '};' \
        ) >"$@"
 
 # This .tmp business is to keep from having to re-compile options.cpp

diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 062aca4780b3cd013cd24b7dccc11e0f8e443061..7225b8108e09a2ff20c7c96c4ffe4874d300a9f7 100644 (file)
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -137,7 +137,8 @@ char const* const* Configuration::getDebugTags() {
 #if CVC4_DEBUG
   return Debug_tags;
 #else /* CVC4_DEBUG */
-  return NULL;
+  static char const* no_tags[] = { NULL };
+  return no_tags;
 #endif /* CVC4_DEBUG */
 }
 
@@ -153,7 +154,8 @@ char const* const* Configuration::getTraceTags() {
 #if CVC4_TRACING
   return Trace_tags;
 #else /* CVC4_TRACING */
-  return NULL;
+  static char const* no_tags[] = { NULL };
+  return no_tags;
 #endif /* CVC4_TRACING */
 }
 

diff --git a/src/util/configuration.i b/src/util/configuration.i
index 17c1b974be3dedeae37561c7b3ccf40171a0ab7e..240131592457f5688e72f3c68d0a7ec10a301906 100644 (file)
--- a/src/util/configuration.i
+++ b/src/util/configuration.i
@@ -2,4 +2,6 @@
 #include "util/configuration.h"
 %}
 
+%apply char **STRING_ARRAY { char const* const* }
 %include "util/configuration.h"
+%clear char const* const*;

diff --git a/src/util/options.i b/src/util/options.i
index 9e0caccd6dad2e77c9417371fbf8560be680669b..bdafefd07162a1b0cbc4e0301e20fe939d540f63 100644 (file)
--- a/src/util/options.i
+++ b/src/util/options.i
@@ -5,4 +5,6 @@
 %ignore CVC4::operator<<(std::ostream&, Options::SimplificationMode);
 %ignore CVC4::operator<<(std::ostream&, Options::ArithPivotRule);
 
+%apply char** STRING_ARRAY { char* argv[] }
 %include "util/options.h"
+%clear char* argv[];

diff --git a/test/system/CVC4JavaTest.java b/test/system/CVC4JavaTest.java
index 8151300f4b6e7daba3bfa79523e22e85d49c30ec..a35ee3771b62a64e4e1fc2864c988961a5163248 100644 (file)
--- a/test/system/CVC4JavaTest.java
+++ b/test/system/CVC4JavaTest.java
@@ -6,6 +6,7 @@ import edu.nyu.acsys.CVC4.Expr;
 import edu.nyu.acsys.CVC4.Type;
 import edu.nyu.acsys.CVC4.BoolExpr;
 import edu.nyu.acsys.CVC4.Kind;
+import edu.nyu.acsys.CVC4.Result;
 import edu.nyu.acsys.CVC4.Configuration;
 
 //import edu.nyu.acsys.CVC4.Exception;
@@ -18,29 +19,32 @@ public class CVC4JavaTest {
     try {
       System.loadLibrary("cvc4bindings_java");
 
-      CVC4.getDebugChannel().on("current");
+      //CVC4.getDebugChannel().on("current");
 
-System.out.println(Configuration.about());
-System.out.println("constructing");
+      System.out.println(Configuration.about());
+
+      String[] tags = Configuration.getDebugTags();
+      System.out.print("available debug tags:");
+      for(int i = 0; i < tags.length; ++i) {
+        System.out.print(" " + tags[i]);
+      }
+      System.out.println();
 
       ExprManager em = new ExprManager();
       SmtEngine smt = new SmtEngine(em);
 
-System.out.println("getting type");
       Type t = em.booleanType();
-System.out.println("making vars");
       Expr a = em.mkVar("a", em.booleanType());
       Expr b = em.mkVar("b", em.booleanType());
-System.out.println("making sausage");
-      BoolExpr e = new BoolExpr(em.mkExpr(Kind.AND, a, b));
-
-System.out.println("about to check");
+      BoolExpr e = new BoolExpr(em.mkExpr(Kind.AND, a, b, new BoolExpr(a).notExpr()));
+      System.out.println("==> " + e);
 
-      System.out.println(smt.checkSat(e));
+      Result r = smt.checkSat(e);
+      boolean correct = r.isSat() == Result.Sat.UNSAT;
 
       System.out.println(smt.getStatisticsRegistry());
 
-      System.exit(1);
+      System.exit(correct ? 0 : 1);
     } catch(Exception e) {
       System.err.println(e);
       System.exit(1);