Z3
ParamDescrs.java
Go to the documentation of this file.
1 
18 package com.microsoft.z3;
19 
21 
25 public class ParamDescrs extends Z3Object {
29  public void validate(Params p)
30  {
31 
32  Native.paramsValidate(getContext().nCtx(), p.getNativeObject(),
33  getNativeObject());
34  }
35 
40  {
41 
43  getContext().nCtx(), getNativeObject(), name.getNativeObject()));
44  }
45 
51  {
52  return Native.paramDescrsGetDocumentation(getContext().nCtx(), getNativeObject(), name.getNativeObject());
53  }
54 
60  public Symbol[] getNames()
61  {
62  int sz = Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
63  Symbol[] names = new Symbol[sz];
64  for (int i = 0; i < sz; ++i)
65  {
66  names[i] = Symbol.create(getContext(), Native.paramDescrsGetName(
67  getContext().nCtx(), getNativeObject(), i));
68  }
69  return names;
70  }
71 
75  public int size()
76  {
77  return Native.paramDescrsSize(getContext().nCtx(), getNativeObject());
78  }
79 
83  @Override
84  public String toString() {
85  return Native.paramDescrsToString(getContext().nCtx(), getNativeObject());
86  }
87 
88  ParamDescrs(Context ctx, long obj)
89  {
90  super(ctx, obj);
91  }
92 
93  @Override
94  void incRef() {
95  Native.paramDescrsIncRef(getContext().nCtx(), getNativeObject());
96  }
97 
98  @Override
99  void addToReferenceQueue() {
100  getContext().getParamDescrsDRQ().storeReference(getContext(), this);
101  }
102 }
com.microsoft.z3.Params
Definition: Params.java:24
com.microsoft.z3.enumerations
Definition: Z3_ast_kind.java:5
com.microsoft.z3.ParamDescrs.getKind
Z3_param_kind getKind(Symbol name)
Definition: ParamDescrs.java:39
com.microsoft.z3.ParamDescrs.validate
void validate(Params p)
Definition: ParamDescrs.java:29
com.microsoft.z3.Native.paramDescrsGetDocumentation
static String paramDescrsGetDocumentation(long a0, long a1, long a2)
Definition: Native.java:909
com.microsoft.z3.enumerations.Z3_param_kind
Definition: Z3_param_kind.java:13
com.microsoft.z3.Native.paramDescrsGetKind
static int paramDescrsGetKind(long a0, long a1, long a2)
Definition: Native.java:882
com.microsoft.z3.enumerations.Z3_param_kind.fromInt
static final Z3_param_kind fromInt(int v)
Definition: Z3_param_kind.java:38
com.microsoft
com.microsoft.z3.Native.paramsValidate
static void paramsValidate(long a0, long a1, long a2)
Definition: Native.java:858
com.microsoft.z3.Context.getParamDescrsDRQ
IDecRefQueue< ParamDescrs > getParamDescrsDRQ()
Definition: Context.java:4073
com.microsoft.z3.ParamDescrs
Definition: ParamDescrs.java:25
com.microsoft.z3.IDecRefQueue.storeReference
void storeReference(Context ctx, T obj)
Definition: IDecRefQueue.java:56
com.microsoft.z3.ParamDescrs.getDocumentation
String getDocumentation(Symbol name)
Definition: ParamDescrs.java:50
com.microsoft.z3.Native.paramDescrsSize
static int paramDescrsSize(long a0, long a1)
Definition: Native.java:891
com.microsoft.z3.ParamDescrs.size
int size()
Definition: ParamDescrs.java:75
com.microsoft.z3.Native.paramDescrsGetName
static long paramDescrsGetName(long a0, long a1, int a2)
Definition: Native.java:900
com.microsoft.z3.ParamDescrs.getNames
Symbol[] getNames()
Definition: ParamDescrs.java:60
com.microsoft.z3.Symbol
Definition: Symbol.java:25
com.microsoft.z3.Native
Definition: Native.java:4
com.microsoft.z3
Definition: AlgebraicNum.java:18
com.microsoft.z3.Native.paramDescrsToString
static String paramDescrsToString(long a0, long a1)
Definition: Native.java:918
com
com.microsoft.z3.Context
Definition: Context.java:35
com.microsoft.z3.ParamDescrs.toString
String toString()
Definition: ParamDescrs.java:84
com.microsoft.z3.Z3Object
Definition: Z3Object.java:24
z3py.String
def String(name, ctx=None)
Definition: z3py.py:10111