summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/expr.i46
-rw-r--r--src/expr/expr_manager.i2
-rw-r--r--src/expr/type.i45
-rw-r--r--src/smt/smt_engine.i2
4 files changed, 91 insertions, 4 deletions
diff --git a/src/expr/expr.i b/src/expr/expr.i
index 31788f06b..b50686f52 100644
--- a/src/expr/expr.i
+++ b/src/expr/expr.i
@@ -15,6 +15,50 @@
%rename(apply) CVC4::ExprHashFunction::operator()(CVC4::Expr) const;
#endif /* SWIGPYTHON */
+#ifdef SWIGJAVA
+%typemap(javabody) CVC4::Expr %{
+ private long swigCPtr;
+ protected boolean swigCMemOwn;
+
+ protected $javaclassname(long cPtr, boolean cMemoryOwn) {
+ swigCMemOwn = cMemoryOwn;
+ swigCPtr = cPtr;
+ this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+ }
+
+ protected static long getCPtr($javaclassname obj) {
+ return (obj == null) ? 0 : obj.swigCPtr;
+ }
+%}
+%javamethodmodifiers CVC4::Expr::operator=(const Expr&) "protected";
+%typemap(javacode) CVC4::Expr %{
+ // a ref is kept here to keep Java GC from collecting the ExprManager
+ // before the Expr
+ private Object em;
+
+ public Expr assign(Expr e) {
+ Expr r = assignInternal(e);
+ this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+ return r;
+ }
+%}
+%typemap(javaconstruct) Expr {
+ this($imcall, true);
+ this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+ }
+%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::Expr {
+ SmtEngine.dlRef(em);
+ em = null;
+ if (swigCPtr != 0) {
+ if (swigCMemOwn) {
+ swigCMemOwn = false;
+ CVC4JNI.delete_Expr(swigCPtr);
+ }
+ swigCPtr = 0;
+ }
+ }
+#endif /* SWIGJAVA */
+
%ignore CVC4::operator<<(std::ostream&, const Expr&);
%ignore CVC4::operator<<(std::ostream&, const TypeCheckingException&);
@@ -23,7 +67,7 @@
%ignore CVC4::expr::operator<<(std::ostream&, ExprDag);
%ignore CVC4::expr::operator<<(std::ostream&, ExprSetLanguage);
-%rename(assign) CVC4::Expr::operator=(const Expr&);
+%rename(assignInternal) CVC4::Expr::operator=(const Expr&);
%rename(equals) CVC4::Expr::operator==(const Expr&) const;
%ignore CVC4::Expr::operator!=(const Expr&) const;
%rename(less) CVC4::Expr::operator<(const Expr&) const;
diff --git a/src/expr/expr_manager.i b/src/expr/expr_manager.i
index b29f59621..fccadf43c 100644
--- a/src/expr/expr_manager.i
+++ b/src/expr/expr_manager.i
@@ -7,7 +7,7 @@
// before the ExprManager
private Object options;
%}
-%typemap(javaconstruct) CVC4::ExprManager {
+%typemap(javaconstruct) ExprManager {
this($imcall, true);
this.options = SmtEngine.mkRef(options); // keep ref to options in SWIG proxy class
}
diff --git a/src/expr/type.i b/src/expr/type.i
index 6394dda67..16d059eac 100644
--- a/src/expr/type.i
+++ b/src/expr/type.i
@@ -8,9 +8,52 @@
%rename(apply) CVC4::TypeHashFunction::operator()(const CVC4::Type&) const;
#endif /* SWIGPYTHON */
+#ifdef SWIGJAVA
+%typemap(javabody) CVC4::Type %{
+ private long swigCPtr;
+ protected boolean swigCMemOwn;
+
+ protected $javaclassname(long cPtr, boolean cMemoryOwn) {
+ swigCMemOwn = cMemoryOwn;
+ swigCPtr = cPtr;
+ this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+ }
+
+ protected static long getCPtr($javaclassname obj) {
+ return (obj == null) ? 0 : obj.swigCPtr;
+ }
+%}
+%javamethodmodifiers CVC4::Type::operator=(const Type&) "protected";
+%typemap(javacode) CVC4::Type %{
+ // a ref is kept here to keep Java GC from collecting the ExprManager
+ // before the Type
+ private Object em;
+
+ public Type assign(Type t) {
+ Type r = assignInternal(t);
+ this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+ return r;
+ }
+%}
+%typemap(javaconstruct) Type {
+ this($imcall, true);
+ this.em = SmtEngine.mkRef(getExprManager()); // keep ref to em in SWIG proxy class
+ }
+%typemap(javadestruct, methodname="delete", methodmodifiers="public synchronized") CVC4::Type {
+ SmtEngine.dlRef(em);
+ em = null;
+ if (swigCPtr != 0) {
+ if (swigCMemOwn) {
+ swigCMemOwn = false;
+ CVC4JNI.delete_Type(swigCPtr);
+ }
+ swigCPtr = 0;
+ }
+ }
+#endif /* SWIGJAVA */
%ignore CVC4::operator<<(std::ostream&, const Type&);
-%rename(assign) CVC4::Type::operator=(const Type&);
+%rename(assignInternal) CVC4::Type::operator=(const Type&);
%rename(equals) CVC4::Type::operator==(const Type&) const;
%ignore CVC4::Type::operator!=(const Type&) const;
%rename(less) CVC4::Type::operator<(const Type&) const;
diff --git a/src/smt/smt_engine.i b/src/smt/smt_engine.i
index 7bece21b3..9cf4467a8 100644
--- a/src/smt/smt_engine.i
+++ b/src/smt/smt_engine.i
@@ -27,7 +27,7 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEngine_dlRef(JNIEnv* jenv, jc
}
}
%}
-%typemap(javaconstruct) CVC4::SmtEngine {
+%typemap(javaconstruct) SmtEngine {
this($imcall, true);
emRef = mkRef(em); // keep ref to expr manager in SWIG proxy class
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback