Go to the documentation of this file.00001
00018 package com.microsoft.z3;
00019
00020 import com.microsoft.z3.enumerations.Z3_param_kind;
00021
00025 public class ParamDescrs extends Z3Object
00026 {
00030 public void validate(Params p) throws Z3Exception
00031 {
00032
00033 Native.paramsValidate(getContext().nCtx(), p.getNativeObject(),
00034 getNativeObject());
00035 }
00036
00040 public Z3_param_kind getKind(Symbol name) throws Z3Exception
00041 {
00042
00043 return Z3_param_kind.fromInt(Native.paramDescrsGetKind(
00044 getContext().nCtx(), getNativeObject(), name.getNativeObject()));
00045 }
00046
00052 public Symbol[] getNames() throws Z3Exception
00053 {
00054 int sz = Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
00055 Symbol[] names = new Symbol[sz];
00056 for (int i = 0; i < sz; ++i)
00057 {
00058 names[i] = Symbol.create(getContext(), Native.paramDescrsGetName(
00059 getContext().nCtx(), getNativeObject(), i));
00060 }
00061 return names;
00062 }
00063
00067 public int size() throws Z3Exception
00068 {
00069 return Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
00070 }
00071
00075 public String toString()
00076 {
00077 try
00078 {
00079 return Native.paramDescrsToString(getContext().nCtx(), getNativeObject());
00080 } catch (Z3Exception e)
00081 {
00082 return "Z3Exception: " + e.getMessage();
00083 }
00084 }
00085
00086 ParamDescrs(Context ctx, long obj) throws Z3Exception
00087 {
00088 super(ctx, obj);
00089 }
00090
00091 void incRef(long o) throws Z3Exception
00092 {
00093 getContext().paramDescrs_DRQ().incAndClear(getContext(), o);
00094 super.incRef(o);
00095 }
00096
00097 void decRef(long o) throws Z3Exception
00098 {
00099 getContext().paramDescrs_DRQ().add(o);
00100 super.decRef(o);
00101 }
00102 }