Z3 |

ApplyResult.java
Go to the documentation of this file.
1
18 package com.microsoft.z3;
19
24 public 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}
com.microsoft.z3.ApplyResult
Definition: ApplyResult.java:24
com.microsoft.z3.ApplyResult.getSubgoals
Goal[] getSubgoals()
Definition: ApplyResult.java:39
com.microsoft.z3.ApplyResult.toString
String toString()
Definition: ApplyResult.java:53
com.microsoft.z3.ApplyResult.getNumSubgoals
int getNumSubgoals()
Definition: ApplyResult.java:28
com.microsoft.z3.Context
Definition: Context.java:36
com.microsoft.z3.Context.getApplyResultDRQ
IDecRefQueue< ApplyResult > getApplyResultDRQ()
Definition: Context.java:4085
com.microsoft.z3.Goal
Definition: Goal.java:26
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10693