Z3
src/api/java/Z3Object.java
Go to the documentation of this file.
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines