Z3
src
api
java
ParamDescrs.java
Go to the documentation of this file.
1
18
package
com.microsoft.z3;
19
20
import
com
.
microsoft
.
z3
.
enumerations
.
Z3_param_kind
;
21
25
public
class
ParamDescrs
extends
Z3Object
{
29
public
void
validate
(
Params
p)
30
{
31
32
Native
.
paramsValidate
(getContext().nCtx(), p.getNativeObject(),
33
getNativeObject());
34
}
35
39
public
Z3_param_kind
getKind
(
Symbol
name)
40
{
41
42
return
Z3_param_kind
.
fromInt
(
Native
.
paramDescrsGetKind
(
43
getContext().nCtx(), getNativeObject(), name.getNativeObject()));
44
}
45
50
public
String
getDocumentation
(
Symbol
name)
51
{
52
return
Native
.
paramDescrsGetDocumentation
(getContext().nCtx(), getNativeObject(), name.getNativeObject());
53
}
54
60
public
Symbol
[]
getNames
()
61
{
62
int
sz =
Native
.
paramDescrsSize
(getContext().nCtx(), getNativeObject());
63
Symbol
[] names =
new
Symbol
[sz];
64
for
(
int
i = 0; i < sz; ++i)
65
{
66
names[i] =
Symbol
.create(getContext(),
Native
.
paramDescrsGetName
(
67
getContext().nCtx(), getNativeObject(), i));
68
}
69
return
names;
70
}
71
75
public
int
size
()
76
{
77
return
Native
.
paramDescrsSize
(getContext().nCtx(), getNativeObject());
78
}
79
83
@Override
84
public
String
toString
() {
85
return
Native
.
paramDescrsToString
(getContext().nCtx(), getNativeObject());
86
}
87
88
ParamDescrs
(
Context
ctx,
long
obj)
89
{
90
super(ctx, obj);
91
}
92
93
@Override
94
void
incRef() {
95
Native.paramDescrsIncRef(getContext().nCtx(), getNativeObject());
96
}
97
98
@Override
99
void
addToReferenceQueue() {
100
getContext().
getParamDescrsDRQ
().
storeReference
(getContext(),
this
);
101
}
102
}
com.microsoft.z3.Params
Definition:
Params.java:24
com.microsoft.z3.enumerations
Definition:
Z3_ast_kind.java:5
com.microsoft.z3.ParamDescrs.getKind
Z3_param_kind getKind(Symbol name)
Definition:
ParamDescrs.java:39
com.microsoft.z3.ParamDescrs.validate
void validate(Params p)
Definition:
ParamDescrs.java:29
com.microsoft.z3.Native.paramDescrsGetDocumentation
static String paramDescrsGetDocumentation(long a0, long a1, long a2)
Definition:
Native.java:909
com.microsoft.z3.enumerations.Z3_param_kind
Definition:
Z3_param_kind.java:13
com.microsoft.z3.Native.paramDescrsGetKind
static int paramDescrsGetKind(long a0, long a1, long a2)
Definition:
Native.java:882
com.microsoft.z3.enumerations.Z3_param_kind.fromInt
static final Z3_param_kind fromInt(int v)
Definition:
Z3_param_kind.java:38
com.microsoft
com.microsoft.z3.Native.paramsValidate
static void paramsValidate(long a0, long a1, long a2)
Definition:
Native.java:858
com.microsoft.z3.Context.getParamDescrsDRQ
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
Definition:
Context.java:4073
com.microsoft.z3.ParamDescrs
Definition:
ParamDescrs.java:25
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition:
IDecRefQueue.java:56
com.microsoft.z3.ParamDescrs.getDocumentation
String getDocumentation(Symbol name)
Definition:
ParamDescrs.java:50
com.microsoft.z3.Native.paramDescrsSize
static int paramDescrsSize(long a0, long a1)
Definition:
Native.java:891
com.microsoft.z3.ParamDescrs.size
int size()
Definition:
ParamDescrs.java:75
com.microsoft.z3.Native.paramDescrsGetName
static long paramDescrsGetName(long a0, long a1, int a2)
Definition:
Native.java:900
com.microsoft.z3.ParamDescrs.getNames
Symbol[] getNames()
Definition:
ParamDescrs.java:60
com.microsoft.z3.Symbol
Definition:
Symbol.java:25
com.microsoft.z3.Native
Definition:
Native.java:4
com.microsoft.z3
Definition:
AlgebraicNum.java:18
com.microsoft.z3.Native.paramDescrsToString
static String paramDescrsToString(long a0, long a1)
Definition:
Native.java:918
com
com.microsoft.z3.Context
Definition:
Context.java:35
com.microsoft.z3.ParamDescrs.toString
String toString()
Definition:
ParamDescrs.java:84
com.microsoft.z3.Z3Object
Definition:
Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition:
z3py.py:10111
Generated on Sat May 9 2020 00:00:00 for Z3 by
1.8.17