Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
ParamDescrs Class Reference
+ Inheritance diagram for ParamDescrs:

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

Detailed Description

A ParamDescrs describes a set of parameters.

Definition at line 25 of file ParamDescrs.java.


Constructor & Destructor Documentation

ParamDescrs ( Context  ctx,
long  obj 
) throws Z3Exception [inline, package]

Definition at line 86 of file ParamDescrs.java.

    {
        super(ctx, obj);
    }

Member Function Documentation

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.

Exceptions:
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());
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines