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 
56  public Model convertModel(int i, Model m)
57  {
58  return new Model(getContext(),
59  Native.applyResultConvertModel(getContext().nCtx(), getNativeObject(), i, m.getNativeObject()));
60  }
61 
65  @Override
66  public String toString() {
67  return Native.applyResultToString(getContext().nCtx(), getNativeObject());
68  }
69 
70  ApplyResult(Context ctx, long obj)
71  {
72  super(ctx, obj);
73  }
74 
75  @Override
76  void incRef() {
77  Native.applyResultIncRef(getContext().nCtx(), getNativeObject());
78  }
79 
80  @Override
81  void addToReferenceQueue() {
82  getContext().getApplyResultDRQ().storeReference(getContext(), this);
83  }
84 }
Model convertModel(int i, Model m)
static int applyResultGetNumSubgoals(long a0, long a1)
Definition: Native.java:4105
static void applyResultIncRef(long a0, long a1)
Definition: Native.java:4080
void storeReference(Context ctx, T obj)
IDecRefQueue< ApplyResult > getApplyResultDRQ()
Definition: Context.java:3949
static String applyResultToString(long a0, long a1)
Definition: Native.java:4096
static long applyResultConvertModel(long a0, long a1, int a2, long a3)
Definition: Native.java:4123
static long applyResultGetSubgoal(long a0, long a1, int a2)
Definition: Native.java:4114
def String(name, ctx=None)
Definition: z3py.py:9443