fix some Java compatibility-layer interface problems; also fix some Mac OS X build issues

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