* Fix language bindings: various issues

** remove a number of warnings in bindings generation
** give appropriate names for operator-overloading
** make sure Java language bindings are built with -fno-strict-aliasing, to ensure the optimizer doesn't produce bad code

* Also remove BitVector::equals(), which wasn't used and was inconsistently implemented (operator==() is still there).

(this commit was certified error- and warning-free by the test-and-commit script.)

11 files changed, 43 insertions, 8 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index aa122905b..f3ae43b05 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -141,8 +141,7 @@ EXTRA_DIST = \
 	array_store_all.i \
 	ascription_type.i \
 	rational.i \
-	hash.i \
-	util_model.i
+	hash.i
 
 DISTCLEANFILES = \
 	integer.h.tmp \
diff --git a/src/util/array_store_all.i b/src/util/array_store_all.i
index afc14d089..5e8fd7140 100644
--- a/src/util/array_store_all.i
+++ b/src/util/array_store_all.i
@@ -2,5 +2,12 @@
 #include "util/array_store_all.h"
 %}
 
+%rename(equals) CVC4::ArrayStoreAll::operator==(const ArrayStoreAll&) const;
+%ignore CVC4::ArrayStoreAll::operator!=(const ArrayStoreAll&) const;
+%rename(less) CVC4::ArrayStoreAll::operator<(const ArrayStoreAll&) const;
+%rename(lessEqual) CVC4::ArrayStoreAll::operator<=(const ArrayStoreAll&) const;
+%rename(greater) CVC4::ArrayStoreAll::operator>(const ArrayStoreAll&) const;
+%rename(greaterEqual) CVC4::ArrayStoreAll::operator>=(const ArrayStoreAll&) const;
+
 %include "expr/type.i"
 %include "util/array_store_all.h"
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index 9438113cf..bb0099157 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -97,11 +97,6 @@ public:
     return d_value != y.d_value;
   }
 
-  BitVector equals(const BitVector& y) const {
-    CheckArgument(d_size == y.d_size, y);
-    return d_value == y.d_value; 
-  }
-
   BitVector concat (const BitVector& other) const {
     return BitVector(d_size + other.d_size, (d_value.multiplyByPow2(other.d_size)) + other.d_value);
   }
diff --git a/src/util/bitvector.i b/src/util/bitvector.i
index 085a59b2d..220e284b3 100644
--- a/src/util/bitvector.i
+++ b/src/util/bitvector.i
@@ -11,9 +11,17 @@
 %rename(minus) CVC4::BitVector::operator-(const BitVector&) const;
 %rename(minus) CVC4::BitVector::operator-() const;
 %rename(times) CVC4::BitVector::operator*(const BitVector&) const;
+%rename(bitXor) CVC4::BitVector::operator^(const BitVector&) const;
+%rename(bitOr) CVC4::BitVector::operator|(const BitVector&) const;
+%rename(bitAnd) CVC4::BitVector::operator&(const BitVector&) const;
 %rename(complement) CVC4::BitVector::operator~() const;
+%rename(less) CVC4::BitVector::operator<(const BitVector&) const;
+%rename(lessEqual) CVC4::BitVector::operator<=(const BitVector&) const;
+%rename(greater) CVC4::BitVector::operator>(const BitVector&) const;
+%rename(greaterEqual) CVC4::BitVector::operator>=(const BitVector&) const;
 
 %rename(equals) CVC4::BitVectorExtract::operator==(const BitVectorExtract&) const;
+%rename(equals) CVC4::BitVectorBitOf::operator==(const BitVectorBitOf&) const;
 
 %rename(toUnsigned) CVC4::BitVectorSize::operator unsigned() const;
 %rename(toUnsigned) CVC4::BitVectorRepeat::operator unsigned() const;
diff --git a/src/util/bool.i b/src/util/bool.i
index 39c1c35d4..47a0c4217 100644
--- a/src/util/bool.i
+++ b/src/util/bool.i
@@ -2,4 +2,6 @@
 #include "util/bool.h"
 %}
 
+%rename(apply) CVC4::BoolHashFunction::operator()(bool) const;
+
 %include "util/bool.h"
diff --git a/src/util/datatype.i b/src/util/datatype.i
index 068a338b4..c07caa805 100644
--- a/src/util/datatype.i
+++ b/src/util/datatype.i
@@ -41,6 +41,7 @@
 %rename(endConst) CVC4::Datatype::end() const;
 
 %rename(getConstructor) CVC4::Datatype::operator[](size_t) const;
+%ignore CVC4::Datatype::operator[](std::string) const;
 
 %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const;
 %ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const;
@@ -51,6 +52,7 @@
 %rename(endConst) CVC4::DatatypeConstructor::end() const;
 
 %rename(getArg) CVC4::DatatypeConstructor::operator[](size_t) const;
+%rename(getArg) CVC4::DatatypeConstructor::operator[](std::string) const;
 
 %ignore CVC4::operator<<(std::ostream&, const Datatype&);
 %ignore CVC4::operator<<(std::ostream&, const DatatypeConstructor&);
diff --git a/src/util/integer.i b/src/util/integer.i
index bad6b196f..c8d2f7bdf 100644
--- a/src/util/integer.i
+++ b/src/util/integer.i
@@ -5,6 +5,7 @@
 %ignore CVC4::Integer::Integer(int);
 %ignore CVC4::Integer::Integer(unsigned int);
 %ignore CVC4::Integer::Integer(const std::string&);
+%ignore CVC4::Integer::Integer(const std::string&, unsigned int);
 
 %rename(assign) CVC4::Integer::operator=(const Integer&);
 %rename(equals) CVC4::Integer::operator==(const Integer&) const;
@@ -25,6 +26,8 @@
 %rename(greater) CVC4::Integer::operator>(const Integer&) const;
 %rename(greaterEqual) CVC4::Integer::operator>=(const Integer&) const;
 
+%rename(apply) CVC4::IntegerHashFunction::operator()(const CVC4::Integer&) const;
+
 %ignore CVC4::operator<<(std::ostream&, const Integer&);
 
 %include "util/integer.h"
diff --git a/src/util/rational.i b/src/util/rational.i
index 135302c66..a65c78327 100644
--- a/src/util/rational.i
+++ b/src/util/rational.i
@@ -7,6 +7,7 @@
 %ignore CVC4::Rational::Rational(int, int);
 %ignore CVC4::Rational::Rational(unsigned int, unsigned int);
 %ignore CVC4::Rational::Rational(const std::string&);
+%ignore CVC4::Rational::Rational(const std::string&, unsigned int);
 
 %rename(assign) CVC4::Rational::operator=(const Rational&);
 %rename(equals) CVC4::Rational::operator==(const Rational&) const;
@@ -25,6 +26,8 @@
 %rename(greater) CVC4::Rational::operator>(const Rational&) const;
 %rename(greaterEqual) CVC4::Rational::operator>=(const Rational&) const;
 
+%rename(apply) CVC4::RationalHashFunction::operator()(const CVC4::Rational&) const;
+
 %ignore CVC4::operator<<(std::ostream&, const Rational&);
 
 %include "util/rational.h"
diff --git a/src/util/sexpr.i b/src/util/sexpr.i
index dba8a0f29..5d78142f3 100644
--- a/src/util/sexpr.i
+++ b/src/util/sexpr.i
@@ -10,4 +10,7 @@
   std::string toString() const { return self->getValue(); }
 };/* CVC4::SExpr */
 
+%rename(equals) CVC4::SExpr::operator==(const SExpr&) const;
+%ignore CVC4::SExpr::operator!=(const SExpr&) const;
+
 %include "util/sexpr.h"
diff --git a/src/util/statistics.i b/src/util/statistics.i
index 7cc737d6c..a14fc29dd 100644
--- a/src/util/statistics.i
+++ b/src/util/statistics.i
@@ -2,5 +2,7 @@
 #include "util/statistics.h"
 %}
 
-%include "util/statistics.h"
+%rename(assign) CVC4::Statistics::operator=(const StatisticsBase&);
+%rename(assign) CVC4::Statistics::operator=(const Statistics& stats);
 
+%include "util/statistics.h"
diff --git a/src/util/subrange_bound.i b/src/util/subrange_bound.i
index 6b02414ab..c619b5e31 100644
--- a/src/util/subrange_bound.i
+++ b/src/util/subrange_bound.i
@@ -4,6 +4,17 @@
 
 %rename(equals) CVC4::SubrangeBound::operator==(const SubrangeBound&) const;
 %ignore CVC4::SubrangeBound::operator!=(const SubrangeBound&) const;
+%rename(less) CVC4::SubrangeBound::operator<(const SubrangeBound&) const;
+%rename(lessEqual) CVC4::SubrangeBound::operator<=(const SubrangeBound&) const;
+%rename(greater) CVC4::SubrangeBound::operator>(const SubrangeBound&) const;
+%rename(greaterEqual) CVC4::SubrangeBound::operator>=(const SubrangeBound&) const;
+
+%rename(equals) CVC4::SubrangeBounds::operator==(const SubrangeBounds&) const;
+%ignore CVC4::SubrangeBounds::operator!=(const SubrangeBounds&) const;
+%rename(less) CVC4::SubrangeBounds::operator<(const SubrangeBounds&) const;
+%rename(lessEqual) CVC4::SubrangeBounds::operator<=(const SubrangeBounds&) const;
+%rename(greater) CVC4::SubrangeBounds::operator>(const SubrangeBounds&) const;
+%rename(greaterEqual) CVC4::SubrangeBounds::operator>=(const SubrangeBounds&) const;
 
 %ignore CVC4::operator<<(std::ostream&, const SubrangeBound&);