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.Context.getApplyResultDRQ
IDecRefQueue< ApplyResult > getApplyResultDRQ()
Definition: Context.java:4043
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
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.Native.applyResultToString
static String applyResultToString(long a0, long a1)
Definition: Native.java:4469
com.microsoft.z3.Native.applyResultGetNumSubgoals
static int applyResultGetNumSubgoals(long a0, long a1)
Definition: Native.java:4478
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3.ApplyResult
Definition: ApplyResult.java:24
com.microsoft.z3.ApplyResult.getSubgoals
Goal[] getSubgoals()
Definition: ApplyResult.java:39
com.microsoft.z3.Goal
Definition: Goal.java:26
com.microsoft.z3.Native.applyResultGetSubgoal
static long applyResultGetSubgoal(long a0, long a1, int a2)
Definition: Native.java:4487
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111