Merge branch 'master' into bv-core

10 files changed, 134 insertions, 23 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 1952108f6..f95382cb1 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -119,11 +119,12 @@ EXTRA_DIST = \
 	bool.i \
 	sexpr.i \
 	datatype.i \
+	tuple.i \
+	record.i \
 	output.i \
 	cardinality.i \
 	result.i \
 	configuration.i \
-	cvc4_assert.i \
 	bitvector.i \
 	subrange_bound.i \
 	exception.i \
diff --git a/src/util/cvc4_assert.i b/src/util/cvc4_assert.i
deleted file mode 100644
index 45d76312d..000000000
--- a/src/util/cvc4_assert.i
+++ /dev/null
@@ -1,8 +0,0 @@
-%{
-#include "util/cvc4_assert.h"
-%}
-
-%rename(CVC4IllegalArgumentException) CVC4::IllegalArgumentException;
-%ignore CVC4::InternalErrorException::InternalErrorException(const char*, const char*, unsigned, const char*, ...);
-
-%include "util/cvc4_assert.h"
diff --git a/src/util/output.h b/src/util/output.h
index 477035a16..0b89980f2 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -570,7 +570,7 @@ public:
  * used for clearly separating different phases of an algorithm,
  * or iterations of a loop, or... etc.
  */
-class IndentedScope {
+class CVC4_PUBLIC IndentedScope {
   CVC4ostream d_out;
 public:
   inline IndentedScope(CVC4ostream out);
diff --git a/src/util/output.i b/src/util/output.i
index dc524e185..74953ba53 100644
--- a/src/util/output.i
+++ b/src/util/output.i
@@ -3,6 +3,7 @@
 %}
 
 %ignore CVC4::null_streambuf;
+%ignore std::streambuf;
 %feature("valuewrapper") std::ostream;
 
 // There are issues with SWIG's attempted wrapping of these variables when
@@ -10,13 +11,17 @@
 %ignore CVC4::null_sb;
 %ignore CVC4::null_os;
 %ignore CVC4::DumpOutC::dump_cout;
+%ignore CVC4::CVC4ostream;
 
 %ignore operator<<;
 %ignore on(std::string);
 %ignore isOn(std::string);
 %ignore off(std::string);
 %ignore printf(std::string, const char*, ...);
-%ignore operator()(std::string);
+
+%ignore CVC4::IndentedScope;
+%ignore CVC4::push(CVC4ostream&);
+%ignore CVC4::pop(CVC4ostream&);
 
 %ignore CVC4::ScopedDebug::ScopedDebug(std::string);
 %ignore CVC4::ScopedDebug::ScopedDebug(std::string, bool);
@@ -24,6 +29,22 @@
 %ignore CVC4::ScopedTrace::ScopedTrace(std::string);
 %ignore CVC4::ScopedTrace::ScopedTrace(std::string, bool);
 
+%ignore CVC4::WarningC::WarningC(std::ostream*);
+%ignore CVC4::MessageC::MessageC(std::ostream*);
+%ignore CVC4::NoticeC::NoticeC(std::ostream*);
+%ignore CVC4::ChatC::ChatC(std::ostream*);
+%ignore CVC4::TraceC::TraceC(std::ostream*);
+%ignore CVC4::DebugC::DebugC(std::ostream*);
+%ignore CVC4::DumpOutC::DumpOutC(std::ostream*);
+
+%ignore CVC4::WarningC::operator();
+%ignore CVC4::MessageC::operator();
+%ignore CVC4::NoticeC::operator();
+%ignore CVC4::ChatC::operator();
+%ignore CVC4::TraceC::operator();
+%ignore CVC4::DebugC::operator();
+%ignore CVC4::DumpOutC::operator();
+
 %ignore CVC4::WarningC::getStream();
 %ignore CVC4::MessageC::getStream();
 %ignore CVC4::NoticeC::getStream();
@@ -43,7 +64,7 @@
 %ignore operator std::ostream&;
 %ignore operator CVC4ostream;
 
-%rename(get) operator();
+%rename(get) operator ();
 %rename(ok) operator bool;
 
 %include "util/output.h"
diff --git a/src/util/record.i b/src/util/record.i
index f662178c2..2805d2fdf 100644
--- a/src/util/record.i
+++ b/src/util/record.i
@@ -1,5 +1,93 @@
 %{
 #include "util/record.h"
+
+#ifdef SWIGJAVA
+
+#include "bindings/java_iterator_adapter.h"
+#include "bindings/java_stream_adapters.h"
+
+#endif /* SWIGJAVA */
 %}
 
+%rename(equals) CVC4::RecordSelect::operator==(const RecordSelect&) const;
+%ignore CVC4::RecordSelect::operator!=(const RecordSelect&) const;
+
+%rename(equals) CVC4::RecordUpdate::operator==(const RecordUpdate&) const;
+%ignore CVC4::RecordUpdate::operator!=(const RecordUpdate&) const;
+
+%rename(equals) CVC4::Record::operator==(const Record&) const;
+%ignore CVC4::Record::operator!=(const Record&) const;
+%rename(getField) CVC4::Record::operator[](size_t) const;
+
+// These Object arrays are always of two elements, the first is a String and the second a
+// Type.  (On the C++ side, it is a std::pair<std::string, Type>.)
+%typemap(jni) std::pair<std::string, CVC4::Type> "jobjectArray";
+%typemap(jtype) std::pair<std::string, CVC4::Type> "java.lang.Object[]";
+%typemap(jstype) std::pair<std::string, CVC4::Type> "java.lang.Object[]";
+%typemap(javaout) std::pair<std::string, CVC4::Type> { return $jnicall; }
+%typemap(out) std::pair<std::string, CVC4::Type> {
+      $result = jenv->NewObjectArray(2, jenv->FindClass("java/lang/Object"), $null);
+      jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str()));
+      jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/Type");
+      jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
+      jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::Type($1.second)), true));
+    };
+
+#ifdef SWIGJAVA
+
+// Instead of Record::begin() and end(), create an
+// iterator() method on the Java side that returns a Java-style
+// Iterator.
+%ignore CVC4::Record::begin() const;
+%ignore CVC4::Record::end() const;
+%extend CVC4::Record {
+  CVC4::Type find(std::string name) const {
+    CVC4::Record::const_iterator i;
+    for(i = $self->begin(); i != $self->end(); ++i) {
+      if((*i).first == name) {
+        return (*i).second;
+      }
+    }
+    return CVC4::Type();
+  }
+
+  CVC4::JavaIteratorAdapter<CVC4::Record> iterator() {
+    return CVC4::JavaIteratorAdapter<CVC4::Record>(*$self);
+  }
+}
+
+// Record is "iterable" on the Java side
+%typemap(javainterfaces) CVC4::Record "java.lang.Iterable<Object[]>";
+
+// the JavaIteratorAdapter should not be public, and implements Iterator
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Record> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Record> "java.util.Iterator<Object[]>";
+// add some functions to the Java side (do it here because there's no way to do these in C++)
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::Record> "
+  public void remove() {
+    throw new java.lang.UnsupportedOperationException();
+  }
+
+  public Object[] next() {
+    if(hasNext()) {
+      return getNext();
+    } else {
+      throw new java.util.NoSuchElementException();
+    }
+  }
+"
+// getNext() just allows C++ iterator access from Java-side next(), make it private
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::Record>::getNext() "private";
+
+#endif /* SWIGJAVA */
+
 %include "util/record.h"
+
+#ifdef SWIGJAVA
+
+%include "bindings/java_iterator_adapter.h"
+%include "bindings/java_stream_adapters.h"
+
+%template(JavaIteratorAdapter_Record) CVC4::JavaIteratorAdapter<CVC4::Record>;
+
+#endif /* SWIGJAVA */
diff --git a/src/util/sexpr.h b/src/util/sexpr.h
index 135a83c7e..e9ea83aa1 100644
--- a/src/util/sexpr.h
+++ b/src/util/sexpr.h
@@ -37,6 +37,13 @@
 
 namespace CVC4 {
 
+class CVC4_PUBLIC SExprKeyword {
+  std::string d_str;
+public:
+  SExprKeyword(const std::string& s) : d_str(s) {}
+  const std::string& getString() const { return d_str; }
+};/* class SExpr::Keyword */
+
 /**
  * A simple S-expression. An S-expression is either an atom with a
  * string value, or a list of other S-expressions.
@@ -65,11 +72,7 @@ class CVC4_PUBLIC SExpr {
 
 public:
 
-  class CVC4_PUBLIC Keyword : protected std::string {
-  public:
-    Keyword(const std::string& s) : std::string(s) {}
-    const std::string& getString() const { return *this; }
-  };/* class SExpr::Keyword */
+  typedef SExprKeyword Keyword;
 
   SExpr() :
     d_sexprType(SEXPR_STRING),
diff --git a/src/util/sexpr.i b/src/util/sexpr.i
index 5d78142f3..4c89c5019 100644
--- a/src/util/sexpr.i
+++ b/src/util/sexpr.i
@@ -10,6 +10,11 @@
   std::string toString() const { return self->getValue(); }
 };/* CVC4::SExpr */
 
+%ignore CVC4::SExpr::SExpr(int);
+%ignore CVC4::SExpr::SExpr(unsigned int);
+%ignore CVC4::SExpr::SExpr(unsigned long);
+%ignore CVC4::SExpr::SExpr(const char*);
+
 %rename(equals) CVC4::SExpr::operator==(const SExpr&) const;
 %ignore CVC4::SExpr::operator!=(const SExpr&) const;
 
diff --git a/src/util/statistics.i b/src/util/statistics.i
index 7f3bbe526..bd3a4eeb9 100644
--- a/src/util/statistics.i
+++ b/src/util/statistics.i
@@ -62,7 +62,7 @@
       jenv->SetObjectArrayElement($result, 0, jenv->NewStringUTF($1.first.c_str()));
       jclass clazz = jenv->FindClass("edu/nyu/acsys/CVC4/SExpr");
       jmethodID methodid = jenv->GetMethodID(clazz, "<init>", "(JZ)V");
-      jenv->SetObjectArrayElement($result, 1, jenv->NewObject(jenv->FindClass("edu/nyu/acsys/CVC4/SExpr"), methodid, reinterpret_cast<long>(new CVC4::SExpr($1.second)), true));
+      jenv->SetObjectArrayElement($result, 1, jenv->NewObject(clazz, methodid, reinterpret_cast<long>(new CVC4::SExpr($1.second)), true));
     };
 
 #endif /* SWIGJAVA */
diff --git a/src/util/tuple.i b/src/util/tuple.i
index d7301d201..f3de7b51b 100644
--- a/src/util/tuple.i
+++ b/src/util/tuple.i
@@ -2,4 +2,10 @@
 #include "util/tuple.h"
 %}
 
+%rename(equals) CVC4::TupleSelect::operator==(const TupleSelect&) const;
+%ignore CVC4::TupleSelect::operator!=(const TupleSelect&) const;
+
+%rename(equals) CVC4::TupleUpdate::operator==(const TupleUpdate&) const;
+%ignore CVC4::TupleUpdate::operator!=(const TupleUpdate&) const;
+
 %include "util/tuple.h"
diff --git a/src/util/util_model.i b/src/util/util_model.i
deleted file mode 100644
index 0d1b3bc81..000000000
--- a/src/util/util_model.i
+++ /dev/null
@@ -1,5 +0,0 @@
-%{
-#include "util/util_model.h"
-%}
-
-%include "util/util_model.h"