Z3
ParamDescrs.java
Go to the documentation of this file.
1
18package com.microsoft.z3;
19
20import com.microsoft.z3.enumerations.Z3_param_kind;
21
25public class ParamDescrs extends Z3Object {
29 public void validate(Params p)
30 {
31
32 Native.paramsValidate(getContext().nCtx(), p.getNativeObject(),
33 getNativeObject());
34 }
35
40 {
41
42 return Z3_param_kind.fromInt(Native.paramDescrsGetKind(
43 getContext().nCtx(), getNativeObject(), name.getNativeObject()));
44 }
45
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}
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
Definition: Context.java:4115
void storeReference(Context ctx, T obj)
String getDocumentation(Symbol name)
Z3_param_kind getKind(Symbol name)
def String(name, ctx=None)
Definition: z3py.py:10693
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params).
Definition: z3_api.h:1317