considerable bindings interface work, some improvements to build

3 files changed, 88 insertions, 3 deletions

diff --git a/test/system/CVC4JavaTest.java b/test/system/CVC4JavaTest.java
new file mode 100644
index 000000000..8151300f4
--- /dev/null
+++ b/test/system/CVC4JavaTest.java
@@ -0,0 +1,50 @@
+import edu.nyu.acsys.CVC4.CVC4;
+
+import edu.nyu.acsys.CVC4.SmtEngine;
+import edu.nyu.acsys.CVC4.ExprManager;
+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.Configuration;
+
+//import edu.nyu.acsys.CVC4.Exception;
+
+import edu.nyu.acsys.CVC4.Parser;
+import edu.nyu.acsys.CVC4.ParserBuilder;
+
+public class CVC4JavaTest {
+  public static void main(String[] args) {
+    try {
+      System.loadLibrary("cvc4bindings_java");
+
+      CVC4.getDebugChannel().on("current");
+
+System.out.println(Configuration.about());
+System.out.println("constructing");
+
+      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");
+
+      System.out.println(smt.checkSat(e));
+
+      System.out.println(smt.getStatisticsRegistry());
+
+      System.exit(1);
+    } catch(Exception e) {
+      System.err.println(e);
+      System.exit(1);
+    }
+  }
+}
+
diff --git a/test/system/Makefile.am b/test/system/Makefile.am
index 4f0fcea14..0f80aa454 100644
--- a/test/system/Makefile.am
+++ b/test/system/Makefile.am
@@ -1,15 +1,23 @@
 TESTS_ENVIRONMENT =
+TEST_EXTENSIONS = .class
 TESTS = \
 	boilerplate \
 	ouroborous
 #	cvc3_main
 
+if CVC4_LANGUAGE_BINDING_JAVA
+TESTS += CVC4JavaTest.class
+endif
+
+CLASS_LOG_COMPILER = @srcdir@/run_java_test $(JAVA) -classpath .:@abs_top_builddir@/src/bindings/cvc4.jar -Djava.library.path=$(abs_top_builddir)/src/bindings/.libs:$(abs_top_builddir)/src/.libs
+
 # Things that aren't tests but that tests rely on and need to
 # go into the distribution
 TEST_DEPS_DIST = \
 	cvc3_main.cpp \
 	cvc3_george.h \
-	cvc3_george.cpp
+	cvc3_george.cpp \
+	CVC4JavaTest.java
 
 # Make-level dependencies; these don't go in the source distribution
 # but should trigger a re-compile of all unit tests.  Libraries are
@@ -54,12 +62,25 @@ LIBADD = \
 	@abs_top_builddir@/src/libcvc4.la
 
 # WHEN SYSTEM TESTS ARE ADDED, BUILD LIKE THIS:
-$(TESTS:%=%.lo): %.lo: %.cpp
+$(filter-out %.class.lo,$(TESTS:%=%.lo)): %.lo: %.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) $(AM_CXXFLAGS) -c -o $@ $+
-$(TESTS): %: %.lo $(LIBADD)
+$(filter-out %.class,$(TESTS)): %: %.lo $(LIBADD)
 	$(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $<
 cvc3_main: cvc3_george.lo $(LIBADD)
 	$(AM_V_CXXLD)$(system_LINK) $(LIBADD) $(AM_LDFLAGS) $+
+CVC4JavaTest.class: CVC4JavaTest.java @abs_top_builddir@/src/bindings/cvc4.jar @abs_top_builddir@/src/bindings/libcvc4bindings_java.la
+	$(AM_V_JAVAC)$(JAVAC) -classpath @abs_top_builddir@/src/bindings/cvc4.jar -d $(builddir) $<
+#CVC4JavaTest: CVC4JavaTest.class
+#	$(AM_V_GEN)( \
+#	echo "#!/bin/bash"; \
+#	echo "exec $(JAVA) -classpath @abs_top_builddir@/src/bindings/cvc4.jar -Djava.library.path=@abs_top_builddir@/src/bindings/.libs CVC4JavaTest"; \
+#	) >$@; \
+#	chmod +x $@
+
+# for silent automake rules
+AM_V_JAVAC = $(am__v_JAVAC_$(V))
+am__v_JAVAC_ = $(am__v_JAVAC_$(AM_DEFAULT_VERBOSITY))
+am__v_JAVAC_0 = @echo "  JAVAC " $@;
 
 # trick automake into setting LTCXXCOMPILE, CXXLINK, etc.
 if CVC4_FALSE
diff --git a/test/system/run_java_test b/test/system/run_java_test
new file mode 100755
index 000000000..205d869f2
--- /dev/null
+++ b/test/system/run_java_test
@@ -0,0 +1,14 @@
+#!/bin/bash
+#
+# run_java_test
+# Morgan Deters, September 2011
+#
+# The purpose of this script is to change an automake test command
+# line into something that a JVM likes.  In particular, any dir/Foo.class
+# listed on the command line is stripped of its dir/ and its .class extension.
+# Works only for tests in the default package.
+#
+args=("$@")
+args[$((${#args}))]="$(echo "${args[${#args}]}" | sed 's,\(.*\/\)\?\(.*\)\.class$,\2,')"
+echo "${args[@]}"
+exec "${args[@]}"