Public Member Functions | |
void | validate (Params p) throws Z3Exception |
Z3_param_kind | getKind (Symbol name) throws Z3Exception |
Symbol[] | getNames () throws Z3Exception |
int | size () throws Z3Exception |
String | toString () |
Package Functions | |
ParamDescrs (Context ctx, long obj) throws Z3Exception | |
void | incRef (long o) throws Z3Exception |
void | decRef (long o) throws Z3Exception |
A ParamDescrs describes a set of parameters.
Definition at line 25 of file ParamDescrs.java.
ParamDescrs | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 86 of file ParamDescrs.java.
{ super(ctx, obj); }
void decRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 97 of file ParamDescrs.java.
{ getContext().paramDescrs_DRQ().add(o); super.decRef(o); }
Z3_param_kind getKind | ( | Symbol | name | ) | throws Z3Exception [inline] |
Retrieve kind of parameter.
Definition at line 40 of file ParamDescrs.java.
{ return Z3_param_kind.fromInt(Native.paramDescrsGetKind( getContext().nCtx(), getNativeObject(), name.getNativeObject())); }
Symbol [] getNames | ( | ) | throws Z3Exception [inline] |
Retrieve all names of parameters.
Z3Exception |
Definition at line 52 of file ParamDescrs.java.
{ int sz = Native.paramDescrsSize(getContext().nCtx(), getNativeObject()); Symbol[] names = new Symbol[sz]; for (int i = 0; i < sz; ++i) { names[i] = Symbol.create(getContext(), Native.paramDescrsGetName( getContext().nCtx(), getNativeObject(), i)); } return names; }
void incRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 91 of file ParamDescrs.java.
{ getContext().paramDescrs_DRQ().incAndClear(getContext(), o); super.incRef(o); }
int size | ( | ) | throws Z3Exception [inline] |
The size of the ParamDescrs.
Definition at line 67 of file ParamDescrs.java.
{ return Native.paramDescrsSize(getContext().nCtx(), getNativeObject()); }
String toString | ( | ) | [inline] |
Retrieves a string representation of the ParamDescrs.
Definition at line 75 of file ParamDescrs.java.
{ try { return Native.paramDescrsToString(getContext().nCtx(), getNativeObject()); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }
void validate | ( | Params | p | ) | throws Z3Exception [inline] |
validate a set of parameters.
Definition at line 30 of file ParamDescrs.java.
{ Native.paramsValidate(getContext().nCtx(), p.getNativeObject(), getNativeObject()); }