summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2013-11-27 17:37:30 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2013-11-27 17:37:30 -0500
commitb28a42c3a4fd8c9b079b157ad8ff36e581b60d29 (patch)
treebdd4097f09eb093c251ac662f3783980c807e325
parent7845fb33d5eda80bbe1149e302f7cf2f8f82bcdc (diff)
Java bindings improvements for CASCADE, minor cleanup.
-rw-r--r--src/cvc4.i1
-rw-r--r--src/util/Makefile.am3
-rw-r--r--src/util/regexp.h9
-rw-r--r--src/util/regexp.i33
4 files changed, 41 insertions, 5 deletions
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"
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback