* 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.)

16 files changed, 57 insertions, 13 deletions

diff --git a/configure.ac b/configure.ac
index 940ad43d4..682f0de7c 100644
--- a/configure.ac
+++ b/configure.ac
@@ -743,7 +743,13 @@ AC_SUBST([CVC4_NEED_INT64_T_OVERLOADS])
 AC_PROG_ANTLR
 
 CVC4_CXX_OPTION([-Wno-conversion-null], [WNO_CONVERSION_NULL])
+CVC4_CXX_OPTION([-Wno-uninitialized], [WNO_UNINITIALIZED])
+CVC4_CXX_OPTION([-Wno-unused-variable], [WNO_UNUSED_VARIABLE])
+CVC4_CXX_OPTION([-fno-strict-aliasing], [FNO_STRICT_ALIASING])
 AC_SUBST([WNO_CONVERSION_NULL])
+AC_SUBST([WNO_UNINITIALIZED])
+AC_SUBST([WNO_UNUSED_VARIABLE])
+AC_SUBST([FNO_STRICT_ALIASING])
 
 # Doxygen configuration
 AC_ARG_ENABLE([internals-documentation],
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index 68a65b2c9..a747a3812 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -141,7 +141,7 @@ endif
 endif
 
 nodist_java_libcvc4jni_la_SOURCES = java.cpp
-java_libcvc4jni_la_CXXFLAGS = -fno-strict-aliasing
+java_libcvc4jni_la_CXXFLAGS = @FNO_STRICT_ALIASING@ @WNO_UNUSED_VARIABLE@ @WNO_UNINITIALIZED@
 nodist_csharp_CVC4_la_SOURCES = csharp.cpp
 nodist_perl_CVC4_la_SOURCES = perl.cpp
 nodist_php_CVC4_la_SOURCES = php.cpp
@@ -168,7 +168,7 @@ MOSTLYCLEANFILES = \
 	CVC4.jar
 
 java_libcvc4jni_la-java.lo java.lo: java.cpp
-	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) -o $@ $<
+	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) $(java_libcvc4jni_la_CXXFLAGS) -o $@ $<
 CVC4.jar: java.cpp
 	$(AM_V_GEN) \
 	(cd java; \
diff --git a/src/cvc4.i b/src/cvc4.i
index ee760c569..53444539a 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -111,6 +111,7 @@ using namespace CVC4;
 %}
 
 %typemap(throws) ModalException = Exception;
+%typemap(throws) LogicException = Exception;
 %typemap(throws) OptionException = Exception;
 %typemap(throws) IllegalArgumentException = Exception;
 %typemap(throws) AssertionException = Exception;
@@ -124,7 +125,7 @@ using namespace CVC4;
 
 // Generate an error if the mapping from C++ CVC4 Exception to Java CVC4 Exception doesn't exist above
 %typemap(throws) SWIGTYPE, SWIGTYPE &, SWIGTYPE *, SWIGTYPE [], SWIGTYPE [ANY] %{
-#error "exception $1_type doesn't map to Java correctly"
+#error "exception $1_type doesn't map to Java correctly---please edit src/cvc4.i and add it"
 %}
 
 %include "java/typemaps.i" // primitive pointers and references
@@ -151,7 +152,6 @@ using namespace CVC4;
 %include "util/array.i"
 %include "util/array_store_all.i"
 %include "util/hash.i"
-%include "util/util_model.i"
 
 %include "expr/type.i"
 %include "util/ascription_type.i"
diff --git a/src/expr/command.h b/src/expr/command.h
index b0a7ddb36..342aec5ff 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -320,6 +320,7 @@ protected:
 public:
   DeclarationDefinitionCommand(const std::string& id) throw();
   ~DeclarationDefinitionCommand() throw() {}
+  virtual void invoke(SmtEngine* smtEngine) throw() = 0;
   std::string getSymbol() const throw();
 };/* class DeclarationDefinitionCommand */
 
diff --git a/src/expr/type.i b/src/expr/type.i
index 0646ec8cd..870cb228c 100644
--- a/src/expr/type.i
+++ b/src/expr/type.i
@@ -21,6 +21,7 @@
 %rename(toBitVectorType) CVC4::Type::operator BitVectorType() const;
 %rename(toFunctionType) CVC4::Type::operator FunctionType() const;
 %rename(toTupleType) CVC4::Type::operator TupleType() const;
+%rename(toSExprType) CVC4::Type::operator SExprType() const;
 %rename(toArrayType) CVC4::Type::operator ArrayType() const;
 %rename(toDatatypeType) CVC4::Type::operator DatatypeType() const;
 %rename(toConstructorType) CVC4::Type::operator ConstructorType() const;
@@ -28,7 +29,8 @@
 %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;
+%rename(toPredicateSubtype) CVC4::Type::operator PredicateSubtype() const;
+%rename(toSubrangeType) CVC4::Type::operator SubrangeType() const;
 
 namespace CVC4 {
   namespace expr {
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&);