00001 00018 package com.microsoft.z3; 00019 00024 public class Z3Object extends IDisposable 00025 { 00029 protected void finalize() throws Z3Exception 00030 { 00031 dispose(); 00032 } 00033 00037 public void dispose() throws Z3Exception 00038 { 00039 if (m_n_obj != 0) 00040 { 00041 decRef(m_n_obj); 00042 m_n_obj = 0; 00043 } 00044 00045 if (m_ctx != null) 00046 { 00047 m_ctx.m_refCount--; 00048 m_ctx = null; 00049 } 00050 } 00051 00052 private Context m_ctx = null; 00053 private long m_n_obj = 0; 00054 00055 Z3Object(Context ctx) 00056 { 00057 ctx.m_refCount++; 00058 m_ctx = ctx; 00059 } 00060 00061 Z3Object(Context ctx, long obj) throws Z3Exception 00062 { 00063 ctx.m_refCount++; 00064 m_ctx = ctx; 00065 incRef(obj); 00066 m_n_obj = obj; 00067 } 00068 00069 void incRef(long o) throws Z3Exception 00070 { 00071 } 00072 00073 void decRef(long o) throws Z3Exception 00074 { 00075 } 00076 00077 void checkNativeObject(long obj) throws Z3Exception 00078 { 00079 } 00080 00081 long getNativeObject() 00082 { 00083 return m_n_obj; 00084 } 00085 00086 void setNativeObject(long value) throws Z3Exception 00087 { 00088 if (value != 0) 00089 { 00090 checkNativeObject(value); 00091 incRef(value); 00092 } 00093 if (m_n_obj != 0) 00094 { 00095 decRef(m_n_obj); 00096 } 00097 m_n_obj = value; 00098 } 00099 00100 static long getNativeObject(Z3Object s) 00101 { 00102 if (s == null) 00103 return 0; 00104 return s.getNativeObject(); 00105 } 00106 00107 Context getContext() 00108 { 00109 return m_ctx; 00110 } 00111 00112 static long[] arrayToNative(Z3Object[] a) 00113 { 00114 if (a == null) 00115 return null; 00116 long[] an = new long[a.length]; 00117 for (int i = 0; i < a.length; i++) 00118 an[i] = (a[i] == null) ? 0 : a[i].getNativeObject(); 00119 return an; 00120 } 00121 00122 static int arrayLength(Z3Object[] a) 00123 { 00124 return (a == null) ? 0 : a.length; 00125 } 00126 }