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());
    }