interface cleanup, java bindings work

6 files changed, 56 insertions, 26 deletions

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;
   }