Z3 |

Public Member Functions
ParamDescrs Class Reference
Inheritance diagram for ParamDescrs:

## Public Member Functions
void | validate (Params p)
Z3_param_kind | getKind (Symbol name)
String | getDocumentation (Symbol name)
Symbol[] | getNames ()
int | size ()
String | toString ()

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

A ParamDescrs describes a set of parameters.

Definition at line 25 of file ParamDescrs.java.

## Member Function Documentation

## ◆ getDocumentation()

String getDocumentation | ( | Symbol | name | ) |
| inline

Retrieve documentation of parameter.

Definition at line 50 of file ParamDescrs.java.

51 {
52 return Native.paramDescrsGetDocumentation(getContext().nCtx(), getNativeObject(), name.getNativeObject());
53 }

## ◆ getKind()

Z3_param_kind getKind | ( | Symbol | name | ) |
| inline

Retrieve kind of parameter.

Definition at line 39 of file ParamDescrs.java.

40 {
41
42 return Z3_param_kind.fromInt(Native.paramDescrsGetKind(
43 getContext().nCtx(), getNativeObject(), name.getNativeObject()));
44 }
Z3_param_kind
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params).
Definition: z3_api.h:1317

## ◆ getNames()

Symbol[] getNames | ( |  | ) |
| inline

Retrieve all names of parameters.

Exceptions

  Z3Exception |

Definition at line 60 of file ParamDescrs.java.

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 }

## ◆ size()

int size | ( |  | ) |
| inline

The size of the ParamDescrs.

Definition at line 75 of file ParamDescrs.java.

76 {
77 return Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
78 }

Referenced by ParamDescrsRef.__len__(), Goal.__len__(), BitVecNumRef.as_signed_long(), and BitVecSortRef.subsort().

## ◆ toString()

String toString | ( |  | ) |
| inline

Retrieves a string representation of the ParamDescrs.

Definition at line 84 of file ParamDescrs.java.

84 {
85 return Native.paramDescrsToString(getContext().nCtx(), getNativeObject());
86 }

## ◆ validate()

void validate | ( | Params | p | ) |
| inline

validate a set of parameters.

Definition at line 29 of file ParamDescrs.java.

30 {
31
32 Native.paramsValidate(getContext().nCtx(), p.getNativeObject(),
33 getNativeObject());
34 }