diff options
Diffstat (limited to 'src/proof/unsat_core.i')
-rw-r--r-- | src/proof/unsat_core.i | 61 |
1 files changed, 27 insertions, 34 deletions
diff --git a/src/proof/unsat_core.i b/src/proof/unsat_core.i index c37c8551d..780a75996 100644 --- a/src/proof/unsat_core.i +++ b/src/proof/unsat_core.i @@ -1,17 +1,37 @@ %{ #include "proof/unsat_core.h" +%} + +%ignore CVC4::operator<<(std::ostream&, const UnsatCore&); #ifdef SWIGJAVA -#include "bindings/java_iterator_adapter.h" -#include "bindings/java_stream_adapters.h" +%typemap(javabody) CVC4::UnsatCore %{ + private long swigCPtr; + protected boolean swigCMemOwn; + private ExprManager em; -#endif /* SWIGJAVA */ + protected $javaclassname(ExprManager em, long cPtr, boolean cMemoryOwn) { + swigCMemOwn = cMemoryOwn; + swigCPtr = cPtr; + this.em = em; + } + + protected static long getCPtr($javaclassname obj) { + return (obj == null) ? 0 : obj.swigCPtr; + } + + public JavaIteratorAdapter_UnsatCore iterator() { + return new JavaIteratorAdapter_UnsatCore(this.em, this); + } %} -%ignore CVC4::operator<<(std::ostream&, const UnsatCore&); +%typemap(javaout) CVC4::Expr { + return new Expr(this.em, $jnicall, true); +} -#ifdef SWIGJAVA +%ignore CVC4::UnsatCore::UnsatCore(); +%ignore CVC4::UnsatCore::UnsatCore(SmtEngine* smt, std::vector<Expr> core); // Instead of UnsatCore::begin() and end(), create an // iterator() method on the Java side that returns a Java-style @@ -20,12 +40,8 @@ %ignore CVC4::UnsatCore::end(); %ignore CVC4::UnsatCore::begin() const; %ignore CVC4::UnsatCore::end() const; -%extend CVC4::UnsatCore { - CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> iterator() - { - return CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr>(*$self); - } +%extend CVC4::UnsatCore { std::string toString() { std::stringstream ss; @@ -37,36 +53,13 @@ // UnsatCore is "iterable" on the Java side %typemap(javainterfaces) CVC4::UnsatCore "java.lang.Iterable<edu.stanford.CVC4.Expr>"; -// the JavaIteratorAdapter should not be public, and implements Iterator -%typemap(javaclassmodifiers) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> "class"; -%typemap(javainterfaces) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr> "java.util.Iterator<edu.stanford.CVC4.Expr>"; -// 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::UnsatCore, CVC4::Expr> " - public void remove() { - throw new java.lang.UnsupportedOperationException(); - } - - public edu.stanford.CVC4.Expr 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::UnsatCore, CVC4::Expr>::getNext() "private"; - #endif /* SWIGJAVA */ %include "proof/unsat_core.h" #ifdef SWIGJAVA -%include <std_vector.i> - -%include "bindings/java_iterator_adapter.h" - +SWIG_JAVA_ITERATOR_ADAPTER(CVC4::UnsatCore, CVC4::Expr) %template(JavaIteratorAdapter_UnsatCore) CVC4::JavaIteratorAdapter<CVC4::UnsatCore, CVC4::Expr>; #endif /* SWIGJAVA */ |