Z3
src
api
java
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:4467
com.microsoft.z3.Native.applyResultGetNumSubgoals
static int applyResultGetNumSubgoals(long a0, long a1)
Definition:
Native.java:4476
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:4485
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:10085
Generated on Thu Feb 27 2020 00:00:00 for Z3 by
1.8.17