Java binding now working. Some interface types still need some work (e.g. iterators aren't functional). Also, output isn't very flexible yet, as I told SWIG to ignore all the operator<<'s.

8 files changed, 39 insertions, 26 deletions

diff --git a/config/bindings.m4 b/config/bindings.m4
index 8231411ed..5758518ef 100644
--- 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 d4ea2ef48..b08c32099 100644
--- 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 e69150b7b..03c258778 100644
--- 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 b8bdfabeb..f3aba34cd 100644
--- 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 062aca478..7225b8108 100644
--- 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 17c1b974b..240131592 100644
--- 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 9e0caccd6..bdafefd07 100644
--- 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 8151300f4..a35ee3771 100644
--- 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);