From: Morgan Deters Date: Mon, 12 Nov 2012 18:34:32 +0000 (+0000) Subject: * Fix language bindings: various issues X-Git-Tag: cvc5-1.0.0~7617 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1c2c416b953309279c43c86a46b5690642ff95dd;p=cvc5.git * 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 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&);