Java bindings fixes.

diff --git a/src/cvc4.i b/src/cvc4.i
index cd5896ff33c6398821a3c676944d57294571290d..a84d69cf772091f1b2fd51bc88347ca0b3862172 100644 (file)
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -283,9 +283,9 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 
 #endif /* SWIGJAVA */
 
+%include "util/exception.i"
 %include "util/integer.i"
 %include "util/rational.i"
-%include "util/exception.i"
 %include "util/language.i"
 %include "util/cardinality.i"
 %include "util/bool.i"
@@ -303,6 +303,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 
 %include "expr/type.i"
 %include "util/ascription_type.i"
+%include "util/emptyset.i"
 %include "util/datatype.i"
 %include "util/tuple.i"
 %include "util/record.i"

diff --git a/src/expr/kind.i b/src/expr/kind.i
index 95c350cf3abe7c1d4ea89b64bc9bebd047bddb6c..189c94f1f21a4c96bccca2159e586b24d3a298c5 100644 (file)
--- a/src/expr/kind.i
+++ b/src/expr/kind.i
@@ -8,6 +8,9 @@
 
 %ignore CVC4::theory::operator++(TheoryId&);
 
+%rename(apply) CVC4::kind::KindHashFunction::operator()(::CVC4::Kind) const;
+%rename(apply) CVC4::TypeConstantHashFunction::operator()(TypeConstant) const;
+
 %rename(Kind) CVC4::kind::Kind_t;
 
 %include "expr/kind.h"

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 9122f9ddb596e2f0698f1e2f2ded01d1222a4702..5cf5da1e09ed4198e1cca4c1e6516f66dbdf0695 100644 (file)
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -148,6 +148,7 @@ EXTRA_DIST = \
        language.i \
        array.i \
        array_store_all.i \
+       emptyset.i \
        ascription_type.i \
        rational.i \
        hash.i \

diff --git a/src/util/emptyset.i b/src/util/emptyset.i
new file mode 100644 (file)
index 0000000..ce4f3a4
--- /dev/null
+++ b/src/util/emptyset.i
@@ -0,0 +1,17 @@
+%{
+#include "util/emptyset.h"
+%}
+
+%rename(equals) CVC4::EmptySet::operator==(const EmptySet&) const;
+%ignore CVC4::EmptySet::operator!=(const EmptySet&) const;
+
+%rename(less) CVC4::EmptySet::operator<(const EmptySet&) const;
+%rename(lessEqual) CVC4::EmptySet::operator<=(const EmptySet&) const;
+%rename(greater) CVC4::EmptySet::operator>(const EmptySet&) const;
+%rename(greaterEqual) CVC4::EmptySet::operator>=(const EmptySet&) const;
+
+%rename(apply) CVC4::EmptySetHashFunction::operator()(const EmptySet&) const;
+
+%ignore CVC4::operator<<(std::ostream& out, const EmptySet& es);
+
+%include "util/emptyset.h"

diff --git a/src/util/predicate.h b/src/util/predicate.h
index 686e92dc8ffa6afa22fec94741edf067fe8765a6..5fb3f806a0ede59e66ee1a2bc7564be56eb97366 100644 (file)
--- a/src/util/predicate.h
+++ b/src/util/predicate.h
@@ -52,7 +52,7 @@ public:
 
   bool operator==(const Predicate& p) const;
 
-  friend std::ostream& operator<<(std::ostream& out, const Predicate& p);
+  friend std::ostream& CVC4::operator<<(std::ostream& out, const Predicate& p);
   friend size_t PredicateHashFunction::operator()(const Predicate& p) const;
 
 };/* class Predicate */

diff --git a/src/util/predicate.i b/src/util/predicate.i
index f29cd16d528d6b89ebaa58700b302559feaf14fc..eedbb2e83813a471fcf95d65cb42d790c30db0c7 100644 (file)
--- a/src/util/predicate.i
+++ b/src/util/predicate.i
@@ -7,6 +7,6 @@
 
 %rename(apply) CVC4::PredicateHashFunction::operator()(const Predicate&) const;
 
-%ignore CVC4::operator<<(std::ostream& out, const Predicate& p);
+%ignore CVC4::operator<<(std::ostream&, const Predicate&);
 
 %include "util/predicate.h"