Fixes for warnings from clang++, from -std=gnu++0x, from swig, and from javac

36 files changed, 362 insertions, 40 deletions

diff --git a/config/bindings.m4 b/config/bindings.m4
index 1c4c42695..6aa9b1ac5 100644
--- a/config/bindings.m4
+++ b/config/bindings.m4
@@ -2,7 +2,7 @@
 # -----------------------
 # Supported language bindings for CVC4.
 AC_DEFUN([CVC4_SUPPORTED_BINDINGS],
-[c,java])
+[c,c++,java])
 
 # CVC4_ALL_BINDINGS
 # -----------------
diff --git a/config/cvc4.m4 b/config/cvc4.m4
index c530b8543..0eca68c13 100644
--- a/config/cvc4.m4
+++ b/config/cvc4.m4
@@ -94,7 +94,7 @@ AC_CONFIG_FILES([$1.tmp:$1.in],
 AC_DEFUN([CVC4_CXX_OPTION], [
 AC_MSG_CHECKING([whether $CXX supports $1])
 cvc4_save_CXXFLAGS="$CXXFLAGS"
-CXXFLAGS="$CXXFLAGS $1"
+CXXFLAGS="$CXXFLAGS $WERROR $1"
 AC_LANG_PUSH([C++])
 AC_COMPILE_IFELSE([AC_LANG_SOURCE([int main() { return 0; }])],
                   [AC_MSG_RESULT([yes]); $2='$1'],
diff --git a/configure.ac b/configure.ac
index a4b8892ab..b8127592f 100644
--- a/configure.ac
+++ b/configure.ac
@@ -743,11 +743,17 @@ AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
 # Check for ANTLR runantlr script (defined in config/antlr.m4)
 AC_PROG_ANTLR
 
+CVC4_CXX_OPTION([-Werror], [WERROR])
 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
+CVC4_CXX_OPTION([-Wno-tautological-compare], [WNO_TAUTOLOGICAL_COMPARE])
+CVC4_CXX_OPTION([-Wno-parentheses], [WNO_PARENTHESES])
 CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
 CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
 CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
+AC_SUBST([WERROR])
 AC_SUBST([WNO_CONVERSION_NULL])
+AC_SUBST([WNO_TAUTOLOGICAL_COMPARE])
+AC_SUBST([WNO_PARENTHESES])
 AC_SUBST([WNO_UNINITIALIZED])
 AC_SUBST([WNO_UNUSED_VARIABLE])
 AC_SUBST([FNO_STRICT_ALIASING])
diff --git a/examples/api/java/Makefile.am b/examples/api/java/Makefile.am
index 55f637604..84c818737 100644
--- a/examples/api/java/Makefile.am
+++ b/examples/api/java/Makefile.am
@@ -6,7 +6,8 @@ noinst_DATA += \
 	BitVectorsAndArrays.class \
 	Combination.class \
 	HelloWorld.class \
-	LinearArith.class
+	LinearArith.class \
+	PipedInput.class
 endif
 
 %.class: %.java
@@ -17,7 +18,8 @@ EXTRA_DIST = \
 	BitVectorsAndArrays.java \
 	Combination.java \
 	HelloWorld.java \
-	LinearArith.java
+	LinearArith.java \
+	PipedInput.java
 
 # for installation
 examplesdir = $(docdir)/$(subdir)
diff --git a/examples/api/java/PipedInput.java b/examples/api/java/PipedInput.java
new file mode 100644
index 000000000..3a5470914
--- /dev/null
+++ b/examples/api/java/PipedInput.java
@@ -0,0 +1,69 @@
+/*********************                                                        */
+/*! \file PipedInput.java
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief A simple demonstration of the input parsing capabilities of CVC4
+ ** when used from Java
+ **
+ ** A simple demonstration of the input parsing capabilities of CVC4 when
+ ** used from Java.
+ **/
+
+import edu.nyu.acsys.CVC4.*;
+import java.io.*;
+
+public class PipedInput {
+  public static void main(String[] args) throws IOException {
+    System.loadLibrary("cvc4jni");
+
+    // Boilerplate setup for CVC4
+    ExprManager exprMgr = new ExprManager();
+    SmtEngine smt = new SmtEngine(exprMgr);
+    smt.setOption("incremental", new SExpr(true));
+    smt.setOption("output-language", new SExpr("smt2"));
+
+    // Set up a pair of connected Java streams
+    PipedOutputStream solverPipe = new PipedOutputStream();
+    PrintWriter toSolver = new PrintWriter(solverPipe);
+    PipedInputStream stream = new PipedInputStream(solverPipe);
+
+    // Write some things to CVC4's input stream, making sure to flush()
+    toSolver.println("(set-logic QF_LIA)");
+    toSolver.println("(declare-fun x () Int)");
+    toSolver.println("(assert (= x 5))");
+    toSolver.println("(check-sat)");
+    toSolver.flush();
+
+    // Set up the CVC4 parser
+    ParserBuilder pbuilder =
+      new ParserBuilder(exprMgr, "<string 1>")
+      .withInputLanguage(InputLanguage.INPUT_LANG_SMTLIB_V2)
+      .withLineBufferedStreamInput((java.io.InputStream)stream);
+    Parser parser = pbuilder.build();
+
+    // Read all the commands thus far
+    Command cmd;
+    while((cmd = parser.nextCommand()) != null) {
+      System.out.println(cmd);
+      cmd.invoke(smt, System.out);
+    }
+
+    // Write some more things to CVC4's input stream, making sure to flush()
+    toSolver.println("(assert (= x 10))");
+    toSolver.println("(check-sat)");
+    toSolver.flush();
+
+    // Read all the commands thus far
+    while((cmd = parser.nextCommand()) != null) {
+      System.out.println(cmd);
+      cmd.invoke(smt, System.out);
+    }
+  }
+}
diff --git a/src/bindings/compat/c/c_interface.cpp b/src/bindings/compat/c/c_interface.cpp
index 6540f428c..8219d5169 100644
--- a/src/bindings/compat/c/c_interface.cpp
+++ b/src/bindings/compat/c/c_interface.cpp
@@ -31,6 +31,7 @@
 //#include "fdstream.h"
 #include <string>
 #include <cassert>
+#include <cerrno>
 #include <unistd.h>
 
 #ifdef CVC4_DEBUG
@@ -862,7 +863,12 @@ extern "C" void vc_printExprFile(VC vc, Expr e, int fd)
     CVC3::ValidityChecker* cvc = (CVC3::ValidityChecker*) vc;
     cvc->printExpr(fromExpr(e), ss);
     string s = ss.str();
-    write(fd, s.c_str(), s.size());
+    ssize_t e = write(fd, s.c_str(), s.size());
+    if(e < 0) {
+      IF_DEBUG(cerr << "write() failed, errno == " << errno << endl;)
+      c_interface_error_string = "write() failed";
+      c_interface_error_flag = errno;
+    }
   } catch(CVC3::Exception ex) {
     signal_error("vc_printExpr",error_int,ex);
   }
diff --git a/src/bindings/compat/java/Makefile.am b/src/bindings/compat/java/Makefile.am
index 3b0df308a..e465195d9 100644
--- a/src/bindings/compat/java/Makefile.am
+++ b/src/bindings/compat/java/Makefile.am
@@ -16,7 +16,7 @@ AM_CPPFLAGS = \
 	-D__BUILDING_CVC4BINDINGSLIB \
 	-I@builddir@/../../.. -I@srcdir@/../../../include -I@srcdir@/../../.. \
 	-I@builddir@/cvc3 -I@srcdir@/include/cvc3
-AM_CXXFLAGS = -Wall
+AM_CXXFLAGS = -Wall -Wno-unused-variable
 
 javadatadir = $(datadir)/java
 javalibdir = $(libdir)/jni
diff --git a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
index af588a4ff..fa608a785 100644
--- a/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
+++ b/src/bindings/compat/java/src/cvc3/ValidityChecker_impl.cpp
@@ -87,10 +87,12 @@ return toJavaVCopy(env, result);
 DEFINITION: Java_cvc3_ValidityChecker_jniAnyType
 jobject m ValidityChecker vc
 assert(false);// Unimplemented
+return NULL;
 
 DEFINITION: Java_cvc3_ValidityChecker_jniArrayLiteral
 jobject m ValidityChecker vc c Expr indexVar c Expr bodyExpr
 assert(false);// Unimplemented
+return NULL;
 
 DEFINITION: Java_cvc3_ValidityChecker_jniArrayType
 jobject m ValidityChecker vc c Type typeIndex c Type typeData
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 0cd35ce0d..9fbdeb8d0 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1261,6 +1261,7 @@ Type ValidityChecker::createType(const std::string& typeName) {
 
 Type ValidityChecker::createType(const std::string& typeName, const Type& def) {
   d_parserContext->defineType(typeName, def);
+  return def;
 }
 
 Type ValidityChecker::lookupType(const std::string& typeName) {
@@ -1279,6 +1280,7 @@ Expr ValidityChecker::varExpr(const std::string& name, const Type& type,
                               const Expr& def) {
   CVC4::CheckArgument(def.getType() == type, def, "expected types to match");
   d_parserContext->defineVar(name, def);
+  return def;
 }
 
 Expr ValidityChecker::lookupVar(const std::string& name, Type* type) {
diff --git a/src/cvc4.i b/src/cvc4.i
index 925152248..ebb8cbd63 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -62,6 +62,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %template(vectorCommandPtr) std::vector< CVC4::Command* >;
 %template(vectorType) std::vector< CVC4::Type >;
 %template(vectorExpr) std::vector< CVC4::Expr >;
+%template(vectorVectorExpr) std::vector< std::vector< CVC4::Expr > >;
 %template(vectorDatatypeType) std::vector< CVC4::DatatypeType >;
 %template(vectorSExpr) std::vector< CVC4::SExpr >;
 %template(vectorString) std::vector< std::string >;
@@ -177,7 +178,8 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
   *(CVC4::JavaInputStreamAdapter **)&$result = $1;
 %}
 %typemap(javacode) CVC4::JavaInputStreamAdapter %{
-  private static java.util.HashMap streams = new java.util.HashMap();
+  private static java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter> streams =
+    new java.util.HashMap<java.io.InputStream, JavaInputStreamAdapter>();
   public static JavaInputStreamAdapter get(java.io.InputStream is) {
     if(streams.containsKey(is)) {
       return (JavaInputStreamAdapter) streams.get(is);
@@ -195,6 +197,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %}
 %ignore CVC4::JavaInputStreamAdapter::init(JNIEnv*);
 %ignore CVC4::JavaInputStreamAdapter::pullAdapters(JNIEnv*);
+%ignore CVC4::JavaInputStreamAdapter::pull(JNIEnv*);
 %javamethodmodifiers CVC4::JavaInputStreamAdapter::getInputStream() const "private";
 %javamethodmodifiers CVC4::JavaInputStreamAdapter::JavaInputStreamAdapter(jobject) "private";
 
@@ -256,6 +259,8 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "expr/type.i"
 %include "util/ascription_type.i"
 %include "util/datatype.i"
+%include "util/tuple.i"
+%include "util/record.i"
 %include "util/uninterpreted_constant.i"
 
 %include "expr/kind.i"
diff --git a/src/expr/command.i b/src/expr/command.i
index 09e54fec0..6085a444f 100644
--- a/src/expr/command.i
+++ b/src/expr/command.i
@@ -1,5 +1,12 @@
 %{
 #include "expr/command.h"
+
+#ifdef SWIGJAVA
+
+#include "bindings/java_iterator_adapter.h"
+#include "bindings/java_stream_adapters.h"
+
+#endif /* SWIGJAVA */
 %}
 
 %ignore CVC4::operator<<(std::ostream&, const Command&) throw();
@@ -7,8 +14,55 @@
 %ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw();
 
 %ignore CVC4::GetProofCommand;
+%ignore CVC4::CommandPrintSuccess::Scope;
+
+#ifdef SWIGJAVA
+
+// Instead of CommandSequence::begin() and end(), create an
+// iterator() method on the Java side that returns a Java-style
+// Iterator.
+%ignore CVC4::CommandSequence::begin();
+%ignore CVC4::CommandSequence::end();
+%ignore CVC4::CommandSequence::begin() const;
+%ignore CVC4::CommandSequence::end() const;
+%extend CVC4::CommandSequence {
+  CVC4::JavaIteratorAdapter<CVC4::CommandSequence> iterator() {
+    return CVC4::JavaIteratorAdapter<CVC4::CommandSequence>(*$self);
+  }
+}
+
+// CommandSequence is "iterable" on the Java side
+%typemap(javainterfaces) CVC4::CommandSequence "java.lang.Iterable<edu.nyu.acsys.CVC4.Command>";
 
-%rename(beginConst) CVC4::CommandSequence::begin() const throw();
-%rename(endConst) CVC4::CommandSequence::end() const throw();
+// the JavaIteratorAdapter should not be public, and implements Iterator
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "java.util.Iterator<edu.nyu.acsys.CVC4.Command>";
+// add some functions to the Java side (do it here because there's no way to do these in C++)
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::CommandSequence> "
+  public void remove() {
+    throw new java.lang.UnsupportedOperationException();
+  }
+
+  public edu.nyu.acsys.CVC4.Command next() {
+    if(hasNext()) {
+      return getNext();
+    } else {
+      throw new java.util.NoSuchElementException();
+    }
+  }
+"
+// getNext() just allows C++ iterator access from Java-side next(), make it private
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::CommandSequence>::getNext() "private";
+
+#endif /* SWIGJAVA */
 
 %include "expr/command.h"
+
+#ifdef SWIGJAVA
+
+%include "bindings/java_iterator_adapter.h"
+%include "bindings/java_stream_adapters.h"
+
+%template(JavaIteratorAdapter_CommandSequence) CVC4::JavaIteratorAdapter<CVC4::CommandSequence>;
+
+#endif /* SWIGJAVA */
diff --git a/src/expr/expr.i b/src/expr/expr.i
index 34f074a6d..92ab517b1 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -1,5 +1,12 @@
 %{
 #include "expr/expr.h"
+
+#ifdef SWIGJAVA
+
+#include "bindings/java_iterator_adapter.h"
+#include "bindings/java_stream_adapters.h"
+
+#endif /* SWIGJAVA */
 %}
 
 %rename(apply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
@@ -29,6 +36,44 @@ namespace CVC4 {
   }/* CVC4::expr namespace */
 }/* CVC4 namespace */
 
+#ifdef SWIGJAVA
+
+// Instead of Expr::begin() and end(), create an
+// iterator() method on the Java side that returns a Java-style
+// Iterator.
+%ignore CVC4::Expr::begin() const;
+%ignore CVC4::Expr::end() const;
+%extend CVC4::Expr {
+  CVC4::JavaIteratorAdapter<CVC4::Expr> iterator() {
+    return CVC4::JavaIteratorAdapter<CVC4::Expr>(*$self);
+  }
+}
+
+// Expr is "iterable" on the Java side
+%typemap(javainterfaces) CVC4::Expr "java.lang.Iterable<edu.nyu.acsys.CVC4.Expr>";
+
+// the JavaIteratorAdapter should not be public, and implements Iterator
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Expr> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Expr> "java.util.Iterator<edu.nyu.acsys.CVC4.Expr>";
+// add some functions to the Java side (do it here because there's no way to do these in C++)
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Expr> "
+  public void remove() {
+    throw new java.lang.UnsupportedOperationException();
+  }
+
+  public edu.nyu.acsys.CVC4.Expr next() {
+    if(hasNext()) {
+      return getNext();
+    } else {
+      throw new java.util.NoSuchElementException();
+    }
+  }
+"
+// getNext() just allows C++ iterator access from Java-side next(), make it private
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Expr>::getNext() "private";
+
+#endif /* SWIGJAVA */
+
 %include "expr/expr.h"
 
 %template(getConstTypeConstant) CVC4::Expr::getConst<CVC4::TypeConstant>;
@@ -52,4 +97,13 @@ namespace CVC4 {
 %template(getConstString) CVC4::Expr::getConst<std::string>;
 %template(getConstBoolean) CVC4::Expr::getConst<bool>;
 
+#ifdef SWIGJAVA
+
+%include "bindings/java_iterator_adapter.h"
+%include "bindings/java_stream_adapters.h"
+
+%template(JavaIteratorAdapter_Expr) CVC4::JavaIteratorAdapter<CVC4::Expr>;
+
+#endif /* SWIGJAVA */
+
 %include "expr/expr.h"
diff --git a/src/expr/variable_type_map.i b/src/expr/variable_type_map.i
index a5d50361f..95c705c1e 100644
--- a/src/expr/variable_type_map.i
+++ b/src/expr/variable_type_map.i
@@ -5,4 +5,8 @@
 %rename(get) CVC4::VariableTypeMap::operator[](Expr);
 %rename(get) CVC4::VariableTypeMap::operator[](Type);
 
+%ignore CVC4::ExprManagerMapCollection::d_typeMap;
+%ignore CVC4::ExprManagerMapCollection::d_to;
+%ignore CVC4::ExprManagerMapCollection::d_from;
+
 %include "expr/variable_type_map.h"
diff --git a/src/parser/cvc/Makefile.am b/src/parser/cvc/Makefile.am
index b1cfe7bd8..7c5d48c1c 100644
--- a/src/parser/cvc/Makefile.am
+++ b/src/parser/cvc/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
 	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable $(WNO_CONVERSION_NULL)
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable $(WNO_CONVERSION_NULL)
 
 # Compile generated C files using C++ compiler
 CC=$(CXX)
diff --git a/src/parser/parser.i b/src/parser/parser.i
index 5b23555ea..37aefb901 100644
--- a/src/parser/parser.i
+++ b/src/parser/parser.i
@@ -19,6 +19,8 @@ namespace CVC4 {
   }/* namespace CVC4::parser */
 }/* namespace CVC4 */
 
+%ignore CVC4::parser::Parser::ExprStream;
+
 %include "parser/parser.h"
 
 %{
diff --git a/src/parser/parser_exception.i b/src/parser/parser_exception.i
index 5be81034d..39f67e6f5 100644
--- a/src/parser/parser_exception.i
+++ b/src/parser/parser_exception.i
@@ -3,5 +3,6 @@
 %}
 
 %ignore CVC4::parser::ParserException::ParserException(const char*);
+%ignore CVC4::parser::ParserEndOfFileException::ParserEndOfFileException(const char*);
 
 %include "parser/parser_exception.h"
diff --git a/src/parser/smt1/Makefile.am b/src/parser/smt1/Makefile.am
index 578fae272..90ee7eb31 100644
--- a/src/parser/smt1/Makefile.am
+++ b/src/parser/smt1/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
 	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable
 
 # Compile generated C files using C++ compiler
 AM_CFLAGS = $(AM_CXXFLAGS)
diff --git a/src/parser/smt2/Makefile.am b/src/parser/smt2/Makefile.am
index ec445427a..bf42e9288 100644
--- a/src/parser/smt2/Makefile.am
+++ b/src/parser/smt2/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
 	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable
 
 # Compile generated C files using C++ compiler
 AM_CFLAGS = $(AM_CXXFLAGS)
diff --git a/src/parser/tptp/Makefile.am b/src/parser/tptp/Makefile.am
index 0db7773b2..b5ac965e8 100644
--- a/src/parser/tptp/Makefile.am
+++ b/src/parser/tptp/Makefile.am
@@ -1,7 +1,7 @@
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4PARSERLIB \
 	-I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../.. $(ANTLR_INCLUDES)
-AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) -Wno-unused-function -Wno-unused-variable
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) $(WNO_PARENTHESES) $(WNO_TAUTOLOGICAL_COMPARE) -Wno-unused-function -Wno-unused-variable
 
 # Compile generated C files using C++ compiler
 AM_CFLAGS = $(AM_CXXFLAGS)
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index 0923848e9..c3cd488d8 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -31,6 +31,7 @@ class AstPrinter : public CVC4::Printer {
   void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
   void toStream(std::ostream& out, Model& m, const Command* c) const throw();
 public:
+  using CVC4::Printer::toStream;
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index 524344612..bad05b5c8 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -24,6 +24,8 @@
 #include "smt/options.h"
 #include "theory/model.h"
 #include "theory/arrays/theory_arrays_rewriter.h"
+#include "printer/dagification_visitor.h"
+#include "util/node_visitor.h"
 
 #include <iostream>
 #include <vector>
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index 77d770bb2..71ad947bf 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -22,9 +22,6 @@
 #include <iostream>
 
 #include "printer/printer.h"
-#include "printer/dagification_visitor.h"
-#include "theory/substitutions.h"
-#include "util/node_visitor.h"
 
 namespace CVC4 {
 namespace printer {
@@ -34,6 +31,7 @@ class CvcPrinter : public CVC4::Printer {
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, bool bracket) const throw();
   void toStream(std::ostream& out, Model& m, const Command* c) const throw();
 public:
+  using CVC4::Printer::toStream;
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
diff --git a/src/printer/smt1/smt1_printer.h b/src/printer/smt1/smt1_printer.h
index ca19c19c2..118f6b028 100644
--- a/src/printer/smt1/smt1_printer.h
+++ b/src/printer/smt1/smt1_printer.h
@@ -30,6 +30,7 @@ namespace smt1 {
 class Smt1Printer : public CVC4::Printer {
   void toStream(std::ostream& out, Model& m, const Command* c) const throw();
 public:
+  using CVC4::Printer::toStream;
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 32a0c94ba..cf0d06e6c 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -32,6 +32,7 @@ class Smt2Printer : public CVC4::Printer {
   void toStream(std::ostream& out, Model& m, const Command* c) const throw();
   void toStream(std::ostream& out, Model& m) const throw();
 public:
+  using CVC4::Printer::toStream;
   void toStream(std::ostream& out, TNode n, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const Command* c, int toDepth, bool types, size_t dag) const throw();
   void toStream(std::ostream& out, const CommandStatus* s) const throw();
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 09d8fcbd4..2eabdbea3 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -304,7 +304,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
     }
   }
 
-  BooleanTermCache::iterator i = d_termCache.find(make_pair<Node, theory::TheoryId>(top, parentTheory));
+  BooleanTermCache::iterator i = d_termCache.find(pair<Node, theory::TheoryId>(top, parentTheory));
   if(i != d_termCache.end()) {
     return (*i).second.isNull() ? Node(top) : (*i).second;
   }
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index c53bb8ce5..c326d95d3 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -2,6 +2,7 @@
 #include "smt/smt_engine.h"
 %}
 
+%ignore CVC4::SmtEngine::setLogic(const char*);
 %ignore CVC4::SmtEngine::getProof;
 %ignore CVC4::stats::getStatisticsRegistry(SmtEngine*);
 %ignore CVC4::smt::beforeSearch(std::string, bool, SmtEngine*);
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 1952108f6..f95382cb1 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -119,11 +119,12 @@ EXTRA_DIST = \
 	bool.i \
 	sexpr.i \
 	datatype.i \
+	tuple.i \
+	record.i \
 	output.i \
 	cardinality.i \
 	result.i \
 	configuration.i \
-	cvc4_assert.i \
 	bitvector.i \
 	subrange_bound.i \
 	exception.i \
diff --git a/src/util/cvc4_assert.i b/src/util/cvc4_assert.i
deleted file mode 100644
index 45d76312d..000000000
--- a/src/util/cvc4_assert.i
+++ /dev/null
@@ -1,8 +0,0 @@
-%{
-#include "util/cvc4_assert.h"
-%}
-
-%rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException;
-%ignore CVC4::InternalErrorException::InternalErrorException(const char*, const char*, unsigned, const char*, ...);
-
-%include "util/cvc4_assert.h"
diff --git a/src/util/output.h b/src/util/output.h
index 477035a16..0b89980f2 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -570,7 +570,7 @@ public:
  * used for clearly separating different phases of an algorithm,
  * or iterations of a loop, or... etc.
  */
-class IndentedScope {
+class CVC4_PUBLIC IndentedScope {
   CVC4ostream d_out;
 public:
   inline IndentedScope(CVC4ostream out);
diff --git a/src/util/output.i b/src/util/output.i
index dc524e185..74953ba53 100644
--- a/src/util/output.i
+++ b/src/util/output.i
@@ -3,6 +3,7 @@
 %}
 
 %ignore CVC4::null_streambuf;
+%ignore std::streambuf;
 %feature("valuewrapper") std::ostream;
 
 // There are issues with SWIG's attempted wrapping of these variables when
@@ -10,13 +11,17 @@
 %ignore CVC4::null_sb;
 %ignore CVC4::null_os;
 %ignore CVC4::DumpOutC::dump_cout;
+%ignore CVC4::CVC4ostream;
 
 %ignore operator<<;
 %ignore on(std::string);
 %ignore isOn(std::string);
 %ignore off(std::string);
 %ignore printf(std::string, const char*, ...);
-%ignore operator()(std::string);
+
+%ignore CVC4::IndentedScope;
+%ignore CVC4::push(CVC4ostream&);
+%ignore CVC4::pop(CVC4ostream&);
 
 %ignore CVC4::ScopedDebug::ScopedDebug(std::string);
 %ignore CVC4::ScopedDebug::ScopedDebug(std::string, bool);
@@ -24,6 +29,22 @@
 %ignore CVC4::ScopedTrace::ScopedTrace(std::string);
 %ignore CVC4::ScopedTrace::ScopedTrace(std::string, bool);
 
+%ignore CVC4::WarningC::WarningC(std::ostream*);
+%ignore CVC4::MessageC::MessageC(std::ostream*);
+%ignore CVC4::NoticeC::NoticeC(std::ostream*);
+%ignore CVC4::ChatC::ChatC(std::ostream*);
+%ignore CVC4::TraceC::TraceC(std::ostream*);
+%ignore CVC4::DebugC::DebugC(std::ostream*);
+%ignore CVC4::DumpOutC::DumpOutC(std::ostream*);
+
+%ignore CVC4::WarningC::operator();
+%ignore CVC4::MessageC::operator();
+%ignore CVC4::NoticeC::operator();
+%ignore CVC4::ChatC::operator();
+%ignore CVC4::TraceC::operator();
+%ignore CVC4::DebugC::operator();
+%ignore CVC4::DumpOutC::operator();
+
 %ignore CVC4::WarningC::getStream();
 %ignore CVC4::MessageC::getStream();
 %ignore CVC4::NoticeC::getStream();
@@ -43,7 +64,7 @@
 %ignore operator std::ostream&;
 %ignore operator CVC4ostream;
 
-%rename(get) operator();
+%rename(get) operator ();
 %rename(ok) operator bool;
 
 %include "util/output.h"
diff --git a/src/util/record.i b/src/util/record.i
index f662178c2..2805d2fdf 100644
--- a/src/util/record.i
+++ b/src/util/record.i
@@ -1,5 +1,93 @@
 %{
 #include "util/record.h"
+
+#ifdef SWIGJAVA
+
+#include "bindings/java_iterator_adapter.h"
+#include "bindings/java_stream_adapters.h"
+
+#endif /* SWIGJAVA */
 %}
 
+%rename(equals) CVC4::RecordSelect::operator==(const RecordSelect&) const;
+%ignore CVC4::RecordSelect::operator!=(const RecordSelect&) const;
+
+%rename(equals) CVC4::RecordUpdate::operator==(const RecordUpdate&) const;
+%ignore CVC4::RecordUpdate::operator!=(const RecordUpdate&) const;
+
+%rename(equals) CVC4::Record::operator==(const Record&) const;
+%ignore CVC4::Record::operator!=(const Record&) const;
+%rename(getField) CVC4::Record::operator[](size_t) const;
+
+// These Object arrays are always of two elements, the first is a String and the second a
+// Type.  (On the C++ side, it is a std::pair<std::string, Type>.)
+%typemap(jni) std::pair<std::string, CVC4::Type> "jobjectArray";
+%typemap(jtype) std::pair<std::string, CVC4::Type> "java.lang.Object[]";
+%typemap(jstype) std::pair<std::string, CVC4::Type> "java.lang.Object[]";
+%typemap(javaout) std::pair<std::string, CVC4::Type> { return $jnicall; }
+%typemap(out) std::pair<std::string, CVC4::Type> {
+      $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null);
+      jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str()));
+      jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/Type");
+      jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
+      jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::Type($1.second)), true));
+    };
+
+#ifdef SWIGJAVA
+
+// Instead of Record::begin() and end(), create an
+// iterator() method on the Java side that returns a Java-style
+// Iterator.
+%ignore CVC4::Record::begin() const;
+%ignore CVC4::Record::end() const;
+%extend CVC4::Record {
+  CVC4::Type find(std::string name) const {
+    CVC4::Record::const_iterator i;
+    for(i = $self->begin(); i != $self->end(); ++i) {
+      if((*i).first == name) {
+        return (*i).second;
+      }
+    }
+    return CVC4::Type();
+  }
+
+  CVC4::JavaIteratorAdapter<CVC4::Record> iterator() {
+    return CVC4::JavaIteratorAdapter<CVC4::Record>(*$self);
+  }
+}
+
+// Record is "iterable" on the Java side
+%typemap(javainterfaces) CVC4::Record "java.lang.Iterable<Object[]>";
+
+// the JavaIteratorAdapter should not be public, and implements Iterator
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Record> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Record> "java.util.Iterator<Object[]>";
+// add some functions to the Java side (do it here because there's no way to do these in C++)
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Record> "
+  public void remove() {
+    throw new java.lang.UnsupportedOperationException();
+  }
+
+  public Object[] next() {
+    if(hasNext()) {
+      return getNext();
+    } else {
+      throw new java.util.NoSuchElementException();
+    }
+  }
+"
+// getNext() just allows C++ iterator access from Java-side next(), make it private
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Record>::getNext() "private";
+
+#endif /* SWIGJAVA */
+
 %include "util/record.h"
+
+#ifdef SWIGJAVA
+
+%include "bindings/java_iterator_adapter.h"
+%include "bindings/java_stream_adapters.h"
+
+%template(JavaIteratorAdapter_Record) CVC4::JavaIteratorAdapter<CVC4::Record>;
+
+#endif /* SWIGJAVA */
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 135a83c7e..e9ea83aa1 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -37,6 +37,13 @@
 
 namespace CVC4 {
 
+class CVC4_PUBLIC SExprKeyword {
+  std::string d_str;
+public:
+  SExprKeyword(const std::string& s) : d_str(s) {}
+  const std::string& getString() const { return d_str; }
+};/* class SExpr::Keyword */
+
 /**
  * A simple S-expression. An S-expression is either an atom with a
  * string value, or a list of other S-expressions.
@@ -65,11 +72,7 @@ class CVC4_PUBLIC SExpr {
 
 public:
 
-  class CVC4_PUBLIC Keyword : protected std::string {
-  public:
-    Keyword(const std::string& s) : std::string(s) {}
-    const std::string& getString() const { return *this; }
-  };/* class SExpr::Keyword */
+  typedef SExprKeyword Keyword;
 
   SExpr() :
     d_sexprType(SEXPR_STRING),
diff --git a/src/util/sexpr.i b/src/util/sexpr.i
index 5d78142f3..4c89c5019 100644
--- a/src/util/sexpr.i
+++ b/src/util/sexpr.i
@@ -10,6 +10,11 @@
   std::string toString() const { return self->getValue(); }
 };/* CVC4::SExpr */
 
+%ignore CVC4::SExpr::SExpr(int);
+%ignore CVC4::SExpr::SExpr(unsigned int);
+%ignore CVC4::SExpr::SExpr(unsigned long);
+%ignore CVC4::SExpr::SExpr(const char*);
+
 %rename(equals) CVC4::SExpr::operator==(const SExpr&) const;
 %ignore CVC4::SExpr::operator!=(const SExpr&) const;
 
diff --git a/src/util/statistics.i b/src/util/statistics.i
index 7f3bbe526..bd3a4eeb9 100644
--- a/src/util/statistics.i
+++ b/src/util/statistics.i
@@ -62,7 +62,7 @@
       jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str()));
       jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/SExpr");
       jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
-      jenv->SetObjectArrayElement($result, 1, jenv->NewObject(jenv->FindClass("edu/nyu/acsys/CVC4/SExpr"), methodid, reinterpret_cast<long>(new CVC4::SExpr($1.second)), true));
+      jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::SExpr($1.second)), true));
     };
 
 #endif /* SWIGJAVA */
diff --git a/src/util/tuple.i b/src/util/tuple.i
index d7301d201..f3de7b51b 100644
--- a/src/util/tuple.i
+++ b/src/util/tuple.i
@@ -2,4 +2,10 @@
 #include "util/tuple.h"
 %}
 
+%rename(equals) CVC4::TupleSelect::operator==(const TupleSelect&) const;
+%ignore CVC4::TupleSelect::operator!=(const TupleSelect&) const;
+
+%rename(equals) CVC4::TupleUpdate::operator==(const TupleUpdate&) const;
+%ignore CVC4::TupleUpdate::operator!=(const TupleUpdate&) const;
+
 %include "util/tuple.h"
diff --git a/src/util/util_model.i b/src/util/util_model.i
deleted file mode 100644
index 0d1b3bc81..000000000
--- a/src/util/util_model.i
+++ /dev/null
@@ -1,5 +0,0 @@
-%{
-#include "util/util_model.h"
-%}
-
-%include "util/util_model.h"