Z3
src/api/java/ParamDescrs.java
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines