considerable bindings interface work, some improvements to build

28 files changed, 312 insertions, 68 deletions

diff --git a/configure.ac b/configure.ac
index 8a1039bd9..d4ea2ef48 100644
--- a/configure.ac
+++ b/configure.ac
@@ -835,6 +835,30 @@ else
   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
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index 227f239da..31ad8c71f 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -1,3 +1,17 @@
+# 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@/..
@@ -8,6 +22,11 @@ data_DATA =
 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 \
@@ -18,13 +37,13 @@ endif
 #	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 \
@@ -42,8 +61,16 @@ CLEANFILES = \
 	$(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:
@@ -54,10 +81,10 @@ ruby.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)))
diff --git a/src/compat/Makefile.am b/src/compat/Makefile.am
index 905eaa6c4..1e64a61bb 100644
--- a/src/compat/Makefile.am
+++ b/src/compat/Makefile.am
@@ -19,7 +19,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 if CVC4_BUILD_LIBCOMPAT
 
-nobase_lib_LTLIBRARIES = libcvc4compat.la
+lib_LTLIBRARIES = libcvc4compat.la
 if HAVE_CXXTESTGEN
 noinst_LTLIBRARIES = libcvc4compat_noinst.la
 endif
@@ -29,9 +29,13 @@ libcvc4compat_la_LDFLAGS = \
 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 \
diff --git a/src/cvc4.i b/src/cvc4.i
index 4c574f16c..e69150b7b 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -1,20 +1,33 @@
 %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"
@@ -40,3 +53,5 @@ using namespace CVC4;
 %include "smt/bad_option_exception.i"
 %include "smt/no_such_function_exception.i"
 %include "smt/modal_exception.i"
+
+%include "parser/cvc4parser.i"
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index e95e434fe..616a7c8ff 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -506,7 +506,7 @@ protected:
   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 */
diff --git a/src/expr/kind.i b/src/expr/kind.i
index 1c17f3ff9..95c350cf3 100644
--- a/src/expr/kind.i
+++ b/src/expr/kind.i
@@ -8,4 +8,6 @@
 
 %ignore CVC4::theory::operator++(TheoryId&);
 
+%rename(Kind) CVC4::kind::Kind_t;
+
 %include "expr/kind.h"
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index ff47c6eae..0edc7579b 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -184,7 +184,7 @@ bool Type::isBoolean() const {
 /** Cast to a Boolean type */
 Type::operator BooleanType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isBoolean());
+  Assert(isNull() || isBoolean());
   return BooleanType(*this);
 }
 
@@ -197,7 +197,7 @@ bool Type::isInteger() const {
 /** Cast to a integer type */
 Type::operator IntegerType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isInteger());
+  Assert(isNull() || isInteger());
   return IntegerType(*this);
 }
 
@@ -210,7 +210,7 @@ bool Type::isReal() const {
 /** Cast to a real type */
 Type::operator RealType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isReal());
+  Assert(isNull() || isReal());
   return RealType(*this);
 }
 
@@ -223,7 +223,7 @@ bool Type::isPseudoboolean() const {
 /** Cast to a pseudoboolean type */
 Type::operator PseudobooleanType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isPseudoboolean());
+  Assert(isNull() || isPseudoboolean());
   return PseudobooleanType(*this);
 }
 
@@ -236,14 +236,14 @@ bool Type::isBitVector() const {
 /** 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);
 }
 
@@ -256,7 +256,7 @@ bool Type::isDatatype() const {
 /** Cast to a Constructor type */
 Type::operator ConstructorType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isConstructor());
+  Assert(isNull() || isConstructor());
   return ConstructorType(*this);
 }
 
@@ -269,7 +269,7 @@ bool Type::isConstructor() const {
 /** Cast to a Selector type */
 Type::operator SelectorType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isSelector());
+  Assert(isNull() || isSelector());
   return SelectorType(*this);
 }
 
@@ -282,7 +282,7 @@ bool Type::isSelector() const {
 /** Cast to a Tester type */
 Type::operator TesterType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isTester());
+  Assert(isNull() || isTester());
   return TesterType(*this);
 }
 
@@ -310,7 +310,7 @@ bool Type::isPredicate() const {
 /** Cast to a function type */
 Type::operator FunctionType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isFunction());
+  Assert(isNull() || isFunction());
   return FunctionType(*this);
 }
 
@@ -323,7 +323,7 @@ bool Type::isTuple() const {
 /** Cast to a tuple type */
 Type::operator TupleType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isTuple());
+  Assert(isNull() || isTuple());
   return TupleType(*this);
 }
 
@@ -348,7 +348,7 @@ bool Type::isSort() const {
 /** Cast to a sort type */
 Type::operator SortType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isSort());
+  Assert(isNull() || isSort());
   return SortType(*this);
 }
 
@@ -361,7 +361,7 @@ bool Type::isSortConstructor() const {
 /** Cast to a sort type */
 Type::operator SortConstructorType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isSortConstructor());
+  Assert(isNull() || isSortConstructor());
   return SortConstructorType(*this);
 }
 
@@ -374,7 +374,7 @@ bool Type::isKind() const {
 /** Cast to a kind type */
 Type::operator KindType() const throw(AssertionException) {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isKind());
+  Assert(isNull() || isKind());
   return KindType(*this);
 }
 
@@ -392,7 +392,7 @@ vector<Type> FunctionType::getArgTypes() const {
 
 Type FunctionType::getRangeType() const {
   NodeManagerScope nms(d_nodeManager);
-  Assert(isFunction());
+  Assert(isNull() || isFunction());
   return makeType(d_typeNode->getRangeType());
 }
 
@@ -447,78 +447,78 @@ SortType SortConstructorType::instantiate(const std::vector<Type>& params) const
 
 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 {
diff --git a/src/main/Makefile.am b/src/main/Makefile.am
index 42a306752..d53ae55a0 100644
--- a/src/main/Makefile.am
+++ b/src/main/Makefile.am
@@ -17,9 +17,9 @@ libmain_a_SOURCES = \
 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 = \
diff --git a/src/parser/Makefile.am b/src/parser/Makefile.am
index f1802c6c5..d87db20f5 100644
--- a/src/parser/Makefile.am
+++ b/src/parser/Makefile.am
@@ -19,7 +19,7 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
 SUBDIRS = smt smt2 cvc
 
-nobase_lib_LTLIBRARIES = libcvc4parser.la
+lib_LTLIBRARIES = libcvc4parser.la
 if HAVE_CXXTESTGEN
 noinst_LTLIBRARIES = libcvc4parser_noinst.la
 endif
@@ -32,12 +32,14 @@ libcvc4parser_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_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 \
diff --git a/src/parser/cvc4parser.i b/src/parser/cvc4parser.i
new file mode 100644
index 000000000..2ad3bf01d
--- /dev/null
+++ b/src/parser/cvc4parser.i
@@ -0,0 +1,15 @@
+%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"
diff --git a/src/parser/input.i b/src/parser/input.i
new file mode 100644
index 000000000..2a76e2b7a
--- /dev/null
+++ b/src/parser/input.i
@@ -0,0 +1,5 @@
+%{
+#include "parser/input.h"
+%}
+
+%include "parser/input.h"
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 5ce016b85..46544559a 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -53,12 +53,13 @@ enum DeclarationCheck {
   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:
@@ -80,12 +81,13 @@ enum SymbolType {
   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:
diff --git a/src/parser/parser.i b/src/parser/parser.i
new file mode 100644
index 000000000..55119be9a
--- /dev/null
+++ b/src/parser/parser.i
@@ -0,0 +1,14 @@
+%{
+#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"
diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h
index 6f4f051ec..0463a079f 100644
--- a/src/parser/parser_builder.h
+++ b/src/parser/parser_builder.h
@@ -23,7 +23,7 @@
 
 #include <string>
 
-#include "input.h"
+#include "parser/input.h"
 
 #include "util/language.h"
 
diff --git a/src/parser/parser_builder.i b/src/parser/parser_builder.i
new file mode 100644
index 000000000..6b77356bc
--- /dev/null
+++ b/src/parser/parser_builder.i
@@ -0,0 +1,5 @@
+%{
+#include "parser/parser_builder.h"
+%}
+
+%include "parser/parser_builder.h"
diff --git a/src/parser/parser_exception.i b/src/parser/parser_exception.i
new file mode 100644
index 000000000..5be81034d
--- /dev/null
+++ b/src/parser/parser_exception.i
@@ -0,0 +1,7 @@
+%{
+#include "parser/parser_exception.h"
+%}
+
+%ignore CVC4::parser::ParserException::ParserException(const char*);
+
+%include "parser/parser_exception.h"
diff --git a/src/smt/bad_option_exception.i b/src/smt/bad_option_exception.i
index ddb0e3919..eeded5a45 100644
--- a/src/smt/bad_option_exception.i
+++ b/src/smt/bad_option_exception.i
@@ -2,4 +2,6 @@
 #include "smt/bad_option_exception.h"
 %}
 
+%ignore CVC4::BadOptionException::BadOptionException(const char*);
+
 %include "smt/bad_option_exception.h"
diff --git a/src/smt/modal_exception.i b/src/smt/modal_exception.i
index d82d95666..15b8150cf 100644
--- a/src/smt/modal_exception.i
+++ b/src/smt/modal_exception.i
@@ -2,4 +2,6 @@
 #include "smt/modal_exception.h"
 %}
 
+%ignore CVC4::ModalException::ModalException(const char*);
+
 %include "smt/modal_exception.h"
diff --git a/src/util/Assert.i b/src/util/Assert.i
index 11881982b..b43c36520 100644
--- a/src/util/Assert.i
+++ b/src/util/Assert.i
@@ -2,4 +2,7 @@
 #include "util/Assert.h"
 %}
 
+%rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException;
+%ignore CVC4::InternalErrorException::InternalErrorException(const char*, const char*, unsigned, const char*, ...);
+
 %include "util/Assert.h"
diff --git a/src/util/exception.i b/src/util/exception.i
index d3ff896d2..52ff28922 100644
--- a/src/util/exception.i
+++ b/src/util/exception.i
@@ -3,5 +3,6 @@
 %}
 
 %ignore CVC4::operator<<(std::ostream&, const Exception&);
+%ignore CVC4::Exception::Exception(const char*);
 
 %include "util/exception.h"
diff --git a/src/util/hash.i b/src/util/hash.i
index f2f1e6652..470447fc3 100644
--- a/src/util/hash.i
+++ b/src/util/hash.i
@@ -2,4 +2,6 @@
 #include "util/hash.h"
 %}
 
+%rename(apply) CVC4::StringHashFunction::operator()(const std::string&) const;
+
 %include "util/hash.h"
diff --git a/src/util/language.i b/src/util/language.i
index cd261a73c..28e0eb5ac 100644
--- a/src/util/language.i
+++ b/src/util/language.i
@@ -2,9 +2,33 @@
 #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"
diff --git a/src/util/options.i b/src/util/options.i
index ad4815a33..9e0caccd6 100644
--- a/src/util/options.i
+++ b/src/util/options.i
@@ -5,5 +5,4 @@
 %ignore CVC4::operator<<(std::ostream&, Options::SimplificationMode);
 %ignore CVC4::operator<<(std::ostream&, Options::ArithPivotRule);
 
-%import "util/exception.h"
 %include "util/options.h"
diff --git a/src/util/output.i b/src/util/output.i
index c2729203a..10653c2f8 100644
--- a/src/util/output.i
+++ b/src/util/output.i
@@ -2,9 +2,13 @@
 #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"
diff --git a/src/util/stats.h b/src/util/stats.h
index 7d3e33a6f..42cd73c3d 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -212,7 +212,7 @@ public:
     return ss.str();
   }
 
-};/* class DataStat<T> */
+};/* class ReadOnlyDataStat<T> */
 
 
 /**
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[@]}"