interface cleanup, java bindings work

11 files changed, 102 insertions, 37 deletions

diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index 31ad8c71f..c0c7f352e 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -81,7 +81,7 @@ 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@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -package edu.nyu.acsys.CVC4 -o $@ $<
+	$(AM_V_GEN)$(SWIG) -Wall -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@/.. -c++ -MM -o $(patsubst %.d,%.cpp,$@) $<
diff --git a/src/cvc4.i b/src/cvc4.i
index 03c258778..7f7926bfd 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -1,14 +1,45 @@
 %import "bindings/swig.h"
+%include "stdint.i"
+%include "stl.i"
 
 %module CVC4
 // nspace completely broken with Java packaging
 //%nspace;
 
+namespace std {
+  class istream;
+  class ostream;
+  template <class T> class set {};
+  template <class K, class V, class H> class hash_map {};
+}
+
 %{
-namespace CVC4 { class Exception; }
+namespace CVC4 {}
 using namespace CVC4;
+
+#include <iostream>
+#include <vector>
+#include <set>
+#include <string>
+#include <ext/hash_map>
+
+#include "util/sexpr.h"
+#include "util/exception.h"
+#include "expr/type.h"
+#include "expr/expr.h"
+#include "util/datatype.h"
+#include "expr/command.h"
 %}
 
+%template(vectorCommandPtr) std::vector< CVC4::Command* >;
+%template(vectorType) std::vector< CVC4::Type >;
+%template(vectorExpr) std::vector< CVC4::Expr >;
+%template(vectorDatatypeType) std::vector< CVC4::DatatypeType >;
+%template(vectorSExpr) std::vector< CVC4::SExpr >;
+%template(vectorString) std::vector< std::string >;
+%template(setType) std::set< CVC4::Type >;
+%template(hashmapExpr) std::hash_map< CVC4::Expr, CVC4::Expr, CVC4::ExprHashFunction >;
+
 %exception {
   try {
     $action
@@ -38,7 +69,6 @@ using namespace CVC4;
 %include "util/cardinality.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"
@@ -46,16 +76,19 @@ using namespace CVC4;
 %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 "util/ascription_type.i"
+%include "util/datatype.i"
+
+%include "expr/kind.i"
 %include "expr/expr.i"
+%include "expr/command.i"
+%include "expr/declaration_scope.i"
 %include "expr/expr_manager.i"
+%include "expr/expr_stream.i"
 
 %include "smt/smt_engine.i"
 %include "smt/bad_option_exception.i"
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am
index 03de15706..14fee33c9 100644
--- a/src/expr/Makefile.am
+++ b/src/expr/Makefile.am
@@ -53,6 +53,7 @@ EXTRA_DIST = \
 	mkkind \
 	mkmetakind \
 	mkexpr \
+	expr_stream.i \
 	expr_manager.i \
 	declaration_scope.i \
 	command.i \
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h
index 2828ae381..77b92c873 100644
--- a/src/expr/expr_manager_template.h
+++ b/src/expr/expr_manager_template.h
@@ -376,10 +376,6 @@ public:
   /** Make a new sort with the given name. */
   SortType mkSort(const std::string& name) const;
 
-  /** Make a new sort from a constructor. */
-  SortType mkSort(SortConstructorType constructor,
-                  const std::vector<TypeNode>& children) const;
-
   /** Make a sort constructor from a name and arity. */
   SortConstructorType mkSortConstructor(const std::string& name,
                                         size_t arity) const;
diff --git a/src/expr/expr_stream.i b/src/expr/expr_stream.i
new file mode 100644
index 000000000..f1144623b
--- /dev/null
+++ b/src/expr/expr_stream.i
@@ -0,0 +1,5 @@
+%{
+#include "expr/expr_stream.h"
+%}
+
+%include "expr/expr_stream.h"
diff --git a/src/util/ascription_type.i b/src/util/ascription_type.i
index b0b57d5f9..d0b435a4d 100644
--- a/src/util/ascription_type.i
+++ b/src/util/ascription_type.i
@@ -2,7 +2,6 @@
 #include "util/ascription_type.h"
 %}
 
-
 %rename(equals) CVC4::AscriptionType::operator==(const AscriptionType&) const;
 %ignore CVC4::AscriptionType::operator!=(const AscriptionType&) const;
 
diff --git a/src/util/datatype.h b/src/util/datatype.h
index c64f420dd..148d85870 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -326,9 +326,9 @@ public:
   };/* class Datatype::Constructor */
 
   /** The type for iterators over constructors. */
-  typedef std::vector<Constructor>::iterator iterator;
+  typedef typename std::vector<Constructor>::iterator iterator;
   /** The (const) type for iterators over constructors. */
-  typedef std::vector<Constructor>::const_iterator const_iterator;
+  typedef typename std::vector<Constructor>::const_iterator const_iterator;
 
 private:
   std::string d_name;
@@ -448,13 +448,13 @@ public:
   inline bool isResolved() const throw();
 
   /** Get the beginning iterator over Constructors. */
-  inline iterator begin() throw();
+  inline std::vector<Constructor>::iterator begin() throw();
   /** Get the ending iterator over Constructors. */
-  inline iterator end() throw();
+  inline std::vector<Constructor>::iterator end() throw();
   /** Get the beginning const_iterator over Constructors. */
-  inline const_iterator begin() const throw();
+  inline std::vector<Constructor>::const_iterator begin() const throw();
   /** Get the ending const_iterator over Constructors. */
-  inline const_iterator end() const throw();
+  inline std::vector<Constructor>::const_iterator end() const throw();
 
   /** Get the ith Constructor. */
   const Constructor& operator[](size_t index) const;
diff --git a/src/util/datatype.i b/src/util/datatype.i
index 802f227eb..f306d7682 100644
--- a/src/util/datatype.i
+++ b/src/util/datatype.i
@@ -1,7 +1,25 @@
 %{
 #include "util/datatype.h"
+namespace CVC4 {
+//typedef CVC4::Datatype::Constructor DatatypeConstructor;
+}
 %}
 
+namespace CVC4 {
+%rename(DatatypeConstructor) CVC4::Datatype::Constructor;
+//%rename(DatatypeConstructor) CVC4::Constructor;
+}
+
+%extend std::vector< CVC4::Datatype > {
+  %ignore vector(size_type);
+};
+%template(vectorDatatype) std::vector< CVC4::Datatype >;
+
+%extend std::vector< CVC4::Datatype::Constructor > {
+  %ignore vector(size_type);
+};
+%template(vectorDatatypeConstructor) std::vector< CVC4::Datatype::Constructor >;
+
 %rename(equals) CVC4::Datatype::operator==(const Datatype&) const;
 %ignore CVC4::Datatype::operator!=(const Datatype&) const;
 
@@ -19,4 +37,5 @@
 %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/integer.h.in b/src/util/integer.h.in
index b62feb512..b2973081d 100644
--- a/src/util/integer.h.in
+++ b/src/util/integer.h.in
@@ -26,8 +26,14 @@
 
 #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/rational.h.in b/src/util/rational.h.in
index 13cdb059b..17c1e31fc 100644
--- a/src/util/rational.h.in
+++ b/src/util/rational.h.in
@@ -26,8 +26,14 @@
 
 #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/stats.h b/src/util/stats.h
index 42cd73c3d..3a2847512 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -45,7 +45,7 @@ class ExprManager;
 
 class CVC4_PUBLIC Stat;
 
-inline std::ostream& operator<<(std::ostream& os, const ::timespec& t);
+inline std::ostream& operator<<(std::ostream& os, const timespec& t);
 
 /**
  * The main statistics registry.  This registry maintains the list of
@@ -546,11 +546,11 @@ public:
 };/* class ListStat */
 
 /****************************************************************************/
-/* Some utility functions for ::timespec                                    */
+/* Some utility functions for timespec                                    */
 /****************************************************************************/
 
 /** Compute the sum of two timespecs. */
-inline ::timespec& operator+=(::timespec& a, const ::timespec& b) {
+inline timespec& operator+=(timespec& a, const timespec& b) {
   // assumes a.tv_nsec and b.tv_nsec are in range
   const long nsec_per_sec = 1000000000L; // one thousand million
   Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec);
@@ -572,7 +572,7 @@ inline ::timespec& operator+=(::timespec& a, const ::timespec& b) {
 }
 
 /** Compute the difference of two timespecs. */
-inline ::timespec& operator-=(::timespec& a, const ::timespec& b) {
+inline timespec& operator-=(timespec& a, const timespec& b) {
   // assumes a.tv_nsec and b.tv_nsec are in range
   const long nsec_per_sec = 1000000000L; // one thousand million
   Assert(a.tv_nsec >= 0 && a.tv_nsec < nsec_per_sec);
@@ -593,57 +593,57 @@ inline ::timespec& operator-=(::timespec& a, const ::timespec& b) {
 }
 
 /** Add two timespecs. */
-inline ::timespec operator+(const ::timespec& a, const ::timespec& b) {
-  ::timespec result = a;
+inline timespec operator+(const timespec& a, const timespec& b) {
+  timespec result = a;
   return result += b;
 }
 
 /** Subtract two timespecs. */
-inline ::timespec operator-(const ::timespec& a, const ::timespec& b) {
-  ::timespec result = a;
+inline timespec operator-(const timespec& a, const timespec& b) {
+  timespec result = a;
   return result -= b;
 }
 
 /** Compare two timespecs for equality. */
-inline bool operator==(const ::timespec& a, const ::timespec& b) {
+inline bool operator==(const timespec& a, const timespec& b) {
   // assumes a.tv_nsec and b.tv_nsec are in range
   return a.tv_sec == b.tv_sec && a.tv_nsec == b.tv_nsec;
 }
 
 /** Compare two timespecs for disequality. */
-inline bool operator!=(const ::timespec& a, const ::timespec& b) {
+inline bool operator!=(const timespec& a, const timespec& b) {
   // assumes a.tv_nsec and b.tv_nsec are in range
   return !(a == b);
 }
 
 /** Compare two timespecs, returning true iff a < b. */
-inline bool operator<(const ::timespec& a, const ::timespec& b) {
+inline bool operator<(const timespec& a, const timespec& b) {
   // assumes a.tv_nsec and b.tv_nsec are in range
   return a.tv_sec < b.tv_sec ||
     (a.tv_sec == b.tv_sec && a.tv_nsec < b.tv_nsec);
 }
 
 /** Compare two timespecs, returning true iff a > b. */
-inline bool operator>(const ::timespec& a, const ::timespec& b) {
+inline bool operator>(const timespec& a, const timespec& b) {
   // assumes a.tv_nsec and b.tv_nsec are in range
   return a.tv_sec > b.tv_sec ||
     (a.tv_sec == b.tv_sec && a.tv_nsec > b.tv_nsec);
 }
 
 /** Compare two timespecs, returning true iff a <= b. */
-inline bool operator<=(const ::timespec& a, const ::timespec& b) {
+inline bool operator<=(const timespec& a, const timespec& b) {
   // assumes a.tv_nsec and b.tv_nsec are in range
   return !(a > b);
 }
 
 /** Compare two timespecs, returning true iff a >= b. */
-inline bool operator>=(const ::timespec& a, const ::timespec& b) {
+inline bool operator>=(const timespec& a, const timespec& b) {
   // assumes a.tv_nsec and b.tv_nsec are in range
   return !(a < b);
 }
 
 /** Output a timespec on an output stream. */
-inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) {
+inline std::ostream& operator<<(std::ostream& os, const timespec& t) {
   // assumes t.tv_nsec is in range
   return os << t.tv_sec << "."
             << std::setfill('0') << std::setw(8) << std::right << t.tv_nsec;
@@ -655,11 +655,11 @@ inline std::ostream& operator<<(std::ostream& os, const ::timespec& t) {
  * arbitrarily, like a stopwatch; the value of the statistic at the
  * end is the accumulated time over all (start,stop) pairs.
  */
-class CVC4_PUBLIC TimerStat : public BackedStat< ::timespec > {
+class CVC4_PUBLIC TimerStat : public BackedStat< timespec > {
 
   // strange: timespec isn't placed in 'std' namespace ?!
   /** The last start time of this timer */
-  ::timespec d_start;
+  timespec d_start;
 
   /** Whether this timer is currently running */
   bool d_running;
@@ -693,9 +693,9 @@ public:
    * timers have a 0.0 value and are not running.
    */
   TimerStat(const std::string& name) :
-    BackedStat< ::timespec >(name, ::timespec()),
+    BackedStat< timespec >(name, timespec()),
     d_running(false) {
-    /* ::timespec is POD and so may not be initialized to zero;
+    /* timespec is POD and so may not be initialized to zero;
      * here, ensure it is */
     d_data.tv_sec = d_data.tv_nsec = 0;
   }