Z3
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 
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 }
Z3_param_kind getKind(Symbol name)
void storeReference(Context ctx, T obj)
String getDocumentation(Symbol name)
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params).
Definition: z3_api.h:1243
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
Definition: Context.java:3979
def String(name, ctx=None)
Definition: z3py.py:9443