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

30 files changed, 312 insertions, 21 deletions

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"