1 files changed, 16 insertions, 34 deletions

diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index 635e593bb..95a5f4f3b 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -3,51 +3,33 @@
 %}
 
 #ifdef SWIGJAVA
+
 %typemap(javacode) CVC4::SmtEngine %{
   // a ref is kept here to keep Java GC from collecting the EM
   // before the SmtEngine
-  private Object emRef;
-  static final native Object mkRef(Object obj);
-  static final native void dlRef(Object obj);
+  private ExprManager em;
 %}
-%native (mkRef) jobject SmtEngine::mkRef(jobject);
-%native (dlRef) void SmtEngine::dlRef(jobject);
-%{
-extern "C" {
-SWIGEXPORT jobject JNICALL Java_edu_stanford_CVC4_SmtEngine_mkRef(JNIEnv* jenv, jclass jcls, jobject o) {
-  if(o == NULL) {
-    return NULL;
-  }
-  return jenv->NewGlobalRef(o);
+
+%typemap(javaconstruct) SmtEngine {
+  this($imcall, true);
+  this.em = em; // keep ref to expr manager in SWIG proxy class
 }
-SWIGEXPORT void JNICALL Java_edu_stanford_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jclass jcls, jobject o) {
-  if(o != NULL) {
-    jenv->DeleteGlobalRef(o);
-  }
+
+%typemap(javaout) CVC4::Expr {
+  return new Expr(this.em, $jnicall, true);
 }
+
+%typemap(javaout) CVC4::UnsatCore {
+  return new UnsatCore(this.em, $jnicall, true);
 }
-%}
-%typemap(javaconstruct) SmtEngine {
-    this($imcall, true);
-    emRef = mkRef(em); // keep ref to expr manager in SWIG proxy class
-  }
-%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::SmtEngine {
-    dlRef(emRef);
-    emRef = null;
-    if (swigCPtr != 0) {
-      if (swigCMemOwn) {
-        swigCMemOwn = false;
-        CVC4JNI.delete_SmtEngine(swigCPtr);
-      }
-      swigCPtr = 0;
-    }
-  }
-
-%template(Map_ExprExpr) std::map<CVC4::Expr, CVC4::Expr>;
+
+// %template(Map_ExprExpr) std::map<CVC4::Expr, CVC4::Expr>;
+%ignore CVC4::SmtEngine::getSynthSolutions(std::map<Expr, Expr>& sol_map);
 
 #endif // SWIGJAVA
 
 %ignore CVC4::SmtEngine::setLogic(const char*);
+%ignore CVC4::SmtEngine::setReplayStream(ExprStream* exprStream);
 %ignore CVC4::smt::currentProofManager();
 
 %include "smt/smt_engine.h"