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() throws Z3Exception
30  {
31  return Native.applyResultGetNumSubgoals(getContext().nCtx(),
32  getNativeObject());
33  }
34 
40  public Goal[] getSubgoals() throws Z3Exception
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) throws Z3Exception
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) throws Z3Exception
78  {
79  super(ctx, obj);
80  }
81 
82  void incRef(long o) throws Z3Exception
83  {
84  getContext().applyResult_DRQ().incAndClear(getContext(), o);
85  super.incRef(o);
86  }
87 
88  void decRef(long o) throws Z3Exception
89  {
90  getContext().applyResult_DRQ().add(o);
91  super.decRef(o);
92  }
93 }
Model convertModel(int i, Model m)
static int applyResultGetNumSubgoals(long a0, long a1)
Definition: Native.java:4120
static String applyResultToString(long a0, long a1)
Definition: Native.java:4111
static long applyResultConvertModel(long a0, long a1, int a2, long a3)
Definition: Native.java:4138
static long applyResultGetSubgoal(long a0, long a1, int a2)
Definition: Native.java:4129