Z3
ApplyResult.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
24 public class ApplyResult extends Z3Object
25 {
29  public int getNumSubgoals()
30  {
31  return Native.applyResultGetNumSubgoals(getContext().nCtx(),
32  getNativeObject());
33  }
34 
40  public Goal[] getSubgoals()
41  {
42  int n = getNumSubgoals();
43  Goal[] res = new Goal[n];
44  for (int i = 0; i < n; i++)
45  res[i] = new Goal(getContext(),
46  Native.applyResultGetSubgoal(getContext().nCtx(), getNativeObject(), i));
47  return res;
48  }
49 
57  public Model convertModel(int i, Model m)
58  {
59  return new Model(getContext(),
60  Native.applyResultConvertModel(getContext().nCtx(), getNativeObject(), i, m.getNativeObject()));
61  }
62 
66  public String toString()
67  {
68  try
69  {
70  return Native.applyResultToString(getContext().nCtx(), getNativeObject());
71  } catch (Z3Exception e)
72  {
73  return "Z3Exception: " + e.getMessage();
74  }
75  }
76 
77  ApplyResult(Context ctx, long obj)
78  {
79  super(ctx, obj);
80  }
81 
82  void incRef(long o)
83  {
84  getContext().getApplyResultDRQ().incAndClear(getContext(), o);
85  super.incRef(o);
86  }
87 
88  void decRef(long o)
89  {
90  getContext().getApplyResultDRQ().add(o);
91  super.decRef(o);
92  }
93 }
Model convertModel(int i, Model m)
static int applyResultGetNumSubgoals(long a0, long a1)
Definition: Native.java:4413
IDecRefQueue getApplyResultDRQ()
Definition: Context.java:3699
void incAndClear(Context ctx, long o)
static String applyResultToString(long a0, long a1)
Definition: Native.java:4404
static long applyResultConvertModel(long a0, long a1, int a2, long a3)
Definition: Native.java:4431
static long applyResultGetSubgoal(long a0, long a1, int a2)
Definition: Native.java:4422