Java datatype API fixups, datatype API examples

9 files changed, 194 insertions, 37 deletions

diff --git a/src/cvc4.i b/src/cvc4.i
index ec3aa43cb..aadbc374d 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -269,6 +269,7 @@ std::set<JavaInputStreamAdapter*> CVC4::JavaInputStreamAdapter::s_adapters;
 %include "util/record.i"
 %include "util/regexp.i"
 %include "util/uninterpreted_constant.i"
+%include "util/proof.i"
 
 %include "expr/kind.i"
 %include "expr/expr.i"
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 477eeeb99..d555ca529 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -253,7 +253,7 @@ public:
   virtual void printResolutions(std::ostream& out, std::ostream& paren) = 0;
 };/* class SatProof */
 
-class LFSCSatProof: public SatProof {
+class LFSCSatProof : public SatProof {
 private:
   void printResolution(ClauseId id, std::ostream& out, std::ostream& paren);
 public:
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 739299b7d..0a7772a4b 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -44,7 +44,7 @@ namespace CVC4 {
     void addDeclaration(Expr atom);
   };
 
-  class LFSCTheoryProof: public TheoryProof {
+  class LFSCTheoryProof : public TheoryProof {
     void printDeclarations(std::ostream& os, std::ostream& paren);
   public:
     static void printTerm(Expr term, std::ostream& os);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ec37eaf26..f26456cae 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2506,7 +2506,7 @@ void SmtEnginePrivate::doMiplibTrick() {
         const uint64_t mark = (*j).second;
         const unsigned numVars = pos.getKind() == kind::AND ? pos.getNumChildren() : 1;
         uint64_t expected = (uint64_t(1) << (1 << numVars)) - 1;
-        expected = (expected == 0) ? -1 : expected;// fix for overflow
+        expected = (expected == 0) ? -1 : expected; // fix for overflow
         Debug("miplib") << "[" << pos << "] => " << hex << mark << " expect " << expected << dec << endl;
         Assert(pos.getKind() == kind::AND || pos.isVar());
         if(mark != expected) {
@@ -2514,7 +2514,7 @@ void SmtEnginePrivate::doMiplibTrick() {
         } else {
           if(mark != 3) { // exclude single-var case; nothing to check there
             uint64_t sz = (uint64_t(1) << checks[pos_var].size()) - 1;
-            sz = (sz == 0) ? -1 : sz;// fix for overflow
+            sz = (sz == 0) ? -1 : sz; // fix for overflow
             Assert(sz == mark, "expected size %u == mark %u", sz, mark);
             for(size_t k = 0; k < checks[pos_var].size(); ++k) {
               if((k & (k - 1)) != 0) {
@@ -2534,12 +2534,12 @@ void SmtEnginePrivate::doMiplibTrick() {
                   break;
                 }
               } else {
-                Assert(checks[pos_var][k] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos.toString().c_str(), var.toString().c_str(), k, checks[pos_var][k].toString().c_str());// we never set for single-positive-var
+                Assert(checks[pos_var][k] == 0, "checks[(%s,%s)][%u] should be 0, but it's %s", pos.toString().c_str(), var.toString().c_str(), k, checks[pos_var][k].toString().c_str()); // we never set for single-positive-var
               }
             }
           }
           if(!eligible) {
-            eligible = true;// next is still eligible
+            eligible = true; // next is still eligible
             continue;
           }
 
@@ -2563,7 +2563,7 @@ void SmtEnginePrivate::doMiplibTrick() {
               Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
               d_assertionsToCheck.push_back(Rewriter::rewrite(geq.andNode(leq)));
               SubstitutionMap nullMap(&d_fakeContext);
-              Theory::PPAssertStatus status CVC4_UNUSED;// just for assertions
+              Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions
               status = d_smt.d_theoryEngine->solve(geq, nullMap);
               Assert(status == Theory::PP_ASSERT_STATUS_UNSOLVED,
                      "unexpected solution from arith's ppAssert()");
@@ -3493,7 +3493,7 @@ Expr SmtEngine::simplify(const Expr& ex) throw(TypeCheckingException, LogicExcep
 
   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
   if( options::typeChecking() ) {
-    e.getType(true);// ensure expr is type-checked at this point
+    e.getType(true); // ensure expr is type-checked at this point
   }
 
   // Make sure all preprocessing is done
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index ff4105241..00c332bd1 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -43,8 +43,8 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jc
   }
 
 %ignore CVC4::SmtEngine::setLogic(const char*);
-%ignore CVC4::SmtEngine::getProof;
 %ignore CVC4::stats::getStatisticsRegistry(SmtEngine*);
 %ignore CVC4::smt::beforeSearch(std::string, bool, SmtEngine*);
+%ignore CVC4::smt::currentProofManager();
 
 %include "smt/smt_engine.h"
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 5fa893336..8d70e4ffc 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -102,7 +102,7 @@ void Datatype::resolve(ExprManager* em,
   CheckArgument(&self.getDatatype() == this, resolutions, "Datatype::resolve(): resolutions doesn't contain me!");
   d_resolved = true;
   size_t index = 0;
-  for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
+  for(std::vector<DatatypeConstructor>::iterator i = d_constructors.begin(), i_end = d_constructors.end(); i != i_end; ++i) {
     (*i).resolve(em, self, resolutions, placeholders, replacements, paramTypes, paramReplacements);
     Node::fromExpr((*i).d_constructor).setAttribute(DatatypeIndexAttr(), index);
     Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++);
@@ -416,7 +416,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
   NodeManager* nm = NodeManager::fromExprManager(em);
   TypeNode selfTypeNode = TypeNode::fromType(self);
   size_t index = 0;
-  for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
+  for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) {
     if((*i).d_selector.isNull()) {
       // the unresolved type wasn't created here; do name resolution
       string typeName = (*i).d_name.substr((*i).d_name.find('\0') + 1);
@@ -461,7 +461,7 @@ void DatatypeConstructor::resolve(ExprManager* em, DatatypeType self,
   d_tester = nm->mkSkolem(getTesterName(), nm->mkTesterType(selfTypeNode), "is a tester", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
   d_constructor = nm->mkSkolem(getName(), nm->mkConstructorType(*this, selfTypeNode), "is a constructor", NodeManager::SKOLEM_EXACT_NAME | NodeManager::SKOLEM_NO_NOTIFY).toExpr();
   // associate constructor with all selectors
-  for(iterator i = begin(), i_end = end(); i != i_end; ++i) {
+  for(std::vector<DatatypeConstructorArg>::iterator i = d_args.begin(), i_end = d_args.end(); i != i_end; ++i) {
     (*i).d_constructor = d_constructor;
   }
 }
diff --git a/src/util/datatype.h b/src/util/datatype.h
index 802704803..99a303950 100644
--- a/src/util/datatype.h
+++ b/src/util/datatype.h
@@ -40,6 +40,47 @@ namespace CVC4 {
 
 class CVC4_PUBLIC ExprManager;
 
+class CVC4_PUBLIC DatatypeConstructor;
+class CVC4_PUBLIC DatatypeConstructorArg;
+
+class CVC4_PUBLIC DatatypeConstructorIterator {
+  const std::vector<DatatypeConstructor>* d_v;
+  size_t d_i;
+
+  friend class Datatype;
+
+  DatatypeConstructorIterator(const std::vector<DatatypeConstructor>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) {
+  }
+
+public:
+  typedef const DatatypeConstructor& value_type;
+  const DatatypeConstructor& operator*() const { return (*d_v)[d_i]; }
+  const DatatypeConstructor* operator->() const { return &(*d_v)[d_i]; }
+  DatatypeConstructorIterator& operator++() { ++d_i; return *this; }
+  DatatypeConstructorIterator operator++(int) { DatatypeConstructorIterator i(*this); ++d_i; return i; }
+  bool operator==(const DatatypeConstructorIterator& other) const { return d_v == other.d_v && d_i == other.d_i; }
+  bool operator!=(const DatatypeConstructorIterator& other) const { return d_v != other.d_v || d_i != other.d_i; }
+};/* class DatatypeConstructorIterator */
+
+class CVC4_PUBLIC DatatypeConstructorArgIterator {
+  const std::vector<DatatypeConstructorArg>* d_v;
+  size_t d_i;
+
+  friend class DatatypeConstructor;
+
+  DatatypeConstructorArgIterator(const std::vector<DatatypeConstructorArg>& v, bool start) : d_v(&v), d_i(start ? 0 : v.size()) {
+  }
+
+public:
+  typedef const DatatypeConstructorArg& value_type;
+  const DatatypeConstructorArg& operator*() const { return (*d_v)[d_i]; }
+  const DatatypeConstructorArg* operator->() const { return &(*d_v)[d_i]; }
+  DatatypeConstructorArgIterator& operator++() { ++d_i; return *this; }
+  DatatypeConstructorArgIterator operator++(int) { DatatypeConstructorArgIterator i(*this); ++d_i; return i; }
+  bool operator==(const DatatypeConstructorArgIterator& other) const { return d_v == other.d_v && d_i == other.d_i; }
+  bool operator!=(const DatatypeConstructorArgIterator& other) const { return d_v != other.d_v || d_i != other.d_i; }
+};/* class DatatypeConstructorArgIterator */
+
 /**
  * An exception that is thrown when a datatype resolution fails.
  */
@@ -134,9 +175,9 @@ class CVC4_PUBLIC DatatypeConstructor {
 public:
 
   /** The type for iterators over constructor arguments. */
-  typedef std::vector<DatatypeConstructorArg>::iterator iterator;
+  typedef DatatypeConstructorArgIterator iterator;
   /** The (const) type for iterators over constructor arguments. */
-  typedef std::vector<DatatypeConstructorArg>::const_iterator const_iterator;
+  typedef DatatypeConstructorArgIterator const_iterator;
 
 private:
 
@@ -394,9 +435,9 @@ public:
   static size_t indexOf(Expr item) CVC4_PUBLIC;
 
   /** The type for iterators over constructors. */
-  typedef std::vector<DatatypeConstructor>::iterator iterator;
+  typedef DatatypeConstructorIterator iterator;
   /** The (const) type for iterators over constructors. */
-  typedef std::vector<DatatypeConstructor>::const_iterator const_iterator;
+  typedef DatatypeConstructorIterator const_iterator;
 
 private:
   std::string d_name;
@@ -540,13 +581,13 @@ public:
   inline bool isResolved() const throw();
 
   /** Get the beginning iterator over DatatypeConstructors. */
-  inline std::vector<DatatypeConstructor>::iterator begin() throw();
+  inline iterator begin() throw();
   /** Get the ending iterator over DatatypeConstructors. */
-  inline std::vector<DatatypeConstructor>::iterator end() throw();
+  inline iterator end() throw();
   /** Get the beginning const_iterator over DatatypeConstructors. */
-  inline std::vector<DatatypeConstructor>::const_iterator begin() const throw();
+  inline const_iterator begin() const throw();
   /** Get the ending const_iterator over DatatypeConstructors. */
-  inline std::vector<DatatypeConstructor>::const_iterator end() const throw();
+  inline const_iterator end() const throw();
 
   /** Get the ith DatatypeConstructor. */
   const DatatypeConstructor& operator[](size_t index) const;
@@ -669,19 +710,19 @@ inline bool Datatype::isResolved() const throw() {
 }
 
 inline Datatype::iterator Datatype::begin() throw() {
-  return d_constructors.begin();
+  return iterator(d_constructors, true);
 }
 
 inline Datatype::iterator Datatype::end() throw() {
-  return d_constructors.end();
+  return iterator(d_constructors, false);
 }
 
 inline Datatype::const_iterator Datatype::begin() const throw() {
-  return d_constructors.begin();
+  return const_iterator(d_constructors, true);
 }
 
 inline Datatype::const_iterator Datatype::end() const throw() {
-  return d_constructors.end();
+  return const_iterator(d_constructors, false);
 }
 
 inline bool DatatypeConstructor::isResolved() const throw() {
@@ -710,19 +751,19 @@ inline bool DatatypeConstructorArg::isResolved() const throw() {
 }
 
 inline DatatypeConstructor::iterator DatatypeConstructor::begin() throw() {
-  return d_args.begin();
+  return iterator(d_args, true);
 }
 
 inline DatatypeConstructor::iterator DatatypeConstructor::end() throw() {
-  return d_args.end();
+  return iterator(d_args, false);
 }
 
 inline DatatypeConstructor::const_iterator DatatypeConstructor::begin() const throw() {
-  return d_args.begin();
+  return const_iterator(d_args, true);
 }
 
 inline DatatypeConstructor::const_iterator DatatypeConstructor::end() const throw() {
-  return d_args.end();
+  return const_iterator(d_args, false);
 }
 
 }/* CVC4 namespace */
diff --git a/src/util/datatype.i b/src/util/datatype.i
index c07caa805..403fb31bc 100644
--- a/src/util/datatype.i
+++ b/src/util/datatype.i
@@ -1,5 +1,12 @@
 %{
 #include "util/datatype.h"
+
+#ifdef SWIGJAVA
+
+#include "bindings/java_iterator_adapter.h"
+#include "bindings/java_stream_adapters.h"
+
+#endif /* SWIGJAVA */
 %}
 
 %extend std::vector< CVC4::Datatype > {
@@ -32,34 +39,137 @@
   %ignore set(int i, const CVC4::Datatype::Constructor& x);
   %ignore to_array();
 };
-%template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >;
+//%template(vectorDatatypeConstructor) std::vector< CVC4::DatatypeConstructor >;
 
 %rename(equals) CVC4::Datatype::operator==(const Datatype&) const;
 %ignore CVC4::Datatype::operator!=(const Datatype&) const;
 
-%rename(beginConst) CVC4::Datatype::begin() const;
-%rename(endConst) CVC4::Datatype::end() const;
+%ignore CVC4::Datatype::begin();
+%ignore CVC4::Datatype::end();
+%ignore CVC4::Datatype::begin() const;
+%ignore CVC4::Datatype::end() const;
 
-%rename(getConstructor) CVC4::Datatype::operator[](size_t) const;
-%ignore CVC4::Datatype::operator[](std::string) const;
+%rename(get) CVC4::Datatype::operator[](size_t) const;
+%rename(get) CVC4::Datatype::operator[](std::string) const;
 
 %rename(apply) CVC4::DatatypeHashFunction::operator()(const Datatype&) const;
 %ignore CVC4::DatatypeHashFunction::operator()(const Datatype*) const;
 %rename(apply) CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor&) const;
 %ignore CVC4::DatatypeHashFunction::operator()(const DatatypeConstructor*) const;
 
-%rename(beginConst) CVC4::DatatypeConstructor::begin() const;
-%rename(endConst) CVC4::DatatypeConstructor::end() const;
+%ignore CVC4::DatatypeConstructor::begin();
+%ignore CVC4::DatatypeConstructor::end();
+%ignore CVC4::DatatypeConstructor::begin() const;
+%ignore CVC4::DatatypeConstructor::end() const;
 
-%rename(getArg) CVC4::DatatypeConstructor::operator[](size_t) const;
-%rename(getArg) CVC4::DatatypeConstructor::operator[](std::string) const;
+%rename(get) CVC4::DatatypeConstructor::operator[](size_t) const;
+%rename(get) CVC4::DatatypeConstructor::operator[](std::string) const;
 
 %ignore CVC4::operator<<(std::ostream&, const Datatype&);
 %ignore CVC4::operator<<(std::ostream&, const DatatypeConstructor&);
 %ignore CVC4::operator<<(std::ostream&, const DatatypeConstructorArg&);
 
+%ignore CVC4::DatatypeConstructorIterator;
+%ignore CVC4::DatatypeConstructorArgIterator;
+
 %feature("valuewrapper") CVC4::DatatypeUnresolvedType;
 %feature("valuewrapper") CVC4::DatatypeConstructor;
 
+#ifdef SWIGJAVA
+
+// Instead of Datatype::begin() and end(), create an
+// iterator() method on the Java side that returns a Java-style
+// Iterator.
+%extend CVC4::Datatype {
+  CVC4::JavaIteratorAdapter<CVC4::Datatype> iterator() {
+    return CVC4::JavaIteratorAdapter<CVC4::Datatype>(*$self);
+  }
+
+  std::string toString() const {
+    std::stringstream ss;
+    ss << *$self;
+    return ss.str();
+  }
+}
+%extend CVC4::DatatypeConstructor {
+  CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> iterator() {
+    return CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>(*$self);
+  }
+
+  std::string toString() const {
+    std::stringstream ss;
+    ss << *$self;
+    return ss.str();
+  }
+}
+%extend CVC4::DatatypeConstructorArg {
+  std::string toString() const {
+    std::stringstream ss;
+    ss << *$self;
+    return ss.str();
+  }
+}
+
+// Datatype is "iterable" on the Java side
+%typemap(javainterfaces) CVC4::Datatype "java.lang.Iterable<DatatypeConstructor>";
+%typemap(javainterfaces) CVC4::DatatypeConstructor "java.lang.Iterable<DatatypeConstructorArg>";
+
+// the JavaIteratorAdapter should not be public, and implements Iterator
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::Datatype> "class";
+%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "class";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::Datatype> "java.util.Iterator<DatatypeConstructor>";
+%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "java.util.Iterator<DatatypeConstructorArg>";
+// 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::Datatype> "
+  public void remove() {
+    throw new java.lang.UnsupportedOperationException();
+  }
+
+  public DatatypeConstructor next() {
+    if(hasNext()) {
+      return getNext();
+    } else {
+      throw new java.util.NoSuchElementException();
+    }
+  }
+"
+%typemap(javacode) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor> "
+  public void remove() {
+    throw new java.lang.UnsupportedOperationException();
+  }
+
+  public DatatypeConstructorArg 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::Datatype>::getNext() "private";
+%javamethodmodifiers CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>::getNext() "private";
+
+// map the types appropriately.
+%typemap(jni) CVC4::Datatype::iterator::value_type "jobject";
+%typemap(jtype) CVC4::Datatype::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructor";
+%typemap(jstype) CVC4::Datatype::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructor";
+%typemap(javaout) CVC4::Datatype::iterator::value_type { return $jnicall; }
+%typemap(jni) CVC4::DatatypeConstructor::iterator::value_type "jobject";
+%typemap(jtype) CVC4::DatatypeConstructor::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructorArg";
+%typemap(jstype) CVC4::DatatypeConstructor::iterator::value_type "edu.nyu.acsys.CVC4.DatatypeConstructorArg";
+%typemap(javaout) CVC4::DatatypeConstructor::iterator::value_type { return $jnicall; }
+
+#endif /* SWIGJAVA */
+
 %include "util/datatype.h"
 
+#ifdef SWIGJAVA
+
+%include "bindings/java_iterator_adapter.h"
+%include "bindings/java_stream_adapters.h"
+
+%template(JavaIteratorAdapter_Datatype) CVC4::JavaIteratorAdapter<CVC4::Datatype>;
+%template(JavaIteratorAdapter_DatatypeConstructor) CVC4::JavaIteratorAdapter<CVC4::DatatypeConstructor>;
+
+#endif /* SWIGJAVA */
diff --git a/src/util/proof.i b/src/util/proof.i
new file mode 100644
index 000000000..22dff1043
--- /dev/null
+++ b/src/util/proof.i
@@ -0,0 +1,5 @@
+%{
+#include "util/proof.h"
+%}
+
+%include "util/proof.h"