AC_MSG_RESULT([no (user didn't request it)])
fi
+# Java
+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)])
+if test "$cvc4_build_java_bindings"; then
+ dnl AM_PROG_GCJ
+ if test -z "$JAVA"; then
+ AC_CHECK_PROGS(JAVA, java, java, [])
+ else
+ AC_CHECK_PROG(JAVA, "$JAVA", "$JAVA", [])
+ fi
+ if test -z "$JAVAC"; then
+ AC_CHECK_PROGS(JAVAC, javac gcj, javac, [])
+ if test "$JAVAC" = gcj; then JAVAC='gcj -C'; fi
+ else
+ AC_CHECK_PROG(JAVAC, "$JAVAC", "$JAVAC", [])
+ fi
+ if test -z "$JAR"; then
+ AC_CHECK_PROGS(JAR, jar, jar, [])
+ else
+ AC_CHECK_PROG(JAR, "$JAR", "$JAR", [])
+ fi
+fi
+
# Prepare configure output
if test "$enable_shared" = yes; then BUILDING_SHARED=1; else BUILDING_SHARED=0; fi
+# LIBCVC4BINDINGS_VERSION (-version-info) is in the form current:revision:age
+#
+# current -
+# increment if interfaces have been added, removed or changed
+# revision -
+# increment if source code has changed
+# set to zero if current is incremented
+# age -
+# increment if interfaces have been added
+# set to zero if interfaces have been removed
+# or changed
+#
+LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@
+
AM_CPPFLAGS = \
-D__BUILDING_CVC4BINDINGSLIB \
-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
if CVC4_LANGUAGE_BINDING_JAVA
lib_LTLIBRARIES += libcvc4bindings_java.la
data_DATA += cvc4.jar
+libcvc4bindings_java_la_LDFLAGS = \
+ -version-info $(LIBCVC4BINDINGS_VERSION)
+libcvc4bindings_java_la_LIBADD = \
+ -L@builddir@/.. -lcvc4 \
+ -L@builddir@/../parser -lcvc4parser
endif
# cvc4bindings_csharp.so \
# cvc4bindings_perl.so \
# cvc4bindings_tcl.so
nodist_libcvc4bindings_java_la_SOURCES = java.cpp
-#nodist_cvc4bindings_csharp_so_SOURCES = csharp.cpp
-#nodist_cvc4bindings_perl_so_SOURCES = perl.cpp
-#nodist_cvc4bindings_php_so_SOURCES = php.cpp
-#nodist_cvc4bindings_python_so_SOURCES = python.cpp
-#nodist_cvc4bindings_ocaml_so_SOURCES = ocaml.cpp
-#nodist_cvc4bindings_ruby_so_SOURCES = ruby.cpp
-#nodist_cvc4bindings_tcl_so_SOURCES = tcl.cpp
+nodist_libcvc4bindings_csharp_la_SOURCES = csharp.cpp
+nodist_libcvc4bindings_perl_la_SOURCES = perl.cpp
+nodist_libcvc4bindings_php_la_SOURCES = php.cpp
+nodist_libcvc4bindings_python_la_SOURCES = python.cpp
+nodist_libcvc4bindings_ocaml_la_SOURCES = ocaml.cpp
+nodist_libcvc4bindings_ruby_la_SOURCES = ruby.cpp
+nodist_libcvc4bindings_tcl_la_SOURCES = tcl.cpp
BUILT_SOURCES = \
java.cpp \
$(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) \
cvc4.jar
-java.lo: java.cpp; $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) -o $@ $<
-cvc4.jar: java.cpp; $(AM_V_GEN)jar cf $@ -C java .
+java.lo: java.cpp
+ $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) -o $@ $<
+cvc4.jar: java.cpp
+ $(AM_V_GEN) \
+ (cd java; \
+ rm -fr classes; \
+ mkdir -p classes; \
+ $(JAVAC) -classpath . -d classes `find . -name '*.java'`; \
+ cd classes); \
+ $(JAR) cf $@ -C java/classes .
java.cpp:
csharp.cpp:
perl.cpp:
tcl.cpp:
$(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i
$(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@)
- $(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -module cvc4 -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -package edu.nyu.acsys -o $@ $<
+ $(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -package edu.nyu.acsys.CVC4 -o $@ $<
$(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.d: @srcdir@/../cvc4.i
- $(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -module cvc4 -c++ -MM -o $(patsubst %.d,%.cpp,$@) $<
+ $(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -MM -o $(patsubst %.d,%.cpp,$@) $<
# .PHONY so they get rebuilt each time
.PHONY: .swig_deps $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS)))
.swig_deps: $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS)))
if CVC4_BUILD_LIBCOMPAT
-nobase_lib_LTLIBRARIES = libcvc4compat.la
+lib_LTLIBRARIES = libcvc4compat.la
if HAVE_CXXTESTGEN
noinst_LTLIBRARIES = libcvc4compat_noinst.la
endif
libcvc4compat_noinst_la_LDFLAGS =
libcvc4compat_la_LIBADD = \
- @builddir@/../lib/libreplacements.la
+ @builddir@/../lib/libreplacements.la \
+ -L@builddir@/.. -lcvc4 \
+ -L@builddir@/../parser -lcvc4parser
libcvc4compat_noinst_la_LIBADD = \
- @builddir@/../lib/libreplacements.la
+ @builddir@/../lib/libreplacements.la \
+ -L@builddir@/.. -lcvc4 \
+ -L@builddir@/../parser -lcvc4parser
libcvc4compat_la_SOURCES = \
cvc3_compat.h \
%import "bindings/swig.h"
-%module cvc4
-%nspace;
+%module CVC4
+// nspace completely broken with Java packaging
+//%nspace;
%{
-namespace CVC4 {}
+namespace CVC4 { class Exception; }
using namespace CVC4;
%}
+%exception {
+ try {
+ $action
+ } catch(CVC4::Exception& e) {
+ ::std::cerr << e << ::std::endl;
+ jclass clazz = jenv->FindClass("java/lang/RuntimeException");
+ jenv->ThrowNew(clazz, e.toString().c_str());
+ }
+}
+
+%include "std_string.i" // map std::string to java.lang.String
+
%include "util/integer.i"
%include "util/rational.i"
+%include "util/stats.i"
%include "util/exception.i"
%include "util/language.i"
%include "util/options.i"
%include "util/cardinality.i"
-%include "util/stats.i"
%include "util/bool.i"
%include "util/sexpr.i"
%include "util/datatype.i"
%include "smt/bad_option_exception.i"
%include "smt/no_such_function_exception.i"
%include "smt/modal_exception.i"
+
+%include "parser/cvc4parser.i"
friend class ExprManager;
friend class NodeManager;
friend class TypeCheckingException;
- friend std::ostream& operator<<(std::ostream& out, const Expr& e);
+ friend std::ostream& CVC4::operator<<(std::ostream& out, const Expr& e);
template <bool ref_count> friend class NodeTemplate;
};/* class Expr */
%ignore CVC4::theory::operator++(TheoryId&);
+%rename(Kind) CVC4::kind::Kind_t;
+
%include "expr/kind.h"
/** Cast to a Boolean type */
Type::operator BooleanType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isBoolean());
+ Assert(isNull() || isBoolean());
return BooleanType(*this);
}
/** Cast to a integer type */
Type::operator IntegerType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isInteger());
+ Assert(isNull() || isInteger());
return IntegerType(*this);
}
/** Cast to a real type */
Type::operator RealType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isReal());
+ Assert(isNull() || isReal());
return RealType(*this);
}
/** Cast to a pseudoboolean type */
Type::operator PseudobooleanType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isPseudoboolean());
+ Assert(isNull() || isPseudoboolean());
return PseudobooleanType(*this);
}
/** Cast to a bit-vector type */
Type::operator BitVectorType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isBitVector());
+ Assert(isNull() || isBitVector());
return BitVectorType(*this);
}
/** Cast to a Constructor type */
Type::operator DatatypeType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isDatatype());
+ Assert(isNull() || isDatatype());
return DatatypeType(*this);
}
/** Cast to a Constructor type */
Type::operator ConstructorType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isConstructor());
+ Assert(isNull() || isConstructor());
return ConstructorType(*this);
}
/** Cast to a Selector type */
Type::operator SelectorType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isSelector());
+ Assert(isNull() || isSelector());
return SelectorType(*this);
}
/** Cast to a Tester type */
Type::operator TesterType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isTester());
+ Assert(isNull() || isTester());
return TesterType(*this);
}
/** Cast to a function type */
Type::operator FunctionType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isFunction());
+ Assert(isNull() || isFunction());
return FunctionType(*this);
}
/** Cast to a tuple type */
Type::operator TupleType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isTuple());
+ Assert(isNull() || isTuple());
return TupleType(*this);
}
/** Cast to a sort type */
Type::operator SortType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isSort());
+ Assert(isNull() || isSort());
return SortType(*this);
}
/** Cast to a sort type */
Type::operator SortConstructorType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isSortConstructor());
+ Assert(isNull() || isSortConstructor());
return SortConstructorType(*this);
}
/** Cast to a kind type */
Type::operator KindType() const throw(AssertionException) {
NodeManagerScope nms(d_nodeManager);
- Assert(isKind());
+ Assert(isNull() || isKind());
return KindType(*this);
}
Type FunctionType::getRangeType() const {
NodeManagerScope nms(d_nodeManager);
- Assert(isFunction());
+ Assert(isNull() || isFunction());
return makeType(d_typeNode->getRangeType());
}
BooleanType::BooleanType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isBoolean());
+ Assert(isNull() || isBoolean());
}
IntegerType::IntegerType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isInteger());
+ Assert(isNull() || isInteger());
}
RealType::RealType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isReal());
+ Assert(isNull() || isReal());
}
PseudobooleanType::PseudobooleanType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isPseudoboolean());
+ Assert(isNull() || isPseudoboolean());
}
BitVectorType::BitVectorType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isBitVector());
+ Assert(isNull() || isBitVector());
}
DatatypeType::DatatypeType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isDatatype());
+ Assert(isNull() || isDatatype());
}
ConstructorType::ConstructorType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isConstructor());
+ Assert(isNull() || isConstructor());
}
SelectorType::SelectorType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isSelector());
+ Assert(isNull() || isSelector());
}
TesterType::TesterType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isTester());
+ Assert(isNull() || isTester());
}
FunctionType::FunctionType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isFunction());
+ Assert(isNull() || isFunction());
}
TupleType::TupleType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isTuple());
+ Assert(isNull() || isTuple());
}
ArrayType::ArrayType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isArray());
+ Assert(isNull() || isArray());
}
KindType::KindType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isKind());
+ Assert(isNull() || isKind());
}
SortType::SortType(const Type& t) throw(AssertionException) :
Type(t) {
- Assert(isSort());
+ Assert(isNull() || isSort());
}
SortConstructorType::SortConstructorType(const Type& t)
throw(AssertionException) :
Type(t) {
- Assert(isSortConstructor());
+ Assert(isNull() || isSortConstructor());
}
unsigned BitVectorType::getSize() const {
cvc4_SOURCES =
cvc4_LDADD = \
libmain.a \
- ../parser/libcvc4parser.la \
- ../libcvc4.la \
- ../lib/libreplacements.la \
+ @builddir@/../parser/libcvc4parser.la \
+ @builddir@/../libcvc4.la \
+ @builddir@/../lib/libreplacements.la \
$(READLINE_LDFLAGS)
BUILT_SOURCES = \
SUBDIRS = smt smt2 cvc
-nobase_lib_LTLIBRARIES = libcvc4parser.la
+lib_LTLIBRARIES = libcvc4parser.la
if HAVE_CXXTESTGEN
noinst_LTLIBRARIES = libcvc4parser_noinst.la
endif
@builddir@/smt/libparsersmt.la \
@builddir@/smt2/libparsersmt2.la \
@builddir@/cvc/libparsercvc.la \
- @builddir@/../lib/libreplacements.la
+ @builddir@/../lib/libreplacements.la \
+ -L@builddir@/.. -lcvc4
libcvc4parser_noinst_la_LIBADD = \
@builddir@/smt/libparsersmt.la \
@builddir@/smt2/libparsersmt2.la \
@builddir@/cvc/libparsercvc.la \
- @builddir@/../lib/libreplacements.la
+ @builddir@/../lib/libreplacements.la \
+ -L@builddir@/.. -lcvc4
libcvc4parser_la_SOURCES = \
antlr_input.h \
--- /dev/null
+%import "bindings/swig.h"
+
+%module CVC4Parser
+// nspace completely broken with Java packaging
+//%nspace;
+
+%{
+namespace CVC4 {}
+using namespace CVC4;
+%}
+
+%include "parser/parser_exception.i"
+%include "parser/input.i"
+%include "parser/parser.i"
+%include "parser/parser_builder.i"
--- /dev/null
+%{
+#include "parser/input.h"
+%}
+
+%include "parser/input.h"
CHECK_UNDECLARED,
/** Don't check anything */
CHECK_NONE
-};
+};/* enum DeclarationCheck */
/**
* Returns a string representation of the given object (for
* debugging).
*/
+inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) CVC4_PUBLIC;
inline std::ostream& operator<<(std::ostream& out, DeclarationCheck check) {
switch(check) {
case CHECK_NONE:
SYM_VARIABLE,
/** Sorts */
SYM_SORT
-};
+};/* enum SymbolType */
/**
* Returns a string representation of the given object (for
* debugging).
*/
+inline std::ostream& operator<<(std::ostream& out, SymbolType type) CVC4_PUBLIC;
inline std::ostream& operator<<(std::ostream& out, SymbolType type) {
switch(type) {
case SYM_VARIABLE:
--- /dev/null
+%{
+#include "parser/parser.h"
+%}
+
+namespace CVC4 {
+ namespace parser {
+ enum DeclarationCheck;
+ enum SymbolType;
+ %ignore operator<<(std::ostream&, DeclarationCheck);
+ %ignore operator<<(std::ostream&, SymbolType);
+ }/* namespace CVC4::parser */
+}/* namespace CVC4 */
+
+%include "parser/parser.h"
#include <string>
-#include "input.h"
+#include "parser/input.h"
#include "util/language.h"
--- /dev/null
+%{
+#include "parser/parser_builder.h"
+%}
+
+%include "parser/parser_builder.h"
--- /dev/null
+%{
+#include "parser/parser_exception.h"
+%}
+
+%ignore CVC4::parser::ParserException::ParserException(const char*);
+
+%include "parser/parser_exception.h"
#include "smt/bad_option_exception.h"
%}
+%ignore CVC4::BadOptionException::BadOptionException(const char*);
+
%include "smt/bad_option_exception.h"
#include "smt/modal_exception.h"
%}
+%ignore CVC4::ModalException::ModalException(const char*);
+
%include "smt/modal_exception.h"
#include "util/Assert.h"
%}
+%rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException;
+%ignore CVC4::InternalErrorException::InternalErrorException(const char*, const char*, unsigned, const char*, ...);
+
%include "util/Assert.h"
%}
%ignore CVC4::operator<<(std::ostream&, const Exception&);
+%ignore CVC4::Exception::Exception(const char*);
%include "util/exception.h"
#include "util/hash.h"
%}
+%rename(apply) CVC4::StringHashFunction::operator()(const std::string&) const;
+
%include "util/hash.h"
#include "util/language.h"
%}
-%import "util/language.h"
+namespace CVC4 {
+ namespace language {
+ namespace input {
+ %ignore operator<<(std::ostream&, Language);
+ }/* CVC4::language::input namespace */
-%ignore CVC4::operator<<(std::ostream&, CVC4::language::input::Language);
-%ignore CVC4::operator<<(std::ostream&, CVC4::language::output::Language);
+ namespace output {
+ %ignore operator<<(std::ostream&, Language);
+ }/* CVC4::language::output namespace */
+ }/* CVC4::language namespace */
+}/* CVC4 namespace */
+
+// These clash in the monolithic Java namespace, so we rename them.
+%rename(InputLanguage) CVC4::language::input::Language;
+%rename(OutputLanguage) CVC4::language::output::Language;
+
+%rename(INPUT_LANG_AUTO) CVC4::language::input::LANG_AUTO;
+%rename(INPUT_LANG_SMTLIB) CVC4::language::input::LANG_SMTLIB;
+%rename(INPUT_LANG_SMTLIB_V2) CVC4::language::input::LANG_SMTLIB_V2;
+%rename(INPUT_LANG_CVC4) CVC4::language::input::LANG_CVC4;
+%rename(INPUT_LANG_MAX) CVC4::language::input::LANG_MAX;
+
+%rename(OUTPUT_LANG_AUTO) CVC4::language::output::LANG_AUTO;
+%rename(OUTPUT_LANG_SMTLIB) CVC4::language::output::LANG_SMTLIB;
+%rename(OUTPUT_LANG_SMTLIB_V2) CVC4::language::output::LANG_SMTLIB_V2;
+%rename(OUTPUT_LANG_CVC4) CVC4::language::output::LANG_CVC4;
+%rename(OUTPUT_LANG_AST) CVC4::language::output::LANG_AST;
+%rename(OUTPUT_LANG_MAX) CVC4::language::output::LANG_MAX;
%include "util/language.h"
%ignore CVC4::operator<<(std::ostream&, Options::SimplificationMode);
%ignore CVC4::operator<<(std::ostream&, Options::ArithPivotRule);
-%import "util/exception.h"
%include "util/options.h"
#include "util/output.h"
%}
-%import "util/output.h"
-
%feature("valuewrapper") CVC4::null_streambuf;
%feature("valuewrapper") std::ostream;
+// There are issues with SWIG's attempted wrapping of these variables when
+// it tries to generate the getters and setters. For now, just ignore them.
+%ignore CVC4::null_sb;
+%ignore CVC4::null_os;
+%ignore CVC4::DumpC::dump_cout;
+
%include "util/output.h"
return ss.str();
}
-};/* class DataStat<T> */
+};/* class ReadOnlyDataStat<T> */
/**
--- /dev/null
+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);
+ }
+ }
+}
+
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
@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
--- /dev/null
+#!/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[@]}"
projects / cvc5.git / commitdiff