From b28a42c3a4fd8c9b079b157ad8ff36e581b60d29 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 27 Nov 2013 17:37:30 -0500
Subject: [PATCH] Java bindings improvements for CASCADE, minor cleanup.

---
 src/cvc4.i           |  1 +
 src/util/Makefile.am |  3 ++-
 src/util/regexp.h    |  9 +++++----
 src/util/regexp.i    | 33 +++++++++++++++++++++++++++++++++
 4 files changed, 41 insertions(+), 5 deletions(-)
 create mode 100644 src/util/regexp.i

diff --git a/src/cvc4.i b/src/cvc4.i
index da15d4b5d..52c4f4ea7 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -266,6 +266,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "util/datatype.i"
 %include "util/tuple.i"
 %include "util/record.i"
+%include "util/regexp.i"
 %include "util/uninterpreted_constant.i"
 
 %include "expr/kind.i"
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 5647a2057..5b8da8828 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -143,7 +143,8 @@ EXTRA_DIST = \
 	hash.i \
 	predicate.i \
 	uninterpreted_constant.i \
-	chain.i
+	chain.i \
+	regexp.i
 
 DISTCLEANFILES = \
 	integer.h.tmp \
diff --git a/src/util/regexp.h b/src/util/regexp.h
index 85e827a8d..bcd569df0 100644
--- a/src/util/regexp.h
+++ b/src/util/regexp.h
@@ -219,13 +219,13 @@ public:
 
 namespace strings {
 
-struct StringHashFunction {
+struct CVC4_PUBLIC StringHashFunction {
   size_t operator()(const ::CVC4::String& s) const {
     return __gnu_cxx::hash<const char*>()(s.toString().c_str());
   }
 };/* struct StringHashFunction */
 
-}
+}/* CVC4::strings namespace */
 
 inline std::ostream& operator <<(std::ostream& os, const String& s) CVC4_PUBLIC;
 inline std::ostream& operator <<(std::ostream& os, const String& s) {
@@ -296,7 +296,7 @@ public:
     return d_str;
   }
 
-};/* class String */
+};/* class RegExp */
 
 /**
  * Hash function for the RegExp constants.
@@ -311,6 +311,7 @@ inline std::ostream& operator <<(std::ostream& os, const RegExp& s) CVC4_PUBLIC;
 inline std::ostream& operator <<(std::ostream& os, const RegExp& s) {
   return os << s.toString();
 }
+
 }/* CVC4 namespace */
 
-#endif /* __CVC4__STRING_H */
+#endif /* __CVC4__REGEXP_H */
diff --git a/src/util/regexp.i b/src/util/regexp.i
new file mode 100644
index 000000000..60765391d
--- /dev/null
+++ b/src/util/regexp.i
@@ -0,0 +1,33 @@
+%{
+#include "util/regexp.h"
+%}
+
+%rename(CVC4String) String;
+%rename(CVC4StringHashFunction) CVC4::strings::StringHashFunction;
+
+%ignore CVC4::String::String(const std::string&);
+
+%rename(assign) CVC4::String::operator=(const String&);
+%rename(getChar) CVC4::String::operator[](const unsigned int) const;
+%rename(equals) CVC4::String::operator==(const String&) const;
+%ignore CVC4::String::operator!=(const String&) const;
+%rename(less) CVC4::String::operator<(const String&) const;
+%rename(lessEqual) CVC4::String::operator<=(const String&) const;
+%rename(greater) CVC4::String::operator>(const String&) const;
+%rename(greaterEqual) CVC4::String::operator>=(const String&) const;
+
+%rename(assign) CVC4::RegExp::operator=(const RegExp&);
+%rename(equals) CVC4::RegExp::operator==(const RegExp&) const;
+%ignore CVC4::RegExp::operator!=(const RegExp&) const;
+%rename(less) CVC4::RegExp::operator<(const RegExp&) const;
+%rename(lessEqual) CVC4::RegExp::operator<=(const RegExp&) const;
+%rename(greater) CVC4::RegExp::operator>(const RegExp&) const;
+%rename(greaterEqual) CVC4::RegExp::operator>=(const RegExp&) const;
+
+%rename(apply) CVC4::strings::StringHashFunction::operator()(const ::CVC4::String&) const;
+%rename(apply) CVC4::RegExpHashFunction::operator()(const RegExp&) const;
+
+%ignore CVC4::operator<<(std::ostream&, const String&);
+%ignore CVC4::operator<<(std::ostream&, const RegExp&);
+
+%include "util/regexp.h"
-- 
2.30.2