diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-03-07 21:38:04 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-03-07 21:38:04 +0000 |
commit | a9288938b0244551b713bd3687a62a6aa0762b56 (patch) | |
tree | 3730f4c67351e66a37d5750db8217fc2b4e0c949 /src/bindings | |
parent | c409b60e8c507997a24ba9ea1c611da9132d1e10 (diff) |
fix some Java compatibility-layer interface problems; also fix some Mac OS X build issues
Diffstat (limited to 'src/bindings')
-rw-r--r-- | src/bindings/compat/java/Makefile.am | 70 | ||||
-rw-r--r-- | src/bindings/compat/java/include/cvc3/JniUtils.h | 4 | ||||
-rw-r--r-- | src/bindings/compat/java/src/cvc3/Embedded.java | 2 | ||||
-rw-r--r-- | src/bindings/compat/java/src/cvc3/Expr_impl.cpp | 10 | ||||
-rw-r--r-- | src/bindings/compat/java/src/cvc3/JniUtils.cpp | 4 | ||||
-rw-r--r-- | src/bindings/compat/java/src/cvc3/Type_impl.cpp | 10 | ||||
-rw-r--r-- | src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp | 12 |
7 files changed, 56 insertions, 56 deletions
diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am index 7c22e6231..d268d4d76 100644 --- a/src/bindings/compat/java/Makefile.am +++ b/src/bindings/compat/java/Makefile.am @@ -14,7 +14,8 @@ LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@ AM_CPPFLAGS = \ -D__BUILDING_CVC4BINDINGSLIB \ - -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../.. -I@builddir@/cvc3 + -I@srcdir@/../../../include -I@srcdir@/../../.. \ + -I@srcdir@/include/cvc3 -I@builddir@/../../.. -I@builddir@/cvc3 AM_CXXFLAGS = -Wall javadatadir = $(datadir)/java @@ -25,10 +26,12 @@ BUILT_SOURCES = if CVC4_LANGUAGE_BINDING_JAVA lib_LTLIBRARIES += libcvc4bindings_java_compat.la -javadata_DATA += cvc4compat.jar +javadata_DATA += CVC4compat.jar libcvc4bindings_java_compat_la_LDFLAGS = \ -version-info $(LIBCVC4BINDINGS_VERSION) libcvc4bindings_java_compat_la_LIBADD = \ + -L@builddir@/../../.. -lcvc4 \ + -L@builddir@/../../../parser -lcvc4parser \ -L@builddir@/../../../compat -lcvc4compat BUILT_SOURCES += $(JNI_CPP_FILES) @@ -37,7 +40,6 @@ endif # source files # java files of the library wrapper LIB_FILES = \ - JniUtils \ Cvc3Exception \ TypecheckException \ SoundException \ @@ -80,48 +82,44 @@ TEST_FILES = Test # java files of the stand alone program PROG_FILES = TimeoutHandler Cvc3 # all java files, library and stand alone -JAVA_FILES = $(LIB_FILES) $(TEST_FILES) $(PROG_FILES) -# jni files of the library wrapper -JNI_FILES = \ - EmbeddedManager \ - Expr \ - ExprMut \ - ExprManager \ - Type \ - TypeMut \ - Op \ - OpMut \ - Rational \ - RationalMut \ - Theorem \ - TheoremMut \ - Proof \ - ProofMut \ - Context \ - ContextMut \ - Flag \ - Flags \ - FlagsMut \ - Statistics \ - StatisticsMut \ - ValidityChecker - -# stub files -IMPL_FILES = $(patsubst %,src/cvc3/%_impl.cpp,$(JNI_FILES)) +JAVA_FILES = JniUtils $(LIB_FILES) $(TEST_FILES) $(PROG_FILES) # generated files -JNI_CPP_FILES = $(patsubst %,%.cpp,$(JNI_FILES)) +JNI_CPP_FILES = \ + EmbeddedManager.cpp \ + Expr.cpp \ + ExprMut.cpp \ + ExprManager.cpp \ + ValidityChecker.cpp +# Type.cpp \ +# TypeMut.cpp \ +# Op.cpp \ +# OpMut.cpp \ +# Rational.cpp \ +# RationalMut.cpp \ +# Theorem.cpp \ +# TheoremMut.cpp \ +# Proof.cpp \ +# ProofMut.cpp \ +# Context.cpp \ +# ContextMut.cpp \ +# Flag.cpp \ +# Flags.cpp \ +# FlagsMut.cpp \ +# Statistics.cpp \ +# StatisticsMut.cpp \ # non-generated files SRC_CPP_FILES = src/cvc3/JniUtils.cpp # all cpp files (to compile) CPP_FILES = $(SRC_CPP_FILES) $(JNI_CPP_FILES) -dist_libcvc4bindings_java_compat_la_SOURCES = $(SRC_CPP_FILES) $(IMPL_FILES) include/cvc3/JniUtils.h +dist_libcvc4bindings_java_compat_la_SOURCES = $(SRC_CPP_FILES) include/cvc3/JniUtils.h nodist_libcvc4bindings_java_compat_la_SOURCES = $(JNI_CPP_FILES) EXTRA_DIST = \ formula_value.h \ create_impl.py \ Cvc3_manifest \ + $(SRC_CPP_FILES:%=src/cvc3/%_impl.cpp) \ $(JAVA_FILES:%=src/cvc3/%.java) # compile each cpp file @@ -134,7 +132,7 @@ $(JNI_CPP_FILES): %.cpp: src/cvc3/%_impl.cpp $(builddir)/cvc3/%.h include/cvc3/J JniUtils.lo: src/cvc3/JniUtils.cpp .headers $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) $(JAVA_CPPFLAGS) -I . -o $@ $< -$(LIB_FILES:%=classes/cvc3/%.class): .classes +$(LIB_FILES:%=classes/cvc3/%.class) classes/cvc3/JniUtils.class: .classes .classes: $(AM_V_GEN)mkdir -p classes && $(JAVAC) -source 1.4 -sourcepath $(srcdir)/src -d classes $(LIB_FILES:%=$(srcdir)/src/cvc3/%.java) @touch .classes @@ -144,9 +142,9 @@ $(LIB_FILES:%=cvc3/%.h): %.h: classes/%.class .cvc3dir $(AM_V_GEN)$(JAVAH) -jni -force -classpath classes -o $@ cvc3.$(@:cvc3/%.h=%) .cvc3dir: @mkdir -p cvc3 && touch $@ -cvc4compat.jar: $(LIB_FILES:%=classes/cvc3/%.class) +CVC4compat.jar: $(LIB_FILES:%=classes/cvc3/%.class) classes/cvc3/JniUtils.class $(AM_V_GEN)$(JAR) cf $@ -C classes . clean-local: rm -fr classes cvc3 -MOSTLYCLEANFILES = .cvc3dir .classes .headers cvc4compat.jar $(JNI_CPP_FILES) +MOSTLYCLEANFILES = .cvc3dir .classes .headers CVC4compat.jar $(JNI_CPP_FILES) diff --git a/src/bindings/compat/java/include/cvc3/JniUtils.h b/src/bindings/compat/java/include/cvc3/JniUtils.h index c6bcc04f8..d4688fc25 100644 --- a/src/bindings/compat/java/include/cvc3/JniUtils.h +++ b/src/bindings/compat/java/include/cvc3/JniUtils.h @@ -244,7 +244,7 @@ namespace Java_cvc3_JniUtils { // hash map - template <class K, class V> jobjectArray toJavaHCopy(JNIEnv* env, const Hash::hash_map<K, V>& hm) { + /*template <class K, class V> jobjectArray toJavaHCopy(JNIEnv* env, const Hash::hash_map<K, V>& hm) { jobjectArray jarray = (jobjectArray) env->NewObjectArray( hm.size() * 2, @@ -262,7 +262,7 @@ namespace Java_cvc3_JniUtils { ++i; } return jarray; - } + }*/ template <class V> jobjectArray toJavaHCopy(JNIEnv* env, const CVC3::ExprMap<V>& hm) { jobjectArray jarray = (jobjectArray) diff --git a/src/bindings/compat/java/src/cvc3/Embedded.java b/src/bindings/compat/java/src/cvc3/Embedded.java index c645f2655..fdeeef058 100644 --- a/src/bindings/compat/java/src/cvc3/Embedded.java +++ b/src/bindings/compat/java/src/cvc3/Embedded.java @@ -12,6 +12,8 @@ public abstract class Embedded { // load jni c++ library static { + System.loadLibrary("cvc4"); + System.loadLibrary("cvc4parser"); System.loadLibrary("cvc4bindings_java_compat"); /* diff --git a/src/bindings/compat/java/src/cvc3/Expr_impl.cpp b/src/bindings/compat/java/src/cvc3/Expr_impl.cpp index 58c26eb03..f002109c5 100644 --- a/src/bindings/compat/java/src/cvc3/Expr_impl.cpp +++ b/src/bindings/compat/java/src/cvc3/Expr_impl.cpp @@ -1,7 +1,7 @@ -INCLUDE: <expr.h> -INCLUDE: <theory_array.h> -INCLUDE: <theory_arith.h> -INCLUDE: <theory_bitvector.h> +//INCLUDE: <expr.h> +//INCLUDE: <theory_array.h> +//INCLUDE: <theory_arith.h> +//INCLUDE: <theory_bitvector.h> DEFINITION: Java_cvc3_Expr_jniEquals jboolean c Expr expr1 c Expr expr2 @@ -282,7 +282,7 @@ return expr->arity(); DEFINITION: Java_cvc3_Expr_jniGetKid jobject c Expr expr n int i -return embed_const_ref<Expr>(env, &((*expr)[ji])); +return embed_copy<Expr>(env, (*expr)[ji]); DEFINITION: Java_cvc3_Expr_jniGetKids jobjectArray c Expr expr diff --git a/src/bindings/compat/java/src/cvc3/JniUtils.cpp b/src/bindings/compat/java/src/cvc3/JniUtils.cpp index f291b221b..9ae2023f6 100644 --- a/src/bindings/compat/java/src/cvc3/JniUtils.cpp +++ b/src/bindings/compat/java/src/cvc3/JniUtils.cpp @@ -19,7 +19,7 @@ namespace Java_cvc3_JniUtils { /// Embedding of c++ objects in java objects - /*Embedded* unembed(JNIEnv* env, jobject jobj) { + Embedded* unembed(JNIEnv* env, jobject jobj) { Embedded* embedded = (Embedded*) env->GetDirectBufferAddress(jobj); DebugAssert(embedded != NULL, "JniUtils::unembed: embedded object is NULL"); return embedded; @@ -29,7 +29,7 @@ namespace Java_cvc3_JniUtils { Embedded* embedded = unembed(env, jobj); DebugAssert(embedded != NULL, "JniUtils::deleteEmbedded: embedded object is NULL"); delete embedded; - }*/ + } diff --git a/src/bindings/compat/java/src/cvc3/Type_impl.cpp b/src/bindings/compat/java/src/cvc3/Type_impl.cpp index ce201fa15..769ce984a 100644 --- a/src/bindings/compat/java/src/cvc3/Type_impl.cpp +++ b/src/bindings/compat/java/src/cvc3/Type_impl.cpp @@ -1,8 +1,8 @@ -INCLUDE: "kinds.h" -INCLUDE: "type.h" -INCLUDE: "theory_array.h" -INCLUDE: "theory_bitvector.h" -INCLUDE: "theory_datatype.h" +//INCLUDE: "kinds.h" +//INCLUDE: "type.h" +//INCLUDE: "theory_array.h" +//INCLUDE: "theory_bitvector.h" +//INCLUDE: "theory_datatype.h" DEFINITION: Java_cvc3_Type_jniConstr jobject c Expr expr diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp index e27e44913..34feaacbb 100644 --- a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp +++ b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp @@ -1,14 +1,14 @@ INCLUDE: <sstream> -INCLUDE: <theory_arith.h> -INCLUDE: <theory_array.h> +//INCLUDE: <theory_arith.h> +//INCLUDE: <theory_array.h> DEFINITION: Java_cvc3_ValidityChecker_jniCreate1 jobject -return embed_own<ValidityChecker>(env, VCL::create()); +return embed_own<ValidityChecker>(env, ValidityChecker::create()); DEFINITION: Java_cvc3_ValidityChecker_jniCreate2 jobject c CLFlags flags -return embed_own<ValidityChecker>(env, VCL::create(*flags)); +return embed_own<ValidityChecker>(env, ValidityChecker::create(*flags)); @@ -86,11 +86,11 @@ return toJavaVCopy(env, result); DEFINITION: Java_cvc3_ValidityChecker_jniAnyType jobject m ValidityChecker vc -return embed_copy(env, Type::anyType(vc->getEM())); +Unimplemented(); DEFINITION: Java_cvc3_ValidityChecker_jniArrayLiteral jobject m ValidityChecker vc c Expr indexVar c Expr bodyExpr -return embed_copy(env, CVC3::arrayLiteral(*indexVar, *bodyExpr)); +Unimplemented(); DEFINITION: Java_cvc3_ValidityChecker_jniArrayType jobject m ValidityChecker vc c Type typeIndex c Type typeData |