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
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
}
com.microsoft.z3.ApplyResult.convertModel
Model convertModel(int i, Model m)
Definition:
ApplyResult.java:56
com.microsoft.z3.Native.applyResultGetNumSubgoals
static int applyResultGetNumSubgoals(long a0, long a1)
Definition:
Native.java:4248
com.microsoft.z3.ApplyResult.toString
String toString()
Definition:
ApplyResult.java:66
com.microsoft.z3.Context
Definition:
Context.java:35
com.microsoft.z3.ApplyResult.getNumSubgoals
int getNumSubgoals()
Definition:
ApplyResult.java:28
com.microsoft.z3.ApplyResult.getSubgoals
Goal [] getSubgoals()
Definition:
ApplyResult.java:39
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition:
IDecRefQueue.java:56
com.microsoft.z3.Context.getApplyResultDRQ
IDecRefQueue< ApplyResult > getApplyResultDRQ()
Definition:
Context.java:3972
com.microsoft.z3.Goal
Definition:
Goal.java:26
com.microsoft.z3.Native.applyResultToString
static String applyResultToString(long a0, long a1)
Definition:
Native.java:4239
com.microsoft.z3.Native.applyResultConvertModel
static long applyResultConvertModel(long a0, long a1, int a2, long a3)
Definition:
Native.java:4266
com.microsoft.z3.Z3Object
Definition:
Z3Object.java:24
com.microsoft.z3.ApplyResult
Definition:
ApplyResult.java:24
com.microsoft.z3.Model
Definition:
Model.java:25
com.microsoft.z3.Native.applyResultGetSubgoal
static long applyResultGetSubgoal(long a0, long a1, int a2)
Definition:
Native.java:4257
z3py.String
def String(name, ctx=None)
Definition:
z3py.py:9821
Generated on Tue Aug 21 2018 11:47:59 for Z3 by
1.8.14