Z3
ParamDescrs.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public class ParamDescrs extends Z3Object
26 {
30  public void validate(Params p) throws Z3Exception
31  {
32 
33  Native.paramsValidate(getContext().nCtx(), p.getNativeObject(),
34  getNativeObject());
35  }
36 
41  {
42 
44  getContext().nCtx(), getNativeObject(), name.getNativeObject()));
45  }
46 
52  public Symbol[] getNames() throws Z3Exception
53  {
54  int sz = Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
55  Symbol[] names = new Symbol[sz];
56  for (int i = 0; i < sz; ++i)
57  {
58  names[i] = Symbol.create(getContext(), Native.paramDescrsGetName(
59  getContext().nCtx(), getNativeObject(), i));
60  }
61  return names;
62  }
63 
67  public int size() throws Z3Exception
68  {
69  return Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
70  }
71 
75  public String toString()
76  {
77  try
78  {
79  return Native.paramDescrsToString(getContext().nCtx(), getNativeObject());
80  } catch (Z3Exception e)
81  {
82  return "Z3Exception: " + e.getMessage();
83  }
84  }
85 
86  ParamDescrs(Context ctx, long obj) throws Z3Exception
87  {
88  super(ctx, obj);
89  }
90 
91  void incRef(long o) throws Z3Exception
92  {
93  getContext().paramDescrs_DRQ().incAndClear(getContext(), o);
94  super.incRef(o);
95  }
96 
97  void decRef(long o) throws Z3Exception
98  {
99  getContext().paramDescrs_DRQ().add(o);
100  super.decRef(o);
101  }
102 }
static int paramDescrsGetKind(long a0, long a1, long a2)
Definition: Native.java:729
static void paramsValidate(long a0, long a1, long a2)
Definition: Native.java:705
Z3_param_kind getKind(Symbol name)
static String paramDescrsToString(long a0, long a1)
Definition: Native.java:756
static final Z3_param_kind fromInt(int v)
static int paramDescrsSize(long a0, long a1)
Definition: Native.java:738
static long paramDescrsGetName(long a0, long a1, int a2)
Definition: Native.java:747