Z3
Data Structures | 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 27 of file ParamDescrs.java.

Member Function Documentation

◆ getDocumentation()

String getDocumentation ( Symbol  name)
inline

Retrieve documentation of parameter.

Definition at line 52 of file ParamDescrs.java.

53  {
54  return Native.paramDescrsGetDocumentation(getContext().nCtx(), getNativeObject(), name.getNativeObject());
55  }

◆ getKind()

Z3_param_kind getKind ( Symbol  name)
inline

Retrieve kind of parameter.

Definition at line 41 of file ParamDescrs.java.

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

◆ getNames()

Symbol [] getNames ( )
inline

Retrieve all names of parameters.

Exceptions
Z3Exception

Definition at line 62 of file ParamDescrs.java.

63  {
64  int sz = Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
65  Symbol[] names = new Symbol[sz];
66  for (int i = 0; i < sz; ++i)
67  {
68  names[i] = Symbol.create(getContext(), Native.paramDescrsGetName(
69  getContext().nCtx(), getNativeObject(), i));
70  }
71  return names;
72  }

◆ size()

int size ( )
inline

The size of the ParamDescrs.

Definition at line 77 of file ParamDescrs.java.

78  {
79  return Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
80  }

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 86 of file ParamDescrs.java.

86  {
87  return Native.paramDescrsToString(getContext().nCtx(), getNativeObject());
88  }

◆ validate()

void validate ( Params  p)
inline

validate a set of parameters.

Definition at line 31 of file ParamDescrs.java.

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