Merge from "swig" branch: language binding for Java is compiling and linking. Enable with --enable-language-bindings=java

52 files changed, 625 insertions, 69 deletions

diff --git a/config/bindings.m4 b/config/bindings.m4
index cdab33e3e..8231411ed 100644
--- a/config/bindings.m4
+++ b/config/bindings.m4
@@ -58,7 +58,7 @@ else
         c++) AC_MSG_RESULT([C++ is built by default]);;
         java)
           JAVA_INCLUDES="-I/usr/lib/jvm/java-6-sun-1.6.0.26/include -I/usr/lib/jvm/java-6-sun-1.6.0.26/include/linux"
-          cvc4_build_java_binding=yes
+          cvc4_build_java_bindings=yes
           AC_MSG_RESULT([Java support will be built]);;
         csharp)
           binding_error=yes
diff --git a/library_versions b/library_versions
index d344bc763..2ff790479 100644
--- a/library_versions
+++ b/library_versions
@@ -1,4 +1,7 @@
-# Format is CVC4-RELEASE-VERSION-REGEXP (LIBRARY:VERSION)*
+# library_versions
+#
+# Format is:
+#   CVC4-RELEASE-VERSION-REGEXP (LIBRARY:VERSION)*
 #
 # This file contains library version release information.
 # Lines are matched while processing configure.ac (and generating
@@ -8,5 +11,14 @@
 # column, are then used.  If there are no matching lines, an error
 # is raised and the configure script is not generated.
 #
+# When a new CVC4 release is cut, this library_versions file should
+# be extended to provide library version information for that
+# release.  PLEASE DON'T REMOVE LINES (or edit historical lines)
+# from this file unless they are truly in error and the release
+# wasn't made with that erroneous information; this file should
+# ultimately provide a nice historical log of the mapping between
+# CVC4 release numbers and the corresponding interface version
+# information of libraries.
+#
 0\..* libcvc4:0:0:0 libcvc4parser:0:0:0 libcvc4compat:0:0:0 libcvc4bindings:0:0:0
 1\.0 libcvc4:0:0:0 libcvc4parser:0:0:0 libcvc4compat:0:0:0 libcvc4bindings:0:0:0
diff --git a/src/Makefile.am b/src/Makefile.am
index e6c00c943..199accf85 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -17,7 +17,7 @@ AM_CPPFLAGS = \
 	-I@srcdir@/include -I@srcdir@ -I@builddir@
 AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
 
-SUBDIRS = lib expr util context theory prop smt printer bindings . parser compat main
+SUBDIRS = lib expr util context theory prop smt printer . parser compat bindings main
 
 lib_LTLIBRARIES = libcvc4.la
 if HAVE_CXXTESTGEN
@@ -57,7 +57,8 @@ EXTRA_DIST = \
 	include/cvc4parser_private.h \
 	include/cvc4parser_public.h \
 	include/cvc4_private.h \
-	include/cvc4_public.h
+	include/cvc4_public.h \
+	cvc4.i
 
 subversion_versioninfo.cpp: svninfo
 	$(AM_V_GEN)( \
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index cd314f957..7c4d7c5a3 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -4,8 +4,10 @@ AM_CPPFLAGS = \
 AM_CXXFLAGS = -Wall $(FLAG_VISIBILITY_HIDDEN)
 
 lib_LTLIBRARIES =
+data_DATA =
 if CVC4_LANGUAGE_BINDING_JAVA
 lib_LTLIBRARIES += libcvc4bindings_java.la
+data_DATA += cvc4.jar
 endif
 #	cvc4bindings_csharp.so \
 #	cvc4bindings_perl.so \
@@ -36,23 +38,30 @@ BUILT_SOURCES = \
 
 CLEANFILES = \
 	$(BUILT_SOURCES) \
-	cvc4.java \
-	cvc4.cs \
-	cvc4JNI.java \
-	cvc4.php \
-	cvc4PINVOKE.cs \
-	cvc4.pm \
-	cvc4.py \
-	php_cvc4.h
+        .swig_deps \
+	$(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) \
+	cvc4.jar
 
-java.lo: java.cpp; $(LTCXXCOMPILE) $(JAVA_INCLUDES) -o $@ $<
-java.cpp::
-csharp.cpp::
-perl.cpp::
-php.cpp::
-python.cpp::
-ocaml.cpp::
-ruby.cpp::
-tcl.cpp::
-$(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))):: %.cpp: @srcdir@/../smt/smt_engine.h
-	$(AM_V_GEN)$(SWIG) -w503 -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -module cvc4 -c++ -$(patsubst %.cpp,%,$@) -o $@ $<
+java.lo: java.cpp; $(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_INCLUDES) -o $@ $<
+cvc4.jar: java.cpp; $(AM_V_GEN)jar cf $@ -C java .
+java.cpp:
+csharp.cpp:
+perl.cpp:
+php.cpp:
+python.cpp:
+ocaml.cpp:
+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 $@ $<
+
+$(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,$@) $<
+# .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)))
+	$(AM_V_GEN)cat $+ >$@
+@mk_include@ .swig_deps
+
+clean-local:; rm -fr $(patsubst %.cpp,%,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS)))
diff --git a/src/bindings/swig.h b/src/bindings/swig.h
new file mode 100644
index 000000000..7dec263f6
--- /dev/null
+++ b/src/bindings/swig.h
@@ -0,0 +1,38 @@
+/*********************                                                        */
+/*! \file swig.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Common swig checks and definitions
+ **
+ ** Common swig checks and definitions, when generating swig interfaces.
+ **/
+
+#ifndef __CVC4__BINDINGS__SWIG_H
+#define __CVC4__BINDINGS__SWIG_H
+
+#ifndef SWIG
+#  error This file should only be included when generating swig interfaces.
+#endif /* SWIG */
+
+#if !defined(SWIG_VERSION) || SWIG_VERSION < 0x020000
+#  error CVC4 bindings require swig version 2.0.0 or later, sorry.
+#endif /* SWIG_VERSION */
+
+%import "cvc4_public.h"
+%import "util/tls.h"
+
+// swig doesn't like the __thread storage class...
+#define __thread
+// ...or GCC attributes
+#define __attribute__(x)
+
+#endif /* __CVC4__BINDINGS__SWIG_H */
diff --git a/src/cvc4.i b/src/cvc4.i
new file mode 100644
index 000000000..4c574f16c
--- /dev/null
+++ b/src/cvc4.i
@@ -0,0 +1,42 @@
+%import "bindings/swig.h"
+
+%module cvc4
+%nspace;
+
+%{
+namespace CVC4 {}
+using namespace CVC4;
+%}
+
+%include "util/integer.i"
+%include "util/rational.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 "util/output.i"
+%include "util/result.i"
+%include "util/configuration.i"
+%include "util/Assert.i"
+%include "util/bitvector.i"
+%include "util/subrange_bound.i"
+%include "util/array.i"
+%include "util/ascription_type.i"
+%include "util/pseudoboolean.i"
+%include "util/hash.i"
+
+%include "expr/command.i"
+%include "expr/declaration_scope.i"
+%include "expr/kind.i"
+%include "expr/type.i"
+%include "expr/expr.i"
+%include "expr/expr_manager.i"
+
+%include "smt/smt_engine.i"
+%include "smt/bad_option_exception.i"
+%include "smt/no_such_function_exception.i"
+%include "smt/modal_exception.i"
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 738604f90..03de15706 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -52,7 +52,13 @@ EXTRA_DIST = \
 	type_checker_template.cpp \
 	mkkind \
 	mkmetakind \
-	mkexpr
+	mkexpr \
+	expr_manager.i \
+	declaration_scope.i \
+	command.i \
+	type.i \
+	kind.i \
+	expr.i
 
 BUILT_SOURCES = \
 	kind.h \
diff --git a/src/expr/command.i b/src/expr/command.i
new file mode 100644
index 000000000..3a029b785
--- /dev/null
+++ b/src/expr/command.i
@@ -0,0 +1,12 @@
+%{
+#include "expr/command.h"
+%}
+
+%ignore CVC4::operator<<(std::ostream&, const Command&);
+%ignore CVC4::operator<<(std::ostream&, const Command*);
+%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status);
+
+%rename(beginConst) CVC4::CommandSequence::begin() const;
+%rename(endConst) CVC4::CommandSequence::end() const;
+
+%include "expr/command.h"
diff --git a/src/expr/declaration_scope.i b/src/expr/declaration_scope.i
new file mode 100644
index 000000000..e32c4ee4f
--- /dev/null
+++ b/src/expr/declaration_scope.i
@@ -0,0 +1,5 @@
+%{
+#include "expr/declaration_scope.h"
+%}
+
+%include "expr/declaration_scope.h"
diff --git a/src/expr/expr.i b/src/expr/expr.i
new file mode 100644
index 000000000..ff4d219a2
--- /dev/null
+++ b/src/expr/expr.i
@@ -0,0 +1,25 @@
+%{
+#include "expr/expr.h"
+%}
+
+%rename(apply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
+
+%ignore CVC4::operator<<(std::ostream&, const Expr&);
+%ignore CVC4::operator<<(std::ostream&, const TypeCheckingException&);
+
+%ignore CVC4::expr::operator<<(std::ostream&, ExprSetDepth);
+%ignore CVC4::expr::operator<<(std::ostream&, ExprPrintTypes);
+%ignore CVC4::expr::operator<<(std::ostream&, ExprSetLanguage);
+
+%rename(assign) CVC4::Expr::operator=(const Expr&);
+%rename(equals) CVC4::Expr::operator==(const Expr&) const;
+%ignore CVC4::Expr::operator!=(const Expr&) const;
+%rename(less) CVC4::Expr::operator<(const Expr&) const;
+%rename(lessEqual) CVC4::Expr::operator<=(const Expr&) const;
+%rename(greater) CVC4::Expr::operator>(const Expr&) const;
+%rename(greaterEqual) CVC4::Expr::operator>=(const Expr&) const;
+
+%rename(getChild) CVC4::Expr::operator[](unsigned i) const;
+%ignore CVC4::Expr::operator bool() const;// can just use isNull()
+
+%include "expr/expr.h"
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
new file mode 100644
index 000000000..739da614a
--- /dev/null
+++ b/src/expr/expr_manager.i
@@ -0,0 +1,5 @@
+%{
+#include "expr/expr_manager.h"
+%}
+
+%include "expr/expr_manager.h"
diff --git a/src/expr/kind.i b/src/expr/kind.i
new file mode 100644
index 000000000..1c17f3ff9
--- /dev/null
+++ b/src/expr/kind.i
@@ -0,0 +1,11 @@
+%{
+#include "expr/kind.h"
+%}
+
+%ignore CVC4::kind::operator<<(std::ostream&, CVC4::Kind);
+%ignore CVC4::operator<<(std::ostream&, TypeConstant);
+%ignore CVC4::theory::operator<<(std::ostream&, TheoryId);
+
+%ignore CVC4::theory::operator++(TheoryId&);
+
+%include "expr/kind.h"
diff --git a/src/expr/type.cpp b/src/expr/type.cpp
index 28bcb460f..ff47c6eae 100644
--- a/src/expr/type.cpp
+++ b/src/expr/type.cpp
@@ -114,6 +114,18 @@ bool Type::operator<(const Type& t) const {
   return *d_typeNode < *t.d_typeNode;
 }
 
+bool Type::operator<=(const Type& t) const {
+  return *d_typeNode <= *t.d_typeNode;
+}
+
+bool Type::operator>(const Type& t) const {
+  return *d_typeNode > *t.d_typeNode;
+}
+
+bool Type::operator>=(const Type& t) const {
+  return *d_typeNode >= *t.d_typeNode;
+}
+
 Type Type::substitute(const Type& type, const Type& replacement) const {
   NodeManagerScope nms(d_nodeManager);
   return makeType(d_typeNode->substitute(*type.d_typeNode,
@@ -610,7 +622,7 @@ BooleanType TesterType::getRangeType() const {
   return BooleanType(makeType(d_nodeManager->booleanType()));
 }
 
-size_t TypeHashFunction::operator()(const Type& t) {
+size_t TypeHashFunction::operator()(const Type& t) const {
   return TypeNodeHashFunction()(NodeManager::fromType(t));
 }
 
diff --git a/src/expr/type.h b/src/expr/type.h
index 5bff8d12a..f470f0874 100644
--- a/src/expr/type.h
+++ b/src/expr/type.h
@@ -63,7 +63,7 @@ class Type;
 /** Strategy for hashing Types */
 struct CVC4_PUBLIC TypeHashFunction {
   /** Return a hash code for type t */
-  size_t operator()(const CVC4::Type& t);
+  size_t operator()(const CVC4::Type& t) const;
 };/* struct TypeHashFunction */
 
 /**
@@ -84,7 +84,7 @@ class CVC4_PUBLIC Type {
   friend class NodeManager;
   friend class TypeNode;
   friend struct TypeHashStrategy;
-  friend std::ostream& operator<<(std::ostream& out, const Type& t);
+  friend std::ostream& CVC4::operator<<(std::ostream& out, const Type& t);
 
 protected:
 
@@ -191,6 +191,21 @@ public:
   bool operator<(const Type& t) const;
 
   /**
+   * An ordering on Types so they can be stored in maps, etc.
+   */
+  bool operator<=(const Type& t) const;
+
+  /**
+   * An ordering on Types so they can be stored in maps, etc.
+   */
+  bool operator>(const Type& t) const;
+
+  /**
+   * An ordering on Types so they can be stored in maps, etc.
+   */
+  bool operator>=(const Type& t) const;
+
+  /**
    * Is this the Boolean type?
    * @return true if the type is a Boolean type
    */
diff --git a/src/expr/type.i b/src/expr/type.i
new file mode 100644
index 000000000..314903342
--- /dev/null
+++ b/src/expr/type.i
@@ -0,0 +1,33 @@
+%{
+#include "expr/type.h"
+%}
+
+%rename(apply) CVC4::TypeHashFunction::operator()(const CVC4::Type&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const Type&);
+
+%rename(assign) CVC4::Type::operator=(const Type&);
+%rename(equals) CVC4::Type::operator==(const Type&) const;
+%ignore CVC4::Type::operator!=(const Type&) const;
+%rename(less) CVC4::Type::operator<(const Type&) const;
+%rename(lessEqual) CVC4::Type::operator<=(const Type&) const;
+%rename(greater) CVC4::Type::operator>(const Type&) const;
+%rename(greaterEqual) CVC4::Type::operator>=(const Type&) const;
+
+%rename(toBooleanType) CVC4::Type::operator BooleanType() const;
+%rename(toIntegerType) CVC4::Type::operator IntegerType() const;
+%rename(toRealType) CVC4::Type::operator RealType() const;
+%rename(toPseudobooleanType) CVC4::Type::operator PseudobooleanType() const;
+%rename(toBitVectorType) CVC4::Type::operator BitVectorType() const;
+%rename(toFunctionType) CVC4::Type::operator FunctionType() const;
+%rename(toTupleType) CVC4::Type::operator TupleType() const;
+%rename(toArrayType) CVC4::Type::operator ArrayType() const;
+%rename(toDatatypeType) CVC4::Type::operator DatatypeType() const;
+%rename(toConstructorType) CVC4::Type::operator ConstructorType() const;
+%rename(toSelectorType) CVC4::Type::operator SelectorType() const;
+%rename(toTesterType) CVC4::Type::operator TesterType() const;
+%rename(toSortType) CVC4::Type::operator SortType() const;
+%rename(toSortConstructorType) CVC4::Type::operator SortConstructorType() const;
+%rename(toKindType) CVC4::Type::operator KindType() const;
+
+%include "expr/type.h"
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 25af3aae6..966611764 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -179,13 +179,46 @@ public:
    * that subexpressions have to be smaller than the enclosing expressions.
    *
    * @param typeNode the node to compare to
-   * @return true if this expression is smaller
+   * @return true if this expression is lesser
    */
   inline bool operator<(const TypeNode& typeNode) const {
     return d_nv->d_id < typeNode.d_nv->d_id;
   }
 
   /**
+   * We compare by expression ids so, keeping things deterministic and having
+   * that subexpressions have to be smaller than the enclosing expressions.
+   *
+   * @param typeNode the node to compare to
+   * @return true if this expression is lesser or equal
+   */
+  inline bool operator<=(const TypeNode& typeNode) const {
+    return d_nv->d_id <= typeNode.d_nv->d_id;
+  }
+
+  /**
+   * We compare by expression ids so, keeping things deterministic and having
+   * that subexpressions have to be smaller than the enclosing expressions.
+   *
+   * @param typeNode the node to compare to
+   * @return true if this expression is greater
+   */
+  inline bool operator>(const TypeNode& typeNode) const {
+    return d_nv->d_id > typeNode.d_nv->d_id;
+  }
+
+  /**
+   * We compare by expression ids so, keeping things deterministic and having
+   * that subexpressions have to be smaller than the enclosing expressions.
+   *
+   * @param typeNode the node to compare to
+   * @return true if this expression is greater or equal
+   */
+  inline bool operator>=(const TypeNode& typeNode) const {
+    return d_nv->d_id >= typeNode.d_nv->d_id;
+  }
+
+  /**
    * Returns the i-th child of this node.
    *
    * @param i the index of the child
diff --git a/src/smt/Makefile.am b/src/smt/Makefile.am
index 2f9f08302..3e777ec89 100644
--- a/src/smt/Makefile.am
+++ b/src/smt/Makefile.am
@@ -11,3 +11,9 @@ libsmt_la_SOURCES = \
 	modal_exception.h \
 	bad_option_exception.h \
 	no_such_function_exception.h
+
+EXTRA_DIST = \
+	bad_option_exception.i \
+	no_such_function_exception.i \
+	modal_exception.i \
+	smt_engine.i
diff --git a/src/smt/bad_option_exception.i b/src/smt/bad_option_exception.i
new file mode 100644
index 000000000..ddb0e3919
--- /dev/null
+++ b/src/smt/bad_option_exception.i
@@ -0,0 +1,5 @@
+%{
+#include "smt/bad_option_exception.h"
+%}
+
+%include "smt/bad_option_exception.h"
diff --git a/src/smt/modal_exception.i b/src/smt/modal_exception.i
new file mode 100644
index 000000000..d82d95666
--- /dev/null
+++ b/src/smt/modal_exception.i
@@ -0,0 +1,5 @@
+%{
+#include "smt/modal_exception.h"
+%}
+
+%include "smt/modal_exception.h"
diff --git a/src/smt/no_such_function_exception.i b/src/smt/no_such_function_exception.i
new file mode 100644
index 000000000..0c67ad0d3
--- /dev/null
+++ b/src/smt/no_such_function_exception.i
@@ -0,0 +1,5 @@
+%{
+#include "smt/no_such_function_exception.h"
+%}
+
+%include "smt/no_such_function_exception.h"
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 698f9ba2e..d2abf2fce 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -23,26 +23,6 @@
 
 #include <vector>
 
-#if SWIG
-%include "cvc4_public.h"
-%include "util/rational.h"
-%include "util/exception.h"
-%include "expr/kind.h"
-%include "util/integer.h"
-%include "util/cardinality.h"
-%include "util/sexpr.h"
-%include "util/language.h"
-%include "expr/type.h"
-%include "expr/expr.h"
-%include "expr/expr_manager.h"
-%{
-#include "util/integer.h"
-#include "expr/expr_manager.h"
-#include "expr/type.h"
-#include "expr/expr.h"
-%}
-#endif
-
 #include "context/cdlist_forward.h"
 #include "context/cdmap_forward.h"
 #include "context/cdset_forward.h"
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
new file mode 100644
index 000000000..64a4f93e2
--- /dev/null
+++ b/src/smt/smt_engine.i
@@ -0,0 +1,5 @@
+%{
+#include "smt/smt_engine.h"
+%}
+
+%include "smt/smt_engine.h"
diff --git a/src/util/Assert.i b/src/util/Assert.i
new file mode 100644
index 000000000..11881982b
--- /dev/null
+++ b/src/util/Assert.i
@@ -0,0 +1,5 @@
+%{
+#include "util/Assert.h"
+%}
+
+%include "util/Assert.h"
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 7f5fb459e..b8bdfabeb 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -139,4 +139,24 @@ EXTRA_DIST = \
 	rational_gmp_imp.cpp \
 	rational.h.in \
 	integer.h.in \
-	tls.h.in
+	tls.h.in \
+	integer.i \
+	stats.i \
+	bool.i \
+	sexpr.i \
+	datatype.i \
+	output.i \
+	cardinality.i \
+	result.i \
+	configuration.i \
+	Assert.i \
+	bitvector.i \
+	subrange_bound.i \
+	exception.i \
+	language.i \
+	array.i \
+	options.i \
+	ascription_type.i \
+	rational.i \
+	pseudoboolean.i \
+	hash.i
diff --git a/src/util/array.i b/src/util/array.i
new file mode 100644
index 000000000..593ce9490
--- /dev/null
+++ b/src/util/array.i
@@ -0,0 +1,5 @@
+%{
+#include "util/array.h"
+%}
+
+%include "util/array.h"
diff --git a/src/util/ascription_type.i b/src/util/ascription_type.i
new file mode 100644
index 000000000..b0b57d5f9
--- /dev/null
+++ b/src/util/ascription_type.i
@@ -0,0 +1,11 @@
+%{
+#include "util/ascription_type.h"
+%}
+
+
+%rename(equals) CVC4::AscriptionType::operator==(const AscriptionType&) const;
+%ignore CVC4::AscriptionType::operator!=(const AscriptionType&) const;
+
+%ignore CVC4::operator<<(std::ostream&, AscriptionType);
+
+%include "util/ascription_type.h"
diff --git a/src/util/bitvector.i b/src/util/bitvector.i
new file mode 100644
index 000000000..085a59b2d
--- /dev/null
+++ b/src/util/bitvector.i
@@ -0,0 +1,28 @@
+%{
+#include "util/bitvector.h"
+%}
+
+%ignore CVC4::BitVector::BitVector(unsigned, unsigned);
+
+%rename(assign) CVC4::BitVector::operator=(const BitVector&);
+%rename(equals) CVC4::BitVector::operator==(const BitVector&) const;
+%ignore CVC4::BitVector::operator!=(const BitVector&) const;
+%rename(plus) CVC4::BitVector::operator+(const BitVector&) const;
+%rename(minus) CVC4::BitVector::operator-(const BitVector&) const;
+%rename(minus) CVC4::BitVector::operator-() const;
+%rename(times) CVC4::BitVector::operator*(const BitVector&) const;
+%rename(complement) CVC4::BitVector::operator~() const;
+
+%rename(equals) CVC4::BitVectorExtract::operator==(const BitVectorExtract&) const;
+
+%rename(toUnsigned) CVC4::BitVectorSize::operator unsigned() const;
+%rename(toUnsigned) CVC4::BitVectorRepeat::operator unsigned() const;
+%rename(toUnsigned) CVC4::BitVectorZeroExtend::operator unsigned() const;
+%rename(toUnsigned) CVC4::BitVectorSignExtend::operator unsigned() const;
+%rename(toUnsigned) CVC4::BitVectorRotateLeft::operator unsigned() const;
+%rename(toUnsigned) CVC4::BitVectorRotateRight::operator unsigned() const;
+
+%ignore CVC4::operator<<(std::ostream&, const BitVector&);
+%ignore CVC4::operator<<(std::ostream&, const BitVectorExtract&);
+
+%include "util/bitvector.h"
diff --git a/src/util/bool.i b/src/util/bool.i
new file mode 100644
index 000000000..39c1c35d4
--- /dev/null
+++ b/src/util/bool.i
@@ -0,0 +1,5 @@
+%{
+#include "util/bool.h"
+%}
+
+%include "util/bool.h"
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 6985ae38e..e08f09bb6 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -22,11 +22,6 @@
 #ifndef __CVC4__CARDINALITY_H
 #define __CVC4__CARDINALITY_H
 
-#if SWIG
-%include "util/integer.h"
-%include "util/Assert.h"
-#endif /* SWIG */
-
 #include <iostream>
 #include <utility>
 
diff --git a/src/util/cardinality.i b/src/util/cardinality.i
new file mode 100644
index 000000000..760f746c0
--- /dev/null
+++ b/src/util/cardinality.i
@@ -0,0 +1,23 @@
+%{
+#include "util/cardinality.h"
+%}
+
+%feature("valuewrapper") CVC4::Cardinality::Beth;
+
+%rename(plusAssign) CVC4::Cardinality::operator+=(const Cardinality&);
+%rename(timesAssign) CVC4::Cardinality::operator*=(const Cardinality&);
+%rename(powerAssign) CVC4::Cardinality::operator^=(const Cardinality&);
+%rename(plus) CVC4::Cardinality::operator+(const Cardinality&) const;
+%rename(times) CVC4::Cardinality::operator*(const Cardinality&) const;
+%rename(power) CVC4::Cardinality::operator^(const Cardinality&) const;
+%rename(equals) CVC4::Cardinality::operator==(const Cardinality&) const;
+%ignore CVC4::Cardinality::operator!=(const Cardinality&) const;
+%rename(less) CVC4::Cardinality::operator<(const Cardinality&) const;
+%rename(lessEqual) CVC4::Cardinality::operator<=(const Cardinality&) const;
+%rename(greater) CVC4::Cardinality::operator>(const Cardinality&) const;
+%rename(greaterEqual) CVC4::Cardinality::operator>=(const Cardinality&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const Cardinality&);
+%ignore CVC4::operator<<(std::ostream&, Cardinality::Beth);
+
+%include "util/cardinality.h"
diff --git a/src/util/configuration.i b/src/util/configuration.i
new file mode 100644
index 000000000..17c1b974b
--- /dev/null
+++ b/src/util/configuration.i
@@ -0,0 +1,5 @@
+%{
+#include "util/configuration.h"
+%}
+
+%include "util/configuration.h"
diff --git a/src/util/datatype.i b/src/util/datatype.i
new file mode 100644
index 000000000..802f227eb
--- /dev/null
+++ b/src/util/datatype.i
@@ -0,0 +1,22 @@
+%{
+#include "util/datatype.h"
+%}
+
+%rename(equals) CVC4::Datatype::operator==(const Datatype&) const;
+%ignore CVC4::Datatype::operator!=(const Datatype&) const;
+
+%rename(beginConst) CVC4::Datatype::begin() const;
+%rename(endConst) CVC4::Datatype::end() const;
+
+%rename(getConstructor) CVC4::Datatype::operator[](size_t) const;
+
+%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const;
+%ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const;
+%rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor&) const;
+%ignore CVC4::DatatypeHashFunction::operator()(const Datatype::Constructor*) const;
+
+%ignore CVC4::operator<<(std::ostream&, const Datatype&);
+%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor&);
+%ignore CVC4::operator<<(std::ostream&, const Datatype::Constructor::Arg&);
+
+%include "util/datatype.h"
diff --git a/src/util/exception.h b/src/util/exception.h
index 1b1eb224e..43a0354ca 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -30,16 +30,20 @@ namespace CVC4 {
 class CVC4_PUBLIC Exception {
 protected:
   std::string d_msg;
+
 public:
   // Constructors
   Exception() : d_msg("Unknown exception") {}
   Exception(const std::string& msg) : d_msg(msg) {}
   Exception(const char* msg) : d_msg(msg) {}
+
   // Destructor
   virtual ~Exception() throw() {}
+
   // NON-VIRTUAL METHOD for setting and printing the error message
   void setMessage(const std::string& msg) { d_msg = msg; }
   std::string getMessage() const { return d_msg; }
+
   /**
    * Get this exception as a string.  Note that
    *   cout << ex.toString();
@@ -57,16 +61,17 @@ public:
     toStream(ss);
     return ss.str();
   }
+
   /**
    * Printing: feel free to redefine toStream().  When overridden in
    * a derived class, it's recommended that this method print the
    * type of exception before the actual message.
    */
   virtual void toStream(std::ostream& os) const { os << d_msg; }
-  // No need to overload operator<< for the inherited classes
-  friend std::ostream& operator<<(std::ostream& os, const Exception& e);
+
 };/* class Exception */
 
+inline std::ostream& operator<<(std::ostream& os, const Exception& e) CVC4_PUBLIC;
 inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
   e.toStream(os);
   return os;
diff --git a/src/util/exception.i b/src/util/exception.i
new file mode 100644
index 000000000..d3ff896d2
--- /dev/null
+++ b/src/util/exception.i
@@ -0,0 +1,7 @@
+%{
+#include "util/exception.h"
+%}
+
+%ignore CVC4::operator<<(std::ostream&, const Exception&);
+
+%include "util/exception.h"
diff --git a/src/util/hash.h b/src/util/hash.h
index 10211970f..bd3fee597 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -22,6 +22,9 @@
 #ifndef __CVC4__HASH_H
 #define __CVC4__HASH_H
 
+// in case it's not been declared as a namespace yet
+namespace __gnu_cxx {}
+
 #include <ext/hash_map>
 namespace std { using namespace __gnu_cxx; }
 
diff --git a/src/util/hash.i b/src/util/hash.i
new file mode 100644
index 000000000..f2f1e6652
--- /dev/null
+++ b/src/util/hash.i
@@ -0,0 +1,5 @@
+%{
+#include "util/hash.h"
+%}
+
+%include "util/hash.h"
diff --git a/src/util/integer.h.in b/src/util/integer.h.in
index b2973081d..b62feb512 100644
--- a/src/util/integer.h.in
+++ b/src/util/integer.h.in
@@ -26,14 +26,8 @@
 
 #ifdef CVC4_CLN_IMP
 #  include "util/integer_cln_imp.h"
-#  if SWIG
-     %include "util/integer_cln_imp.h"
-#  endif /* SWIG */
 #endif /* CVC4_CLN_IMP */
 
 #ifdef CVC4_GMP_IMP
 #  include "util/integer_gmp_imp.h"
-#  if SWIG
-     %include "util/integer_gmp_imp.h"
-#  endif /* SWIG */
 #endif /* CVC4_GMP_IMP */
diff --git a/src/util/integer.i b/src/util/integer.i
new file mode 100644
index 000000000..4aaa532a7
--- /dev/null
+++ b/src/util/integer.i
@@ -0,0 +1,29 @@
+%{
+#include "util/integer.h"
+%}
+
+%ignore CVC4::Integer::Integer(int);
+%ignore CVC4::Integer::Integer(unsigned int);
+
+%rename(assign) CVC4::Integer::operator=(const Integer&);
+%rename(equals) CVC4::Integer::operator==(const Integer&) const;
+%ignore CVC4::Integer::operator!=(const Integer&) const;
+%rename(plus) CVC4::Integer::operator+(const Integer&) const;
+%rename(minus) CVC4::Integer::operator-() const;
+%rename(minus) CVC4::Integer::operator-(const Integer&) const;
+%rename(times) CVC4::Integer::operator*(const Integer&) const;
+%rename(dividedBy) CVC4::Integer::operator/(const Integer&) const;
+%rename(modulo) CVC4::Integer::operator%(const Integer&) const;
+%rename(plusAssign) CVC4::Integer::operator+=(const Integer&);
+%rename(minusAssign) CVC4::Integer::operator-=(const Integer&);
+%rename(timesAssign) CVC4::Integer::operator*=(const Integer&);
+%rename(dividedByAssign) CVC4::Integer::operator/=(const Integer&);
+%rename(moduloAssign) CVC4::Integer::operator%=(const Integer&);
+%rename(less) CVC4::Integer::operator<(const Integer&) const;
+%rename(lessEqual) CVC4::Integer::operator<=(const Integer&) const;
+%rename(greater) CVC4::Integer::operator>(const Integer&) const;
+%rename(greaterEqual) CVC4::Integer::operator>=(const Integer&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const Integer&);
+
+%include "util/integer.h"
diff --git a/src/util/language.i b/src/util/language.i
new file mode 100644
index 000000000..cd261a73c
--- /dev/null
+++ b/src/util/language.i
@@ -0,0 +1,10 @@
+%{
+#include "util/language.h"
+%}
+
+%import "util/language.h"
+
+%ignore CVC4::operator<<(std::ostream&, CVC4::language::input::Language);
+%ignore CVC4::operator<<(std::ostream&, CVC4::language::output::Language);
+
+%include "util/language.h"
diff --git a/src/util/matcher.h b/src/util/matcher.h
index 6daceb8fd..871fe528f 100644
--- a/src/util/matcher.h
+++ b/src/util/matcher.h
@@ -16,7 +16,7 @@
  ** A class representing a type matcher.
  **/
 
-#include "cvc4_public.h"
+#include "cvc4_private.h"
 
 #ifndef __CVC4__MATCHER_H
 #define __CVC4__MATCHER_H
diff --git a/src/util/options.i b/src/util/options.i
new file mode 100644
index 000000000..ad4815a33
--- /dev/null
+++ b/src/util/options.i
@@ -0,0 +1,9 @@
+%{
+#include "util/options.h"
+%}
+
+%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.h b/src/util/output.h
index e096ff028..da1efe68a 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -23,6 +23,7 @@
 
 #include <ios>
 #include <iostream>
+#include <streambuf>
 #include <string>
 #include <cstdio>
 #include <cstdarg>
@@ -71,6 +72,9 @@ class CVC4_PUBLIC CVC4ostream {
   /** The endl manipulator (why do we need to keep this?) */
   std::ostream& (*const d_endl)(std::ostream&);
 
+  // do not allow use
+  CVC4ostream& operator=(const CVC4ostream&);
+
 public:
   CVC4ostream() :
     d_os(NULL),
diff --git a/src/util/output.i b/src/util/output.i
new file mode 100644
index 000000000..c2729203a
--- /dev/null
+++ b/src/util/output.i
@@ -0,0 +1,10 @@
+%{
+#include "util/output.h"
+%}
+
+%import "util/output.h"
+
+%feature("valuewrapper") CVC4::null_streambuf;
+%feature("valuewrapper") std::ostream;
+
+%include "util/output.h"
diff --git a/src/util/pseudoboolean.i b/src/util/pseudoboolean.i
new file mode 100644
index 000000000..2505a7c1e
--- /dev/null
+++ b/src/util/pseudoboolean.i
@@ -0,0 +1,11 @@
+%{
+#include "util/pseudoboolean.h"
+%}
+
+%rename(toBool) CVC4::Pseudoboolean::operator bool() const;
+%rename(toInt) CVC4::Pseudoboolean::operator int() const;
+%rename(toInteger) CVC4::Pseudoboolean::operator Integer() const;
+
+%ignore CVC4::operator<<(std::ostream&, CVC4::Pseudoboolean);
+
+%include "util/pseudoboolean.h"
diff --git a/src/util/rational.h.in b/src/util/rational.h.in
index 17c1e31fc..13cdb059b 100644
--- a/src/util/rational.h.in
+++ b/src/util/rational.h.in
@@ -26,14 +26,8 @@
 
 #ifdef CVC4_CLN_IMP
 #  include "util/rational_cln_imp.h"
-#  if SWIG
-     %include "util/rational_cln_imp.h"
-#  endif /* SWIG */
 #endif /* CVC4_CLN_IMP */
 
 #ifdef CVC4_GMP_IMP
 #  include "util/rational_gmp_imp.h"
-#  if SWIG
-     %include "util/rational_gmp_imp.h"
-#  endif /* SWIG */
 #endif /* CVC4_GMP_IMP */
diff --git a/src/util/rational.i b/src/util/rational.i
new file mode 100644
index 000000000..512d3ea50
--- /dev/null
+++ b/src/util/rational.i
@@ -0,0 +1,29 @@
+%{
+#include "util/rational.h"
+%}
+
+%ignore CVC4::Rational::Rational(int);
+%ignore CVC4::Rational::Rational(unsigned int);
+%ignore CVC4::Rational::Rational(int, int);
+%ignore CVC4::Rational::Rational(unsigned int, unsigned int);
+
+%rename(assign) CVC4::Rational::operator=(const Rational&);
+%rename(equals) CVC4::Rational::operator==(const Rational&) const;
+%ignore CVC4::Rational::operator!=(const Rational&) const;
+%rename(plus) CVC4::Rational::operator+(const Rational&) const;
+%rename(minus) CVC4::Rational::operator-() const;
+%rename(minus) CVC4::Rational::operator-(const Rational&) const;
+%rename(times) CVC4::Rational::operator*(const Rational&) const;
+%rename(dividedBy) CVC4::Rational::operator/(const Rational&) const;
+%rename(plusAssign) CVC4::Rational::operator+=(const Rational&);
+%rename(minusAssign) CVC4::Rational::operator-=(const Rational&);
+%rename(timesAssign) CVC4::Rational::operator*=(const Rational&);
+%rename(dividedByAssign) CVC4::Rational::operator/=(const Rational&);
+%rename(less) CVC4::Rational::operator<(const Rational&) const;
+%rename(lessEqual) CVC4::Rational::operator<=(const Rational&) const;
+%rename(greater) CVC4::Rational::operator>(const Rational&) const;
+%rename(greaterEqual) CVC4::Rational::operator>=(const Rational&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const Rational&);
+
+%include "util/rational.h"
diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h
index a883500f9..2f2c14ed8 100644
--- a/src/util/rational_cln_imp.h
+++ b/src/util/rational_cln_imp.h
@@ -258,6 +258,11 @@ public:
     return (*this);
   }
 
+  Rational& operator/=(const Rational& y){
+    d_value /= y.d_value;
+    return (*this);
+  }
+
   /** Returns a string representing the rational in the given base. */
   std::string toString(int base = 10) const {
     std::stringstream ss;
diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h
index b97965169..37c3c8364 100644
--- a/src/util/rational_gmp_imp.h
+++ b/src/util/rational_gmp_imp.h
@@ -239,6 +239,11 @@ public:
     return (*this);
   }
 
+  Rational& operator/=(const Rational& y){
+    d_value /= y.d_value;
+    return (*this);
+  }
+
   /** Returns a string representing the rational in the given base. */
   std::string toString(int base = 10) const {
     return d_value.get_str(base);
diff --git a/src/util/result.i b/src/util/result.i
new file mode 100644
index 000000000..c0d86b30a
--- /dev/null
+++ b/src/util/result.i
@@ -0,0 +1,14 @@
+%{
+#include "util/result.h"
+%}
+
+%ignore CVC4::operator<<(std::ostream&, const Result& r);
+
+%rename(equals) CVC4::Result::operator==(const Result& r) const;
+%ignore CVC4::Result::operator!=(const Result& r) const;
+
+%ignore CVC4::operator<<(std::ostream&, enum Result::Sat);
+%ignore CVC4::operator<<(std::ostream&, enum Result::Validity);
+%ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation);
+
+%include "util/result.h"
diff --git a/src/util/sexpr.i b/src/util/sexpr.i
new file mode 100644
index 000000000..c925f9f95
--- /dev/null
+++ b/src/util/sexpr.i
@@ -0,0 +1,7 @@
+%{
+#include "util/sexpr.h"
+%}
+
+%ignore CVC4::operator<<(std::ostream&, const SExpr&);
+
+%include "util/sexpr.h"
diff --git a/src/util/stats.i b/src/util/stats.i
new file mode 100644
index 000000000..48828cb7e
--- /dev/null
+++ b/src/util/stats.i
@@ -0,0 +1,21 @@
+%{
+#include "util/stats.h"
+%}
+
+%ignore CVC4::operator<<(std::ostream&, const ::timespec&);
+
+%rename(increment) CVC4::IntStat::operator++();
+%rename(plusAssign) CVC4::IntStat::operator+=(int64_t);
+
+%rename(plusAssign) CVC4::operator+=(::timespec&, const ::timespec&);
+%rename(minusAssign) CVC4::operator-=(::timespec&, const ::timespec&);
+%rename(plus) CVC4::operator+(const ::timespec&, const ::timespec&);
+%rename(minus) CVC4::operator-(const ::timespec&, const ::timespec&);
+%rename(equals) CVC4::operator==(const ::timespec&, const ::timespec&);
+%ignore CVC4::operator!=(const ::timespec&, const ::timespec&);
+%rename(less) CVC4::operator<(const ::timespec&, const ::timespec&);
+%rename(lessEqual) CVC4::operator<=(const ::timespec&, const ::timespec&);
+%rename(greater) CVC4::operator>(const ::timespec&, const ::timespec&);
+%rename(greaterEqual) CVC4::operator>=(const ::timespec&, const ::timespec&);
+
+%include "util/stats.h"
diff --git a/src/util/subrange_bound.i b/src/util/subrange_bound.i
new file mode 100644
index 000000000..6b02414ab
--- /dev/null
+++ b/src/util/subrange_bound.i
@@ -0,0 +1,10 @@
+%{
+#include "util/subrange_bound.h"
+%}
+
+%rename(equals) CVC4::SubrangeBound::operator==(const SubrangeBound&) const;
+%ignore CVC4::SubrangeBound::operator!=(const SubrangeBound&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const SubrangeBound&);
+
+%include "util/subrange_bound.h"