Z3
ApplyResult.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
24public class ApplyResult extends Z3Object {
28 public int getNumSubgoals()
29 {
30 return Native.applyResultGetNumSubgoals(getContext().nCtx(),
31 getNativeObject());
32 }
33
39 public Goal[] getSubgoals()
40 {
41 int n = getNumSubgoals();
42 Goal[] res = new Goal[n];
43 for (int i = 0; i < n; i++)
44 res[i] = new Goal(getContext(),
45 Native.applyResultGetSubgoal(getContext().nCtx(), getNativeObject(), i));
46 return res;
47 }
48
52 @Override
53 public String toString() {
54 return Native.applyResultToString(getContext().nCtx(), getNativeObject());
55 }
56
57 ApplyResult(Context ctx, long obj)
58 {
59 super(ctx, obj);
60 }
61
62 @Override
63 void incRef() {
64 Native.applyResultIncRef(getContext().nCtx(), getNativeObject());
65 }
66
67 @Override
68 void addToReferenceQueue() {
69 getContext().getApplyResultDRQ().storeReference(getContext(), this);
70 }
71}
IDecRefQueue< ApplyResult > getApplyResultDRQ()
Definition: Context.java:4085
void storeReference(Context ctx, T obj)
def String(name, ctx=None)
Definition: z3py.py:10693