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 }