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;
21 using System.Diagnostics.Contracts;
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 Symbol[] Names
53  {
54  get
55  {
56  uint sz = Native.Z3_param_descrs_size(Context.nCtx, NativeObject);
57  Symbol[] names = new Symbol[sz];
58  for (uint i = 0; i < sz; ++i) {
59  names[i] = Symbol.Create(Context, Native.Z3_param_descrs_get_name(Context.nCtx, NativeObject, i));
60  }
61  return names;
62  }
63  }
64 
68  public uint Size
69  {
70  get { return Native.Z3_param_descrs_size(Context.nCtx, NativeObject); }
71  }
72 
76  public override string ToString()
77  {
78  return Native.Z3_param_descrs_to_string(Context.nCtx, NativeObject);
79  }
80 
81  #region Internal
82  internal ParamDescrs(Context ctx, IntPtr obj)
83  : base(ctx, obj)
84  {
85  Contract.Requires(ctx != null);
86  }
87 
88  internal class DecRefQueue : IDecRefQueue
89  {
90  public DecRefQueue() : base() { }
91  public DecRefQueue(uint move_limit) : base(move_limit) { }
92  internal override void IncRef(Context ctx, IntPtr obj)
93  {
94  Native.Z3_param_descrs_inc_ref(ctx.nCtx, obj);
95  }
96 
97  internal override void DecRef(Context ctx, IntPtr obj)
98  {
99  Native.Z3_param_descrs_dec_ref(ctx.nCtx, obj);
100  }
101  };
102 
103  internal override void IncRef(IntPtr o)
104  {
105  Context.ParamDescrs_DRQ.IncAndClear(Context, o);
106  base.IncRef(o);
107  }
108 
109  internal override void DecRef(IntPtr o)
110  {
111  Context.ParamDescrs_DRQ.Add(o);
112  base.DecRef(o);
113  }
114  #endregion
115  }
116 }
static uint Z3_param_descrs_size(Z3_context a0, Z3_param_descrs a1)
Definition: Native.cs:2114
using System
Z3_param_kind
Z3_param_kind
static void Z3_param_descrs_dec_ref(Z3_context a0, Z3_param_descrs a1)
Definition: Native.cs:2099
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:76
static void Z3_param_descrs_inc_ref(Z3_context a0, Z3_param_descrs a1)
Definition: Native.cs:2092
static uint Z3_param_descrs_get_kind(Z3_context a0, Z3_param_descrs a1, IntPtr a2)
Definition: Native.cs:2106
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
static void Z3_params_validate(Z3_context a0, Z3_params a1, Z3_param_descrs a2)
Definition: Native.cs:2085
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:31
IDecRefQueue ParamDescrs_DRQ
ParamDescrs DRQ
Definition: Context.cs:4509
static string Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1)
Definition: Native.cs:2130
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
Z3_param_kind GetKind(Symbol name)
Retrieve kind of parameter.
Definition: ParamDescrs.cs:43
static IntPtr Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, uint a2)
Definition: Native.cs:2122
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30