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.

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

getKind()

Z3_param_kind getKind ( Symbol  name )

inline

Retrieve kind of parameter.

Definition at line 39 of file ParamDescrs.java.

    {
 
        return Z3_param_kind.fromInt(Native.paramDescrsGetKind(
                getContext().nCtx(), getNativeObject(), name.getNativeObject()));
    }

getNames()

Symbol [] getNames ( )

inline

Retrieve all names of parameters.

Exceptions

Z3Exception

Definition at line 60 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;
    }

size()

int size ( )

inline

The size of the ParamDescrs.

Definition at line 75 of file ParamDescrs.java.

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

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.

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

validate()

void validate ( Params  p )

inline

validate a set of parameters.

Definition at line 29 of file ParamDescrs.java.

    {
 
        Native.paramsValidate(getContext().nCtx(), p.getNativeObject(),
                getNativeObject());
    }