Z3
Params.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: Parameters
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 Params : Z3Object
30  {
34  public void Add(Symbol name, bool value)
35  {
36  Contract.Requires(name != null);
37 
38  Native.Z3_params_set_bool(Context.nCtx, NativeObject, name.NativeObject, (value) ? 1 : 0);
39  }
40 
44  public void Add(Symbol name, uint value)
45  {
46  Contract.Requires(name != null);
47 
48  Native.Z3_params_set_uint(Context.nCtx, NativeObject, name.NativeObject, value);
49  }
50 
54  public void Add(Symbol name, double value)
55  {
56  Contract.Requires(name != null);
57 
58  Native.Z3_params_set_double(Context.nCtx, NativeObject, name.NativeObject, value);
59  }
60 
64  public void Add(Symbol name, string value)
65  {
66  Contract.Requires(value != null);
67 
68  Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, Context.MkSymbol(value).NativeObject);
69  }
70 
74  public void Add(Symbol name, Symbol value)
75  {
76  Contract.Requires(name != null);
77  Contract.Requires(value != null);
78 
79  Native.Z3_params_set_symbol(Context.nCtx, NativeObject, name.NativeObject, value.NativeObject);
80  }
81 
82 
86  public void Add(string name, bool value)
87  {
88  Native.Z3_params_set_bool(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, (value) ? 1 : 0);
89  }
90 
94  public void Add(string name, uint value)
95  {
96  Native.Z3_params_set_uint(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
97  }
98 
102  public void Add(string name, double value)
103  {
104  Native.Z3_params_set_double(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value);
105  }
106 
110  public void Add(string name, Symbol value)
111  {
112  Contract.Requires(value != null);
113 
114  Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, value.NativeObject);
115  }
116 
120  public void Add(string name, string value)
121  {
122  Contract.Requires(name != null);
123  Contract.Requires(value != null);
124 
125  Native.Z3_params_set_symbol(Context.nCtx, NativeObject, Context.MkSymbol(name).NativeObject, Context.MkSymbol(value).NativeObject);
126  }
127 
131  public override string ToString()
132  {
133  return Native.Z3_params_to_string(Context.nCtx, NativeObject);
134  }
135 
136  #region Internal
137  internal Params(Context ctx)
138  : base(ctx, Native.Z3_mk_params(ctx.nCtx))
139  {
140  Contract.Requires(ctx != null);
141  }
142 
143  internal class DecRefQueue : IDecRefQueue
144  {
145  public DecRefQueue() : base() { }
146  public DecRefQueue(uint move_limit) : base(move_limit) { }
147  internal override void IncRef(Context ctx, IntPtr obj)
148  {
149  Native.Z3_params_inc_ref(ctx.nCtx, obj);
150  }
151 
152  internal override void DecRef(Context ctx, IntPtr obj)
153  {
154  Native.Z3_params_dec_ref(ctx.nCtx, obj);
155  }
156  };
157 
158  internal override void IncRef(IntPtr o)
159  {
160  Context.Params_DRQ.IncAndClear(Context, o);
161  base.IncRef(o);
162  }
163 
164  internal override void DecRef(IntPtr o)
165  {
166  Context.Params_DRQ.Add(o);
167  base.DecRef(o);
168  }
169  #endregion
170  }
171 }
static void Z3_params_set_uint(Z3_context a0, Z3_params a1, IntPtr a2, uint a3)
Definition: Native.cs:2056
void Add(string name, uint value)
Adds a parameter setting.
Definition: Params.cs:94
using System
void Add(Symbol name, bool value)
Adds a parameter setting.
Definition: Params.cs:34
IDecRefQueue Params_DRQ
Params DRQ
Definition: Context.cs:4504
void Add(string name, string value)
Adds a parameter setting.
Definition: Params.cs:120
void Add(Symbol name, string value)
Adds a parameter setting.
Definition: Params.cs:64
void Add(Symbol name, Symbol value)
Adds a parameter setting.
Definition: Params.cs:74
override string ToString()
A string representation of the parameter set.
Definition: Params.cs:131
void Add(string name, Symbol value)
Adds a parameter setting.
Definition: Params.cs:110
static string Z3_params_to_string(Z3_context a0, Z3_params a1)
Definition: Native.cs:2077
void Add(string name, bool value)
Adds a parameter setting.
Definition: Params.cs:86
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
void Add(Symbol name, double value)
Adds a parameter setting.
Definition: Params.cs:54
DecRefQueue interface
Definition: IDecRefQueue.cs:32
static void Z3_params_set_symbol(Z3_context a0, Z3_params a1, IntPtr a2, IntPtr a3)
Definition: Native.cs:2070
IntSymbol MkSymbol(int i)
Creates a new symbol using an integer.
Definition: Context.cs:84
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
static Z3_params Z3_mk_params(Z3_context a0)
Definition: Native.cs:2027
static void Z3_params_set_double(Z3_context a0, Z3_params a1, IntPtr a2, double a3)
Definition: Native.cs:2063
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
static void Z3_params_set_bool(Z3_context a0, Z3_params a1, IntPtr a2, int a3)
Definition: Native.cs:2049
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
void Add(Symbol name, uint value)
Adds a parameter setting.
Definition: Params.cs:44
static void Z3_params_inc_ref(Z3_context a0, Z3_params a1)
Definition: Native.cs:2035
void Add(string name, double value)
Adds a parameter setting.
Definition: Params.cs:102
static void Z3_params_dec_ref(Z3_context a0, Z3_params a1)
Definition: Native.cs:2042