Java bindings improvements for CASCADE, minor cleanup.

diff --git a/src/cvc4.i b/src/cvc4.i
index da15d4b5dd8efb760f4a6ca49e635b4ee715dfdc..52c4f4ea7c4009c276a863b851b1786c33a111e2 100644 (file)
--- 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 5647a20577bd7e3c4a5e87995b97d5d5fbfc4009..5b8da882845402da684e36008b36bd6dc9663286 100644 (file)
--- 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 85e827a8d3b4972ad30cce2c693f7ad05efb6969..bcd569df06073e58313267bfad39a2b4f322cfff 100644 (file)
--- 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 (file)
index 0000000..6076539
--- /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"