Z3
src/api/java/ApplyResult.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00024 public class ApplyResult extends Z3Object
00025 {
00029     public int getNumSubgoals() throws Z3Exception
00030     {
00031         return Native.applyResultGetNumSubgoals(getContext().nCtx(),
00032                 getNativeObject());
00033     }
00034 
00040     public Goal[] getSubgoals() throws Z3Exception
00041     {
00042         int n = getNumSubgoals();
00043         Goal[] res = new Goal[n];
00044         for (int i = 0; i < n; i++)
00045             res[i] = new Goal(getContext(), 
00046                 Native.applyResultGetSubgoal(getContext().nCtx(), getNativeObject(), i));
00047         return res;
00048     }
00049 
00057     public Model convertModel(int i, Model m) throws Z3Exception
00058     {
00059         return new Model(getContext(), 
00060             Native.applyResultConvertModel(getContext().nCtx(), getNativeObject(), i, m.getNativeObject()));
00061     }
00062 
00066     public String toString()
00067     {
00068         try
00069         {
00070             return Native.applyResultToString(getContext().nCtx(), getNativeObject());
00071         } catch (Z3Exception e)
00072         {
00073             return "Z3Exception: " + e.getMessage();
00074         }
00075     }
00076 
00077     ApplyResult(Context ctx, long obj) throws Z3Exception
00078     {
00079         super(ctx, obj);
00080     }
00081 
00082     void incRef(long o) throws Z3Exception
00083     {
00084         getContext().applyResult_DRQ().incAndClear(getContext(), o);
00085         super.incRef(o);
00086     }
00087 
00088     void decRef(long o) throws Z3Exception
00089     {
00090         getContext().applyResult_DRQ().add(o);
00091         super.decRef(o);
00092     }
00093 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines