diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-21 03:26:13 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-21 03:26:13 +0000 |
commit | 3b1689612bb2ff984aa90cd84093ffc043d78ba9 (patch) | |
tree | 872cf423273a331e110ff3868cd5281c960dd3b1 /test/system | |
parent | 69d8f8da6bbb856964d47a583ceb4e50060e9457 (diff) |
considerable bindings interface work, some improvements to build
Diffstat (limited to 'test/system')
-rw-r--r-- | test/system/CVC4JavaTest.java | 50 | ||||
-rw-r--r-- | test/system/Makefile.am | 27 | ||||
-rwxr-xr-x | test/system/run_java_test | 14 |
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[@]}" |