Z3
ParamDescrs.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Parameter.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Parameter Descriptions
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-20
15 
16 Notes:
17 
18 --*/
19 
20 using System;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  public class ParamDescrs : Z3Object
30  {
34  public void Validate(Params p)
35  {
36  Contract.Requires(p != null);
37  Native.Z3_params_validate(Context.nCtx, p.NativeObject, NativeObject);
38  }
39 
44  {
45  Contract.Requires(name != null);
46  return (Z3_param_kind)Native.Z3_param_descrs_get_kind(Context.nCtx, NativeObject, name.NativeObject);
47  }
48 
52  public string GetDocumentation(Symbol name)
53  {
54  Contract.Requires(name != null);
55  return Native.Z3_param_descrs_get_documentation(Context.nCtx, NativeObject, name.NativeObject);
56  }
57 
61  public Symbol[] Names
62  {
63  get
64  {
65  uint sz = Native.Z3_param_descrs_size(Context.nCtx, NativeObject);
66  Symbol[] names = new Symbol[sz];
67  for (uint i = 0; i < sz; ++i) {
68  names[i] = Symbol.Create(Context, Native.Z3_param_descrs_get_name(Context.nCtx, NativeObject, i));
69  }
70  return names;
71  }
72  }
73 
77  public uint Size
78  {
79  get { return Native.Z3_param_descrs_size(Context.nCtx, NativeObject); }
80  }
81 
85  public override string ToString()
86  {
87  return Native.Z3_param_descrs_to_string(Context.nCtx, NativeObject);
88  }
89 
90  #region Internal
91  internal ParamDescrs(Context ctx, IntPtr obj)
92  : base(ctx, obj)
93  {
94  Contract.Requires(ctx != null);
95  }
96 
97  internal class DecRefQueue : IDecRefQueue
98  {
99  public DecRefQueue() : base() { }
100  public DecRefQueue(uint move_limit) : base(move_limit) { }
101  internal override void IncRef(Context ctx, IntPtr obj)
102  {
103  Native.Z3_param_descrs_inc_ref(ctx.nCtx, obj);
104  }
105 
106  internal override void DecRef(Context ctx, IntPtr obj)
107  {
108  Native.Z3_param_descrs_dec_ref(ctx.nCtx, obj);
109  }
110  };
111 
112  internal override void IncRef(IntPtr o)
113  {
114  Context.ParamDescrs_DRQ.IncAndClear(Context, o);
115  base.IncRef(o);
116  }
117 
118  internal override void DecRef(IntPtr o)
119  {
120  Context.ParamDescrs_DRQ.Add(o);
121  base.DecRef(o);
122  }
123  #endregion
124  }
125 }
void Validate(Params p)
validate a set of parameters.
Definition: ParamDescrs.cs:34
override string ToString()
Retrieves a string representation of the ParamDescrs.
Definition: ParamDescrs.cs:85
Z3_param_kind
The different kinds of parameters that can be associated with parameter sets. (see Z3_mk_params)...
Definition: z3_api.h:1243
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
DecRefQueue interface
Definition: IDecRefQueue.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
string GetDocumentation(Symbol name)
Retrieve documentation of parameter.
Definition: ParamDescrs.cs:52
IDecRefQueue ParamDescrs_DRQ
ParamDescrs DRQ
Definition: Context.cs:4928
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Z3_param_kind GetKind(Symbol name)
Retrieve kind of parameter.
Definition: ParamDescrs.cs:43
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30