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
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
}
com.microsoft.z3.ApplyResult.convertModel
Model convertModel(int i, Model m)
Definition:
ApplyResult.java:57
com.microsoft.z3.Native.applyResultGetNumSubgoals
static int applyResultGetNumSubgoals(long a0, long a1)
Definition:
Native.java:4413
com.microsoft.z3.ApplyResult.toString
String toString()
Definition:
ApplyResult.java:66
com.microsoft.z3.Context.getApplyResultDRQ
IDecRefQueue getApplyResultDRQ()
Definition:
Context.java:3699
com.microsoft.z3.Context
Definition:
Context.java:27
com.microsoft.z3.ApplyResult.getNumSubgoals
int getNumSubgoals()
Definition:
ApplyResult.java:29
com.microsoft.z3.ApplyResult.getSubgoals
Goal[] getSubgoals()
Definition:
ApplyResult.java:40
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3.Goal
Definition:
Goal.java:26
com.microsoft.z3.IDecRefQueue.incAndClear
void incAndClear(Context ctx, long o)
Definition:
IDecRefQueue.java:44
com.microsoft.z3.Native.applyResultToString
static String applyResultToString(long a0, long a1)
Definition:
Native.java:4404
com.microsoft.z3.Native.applyResultConvertModel
static long applyResultConvertModel(long a0, long a1, int a2, long a3)
Definition:
Native.java:4431
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.Z3Exception
Definition:
Z3Exception.java:25
com.microsoft.z3.IDecRefQueue.add
void add(long o)
Definition:
IDecRefQueue.java:51
com.microsoft.z3.Native.applyResultGetSubgoal
static long applyResultGetSubgoal(long a0, long a1, int a2)
Definition:
Native.java:4422
Generated on Tue Jul 19 2016 21:26:48 for Z3 by
1.8.11