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

diff --git a/configure.ac b/configure.ac
index 940ad43d4864604a9f05c31ffb525ee4f904e805..682f0de7c6e9419dea75b02d0daa93f6fd863da8 100644 (file)
--- 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 68a65b2c93d2731c9aa61027aafb19b0dff7d45b..a747a38128f75a4ce2266ccfdcb8928a4bd8e3e3 100644 (file)
--- 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 ee760c5694eeaec4e227173bfa96846a2048ef4c..53444539a3d5d5201c522e097b630e7fd627c394 100644 (file)
--- 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 b0a7ddb360793eab25edeef3fd51fa4ebbfbdbab..342aec5fff017666f091772ef8d7f742b4eb7342 100644 (file)
--- 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 0646ec8cd363a2ce971c6eadec58f9e7188f29d9..870cb228c7539d4db42c90bb8667aff615c8e4a4 100644 (file)
--- 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 aa122905b52b9ed9f7c8e2b0fb16421413b705fe..f3ae43b05ffe9414aa019e59e164fc65d1d940a0 100644 (file)
--- 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 afc14d08949339432824a54944c19a04753152b0..5e8fd71408d1562d17249cccf2a82c4b105f2ddd 100644 (file)
--- 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 9438113cf7f59645b897b248bf2b3ae3b0c20587..bb0099157186c5a33705656ebc3dfd4c88a2c031 100644 (file)
--- 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 085a59b2dcc24bc57240afc489d3b93a6c9d1de7..220e284b3335e7be5a27037bbac1fc914fc381a4 100644 (file)
--- 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 39c1c35d45b8bbe53914b3ced6ca73b876e37586..47a0c42172e8ee07d578ec1557b0d0ad91163ac1 100644 (file)
--- 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 068a338b4462f3cbaaf0bedc8c65073e2c69ffe2..c07caa8057ae06a43e07dc87208227c3ee555264 100644 (file)
--- 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 bad6b196fcafcc34ff6c82db196ab6f89415bf14..c8d2f7bdff5fcfe7b678a966ce640a6575789c2e 100644 (file)
--- 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 135302c66846b1ab342eaaa2a46a5517145361c0..a65c783275e7fd20be9e206dd8811acbf5561812 100644 (file)
--- 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 dba8a0f2921c1f75a811a081aae1a8b7352b29b6..5d78142f3e676878d2b45366c10192d66871e7d9 100644 (file)
--- 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 7cc737d6ccc46cd9635343404762718052030fc9..a14fc29dd9e851799c2e5cf90237207029a7fc3d 100644 (file)
--- 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 6b02414ab84da94bef122fab4af8b3b75749b4ae..c619b5e3106b673af420403052e1ca2ab7ed0cde 100644 (file)
--- 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&);