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 }
static int applyResultGetNumSubgoals(long a0, long a1)
Definition: Native.java:4323
void storeReference(Context ctx, T obj)
IDecRefQueue< ApplyResult > getApplyResultDRQ()
Definition: Context.java:4041
static String applyResultToString(long a0, long a1)
Definition: Native.java:4314
static long applyResultGetSubgoal(long a0, long a1, int a2)
Definition: Native.java:4332
def String(name, ctx=None)
Definition: z3py.py:9972